Step | Hyp | Ref
| Expression |
1 | | dchrval.g |
. 2
DChr |
2 | | df-dchr 24958 |
. . . 4
DChr ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit
|
3 | 2 | a1i 11 |
. . 3
DChr ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit
|
4 | | fvexd 6203 |
. . . 4
ℤ/nℤ |
5 | | ovex 6678 |
. . . . . . 7
mulGrp MndHom mulGrpℂfld |
6 | 5 | rabex 4813 |
. . . . . 6
mulGrp MndHom mulGrpℂfld
Unit
|
7 | 6 | a1i 11 |
. . . . 5
ℤ/nℤ
mulGrp MndHom mulGrpℂfld
Unit
|
8 | | dchrval.d |
. . . . . . . . . . 11
mulGrp MndHom mulGrpℂfld |
9 | 8 | ad2antrr 762 |
. . . . . . . . . 10
ℤ/nℤ
mulGrp MndHom mulGrpℂfld |
10 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
11 | 10 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
ℤ/nℤ ℤ/nℤ |
12 | | dchrval.z |
. . . . . . . . . . . . . . . 16
ℤ/nℤ |
13 | 11, 12 | syl6reqr 2675 |
. . . . . . . . . . . . . . 15
ℤ/nℤ |
14 | 13 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
ℤ/nℤ |
15 | 14 | biimpar 502 |
. . . . . . . . . . . . 13
ℤ/nℤ |
16 | 15 | fveq2d 6195 |
. . . . . . . . . . . 12
ℤ/nℤ mulGrp mulGrp |
17 | 16 | oveq1d 6665 |
. . . . . . . . . . 11
ℤ/nℤ mulGrp MndHom mulGrpℂfld mulGrp MndHom mulGrpℂfld |
18 | 15 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
ℤ/nℤ |
19 | | dchrval.b |
. . . . . . . . . . . . . . 15
|
20 | 18, 19 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
ℤ/nℤ |
21 | 15 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
ℤ/nℤ Unit Unit |
22 | | dchrval.u |
. . . . . . . . . . . . . . 15
Unit |
23 | 21, 22 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
ℤ/nℤ Unit |
24 | 20, 23 | difeq12d 3729 |
. . . . . . . . . . . . 13
ℤ/nℤ
Unit |
25 | 24 | xpeq1d 5138 |
. . . . . . . . . . . 12
ℤ/nℤ Unit |
26 | 25 | sseq1d 3632 |
. . . . . . . . . . 11
ℤ/nℤ Unit |
27 | 17, 26 | rabeqbidv 3195 |
. . . . . . . . . 10
ℤ/nℤ
mulGrp MndHom mulGrpℂfld
Unit
mulGrp MndHom mulGrpℂfld
|
28 | 9, 27 | eqtr4d 2659 |
. . . . . . . . 9
ℤ/nℤ
mulGrp MndHom mulGrpℂfld
Unit |
29 | 28 | eqeq2d 2632 |
. . . . . . . 8
ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit |
30 | 29 | biimpar 502 |
. . . . . . 7
ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit |
31 | 30 | opeq2d 4409 |
. . . . . 6
ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit
|
32 | 30 | sqxpeqd 5141 |
. . . . . . . 8
ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit |
33 | 32 | reseq2d 5396 |
. . . . . . 7
ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit
|
34 | 33 | opeq2d 4409 |
. . . . . 6
ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit
|
35 | 31, 34 | preq12d 4276 |
. . . . 5
ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit
|
36 | 7, 35 | csbied 3560 |
. . . 4
ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit
|
37 | 4, 36 | csbied 3560 |
. . 3
ℤ/nℤ mulGrp MndHom mulGrpℂfld
Unit
|
38 | | dchrval.n |
. . 3
|
39 | | prex 4909 |
. . . 4
|
40 | 39 | a1i 11 |
. . 3
|
41 | 3, 37, 38, 40 | fvmptd 6288 |
. 2
DChr
|
42 | 1, 41 | syl5eq 2668 |
1
|