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	\|- ( ( 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 )