proposition: Lemma sum_of_gen_binom0 E n a: natp n -> cardinal E = n -> finite_int_fam a -> (csum a) ^c n = csumb (graphs_sum_eq (domain a) n) (fun p => (cardinal (partitions_pi p E)) *c (cprodb (domain a) (fun i=> ((Vg a i) ^c (Vg p i))))).
proof: Proof. move=> nN cEn fifa. set F:=csum a; set I := domain a. have sN:= (finite_sum_finite fifa). have cF: csum a = cardinal F by symmetry; apply: card_nat. have [pF] := (card_partitions1 fifa cF). move /partitions_piP => pipF. rewrite - {1} cEn cpowcr. pose g f i := (Vfi f (Vg pF i)). pose f1 f := (Lg I (fun i=> cardinal (g f i))). pose f2 f := Lg I (g f). have g_propP: forall f i, inc f (functions E F) -> inc i I -> forall x , inc x (g f i) <-> (inc x E /\ inc (Vf f x) (Vg pF i)). move=> f i /functionsP [ff sf tf] iI x; rewrite - sf; split. rewrite /g; aw; move /iim_fun_P => [u pa pb]. split; [ Wtac | rewrite - (Vf_pr ff pb) //]. move => [pa pb]; apply /iim_fun_P; ex_tac; apply: Vf_pr3 =>//. have prop0F:= (pip_prop0 pipF). have [da cVa [fga duja uea]] := pipF. have sfa: forall f, inc f (functions E F) -> unionb (Lg I (g f)) = E. move=> f fs; move: (fs) => /functionsP [ff sf tf]. rewrite - sf;set_extens t => ts. move /setUb_P: ts; aw; move => [y yI]; rewrite LgV//. by move /(g_propP _ _ fs yI) => []; rewrite sf. move: (Vf_target ff ts). rewrite tf -uea; move /setUb_P; rewrite da; move=> [y yda Vy]. apply /setUb_P;exists y => //;aw; trivial;rewrite LgV//; apply/ (g_propP _ _ fs yda). split=>//; ue. have sfb: forall f, inc f (functions E F) -> mutually_disjoint (Lg I (g f)). move=> f fs;apply: mutually_disjoint_prop2. move=> i j y iI jI / (g_propP _ _ fs iI) [yE W1]/(g_propP _ _ fs jI) [_ W2]. rewrite /I - da in iI jI; case: (duja i j iI jI) => // W; empty_tac1 (Vf f y). have sfc:forall f, inc f (functions E F) -> inc (f2 f) (partitions_pi (f1 f) E). move=> f fs; rewrite /f1/f2;apply /partitions_piP; hnf; saw. move => i iF; rewrite !LgV//. hnf. split; aww. have sfd: forall f, inc f (functions E F) -> inc (f1 f) (graphs_sum_eq I n). move=> f fs ; apply /(graphs_sum_eqP _ nN); rewrite /f1. rewrite - cEn -(sfa _ fs);saw; last first. - by hnf;aw; move => i itf; rewrite LgV//; fprops. - by fprops. - apply:Eqc_disjointU; fprops. split;fprops; rewrite /disjointU_fam; aw; trivial. by move => i idf; rewrite !LgV //; aw. set G:= Lg (graphs_sum_eq I n) (fun p => (Zo (functions E F) (fun f=> f1 f = p))). have g1: unionb G = (functions E F). rewrite /G;set_extens f. by move /setUb_P; aw;move=> [y ys]; rewrite LgV// => /Zo_S. move=> fsf;move: (sfd _ fsf) => fa; apply /setUb_P; aw; ex_tac. by rewrite LgV//;apply: Zo_i. have g2: mutually_disjoint G. rewrite /G;apply: mutually_disjoint_prop2. by move=> i j y ip jp /Zo_hi <- /Zo_hi <- . rewrite /f1/partitions_pi /partition_with_pi_elements. symmetry; rewrite /cpow -g1. apply: Eqc_disjointU; fprops. rewrite /disjointU_fam Lgd. hnf; aw;split; first by rewrite /G; aw. move => p pd; rewrite !LgV//. set X:= (partitions_pi p E). set Y := productb (Lg I (fun i=> (functions (Vg p i) (Vg pF i)))). transitivity (cardinal (X\times Y)). rewrite - (cardinal_indexed _ p). rewrite cprod2_pr1/cprod -/(partitions_pi p E) -/X; aw. apply: Eqc_setX; aw; trivial. rewrite /cprodb /cprod; aw; apply: Eqc_setXb; hnf ;aw;split;fprops. by move=> i iI;rewrite !LgV// double_cardinal -(cVa _ iI) -/(cpow _ _) cpowcl. set (Z:= (Zo (functions E F) (fun f => f1 f = p))). have phi1: forall f, inc f Z -> inc (f2 f) X. move=> f /Zo_P [fs f1f];rewrite /X -f1f; apply: sfc =>//. set WI:= fun f i => equipotent_ex (Vg p i) (g f i). have W1: forall f i, inc f Z -> inc i I -> bijection_prop (WI f i) (Vg p i) (g f i). move=> f i fZ iI; rewrite /WI; apply: equipotent_ex_pr1. by move: fZ => /Zo_P [fa fb]; rewrite -fb; rewrite /f1 LgV//;aw. have W2: forall f f' i, inc f Z -> inc f' Z-> inc i I -> f2 f = f2 f' -> WI f i = WI f' i. move=> f f' i fZ f'Z iI sf1; rewrite /WI. by move: (f_equal (Vg ^~i) sf1); rewrite /f2 !LgV //; move=> ->. set WJ:= fun f i => (restriction2 f (g f i) (Vg pF i)) \co (WI f i). have W3: forall f i, inc f Z -> inc i I -> [/\restriction2_axioms f (g f i) (Vg pF i) , function (restriction2 f (g f i) (Vg pF i)) & (restriction2 f (g f i) (Vg pF i)) \coP (WI f i)]. move=> f i fZ iI. have [bVf sVf tW] := (W1 _ _ fZ iI). move: fZ=> /Zo_P [feF f1f]. have g1P := (g_propP _ _ feF iI). move: feF => /functionsP [ff sf tf]. have sgi: sub (g f i) (source f) by rewrite sf; move=> t /g1P; case. have ra:restriction2_axioms f (g f i) (Vg pF i). split => //; first by rewrite tf; apply: prop0F; ue. by move=> t /(Vf_image_P ff sgi) [u /g1P [uE pr] ->]. have fr:= (proj31 (restriction2_prop ra)). by split => //; split => //; [ fct_tac | rewrite /restriction2;aw]. set f3:= fun f => (Lg I (WJ f)). have phi2: forall f, inc f Z -> inc (f3 f) Y. rewrite /f3; move=> f fZ; apply /setXb_P; aw; split;fprops => i iV. rewrite !LgV//. move: (W3 _ _ fZ iV)(W1 _ _ fZ iV) => [p1 p2 p3][p4 p5 p6]. rewrite /WJ; apply /functionsP. by saw; [ fct_tac | rewrite /restriction2; aw]. symmetry; apply/card_eqP. exists (Lf (fun f =>(J (f2 f) (f3 f))) Z (X \times Y)). hnf;aw;rewrite /G; saw; apply: lf_bijective. move=> f fZ; apply:setXp_i; fprops. move=> u v uZ vZ eq. move: (pr1_def eq)(pr2_def eq)=> sf2 sf3. move: (uZ) => /Zo_S usf. move: (uZ)(vZ) => /Zo_P [] /functionsP [fu su tu] f1u /Zo_P [] /functionsP [fv sv tv] f1v. apply: function_exten =>//; try ue. rewrite su -(sfa _ usf); move=> x /setUb_P; aw. move => [i iI]; rewrite LgV // => xgui. move: (f_equal (Vg ^~i) sf3); rewrite /f3 ! LgV// /WJ => eq2. move:(W2 _ _ _ uZ vZ iI sf2) => eq3. move: (W3 _ _ uZ iI)(W1 _ _ uZ iI) => [p1 p2 p3][p4 p5 p6]. move: (W3 _ _ vZ iI)(W1 _ _ vZ iI) => [p7 p8 p9][p10 p11 p12]. rewrite -p6 in xgui. move: p4 => [_ sW]; move: ((proj2 sW) _ xgui) => [y ys vy]. move: (f_equal (Vf ^~ y) eq2); rewrite ! compfV //; last by ue. rewrite (restriction2_V p1); last by rewrite - vy -p6. rewrite (restriction2_V p7); first by rewrite - eq3 vy. Wtac; [ fct_tac |by rewrite p11 -p5 ]. move=> y /setX_P [py Py Qy]. move: (Py) => /partitions_piP [dy cVy pfay]. move: (pfay) =>[fgy dujy uey]. move: (Qy) => /Zo_P; aw; move=> [_ [fgQ dQ Qv]]. move /(graphs_sum_eqP _ nN): (pd) => [fgp dp csp cVip]. set WK:= fun i => equipotent_ex (Vg p i) (Vg (P y) i). have W4: forall i, inc i I -> (bijection_prop (WK i) (Vg p i) (Vg (P y) i)). move=> i iI; apply: equipotent_ex_pr1; rewrite - cVy; aw; trivial; ue. pose hb i := (canonical_injection (Vg pF i) F) \co ((Vg (Q y) i) \co (inverse_fun (WK i))). have Hv:forall i, inc i I -> [/\ (Vg (Q y) i) \coP (inverse_fun (WK i)), function ( (Vg (Q y) i) \co (inverse_fun (WK i))) & (canonical_injection (Vg pF i) F) \coP ((Vg (Q y) i) \co (inverse_fun (WK i)))]. move=> i iI. move: (W4 _ iI)(Qv _ iI); rewrite LgV //; move => [bVf sw tW]. move /functionsP => [fVg sVg tV]. have p1: (Vg (Q y)i ) \coP (inverse_fun (WK i)). split => //; [ by apply: bijective_inv_f | aw; ue]. have p2:function ((Vg (Q y) i) \co (inverse_fun (WK i))) by fct_tac. split => //;split => //. apply: ci_f; apply: prop0F; ue. by rewrite /canonical_injection; aw. have Hw:forall i, inc i I -> function_prop (hb i) (Vg (P y) i) F. move=> i iI. move: (Hv _ iI) => [p1 p2 p3];rewrite /hb. hnf;rewrite compf_s compf_s compf_t. split; first (by fct_tac); last by rewrite /canonical_injection; aw. rewrite ifun_s; by move: (W4 _ iI); move => [bVf sw tW]. rewrite -fgp -dy in Hw. move: (extension_partition1 pfay Hw). set w := common_ext _ _ _;move => [[fw sw tw] alaw]. rewrite dy fgp in alaw. have wsf:inc w (functions E F) by apply /functionsP. have gp1: forall j x, inc j I -> inc x (Vg (P y) j) -> inc (Vf w x) (Vg pF j). move=> j x jI xV. move: (alaw _ jI) =>[p1 p2 p3]; rewrite (p3 _ xV). move: (Hv _ jI) => [p4 p5 p6]. move: (W4 _ jI) (Qv _ jI);rewrite LgV //; move => [awj sWj tWj]. move /functionsP => [fVj sVj tVj]. rewrite /hb; set aux := (Vg (Q y) j) \co _. have xsa: inc x (source aux) by rewrite /aux; aw; rewrite tWj. have xta: inc (Vf aux x) (Vg pF j). have <-:(target aux = Vg pF j) by rewrite /aux; aw. Wtac. rewrite compfV// ci_V //; apply: prop0F; ue. have gp2: forall i, inc i I -> g w i = Vg (P y) i. move => i iI; set_extens x. move /(g_propP _ _ wsf iI) => []; rewrite - uey; move /setUb_P. move=> [j]; rewrite dy fgp => jI xVj pa. have Wp':= (gp1 _ _ jI xVj). hnf in duja; rewrite da in duja; case: (duja _ _ iI jI) => h; try ue. empty_tac1 (Vf w x). move: (alaw _ iI)=> [p1 p2 p3] p4; apply /(g_propP _ _ wsf iI). split; [ by rewrite - sw; apply: p1 | by apply: gp1]. have wZ:inc w Z. apply: Zo_i => //. apply: fgraph_exten =>//;rewrite /f1; aww; try ue. move=> x xI /=; rewrite LgV //; rewrite gp2 //; apply: cVy; ue. ex_tac. have ->: (f2 w = P y). apply: fgraph_exten =>//;rewrite /f2; aww; try ue. move=> x xI /=; rewrite LgV //gp2 =>//. suff: (f3 w = Q y) by move=> ->; aw. apply: fgraph_exten =>//;rewrite /f3; aww; try ue. move => i iI; rewrite LgV//. move: (W4 _ iI)(Qv _ iI); rewrite LgV//; move => [bVf sVf tW]. move => /functionsP [fVg sVg tV]. have ww: (WI w i = WK i) by rewrite /WI /WK gp2 //. move: (W3 _ _ wZ iI); rewrite /WJ ww (gp2 _ iI); move => [ra rd cr]. apply: function_exten; [apply: compf_f =>//; aw; ue | exact fVg | aw; ue | | ]. aw; rewrite /restriction2; aw; ue. rewrite corresp_s => x xs. have fW: function (WK i) by fct_tac. have p1:inc (Vf (WK i)x ) (target (WK i)) by Wtac. move: (p1); rewrite tW => p11. rewrite compfV //restriction2_V //. move: (proj33 (alaw _ iI)); rewrite -tW => p3;rewrite (p3 _ p1) /hb. have p2: (Vg (Q y) i) \coP (inverse_fun (WK i)). split => //; [ by apply: bijective_inv_f | aw; ue]. have p0:function ((Vg (Q y) i) \co (inverse_fun (WK i))) by fct_tac. rewrite da in prop0F; move: (@prop0F i iI)=> pf0. have p4: (canonical_injection (Vg pF i) F) \coP ( (Vg (Q y) i) \co (inverse_fun (WK i))). by split;fprops;rewrite /canonical_injection; aw. rewrite !compfV//;aw; trivial. have <-: x = Vf (inverse_fun (WK i)) (Vf (WK i) x) by rewrite inverse_V2 =>//. by rewrite ci_V // -tV //; Wtac; rewrite sVg - sVf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)