Metamath Proof Explorer


Definition df-extdg

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

Ref Expression
Assertion df-extdg [:] = ( 𝑒 ∈ V , 𝑓 ∈ ( /FldExt “ { 𝑒 } ) ↦ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cextdg [:]
1 ve 𝑒
2 cvv V
3 vf 𝑓
4 cfldext /FldExt
5 1 cv 𝑒
6 5 csn { 𝑒 }
7 4 6 cima ( /FldExt “ { 𝑒 } )
8 cldim dim
9 csra subringAlg
10 5 9 cfv ( subringAlg ‘ 𝑒 )
11 cbs Base
12 3 cv 𝑓
13 12 11 cfv ( Base ‘ 𝑓 )
14 13 10 cfv ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) )
15 14 8 cfv ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) )
16 1 3 2 7 15 cmpo ( 𝑒 ∈ V , 𝑓 ∈ ( /FldExt “ { 𝑒 } ) ↦ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) )
17 0 16 wceq [:] = ( 𝑒 ∈ V , 𝑓 ∈ ( /FldExt “ { 𝑒 } ) ↦ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) )