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