Step | Hyp | Ref
| Expression |
1 | | lssset.s |
. 2
β’ π = (LSubSpβπ) |
2 | | elex 3462 |
. . 3
β’ (π β π β π β V) |
3 | | fveq2 6843 |
. . . . . . . 8
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
4 | | lssset.v |
. . . . . . . 8
β’ π = (Baseβπ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . . 7
β’ (π€ = π β (Baseβπ€) = π) |
6 | 5 | pweqd 4578 |
. . . . . 6
β’ (π€ = π β π« (Baseβπ€) = π« π) |
7 | 6 | difeq1d 4082 |
. . . . 5
β’ (π€ = π β (π« (Baseβπ€) β {β
}) =
(π« π β
{β
})) |
8 | | fveq2 6843 |
. . . . . . . . 9
β’ (π€ = π β (Scalarβπ€) = (Scalarβπ)) |
9 | | lssset.f |
. . . . . . . . 9
β’ πΉ = (Scalarβπ) |
10 | 8, 9 | eqtr4di 2791 |
. . . . . . . 8
β’ (π€ = π β (Scalarβπ€) = πΉ) |
11 | 10 | fveq2d 6847 |
. . . . . . 7
β’ (π€ = π β (Baseβ(Scalarβπ€)) = (BaseβπΉ)) |
12 | | lssset.b |
. . . . . . 7
β’ π΅ = (BaseβπΉ) |
13 | 11, 12 | eqtr4di 2791 |
. . . . . 6
β’ (π€ = π β (Baseβ(Scalarβπ€)) = π΅) |
14 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π€ = π β (
Β·π βπ€) = ( Β·π
βπ)) |
15 | | lssset.t |
. . . . . . . . . . . 12
β’ Β· = (
Β·π βπ) |
16 | 14, 15 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π€ = π β (
Β·π βπ€) = Β· ) |
17 | 16 | oveqd 7375 |
. . . . . . . . . 10
β’ (π€ = π β (π₯( Β·π
βπ€)π) = (π₯ Β· π)) |
18 | 17 | oveq1d 7373 |
. . . . . . . . 9
β’ (π€ = π β ((π₯( Β·π
βπ€)π)(+gβπ€)π) = ((π₯ Β· π)(+gβπ€)π)) |
19 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π€ = π β (+gβπ€) = (+gβπ)) |
20 | | lssset.p |
. . . . . . . . . . 11
β’ + =
(+gβπ) |
21 | 19, 20 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π€ = π β (+gβπ€) = + ) |
22 | 21 | oveqd 7375 |
. . . . . . . . 9
β’ (π€ = π β ((π₯ Β· π)(+gβπ€)π) = ((π₯ Β· π) + π)) |
23 | 18, 22 | eqtrd 2773 |
. . . . . . . 8
β’ (π€ = π β ((π₯( Β·π
βπ€)π)(+gβπ€)π) = ((π₯ Β· π) + π)) |
24 | 23 | eleq1d 2819 |
. . . . . . 7
β’ (π€ = π β (((π₯( Β·π
βπ€)π)(+gβπ€)π) β π β ((π₯ Β· π) + π) β π )) |
25 | 24 | 2ralbidv 3209 |
. . . . . 6
β’ (π€ = π β (βπ β π βπ β π ((π₯( Β·π
βπ€)π)(+gβπ€)π) β π β βπ β π βπ β π ((π₯ Β· π) + π) β π )) |
26 | 13, 25 | raleqbidv 3318 |
. . . . 5
β’ (π€ = π β (βπ₯ β (Baseβ(Scalarβπ€))βπ β π βπ β π ((π₯( Β·π
βπ€)π)(+gβπ€)π) β π β βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π )) |
27 | 7, 26 | rabeqbidv 3423 |
. . . 4
β’ (π€ = π β {π β (π« (Baseβπ€) β {β
}) β£
βπ₯ β
(Baseβ(Scalarβπ€))βπ β π βπ β π ((π₯( Β·π
βπ€)π)(+gβπ€)π) β π } = {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π }) |
28 | | df-lss 20408 |
. . . 4
β’ LSubSp =
(π€ β V β¦ {π β (π«
(Baseβπ€) β
{β
}) β£ βπ₯ β (Baseβ(Scalarβπ€))βπ β π βπ β π ((π₯( Β·π
βπ€)π)(+gβπ€)π) β π }) |
29 | 4 | fvexi 6857 |
. . . . . . 7
β’ π β V |
30 | 29 | pwex 5336 |
. . . . . 6
β’ π«
π β V |
31 | 30 | difexi 5286 |
. . . . 5
β’
(π« π β
{β
}) β V |
32 | 31 | rabex 5290 |
. . . 4
β’ {π β (π« π β {β
}) β£
βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π } β V |
33 | 27, 28, 32 | fvmpt 6949 |
. . 3
β’ (π β V β
(LSubSpβπ) = {π β (π« π β {β
}) β£
βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π }) |
34 | 2, 33 | syl 17 |
. 2
β’ (π β π β (LSubSpβπ) = {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π }) |
35 | 1, 34 | eqtrid 2785 |
1
β’ (π β π β π = {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π }) |