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 | ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) | |
| Assertion | qsidom | ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑄 ∈ IDomn ↔ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | qsidom.1 | ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) | |
| 2 | 1 | qsidomlem1 | ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑄 ∈ IDomn ) → 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) |
| 3 | 1 | qsidomlem2 | ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑄 ∈ IDomn ) |
| 4 | 3 | adantlr | ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑄 ∈ IDomn ) |
| 5 | 2 4 | impbida | ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑄 ∈ IDomn ↔ 𝐼 ∈ ( PrmIdeal ‘ 𝑅 ) ) ) |