Step | Hyp | Ref
| Expression |
1 | | dchrval.g |
. . . 4
β’ πΊ = (DChrβπ) |
2 | | dchrval.z |
. . . 4
β’ π =
(β€/nβ€βπ) |
3 | | dchrval.b |
. . . 4
β’ π΅ = (Baseβπ) |
4 | | dchrval.u |
. . . 4
β’ π = (Unitβπ) |
5 | | dchrval.n |
. . . 4
β’ (π β π β β) |
6 | | eqidd 2737 |
. . . 4
β’ (π β {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯} = {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}) |
7 | 1, 2, 3, 4, 5, 6 | dchrval 26488 |
. . 3
β’ (π β πΊ = {β¨(Baseβndx), {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}β©, β¨(+gβndx), (
βf Β· βΎ ({π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯} Γ {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}))β©}) |
8 | 7 | fveq2d 6829 |
. 2
β’ (π β (BaseβπΊ) =
(Baseβ{β¨(Baseβndx), {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}β©, β¨(+gβndx), (
βf Β· βΎ ({π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯} Γ {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}))β©})) |
9 | | dchrbas.b |
. 2
β’ π· = (BaseβπΊ) |
10 | | ovex 7370 |
. . . 4
β’
((mulGrpβπ)
MndHom (mulGrpββfld)) β V |
11 | 10 | rabex 5276 |
. . 3
β’ {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯} β V |
12 | | eqid 2736 |
. . . 4
β’
{β¨(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 17093 |
. . 3
β’ ({π₯ β ((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 5 |
. 2
β’ {π₯ β ((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 | 8, 9, 14 | 3eqtr4g 2801 |
1
β’ (π β π· = {π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β£ ((π΅ β π) Γ {0}) β π₯}) |