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	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ PrmRing )

Proof

Step	Hyp	Ref	Expression
1		drngnzr	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
2		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
4		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
5	2 3 4	drngnidl	⊢ ( 𝑅 ∈ DivRing → ( LIdeal ‘ 𝑅 ) = { { ( 0g ‘ 𝑅 ) } , ( Base ‘ 𝑅 ) } )
6	2 3 4	smprngprmrng	⊢ ( ( 𝑅 ∈ NzRing ∧ ( LIdeal ‘ 𝑅 ) = { { ( 0g ‘ 𝑅 ) } , ( Base ‘ 𝑅 ) } ) → 𝑅 ∈ PrmRing )
7	1 5 6	syl2anc	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ PrmRing )