# 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 𝑄 = ( eval1𝑅 )
evl1varpw.w 𝑊 = ( Poly1𝑅 )
evl1varpw.g 𝐺 = ( mulGrp ‘ 𝑊 )
evl1varpw.x 𝑋 = ( var1𝑅 )
evl1varpw.b 𝐵 = ( Base ‘ 𝑅 )
evl1varpw.e = ( .g𝐺 )
evl1varpw.r ( 𝜑𝑅 ∈ CRing )
evl1varpw.n ( 𝜑𝑁 ∈ ℕ0 )
evl1scvarpw.t1 × = ( ·𝑠𝑊 )
evl1scvarpw.a ( 𝜑𝐴𝐵 )
evl1scvarpw.s 𝑆 = ( 𝑅s 𝐵 )
evl1scvarpw.t2 = ( .r𝑆 )
evl1scvarpw.m 𝑀 = ( mulGrp ‘ 𝑆 )
evl1scvarpw.f 𝐹 = ( .g𝑀 )
Assertion evl1scvarpw ( 𝜑 → ( 𝑄 ‘ ( 𝐴 × ( 𝑁 𝑋 ) ) ) = ( ( 𝐵 × { 𝐴 } ) ( 𝑁 𝐹 ( 𝑄𝑋 ) ) ) )

### Proof

Step Hyp Ref Expression
1 evl1varpw.q 𝑄 = ( eval1𝑅 )
2 evl1varpw.w 𝑊 = ( Poly1𝑅 )
3 evl1varpw.g 𝐺 = ( mulGrp ‘ 𝑊 )
4 evl1varpw.x 𝑋 = ( var1𝑅 )
5 evl1varpw.b 𝐵 = ( Base ‘ 𝑅 )
6 evl1varpw.e = ( .g𝐺 )
7 evl1varpw.r ( 𝜑𝑅 ∈ CRing )
8 evl1varpw.n ( 𝜑𝑁 ∈ ℕ0 )
9 evl1scvarpw.t1 × = ( ·𝑠𝑊 )
10 evl1scvarpw.a ( 𝜑𝐴𝐵 )
11 evl1scvarpw.s 𝑆 = ( 𝑅s 𝐵 )
12 evl1scvarpw.t2 = ( .r𝑆 )
13 evl1scvarpw.m 𝑀 = ( mulGrp ‘ 𝑆 )
14 evl1scvarpw.f 𝐹 = ( .g𝑀 )
15 2 ply1assa ( 𝑅 ∈ CRing → 𝑊 ∈ AssAlg )
16 7 15 syl ( 𝜑𝑊 ∈ AssAlg )
17 10 5 eleqtrdi ( 𝜑𝐴 ∈ ( Base ‘ 𝑅 ) )
18 2 ply1sca ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑊 ) )
19 18 eqcomd ( 𝑅 ∈ CRing → ( Scalar ‘ 𝑊 ) = 𝑅 )
20 7 19 syl ( 𝜑 → ( Scalar ‘ 𝑊 ) = 𝑅 )
21 20 fveq2d ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ 𝑅 ) )
22 17 21 eleqtrrd ( 𝜑𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
23 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
24 7 23 syl ( 𝜑𝑅 ∈ Ring )
25 2 ply1ring ( 𝑅 ∈ Ring → 𝑊 ∈ Ring )
26 24 25 syl ( 𝜑𝑊 ∈ Ring )
27 3 ringmgp ( 𝑊 ∈ Ring → 𝐺 ∈ Mnd )
28 26 27 syl ( 𝜑𝐺 ∈ Mnd )
29 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
30 4 2 29 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
31 24 30 syl ( 𝜑𝑋 ∈ ( Base ‘ 𝑊 ) )
32 3 29 mgpbas ( Base ‘ 𝑊 ) = ( Base ‘ 𝐺 )
33 32 6 mulgnn0cl ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑁 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
34 28 8 31 33 syl3anc ( 𝜑 → ( 𝑁 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
35 eqid ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
36 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
37 eqid ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
38 eqid ( .r𝑊 ) = ( .r𝑊 )
39 35 36 37 29 38 9 asclmul1 ( ( 𝑊 ∈ AssAlg ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑁 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) = ( 𝐴 × ( 𝑁 𝑋 ) ) )
40 16 22 34 39 syl3anc ( 𝜑 → ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) = ( 𝐴 × ( 𝑁 𝑋 ) ) )
41 40 eqcomd ( 𝜑 → ( 𝐴 × ( 𝑁 𝑋 ) ) = ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) )
42 41 fveq2d ( 𝜑 → ( 𝑄 ‘ ( 𝐴 × ( 𝑁 𝑋 ) ) ) = ( 𝑄 ‘ ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) ) )
43 1 2 11 5 evl1rhm ( 𝑅 ∈ CRing → 𝑄 ∈ ( 𝑊 RingHom 𝑆 ) )
44 7 43 syl ( 𝜑𝑄 ∈ ( 𝑊 RingHom 𝑆 ) )
45 2 ply1lmod ( 𝑅 ∈ Ring → 𝑊 ∈ LMod )
46 24 45 syl ( 𝜑𝑊 ∈ LMod )
47 35 36 26 46 37 29 asclf ( 𝜑 → ( algSc ‘ 𝑊 ) : ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) )
48 47 22 ffvelrnd ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝑊 ) )
49 29 38 12 rhmmul ( ( 𝑄 ∈ ( 𝑊 RingHom 𝑆 ) ∧ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑁 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) → ( 𝑄 ‘ ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) ) = ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ) ( 𝑄 ‘ ( 𝑁 𝑋 ) ) ) )
50 44 48 34 49 syl3anc ( 𝜑 → ( 𝑄 ‘ ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) ) = ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ) ( 𝑄 ‘ ( 𝑁 𝑋 ) ) ) )
51 1 2 5 35 evl1sca ( ( 𝑅 ∈ CRing ∧ 𝐴𝐵 ) → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ) = ( 𝐵 × { 𝐴 } ) )
52 7 10 51 syl2anc ( 𝜑 → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ) = ( 𝐵 × { 𝐴 } ) )
53 1 2 3 4 5 6 7 8 evl1varpw ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( 𝑄𝑋 ) ) )
54 11 fveq2i ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ ( 𝑅s 𝐵 ) )
55 13 54 eqtri 𝑀 = ( mulGrp ‘ ( 𝑅s 𝐵 ) )
56 55 fveq2i ( .g𝑀 ) = ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) )
57 14 56 eqtri 𝐹 = ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) )
58 57 a1i ( 𝜑𝐹 = ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) )
59 58 eqcomd ( 𝜑 → ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = 𝐹 )
60 59 oveqd ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( 𝑄𝑋 ) ) = ( 𝑁 𝐹 ( 𝑄𝑋 ) ) )
61 53 60 eqtrd ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 𝐹 ( 𝑄𝑋 ) ) )
62 52 61 oveq12d ( 𝜑 → ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ) ( 𝑄 ‘ ( 𝑁 𝑋 ) ) ) = ( ( 𝐵 × { 𝐴 } ) ( 𝑁 𝐹 ( 𝑄𝑋 ) ) ) )
63 42 50 62 3eqtrd ( 𝜑 → ( 𝑄 ‘ ( 𝐴 × ( 𝑁 𝑋 ) ) ) = ( ( 𝐵 × { 𝐴 } ) ( 𝑁 𝐹 ( 𝑄𝑋 ) ) ) )