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 ‘ 𝐹 ) )