Metamath Proof Explorer

Theorem extdggt0

Description: Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023)

Ref Expression
Assertion extdggt0 ⊢ E /FldExt F → 0 < E .:. F

Proof

Step Hyp Ref Expression
1 fldextfld1 ⊢ E /FldExt F → E ∈ Field
2 isfld ⊢ E ∈ Field ↔ E ∈ DivRing ∧ E ∈ CRing
3 2 simplbi ⊢ E ∈ Field → E ∈ DivRing
4 1 3 syl ⊢ E /FldExt F → E ∈ DivRing
5 fldextress ⊢ E /FldExt F → F = E ↾ 𝑠 Base F
6 fldextfld2 ⊢ E /FldExt F → F ∈ Field
7 isfld ⊢ F ∈ Field ↔ F ∈ DivRing ∧ F ∈ CRing
8 7 simplbi ⊢ F ∈ Field → F ∈ DivRing
9 6 8 syl ⊢ E /FldExt F → F ∈ DivRing
10 5 9 eqeltrrd ⊢ E /FldExt F → E ↾ 𝑠 Base F ∈ DivRing
11 eqid ⊢ Base F = Base F
12 11 fldextsubrg ⊢ E /FldExt F → Base F ∈ SubRing ⁡ E
13 eqid ⊢ subringAlg ⁡ E ⁡ Base F = subringAlg ⁡ E ⁡ Base F
14 eqid ⊢ E ↾ 𝑠 Base F = E ↾ 𝑠 Base F
15 13 14 sralvec ⊢ E ∈ DivRing ∧ E ↾ 𝑠 Base F ∈ DivRing ∧ Base F ∈ SubRing ⁡ E → subringAlg ⁡ E ⁡ Base F ∈ LVec
16 4 10 12 15 syl3anc ⊢ E /FldExt F → subringAlg ⁡ E ⁡ Base F ∈ LVec
17 eqid ⊢ Base E = Base E
18 17 subrgss ⊢ Base F ∈ SubRing ⁡ E → Base F ⊆ Base E
19 12 18 syl ⊢ E /FldExt F → Base F ⊆ Base E
20 13 17 sradrng ⊢ E ∈ DivRing ∧ Base F ⊆ Base E → subringAlg ⁡ E ⁡ Base F ∈ DivRing
21 4 19 20 syl2anc ⊢ E /FldExt F → subringAlg ⁡ E ⁡ Base F ∈ DivRing
22 drngdimgt0 ⊢ subringAlg ⁡ E ⁡ Base F ∈ LVec ∧ subringAlg ⁡ E ⁡ Base F ∈ DivRing → 0 < dim ⁡ subringAlg ⁡ E ⁡ Base F
23 16 21 22 syl2anc ⊢ E /FldExt F → 0 < dim ⁡ subringAlg ⁡ E ⁡ Base F
24 extdgval ⊢ E /FldExt F → E .:. F = dim ⁡ subringAlg ⁡ E ⁡ Base F
25 23 24 breqtrrd ⊢ E /FldExt F → 0 < E .:. F