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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mulgnnsubcl.t	⊢ · = ( .g ‘ 𝐺 )
	mulgnnsubcl.p	⊢ + = ( +g ‘ 𝐺 )
	mulgnnsubcl.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	mulgnnsubcl.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
	mulgnnsubcl.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
	mulgnn0subcl.z	⊢ 0 = ( 0g ‘ 𝐺 )
	mulgnn0subcl.c	⊢ ( 𝜑 → 0 ∈ 𝑆 )
Assertion	mulgnn0subcl	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		mulgnnsubcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mulgnnsubcl.t	⊢ · = ( .g ‘ 𝐺 )
3		mulgnnsubcl.p	⊢ + = ( +g ‘ 𝐺 )
4		mulgnnsubcl.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5		mulgnnsubcl.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
6		mulgnnsubcl.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
7		mulgnn0subcl.z	⊢ 0 = ( 0g ‘ 𝐺 )
8		mulgnn0subcl.c	⊢ ( 𝜑 → 0 ∈ 𝑆 )
9	1 2 3 4 5 6	mulgnnsubcl	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
10	9	3expa	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
11	10	an32s	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
12	11	3adantl2	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
13		oveq1	⊢ ( 𝑁 = 0 → ( 𝑁 · 𝑋 ) = ( 0 · 𝑋 ) )
14	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
15		simp3	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
16	14 15	sseldd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐵 )
17	1 7 2	mulg0	⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = 0 )
18	16 17	syl	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 0 · 𝑋 ) = 0 )
19	13 18	sylan9eqr	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 𝑁 · 𝑋 ) = 0 )
20	8	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 0 ∈ 𝑆 )
21	20	adantr	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → 0 ∈ 𝑆 )
22	19 21	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
23		simp2	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑁 ∈ ℕ0 )
24		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
25	23 24	sylib	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
26	12 22 25	mpjaodan	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )