# 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}={\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)$
evl1subd.s
evl1subd.d ${⊢}{D}={-}_{{R}}$
Assertion evl1subd

### 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)$
9 evl1subd.s
10 evl1subd.d ${⊢}{D}={-}_{{R}}$
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 grpsubcl
21 17 18 19 20 syl3anc
22 eqid ${⊢}{-}_{\left({R}{↑}_{𝑠}{B}\right)}={-}_{\left({R}{↑}_{𝑠}{B}\right)}$
23 4 9 22 ghmsub
24 15 18 19 23 syl3anc
25 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
26 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
27 5 25 26 3syl ${⊢}{\phi }\to {R}\in \mathrm{Grp}$
28 3 fvexi ${⊢}{B}\in \mathrm{V}$
29 28 a1i ${⊢}{\phi }\to {B}\in \mathrm{V}$
30 eqid ${⊢}{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}={\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
31 4 30 rhmf ${⊢}{O}\in \left({P}\mathrm{RingHom}\left({R}{↑}_{𝑠}{B}\right)\right)\to {O}:{U}⟶{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
32 13 31 syl ${⊢}{\phi }\to {O}:{U}⟶{\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
33 32 18 ffvelrnd ${⊢}{\phi }\to {O}\left({M}\right)\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
34 32 19 ffvelrnd ${⊢}{\phi }\to {O}\left({N}\right)\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}$
35 11 30 10 22 pwssub ${⊢}\left(\left({R}\in \mathrm{Grp}\wedge {B}\in \mathrm{V}\right)\wedge \left({O}\left({M}\right)\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}\wedge {O}\left({N}\right)\in {\mathrm{Base}}_{\left({R}{↑}_{𝑠}{B}\right)}\right)\right)\to {O}\left({M}\right){-}_{\left({R}{↑}_{𝑠}{B}\right)}{O}\left({N}\right)={O}\left({M}\right){{D}}_{f}{O}\left({N}\right)$
36 27 29 33 34 35 syl22anc ${⊢}{\phi }\to {O}\left({M}\right){-}_{\left({R}{↑}_{𝑠}{B}\right)}{O}\left({N}\right)={O}\left({M}\right){{D}}_{f}{O}\left({N}\right)$
37 24 36 eqtrd
38 37 fveq1d
39 11 3 30 5 29 33 pwselbas ${⊢}{\phi }\to {O}\left({M}\right):{B}⟶{B}$
40 39 ffnd ${⊢}{\phi }\to {O}\left({M}\right)Fn{B}$
41 11 3 30 5 29 34 pwselbas ${⊢}{\phi }\to {O}\left({N}\right):{B}⟶{B}$
42 41 ffnd ${⊢}{\phi }\to {O}\left({N}\right)Fn{B}$
43 fnfvof ${⊢}\left(\left({O}\left({M}\right)Fn{B}\wedge {O}\left({N}\right)Fn{B}\right)\wedge \left({B}\in \mathrm{V}\wedge {Y}\in {B}\right)\right)\to \left({O}\left({M}\right){{D}}_{f}{O}\left({N}\right)\right)\left({Y}\right)={O}\left({M}\right)\left({Y}\right){D}{O}\left({N}\right)\left({Y}\right)$
44 40 42 29 6 43 syl22anc ${⊢}{\phi }\to \left({O}\left({M}\right){{D}}_{f}{O}\left({N}\right)\right)\left({Y}\right)={O}\left({M}\right)\left({Y}\right){D}{O}\left({N}\right)\left({Y}\right)$
45 7 simprd ${⊢}{\phi }\to {O}\left({M}\right)\left({Y}\right)={V}$
46 8 simprd ${⊢}{\phi }\to {O}\left({N}\right)\left({Y}\right)={W}$
47 45 46 oveq12d ${⊢}{\phi }\to {O}\left({M}\right)\left({Y}\right){D}{O}\left({N}\right)\left({Y}\right)={V}{D}{W}$
48 38 44 47 3eqtrd
49 21 48 jca