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=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
	drgext.1	$$⊢\phi \to E\in \mathrm{DivRing}$$
	drgext.2	$$⊢\phi \to U\in \mathrm{SubRing}\left(E\right)$$
	drgext.f	$$⊢F=E{\upharpoonright }_{𝑠}U$$
	drgext.3	$$⊢\phi \to F\in \mathrm{DivRing}$$
Assertion	drgextsubrg	$$⊢\phi \to U\in \mathrm{SubRing}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		drgext.b	$$⊢B=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
2		drgext.1	$$⊢\phi \to E\in \mathrm{DivRing}$$
3		drgext.2	$$⊢\phi \to U\in \mathrm{SubRing}\left(E\right)$$
4		drgext.f	$$⊢F=E{\upharpoonright }_{𝑠}U$$
5		drgext.3	$$⊢\phi \to F\in \mathrm{DivRing}$$
6	1	a1i	$$⊢\phi \to B=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
7		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
8	7	subrgss	$$⊢U\in \mathrm{SubRing}\left(E\right)\to U\subseteq {\mathrm{Base}}_E$$
9	3 8	syl	$$⊢\phi \to U\subseteq {\mathrm{Base}}_E$$
10	6 3 9	srasubrg	$$⊢\phi \to U\in \mathrm{SubRing}\left(B\right)$$