Metamath Proof Explorer

Theorem evl1varpw

Description: Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd , the proof is shorter using evls1varpw instead of proving it directly. (Contributed by AV, 15-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 )
Assertion evl1varpw ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( 𝑄𝑋 ) ) )

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 1 5 evl1fval1 𝑄 = ( 𝑅 evalSub1 𝐵 )
10 9 a1i ( 𝜑𝑄 = ( 𝑅 evalSub1 𝐵 ) )
11 2 fveq2i ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ ( Poly1𝑅 ) )
12 3 11 eqtri 𝐺 = ( mulGrp ‘ ( Poly1𝑅 ) )
13 12 fveq2i ( .g𝐺 ) = ( .g ‘ ( mulGrp ‘ ( Poly1𝑅 ) ) )
14 6 13 eqtri = ( .g ‘ ( mulGrp ‘ ( Poly1𝑅 ) ) )
15 5 ressid ( 𝑅 ∈ CRing → ( 𝑅s 𝐵 ) = 𝑅 )
16 7 15 syl ( 𝜑 → ( 𝑅s 𝐵 ) = 𝑅 )
17 16 eqcomd ( 𝜑𝑅 = ( 𝑅s 𝐵 ) )
18 17 fveq2d ( 𝜑 → ( Poly1𝑅 ) = ( Poly1 ‘ ( 𝑅s 𝐵 ) ) )
19 18 fveq2d ( 𝜑 → ( mulGrp ‘ ( Poly1𝑅 ) ) = ( mulGrp ‘ ( Poly1 ‘ ( 𝑅s 𝐵 ) ) ) )
20 19 fveq2d ( 𝜑 → ( .g ‘ ( mulGrp ‘ ( Poly1𝑅 ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅s 𝐵 ) ) ) ) )
21 14 20 syl5eq ( 𝜑 = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅s 𝐵 ) ) ) ) )
22 eqidd ( 𝜑𝑁 = 𝑁 )
23 17 fveq2d ( 𝜑 → ( var1𝑅 ) = ( var1 ‘ ( 𝑅s 𝐵 ) ) )
24 4 23 syl5eq ( 𝜑𝑋 = ( var1 ‘ ( 𝑅s 𝐵 ) ) )
25 21 22 24 oveq123d ( 𝜑 → ( 𝑁 𝑋 ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅s 𝐵 ) ) ) ) ( var1 ‘ ( 𝑅s 𝐵 ) ) ) )
26 10 25 fveq12d ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( ( 𝑅 evalSub1 𝐵 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅s 𝐵 ) ) ) ) ( var1 ‘ ( 𝑅s 𝐵 ) ) ) ) )
27 eqid ( 𝑅 evalSub1 𝐵 ) = ( 𝑅 evalSub1 𝐵 )
28 eqid ( 𝑅s 𝐵 ) = ( 𝑅s 𝐵 )
29 eqid ( Poly1 ‘ ( 𝑅s 𝐵 ) ) = ( Poly1 ‘ ( 𝑅s 𝐵 ) )
30 eqid ( mulGrp ‘ ( Poly1 ‘ ( 𝑅s 𝐵 ) ) ) = ( mulGrp ‘ ( Poly1 ‘ ( 𝑅s 𝐵 ) ) )
31 eqid ( var1 ‘ ( 𝑅s 𝐵 ) ) = ( var1 ‘ ( 𝑅s 𝐵 ) )
32 eqid ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅s 𝐵 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅s 𝐵 ) ) ) )
33 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
34 5 subrgid ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
35 7 33 34 3syl ( 𝜑𝐵 ∈ ( SubRing ‘ 𝑅 ) )
36 27 28 29 30 31 5 32 7 35 8 evls1varpw ( 𝜑 → ( ( 𝑅 evalSub1 𝐵 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅s 𝐵 ) ) ) ) ( var1 ‘ ( 𝑅s 𝐵 ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( ( 𝑅 evalSub1 𝐵 ) ‘ ( var1 ‘ ( 𝑅s 𝐵 ) ) ) ) )
37 9 eqcomi ( 𝑅 evalSub1 𝐵 ) = 𝑄
38 37 a1i ( 𝜑 → ( 𝑅 evalSub1 𝐵 ) = 𝑄 )
39 24 eqcomd ( 𝜑 → ( var1 ‘ ( 𝑅s 𝐵 ) ) = 𝑋 )
40 38 39 fveq12d ( 𝜑 → ( ( 𝑅 evalSub1 𝐵 ) ‘ ( var1 ‘ ( 𝑅s 𝐵 ) ) ) = ( 𝑄𝑋 ) )
41 40 oveq2d ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( ( 𝑅 evalSub1 𝐵 ) ‘ ( var1 ‘ ( 𝑅s 𝐵 ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( 𝑄𝑋 ) ) )
42 26 36 41 3eqtrd ( 𝜑 → ( 𝑄 ‘ ( 𝑁 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅s 𝐵 ) ) ) ( 𝑄𝑋 ) ) )