Step | Hyp | Ref
| Expression |
1 | | pssnel 4431 |
. . 3
β’ (πΆ β π΅ β βπ₯(π₯ β π΅ β§ Β¬ π₯ β πΆ)) |
2 | 1 | 3ad2ant3 1136 |
. 2
β’ (((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β βπ₯(π₯ β π΅ β§ Β¬ π₯ β πΆ)) |
3 | | simpl2 1193 |
. . . . . 6
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β π΅ β π½) |
4 | | lbspss.v |
. . . . . . 7
β’ π = (Baseβπ) |
5 | | lbsind2.j |
. . . . . . 7
β’ π½ = (LBasisβπ) |
6 | 4, 5 | lbsss 20553 |
. . . . . 6
β’ (π΅ β π½ β π΅ β π) |
7 | 3, 6 | syl 17 |
. . . . 5
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β π΅ β π) |
8 | | simprl 770 |
. . . . 5
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β π₯ β π΅) |
9 | 7, 8 | sseldd 3946 |
. . . 4
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β π₯ β π) |
10 | | simpl1l 1225 |
. . . . . 6
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β π β LMod) |
11 | 7 | ssdifssd 4103 |
. . . . . 6
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β (π΅ β {π₯}) β π) |
12 | | simpl3 1194 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β πΆ β π΅) |
13 | 12 | pssssd 4058 |
. . . . . . . . . 10
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β πΆ β π΅) |
14 | 13 | sseld 3944 |
. . . . . . . . 9
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β (π¦ β πΆ β π¦ β π΅)) |
15 | | simprr 772 |
. . . . . . . . . . 11
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β Β¬ π₯ β πΆ) |
16 | | eleq1w 2817 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β (π¦ β πΆ β π₯ β πΆ)) |
17 | 16 | notbid 318 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (Β¬ π¦ β πΆ β Β¬ π₯ β πΆ)) |
18 | 15, 17 | syl5ibrcom 247 |
. . . . . . . . . 10
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β (π¦ = π₯ β Β¬ π¦ β πΆ)) |
19 | 18 | necon2ad 2955 |
. . . . . . . . 9
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β (π¦ β πΆ β π¦ β π₯)) |
20 | 14, 19 | jcad 514 |
. . . . . . . 8
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β (π¦ β πΆ β (π¦ β π΅ β§ π¦ β π₯))) |
21 | | eldifsn 4748 |
. . . . . . . 8
β’ (π¦ β (π΅ β {π₯}) β (π¦ β π΅ β§ π¦ β π₯)) |
22 | 20, 21 | syl6ibr 252 |
. . . . . . 7
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β (π¦ β πΆ β π¦ β (π΅ β {π₯}))) |
23 | 22 | ssrdv 3951 |
. . . . . 6
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β πΆ β (π΅ β {π₯})) |
24 | | lbsind2.n |
. . . . . . 7
β’ π = (LSpanβπ) |
25 | 4, 24 | lspss 20460 |
. . . . . 6
β’ ((π β LMod β§ (π΅ β {π₯}) β π β§ πΆ β (π΅ β {π₯})) β (πβπΆ) β (πβ(π΅ β {π₯}))) |
26 | 10, 11, 23, 25 | syl3anc 1372 |
. . . . 5
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β (πβπΆ) β (πβ(π΅ β {π₯}))) |
27 | | simpl1r 1226 |
. . . . . 6
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β 1 β 0 ) |
28 | | lbsind2.f |
. . . . . . 7
β’ πΉ = (Scalarβπ) |
29 | | lbsind2.o |
. . . . . . 7
β’ 1 =
(1rβπΉ) |
30 | | lbsind2.z |
. . . . . . 7
β’ 0 =
(0gβπΉ) |
31 | 5, 24, 28, 29, 30 | lbsind2 20557 |
. . . . . 6
β’ (((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ π₯ β π΅) β Β¬ π₯ β (πβ(π΅ β {π₯}))) |
32 | 10, 27, 3, 8, 31 | syl211anc 1377 |
. . . . 5
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β Β¬ π₯ β (πβ(π΅ β {π₯}))) |
33 | 26, 32 | ssneldd 3948 |
. . . 4
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β Β¬ π₯ β (πβπΆ)) |
34 | | nelne1 3038 |
. . . 4
β’ ((π₯ β π β§ Β¬ π₯ β (πβπΆ)) β π β (πβπΆ)) |
35 | 9, 33, 34 | syl2anc 585 |
. . 3
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β π β (πβπΆ)) |
36 | 35 | necomd 2996 |
. 2
β’ ((((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β§ (π₯ β π΅ β§ Β¬ π₯ β πΆ)) β (πβπΆ) β π) |
37 | 2, 36 | exlimddv 1939 |
1
β’ (((π β LMod β§ 1 β 0 ) β§ π΅ β π½ β§ πΆ β π΅) β (πβπΆ) β π) |