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 eqid 
 |-  ( Base ` W ) = ( Base ` W )
24 3 23 mgpbas 
 |-  ( Base ` W ) = ( Base ` G )
25 crngring 
 |-  ( R e. CRing -> R e. Ring )
26 7 25 syl 
 |-  ( ph -> R e. Ring )
27 2 ply1ring 
 |-  ( R e. Ring -> W e. Ring )
28 26 27 syl 
 |-  ( ph -> W e. Ring )
29 3 ringmgp 
 |-  ( W e. Ring -> G e. Mnd )
30 28 29 syl 
 |-  ( ph -> G e. Mnd )
31 4 2 23 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` W ) )
32 26 31 syl 
 |-  ( ph -> X e. ( Base ` W ) )
33 24 6 30 8 32 mulgnn0cld 
 |-  ( ph -> ( N .^ X ) e. ( Base ` W ) )
34 eqid 
 |-  ( algSc ` W ) = ( algSc ` W )
35 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
36 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
37 eqid 
 |-  ( .r ` W ) = ( .r ` W )
38 34 35 36 23 37 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 ) ) )
39 16 22 33 38 syl3anc 
 |-  ( ph -> ( ( ( algSc ` W ) ` A ) ( .r ` W ) ( N .^ X ) ) = ( A .X. ( N .^ X ) ) )
40 39 eqcomd 
 |-  ( ph -> ( A .X. ( N .^ X ) ) = ( ( ( algSc ` W ) ` A ) ( .r ` W ) ( N .^ X ) ) )
41 40 fveq2d 
 |-  ( ph -> ( Q ` ( A .X. ( N .^ X ) ) ) = ( Q ` ( ( ( algSc ` W ) ` A ) ( .r ` W ) ( N .^ X ) ) ) )
42 1 2 11 5 evl1rhm 
 |-  ( R e. CRing -> Q e. ( W RingHom S ) )
43 7 42 syl 
 |-  ( ph -> Q e. ( W RingHom S ) )
44 2 ply1lmod 
 |-  ( R e. Ring -> W e. LMod )
45 26 44 syl 
 |-  ( ph -> W e. LMod )
46 34 35 28 45 36 23 asclf 
 |-  ( ph -> ( algSc ` W ) : ( Base ` ( Scalar ` W ) ) --> ( Base ` W ) )
47 46 22 ffvelcdmd 
 |-  ( ph -> ( ( algSc ` W ) ` A ) e. ( Base ` W ) )
48 23 37 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 ) ) ) )
49 43 47 33 48 syl3anc 
 |-  ( ph -> ( Q ` ( ( ( algSc ` W ) ` A ) ( .r ` W ) ( N .^ X ) ) ) = ( ( Q ` ( ( algSc ` W ) ` A ) ) .xb ( Q ` ( N .^ X ) ) ) )
50 1 2 5 34 evl1sca 
 |-  ( ( R e. CRing /\ A e. B ) -> ( Q ` ( ( algSc ` W ) ` A ) ) = ( B X. { A } ) )
51 7 10 50 syl2anc 
 |-  ( ph -> ( Q ` ( ( algSc ` W ) ` A ) ) = ( B X. { A } ) )
52 1 2 3 4 5 6 7 8 evl1varpw 
 |-  ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( Q ` X ) ) )
53 11 fveq2i 
 |-  ( mulGrp ` S ) = ( mulGrp ` ( R ^s B ) )
54 13 53 eqtri 
 |-  M = ( mulGrp ` ( R ^s B ) )
55 54 fveq2i 
 |-  ( .g ` M ) = ( .g ` ( mulGrp ` ( R ^s B ) ) )
56 14 55 eqtri 
 |-  F = ( .g ` ( mulGrp ` ( R ^s B ) ) )
57 56 a1i 
 |-  ( ph -> F = ( .g ` ( mulGrp ` ( R ^s B ) ) ) )
58 57 eqcomd 
 |-  ( ph -> ( .g ` ( mulGrp ` ( R ^s B ) ) ) = F )
59 58 oveqd 
 |-  ( ph -> ( N ( .g ` ( mulGrp ` ( R ^s B ) ) ) ( Q ` X ) ) = ( N F ( Q ` X ) ) )
60 52 59 eqtrd 
 |-  ( ph -> ( Q ` ( N .^ X ) ) = ( N F ( Q ` X ) ) )
61 51 60 oveq12d 
 |-  ( ph -> ( ( Q ` ( ( algSc ` W ) ` A ) ) .xb ( Q ` ( N .^ X ) ) ) = ( ( B X. { A } ) .xb ( N F ( Q ` X ) ) ) )
62 41 49 61 3eqtrd 
 |-  ( ph -> ( Q ` ( A .X. ( N .^ X ) ) ) = ( ( B X. { A } ) .xb ( N F ( Q ` X ) ) ) )