mulgsubcl

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

	Ref	Expression
Hypotheses	mulgnnsubcl.b	$⊢ B = {Base}_{G}$
	mulgnnsubcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgnnsubcl.p	$⊢ \underset{˙}{+} = +_{G}$
	mulgnnsubcl.g	$⊢ φ \to G \in V$
	mulgnnsubcl.s	$⊢ φ \to S \subseteq B$
	mulgnnsubcl.c	$⊢ (φ \land x \in S \land y \in S) \to x \underset{˙}{+} y \in S$
	mulgnn0subcl.z	$⊢ \underset{˙}{0} = 0_{G}$
	mulgnn0subcl.c	$⊢ φ \to \underset{˙}{0} \in S$
	mulgsubcl.i	$⊢ I = {inv}_{g} (G)$
	mulgsubcl.c	$⊢ (φ \land x \in S) \to I (x) \in S$
Assertion	mulgsubcl	$⊢ (φ \land N \in ℤ \land X \in S) \to N \underset{˙}{\cdot} X \in S$

Proof

Step	Hyp	Ref	Expression
1		mulgnnsubcl.b	$⊢ B = {Base}_{G}$
2		mulgnnsubcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgnnsubcl.p	$⊢ \underset{˙}{+} = +_{G}$
4		mulgnnsubcl.g	$⊢ φ \to G \in V$
5		mulgnnsubcl.s	$⊢ φ \to S \subseteq B$
6		mulgnnsubcl.c	$⊢ (φ \land x \in S \land y \in S) \to x \underset{˙}{+} y \in S$
7		mulgnn0subcl.z	$⊢ \underset{˙}{0} = 0_{G}$
8		mulgnn0subcl.c	$⊢ φ \to \underset{˙}{0} \in S$
9		mulgsubcl.i	$⊢ I = {inv}_{g} (G)$
10		mulgsubcl.c	$⊢ (φ \land x \in S) \to I (x) \in S$
11	1 2 3 4 5 6 7 8	mulgnn0subcl	$⊢ (φ \land N \in ℕ_{0} \land X \in S) \to N \underset{˙}{\cdot} X \in S$
12	11	3expa	$⊢ ((φ \land N \in ℕ_{0}) \land X \in S) \to N \underset{˙}{\cdot} X \in S$
13	12	an32s	$⊢ ((φ \land X \in S) \land N \in ℕ_{0}) \to N \underset{˙}{\cdot} X \in S$
14	13	3adantl2	$⊢ ((φ \land N \in ℤ \land X \in S) \land N \in ℕ_{0}) \to N \underset{˙}{\cdot} X \in S$
15		simp2	$⊢ (φ \land N \in ℤ \land X \in S) \to N \in ℤ$
16	15	adantr	$⊢ ((φ \land N \in ℤ \land X \in S) \land - N \in ℕ) \to N \in ℤ$
17	16	zcnd	$⊢ ((φ \land N \in ℤ \land X \in S) \land - N \in ℕ) \to N \in ℂ$
18	17	negnegd	$⊢ ((φ \land N \in ℤ \land X \in S) \land - N \in ℕ) \to - -N = N$
19	18	oveq1d	$⊢ ((φ \land N \in ℤ \land X \in S) \land - N \in ℕ) \to (- -N) \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$
20		id	$⊢ - N \in ℕ \to - N \in ℕ$
21	5	3ad2ant1	$⊢ (φ \land N \in ℤ \land X \in S) \to S \subseteq B$
22		simp3	$⊢ (φ \land N \in ℤ \land X \in S) \to X \in S$
23	21 22	sseldd	$⊢ (φ \land N \in ℤ \land X \in S) \to X \in B$
24	1 2 9	mulgnegnn	$⊢ (- N \in ℕ \land X \in B) \to (- -N) \underset{˙}{\cdot} X = I (-N \underset{˙}{\cdot} X)$
25	20 23 24	syl2anr	$⊢ ((φ \land N \in ℤ \land X \in S) \land - N \in ℕ) \to (- -N) \underset{˙}{\cdot} X = I (-N \underset{˙}{\cdot} X)$
26	19 25	eqtr3d	$⊢ ((φ \land N \in ℤ \land X \in S) \land - N \in ℕ) \to N \underset{˙}{\cdot} X = I (-N \underset{˙}{\cdot} X)$
27		fveq2	$⊢ x = -N \underset{˙}{\cdot} X \to I (x) = I (-N \underset{˙}{\cdot} X)$
28	27	eleq1d	$⊢ x = -N \underset{˙}{\cdot} X \to (I (x) \in S \leftrightarrow I (-N \underset{˙}{\cdot} X) \in S)$
29	10	ralrimiva	$⊢ φ \to \forall x \in S I (x) \in S$
30	29	3ad2ant1	$⊢ (φ \land N \in ℤ \land X \in S) \to \forall x \in S I (x) \in S$
31	30	adantr	$⊢ ((φ \land N \in ℤ \land X \in S) \land - N \in ℕ) \to \forall x \in S I (x) \in S$
32	1 2 3 4 5 6	mulgnnsubcl	$⊢ (φ \land - N \in ℕ \land X \in S) \to -N \underset{˙}{\cdot} X \in S$
33	32	3expa	$⊢ ((φ \land - N \in ℕ) \land X \in S) \to -N \underset{˙}{\cdot} X \in S$
34	33	an32s	$⊢ ((φ \land X \in S) \land - N \in ℕ) \to -N \underset{˙}{\cdot} X \in S$
35	34	3adantl2	$⊢ ((φ \land N \in ℤ \land X \in S) \land - N \in ℕ) \to -N \underset{˙}{\cdot} X \in S$
36	28 31 35	rspcdva	$⊢ ((φ \land N \in ℤ \land X \in S) \land - N \in ℕ) \to I (-N \underset{˙}{\cdot} X) \in S$
37	26 36	eqeltrd	$⊢ ((φ \land N \in ℤ \land X \in S) \land - N \in ℕ) \to N \underset{˙}{\cdot} X \in S$
38	37	adantrl	$⊢ ((φ \land N \in ℤ \land X \in S) \land (N \in ℝ \land - N \in ℕ)) \to N \underset{˙}{\cdot} X \in S$
39		elznn0nn	$⊢ N \in ℤ \leftrightarrow (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
40	15 39	sylib	$⊢ (φ \land N \in ℤ \land X \in S) \to (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
41	14 38 40	mpjaodan	$⊢ (φ \land N \in ℤ \land X \in S) \to N \underset{˙}{\cdot} X \in S$

Metamath Proof Explorer

Theorem mulgsubcl

Proof