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

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 eqtrid ⊢ ( 𝜑 → ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) )
22 eqidd ⊢ ( 𝜑 → 𝑁 = 𝑁 )
23 17 fveq2d ⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) = ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) )
24 4 23 eqtrid ⊢ ( 𝜑 → 𝑋 = ( 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 𝐵 ) ) ) ( 𝑄 ‘ 𝑋 ) ) )