# Metamath Proof Explorer

Description: Polynomial evaluation builder for addition of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses evl1addd.q ${⊢}{O}={\mathrm{eval}}_{1}\left({R}\right)$
evl1addd.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
evl1addd.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
evl1addd.u ${⊢}{U}={\mathrm{Base}}_{{P}}$
evl1addd.1 ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
evl1addd.2 ${⊢}{\phi }\to {Y}\in {B}$
evl1addd.3 ${⊢}{\phi }\to \left({M}\in {U}\wedge {O}\left({M}\right)\left({Y}\right)={V}\right)$
evl1addd.4 ${⊢}{\phi }\to \left({N}\in {U}\wedge {O}\left({N}\right)\left({Y}\right)={W}\right)$

### Proof

Step Hyp Ref Expression
1 evl1addd.q ${⊢}{O}={\mathrm{eval}}_{1}\left({R}\right)$
2 evl1addd.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
3 evl1addd.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
4 evl1addd.u ${⊢}{U}={\mathrm{Base}}_{{P}}$
5 evl1addd.1 ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
6 evl1addd.2 ${⊢}{\phi }\to {Y}\in {B}$
7 evl1addd.3 ${⊢}{\phi }\to \left({M}\in {U}\wedge {O}\left({M}\right)\left({Y}\right)={V}\right)$
8 evl1addd.4 ${⊢}{\phi }\to \left({N}\in {U}\wedge {O}\left({N}\right)\left({Y}\right)={W}\right)$
11 eqid ${⊢}{R}{↑}_{𝑠}{B}={R}{↑}_{𝑠}{B}$
12 1 2 11 3 evl1rhm ${⊢}{R}\in \mathrm{CRing}\to {O}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}{B}\right)\right)$
13 5 12 syl ${⊢}{\phi }\to {O}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}{B}\right)\right)$
14 rhmghm ${⊢}{O}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}{B}\right)\right)\to {O}\in \left({P}\mathrm{GrpHom}\left({R}{↑}_{𝑠}{B}\right)\right)$
15 13 14 syl ${⊢}{\phi }\to {O}\in \left({P}\mathrm{GrpHom}\left({R}{↑}_{𝑠}{B}\right)\right)$
16 ghmgrp1 ${⊢}{O}\in \left({P}\mathrm{GrpHom}\left({R}{↑}_{𝑠}{B}\right)\right)\to {P}\in \mathrm{Grp}$
17 15 16 syl ${⊢}{\phi }\to {P}\in \mathrm{Grp}$
18 7 simpld ${⊢}{\phi }\to {M}\in {U}$
19 8 simpld ${⊢}{\phi }\to {N}\in {U}$
20 4 9 grpcl
21 17 18 19 20 syl3anc
22 eqid ${⊢}{+}_{\left({R}{↑}_{𝑠}{B}\right)}={+}_{\left({R}{↑}_{𝑠}{B}\right)}$
23 4 9 22 ghmlin
24 15 18 19 23 syl3anc
25 eqid ${⊢}{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
26 3 fvexi ${⊢}{B}\in \mathrm{V}$
27 26 a1i ${⊢}{\phi }\to {B}\in \mathrm{V}$
28 4 25 rhmf ${⊢}{O}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}{B}\right)\right)\to {O}:{U}⟶{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
29 13 28 syl ${⊢}{\phi }\to {O}:{U}⟶{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
30 29 18 ffvelrnd ${⊢}{\phi }\to {O}\left({M}\right)\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
31 29 19 ffvelrnd ${⊢}{\phi }\to {O}\left({N}\right)\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
32 11 25 5 27 30 31 10 22 pwsplusgval
33 24 32 eqtrd
34 33 fveq1d
35 11 3 25 5 27 30 pwselbas ${⊢}{\phi }\to {O}\left({M}\right):{B}⟶{B}$
36 35 ffnd ${⊢}{\phi }\to {O}\left({M}\right)Fn{B}$
37 11 3 25 5 27 31 pwselbas ${⊢}{\phi }\to {O}\left({N}\right):{B}⟶{B}$
38 37 ffnd ${⊢}{\phi }\to {O}\left({N}\right)Fn{B}$
39 fnfvof
40 36 38 27 6 39 syl22anc
41 7 simprd ${⊢}{\phi }\to {O}\left({M}\right)\left({Y}\right)={V}$
42 8 simprd ${⊢}{\phi }\to {O}\left({N}\right)\left({Y}\right)={W}$
43 41 42 oveq12d
44 34 40 43 3eqtrd
45 21 44 jca