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

Metamath Proof Explorer

Theorem evls1fn

Description: Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-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 ) )
Assertion evls1fn 
|- ( ph -> O Fn U )

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 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( R ^s ( Base ` R ) ) = ( R ^s ( Base ` R ) )
8 eqid 
 |-  ( R |`s S ) = ( R |`s S )
9 1 6 7 8 2 evls1rhm 
 |-  ( ( R e. CRing /\ S e. ( SubRing ` R ) ) -> O e. ( P RingHom ( R ^s ( Base ` R ) ) ) )
10 4 5 9 syl2anc 
 |-  ( ph -> O e. ( P RingHom ( R ^s ( Base ` R ) ) ) )
11 eqid 
 |-  ( Base ` ( R ^s ( Base ` R ) ) ) = ( Base ` ( R ^s ( Base ` R ) ) )
12 3 11 rhmf 
 |-  ( O e. ( P RingHom ( R ^s ( Base ` R ) ) ) -> O : U --> ( Base ` ( R ^s ( Base ` R ) ) ) )
13 10 12 syl 
 |-  ( ph -> O : U --> ( Base ` ( R ^s ( Base ` R ) ) ) )
14 13 ffnd 
 |-  ( ph -> O Fn U )