# Metamath Proof Explorer

## Theorem evl1scvarpwval

Description: Value of a univariate polynomial evaluation mapping a multiple of an exponentiation of a variable to the multiple of the 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 ( 𝜑𝐴𝐵 )
evl1scvarpwval.c ( 𝜑𝐶𝐵 )
evl1scvarpwval.h 𝐻 = ( mulGrp ‘ 𝑅 )
evl1scvarpwval.e 𝐸 = ( .g𝐻 )
evl1scvarpwval.t · = ( .r𝑅 )
Assertion evl1scvarpwval ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 𝑋 ) ) ) ‘ 𝐶 ) = ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) )

### 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 evl1scvarpwval.c ( 𝜑𝐶𝐵 )
12 evl1scvarpwval.h 𝐻 = ( mulGrp ‘ 𝑅 )
13 evl1scvarpwval.e 𝐸 = ( .g𝐻 )
14 evl1scvarpwval.t · = ( .r𝑅 )
15 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
16 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
17 7 16 syl ( 𝜑𝑅 ∈ Ring )
18 2 ply1ring ( 𝑅 ∈ Ring → 𝑊 ∈ Ring )
19 17 18 syl ( 𝜑𝑊 ∈ Ring )
20 3 ringmgp ( 𝑊 ∈ Ring → 𝐺 ∈ Mnd )
21 19 20 syl ( 𝜑𝐺 ∈ Mnd )
22 4 2 15 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
23 17 22 syl ( 𝜑𝑋 ∈ ( Base ‘ 𝑊 ) )
24 3 15 mgpbas ( Base ‘ 𝑊 ) = ( Base ‘ 𝐺 )
25 24 6 mulgnn0cl ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0𝑋 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑁 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
26 21 8 23 25 syl3anc ( 𝜑 → ( 𝑁 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
27 1 2 3 4 5 6 7 8 11 12 13 evl1varpwval ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 𝐸 𝐶 ) )
28 26 27 jca ( 𝜑 → ( ( 𝑁 𝑋 ) ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝑄 ‘ ( 𝑁 𝑋 ) ) ‘ 𝐶 ) = ( 𝑁 𝐸 𝐶 ) ) )
29 1 2 5 15 7 11 28 10 9 14 evl1vsd ( 𝜑 → ( ( 𝐴 × ( 𝑁 𝑋 ) ) ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 𝑋 ) ) ) ‘ 𝐶 ) = ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) ) )
30 29 simprd ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 × ( 𝑁 𝑋 ) ) ) ‘ 𝐶 ) = ( 𝐴 · ( 𝑁 𝐸 𝐶 ) ) )