This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑆 ) ⊆ 𝐵 )