Theorem finextfldext

Description: A finite field extension is a field extension. (Contributed by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypothesis	finextfldext.1	|- ( ph -> E /FinExt F )
Assertion	finextfldext	|- ( ph -> E /FldExt F )

Proof

Step	Hyp	Ref	Expression
1		finextfldext.1	|- ( ph -> E /FinExt F )
2		df-finext	|- /FinExt = { <. e , f >. | ( e /FldExt f /\ ( e [:] f ) e. NN0 ) }
3	2	relopabiv	|- Rel /FinExt
4	3	brrelex1i	|- ( E /FinExt F -> E e. _V )
5	1 4	syl	|- ( ph -> E e. _V )
6	3	brrelex2i	|- ( E /FinExt F -> F e. _V )
7	1 6	syl	|- ( ph -> F e. _V )
8		breq12	|- ( ( e = E /\ f = F ) -> ( e /FldExt f <-> E /FldExt F ) )
9		oveq12	|- ( ( e = E /\ f = F ) -> ( e [:] f ) = ( E [:] F ) )
10	9	eleq1d	|- ( ( e = E /\ f = F ) -> ( ( e [:] f ) e. NN0 <-> ( E [:] F ) e. NN0 ) )
11	8 10	anbi12d	|- ( ( e = E /\ f = F ) -> ( ( e /FldExt f /\ ( e [:] f ) e. NN0 ) <-> ( E /FldExt F /\ ( E [:] F ) e. NN0 ) ) )
12	11 2	brabga	|- ( ( E e. _V /\ F e. _V ) -> ( E /FinExt F <-> ( E /FldExt F /\ ( E [:] F ) e. NN0 ) ) )
13	5 7 12	syl2anc	|- ( ph -> ( E /FinExt F <-> ( E /FldExt F /\ ( E [:] F ) e. NN0 ) ) )
14	1 13	mpbid	|- ( ph -> ( E /FldExt F /\ ( E [:] F ) e. NN0 ) )
15	14	simpld	|- ( ph -> E /FldExt F )