This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )