# Metamath Proof Explorer

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.3 ( 𝜑 → ( 𝑀𝑈 ∧ ( ( 𝑂𝑀 ) ‘ 𝑌 ) = 𝑉 ) )
evl1addd.4 ( 𝜑 → ( 𝑁𝑈 ∧ ( ( 𝑂𝑁 ) ‘ 𝑌 ) = 𝑊 ) )
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 )
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 ( 𝜑 → ( ( 𝑀 𝑁 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑀 𝑁 ) ) ‘ 𝑌 ) = ( 𝑉 + 𝑊 ) ) )