cycsubg

Description: The cyclic group generated by A is the smallest 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	cycsubg	$⊢ (G \in Grp \land A \in X) \to ran F = ⋂ \{s \in SubGrp (G) \| A \in s\}$

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		ssintab	$⊢ ran F \subseteq ⋂ \{s \| (s \in SubGrp (G) \land A \in s)\} \leftrightarrow \forall s ((s \in SubGrp (G) \land A \in s) \to ran F \subseteq s)$
5	1 2 3	cycsubgss	$⊢ (s \in SubGrp (G) \land A \in s) \to ran F \subseteq s$
6	4 5	mpgbir	$⊢ ran F \subseteq ⋂ \{s \| (s \in SubGrp (G) \land A \in s)\}$
7		df-rab	$⊢ \{s \in SubGrp (G) \| A \in s\} = \{s \| (s \in SubGrp (G) \land A \in s)\}$
8	7	inteqi	$⊢ ⋂ \{s \in SubGrp (G) \| A \in s\} = ⋂ \{s \| (s \in SubGrp (G) \land A \in s)\}$
9	6 8	sseqtrri	$⊢ ran F \subseteq ⋂ \{s \in SubGrp (G) \| A \in s\}$
10	9	a1i	$⊢ (G \in Grp \land A \in X) \to ran F \subseteq ⋂ \{s \in SubGrp (G) \| A \in s\}$
11	1 2 3	cycsubgcl	$⊢ (G \in Grp \land A \in X) \to (ran F \in SubGrp (G) \land A \in ran F)$
12		eleq2	$⊢ s = ran F \to (A \in s \leftrightarrow A \in ran F)$
13	12	elrab	$⊢ ran F \in \{s \in SubGrp (G) \| A \in s\} \leftrightarrow (ran F \in SubGrp (G) \land A \in ran F)$
14	11 13	sylibr	$⊢ (G \in Grp \land A \in X) \to ran F \in \{s \in SubGrp (G) \| A \in s\}$
15		intss1	$⊢ ran F \in \{s \in SubGrp (G) \| A \in s\} \to ⋂ \{s \in SubGrp (G) \| A \in s\} \subseteq ran F$
16	14 15	syl	$⊢ (G \in Grp \land A \in X) \to ⋂ \{s \in SubGrp (G) \| A \in s\} \subseteq ran F$
17	10 16	eqssd	$⊢ (G \in Grp \land A \in X) \to ran F = ⋂ \{s \in SubGrp (G) \| A \in s\}$

Metamath Proof Explorer