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

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 ( ( 𝐹 ∈ Field ∧ 𝐴 ∈ ( SubDRing ‘ 𝐹 ) ) → ( 𝐹 ↾s 𝐴 ) ∈ Field )

Proof

Step Hyp Ref Expression
1 issdrg ⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝐹 ) ↔ ( 𝐹 ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ 𝐹 ) ∧ ( 𝐹 ↾s 𝐴 ) ∈ DivRing ) )
2 1 simp3bi ⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝐹 ) → ( 𝐹 ↾s 𝐴 ) ∈ DivRing )
3 2 adantl ⊢ ( ( 𝐹 ∈ Field ∧ 𝐴 ∈ ( SubDRing ‘ 𝐹 ) ) → ( 𝐹 ↾s 𝐴 ) ∈ DivRing )
4 isfld ⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
5 4 simprbi ⊢ ( 𝐹 ∈ Field → 𝐹 ∈ CRing )
6 1 simp2bi ⊢ ( 𝐴 ∈ ( SubDRing ‘ 𝐹 ) → 𝐴 ∈ ( SubRing ‘ 𝐹 ) )
7 eqid ⊢ ( 𝐹 ↾s 𝐴 ) = ( 𝐹 ↾s 𝐴 )
8 7 subrgcrng ⊢ ( ( 𝐹 ∈ CRing ∧ 𝐴 ∈ ( SubRing ‘ 𝐹 ) ) → ( 𝐹 ↾s 𝐴 ) ∈ CRing )
9 5 6 8 syl2an ⊢ ( ( 𝐹 ∈ Field ∧ 𝐴 ∈ ( SubDRing ‘ 𝐹 ) ) → ( 𝐹 ↾s 𝐴 ) ∈ CRing )
10 isfld ⊢ ( ( 𝐹 ↾s 𝐴 ) ∈ Field ↔ ( ( 𝐹 ↾s 𝐴 ) ∈ DivRing ∧ ( 𝐹 ↾s 𝐴 ) ∈ CRing ) )
11 3 9 10 sylanbrc ⊢ ( ( 𝐹 ∈ Field ∧ 𝐴 ∈ ( SubDRing ‘ 𝐹 ) ) → ( 𝐹 ↾s 𝐴 ) ∈ Field )