Definition df-extdg 31620

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 31618	. 2 class [:]
2		ve	. . 3 setvar 𝑒
3		vf	. . 3 setvar 𝑓
4		cvv 3422	. . 3 class V
5		cfldext 31615	. . . 4 class /FldExt
6	2	cv 1538	. . . . 5 class 𝑒
7	6	csn 4558	. . . 4 class {𝑒}
8	5, 7	cima 5583	. . 3 class (/FldExt “ {𝑒})
9	3	cv 1538	. . . . . 6 class 𝑓
10		cbs 16840	. . . . . 6 class Base
11	9, 10	cfv 6418	. . . . 5 class (Base‘𝑓)
12		csra 20345	. . . . . 6 class subringAlg
13	6, 12	cfv 6418	. . . . 5 class (subringAlg ‘𝑒)
14	11, 13	cfv 6418	. . . 4 class ((subringAlg ‘𝑒)‘(Base‘𝑓))
15		cldim 31586	. . . 4 class dim
16	14, 15	cfv 6418	. . 3 class (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))
17	2, 3, 4, 8, 16	cmpo 7257	. 2 class (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
18	1, 17	wceq 1539	1 wff [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))

This definition is referenced by:  extdgval  31631