Metamath Proof Explorer

Theorem mzpcompact2lem

Description: Lemma for mzpcompact2 . (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Hypothesis mzpcompact2lem.i 
|- B e. _V
Assertion mzpcompact2lem 
|- ( A e. ( mzPoly ` B ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ A = ( c e. ( ZZ ^m B ) |-> ( b ` ( c |` a ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mzpcompact2lem.i 
 |-  B e. _V
2 tru 
 |-  T.
3 0fi 
 |-  (/) e. Fin
4 0ex 
 |-  (/) e. _V
5 mzpconst 
 |-  ( ( (/) e. _V /\ f e. ZZ ) -> ( ( ZZ ^m (/) ) X. { f } ) e. ( mzPoly ` (/) ) )
6 4 5 mpan 
 |-  ( f e. ZZ -> ( ( ZZ ^m (/) ) X. { f } ) e. ( mzPoly ` (/) ) )
7 0ss 
 |-  (/) C_ B
8 7 a1i 
 |-  ( f e. ZZ -> (/) C_ B )
9 fconstmpt 
 |-  ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> f )
10 simpr 
 |-  ( ( f e. ZZ /\ d e. ( ZZ ^m B ) ) -> d e. ( ZZ ^m B ) )
11 elmapssres 
 |-  ( ( d e. ( ZZ ^m B ) /\ (/) C_ B ) -> ( d |` (/) ) e. ( ZZ ^m (/) ) )
12 10 7 11 sylancl 
 |-  ( ( f e. ZZ /\ d e. ( ZZ ^m B ) ) -> ( d |` (/) ) e. ( ZZ ^m (/) ) )
13 vex 
 |-  f e. _V
14 13 fvconst2 
 |-  ( ( d |` (/) ) e. ( ZZ ^m (/) ) -> ( ( ( ZZ ^m (/) ) X. { f } ) ` ( d |` (/) ) ) = f )
15 12 14 syl 
 |-  ( ( f e. ZZ /\ d e. ( ZZ ^m B ) ) -> ( ( ( ZZ ^m (/) ) X. { f } ) ` ( d |` (/) ) ) = f )
16 15 mpteq2dva 
 |-  ( f e. ZZ -> ( d e. ( ZZ ^m B ) |-> ( ( ( ZZ ^m (/) ) X. { f } ) ` ( d |` (/) ) ) ) = ( d e. ( ZZ ^m B ) |-> f ) )
17 9 16 eqtr4id 
 |-  ( f e. ZZ -> ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( ( ( ZZ ^m (/) ) X. { f } ) ` ( d |` (/) ) ) ) )
18 fveq1 
 |-  ( b = ( ( ZZ ^m (/) ) X. { f } ) -> ( b ` ( d |` (/) ) ) = ( ( ( ZZ ^m (/) ) X. { f } ) ` ( d |` (/) ) ) )
19 18 mpteq2dv 
 |-  ( b = ( ( ZZ ^m (/) ) X. { f } ) -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` (/) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( ( ZZ ^m (/) ) X. { f } ) ` ( d |` (/) ) ) ) )
20 19 eqeq2d 
 |-  ( b = ( ( ZZ ^m (/) ) X. { f } ) -> ( ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` (/) ) ) ) <-> ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( ( ( ZZ ^m (/) ) X. { f } ) ` ( d |` (/) ) ) ) ) )
21 20 anbi2d 
 |-  ( b = ( ( ZZ ^m (/) ) X. { f } ) -> ( ( (/) C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` (/) ) ) ) ) <-> ( (/) C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( ( ( ZZ ^m (/) ) X. { f } ) ` ( d |` (/) ) ) ) ) ) )
22 21 rspcev 
 |-  ( ( ( ( ZZ ^m (/) ) X. { f } ) e. ( mzPoly ` (/) ) /\ ( (/) C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( ( ( ZZ ^m (/) ) X. { f } ) ` ( d |` (/) ) ) ) ) ) -> E. b e. ( mzPoly ` (/) ) ( (/) C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` (/) ) ) ) ) )
23 6 8 17 22 syl12anc 
 |-  ( f e. ZZ -> E. b e. ( mzPoly ` (/) ) ( (/) C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` (/) ) ) ) ) )
24 fveq2 
 |-  ( a = (/) -> ( mzPoly ` a ) = ( mzPoly ` (/) ) )
25 sseq1 
 |-  ( a = (/) -> ( a C_ B <-> (/) C_ B ) )
