Metamath Proof Explorer

Theorem irngval

Description: The elements of a field R integral over a subset S . In the case of a subfield, those are the algebraic numbers over the field S within the field R . That is, the numbers X which are roots of monic polynomials P ( X ) with coefficients in S . (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 )
irngval.r 
|- ( ph -> R e. Ring )
irngval.s 
|- ( ph -> S C_ B )
Assertion irngval 
|- ( ph -> ( R IntgRing S ) = U_ f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) )

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 irngval.r 
 |-  ( ph -> R e. Ring )
6 irngval.s 
 |-  ( ph -> S C_ B )
7 5 elexd 
 |-  ( ph -> R e. _V )
8 3 fvexi 
 |-  B e. _V
9 8 a1i 
 |-  ( ph -> B e. _V )
10 9 6 ssexd 
 |-  ( ph -> S e. _V )
11 fvexd 
 |-  ( ph -> ( Monic1p ` U ) e. _V )
12 fvex 
 |-  ( O ` f ) e. _V
13 12 cnvex 
 |-  `' ( O ` f ) e. _V
14 13 imaex 
 |-  ( `' ( O ` f ) " { .0. } ) e. _V
15 14 rgenw 
 |-  A. f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) e. _V
16 iunexg 
 |-  ( ( ( Monic1p ` U ) e. _V /\ A. f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) e. _V ) -> U_ f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) e. _V )
17 11 15 16 sylancl 
 |-  ( ph -> U_ f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) e. _V )
18 oveq12 
 |-  ( ( r = R /\ s = S ) -> ( r |`s s ) = ( R |`s S ) )
19 18 2 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( r |`s s ) = U )
20 19 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( Monic1p ` ( r |`s s ) ) = ( Monic1p ` U ) )
21 oveq12 
 |-  ( ( r = R /\ s = S ) -> ( r evalSub1 s ) = ( R evalSub1 S ) )
22 21 1 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( r evalSub1 s ) = O )
23 22 fveq1d 
 |-  ( ( r = R /\ s = S ) -> ( ( r evalSub1 s ) ` f ) = ( O ` f ) )
24 23 cnveqd 
 |-  ( ( r = R /\ s = S ) -> `' ( ( r evalSub1 s ) ` f ) = `' ( O ` f ) )
25 simpl 
 |-  ( ( r = R /\ s = S ) -> r = R )
26 25 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( 0g ` r ) = ( 0g ` R ) )
27 26 4 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( 0g ` r ) = .0. )
28 27 sneqd 
 |-  ( ( r = R /\ s = S ) -> { ( 0g ` r ) } = { .0. } )
29 24 28 imaeq12d 
 |-  ( ( r = R /\ s = S ) -> ( `' ( ( r evalSub1 s ) ` f ) " { ( 0g ` r ) } ) = ( `' ( O ` f ) " { .0. } ) )
30 20 29 iuneq12d 
 |-  ( ( r = R /\ s = S ) -> U_ f e. ( Monic1p ` ( r |`s s ) ) ( `' ( ( r evalSub1 s ) ` f ) " { ( 0g ` r ) } ) = U_ f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) )
31 df-irng 
 |-  IntgRing = ( r e. _V , s e. _V |-> U_ f e. ( Monic1p ` ( r |`s s ) ) ( `' ( ( r evalSub1 s ) ` f ) " { ( 0g ` r ) } ) )
32 30 31 ovmpoga 
 |-  ( ( R e. _V /\ S e. _V /\ U_ f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) e. _V ) -> ( R IntgRing S ) = U_ f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) )
33 7 10 17 32 syl3anc 
 |-  ( ph -> ( R IntgRing S ) = U_ f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) )