Metamath Proof Explorer

Theorem gsummpt2co

Description: Split a finite sum into a sum of a collection of sums over disjoint subsets. (Contributed by Thierry Arnoux, 27-Mar-2018)

Ref Expression
Hypotheses gsummpt2co.b ⊢B=BaseW
gsummpt2co.z ⊢0˙=0W
gsummpt2co.w ⊢φ→W∈CMnd
gsummpt2co.a ⊢φ→A∈Fin
gsummpt2co.e ⊢φ→E∈V
gsummpt2co.1 ⊢φ∧x∈A→C∈B
gsummpt2co.2 ⊢φ∧x∈A→D∈E
gsummpt2co.3 ⊢F=x∈A⟼D
Assertion gsummpt2co ⊢φ→∑Wx∈AC=∑Wy∈E∑Wx∈F-1yC

Proof

Step Hyp Ref Expression
1 gsummpt2co.b ⊢B=BaseW
2 gsummpt2co.z ⊢0˙=0W
3 gsummpt2co.w ⊢φ→W∈CMnd
4 gsummpt2co.a ⊢φ→A∈Fin
5 gsummpt2co.e ⊢φ→E∈V
6 gsummpt2co.1 ⊢φ∧x∈A→C∈B
7 gsummpt2co.2 ⊢φ∧x∈A→D∈E
8 gsummpt2co.3 ⊢F=x∈A⟼D
9 nfcsb1v ⊢Ⅎ_x⦋2nd⁡p/x⦌C
10 csbeq1a ⊢x=2nd⁡p→C=⦋2nd⁡p/x⦌C
11 ssidd ⊢φ→B⊆B
12 elcnv ⊢p∈F-1↔∃z∃xp=zx∧xFz
13 vex ⊢z∈V
14 vex ⊢x∈V
15 13 14 op2ndd ⊢p=zx→2nd⁡p=x
16 15 adantr ⊢p=zx∧xFz→2nd⁡p=x
17 8 dmmptss ⊢dom⁡F⊆A
18 14 13 breldm ⊢xFz→x∈dom⁡F
19 17 18 sselid ⊢xFz→x∈A
20 19 adantl ⊢p=zx∧xFz→x∈A
21 16 20 eqeltrd ⊢p=zx∧xFz→2nd⁡p∈A
22 21 exlimivv ⊢∃z∃xp=zx∧xFz→2nd⁡p∈A
23 12 22 sylbi ⊢p∈F-1→2nd⁡p∈A
24 23 adantl ⊢φ∧p∈F-1→2nd⁡p∈A
25 8 funmpt2 ⊢Fun⁡F
26 funcnvcnv ⊢Fun⁡F→Fun⁡F-1-1
27 25 26 ax-mp ⊢Fun⁡F-1-1
28 27 a1i ⊢φ∧x∈A→Fun⁡F-1-1
29 dfdm4 ⊢dom⁡F=ran⁡F-1
30 8 dmeqi ⊢dom⁡F=dom⁡x∈A⟼D
31 7 ralrimiva ⊢φ→∀x∈AD∈E
32 dmmptg ⊢∀x∈AD∈E→dom⁡x∈A⟼D=A
33 31 32 syl ⊢φ→dom⁡x∈A⟼D=A
34 30 33 eqtrid ⊢φ→dom⁡F=A
35 29 34 eqtr3id ⊢φ→ran⁡F-1=A
36 35 eleq2d ⊢φ→x∈ran⁡F-1↔x∈A
37 36 biimpar ⊢φ∧x∈A→x∈ran⁡F-1
38 relcnv ⊢Rel⁡F-1
39 fcnvgreu ⊢Rel⁡F-1∧Fun⁡F-1-1∧x∈ran⁡F-1→∃!p∈F-1x=2nd⁡p
40 38 39 mpanl1 ⊢Fun⁡F-1-1∧x∈ran⁡F-1→∃!p∈F-1x=2nd⁡p
41 28 37 40 syl2anc ⊢φ∧x∈A→∃!p∈F-1x=2nd⁡p
42 9 1 2 10 3 4 11 6 24 41 gsummptf1o ⊢φ→∑Wx∈AC=∑Wp∈F-1⦋2nd⁡p/x⦌C
43 8 rnmptss ⊢∀x∈AD∈E→ran⁡F⊆E
44 31 43 syl ⊢φ→ran⁡F⊆E
45 dfcnv2 ⊢ran⁡F⊆E→F-1=⋃z∈Ez×F-1z
46 44 45 syl ⊢φ→F-1=⋃z∈Ez×F-1z
47 46 mpteq1d ⊢φ→p∈F-1⟼⦋2nd⁡p/x⦌C=p∈⋃z∈Ez×F-1z⟼⦋2nd⁡p/x⦌C
48 nfcv ⊢Ⅎ_z⦋2nd⁡p/x⦌C
49 csbeq1 ⊢2nd⁡p=x→⦋2nd⁡p/x⦌C=⦋x/x⦌C
50 15 49 syl ⊢p=zx→⦋2nd⁡p/x⦌C=⦋x/x⦌C
51 csbid ⊢⦋x/x⦌C=C
52 50 51 eqtrdi ⊢p=zx→⦋2nd⁡p/x⦌C=C
53 48 9 52 mpomptxf ⊢p∈⋃z∈Ez×F-1z⟼⦋2nd⁡p/x⦌C=z∈E,x∈F-1z⟼C
54 47 53 eqtrdi ⊢φ→p∈F-1⟼⦋2nd⁡p/x⦌C=z∈E,x∈F-1z⟼C
55 54 oveq2d ⊢φ→∑Wp∈F-1⦋2nd⁡p/x⦌C=∑Wz∈E,x∈F-1z⟼C
56 mptfi ⊢A∈Fin→x∈A⟼D∈Fin
57 8 56 eqeltrid ⊢A∈Fin→F∈Fin
58 cnvfi ⊢F∈Fin→F-1∈Fin
59 4 57 58 3syl ⊢φ→F-1∈Fin
60 imaexg ⊢F-1∈Fin→F-1z∈V
61 59 60 syl ⊢φ→F-1z∈V
62 61 adantr ⊢φ∧z∈E→F-1z∈V
63 simpll ⊢φ∧z∈E∧x∈F-1z→φ
64 imassrn ⊢F-1z⊆ran⁡F-1
65 64 29 sseqtrri ⊢F-1z⊆dom⁡F
66 65 17 sstri ⊢F-1z⊆A
67 13 14 elimasn ⊢x∈F-1z↔zx∈F-1
68 67 biimpi ⊢x∈F-1z→zx∈F-1
69 68 adantl ⊢φ∧z∈E∧x∈F-1z→zx∈F-1
70 69 67 sylibr ⊢φ∧z∈E∧x∈F-1z→x∈F-1z
71 66 70 sselid ⊢φ∧z∈E∧x∈F-1z→x∈A
72 63 71 6 syl2anc ⊢φ∧z∈E∧x∈F-1z→C∈B
73 72 anasss ⊢φ∧z∈E∧x∈F-1z→C∈B
74 df-br ⊢zF-1x↔zx∈F-1
75 69 74 sylibr ⊢φ∧z∈E∧x∈F-1z→zF-1x
76 75 anasss ⊢φ∧z∈E∧x∈F-1z→zF-1x
77 76 pm2.24d ⊢φ∧z∈E∧x∈F-1z→¬zF-1x→C=0˙
78 77 imp ⊢φ∧z∈E∧x∈F-1z∧¬zF-1x→C=0˙
79 78 anasss ⊢φ∧z∈E∧x∈F-1z∧¬zF-1x→C=0˙
80 1 2 3 5 62 73 59 79 gsum2d2 ⊢φ→∑Wz∈E,x∈F-1z⟼C=∑Wz∈E∑Wx∈F-1zC
81 42 55 80 3eqtrd ⊢φ→∑Wx∈AC=∑Wz∈E∑Wx∈F-1zC
82 nfcv ⊢Ⅎ_z∑Wx∈F-1yC
83 nfcv ⊢Ⅎ_y∑Wx∈F-1zC
84 sneq ⊢y=z→y=z
85 84 imaeq2d ⊢y=z→F-1y=F-1z
86 85 mpteq1d ⊢y=z→x∈F-1y⟼C=x∈F-1z⟼C
87 86 oveq2d ⊢y=z→∑Wx∈F-1yC=∑Wx∈F-1zC
88 82 83 87 cbvmpt ⊢y∈E⟼∑Wx∈F-1yC=z∈E⟼∑Wx∈F-1zC
89 88 oveq2i ⊢∑Wy∈E∑Wx∈F-1yC=∑Wz∈E∑Wx∈F-1zC
90 81 89 eqtr4di ⊢φ→∑Wx∈AC=∑Wy∈E∑Wx∈F-1yC