Definition df-extdg

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

	Ref	Expression
Assertion	df-extdg	⊢ [:] = ( 𝑒 ∈ V , 𝑓 ∈ ( /FldExt “ { 𝑒 } ) ↦ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cextdg	⊢ [:]
1		ve	⊢ 𝑒
2		cvv	⊢ V
3		vf	⊢ 𝑓
4		cfldext	⊢ /FldExt
5	1	cv	⊢ 𝑒
6	5	csn	⊢ { 𝑒 }
7	4 6	cima	⊢ ( /FldExt “ { 𝑒 } )
8		cldim	⊢ dim
9		csra	⊢ subringAlg
10	5 9	cfv	⊢ ( subringAlg ‘ 𝑒 )
11		cbs	⊢ Base
12	3	cv	⊢ 𝑓
13	12 11	cfv	⊢ ( Base ‘ 𝑓 )
14	13 10	cfv	⊢ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) )
15	14 8	cfv	⊢ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) )
16	1 3 2 7 15	cmpo	⊢ ( 𝑒 ∈ V , 𝑓 ∈ ( /FldExt “ { 𝑒 } ) ↦ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) )
17	0 16	wceq	⊢ [:] = ( 𝑒 ∈ V , 𝑓 ∈ ( /FldExt “ { 𝑒 } ) ↦ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) )