Metamath Proof Explorer

Theorem drngdimgt0

Description: The dimension of a vector space that is also a division ring is greater than zero. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion drngdimgt0 
|- ( ( F e. LVec /\ F e. DivRing ) -> 0 < ( dim ` F ) )

Proof

Step Hyp Ref Expression
1 1m1e0 
 |-  ( 1 - 1 ) = 0
2 simpl 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> F e. LVec )
3 simpr 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> F e. DivRing )
4 drngring 
 |-  ( F e. DivRing -> F e. Ring )
5 eqid 
 |-  ( Base ` F ) = ( Base ` F )
6 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
7 5 6 ringidcl 
 |-  ( F e. Ring -> ( 1r ` F ) e. ( Base ` F ) )
8 3 4 7 3syl 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> ( 1r ` F ) e. ( Base ` F ) )
9 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
10 9 6 drngunz 
 |-  ( F e. DivRing -> ( 1r ` F ) =/= ( 0g ` F ) )
11 10 adantl 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> ( 1r ` F ) =/= ( 0g ` F ) )
12 eqid 
 |-  ( LSpan ` F ) = ( LSpan ` F )
13 eqid 
 |-  ( F |`s ( ( LSpan ` F ) ` { ( 1r ` F ) } ) ) = ( F |`s ( ( LSpan ` F ) ` { ( 1r ` F ) } ) )
14 5 12 9 13 lsatdim 
 |-  ( ( F e. LVec /\ ( 1r ` F ) e. ( Base ` F ) /\ ( 1r ` F ) =/= ( 0g ` F ) ) -> ( dim ` ( F |`s ( ( LSpan ` F ) ` { ( 1r ` F ) } ) ) ) = 1 )
15 2 8 11 14 syl3anc 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> ( dim ` ( F |`s ( ( LSpan ` F ) ` { ( 1r ` F ) } ) ) ) = 1 )
16 lveclmod 
 |-  ( F e. LVec -> F e. LMod )
17 16 adantr 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> F e. LMod )
18 8 snssd 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> { ( 1r ` F ) } C_ ( Base ` F ) )
19 eqid 
 |-  ( LSubSp ` F ) = ( LSubSp ` F )
20 5 19 12 lspcl 
 |-  ( ( F e. LMod /\ { ( 1r ` F ) } C_ ( Base ` F ) ) -> ( ( LSpan ` F ) ` { ( 1r ` F ) } ) e. ( LSubSp ` F ) )
21 17 18 20 syl2anc 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> ( ( LSpan ` F ) ` { ( 1r ` F ) } ) e. ( LSubSp ` F ) )
22 13 lssdimle 
 |-  ( ( F e. LVec /\ ( ( LSpan ` F ) ` { ( 1r ` F ) } ) e. ( LSubSp ` F ) ) -> ( dim ` ( F |`s ( ( LSpan ` F ) ` { ( 1r ` F ) } ) ) ) <_ ( dim ` F ) )
23 2 21 22 syl2anc 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> ( dim ` ( F |`s ( ( LSpan ` F ) ` { ( 1r ` F ) } ) ) ) <_ ( dim ` F ) )
24 15 23 eqbrtrrd 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> 1 <_ ( dim ` F ) )
25 1nn0 
 |-  1 e. NN0
26 dimcl 
 |-  ( F e. LVec -> ( dim ` F ) e. NN0* )
27 26 adantr 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> ( dim ` F ) e. NN0* )
28 xnn0lem1lt 
 |-  ( ( 1 e. NN0 /\ ( dim ` F ) e. NN0* ) -> ( 1 <_ ( dim ` F ) <-> ( 1 - 1 ) < ( dim ` F ) ) )
29 25 27 28 sylancr 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> ( 1 <_ ( dim ` F ) <-> ( 1 - 1 ) < ( dim ` F ) ) )
30 24 29 mpbid 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> ( 1 - 1 ) < ( dim ` F ) )
31 1 30 eqbrtrrid 
 |-  ( ( F e. LVec /\ F e. DivRing ) -> 0 < ( dim ` F ) )