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 ‘ 𝐹 ) ) ) )