# Metamath Proof Explorer

## Theorem evl1vsd

Description: Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses evl1addd.q 𝑂 = ( eval1𝑅 )
evl1addd.p 𝑃 = ( Poly1𝑅 )
evl1addd.b 𝐵 = ( Base ‘ 𝑅 )
evl1addd.u 𝑈 = ( Base ‘ 𝑃 )
evl1addd.1 ( 𝜑𝑅 ∈ CRing )
evl1addd.3 ( 𝜑 → ( 𝑀𝑈 ∧ ( ( 𝑂𝑀 ) ‘ 𝑌 ) = 𝑉 ) )
evl1vsd.4 ( 𝜑𝑁𝐵 )
evl1vsd.s = ( ·𝑠𝑃 )
evl1vsd.t · = ( .r𝑅 )
Assertion evl1vsd ( 𝜑 → ( ( 𝑁 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑁 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 · 𝑉 ) ) )

### Proof

Step Hyp Ref Expression
1 evl1addd.q 𝑂 = ( eval1𝑅 )
2 evl1addd.p 𝑃 = ( Poly1𝑅 )
3 evl1addd.b 𝐵 = ( Base ‘ 𝑅 )
4 evl1addd.u 𝑈 = ( Base ‘ 𝑃 )
5 evl1addd.1 ( 𝜑𝑅 ∈ CRing )
7 evl1addd.3 ( 𝜑 → ( 𝑀𝑈 ∧ ( ( 𝑂𝑀 ) ‘ 𝑌 ) = 𝑉 ) )
8 evl1vsd.4 ( 𝜑𝑁𝐵 )
9 evl1vsd.s = ( ·𝑠𝑃 )
10 evl1vsd.t · = ( .r𝑅 )
11 eqid ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
12 1 2 3 11 4 5 8 6 evl1scad ( 𝜑 → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ) ‘ 𝑌 ) = 𝑁 ) )
13 eqid ( .r𝑃 ) = ( .r𝑃 )
14 1 2 3 4 5 6 12 7 13 10 evl1muld ( 𝜑 → ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ( .r𝑃 ) 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ( .r𝑃 ) 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 · 𝑉 ) ) )
15 2 ply1assa ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )
16 5 15 syl ( 𝜑𝑃 ∈ AssAlg )
17 2 ply1sca ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
18 5 17 syl ( 𝜑𝑅 = ( Scalar ‘ 𝑃 ) )
19 18 fveq2d ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
20 3 19 syl5eq ( 𝜑𝐵 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
21 8 20 eleqtrd ( 𝜑𝑁 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
22 7 simpld ( 𝜑𝑀𝑈 )
23 eqid ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
24 eqid ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
25 11 23 24 4 13 9 asclmul1 ( ( 𝑃 ∈ AssAlg ∧ 𝑁 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑀𝑈 ) → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ( .r𝑃 ) 𝑀 ) = ( 𝑁 𝑀 ) )
26 16 21 22 25 syl3anc ( 𝜑 → ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ( .r𝑃 ) 𝑀 ) = ( 𝑁 𝑀 ) )
27 26 eleq1d ( 𝜑 → ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ( .r𝑃 ) 𝑀 ) ∈ 𝑈 ↔ ( 𝑁 𝑀 ) ∈ 𝑈 ) )
28 26 fveq2d ( 𝜑 → ( 𝑂 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ( .r𝑃 ) 𝑀 ) ) = ( 𝑂 ‘ ( 𝑁 𝑀 ) ) )
29 28 fveq1d ( 𝜑 → ( ( 𝑂 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ( .r𝑃 ) 𝑀 ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑁 𝑀 ) ) ‘ 𝑌 ) )
30 29 eqeq1d ( 𝜑 → ( ( ( 𝑂 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ( .r𝑃 ) 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 · 𝑉 ) ↔ ( ( 𝑂 ‘ ( 𝑁 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 · 𝑉 ) ) )
31 27 30 anbi12d ( 𝜑 → ( ( ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ( .r𝑃 ) 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( ( ( algSc ‘ 𝑃 ) ‘ 𝑁 ) ( .r𝑃 ) 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 · 𝑉 ) ) ↔ ( ( 𝑁 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑁 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 · 𝑉 ) ) ) )
32 14 31 mpbid ( 𝜑 → ( ( 𝑁 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑁 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 · 𝑉 ) ) )