Metamath Proof Explorer

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 
|- ( R e. CRing -> ( R e. PrmRing <-> R e. IDomn ) )

Proof

Step Hyp Ref Expression
1 crngring 
 |-  ( R e. CRing -> R e. Ring )
2 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
3 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
4 2 3 isprmrng 
 |-  ( R e. PrmRing <-> ( R e. Ring /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) )
5 4 a1i 
 |-  ( R e. CRing -> ( R e. PrmRing <-> ( R e. Ring /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) ) )
6 1 5 mpbirand 
 |-  ( R e. CRing -> ( R e. PrmRing <-> { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) )
7 ibar 
 |-  ( R e. CRing -> ( { ( 0g ` R ) } e. ( PrmIdeal ` R ) <-> ( R e. CRing /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) ) )
8 2 prmidl0 
 |-  ( ( R e. CRing /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) <-> R e. IDomn )
9 8 a1i 
 |-  ( R e. CRing -> ( ( R e. CRing /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) <-> R e. IDomn ) )
10 6 7 9 3bitrd 
 |-  ( R e. CRing -> ( R e. PrmRing <-> R e. IDomn ) )