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/FldExtF→0<E.:.F

Proof

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