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

Metamath Proof Explorer

Theorem evl1vard

Description: Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses evl1var.q 
|- O = ( eval1 ` R )
evl1var.v 
|- X = ( var1 ` R )
evl1var.b 
|- B = ( Base ` R )
evl1vard.p 
|- P = ( Poly1 ` R )
evl1vard.u 
|- U = ( Base ` P )
evl1vard.1 
|- ( ph -> R e. CRing )
evl1vard.2 
|- ( ph -> Y e. B )
Assertion evl1vard 
|- ( ph -> ( X e. U /\ ( ( O ` X ) ` Y ) = Y ) )

Proof

Step Hyp Ref Expression
1 evl1var.q 
 |-  O = ( eval1 ` R )
2 evl1var.v 
 |-  X = ( var1 ` R )
3 evl1var.b 
 |-  B = ( Base ` R )
4 evl1vard.p 
 |-  P = ( Poly1 ` R )
5 evl1vard.u 
 |-  U = ( Base ` P )
6 evl1vard.1 
 |-  ( ph -> R e. CRing )
7 evl1vard.2 
 |-  ( ph -> Y e. B )
8 crngring 
 |-  ( R e. CRing -> R e. Ring )
9 2 4 5 vr1cl 
 |-  ( R e. Ring -> X e. U )
10 6 8 9 3syl 
 |-  ( ph -> X e. U )
11 1 2 3 evl1var 
 |-  ( R e. CRing -> ( O ` X ) = ( _I |` B ) )
12 6 11 syl 
 |-  ( ph -> ( O ` X ) = ( _I |` B ) )
13 12 fveq1d 
 |-  ( ph -> ( ( O ` X ) ` Y ) = ( ( _I |` B ) ` Y ) )
14 fvresi 
 |-  ( Y e. B -> ( ( _I |` B ) ` Y ) = Y )
15 7 14 syl 
 |-  ( ph -> ( ( _I |` B ) ` Y ) = Y )
16 13 15 eqtrd 
 |-  ( ph -> ( ( O ` X ) ` Y ) = Y )
17 10 16 jca 
 |-  ( ph -> ( X e. U /\ ( ( O ` X ) ` Y ) = Y ) )