Theorem crngprmringidom

Description: A commutative ring is a prime ring if and only if it is an integral domain. (Contributed by AV, 27-Jun-2026)

	Ref	Expression
Assertion	crngprmringidom	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ PrmRing ↔ 𝑅 ∈ IDomn ) )

Proof

Step	Hyp	Ref	Expression
1		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
2		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
3		eqid	⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
4	2 3	isprmrng	⊢ ( 𝑅 ∈ PrmRing ↔ ( 𝑅 ∈ Ring ∧ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) )
5	4	a1i	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ PrmRing ↔ ( 𝑅 ∈ Ring ∧ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) ) )
6	1 5	mpbirand	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ PrmRing ↔ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) )
7		ibar	⊢ ( 𝑅 ∈ CRing → ( { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝑅 ∈ CRing ∧ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) ) )
8	2	prmidl0	⊢ ( ( 𝑅 ∈ CRing ∧ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) ↔ 𝑅 ∈ IDomn )
9	8	a1i	⊢ ( 𝑅 ∈ CRing → ( ( 𝑅 ∈ CRing ∧ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) ↔ 𝑅 ∈ IDomn ) )
10	6 7 9	3bitrd	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ∈ PrmRing ↔ 𝑅 ∈ IDomn ) )