Metamath Proof Explorer


Theorem evl1varpw

Description: Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd , the proof is shorter using evls1varpw instead of proving it directly. (Contributed by AV, 15-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 )
Assertion evl1varpw
|- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( Q ` X ) ) )

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 1 5 evl1fval1
 |-  Q = ( R evalSub1 B )
10 9 a1i
 |-  ( ph -> Q = ( R evalSub1 B ) )
11 2 fveq2i
 |-  ( mulGrp ` W ) = ( mulGrp ` ( Poly1 ` R ) )
12 3 11 eqtri
 |-  G = ( mulGrp ` ( Poly1 ` R ) )
13 12 fveq2i
 |-  ( .g ` G ) = ( .g ` ( mulGrp ` ( Poly1 ` R ) ) )
14 6 13 eqtri
 |-  .^ = ( .g ` ( mulGrp ` ( Poly1 ` R ) ) )
15 5 ressid
 |-  ( R e. CRing -> ( R |`s B ) = R )
16 7 15 syl
 |-  ( ph -> ( R |`s B ) = R )
17 16 eqcomd
 |-  ( ph -> R = ( R |`s B ) )
18 17 fveq2d
 |-  ( ph -> ( Poly1 ` R ) = ( Poly1 ` ( R |`s B ) ) )
19 18 fveq2d
 |-  ( ph -> ( mulGrp ` ( Poly1 ` R ) ) = ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) )
20 19 fveq2d
 |-  ( ph -> ( .g ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) )
21 14 20 eqtrid
 |-  ( ph -> .^ = ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) )
22 eqidd
 |-  ( ph -> N = N )
23 17 fveq2d
 |-  ( ph -> ( var1 ` R ) = ( var1 ` ( R |`s B ) ) )
24 4 23 eqtrid
 |-  ( ph -> X = ( var1 ` ( R |`s B ) ) )
25 21 22 24 oveq123d
 |-  ( ph -> ( N .^ X ) = ( N ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) ( var1 ` ( R |`s B ) ) ) )
26 10 25 fveq12d
 |-  ( ph -> ( Q ` ( N .^ X ) ) = ( ( R evalSub1 B ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) ( var1 ` ( R |`s B ) ) ) ) )
27 eqid
 |-  ( R evalSub1 B ) = ( R evalSub1 B )
28 eqid
 |-  ( R |`s B ) = ( R |`s B )
29 eqid
 |-  ( Poly1 ` ( R |`s B ) ) = ( Poly1 ` ( R |`s B ) )
30 eqid
 |-  ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) = ( mulGrp ` ( Poly1 ` ( R |`s B ) ) )
31 eqid
 |-  ( var1 ` ( R |`s B ) ) = ( var1 ` ( R |`s B ) )
32 eqid
 |-  ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) )
33 crngring
 |-  ( R e. CRing -> R e. Ring )
34 5 subrgid
 |-  ( R e. Ring -> B e. ( SubRing ` R ) )
35 7 33 34 3syl
 |-  ( ph -> B e. ( SubRing ` R ) )
36 27 28 29 30 31 5 32 7 35 8 evls1varpw
 |-  ( ph -> ( ( R evalSub1 B ) ` ( N ( .g ` ( mulGrp ` ( Poly1 ` ( R |`s B ) ) ) ) ( var1 ` ( R |`s B ) ) ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( ( R evalSub1 B ) ` ( var1 ` ( R |`s B ) ) ) ) )
37 9 eqcomi
 |-  ( R evalSub1 B ) = Q
38 37 a1i
 |-  ( ph -> ( R evalSub1 B ) = Q )
39 24 eqcomd
 |-  ( ph -> ( var1 ` ( R |`s B ) ) = X )
40 38 39 fveq12d
 |-  ( ph -> ( ( R evalSub1 B ) ` ( var1 ` ( R |`s B ) ) ) = ( Q ` X ) )
41 40 oveq2d
 |-  ( ph -> ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( ( R evalSub1 B ) ` ( var1 ` ( R |`s B ) ) ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( Q ` X ) ) )
42 26 36 41 3eqtrd
 |-  ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( Q ` X ) ) )