This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑅 ) ) )