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

Metamath Proof Explorer

Theorem gsumccatsn

Description: Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsumccat.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumccat.p ⊢ + = ( +g ‘ 𝐺 )
Assertion gsumccatsn ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( 𝐺 Σg 𝑊 ) + 𝑍 ) )

Proof

Step Hyp Ref Expression
1 gsumccat.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumccat.p ⊢ + = ( +g ‘ 𝐺 )
3 s1cl ⊢ ( 𝑍 ∈ 𝐵 → ⟨“ 𝑍 ”⟩ ∈ Word 𝐵 )
4 1 2 gsumccat ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ ⟨“ 𝑍 ”⟩ ∈ Word 𝐵 ) → ( 𝐺 Σg ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg ⟨“ 𝑍 ”⟩ ) ) )
5 3 4 syl3an3 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg ⟨“ 𝑍 ”⟩ ) ) )
6 1 gsumws1 ⊢ ( 𝑍 ∈ 𝐵 → ( 𝐺 Σg ⟨“ 𝑍 ”⟩ ) = 𝑍 )
7 6 3ad2ant3 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐺 Σg ⟨“ 𝑍 ”⟩ ) = 𝑍 )
8 7 oveq2d ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝐺 Σg 𝑊 ) + ( 𝐺 Σg ⟨“ 𝑍 ”⟩ ) ) = ( ( 𝐺 Σg 𝑊 ) + 𝑍 ) )
9 5 8 eqtrd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑊 ++ ⟨“ 𝑍 ”⟩ ) ) = ( ( 𝐺 Σg 𝑊 ) + 𝑍 ) )