26 reseq2 
 |-  ( a = (/) -> ( d |` a ) = ( d |` (/) ) )
27 26 fveq2d 
 |-  ( a = (/) -> ( b ` ( d |` a ) ) = ( b ` ( d |` (/) ) ) )
28 27 mpteq2dv 
 |-  ( a = (/) -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` (/) ) ) ) )
29 28 eqeq2d 
 |-  ( a = (/) -> ( ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` (/) ) ) ) ) )
30 25 29 anbi12d 
 |-  ( a = (/) -> ( ( a C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( (/) C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` (/) ) ) ) ) ) )
31 24 30 rexeqbidv 
 |-  ( a = (/) -> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. b e. ( mzPoly ` (/) ) ( (/) C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` (/) ) ) ) ) ) )
32 31 rspcev 
 |-  ( ( (/) e. Fin /\ E. b e. ( mzPoly ` (/) ) ( (/) C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` (/) ) ) ) ) ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
33 3 23 32 sylancr 
 |-  ( f e. ZZ -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
34 33 adantl 
 |-  ( ( T. /\ f e. ZZ ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
35 snfi 
 |-  { f } e. Fin
36 vsnex 
 |-  { f } e. _V
37 vsnid 
 |-  f e. { f }
38 mzpproj 
 |-  ( ( { f } e. _V /\ f e. { f } ) -> ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) e. ( mzPoly ` { f } ) )
39 36 37 38 mp2an 
 |-  ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) e. ( mzPoly ` { f } )
40 39 a1i 
 |-  ( f e. B -> ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) e. ( mzPoly ` { f } ) )
41 snssi 
 |-  ( f e. B -> { f } C_ B )
42 fveq1 
 |-  ( g = d -> ( g ` f ) = ( d ` f ) )
43 42 cbvmptv 
 |-  ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( d ` f ) )
44 simpr 
 |-  ( ( f e. B /\ d e. ( ZZ ^m B ) ) -> d e. ( ZZ ^m B ) )
45 simpl 
 |-  ( ( f e. B /\ d e. ( ZZ ^m B ) ) -> f e. B )
46 45 snssd 
 |-  ( ( f e. B /\ d e. ( ZZ ^m B ) ) -> { f } C_ B )
47 elmapssres 
 |-  ( ( d e. ( ZZ ^m B ) /\ { f } C_ B ) -> ( d |` { f } ) e. ( ZZ ^m { f } ) )
48 44 46 47 syl2anc 
 |-  ( ( f e. B /\ d e. ( ZZ ^m B ) ) -> ( d |` { f } ) e. ( ZZ ^m { f } ) )
49 fveq1 
 |-  ( g = ( d |` { f } ) -> ( g ` f ) = ( ( d |` { f } ) ` f ) )
50 eqid 
 |-  ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) = ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) )
51 fvex 
 |-  ( ( d |` { f } ) ` f ) e. _V
52 49 50 51 fvmpt 
 |-  ( ( d |` { f } ) e. ( ZZ ^m { f } ) -> ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) ` ( d |` { f } ) ) = ( ( d |` { f } ) ` f ) )
53 48 52 syl 
 |-  ( ( f e. B /\ d e. ( ZZ ^m B ) ) -> ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) ` ( d |` { f } ) ) = ( ( d |` { f } ) ` f ) )
54 fvres 
 |-  ( f e. { f } -> ( ( d |` { f } ) ` f ) = ( d ` f ) )
55 37 54 ax-mp 
 |-  ( ( d |` { f } ) ` f ) = ( d ` f )
56 53 55 eqtr2di 
 |-  ( ( f e. B /\ d e. ( ZZ ^m B ) ) -> ( d ` f ) = ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) ` ( d |` { f } ) ) )
57 56 mpteq2dva 
 |-  ( f e. B -> ( d e. ( ZZ ^m B ) |-> ( d ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) ` ( d |` { f } ) ) ) )
58 43 57 eqtrid 
 |-  ( f e. B -> ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) ` ( d |` { f } ) ) ) )
59 fveq1 
 |-  ( b = ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) -> ( b ` ( d |` { f } ) ) = ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) ` ( d |` { f } ) ) )
60 59 mpteq2dv 
 |-  ( b = ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` { f } ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) ` ( d |` { f } ) ) ) )
61 60 eqeq2d 
 |-  ( b = ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) -> ( ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` { f } ) ) ) <-> ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) ` ( d |` { f } ) ) ) ) )
62 61 anbi2d 
 |-  ( b = ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) -> ( ( { f } C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` { f } ) ) ) ) <-> ( { f } C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) ` ( d |` { f } ) ) ) ) ) )
