Metamath Proof Explorer

Theorem evls1maprnss

Description: The function F mapping polynomials p to their subring evaluation at a given point A takes all values in the subring S . (Contributed by Thierry Arnoux, 25-Feb-2025)

Ref Expression
Hypotheses evls1maprhm.q 
|- O = ( R evalSub1 S )
evls1maprhm.p 
|- P = ( Poly1 ` ( R |`s S ) )
evls1maprhm.b 
|- B = ( Base ` R )
evls1maprhm.u 
|- U = ( Base ` P )
evls1maprhm.r 
|- ( ph -> R e. CRing )
evls1maprhm.s 
|- ( ph -> S e. ( SubRing ` R ) )
evls1maprhm.y 
|- ( ph -> X e. B )
evls1maprhm.f 
|- F = ( p e. U |-> ( ( O ` p ) ` X ) )
Assertion evls1maprnss 
|- ( ph -> S C_ ran F )

Proof

Step Hyp Ref Expression
1 evls1maprhm.q 
 |-  O = ( R evalSub1 S )
2 evls1maprhm.p 
 |-  P = ( Poly1 ` ( R |`s S ) )
3 evls1maprhm.b 
 |-  B = ( Base ` R )
4 evls1maprhm.u 
 |-  U = ( Base ` P )
5 evls1maprhm.r 
 |-  ( ph -> R e. CRing )
6 evls1maprhm.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
7 evls1maprhm.y 
 |-  ( ph -> X e. B )
8 evls1maprhm.f 
 |-  F = ( p e. U |-> ( ( O ` p ) ` X ) )
9 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
10 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
11 eqid 
 |-  ( R |`s S ) = ( R |`s S )
12 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
13 9 10 11 2 6 12 subrg1ascl 
 |-  ( ph -> ( algSc ` P ) = ( ( algSc ` ( Poly1 ` R ) ) |` S ) )
14 13 adantr 
 |-  ( ( ph /\ y e. S ) -> ( algSc ` P ) = ( ( algSc ` ( Poly1 ` R ) ) |` S ) )
15 14 fveq1d 
 |-  ( ( ph /\ y e. S ) -> ( ( algSc ` P ) ` y ) = ( ( ( algSc ` ( Poly1 ` R ) ) |` S ) ` y ) )
16 simpr 
 |-  ( ( ph /\ y e. S ) -> y e. S )
17 16 fvresd 
 |-  ( ( ph /\ y e. S ) -> ( ( ( algSc ` ( Poly1 ` R ) ) |` S ) ` y ) = ( ( algSc ` ( Poly1 ` R ) ) ` y ) )
18 15 17 eqtrd 
 |-  ( ( ph /\ y e. S ) -> ( ( algSc ` P ) ` y ) = ( ( algSc ` ( Poly1 ` R ) ) ` y ) )
19 6 adantr 
 |-  ( ( ph /\ y e. S ) -> S e. ( SubRing ` R ) )
20 10 11 9 2 4 19 16 asclply1subcl 
 |-  ( ( ph /\ y e. S ) -> ( ( algSc ` ( Poly1 ` R ) ) ` y ) e. U )
21 18 20 eqeltrd 
 |-  ( ( ph /\ y e. S ) -> ( ( algSc ` P ) ` y ) e. U )
22 fveq2 
 |-  ( p = ( ( algSc ` P ) ` y ) -> ( O ` p ) = ( O ` ( ( algSc ` P ) ` y ) ) )
23 22 fveq1d 
 |-  ( p = ( ( algSc ` P ) ` y ) -> ( ( O ` p ) ` X ) = ( ( O ` ( ( algSc ` P ) ` y ) ) ` X ) )
24 23 eqeq2d 
 |-  ( p = ( ( algSc ` P ) ` y ) -> ( y = ( ( O ` p ) ` X ) <-> y = ( ( O ` ( ( algSc ` P ) ` y ) ) ` X ) ) )
25 24 adantl 
 |-  ( ( ( ph /\ y e. S ) /\ p = ( ( algSc ` P ) ` y ) ) -> ( y = ( ( O ` p ) ` X ) <-> y = ( ( O ` ( ( algSc ` P ) ` y ) ) ` X ) ) )
26 5 adantr 
 |-  ( ( ph /\ y e. S ) -> R e. CRing )
27 1 2 11 3 12 26 19 16 evls1sca 
 |-  ( ( ph /\ y e. S ) -> ( O ` ( ( algSc ` P ) ` y ) ) = ( B X. { y } ) )
28 27 fveq1d 
 |-  ( ( ph /\ y e. S ) -> ( ( O ` ( ( algSc ` P ) ` y ) ) ` X ) = ( ( B X. { y } ) ` X ) )
29 7 adantr 
 |-  ( ( ph /\ y e. S ) -> X e. B )
30 vex 
 |-  y e. _V
31 30 fvconst2 
 |-  ( X e. B -> ( ( B X. { y } ) ` X ) = y )
32 29 31 syl 
 |-  ( ( ph /\ y e. S ) -> ( ( B X. { y } ) ` X ) = y )
33 28 32 eqtr2d 
 |-  ( ( ph /\ y e. S ) -> y = ( ( O ` ( ( algSc ` P ) ` y ) ) ` X ) )
34 21 25 33 rspcedvd 
 |-  ( ( ph /\ y e. S ) -> E. p e. U y = ( ( O ` p ) ` X ) )
35 8 34 16 elrnmptd 
 |-  ( ( ph /\ y e. S ) -> y e. ran F )
36 35 ex 
 |-  ( ph -> ( y e. S -> y e. ran F ) )
37 36 ssrdv 
 |-  ( ph -> S C_ ran F )