Metamath Proof Explorer


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 Mnd W Word B G W B

Proof

Step Hyp Ref Expression
1 gsumwcl.b B = Base G
2 1 submid G Mnd B SubMnd G
3 gsumwsubmcl B SubMnd G W Word B G W B
4 2 3 sylan G Mnd W Word B G W B