Theorem irngssv

Description: An integral element is an element of the base set. (Contributed by Thierry Arnoux, 28-Jan-2025)

	Ref	Expression
Hypotheses	irngval.o	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
	irngval.u	⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
	irngval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	irngval.0	⊢ 0 = ( 0g ‘ 𝑅 )
	elirng.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	elirng.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
Assertion	irngssv	⊢ ( 𝜑 → ( 𝑅 IntgRing 𝑆 ) ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		irngval.o	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2		irngval.u	⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
3		irngval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		irngval.0	⊢ 0 = ( 0g ‘ 𝑅 )
5		elirng.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		elirng.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7	1 2 3 4 5 6	elirng	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑅 IntgRing 𝑆 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑥 ) = 0 ) ) )
8		simpl	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑥 ) = 0 ) → 𝑥 ∈ 𝐵 )
9	7 8	biimtrdi	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑅 IntgRing 𝑆 ) → 𝑥 ∈ 𝐵 ) )
10	9	ssrdv	⊢ ( 𝜑 → ( 𝑅 IntgRing 𝑆 ) ⊆ 𝐵 )