Metamath Proof Explorer

Theorem evl1scvarpw

Description: Univariate polynomial evaluation maps a multiple of an exponentiation of a variable to the multiple of an 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 )
evl1scvarpw.s 
|- S = ( R ^s B )
evl1scvarpw.t2 
|- .xb = ( .r ` S )
evl1scvarpw.m 
|- M = ( mulGrp ` S )
evl1scvarpw.f 
|- F = ( .g ` M )
Assertion evl1scvarpw 
|- ( ph -> ( Q ` ( A .X. ( N .^ X ) ) ) = ( ( B X. { A } ) .xb ( N F ( 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 evl1scvarpw.t1 
 |-  .X. = ( .s ` W )
10 evl1scvarpw.a 
 |-  ( ph -> A e. B )
11 evl1scvarpw.s 
 |-  S = ( R ^s B )
12 evl1scvarpw.t2 
 |-  .xb = ( .r ` S )
13 evl1scvarpw.m 
 |-  M = ( mulGrp ` S )
14 evl1scvarpw.f 
 |-  F = ( .g ` M )
15 2 ply1assa 
 |-  ( R e. CRing -> W e. AssAlg )
16 7 15 syl 
 |-  ( ph -> W e. AssAlg )
17 10 5 eleqtrdi 
 |-  ( ph -> A e. ( Base ` R ) )
18 2 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` W ) )
19 18 eqcomd 
 |-  ( R e. CRing -> ( Scalar ` W ) = R )
20 7 19 syl 
 |-  ( ph -> ( Scalar ` W ) = R )
21 20 fveq2d 
 |-  ( ph -> ( Base ` ( Scalar ` W ) ) = ( Base ` R ) )
22 17 21 eleqtrrd 
 |-  ( ph -> A e. ( Base ` ( Scalar ` W ) ) )
23 crngring 
 |-  ( R e. CRing -> R e. Ring )
24 7 23 syl 
 |-  ( ph -> R e. Ring )
25 2 ply1ring 
 |-  ( R e. Ring -> W e. Ring )
26 24 25 syl 
 |-  ( ph -> W e. Ring )
27 3 ringmgp 
 |-  ( W e. Ring -> G e. Mnd )
28 26 27 syl 
 |-  ( ph -> G e. Mnd )
29 eqid 
 |-  ( Base ` W ) = ( Base ` W )
30 4 2 29 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` W ) )
31 24 30 syl 
 |-  ( ph -> X e. ( Base ` W ) )
32 3 29 mgpbas 
 |-  ( Base ` W ) = ( Base ` G )
33 32 6 mulgnn0cl 
 |-  ( ( G e. Mnd /\ N e. NN0 /\ X e. ( Base ` W ) ) -> ( N .^ X ) e. ( Base ` W ) )
34 28 8 31 33 syl3anc 
 |-  ( ph -> ( N .^ X ) e. ( Base ` W ) )
35 eqid 
 |-  ( algSc ` W ) = ( algSc ` W )
36 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
37 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
38 eqid 
 |-  ( .r ` W ) = ( .r ` W )
39 35 36 37 29 38 9 asclmul1 
 |-  ( ( W e. AssAlg /\ A e. ( Base ` ( Scalar ` W ) ) /\ ( N .^ X ) e. ( Base ` W ) ) -> ( ( ( algSc ` W ) ` A ) ( .r ` W ) ( N .^ X ) ) = ( A .X. ( N .^ X ) ) )
40 16 22 34 39 syl3anc 
 |-  ( ph -> ( ( ( algSc ` W ) ` A ) ( .r ` W ) ( N .^ X ) ) = ( A .X. ( N .^ X ) ) )
41 40 eqcomd 
 |-  ( ph -> ( A .X. ( N .^ X ) ) = ( ( ( algSc ` W ) ` A ) ( .r ` W ) ( N .^ X ) ) )
42 41 fveq2d 
 |-  ( ph -> ( Q ` ( A .X. ( N .^ X ) ) ) = ( Q ` ( ( ( algSc ` W ) ` A ) ( .r ` W ) ( N .^ X ) ) ) )
43 1 2 11 5 evl1rhm 
 |-  ( R e. CRing -> Q e. ( W RingHom S ) )
44 7 43 syl 
 |-  ( ph -> Q e. ( W RingHom S ) )
45 2 ply1lmod 
 |-  ( R e. Ring -> W e. LMod )
46 24 45 syl 
 |-  ( ph -> W e. LMod )
47 35 36 26 46 37 29 asclf 
 |-  ( ph -> ( algSc ` W ) : ( Base ` ( Scalar ` W ) ) --> ( Base ` W ) )
48 47 22 ffvelrnd 
 |-  ( ph -> ( ( algSc ` W ) ` A ) e. ( Base ` W ) )
49 29 38 12 rhmmul 
 |-  ( ( Q e. ( W RingHom S ) /\ ( ( algSc ` W ) ` A ) e. ( Base ` W ) /\ ( N .^ X ) e. ( Base ` W ) ) -> ( Q ` ( ( ( algSc ` W ) ` A ) ( .r ` W ) ( N .^ X ) ) ) = ( ( Q ` ( ( algSc ` W ) ` A ) ) .xb ( Q ` ( N .^ X ) ) ) )
50 44 48 34 49 syl3anc 
 |-  ( ph -> ( Q ` ( ( ( algSc ` W ) ` A ) ( .r ` W ) ( N .^ X ) ) ) = ( ( Q ` ( ( algSc ` W ) ` A ) ) .xb ( Q ` ( N .^ X ) ) ) )
51 1 2 5 35 evl1sca 
 |-  ( ( R e. CRing /\ A e. B ) -> ( Q ` ( ( algSc ` W ) ` A ) ) = ( B X. { A } ) )
52 7 10 51 syl2anc 
 |-  ( ph -> ( Q ` ( ( algSc ` W ) ` A ) ) = ( B X. { A } ) )
53 1 2 3 4 5 6 7 8 evl1varpw 
 |-  ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( Q ` X ) ) )
54 11 fveq2i 
 |-  ( mulGrp ` S ) = ( mulGrp ` ( R ^s B ) )
55 13 54 eqtri 
 |-  M = ( mulGrp ` ( R ^s B ) )
56 55 fveq2i 
 |-  ( .g ` M ) = ( .g ` ( mulGrp ` ( R ^s B ) ) )
57 14 56 eqtri 
 |-  F = ( .g ` ( mulGrp ` ( R ^s B ) ) )
58 57 a1i 
 |-  ( ph -> F = ( .g ` ( mulGrp ` ( R ^s B ) ) ) )
59 58 eqcomd 
 |-  ( ph -> ( .g ` ( mulGrp ` ( R ^s B ) ) ) = F )
60 59 oveqd 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( Q ` X ) ) = ( N F ( Q ` X ) ) )
61 53 60 eqtrd 
 |-  ( ph -> ( Q ` ( N .^ X ) ) = ( N F ( Q ` X ) ) )
62 52 61 oveq12d 
 |-  ( ph -> ( ( Q ` ( ( algSc ` W ) ` A ) ) .xb ( Q ` ( N .^ X ) ) ) = ( ( B X. { A } ) .xb ( N F ( Q ` X ) ) ) )
63 42 50 62 3eqtrd 
 |-  ( ph -> ( Q ` ( A .X. ( N .^ X ) ) ) = ( ( B X. { A } ) .xb ( N F ( Q ` X ) ) ) )