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

Metamath Proof Explorer

Theorem fveval1fvcl

Description: The function value of the evaluation function of a polynomial is an element of the underlying ring. (Contributed by AV, 17-Sep-2019)

Ref Expression
Hypotheses fveval1fvcl.q 
|- O = ( eval1 ` R )
fveval1fvcl.p 
|- P = ( Poly1 ` R )
fveval1fvcl.b 
|- B = ( Base ` R )
fveval1fvcl.u 
|- U = ( Base ` P )
fveval1fvcl.r 
|- ( ph -> R e. CRing )
fveval1fvcl.y 
|- ( ph -> Y e. B )
fveval1fvcl.m 
|- ( ph -> M e. U )
Assertion fveval1fvcl 
|- ( ph -> ( ( O ` M ) ` Y ) e. B )

Proof

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