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

Metamath Proof Explorer

Theorem evl1scvarpwval

Description: Value of a univariate polynomial evaluation mapping a multiple of an exponentiation of a variable to the multiple of the exponentiation of the evaluated variable. (Contributed by AV, 18-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 )
evl1scvarpw.t1 
|- .X. = ( .s ` W )
evl1scvarpw.a 
|- ( ph -> A e. B )
evl1scvarpwval.c 
|- ( ph -> C e. B )
evl1scvarpwval.h 
|- H = ( mulGrp ` R )
evl1scvarpwval.e 
|- E = ( .g ` H )
evl1scvarpwval.t 
|- .x. = ( .r ` R )
Assertion evl1scvarpwval 
|- ( ph -> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) = ( A .x. ( 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 evl1scvarpw.t1 
 |-  .X. = ( .s ` W )
10 evl1scvarpw.a 
 |-  ( ph -> A e. B )
11 evl1scvarpwval.c 
 |-  ( ph -> C e. B )
12 evl1scvarpwval.h 
 |-  H = ( mulGrp ` R )
13 evl1scvarpwval.e 
 |-  E = ( .g ` H )
14 evl1scvarpwval.t 
 |-  .x. = ( .r ` R )
15 eqid 
 |-  ( Base ` W ) = ( Base ` W )
16 3 15 mgpbas 
 |-  ( Base ` W ) = ( Base ` G )
17 crngring 
 |-  ( R e. CRing -> R e. Ring )
18 7 17 syl 
 |-  ( ph -> R e. Ring )
19 2 ply1ring 
 |-  ( R e. Ring -> W e. Ring )
20 18 19 syl 
 |-  ( ph -> W e. Ring )
21 3 ringmgp 
 |-  ( W e. Ring -> G e. Mnd )
22 20 21 syl 
 |-  ( ph -> G e. Mnd )
23 4 2 15 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` W ) )
24 18 23 syl 
 |-  ( ph -> X e. ( Base ` W ) )
25 16 6 22 8 24 mulgnn0cld 
 |-  ( ph -> ( N .^ X ) e. ( Base ` W ) )
26 1 2 3 4 5 6 7 8 11 12 13 evl1varpwval 
 |-  ( ph -> ( ( Q ` ( N .^ X ) ) ` C ) = ( N E C ) )
27 25 26 jca 
 |-  ( ph -> ( ( N .^ X ) e. ( Base ` W ) /\ ( ( Q ` ( N .^ X ) ) ` C ) = ( N E C ) ) )
28 1 2 5 15 7 11 27 10 9 14 evl1vsd 
 |-  ( ph -> ( ( A .X. ( N .^ X ) ) e. ( Base ` W ) /\ ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) = ( A .x. ( N E C ) ) ) )
29 28 simprd 
 |-  ( ph -> ( ( Q ` ( A .X. ( N .^ X ) ) ) ` C ) = ( A .x. ( N E C ) ) )