Theorem evls1subd

Description: Univariate polynomial evaluation of a difference of polynomials. (Contributed by Thierry Arnoux, 25-Apr-2025)

	Ref	Expression
Hypotheses	ressply1evl.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
	ressply1evl.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	ressply1evl.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
	ressply1evl.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	ressply1evl.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	evls1subd.1	⊢ 𝐷 = ( -g ‘ 𝑊 )
	evls1subd.2	⊢ − = ( -g ‘ 𝑆 )
	evls1subd.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evls1subd.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evls1subd.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
	evls1subd.n	⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
	evls1subd.y	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion	evls1subd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 𝐷 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) − ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ressply1evl.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2		ressply1evl.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
3		ressply1evl.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4		ressply1evl.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5		ressply1evl.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
6		evls1subd.1	⊢ 𝐷 = ( -g ‘ 𝑊 )
7		evls1subd.2	⊢ − = ( -g ‘ 𝑆 )
8		evls1subd.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
9		evls1subd.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10		evls1subd.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
11		evls1subd.n	⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
12		evls1subd.y	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
13	6	oveqi	⊢ ( 𝑀 𝐷 𝑁 ) = ( 𝑀 ( -g ‘ 𝑊 ) 𝑁 )
14		eqid	⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
15		eqid	⊢ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) = ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 )
16	14 4 3 5 9 15 10 11	ressply1sub	⊢ ( 𝜑 → ( 𝑀 ( -g ‘ 𝑊 ) 𝑁 ) = ( 𝑀 ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
17	13 16	eqtrid	⊢ ( 𝜑 → ( 𝑀 𝐷 𝑁 ) = ( 𝑀 ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
18	14 4 3 5	subrgply1	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝐵 ∈ ( SubRing ‘ ( Poly1 ‘ 𝑆 ) ) )
19		subrgsubg	⊢ ( 𝐵 ∈ ( SubRing ‘ ( Poly1 ‘ 𝑆 ) ) → 𝐵 ∈ ( SubGrp ‘ ( Poly1 ‘ 𝑆 ) ) )
20	9 18 19	3syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ ( Poly1 ‘ 𝑆 ) ) )
21		eqid	⊢ ( -g ‘ ( Poly1 ‘ 𝑆 ) ) = ( -g ‘ ( Poly1 ‘ 𝑆 ) )
22		eqid	⊢ ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) = ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) )
23	21 15 22	subgsub	⊢ ( ( 𝐵 ∈ ( SubGrp ‘ ( Poly1 ‘ 𝑆 ) ) ∧ 𝑀 ∈ 𝐵 ∧ 𝑁 ∈ 𝐵 ) → ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) = ( 𝑀 ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
24	20 10 11 23	syl3anc	⊢ ( 𝜑 → ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) = ( 𝑀 ( -g ‘ ( ( Poly1 ‘ 𝑆 ) ↾s 𝐵 ) ) 𝑁 ) )
25	17 24	eqtr4d	⊢ ( 𝜑 → ( 𝑀 𝐷 𝑁 ) = ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) )
26	25	fveq2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 𝐷 𝑁 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) )
27	26	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 𝐷 𝑁 ) ) ‘ 𝐶 ) = ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) )
28		eqid	⊢ ( eval1 ‘ 𝑆 ) = ( eval1 ‘ 𝑆 )
29	1 2 3 4 5 28 8 9	ressply1evl	⊢ ( 𝜑 → 𝑄 = ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) )
30	29	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑀 𝐷 𝑁 ) ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ ( 𝑀 𝐷 𝑁 ) ) )
31	4	subrgring	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
32	3	ply1ring	⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ Ring )
33	9 31 32	3syl	⊢ ( 𝜑 → 𝑊 ∈ Ring )
34	33	ringgrpd	⊢ ( 𝜑 → 𝑊 ∈ Grp )
35	5 6	grpsubcl	⊢ ( ( 𝑊 ∈ Grp ∧ 𝑀 ∈ 𝐵 ∧ 𝑁 ∈ 𝐵 ) → ( 𝑀 𝐷 𝑁 ) ∈ 𝐵 )
36	34 10 11 35	syl3anc	⊢ ( 𝜑 → ( 𝑀 𝐷 𝑁 ) ∈ 𝐵 )
37	36	fvresd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ ( 𝑀 𝐷 𝑁 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 𝐷 𝑁 ) ) )
38	30 37	eqtr2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 𝐷 𝑁 ) ) = ( 𝑄 ‘ ( 𝑀 𝐷 𝑁 ) ) )
39	38	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 𝐷 𝑁 ) ) ‘ 𝐶 ) = ( ( 𝑄 ‘ ( 𝑀 𝐷 𝑁 ) ) ‘ 𝐶 ) )
40		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
41		eqid	⊢ ( PwSer1 ‘ 𝑈 ) = ( PwSer1 ‘ 𝑈 )
42		eqid	⊢ ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑈 ) )
43	14 4 3 5 9 41 42 40	ressply1bas2	⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) )
44		inss2	⊢ ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) )
45	43 44	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
46	45 10	sseldd	⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
47	29	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑀 ) )
48	10	fvresd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑀 ) = ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) )
49	47 48	eqtr2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) = ( 𝑄 ‘ 𝑀 ) )
50	49	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) )
51	46 50	jca	⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑀 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) ) )
52	45 11	sseldd	⊢ ( 𝜑 → 𝑁 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
53	29	fveq1d	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) = ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑁 ) )
54	11	fvresd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ↾ 𝐵 ) ‘ 𝑁 ) = ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) )
55	53 54	eqtr2d	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) = ( 𝑄 ‘ 𝑁 ) )
56	55	fveq1d	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) )
57	52 56	jca	⊢ ( 𝜑 → ( 𝑁 ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ 𝑁 ) ‘ 𝐶 ) = ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )
58	28 14 2 40 8 12 51 57 21 7	evl1subd	⊢ ( 𝜑 → ( ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) − ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) ) )
59	58	simprd	⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝑆 ) ‘ ( 𝑀 ( -g ‘ ( Poly1 ‘ 𝑆 ) ) 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) − ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )
60	27 39 59	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 𝐷 𝑁 ) ) ‘ 𝐶 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) − ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐶 ) ) )