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 ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 relfldext ⊢ Rel /FldExt
2 1 brrelex1i ⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ V )
3 elrelimasn ⊢ ( Rel /FldExt → ( 𝐹 ∈ ( /FldExt “ { 𝐸 } ) ↔ 𝐸 /FldExt 𝐹 ) )
4 1 3 ax-mp ⊢ ( 𝐹 ∈ ( /FldExt “ { 𝐸 } ) ↔ 𝐸 /FldExt 𝐹 )
5 4 biimpri ⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ ( /FldExt “ { 𝐸 } ) )
6 fvexd ⊢ ( 𝐸 /FldExt 𝐹 → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ V )
7 simpl ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → 𝑒 = 𝐸 )
8 7 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( subringAlg ‘ 𝑒 ) = ( subringAlg ‘ 𝐸 ) )
9 simpr ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
10 9 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
11 8 10 fveq12d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) )
12 11 fveq2d ⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
13 sneq ⊢ ( 𝑒 = 𝐸 → { 𝑒 } = { 𝐸 } )
14 13 imaeq2d ⊢ ( 𝑒 = 𝐸 → ( /FldExt “ { 𝑒 } ) = ( /FldExt “ { 𝐸 } ) )
15 df-extdg ⊢ [:] = ( 𝑒 ∈ V , 𝑓 ∈ ( /FldExt “ { 𝑒 } ) ↦ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) )
16 12 14 15 ovmpox ⊢ ( ( 𝐸 ∈ V ∧ 𝐹 ∈ ( /FldExt “ { 𝐸 } ) ∧ ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ V ) → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
17 2 5 6 16 syl3anc ⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )