Theorem mulgsubcl

Description: Closure of the group multiple (exponentiation) operation in a subgroup. (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 ∈ 𝑆 )
	mulgsubcl.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
	mulgsubcl.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
Assertion	mulgsubcl	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )

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		mulgsubcl.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
10		mulgsubcl.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
11	1 2 3 4 5 6 7 8	mulgnn0subcl	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
12	11	3expa	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
13	12	an32s	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
14	13	3adantl2	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
15		simp2	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑁 ∈ ℤ )
16	15	adantr	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
17	16	zcnd	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
18	17	negnegd	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → - - 𝑁 = 𝑁 )
19	18	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → ( - - 𝑁 · 𝑋 ) = ( 𝑁 · 𝑋 ) )
20		id	⊢ ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℕ )
21	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑆 ⊆ 𝐵 )
22		simp3	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
23	21 22	sseldd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐵 )
24	1 2 9	mulgnegnn	⊢ ( ( - 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( - - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) )
25	20 23 24	syl2anr	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → ( - - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) )
26	19 25	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → ( 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) )
27		fveq2	⊢ ( 𝑥 = ( - 𝑁 · 𝑋 ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) )
28	27	eleq1d	⊢ ( 𝑥 = ( - 𝑁 · 𝑋 ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ↔ ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) ∈ 𝑆 ) )
29	10	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
30	29	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
31	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 )
32	1 2 3 4 5 6	mulgnnsubcl	⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆 ) → ( - 𝑁 · 𝑋 ) ∈ 𝑆 )
33	32	3expa	⊢ ( ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) ∧ 𝑋 ∈ 𝑆 ) → ( - 𝑁 · 𝑋 ) ∈ 𝑆 )
34	33	an32s	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → ( - 𝑁 · 𝑋 ) ∈ 𝑆 )
35	34	3adantl2	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → ( - 𝑁 · 𝑋 ) ∈ 𝑆 )
36	28 31 35	rspcdva	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → ( 𝐼 ‘ ( - 𝑁 · 𝑋 ) ) ∈ 𝑆 )
37	26 36	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ - 𝑁 ∈ ℕ ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
38	37	adantrl	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )
39		elznn0nn	⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
40	15 39	sylib	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
41	14 38 40	mpjaodan	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) ∈ 𝑆 )