This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )