Theorem drngdomn

Description: A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015)

	Ref	Expression
Assertion	drngdomn	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Domn )

Proof

Step	Hyp	Ref	Expression
1		drngnzr	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
2		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
4		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
5	2 3 4	isdrng	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) )
6	5	simprbi	⊢ ( 𝑅 ∈ DivRing → ( Unit ‘ 𝑅 ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
7		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
8		eqid	⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
9	8 3	unitrrg	⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) )
10	7 9	syl	⊢ ( 𝑅 ∈ DivRing → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) )
11	6 10	eqsstrrd	⊢ ( 𝑅 ∈ DivRing → ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ⊆ ( RLReg ‘ 𝑅 ) )
12	2 8 4	isdomn2	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ⊆ ( RLReg ‘ 𝑅 ) ) )
13	1 11 12	sylanbrc	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Domn )