Theorem subrfld

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

	Ref	Expression
Hypotheses	subrfld.1	⊢ ( 𝜑 → 𝑅 ∈ Field )
	subrfld.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
Assertion	subrfld	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ IDomn )

Proof

Step	Hyp	Ref	Expression
1		subrfld.1	⊢ ( 𝜑 → 𝑅 ∈ Field )
2		subrfld.2	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
3		fldidom	⊢ ( 𝑅 ∈ Field → 𝑅 ∈ IDomn )
4	1 3	syl	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
5	4 2	subridom	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ IDomn )