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 = ( Base ` G )
gsumzsplit.0
|- .0. = ( 0g ` G )
gsumzsplit.p
|- .+ = ( +g ` G )
gsumzsplit.z
|- Z = ( Cntz ` G )
gsumzsplit.g
|- ( ph -> G e. Mnd )
gsumzsplit.a
|- ( ph -> A e. V )
gsumzsplit.f
|- ( ph -> F : A --> B )
gsumzsplit.c
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumzsplit.w
|- ( ph -> F finSupp .0. )
gsumzsplit.i
|- ( ph -> ( C i^i D ) = (/) )
gsumzsplit.u
|- ( ph -> A = ( C u. D ) )
Assertion gsumzsplit
|- ( ph -> ( G gsum F ) = ( ( G gsum ( F |` C ) ) .+ ( G gsum ( F |` D ) ) ) )

Proof

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