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

Metamath Proof Explorer

Theorem fldextress

Description: Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion fldextress 
|- ( E /FldExt F -> F = ( E |`s ( Base ` F ) ) )

Proof

Step Hyp Ref Expression
1 fldextfld1 
 |-  ( E /FldExt F -> E e. Field )
2 fldextfld2 
 |-  ( E /FldExt F -> F e. Field )
3 brfldext 
 |-  ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )
4 1 2 3 syl2anc 
 |-  ( E /FldExt F -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )
5 4 ibi 
 |-  ( E /FldExt F -> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) )
6 5 simpld 
 |-  ( E /FldExt F -> F = ( E |`s ( Base ` F ) ) )