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

Metamath Proof Explorer

Theorem extdg1b

Description: The degree of the extension E /FldExt F is 1 iff E and F are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023)

Ref Expression
Assertion extdg1b 
|- ( E /FldExt F -> ( ( E [:] F ) = 1 <-> E = F ) )

Proof

Step Hyp Ref Expression
1 extdg1id 
 |-  ( ( E /FldExt F /\ ( E [:] F ) = 1 ) -> E = F )
2 oveq1 
 |-  ( E = F -> ( E [:] F ) = ( F [:] F ) )
3 2 adantl 
 |-  ( ( E /FldExt F /\ E = F ) -> ( E [:] F ) = ( F [:] F ) )
4 fldextfld2 
 |-  ( E /FldExt F -> F e. Field )
5 4 adantr 
 |-  ( ( E /FldExt F /\ E = F ) -> F e. Field )
6 extdgid 
 |-  ( F e. Field -> ( F [:] F ) = 1 )
7 5 6 syl 
 |-  ( ( E /FldExt F /\ E = F ) -> ( F [:] F ) = 1 )
8 3 7 eqtrd 
 |-  ( ( E /FldExt F /\ E = F ) -> ( E [:] F ) = 1 )
9 1 8 impbida 
 |-  ( E /FldExt F -> ( ( E [:] F ) = 1 <-> E = F ) )