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 e. Field /\ A e. ( SubDRing ` F ) ) -> ( F |`s A ) e. Field )

Proof

Step	Hyp	Ref	Expression
1		issdrg	|- ( A e. ( SubDRing ` F ) <-> ( F e. DivRing /\ A e. ( SubRing ` F ) /\ ( F |`s A ) e. DivRing ) )
2	1	simp3bi	|- ( A e. ( SubDRing ` F ) -> ( F |`s A ) e. DivRing )
3	2	adantl	|- ( ( F e. Field /\ A e. ( SubDRing ` F ) ) -> ( F |`s A ) e. DivRing )
4		isfld	|- ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) )
5	4	simprbi	|- ( F e. Field -> F e. CRing )
6	1	simp2bi	|- ( A e. ( SubDRing ` F ) -> A e. ( SubRing ` F ) )
7		eqid	|- ( F |`s A ) = ( F |`s A )
8	7	subrgcrng	|- ( ( F e. CRing /\ A e. ( SubRing ` F ) ) -> ( F |`s A ) e. CRing )
9	5 6 8	syl2an	|- ( ( F e. Field /\ A e. ( SubDRing ` F ) ) -> ( F |`s A ) e. CRing )
10		isfld	|- ( ( F |`s A ) e. Field <-> ( ( F |`s A ) e. DivRing /\ ( F |`s A ) e. CRing ) )
11	3 9 10	sylanbrc	|- ( ( F e. Field /\ A e. ( SubDRing ` F ) ) -> ( F |`s A ) e. Field )