Metamath Proof Explorer


Theorem isprrngo

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

Ref Expression
Hypotheses isprrng.1 𝐺 = ( 1st𝑅 )
isprrng.2 𝑍 = ( GId ‘ 𝐺 )
Assertion isprrngo ( 𝑅 ∈ PrRing ↔ ( 𝑅 ∈ RingOps ∧ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 isprrng.1 𝐺 = ( 1st𝑅 )
2 isprrng.2 𝑍 = ( GId ‘ 𝐺 )
3 fveq2 ( 𝑟 = 𝑅 → ( 1st𝑟 ) = ( 1st𝑅 ) )
4 3 1 eqtr4di ( 𝑟 = 𝑅 → ( 1st𝑟 ) = 𝐺 )
5 4 fveq2d ( 𝑟 = 𝑅 → ( GId ‘ ( 1st𝑟 ) ) = ( GId ‘ 𝐺 ) )
6 5 2 eqtr4di ( 𝑟 = 𝑅 → ( GId ‘ ( 1st𝑟 ) ) = 𝑍 )
7 6 sneqd ( 𝑟 = 𝑅 → { ( GId ‘ ( 1st𝑟 ) ) } = { 𝑍 } )
8 fveq2 ( 𝑟 = 𝑅 → ( PrIdl ‘ 𝑟 ) = ( PrIdl ‘ 𝑅 ) )
9 7 8 eleq12d ( 𝑟 = 𝑅 → ( { ( GId ‘ ( 1st𝑟 ) ) } ∈ ( PrIdl ‘ 𝑟 ) ↔ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) )
10 df-prrngo PrRing = { 𝑟 ∈ RingOps ∣ { ( GId ‘ ( 1st𝑟 ) ) } ∈ ( PrIdl ‘ 𝑟 ) }
11 9 10 elrab2 ( 𝑅 ∈ PrRing ↔ ( 𝑅 ∈ RingOps ∧ { 𝑍 } ∈ ( PrIdl ‘ 𝑅 ) ) )