Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsumzsplit Structured version   Visualization version   GIF version

Theorem gsumzsplit 19120
 Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.)
Hypotheses
Ref Expression
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
Ref Expression
gsumzsplit (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹𝐶)) + (𝐺 Σg (𝐹𝐷))))

Proof of Theorem gsumzsplit
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 gsumzsplit.b . . 3 𝐵 = (Base‘𝐺)
2 gsumzsplit.0 . . 3 0 = (0g𝐺)
3 gsumzsplit.p . . 3 + = (+g𝐺)
4 gsumzsplit.z . . 3 𝑍 = (Cntz‘𝐺)
5 gsumzsplit.g . . 3 (𝜑𝐺 ∈ Mnd)
6 gsumzsplit.a . . 3 (𝜑𝐴𝑉)
7 gsumzsplit.f . . . 4 (𝜑𝐹:𝐴𝐵)
82fvexi 6676 . . . . 5 0 ∈ V
98a1i 11 . . . 4 (𝜑0 ∈ V)
10 gsumzsplit.w . . . 4 (𝜑𝐹 finSupp 0 )
117, 6, 9, 10fsuppmptif 8901 . . 3 (𝜑 → (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) finSupp 0 )
127, 6, 9, 10fsuppmptif 8901 . . 3 (𝜑 → (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) finSupp 0 )
131submacs 18062 . . . . 5 (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵))
14 acsmre 16986 . . . . 5 ((SubMnd‘𝐺) ∈ (ACS‘𝐵) → (SubMnd‘𝐺) ∈ (Moore‘𝐵))
155, 13, 143syl 18 . . . 4 (𝜑 → (SubMnd‘𝐺) ∈ (Moore‘𝐵))
167frnd 6509 . . . 4 (𝜑 → ran 𝐹𝐵)
17 eqid 2758 . . . . 5 (mrCls‘(SubMnd‘𝐺)) = (mrCls‘(SubMnd‘𝐺))
1817mrccl 16945 . . . 4 (((SubMnd‘𝐺) ∈ (Moore‘𝐵) ∧ ran 𝐹𝐵) → ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺))
1915, 16, 18syl2anc 587 . . 3 (𝜑 → ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺))
20 gsumzsplit.c . . . . 5 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
21 eqid 2758 . . . . . 6 (𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) = (𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
224, 17, 21cntzspan 19037 . . . . 5 ((𝐺 ∈ Mnd ∧ ran 𝐹 ⊆ (𝑍‘ran 𝐹)) → (𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd)
235, 20, 22syl2anc 587 . . . 4 (𝜑 → (𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd)
2421, 4submcmn2 19032 . . . . 5 (((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺) → ((𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))))
2519, 24syl 17 . . . 4 (𝜑 → ((𝐺s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))))
2623, 25mpbid 235 . . 3 (𝜑 → ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)))
2715, 17, 16mrcssidd 16959 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
2827adantr 484 . . . . . 6 ((𝜑𝑘𝐴) → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
297ffnd 6503 . . . . . . 7 (𝜑𝐹 Fn 𝐴)
30 fnfvelrn 6844 . . . . . . 7 ((𝐹 Fn 𝐴𝑘𝐴) → (𝐹𝑘) ∈ ran 𝐹)
3129, 30sylan 583 . . . . . 6 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ran 𝐹)
3228, 31sseldd 3895 . . . . 5 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
332subm0cl 18047 . . . . . . 7 (((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺) → 0 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
3419, 33syl 17 . . . . . 6 (𝜑0 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
3534adantr 484 . . . . 5 ((𝜑𝑘𝐴) → 0 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
3632, 35ifcld 4469 . . . 4 ((𝜑𝑘𝐴) → if(𝑘𝐶, (𝐹𝑘), 0 ) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
3736fmpttd 6875 . . 3 (𝜑 → (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )):𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
3832, 35ifcld 4469 . . . 4 ((𝜑𝑘𝐴) → if(𝑘𝐷, (𝐹𝑘), 0 ) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
3938fmpttd 6875 . . 3 (𝜑 → (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )):𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
401, 2, 3, 4, 5, 6, 11, 12, 19, 26, 37, 39gsumzadd 19115 . 2 (𝜑 → (𝐺 Σg ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ∘f + (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )))) = ((𝐺 Σg (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 ))) + (𝐺 Σg (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )))))
417feqmptd 6725 . . . . 5 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
42 iftrue 4429 . . . . . . . . . 10 (𝑘𝐶 → if(𝑘𝐶, (𝐹𝑘), 0 ) = (𝐹𝑘))
4342adantl 485 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑘𝐶) → if(𝑘𝐶, (𝐹𝑘), 0 ) = (𝐹𝑘))
44 gsumzsplit.i . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝐷) = ∅)
45 noel 4232 . . . . . . . . . . . . . . . 16 ¬ 𝑘 ∈ ∅
46 eleq2 2840 . . . . . . . . . . . . . . . 16 ((𝐶𝐷) = ∅ → (𝑘 ∈ (𝐶𝐷) ↔ 𝑘 ∈ ∅))
4745, 46mtbiri 330 . . . . . . . . . . . . . . 15 ((𝐶𝐷) = ∅ → ¬ 𝑘 ∈ (𝐶𝐷))
4844, 47syl 17 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝑘 ∈ (𝐶𝐷))
4948adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ¬ 𝑘 ∈ (𝐶𝐷))
50 elin 3876 . . . . . . . . . . . . 13 (𝑘 ∈ (𝐶𝐷) ↔ (𝑘𝐶𝑘𝐷))
5149, 50sylnib 331 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → ¬ (𝑘𝐶𝑘𝐷))
52 imnan 403 . . . . . . . . . . . 12 ((𝑘𝐶 → ¬ 𝑘𝐷) ↔ ¬ (𝑘𝐶𝑘𝐷))
5351, 52sylibr 237 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝑘𝐶 → ¬ 𝑘𝐷))
5453imp 410 . . . . . . . . . 10 (((𝜑𝑘𝐴) ∧ 𝑘𝐶) → ¬ 𝑘𝐷)
5554iffalsed 4434 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑘𝐶) → if(𝑘𝐷, (𝐹𝑘), 0 ) = 0 )
5643, 55oveq12d 7173 . . . . . . . 8 (((𝜑𝑘𝐴) ∧ 𝑘𝐶) → (if(𝑘𝐶, (𝐹𝑘), 0 ) + if(𝑘𝐷, (𝐹𝑘), 0 )) = ((𝐹𝑘) + 0 ))
577ffvelrnda 6847 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ 𝐵)
581, 3, 2mndrid 18003 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝐹𝑘) ∈ 𝐵) → ((𝐹𝑘) + 0 ) = (𝐹𝑘))
595, 57, 58syl2an2r 684 . . . . . . . . 9 ((𝜑𝑘𝐴) → ((𝐹𝑘) + 0 ) = (𝐹𝑘))
6059adantr 484 . . . . . . . 8 (((𝜑𝑘𝐴) ∧ 𝑘𝐶) → ((𝐹𝑘) + 0 ) = (𝐹𝑘))
6156, 60eqtrd 2793 . . . . . . 7 (((𝜑𝑘𝐴) ∧ 𝑘𝐶) → (if(𝑘𝐶, (𝐹𝑘), 0 ) + if(𝑘𝐷, (𝐹𝑘), 0 )) = (𝐹𝑘))
6253con2d 136 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝑘𝐷 → ¬ 𝑘𝐶))
6362imp 410 . . . . . . . . . 10 (((𝜑𝑘𝐴) ∧ 𝑘𝐷) → ¬ 𝑘𝐶)
6463iffalsed 4434 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑘𝐷) → if(𝑘𝐶, (𝐹𝑘), 0 ) = 0 )
65 iftrue 4429 . . . . . . . . . 10 (𝑘𝐷 → if(𝑘𝐷, (𝐹𝑘), 0 ) = (𝐹𝑘))
6665adantl 485 . . . . . . . . 9 (((𝜑𝑘𝐴) ∧ 𝑘𝐷) → if(𝑘𝐷, (𝐹𝑘), 0 ) = (𝐹𝑘))
6764, 66oveq12d 7173 . . . . . . . 8 (((𝜑𝑘𝐴) ∧ 𝑘𝐷) → (if(𝑘𝐶, (𝐹𝑘), 0 ) + if(𝑘𝐷, (𝐹𝑘), 0 )) = ( 0 + (𝐹𝑘)))
681, 3, 2mndlid 18002 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ (𝐹𝑘) ∈ 𝐵) → ( 0 + (𝐹𝑘)) = (𝐹𝑘))
695, 57, 68syl2an2r 684 . . . . . . . . 9 ((𝜑𝑘𝐴) → ( 0 + (𝐹𝑘)) = (𝐹𝑘))
7069adantr 484 . . . . . . . 8 (((𝜑𝑘𝐴) ∧ 𝑘𝐷) → ( 0 + (𝐹𝑘)) = (𝐹𝑘))
7167, 70eqtrd 2793 . . . . . . 7 (((𝜑𝑘𝐴) ∧ 𝑘𝐷) → (if(𝑘𝐶, (𝐹𝑘), 0 ) + if(𝑘𝐷, (𝐹𝑘), 0 )) = (𝐹𝑘))
72 gsumzsplit.u . . . . . . . . . 10 (𝜑𝐴 = (𝐶𝐷))
7372eleq2d 2837 . . . . . . . . 9 (𝜑 → (𝑘𝐴𝑘 ∈ (𝐶𝐷)))
74 elun 4056 . . . . . . . . 9 (𝑘 ∈ (𝐶𝐷) ↔ (𝑘𝐶𝑘𝐷))
7573, 74bitrdi 290 . . . . . . . 8 (𝜑 → (𝑘𝐴 ↔ (𝑘𝐶𝑘𝐷)))
7675biimpa 480 . . . . . . 7 ((𝜑𝑘𝐴) → (𝑘𝐶𝑘𝐷))
7761, 71, 76mpjaodan 956 . . . . . 6 ((𝜑𝑘𝐴) → (if(𝑘𝐶, (𝐹𝑘), 0 ) + if(𝑘𝐷, (𝐹𝑘), 0 )) = (𝐹𝑘))
7877mpteq2dva 5130 . . . . 5 (𝜑 → (𝑘𝐴 ↦ (if(𝑘𝐶, (𝐹𝑘), 0 ) + if(𝑘𝐷, (𝐹𝑘), 0 ))) = (𝑘𝐴 ↦ (𝐹𝑘)))
7941, 78eqtr4d 2796 . . . 4 (𝜑𝐹 = (𝑘𝐴 ↦ (if(𝑘𝐶, (𝐹𝑘), 0 ) + if(𝑘𝐷, (𝐹𝑘), 0 ))))
801, 2mndidcl 17997 . . . . . . . 8 (𝐺 ∈ Mnd → 0𝐵)
815, 80syl 17 . . . . . . 7 (𝜑0𝐵)
8281adantr 484 . . . . . 6 ((𝜑𝑘𝐴) → 0𝐵)
8357, 82ifcld 4469 . . . . 5 ((𝜑𝑘𝐴) → if(𝑘𝐶, (𝐹𝑘), 0 ) ∈ 𝐵)
8457, 82ifcld 4469 . . . . 5 ((𝜑𝑘𝐴) → if(𝑘𝐷, (𝐹𝑘), 0 ) ∈ 𝐵)
85 eqidd 2759 . . . . 5 (𝜑 → (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) = (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )))
86 eqidd 2759 . . . . 5 (𝜑 → (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) = (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )))
876, 83, 84, 85, 86offval2 7429 . . . 4 (𝜑 → ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ∘f + (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 ))) = (𝑘𝐴 ↦ (if(𝑘𝐶, (𝐹𝑘), 0 ) + if(𝑘𝐷, (𝐹𝑘), 0 ))))
8879, 87eqtr4d 2796 . . 3 (𝜑𝐹 = ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ∘f + (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 ))))
8988oveq2d 7171 . 2 (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ∘f + (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )))))
9041reseq1d 5826 . . . . . 6 (𝜑 → (𝐹𝐶) = ((𝑘𝐴 ↦ (𝐹𝑘)) ↾ 𝐶))
91 ssun1 4079 . . . . . . . 8 𝐶 ⊆ (𝐶𝐷)
9291, 72sseqtrrid 3947 . . . . . . 7 (𝜑𝐶𝐴)
9342mpteq2ia 5126 . . . . . . . 8 (𝑘𝐶 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) = (𝑘𝐶 ↦ (𝐹𝑘))
94 resmpt 5881 . . . . . . . 8 (𝐶𝐴 → ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ↾ 𝐶) = (𝑘𝐶 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )))
95 resmpt 5881 . . . . . . . 8 (𝐶𝐴 → ((𝑘𝐴 ↦ (𝐹𝑘)) ↾ 𝐶) = (𝑘𝐶 ↦ (𝐹𝑘)))
9693, 94, 953eqtr4a 2819 . . . . . . 7 (𝐶𝐴 → ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ↾ 𝐶) = ((𝑘𝐴 ↦ (𝐹𝑘)) ↾ 𝐶))
9792, 96syl 17 . . . . . 6 (𝜑 → ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ↾ 𝐶) = ((𝑘𝐴 ↦ (𝐹𝑘)) ↾ 𝐶))
9890, 97eqtr4d 2796 . . . . 5 (𝜑 → (𝐹𝐶) = ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ↾ 𝐶))
9998oveq2d 7171 . . . 4 (𝜑 → (𝐺 Σg (𝐹𝐶)) = (𝐺 Σg ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ↾ 𝐶)))
10083fmpttd 6875 . . . . 5 (𝜑 → (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )):𝐴𝐵)
10137frnd 6509 . . . . . 6 (𝜑 → ran (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
1024cntzidss 18540 . . . . . 6 ((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ ran (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → ran (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ⊆ (𝑍‘ran (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 ))))
10326, 101, 102syl2anc 587 . . . . 5 (𝜑 → ran (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ⊆ (𝑍‘ran (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 ))))
104 eldifn 4035 . . . . . . . 8 (𝑘 ∈ (𝐴𝐶) → ¬ 𝑘𝐶)
105104adantl 485 . . . . . . 7 ((𝜑𝑘 ∈ (𝐴𝐶)) → ¬ 𝑘𝐶)
106105iffalsed 4434 . . . . . 6 ((𝜑𝑘 ∈ (𝐴𝐶)) → if(𝑘𝐶, (𝐹𝑘), 0 ) = 0 )
107106, 6suppss2 7879 . . . . 5 (𝜑 → ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) supp 0 ) ⊆ 𝐶)
1081, 2, 4, 5, 6, 100, 103, 107, 11gsumzres 19102 . . . 4 (𝜑 → (𝐺 Σg ((𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 )) ↾ 𝐶)) = (𝐺 Σg (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 ))))
10999, 108eqtrd 2793 . . 3 (𝜑 → (𝐺 Σg (𝐹𝐶)) = (𝐺 Σg (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 ))))
11041reseq1d 5826 . . . . . 6 (𝜑 → (𝐹𝐷) = ((𝑘𝐴 ↦ (𝐹𝑘)) ↾ 𝐷))
111 ssun2 4080 . . . . . . . 8 𝐷 ⊆ (𝐶𝐷)
112111, 72sseqtrrid 3947 . . . . . . 7 (𝜑𝐷𝐴)
11365mpteq2ia 5126 . . . . . . . 8 (𝑘𝐷 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) = (𝑘𝐷 ↦ (𝐹𝑘))
114 resmpt 5881 . . . . . . . 8 (𝐷𝐴 → ((𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) ↾ 𝐷) = (𝑘𝐷 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )))
115 resmpt 5881 . . . . . . . 8 (𝐷𝐴 → ((𝑘𝐴 ↦ (𝐹𝑘)) ↾ 𝐷) = (𝑘𝐷 ↦ (𝐹𝑘)))
116113, 114, 1153eqtr4a 2819 . . . . . . 7 (𝐷𝐴 → ((𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) ↾ 𝐷) = ((𝑘𝐴 ↦ (𝐹𝑘)) ↾ 𝐷))
117112, 116syl 17 . . . . . 6 (𝜑 → ((𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) ↾ 𝐷) = ((𝑘𝐴 ↦ (𝐹𝑘)) ↾ 𝐷))
118110, 117eqtr4d 2796 . . . . 5 (𝜑 → (𝐹𝐷) = ((𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) ↾ 𝐷))
119118oveq2d 7171 . . . 4 (𝜑 → (𝐺 Σg (𝐹𝐷)) = (𝐺 Σg ((𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) ↾ 𝐷)))
12084fmpttd 6875 . . . . 5 (𝜑 → (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )):𝐴𝐵)
12139frnd 6509 . . . . . 6 (𝜑 → ran (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
1224cntzidss 18540 . . . . . 6 ((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ ran (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → ran (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) ⊆ (𝑍‘ran (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 ))))
12326, 121, 122syl2anc 587 . . . . 5 (𝜑 → ran (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) ⊆ (𝑍‘ran (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 ))))
124 eldifn 4035 . . . . . . . 8 (𝑘 ∈ (𝐴𝐷) → ¬ 𝑘𝐷)
125124adantl 485 . . . . . . 7 ((𝜑𝑘 ∈ (𝐴𝐷)) → ¬ 𝑘𝐷)
126125iffalsed 4434 . . . . . 6 ((𝜑𝑘 ∈ (𝐴𝐷)) → if(𝑘𝐷, (𝐹𝑘), 0 ) = 0 )
127126, 6suppss2 7879 . . . . 5 (𝜑 → ((𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) supp 0 ) ⊆ 𝐷)
1281, 2, 4, 5, 6, 120, 123, 127, 12gsumzres 19102 . . . 4 (𝜑 → (𝐺 Σg ((𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )) ↾ 𝐷)) = (𝐺 Σg (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 ))))
129119, 128eqtrd 2793 . . 3 (𝜑 → (𝐺 Σg (𝐹𝐷)) = (𝐺 Σg (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 ))))
130109, 129oveq12d 7173 . 2 (𝜑 → ((𝐺 Σg (𝐹𝐶)) + (𝐺 Σg (𝐹𝐷))) = ((𝐺 Σg (𝑘𝐴 ↦ if(𝑘𝐶, (𝐹𝑘), 0 ))) + (𝐺 Σg (𝑘𝐴 ↦ if(𝑘𝐷, (𝐹𝑘), 0 )))))
13140, 89, 1303eqtr4d 2803 1 (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹𝐶)) + (𝐺 Σg (𝐹𝐷))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  Vcvv 3409   ∖ cdif 3857   ∪ cun 3858   ∩ cin 3859   ⊆ wss 3860  ∅c0 4227  ifcif 4423   class class class wbr 5035   ↦ cmpt 5115  ran crn 5528   ↾ cres 5529   Fn wfn 6334  ⟶wf 6335  ‘cfv 6339  (class class class)co 7155   ∘f cof 7408   finSupp cfsupp 8871  Basecbs 16546   ↾s cress 16547  +gcplusg 16628  0gc0g 16776   Σg cgsu 16777  Moorecmre 16916  mrClscmrc 16917  ACScacs 16919  Mndcmnd 17982  SubMndcsubmnd 18026  Cntzccntz 18517  CMndccmn 18978 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-cnex 10636  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656  ax-pre-mulgt0 10657 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-iin 4889  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-se 5487  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-of 7410  df-om 7585  df-1st 7698  df-2nd 7699  df-supp 7841  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-1o 8117  df-er 8304  df-en 8533  df-dom 8534  df-sdom 8535  df-fin 8536  df-fsupp 8872  df-oi 9012  df-card 9406  df-pnf 10720  df-mnf 10721  df-xr 10722  df-ltxr 10723  df-le 10724  df-sub 10915  df-neg 10916  df-nn 11680  df-2 11742  df-n0 11940  df-z 12026  df-uz 12288  df-fz 12945  df-fzo 13088  df-seq 13424  df-hash 13746  df-ndx 16549  df-slot 16550  df-base 16552  df-sets 16553  df-ress 16554  df-plusg 16641  df-0g 16778  df-gsum 16779  df-mre 16920  df-mrc 16921  df-acs 16923  df-mgm 17923  df-sgrp 17972  df-mnd 17983  df-submnd 18028  df-cntz 18519  df-cmn 18980 This theorem is referenced by:  gsumsplit  19121  gsumzunsnd  19149  dpjidcl  19253
 Copyright terms: Public domain W3C validator