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

Metamath Proof Explorer

Theorem evl1varpwval

Description: Value of a univariate polynomial evaluation mapping the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-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 )
evl1varpwval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
evl1varpwval.h ⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
evl1varpwval.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
Assertion evl1varpwval ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 𝐸 𝐶 ) )

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 evl1varpwval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
10 evl1varpwval.h ⊢ 𝐻 = ( mulGrp ‘ 𝑅 )
11 evl1varpwval.e ⊢ 𝐸 = ( .g ‘ 𝐻 )
12 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13 1 4 5 2 12 7 9 evl1vard ⊢ ( 𝜑 → ( 𝑋 ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐶 ) = 𝐶 ) )
14 3 fveq2i ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
15 6 14 eqtri ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
16 10 fveq2i ⊢ ( .g ‘ 𝐻 ) = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
17 11 16 eqtri ⊢ 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
18 1 2 5 12 7 9 13 15 17 8 evl1expd ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝑋 ) ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 𝐸 𝐶 ) ) )
19 18 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 𝐸 𝐶 ) )