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	$$⊢\underset{\dot{}}{0}=0_R$$
	isprmrng.p	$$⊢P=\mathrm{PrmIdeal}\left(R\right)$$
Assertion	isprmrng	Could not format assertion : No typesetting found for |- ( R e. PrmRing <-> ( R e. Ring /\ { .0. } e. P ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isprmrng.z	$$⊢\underset{\dot{}}{0}=0_R$$
2		isprmrng.p	$$⊢P=\mathrm{PrmIdeal}\left(R\right)$$
3		fveq2	$$⊢r=R\to 0_r=0_R$$
4	3	sneqd	$$⊢r=R\to \left\{0_r\right\}=\left\{0_R\right\}$$
5		fveq2	$$⊢r=R\to \mathrm{PrmIdeal}\left(r\right)=\mathrm{PrmIdeal}\left(R\right)$$
6	4 5	eleq12d	$$⊢r=R\to \left(\left\{0_r\right\}\in \mathrm{PrmIdeal}\left(r\right)\leftrightarrow \left\{0_R\right\}\in \mathrm{PrmIdeal}\left(R\right)\right)$$
7		df-prmring	Could not format PrmRing = { r e. Ring | { ( 0g ` r ) } e. ( PrmIdeal ` r ) } : No typesetting found for |- PrmRing = { r e. Ring | { ( 0g ` r ) } e. ( PrmIdeal ` r ) } with typecode |-
8	6 7	elrab2	Could not format ( R e. PrmRing <-> ( R e. Ring /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( R e. PrmRing <-> ( R e. Ring /\ { ( 0g ` R ) } e. ( PrmIdeal ` R ) ) ) with typecode |-
9	1	sneqi	$$⊢\left\{\underset{\dot{}}{0}\right\}=\left\{0_R\right\}$$
10	9 2	eleq12i	$$⊢\left\{\underset{\dot{}}{0}\right\}\in P\leftrightarrow \left\{0_R\right\}\in \mathrm{PrmIdeal}\left(R\right)$$
11	10	bicomi	$$⊢\left\{0_R\right\}\in \mathrm{PrmIdeal}\left(R\right)\leftrightarrow \left\{\underset{\dot{}}{0}\right\}\in P$$
12	11	anbi2i	$$⊢\left(R\in \mathrm{Ring}\wedge \left\{0_R\right\}\in \mathrm{PrmIdeal}\left(R\right)\right)\leftrightarrow \left(R\in \mathrm{Ring}\wedge \left\{\underset{\dot{}}{0}\right\}\in P\right)$$
13	8 12	bitri	Could not format ( R e. PrmRing <-> ( R e. Ring /\ { .0. } e. P ) ) : No typesetting found for |- ( R e. PrmRing <-> ( R e. Ring /\ { .0. } e. P ) ) with typecode |-