Step |
Hyp |
Ref |
Expression |
1 |
|
dchrval.g |
|- G = ( DChr ` N ) |
2 |
|
dchrval.z |
|- Z = ( Z/nZ ` N ) |
3 |
|
dchrval.b |
|- B = ( Base ` Z ) |
4 |
|
dchrval.u |
|- U = ( Unit ` Z ) |
5 |
|
dchrval.n |
|- ( ph -> N e. NN ) |
6 |
|
dchrbas.b |
|- D = ( Base ` G ) |
7 |
1 2 3 4 5 6
|
dchrbas |
|- ( ph -> D = { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } ) |
8 |
7
|
eleq2d |
|- ( ph -> ( X e. D <-> X e. { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } ) ) |
9 |
|
sseq2 |
|- ( x = X -> ( ( ( B \ U ) X. { 0 } ) C_ x <-> ( ( B \ U ) X. { 0 } ) C_ X ) ) |
10 |
9
|
elrab |
|- ( X e. { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) ) |
11 |
8 10
|
bitrdi |
|- ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) ) ) |