gsumwsubmcl

Description: Closure of the composite in any submonoid. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 1-Oct-2015)

		Ref	Expression
	Assertion	gsumwsubmcl	$⊢ (S \in SubMnd (G) \land W \in Word S) \to \sum_{G} W \in S$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ W = \emptyset \to \sum_{G} W = \sum_{G} \emptyset$
2		eqid	$⊢ 0_{G} = 0_{G}$
3	2	gsum0	$⊢ \sum_{G} \emptyset = 0_{G}$
4	1 3	eqtrdi	$⊢ W = \emptyset \to \sum_{G} W = 0_{G}$
5	4	eleq1d	$⊢ W = \emptyset \to (\sum_{G} W \in S \leftrightarrow 0_{G} \in S)$
6		eqid	$⊢ {Base}_{G} = {Base}_{G}$
7		eqid	$⊢ +_{G} = +_{G}$
8		submrcl	$⊢ S \in SubMnd (G) \to G \in Mnd$
9	8	ad2antrr	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to G \in Mnd$
10		lennncl	$⊢ (W \in Word S \land W \neq \emptyset) \to \|W\| \in ℕ$
11	10	adantll	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to \|W\| \in ℕ$
12		nnm1nn0	$⊢ \|W\| \in ℕ \to \|W\| - 1 \in ℕ_{0}$
13	11 12	syl	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to \|W\| - 1 \in ℕ_{0}$
14		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
15	13 14	eleqtrdi	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to \|W\| - 1 \in ℤ_{\geq 0}$
16		wrdf	$⊢ W \in Word S \to W : (0 ..^\|W\|) ⟶ S$
17	16	ad2antlr	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to W : (0 ..^\|W\|) ⟶ S$
18	11	nnzd	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to \|W\| \in ℤ$
19		fzoval	$⊢ \|W\| \in ℤ \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
20	18 19	syl	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to (0 ..^\|W\|) = (0 \dots \|W\| - 1)$
21	20	feq2d	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to (W : (0 ..^\|W\|) ⟶ S \leftrightarrow W : (0 \dots \|W\| - 1) ⟶ S)$
22	17 21	mpbid	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to W : (0 \dots \|W\| - 1) ⟶ S$
23	6	submss	$⊢ S \in SubMnd (G) \to S \subseteq {Base}_{G}$
24	23	ad2antrr	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to S \subseteq {Base}_{G}$
25	22 24	fssd	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to W : (0 \dots \|W\| - 1) ⟶ {Base}_{G}$
26	6 7 9 15 25	gsumval2	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to \sum_{G} W = seq 0 (+_{G}, W) (\|W\| - 1)$
27	22	ffvelcdmda	$⊢ (((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \land x \in (0 \dots \|W\| - 1)) \to W (x) \in S$
28	7	submcl	$⊢ (S \in SubMnd (G) \land x \in S \land y \in S) \to x +_{G} y \in S$
29	28	3expb	$⊢ (S \in SubMnd (G) \land (x \in S \land y \in S)) \to x +_{G} y \in S$
30	29	ad4ant14	$⊢ (((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \land (x \in S \land y \in S)) \to x +_{G} y \in S$
31	15 27 30	seqcl	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to seq 0 (+_{G}, W) (\|W\| - 1) \in S$
32	26 31	eqeltrd	$⊢ ((S \in SubMnd (G) \land W \in Word S) \land W \neq \emptyset) \to \sum_{G} W \in S$
33	2	subm0cl	$⊢ S \in SubMnd (G) \to 0_{G} \in S$
34	33	adantr	$⊢ (S \in SubMnd (G) \land W \in Word S) \to 0_{G} \in S$
35	5 32 34	pm2.61ne	$⊢ (S \in SubMnd (G) \land W \in Word S) \to \sum_{G} W \in S$

Metamath Proof Explorer

Theorem gsumwsubmcl

Proof