dfod2

Description: An alternative definition of the order of a group element is as the cardinality of the cyclic subgroup generated by the element. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	odf1.1	$⊢ X = {Base}_{G}$
	odf1.2	$⊢ O = od (G)$
	odf1.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	odf1.4	$⊢ F = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
Assertion	dfod2	$⊢ (G \in Grp \land A \in X) \to O (A) = if (ran F \in Fin, \|ran F\|, 0)$

Proof

Step	Hyp	Ref	Expression
1		odf1.1	$⊢ X = {Base}_{G}$
2		odf1.2	$⊢ O = od (G)$
3		odf1.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		odf1.4	$⊢ F = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
5		fzfid	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to (0 \dots O (A) - 1) \in Fin$
6	1 3	mulgcl	$⊢ (G \in Grp \land x \in ℤ \land A \in X) \to x \underset{˙}{\cdot} A \in X$
7	6	3expa	$⊢ ((G \in Grp \land x \in ℤ) \land A \in X) \to x \underset{˙}{\cdot} A \in X$
8	7	an32s	$⊢ ((G \in Grp \land A \in X) \land x \in ℤ) \to x \underset{˙}{\cdot} A \in X$
9	8	adantlr	$⊢ (((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \to x \underset{˙}{\cdot} A \in X$
10	9 4	fmptd	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to F : ℤ ⟶ X$
11		frn	$⊢ F : ℤ ⟶ X \to ran F \subseteq X$
12	1	fvexi	$⊢ X \in V$
13	12	ssex	$⊢ ran F \subseteq X \to ran F \in V$
14	10 11 13	3syl	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to ran F \in V$
15		elfzelz	$⊢ y \in (0 \dots O (A) - 1) \to y \in ℤ$
16	15	adantl	$⊢ (((G \in Grp \land A \in X) \land O (A) \in ℕ) \land y \in (0 \dots O (A) - 1)) \to y \in ℤ$
17		ovex	$⊢ y \underset{˙}{\cdot} A \in V$
18		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A$
19	4 18	elrnmpt1s	$⊢ (y \in ℤ \land y \underset{˙}{\cdot} A \in V) \to y \underset{˙}{\cdot} A \in ran F$
20	16 17 19	sylancl	$⊢ (((G \in Grp \land A \in X) \land O (A) \in ℕ) \land y \in (0 \dots O (A) - 1)) \to y \underset{˙}{\cdot} A \in ran F$
21	20	ralrimiva	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to \forall y \in (0 \dots O (A) - 1) y \underset{˙}{\cdot} A \in ran F$
22		zmodfz	$⊢ (x \in ℤ \land O (A) \in ℕ) \to x \mod O (A) \in (0 \dots O (A) - 1)$
23	22	ancoms	$⊢ (O (A) \in ℕ \land x \in ℤ) \to x \mod O (A) \in (0 \dots O (A) - 1)$
24	23	adantll	$⊢ (((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \to x \mod O (A) \in (0 \dots O (A) - 1)$
25		simpllr	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to O (A) \in ℕ$
26		simplr	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to x \in ℤ$
27	15	adantl	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to y \in ℤ$
28		moddvds	$⊢ (O (A) \in ℕ \land x \in ℤ \land y \in ℤ) \to (x \mod O (A) = y \mod O (A) \leftrightarrow O (A) ∥ (x - y))$
29	25 26 27 28	syl3anc	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to (x \mod O (A) = y \mod O (A) \leftrightarrow O (A) ∥ (x - y))$
30	27	zred	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to y \in ℝ$
31	25	nnrpd	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to O (A) \in ℝ^{+}$
32		0z	$⊢ 0 \in ℤ$
33		nnz	$⊢ O (A) \in ℕ \to O (A) \in ℤ$
34	33	adantl	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to O (A) \in ℤ$
35	34	adantr	$⊢ (((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \to O (A) \in ℤ$
36		elfzm11	$⊢ (0 \in ℤ \land O (A) \in ℤ) \to (y \in (0 \dots O (A) - 1) \leftrightarrow (y \in ℤ \land 0 \leq y \land y < O (A)))$
37	32 35 36	sylancr	$⊢ (((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \to (y \in (0 \dots O (A) - 1) \leftrightarrow (y \in ℤ \land 0 \leq y \land y < O (A)))$
38	37	biimpa	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to (y \in ℤ \land 0 \leq y \land y < O (A))$
39	38	simp2d	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to 0 \leq y$
40	38	simp3d	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to y < O (A)$
41		modid	$⊢ ((y \in ℝ \land O (A) \in ℝ^{+}) \land (0 \leq y \land y < O (A))) \to y \mod O (A) = y$
42	30 31 39 40 41	syl22anc	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to y \mod O (A) = y$
43	42	eqeq2d	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to (x \mod O (A) = y \mod O (A) \leftrightarrow x \mod O (A) = y)$
44		eqcom	$⊢ x \mod O (A) = y \leftrightarrow y = x \mod O (A)$
45	43 44	bitrdi	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to (x \mod O (A) = y \mod O (A) \leftrightarrow y = x \mod O (A))$
46		simp-4l	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to G \in Grp$
47		simp-4r	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to A \in X$
48		eqid	$⊢ 0_{G} = 0_{G}$
49	1 2 3 48	odcong	$⊢ (G \in Grp \land A \in X \land (x \in ℤ \land y \in ℤ)) \to (O (A) ∥ (x - y) \leftrightarrow x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A)$
50	46 47 26 27 49	syl112anc	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to (O (A) ∥ (x - y) \leftrightarrow x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A)$
51	29 45 50	3bitr3rd	$⊢ ((((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \land y \in (0 \dots O (A) - 1)) \to (x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A \leftrightarrow y = x \mod O (A))$
52	51	ralrimiva	$⊢ (((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \to \forall y \in (0 \dots O (A) - 1) (x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A \leftrightarrow y = x \mod O (A))$
53		reu6i	$⊢ (x \mod O (A) \in (0 \dots O (A) - 1) \land \forall y \in (0 \dots O (A) - 1) (x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A \leftrightarrow y = x \mod O (A))) \to \exists! y \in (0 \dots O (A) - 1) x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A$
54	24 52 53	syl2anc	$⊢ (((G \in Grp \land A \in X) \land O (A) \in ℕ) \land x \in ℤ) \to \exists! y \in (0 \dots O (A) - 1) x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A$
55	54	ralrimiva	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to \forall x \in ℤ \exists! y \in (0 \dots O (A) - 1) x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A$
56		ovex	$⊢ x \underset{˙}{\cdot} A \in V$
57	56	rgenw	$⊢ \forall x \in ℤ x \underset{˙}{\cdot} A \in V$
58		eqeq1	$⊢ z = x \underset{˙}{\cdot} A \to (z = y \underset{˙}{\cdot} A \leftrightarrow x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A)$
59	58	reubidv	$⊢ z = x \underset{˙}{\cdot} A \to (\exists! y \in (0 \dots O (A) - 1) z = y \underset{˙}{\cdot} A \leftrightarrow \exists! y \in (0 \dots O (A) - 1) x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A)$
60	4 59	ralrnmptw	$⊢ \forall x \in ℤ x \underset{˙}{\cdot} A \in V \to (\forall z \in ran F \exists! y \in (0 \dots O (A) - 1) z = y \underset{˙}{\cdot} A \leftrightarrow \forall x \in ℤ \exists! y \in (0 \dots O (A) - 1) x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A)$
61	57 60	ax-mp	$⊢ \forall z \in ran F \exists! y \in (0 \dots O (A) - 1) z = y \underset{˙}{\cdot} A \leftrightarrow \forall x \in ℤ \exists! y \in (0 \dots O (A) - 1) x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A$
62	55 61	sylibr	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to \forall z \in ran F \exists! y \in (0 \dots O (A) - 1) z = y \underset{˙}{\cdot} A$
63		eqid	$⊢ (y \in (0 \dots O (A) - 1) ⟼ y \underset{˙}{\cdot} A) = (y \in (0 \dots O (A) - 1) ⟼ y \underset{˙}{\cdot} A)$
64	63	f1ompt	$⊢ (y \in (0 \dots O (A) - 1) ⟼ y \underset{˙}{\cdot} A) : (0 \dots O (A) - 1) \underset{1-1 onto}{⟶} ran F \leftrightarrow (\forall y \in (0 \dots O (A) - 1) y \underset{˙}{\cdot} A \in ran F \land \forall z \in ran F \exists! y \in (0 \dots O (A) - 1) z = y \underset{˙}{\cdot} A)$
65	21 62 64	sylanbrc	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to (y \in (0 \dots O (A) - 1) ⟼ y \underset{˙}{\cdot} A) : (0 \dots O (A) - 1) \underset{1-1 onto}{⟶} ran F$
66		f1oen2g	$⊢ ((0 \dots O (A) - 1) \in Fin \land ran F \in V \land (y \in (0 \dots O (A) - 1) ⟼ y \underset{˙}{\cdot} A) : (0 \dots O (A) - 1) \underset{1-1 onto}{⟶} ran F) \to (0 \dots O (A) - 1) \approx ran F$
67	5 14 65 66	syl3anc	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to (0 \dots O (A) - 1) \approx ran F$
68		enfi	$⊢ (0 \dots O (A) - 1) \approx ran F \to ((0 \dots O (A) - 1) \in Fin \leftrightarrow ran F \in Fin)$
69	67 68	syl	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to ((0 \dots O (A) - 1) \in Fin \leftrightarrow ran F \in Fin)$
70	5 69	mpbid	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to ran F \in Fin$
71	70	iftrued	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to if (ran F \in Fin, \|ran F\|, 0) = \|ran F\|$
72		fz01en	$⊢ O (A) \in ℤ \to (0 \dots O (A) - 1) \approx (1 \dots O (A))$
73		ensym	$⊢ (0 \dots O (A) - 1) \approx (1 \dots O (A)) \to (1 \dots O (A)) \approx (0 \dots O (A) - 1)$
74	34 72 73	3syl	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to (1 \dots O (A)) \approx (0 \dots O (A) - 1)$
75		entr	$⊢ ((1 \dots O (A)) \approx (0 \dots O (A) - 1) \land (0 \dots O (A) - 1) \approx ran F) \to (1 \dots O (A)) \approx ran F$
76	74 67 75	syl2anc	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to (1 \dots O (A)) \approx ran F$
77		fzfid	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to (1 \dots O (A)) \in Fin$
78		hashen	$⊢ ((1 \dots O (A)) \in Fin \land ran F \in Fin) \to (\|(1 \dots O (A))\| = \|ran F\| \leftrightarrow (1 \dots O (A)) \approx ran F)$
79	77 70 78	syl2anc	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to (\|(1 \dots O (A))\| = \|ran F\| \leftrightarrow (1 \dots O (A)) \approx ran F)$
80	76 79	mpbird	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to \|(1 \dots O (A))\| = \|ran F\|$
81		nnnn0	$⊢ O (A) \in ℕ \to O (A) \in ℕ_{0}$
82	81	adantl	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to O (A) \in ℕ_{0}$
83		hashfz1	$⊢ O (A) \in ℕ_{0} \to \|(1 \dots O (A))\| = O (A)$
84	82 83	syl	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to \|(1 \dots O (A))\| = O (A)$
85	71 80 84	3eqtr2rd	$⊢ ((G \in Grp \land A \in X) \land O (A) \in ℕ) \to O (A) = if (ran F \in Fin, \|ran F\|, 0)$
86		simp3	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to O (A) = 0$
87	1 2 3 4	odinf	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to \neg ran F \in Fin$
88	87	iffalsed	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to if (ran F \in Fin, \|ran F\|, 0) = 0$
89	86 88	eqtr4d	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to O (A) = if (ran F \in Fin, \|ran F\|, 0)$
90	89	3expa	$⊢ ((G \in Grp \land A \in X) \land O (A) = 0) \to O (A) = if (ran F \in Fin, \|ran F\|, 0)$
91	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
92	91	adantl	$⊢ (G \in Grp \land A \in X) \to O (A) \in ℕ_{0}$
93		elnn0	$⊢ O (A) \in ℕ_{0} \leftrightarrow (O (A) \in ℕ \lor O (A) = 0)$
94	92 93	sylib	$⊢ (G \in Grp \land A \in X) \to (O (A) \in ℕ \lor O (A) = 0)$
95	85 90 94	mpjaodan	$⊢ (G \in Grp \land A \in X) \to O (A) = if (ran F \in Fin, \|ran F\|, 0)$

Metamath Proof Explorer

Theorem dfod2

Proof