Database
BASIC ALGEBRAIC STRUCTURES
Ideals
Principal ideal rings. Divisibility in the integers
lpirring
Next ⟩
drnglpir
Metamath Proof Explorer
Ascii
Unicode
Theorem
lpirring
Description:
Principal ideal rings are rings.
(Contributed by
Stefan O'Rear
, 24-Jan-2015)
Ref
Expression
Assertion
lpirring
⊢
R
∈
LPIR
→
R
∈
Ring
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
LPIdeal
⁡
R
=
LPIdeal
⁡
R
2
eqid
⊢
LIdeal
⁡
R
=
LIdeal
⁡
R
3
1
2
islpir
⊢
R
∈
LPIR
↔
R
∈
Ring
∧
LIdeal
⁡
R
=
LPIdeal
⁡
R
4
3
simplbi
⊢
R
∈
LPIR
→
R
∈
Ring