Metamath Proof Explorer

Theorem sdrgid

Description: Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023)

Ref Expression
Hypothesis sdrgid.1 ⊢ B = Base R
Assertion sdrgid ⊢ R ∈ DivRing → B ∈ SubDRing ⁡ R

Proof

Step Hyp Ref Expression
1 sdrgid.1 ⊢ B = Base R
2 id ⊢ R ∈ DivRing → R ∈ DivRing
3 drngring ⊢ R ∈ DivRing → R ∈ Ring
4 1 subrgid ⊢ R ∈ Ring → B ∈ SubRing ⁡ R
5 3 4 syl ⊢ R ∈ DivRing → B ∈ SubRing ⁡ R
6 1 ressid ⊢ R ∈ DivRing → R ↾ 𝑠 B = R
7 6 2 eqeltrd ⊢ R ∈ DivRing → R ↾ 𝑠 B ∈ DivRing
8 issdrg ⊢ B ∈ SubDRing ⁡ R ↔ R ∈ DivRing ∧ B ∈ SubRing ⁡ R ∧ R ↾ 𝑠 B ∈ DivRing
9 2 5 7 8 syl3anbrc ⊢ R ∈ DivRing → B ∈ SubDRing ⁡ R