This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cycsubgss

Description: The cyclic subgroup generated by an element A is a subset of any subgroup containing A . (Contributed by Mario Carneiro, 13-Jan-2015)

		Ref	Expression
	Hypotheses	cycsubg.x	$⊢ X = {Base}_{G}$
		cycsubg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
		cycsubg.f	$⊢ F = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
	Assertion	cycsubgss	$⊢ (S \in SubGrp (G) \land A \in S) \to ran F \subseteq S$

Proof

Step	Hyp	Ref	Expression
1		cycsubg.x	$⊢ X = {Base}_{G}$
2		cycsubg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		cycsubg.f	$⊢ F = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
4	2	subgmulgcl	$⊢ (S \in SubGrp (G) \land x \in ℤ \land A \in S) \to x \underset{˙}{\cdot} A \in S$
5	4	3expa	$⊢ ((S \in SubGrp (G) \land x \in ℤ) \land A \in S) \to x \underset{˙}{\cdot} A \in S$
6	5	an32s	$⊢ ((S \in SubGrp (G) \land A \in S) \land x \in ℤ) \to x \underset{˙}{\cdot} A \in S$
7	6 3	fmptd	$⊢ (S \in SubGrp (G) \land A \in S) \to F : ℤ ⟶ S$
8	7	frnd	$⊢ (S \in SubGrp (G) \land A \in S) \to ran F \subseteq S$