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 )