Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. 2
β’ (((πΉ β (LIndSβπ) β§ πΈ β πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β πΈ β πΉ) |
2 | | eldifsn 4748 |
. . . 4
β’ (π΄ β (πΎ β { 0 }) β (π΄ β πΎ β§ π΄ β 0 )) |
3 | 2 | biimpri 227 |
. . 3
β’ ((π΄ β πΎ β§ π΄ β 0 ) β π΄ β (πΎ β { 0 })) |
4 | 3 | adantl 483 |
. 2
β’ (((πΉ β (LIndSβπ) β§ πΈ β πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β π΄ β (πΎ β { 0 })) |
5 | | elfvdm 6880 |
. . . . . 6
β’ (πΉ β (LIndSβπ) β π β dom LIndS) |
6 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
7 | | lindfind.s |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
8 | | lindfind.n |
. . . . . . 7
β’ π = (LSpanβπ) |
9 | | lindfind.l |
. . . . . . 7
β’ πΏ = (Scalarβπ) |
10 | | lindfind.k |
. . . . . . 7
β’ πΎ = (BaseβπΏ) |
11 | | lindfind.z |
. . . . . . 7
β’ 0 =
(0gβπΏ) |
12 | 6, 7, 8, 9, 10, 11 | islinds2 21235 |
. . . . . 6
β’ (π β dom LIndS β (πΉ β (LIndSβπ) β (πΉ β (Baseβπ) β§ βπ β πΉ βπ β (πΎ β { 0 }) Β¬ (π Β· π) β (πβ(πΉ β {π}))))) |
13 | 5, 12 | syl 17 |
. . . . 5
β’ (πΉ β (LIndSβπ) β (πΉ β (LIndSβπ) β (πΉ β (Baseβπ) β§ βπ β πΉ βπ β (πΎ β { 0 }) Β¬ (π Β· π) β (πβ(πΉ β {π}))))) |
14 | 13 | ibi 267 |
. . . 4
β’ (πΉ β (LIndSβπ) β (πΉ β (Baseβπ) β§ βπ β πΉ βπ β (πΎ β { 0 }) Β¬ (π Β· π) β (πβ(πΉ β {π})))) |
15 | 14 | simprd 497 |
. . 3
β’ (πΉ β (LIndSβπ) β βπ β πΉ βπ β (πΎ β { 0 }) Β¬ (π Β· π) β (πβ(πΉ β {π}))) |
16 | 15 | ad2antrr 725 |
. 2
β’ (((πΉ β (LIndSβπ) β§ πΈ β πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β βπ β πΉ βπ β (πΎ β { 0 }) Β¬ (π Β· π) β (πβ(πΉ β {π}))) |
17 | | oveq2 7366 |
. . . . 5
β’ (π = πΈ β (π Β· π) = (π Β· πΈ)) |
18 | | sneq 4597 |
. . . . . . 7
β’ (π = πΈ β {π} = {πΈ}) |
19 | 18 | difeq2d 4083 |
. . . . . 6
β’ (π = πΈ β (πΉ β {π}) = (πΉ β {πΈ})) |
20 | 19 | fveq2d 6847 |
. . . . 5
β’ (π = πΈ β (πβ(πΉ β {π})) = (πβ(πΉ β {πΈ}))) |
21 | 17, 20 | eleq12d 2828 |
. . . 4
β’ (π = πΈ β ((π Β· π) β (πβ(πΉ β {π})) β (π Β· πΈ) β (πβ(πΉ β {πΈ})))) |
22 | 21 | notbid 318 |
. . 3
β’ (π = πΈ β (Β¬ (π Β· π) β (πβ(πΉ β {π})) β Β¬ (π Β· πΈ) β (πβ(πΉ β {πΈ})))) |
23 | | oveq1 7365 |
. . . . 5
β’ (π = π΄ β (π Β· πΈ) = (π΄ Β· πΈ)) |
24 | 23 | eleq1d 2819 |
. . . 4
β’ (π = π΄ β ((π Β· πΈ) β (πβ(πΉ β {πΈ})) β (π΄ Β· πΈ) β (πβ(πΉ β {πΈ})))) |
25 | 24 | notbid 318 |
. . 3
β’ (π = π΄ β (Β¬ (π Β· πΈ) β (πβ(πΉ β {πΈ})) β Β¬ (π΄ Β· πΈ) β (πβ(πΉ β {πΈ})))) |
26 | 22, 25 | rspc2va 3590 |
. 2
β’ (((πΈ β πΉ β§ π΄ β (πΎ β { 0 })) β§ βπ β πΉ βπ β (πΎ β { 0 }) Β¬ (π Β· π) β (πβ(πΉ β {π}))) β Β¬ (π΄ Β· πΈ) β (πβ(πΉ β {πΈ}))) |
27 | 1, 4, 16, 26 | syl21anc 837 |
1
β’ (((πΉ β (LIndSβπ) β§ πΈ β πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β Β¬ (π΄ Β· πΈ) β (πβ(πΉ β {πΈ}))) |