Step |
Hyp |
Ref |
Expression |
1 |
|
dchrval.g |
โข ๐บ = ( DChr โ ๐ ) |
2 |
|
dchrval.z |
โข ๐ = ( โค/nโค โ ๐ ) |
3 |
|
dchrval.b |
โข ๐ต = ( Base โ ๐ ) |
4 |
|
dchrval.u |
โข ๐ = ( Unit โ ๐ ) |
5 |
|
dchrval.n |
โข ( ๐ โ ๐ โ โ ) |
6 |
|
dchrbas.b |
โข ๐ท = ( Base โ ๐บ ) |
7 |
|
eqidd |
โข ( ๐ โ { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } = { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ) |
8 |
1 2 3 4 5 7
|
dchrval |
โข ( ๐ โ ๐บ = { โจ ( Base โ ndx ) , { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ร { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ) ) โฉ } ) |
9 |
8
|
fveq2d |
โข ( ๐ โ ( Base โ ๐บ ) = ( Base โ { โจ ( Base โ ndx ) , { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ร { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ) ) โฉ } ) ) |
10 |
|
ovex |
โข ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โ V |
11 |
10
|
rabex |
โข { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } โ V |
12 |
|
eqid |
โข { โจ ( Base โ ndx ) , { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ร { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ) ) โฉ } = { โจ ( Base โ ndx ) , { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ร { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ) ) โฉ } |
13 |
12
|
grpbase |
โข ( { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } โ V โ { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } = ( Base โ { โจ ( Base โ ndx ) , { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ร { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ) ) โฉ } ) ) |
14 |
11 13
|
ax-mp |
โข { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } = ( Base โ { โจ ( Base โ ndx ) , { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ร { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ) ) โฉ } ) |
15 |
9 6 14
|
3eqtr4g |
โข ( ๐ โ ๐ท = { ๐ฅ โ ( ( mulGrp โ ๐ ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ๐ต โ ๐ ) ร { 0 } ) โ ๐ฅ } ) |