mulgnnsubcl

Description: Closure of the group multiple (exponentiation) operation in a subsemigroup. (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$
Assertion	mulgnnsubcl	$⊢ (φ \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		simp2	$⊢ (φ \land N \in ℕ \land X \in S) \to N \in ℕ$
8	5	3ad2ant1	$⊢ (φ \land N \in ℕ \land X \in S) \to S \subseteq B$
9		simp3	$⊢ (φ \land N \in ℕ \land X \in S) \to X \in S$
10	8 9	sseldd	$⊢ (φ \land N \in ℕ \land X \in S) \to X \in B$
11		eqid	$⊢ seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) = seq 1 (\underset{˙}{+}, (ℕ \times \{X\}))$
12	1 3 2 11	mulgnn	$⊢ (N \in ℕ \land X \in B) \to N \underset{˙}{\cdot} X = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (N)$
13	7 10 12	syl2anc	$⊢ (φ \land N \in ℕ \land X \in S) \to N \underset{˙}{\cdot} X = seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (N)$
14		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
15	7 14	eleqtrdi	$⊢ (φ \land N \in ℕ \land X \in S) \to N \in ℤ_{\geq 1}$
16		elfznn	$⊢ x \in (1 \dots N) \to x \in ℕ$
17		fvconst2g	$⊢ (X \in S \land x \in ℕ) \to (ℕ \times \{X\}) (x) = X$
18	9 16 17	syl2an	$⊢ ((φ \land N \in ℕ \land X \in S) \land x \in (1 \dots N)) \to (ℕ \times \{X\}) (x) = X$
19		simpl3	$⊢ ((φ \land N \in ℕ \land X \in S) \land x \in (1 \dots N)) \to X \in S$
20	18 19	eqeltrd	$⊢ ((φ \land N \in ℕ \land X \in S) \land x \in (1 \dots N)) \to (ℕ \times \{X\}) (x) \in S$
21	6	3expb	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
22	21	3ad2antl1	$⊢ ((φ \land N \in ℕ \land X \in S) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
23	15 20 22	seqcl	$⊢ (φ \land N \in ℕ \land X \in S) \to seq 1 (\underset{˙}{+}, (ℕ \times \{X\})) (N) \in S$
24	13 23	eqeltrd	$⊢ (φ \land N \in ℕ \land X \in S) \to N \underset{˙}{\cdot} X \in S$

Metamath Proof Explorer

Theorem mulgnnsubcl

Proof