Step | Hyp | Ref
| Expression |
1 | | elfvex 6930 |
. . 3
β’ (π β (LSubSpβπ) β π β V) |
2 | | lssset.s |
. . 3
β’ π = (LSubSpβπ) |
3 | 1, 2 | eleq2s 2852 |
. 2
β’ (π β π β π β V) |
4 | | lssset.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
5 | | fvprc 6884 |
. . . . . . . . 9
β’ (Β¬
π β V β
(Baseβπ) =
β
) |
6 | 4, 5 | eqtrid 2785 |
. . . . . . . 8
β’ (Β¬
π β V β π = β
) |
7 | 6 | sseq2d 4015 |
. . . . . . 7
β’ (Β¬
π β V β (π β π β π β β
)) |
8 | 7 | biimpcd 248 |
. . . . . 6
β’ (π β π β (Β¬ π β V β π β β
)) |
9 | | ss0 4399 |
. . . . . 6
β’ (π β β
β π = β
) |
10 | 8, 9 | syl6 35 |
. . . . 5
β’ (π β π β (Β¬ π β V β π = β
)) |
11 | 10 | necon1ad 2958 |
. . . 4
β’ (π β π β (π β β
β π β V)) |
12 | 11 | imp 408 |
. . 3
β’ ((π β π β§ π β β
) β π β V) |
13 | 12 | 3adant3 1133 |
. 2
β’ ((π β π β§ π β β
β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π) β π β V) |
14 | | lssset.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
15 | | lssset.b |
. . . . 5
β’ π΅ = (BaseβπΉ) |
16 | | lssset.p |
. . . . 5
β’ + =
(+gβπ) |
17 | | lssset.t |
. . . . 5
β’ Β· = (
Β·π βπ) |
18 | 14, 15, 4, 16, 17, 2 | lssset 20544 |
. . . 4
β’ (π β V β π = {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π }) |
19 | 18 | eleq2d 2820 |
. . 3
β’ (π β V β (π β π β π β {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π })) |
20 | | eldifsn 4791 |
. . . . . 6
β’ (π β (π« π β {β
}) β
(π β π« π β§ π β β
)) |
21 | 4 | fvexi 6906 |
. . . . . . . 8
β’ π β V |
22 | 21 | elpw2 5346 |
. . . . . . 7
β’ (π β π« π β π β π) |
23 | 22 | anbi1i 625 |
. . . . . 6
β’ ((π β π« π β§ π β β
) β (π β π β§ π β β
)) |
24 | 20, 23 | bitri 275 |
. . . . 5
β’ (π β (π« π β {β
}) β
(π β π β§ π β β
)) |
25 | 24 | anbi1i 625 |
. . . 4
β’ ((π β (π« π β {β
}) β§
βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π) β ((π β π β§ π β β
) β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
26 | | eleq2 2823 |
. . . . . . . 8
β’ (π = π β (((π₯ Β· π) + π) β π β ((π₯ Β· π) + π) β π)) |
27 | 26 | raleqbi1dv 3334 |
. . . . . . 7
β’ (π = π β (βπ β π ((π₯ Β· π) + π) β π β βπ β π ((π₯ Β· π) + π) β π)) |
28 | 27 | raleqbi1dv 3334 |
. . . . . 6
β’ (π = π β (βπ β π βπ β π ((π₯ Β· π) + π) β π β βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
29 | 28 | ralbidv 3178 |
. . . . 5
β’ (π = π β (βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π β βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
30 | 29 | elrab 3684 |
. . . 4
β’ (π β {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π } β (π β (π« π β {β
}) β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
31 | | df-3an 1090 |
. . . 4
β’ ((π β π β§ π β β
β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π) β ((π β π β§ π β β
) β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
32 | 25, 30, 31 | 3bitr4i 303 |
. . 3
β’ (π β {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π } β (π β π β§ π β β
β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
33 | 19, 32 | bitrdi 287 |
. 2
β’ (π β V β (π β π β (π β π β§ π β β
β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π))) |
34 | 3, 13, 33 | pm5.21nii 380 |
1
β’ (π β π β (π β π β§ π β β
β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |