Metamath Proof Explorer

Theorem mzpcong

Description: Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion mzpcong 
|- ( ( F e. ( mzPoly ` V ) /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) -> N || ( ( F ` X ) - ( F ` Y ) ) )

Proof

Step Hyp Ref Expression
1 elfvex 
 |-  ( F e. ( mzPoly ` V ) -> V e. _V )
2 1 3anim1i 
 |-  ( ( F e. ( mzPoly ` V ) /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) -> ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) )
3 simp1 
 |-  ( ( F e. ( mzPoly ` V ) /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) -> F e. ( mzPoly ` V ) )
4 simpl3l 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. ZZ ) -> N e. ZZ )
5 simpr 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. ZZ ) -> b e. ZZ )
6 congid 
 |-  ( ( N e. ZZ /\ b e. ZZ ) -> N || ( b - b ) )
7 4 5 6 syl2anc 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. ZZ ) -> N || ( b - b ) )
8 simpl2l 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. ZZ ) -> X e. ( ZZ ^m V ) )
9 vex 
 |-  b e. _V
10 9 fvconst2 
 |-  ( X e. ( ZZ ^m V ) -> ( ( ( ZZ ^m V ) X. { b } ) ` X ) = b )
11 8 10 syl 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. ZZ ) -> ( ( ( ZZ ^m V ) X. { b } ) ` X ) = b )
12 simpl2r 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. ZZ ) -> Y e. ( ZZ ^m V ) )
13 9 fvconst2 
 |-  ( Y e. ( ZZ ^m V ) -> ( ( ( ZZ ^m V ) X. { b } ) ` Y ) = b )
14 12 13 syl 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. ZZ ) -> ( ( ( ZZ ^m V ) X. { b } ) ` Y ) = b )
15 11 14 oveq12d 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. ZZ ) -> ( ( ( ( ZZ ^m V ) X. { b } ) ` X ) - ( ( ( ZZ ^m V ) X. { b } ) ` Y ) ) = ( b - b ) )
16 7 15 breqtrrd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. ZZ ) -> N || ( ( ( ( ZZ ^m V ) X. { b } ) ` X ) - ( ( ( ZZ ^m V ) X. { b } ) ` Y ) ) )
17 simpr 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. V ) -> b e. V )
18 simpl3r 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. V ) -> A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) )
19 fveq2 
 |-  ( k = b -> ( X ` k ) = ( X ` b ) )
20 fveq2 
 |-  ( k = b -> ( Y ` k ) = ( Y ` b ) )
21 19 20 oveq12d 
 |-  ( k = b -> ( ( X ` k ) - ( Y ` k ) ) = ( ( X ` b ) - ( Y ` b ) ) )
22 21 breq2d 
 |-  ( k = b -> ( N || ( ( X ` k ) - ( Y ` k ) ) <-> N || ( ( X ` b ) - ( Y ` b ) ) ) )
23 22 rspcva 
 |-  ( ( b e. V /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) -> N || ( ( X ` b ) - ( Y ` b ) ) )
24 17 18 23 syl2anc 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. V ) -> N || ( ( X ` b ) - ( Y ` b ) ) )
25 simpl2l 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. V ) -> X e. ( ZZ ^m V ) )
26 fveq1 
 |-  ( c = X -> ( c ` b ) = ( X ` b ) )
27 eqid 
 |-  ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) = ( c e. ( ZZ ^m V ) |-> ( c ` b ) )
28 fvex 
 |-  ( X ` b ) e. _V
29 26 27 28 fvmpt 
 |-  ( X e. ( ZZ ^m V ) -> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` X ) = ( X ` b ) )
30 25 29 syl 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. V ) -> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` X ) = ( X ` b ) )
31 simpl2r 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. V ) -> Y e. ( ZZ ^m V ) )
32 fveq1 
 |-  ( c = Y -> ( c ` b ) = ( Y ` b ) )
33 fvex 
 |-  ( Y ` b ) e. _V
34 32 27 33 fvmpt 
 |-  ( Y e. ( ZZ ^m V ) -> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` Y ) = ( Y ` b ) )
