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

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