Step | Hyp | Ref
| Expression |
1 | | islbs2.v |
. . . . 5
β’ π = (Baseβπ) |
2 | | islbs2.j |
. . . . 5
β’ π½ = (LBasisβπ) |
3 | 1, 2 | lbsss 20554 |
. . . 4
β’ (π΅ β π½ β π΅ β π) |
4 | 3 | adantl 483 |
. . 3
β’ ((π β LVec β§ π΅ β π½) β π΅ β π) |
5 | | islbs2.n |
. . . . 5
β’ π = (LSpanβπ) |
6 | 1, 2, 5 | lbssp 20556 |
. . . 4
β’ (π΅ β π½ β (πβπ΅) = π) |
7 | 6 | adantl 483 |
. . 3
β’ ((π β LVec β§ π΅ β π½) β (πβπ΅) = π) |
8 | | lveclmod 20583 |
. . . . . . 7
β’ (π β LVec β π β LMod) |
9 | | eqid 2737 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
10 | 9 | lvecdrng 20582 |
. . . . . . . 8
β’ (π β LVec β
(Scalarβπ) β
DivRing) |
11 | | eqid 2737 |
. . . . . . . . 9
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
12 | | eqid 2737 |
. . . . . . . . 9
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
13 | 11, 12 | drngunz 20217 |
. . . . . . . 8
β’
((Scalarβπ)
β DivRing β (1rβ(Scalarβπ)) β
(0gβ(Scalarβπ))) |
14 | 10, 13 | syl 17 |
. . . . . . 7
β’ (π β LVec β
(1rβ(Scalarβπ)) β
(0gβ(Scalarβπ))) |
15 | 8, 14 | jca 513 |
. . . . . 6
β’ (π β LVec β (π β LMod β§
(1rβ(Scalarβπ)) β
(0gβ(Scalarβπ)))) |
16 | 2, 5, 9, 12, 11 | lbsind2 20558 |
. . . . . 6
β’ (((π β LMod β§
(1rβ(Scalarβπ)) β
(0gβ(Scalarβπ))) β§ π΅ β π½ β§ π₯ β π΅) β Β¬ π₯ β (πβ(π΅ β {π₯}))) |
17 | 15, 16 | syl3an1 1164 |
. . . . 5
β’ ((π β LVec β§ π΅ β π½ β§ π₯ β π΅) β Β¬ π₯ β (πβ(π΅ β {π₯}))) |
18 | 17 | 3expa 1119 |
. . . 4
β’ (((π β LVec β§ π΅ β π½) β§ π₯ β π΅) β Β¬ π₯ β (πβ(π΅ β {π₯}))) |
19 | 18 | ralrimiva 3144 |
. . 3
β’ ((π β LVec β§ π΅ β π½) β βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯}))) |
20 | 4, 7, 19 | 3jca 1129 |
. 2
β’ ((π β LVec β§ π΅ β π½) β (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) |
21 | | simpr1 1195 |
. . 3
β’ ((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β π΅ β π) |
22 | | simpr2 1196 |
. . 3
β’ ((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β (πβπ΅) = π) |
23 | | id 22 |
. . . . . . . 8
β’ (π₯ = π¦ β π₯ = π¦) |
24 | | sneq 4601 |
. . . . . . . . . 10
β’ (π₯ = π¦ β {π₯} = {π¦}) |
25 | 24 | difeq2d 4087 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π΅ β {π₯}) = (π΅ β {π¦})) |
26 | 25 | fveq2d 6851 |
. . . . . . . 8
β’ (π₯ = π¦ β (πβ(π΅ β {π₯})) = (πβ(π΅ β {π¦}))) |
27 | 23, 26 | eleq12d 2832 |
. . . . . . 7
β’ (π₯ = π¦ β (π₯ β (πβ(π΅ β {π₯})) β π¦ β (πβ(π΅ β {π¦})))) |
28 | 27 | notbid 318 |
. . . . . 6
β’ (π₯ = π¦ β (Β¬ π₯ β (πβ(π΅ β {π₯})) β Β¬ π¦ β (πβ(π΅ β {π¦})))) |
29 | | simplr3 1218 |
. . . . . 6
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯}))) |
30 | | simprl 770 |
. . . . . 6
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π¦ β π΅) |
31 | 28, 29, 30 | rspcdva 3585 |
. . . . 5
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β Β¬ π¦ β (πβ(π΅ β {π¦}))) |
32 | | simpll 766 |
. . . . . . . 8
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π β LVec) |
33 | | simprr 772 |
. . . . . . . . 9
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))})) |
34 | | eldifsn 4752 |
. . . . . . . . 9
β’ (π§ β
((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) β (π§ β (Baseβ(Scalarβπ)) β§ π§ β
(0gβ(Scalarβπ)))) |
35 | 33, 34 | sylib 217 |
. . . . . . . 8
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β (π§ β (Baseβ(Scalarβπ)) β§ π§ β
(0gβ(Scalarβπ)))) |
36 | 21 | adantr 482 |
. . . . . . . . 9
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π΅ β π) |
37 | 36, 30 | sseldd 3950 |
. . . . . . . 8
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π¦ β π) |
38 | | eqid 2737 |
. . . . . . . . 9
β’ (
Β·π βπ) = ( Β·π
βπ) |
39 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
40 | 1, 9, 38, 39, 11, 5 | lspsnvs 20591 |
. . . . . . . 8
β’ ((π β LVec β§ (π§ β
(Baseβ(Scalarβπ)) β§ π§ β
(0gβ(Scalarβπ))) β§ π¦ β π) β (πβ{(π§( Β·π
βπ)π¦)}) = (πβ{π¦})) |
41 | 32, 35, 37, 40 | syl3anc 1372 |
. . . . . . 7
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β (πβ{(π§( Β·π
βπ)π¦)}) = (πβ{π¦})) |
42 | 41 | sseq1d 3980 |
. . . . . 6
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β ((πβ{(π§( Β·π
βπ)π¦)}) β (πβ(π΅ β {π¦})) β (πβ{π¦}) β (πβ(π΅ β {π¦})))) |
43 | | eqid 2737 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
44 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β π β LMod) |
45 | 44 | adantr 482 |
. . . . . . 7
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π β LMod) |
46 | 36 | ssdifssd 4107 |
. . . . . . . 8
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β (π΅ β {π¦}) β π) |
47 | 1, 43, 5 | lspcl 20453 |
. . . . . . . 8
β’ ((π β LMod β§ (π΅ β {π¦}) β π) β (πβ(π΅ β {π¦})) β (LSubSpβπ)) |
48 | 45, 46, 47 | syl2anc 585 |
. . . . . . 7
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β (πβ(π΅ β {π¦})) β (LSubSpβπ)) |
49 | 35 | simpld 496 |
. . . . . . . 8
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β π§ β (Baseβ(Scalarβπ))) |
50 | 1, 9, 38, 39 | lmodvscl 20355 |
. . . . . . . 8
β’ ((π β LMod β§ π§ β
(Baseβ(Scalarβπ)) β§ π¦ β π) β (π§( Β·π
βπ)π¦) β π) |
51 | 45, 49, 37, 50 | syl3anc 1372 |
. . . . . . 7
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β (π§( Β·π
βπ)π¦) β π) |
52 | 1, 43, 5, 45, 48, 51 | lspsnel5 20472 |
. . . . . 6
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β ((π§( Β·π
βπ)π¦) β (πβ(π΅ β {π¦})) β (πβ{(π§( Β·π
βπ)π¦)}) β (πβ(π΅ β {π¦})))) |
53 | 1, 43, 5, 45, 48, 37 | lspsnel5 20472 |
. . . . . 6
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β (π¦ β (πβ(π΅ β {π¦})) β (πβ{π¦}) β (πβ(π΅ β {π¦})))) |
54 | 42, 52, 53 | 3bitr4d 311 |
. . . . 5
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β ((π§( Β·π
βπ)π¦) β (πβ(π΅ β {π¦})) β π¦ β (πβ(π΅ β {π¦})))) |
55 | 31, 54 | mtbird 325 |
. . . 4
β’ (((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β§ (π¦ β π΅ β§ π§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}))) β Β¬ (π§( Β·π
βπ)π¦) β (πβ(π΅ β {π¦}))) |
56 | 55 | ralrimivva 3198 |
. . 3
β’ ((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β βπ¦ β π΅ βπ§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π§( Β·π
βπ)π¦) β (πβ(π΅ β {π¦}))) |
57 | 1, 9, 38, 39, 2, 5, 11 | islbs 20553 |
. . . 4
β’ (π β LVec β (π΅ β π½ β (π΅ β π β§ (πβπ΅) = π β§ βπ¦ β π΅ βπ§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π§( Β·π
βπ)π¦) β (πβ(π΅ β {π¦}))))) |
58 | 57 | adantr 482 |
. . 3
β’ ((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β (π΅ β π½ β (π΅ β π β§ (πβπ΅) = π β§ βπ¦ β π΅ βπ§ β ((Baseβ(Scalarβπ)) β
{(0gβ(Scalarβπ))}) Β¬ (π§( Β·π
βπ)π¦) β (πβ(π΅ β {π¦}))))) |
59 | 21, 22, 56, 58 | mpbir3and 1343 |
. 2
β’ ((π β LVec β§ (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯})))) β π΅ β π½) |
60 | 20, 59 | impbida 800 |
1
β’ (π β LVec β (π΅ β π½ β (π΅ β π β§ (πβπ΅) = π β§ βπ₯ β π΅ Β¬ π₯ β (πβ(π΅ β {π₯}))))) |