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 
|- 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 biimtrdi 
 |-  ( ph -> ( x e. ( R IntgRing S ) -> x e. B ) )
10 9 ssrdv 
 |-  ( ph -> ( R IntgRing S ) C_ B )