This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ .:. = e ∈ V , f ∈ /FldExt e ⟼ dim ⁡ subringAlg ⁡ e ⁡ Base f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cextdg class .:.
1 ve setvar e
2 cvv class V
3 vf setvar f
4 cfldext class /FldExt
5 1 cv setvar e
6 5 csn class e
7 4 6 cima class /FldExt e
8 cldim class dim
9 csra class subringAlg
10 5 9 cfv class subringAlg ⁡ e
11 cbs class Base
12 3 cv setvar f
13 12 11 cfv class Base f
14 13 10 cfv class subringAlg ⁡ e ⁡ Base f
15 14 8 cfv class dim ⁡ subringAlg ⁡ e ⁡ Base f
16 1 3 2 7 15 cmpo class e ∈ V , f ∈ /FldExt e ⟼ dim ⁡ subringAlg ⁡ e ⁡ Base f
17 0 16 wceq wff .:. = e ∈ V , f ∈ /FldExt e ⟼ dim ⁡ subringAlg ⁡ e ⁡ Base f