Theorem fldsdrgfldext2

Description: A sub-sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025)

	Ref	Expression
Hypotheses	fldsdrgfldext.1	$$⊢G=F{\upharpoonright }_{𝑠}A$$
	fldsdrgfldext.2	$$⊢\phi \to F\in \mathrm{Field}$$
	fldsdrgfldext.3	$$⊢\phi \to A\in \mathrm{SubDRing}\left(F\right)$$
	fldsdrgfldext2.b	$$⊢\phi \to B\in \mathrm{SubDRing}\left(G\right)$$
	fldsdrgfldext2.h	$$⊢H=F{\upharpoonright }_{𝑠}B$$
Assertion	fldsdrgfldext2	$$⊢\phi \to G{/}_{\mathrm{FldExt}}H$$

Proof

Step	Hyp	Ref	Expression
1		fldsdrgfldext.1	$$⊢G=F{\upharpoonright }_{𝑠}A$$
2		fldsdrgfldext.2	$$⊢\phi \to F\in \mathrm{Field}$$
3		fldsdrgfldext.3	$$⊢\phi \to A\in \mathrm{SubDRing}\left(F\right)$$
4		fldsdrgfldext2.b	$$⊢\phi \to B\in \mathrm{SubDRing}\left(G\right)$$
5		fldsdrgfldext2.h	$$⊢H=F{\upharpoonright }_{𝑠}B$$
6		eqid	$$⊢G{\upharpoonright }_{𝑠}B=G{\upharpoonright }_{𝑠}B$$
7		fldsdrgfld	$$⊢\left(F\in \mathrm{Field}\wedge A\in \mathrm{SubDRing}\left(F\right)\right)\to F{\upharpoonright }_{𝑠}A\in \mathrm{Field}$$
8	2 3 7	syl2anc	$$⊢\phi \to F{\upharpoonright }_{𝑠}A\in \mathrm{Field}$$
9	1 8	eqeltrid	$$⊢\phi \to G\in \mathrm{Field}$$
10	6 9 4	fldsdrgfldext	$$⊢\phi \to G{/}_{\mathrm{FldExt}}\left(G{\upharpoonright }_{𝑠}B\right)$$
11		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
12	11	sdrgss	$$⊢B\in \mathrm{SubDRing}\left(G\right)\to B\subseteq {\mathrm{Base}}_G$$
13	4 12	syl	$$⊢\phi \to B\subseteq {\mathrm{Base}}_G$$
14		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
15	14	sdrgss	$$⊢A\in \mathrm{SubDRing}\left(F\right)\to A\subseteq {\mathrm{Base}}_F$$
16	1 14	ressbas2	$$⊢A\subseteq {\mathrm{Base}}_F\to A={\mathrm{Base}}_G$$
17	3 15 16	3syl	$$⊢\phi \to A={\mathrm{Base}}_G$$
18	13 17	sseqtrrd	$$⊢\phi \to B\subseteq A$$
19		ressabs	$$⊢\left(A\in \mathrm{SubDRing}\left(F\right)\wedge B\subseteq A\right)\to \left(F{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=F{\upharpoonright }_{𝑠}B$$
20	3 18 19	syl2anc	$$⊢\phi \to \left(F{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=F{\upharpoonright }_{𝑠}B$$
21	1	oveq1i	$$⊢G{\upharpoonright }_{𝑠}B=\left(F{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B$$
22	20 21 5	3eqtr4g	$$⊢\phi \to G{\upharpoonright }_{𝑠}B=H$$
23	10 22	breqtrd	$$⊢\phi \to G{/}_{\mathrm{FldExt}}H$$