35 31 34 syl 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. V ) -> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` Y ) = ( Y ` b ) )
36 30 35 oveq12d 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. V ) -> ( ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` X ) - ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` Y ) ) = ( ( X ` b ) - ( Y ` b ) ) )
37 24 36 breqtrrd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ b e. V ) -> N || ( ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` X ) - ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` Y ) ) )
38 simp13l 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> N e. ZZ )
39 simp2l 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> b : ( ZZ ^m V ) --> ZZ )
40 simp12l 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> X e. ( ZZ ^m V ) )
41 39 40 ffvelrnd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( b ` X ) e. ZZ )
42 simp12r 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> Y e. ( ZZ ^m V ) )
43 39 42 ffvelrnd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( b ` Y ) e. ZZ )
44 simp3l 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> c : ( ZZ ^m V ) --> ZZ )
45 44 40 ffvelrnd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( c ` X ) e. ZZ )
46 44 42 ffvelrnd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( c ` Y ) e. ZZ )
47 simp2r 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> N || ( ( b ` X ) - ( b ` Y ) ) )
48 simp3r 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> N || ( ( c ` X ) - ( c ` Y ) ) )
49 congadd 
 |-  ( ( ( N e. ZZ /\ ( b ` X ) e. ZZ /\ ( b ` Y ) e. ZZ ) /\ ( ( c ` X ) e. ZZ /\ ( c ` Y ) e. ZZ ) /\ ( N || ( ( b ` X ) - ( b ` Y ) ) /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> N || ( ( ( b ` X ) + ( c ` X ) ) - ( ( b ` Y ) + ( c ` Y ) ) ) )
50 38 41 43 45 46 47 48 49 syl322anc 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> N || ( ( ( b ` X ) + ( c ` X ) ) - ( ( b ` Y ) + ( c ` Y ) ) ) )
51 39 ffnd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> b Fn ( ZZ ^m V ) )
52 44 ffnd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> c Fn ( ZZ ^m V ) )
53 ovexd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( ZZ ^m V ) e. _V )
54 fnfvof 
 |-  ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( ( ZZ ^m V ) e. _V /\ X e. ( ZZ ^m V ) ) ) -> ( ( b oF + c ) ` X ) = ( ( b ` X ) + ( c ` X ) ) )
55 51 52 53 40 54 syl22anc 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( ( b oF + c ) ` X ) = ( ( b ` X ) + ( c ` X ) ) )
56 fnfvof 
 |-  ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( ( ZZ ^m V ) e. _V /\ Y e. ( ZZ ^m V ) ) ) -> ( ( b oF + c ) ` Y ) = ( ( b ` Y ) + ( c ` Y ) ) )
57 51 52 53 42 56 syl22anc 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( ( b oF + c ) ` Y ) = ( ( b ` Y ) + ( c ` Y ) ) )
58 55 57 oveq12d 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( ( ( b oF + c ) ` X ) - ( ( b oF + c ) ` Y ) ) = ( ( ( b ` X ) + ( c ` X ) ) - ( ( b ` Y ) + ( c ` Y ) ) ) )
59 50 58 breqtrrd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> N || ( ( ( b oF + c ) ` X ) - ( ( b oF + c ) ` Y ) ) )
60 congmul 
 |-  ( ( ( N e. ZZ /\ ( b ` X ) e. ZZ /\ ( b ` Y ) e. ZZ ) /\ ( ( c ` X ) e. ZZ /\ ( c ` Y ) e. ZZ ) /\ ( N || ( ( b ` X ) - ( b ` Y ) ) /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> N || ( ( ( b ` X ) x. ( c ` X ) ) - ( ( b ` Y ) x. ( c ` Y ) ) ) )
61 38 41 43 45 46 47 48 60 syl322anc 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> N || ( ( ( b ` X ) x. ( c ` X ) ) - ( ( b ` Y ) x. ( c ` Y ) ) ) )
62 fnfvof 
 |-  ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( ( ZZ ^m V ) e. _V /\ X e. ( ZZ ^m V ) ) ) -> ( ( b oF x. c ) ` X ) = ( ( b ` X ) x. ( c ` X ) ) )
63 51 52 53 40 62 syl22anc 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( ( b oF x. c ) ` X ) = ( ( b ` X ) x. ( c ` X ) ) )
64 fnfvof 
 |-  ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( ( ZZ ^m V ) e. _V /\ Y e. ( ZZ ^m V ) ) ) -> ( ( b oF x. c ) ` Y ) = ( ( b ` Y ) x. ( c ` Y ) ) )
65 51 52 53 42 64 syl22anc 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( ( b oF x. c ) ` Y ) = ( ( b ` Y ) x. ( c ` Y ) ) )
66 63 65 oveq12d 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> ( ( ( b oF x. c ) ` X ) - ( ( b oF x. c ) ` Y ) ) = ( ( ( b ` X ) x. ( c ` X ) ) - ( ( b ` Y ) x. ( c ` Y ) ) ) )
67 61 66 breqtrrd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ N || ( ( b ` X ) - ( b ` Y ) ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ N || ( ( c ` X ) - ( c ` Y ) ) ) ) -> N || ( ( ( b oF x. c ) ` X ) - ( ( b oF x. c ) ` Y ) ) )
68 fveq1 
 |-  ( a = ( ( ZZ ^m V ) X. { b } ) -> ( a ` X ) = ( ( ( ZZ ^m V ) X. { b } ) ` X ) )
69 fveq1 
 |-  ( a = ( ( ZZ ^m V ) X. { b } ) -> ( a ` Y ) = ( ( ( ZZ ^m V ) X. { b } ) ` Y ) )
