Metamath Proof Explorer


Theorem 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 · ˙ = G
odf1o1.o O = od G
odf1o1.k K = mrCls SubGrp G
Assertion odf1o2 G Grp A X O A x 0 ..^ O A x · ˙ A : 0 ..^ O A 1-1 onto K A

Proof

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