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.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	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 )
6		evl1addd.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
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	⊢ ( 𝜑 → ( ( 𝑁 ∙ 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑁 ∙ 𝑀 ) ) ‘ 𝑌 ) = ( 𝑁 · 𝑉 ) ) )