63 62 rspcev 
 |-  ( ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) e. ( mzPoly ` { f } ) /\ ( { f } C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( ( g e. ( ZZ ^m { f } ) |-> ( g ` f ) ) ` ( d |` { f } ) ) ) ) ) -> E. b e. ( mzPoly ` { f } ) ( { f } C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` { f } ) ) ) ) )
64 40 41 58 63 syl12anc 
 |-  ( f e. B -> E. b e. ( mzPoly ` { f } ) ( { f } C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` { f } ) ) ) ) )
65 fveq2 
 |-  ( a = { f } -> ( mzPoly ` a ) = ( mzPoly ` { f } ) )
66 sseq1 
 |-  ( a = { f } -> ( a C_ B <-> { f } C_ B ) )
67 reseq2 
 |-  ( a = { f } -> ( d |` a ) = ( d |` { f } ) )
68 67 fveq2d 
 |-  ( a = { f } -> ( b ` ( d |` a ) ) = ( b ` ( d |` { f } ) ) )
69 68 mpteq2dv 
 |-  ( a = { f } -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` { f } ) ) ) )
70 69 eqeq2d 
 |-  ( a = { f } -> ( ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` { f } ) ) ) ) )
71 66 70 anbi12d 
 |-  ( a = { f } -> ( ( a C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( { f } C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` { f } ) ) ) ) ) )
72 65 71 rexeqbidv 
 |-  ( a = { f } -> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. b e. ( mzPoly ` { f } ) ( { f } C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` { f } ) ) ) ) ) )
73 72 rspcev 
 |-  ( ( { f } e. Fin /\ E. b e. ( mzPoly ` { f } ) ( { f } C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` { f } ) ) ) ) ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
74 35 64 73 sylancr 
 |-  ( f e. B -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
75 74 adantl 
 |-  ( ( T. /\ f e. B ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
76 simplll 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> h e. Fin )
77 simprll 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> j e. Fin )
78 unfi 
 |-  ( ( h e. Fin /\ j e. Fin ) -> ( h u. j ) e. Fin )
79 76 77 78 syl2anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( h u. j ) e. Fin )
80 vex 
 |-  h e. _V
81 vex 
 |-  j e. _V
82 80 81 unex 
 |-  ( h u. j ) e. _V
83 82 a1i 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( h u. j ) e. _V )
84 ssun1 
 |-  h C_ ( h u. j )
85 84 a1i 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> h C_ ( h u. j ) )
86 simpllr 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> i e. ( mzPoly ` h ) )
87 mzpresrename 
 |-  ( ( ( h u. j ) e. _V /\ h C_ ( h u. j ) /\ i e. ( mzPoly ` h ) ) -> ( l e. ( ZZ ^m ( h u. j ) ) |-> ( i ` ( l |` h ) ) ) e. ( mzPoly ` ( h u. j ) ) )
88 83 85 86 87 syl3anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( l e. ( ZZ ^m ( h u. j ) ) |-> ( i ` ( l |` h ) ) ) e. ( mzPoly ` ( h u. j ) ) )
89 ssun2 
 |-  j C_ ( h u. j )
90 89 a1i 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> j C_ ( h u. j ) )
91 simprlr 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> k e. ( mzPoly ` j ) )
92 mzpresrename 
 |-  ( ( ( h u. j ) e. _V /\ j C_ ( h u. j ) /\ k e. ( mzPoly ` j ) ) -> ( l e. ( ZZ ^m ( h u. j ) ) |-> ( k ` ( l |` j ) ) ) e. ( mzPoly ` ( h u. j ) ) )
93 83 90 91 92 syl3anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( l e. ( ZZ ^m ( h u. j ) ) |-> ( k ` ( l |` j ) ) ) e. ( mzPoly ` ( h u. j ) ) )
94 mzpaddmpt 
 |-  ( ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( i ` ( l |` h ) ) ) e. ( mzPoly ` ( h u. j ) ) /\ ( l e. ( ZZ ^m ( h u. j ) ) |-> ( k ` ( l |` j ) ) ) e. ( mzPoly ` ( h u. j ) ) ) -> ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) e. ( mzPoly ` ( h u. j ) ) )
95 88 93 94 syl2anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) e. ( mzPoly ` ( h u. j ) ) )
96 simplr 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> h C_ B )
97 simprr 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> j C_ B )
98 96 97 unssd 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( h u. j ) C_ B )
99 ovex 
 |-  ( ZZ ^m B ) e. _V
100 99 a1i 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( ZZ ^m B ) e. _V )
101 1 a1i 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> B e. _V )
102 mzpresrename 
 |-  ( ( B e. _V /\ h C_ B /\ i e. ( mzPoly ` h ) ) -> ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) e. ( mzPoly ` B ) )
103 101 96 86 102 syl3anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) e. ( mzPoly ` B ) )
104 mzpf 
 |-  ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) e. ( mzPoly ` B ) -> ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) : ( ZZ ^m B ) --> ZZ )
105 ffn 
 |-  ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) : ( ZZ ^m B ) --> ZZ -> ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) Fn ( ZZ ^m B ) )
106 103 104 105 3syl 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) Fn ( ZZ ^m B ) )
107 mzpresrename 
 |-  ( ( B e. _V /\ j C_ B /\ k e. ( mzPoly ` j ) ) -> ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) e. ( mzPoly ` B ) )
108 101 97 91 107 syl3anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) e. ( mzPoly ` B ) )
109 mzpf 
 |-  ( ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) e. ( mzPoly ` B ) -> ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) : ( ZZ ^m B ) --> ZZ )
110 ffn 
 |-  ( ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) : ( ZZ ^m B ) --> ZZ -> ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) Fn ( ZZ ^m B ) )
111 108 109 110 3syl 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) Fn ( ZZ ^m B ) )
112 ofmpteq 
 |-  ( ( ( ZZ ^m B ) e. _V /\ ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) Fn ( ZZ ^m B ) /\ ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) Fn ( ZZ ^m B ) ) -> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( i ` ( d |` h ) ) + ( k ` ( d |` j ) ) ) ) )
113 100 106 111 112 syl3anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( i ` ( d |` h ) ) + ( k ` ( d |` j ) ) ) ) )
114 elmapi 
 |-  ( d e. ( ZZ ^m B ) -> d : B --> ZZ )
115 fssres 
 |-  ( ( d : B --> ZZ /\ ( h u. j ) C_ B ) -> ( d |` ( h u. j ) ) : ( h u. j ) --> ZZ )
116 114 98 115 syl2anr 
 |-  ( ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) /\ d e. ( ZZ ^m B ) ) -> ( d |` ( h u. j ) ) : ( h u. j ) --> ZZ )
117 zex 
 |-  ZZ e. _V
118 117 82 elmap 
 |-  ( ( d |` ( h u. j ) ) e. ( ZZ ^m ( h u. j ) ) <-> ( d |` ( h u. j ) ) : ( h u. j ) --> ZZ )
119 116 118 sylibr 
 |-  ( ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) /\ d e. ( ZZ ^m B ) ) -> ( d |` ( h u. j ) ) e. ( ZZ ^m ( h u. j ) ) )
120 reseq1 
 |-  ( l = ( d |` ( h u. j ) ) -> ( l |` h ) = ( ( d |` ( h u. j ) ) |` h ) )
121 120 fveq2d 
 |-  ( l = ( d |` ( h u. j ) ) -> ( i ` ( l |` h ) ) = ( i ` ( ( d |` ( h u. j ) ) |` h ) ) )
122 reseq1 
 |-  ( l = ( d |` ( h u. j ) ) -> ( l |` j ) = ( ( d |` ( h u. j ) ) |` j ) )
123 122 fveq2d 
 |-  ( l = ( d |` ( h u. j ) ) -> ( k ` ( l |` j ) ) = ( k ` ( ( d |` ( h u. j ) ) |` j ) ) )
124 121 123 oveq12d 
 |-  ( l = ( d |` ( h u. j ) ) -> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) = ( ( i ` ( ( d |` ( h u. j ) ) |` h ) ) + ( k ` ( ( d |` ( h u. j ) ) |` j ) ) ) )
125 eqid 
 |-  ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) = ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) )
126 ovex 
 |-  ( ( i ` ( ( d |` ( h u. j ) ) |` h ) ) + ( k ` ( ( d |` ( h u. j ) ) |` j ) ) ) e. _V
127 124 125 126 fvmpt 
 |-  ( ( d |` ( h u. j ) ) e. ( ZZ ^m ( h u. j ) ) -> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) = ( ( i ` ( ( d |` ( h u. j ) ) |` h ) ) + ( k ` ( ( d |` ( h u. j ) ) |` j ) ) ) )
128 119 127 syl 
 |-  ( ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) /\ d e. ( ZZ ^m B ) ) -> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) = ( ( i ` ( ( d |` ( h u. j ) ) |` h ) ) + ( k ` ( ( d |` ( h u. j ) ) |` j ) ) ) )
129 resabs1 
 |-  ( h C_ ( h u. j ) -> ( ( d |` ( h u. j ) ) |` h ) = ( d |` h ) )
130 84 129 ax-mp 
 |-  ( ( d |` ( h u. j ) ) |` h ) = ( d |` h )
131 130 fveq2i 
 |-  ( i ` ( ( d |` ( h u. j ) ) |` h ) ) = ( i ` ( d |` h ) )
132 resabs1 
 |-  ( j C_ ( h u. j ) -> ( ( d |` ( h u. j ) ) |` j ) = ( d |` j ) )
133 89 132 ax-mp 
 |-  ( ( d |` ( h u. j ) ) |` j ) = ( d |` j )
134 133 fveq2i 
 |-  ( k ` ( ( d |` ( h u. j ) ) |` j ) ) = ( k ` ( d |` j ) )
135 131 134 oveq12i 
 |-  ( ( i ` ( ( d |` ( h u. j ) ) |` h ) ) + ( k ` ( ( d |` ( h u. j ) ) |` j ) ) ) = ( ( i ` ( d |` h ) ) + ( k ` ( d |` j ) ) )
136 128 135 eqtr2di 
 |-  ( ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) /\ d e. ( ZZ ^m B ) ) -> ( ( i ` ( d |` h ) ) + ( k ` ( d |` j ) ) ) = ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) )
137 136 mpteq2dva 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( d e. ( ZZ ^m B ) |-> ( ( i ` ( d |` h ) ) + ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) )
138 113 137 eqtrd 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) )
139 fveq1 
 |-  ( b = ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) -> ( b ` ( d |` ( h u. j ) ) ) = ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) )
140 139 mpteq2dv 
 |-  ( b = ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) )
141 140 eqeq2d 
 |-  ( b = ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) -> ( ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) <-> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) ) )
142 141 anbi2d 
 |-  ( b = ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) -> ( ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) <-> ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) ) ) )
143 142 rspcev 
 |-  ( ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) e. ( mzPoly ` ( h u. j ) ) /\ ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) + ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) ) ) -> E. b e. ( mzPoly ` ( h u. j ) ) ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) )
144 95 98 138 143 syl12anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> E. b e. ( mzPoly ` ( h u. j ) ) ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) )
145 mzpmulmpt 
 |-  ( ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( i ` ( l |` h ) ) ) e. ( mzPoly ` ( h u. j ) ) /\ ( l e. ( ZZ ^m ( h u. j ) ) |-> ( k ` ( l |` j ) ) ) e. ( mzPoly ` ( h u. j ) ) ) -> ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) e. ( mzPoly ` ( h u. j ) ) )
146 88 93 145 syl2anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) e. ( mzPoly ` ( h u. j ) ) )
147 ofmpteq 
 |-  ( ( ( ZZ ^m B ) e. _V /\ ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) Fn ( ZZ ^m B ) /\ ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) Fn ( ZZ ^m B ) ) -> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( i ` ( d |` h ) ) x. ( k ` ( d |` j ) ) ) ) )
148 100 106 111 147 syl3anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( i ` ( d |` h ) ) x. ( k ` ( d |` j ) ) ) ) )
149 121 123 oveq12d 
 |-  ( l = ( d |` ( h u. j ) ) -> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) = ( ( i ` ( ( d |` ( h u. j ) ) |` h ) ) x. ( k ` ( ( d |` ( h u. j ) ) |` j ) ) ) )
150 eqid 
 |-  ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) = ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) )
