irngssv

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

Step	Hyp	Ref	Expression
1		irngval.o	$⊢ O = R {evalSub}_{1} S$
2		irngval.u	$⊢ U = R ↾_{𝑠} S$
3		irngval.b	$⊢ B = {Base}_{R}$
4		irngval.0	$⊢ \underset{˙}{0} = 0_{R}$
5		elirng.r	$⊢ φ \to R \in CRing$
6		elirng.s	$⊢ φ \to S \in SubRing (R)$
7	1 2 3 4 5 6	elirng	$⊢ φ \to (x \in (R IntgRing S) \leftrightarrow (x \in B \land \exists f \in {Monic}_{1p} (U) O (f) (x) = \underset{˙}{0}))$
8		simpl	$⊢ (x \in B \land \exists f \in {Monic}_{1p} (U) O (f) (x) = \underset{˙}{0}) \to x \in B$
9	7 8	biimtrdi	$⊢ φ \to (x \in (R IntgRing S) \to x \in B)$
10	9	ssrdv	$⊢ φ \to R IntgRing S \subseteq B$

Metamath Proof Explorer