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 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
24 3 23 mgpbas ( Base ‘ 𝑊 ) = ( Base ‘ 𝐺 )
25 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
26 7 25 syl ( 𝜑𝑅 ∈ Ring )
27 2 ply1ring ( 𝑅 ∈ Ring → 𝑊 ∈ Ring )
28 26 27 syl ( 𝜑𝑊 ∈ Ring )
29 3 ringmgp ( 𝑊 ∈ Ring → 𝐺 ∈ Mnd )
30 28 29 syl ( 𝜑𝐺 ∈ Mnd )
31 4 2 23 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
32 26 31 syl ( 𝜑𝑋 ∈ ( Base ‘ 𝑊 ) )
33 24 6 30 8 32 mulgnn0cld ( 𝜑 → ( 𝑁 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
34 eqid ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
35 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
36 eqid ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
37 eqid ( .r𝑊 ) = ( .r𝑊 )
38 34 35 36 23 37 9 asclmul1 ( ( 𝑊 ∈ AssAlg ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑁 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) = ( 𝐴 × ( 𝑁 𝑋 ) ) )
39 16 22 33 38 syl3anc ( 𝜑 → ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) = ( 𝐴 × ( 𝑁 𝑋 ) ) )
40 39 eqcomd ( 𝜑 → ( 𝐴 × ( 𝑁 𝑋 ) ) = ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) )
41 40 fveq2d ( 𝜑 → ( 𝑄 ‘ ( 𝐴 × ( 𝑁 𝑋 ) ) ) = ( 𝑄 ‘ ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) ) )
42 1 2 11 5 evl1rhm ( 𝑅 ∈ CRing → 𝑄 ∈ ( 𝑊 RingHom 𝑆 ) )
43 7 42 syl ( 𝜑𝑄 ∈ ( 𝑊 RingHom 𝑆 ) )
44 2 ply1lmod ( 𝑅 ∈ Ring → 𝑊 ∈ LMod )
45 26 44 syl ( 𝜑𝑊 ∈ LMod )
46 34 35 28 45 36 23 asclf ( 𝜑 → ( algSc ‘ 𝑊 ) : ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⟶ ( Base ‘ 𝑊 ) )
47 46 22 ffvelcdmd ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝑊 ) )
48 23 37 12 rhmmul ( ( 𝑄 ∈ ( 𝑊 RingHom 𝑆 ) ∧ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑁 𝑋 ) ∈ ( Base ‘ 𝑊 ) ) → ( 𝑄 ‘ ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) ) = ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ) ( 𝑄 ‘ ( 𝑁 𝑋 ) ) ) )
49 43 47 33 48 syl3anc ( 𝜑 → ( 𝑄 ‘ ( ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ( .r𝑊 ) ( 𝑁 𝑋 ) ) ) = ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ) ( 𝑄 ‘ ( 𝑁 𝑋 ) ) ) )
50 1 2 5 34 evl1sca ( ( 𝑅 ∈ CRing ∧ 𝐴𝐵 ) → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ) = ( 𝐵 × { 𝐴 } ) )
51 7 10 50 syl2anc ( 𝜑 → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ) = ( 𝐵 × { 𝐴 } ) )
52 1 2 3 4 5 6 7 8 evl1varpw ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( 𝑄𝑋 ) ) )
53 11 fveq2i ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ ( 𝑅s 𝐵 ) )
54 13 53 eqtri 𝑀 = ( mulGrp ‘ ( 𝑅s 𝐵 ) )
55 54 fveq2i ( .g𝑀 ) = ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) )
56 14 55 eqtri 𝐹 = ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) )
57 56 a1i ( 𝜑𝐹 = ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) )
58 57 eqcomd ( 𝜑 → ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) = 𝐹 )
59 58 oveqd ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( 𝑄𝑋 ) ) = ( 𝑁 𝐹 ( 𝑄𝑋 ) ) )
60 52 59 eqtrd ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 𝐹 ( 𝑄𝑋 ) ) )
61 51 60 oveq12d ( 𝜑 → ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝐴 ) ) ( 𝑄 ‘ ( 𝑁 𝑋 ) ) ) = ( ( 𝐵 × { 𝐴 } ) ( 𝑁 𝐹 ( 𝑄𝑋 ) ) ) )
62 41 49 61 3eqtrd ( 𝜑 → ( 𝑄 ‘ ( 𝐴 × ( 𝑁 𝑋 ) ) ) = ( ( 𝐵 × { 𝐴 } ) ( 𝑁 𝐹 ( 𝑄𝑋 ) ) ) )