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 \in Mnd \land W \in Word B) \to \sum_{G} W \in B$

Step	Hyp	Ref	Expression
1		gsumwcl.b	$⊢ B = {Base}_{G}$
2	1	submid	$⊢ G \in Mnd \to B \in SubMnd (G)$
3		gsumwsubmcl	$⊢ (B \in SubMnd (G) \land W \in Word B) \to \sum_{G} W \in B$
4	2 3	sylan	$⊢ (G \in Mnd \land W \in Word B) \to \sum_{G} W \in B$