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 ffvelcdmd 
 |-  ( ph -> ( O ` M ) e. ( Base ` ( R ^s B ) ) )
34 32 19 ffvelcdmd 
 |-  ( 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 ) ) )