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	|- B = ( Base ` G )
Assertion	gsumwcl	|- ( ( G e. Mnd /\ W e. Word B ) -> ( G gsum W ) e. B )

Proof

Step	Hyp	Ref	Expression
1		gsumwcl.b	|- B = ( Base ` G )
2	1	submid	|- ( G e. Mnd -> B e. ( SubMnd ` G ) )
3		gsumwsubmcl	|- ( ( B e. ( SubMnd ` G ) /\ W e. Word B ) -> ( G gsum W ) e. B )
4	2 3	sylan	|- ( ( G e. Mnd /\ W e. Word B ) -> ( G gsum W ) e. B )