Step | Hyp | Ref
| Expression |
1 | | lvecdim0.1 |
. . 3
β’ 0 =
(0gβπ) |
2 | 1 | lvecdim0i 32365 |
. 2
β’ ((π β LVec β§
(dimβπ) = 0) β
(Baseβπ) = { 0
}) |
3 | | simpl 484 |
. . . 4
β’ ((π β LVec β§
(Baseβπ) = { 0 }) β
π β
LVec) |
4 | | eqid 2733 |
. . . . . . . 8
β’
(LBasisβπ) =
(LBasisβπ) |
5 | 4 | lbsex 20671 |
. . . . . . 7
β’ (π β LVec β
(LBasisβπ) β
β
) |
6 | | n0 4310 |
. . . . . . 7
β’
((LBasisβπ)
β β
β βπ π β (LBasisβπ)) |
7 | 5, 6 | sylib 217 |
. . . . . 6
β’ (π β LVec β βπ π β (LBasisβπ)) |
8 | 3, 7 | syl 17 |
. . . . 5
β’ ((π β LVec β§
(Baseβπ) = { 0 }) β
βπ π β (LBasisβπ)) |
9 | 1 | fvexi 6860 |
. . . . . . . . . 10
β’ 0 β
V |
10 | 9 | snid 4626 |
. . . . . . . . 9
β’ 0 β {
0
} |
11 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β π = { 0 }) |
12 | 10, 11 | eleqtrrid 2841 |
. . . . . . . 8
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β 0 β π) |
13 | | simplll 774 |
. . . . . . . . 9
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β π β LVec) |
14 | 4 | lbslinds 21262 |
. . . . . . . . . 10
β’
(LBasisβπ)
β (LIndSβπ) |
15 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β π β (LBasisβπ)) |
16 | 14, 15 | sselid 3946 |
. . . . . . . . 9
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β π β (LIndSβπ)) |
17 | 1 | 0nellinds 32213 |
. . . . . . . . 9
β’ ((π β LVec β§ π β (LIndSβπ)) β Β¬ 0 β π) |
18 | 13, 16, 17 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β Β¬ 0 β π) |
19 | 12, 18 | pm2.65da 816 |
. . . . . . 7
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
Β¬ π = { 0
}) |
20 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
π β
(LBasisβπ)) |
21 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
22 | 21, 4 | lbsss 20582 |
. . . . . . . . . . . 12
β’ (π β (LBasisβπ) β π β (Baseβπ)) |
23 | 20, 22 | syl 17 |
. . . . . . . . . . 11
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
π β (Baseβπ)) |
24 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
(Baseβπ) = { 0
}) |
25 | 23, 24 | sseqtrd 3988 |
. . . . . . . . . 10
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
π β { 0
}) |
26 | | sssn 4790 |
. . . . . . . . . 10
β’ (π β { 0 } β (π = β
β¨ π = { 0 })) |
27 | 25, 26 | sylib 217 |
. . . . . . . . 9
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
(π = β
β¨ π = { 0 })) |
28 | 27 | orcomd 870 |
. . . . . . . 8
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
(π = { 0 } β¨ π = β
)) |
29 | 28 | ord 863 |
. . . . . . 7
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
(Β¬ π = { 0 } β
π =
β
)) |
30 | 19, 29 | mpd 15 |
. . . . . 6
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
π =
β
) |
31 | 30, 20 | eqeltrrd 2835 |
. . . . 5
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
β
β (LBasisβπ)) |
32 | 8, 31 | exlimddv 1939 |
. . . 4
β’ ((π β LVec β§
(Baseβπ) = { 0 }) β
β
β (LBasisβπ)) |
33 | 4 | dimval 32362 |
. . . 4
β’ ((π β LVec β§ β
β (LBasisβπ))
β (dimβπ) =
(β―ββ
)) |
34 | 3, 32, 33 | syl2anc 585 |
. . 3
β’ ((π β LVec β§
(Baseβπ) = { 0 }) β
(dimβπ) =
(β―ββ
)) |
35 | | hash0 14276 |
. . 3
β’
(β―ββ
) = 0 |
36 | 34, 35 | eqtrdi 2789 |
. 2
β’ ((π β LVec β§
(Baseβπ) = { 0 }) β
(dimβπ) =
0) |
37 | 2, 36 | impbida 800 |
1
β’ (π β LVec β
((dimβπ) = 0 β
(Baseβπ) = { 0
})) |