# 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}={\mathrm{Base}}_{{G}}$
gsumzsplit.0
gsumzsplit.p
gsumzsplit.z ${⊢}{Z}=\mathrm{Cntz}\left({G}\right)$
gsumzsplit.g ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
gsumzsplit.a ${⊢}{\phi }\to {A}\in {V}$
gsumzsplit.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
gsumzsplit.c ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq {Z}\left(\mathrm{ran}{F}\right)$
gsumzsplit.w
gsumzsplit.i ${⊢}{\phi }\to {C}\cap {D}=\varnothing$
gsumzsplit.u ${⊢}{\phi }\to {A}={C}\cup {D}$
Assertion gsumzsplit

### Proof

Step Hyp Ref Expression
1 gsumzsplit.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsumzsplit.0
3 gsumzsplit.p
4 gsumzsplit.z ${⊢}{Z}=\mathrm{Cntz}\left({G}\right)$
5 gsumzsplit.g ${⊢}{\phi }\to {G}\in \mathrm{Mnd}$
6 gsumzsplit.a ${⊢}{\phi }\to {A}\in {V}$
7 gsumzsplit.f ${⊢}{\phi }\to {F}:{A}⟶{B}$
8 gsumzsplit.c ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq {Z}\left(\mathrm{ran}{F}\right)$
9 gsumzsplit.w
10 gsumzsplit.i ${⊢}{\phi }\to {C}\cap {D}=\varnothing$
11 gsumzsplit.u ${⊢}{\phi }\to {A}={C}\cup {D}$
12 2 fvexi
13 12 a1i
14 7 6 13 9 fsuppmptif
15 7 6 13 9 fsuppmptif
16 1 submacs ${⊢}{G}\in \mathrm{Mnd}\to \mathrm{SubMnd}\left({G}\right)\in \mathrm{ACS}\left({B}\right)$
17 acsmre ${⊢}\mathrm{SubMnd}\left({G}\right)\in \mathrm{ACS}\left({B}\right)\to \mathrm{SubMnd}\left({G}\right)\in \mathrm{Moore}\left({B}\right)$
18 5 16 17 3syl ${⊢}{\phi }\to \mathrm{SubMnd}\left({G}\right)\in \mathrm{Moore}\left({B}\right)$
19 7 frnd ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq {B}$
20 eqid ${⊢}\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)=\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)$
21 20 mrccl ${⊢}\left(\mathrm{SubMnd}\left({G}\right)\in \mathrm{Moore}\left({B}\right)\wedge \mathrm{ran}{F}\subseteq {B}\right)\to \mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\in \mathrm{SubMnd}\left({G}\right)$
22 18 19 21 syl2anc ${⊢}{\phi }\to \mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\in \mathrm{SubMnd}\left({G}\right)$
23 eqid ${⊢}{G}{↾}_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)={G}{↾}_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)$
24 4 20 23 cntzspan ${⊢}\left({G}\in \mathrm{Mnd}\wedge \mathrm{ran}{F}\subseteq {Z}\left(\mathrm{ran}{F}\right)\right)\to {G}{↾}_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\in \mathrm{CMnd}$
25 5 8 24 syl2anc ${⊢}{\phi }\to {G}{↾}_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\in \mathrm{CMnd}$
26 23 4 submcmn2 ${⊢}\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\in \mathrm{SubMnd}\left({G}\right)\to \left({G}{↾}_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\in \mathrm{CMnd}↔\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\subseteq {Z}\left(\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\right)\right)$
27 22 26 syl ${⊢}{\phi }\to \left({G}{↾}_{𝑠}\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\in \mathrm{CMnd}↔\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\subseteq {Z}\left(\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\right)\right)$
28 25 27 mpbid ${⊢}{\phi }\to \mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\subseteq {Z}\left(\mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)\right)$
29 18 20 19 mrcssidd ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq \mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)$
30 29 adantr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \mathrm{ran}{F}\subseteq \mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)$
31 7 ffnd ${⊢}{\phi }\to {F}Fn{A}$
32 fnfvelrn ${⊢}\left({F}Fn{A}\wedge {k}\in {A}\right)\to {F}\left({k}\right)\in \mathrm{ran}{F}$
33 31 32 sylan ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {F}\left({k}\right)\in \mathrm{ran}{F}$
34 30 33 sseldd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {F}\left({k}\right)\in \mathrm{mrCls}\left(\mathrm{SubMnd}\left({G}\right)\right)\left(\mathrm{ran}{F}\right)$
35 2 subm0cl
36 22 35 syl
38 34 37 ifcld
39 38 fmpttd
40 34 37 ifcld
41 40 fmpttd
42 1 2 3 4 5 6 14 15 22 28 39 41 gsumzadd
43 7 feqmptd ${⊢}{\phi }\to {F}=\left({k}\in {A}⟼{F}\left({k}\right)\right)$
44 iftrue
46 noel ${⊢}¬{k}\in \varnothing$
47 eleq2 ${⊢}{C}\cap {D}=\varnothing \to \left({k}\in \left({C}\cap {D}\right)↔{k}\in \varnothing \right)$
48 46 47 mtbiri ${⊢}{C}\cap {D}=\varnothing \to ¬{k}\in \left({C}\cap {D}\right)$
49 10 48 syl ${⊢}{\phi }\to ¬{k}\in \left({C}\cap {D}\right)$
50 49 adantr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to ¬{k}\in \left({C}\cap {D}\right)$
51 elin ${⊢}{k}\in \left({C}\cap {D}\right)↔\left({k}\in {C}\wedge {k}\in {D}\right)$
52 50 51 sylnib ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to ¬\left({k}\in {C}\wedge {k}\in {D}\right)$
53 imnan ${⊢}\left({k}\in {C}\to ¬{k}\in {D}\right)↔¬\left({k}\in {C}\wedge {k}\in {D}\right)$
54 52 53 sylibr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {C}\to ¬{k}\in {D}\right)$
55 54 imp ${⊢}\left(\left({\phi }\wedge {k}\in {A}\right)\wedge {k}\in {C}\right)\to ¬{k}\in {D}$
56 55 iffalsed
57 45 56 oveq12d
58 7 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {F}\left({k}\right)\in {B}$
59 1 3 2 mndrid
60 5 58 59 syl2an2r
62 57 61 eqtrd
63 54 con2d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {D}\to ¬{k}\in {C}\right)$
64 63 imp ${⊢}\left(\left({\phi }\wedge {k}\in {A}\right)\wedge {k}\in {D}\right)\to ¬{k}\in {C}$
65 64 iffalsed
66 iftrue
68 65 67 oveq12d
69 1 3 2 mndlid
70 5 58 69 syl2an2r
72 68 71 eqtrd
73 11 eleq2d ${⊢}{\phi }\to \left({k}\in {A}↔{k}\in \left({C}\cup {D}\right)\right)$
74 elun ${⊢}{k}\in \left({C}\cup {D}\right)↔\left({k}\in {C}\vee {k}\in {D}\right)$
75 73 74 syl6bb ${⊢}{\phi }\to \left({k}\in {A}↔\left({k}\in {C}\vee {k}\in {D}\right)\right)$
76 75 biimpa ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {C}\vee {k}\in {D}\right)$
77 62 72 76 mpjaodan
78 77 mpteq2dva
79 43 78 eqtr4d
80 1 2 mndidcl
81 5 80 syl
83 58 82 ifcld
84 58 82 ifcld
85 eqidd
86 eqidd
87 6 83 84 85 86 offval2
88 79 87 eqtr4d
89 88 oveq2d
90 43 reseq1d ${⊢}{\phi }\to {{F}↾}_{{C}}={\left({k}\in {A}⟼{F}\left({k}\right)\right)↾}_{{C}}$
91 ssun1 ${⊢}{C}\subseteq {C}\cup {D}$
92 91 11 sseqtrrid ${⊢}{\phi }\to {C}\subseteq {A}$
93 44 mpteq2ia
94 resmpt
95 resmpt ${⊢}{C}\subseteq {A}\to {\left({k}\in {A}⟼{F}\left({k}\right)\right)↾}_{{C}}=\left({k}\in {C}⟼{F}\left({k}\right)\right)$
96 93 94 95 3eqtr4a
97 92 96 syl
98 90 97 eqtr4d
99 98 oveq2d
100 83 fmpttd
101 39 frnd
102 4 cntzidss
103 28 101 102 syl2anc
104 eldifn ${⊢}{k}\in \left({A}\setminus {C}\right)\to ¬{k}\in {C}$
105 104 adantl ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {C}\right)\right)\to ¬{k}\in {C}$
106 105 iffalsed
107 106 6 suppss2
108 1 2 4 5 6 100 103 107 14 gsumzres
109 99 108 eqtrd
110 43 reseq1d ${⊢}{\phi }\to {{F}↾}_{{D}}={\left({k}\in {A}⟼{F}\left({k}\right)\right)↾}_{{D}}$
111 ssun2 ${⊢}{D}\subseteq {C}\cup {D}$
112 111 11 sseqtrrid ${⊢}{\phi }\to {D}\subseteq {A}$
113 66 mpteq2ia
114 resmpt
115 resmpt ${⊢}{D}\subseteq {A}\to {\left({k}\in {A}⟼{F}\left({k}\right)\right)↾}_{{D}}=\left({k}\in {D}⟼{F}\left({k}\right)\right)$
116 113 114 115 3eqtr4a
117 112 116 syl
118 110 117 eqtr4d
119 118 oveq2d
120 84 fmpttd
121 41 frnd
122 4 cntzidss
123 28 121 122 syl2anc
124 eldifn ${⊢}{k}\in \left({A}\setminus {D}\right)\to ¬{k}\in {D}$
125 124 adantl ${⊢}\left({\phi }\wedge {k}\in \left({A}\setminus {D}\right)\right)\to ¬{k}\in {D}$
126 125 iffalsed
127 126 6 suppss2
128 1 2 4 5 6 120 123 127 15 gsumzres
129 119 128 eqtrd
130 109 129 oveq12d
131 42 89 130 3eqtr4d