odngen

Description: A cyclic subgroup of size ( OA ) has ( phi( OA ) ) generators. (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	odhash.x	$⊢ X = {Base}_{G}$
	odhash.o	$⊢ O = od (G)$
	odhash.k	$⊢ K = mrCls (SubGrp (G))$
Assertion	odngen	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \|\{x \in K (\{A\}) \| O (x) = O (A)\}\| = ϕ (O (A))$

Proof

Step	Hyp	Ref	Expression
1		odhash.x	$⊢ X = {Base}_{G}$
2		odhash.o	$⊢ O = od (G)$
3		odhash.k	$⊢ K = mrCls (SubGrp (G))$
4		eqid	$⊢ (y \in (0 ..^O (A)) ⟼ y \cdot_{G} A) = (y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)$
5	4	mptpreima	$⊢ {(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} [\{x \in K (\{A\}) \| O (x) = O (A)\}] = \{y \in (0 ..^O (A)) \| y \cdot_{G} A \in \{x \in K (\{A\}) \| O (x) = O (A)\}\}$
6	5	fveq2i	$⊢ \|{(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} [\{x \in K (\{A\}) \| O (x) = O (A)\}]\| = \|\{y \in (0 ..^O (A)) \| y \cdot_{G} A \in \{x \in K (\{A\}) \| O (x) = O (A)\}\}\|$
7		eqid	$⊢ \cdot_{G} = \cdot_{G}$
8	1 7 2 3	odf1o2	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to (y \in (0 ..^O (A)) ⟼ y \cdot_{G} A) : (0 ..^O (A)) \underset{1-1 onto}{⟶} K (\{A\})$
9		f1ocnv	$⊢ (y \in (0 ..^O (A)) ⟼ y \cdot_{G} A) : (0 ..^O (A)) \underset{1-1 onto}{⟶} K (\{A\}) \to {(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} : K (\{A\}) \underset{1-1 onto}{⟶} (0 ..^O (A))$
10		f1of1	$⊢ {(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} : K (\{A\}) \underset{1-1 onto}{⟶} (0 ..^O (A)) \to {(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} : K (\{A\}) \underset{1-1}{⟶} (0 ..^O (A))$
11	8 9 10	3syl	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to {(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} : K (\{A\}) \underset{1-1}{⟶} (0 ..^O (A))$
12		ssrab2	$⊢ \{x \in K (\{A\}) \| O (x) = O (A)\} \subseteq K (\{A\})$
13		fvex	$⊢ K (\{A\}) \in V$
14	13	rabex	$⊢ \{x \in K (\{A\}) \| O (x) = O (A)\} \in V$
15	14	f1imaen	$⊢ ({(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} : K (\{A\}) \underset{1-1}{⟶} (0 ..^O (A)) \land \{x \in K (\{A\}) \| O (x) = O (A)\} \subseteq K (\{A\})) \to {(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} [\{x \in K (\{A\}) \| O (x) = O (A)\}] \approx \{x \in K (\{A\}) \| O (x) = O (A)\}$
16		hasheni	$⊢ {(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} [\{x \in K (\{A\}) \| O (x) = O (A)\}] \approx \{x \in K (\{A\}) \| O (x) = O (A)\} \to \|{(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} [\{x \in K (\{A\}) \| O (x) = O (A)\}]\| = \|\{x \in K (\{A\}) \| O (x) = O (A)\}\|$
17	15 16	syl	$⊢ ({(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} : K (\{A\}) \underset{1-1}{⟶} (0 ..^O (A)) \land \{x \in K (\{A\}) \| O (x) = O (A)\} \subseteq K (\{A\})) \to \|{(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} [\{x \in K (\{A\}) \| O (x) = O (A)\}]\| = \|\{x \in K (\{A\}) \| O (x) = O (A)\}\|$
18	11 12 17	sylancl	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \|{(y \in (0 ..^O (A)) ⟼ y \cdot_{G} A)}^{-1} [\{x \in K (\{A\}) \| O (x) = O (A)\}]\| = \|\{x \in K (\{A\}) \| O (x) = O (A)\}\|$
19		simpl1	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in (0 ..^O (A))) \to G \in Grp$
20		simpl2	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in (0 ..^O (A))) \to A \in X$
21		elfzoelz	$⊢ y \in (0 ..^O (A)) \to y \in ℤ$
22	21	adantl	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in (0 ..^O (A))) \to y \in ℤ$
23	1 7 3	cycsubg2cl	$⊢ (G \in Grp \land A \in X \land y \in ℤ) \to y \cdot_{G} A \in K (\{A\})$
24	19 20 22 23	syl3anc	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in (0 ..^O (A))) \to y \cdot_{G} A \in K (\{A\})$
25		fveqeq2	$⊢ x = y \cdot_{G} A \to (O (x) = O (A) \leftrightarrow O (y \cdot_{G} A) = O (A))$
26	25	elrab3	$⊢ y \cdot_{G} A \in K (\{A\}) \to (y \cdot_{G} A \in \{x \in K (\{A\}) \| O (x) = O (A)\} \leftrightarrow O (y \cdot_{G} A) = O (A))$
27	24 26	syl	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in (0 ..^O (A))) \to (y \cdot_{G} A \in \{x \in K (\{A\}) \| O (x) = O (A)\} \leftrightarrow O (y \cdot_{G} A) = O (A))$
28		simpl3	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in (0 ..^O (A))) \to O (A) \in ℕ$
29	1 2 7	odmulgeq	$⊢ ((G \in Grp \land A \in X \land y \in ℤ) \land O (A) \in ℕ) \to (O (y \cdot_{G} A) = O (A) \leftrightarrow y \gcd O (A) = 1)$
30	19 20 22 28 29	syl31anc	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in (0 ..^O (A))) \to (O (y \cdot_{G} A) = O (A) \leftrightarrow y \gcd O (A) = 1)$
31	27 30	bitrd	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in (0 ..^O (A))) \to (y \cdot_{G} A \in \{x \in K (\{A\}) \| O (x) = O (A)\} \leftrightarrow y \gcd O (A) = 1)$
32	31	rabbidva	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \{y \in (0 ..^O (A)) \| y \cdot_{G} A \in \{x \in K (\{A\}) \| O (x) = O (A)\}\} = \{y \in (0 ..^O (A)) \| y \gcd O (A) = 1\}$
33	32	fveq2d	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \|\{y \in (0 ..^O (A)) \| y \cdot_{G} A \in \{x \in K (\{A\}) \| O (x) = O (A)\}\}\| = \|\{y \in (0 ..^O (A)) \| y \gcd O (A) = 1\}\|$
34		dfphi2	$⊢ O (A) \in ℕ \to ϕ (O (A)) = \|\{y \in (0 ..^O (A)) \| y \gcd O (A) = 1\}\|$
35	34	3ad2ant3	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to ϕ (O (A)) = \|\{y \in (0 ..^O (A)) \| y \gcd O (A) = 1\}\|$
36	33 35	eqtr4d	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \|\{y \in (0 ..^O (A)) \| y \cdot_{G} A \in \{x \in K (\{A\}) \| O (x) = O (A)\}\}\| = ϕ (O (A))$
37	6 18 36	3eqtr3a	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to \|\{x \in K (\{A\}) \| O (x) = O (A)\}\| = ϕ (O (A))$

Metamath Proof Explorer

Theorem odngen

Proof