Metamath Proof Explorer

Theorem extdgid

Description: A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023)

Ref Expression
Assertion extdgid ⊢ E ∈ Field → E .:. E = 1

Proof

Step Hyp Ref Expression
1 fldextid ⊢ E ∈ Field → E /FldExt E
2 extdgval ⊢ E /FldExt E → E .:. E = dim ⁡ subringAlg ⁡ E ⁡ Base E
3 1 2 syl ⊢ E ∈ Field → E .:. E = dim ⁡ subringAlg ⁡ E ⁡ Base E
4 isfld ⊢ E ∈ Field ↔ E ∈ DivRing ∧ E ∈ CRing
5 4 simplbi ⊢ E ∈ Field → E ∈ DivRing
6 rlmval ⊢ ringLMod ⁡ E = subringAlg ⁡ E ⁡ Base E
7 6 eqcomi ⊢ subringAlg ⁡ E ⁡ Base E = ringLMod ⁡ E
8 7 rlmdim ⊢ E ∈ DivRing → dim ⁡ subringAlg ⁡ E ⁡ Base E = 1
9 5 8 syl ⊢ E ∈ Field → dim ⁡ subringAlg ⁡ E ⁡ Base E = 1
10 3 9 eqtrd ⊢ E ∈ Field → E .:. E = 1