Theorem evls1muld

Description: Univariate polynomial evaluation of a product of polynomials. (Contributed by Thierry Arnoux, 24-Jan-2025)

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

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		evls1muld.1	⊢ × = ( .r ‘ 𝑊 )
7		evls1muld.2	⊢ · = ( .r ‘ 𝑆 )
8		evls1muld.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
9		evls1muld.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10		evls1muld.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
11		evls1muld.n	⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
12		evls1muld.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
13		id	⊢ ( 𝜑 → 𝜑 )
14		eqid	⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
15		eqid	⊢ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) = ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 )
16	14 4 3 5 9 15	ressply1mul	⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ 𝐵 ∧ 𝑁 ∈ 𝐵 ) ) → ( 𝑀 ( .r ‘ 𝑊 ) 𝑁 ) = ( 𝑀 ( .r ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
17	13 10 11 16	syl12anc	⊢ ( 𝜑 → ( 𝑀 ( .r ‘ 𝑊 ) 𝑁 ) = ( 𝑀 ( .r ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
18	6	oveqi	⊢ ( 𝑀 × 𝑁 ) = ( 𝑀 ( .r ‘ 𝑊 ) 𝑁 )
19	5	fvexi	⊢ 𝐵 ∈ V
20		eqid	⊢ ( .r ‘ ( Poly1 ‘ 𝑆 ) ) = ( .r ‘ ( Poly1 ‘ 𝑆 ) )
21	15 20	ressmulr	⊢ ( 𝐵 ∈ V → ( .r ‘ ( Poly1 ‘ 𝑆 ) ) = ( .r ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) )
22	19 21	ax-mp	⊢ ( .r ‘ ( Poly1 ‘ 𝑆 ) ) = ( .r ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) )
23	22	oveqi	⊢ ( 𝑀 ( .r ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) = ( 𝑀 ( .r ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 )
24	17 18 23	3eqtr4g	⊢ ( 𝜑 → ( 𝑀 × 𝑁 ) = ( 𝑀 ( .r ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) )
25	24	fveq2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 × 𝑁 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( .r ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) )
26	25	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 × 𝑁 ) ) ‘ 𝐶 ) = ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( .r ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) )
27		eqid	⊢ ( eval1 ‘ 𝑆 ) = ( eval1 ‘ 𝑆 )
28	1 2 3 4 5 27 8 9	ressply1evl	⊢ ( 𝜑 → 𝑄 = ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) )
29	28	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑀 × 𝑁 ) ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ ( 𝑀 × 𝑁 ) ) )
30	4	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
31	3	ply1ring	⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ Ring )
32	9 30 31	3syl	⊢ ( 𝜑 → 𝑊 ∈ Ring )
33	5 6 32 10 11	ringcld	⊢ ( 𝜑 → ( 𝑀 × 𝑁 ) ∈ 𝐵 )
34	33	fvresd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ ( 𝑀 × 𝑁 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 × 𝑁 ) ) )
35	29 34	eqtr2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 × 𝑁 ) ) = ( 𝑄 ‘ ( 𝑀 × 𝑁 ) ) )
36	35	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 × 𝑁 ) ) ‘ 𝐶 ) = ( ( 𝑄 ‘ ( 𝑀 × 𝑁 ) ) ‘ 𝐶 ) )
37		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
38		eqid	⊢ ( PwSer1 ‘ 𝑈 ) = ( PwSer1 ‘ 𝑈 )
39		eqid	⊢ ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑈 ) )
40	14 4 3 5 9 38 39 37	ressply1bas2	⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) )
41		inss2	⊢ ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) )
42	40 41	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
43	42 10	sseldd	⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
44	28	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑀 ) )
45	10	fvresd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑀 ) = ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) )
46	44 45	eqtr2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) = ( 𝑄 ‘ 𝑀 ) )
47	46	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) )
48	43 47	jca	⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) ) )
49	42 11	sseldd	⊢ ( 𝜑 → 𝑁 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
50	28	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑁 ) )
51	11	fvresd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑁 ) = ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) )
52	50 51	eqtr2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) = ( 𝑄 ‘ 𝑁 ) )
53	52	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) )
54	49 53	jca	⊢ ( 𝜑 → ( 𝑁 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )
55	27 14 2 37 8 12 48 54 20 7	evl1muld	⊢ ( 𝜑 → ( ( 𝑀 ( .r ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( .r ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
56	55	simprd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( .r ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )
57	26 36 56	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 × 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) · ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )