Metamath Proof Explorer

Theorem fldextsdrg

Description: Deduce sub-division-ring from field extension. (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses fldextsdrg.1 ⊢ B = Base F
fldextsdrg.2 ⊢ φ → E /FldExt F
Assertion fldextsdrg ⊢ φ → B ∈ SubDRing ⁡ E

Proof

Step Hyp Ref Expression
1 fldextsdrg.1 ⊢ B = Base F
2 fldextsdrg.2 ⊢ φ → E /FldExt F
3 fldextfld1 ⊢ E /FldExt F → E ∈ Field
4 2 3 syl ⊢ φ → E ∈ Field
5 4 flddrngd ⊢ φ → E ∈ DivRing
6 1 fldextsubrg ⊢ E /FldExt F → B ∈ SubRing ⁡ E
7 2 6 syl ⊢ φ → B ∈ SubRing ⁡ E
8 fldextress ⊢ E /FldExt F → F = E ↾ 𝑠 Base F
9 2 8 syl ⊢ φ → F = E ↾ 𝑠 Base F
10 1 oveq2i ⊢ E ↾ 𝑠 B = E ↾ 𝑠 Base F
11 9 10 eqtr4di ⊢ φ → F = E ↾ 𝑠 B
12 fldextfld2 ⊢ E /FldExt F → F ∈ Field
13 2 12 syl ⊢ φ → F ∈ Field
14 11 13 eqeltrrd ⊢ φ → E ↾ 𝑠 B ∈ Field
15 14 flddrngd ⊢ φ → E ↾ 𝑠 B ∈ DivRing
16 issdrg ⊢ B ∈ SubDRing ⁡ E ↔ E ∈ DivRing ∧ B ∈ SubRing ⁡ E ∧ E ↾ 𝑠 B ∈ DivRing
17 5 7 15 16 syl3anbrc ⊢ φ → B ∈ SubDRing ⁡ E