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

Metamath Proof Explorer

Theorem gsumadd

Description: The sum of two group sums. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

Ref Expression
Hypotheses gsumadd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumadd.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsumadd.p ⊢ + = ( +g ‘ 𝐺 )
gsumadd.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsumadd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumadd.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumadd.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
gsumadd.fn ⊢ ( 𝜑 → 𝐹 finSupp 0 )
gsumadd.hn ⊢ ( 𝜑 → 𝐻 finSupp 0 )
Assertion gsumadd ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 gsumadd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumadd.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumadd.p ⊢ + = ( +g ‘ 𝐺 )
4 gsumadd.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5 gsumadd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 gsumadd.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 gsumadd.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
8 gsumadd.fn ⊢ ( 𝜑 → 𝐹 finSupp 0 )
9 gsumadd.hn ⊢ ( 𝜑 → 𝐻 finSupp 0 )
10 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
11 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
12 4 11 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
13 1 submid ⊢ ( 𝐺 ∈ Mnd → 𝐵 ∈ ( SubMnd ‘ 𝐺 ) )
14 12 13 syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubMnd ‘ 𝐺 ) )
15 ssid ⊢ 𝐵 ⊆ 𝐵
16 1 10 cntzcmn ⊢ ( ( 𝐺 ∈ CMnd ∧ 𝐵 ⊆ 𝐵 ) → ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) = 𝐵 )
17 4 15 16 sylancl ⊢ ( 𝜑 → ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) = 𝐵 )
18 15 17 sseqtrrid ⊢ ( 𝜑 → 𝐵 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) )
19 1 2 3 10 12 5 8 9 14 18 6 7 gsumzadd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘f + 𝐻 ) ) = ( ( 𝐺 Σg 𝐹 ) + ( 𝐺 Σg 𝐻 ) ) )