Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-extdg Structured version   Visualization version   GIF version

Definition df-extdg 31096
Description: Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.)
Assertion
Ref Expression
df-extdg [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
Distinct variable group:   𝑒,𝑓

Detailed syntax breakdown of Definition df-extdg
StepHypRef Expression
1 cextdg 31094 . 2 class [:]
2 ve . . 3 setvar 𝑒
3 vf . . 3 setvar 𝑓
4 cvv 3481 . . 3 class V
5 cfldext 31091 . . . 4 class /FldExt
62cv 1537 . . . . 5 class 𝑒
76csn 4551 . . . 4 class {𝑒}
85, 7cima 5546 . . 3 class (/FldExt “ {𝑒})
93cv 1537 . . . . . 6 class 𝑓
10 cbs 16486 . . . . . 6 class Base
119, 10cfv 6344 . . . . 5 class (Base‘𝑓)
12 csra 19943 . . . . . 6 class subringAlg
136, 12cfv 6344 . . . . 5 class (subringAlg ‘𝑒)
1411, 13cfv 6344 . . . 4 class ((subringAlg ‘𝑒)‘(Base‘𝑓))
15 cldim 31062 . . . 4 class dim
1614, 15cfv 6344 . . 3 class (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))
172, 3, 4, 8, 16cmpo 7152 . 2 class (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
181, 17wceq 1538 1 wff [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
Colors of variables: wff setvar class
This definition is referenced by:  extdgval  31107
  Copyright terms: Public domain W3C validator