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

Metamath Proof Explorer

Theorem evls1fvf

Description: The subring evaluation function for a univariate polynomial as a function, with domain and codomain. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses evls1fn.o 
|- O = ( R evalSub1 S )
evls1fn.p 
|- P = ( Poly1 ` ( R |`s S ) )
evls1fn.u 
|- U = ( Base ` P )
evls1fn.1 
|- ( ph -> R e. CRing )
evls1fn.2 
|- ( ph -> S e. ( SubRing ` R ) )
evls1fvf.b 
|- B = ( Base ` R )
evls1fvf.q 
|- ( ph -> Q e. U )
Assertion evls1fvf 
|- ( ph -> ( O ` Q ) : B --> B )

Proof

Step Hyp Ref Expression
1 evls1fn.o 
 |-  O = ( R evalSub1 S )
2 evls1fn.p 
 |-  P = ( Poly1 ` ( R |`s S ) )
3 evls1fn.u 
 |-  U = ( Base ` P )
4 evls1fn.1 
 |-  ( ph -> R e. CRing )
5 evls1fn.2 
 |-  ( ph -> S e. ( SubRing ` R ) )
6 evls1fvf.b 
 |-  B = ( Base ` R )
7 evls1fvf.q 
 |-  ( ph -> Q e. U )
8 eqid 
 |-  ( R ^s B ) = ( R ^s B )
9 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
10 6 fvexi 
 |-  B e. _V
11 10 a1i 
 |-  ( ph -> B e. _V )
12 eqid 
 |-  ( R |`s S ) = ( R |`s S )
13 1 6 8 12 2 evls1rhm 
 |-  ( ( R e. CRing /\ S e. ( SubRing ` R ) ) -> O e. ( P RingHom ( R ^s B ) ) )
14 4 5 13 syl2anc 
 |-  ( ph -> O e. ( P RingHom ( R ^s B ) ) )
15 3 9 rhmf 
 |-  ( O e. ( P RingHom ( R ^s B ) ) -> O : U --> ( Base ` ( R ^s B ) ) )
16 14 15 syl 
 |-  ( ph -> O : U --> ( Base ` ( R ^s B ) ) )
17 16 7 ffvelcdmd 
 |-  ( ph -> ( O ` Q ) e. ( Base ` ( R ^s B ) ) )
18 8 6 9 4 11 17 pwselbas 
 |-  ( ph -> ( O ` Q ) : B --> B )