151 ovex 
 |-  ( ( i ` ( ( d |` ( h u. j ) ) |` h ) ) x. ( k ` ( ( d |` ( h u. j ) ) |` j ) ) ) e. _V
152 149 150 151 fvmpt 
 |-  ( ( d |` ( h u. j ) ) e. ( ZZ ^m ( h u. j ) ) -> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) = ( ( i ` ( ( d |` ( h u. j ) ) |` h ) ) x. ( k ` ( ( d |` ( h u. j ) ) |` j ) ) ) )
153 119 152 syl 
 |-  ( ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) /\ d e. ( ZZ ^m B ) ) -> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) = ( ( i ` ( ( d |` ( h u. j ) ) |` h ) ) x. ( k ` ( ( d |` ( h u. j ) ) |` j ) ) ) )
154 131 134 oveq12i 
 |-  ( ( i ` ( ( d |` ( h u. j ) ) |` h ) ) x. ( k ` ( ( d |` ( h u. j ) ) |` j ) ) ) = ( ( i ` ( d |` h ) ) x. ( k ` ( d |` j ) ) )
155 153 154 eqtr2di 
 |-  ( ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) /\ d e. ( ZZ ^m B ) ) -> ( ( i ` ( d |` h ) ) x. ( k ` ( d |` j ) ) ) = ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) )
156 155 mpteq2dva 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( d e. ( ZZ ^m B ) |-> ( ( i ` ( d |` h ) ) x. ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) )
157 148 156 eqtrd 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) )
158 fveq1 
 |-  ( b = ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) -> ( b ` ( d |` ( h u. j ) ) ) = ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) )
159 158 mpteq2dv 
 |-  ( b = ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) )
160 159 eqeq2d 
 |-  ( b = ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) -> ( ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) <-> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) ) )
161 160 anbi2d 
 |-  ( b = ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) -> ( ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) <-> ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) ) ) )
162 161 rspcev 
 |-  ( ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) e. ( mzPoly ` ( h u. j ) ) /\ ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( ( l e. ( ZZ ^m ( h u. j ) ) |-> ( ( i ` ( l |` h ) ) x. ( k ` ( l |` j ) ) ) ) ` ( d |` ( h u. j ) ) ) ) ) ) -> E. b e. ( mzPoly ` ( h u. j ) ) ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) )
163 146 98 157 162 syl12anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> E. b e. ( mzPoly ` ( h u. j ) ) ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) )
164 fveq2 
 |-  ( a = ( h u. j ) -> ( mzPoly ` a ) = ( mzPoly ` ( h u. j ) ) )
165 sseq1 
 |-  ( a = ( h u. j ) -> ( a C_ B <-> ( h u. j ) C_ B ) )
166 reseq2 
 |-  ( a = ( h u. j ) -> ( d |` a ) = ( d |` ( h u. j ) ) )
167 166 fveq2d 
 |-  ( a = ( h u. j ) -> ( b ` ( d |` a ) ) = ( b ` ( d |` ( h u. j ) ) ) )
168 167 mpteq2dv 
 |-  ( a = ( h u. j ) -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) )
169 168 eqeq2d 
 |-  ( a = ( h u. j ) -> ( ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) )
170 165 169 anbi12d 
 |-  ( a = ( h u. j ) -> ( ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) ) )
171 164 170 rexeqbidv 
 |-  ( a = ( h u. j ) -> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. b e. ( mzPoly ` ( h u. j ) ) ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) ) )
172 168 eqeq2d 
 |-  ( a = ( h u. j ) -> ( ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) )
173 165 172 anbi12d 
 |-  ( a = ( h u. j ) -> ( ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) ) )
174 164 173 rexeqbidv 
 |-  ( a = ( h u. j ) -> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. b e. ( mzPoly ` ( h u. j ) ) ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) ) )
175 171 174 anbi12d 
 |-  ( a = ( h u. j ) -> ( ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) <-> ( E. b e. ( mzPoly ` ( h u. j ) ) ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) /\ E. b e. ( mzPoly ` ( h u. j ) ) ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) ) ) )
176 175 rspcev 
 |-  ( ( ( h u. j ) e. Fin /\ ( E. b e. ( mzPoly ` ( h u. j ) ) ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) /\ E. b e. ( mzPoly ` ( h u. j ) ) ( ( h u. j ) C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` ( h u. j ) ) ) ) ) ) ) -> E. a e. Fin ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
177 79 144 163 176 syl12anc 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ h C_ B ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> E. a e. Fin ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
178 177 adantlrr 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ j C_ B ) ) -> E. a e. Fin ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
179 178 adantrrr 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> E. a e. Fin ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
180 simplrr 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) )
181 simprrr 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) )
182 180 181 oveq12d 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( f oF + g ) = ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) )
183 182 eqeq1d 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
184 183 anbi2d 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
185 184 rexbidv 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
186 180 181 oveq12d 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( f oF x. g ) = ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) )
187 186 eqeq1d 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
188 187 anbi2d 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
189 188 rexbidv 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
190 185 189 anbi12d 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) <-> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) ) )
191 190 rexbidv 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( E. a e. Fin ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) <-> E. a e. Fin ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF + ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) oF x. ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) ) )
192 179 191 mpbird 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> E. a e. Fin ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
193 r19.40 
 |-  ( E. a e. Fin ( E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
194 192 193 syl 
 |-  ( ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) /\ ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
195 194 exp32 
 |-  ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) -> ( ( j e. Fin /\ k e. ( mzPoly ` j ) ) -> ( ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) ) ) )
196 195 rexlimdvv 
 |-  ( ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) /\ ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) -> ( E. j e. Fin E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) ) )
197 196 ex 
 |-  ( ( h e. Fin /\ i e. ( mzPoly ` h ) ) -> ( ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) -> ( E. j e. Fin E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) ) ) )
198 197 rexlimivv 
 |-  ( E. h e. Fin E. i e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) -> ( E. j e. Fin E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) ) )
199 198 imp 
 |-  ( ( E. h e. Fin E. i e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) /\ E. j e. Fin E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
200 199 ad2ant2l 
 |-  ( ( ( f : ( ZZ ^m B ) --> ZZ /\ E. h e. Fin E. i e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( g : ( ZZ ^m B ) --> ZZ /\ E. j e. Fin E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
201 200 3adant1 
 |-  ( ( T. /\ ( f : ( ZZ ^m B ) --> ZZ /\ E. h e. Fin E. i e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( g : ( ZZ ^m B ) --> ZZ /\ E. j e. Fin E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) /\ E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
202 201 simpld 
 |-  ( ( T. /\ ( f : ( ZZ ^m B ) --> ZZ /\ E. h e. Fin E. i e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( g : ( ZZ ^m B ) --> ZZ /\ E. j e. Fin E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
203 201 simprd 
 |-  ( ( T. /\ ( f : ( ZZ ^m B ) --> ZZ /\ E. h e. Fin E. i e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) /\ ( g : ( ZZ ^m B ) --> ZZ /\ E. j e. Fin E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
204 eqeq1 
 |-  ( e = ( ( ZZ ^m B ) X. { f } ) -> ( e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
205 204 anbi2d 
 |-  ( e = ( ( ZZ ^m B ) X. { f } ) -> ( ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( a C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
206 205 2rexbidv 
 |-  ( e = ( ( ZZ ^m B ) X. { f } ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( ( ZZ ^m B ) X. { f } ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
207 eqeq1 
 |-  ( e = ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) -> ( e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
208 207 anbi2d 
 |-  ( e = ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) -> ( ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( a C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
209 208 2rexbidv 
 |-  ( e = ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( g e. ( ZZ ^m B ) |-> ( g ` f ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
210 eqeq1 
 |-  ( e = f -> ( e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
211 210 anbi2d 
 |-  ( e = f -> ( ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( a C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
212 211 2rexbidv 
 |-  ( e = f -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
213 fveq2 
 |-  ( a = h -> ( mzPoly ` a ) = ( mzPoly ` h ) )
214 sseq1 
 |-  ( a = h -> ( a C_ B <-> h C_ B ) )
215 reseq2 
 |-  ( a = h -> ( d |` a ) = ( d |` h ) )
216 215 fveq2d 
 |-  ( a = h -> ( b ` ( d |` a ) ) = ( b ` ( d |` h ) ) )
217 216 mpteq2dv 
 |-  ( a = h -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` h ) ) ) )
218 217 eqeq2d 
 |-  ( a = h -> ( f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` h ) ) ) ) )
219 214 218 anbi12d 
 |-  ( a = h -> ( ( a C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` h ) ) ) ) ) )
220 213 219 rexeqbidv 
 |-  ( a = h -> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. b e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` h ) ) ) ) ) )
221 fveq1 
 |-  ( b = i -> ( b ` ( d |` h ) ) = ( i ` ( d |` h ) ) )
222 221 mpteq2dv 
 |-  ( b = i -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` h ) ) ) = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) )
223 222 eqeq2d 
 |-  ( b = i -> ( f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` h ) ) ) <-> f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) )
224 223 anbi2d 
 |-  ( b = i -> ( ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` h ) ) ) ) <-> ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) )
225 224 cbvrexvw 
 |-  ( E. b e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` h ) ) ) ) <-> E. i e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) )
226 220 225 bitrdi 
 |-  ( a = h -> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. i e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) )
227 226 cbvrexvw 
 |-  ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. h e. Fin E. i e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) )
228 212 227 bitrdi 
 |-  ( e = f -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. h e. Fin E. i e. ( mzPoly ` h ) ( h C_ B /\ f = ( d e. ( ZZ ^m B ) |-> ( i ` ( d |` h ) ) ) ) ) )
229 eqeq1 
 |-  ( e = g -> ( e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
230 229 anbi2d 
 |-  ( e = g -> ( ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( a C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
231 230 2rexbidv 
 |-  ( e = g -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
232 fveq2 
 |-  ( a = j -> ( mzPoly ` a ) = ( mzPoly ` j ) )
233 sseq1 
 |-  ( a = j -> ( a C_ B <-> j C_ B ) )
234 reseq2 
 |-  ( a = j -> ( d |` a ) = ( d |` j ) )
235 234 fveq2d 
 |-  ( a = j -> ( b ` ( d |` a ) ) = ( b ` ( d |` j ) ) )
236 235 mpteq2dv 
 |-  ( a = j -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` j ) ) ) )
237 236 eqeq2d 
 |-  ( a = j -> ( g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` j ) ) ) ) )
238 233 237 anbi12d 
 |-  ( a = j -> ( ( a C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` j ) ) ) ) ) )
239 232 238 rexeqbidv 
 |-  ( a = j -> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. b e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` j ) ) ) ) ) )
240 fveq1 
 |-  ( b = k -> ( b ` ( d |` j ) ) = ( k ` ( d |` j ) ) )
241 240 mpteq2dv 
 |-  ( b = k -> ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` j ) ) ) = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) )
242 241 eqeq2d 
 |-  ( b = k -> ( g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` j ) ) ) <-> g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) )
243 242 anbi2d 
 |-  ( b = k -> ( ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` j ) ) ) ) <-> ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) )
244 243 cbvrexvw 
 |-  ( E. b e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` j ) ) ) ) <-> E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) )
245 239 244 bitrdi 
 |-  ( a = j -> ( E. b e. ( mzPoly ` a ) ( a C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) )
246 245 cbvrexvw 
 |-  ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. j e. Fin E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) )
247 231 246 bitrdi 
 |-  ( e = g -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. j e. Fin E. k e. ( mzPoly ` j ) ( j C_ B /\ g = ( d e. ( ZZ ^m B ) |-> ( k ` ( d |` j ) ) ) ) ) )
248 eqeq1 
 |-  ( e = ( f oF + g ) -> ( e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
249 248 anbi2d 
 |-  ( e = ( f oF + g ) -> ( ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
250 249 2rexbidv 
 |-  ( e = ( f oF + g ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF + g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
251 eqeq1 
 |-  ( e = ( f oF x. g ) -> ( e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
252 251 anbi2d 
 |-  ( e = ( f oF x. g ) -> ( ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
253 252 2rexbidv 
 |-  ( e = ( f oF x. g ) -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ ( f oF x. g ) = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
254 eqeq1 
 |-  ( e = A -> ( e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> A = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
255 254 anbi2d 
 |-  ( e = A -> ( ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( a C_ B /\ A = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
256 255 2rexbidv 
 |-  ( e = A -> ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ e = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ A = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) ) )
257 34 75 202 203 206 209 228 247 250 253 256 mzpindd 
 |-  ( ( T. /\ A e. ( mzPoly ` B ) ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ A = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
258 2 257 mpan 
 |-  ( A e. ( mzPoly ` B ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ A = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) )
259 reseq1 
 |-  ( d = c -> ( d |` a ) = ( c |` a ) )
260 259 fveq2d 
 |-  ( d = c -> ( b ` ( d |` a ) ) = ( b ` ( c |` a ) ) )
261 260 cbvmptv 
 |-  ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) = ( c e. ( ZZ ^m B ) |-> ( b ` ( c |` a ) ) )
262 261 eqeq2i 
 |-  ( A = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) <-> A = ( c e. ( ZZ ^m B ) |-> ( b ` ( c |` a ) ) ) )
263 262 anbi2i 
 |-  ( ( a C_ B /\ A = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> ( a C_ B /\ A = ( c e. ( ZZ ^m B ) |-> ( b ` ( c |` a ) ) ) ) )
264 263 2rexbii 
 |-  ( E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ A = ( d e. ( ZZ ^m B ) |-> ( b ` ( d |` a ) ) ) ) <-> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ A = ( c e. ( ZZ ^m B ) |-> ( b ` ( c |` a ) ) ) ) )
265 258 264 sylib 
 |-  ( A e. ( mzPoly ` B ) -> E. a e. Fin E. b e. ( mzPoly ` a ) ( a C_ B /\ A = ( c e. ( ZZ ^m B ) |-> ( b ` ( c |` a ) ) ) ) )