odf1o2

Description: An element with nonzero order has as many multiples as its order. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	odf1o1.x	$⊢ X = {Base}_{G}$
	odf1o1.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	odf1o1.o	$⊢ O = od (G)$
	odf1o1.k	$⊢ K = mrCls (SubGrp (G))$
Assertion	odf1o2	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) \underset{1-1 onto}{⟶} K (\{A\})$

Proof

Step	Hyp	Ref	Expression
1		odf1o1.x	$⊢ X = {Base}_{G}$
2		odf1o1.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		odf1o1.o	$⊢ O = od (G)$
4		odf1o1.k	$⊢ K = mrCls (SubGrp (G))$
5		simpl1	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land x \in (0 ..^O (A))) \to G \in Grp$
6		elfzoelz	$⊢ x \in (0 ..^O (A)) \to x \in ℤ$
7	6	adantl	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land x \in (0 ..^O (A))) \to x \in ℤ$
8		simpl2	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land x \in (0 ..^O (A))) \to A \in X$
9	1 2	mulgcl	$⊢ (G \in Grp \land x \in ℤ \land A \in X) \to x \underset{˙}{\cdot} A \in X$
10	5 7 8 9	syl3anc	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land x \in (0 ..^O (A))) \to x \underset{˙}{\cdot} A \in X$
11	10	ex	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to (x \in (0 ..^O (A)) \to x \underset{˙}{\cdot} A \in X)$
12		simpl3	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to O (A) \in ℕ$
13	12	nncnd	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to O (A) \in ℂ$
14	13	subid1d	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to O (A) - 0 = O (A)$
15	14	breq1d	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to ((O (A) - 0) ∥ (x - y) \leftrightarrow O (A) ∥ (x - y))$
16		fzocongeq	$⊢ (x \in (0 ..^O (A)) \land y \in (0 ..^O (A))) \to ((O (A) - 0) ∥ (x - y) \leftrightarrow x = y)$
17	16	adantl	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to ((O (A) - 0) ∥ (x - y) \leftrightarrow x = y)$
18		simpl1	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to G \in Grp$
19		simpl2	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to A \in X$
20	6	ad2antrl	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to x \in ℤ$
21		elfzoelz	$⊢ y \in (0 ..^O (A)) \to y \in ℤ$
22	21	ad2antll	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to y \in ℤ$
23		eqid	$⊢ 0_{G} = 0_{G}$
24	1 3 2 23	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)$
25	18 19 20 22 24	syl112anc	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to (O (A) ∥ (x - y) \leftrightarrow x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A)$
26	15 17 25	3bitr3rd	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land (x \in (0 ..^O (A)) \land y \in (0 ..^O (A)))) \to (x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A \leftrightarrow x = y)$
27	26	ex	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to ((x \in (0 ..^O (A)) \land y \in (0 ..^O (A))) \to (x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A \leftrightarrow x = y))$
28	11 27	dom2lem	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) \underset{1-1}{⟶} X$
29		f1fn	$⊢ (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) \underset{1-1}{⟶} X \to (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) Fn (0 ..^O (A))$
30	28 29	syl	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) Fn (0 ..^O (A))$
31		resss	$⊢ {(x \in ℤ ⟼ x \underset{˙}{\cdot} A) ↾}_{(0 ..^O (A))} \subseteq (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
32	6	ssriv	$⊢ (0 ..^O (A)) \subseteq ℤ$
33		resmpt	$⊢ (0 ..^O (A)) \subseteq ℤ \to {(x \in ℤ ⟼ x \underset{˙}{\cdot} A) ↾}_{(0 ..^O (A))} = (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A)$
34	32 33	ax-mp	$⊢ {(x \in ℤ ⟼ x \underset{˙}{\cdot} A) ↾}_{(0 ..^O (A))} = (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A)$
35		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A$
36	35	cbvmptv	$⊢ (x \in ℤ ⟼ x \underset{˙}{\cdot} A) = (y \in ℤ ⟼ y \underset{˙}{\cdot} A)$
37	31 34 36	3sstr3i	$⊢ (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) \subseteq (y \in ℤ ⟼ y \underset{˙}{\cdot} A)$
38		rnss	$⊢ (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) \subseteq (y \in ℤ ⟼ y \underset{˙}{\cdot} A) \to ran (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) \subseteq ran (y \in ℤ ⟼ y \underset{˙}{\cdot} A)$
39	37 38	mp1i	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to ran (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) \subseteq ran (y \in ℤ ⟼ y \underset{˙}{\cdot} A)$
40		simpr	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in ℤ) \to y \in ℤ$
41		simpl3	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in ℤ) \to O (A) \in ℕ$
42		zmodfzo	$⊢ (y \in ℤ \land O (A) \in ℕ) \to y \mod O (A) \in (0 ..^O (A))$
43	40 41 42	syl2anc	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in ℤ) \to y \mod O (A) \in (0 ..^O (A))$
44	1 3 2 23	odmod	$⊢ ((G \in Grp \land A \in X \land y \in ℤ) \land O (A) \in ℕ) \to (y \mod O (A)) \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A$
45	44	3an1rs	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in ℤ) \to (y \mod O (A)) \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A$
46	45	eqcomd	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in ℤ) \to y \underset{˙}{\cdot} A = (y \mod O (A)) \underset{˙}{\cdot} A$
47		oveq1	$⊢ x = y \mod O (A) \to x \underset{˙}{\cdot} A = (y \mod O (A)) \underset{˙}{\cdot} A$
48	47	rspceeqv	$⊢ (y \mod O (A) \in (0 ..^O (A)) \land y \underset{˙}{\cdot} A = (y \mod O (A)) \underset{˙}{\cdot} A) \to \exists x \in (0 ..^O (A)) y \underset{˙}{\cdot} A = x \underset{˙}{\cdot} A$
49	43 46 48	syl2anc	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in ℤ) \to \exists x \in (0 ..^O (A)) y \underset{˙}{\cdot} A = x \underset{˙}{\cdot} A$
50		ovex	$⊢ y \underset{˙}{\cdot} A \in V$
51		eqid	$⊢ (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) = (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A)$
52	51	elrnmpt	$⊢ y \underset{˙}{\cdot} A \in V \to (y \underset{˙}{\cdot} A \in ran (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) \leftrightarrow \exists x \in (0 ..^O (A)) y \underset{˙}{\cdot} A = x \underset{˙}{\cdot} A)$
53	50 52	ax-mp	$⊢ y \underset{˙}{\cdot} A \in ran (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) \leftrightarrow \exists x \in (0 ..^O (A)) y \underset{˙}{\cdot} A = x \underset{˙}{\cdot} A$
54	49 53	sylibr	$⊢ ((G \in Grp \land A \in X \land O (A) \in ℕ) \land y \in ℤ) \to y \underset{˙}{\cdot} A \in ran (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A)$
55	54	fmpttd	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to (y \in ℤ ⟼ y \underset{˙}{\cdot} A) : ℤ ⟶ ran (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A)$
56	55	frnd	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to ran (y \in ℤ ⟼ y \underset{˙}{\cdot} A) \subseteq ran (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A)$
57	39 56	eqssd	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to ran (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) = ran (y \in ℤ ⟼ y \underset{˙}{\cdot} A)$
58		eqid	$⊢ (y \in ℤ ⟼ y \underset{˙}{\cdot} A) = (y \in ℤ ⟼ y \underset{˙}{\cdot} A)$
59	1 2 58 4	cycsubg2	$⊢ (G \in Grp \land A \in X) \to K (\{A\}) = ran (y \in ℤ ⟼ y \underset{˙}{\cdot} A)$
60	59	3adant3	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to K (\{A\}) = ran (y \in ℤ ⟼ y \underset{˙}{\cdot} A)$
61	57 60	eqtr4d	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to ran (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) = K (\{A\})$
62		df-fo	$⊢ (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) \underset{onto}{⟶} K (\{A\}) \leftrightarrow ((x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) Fn (0 ..^O (A)) \land ran (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) = K (\{A\}))$
63	30 61 62	sylanbrc	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) \underset{onto}{⟶} K (\{A\})$
64		df-f1	$⊢ (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) \underset{1-1}{⟶} X \leftrightarrow ((x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) ⟶ X \land Fun {(x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A)}^{-1})$
65	64	simprbi	$⊢ (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) \underset{1-1}{⟶} X \to Fun {(x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A)}^{-1}$
66	28 65	syl	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to Fun {(x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A)}^{-1}$
67		dff1o3	$⊢ (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) \underset{1-1 onto}{⟶} K (\{A\}) \leftrightarrow ((x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) \underset{onto}{⟶} K (\{A\}) \land Fun {(x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A)}^{-1})$
68	63 66 67	sylanbrc	$⊢ (G \in Grp \land A \in X \land O (A) \in ℕ) \to (x \in (0 ..^O (A)) ⟼ x \underset{˙}{\cdot} A) : (0 ..^O (A)) \underset{1-1 onto}{⟶} K (\{A\})$

Metamath Proof Explorer

Theorem odf1o2

Proof