This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- .x. = ( .g ` G )
odf1o1.o 
|- O = ( od ` G )
odf1o1.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
Assertion odf1o2 
|- ( ( G e. Grp /\ A e. X /\ ( O ` A ) e. NN ) -> ( x e. ( 0 ..^ ( O ` A ) ) |-> ( x .x. A ) ) : ( 0 ..^ ( O ` A ) ) -1-1-onto-> ( K ` { A } ) )

Proof

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