cyggenod

Description: An element is the generator of a finite group iff the order of the generator equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	iscyg.1	$⊢ B = {Base}_{G}$
	iscyg.2	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	iscyg3.e	$⊢ E = \{x \in B \| ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = B\}$
	cyggenod.o	$⊢ O = od (G)$
Assertion	cyggenod	$⊢ (G \in Grp \land B \in Fin) \to (X \in E \leftrightarrow (X \in B \land O (X) = \|B\|))$

Proof

Step	Hyp	Ref	Expression
1		iscyg.1	$⊢ B = {Base}_{G}$
2		iscyg.2	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		iscyg3.e	$⊢ E = \{x \in B \| ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = B\}$
4		cyggenod.o	$⊢ O = od (G)$
5	1 2 3	iscyggen	$⊢ X \in E \leftrightarrow (X \in B \land ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B)$
6		simplr	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to B \in Fin$
7		simplll	$⊢ (((G \in Grp \land B \in Fin) \land X \in B) \land n \in ℤ) \to G \in Grp$
8		simpr	$⊢ (((G \in Grp \land B \in Fin) \land X \in B) \land n \in ℤ) \to n \in ℤ$
9		simplr	$⊢ (((G \in Grp \land B \in Fin) \land X \in B) \land n \in ℤ) \to X \in B$
10	1 2	mulgcl	$⊢ (G \in Grp \land n \in ℤ \land X \in B) \to n \underset{˙}{\cdot} X \in B$
11	7 8 9 10	syl3anc	$⊢ (((G \in Grp \land B \in Fin) \land X \in B) \land n \in ℤ) \to n \underset{˙}{\cdot} X \in B$
12	11	fmpttd	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to (n \in ℤ ⟼ n \underset{˙}{\cdot} X) : ℤ ⟶ B$
13	12	frnd	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \subseteq B$
14	6 13	ssfid	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \in Fin$
15		hashen	$⊢ (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \in Fin \land B \in Fin) \to (\|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\| = \|B\| \leftrightarrow ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \approx B)$
16	14 6 15	syl2anc	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to (\|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\| = \|B\| \leftrightarrow ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \approx B)$
17		eqid	$⊢ (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = (n \in ℤ ⟼ n \underset{˙}{\cdot} X)$
18	1 4 2 17	dfod2	$⊢ (G \in Grp \land X \in B) \to O (X) = if (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \in Fin, \|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\|, 0)$
19	18	adantlr	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to O (X) = if (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \in Fin, \|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\|, 0)$
20	14	iftrued	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to if (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \in Fin, \|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\|, 0) = \|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\|$
21	19 20	eqtr2d	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to \|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\| = O (X)$
22	21	eqeq1d	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to (\|ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X)\| = \|B\| \leftrightarrow O (X) = \|B\|)$
23		fisseneq	$⊢ (B \in Fin \land ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \subseteq B \land ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \approx B) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B$
24	23	3expia	$⊢ (B \in Fin \land ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \subseteq B) \to (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \approx B \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B)$
25		enrefg	$⊢ B \in Fin \to B \approx B$
26	25	adantr	$⊢ (B \in Fin \land ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \subseteq B) \to B \approx B$
27		breq1	$⊢ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B \to (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \approx B \leftrightarrow B \approx B)$
28	26 27	syl5ibrcom	$⊢ (B \in Fin \land ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \subseteq B) \to (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \approx B)$
29	24 28	impbid	$⊢ (B \in Fin \land ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \subseteq B) \to (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \approx B \leftrightarrow ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B)$
30	6 13 29	syl2anc	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) \approx B \leftrightarrow ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B)$
31	16 22 30	3bitr3rd	$⊢ ((G \in Grp \land B \in Fin) \land X \in B) \to (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B \leftrightarrow O (X) = \|B\|)$
32	31	pm5.32da	$⊢ (G \in Grp \land B \in Fin) \to ((X \in B \land ran (n \in ℤ ⟼ n \underset{˙}{\cdot} X) = B) \leftrightarrow (X \in B \land O (X) = \|B\|))$
33	5 32	bitrid	$⊢ (G \in Grp \land B \in Fin) \to (X \in E \leftrightarrow (X \in B \land O (X) = \|B\|))$

Metamath Proof Explorer

Theorem cyggenod

Proof