Metamath Proof Explorer

Theorem qsidom

Description: An ideal I in the commutative ring R is prime if and only if the factor ring Q is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024)

Ref Expression
Hypothesis qsidom.1 ⊢ Q = R / 𝑠 R ~ QG I
Assertion qsidom ⊢ R ∈ CRing ∧ I ∈ LIdeal ⁡ R → Q ∈ IDomn ↔ I ∈ PrmIdeal ⁡ R

Proof

Step Hyp Ref Expression
1 qsidom.1 ⊢ Q = R / 𝑠 R ~ QG I
2 1 qsidomlem1 ⊢ R ∈ CRing ∧ I ∈ LIdeal ⁡ R ∧ Q ∈ IDomn → I ∈ PrmIdeal ⁡ R
3 1 qsidomlem2 ⊢ R ∈ CRing ∧ I ∈ PrmIdeal ⁡ R → Q ∈ IDomn
4 3 adantlr ⊢ R ∈ CRing ∧ I ∈ LIdeal ⁡ R ∧ I ∈ PrmIdeal ⁡ R → Q ∈ IDomn
5 2 4 impbida ⊢ R ∈ CRing ∧ I ∈ LIdeal ⁡ R → Q ∈ IDomn ↔ I ∈ PrmIdeal ⁡ R