Theorem subrfld

Description: A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	subrfld.1	$$⊢\phi \to R\in \mathrm{Field}$$
	subrfld.2	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
Assertion	subrfld	$$⊢\phi \to R{\upharpoonright }_{𝑠}S\in \mathrm{IDomn}$$

Proof

Step	Hyp	Ref	Expression
1		subrfld.1	$$⊢\phi \to R\in \mathrm{Field}$$
2		subrfld.2	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
3		fldidom	$$⊢R\in \mathrm{Field}\to R\in \mathrm{IDomn}$$
4	1 3	syl	$$⊢\phi \to R\in \mathrm{IDomn}$$
5	4 2	subridom	$$⊢\phi \to R{\upharpoonright }_{𝑠}S\in \mathrm{IDomn}$$