Metamath Proof Explorer

Theorem bralgext

Description: Express the fact that a field extension E / F is algebraic. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses bralgext.b 
|- B = ( Base ` E )
bralgext.c 
|- C = ( Base ` F )
bralgext.e 
|- ( ph -> E e. V )
bralgext.f 
|- ( ph -> F e. V )
Assertion bralgext 
|- ( ph -> ( E /AlgExt F <-> ( E /FldExt F /\ ( E IntgRing C ) = B ) ) )

Proof

Step Hyp Ref Expression
1 bralgext.b 
 |-  B = ( Base ` E )
2 bralgext.c 
 |-  C = ( Base ` F )
3 bralgext.e 
 |-  ( ph -> E e. V )
4 bralgext.f 
 |-  ( ph -> F e. V )
5 breq12 
 |-  ( ( e = E /\ f = F ) -> ( e /FldExt f <-> E /FldExt F ) )
6 simpl 
 |-  ( ( e = E /\ f = F ) -> e = E )
7 fveq2 
 |-  ( f = F -> ( Base ` f ) = ( Base ` F ) )
8 7 2 eqtr4di 
 |-  ( f = F -> ( Base ` f ) = C )
9 8 adantl 
 |-  ( ( e = E /\ f = F ) -> ( Base ` f ) = C )
10 6 9 oveq12d 
 |-  ( ( e = E /\ f = F ) -> ( e IntgRing ( Base ` f ) ) = ( E IntgRing C ) )
11 fveq2 
 |-  ( e = E -> ( Base ` e ) = ( Base ` E ) )
12 11 1 eqtr4di 
 |-  ( e = E -> ( Base ` e ) = B )
13 12 adantr 
 |-  ( ( e = E /\ f = F ) -> ( Base ` e ) = B )
14 10 13 eqeq12d 
 |-  ( ( e = E /\ f = F ) -> ( ( e IntgRing ( Base ` f ) ) = ( Base ` e ) <-> ( E IntgRing C ) = B ) )
15 5 14 anbi12d 
 |-  ( ( e = E /\ f = F ) -> ( ( e /FldExt f /\ ( e IntgRing ( Base ` f ) ) = ( Base ` e ) ) <-> ( E /FldExt F /\ ( E IntgRing C ) = B ) ) )
16 df-algext 
 |-  /AlgExt = { <. e , f >. | ( e /FldExt f /\ ( e IntgRing ( Base ` f ) ) = ( Base ` e ) ) }
17 15 16 brabga 
 |-  ( ( E e. V /\ F e. V ) -> ( E /AlgExt F <-> ( E /FldExt F /\ ( E IntgRing C ) = B ) ) )
18 3 4 17 syl2anc 
 |-  ( ph -> ( E /AlgExt F <-> ( E /FldExt F /\ ( E IntgRing C ) = B ) ) )