Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. 2
β’ (((πΉ LIndF π β§ πΈ β dom πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β πΈ β dom πΉ) |
2 | | eldifsn 4748 |
. . . 4
β’ (π΄ β (πΎ β { 0 }) β (π΄ β πΎ β§ π΄ β 0 )) |
3 | 2 | biimpri 227 |
. . 3
β’ ((π΄ β πΎ β§ π΄ β 0 ) β π΄ β (πΎ β { 0 })) |
4 | 3 | adantl 483 |
. 2
β’ (((πΉ LIndF π β§ πΈ β dom πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β π΄ β (πΎ β { 0 })) |
5 | | simpll 766 |
. . . 4
β’ (((πΉ LIndF π β§ πΈ β dom πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β πΉ LIndF π) |
6 | | lindfind.l |
. . . . . . 7
β’ πΏ = (Scalarβπ) |
7 | | lindfind.k |
. . . . . . 7
β’ πΎ = (BaseβπΏ) |
8 | 6, 7 | elbasfv 17094 |
. . . . . 6
β’ (π΄ β πΎ β π β V) |
9 | 8 | ad2antrl 727 |
. . . . 5
β’ (((πΉ LIndF π β§ πΈ β dom πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β π β V) |
10 | | rellindf 21230 |
. . . . . . 7
β’ Rel
LIndF |
11 | 10 | brrelex1i 5689 |
. . . . . 6
β’ (πΉ LIndF π β πΉ β V) |
12 | 11 | ad2antrr 725 |
. . . . 5
β’ (((πΉ LIndF π β§ πΈ β dom πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β πΉ β V) |
13 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
14 | | lindfind.s |
. . . . . 6
β’ Β· = (
Β·π βπ) |
15 | | lindfind.n |
. . . . . 6
β’ π = (LSpanβπ) |
16 | | lindfind.z |
. . . . . 6
β’ 0 =
(0gβπΏ) |
17 | 13, 14, 15, 6, 7, 16 | islindf 21234 |
. . . . 5
β’ ((π β V β§ πΉ β V) β (πΉ LIndF π β (πΉ:dom πΉβΆ(Baseβπ) β§ βπ β dom πΉβπ β (πΎ β { 0 }) Β¬ (π Β· (πΉβπ)) β (πβ(πΉ β (dom πΉ β {π})))))) |
18 | 9, 12, 17 | syl2anc 585 |
. . . 4
β’ (((πΉ LIndF π β§ πΈ β dom πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β (πΉ LIndF π β (πΉ:dom πΉβΆ(Baseβπ) β§ βπ β dom πΉβπ β (πΎ β { 0 }) Β¬ (π Β· (πΉβπ)) β (πβ(πΉ β (dom πΉ β {π})))))) |
19 | 5, 18 | mpbid 231 |
. . 3
β’ (((πΉ LIndF π β§ πΈ β dom πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β (πΉ:dom πΉβΆ(Baseβπ) β§ βπ β dom πΉβπ β (πΎ β { 0 }) Β¬ (π Β· (πΉβπ)) β (πβ(πΉ β (dom πΉ β {π}))))) |
20 | 19 | simprd 497 |
. 2
β’ (((πΉ LIndF π β§ πΈ β dom πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β βπ β dom πΉβπ β (πΎ β { 0 }) Β¬ (π Β· (πΉβπ)) β (πβ(πΉ β (dom πΉ β {π})))) |
21 | | fveq2 6843 |
. . . . . 6
β’ (π = πΈ β (πΉβπ) = (πΉβπΈ)) |
22 | 21 | oveq2d 7374 |
. . . . 5
β’ (π = πΈ β (π Β· (πΉβπ)) = (π Β· (πΉβπΈ))) |
23 | | sneq 4597 |
. . . . . . . 8
β’ (π = πΈ β {π} = {πΈ}) |
24 | 23 | difeq2d 4083 |
. . . . . . 7
β’ (π = πΈ β (dom πΉ β {π}) = (dom πΉ β {πΈ})) |
25 | 24 | imaeq2d 6014 |
. . . . . 6
β’ (π = πΈ β (πΉ β (dom πΉ β {π})) = (πΉ β (dom πΉ β {πΈ}))) |
26 | 25 | fveq2d 6847 |
. . . . 5
β’ (π = πΈ β (πβ(πΉ β (dom πΉ β {π}))) = (πβ(πΉ β (dom πΉ β {πΈ})))) |
27 | 22, 26 | eleq12d 2828 |
. . . 4
β’ (π = πΈ β ((π Β· (πΉβπ)) β (πβ(πΉ β (dom πΉ β {π}))) β (π Β· (πΉβπΈ)) β (πβ(πΉ β (dom πΉ β {πΈ}))))) |
28 | 27 | notbid 318 |
. . 3
β’ (π = πΈ β (Β¬ (π Β· (πΉβπ)) β (πβ(πΉ β (dom πΉ β {π}))) β Β¬ (π Β· (πΉβπΈ)) β (πβ(πΉ β (dom πΉ β {πΈ}))))) |
29 | | oveq1 7365 |
. . . . 5
β’ (π = π΄ β (π Β· (πΉβπΈ)) = (π΄ Β· (πΉβπΈ))) |
30 | 29 | eleq1d 2819 |
. . . 4
β’ (π = π΄ β ((π Β· (πΉβπΈ)) β (πβ(πΉ β (dom πΉ β {πΈ}))) β (π΄ Β· (πΉβπΈ)) β (πβ(πΉ β (dom πΉ β {πΈ}))))) |
31 | 30 | notbid 318 |
. . 3
β’ (π = π΄ β (Β¬ (π Β· (πΉβπΈ)) β (πβ(πΉ β (dom πΉ β {πΈ}))) β Β¬ (π΄ Β· (πΉβπΈ)) β (πβ(πΉ β (dom πΉ β {πΈ}))))) |
32 | 28, 31 | rspc2va 3590 |
. 2
β’ (((πΈ β dom πΉ β§ π΄ β (πΎ β { 0 })) β§ βπ β dom πΉβπ β (πΎ β { 0 }) Β¬ (π Β· (πΉβπ)) β (πβ(πΉ β (dom πΉ β {π})))) β Β¬ (π΄ Β· (πΉβπΈ)) β (πβ(πΉ β (dom πΉ β {πΈ})))) |
33 | 1, 4, 20, 32 | syl21anc 837 |
1
β’ (((πΉ LIndF π β§ πΈ β dom πΉ) β§ (π΄ β πΎ β§ π΄ β 0 )) β Β¬ (π΄ Β· (πΉβπΈ)) β (πβ(πΉ β (dom πΉ β {πΈ})))) |