# 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}={\mathrm{Base}}_{{R}}$
Assertion sdrgid ${⊢}{R}\in \mathrm{DivRing}\to {B}\in \mathrm{SubDRing}\left({R}\right)$

### Proof

Step Hyp Ref Expression
1 sdrgid.1 ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 id ${⊢}{R}\in \mathrm{DivRing}\to {R}\in \mathrm{DivRing}$
3 drngring ${⊢}{R}\in \mathrm{DivRing}\to {R}\in \mathrm{Ring}$
4 1 subrgid ${⊢}{R}\in \mathrm{Ring}\to {B}\in \mathrm{SubRing}\left({R}\right)$
5 3 4 syl ${⊢}{R}\in \mathrm{DivRing}\to {B}\in \mathrm{SubRing}\left({R}\right)$
6 1 ressid ${⊢}{R}\in \mathrm{DivRing}\to {R}{↾}_{𝑠}{B}={R}$
7 6 2 eqeltrd ${⊢}{R}\in \mathrm{DivRing}\to {R}{↾}_{𝑠}{B}\in \mathrm{DivRing}$
8 issdrg ${⊢}{B}\in \mathrm{SubDRing}\left({R}\right)↔\left({R}\in \mathrm{DivRing}\wedge {B}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}{B}\in \mathrm{DivRing}\right)$
9 2 5 7 8 syl3anbrc ${⊢}{R}\in \mathrm{DivRing}\to {B}\in \mathrm{SubDRing}\left({R}\right)$