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 sseldi 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 syl5eq φ dom F = A
35 29 34 syl5eqr φ 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 syl6eq 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 syl6eq φ 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 biimpi x F -1 z z x F -1
69 68 adantl φ z E x F -1 z z x F -1
70 69 67 sylibr φ z E x F -1 z x F -1 z
71 66 70 sseldi φ z E x F -1 z x A
72 63 71 6 syl2anc φ z E x F -1 z C B
73 72 anasss φ z E x F -1 z C B
74 df-br z F -1 x z x F -1
75 69 74 sylibr φ z E x F -1 z z F -1 x
76 75 anasss φ z E x F -1 z z F -1 x
77 76 pm2.24d φ z E x F -1 z ¬ z F -1 x C = 0 ˙
78 77 imp φ z E x F -1 z ¬ z F -1 x C = 0 ˙
79 78 anasss φ z E x F -1 z ¬ z F -1 x C = 0 ˙
80 1 2 3 5 62 73 59 79 gsum2d2 φ W z E , x F -1 z C = W z E W x F -1 z C
81 42 55 80 3eqtrd φ W x A C = W z E W x F -1 z C
82 nfcv _ z W x F -1 y C
83 nfcv _ y W x F -1 z C
84 sneq y = z y = z
85 84 imaeq2d y = z F -1 y = F -1 z
86 85 mpteq1d y = z x F -1 y C = x F -1 z C
87 86 oveq2d y = z W x F -1 y C = W x F -1 z C
88 82 83 87 cbvmpt y E W x F -1 y C = z E W x F -1 z C
89 88 oveq2i W y E W x F -1 y C = W z E W x F -1 z C
90 81 89 syl6eqr φ W x A C = W y E W x F -1 y C