# Metamath Proof Explorer

## Theorem evl1subd

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

Ref Expression
Hypotheses evl1addd.q
`|- O = ( eval1 ` R )`
evl1addd.p
`|- P = ( Poly1 ` R )`
evl1addd.b
`|- B = ( Base ` R )`
evl1addd.u
`|- U = ( Base ` P )`
evl1addd.1
`|- ( ph -> R e. CRing )`
evl1addd.2
`|- ( ph -> Y e. B )`
evl1addd.3
`|- ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )`
evl1addd.4
`|- ( ph -> ( N e. U /\ ( ( O ` N ) ` Y ) = W ) )`
evl1subd.s
`|- .- = ( -g ` P )`
evl1subd.d
`|- D = ( -g ` R )`
Assertion evl1subd
`|- ( ph -> ( ( M .- N ) e. U /\ ( ( O ` ( M .- N ) ) ` Y ) = ( V D W ) ) )`

### Proof

Step Hyp Ref Expression
1 evl1addd.q
` |-  O = ( eval1 ` R )`
2 evl1addd.p
` |-  P = ( Poly1 ` R )`
3 evl1addd.b
` |-  B = ( Base ` R )`
4 evl1addd.u
` |-  U = ( Base ` P )`
5 evl1addd.1
` |-  ( ph -> R e. CRing )`
6 evl1addd.2
` |-  ( ph -> Y e. B )`
7 evl1addd.3
` |-  ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )`
8 evl1addd.4
` |-  ( ph -> ( N e. U /\ ( ( O ` N ) ` Y ) = W ) )`
9 evl1subd.s
` |-  .- = ( -g ` P )`
10 evl1subd.d
` |-  D = ( -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 grpsubcl
` |-  ( ( P e. Grp /\ M e. U /\ N e. U ) -> ( M .- N ) e. U )`
21 17 18 19 20 syl3anc
` |-  ( ph -> ( M .- N ) e. U )`
22 eqid
` |-  ( -g ` ( R ^s B ) ) = ( -g ` ( R ^s B ) )`
23 4 9 22 ghmsub
` |-  ( ( O e. ( P GrpHom ( R ^s B ) ) /\ M e. U /\ N e. U ) -> ( O ` ( M .- N ) ) = ( ( O ` M ) ( -g ` ( R ^s B ) ) ( O ` N ) ) )`
24 15 18 19 23 syl3anc
` |-  ( ph -> ( O ` ( M .- N ) ) = ( ( O ` M ) ( -g ` ( R ^s B ) ) ( O ` N ) ) )`
25 crngring
` |-  ( R e. CRing -> R e. Ring )`
26 ringgrp
` |-  ( R e. Ring -> R e. Grp )`
27 5 25 26 3syl
` |-  ( ph -> R e. Grp )`
28 3 fvexi
` |-  B e. _V`
29 28 a1i
` |-  ( ph -> B e. _V )`
30 eqid
` |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )`
31 4 30 rhmf
` |-  ( O e. ( P RingHom ( R ^s B ) ) -> O : U --> ( Base ` ( R ^s B ) ) )`
32 13 31 syl
` |-  ( ph -> O : U --> ( Base ` ( R ^s B ) ) )`
33 32 18 ffvelrnd
` |-  ( ph -> ( O ` M ) e. ( Base ` ( R ^s B ) ) )`
34 32 19 ffvelrnd
` |-  ( ph -> ( O ` N ) e. ( Base ` ( R ^s B ) ) )`
35 11 30 10 22 pwssub
` |-  ( ( ( R e. Grp /\ B e. _V ) /\ ( ( O ` M ) e. ( Base ` ( R ^s B ) ) /\ ( O ` N ) e. ( Base ` ( R ^s B ) ) ) ) -> ( ( O ` M ) ( -g ` ( R ^s B ) ) ( O ` N ) ) = ( ( O ` M ) oF D ( O ` N ) ) )`
36 27 29 33 34 35 syl22anc
` |-  ( ph -> ( ( O ` M ) ( -g ` ( R ^s B ) ) ( O ` N ) ) = ( ( O ` M ) oF D ( O ` N ) ) )`
37 24 36 eqtrd
` |-  ( ph -> ( O ` ( M .- N ) ) = ( ( O ` M ) oF D ( O ` N ) ) )`
38 37 fveq1d
` |-  ( ph -> ( ( O ` ( M .- N ) ) ` Y ) = ( ( ( O ` M ) oF D ( O ` N ) ) ` Y ) )`
39 11 3 30 5 29 33 pwselbas
` |-  ( ph -> ( O ` M ) : B --> B )`
40 39 ffnd
` |-  ( ph -> ( O ` M ) Fn B )`
41 11 3 30 5 29 34 pwselbas
` |-  ( ph -> ( O ` N ) : B --> B )`
42 41 ffnd
` |-  ( ph -> ( O ` N ) Fn B )`
43 fnfvof
` |-  ( ( ( ( O ` M ) Fn B /\ ( O ` N ) Fn B ) /\ ( B e. _V /\ Y e. B ) ) -> ( ( ( O ` M ) oF D ( O ` N ) ) ` Y ) = ( ( ( O ` M ) ` Y ) D ( ( O ` N ) ` Y ) ) )`
44 40 42 29 6 43 syl22anc
` |-  ( ph -> ( ( ( O ` M ) oF D ( O ` N ) ) ` Y ) = ( ( ( O ` M ) ` Y ) D ( ( O ` N ) ` Y ) ) )`
45 7 simprd
` |-  ( ph -> ( ( O ` M ) ` Y ) = V )`
46 8 simprd
` |-  ( ph -> ( ( O ` N ) ` Y ) = W )`
47 45 46 oveq12d
` |-  ( ph -> ( ( ( O ` M ) ` Y ) D ( ( O ` N ) ` Y ) ) = ( V D W ) )`
48 38 44 47 3eqtrd
` |-  ( ph -> ( ( O ` ( M .- N ) ) ` Y ) = ( V D W ) )`
49 21 48 jca
` |-  ( ph -> ( ( M .- N ) e. U /\ ( ( O ` ( M .- N ) ) ` Y ) = ( V D W ) ) )`