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

Metamath Proof Explorer

Theorem brfldext

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

Ref Expression
Assertion brfldext 
|- ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( e = E /\ f = F ) -> e = E )
2 1 eleq1d 
 |-  ( ( e = E /\ f = F ) -> ( e e. Field <-> E e. Field ) )
3 simpr 
 |-  ( ( e = E /\ f = F ) -> f = F )
4 3 eleq1d 
 |-  ( ( e = E /\ f = F ) -> ( f e. Field <-> F e. Field ) )
5 2 4 anbi12d 
 |-  ( ( e = E /\ f = F ) -> ( ( e e. Field /\ f e. Field ) <-> ( E e. Field /\ F e. Field ) ) )
6 3 fveq2d 
 |-  ( ( e = E /\ f = F ) -> ( Base ` f ) = ( Base ` F ) )
7 1 6 oveq12d 
 |-  ( ( e = E /\ f = F ) -> ( e |`s ( Base ` f ) ) = ( E |`s ( Base ` F ) ) )
8 3 7 eqeq12d 
 |-  ( ( e = E /\ f = F ) -> ( f = ( e |`s ( Base ` f ) ) <-> F = ( E |`s ( Base ` F ) ) ) )
9 1 fveq2d 
 |-  ( ( e = E /\ f = F ) -> ( SubRing ` e ) = ( SubRing ` E ) )
10 6 9 eleq12d 
 |-  ( ( e = E /\ f = F ) -> ( ( Base ` f ) e. ( SubRing ` e ) <-> ( Base ` F ) e. ( SubRing ` E ) ) )
11 8 10 anbi12d 
 |-  ( ( e = E /\ f = F ) -> ( ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )
12 5 11 anbi12d 
 |-  ( ( e = E /\ f = F ) -> ( ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) <-> ( ( E e. Field /\ F e. Field ) /\ ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) ) )
13 df-fldext 
 |-  /FldExt = { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) }
14 12 13 brabga 
 |-  ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( ( E e. Field /\ F e. Field ) /\ ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) ) )
15 14 bianabs 
 |-  ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )