Database
BASIC ALGEBRAIC STRUCTURES
Rings
Left regular elements and domains
idomringd
Next ⟩
Division rings and fields
Metamath Proof Explorer
Ascii
Unicode
Theorem
idomringd
Description:
An integral domain is a ring.
(Contributed by
Thierry Arnoux
, 22-Mar-2025)
Ref
Expression
Hypothesis
idomringd.1
⊢
φ
→
R
∈
IDomn
Assertion
idomringd
⊢
φ
→
R
∈
Ring
Proof
Step
Hyp
Ref
Expression
1
idomringd.1
⊢
φ
→
R
∈
IDomn
2
1
idomcringd
⊢
φ
→
R
∈
CRing
3
2
crngringd
⊢
φ
→
R
∈
Ring