Step | Hyp | Ref
| Expression |
1 | | asclfval.a |
. 2
β’ π΄ = (algScβπ) |
2 | | fveq2 6843 |
. . . . . . . 8
β’ (π€ = π β (Scalarβπ€) = (Scalarβπ)) |
3 | | asclfval.f |
. . . . . . . 8
β’ πΉ = (Scalarβπ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . . 7
β’ (π€ = π β (Scalarβπ€) = πΉ) |
5 | 4 | fveq2d 6847 |
. . . . . 6
β’ (π€ = π β (Baseβ(Scalarβπ€)) = (BaseβπΉ)) |
6 | | asclfval.k |
. . . . . 6
β’ πΎ = (BaseβπΉ) |
7 | 5, 6 | eqtr4di 2791 |
. . . . 5
β’ (π€ = π β (Baseβ(Scalarβπ€)) = πΎ) |
8 | | fveq2 6843 |
. . . . . . 7
β’ (π€ = π β (
Β·π βπ€) = ( Β·π
βπ)) |
9 | | asclfval.s |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
10 | 8, 9 | eqtr4di 2791 |
. . . . . 6
β’ (π€ = π β (
Β·π βπ€) = Β· ) |
11 | | eqidd 2734 |
. . . . . 6
β’ (π€ = π β π₯ = π₯) |
12 | | fveq2 6843 |
. . . . . . 7
β’ (π€ = π β (1rβπ€) = (1rβπ)) |
13 | | asclfval.o |
. . . . . . 7
β’ 1 =
(1rβπ) |
14 | 12, 13 | eqtr4di 2791 |
. . . . . 6
β’ (π€ = π β (1rβπ€) = 1 ) |
15 | 10, 11, 14 | oveq123d 7379 |
. . . . 5
β’ (π€ = π β (π₯( Β·π
βπ€)(1rβπ€)) = (π₯ Β· 1 )) |
16 | 7, 15 | mpteq12dv 5197 |
. . . 4
β’ (π€ = π β (π₯ β (Baseβ(Scalarβπ€)) β¦ (π₯( Β·π
βπ€)(1rβπ€))) = (π₯ β πΎ β¦ (π₯ Β· 1 ))) |
17 | | df-ascl 21277 |
. . . 4
β’ algSc =
(π€ β V β¦ (π₯ β
(Baseβ(Scalarβπ€)) β¦ (π₯( Β·π
βπ€)(1rβπ€)))) |
18 | 16, 17, 6 | mptfvmpt 7179 |
. . 3
β’ (π β V β
(algScβπ) = (π₯ β πΎ β¦ (π₯ Β· 1 ))) |
19 | | fvprc 6835 |
. . . . 5
β’ (Β¬
π β V β
(algScβπ) =
β
) |
20 | | mpt0 6644 |
. . . . 5
β’ (π₯ β β
β¦ (π₯ Β· 1 )) =
β
|
21 | 19, 20 | eqtr4di 2791 |
. . . 4
β’ (Β¬
π β V β
(algScβπ) = (π₯ β β
β¦ (π₯ Β· 1 ))) |
22 | | fvprc 6835 |
. . . . . . . . 9
β’ (Β¬
π β V β
(Scalarβπ) =
β
) |
23 | 3, 22 | eqtrid 2785 |
. . . . . . . 8
β’ (Β¬
π β V β πΉ = β
) |
24 | 23 | fveq2d 6847 |
. . . . . . 7
β’ (Β¬
π β V β
(BaseβπΉ) =
(Baseββ
)) |
25 | | base0 17093 |
. . . . . . 7
β’ β
=
(Baseββ
) |
26 | 24, 25 | eqtr4di 2791 |
. . . . . 6
β’ (Β¬
π β V β
(BaseβπΉ) =
β
) |
27 | 6, 26 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β πΎ = β
) |
28 | 27 | mpteq1d 5201 |
. . . 4
β’ (Β¬
π β V β (π₯ β πΎ β¦ (π₯ Β· 1 )) = (π₯ β β
β¦ (π₯ Β· 1 ))) |
29 | 21, 28 | eqtr4d 2776 |
. . 3
β’ (Β¬
π β V β
(algScβπ) = (π₯ β πΎ β¦ (π₯ Β· 1 ))) |
30 | 18, 29 | pm2.61i 182 |
. 2
β’
(algScβπ) =
(π₯ β πΎ β¦ (π₯ Β· 1 )) |
31 | 1, 30 | eqtri 2761 |
1
β’ π΄ = (π₯ β πΎ β¦ (π₯ Β· 1 )) |