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

Metamath Proof Explorer

Definition df-irng

Description: Define the subring of elements of a ring r integral over a subset s . (Contributed by Mario Carneiro, 2-Dec-2014) (Revised by Thierry Arnoux, 28-Jan-2025)

Ref Expression
Assertion df-irng 
|- IntgRing = ( r e. _V , s e. _V |-> U_ f e. ( Monic1p ` ( r |`s s ) ) ( `' ( ( r evalSub1 s ) ` f ) " { ( 0g ` r ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cirng 
 |-  IntgRing
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vs 
 |-  s
4 vf 
 |-  f
5 cmn1 
 |-  Monic1p
6 1 cv 
 |-  r
7 cress 
 |-  |`s
8 3 cv 
 |-  s
9 6 8 7 co 
 |-  ( r |`s s )
10 9 5 cfv 
 |-  ( Monic1p ` ( r |`s s ) )
11 ces1 
 |-  evalSub1
12 6 8 11 co 
 |-  ( r evalSub1 s )
13 4 cv 
 |-  f
14 13 12 cfv 
 |-  ( ( r evalSub1 s ) ` f )
15 14 ccnv 
 |-  `' ( ( r evalSub1 s ) ` f )
16 c0g 
 |-  0g
17 6 16 cfv 
 |-  ( 0g ` r )
18 17 csn 
 |-  { ( 0g ` r ) }
19 15 18 cima 
 |-  ( `' ( ( r evalSub1 s ) ` f ) " { ( 0g ` r ) } )
20 4 10 19 ciun 
 |-  U_ f e. ( Monic1p ` ( r |`s s ) ) ( `' ( ( r evalSub1 s ) ` f ) " { ( 0g ` r ) } )
21 1 3 2 2 20 cmpo 
 |-  ( r e. _V , s e. _V |-> U_ f e. ( Monic1p ` ( r |`s s ) ) ( `' ( ( r evalSub1 s ) ` f ) " { ( 0g ` r ) } ) )
22 0 21 wceq 
 |-  IntgRing = ( r e. _V , s e. _V |-> U_ f e. ( Monic1p ` ( r |`s s ) ) ( `' ( ( r evalSub1 s ) ` f ) " { ( 0g ` r ) } ) )