Theorem gsumsplit

Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 5-Jun-2019)

	Ref	Expression
Hypotheses	gsumsplit.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumsplit.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsumsplit.p	⊢ + = ( +g ‘ 𝐺 )
	gsumsplit.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumsplit.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumsplit.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	gsumsplit.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
	gsumsplit.i	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
	gsumsplit.u	⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
Assertion	gsumsplit	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) + ( 𝐺 Σg ( 𝐹 ↾ 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumsplit.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumsplit.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsumsplit.p	⊢ + = ( +g ‘ 𝐺 )
4		gsumsplit.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5		gsumsplit.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		gsumsplit.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7		gsumsplit.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
8		gsumsplit.i	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
9		gsumsplit.u	⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
10		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
11		cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
12	4 11	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
13	1 10 4 6	cntzcmnf	⊢ ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
14	1 2 3 10 12 5 6 13 7 8 9	gsumzsplit	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) + ( 𝐺 Σg ( 𝐹 ↾ 𝐷 ) ) ) )