Metamath Proof Explorer

Theorem mzpsubmpt

Description: The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion mzpsubmpt 
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A - B ) ) e. ( mzPoly ` V ) )

Proof

Step Hyp Ref Expression
1 nfmpt1 
 |-  F/_ x ( x e. ( ZZ ^m V ) |-> A )
2 1 nfel1 
 |-  F/ x ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V )
3 nfmpt1 
 |-  F/_ x ( x e. ( ZZ ^m V ) |-> B )
4 3 nfel1 
 |-  F/ x ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V )
5 2 4 nfan 
 |-  F/ x ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) )
6 mzpf 
 |-  ( ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> B ) : ( ZZ ^m V ) --> ZZ )
7 6 ad2antlr 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> ( x e. ( ZZ ^m V ) |-> B ) : ( ZZ ^m V ) --> ZZ )
8 simpr 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> x e. ( ZZ ^m V ) )
9 mptfcl 
 |-  ( ( x e. ( ZZ ^m V ) |-> B ) : ( ZZ ^m V ) --> ZZ -> ( x e. ( ZZ ^m V ) -> B e. ZZ ) )
10 7 8 9 sylc 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> B e. ZZ )
11 10 zcnd 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> B e. CC )
12 11 mulm1d 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> ( -u 1 x. B ) = -u B )
13 12 oveq2d 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> ( A + ( -u 1 x. B ) ) = ( A + -u B ) )
14 mzpf 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> A ) : ( ZZ ^m V ) --> ZZ )
15 14 ad2antrr 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> ( x e. ( ZZ ^m V ) |-> A ) : ( ZZ ^m V ) --> ZZ )
16 mptfcl 
 |-  ( ( x e. ( ZZ ^m V ) |-> A ) : ( ZZ ^m V ) --> ZZ -> ( x e. ( ZZ ^m V ) -> A e. ZZ ) )
17 15 8 16 sylc 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> A e. ZZ )
18 17 zcnd 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> A e. CC )
19 18 11 negsubd 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> ( A + -u B ) = ( A - B ) )
20 13 19 eqtr2d 
 |-  ( ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) /\ x e. ( ZZ ^m V ) ) -> ( A - B ) = ( A + ( -u 1 x. B ) ) )
21 5 20 mpteq2da 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A - B ) ) = ( x e. ( ZZ ^m V ) |-> ( A + ( -u 1 x. B ) ) ) )
22 elfvex 
 |-  ( ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) -> V e. _V )
23 neg1z 
 |-  -u 1 e. ZZ
24 mzpconstmpt 
 |-  ( ( V e. _V /\ -u 1 e. ZZ ) -> ( x e. ( ZZ ^m V ) |-> -u 1 ) e. ( mzPoly ` V ) )
25 22 23 24 sylancl 
 |-  ( ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> -u 1 ) e. ( mzPoly ` V ) )
26 mzpmulmpt 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> -u 1 ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( -u 1 x. B ) ) e. ( mzPoly ` V ) )
27 25 26 mpancom 
 |-  ( ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> ( -u 1 x. B ) ) e. ( mzPoly ` V ) )
28 mzpaddmpt 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> ( -u 1 x. B ) ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A + ( -u 1 x. B ) ) ) e. ( mzPoly ` V ) )
29 27 28 sylan2 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A + ( -u 1 x. B ) ) ) e. ( mzPoly ` V ) )
30 21 29 eqeltrd 
 |-  ( ( ( x e. ( ZZ ^m V ) |-> A ) e. ( mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A - B ) ) e. ( mzPoly ` V ) )