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=BaseR
Assertion sdrgid RDivRingBSubDRingR

Proof

Step Hyp Ref Expression
1 sdrgid.1 B=BaseR
2 id RDivRingRDivRing
3 drngring RDivRingRRing
4 1 subrgid RRingBSubRingR
5 3 4 syl RDivRingBSubRingR
6 1 ressid RDivRingR𝑠B=R
7 6 2 eqeltrd RDivRingR𝑠BDivRing
8 issdrg BSubDRingRRDivRingBSubRingRR𝑠BDivRing
9 2 5 7 8 syl3anbrc RDivRingBSubDRingR