Database
BASIC ALGEBRAIC STRUCTURES
Division rings and fields
Definition and basic properties
flddrngd
Next ⟩
fldcrngd
Metamath Proof Explorer
Ascii
Unicode
Theorem
flddrngd
Description:
A field is a division ring.
(Contributed by
SN
, 17-Jan-2025)
Ref
Expression
Hypothesis
flddrngd.1
⊢
φ
→
R
∈
Field
Assertion
flddrngd
⊢
φ
→
R
∈
DivRing
Proof
Step
Hyp
Ref
Expression
1
flddrngd.1
⊢
φ
→
R
∈
Field
2
isfld
⊢
R
∈
Field
↔
R
∈
DivRing
∧
R
∈
CRing
3
2
simplbi
⊢
R
∈
Field
→
R
∈
DivRing
4
1
3
syl
⊢
φ
→
R
∈
DivRing