Step | Hyp | Ref
| Expression |
1 | | elfvex 6930 |
. . 3
β’ (π β (LSubSpβπ) β π β V) |
2 | | lssset.s |
. . 3
β’ π = (LSubSpβπ) |
3 | 1, 2 | eleq2s 2849 |
. 2
β’ (π β π β π β V) |
4 | | lssset.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
5 | | fvprc 6884 |
. . . . . . . . 9
β’ (Β¬
π β V β
(Baseβπ) =
β
) |
6 | 4, 5 | eqtrid 2782 |
. . . . . . . 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 2955 |
. . . 4
β’ (π β π β (π β β
β π β V)) |
12 | 11 | imp 405 |
. . 3
β’ ((π β π β§ π β β
) β π β V) |
13 | 12 | 3adant3 1130 |
. 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 20690 |
. . . 4
β’ (π β V β π = {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π }) |
19 | 18 | eleq2d 2817 |
. . 3
β’ (π β V β (π β π β π β {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π })) |
20 | | eldifsn 4791 |
. . . . . 6
β’ (π β (π« π β {β
}) β
(π β π« π β§ π β β
)) |
21 | 4 | fvexi 6906 |
. . . . . . . 8
β’ π β V |
22 | 21 | elpw2 5346 |
. . . . . . 7
β’ (π β π« π β π β π) |
23 | 22 | anbi1i 622 |
. . . . . 6
β’ ((π β π« π β§ π β β
) β (π β π β§ π β β
)) |
24 | 20, 23 | bitri 274 |
. . . . 5
β’ (π β (π« π β {β
}) β
(π β π β§ π β β
)) |
25 | 24 | anbi1i 622 |
. . . 4
β’ ((π β (π« π β {β
}) β§
βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π) β ((π β π β§ π β β
) β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
26 | | eleq2 2820 |
. . . . . . . 8
β’ (π = π β (((π₯ Β· π) + π) β π β ((π₯ Β· π) + π) β π)) |
27 | 26 | raleqbi1dv 3331 |
. . . . . . 7
β’ (π = π β (βπ β π ((π₯ Β· π) + π) β π β βπ β π ((π₯ Β· π) + π) β π)) |
28 | 27 | raleqbi1dv 3331 |
. . . . . 6
β’ (π = π β (βπ β π βπ β π ((π₯ Β· π) + π) β π β βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
29 | 28 | ralbidv 3175 |
. . . . 5
β’ (π = π β (βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π β βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
30 | 29 | elrab 3684 |
. . . 4
β’ (π β {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π } β (π β (π« π β {β
}) β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
31 | | df-3an 1087 |
. . . 4
β’ ((π β π β§ π β β
β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π) β ((π β π β§ π β β
) β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
32 | 25, 30, 31 | 3bitr4i 302 |
. . 3
β’ (π β {π β (π« π β {β
}) β£ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π } β (π β π β§ π β β
β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |
33 | 19, 32 | bitrdi 286 |
. 2
β’ (π β V β (π β π β (π β π β§ π β β
β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π))) |
34 | 3, 13, 33 | pm5.21nii 377 |
1
β’ (π β π β (π β π β§ π β β
β§ βπ₯ β π΅ βπ β π βπ β π ((π₯ Β· π) + π) β π)) |