Definition df-extdg 31121

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 31119	. 2 class [:]
2		ve	. . 3 setvar 𝑒
3		vf	. . 3 setvar 𝑓
4		cvv 3441	. . 3 class V
5		cfldext 31116	. . . 4 class /FldExt
6	2	cv 1537	. . . . 5 class 𝑒
7	6	csn 4525	. . . 4 class {𝑒}
8	5, 7	cima 5522	. . 3 class (/FldExt “ {𝑒})
9	3	cv 1537	. . . . . 6 class 𝑓
10		cbs 16475	. . . . . 6 class Base
11	9, 10	cfv 6324	. . . . 5 class (Base‘𝑓)
12		csra 19933	. . . . . 6 class subringAlg
13	6, 12	cfv 6324	. . . . 5 class (subringAlg ‘𝑒)
14	11, 13	cfv 6324	. . . 4 class ((subringAlg ‘𝑒)‘(Base‘𝑓))
15		cldim 31087	. . . 4 class dim
16	14, 15	cfv 6324	. . 3 class (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))
17	2, 3, 4, 8, 16	cmpo 7137	. 2 class (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
18	1, 17	wceq 1538	1 wff [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))

This definition is referenced by:  extdgval  31132