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 = Base W
gsummpt2co.z ⊢ 0 ˙ = 0 W
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 ⊢ φ → ∑ W x ∈ A C = ∑ W y ∈ E ∑ W x ∈ F -1 y C

Proof

Step Hyp Ref Expression
1 gsummpt2co.b ⊢ B = Base W
2 gsummpt2co.z ⊢ 0 ˙ = 0 W
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 ⦋ 2 nd ⁡ p / x⦌ C
10 csbeq1a ⊢ x = 2 nd ⁡ p → C = ⦋ 2 nd ⁡ p / x⦌ C
11 ssidd ⊢ φ → B ⊆ B
12 elcnv ⊢ p ∈ F -1 ↔ ∃ z ∃ x p = z x ∧ x F z
13 vex ⊢ z ∈ V
14 vex ⊢ x ∈ V
15 13 14 op2ndd ⊢ p = z x → 2 nd ⁡ p = x
16 15 adantr ⊢ p = z x ∧ x F z → 2 nd ⁡ p = x
17 8 dmmptss ⊢ dom ⁡ F ⊆ A
18 14 13 breldm ⊢ x F z → x ∈ dom ⁡ F
19 17 18 sselid ⊢ x F z → x ∈ A
20 19 adantl ⊢ p = z x ∧ x F z → x ∈ A
21 16 20 eqeltrd ⊢ p = z x ∧ x F z → 2 nd ⁡ p ∈ A
22 21 exlimivv ⊢ ∃ z ∃ x p = z x ∧ x F z → 2 nd ⁡ p ∈ A
23 12 22 sylbi ⊢ p ∈ F -1 → 2 nd ⁡ p ∈ A
24 23 adantl ⊢ φ ∧ p ∈ F -1 → 2 nd ⁡ 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 ∈ A D ∈ E
32 dmmptg ⊢ ∀ x ∈ A D ∈ 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 -1 x = 2 nd ⁡ p
40 38 39 mpanl1 ⊢ Fun ⁡ F -1 -1 ∧ x ∈ ran ⁡ F -1 → ∃! p ∈ F -1 x = 2 nd ⁡ p
41 28 37 40 syl2anc ⊢ φ ∧ x ∈ A → ∃! p ∈ F -1 x = 2 nd ⁡ p
42 9 1 2 10 3 4 11 6 24 41 gsummptf1o ⊢ φ → ∑ W x ∈ A C = ∑ W p ∈ F -1 ⦋ 2 nd ⁡ p / x⦌ C
43 8 rnmptss ⊢ ∀ x ∈ A D ∈ E → ran ⁡ F ⊆ E
44 31 43 syl ⊢ φ → ran ⁡ F ⊆ E
45 dfcnv2 ⊢ ran ⁡ F ⊆ E → F -1 = ⋃ z ∈ E z × F -1 z
46 44 45 syl ⊢ φ → F -1 = ⋃ z ∈ E z × F -1 z
47 46 mpteq1d ⊢ φ → p ∈ F -1 ⟼ ⦋ 2 nd ⁡ p / x⦌ C = p ∈ ⋃ z ∈ E z × F -1 z ⟼ ⦋ 2 nd ⁡ p / x⦌ C
48 nfcv ⊢ Ⅎ _ z ⦋ 2 nd ⁡ p / x⦌ C
49 csbeq1 ⊢ 2 nd ⁡ p = x → ⦋ 2 nd ⁡ p / x⦌ C = ⦋ x / x⦌ C
50 15 49 syl ⊢ p = z x → ⦋ 2 nd ⁡ p / x⦌ C = ⦋ x / x⦌ C
51 csbid ⊢ ⦋ x / x⦌ C = C
52 50 51 eqtrdi ⊢ p = z x → ⦋ 2 nd ⁡ p / x⦌ C = C
53 48 9 52 mpomptxf ⊢ p ∈ ⋃ z ∈ E z × F -1 z ⟼ ⦋ 2 nd ⁡ p / x⦌ C = z ∈ E , x ∈ F -1 z ⟼ C
54 47 53 eqtrdi ⊢ φ → p ∈ F -1 ⟼ ⦋ 2 nd ⁡ p / x⦌ C = z ∈ E , x ∈ F -1 z ⟼ C
55 54 oveq2d ⊢ φ → ∑ W p ∈ F -1 ⦋ 2 nd ⁡ p / x⦌ C = ∑ W z ∈ E , x ∈ F -1 z ⟼ 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 -1 z ∈ V
61 59 60 syl ⊢ φ → F -1 z ∈ V
62 61 adantr ⊢ φ ∧ z ∈ E → F -1 z ∈ V
63 simpll ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z → φ
64 imassrn ⊢ F -1 z ⊆ ran ⁡ F -1
65 64 29 sseqtrri ⊢ F -1 z ⊆ dom ⁡ F
66 65 17 sstri ⊢ F -1 z ⊆ A
67 13 14 elimasn ⊢ x ∈ F -1 z ↔ z x ∈ F -1
68 67 bilani ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z → z x ∈ F -1
69 68 67 sylibr ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z → x ∈ F -1 z
70 66 69 sselid ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z → x ∈ A
71 63 70 6 syl2anc ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z → C ∈ B
72 71 anasss ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z → C ∈ B
73 df-br ⊢ z F -1 x ↔ z x ∈ F -1
74 68 73 sylibr ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z → z F -1 x
75 74 anasss ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z → z F -1 x
76 75 pm2.24d ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z → ¬ z F -1 x → C = 0 ˙
77 76 imp ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z ∧ ¬ z F -1 x → C = 0 ˙
78 77 anasss ⊢ φ ∧ z ∈ E ∧ x ∈ F -1 z ∧ ¬ z F -1 x → C = 0 ˙
79 1 2 3 5 62 72 59 78 gsum2d2 ⊢ φ → ∑ W z ∈ E , x ∈ F -1 z ⟼ C = ∑ W z ∈ E ∑ W x ∈ F -1 z C
80 42 55 79 3eqtrd ⊢ φ → ∑ W x ∈ A C = ∑ W z ∈ E ∑ W x ∈ F -1 z C
81 nfcv ⊢ Ⅎ _ z ∑ W x ∈ F -1 y C
82 nfcv ⊢ Ⅎ _ y ∑ W x ∈ F -1 z C
83 sneq ⊢ y = z → y = z
84 83 imaeq2d ⊢ y = z → F -1 y = F -1 z
85 84 mpteq1d ⊢ y = z → x ∈ F -1 y ⟼ C = x ∈ F -1 z ⟼ C
86 85 oveq2d ⊢ y = z → ∑ W x ∈ F -1 y C = ∑ W x ∈ F -1 z C
87 81 82 86 cbvmpt ⊢ y ∈ E ⟼ ∑ W x ∈ F -1 y C = z ∈ E ⟼ ∑ W x ∈ F -1 z C
88 87 oveq2i ⊢ ∑ W y ∈ E ∑ W x ∈ F -1 y C = ∑ W z ∈ E ∑ W x ∈ F -1 z C
89 80 88 eqtr4di ⊢ φ → ∑ W x ∈ A C = ∑ W y ∈ E ∑ W x ∈ F -1 y C