Metamath Proof Explorer

Theorem fldextid

Description: The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023)

Ref Expression
Assertion fldextid ⊢ F ∈ Field → F /FldExt F

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base F = Base F
2 1 ressid ⊢ F ∈ Field → F ↾ 𝑠 Base F = F
3 2 eqcomd ⊢ F ∈ Field → F = F ↾ 𝑠 Base F
4 isfld ⊢ F ∈ Field ↔ F ∈ DivRing ∧ F ∈ CRing
5 4 simplbi ⊢ F ∈ Field → F ∈ DivRing
6 drngring ⊢ F ∈ DivRing → F ∈ Ring
7 1 subrgid ⊢ F ∈ Ring → Base F ∈ SubRing ⁡ F
8 5 6 7 3syl ⊢ F ∈ Field → Base F ∈ SubRing ⁡ F
9 brfldext ⊢ F ∈ Field ∧ F ∈ Field → F /FldExt F ↔ F = F ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ F
10 9 anidms ⊢ F ∈ Field → F /FldExt F ↔ F = F ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ F
11 3 8 10 mpbir2and ⊢ F ∈ Field → F /FldExt F