Metamath Proof Explorer

Theorem divrngpr

Description: Obsolete theorem, use drngprmrng instead. A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	divrngpr	$⊢ R \in DivRingOps \to R \in PrRing$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
2		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
3		eqid	$⊢ GId (1^{st} (R)) = GId (1^{st} (R))$
4		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
5	1 2 3 4	isdrngo1	$⊢ R \in DivRingOps \leftrightarrow (R \in RingOps \land {2^{nd} (R) ↾}_{((ran 1^{st} (R) ∖ \{GId (1^{st} (R))\}) \times (ran 1^{st} (R) ∖ \{GId (1^{st} (R))\}))} \in GrpOp)$
6	5	simplbi	$⊢ R \in DivRingOps \to R \in RingOps$
7		eqid	$⊢ GId (2^{nd} (R)) = GId (2^{nd} (R))$
8	1 2 4 3 7	dvrunz	$⊢ R \in DivRingOps \to GId (2^{nd} (R)) \neq GId (1^{st} (R))$
9	1 2 4 3	divrngidl	$⊢ R \in DivRingOps \to Idl (R) = \{\{GId (1^{st} (R))\}, ran 1^{st} (R)\}$
10	1 2 4 3 7	smprngopr	$⊢ (R \in RingOps \land GId (2^{nd} (R)) \neq GId (1^{st} (R)) \land Idl (R) = \{\{GId (1^{st} (R))\}, ran 1^{st} (R)\}) \to R \in PrRing$
11	6 8 9 10	syl3anc	$⊢ R \in DivRingOps \to R \in PrRing$