This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → 0 < ( dim ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 1m1e0 ⊢ ( 1 − 1 ) = 0
2 simpl ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → 𝐹 ∈ LVec )
3 simpr ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → 𝐹 ∈ DivRing )
4 drngring ⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ Ring )
5 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
6 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
7 5 6 ringidcl ⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
8 3 4 7 3syl ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
9 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
10 9 6 drngunz ⊢ ( 𝐹 ∈ DivRing → ( 1r ‘ 𝐹 ) ≠ ( 0g ‘ 𝐹 ) )
11 10 adantl ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → ( 1r ‘ 𝐹 ) ≠ ( 0g ‘ 𝐹 ) )
12 eqid ⊢ ( LSpan ‘ 𝐹 ) = ( LSpan ‘ 𝐹 )
13 eqid ⊢ ( 𝐹 ↾s ( ( LSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) ) = ( 𝐹 ↾s ( ( LSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) )
14 5 12 9 13 lsatdim ⊢ ( ( 𝐹 ∈ LVec ∧ ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 1r ‘ 𝐹 ) ≠ ( 0g ‘ 𝐹 ) ) → ( dim ‘ ( 𝐹 ↾s ( ( LSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) ) ) = 1 )
15 2 8 11 14 syl3anc ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → ( dim ‘ ( 𝐹 ↾s ( ( LSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) ) ) = 1 )
16 lveclmod ⊢ ( 𝐹 ∈ LVec → 𝐹 ∈ LMod )
17 16 adantr ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → 𝐹 ∈ LMod )
18 8 snssd ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → { ( 1r ‘ 𝐹 ) } ⊆ ( Base ‘ 𝐹 ) )
19 eqid ⊢ ( LSubSp ‘ 𝐹 ) = ( LSubSp ‘ 𝐹 )
20 5 19 12 lspcl ⊢ ( ( 𝐹 ∈ LMod ∧ { ( 1r ‘ 𝐹 ) } ⊆ ( Base ‘ 𝐹 ) ) → ( ( LSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) ∈ ( LSubSp ‘ 𝐹 ) )
21 17 18 20 syl2anc ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → ( ( LSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) ∈ ( LSubSp ‘ 𝐹 ) )
22 13 lssdimle ⊢ ( ( 𝐹 ∈ LVec ∧ ( ( LSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) ∈ ( LSubSp ‘ 𝐹 ) ) → ( dim ‘ ( 𝐹 ↾s ( ( LSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) ) ) ≤ ( dim ‘ 𝐹 ) )
23 2 21 22 syl2anc ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → ( dim ‘ ( 𝐹 ↾s ( ( LSpan ‘ 𝐹 ) ‘ { ( 1r ‘ 𝐹 ) } ) ) ) ≤ ( dim ‘ 𝐹 ) )
24 15 23 eqbrtrrd ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → 1 ≤ ( dim ‘ 𝐹 ) )
25 1nn0 ⊢ 1 ∈ ℕ0
26 dimcl ⊢ ( 𝐹 ∈ LVec → ( dim ‘ 𝐹 ) ∈ ℕ0* )
27 26 adantr ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → ( dim ‘ 𝐹 ) ∈ ℕ0* )
28 xnn0lem1lt ⊢ ( ( 1 ∈ ℕ0 ∧ ( dim ‘ 𝐹 ) ∈ ℕ0* ) → ( 1 ≤ ( dim ‘ 𝐹 ) ↔ ( 1 − 1 ) < ( dim ‘ 𝐹 ) ) )
29 25 27 28 sylancr ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → ( 1 ≤ ( dim ‘ 𝐹 ) ↔ ( 1 − 1 ) < ( dim ‘ 𝐹 ) ) )
30 24 29 mpbid ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → ( 1 − 1 ) < ( dim ‘ 𝐹 ) )
31 1 30 eqbrtrrid ⊢ ( ( 𝐹 ∈ LVec ∧ 𝐹 ∈ DivRing ) → 0 < ( dim ‘ 𝐹 ) )