This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐹 ↾ 𝐷 ) ) ) )