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

Metamath Proof Explorer

Theorem evl1varpwval

Description: Value of a univariate polynomial evaluation mapping the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019)

Ref Expression
Hypotheses evl1varpw.q 
|- Q = ( eval1 ` R )
evl1varpw.w 
|- W = ( Poly1 ` R )
evl1varpw.g 
|- G = ( mulGrp ` W )
evl1varpw.x 
|- X = ( var1 ` R )
evl1varpw.b 
|- B = ( Base ` R )
evl1varpw.e 
|- .^ = ( .g ` G )
evl1varpw.r 
|- ( ph -> R e. CRing )
evl1varpw.n 
|- ( ph -> N e. NN0 )
evl1varpwval.c 
|- ( ph -> C e. B )
evl1varpwval.h 
|- H = ( mulGrp ` R )
evl1varpwval.e 
|- E = ( .g ` H )
Assertion evl1varpwval 
|- ( ph -> ( ( Q ` ( N .^ X ) ) ` C ) = ( N E C ) )

Proof

Step Hyp Ref Expression
1 evl1varpw.q 
 |-  Q = ( eval1 ` R )
2 evl1varpw.w 
 |-  W = ( Poly1 ` R )
3 evl1varpw.g 
 |-  G = ( mulGrp ` W )
4 evl1varpw.x 
 |-  X = ( var1 ` R )
5 evl1varpw.b 
 |-  B = ( Base ` R )
6 evl1varpw.e 
 |-  .^ = ( .g ` G )
7 evl1varpw.r 
 |-  ( ph -> R e. CRing )
8 evl1varpw.n 
 |-  ( ph -> N e. NN0 )
9 evl1varpwval.c 
 |-  ( ph -> C e. B )
10 evl1varpwval.h 
 |-  H = ( mulGrp ` R )
11 evl1varpwval.e 
 |-  E = ( .g ` H )
12 eqid 
 |-  ( Base ` W ) = ( Base ` W )
13 1 4 5 2 12 7 9 evl1vard 
 |-  ( ph -> ( X e. ( Base ` W ) /\ ( ( Q ` X ) ` C ) = C ) )
14 3 fveq2i 
 |-  ( .g ` G ) = ( .g ` ( mulGrp ` W ) )
15 6 14 eqtri 
 |-  .^ = ( .g ` ( mulGrp ` W ) )
16 10 fveq2i 
 |-  ( .g ` H ) = ( .g ` ( mulGrp ` R ) )
17 11 16 eqtri 
 |-  E = ( .g ` ( mulGrp ` R ) )
18 1 2 5 12 7 9 13 15 17 8 evl1expd 
 |-  ( ph -> ( ( N .^ X ) e. ( Base ` W ) /\ ( ( Q ` ( N .^ X ) ) ` C ) = ( N E C ) ) )
19 18 simprd 
 |-  ( ph -> ( ( Q ` ( N .^ X ) ) ` C ) = ( N E C ) )