Step |
Hyp |
Ref |
Expression |
1 |
|
dchrabl.g |
|- G = ( DChr ` N ) |
2 |
|
eqidd |
|- ( N e. NN -> ( Base ` G ) = ( Base ` G ) ) |
3 |
|
eqidd |
|- ( N e. NN -> ( +g ` G ) = ( +g ` G ) ) |
4 |
|
eqid |
|- ( Z/nZ ` N ) = ( Z/nZ ` N ) |
5 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
6 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
7 |
|
simp2 |
|- ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> x e. ( Base ` G ) ) |
8 |
|
simp3 |
|- ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> y e. ( Base ` G ) ) |
9 |
1 4 5 6 7 8
|
dchrmulcl |
|- ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) ) |
10 |
|
fvexd |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( Base ` ( Z/nZ ` N ) ) e. _V ) |
11 |
|
eqid |
|- ( Base ` ( Z/nZ ` N ) ) = ( Base ` ( Z/nZ ` N ) ) |
12 |
1 4 5 11 7
|
dchrf |
|- ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> x : ( Base ` ( Z/nZ ` N ) ) --> CC ) |
13 |
12
|
3adant3r3 |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> x : ( Base ` ( Z/nZ ` N ) ) --> CC ) |
14 |
1 4 5 11 8
|
dchrf |
|- ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> y : ( Base ` ( Z/nZ ` N ) ) --> CC ) |
15 |
14
|
3adant3r3 |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> y : ( Base ` ( Z/nZ ` N ) ) --> CC ) |
16 |
|
simpr3 |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> z e. ( Base ` G ) ) |
17 |
1 4 5 11 16
|
dchrf |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> z : ( Base ` ( Z/nZ ` N ) ) --> CC ) |
18 |
|
mulass |
|- ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( a x. b ) x. c ) = ( a x. ( b x. c ) ) ) |
19 |
18
|
adantl |
|- ( ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) /\ ( a e. CC /\ b e. CC /\ c e. CC ) ) -> ( ( a x. b ) x. c ) = ( a x. ( b x. c ) ) ) |
20 |
10 13 15 17 19
|
caofass |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x oF x. y ) oF x. z ) = ( x oF x. ( y oF x. z ) ) ) |
21 |
|
simpr1 |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> x e. ( Base ` G ) ) |
22 |
|
simpr2 |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> y e. ( Base ` G ) ) |
23 |
1 4 5 6 21 22
|
dchrmul |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x oF x. y ) ) |
24 |
23
|
oveq1d |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) oF x. z ) = ( ( x oF x. y ) oF x. z ) ) |
25 |
1 4 5 6 22 16
|
dchrmul |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( y ( +g ` G ) z ) = ( y oF x. z ) ) |
26 |
25
|
oveq2d |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x oF x. ( y ( +g ` G ) z ) ) = ( x oF x. ( y oF x. z ) ) ) |
27 |
20 24 26
|
3eqtr4d |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) oF x. z ) = ( x oF x. ( y ( +g ` G ) z ) ) ) |
28 |
9
|
3adant3r3 |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) ) |
29 |
1 4 5 6 28 16
|
dchrmul |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( ( x ( +g ` G ) y ) oF x. z ) ) |
30 |
1 4 5 6 22 16
|
dchrmulcl |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( y ( +g ` G ) z ) e. ( Base ` G ) ) |
31 |
1 4 5 6 21 30
|
dchrmul |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x ( +g ` G ) ( y ( +g ` G ) z ) ) = ( x oF x. ( y ( +g ` G ) z ) ) ) |
32 |
27 29 31
|
3eqtr4d |
|- ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) ) |
33 |
|
eqid |
|- ( Unit ` ( Z/nZ ` N ) ) = ( Unit ` ( Z/nZ ` N ) ) |
34 |
|
eqid |
|- ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) = ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) |
35 |
|
id |
|- ( N e. NN -> N e. NN ) |
36 |
1 4 5 11 33 34 35
|
dchr1cl |
|- ( N e. NN -> ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) e. ( Base ` G ) ) |
37 |
|
simpr |
|- ( ( N e. NN /\ x e. ( Base ` G ) ) -> x e. ( Base ` G ) ) |
38 |
1 4 5 11 33 34 6 37
|
dchrmulid2 |
|- ( ( N e. NN /\ x e. ( Base ` G ) ) -> ( ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) ( +g ` G ) x ) = x ) |
39 |
|
eqid |
|- ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) = ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) |
40 |
1 4 5 11 33 34 6 37 39
|
dchrinvcl |
|- ( ( N e. NN /\ x e. ( Base ` G ) ) -> ( ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) e. ( Base ` G ) /\ ( ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) ( +g ` G ) x ) = ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) ) ) |
41 |
40
|
simpld |
|- ( ( N e. NN /\ x e. ( Base ` G ) ) -> ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) e. ( Base ` G ) ) |
42 |
40
|
simprd |
|- ( ( N e. NN /\ x e. ( Base ` G ) ) -> ( ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) ( +g ` G ) x ) = ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) ) |
43 |
2 3 9 32 36 38 41 42
|
isgrpd |
|- ( N e. NN -> G e. Grp ) |
44 |
|
fvexd |
|- ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( Base ` ( Z/nZ ` N ) ) e. _V ) |
45 |
|
mulcom |
|- ( ( a e. CC /\ b e. CC ) -> ( a x. b ) = ( b x. a ) ) |
46 |
45
|
adantl |
|- ( ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ ( a e. CC /\ b e. CC ) ) -> ( a x. b ) = ( b x. a ) ) |
47 |
44 12 14 46
|
caofcom |
|- ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x oF x. y ) = ( y oF x. x ) ) |
48 |
1 4 5 6 7 8
|
dchrmul |
|- ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) = ( x oF x. y ) ) |
49 |
1 4 5 6 8 7
|
dchrmul |
|- ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( y ( +g ` G ) x ) = ( y oF x. x ) ) |
50 |
47 48 49
|
3eqtr4d |
|- ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) |
51 |
2 3 43 50
|
isabld |
|- ( N e. NN -> G e. Abel ) |