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