Theorem drngprmrng

Description: A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 18-Jun-2026)

	Ref	Expression
Assertion	drngprmrng	Could not format assertion : No typesetting found for |- ( R e. DivRing -> R e. PrmRing ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		drngnzr	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{NzRing}$$
2		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
3		eqid	$$⊢0_R=0_R$$
4		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
5	2 3 4	drngnidl	$$⊢R\in \mathrm{DivRing}\to \mathrm{LIdeal}\left(R\right)=\left\{\left\{0_R\right\},{\mathrm{Base}}_R\right\}$$
6	2 3 4	smprngprmrng	Could not format ( ( R e. NzRing /\ ( LIdeal ` R ) = { { ( 0g ` R ) } , ( Base ` R ) } ) -> R e. PrmRing ) : No typesetting found for |- ( ( R e. NzRing /\ ( LIdeal ` R ) = { { ( 0g ` R ) } , ( Base ` R ) } ) -> R e. PrmRing ) with typecode |-
7	1 5 6	syl2anc	Could not format ( R e. DivRing -> R e. PrmRing ) : No typesetting found for |- ( R e. DivRing -> R e. PrmRing ) with typecode |-