# Metamath Proof Explorer

## 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]⟼\mathrm{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 ${setvar}{e}$
2 cvv ${class}\mathrm{V}$
3 vf ${setvar}{f}$
4 cfldext ${class}{/}_{\mathrm{FldExt}}$
5 1 cv ${setvar}{e}$
6 5 csn ${class}\left\{{e}\right\}$
7 4 6 cima ${class}{/}_{\mathrm{FldExt}}\left[\left\{{e}\right\}\right]$
8 cldim ${class}\mathrm{dim}$
9 csra ${class}\mathrm{subringAlg}$
10 5 9 cfv ${class}\mathrm{subringAlg}\left({e}\right)$
11 cbs ${class}\mathrm{Base}$
12 3 cv ${setvar}{f}$
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}\mathrm{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]⟼\mathrm{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]⟼\mathrm{dim}\left(\mathrm{subringAlg}\left({e}\right)\left({\mathrm{Base}}_{{f}}\right)\right)\right)$