Theorem gsumsplit2f

Description: Split a group sum into two parts. (Contributed by AV, 4-Sep-2019)

	Ref	Expression
Hypotheses	gsumsplit2f.n	⊢ Ⅎ 𝑘 𝜑
	gsumsplit2f.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumsplit2f.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsumsplit2f.p	⊢ + = ( +g ‘ 𝐺 )
	gsumsplit2f.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumsplit2f.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumsplit2f.f	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
	gsumsplit2f.w	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
	gsumsplit2f.i	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
	gsumsplit2f.u	⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
Assertion	gsumsplit2f	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ 𝐷 ↦ 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumsplit2f.n	⊢ Ⅎ 𝑘 𝜑
2		gsumsplit2f.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		gsumsplit2f.z	⊢ 0 = ( 0g ‘ 𝐺 )
4		gsumsplit2f.p	⊢ + = ( +g ‘ 𝐺 )
5		gsumsplit2f.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
6		gsumsplit2f.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7		gsumsplit2f.f	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
8		gsumsplit2f.w	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 )
9		gsumsplit2f.i	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
10		gsumsplit2f.u	⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
11		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 )
12	1 7 11	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 ⟶ 𝐵 )
13	2 3 4 5 6 12 8 9 10	gsumsplit	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐶 ) ) + ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐷 ) ) ) )
14		ssun1	⊢ 𝐶 ⊆ ( 𝐶 ∪ 𝐷 )
15	14 10	sseqtrrid	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
16	15	resmptd	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐶 ) = ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) )
17	16	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐶 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) )
18		ssun2	⊢ 𝐷 ⊆ ( 𝐶 ∪ 𝐷 )
19	18 10	sseqtrrid	⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
20	19	resmptd	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐷 ) = ( 𝑘 ∈ 𝐷 ↦ 𝑋 ) )
21	20	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐷 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐷 ↦ 𝑋 ) ) )
22	17 21	oveq12d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐶 ) ) + ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐷 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ 𝐷 ↦ 𝑋 ) ) ) )
23	13 22	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ 𝐷 ↦ 𝑋 ) ) ) )