Metamath Proof Explorer

Theorem fldsdrgfldext

Description: A sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025)

Ref Expression
Hypotheses fldsdrgfldext.1 ⊢ G = F ↾ 𝑠 A
fldsdrgfldext.2 ⊢ φ → F ∈ Field
fldsdrgfldext.3 ⊢ φ → A ∈ SubDRing ⁡ F
Assertion fldsdrgfldext ⊢ φ → F /FldExt G

Proof

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