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 |`s A )
	fldsdrgfldext.2	|- ( ph -> F e. Field )
	fldsdrgfldext.3	|- ( ph -> A e. ( SubDRing ` F ) )
	fldsdrgfldext2.b	|- ( ph -> B e. ( SubDRing ` G ) )
	fldsdrgfldext2.h	|- H = ( F |`s B )
Assertion	fldsdrgfldext2	|- ( ph -> G /FldExt H )

Proof

Step	Hyp	Ref	Expression
1		fldsdrgfldext.1	|- G = ( F |`s A )
2		fldsdrgfldext.2	|- ( ph -> F e. Field )
3		fldsdrgfldext.3	|- ( ph -> A e. ( SubDRing ` F ) )
4		fldsdrgfldext2.b	|- ( ph -> B e. ( SubDRing ` G ) )
5		fldsdrgfldext2.h	|- H = ( F |`s B )
6		eqid	|- ( G |`s B ) = ( G |`s B )
7		fldsdrgfld	|- ( ( F e. Field /\ A e. ( SubDRing ` F ) ) -> ( F |`s A ) e. Field )
8	2 3 7	syl2anc	|- ( ph -> ( F |`s A ) e. Field )
9	1 8	eqeltrid	|- ( ph -> G e. Field )
10	6 9 4	fldsdrgfldext	|- ( ph -> G /FldExt ( G |`s B ) )
11		eqid	|- ( Base ` G ) = ( Base ` G )
12	11	sdrgss	|- ( B e. ( SubDRing ` G ) -> B C_ ( Base ` G ) )
13	4 12	syl	|- ( ph -> B C_ ( Base ` G ) )
14		eqid	|- ( Base ` F ) = ( Base ` F )
15	14	sdrgss	|- ( A e. ( SubDRing ` F ) -> A C_ ( Base ` F ) )
16	1 14	ressbas2	|- ( A C_ ( Base ` F ) -> A = ( Base ` G ) )
17	3 15 16	3syl	|- ( ph -> A = ( Base ` G ) )
18	13 17	sseqtrrd	|- ( ph -> B C_ A )
19		ressabs	|- ( ( A e. ( SubDRing ` F ) /\ B C_ A ) -> ( ( F |`s A ) |`s B ) = ( F |`s B ) )
20	3 18 19	syl2anc	|- ( ph -> ( ( F |`s A ) |`s B ) = ( F |`s B ) )
21	1	oveq1i	|- ( G |`s B ) = ( ( F |`s A ) |`s B )
22	20 21 5	3eqtr4g	|- ( ph -> ( G |`s B ) = H )
23	10 22	breqtrd	|- ( ph -> G /FldExt H )