Definition df-extdg

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

	Ref	Expression
Assertion	df-extdg	|- [:] = ( e e. _V , f e. ( /FldExt " { e } ) |-> ( dim ` ( ( subringAlg ` e ) ` ( Base ` f ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cextdg	|- [:]
1		ve	|- e
2		cvv	|- _V
3		vf	|- f
4		cfldext	|- /FldExt
5	1	cv	|- e
6	5	csn	|- { e }
7	4 6	cima	|- ( /FldExt " { e } )
8		cldim	|- dim
9		csra	|- subringAlg
10	5 9	cfv	|- ( subringAlg ` e )
11		cbs	|- Base
12	3	cv	|- f
13	12 11	cfv	|- ( Base ` f )
14	13 10	cfv	|- ( ( subringAlg ` e ) ` ( Base ` f ) )
15	14 8	cfv	|- ( dim ` ( ( subringAlg ` e ) ` ( Base ` f ) ) )
16	1 3 2 7 15	cmpo	|- ( e e. _V , f e. ( /FldExt " { e } ) |-> ( dim ` ( ( subringAlg ` e ) ` ( Base ` f ) ) ) )
17	0 16	wceq	|- [:] = ( e e. _V , f e. ( /FldExt " { e } ) |-> ( dim ` ( ( subringAlg ` e ) ` ( Base ` f ) ) ) )