Metamath Proof Explorer

Theorem drngdomn

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

Ref Expression
Assertion drngdomn ⊢ R ∈ DivRing → R ∈ Domn

Proof

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