Theorem fldsdrgfldext

Description: A 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 ) )
Assertion	fldsdrgfldext	|- ( ph -> F /FldExt G )

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		fldsdrgfld	|- ( ( F e. Field /\ A e. ( SubDRing ` F ) ) -> ( F |`s A ) e. Field )
5	2 3 4	syl2anc	|- ( ph -> ( F |`s A ) e. Field )
6	1 5	eqeltrid	|- ( ph -> G e. Field )
7		eqid	|- ( Base ` F ) = ( Base ` F )
8	7	sdrgss	|- ( A e. ( SubDRing ` F ) -> A C_ ( Base ` F ) )
9	1 7	ressbas2	|- ( A C_ ( Base ` F ) -> A = ( Base ` G ) )
10	3 8 9	3syl	|- ( ph -> A = ( Base ` G ) )
11	10	oveq2d	|- ( ph -> ( F |`s A ) = ( F |`s ( Base ` G ) ) )
12	1 11	eqtrid	|- ( ph -> G = ( F |`s ( Base ` G ) ) )
13		sdrgsubrg	|- ( A e. ( SubDRing ` F ) -> A e. ( SubRing ` F ) )
14	3 13	syl	|- ( ph -> A e. ( SubRing ` F ) )
15	10 14	eqeltrrd	|- ( ph -> ( Base ` G ) e. ( SubRing ` F ) )
16		brfldext	|- ( ( F e. Field /\ G e. Field ) -> ( F /FldExt G <-> ( G = ( F |`s ( Base ` G ) ) /\ ( Base ` G ) e. ( SubRing ` F ) ) ) )
17	16	biimpar	|- ( ( ( F e. Field /\ G e. Field ) /\ ( G = ( F |`s ( Base ` G ) ) /\ ( Base ` G ) e. ( SubRing ` F ) ) ) -> F /FldExt G )
18	2 6 12 15 17	syl22anc	|- ( ph -> F /FldExt G )