Theorem gsumzsplit 18150

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.

Step	Hyp	Ref	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 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
8		fvex 6113	. . . . . 6 ⊢ (0g‘𝐺) ∈ V
9	2, 8	eqeltri 2684	. . . . 5 ⊢ 0 ∈ V
10	9	a1i 11	. . . 4 ⊢ (𝜑 → 0 ∈ V)
11		gsumzsplit.w	. . . 4 ⊢ (𝜑 → 𝐹 finSupp 0 )
12	7, 6, 10, 11	fsuppmptif 8188	. . 3 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) finSupp 0 )
13	7, 6, 10, 11	fsuppmptif 8188	. . 3 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) finSupp 0 )
14	1	submacs 17188	. . . . 5 ⊢ (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵))
15		acsmre 16136	. . . . 5 ⊢ ((SubMnd‘𝐺) ∈ (ACS‘𝐵) → (SubMnd‘𝐺) ∈ (Moore‘𝐵))
16	5, 14, 15	3syl 18	. . . 4 ⊢ (𝜑 → (SubMnd‘𝐺) ∈ (Moore‘𝐵))
17		frn 5966	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
18	7, 17	syl 17	. . . 4 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐵)
19		eqid 2610	. . . . 5 ⊢ (mrCls‘(SubMnd‘𝐺)) = (mrCls‘(SubMnd‘𝐺))
20	19	mrccl 16094	. . . 4 ⊢ (((SubMnd‘𝐺) ∈ (Moore‘𝐵) ∧ ran 𝐹 ⊆ 𝐵) → ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺))
21	16, 18, 20	syl2anc 691	. . 3 ⊢ (𝜑 → ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺))
22		gsumzsplit.c	. . . . 5 ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
23		eqid 2610	. . . . . 6 ⊢ (𝐺 ↾s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) = (𝐺 ↾s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
24	4, 19, 23	cntzspan 18070	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ ran 𝐹 ⊆ (𝑍‘ran 𝐹)) → (𝐺 ↾s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd)
25	5, 22, 24	syl2anc 691	. . . 4 ⊢ (𝜑 → (𝐺 ↾s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd)
26	23, 4	submcmn2 18067	. . . . 5 ⊢ (((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺) → ((𝐺 ↾s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))))
27	21, 26	syl 17	. . . 4 ⊢ (𝜑 → ((𝐺 ↾s ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))))
28	25, 27	mpbid 221	. . 3 ⊢ (𝜑 → ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)))
29	16, 19, 18	mrcssidd 16108	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
30	29	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
31		ffn 5958	. . . . . . . 8 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
32	7, 31	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐹 Fn 𝐴)
33		fnfvelrn 6264	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ran 𝐹)
34	32, 33	sylan 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ran 𝐹)
35	30, 34	sseldd 3569	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
36	2	subm0cl 17175	. . . . . . 7 ⊢ (((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺) → 0 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
37	21, 36	syl 17	. . . . . 6 ⊢ (𝜑 → 0 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
38	37	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
39	35, 38	ifcld 4081	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
40		eqid 2610	. . . 4 ⊢ (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))
41	39, 40	fmptd 6292	. . 3 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )):𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
42	35, 38	ifcld 4081	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
43		eqid 2610	. . . 4 ⊢ (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))
44	42, 43	fmptd 6292	. . 3 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )):𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
45	1, 2, 3, 4, 5, 6, 12, 13, 21, 28, 41, 44	gsumzadd 18145	. 2 ⊢ (𝜑 → (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ∘𝑓 + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))) + (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))))
46	7	feqmptd 6159	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
47		iftrue 4042	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝐶 → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) = (𝐹‘𝑘))
48	47	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) = (𝐹‘𝑘))
49		gsumzsplit.i	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅)
50		noel 3878	. . . . . . . . . . . . . . . 16 ⊢ ¬ 𝑘 ∈ ∅
51		eleq2 2677	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∩ 𝐷) = ∅ → (𝑘 ∈ (𝐶 ∩ 𝐷) ↔ 𝑘 ∈ ∅))
52	50, 51	mtbiri 316	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∩ 𝐷) = ∅ → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷))
53	49, 52	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷))
54	53	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷))
55		elin 3758	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (𝐶 ∩ 𝐷) ↔ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷))
56	54, 55	sylnib 317	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷))
57		imnan 437	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ 𝐶 → ¬ 𝑘 ∈ 𝐷) ↔ ¬ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷))
58	56, 57	sylibr 223	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐶 → ¬ 𝑘 ∈ 𝐷))
59	58	imp 444	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → ¬ 𝑘 ∈ 𝐷)
60	59	iffalsed 4047	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) = 0 )
61	48, 60	oveq12d 6567	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = ((𝐹‘𝑘) + 0 ))
62	7	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝐵)
63	1, 3, 2	mndrid 17135	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ (𝐹‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘) + 0 ) = (𝐹‘𝑘))
64	5, 63	sylan 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐹‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘) + 0 ) = (𝐹‘𝑘))
65	62, 64	syldan 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) + 0 ) = (𝐹‘𝑘))
66	65	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → ((𝐹‘𝑘) + 0 ) = (𝐹‘𝑘))
67	61, 66	eqtrd 2644	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝐹‘𝑘))
68	58	con2d 128	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐷 → ¬ 𝑘 ∈ 𝐶))
69	68	imp 444	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → ¬ 𝑘 ∈ 𝐶)
70	69	iffalsed 4047	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) = 0 )
71		iftrue 4042	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝐷 → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) = (𝐹‘𝑘))
72	71	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) = (𝐹‘𝑘))
73	70, 72	oveq12d 6567	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = ( 0 + (𝐹‘𝑘)))
74	1, 3, 2	mndlid 17134	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ (𝐹‘𝑘) ∈ 𝐵) → ( 0 + (𝐹‘𝑘)) = (𝐹‘𝑘))
75	5, 74	sylan 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐹‘𝑘) ∈ 𝐵) → ( 0 + (𝐹‘𝑘)) = (𝐹‘𝑘))
76	62, 75	syldan 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ( 0 + (𝐹‘𝑘)) = (𝐹‘𝑘))
77	76	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → ( 0 + (𝐹‘𝑘)) = (𝐹‘𝑘))
78	73, 77	eqtrd 2644	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝐹‘𝑘))
79		gsumzsplit.u	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷))
80	79	eleq2d 2673	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↔ 𝑘 ∈ (𝐶 ∪ 𝐷)))
81		elun 3715	. . . . . . . . 9 ⊢ (𝑘 ∈ (𝐶 ∪ 𝐷) ↔ (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷))
82	80, 81	syl6bb 275	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↔ (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷)))
83	82	biimpa 500	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷))
84	67, 78, 83	mpjaodan 823	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝐹‘𝑘))
85	84	mpteq2dva 4672	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))) = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
86	46, 85	eqtr4d 2647	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))))
87	1, 2	mndidcl 17131	. . . . . . . 8 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
88	5, 87	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ∈ 𝐵)
89	88	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ∈ 𝐵)
90	62, 89	ifcld 4081	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) ∈ 𝐵)
91	62, 89	ifcld 4081	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) ∈ 𝐵)
92		eqidd 2611	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )))
93		eqidd 2611	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))
94	6, 90, 91, 92, 93	offval2 6812	. . . 4 ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ∘𝑓 + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))) = (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))))
95	86, 94	eqtr4d 2647	. . 3 ⊢ (𝜑 → 𝐹 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ∘𝑓 + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))))
96	95	oveq2d 6565	. 2 ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ∘𝑓 + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))))
97	46	reseq1d 5316	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶))
98		ssun1 3738	. . . . . . . 8 ⊢ 𝐶 ⊆ (𝐶 ∪ 𝐷)
99	98, 79	syl5sseqr 3617	. . . . . . 7 ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
100	47	mpteq2ia 4668	. . . . . . . 8 ⊢ (𝑘 ∈ 𝐶 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) = (𝑘 ∈ 𝐶 ↦ (𝐹‘𝑘))
101		resmpt 5369	. . . . . . . 8 ⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶) = (𝑘 ∈ 𝐶 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )))
102		resmpt 5369	. . . . . . . 8 ⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶) = (𝑘 ∈ 𝐶 ↦ (𝐹‘𝑘)))
103	100, 101, 102	3eqtr4a 2670	. . . . . . 7 ⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶))
104	99, 103	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶))
105	97, 104	eqtr4d 2647	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶))
106	105	oveq2d 6565	. . . 4 ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) = (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶)))
107	90, 40	fmptd 6292	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )):𝐴⟶𝐵)
108		frn 5966	. . . . . . 7 ⊢ ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )):𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
109	41, 108	syl 17	. . . . . 6 ⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
110	4	cntzidss 17593	. . . . . 6 ⊢ ((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ⊆ (𝑍‘ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))))
111	28, 109, 110	syl2anc 691	. . . . 5 ⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ⊆ (𝑍‘ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))))
112		eldifn 3695	. . . . . . . 8 ⊢ (𝑘 ∈ (𝐴 ∖ 𝐶) → ¬ 𝑘 ∈ 𝐶)
113	112	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐶)) → ¬ 𝑘 ∈ 𝐶)
114	113	iffalsed 4047	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐶)) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) = 0 )
115	114, 6	suppss2 7216	. . . . 5 ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) supp 0 ) ⊆ 𝐶)
116	1, 2, 4, 5, 6, 107, 111, 115, 12	gsumzres 18133	. . . 4 ⊢ (𝜑 → (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶)) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))))
117	106, 116	eqtrd 2644	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))))
118	46	reseq1d 5316	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷))
119		ssun2 3739	. . . . . . . 8 ⊢ 𝐷 ⊆ (𝐶 ∪ 𝐷)
120	119, 79	syl5sseqr 3617	. . . . . . 7 ⊢ (𝜑 → 𝐷 ⊆ 𝐴)
121	71	mpteq2ia 4668	. . . . . . . 8 ⊢ (𝑘 ∈ 𝐷 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝑘 ∈ 𝐷 ↦ (𝐹‘𝑘))
122		resmpt 5369	. . . . . . . 8 ⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷) = (𝑘 ∈ 𝐷 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))
123		resmpt 5369	. . . . . . . 8 ⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷) = (𝑘 ∈ 𝐷 ↦ (𝐹‘𝑘)))
124	121, 122, 123	3eqtr4a 2670	. . . . . . 7 ⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷))
125	120, 124	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷))
126	118, 125	eqtr4d 2647	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷))
127	126	oveq2d 6565	. . . 4 ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐷)) = (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷)))
128	91, 43	fmptd 6292	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )):𝐴⟶𝐵)
129		frn 5966	. . . . . . 7 ⊢ ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )):𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
130	44, 129	syl 17	. . . . . 6 ⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))
131	4	cntzidss 17593	. . . . . 6 ⊢ ((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ⊆ (𝑍‘ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))))
132	28, 130, 131	syl2anc 691	. . . . 5 ⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ⊆ (𝑍‘ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))))
133		eldifn 3695	. . . . . . . 8 ⊢ (𝑘 ∈ (𝐴 ∖ 𝐷) → ¬ 𝑘 ∈ 𝐷)
134	133	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐷)) → ¬ 𝑘 ∈ 𝐷)
135	134	iffalsed 4047	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐷)) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) = 0 )
136	135, 6	suppss2 7216	. . . . 5 ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) supp 0 ) ⊆ 𝐷)
137	1, 2, 4, 5, 6, 128, 132, 136, 13	gsumzres 18133	. . . 4 ⊢ (𝜑 → (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷)) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))))
138	127, 137	eqtrd 2644	. . 3 ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐷)) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))))
139	117, 138	oveq12d 6567	. 2 ⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ 𝐶)) + (𝐺 Σg (𝐹 ↾ 𝐷))) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))) + (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))))
140	45, 96, 139	3eqtr4d 2654	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ 𝐶)) + (𝐺 Σg (𝐹 ↾ 𝐷))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  ran crn 5039   ↾ cres 5040   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘_𝑓 cof 6793   finSupp cfsupp 8158  Basecbs 15695   ↾_s cress 15696  +_gcplusg 15768  0_gc0g 15923   Σ_g cgsu 15924  Moorecmre 16065  mrClscmrc 16066  ACScacs 16068  Mndcmnd 17117  SubMndcsubmnd 17157  Cntzccntz 17571  CMndccmn 18016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-0g 15925  df-gsum 15926  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-cntz 17573  df-cmn 18018

This theorem is referenced by:  gsumsplit  18151  gsumzunsnd  18178  dpjidcl  18280