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

Metamath Proof Explorer

Theorem fldextid

Description: The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023)

Ref Expression
Assertion fldextid 
|- ( F e. Field -> F /FldExt F )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` F ) = ( Base ` F )
2 1 ressid 
 |-  ( F e. Field -> ( F |`s ( Base ` F ) ) = F )
3 2 eqcomd 
 |-  ( F e. Field -> F = ( F |`s ( Base ` F ) ) )
4 isfld 
 |-  ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
5 4 simplbi 
 |-  ( F e. Field -> F e. DivRing )
6 drngring 
 |-  ( F e. DivRing -> F e. Ring )
7 1 subrgid 
 |-  ( F e. Ring -> ( Base ` F ) e. ( SubRing ` F ) )
8 5 6 7 3syl 
 |-  ( F e. Field -> ( Base ` F ) e. ( SubRing ` F ) )
9 brfldext 
 |-  ( ( F e. Field /\ F e. Field ) -> ( F /FldExt F <-> ( F = ( F |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` F ) ) ) )
10 9 anidms 
 |-  ( F e. Field -> ( F /FldExt F <-> ( F = ( F |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` F ) ) ) )
11 3 8 10 mpbir2and 
 |-  ( F e. Field -> F /FldExt F )