# Metamath Proof Explorer

## Theorem isprrngo

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

Ref Expression
Hypotheses isprrng.1 ${⊢}{G}={1}^{st}\left({R}\right)$
isprrng.2 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
Assertion isprrngo ${⊢}{R}\in \mathrm{PrRing}↔\left({R}\in \mathrm{RingOps}\wedge \left\{{Z}\right\}\in \mathrm{PrIdl}\left({R}\right)\right)$

### Proof

Step Hyp Ref Expression
1 isprrng.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 isprrng.2 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
3 fveq2 ${⊢}{r}={R}\to {1}^{st}\left({r}\right)={1}^{st}\left({R}\right)$
4 3 1 eqtr4di ${⊢}{r}={R}\to {1}^{st}\left({r}\right)={G}$
5 4 fveq2d ${⊢}{r}={R}\to \mathrm{GId}\left({1}^{st}\left({r}\right)\right)=\mathrm{GId}\left({G}\right)$
6 5 2 eqtr4di ${⊢}{r}={R}\to \mathrm{GId}\left({1}^{st}\left({r}\right)\right)={Z}$
7 6 sneqd ${⊢}{r}={R}\to \left\{\mathrm{GId}\left({1}^{st}\left({r}\right)\right)\right\}=\left\{{Z}\right\}$
8 fveq2 ${⊢}{r}={R}\to \mathrm{PrIdl}\left({r}\right)=\mathrm{PrIdl}\left({R}\right)$
9 7 8 eleq12d ${⊢}{r}={R}\to \left(\left\{\mathrm{GId}\left({1}^{st}\left({r}\right)\right)\right\}\in \mathrm{PrIdl}\left({r}\right)↔\left\{{Z}\right\}\in \mathrm{PrIdl}\left({R}\right)\right)$
10 df-prrngo ${⊢}\mathrm{PrRing}=\left\{{r}\in \mathrm{RingOps}|\left\{\mathrm{GId}\left({1}^{st}\left({r}\right)\right)\right\}\in \mathrm{PrIdl}\left({r}\right)\right\}$
11 9 10 elrab2 ${⊢}{R}\in \mathrm{PrRing}↔\left({R}\in \mathrm{RingOps}\wedge \left\{{Z}\right\}\in \mathrm{PrIdl}\left({R}\right)\right)$