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