Step | Hyp | Ref
| Expression |
1 | | eldifsn 4748 |
. 2
β’ (π΄ β (πΎ β { 0 }) β (π΄ β πΎ β§ π΄ β 0 )) |
2 | | elfvdm 6880 |
. . . . . . . 8
β’ (π΅ β (LBasisβπ) β π β dom LBasis) |
3 | | lbsss.j |
. . . . . . . 8
β’ π½ = (LBasisβπ) |
4 | 2, 3 | eleq2s 2852 |
. . . . . . 7
β’ (π΅ β π½ β π β dom LBasis) |
5 | | lbsss.v |
. . . . . . . 8
β’ π = (Baseβπ) |
6 | | lbsind.f |
. . . . . . . 8
β’ πΉ = (Scalarβπ) |
7 | | lbsind.s |
. . . . . . . 8
β’ Β· = (
Β·π βπ) |
8 | | lbsind.k |
. . . . . . . 8
β’ πΎ = (BaseβπΉ) |
9 | | lbssp.n |
. . . . . . . 8
β’ π = (LSpanβπ) |
10 | | lbsind.z |
. . . . . . . 8
β’ 0 =
(0gβπΉ) |
11 | 5, 6, 7, 8, 3, 9, 10 | islbs 20552 |
. . . . . . 7
β’ (π β dom LBasis β (π΅ β π½ β (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ βπ¦ β (πΎ β { 0 }) Β¬ (π¦ Β· π₯) β (πβ(π΅ β {π₯}))))) |
12 | 4, 11 | syl 17 |
. . . . . 6
β’ (π΅ β π½ β (π΅ β π½ β (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ βπ¦ β (πΎ β { 0 }) Β¬ (π¦ Β· π₯) β (πβ(π΅ β {π₯}))))) |
13 | 12 | ibi 267 |
. . . . 5
β’ (π΅ β π½ β (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ βπ¦ β (πΎ β { 0 }) Β¬ (π¦ Β· π₯) β (πβ(π΅ β {π₯})))) |
14 | 13 | simp3d 1145 |
. . . 4
β’ (π΅ β π½ β βπ₯ β π΅ βπ¦ β (πΎ β { 0 }) Β¬ (π¦ Β· π₯) β (πβ(π΅ β {π₯}))) |
15 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = πΈ β (π¦ Β· π₯) = (π¦ Β· πΈ)) |
16 | | sneq 4597 |
. . . . . . . . 9
β’ (π₯ = πΈ β {π₯} = {πΈ}) |
17 | 16 | difeq2d 4083 |
. . . . . . . 8
β’ (π₯ = πΈ β (π΅ β {π₯}) = (π΅ β {πΈ})) |
18 | 17 | fveq2d 6847 |
. . . . . . 7
β’ (π₯ = πΈ β (πβ(π΅ β {π₯})) = (πβ(π΅ β {πΈ}))) |
19 | 15, 18 | eleq12d 2828 |
. . . . . 6
β’ (π₯ = πΈ β ((π¦ Β· π₯) β (πβ(π΅ β {π₯})) β (π¦ Β· πΈ) β (πβ(π΅ β {πΈ})))) |
20 | 19 | notbid 318 |
. . . . 5
β’ (π₯ = πΈ β (Β¬ (π¦ Β· π₯) β (πβ(π΅ β {π₯})) β Β¬ (π¦ Β· πΈ) β (πβ(π΅ β {πΈ})))) |
21 | | oveq1 7365 |
. . . . . . 7
β’ (π¦ = π΄ β (π¦ Β· πΈ) = (π΄ Β· πΈ)) |
22 | 21 | eleq1d 2819 |
. . . . . 6
β’ (π¦ = π΄ β ((π¦ Β· πΈ) β (πβ(π΅ β {πΈ})) β (π΄ Β· πΈ) β (πβ(π΅ β {πΈ})))) |
23 | 22 | notbid 318 |
. . . . 5
β’ (π¦ = π΄ β (Β¬ (π¦ Β· πΈ) β (πβ(π΅ β {πΈ})) β Β¬ (π΄ Β· πΈ) β (πβ(π΅ β {πΈ})))) |
24 | 20, 23 | rspc2v 3589 |
. . . 4
β’ ((πΈ β π΅ β§ π΄ β (πΎ β { 0 })) β (βπ₯ β π΅ βπ¦ β (πΎ β { 0 }) Β¬ (π¦ Β· π₯) β (πβ(π΅ β {π₯})) β Β¬ (π΄ Β· πΈ) β (πβ(π΅ β {πΈ})))) |
25 | 14, 24 | syl5com 31 |
. . 3
β’ (π΅ β π½ β ((πΈ β π΅ β§ π΄ β (πΎ β { 0 })) β Β¬ (π΄ Β· πΈ) β (πβ(π΅ β {πΈ})))) |
26 | 25 | impl 457 |
. 2
β’ (((π΅ β π½ β§ πΈ β π΅) β§ π΄ β (πΎ β { 0 })) β Β¬ (π΄ Β· πΈ) β (πβ(π΅ β {πΈ}))) |
27 | 1, 26 | sylan2br 596 |
1
β’ (((π΅ β π½ β§ πΈ β π΅) β§ (π΄ β πΎ β§ π΄ β 0 )) β Β¬ (π΄ Β· πΈ) β (πβ(π΅ β {πΈ}))) |