Step | Hyp | Ref
| Expression |
1 | | ovex 7391 |
. . . 4
β’ (π LMHom π) β V |
2 | | eqid 2733 |
. . . . 5
β’
({β¨(Baseβndx), (π LMHom π)β©, β¨(+gβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}) = ({β¨(Baseβndx), (π LMHom π)β©, β¨(+gβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}) |
3 | 2 | algbase 41548 |
. . . 4
β’ ((π LMHom π) β V β (π LMHom π) = (Baseβ({β¨(Baseβndx),
(π LMHom π)β©, β¨(+gβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}))) |
4 | 1, 3 | mp1i 13 |
. . 3
β’ (π β V β (π LMHom π) = (Baseβ({β¨(Baseβndx),
(π LMHom π)β©, β¨(+gβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}))) |
5 | | mendbas.a |
. . . . 5
β’ π΄ = (MEndoβπ) |
6 | | eqid 2733 |
. . . . . 6
β’ (π LMHom π) = (π LMHom π) |
7 | | eqid 2733 |
. . . . . 6
β’ (π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦)) = (π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦)) |
8 | | eqid 2733 |
. . . . . 6
β’ (π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦)) = (π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦)) |
9 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
10 | | eqid 2733 |
. . . . . 6
β’ (π₯ β
(Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) = (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) |
11 | 6, 7, 8, 9, 10 | mendval 41553 |
. . . . 5
β’ (π β V β
(MEndoβπ) =
({β¨(Baseβndx), (π LMHom π)β©, β¨(+gβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©})) |
12 | 5, 11 | eqtrid 2785 |
. . . 4
β’ (π β V β π΄ = ({β¨(Baseβndx),
(π LMHom π)β©, β¨(+gβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©})) |
13 | 12 | fveq2d 6847 |
. . 3
β’ (π β V β
(Baseβπ΄) =
(Baseβ({β¨(Baseβndx), (π LMHom π)β©, β¨(+gβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}))) |
14 | 4, 13 | eqtr4d 2776 |
. 2
β’ (π β V β (π LMHom π) = (Baseβπ΄)) |
15 | | base0 17093 |
. . 3
β’ β
=
(Baseββ
) |
16 | | reldmlmhm 20501 |
. . . 4
β’ Rel dom
LMHom |
17 | 16 | ovprc1 7397 |
. . 3
β’ (Β¬
π β V β (π LMHom π) = β
) |
18 | | fvprc 6835 |
. . . . 5
β’ (Β¬
π β V β
(MEndoβπ) =
β
) |
19 | 5, 18 | eqtrid 2785 |
. . . 4
β’ (Β¬
π β V β π΄ = β
) |
20 | 19 | fveq2d 6847 |
. . 3
β’ (Β¬
π β V β
(Baseβπ΄) =
(Baseββ
)) |
21 | 15, 17, 20 | 3eqtr4a 2799 |
. 2
β’ (Β¬
π β V β (π LMHom π) = (Baseβπ΄)) |
22 | 14, 21 | pm2.61i 182 |
1
β’ (π LMHom π) = (Baseβπ΄) |