Metamath Proof Explorer


Theorem drgextsubrg

Description: The scalar field is a subring of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023)

Ref Expression
Hypotheses drgext.b B=subringAlgEU
drgext.1 φEDivRing
drgext.2 φUSubRingE
drgext.f F=E𝑠U
drgext.3 φFDivRing
Assertion drgextsubrg φUSubRingB

Proof

Step Hyp Ref Expression
1 drgext.b B=subringAlgEU
2 drgext.1 φEDivRing
3 drgext.2 φUSubRingE
4 drgext.f F=E𝑠U
5 drgext.3 φFDivRing
6 1 a1i φB=subringAlgEU
7 eqid BaseE=BaseE
8 7 subrgss USubRingEUBaseE
9 3 8 syl φUBaseE
10 6 3 9 srasubrg φUSubRingB