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

Metamath Proof Explorer

Theorem evl1fvf

Description: The univariate polynomial evaluation function as a function, with domain and codomain. (Contributed by Thierry Arnoux, 8-Jun-2025)

Ref Expression
Hypotheses evl1fvf.o 
|- O = ( eval1 ` R )
evl1fvf.p 
|- P = ( Poly1 ` R )
evl1fvf.u 
|- U = ( Base ` P )
evl1fvf.r 
|- ( ph -> R e. CRing )
evl1fvf.b 
|- B = ( Base ` R )
evl1fvf.q 
|- ( ph -> Q e. U )
Assertion evl1fvf 
|- ( ph -> ( O ` Q ) : B --> B )

Proof

Step Hyp Ref Expression
1 evl1fvf.o 
 |-  O = ( eval1 ` R )
2 evl1fvf.p 
 |-  P = ( Poly1 ` R )
3 evl1fvf.u 
 |-  U = ( Base ` P )
4 evl1fvf.r 
 |-  ( ph -> R e. CRing )
5 evl1fvf.b 
 |-  B = ( Base ` R )
6 evl1fvf.q 
 |-  ( ph -> Q e. U )
7 eqid 
 |-  ( R ^s B ) = ( R ^s B )
8 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
9 5 fvexi 
 |-  B e. _V
10 9 a1i 
 |-  ( ph -> B e. _V )
11 1 2 7 5 evl1rhm 
 |-  ( R e. CRing -> O e. ( P RingHom ( R ^s B ) ) )
12 3 8 rhmf 
 |-  ( O e. ( P RingHom ( R ^s B ) ) -> O : U --> ( Base ` ( R ^s B ) ) )
13 4 11 12 3syl 
 |-  ( ph -> O : U --> ( Base ` ( R ^s B ) ) )
14 13 6 ffvelcdmd 
 |-  ( ph -> ( O ` Q ) e. ( Base ` ( R ^s B ) ) )
15 7 5 8 4 10 14 pwselbas 
 |-  ( ph -> ( O ` Q ) : B --> B )