Step | Hyp | Ref
| Expression |
1 | | mendvscafval.a |
. . 3
β’ π΄ = (MEndoβπ) |
2 | 1 | fveq2i 6892 |
. 2
β’ (
Β·π βπ΄) = ( Β·π
β(MEndoβπ)) |
3 | | mendvscafval.b |
. . . . . . 7
β’ π΅ = (Baseβπ΄) |
4 | 1 | mendbas 41912 |
. . . . . . 7
β’ (π LMHom π) = (Baseβπ΄) |
5 | 3, 4 | eqtr4i 2764 |
. . . . . 6
β’ π΅ = (π LMHom π) |
6 | | eqid 2733 |
. . . . . 6
β’ (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf
(+gβπ)π¦)) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf
(+gβπ)π¦)) |
7 | | eqid 2733 |
. . . . . 6
β’ (π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦)) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦)) |
8 | | mendvscafval.s |
. . . . . 6
β’ π = (Scalarβπ) |
9 | | mendvscafval.k |
. . . . . . 7
β’ πΎ = (Baseβπ) |
10 | | eqid 2733 |
. . . . . . 7
β’ π΅ = π΅ |
11 | | mendvscafval.e |
. . . . . . . . 9
β’ πΈ = (Baseβπ) |
12 | 11 | xpeq1i 5702 |
. . . . . . . 8
β’ (πΈ Γ {π₯}) = ((Baseβπ) Γ {π₯}) |
13 | | eqid 2733 |
. . . . . . . 8
β’ π¦ = π¦ |
14 | | mendvscafval.v |
. . . . . . . . 9
β’ Β· = (
Β·π βπ) |
15 | | ofeq 7670 |
. . . . . . . . 9
β’ ( Β· = (
Β·π βπ) β βf Β· =
βf ( Β·π βπ)) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . 8
β’
βf Β· =
βf ( Β·π βπ) |
17 | 12, 13, 16 | oveq123i 7420 |
. . . . . . 7
β’ ((πΈ Γ {π₯}) βf Β· π¦) = (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦) |
18 | 9, 10, 17 | mpoeq123i 7482 |
. . . . . 6
β’ (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) = (π₯ β (Baseβπ), π¦ β π΅ β¦ (((Baseβπ) Γ {π₯}) βf (
Β·π βπ)π¦)) |
19 | 5, 6, 7, 8, 18 | mendval 41911 |
. . . . 5
β’ (π β V β
(MEndoβπ) =
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦))β©})) |
20 | 19 | fveq2d 6893 |
. . . 4
β’ (π β V β (
Β·π β(MEndoβπ)) = ( Β·π
β({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦))β©}))) |
21 | 9 | fvexi 6903 |
. . . . . 6
β’ πΎ β V |
22 | 3 | fvexi 6903 |
. . . . . 6
β’ π΅ β V |
23 | 21, 22 | mpoex 8063 |
. . . . 5
β’ (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) β V |
24 | | eqid 2733 |
. . . . . 6
β’
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦))β©}) = ({β¨(Baseβndx), π΅β©,
β¨(+gβndx), (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦))β©}) |
25 | 24 | algvsca 41910 |
. . . . 5
β’ ((π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) β V β (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) = ( Β·π
β({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦))β©}))) |
26 | 23, 25 | mp1i 13 |
. . . 4
β’ (π β V β (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) = ( Β·π
β({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ βf
(+gβπ)π¦))β©, β¨(.rβndx),
(π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦))β©}))) |
27 | 20, 26 | eqtr4d 2776 |
. . 3
β’ (π β V β (
Β·π β(MEndoβπ)) = (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦))) |
28 | | fvprc 6881 |
. . . . . 6
β’ (Β¬
π β V β
(MEndoβπ) =
β
) |
29 | 28 | fveq2d 6893 |
. . . . 5
β’ (Β¬
π β V β (
Β·π β(MEndoβπ)) = ( Β·π
ββ
)) |
30 | | vscaid 17262 |
. . . . . 6
β’
Β·π = Slot (
Β·π βndx) |
31 | 30 | str0 17119 |
. . . . 5
β’ β
=
( Β·π ββ
) |
32 | 29, 31 | eqtr4di 2791 |
. . . 4
β’ (Β¬
π β V β (
Β·π β(MEndoβπ)) = β
) |
33 | | fvprc 6881 |
. . . . . . . . 9
β’ (Β¬
π β V β
(Scalarβπ) =
β
) |
34 | 8, 33 | eqtrid 2785 |
. . . . . . . 8
β’ (Β¬
π β V β π = β
) |
35 | 34 | fveq2d 6893 |
. . . . . . 7
β’ (Β¬
π β V β
(Baseβπ) =
(Baseββ
)) |
36 | | base0 17146 |
. . . . . . 7
β’ β
=
(Baseββ
) |
37 | 35, 9, 36 | 3eqtr4g 2798 |
. . . . . 6
β’ (Β¬
π β V β πΎ = β
) |
38 | 37 | orcd 872 |
. . . . 5
β’ (Β¬
π β V β (πΎ = β
β¨ π΅ = β
)) |
39 | | 0mpo0 7489 |
. . . . 5
β’ ((πΎ = β
β¨ π΅ = β
) β (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) = β
) |
40 | 38, 39 | syl 17 |
. . . 4
β’ (Β¬
π β V β (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) = β
) |
41 | 32, 40 | eqtr4d 2776 |
. . 3
β’ (Β¬
π β V β (
Β·π β(MEndoβπ)) = (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦))) |
42 | 27, 41 | pm2.61i 182 |
. 2
β’ (
Β·π β(MEndoβπ)) = (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) |
43 | 2, 42 | eqtri 2761 |
1
β’ (
Β·π βπ΄) = (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) |