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

Metamath Proof Explorer

Theorem extdgval

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

Ref Expression
Assertion extdgval ⊢ E /FldExt F → E .:. F = dim ⁡ subringAlg ⁡ E ⁡ Base F

Proof

Step Hyp Ref Expression
1 relfldext ⊢ Rel ⁡ /FldExt
2 1 brrelex1i ⊢ E /FldExt F → E ∈ V
3 elrelimasn ⊢ Rel ⁡ /FldExt → F ∈ /FldExt E ↔ E /FldExt F
4 1 3 ax-mp ⊢ F ∈ /FldExt E ↔ E /FldExt F
5 4 biimpri ⊢ E /FldExt F → F ∈ /FldExt E
6 fvexd ⊢ E /FldExt F → dim ⁡ subringAlg ⁡ E ⁡ Base F ∈ V
7 simpl ⊢ e = E ∧ f = F → e = E
8 7 fveq2d ⊢ e = E ∧ f = F → subringAlg ⁡ e = subringAlg ⁡ E
9 simpr ⊢ e = E ∧ f = F → f = F
10 9 fveq2d ⊢ e = E ∧ f = F → Base f = Base F
11 8 10 fveq12d ⊢ e = E ∧ f = F → subringAlg ⁡ e ⁡ Base f = subringAlg ⁡ E ⁡ Base F
12 11 fveq2d ⊢ e = E ∧ f = F → dim ⁡ subringAlg ⁡ e ⁡ Base f = dim ⁡ subringAlg ⁡ E ⁡ Base F
13 sneq ⊢ e = E → e = E
14 13 imaeq2d ⊢ e = E → /FldExt e = /FldExt E
15 df-extdg ⊢ .:. = e ∈ V , f ∈ /FldExt e ⟼ dim ⁡ subringAlg ⁡ e ⁡ Base f
16 12 14 15 ovmpox ⊢ E ∈ V ∧ F ∈ /FldExt E ∧ dim ⁡ subringAlg ⁡ E ⁡ Base F ∈ V → E .:. F = dim ⁡ subringAlg ⁡ E ⁡ Base F
17 2 5 6 16 syl3anc ⊢ E /FldExt F → E .:. F = dim ⁡ subringAlg ⁡ E ⁡ Base F