Definition df-extdg 31055

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 31053	. 2 class [:]
2		ve	. . 3 setvar 𝑒
3		vf	. . 3 setvar 𝑓
4		cvv 3491	. . 3 class V
5		cfldext 31050	. . . 4 class /FldExt
6	2	cv 1535	. . . . 5 class 𝑒
7	6	csn 4560	. . . 4 class {𝑒}
8	5, 7	cima 5551	. . 3 class (/FldExt “ {𝑒})
9	3	cv 1535	. . . . . 6 class 𝑓
10		cbs 16476	. . . . . 6 class Base
11	9, 10	cfv 6348	. . . . 5 class (Base‘𝑓)
12		csra 19933	. . . . . 6 class subringAlg
13	6, 12	cfv 6348	. . . . 5 class (subringAlg ‘𝑒)
14	11, 13	cfv 6348	. . . 4 class ((subringAlg ‘𝑒)‘(Base‘𝑓))
15		cldim 31021	. . . 4 class dim
16	14, 15	cfv 6348	. . 3 class (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))
17	2, 3, 4, 8, 16	cmpo 7151	. 2 class (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))
18	1, 17	wceq 1536	1 wff [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓))))

This definition is referenced by:  extdgval  31066