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 syl5eq 
 |-  ( 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 syl5eq 
 |-  ( 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 ) ) )