Metamath Proof Explorer

Theorem brfinext

Description: The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion brfinext 
|- ( E /FldExt F -> ( E /FinExt F <-> ( E [:] F ) e. NN0 ) )

Proof

Step Hyp Ref Expression
1 fldextfld1 
 |-  ( E /FldExt F -> E e. Field )
2 fldextfld2 
 |-  ( E /FldExt F -> F e. Field )
3 breq12 
 |-  ( ( e = E /\ f = F ) -> ( e /FldExt f <-> E /FldExt F ) )
4 oveq12 
 |-  ( ( e = E /\ f = F ) -> ( e [:] f ) = ( E [:] F ) )
5 4 eleq1d 
 |-  ( ( e = E /\ f = F ) -> ( ( e [:] f ) e. NN0 <-> ( E [:] F ) e. NN0 ) )
6 3 5 anbi12d 
 |-  ( ( e = E /\ f = F ) -> ( ( e /FldExt f /\ ( e [:] f ) e. NN0 ) <-> ( E /FldExt F /\ ( E [:] F ) e. NN0 ) ) )
7 df-finext 
 |-  /FinExt = { <. e , f >. | ( e /FldExt f /\ ( e [:] f ) e. NN0 ) }
8 6 7 brabga 
 |-  ( ( E e. Field /\ F e. Field ) -> ( E /FinExt F <-> ( E /FldExt F /\ ( E [:] F ) e. NN0 ) ) )
9 1 2 8 syl2anc 
 |-  ( E /FldExt F -> ( E /FinExt F <-> ( E /FldExt F /\ ( E [:] F ) e. NN0 ) ) )
10 9 bianabs 
 |-  ( E /FldExt F -> ( E /FinExt F <-> ( E [:] F ) e. NN0 ) )