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

Metamath Proof Explorer

Theorem cycsubggend

Description: The cyclic subgroup generated by A includes its generator. Although this theorem holds for any class G , the definition of F is only meaningful if G is a group. (Contributed by Rohan Ridenour, 3-Aug-2023)

		Ref	Expression
	Hypotheses	cycsubggend.1	$⊢ B = {Base}_{G}$
		cycsubggend.2	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
		cycsubggend.3	$⊢ F = (n \in ℤ ⟼ n \underset{˙}{\cdot} A)$
		cycsubggend.4	$⊢ φ \to A \in B$
	Assertion	cycsubggend	$⊢ φ \to A \in ran F$

Proof

Step	Hyp	Ref	Expression
1		cycsubggend.1	$⊢ B = {Base}_{G}$
2		cycsubggend.2	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		cycsubggend.3	$⊢ F = (n \in ℤ ⟼ n \underset{˙}{\cdot} A)$
4		cycsubggend.4	$⊢ φ \to A \in B$
5		1zzd	$⊢ φ \to 1 \in ℤ$
6		simpr	$⊢ (φ \land n = 1) \to n = 1$
7	6	oveq1d	$⊢ (φ \land n = 1) \to n \underset{˙}{\cdot} A = 1 \underset{˙}{\cdot} A$
8	4	adantr	$⊢ (φ \land n = 1) \to A \in B$
9	1 2	mulg1	$⊢ A \in B \to 1 \underset{˙}{\cdot} A = A$
10	8 9	syl	$⊢ (φ \land n = 1) \to 1 \underset{˙}{\cdot} A = A$
11	7 10	eqtr2d	$⊢ (φ \land n = 1) \to A = n \underset{˙}{\cdot} A$
12	3 5 4 11	elrnmptdv	$⊢ φ \to A \in ran F$