# Metamath Proof Explorer

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

Ref Expression
`|- O = ( eval1 ` R )`
`|- P = ( Poly1 ` R )`
`|- B = ( Base ` R )`
`|- U = ( Base ` P )`
`|- ( ph -> R e. CRing )`
`|- ( ph -> Y e. B )`
`|- ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )`
`|- ( ph -> ( N e. U /\ ( ( O ` N ) ` Y ) = W ) )`
`|- .+b = ( +g ` P )`
`|- .+ = ( +g ` R )`
`|- ( ph -> ( ( M .+b N ) e. U /\ ( ( O ` ( M .+b N ) ) ` Y ) = ( V .+ W ) ) )`

### Proof

Step Hyp Ref Expression
` |-  O = ( eval1 ` R )`
` |-  P = ( Poly1 ` R )`
` |-  B = ( Base ` R )`
` |-  U = ( Base ` P )`
` |-  ( ph -> R e. CRing )`
` |-  ( ph -> Y e. B )`
` |-  ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )`
` |-  ( ph -> ( N e. U /\ ( ( O ` N ) ` Y ) = W ) )`
` |-  .+b = ( +g ` P )`
` |-  .+ = ( +g ` R )`
11 eqid
` |-  ( R ^s B ) = ( R ^s B )`
12 1 2 11 3 evl1rhm
` |-  ( R e. CRing -> O e. ( P RingHom ( R ^s B ) ) )`
13 5 12 syl
` |-  ( ph -> O e. ( P RingHom ( R ^s B ) ) )`
14 rhmghm
` |-  ( O e. ( P RingHom ( R ^s B ) ) -> O e. ( P GrpHom ( R ^s B ) ) )`
15 13 14 syl
` |-  ( ph -> O e. ( P GrpHom ( R ^s B ) ) )`
16 ghmgrp1
` |-  ( O e. ( P GrpHom ( R ^s B ) ) -> P e. Grp )`
17 15 16 syl
` |-  ( ph -> P e. Grp )`
18 7 simpld
` |-  ( ph -> M e. U )`
19 8 simpld
` |-  ( ph -> N e. U )`
20 4 9 grpcl
` |-  ( ( P e. Grp /\ M e. U /\ N e. U ) -> ( M .+b N ) e. U )`
21 17 18 19 20 syl3anc
` |-  ( ph -> ( M .+b N ) e. U )`
22 eqid
` |-  ( +g ` ( R ^s B ) ) = ( +g ` ( R ^s B ) )`
23 4 9 22 ghmlin
` |-  ( ( O e. ( P GrpHom ( R ^s B ) ) /\ M e. U /\ N e. U ) -> ( O ` ( M .+b N ) ) = ( ( O ` M ) ( +g ` ( R ^s B ) ) ( O ` N ) ) )`
24 15 18 19 23 syl3anc
` |-  ( ph -> ( O ` ( M .+b N ) ) = ( ( O ` M ) ( +g ` ( R ^s B ) ) ( O ` N ) ) )`
25 eqid
` |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )`
26 3 fvexi
` |-  B e. _V`
27 26 a1i
` |-  ( ph -> B e. _V )`
28 4 25 rhmf
` |-  ( O e. ( P RingHom ( R ^s B ) ) -> O : U --> ( Base ` ( R ^s B ) ) )`
29 13 28 syl
` |-  ( ph -> O : U --> ( Base ` ( R ^s B ) ) )`
30 29 18 ffvelrnd
` |-  ( ph -> ( O ` M ) e. ( Base ` ( R ^s B ) ) )`
31 29 19 ffvelrnd
` |-  ( ph -> ( O ` N ) e. ( Base ` ( R ^s B ) ) )`
32 11 25 5 27 30 31 10 22 pwsplusgval
` |-  ( ph -> ( ( O ` M ) ( +g ` ( R ^s B ) ) ( O ` N ) ) = ( ( O ` M ) oF .+ ( O ` N ) ) )`
33 24 32 eqtrd
` |-  ( ph -> ( O ` ( M .+b N ) ) = ( ( O ` M ) oF .+ ( O ` N ) ) )`
34 33 fveq1d
` |-  ( ph -> ( ( O ` ( M .+b N ) ) ` Y ) = ( ( ( O ` M ) oF .+ ( O ` N ) ) ` Y ) )`
35 11 3 25 5 27 30 pwselbas
` |-  ( ph -> ( O ` M ) : B --> B )`
36 35 ffnd
` |-  ( ph -> ( O ` M ) Fn B )`
37 11 3 25 5 27 31 pwselbas
` |-  ( ph -> ( O ` N ) : B --> B )`
38 37 ffnd
` |-  ( ph -> ( O ` N ) Fn B )`
39 fnfvof
` |-  ( ( ( ( O ` M ) Fn B /\ ( O ` N ) Fn B ) /\ ( B e. _V /\ Y e. B ) ) -> ( ( ( O ` M ) oF .+ ( O ` N ) ) ` Y ) = ( ( ( O ` M ) ` Y ) .+ ( ( O ` N ) ` Y ) ) )`
40 36 38 27 6 39 syl22anc
` |-  ( ph -> ( ( ( O ` M ) oF .+ ( O ` N ) ) ` Y ) = ( ( ( O ` M ) ` Y ) .+ ( ( O ` N ) ` Y ) ) )`
41 7 simprd
` |-  ( ph -> ( ( O ` M ) ` Y ) = V )`
42 8 simprd
` |-  ( ph -> ( ( O ` N ) ` Y ) = W )`
43 41 42 oveq12d
` |-  ( ph -> ( ( ( O ` M ) ` Y ) .+ ( ( O ` N ) ` Y ) ) = ( V .+ W ) )`
44 34 40 43 3eqtrd
` |-  ( ph -> ( ( O ` ( M .+b N ) ) ` Y ) = ( V .+ W ) )`
45 21 44 jca
` |-  ( ph -> ( ( M .+b N ) e. U /\ ( ( O ` ( M .+b N ) ) ` Y ) = ( V .+ W ) ) )`