isprrngo

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

	Ref	Expression
Hypotheses	isprrng.1	$⊢ G = 1^{st} (R)$
	isprrng.2	$⊢ Z = GId (G)$
Assertion	isprrngo	$⊢ R \in PrRing \leftrightarrow (R \in RingOps \land \{Z\} \in PrIdl (R))$

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

Metamath Proof Explorer