This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fldsdrgfldext2

Description: A sub-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
fldsdrgfldext2.b ⊢ φ → B ∈ SubDRing ⁡ G
fldsdrgfldext2.h ⊢ H = F ↾ 𝑠 B
Assertion fldsdrgfldext2 ⊢ φ → G /FldExt H

Proof

Step Hyp Ref Expression
1 fldsdrgfldext.1 ⊢ G = F ↾ 𝑠 A
2 fldsdrgfldext.2 ⊢ φ → F ∈ Field
3 fldsdrgfldext.3 ⊢ φ → A ∈ SubDRing ⁡ F
4 fldsdrgfldext2.b ⊢ φ → B ∈ SubDRing ⁡ G
5 fldsdrgfldext2.h ⊢ H = F ↾ 𝑠 B
6 eqid ⊢ G ↾ 𝑠 B = G ↾ 𝑠 B
7 fldsdrgfld ⊢ F ∈ Field ∧ A ∈ SubDRing ⁡ F → F ↾ 𝑠 A ∈ Field
8 2 3 7 syl2anc ⊢ φ → F ↾ 𝑠 A ∈ Field
9 1 8 eqeltrid ⊢ φ → G ∈ Field
10 6 9 4 fldsdrgfldext ⊢ φ → G /FldExt G ↾ 𝑠 B
11 eqid ⊢ Base G = Base G
12 11 sdrgss ⊢ B ∈ SubDRing ⁡ G → B ⊆ Base G
13 4 12 syl ⊢ φ → B ⊆ Base G
14 eqid ⊢ Base F = Base F
15 14 sdrgss ⊢ A ∈ SubDRing ⁡ F → A ⊆ Base F
16 1 14 ressbas2 ⊢ A ⊆ Base F → A = Base G
17 3 15 16 3syl ⊢ φ → A = Base G
18 13 17 sseqtrrd ⊢ φ → B ⊆ A
19 ressabs ⊢ A ∈ SubDRing ⁡ F ∧ B ⊆ A → F ↾ 𝑠 A ↾ 𝑠 B = F ↾ 𝑠 B
20 3 18 19 syl2anc ⊢ φ → F ↾ 𝑠 A ↾ 𝑠 B = F ↾ 𝑠 B
21 1 oveq1i ⊢ G ↾ 𝑠 B = F ↾ 𝑠 A ↾ 𝑠 B
22 20 21 5 3eqtr4g ⊢ φ → G ↾ 𝑠 B = H
23 10 22 breqtrd ⊢ φ → G /FldExt H