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 𝑊 ) + 𝑍 ) )