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

Metamath Proof Explorer

Theorem elirng

Description: Property for an element X of a field R to be integral over a subring 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 )
elirng.r 
|- ( ph -> R e. CRing )
elirng.s 
|- ( ph -> S e. ( SubRing ` R ) )
Assertion elirng 
|- ( ph -> ( X e. ( R IntgRing S ) <-> ( X e. B /\ E. f e. ( Monic1p ` U ) ( ( O ` f ) ` X ) = .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 elirng.r 
 |-  ( ph -> R e. CRing )
6 elirng.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
7 5 crngringd 
 |-  ( ph -> R e. Ring )
8 3 subrgss 
 |-  ( S e. ( SubRing ` R ) -> S C_ B )
9 6 8 syl 
 |-  ( ph -> S C_ B )
10 1 2 3 4 7 9 irngval 
 |-  ( ph -> ( R IntgRing S ) = U_ f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) )
11 10 eleq2d 
 |-  ( ph -> ( X e. ( R IntgRing S ) <-> X e. U_ f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) ) )
12 eliun 
 |-  ( X e. U_ f e. ( Monic1p ` U ) ( `' ( O ` f ) " { .0. } ) <-> E. f e. ( Monic1p ` U ) X e. ( `' ( O ` f ) " { .0. } ) )
13 11 12 bitrdi 
 |-  ( ph -> ( X e. ( R IntgRing S ) <-> E. f e. ( Monic1p ` U ) X e. ( `' ( O ` f ) " { .0. } ) ) )
14 eqid 
 |-  ( R ^s B ) = ( R ^s B )
15 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
16 7 adantr 
 |-  ( ( ph /\ f e. ( Monic1p ` U ) ) -> R e. Ring )
17 3 fvexi 
 |-  B e. _V
18 17 a1i 
 |-  ( ( ph /\ f e. ( Monic1p ` U ) ) -> B e. _V )
19 eqid 
 |-  ( Poly1 ` U ) = ( Poly1 ` U )
20 1 3 14 2 19 evls1rhm 
 |-  ( ( R e. CRing /\ S e. ( SubRing ` R ) ) -> O e. ( ( Poly1 ` U ) RingHom ( R ^s B ) ) )
21 5 6 20 syl2anc 
 |-  ( ph -> O e. ( ( Poly1 ` U ) RingHom ( R ^s B ) ) )
22 eqid 
 |-  ( Base ` ( Poly1 ` U ) ) = ( Base ` ( Poly1 ` U ) )
23 22 15 rhmf 
 |-  ( O e. ( ( Poly1 ` U ) RingHom ( R ^s B ) ) -> O : ( Base ` ( Poly1 ` U ) ) --> ( Base ` ( R ^s B ) ) )
24 21 23 syl 
 |-  ( ph -> O : ( Base ` ( Poly1 ` U ) ) --> ( Base ` ( R ^s B ) ) )
25 24 adantr 
 |-  ( ( ph /\ f e. ( Monic1p ` U ) ) -> O : ( Base ` ( Poly1 ` U ) ) --> ( Base ` ( R ^s B ) ) )
26 eqid 
 |-  ( Monic1p ` U ) = ( Monic1p ` U )
27 19 22 26 mon1pcl 
 |-  ( f e. ( Monic1p ` U ) -> f e. ( Base ` ( Poly1 ` U ) ) )
28 27 adantl 
 |-  ( ( ph /\ f e. ( Monic1p ` U ) ) -> f e. ( Base ` ( Poly1 ` U ) ) )
29 25 28 ffvelcdmd 
 |-  ( ( ph /\ f e. ( Monic1p ` U ) ) -> ( O ` f ) e. ( Base ` ( R ^s B ) ) )
30 14 3 15 16 18 29 pwselbas 
 |-  ( ( ph /\ f e. ( Monic1p ` U ) ) -> ( O ` f ) : B --> B )
31 ffn 
 |-  ( ( O ` f ) : B --> B -> ( O ` f ) Fn B )
32 fniniseg 
 |-  ( ( O ` f ) Fn B -> ( X e. ( `' ( O ` f ) " { .0. } ) <-> ( X e. B /\ ( ( O ` f ) ` X ) = .0. ) ) )
33 30 31 32 3syl 
 |-  ( ( ph /\ f e. ( Monic1p ` U ) ) -> ( X e. ( `' ( O ` f ) " { .0. } ) <-> ( X e. B /\ ( ( O ` f ) ` X ) = .0. ) ) )
34 33 rexbidva 
 |-  ( ph -> ( E. f e. ( Monic1p ` U ) X e. ( `' ( O ` f ) " { .0. } ) <-> E. f e. ( Monic1p ` U ) ( X e. B /\ ( ( O ` f ) ` X ) = .0. ) ) )
35 13 34 bitrd 
 |-  ( ph -> ( X e. ( R IntgRing S ) <-> E. f e. ( Monic1p ` U ) ( X e. B /\ ( ( O ` f ) ` X ) = .0. ) ) )
36 r19.42v 
 |-  ( E. f e. ( Monic1p ` U ) ( X e. B /\ ( ( O ` f ) ` X ) = .0. ) <-> ( X e. B /\ E. f e. ( Monic1p ` U ) ( ( O ` f ) ` X ) = .0. ) )
37 35 36 bitrdi 
 |-  ( ph -> ( X e. ( R IntgRing S ) <-> ( X e. B /\ E. f e. ( Monic1p ` U ) ( ( O ` f ) ` X ) = .0. ) ) )