Definition df-extdg 33694

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

Step	Hyp	Ref	Expression
1		cextdg 33692	. 2 class [:]
2		ve	. . 3 setvar 𝑒
3		vf	. . 3 setvar 𝑓
4		cvv 3480	. . 3 class V
5		cfldext 33689	. . . 4 class /FldExt
6	2	cv 1539	. . . . 5 class 𝑒
7	6	csn 4626	. . . 4 class {𝑒}
8	5, 7	cima 5688	. . 3 class (/FldExt “ {𝑒})
9	3	cv 1539	. . . . . 6 class 𝑓
10		cbs 17247	. . . . . 6 class Base
11	9, 10	cfv 6561	. . . . 5 class (Base‘𝑓)
12		csra 21170	. . . . . 6 class subringAlg
13	6, 12	cfv 6561	. . . . 5 class (subringAlg ‘𝑒)
14	11, 13	cfv 6561	. . . 4 class ((subringAlg ‘𝑒)‘(Base‘𝑓))
15		cldim 33649	. . . 4 class dim
16	14, 15	cfv 6561	. . 3 class (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))
17	2, 3, 4, 8, 16	cmpo 7433	. 2 class (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
18	1, 17	wceq 1540	1 wff [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))

This definition is referenced by:  extdgval  33705