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 ‘ 𝑅 )
	isprmrng.p	⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
Assertion	isprmrng	⊢ ( 𝑅 ∈ PrmRing ↔ ( 𝑅 ∈ Ring ∧ { 0 } ∈ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		isprmrng.z	⊢ 0 = ( 0g ‘ 𝑅 )
2		isprmrng.p	⊢ 𝑃 = ( PrmIdeal ‘ 𝑅 )
3		fveq2	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
4	3	sneqd	⊢ ( 𝑟 = 𝑅 → { ( 0g ‘ 𝑟 ) } = { ( 0g ‘ 𝑅 ) } )
5		fveq2	⊢ ( 𝑟 = 𝑅 → ( PrmIdeal ‘ 𝑟 ) = ( PrmIdeal ‘ 𝑅 ) )
6	4 5	eleq12d	⊢ ( 𝑟 = 𝑅 → ( { ( 0g ‘ 𝑟 ) } ∈ ( PrmIdeal ‘ 𝑟 ) ↔ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) )
7		df-prmring	⊢ PrmRing = { 𝑟 ∈ Ring ∣ { ( 0g ‘ 𝑟 ) } ∈ ( PrmIdeal ‘ 𝑟 ) }
8	6 7	elrab2	⊢ ( 𝑅 ∈ PrmRing ↔ ( 𝑅 ∈ Ring ∧ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) )
9	1	sneqi	⊢ { 0 } = { ( 0g ‘ 𝑅 ) }
10	9 2	eleq12i	⊢ ( { 0 } ∈ 𝑃 ↔ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) )
11	10	bicomi	⊢ ( { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ↔ { 0 } ∈ 𝑃 )
12	11	anbi2i	⊢ ( ( 𝑅 ∈ Ring ∧ { ( 0g ‘ 𝑅 ) } ∈ ( PrmIdeal ‘ 𝑅 ) ) ↔ ( 𝑅 ∈ Ring ∧ { 0 } ∈ 𝑃 ) )
13	8 12	bitri	⊢ ( 𝑅 ∈ PrmRing ↔ ( 𝑅 ∈ Ring ∧ { 0 } ∈ 𝑃 ) )