70 68 69 oveq12d 
 |-  ( a = ( ( ZZ ^m V ) X. { b } ) -> ( ( a ` X ) - ( a ` Y ) ) = ( ( ( ( ZZ ^m V ) X. { b } ) ` X ) - ( ( ( ZZ ^m V ) X. { b } ) ` Y ) ) )
71 70 breq2d 
 |-  ( a = ( ( ZZ ^m V ) X. { b } ) -> ( N || ( ( a ` X ) - ( a ` Y ) ) <-> N || ( ( ( ( ZZ ^m V ) X. { b } ) ` X ) - ( ( ( ZZ ^m V ) X. { b } ) ` Y ) ) ) )
72 fveq1 
 |-  ( a = ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) -> ( a ` X ) = ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` X ) )
73 fveq1 
 |-  ( a = ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) -> ( a ` Y ) = ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` Y ) )
74 72 73 oveq12d 
 |-  ( a = ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) -> ( ( a ` X ) - ( a ` Y ) ) = ( ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` X ) - ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` Y ) ) )
75 74 breq2d 
 |-  ( a = ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) -> ( N || ( ( a ` X ) - ( a ` Y ) ) <-> N || ( ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` X ) - ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` Y ) ) ) )
76 fveq1 
 |-  ( a = b -> ( a ` X ) = ( b ` X ) )
77 fveq1 
 |-  ( a = b -> ( a ` Y ) = ( b ` Y ) )
78 76 77 oveq12d 
 |-  ( a = b -> ( ( a ` X ) - ( a ` Y ) ) = ( ( b ` X ) - ( b ` Y ) ) )
79 78 breq2d 
 |-  ( a = b -> ( N || ( ( a ` X ) - ( a ` Y ) ) <-> N || ( ( b ` X ) - ( b ` Y ) ) ) )
80 fveq1 
 |-  ( a = c -> ( a ` X ) = ( c ` X ) )
81 fveq1 
 |-  ( a = c -> ( a ` Y ) = ( c ` Y ) )
82 80 81 oveq12d 
 |-  ( a = c -> ( ( a ` X ) - ( a ` Y ) ) = ( ( c ` X ) - ( c ` Y ) ) )
83 82 breq2d 
 |-  ( a = c -> ( N || ( ( a ` X ) - ( a ` Y ) ) <-> N || ( ( c ` X ) - ( c ` Y ) ) ) )
84 fveq1 
 |-  ( a = ( b oF + c ) -> ( a ` X ) = ( ( b oF + c ) ` X ) )
85 fveq1 
 |-  ( a = ( b oF + c ) -> ( a ` Y ) = ( ( b oF + c ) ` Y ) )
86 84 85 oveq12d 
 |-  ( a = ( b oF + c ) -> ( ( a ` X ) - ( a ` Y ) ) = ( ( ( b oF + c ) ` X ) - ( ( b oF + c ) ` Y ) ) )
87 86 breq2d 
 |-  ( a = ( b oF + c ) -> ( N || ( ( a ` X ) - ( a ` Y ) ) <-> N || ( ( ( b oF + c ) ` X ) - ( ( b oF + c ) ` Y ) ) ) )
88 fveq1 
 |-  ( a = ( b oF x. c ) -> ( a ` X ) = ( ( b oF x. c ) ` X ) )
89 fveq1 
 |-  ( a = ( b oF x. c ) -> ( a ` Y ) = ( ( b oF x. c ) ` Y ) )
90 88 89 oveq12d 
 |-  ( a = ( b oF x. c ) -> ( ( a ` X ) - ( a ` Y ) ) = ( ( ( b oF x. c ) ` X ) - ( ( b oF x. c ) ` Y ) ) )
91 90 breq2d 
 |-  ( a = ( b oF x. c ) -> ( N || ( ( a ` X ) - ( a ` Y ) ) <-> N || ( ( ( b oF x. c ) ` X ) - ( ( b oF x. c ) ` Y ) ) ) )
92 fveq1 
 |-  ( a = F -> ( a ` X ) = ( F ` X ) )
93 fveq1 
 |-  ( a = F -> ( a ` Y ) = ( F ` Y ) )
94 92 93 oveq12d 
 |-  ( a = F -> ( ( a ` X ) - ( a ` Y ) ) = ( ( F ` X ) - ( F ` Y ) ) )
95 94 breq2d 
 |-  ( a = F -> ( N || ( ( a ` X ) - ( a ` Y ) ) <-> N || ( ( F ` X ) - ( F ` Y ) ) ) )
96 16 37 59 67 71 75 79 83 87 91 95 mzpindd 
 |-  ( ( ( V e. _V /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) /\ F e. ( mzPoly ` V ) ) -> N || ( ( F ` X ) - ( F ` Y ) ) )
97 2 3 96 syl2anc 
 |-  ( ( F e. ( mzPoly ` V ) /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) -> N || ( ( F ` X ) - ( F ` Y ) ) )