Metamath Proof Explorer

Theorem fldsdrgfld

Description: A sub-division-ring of a field is itself a field, so it is a subfield. We can therefore use SubDRing to express subfields. (Contributed by Thierry Arnoux, 11-Jan-2025)

Ref Expression
Assertion fldsdrgfld ⊢ F ∈ Field ∧ A ∈ SubDRing ⁡ F → F ↾ 𝑠 A ∈ Field

Proof

Step Hyp Ref Expression
1 issdrg ⊢ A ∈ SubDRing ⁡ F ↔ F ∈ DivRing ∧ A ∈ SubRing ⁡ F ∧ F ↾ 𝑠 A ∈ DivRing
2 1 simp3bi ⊢ A ∈ SubDRing ⁡ F → F ↾ 𝑠 A ∈ DivRing
3 2 adantl ⊢ F ∈ Field ∧ A ∈ SubDRing ⁡ F → F ↾ 𝑠 A ∈ DivRing
4 isfld ⊢ F ∈ Field ↔ F ∈ DivRing ∧ F ∈ CRing
5 4 simprbi ⊢ F ∈ Field → F ∈ CRing
6 1 simp2bi ⊢ A ∈ SubDRing ⁡ F → A ∈ SubRing ⁡ F
7 eqid ⊢ F ↾ 𝑠 A = F ↾ 𝑠 A
8 7 subrgcrng ⊢ F ∈ CRing ∧ A ∈ SubRing ⁡ F → F ↾ 𝑠 A ∈ CRing
9 5 6 8 syl2an ⊢ F ∈ Field ∧ A ∈ SubDRing ⁡ F → F ↾ 𝑠 A ∈ CRing
10 isfld ⊢ F ↾ 𝑠 A ∈ Field ↔ F ↾ 𝑠 A ∈ DivRing ∧ F ↾ 𝑠 A ∈ CRing
11 3 9 10 sylanbrc ⊢ F ∈ Field ∧ A ∈ SubDRing ⁡ F → F ↾ 𝑠 A ∈ Field