Theorem prrngorngo

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

	Ref	Expression
Assertion	prrngorngo	$$⊢R\in \mathrm{PrRing}\to R\in \mathrm{RingOps}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢1^{st}\left(R\right)=1^{st}\left(R\right)$$
2		eqid	$$⊢\mathrm{GId}\left(1^{st}\left(R\right)\right)=\mathrm{GId}\left(1^{st}\left(R\right)\right)$$
3	1 2	isprrngo	$$⊢R\in \mathrm{PrRing}\leftrightarrow \left(R\in \mathrm{RingOps}\wedge \left\{\mathrm{GId}\left(1^{st}\left(R\right)\right)\right\}\in \mathrm{PrIdl}\left(R\right)\right)$$
4	3	simplbi	$$⊢R\in \mathrm{PrRing}\to R\in \mathrm{RingOps}$$