This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda 
 |-  ( ( 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 ) ) ) )