Theorem evls1addd

Description: Univariate polynomial evaluation of a sum of polynomials. (Contributed by Thierry Arnoux, 8-Feb-2025)

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

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