Metamath Proof Explorer


Theorem gsumzsplit

Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

Ref Expression
Hypotheses gsumzsplit.b B=BaseG
gsumzsplit.0 0˙=0G
gsumzsplit.p +˙=+G
gsumzsplit.z Z=CntzG
gsumzsplit.g φGMnd
gsumzsplit.a φAV
gsumzsplit.f φF:AB
gsumzsplit.c φranFZranF
gsumzsplit.w φfinSupp0˙F
gsumzsplit.i φCD=
gsumzsplit.u φA=CD
Assertion gsumzsplit φGF=GFC+˙GFD

Proof

Step Hyp Ref Expression
1 gsumzsplit.b B=BaseG
2 gsumzsplit.0 0˙=0G
3 gsumzsplit.p +˙=+G
4 gsumzsplit.z Z=CntzG
5 gsumzsplit.g φGMnd
6 gsumzsplit.a φAV
7 gsumzsplit.f φF:AB
8 gsumzsplit.c φranFZranF
9 gsumzsplit.w φfinSupp0˙F
10 gsumzsplit.i φCD=
11 gsumzsplit.u φA=CD
12 2 fvexi 0˙V
13 12 a1i φ0˙V
14 7 6 13 9 fsuppmptif φfinSupp0˙kAifkCFk0˙
15 7 6 13 9 fsuppmptif φfinSupp0˙kAifkDFk0˙
16 1 submacs GMndSubMndGACSB
17 acsmre SubMndGACSBSubMndGMooreB
18 5 16 17 3syl φSubMndGMooreB
19 7 frnd φranFB
20 eqid mrClsSubMndG=mrClsSubMndG
21 20 mrccl SubMndGMooreBranFBmrClsSubMndGranFSubMndG
22 18 19 21 syl2anc φmrClsSubMndGranFSubMndG
23 eqid G𝑠mrClsSubMndGranF=G𝑠mrClsSubMndGranF
24 4 20 23 cntzspan GMndranFZranFG𝑠mrClsSubMndGranFCMnd
25 5 8 24 syl2anc φG𝑠mrClsSubMndGranFCMnd
26 23 4 submcmn2 mrClsSubMndGranFSubMndGG𝑠mrClsSubMndGranFCMndmrClsSubMndGranFZmrClsSubMndGranF
27 22 26 syl φG𝑠mrClsSubMndGranFCMndmrClsSubMndGranFZmrClsSubMndGranF
28 25 27 mpbid φmrClsSubMndGranFZmrClsSubMndGranF
29 18 20 19 mrcssidd φranFmrClsSubMndGranF
30 29 adantr φkAranFmrClsSubMndGranF
31 7 ffnd φFFnA
32 fnfvelrn FFnAkAFkranF
33 31 32 sylan φkAFkranF
34 30 33 sseldd φkAFkmrClsSubMndGranF
35 2 subm0cl mrClsSubMndGranFSubMndG0˙mrClsSubMndGranF
36 22 35 syl φ0˙mrClsSubMndGranF
37 36 adantr φkA0˙mrClsSubMndGranF
38 34 37 ifcld φkAifkCFk0˙mrClsSubMndGranF
39 38 fmpttd φkAifkCFk0˙:AmrClsSubMndGranF
40 34 37 ifcld φkAifkDFk0˙mrClsSubMndGranF
41 40 fmpttd φkAifkDFk0˙:AmrClsSubMndGranF
42 1 2 3 4 5 6 14 15 22 28 39 41 gsumzadd φGkAifkCFk0˙+˙fkAifkDFk0˙=GkAifkCFk0˙+˙GkAifkDFk0˙
43 7 feqmptd φF=kAFk
44 iftrue kCifkCFk0˙=Fk
45 44 adantl φkAkCifkCFk0˙=Fk
46 noel ¬k
47 eleq2 CD=kCDk
48 46 47 mtbiri CD=¬kCD
49 10 48 syl φ¬kCD
50 49 adantr φkA¬kCD
51 elin kCDkCkD
52 50 51 sylnib φkA¬kCkD
53 imnan kC¬kD¬kCkD
54 52 53 sylibr φkAkC¬kD
55 54 imp φkAkC¬kD
56 55 iffalsed φkAkCifkDFk0˙=0˙
57 45 56 oveq12d φkAkCifkCFk0˙+˙ifkDFk0˙=Fk+˙0˙
58 7 ffvelrnda φkAFkB
59 1 3 2 mndrid GMndFkBFk+˙0˙=Fk
60 5 58 59 syl2an2r φkAFk+˙0˙=Fk
61 60 adantr φkAkCFk+˙0˙=Fk
62 57 61 eqtrd φkAkCifkCFk0˙+˙ifkDFk0˙=Fk
63 54 con2d φkAkD¬kC
64 63 imp φkAkD¬kC
65 64 iffalsed φkAkDifkCFk0˙=0˙
66 iftrue kDifkDFk0˙=Fk
67 66 adantl φkAkDifkDFk0˙=Fk
68 65 67 oveq12d φkAkDifkCFk0˙+˙ifkDFk0˙=0˙+˙Fk
69 1 3 2 mndlid GMndFkB0˙+˙Fk=Fk
70 5 58 69 syl2an2r φkA0˙+˙Fk=Fk
71 70 adantr φkAkD0˙+˙Fk=Fk
72 68 71 eqtrd φkAkDifkCFk0˙+˙ifkDFk0˙=Fk
73 11 eleq2d φkAkCD
74 elun kCDkCkD
75 73 74 bitrdi φkAkCkD
76 75 biimpa φkAkCkD
77 62 72 76 mpjaodan φkAifkCFk0˙+˙ifkDFk0˙=Fk
78 77 mpteq2dva φkAifkCFk0˙+˙ifkDFk0˙=kAFk
79 43 78 eqtr4d φF=kAifkCFk0˙+˙ifkDFk0˙
80 1 2 mndidcl GMnd0˙B
81 5 80 syl φ0˙B
82 81 adantr φkA0˙B
83 58 82 ifcld φkAifkCFk0˙B
84 58 82 ifcld φkAifkDFk0˙B
85 eqidd φkAifkCFk0˙=kAifkCFk0˙
86 eqidd φkAifkDFk0˙=kAifkDFk0˙
87 6 83 84 85 86 offval2 φkAifkCFk0˙+˙fkAifkDFk0˙=kAifkCFk0˙+˙ifkDFk0˙
88 79 87 eqtr4d φF=kAifkCFk0˙+˙fkAifkDFk0˙
89 88 oveq2d φGF=GkAifkCFk0˙+˙fkAifkDFk0˙
90 43 reseq1d φFC=kAFkC
91 ssun1 CCD
92 91 11 sseqtrrid φCA
93 44 mpteq2ia kCifkCFk0˙=kCFk
94 resmpt CAkAifkCFk0˙C=kCifkCFk0˙
95 resmpt CAkAFkC=kCFk
96 93 94 95 3eqtr4a CAkAifkCFk0˙C=kAFkC
97 92 96 syl φkAifkCFk0˙C=kAFkC
98 90 97 eqtr4d φFC=kAifkCFk0˙C
99 98 oveq2d φGFC=GkAifkCFk0˙C
100 83 fmpttd φkAifkCFk0˙:AB
101 39 frnd φrankAifkCFk0˙mrClsSubMndGranF
102 4 cntzidss mrClsSubMndGranFZmrClsSubMndGranFrankAifkCFk0˙mrClsSubMndGranFrankAifkCFk0˙ZrankAifkCFk0˙
103 28 101 102 syl2anc φrankAifkCFk0˙ZrankAifkCFk0˙
104 eldifn kAC¬kC
105 104 adantl φkAC¬kC
106 105 iffalsed φkACifkCFk0˙=0˙
107 106 6 suppss2 φkAifkCFk0˙supp0˙C
108 1 2 4 5 6 100 103 107 14 gsumzres φGkAifkCFk0˙C=GkAifkCFk0˙
109 99 108 eqtrd φGFC=GkAifkCFk0˙
110 43 reseq1d φFD=kAFkD
111 ssun2 DCD
112 111 11 sseqtrrid φDA
113 66 mpteq2ia kDifkDFk0˙=kDFk
114 resmpt DAkAifkDFk0˙D=kDifkDFk0˙
115 resmpt DAkAFkD=kDFk
116 113 114 115 3eqtr4a DAkAifkDFk0˙D=kAFkD
117 112 116 syl φkAifkDFk0˙D=kAFkD
118 110 117 eqtr4d φFD=kAifkDFk0˙D
119 118 oveq2d φGFD=GkAifkDFk0˙D
120 84 fmpttd φkAifkDFk0˙:AB
121 41 frnd φrankAifkDFk0˙mrClsSubMndGranF
122 4 cntzidss mrClsSubMndGranFZmrClsSubMndGranFrankAifkDFk0˙mrClsSubMndGranFrankAifkDFk0˙ZrankAifkDFk0˙
123 28 121 122 syl2anc φrankAifkDFk0˙ZrankAifkDFk0˙
124 eldifn kAD¬kD
125 124 adantl φkAD¬kD
126 125 iffalsed φkADifkDFk0˙=0˙
127 126 6 suppss2 φkAifkDFk0˙supp0˙D
128 1 2 4 5 6 120 123 127 15 gsumzres φGkAifkDFk0˙D=GkAifkDFk0˙
129 119 128 eqtrd φGFD=GkAifkDFk0˙
130 109 129 oveq12d φGFC+˙GFD=GkAifkCFk0˙+˙GkAifkDFk0˙
131 42 89 130 3eqtr4d φGF=GFC+˙GFD