| Step | Hyp | Ref
| Expression |
|---|
| 1 | | lvecdim0.1 |
. . 3
β’ 0 =
(0gβπ) |
| 2 | 1 | lvecdim0i 32685 |
. 2
β’ ((π β LVec β§
(dimβπ) = 0) β
(Baseβπ) = { 0
}) |
| 3 | | simpl 483 |
. . . 4
β’ ((π β LVec β§
(Baseβπ) = { 0 }) β
π β
LVec) |
| 4 | | eqid 2732 |
. . . . . . . 8
β’
(LBasisβπ) =
(LBasisβπ) |
| 5 | 4 | lbsex 20777 |
. . . . . . 7
β’ (π β LVec β
(LBasisβπ) β
β
) |
| 6 | | n0 4346 |
. . . . . . 7
β’
((LBasisβπ)
β β
β βπ π β (LBasisβπ)) |
| 7 | 5, 6 | sylib 217 |
. . . . . 6
β’ (π β LVec β βπ π β (LBasisβπ)) |
| 8 | 3, 7 | syl 17 |
. . . . 5
β’ ((π β LVec β§
(Baseβπ) = { 0 }) β
βπ π β (LBasisβπ)) |
| 9 | 1 | fvexi 6905 |
. . . . . . . . . 10
β’ 0 β
V |
| 10 | 9 | snid 4664 |
. . . . . . . . 9
β’ 0 β {
0
} |
| 11 | | simpr 485 |
. . . . . . . . 9
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β π = { 0 }) |
| 12 | 10, 11 | eleqtrrid 2840 |
. . . . . . . 8
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β 0 β π) |
| 13 | | simplll 773 |
. . . . . . . . 9
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β π β LVec) |
| 14 | 4 | lbslinds 21387 |
. . . . . . . . . 10
β’
(LBasisβπ)
β (LIndSβπ) |
| 15 | | simplr 767 |
. . . . . . . . . 10
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β π β (LBasisβπ)) |
| 16 | 14, 15 | sselid 3980 |
. . . . . . . . 9
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β π β (LIndSβπ)) |
| 17 | 1 | 0nellinds 32478 |
. . . . . . . . 9
β’ ((π β LVec β§ π β (LIndSβπ)) β Β¬ 0 β π) |
| 18 | 13, 16, 17 | syl2anc 584 |
. . . . . . . 8
β’ ((((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β§
π = { 0 }) β Β¬ 0 β π) |
| 19 | 12, 18 | pm2.65da 815 |
. . . . . . 7
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
Β¬ π = { 0
}) |
| 20 | | simpr 485 |
. . . . . . . . . . . 12
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
π β
(LBasisβπ)) |
| 21 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
| 22 | 21, 4 | lbsss 20687 |
. . . . . . . . . . . 12
β’ (π β (LBasisβπ) β π β (Baseβπ)) |
| 23 | 20, 22 | syl 17 |
. . . . . . . . . . 11
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
π β (Baseβπ)) |
| 24 | | simplr 767 |
. . . . . . . . . . 11
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
(Baseβπ) = { 0
}) |
| 25 | 23, 24 | sseqtrd 4022 |
. . . . . . . . . 10
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
π β { 0
}) |
| 26 | | sssn 4829 |
. . . . . . . . . 10
β’ (π β { 0 } β (π = β
β¨ π = { 0 })) |
| 27 | 25, 26 | sylib 217 |
. . . . . . . . 9
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
(π = β
β¨ π = { 0 })) |
| 28 | 27 | orcomd 869 |
. . . . . . . 8
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
(π = { 0 } β¨ π = β
)) |
| 29 | 28 | ord 862 |
. . . . . . 7
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
(Β¬ π = { 0 } β
π =
β
)) |
| 30 | 19, 29 | mpd 15 |
. . . . . 6
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
π =
β
) |
| 31 | 30, 20 | eqeltrrd 2834 |
. . . . 5
β’ (((π β LVec β§
(Baseβπ) = { 0 }) β§
π β
(LBasisβπ)) β
β
β (LBasisβπ)) |
| 32 | 8, 31 | exlimddv 1938 |
. . . 4
β’ ((π β LVec β§
(Baseβπ) = { 0 }) β
β
β (LBasisβπ)) |
| 33 | 4 | dimval 32681 |
. . . 4
β’ ((π β LVec β§ β
β (LBasisβπ))
β (dimβπ) =
(β―ββ
)) |
| 34 | 3, 32, 33 | syl2anc 584 |
. . 3
β’ ((π β LVec β§
(Baseβπ) = { 0 }) β
(dimβπ) =
(β―ββ
)) |
| 35 | | hash0 14326 |
. . 3
β’
(β―ββ
) = 0 |
| 36 | 34, 35 | eqtrdi 2788 |
. 2
β’ ((π β LVec β§
(Baseβπ) = { 0 }) β
(dimβπ) =
0) |
| 37 | 2, 36 | impbida 799 |
1
β’ (π β LVec β
((dimβπ) = 0 β
(Baseβπ) = { 0
})) |
