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

Metamath Proof Explorer

Theorem extdgval

Description: Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion extdgval 
|- ( E /FldExt F -> ( E [:] F ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 relfldext 
 |-  Rel /FldExt
2 1 brrelex1i 
 |-  ( E /FldExt F -> E e. _V )
3 elrelimasn 
 |-  ( Rel /FldExt -> ( F e. ( /FldExt " { E } ) <-> E /FldExt F ) )
4 1 3 ax-mp 
 |-  ( F e. ( /FldExt " { E } ) <-> E /FldExt F )
5 4 biimpri 
 |-  ( E /FldExt F -> F e. ( /FldExt " { E } ) )
6 fvexd 
 |-  ( E /FldExt F -> ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) e. _V )
7 simpl 
 |-  ( ( e = E /\ f = F ) -> e = E )
8 7 fveq2d 
 |-  ( ( e = E /\ f = F ) -> ( subringAlg ` e ) = ( subringAlg ` E ) )
9 simpr 
 |-  ( ( e = E /\ f = F ) -> f = F )
10 9 fveq2d 
 |-  ( ( e = E /\ f = F ) -> ( Base ` f ) = ( Base ` F ) )
11 8 10 fveq12d 
 |-  ( ( e = E /\ f = F ) -> ( ( subringAlg ` e ) ` ( Base ` f ) ) = ( ( subringAlg ` E ) ` ( Base ` F ) ) )
12 11 fveq2d 
 |-  ( ( e = E /\ f = F ) -> ( dim ` ( ( subringAlg ` e ) ` ( Base ` f ) ) ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )
13 sneq 
 |-  ( e = E -> { e } = { E } )
14 13 imaeq2d 
 |-  ( e = E -> ( /FldExt " { e } ) = ( /FldExt " { E } ) )
15 df-extdg 
 |-  [:] = ( e e. _V , f e. ( /FldExt " { e } ) |-> ( dim ` ( ( subringAlg ` e ) ` ( Base ` f ) ) ) )
16 12 14 15 ovmpox 
 |-  ( ( E e. _V /\ F e. ( /FldExt " { E } ) /\ ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) e. _V ) -> ( E [:] F ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )
17 2 5 6 16 syl3anc 
 |-  ( E /FldExt F -> ( E [:] F ) = ( dim ` ( ( subringAlg ` E ) ` ( Base ` F ) ) ) )