proposition: Lemma infinite_prod3 X c (Y:= Lg (domain X) (fun z => \aleph (Vg X z))) (b:= omega0 ^o c): \0o <o c -> ofg_Mlt_lto X -> domain X = b -> (cprod Y) = (\csup (range Y)) ^c (cardinal b).
proof: Proof. move => cp ax db. have oc:= proj32_1 cp. have lb: limit_ordinal b by apply: indecomp_limit2. move: (lb); rewrite -db => lb1. move: (increasing_sup_limit4 ax lb1) (aleph_sum_pr6 ax lb1); rewrite -/Y. set a := \osup (range X); move=> [la sra sav] pa. move: ax => [gx ofx si]; rewrite sav. apply: cleA; first by apply : infinite_increasing_power_bound1. have pb: \aleph a <=c cprod Y. rewrite pa;apply:compare_sum_prod1 => //; rewrite /allf/Y; fprops. by aw; move=> i idx; rewrite LgV//; apply:infinite_ge2; apply: CIS_aleph;apply: ofx. move: (cpow_Mleeq (cardinal b) pb (aleph_nz (proj31 la))). rewrite db;move => h; apply: (cleT h); clear pa pb h. have dY: domain Y = b by rewrite /Y; aw. set f := Lg (coarse b) (fun z => Vg Y (P z)). have df: domain f = (coarse b) by rewrite /f; aw. have fgf: fgraph f by rewrite /f; fprops. have fgY: fgraph Y by rewrite /Y; fprops. have ->: cprod Y ^c cardinal b = cprod f. set g := Lg b (fun z => (singleton z) \times b). have pa: partition_w_fam g (domain f). split => //. rewrite /g; fprops. hnf;rewrite /g; aw;move => i j id jd; rewrite !LgV//. case: (equal_or_not i j) => ij; [ by left | right ]. apply: disjoint_pr => u /setX_P [_ p1 _] /setX_P [_ p2 _]. by case: ij; move: p1 p2 => /set1_P <- /set1_P <-. rewrite df /coarse /g; set_extens t. move /setUb_P; aw; move => [y yb]; rewrite LgV//; move => /setX_P [p1] /set1_P. move => p2 p3; apply /setX_P;split => //; ue. move => /setX_P [p1 p2 p3]; apply /setUb_P; aw; exists (P t) => //. rewrite LgV //;apply /setX_P;split;fprops. rewrite (cprod_An pa) (cpow_prod _ Y) dY /g; aw; congr cprod. apply: Lg_exten; move => x xb. set s:= ((singleton x) \times b). have xx: cardinal s = cardinal b. symmetry; apply /card_eqP; apply: Eq_rindexed. rewrite - xx cpowcr - cprod_of_same; rewrite LgV//; apply: cprodb_exten. move => v vd; aw; rewrite /f LgV//. by move: vd => /setX_P [_ /set1_P -> _]. move:vd => /setX_P [p1 /set1_P p2 p3]; apply /setX_P;split => //; ue. set g := Lg b (fun z => Zo (coarse b) (fun t => (P t) +#o (Q t) =z)). have pg: partition_w_fam g (domain f). split => //; rewrite /g /coarse/mutually_disjoint; aw. - fprops. - move => i j ib jb; case: (equal_or_not i j) => ij; [ by left | right ]. rewrite !LgV//;apply: disjoint_pr => u /Zo_hi p1 /Zo_hi p2; case: ij. by rewrite - p1 - p2. - rewrite df /coarse;set_extens t. by move /setUb_P; aw; move => [y yb]; rewrite LgV//; move => /Zo_P []. move: lb => [ob _ _] tb. move: (tb) => /setX_P [pt /(oltP ob) p1 /(oltP ob) p2]. have pa: inc (natural_sum (P t) (Q t)) b. by apply /(oltP ob); apply:natural_small. by apply /setUb_P; aw; ex_tac; rewrite LgV//;apply: Zo_i. rewrite (cprod_An pg). apply: cprod_increasing; [ by rewrite dY /g; aw | aw]. rewrite /g; aw => x xb; rewrite LgV//. move: (natural_finite_cover oc xb). rewrite - /b /coarse; set E:= Zo _ _; move => [pa pb]. have dr: domain (restr f E) = E. rewrite restr_d //; rewrite /E df; apply: Zo_S. have xd: inc x (domain X) by ue. have le1: forall i, inc i E -> Vg f i <=c Vg Y x. rewrite /f; move => i => /Zo_P [qa qb]; rewrite LgV//. move: qa => /setX_P [_ ipb iqb]. have op:= (Os_ordinal (proj31 lb) ipb). have oq := (Os_ordinal (proj31 lb) iqb). move: (ord_compare_nat_sum1 op oq); rewrite qb. case: (equal_or_not (P i) x) => eq1. rewrite eq1 => _; apply: cleR; rewrite /Y LgV//; apply CIS_aleph. by apply: ofx. have pd: inc (P i) (domain X) by ue. move => eq2; move: (proj1 (si _ _ pd xd (conj eq2 eq1))) => le2. by rewrite /Y !LgV//; apply: aleph_le_lec. have ix: infinite_c (Vg Y x). by rewrite /Y LgV//; apply: CIS_aleph; apply: ofx. rewrite - (cpow_inf ix pa pb) cpowcr - cprod_of_same LgV //. apply: cprod_increasing; aw; trivial => t tE. by rewrite LgV// LgV//; apply: le1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)