cycsubg2cl

Description: Any multiple of an element is contained in the generated cyclic subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	cycsubg2cl.x	$⊢ X = {Base}_{G}$
	cycsubg2cl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	cycsubg2cl.k	$⊢ K = mrCls (SubGrp (G))$
Assertion	cycsubg2cl	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to N \underset{˙}{\cdot} A \in K (\{A\})$

Step	Hyp	Ref	Expression
1		cycsubg2cl.x	$⊢ X = {Base}_{G}$
2		cycsubg2cl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		cycsubg2cl.k	$⊢ K = mrCls (SubGrp (G))$
4	1	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS (X)$
5	4	acsmred	$⊢ G \in Grp \to SubGrp (G) \in Moore (X)$
6	5	3ad2ant1	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to SubGrp (G) \in Moore (X)$
7		simp2	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to A \in X$
8	7	snssd	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to \{A\} \subseteq X$
9	3	mrccl	$⊢ (SubGrp (G) \in Moore (X) \land \{A\} \subseteq X) \to K (\{A\}) \in SubGrp (G)$
10	6 8 9	syl2anc	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to K (\{A\}) \in SubGrp (G)$
11		simp3	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to N \in ℤ$
12	6 3 8	mrcssidd	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to \{A\} \subseteq K (\{A\})$
13		snssg	$⊢ A \in X \to (A \in K (\{A\}) \leftrightarrow \{A\} \subseteq K (\{A\}))$
14	13	3ad2ant2	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to (A \in K (\{A\}) \leftrightarrow \{A\} \subseteq K (\{A\}))$
15	12 14	mpbird	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to A \in K (\{A\})$
16	2	subgmulgcl	$⊢ (K (\{A\}) \in SubGrp (G) \land N \in ℤ \land A \in K (\{A\})) \to N \underset{˙}{\cdot} A \in K (\{A\})$
17	10 11 15 16	syl3anc	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to N \underset{˙}{\cdot} A \in K (\{A\})$

Metamath Proof Explorer