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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumzsplit.0 ⊢ 0 = ( 0g ‘ 𝐺 )
gsumzsplit.p ⊢ + = ( +g ‘ 𝐺 )
gsumzsplit.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
gsumzsplit.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumzsplit.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumzsplit.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumzsplit.c ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
gsumzsplit.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
gsumzsplit.i ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
gsumzsplit.u ⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
Assertion gsumzsplit ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) + ( 𝐺 Σg ( 𝐹 ↾ 𝐷 ) ) ) )

Proof

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