Metamath Proof Explorer

Theorem extdgcl

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

Ref Expression
Assertion extdgcl ⊢ E /FldExt F → E .:. F ∈ ℕ 0 *

Proof

Step Hyp Ref Expression
1 extdgval ⊢ E /FldExt F → E .:. F = dim ⁡ subringAlg ⁡ E ⁡ Base F
2 fldextfld1 ⊢ E /FldExt F → E ∈ Field
3 isfld ⊢ E ∈ Field ↔ E ∈ DivRing ∧ E ∈ CRing
4 2 3 sylib ⊢ E /FldExt F → E ∈ DivRing ∧ E ∈ CRing
5 4 simpld ⊢ E /FldExt F → E ∈ DivRing
6 fldextress ⊢ E /FldExt F → F = E ↾ 𝑠 Base F
7 fldextfld2 ⊢ E /FldExt F → F ∈ Field
8 isfld ⊢ F ∈ Field ↔ F ∈ DivRing ∧ F ∈ CRing
9 7 8 sylib ⊢ E /FldExt F → F ∈ DivRing ∧ F ∈ CRing
10 9 simpld ⊢ E /FldExt F → F ∈ DivRing
11 6 10 eqeltrrd ⊢ E /FldExt F → E ↾ 𝑠 Base F ∈ DivRing
12 eqid ⊢ Base F = Base F
13 12 fldextsubrg ⊢ E /FldExt F → Base F ∈ SubRing ⁡ E
14 eqid ⊢ subringAlg ⁡ E ⁡ Base F = subringAlg ⁡ E ⁡ Base F
15 eqid ⊢ E ↾ 𝑠 Base F = E ↾ 𝑠 Base F
16 14 15 sralvec ⊢ E ∈ DivRing ∧ E ↾ 𝑠 Base F ∈ DivRing ∧ Base F ∈ SubRing ⁡ E → subringAlg ⁡ E ⁡ Base F ∈ LVec
17 5 11 13 16 syl3anc ⊢ E /FldExt F → subringAlg ⁡ E ⁡ Base F ∈ LVec
18 dimcl ⊢ subringAlg ⁡ E ⁡ Base F ∈ LVec → dim ⁡ subringAlg ⁡ E ⁡ Base F ∈ ℕ 0 *
19 17 18 syl ⊢ E /FldExt F → dim ⁡ subringAlg ⁡ E ⁡ Base F ∈ ℕ 0 *
20 1 19 eqeltrd ⊢ E /FldExt F → E .:. F ∈ ℕ 0 *