Theorem evl1addd

Description: Polynomial evaluation builder for addition 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	⊢ ( 𝜑 → ( 𝑀 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = 𝑉 ) )
	evl1addd.4	⊢ ( 𝜑 → ( 𝑁 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) = 𝑊 ) )
	evl1addd.g	⊢ ✚ = ( +g ‘ 𝑃 )
	evl1addd.a	⊢ + = ( +g ‘ 𝑅 )
Assertion	evl1addd	⊢ ( 𝜑 → ( ( 𝑀 ✚ 𝑁 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝑌 ) = ( 𝑉 + 𝑊 ) ) )

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		evl1addd.4	⊢ ( 𝜑 → ( 𝑁 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) = 𝑊 ) )
9		evl1addd.g	⊢ ✚ = ( +g ‘ 𝑃 )
10		evl1addd.a	⊢ + = ( +g ‘ 𝑅 )
11		eqid	⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
12	1 2 11 3	evl1rhm	⊢ ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) )
13	5 12	syl	⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) )
14		rhmghm	⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) → 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐵 ) ) )
15	13 14	syl	⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐵 ) ) )
16		ghmgrp1	⊢ ( 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐵 ) ) → 𝑃 ∈ Grp )
17	15 16	syl	⊢ ( 𝜑 → 𝑃 ∈ Grp )
18	7	simpld	⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
19	8	simpld	⊢ ( 𝜑 → 𝑁 ∈ 𝑈 )
20	4 9	grpcl	⊢ ( ( 𝑃 ∈ Grp ∧ 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑈 ) → ( 𝑀 ✚ 𝑁 ) ∈ 𝑈 )
21	17 18 19 20	syl3anc	⊢ ( 𝜑 → ( 𝑀 ✚ 𝑁 ) ∈ 𝑈 )
22		eqid	⊢ ( +g ‘ ( 𝑅 ↑s 𝐵 ) ) = ( +g ‘ ( 𝑅 ↑s 𝐵 ) )
23	4 9 22	ghmlin	⊢ ( ( 𝑂 ∈ ( 𝑃 GrpHom ( 𝑅 ↑s 𝐵 ) ) ∧ 𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑈 ) → ( 𝑂 ‘ ( 𝑀 ✚ 𝑁 ) ) = ( ( 𝑂 ‘ 𝑀 ) ( +g ‘ ( 𝑅 ↑s 𝐵 ) ) ( 𝑂 ‘ 𝑁 ) ) )
24	15 18 19 23	syl3anc	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑀 ✚ 𝑁 ) ) = ( ( 𝑂 ‘ 𝑀 ) ( +g ‘ ( 𝑅 ↑s 𝐵 ) ) ( 𝑂 ‘ 𝑁 ) ) )
25		eqid	⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
26	3	fvexi	⊢ 𝐵 ∈ V
27	26	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
28	4 25	rhmf	⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
29	13 28	syl	⊢ ( 𝜑 → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
30	29 18	ffvelrnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
31	29 19	ffvelrnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑁 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
32	11 25 5 27 30 31 10 22	pwsplusgval	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ( +g ‘ ( 𝑅 ↑s 𝐵 ) ) ( 𝑂 ‘ 𝑁 ) ) = ( ( 𝑂 ‘ 𝑀 ) ∘f + ( 𝑂 ‘ 𝑁 ) ) )
33	24 32	eqtrd	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑀 ✚ 𝑁 ) ) = ( ( 𝑂 ‘ 𝑀 ) ∘f + ( 𝑂 ‘ 𝑁 ) ) )
34	33	fveq1d	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ 𝑀 ) ∘f + ( 𝑂 ‘ 𝑁 ) ) ‘ 𝑌 ) )
35	11 3 25 5 27 30	pwselbas	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) : 𝐵 ⟶ 𝐵 )
36	35	ffnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) Fn 𝐵 )
37	11 3 25 5 27 31	pwselbas	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑁 ) : 𝐵 ⟶ 𝐵 )
38	37	ffnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑁 ) Fn 𝐵 )
39		fnfvof	⊢ ( ( ( ( 𝑂 ‘ 𝑀 ) Fn 𝐵 ∧ ( 𝑂 ‘ 𝑁 ) Fn 𝐵 ) ∧ ( 𝐵 ∈ V ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑂 ‘ 𝑀 ) ∘f + ( 𝑂 ‘ 𝑁 ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) + ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) ) )
40	36 38 27 6 39	syl22anc	⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝑀 ) ∘f + ( 𝑂 ‘ 𝑁 ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) + ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) ) )
41	7	simprd	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = 𝑉 )
42	8	simprd	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) = 𝑊 )
43	41 42	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) + ( ( 𝑂 ‘ 𝑁 ) ‘ 𝑌 ) ) = ( 𝑉 + 𝑊 ) )
44	34 40 43	3eqtrd	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝑌 ) = ( 𝑉 + 𝑊 ) )
45	21 44	jca	⊢ ( 𝜑 → ( ( 𝑀 ✚ 𝑁 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝑌 ) = ( 𝑉 + 𝑊 ) ) )