Theorem isprmrng

Description: The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 18-Jun-2026)

	Ref	Expression
Hypotheses	isprmrng.z	|- .0. = ( 0g ` R )
	isprmrng.p	|- P = ( PrmIdeal ` R )
Assertion	isprmrng	|- ( R e. PrmRing <-> ( R e. Ring /\ { .0. } e. P ) )

Proof

Step	Hyp	Ref	Expression
1		isprmrng.z	|- .0. = ( 0g ` R )
2		isprmrng.p	|- P = ( PrmIdeal ` R )
3		fveq2	|- ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
4	3	sneqd	|- ( r = R -> { ( 0g ` r ) } = { ( 0g ` R ) } )
5		fveq2	|- ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) )
6	4 5	eleq12d	|- ( r = R -> ( { ( 0g ` r ) } e. ( PrmIdeal ` r ) <-> { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) )
7		df-prmring	|- PrmRing = { r e. Ring | { ( 0g ` r ) } e. ( PrmIdeal ` r ) }
8	6 7	elrab2	|- ( R e. PrmRing <-> ( R e. Ring /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) )
9	1	sneqi	|- { .0. } = { ( 0g ` R ) }
10	9 2	eleq12i	|- ( { .0. } e. P <-> { ( 0g ` R ) } e. ( PrmIdeal ` R ) )
11	10	bicomi	|- ( { ( 0g ` R ) } e. ( PrmIdeal ` R ) <-> { .0. } e. P )
12	11	anbi2i	|- ( ( R e. Ring /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) <-> ( R e. Ring /\ { .0. } e. P ) )
13	8 12	bitri	|- ( R e. PrmRing <-> ( R e. Ring /\ { .0. } e. P ) )