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	|- O = ( R evalSub1 S )
	irngval.u	|- U = ( R |`s S )
	irngval.b	|- B = ( Base ` R )
	irngval.0	|- .0. = ( 0g ` R )
	elirng.r	|- ( ph -> R e. CRing )
	elirng.s	|- ( ph -> S e. ( SubRing ` R ) )
Assertion	irngssv	|- ( ph -> ( R IntgRing S ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		irngval.o	|- O = ( R evalSub1 S )
2		irngval.u	|- U = ( R |`s S )
3		irngval.b	|- B = ( Base ` R )
4		irngval.0	|- .0. = ( 0g ` R )
5		elirng.r	|- ( ph -> R e. CRing )
6		elirng.s	|- ( ph -> S e. ( SubRing ` R ) )
7	1 2 3 4 5 6	elirng	|- ( ph -> ( x e. ( R IntgRing S ) <-> ( x e. B /\ E. f e. ( Monic1p ` U ) ( ( O ` f ) ` x ) = .0. ) ) )
8		simpl	|- ( ( x e. B /\ E. f e. ( Monic1p ` U ) ( ( O ` f ) ` x ) = .0. ) -> x e. B )
9	7 8	syl6bi	|- ( ph -> ( x e. ( R IntgRing S ) -> x e. B ) )
10	9	ssrdv	|- ( ph -> ( R IntgRing S ) C_ B )