Step | Hyp | Ref
| Expression |
1 | | fvex 6856 |
. . . . 5
β’
(Scalarβπ)
β V |
2 | | eqid 2733 |
. . . . . 6
β’
({β¨(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 | algsca 41551 |
. . . . 5
β’
((Scalarβπ)
β V β (Scalarβπ) = (Scalarβ({β¨(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 |
. . . 4
β’ (π β V β
(Scalarβπ) =
(Scalarβ({β¨(Baseβndx), (π LMHom π)β©, β¨(+gβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}))) |
5 | | eqid 2733 |
. . . . . 6
β’ (π LMHom π) = (π LMHom π) |
6 | | eqid 2733 |
. . . . . 6
β’ (π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦)) = (π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦)) |
7 | | eqid 2733 |
. . . . . 6
β’ (π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦)) = (π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦)) |
8 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
9 | | eqid 2733 |
. . . . . 6
β’ (π₯ β
(Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) = (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) |
10 | 5, 6, 7, 8, 9 | 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 (
Β·π βπ)π¦))β©})) |
11 | 10 | fveq2d 6847 |
. . . 4
β’ (π β V β
(Scalarβ(MEndoβπ)) = (Scalarβ({β¨(Baseβndx),
(π LMHom π)β©, β¨(+gβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β (π LMHom π), π¦ β (π LMHom π) β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
(Scalarβπ)β©,
β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β (π LMHom π) β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦))β©}))) |
12 | 4, 11 | eqtr4d 2776 |
. . 3
β’ (π β V β
(Scalarβπ) =
(Scalarβ(MEndoβπ))) |
13 | | scaid 17201 |
. . . . . 6
β’ Scalar =
Slot (Scalarβndx) |
14 | 13 | str0 17066 |
. . . . 5
β’ β
=
(Scalarββ
) |
15 | 14 | eqcomi 2742 |
. . . 4
β’
(Scalarββ
) = β
|
16 | | eqid 2733 |
. . . 4
β’
(MEndoβπ) =
(MEndoβπ) |
17 | 15, 16 | fveqprc 17068 |
. . 3
β’ (Β¬
π β V β
(Scalarβπ) =
(Scalarβ(MEndoβπ))) |
18 | 12, 17 | pm2.61i 182 |
. 2
β’
(Scalarβπ) =
(Scalarβ(MEndoβπ)) |
19 | | mendsca.s |
. 2
β’ π = (Scalarβπ) |
20 | | mendsca.a |
. . 3
β’ π΄ = (MEndoβπ) |
21 | 20 | fveq2i 6846 |
. 2
β’
(Scalarβπ΄) =
(Scalarβ(MEndoβπ)) |
22 | 18, 19, 21 | 3eqtr4i 2771 |
1
β’ π = (Scalarβπ΄) |