cycsubg2

Description: The subgroup generated by an element is exhausted by its multiples. (Contributed by Stefan O'Rear, 6-Sep-2015)

Step	Hyp	Ref	Expression
1		cycsubg2.x	$⊢ X = {Base}_{G}$
2		cycsubg2.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		cycsubg2.f	$⊢ F = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
4		cycsubg2.k	$⊢ K = mrCls (SubGrp (G))$
5		snssg	$⊢ A \in X \to (A \in y \leftrightarrow \{A\} \subseteq y)$
6	5	bicomd	$⊢ A \in X \to (\{A\} \subseteq y \leftrightarrow A \in y)$
7	6	adantl	$⊢ (G \in Grp \land A \in X) \to (\{A\} \subseteq y \leftrightarrow A \in y)$
8	7	rabbidv	$⊢ (G \in Grp \land A \in X) \to \{y \in SubGrp (G) \| \{A\} \subseteq y\} = \{y \in SubGrp (G) \| A \in y\}$
9	8	inteqd	$⊢ (G \in Grp \land A \in X) \to ⋂ \{y \in SubGrp (G) \| \{A\} \subseteq y\} = ⋂ \{y \in SubGrp (G) \| A \in y\}$
10	1	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS (X)$
11	10	acsmred	$⊢ G \in Grp \to SubGrp (G) \in Moore (X)$
12		snssi	$⊢ A \in X \to \{A\} \subseteq X$
13	4	mrcval	$⊢ (SubGrp (G) \in Moore (X) \land \{A\} \subseteq X) \to K (\{A\}) = ⋂ \{y \in SubGrp (G) \| \{A\} \subseteq y\}$
14	11 12 13	syl2an	$⊢ (G \in Grp \land A \in X) \to K (\{A\}) = ⋂ \{y \in SubGrp (G) \| \{A\} \subseteq y\}$
15	1 2 3	cycsubg	$⊢ (G \in Grp \land A \in X) \to ran F = ⋂ \{y \in SubGrp (G) \| A \in y\}$
16	9 14 15	3eqtr4d	$⊢ (G \in Grp \land A \in X) \to K (\{A\}) = ran F$

Metamath Proof Explorer