Step |
Hyp |
Ref |
Expression |
0 |
|
cdchr |
|- DChr |
1 |
|
vn |
|- n |
2 |
|
cn |
|- NN |
3 |
|
czn |
|- Z/nZ |
4 |
1
|
cv |
|- n |
5 |
4 3
|
cfv |
|- ( Z/nZ ` n ) |
6 |
|
vz |
|- z |
7 |
|
vx |
|- x |
8 |
|
cmgp |
|- mulGrp |
9 |
6
|
cv |
|- z |
10 |
9 8
|
cfv |
|- ( mulGrp ` z ) |
11 |
|
cmhm |
|- MndHom |
12 |
|
ccnfld |
|- CCfld |
13 |
12 8
|
cfv |
|- ( mulGrp ` CCfld ) |
14 |
10 13 11
|
co |
|- ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) |
15 |
|
cbs |
|- Base |
16 |
9 15
|
cfv |
|- ( Base ` z ) |
17 |
|
cui |
|- Unit |
18 |
9 17
|
cfv |
|- ( Unit ` z ) |
19 |
16 18
|
cdif |
|- ( ( Base ` z ) \ ( Unit ` z ) ) |
20 |
|
cc0 |
|- 0 |
21 |
20
|
csn |
|- { 0 } |
22 |
19 21
|
cxp |
|- ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) |
23 |
7
|
cv |
|- x |
24 |
22 23
|
wss |
|- ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x |
25 |
24 7 14
|
crab |
|- { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } |
26 |
|
vb |
|- b |
27 |
|
cnx |
|- ndx |
28 |
27 15
|
cfv |
|- ( Base ` ndx ) |
29 |
26
|
cv |
|- b |
30 |
28 29
|
cop |
|- <. ( Base ` ndx ) , b >. |
31 |
|
cplusg |
|- +g |
32 |
27 31
|
cfv |
|- ( +g ` ndx ) |
33 |
|
cmul |
|- x. |
34 |
33
|
cof |
|- oF x. |
35 |
29 29
|
cxp |
|- ( b X. b ) |
36 |
34 35
|
cres |
|- ( oF x. |` ( b X. b ) ) |
37 |
32 36
|
cop |
|- <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. |
38 |
30 37
|
cpr |
|- { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } |
39 |
26 25 38
|
csb |
|- [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } |
40 |
6 5 39
|
csb |
|- [_ ( Z/nZ ` n ) / z ]_ [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } |
41 |
1 2 40
|
cmpt |
|- ( n e. NN |-> [_ ( Z/nZ ` n ) / z ]_ [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } ) |
42 |
0 41
|
wceq |
|- DChr = ( n e. NN |-> [_ ( Z/nZ ` n ) / z ]_ [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } ) |