Theorem gsumwcl

Description: Closure of the composite of a word in a structure G . (Contributed by Stefan O'Rear, 15-Aug-2015)

	Ref	Expression
Hypothesis	gsumwcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	gsumwcl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ) → ( 𝐺 Σg 𝑊 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		gsumwcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2	1	submid	⊢ ( 𝐺 ∈ Mnd → 𝐵 ∈ ( SubMnd ‘ 𝐺 ) )
3		gsumwsubmcl	⊢ ( ( 𝐵 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑊 ∈ Word 𝐵 ) → ( 𝐺 Σg 𝑊 ) ∈ 𝐵 )
4	2 3	sylan	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ) → ( 𝐺 Σg 𝑊 ) ∈ 𝐵 )