Theorem mulgnn0subcl

Description: Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Hypotheses	mulgnnsubcl.b	$$⊢B={\mathrm{Base}}_G$$
	mulgnnsubcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mulgnnsubcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mulgnnsubcl.g	$$⊢\phi \to G\in V$$
	mulgnnsubcl.s	$$⊢\phi \to S\subseteq B$$
	mulgnnsubcl.c	$$⊢\left(\phi \wedge x\in S\wedge y\in S\right)\to x\underset{\dot{}}{+}y\in S$$
	mulgnn0subcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
	mulgnn0subcl.c	$$⊢\phi \to \underset{\dot{}}{0}\in S$$
Assertion	mulgnn0subcl	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to N\underset{\dot{}}{·}X\in S$$

Proof

Step	Hyp	Ref	Expression
1		mulgnnsubcl.b	$$⊢B={\mathrm{Base}}_G$$
2		mulgnnsubcl.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		mulgnnsubcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		mulgnnsubcl.g	$$⊢\phi \to G\in V$$
5		mulgnnsubcl.s	$$⊢\phi \to S\subseteq B$$
6		mulgnnsubcl.c	$$⊢\left(\phi \wedge x\in S\wedge y\in S\right)\to x\underset{\dot{}}{+}y\in S$$
7		mulgnn0subcl.z	$$⊢\underset{\dot{}}{0}=0_G$$
8		mulgnn0subcl.c	$$⊢\phi \to \underset{\dot{}}{0}\in S$$
9	1 2 3 4 5 6	mulgnnsubcl	$$⊢\left(\phi \wedge N\in \mathbb{N}\wedge X\in S\right)\to N\underset{\dot{}}{·}X\in S$$
10	9	3expa	$$⊢\left(\left(\phi \wedge N\in \mathbb{N}\right)\wedge X\in S\right)\to N\underset{\dot{}}{·}X\in S$$
11	10	an32s	$$⊢\left(\left(\phi \wedge X\in S\right)\wedge N\in \mathbb{N}\right)\to N\underset{\dot{}}{·}X\in S$$
12	11	3adantl2	$$⊢\left(\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\wedge N\in \mathbb{N}\right)\to N\underset{\dot{}}{·}X\in S$$
13		oveq1	$$⊢N=0\to N\underset{\dot{}}{·}X=0\underset{\dot{}}{·}X$$
14	5	3ad2ant1	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to S\subseteq B$$
15		simp3	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to X\in S$$
16	14 15	sseldd	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to X\in B$$
17	1 7 2	mulg0	$$⊢X\in B\to 0\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
18	16 17	syl	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to 0\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
19	13 18	sylan9eqr	$$⊢\left(\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\wedge N=0\right)\to N\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
20	8	3ad2ant1	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to \underset{\dot{}}{0}\in S$$
21	20	adantr	$$⊢\left(\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\wedge N=0\right)\to \underset{\dot{}}{0}\in S$$
22	19 21	eqeltrd	$$⊢\left(\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\wedge N=0\right)\to N\underset{\dot{}}{·}X\in S$$
23		simp2	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to N\in {\mathbb{N}}_0$$
24		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
25	23 24	sylib	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to \left(N\in \mathbb{N}\vee N=0\right)$$
26	12 22 25	mpjaodan	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\wedge X\in S\right)\to N\underset{\dot{}}{·}X\in S$$