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

Metamath Proof Explorer

Theorem evlvar

Description: Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019)

Ref Expression
Hypotheses evlvar.q 
|- Q = ( I eval S )
evlvar.v 
|- V = ( I mVar S )
evlvar.b 
|- B = ( Base ` S )
evlvar.i 
|- ( ph -> I e. W )
evlvar.s 
|- ( ph -> S e. CRing )
evlvar.x 
|- ( ph -> X e. I )
Assertion evlvar 
|- ( ph -> ( Q ` ( V ` X ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )

Proof

Step Hyp Ref Expression
1 evlvar.q 
 |-  Q = ( I eval S )
2 evlvar.v 
 |-  V = ( I mVar S )
3 evlvar.b 
 |-  B = ( Base ` S )
4 evlvar.i 
 |-  ( ph -> I e. W )
5 evlvar.s 
 |-  ( ph -> S e. CRing )
6 evlvar.x 
 |-  ( ph -> X e. I )
7 eqid 
 |-  ( ( I evalSub S ) ` B ) = ( ( I evalSub S ) ` B )
8 eqid 
 |-  ( I mVar ( S |`s B ) ) = ( I mVar ( S |`s B ) )
9 eqid 
 |-  ( S |`s B ) = ( S |`s B )
10 crngring 
 |-  ( S e. CRing -> S e. Ring )
11 3 subrgid 
 |-  ( S e. Ring -> B e. ( SubRing ` S ) )
12 5 10 11 3syl 
 |-  ( ph -> B e. ( SubRing ` S ) )
13 7 1 8 9 3 4 5 12 6 evlsvarsrng 
 |-  ( ph -> ( ( ( I evalSub S ) ` B ) ` ( ( I mVar ( S |`s B ) ) ` X ) ) = ( Q ` ( ( I mVar ( S |`s B ) ) ` X ) ) )
14 7 8 9 3 4 5 12 6 evlsvar 
 |-  ( ph -> ( ( ( I evalSub S ) ` B ) ` ( ( I mVar ( S |`s B ) ) ` X ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )
15 2 4 12 9 subrgmvr 
 |-  ( ph -> V = ( I mVar ( S |`s B ) ) )
16 15 fveq1d 
 |-  ( ph -> ( V ` X ) = ( ( I mVar ( S |`s B ) ) ` X ) )
17 16 eqcomd 
 |-  ( ph -> ( ( I mVar ( S |`s B ) ) ` X ) = ( V ` X ) )
18 17 fveq2d 
 |-  ( ph -> ( Q ` ( ( I mVar ( S |`s B ) ) ` X ) ) = ( Q ` ( V ` X ) ) )
19 13 14 18 3eqtr3rd 
 |-  ( ph -> ( Q ` ( V ` X ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )