Metamath Proof Explorer

Theorem mzpsubst

Description: Substituting polynomials for the variables of a polynomial results in a polynomial. G is expected to depend on y and provide the polynomials which are being substituted. (Contributed by Stefan O'Rear, 5-Oct-2014)

Ref Expression
Assertion mzpsubst 
|- ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ A. y e. V G e. ( mzPoly ` W ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ A. y e. V G e. ( mzPoly ` W ) ) -> W e. _V )
2 elfvex 
 |-  ( F e. ( mzPoly ` V ) -> V e. _V )
3 2 3ad2ant2 
 |-  ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ A. y e. V G e. ( mzPoly ` W ) ) -> V e. _V )
4 simp3 
 |-  ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ A. y e. V G e. ( mzPoly ` W ) ) -> A. y e. V G e. ( mzPoly ` W ) )
5 simp2 
 |-  ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ A. y e. V G e. ( mzPoly ` W ) ) -> F e. ( mzPoly ` V ) )
6 simpr 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. ZZ ) /\ x e. ( ZZ ^m W ) ) -> x e. ( ZZ ^m W ) )
7 simpll3 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. ZZ ) /\ x e. ( ZZ ^m W ) ) -> A. y e. V G e. ( mzPoly ` W ) )
8 simpll2 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. ZZ ) /\ x e. ( ZZ ^m W ) ) -> V e. _V )
9 mzpf 
 |-  ( G e. ( mzPoly ` W ) -> G : ( ZZ ^m W ) --> ZZ )
10 9 ffvelrnda 
 |-  ( ( G e. ( mzPoly ` W ) /\ x e. ( ZZ ^m W ) ) -> ( G ` x ) e. ZZ )
11 10 expcom 
 |-  ( x e. ( ZZ ^m W ) -> ( G e. ( mzPoly ` W ) -> ( G ` x ) e. ZZ ) )
12 11 ralimdv 
 |-  ( x e. ( ZZ ^m W ) -> ( A. y e. V G e. ( mzPoly ` W ) -> A. y e. V ( G ` x ) e. ZZ ) )
13 12 imp 
 |-  ( ( x e. ( ZZ ^m W ) /\ A. y e. V G e. ( mzPoly ` W ) ) -> A. y e. V ( G ` x ) e. ZZ )
14 eqid 
 |-  ( y e. V |-> ( G ` x ) ) = ( y e. V |-> ( G ` x ) )
15 14 fmpt 
 |-  ( A. y e. V ( G ` x ) e. ZZ <-> ( y e. V |-> ( G ` x ) ) : V --> ZZ )
16 13 15 sylib 
 |-  ( ( x e. ( ZZ ^m W ) /\ A. y e. V G e. ( mzPoly ` W ) ) -> ( y e. V |-> ( G ` x ) ) : V --> ZZ )
17 16 adantr 
 |-  ( ( ( x e. ( ZZ ^m W ) /\ A. y e. V G e. ( mzPoly ` W ) ) /\ V e. _V ) -> ( y e. V |-> ( G ` x ) ) : V --> ZZ )
18 zex 
 |-  ZZ e. _V
19 simpr 
 |-  ( ( ( x e. ( ZZ ^m W ) /\ A. y e. V G e. ( mzPoly ` W ) ) /\ V e. _V ) -> V e. _V )
20 elmapg 
 |-  ( ( ZZ e. _V /\ V e. _V ) -> ( ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) <-> ( y e. V |-> ( G ` x ) ) : V --> ZZ ) )
21 18 19 20 sylancr 
 |-  ( ( ( x e. ( ZZ ^m W ) /\ A. y e. V G e. ( mzPoly ` W ) ) /\ V e. _V ) -> ( ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) <-> ( y e. V |-> ( G ` x ) ) : V --> ZZ ) )
22 17 21 mpbird 
 |-  ( ( ( x e. ( ZZ ^m W ) /\ A. y e. V G e. ( mzPoly ` W ) ) /\ V e. _V ) -> ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) )
23 6 7 8 22 syl21anc 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. ZZ ) /\ x e. ( ZZ ^m W ) ) -> ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) )
24 vex 
 |-  b e. _V
25 24 fvconst2 
 |-  ( ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) -> ( ( ( ZZ ^m V ) X. { b } ) ` ( y e. V |-> ( G ` x ) ) ) = b )
26 23 25 syl 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. ZZ ) /\ x e. ( ZZ ^m W ) ) -> ( ( ( ZZ ^m V ) X. { b } ) ` ( y e. V |-> ( G ` x ) ) ) = b )
27 26 mpteq2dva 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. ZZ ) -> ( x e. ( ZZ ^m W ) |-> ( ( ( ZZ ^m V ) X. { b } ) ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> b ) )
28 mzpconstmpt 
 |-  ( ( W e. _V /\ b e. ZZ ) -> ( x e. ( ZZ ^m W ) |-> b ) e. ( mzPoly ` W ) )
29 28 3ad2antl1 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. ZZ ) -> ( x e. ( ZZ ^m W ) |-> b ) e. ( mzPoly ` W ) )
30 27 29 eqeltrd 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. ZZ ) -> ( x e. ( ZZ ^m W ) |-> ( ( ( ZZ ^m V ) X. { b } ) ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) )
31 simpr 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) /\ x e. ( ZZ ^m W ) ) -> x e. ( ZZ ^m W ) )
32 simpll3 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) /\ x e. ( ZZ ^m W ) ) -> A. y e. V G e. ( mzPoly ` W ) )
33 simpll2 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) /\ x e. ( ZZ ^m W ) ) -> V e. _V )
34 31 32 33 22 syl21anc 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) /\ x e. ( ZZ ^m W ) ) -> ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) )
35 fveq1 
 |-  ( c = ( y e. V |-> ( G ` x ) ) -> ( c ` b ) = ( ( y e. V |-> ( G ` x ) ) ` b ) )
36 eqid 
 |-  ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) = ( c e. ( ZZ ^m V ) |-> ( c ` b ) )
37 fvex 
 |-  ( ( y e. V |-> ( G ` x ) ) ` b ) e. _V
38 35 36 37 fvmpt 
 |-  ( ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) -> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` ( y e. V |-> ( G ` x ) ) ) = ( ( y e. V |-> ( G ` x ) ) ` b ) )
39 34 38 syl 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) /\ x e. ( ZZ ^m W ) ) -> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` ( y e. V |-> ( G ` x ) ) ) = ( ( y e. V |-> ( G ` x ) ) ` b ) )
40 simplr 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) /\ x e. ( ZZ ^m W ) ) -> b e. V )
41 fvex 
 |-  ( [_ b / y ]_ G ` x ) e. _V
42 csbeq1 
 |-  ( a = b -> [_ a / y ]_ G = [_ b / y ]_ G )
43 42 fveq1d 
 |-  ( a = b -> ( [_ a / y ]_ G ` x ) = ( [_ b / y ]_ G ` x ) )
44 nfcv 
 |-  F/_ a ( G ` x )
45 nfcsb1v 
 |-  F/_ y [_ a / y ]_ G
46 nfcv 
 |-  F/_ y x
47 45 46 nffv 
 |-  F/_ y ( [_ a / y ]_ G ` x )
48 csbeq1a 
 |-  ( y = a -> G = [_ a / y ]_ G )
49 48 fveq1d 
 |-  ( y = a -> ( G ` x ) = ( [_ a / y ]_ G ` x ) )
50 44 47 49 cbvmpt 
 |-  ( y e. V |-> ( G ` x ) ) = ( a e. V |-> ( [_ a / y ]_ G ` x ) )
51 43 50 fvmptg 
 |-  ( ( b e. V /\ ( [_ b / y ]_ G ` x ) e. _V ) -> ( ( y e. V |-> ( G ` x ) ) ` b ) = ( [_ b / y ]_ G ` x ) )
52 40 41 51 sylancl 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) /\ x e. ( ZZ ^m W ) ) -> ( ( y e. V |-> ( G ` x ) ) ` b ) = ( [_ b / y ]_ G ` x ) )
53 39 52 eqtrd 
 |-  ( ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) /\ x e. ( ZZ ^m W ) ) -> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` ( y e. V |-> ( G ` x ) ) ) = ( [_ b / y ]_ G ` x ) )
54 53 mpteq2dva 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) -> ( x e. ( ZZ ^m W ) |-> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( [_ b / y ]_ G ` x ) ) )
55 simpr 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) -> b e. V )
56 simpl3 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) -> A. y e. V G e. ( mzPoly ` W ) )
57 nfcsb1v 
 |-  F/_ y [_ b / y ]_ G
58 57 nfel1 
 |-  F/ y [_ b / y ]_ G e. ( mzPoly ` W )
59 csbeq1a 
 |-  ( y = b -> G = [_ b / y ]_ G )
60 59 eleq1d 
 |-  ( y = b -> ( G e. ( mzPoly ` W ) <-> [_ b / y ]_ G e. ( mzPoly ` W ) ) )
61 58 60 rspc 
 |-  ( b e. V -> ( A. y e. V G e. ( mzPoly ` W ) -> [_ b / y ]_ G e. ( mzPoly ` W ) ) )
62 55 56 61 sylc 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) -> [_ b / y ]_ G e. ( mzPoly ` W ) )
63 mzpf 
 |-  ( [_ b / y ]_ G e. ( mzPoly ` W ) -> [_ b / y ]_ G : ( ZZ ^m W ) --> ZZ )
64 62 63 syl 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) -> [_ b / y ]_ G : ( ZZ ^m W ) --> ZZ )
65 64 feqmptd 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) -> [_ b / y ]_ G = ( x e. ( ZZ ^m W ) |-> ( [_ b / y ]_ G ` x ) ) )
66 54 65 eqtr4d 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) -> ( x e. ( ZZ ^m W ) |-> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` ( y e. V |-> ( G ` x ) ) ) ) = [_ b / y ]_ G )
67 66 62 eqeltrd 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ b e. V ) -> ( x e. ( ZZ ^m W ) |-> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) )
68 simp2l 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> b : ( ZZ ^m V ) --> ZZ )
69 68 ffnd 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> b Fn ( ZZ ^m V ) )
70 simp3l 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> c : ( ZZ ^m V ) --> ZZ )
71 70 ffnd 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> c Fn ( ZZ ^m V ) )
72 simp13 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> A. y e. V G e. ( mzPoly ` W ) )
73 simp12 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> V e. _V )
74 simplll 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> b Fn ( ZZ ^m V ) )
75 simpllr 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> c Fn ( ZZ ^m V ) )
76 ovexd 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> ( ZZ ^m V ) e. _V )
77 simpr 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> x e. ( ZZ ^m W ) )
78 simplrl 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> A. y e. V G e. ( mzPoly ` W ) )
79 77 78 12 sylc 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> A. y e. V ( G ` x ) e. ZZ )
80 79 15 sylib 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> ( y e. V |-> ( G ` x ) ) : V --> ZZ )
81 simplrr 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> V e. _V )
82 18 81 20 sylancr 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> ( ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) <-> ( y e. V |-> ( G ` x ) ) : V --> ZZ ) )
83 80 82 mpbird 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) )
84 fnfvof 
 |-  ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( ( ZZ ^m V ) e. _V /\ ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) ) ) -> ( ( b oF + c ) ` ( y e. V |-> ( G ` x ) ) ) = ( ( b ` ( y e. V |-> ( G ` x ) ) ) + ( c ` ( y e. V |-> ( G ` x ) ) ) ) )
85 74 75 76 83 84 syl22anc 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> ( ( b oF + c ) ` ( y e. V |-> ( G ` x ) ) ) = ( ( b ` ( y e. V |-> ( G ` x ) ) ) + ( c ` ( y e. V |-> ( G ` x ) ) ) ) )
86 85 mpteq2dva 
 |-  ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) -> ( x e. ( ZZ ^m W ) |-> ( ( b oF + c ) ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( ( b ` ( y e. V |-> ( G ` x ) ) ) + ( c ` ( y e. V |-> ( G ` x ) ) ) ) ) )
87 69 71 72 73 86 syl22anc 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> ( x e. ( ZZ ^m W ) |-> ( ( b oF + c ) ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( ( b ` ( y e. V |-> ( G ` x ) ) ) + ( c ` ( y e. V |-> ( G ` x ) ) ) ) ) )
88 simp2r 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) )
89 simp3r 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) )
90 mzpaddmpt 
 |-  ( ( ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) -> ( x e. ( ZZ ^m W ) |-> ( ( b ` ( y e. V |-> ( G ` x ) ) ) + ( c ` ( y e. V |-> ( G ` x ) ) ) ) ) e. ( mzPoly ` W ) )
91 88 89 90 syl2anc 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> ( x e. ( ZZ ^m W ) |-> ( ( b ` ( y e. V |-> ( G ` x ) ) ) + ( c ` ( y e. V |-> ( G ` x ) ) ) ) ) e. ( mzPoly ` W ) )
92 87 91 eqeltrd 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> ( x e. ( ZZ ^m W ) |-> ( ( b oF + c ) ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) )
93 fnfvof 
 |-  ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( ( ZZ ^m V ) e. _V /\ ( y e. V |-> ( G ` x ) ) e. ( ZZ ^m V ) ) ) -> ( ( b oF x. c ) ` ( y e. V |-> ( G ` x ) ) ) = ( ( b ` ( y e. V |-> ( G ` x ) ) ) x. ( c ` ( y e. V |-> ( G ` x ) ) ) ) )
94 74 75 76 83 93 syl22anc 
 |-  ( ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) /\ x e. ( ZZ ^m W ) ) -> ( ( b oF x. c ) ` ( y e. V |-> ( G ` x ) ) ) = ( ( b ` ( y e. V |-> ( G ` x ) ) ) x. ( c ` ( y e. V |-> ( G ` x ) ) ) ) )
95 94 mpteq2dva 
 |-  ( ( ( b Fn ( ZZ ^m V ) /\ c Fn ( ZZ ^m V ) ) /\ ( A. y e. V G e. ( mzPoly ` W ) /\ V e. _V ) ) -> ( x e. ( ZZ ^m W ) |-> ( ( b oF x. c ) ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( ( b ` ( y e. V |-> ( G ` x ) ) ) x. ( c ` ( y e. V |-> ( G ` x ) ) ) ) ) )
96 69 71 72 73 95 syl22anc 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> ( x e. ( ZZ ^m W ) |-> ( ( b oF x. c ) ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( ( b ` ( y e. V |-> ( G ` x ) ) ) x. ( c ` ( y e. V |-> ( G ` x ) ) ) ) ) )
97 mzpmulmpt 
 |-  ( ( ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) -> ( x e. ( ZZ ^m W ) |-> ( ( b ` ( y e. V |-> ( G ` x ) ) ) x. ( c ` ( y e. V |-> ( G ` x ) ) ) ) ) e. ( mzPoly ` W ) )
98 88 89 97 syl2anc 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> ( x e. ( ZZ ^m W ) |-> ( ( b ` ( y e. V |-> ( G ` x ) ) ) x. ( c ` ( y e. V |-> ( G ` x ) ) ) ) ) e. ( mzPoly ` W ) )
99 96 98 eqeltrd 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ ( b : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) /\ ( c : ( ZZ ^m V ) --> ZZ /\ ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) ) -> ( x e. ( ZZ ^m W ) |-> ( ( b oF x. c ) ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) )
100 fveq1 
 |-  ( a = ( ( ZZ ^m V ) X. { b } ) -> ( a ` ( y e. V |-> ( G ` x ) ) ) = ( ( ( ZZ ^m V ) X. { b } ) ` ( y e. V |-> ( G ` x ) ) ) )
101 100 mpteq2dv 
 |-  ( a = ( ( ZZ ^m V ) X. { b } ) -> ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( ( ( ZZ ^m V ) X. { b } ) ` ( y e. V |-> ( G ` x ) ) ) ) )
102 101 eleq1d 
 |-  ( a = ( ( ZZ ^m V ) X. { b } ) -> ( ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) <-> ( x e. ( ZZ ^m W ) |-> ( ( ( ZZ ^m V ) X. { b } ) ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) )
103 fveq1 
 |-  ( a = ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) -> ( a ` ( y e. V |-> ( G ` x ) ) ) = ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` ( y e. V |-> ( G ` x ) ) ) )
104 103 mpteq2dv 
 |-  ( a = ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) -> ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` ( y e. V |-> ( G ` x ) ) ) ) )
105 104 eleq1d 
 |-  ( a = ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) -> ( ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) <-> ( x e. ( ZZ ^m W ) |-> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) )
106 fveq1 
 |-  ( a = b -> ( a ` ( y e. V |-> ( G ` x ) ) ) = ( b ` ( y e. V |-> ( G ` x ) ) ) )
107 106 mpteq2dv 
 |-  ( a = b -> ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) )
108 107 eleq1d 
 |-  ( a = b -> ( ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) <-> ( x e. ( ZZ ^m W ) |-> ( b ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) )
109 fveq1 
 |-  ( a = c -> ( a ` ( y e. V |-> ( G ` x ) ) ) = ( c ` ( y e. V |-> ( G ` x ) ) ) )
110 109 mpteq2dv 
 |-  ( a = c -> ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) )
111 110 eleq1d 
 |-  ( a = c -> ( ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) <-> ( x e. ( ZZ ^m W ) |-> ( c ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) )
112 fveq1 
 |-  ( a = ( b oF + c ) -> ( a ` ( y e. V |-> ( G ` x ) ) ) = ( ( b oF + c ) ` ( y e. V |-> ( G ` x ) ) ) )
113 112 mpteq2dv 
 |-  ( a = ( b oF + c ) -> ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( ( b oF + c ) ` ( y e. V |-> ( G ` x ) ) ) ) )
114 113 eleq1d 
 |-  ( a = ( b oF + c ) -> ( ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) <-> ( x e. ( ZZ ^m W ) |-> ( ( b oF + c ) ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) )
115 fveq1 
 |-  ( a = ( b oF x. c ) -> ( a ` ( y e. V |-> ( G ` x ) ) ) = ( ( b oF x. c ) ` ( y e. V |-> ( G ` x ) ) ) )
116 115 mpteq2dv 
 |-  ( a = ( b oF x. c ) -> ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( ( b oF x. c ) ` ( y e. V |-> ( G ` x ) ) ) ) )
117 116 eleq1d 
 |-  ( a = ( b oF x. c ) -> ( ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) <-> ( x e. ( ZZ ^m W ) |-> ( ( b oF x. c ) ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) )
118 fveq1 
 |-  ( a = F -> ( a ` ( y e. V |-> ( G ` x ) ) ) = ( F ` ( y e. V |-> ( G ` x ) ) ) )
119 118 mpteq2dv 
 |-  ( a = F -> ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) = ( x e. ( ZZ ^m W ) |-> ( F ` ( y e. V |-> ( G ` x ) ) ) ) )
120 119 eleq1d 
 |-  ( a = F -> ( ( x e. ( ZZ ^m W ) |-> ( a ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) <-> ( x e. ( ZZ ^m W ) |-> ( F ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) ) )
121 30 67 92 99 102 105 108 111 114 117 120 mzpindd 
 |-  ( ( ( W e. _V /\ V e. _V /\ A. y e. V G e. ( mzPoly ` W ) ) /\ F e. ( mzPoly ` V ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) )
122 1 3 4 5 121 syl31anc 
 |-  ( ( W e. _V /\ F e. ( mzPoly ` V ) /\ A. y e. V G e. ( mzPoly ` W ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( y e. V |-> ( G ` x ) ) ) ) e. ( mzPoly ` W ) )