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}\leftrightarrow \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)\leftrightarrow \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}\leftrightarrow \left(R\in \mathrm{RingOps}\wedge \left\{Z\right\}\in \mathrm{PrIdl}\left(R\right)\right)$$