Definition df-extdg

Description: Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023)

	Ref	Expression
Assertion	df-extdg	$$⊢\left[.:.\right]=\left(e\in \mathrm{V},f\in {/}_{\mathrm{FldExt}}\left[\left\{e\right\}\right]⟼\dim \left(\mathrm{subringAlg}\left(e\right)\left({\mathrm{Base}}_f\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cextdg	$$class\left[.:.\right]$$
1		ve	$$setvare$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		cfldext	$$class{/}_{\mathrm{FldExt}}$$
5	1	cv	$$setvare$$
6	5	csn	$$class\left\{e\right\}$$
7	4 6	cima	$$class{/}_{\mathrm{FldExt}}\left[\left\{e\right\}\right]$$
8		cldim	$$class\dim$$
9		csra	$$class\mathrm{subringAlg}$$
10	5 9	cfv	$$class\mathrm{subringAlg}\left(e\right)$$
11		cbs	$$class\mathrm{Base}$$
12	3	cv	$$setvarf$$
13	12 11	cfv	$$class{\mathrm{Base}}_f$$
14	13 10	cfv	$$class\mathrm{subringAlg}\left(e\right)\left({\mathrm{Base}}_f\right)$$
15	14 8	cfv	$$class\dim \left(\mathrm{subringAlg}\left(e\right)\left({\mathrm{Base}}_f\right)\right)$$
16	1 3 2 7 15	cmpo	$$class\left(e\in \mathrm{V},f\in {/}_{\mathrm{FldExt}}\left[\left\{e\right\}\right]⟼\dim \left(\mathrm{subringAlg}\left(e\right)\left({\mathrm{Base}}_f\right)\right)\right)$$
17	0 16	wceq	$$wff\left[.:.\right]=\left(e\in \mathrm{V},f\in {/}_{\mathrm{FldExt}}\left[\left\{e\right\}\right]⟼\dim \left(\mathrm{subringAlg}\left(e\right)\left({\mathrm{Base}}_f\right)\right)\right)$$