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 = {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$
Assertion	mulgnn0subcl	$⊢ (φ \land N \in ℕ_{0} \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	1 2 3 4 5 6	mulgnnsubcl	$⊢ (φ \land N \in ℕ \land X \in S) \to N \underset{˙}{\cdot} X \in S$
10	9	3expa	$⊢ ((φ \land N \in ℕ) \land X \in S) \to N \underset{˙}{\cdot} X \in S$
11	10	an32s	$⊢ ((φ \land X \in S) \land N \in ℕ) \to N \underset{˙}{\cdot} X \in S$
12	11	3adantl2	$⊢ ((φ \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to N \underset{˙}{\cdot} X \in S$
13		oveq1	$⊢ N = 0 \to N \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
14	5	3ad2ant1	$⊢ (φ \land N \in ℕ_{0} \land X \in S) \to S \subseteq B$
15		simp3	$⊢ (φ \land N \in ℕ_{0} \land X \in S) \to X \in S$
16	14 15	sseldd	$⊢ (φ \land N \in ℕ_{0} \land X \in S) \to X \in B$
17	1 7 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$
18	16 17	syl	$⊢ (φ \land N \in ℕ_{0} \land X \in S) \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$
19	13 18	sylan9eqr	$⊢ ((φ \land N \in ℕ_{0} \land X \in S) \land N = 0) \to N \underset{˙}{\cdot} X = \underset{˙}{0}$
20	8	3ad2ant1	$⊢ (φ \land N \in ℕ_{0} \land X \in S) \to \underset{˙}{0} \in S$
21	20	adantr	$⊢ ((φ \land N \in ℕ_{0} \land X \in S) \land N = 0) \to \underset{˙}{0} \in S$
22	19 21	eqeltrd	$⊢ ((φ \land N \in ℕ_{0} \land X \in S) \land N = 0) \to N \underset{˙}{\cdot} X \in S$
23		simp2	$⊢ (φ \land N \in ℕ_{0} \land X \in S) \to N \in ℕ_{0}$
24		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
25	23 24	sylib	$⊢ (φ \land N \in ℕ_{0} \land X \in S) \to (N \in ℕ \lor N = 0)$
26	12 22 25	mpjaodan	$⊢ (φ \land N \in ℕ_{0} \land X \in S) \to N \underset{˙}{\cdot} X \in S$

Metamath Proof Explorer

Theorem mulgnn0subcl

Proof