This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 × ( 𝑁 ↑ 𝑋 ) ) ) = ( ( 𝐵 × { 𝐴 } ) ∙ ( 𝑁 𝐹 ( 𝑄 ‘ 𝑋 ) ) ) )