Metamath Proof Explorer

Theorem sdrgfldext

Description: A field E and any sub-division-ring F of E form a field extension. (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses sdrgfldext.b ⊢ B = Base E
sdrgfldext.e ⊢ φ → E ∈ Field
sdrgfldext.f ⊢ φ → F ∈ SubDRing ⁡ E
Assertion sdrgfldext ⊢ φ → E /FldExt E ↾ 𝑠 F

Proof

Step Hyp Ref Expression
1 sdrgfldext.b ⊢ B = Base E
2 sdrgfldext.e ⊢ φ → E ∈ Field
3 sdrgfldext.f ⊢ φ → F ∈ SubDRing ⁡ E
4 fldsdrgfld ⊢ E ∈ Field ∧ F ∈ SubDRing ⁡ E → E ↾ 𝑠 F ∈ Field
5 2 3 4 syl2anc ⊢ φ → E ↾ 𝑠 F ∈ Field
6 1 sdrgss ⊢ F ∈ SubDRing ⁡ E → F ⊆ B
7 3 6 syl ⊢ φ → F ⊆ B
8 eqid ⊢ E ↾ 𝑠 F = E ↾ 𝑠 F
9 8 1 ressbas2 ⊢ F ⊆ B → F = Base E ↾ 𝑠 F
10 7 9 syl ⊢ φ → F = Base E ↾ 𝑠 F
11 10 oveq2d ⊢ φ → E ↾ 𝑠 F = E ↾ 𝑠 Base E ↾ 𝑠 F
12 sdrgsubrg ⊢ F ∈ SubDRing ⁡ E → F ∈ SubRing ⁡ E
13 3 12 syl ⊢ φ → F ∈ SubRing ⁡ E
14 10 13 eqeltrrd ⊢ φ → Base E ↾ 𝑠 F ∈ SubRing ⁡ E
15 brfldext ⊢ E ∈ Field ∧ E ↾ 𝑠 F ∈ Field → E /FldExt E ↾ 𝑠 F ↔ E ↾ 𝑠 F = E ↾ 𝑠 Base E ↾ 𝑠 F ∧ Base E ↾ 𝑠 F ∈ SubRing ⁡ E
16 15 biimpar ⊢ E ∈ Field ∧ E ↾ 𝑠 F ∈ Field ∧ E ↾ 𝑠 F = E ↾ 𝑠 Base E ↾ 𝑠 F ∧ Base E ↾ 𝑠 F ∈ SubRing ⁡ E → E /FldExt E ↾ 𝑠 F
17 2 5 11 14 16 syl22anc ⊢ φ → E /FldExt E ↾ 𝑠 F