Theorem sdrgfldext

Description: A field E and any sub-division-ring F of E form a field extension. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	sdrgfldext.b	|- B = ( Base ` E )
	sdrgfldext.e	|- ( ph -> E e. Field )
	sdrgfldext.f	|- ( ph -> F e. ( SubDRing ` E ) )
Assertion	sdrgfldext	|- ( ph -> E /FldExt ( E |`s F ) )

Proof

Step	Hyp	Ref	Expression
1		sdrgfldext.b	|- B = ( Base ` E )
2		sdrgfldext.e	|- ( ph -> E e. Field )
3		sdrgfldext.f	|- ( ph -> F e. ( SubDRing ` E ) )
4		fldsdrgfld	|- ( ( E e. Field /\ F e. ( SubDRing ` E ) ) -> ( E |`s F ) e. Field )
5	2 3 4	syl2anc	|- ( ph -> ( E |`s F ) e. Field )
6	1	sdrgss	|- ( F e. ( SubDRing ` E ) -> F C_ B )
7	3 6	syl	|- ( ph -> F C_ B )
8		eqid	|- ( E |`s F ) = ( E |`s F )
9	8 1	ressbas2	|- ( F C_ B -> F = ( Base ` ( E |`s F ) ) )
10	7 9	syl	|- ( ph -> F = ( Base ` ( E |`s F ) ) )
11	10	oveq2d	|- ( ph -> ( E |`s F ) = ( E |`s ( Base ` ( E |`s F ) ) ) )
12		sdrgsubrg	|- ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
13	3 12	syl	|- ( ph -> F e. ( SubRing ` E ) )
14	10 13	eqeltrrd	|- ( ph -> ( Base ` ( E |`s F ) ) e. ( SubRing ` E ) )
15		brfldext	|- ( ( E e. Field /\ ( E |`s F ) e. Field ) -> ( E /FldExt ( E |`s F ) <-> ( ( E |`s F ) = ( E |`s ( Base ` ( E |`s F ) ) ) /\ ( Base ` ( E |`s F ) ) e. ( SubRing ` E ) ) ) )
16	15	biimpar	|- ( ( ( E e. Field /\ ( E |`s F ) e. Field ) /\ ( ( E |`s F ) = ( E |`s ( Base ` ( E |`s F ) ) ) /\ ( Base ` ( E |`s F ) ) e. ( SubRing ` E ) ) ) -> E /FldExt ( E |`s F ) )
17	2 5 11 14 16	syl22anc	|- ( ph -> E /FldExt ( E |`s F ) )