Theorem evls1vsca

Description: Univariate polynomial evaluation of a scalar product of polynomials. (Contributed by Thierry Arnoux, 25-Feb-2025)

	Ref	Expression
Hypotheses	ressply1evl2.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
	ressply1evl2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	ressply1evl2.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
	ressply1evl2.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	ressply1evl2.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	evls1vsca.1	⊢ × = ( ·𝑠 ‘ 𝑊 )
	evls1vsca.2	⊢ · = ( .r ‘ 𝑆 )
	evls1vsca.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evls1vsca.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evls1vsca.m	⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
	evls1vsca.n	⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
	evls1vsca.y	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion	evls1vsca	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 × 𝑁 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ressply1evl2.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2		ressply1evl2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
3		ressply1evl2.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4		ressply1evl2.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5		ressply1evl2.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
6		evls1vsca.1	⊢ × = ( ·𝑠 ‘ 𝑊 )
7		evls1vsca.2	⊢ · = ( .r ‘ 𝑆 )
8		evls1vsca.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
9		evls1vsca.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10		evls1vsca.m	⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
11		evls1vsca.n	⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
12		evls1vsca.y	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
13		id	⊢ ( 𝜑 → 𝜑 )
14		eqid	⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
15		eqid	⊢ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) = ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 )
16	14 4 3 5 9 15	ressply1vsca	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑅 ∧ 𝑁 ∈ 𝐵 ) ) → ( 𝐴 ( ·𝑠 ‘ 𝑊 ) 𝑁 ) = ( 𝐴 ( ·𝑠 ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
17	13 10 11 16	syl12anc	⊢ ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ 𝑊 ) 𝑁 ) = ( 𝐴 ( ·𝑠 ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
18	6	oveqi	⊢ ( 𝐴 × 𝑁 ) = ( 𝐴 ( ·𝑠 ‘ 𝑊 ) 𝑁 )
19	5	fvexi	⊢ 𝐵 ∈ V
20		eqid	⊢ ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) = ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) )
21	15 20	ressvsca	⊢ ( 𝐵 ∈ V → ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) = ( ·𝑠 ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) )
22	19 21	ax-mp	⊢ ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) = ( ·𝑠 ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) )
23	22	oveqi	⊢ ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) = ( 𝐴 ( ·𝑠 ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 )
24	17 18 23	3eqtr4g	⊢ ( 𝜑 → ( 𝐴 × 𝑁 ) = ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) )
25	24	fveq2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 × 𝑁 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) )
26	25	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 × 𝑁 ) ) ‘ 𝐶 ) = ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) )
27		eqid	⊢ ( eval1 ‘ 𝑆 ) = ( eval1 ‘ 𝑆 )
28	1 2 3 4 5 27 8 9	ressply1evl	⊢ ( 𝜑 → 𝑄 = ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) )
29	28	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 × 𝑁 ) ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ ( 𝐴 × 𝑁 ) ) )
30	4	subrgcrng	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
31	8 9 30	syl2anc	⊢ ( 𝜑 → 𝑈 ∈ CRing )
32		crngring	⊢ ( 𝑈 ∈ CRing → 𝑈 ∈ Ring )
33	3	ply1lmod	⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ LMod )
34	31 32 33	3syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
35	2	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
36	9 35	syl	⊢ ( 𝜑 → 𝑅 ⊆ 𝐾 )
37	4 2	ressbas2	⊢ ( 𝑅 ⊆ 𝐾 → 𝑅 = ( Base ‘ 𝑈 ) )
38	36 37	syl	⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
39	4	ovexi	⊢ 𝑈 ∈ V
40	3	ply1sca	⊢ ( 𝑈 ∈ V → 𝑈 = ( Scalar ‘ 𝑊 ) )
41	39 40	mp1i	⊢ ( 𝜑 → 𝑈 = ( Scalar ‘ 𝑊 ) )
42	41	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
43	38 42	eqtrd	⊢ ( 𝜑 → 𝑅 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
44	10 43	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
45		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
46		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
47	5 45 6 46	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑁 ∈ 𝐵 ) → ( 𝐴 × 𝑁 ) ∈ 𝐵 )
48	34 44 11 47	syl3anc	⊢ ( 𝜑 → ( 𝐴 × 𝑁 ) ∈ 𝐵 )
49	48	fvresd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ ( 𝐴 × 𝑁 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 × 𝑁 ) ) )
50	29 49	eqtr2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 × 𝑁 ) ) = ( 𝑄 ‘ ( 𝐴 × 𝑁 ) ) )
51	50	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 × 𝑁 ) ) ‘ 𝐶 ) = ( ( 𝑄 ‘ ( 𝐴 × 𝑁 ) ) ‘ 𝐶 ) )
52		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
53		eqid	⊢ ( PwSer1 ‘ 𝑈 ) = ( PwSer1 ‘ 𝑈 )
54		eqid	⊢ ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑈 ) )
55	14 4 3 5 9 53 54 52	ressply1bas2	⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) )
56		inss2	⊢ ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) )
57	55 56	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
58	57 11	sseldd	⊢ ( 𝜑 → 𝑁 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
59	28	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑁 ) )
60	11	fvresd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑁 ) = ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) )
61	59 60	eqtr2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) = ( 𝑄 ‘ 𝑁 ) )
62	61	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) )
63	58 62	jca	⊢ ( 𝜑 → ( 𝑁 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )
64	36 10	sseldd	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
65	27 14 2 52 8 12 63 64 20 7	evl1vsd	⊢ ( 𝜑 → ( ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
66	65	simprd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝐴 ( ·𝑠 ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )
67	26 51 66	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 × 𝑁 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )