Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mzpcompact2lem Unicode version

Theorem mzpcompact2lem 26932
Description: Lemma for mzpcompact2 26933. (Contributed by Stefan O'Rear, 9-Oct-2014.)
Hypothesis
Ref Expression
mzpcompact2lem.i  |-  B  e. 
_V
Assertion
Ref Expression
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 ) ) ) ) )
Distinct variable groups:    A, a,
b    B, a, b, c
Allowed substitution hint:    A( c)

Proof of Theorem mzpcompact2lem
Dummy variables  d 
e  f  g  h  i  j  k  l are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tru 1312 . . 3  |-  T.
2 0fin 7103 . . . . . 6  |-  (/)  e.  Fin
3 0ex 4166 . . . . . . . 8  |-  (/)  e.  _V
4 mzpconst 26916 . . . . . . . 8  |-  ( (
(/)  e.  _V  /\  f  e.  ZZ )  ->  (
( ZZ  ^m  (/) )  X. 
{ f } )  e.  (mzPoly `  (/) ) )
53, 4mpan 651 . . . . . . 7  |-  ( f  e.  ZZ  ->  (
( ZZ  ^m  (/) )  X. 
{ f } )  e.  (mzPoly `  (/) ) )
6 0ss 3496 . . . . . . . 8  |-  (/)  C_  B
76a1i 10 . . . . . . 7  |-  ( f  e.  ZZ  ->  (/)  C_  B
)
8 simpr 447 . . . . . . . . . . 11  |-  ( ( f  e.  ZZ  /\  d  e.  ( ZZ  ^m  B ) )  -> 
d  e.  ( ZZ 
^m  B ) )
9 elmapssres 26895 . . . . . . . . . . 11  |-  ( ( d  e.  ( ZZ 
^m  B )  /\  (/)  C_  B )  ->  (
d  |`  (/) )  e.  ( ZZ  ^m  (/) ) )
108, 6, 9sylancl 643 . . . . . . . . . 10  |-  ( ( f  e.  ZZ  /\  d  e.  ( ZZ  ^m  B ) )  -> 
( d  |`  (/) )  e.  ( ZZ  ^m  (/) ) )
11 vex 2804 . . . . . . . . . . 11  |-  f  e. 
_V
1211fvconst2 5745 . . . . . . . . . 10  |-  ( ( d  |`  (/) )  e.  ( ZZ  ^m  (/) )  -> 
( ( ( ZZ 
^m  (/) )  X.  {
f } ) `  ( d  |`  (/) ) )  =  f )
1310, 12syl 15 . . . . . . . . 9  |-  ( ( f  e.  ZZ  /\  d  e.  ( ZZ  ^m  B ) )  -> 
( ( ( ZZ 
^m  (/) )  X.  {
f } ) `  ( d  |`  (/) ) )  =  f )
1413mpteq2dva 4122 . . . . . . . 8  |-  ( f  e.  ZZ  ->  (
d  e.  ( ZZ 
^m  B )  |->  ( ( ( ZZ  ^m  (/) )  X.  { f } ) `  (
d  |`  (/) ) ) )  =  ( d  e.  ( ZZ  ^m  B
)  |->  f ) )
15 fconstmpt 4748 . . . . . . . 8  |-  ( ( ZZ  ^m  B )  X.  { f } )  =  ( d  e.  ( ZZ  ^m  B )  |->  f )
1614, 15syl6reqr 2347 . . . . . . 7  |-  ( f  e.  ZZ  ->  (
( ZZ  ^m  B
)  X.  { f } )  =  ( d  e.  ( ZZ 
^m  B )  |->  ( ( ( ZZ  ^m  (/) )  X.  { f } ) `  (
d  |`  (/) ) ) ) )
17 fveq1 5540 . . . . . . . . . . 11  |-  ( b  =  ( ( ZZ 
^m  (/) )  X.  {
f } )  -> 
( b `  (
d  |`  (/) ) )  =  ( ( ( ZZ 
^m  (/) )  X.  {
f } ) `  ( d  |`  (/) ) ) )
1817mpteq2dv 4123 . . . . . . . . . 10  |-  ( b  =  ( ( ZZ 
^m  (/) )  X.  {
f } )  -> 
( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  (/) ) ) )  =  ( d  e.  ( ZZ  ^m  B
)  |->  ( ( ( ZZ  ^m  (/) )  X. 
{ f } ) `
 ( d  |`  (/) ) ) ) )
1918eqeq2d 2307 . . . . . . . . 9  |-  ( 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  |`  (/) ) ) ) ) )
2019anbi2d 684 . . . . . . . 8  |-  ( 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  |`  (/) ) ) ) ) ) )
2120rspcev 2897 . . . . . . 7  |-  ( ( ( ( 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  |`  (/) ) ) ) ) )
225, 7, 16, 21syl12anc 1180 . . . . . 6  |-  ( f  e.  ZZ  ->  E. b  e.  (mzPoly `  (/) ) (
(/)  C_  B  /\  (
( ZZ  ^m  B
)  X.  { f } )  =  ( d  e.  ( ZZ 
^m  B )  |->  ( b `  ( d  |`  (/) ) ) ) ) )
23 fveq2 5541 . . . . . . . 8  |-  ( a  =  (/)  ->  (mzPoly `  a )  =  (mzPoly `  (/) ) )
24 sseq1 3212 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( a 
C_  B  <->  (/)  C_  B
) )
25 reseq2 4966 . . . . . . . . . . . 12  |-  ( a  =  (/)  ->  ( d  |`  a )  =  ( d  |`  (/) ) )
2625fveq2d 5545 . . . . . . . . . . 11  |-  ( a  =  (/)  ->  ( b `
 ( d  |`  a ) )  =  ( b `  (
d  |`  (/) ) ) )
2726mpteq2dv 4123 . . . . . . . . . 10  |-  ( a  =  (/)  ->  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) )  =  ( d  e.  ( ZZ  ^m  B
)  |->  ( b `  ( d  |`  (/) ) ) ) )
2827eqeq2d 2307 . . . . . . . . 9  |-  ( 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  |`  (/) ) ) ) ) )
2924, 28anbi12d 691 . . . . . . . 8  |-  ( 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  |`  (/) ) ) ) ) ) )
3023, 29rexeqbidv 2762 . . . . . . 7  |-  ( 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  |`  (/) ) ) ) ) ) )
3130rspcev 2897 . . . . . 6  |-  ( (
(/)  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 ) ) ) ) )
322, 22, 31sylancr 644 . . . . 5  |-  ( 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 ) ) ) ) )
3332adantl 452 . . . 4  |-  ( (  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 ) ) ) ) )
34 snfi 6957 . . . . . 6  |-  { f }  e.  Fin
35 snex 4232 . . . . . . . . 9  |-  { f }  e.  _V
3611snid 3680 . . . . . . . . 9  |-  f  e. 
{ f }
37 mzpproj 26918 . . . . . . . . 9  |-  ( ( { f }  e.  _V  /\  f  e.  {
f } )  -> 
( g  e.  ( ZZ  ^m  { f } )  |->  ( g `
 f ) )  e.  (mzPoly `  {
f } ) )
3835, 36, 37mp2an 653 . . . . . . . 8  |-  ( g  e.  ( ZZ  ^m  { f } )  |->  ( g `  f ) )  e.  (mzPoly `  { f } )
3938a1i 10 . . . . . . 7  |-  ( f  e.  B  ->  (
g  e.  ( ZZ 
^m  { f } )  |->  ( g `  f ) )  e.  (mzPoly `  { f } ) )
40 snssi 3775 . . . . . . 7  |-  ( f  e.  B  ->  { f }  C_  B )
41 fveq1 5540 . . . . . . . . 9  |-  ( g  =  d  ->  (
g `  f )  =  ( d `  f ) )
4241cbvmptv 4127 . . . . . . . 8  |-  ( g  e.  ( ZZ  ^m  B )  |->  ( g `
 f ) )  =  ( d  e.  ( ZZ  ^m  B
)  |->  ( d `  f ) )
43 simpr 447 . . . . . . . . . . . 12  |-  ( ( f  e.  B  /\  d  e.  ( ZZ  ^m  B ) )  -> 
d  e.  ( ZZ 
^m  B ) )
44 simpl 443 . . . . . . . . . . . . 13  |-  ( ( f  e.  B  /\  d  e.  ( ZZ  ^m  B ) )  -> 
f  e.  B )
4544snssd 3776 . . . . . . . . . . . 12  |-  ( ( f  e.  B  /\  d  e.  ( ZZ  ^m  B ) )  ->  { f }  C_  B )
46 elmapssres 26895 . . . . . . . . . . . 12  |-  ( ( d  e.  ( ZZ 
^m  B )  /\  { f }  C_  B
)  ->  ( d  |` 
{ f } )  e.  ( ZZ  ^m  { f } ) )
4743, 45, 46syl2anc 642 . . . . . . . . . . 11  |-  ( ( f  e.  B  /\  d  e.  ( ZZ  ^m  B ) )  -> 
( d  |`  { f } )  e.  ( ZZ  ^m  { f } ) )
48 fveq1 5540 . . . . . . . . . . . 12  |-  ( g  =  ( d  |`  { f } )  ->  ( g `  f )  =  ( ( d  |`  { f } ) `  f
) )
49 eqid 2296 . . . . . . . . . . . 12  |-  ( g  e.  ( ZZ  ^m  { f } )  |->  ( g `  f ) )  =  ( g  e.  ( ZZ  ^m  { f } )  |->  ( g `  f ) )
50 fvex 5555 . . . . . . . . . . . 12  |-  ( ( d  |`  { f } ) `  f
)  e.  _V
5148, 49, 50fvmpt 5618 . . . . . . . . . . 11  |-  ( ( d  |`  { f } )  e.  ( ZZ  ^m  { f } )  ->  (
( g  e.  ( ZZ  ^m  { f } )  |->  ( g `
 f ) ) `
 ( d  |`  { f } ) )  =  ( ( d  |`  { f } ) `  f
) )
5247, 51syl 15 . . . . . . . . . 10  |-  ( ( f  e.  B  /\  d  e.  ( ZZ  ^m  B ) )  -> 
( ( g  e.  ( ZZ  ^m  {
f } )  |->  ( g `  f ) ) `  ( d  |`  { f } ) )  =  ( ( d  |`  { f } ) `  f
) )
53 fvres 5558 . . . . . . . . . . 11  |-  ( f  e.  { f }  ->  ( ( d  |`  { f } ) `
 f )  =  ( d `  f
) )
5436, 53ax-mp 8 . . . . . . . . . 10  |-  ( ( d  |`  { f } ) `  f
)  =  ( d `
 f )
5552, 54syl6req 2345 . . . . . . . . 9  |-  ( ( f  e.  B  /\  d  e.  ( ZZ  ^m  B ) )  -> 
( d `  f
)  =  ( ( g  e.  ( ZZ 
^m  { f } )  |->  ( g `  f ) ) `  ( d  |`  { f } ) ) )
5655mpteq2dva 4122 . . . . . . . 8  |-  ( f  e.  B  ->  (
d  e.  ( ZZ 
^m  B )  |->  ( d `  f ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( ( g  e.  ( ZZ 
^m  { f } )  |->  ( g `  f ) ) `  ( d  |`  { f } ) ) ) )
5742, 56syl5eq 2340 . . . . . . 7  |-  ( f  e.  B  ->  (
g  e.  ( ZZ 
^m  B )  |->  ( g `  f ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( ( g  e.  ( ZZ 
^m  { f } )  |->  ( g `  f ) ) `  ( d  |`  { f } ) ) ) )
58 fveq1 5540 . . . . . . . . . . 11  |-  ( b  =  ( g  e.  ( ZZ  ^m  {
f } )  |->  ( g `  f ) )  ->  ( b `  ( d  |`  { f } ) )  =  ( ( g  e.  ( ZZ  ^m  {
f } )  |->  ( g `  f ) ) `  ( d  |`  { f } ) ) )
5958mpteq2dv 4123 . . . . . . . . . 10  |-  ( 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 } ) ) ) )
6059eqeq2d 2307 . . . . . . . . 9  |-  ( 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 } ) ) ) ) )
6160anbi2d 684 . . . . . . . 8  |-  ( 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 } ) ) ) ) ) )
6261rspcev 2897 . . . . . . 7  |-  ( ( ( 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 } ) ) ) ) )
6339, 40, 57, 62syl12anc 1180 . . . . . 6  |-  ( 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 } ) ) ) ) )
64 fveq2 5541 . . . . . . . 8  |-  ( a  =  { f }  ->  (mzPoly `  a )  =  (mzPoly `  { f } ) )
65 sseq1 3212 . . . . . . . . 9  |-  ( a  =  { f }  ->  ( a  C_  B 
<->  { f }  C_  B ) )
66 reseq2 4966 . . . . . . . . . . . 12  |-  ( a  =  { f }  ->  ( d  |`  a )  =  ( d  |`  { f } ) )
6766fveq2d 5545 . . . . . . . . . . 11  |-  ( a  =  { f }  ->  ( b `  ( d  |`  a
) )  =  ( b `  ( d  |`  { f } ) ) )
6867mpteq2dv 4123 . . . . . . . . . 10  |-  ( a  =  { f }  ->  ( d  e.  ( ZZ  ^m  B
)  |->  ( b `  ( d  |`  a
) ) )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  { f } ) ) ) )
6968eqeq2d 2307 . . . . . . . . 9  |-  ( 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 } ) ) ) ) )
7065, 69anbi12d 691 . . . . . . . 8  |-  ( 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 } ) ) ) ) ) )
7164, 70rexeqbidv 2762 . . . . . . 7  |-  ( 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 } ) ) ) ) ) )
7271rspcev 2897 . . . . . 6  |-  ( ( { 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 ) ) ) ) )
7334, 63, 72sylancr 644 . . . . 5  |-  ( 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 ) ) ) ) )
7473adantl 452 . . . 4  |-  ( (  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 ) ) ) ) )
75 simplll 734 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( h  e. 
Fin  /\  i  e.  (mzPoly `  h ) )  /\  h  C_  B
)  /\  ( (
j  e.  Fin  /\  k  e.  (mzPoly `  j
) )  /\  j  C_  B ) )  ->  h  e.  Fin )
76 simprll 738 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( h  e. 
Fin  /\  i  e.  (mzPoly `  h ) )  /\  h  C_  B
)  /\  ( (
j  e.  Fin  /\  k  e.  (mzPoly `  j
) )  /\  j  C_  B ) )  -> 
j  e.  Fin )
77 unfi 7140 . . . . . . . . . . . . . . . . . 18  |-  ( ( h  e.  Fin  /\  j  e.  Fin )  ->  ( h  u.  j
)  e.  Fin )
7875, 76, 77syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
79 vex 2804 . . . . . . . . . . . . . . . . . . . . . 22  |-  h  e. 
_V
80 vex 2804 . . . . . . . . . . . . . . . . . . . . . 22  |-  j  e. 
_V
8179, 80unex 4534 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  u.  j )  e. 
_V
8281a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
83 ssun1 3351 . . . . . . . . . . . . . . . . . . . . 21  |-  h  C_  ( h  u.  j
)
8483a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) )
85 simpllr 735 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( h  e. 
Fin  /\  i  e.  (mzPoly `  h ) )  /\  h  C_  B
)  /\  ( (
j  e.  Fin  /\  k  e.  (mzPoly `  j
) )  /\  j  C_  B ) )  -> 
i  e.  (mzPoly `  h ) )
86 mzpresrename 26931 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )
8782, 84, 85, 86syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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
) ) )
88 ssun2 3352 . . . . . . . . . . . . . . . . . . . . 21  |-  j  C_  ( h  u.  j
)
8988a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) )
90 simprlr 739 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( h  e. 
Fin  /\  i  e.  (mzPoly `  h ) )  /\  h  C_  B
)  /\  ( (
j  e.  Fin  /\  k  e.  (mzPoly `  j
) )  /\  j  C_  B ) )  -> 
k  e.  (mzPoly `  j ) )
91 mzpresrename 26931 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )
9282, 89, 90, 91syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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
) ) )
93 mzpaddmpt 26922 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) )
9487, 92, 93syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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
) ) )
95 simplr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( h  e. 
Fin  /\  i  e.  (mzPoly `  h ) )  /\  h  C_  B
)  /\  ( (
j  e.  Fin  /\  k  e.  (mzPoly `  j
) )  /\  j  C_  B ) )  ->  h  C_  B )
96 simprr 733 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( h  e. 
Fin  /\  i  e.  (mzPoly `  h ) )  /\  h  C_  B
)  /\  ( (
j  e.  Fin  /\  k  e.  (mzPoly `  j
) )  /\  j  C_  B ) )  -> 
j  C_  B )
9795, 96unssd 3364 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
98 ovex 5899 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ZZ 
^m  B )  e. 
_V
9998a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
100 mzpcompact2lem.i . . . . . . . . . . . . . . . . . . . . . . 23  |-  B  e. 
_V
101100a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 26931 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( B  e.  _V  /\  h  C_  B  /\  i  e.  (mzPoly `  h )
)  ->  ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  e.  (mzPoly `  B )
)
103101, 95, 85, 102syl3anc 1182 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 26917 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 5405 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( d  e.  ( ZZ 
^m  B )  |->  ( i `  ( d  |`  h ) ) ) : ( ZZ  ^m  B ) --> ZZ  ->  ( d  e.  ( ZZ 
^m  B )  |->  ( i `  ( d  |`  h ) ) )  Fn  ( ZZ  ^m  B ) )
106103, 104, 1053syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 26931 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( B  e.  _V  /\  j  C_  B  /\  k  e.  (mzPoly `  j )
)  ->  ( d  e.  ( ZZ  ^m  B
)  |->  ( k `  ( d  |`  j
) ) )  e.  (mzPoly `  B )
)
108101, 96, 90, 107syl3anc 1182 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 26917 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 5405 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( d  e.  ( ZZ 
^m  B )  |->  ( k `  ( d  |`  j ) ) ) : ( ZZ  ^m  B ) --> ZZ  ->  ( d  e.  ( ZZ 
^m  B )  |->  ( k `  ( d  |`  j ) ) )  Fn  ( ZZ  ^m  B ) )
111108, 109, 1103syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 26900 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )  o F  +  ( d  e.  ( ZZ 
^m  B )  |->  ( k `  ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( ( i `  ( d  |`  h ) )  +  ( k `  (
d  |`  j ) ) ) ) )
11399, 106, 111, 112syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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
) ) )  o F  +  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( ( i `  ( d  |`  h ) )  +  ( k `  (
d  |`  j ) ) ) ) )
114 elmapi 6808 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( d  e.  ( ZZ  ^m  B )  ->  d : B --> ZZ )
115 fssres 5424 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( d : B --> ZZ  /\  ( h  u.  j
)  C_  B )  ->  ( d  |`  (
h  u.  j ) ) : ( h  u.  j ) --> ZZ )
116114, 97, 115syl2anr 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 10049 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ZZ  e.  _V
118117, 81elmap 6812 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( d  |`  ( h  u.  j ) )  e.  ( ZZ  ^m  (
h  u.  j ) )  <->  ( d  |`  ( h  u.  j
) ) : ( h  u.  j ) --> ZZ )
119116, 118sylibr 203 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 4965 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( l  =  ( d  |`  ( h  u.  j
) )  ->  (
l  |`  h )  =  ( ( d  |`  ( h  u.  j
) )  |`  h
) )
121120fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( l  =  ( d  |`  ( h  u.  j
) )  ->  (
i `  ( l  |`  h ) )  =  ( i `  (
( d  |`  (
h  u.  j ) )  |`  h )
) )
122 reseq1 4965 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( l  =  ( d  |`  ( h  u.  j
) )  ->  (
l  |`  j )  =  ( ( d  |`  ( h  u.  j
) )  |`  j
) )
123122fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( l  =  ( d  |`  ( h  u.  j
) )  ->  (
k `  ( l  |`  j ) )  =  ( k `  (
( d  |`  (
h  u.  j ) )  |`  j )
) )
124121, 123oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 2296 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 5899 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i `  ( ( d  |`  ( h  u.  j ) )  |`  h ) )  +  ( k `  (
( d  |`  (
h  u.  j ) )  |`  j )
) )  e.  _V
127124, 125, 126fvmpt 5618 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 ) ) ) )
128119, 127syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 5000 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( h 
C_  ( h  u.  j )  ->  (
( d  |`  (
h  u.  j ) )  |`  h )  =  ( d  |`  h ) )
13083, 129ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( d  |`  ( h  u.  j ) )  |`  h )  =  ( d  |`  h )
131130fveq2i 5544 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i `
 ( ( d  |`  ( h  u.  j
) )  |`  h
) )  =  ( i `  ( d  |`  h ) )
132 resabs1 5000 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j 
C_  ( h  u.  j )  ->  (
( d  |`  (
h  u.  j ) )  |`  j )  =  ( d  |`  j ) )
13388, 132ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( d  |`  ( h  u.  j ) )  |`  j )  =  ( d  |`  j )
134133fveq2i 5544 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k `
 ( ( d  |`  ( h  u.  j
) )  |`  j
) )  =  ( k `  ( d  |`  j ) )
135131, 134oveq12i 5886 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i `  ( ( d  |`  ( h  u.  j ) )  |`  h ) )  +  ( k `  (
( d  |`  (
h  u.  j ) )  |`  j )
) )  =  ( ( i `  (
d  |`  h ) )  +  ( k `  ( d  |`  j
) ) )
136128, 135syl6req 2345 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 ) ) ) )
137136mpteq2dva 4122 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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
) ) ) ) )
138113, 137eqtrd 2328 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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
) ) )  o F  +  ( 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 5540 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) )
140139mpteq2dv 4123 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) ) )
141140eqeq2d 2307 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  ( l  e.  ( ZZ  ^m  (
h  u.  j ) )  |->  ( ( i `
 ( l  |`  h ) )  +  ( k `  (
l  |`  j ) ) ) )  ->  (
( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  +  ( 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
) ) )  o F  +  ( 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
) ) ) ) ) )
142141anbi2d 684 . . . . . . . . . . . . . . . . . . 19  |-  ( 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
) ) )  o F  +  ( 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 ) ) )  o F  +  ( 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
) ) ) ) ) ) )
143142rspcev 2897 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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
) ) )  o F  +  ( 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
) ) )  o F  +  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  ( h  u.  j
) ) ) ) ) )
14494, 97, 138, 143syl12anc 1180 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) )  o F  +  ( d  e.  ( ZZ  ^m  B ) 
|->  ( k `  (
d  |`  j ) ) ) )  =  ( d  e.  ( ZZ 
^m  B )  |->  ( b `  ( d  |`  ( h  u.  j
) ) ) ) ) )
145 mzpmulmpt 26923 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) ) )
14687, 92, 145syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 26900 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )  o F  x.  (
d  e.  ( ZZ 
^m  B )  |->  ( k `  ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( ( i `  ( d  |`  h ) )  x.  ( k `  (
d  |`  j ) ) ) ) )
14899, 106, 111, 147syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( ( i `  ( d  |`  h ) )  x.  ( k `  (
d  |`  j ) ) ) ) )
149121, 123oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 2296 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 5899 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i `  ( ( d  |`  ( h  u.  j ) )  |`  h ) )  x.  ( k `  (
( d  |`  (
h  u.  j ) )  |`  j )
) )  e.  _V
152149, 150, 151fvmpt 5618 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 ) ) ) )
153119, 152syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 ) ) ) )
154131, 134oveq12i 5886 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i `  ( ( d  |`  ( h  u.  j ) )  |`  h ) )  x.  ( k `  (
( d  |`  (
h  u.  j ) )  |`  j )
) )  =  ( ( i `  (
d  |`  h ) )  x.  ( k `  ( d  |`  j
) ) )
155153, 154syl6req 2345 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 ) ) ) )
156155mpteq2dva 4122 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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
) ) ) ) )
157148, 156eqtrd 2328 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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
) ) )  o F  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 5540 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) )
159158mpteq2dv 4123 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) ) )
160159eqeq2d 2307 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  ( l  e.  ( ZZ  ^m  (
h  u.  j ) )  |->  ( ( i `
 ( l  |`  h ) )  x.  ( k `  (
l  |`  j ) ) ) )  ->  (
( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  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
) ) )  o F  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
) ) ) ) ) )
161160anbi2d 684 . . . . . . . . . . . . . . . . . . 19  |-  ( 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
) ) )  o F  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 ) ) )  o F  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
) ) ) ) ) ) )
162161rspcev 2897 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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
) ) )  o F  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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  ( h  u.  j
) ) ) ) ) )
163146, 97, 157, 162syl12anc 1180 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B ) 
|->  ( k `  (
d  |`  j ) ) ) )  =  ( d  e.  ( ZZ 
^m  B )  |->  ( b `  ( d  |`  ( h  u.  j
) ) ) ) ) )
164 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( h  u.  j )  ->  (mzPoly `  a )  =  (mzPoly `  ( h  u.  j
) ) )
165 sseq1 3212 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( h  u.  j )  ->  (
a  C_  B  <->  ( h  u.  j )  C_  B
) )
166 reseq2 4966 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  ( h  u.  j )  ->  (
d  |`  a )  =  ( d  |`  (
h  u.  j ) ) )
167166fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  ( h  u.  j )  ->  (
b `  ( d  |`  a ) )  =  ( b `  (
d  |`  ( h  u.  j ) ) ) )
168167mpteq2dv 4123 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  ( h  u.  j )  ->  (
d  e.  ( ZZ 
^m  B )  |->  ( b `  ( d  |`  a ) ) )  =  ( d  e.  ( ZZ  ^m  B
)  |->  ( b `  ( d  |`  (
h  u.  j ) ) ) ) )
169168eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( h  u.  j )  ->  (
( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  +  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) )  <-> 
( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  +  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  ( h  u.  j
) ) ) ) ) )
170165, 169anbi12d 691 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( h  u.  j )  ->  (
( a  C_  B  /\  ( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  +  ( 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 ) ) )  o F  +  ( d  e.  ( ZZ 
^m  B )  |->  ( k `  ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  ( h  u.  j
) ) ) ) ) ) )
171164, 170rexeqbidv 2762 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( h  u.  j )  ->  ( E. b  e.  (mzPoly `  a ) ( a 
C_  B  /\  (
( d  e.  ( ZZ  ^m  B ) 
|->  ( i `  (
d  |`  h ) ) )  o F  +  ( 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 ) ) )  o F  +  ( d  e.  ( ZZ  ^m  B ) 
|->  ( k `  (
d  |`  j ) ) ) )  =  ( d  e.  ( ZZ 
^m  B )  |->  ( b `  ( d  |`  ( h  u.  j
) ) ) ) ) ) )
172168eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( h  u.  j )  ->  (
( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  ( h  u.  j
) ) ) ) ) )
173165, 172anbi12d 691 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( h  u.  j )  ->  (
( a  C_  B  /\  ( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  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 ) ) )  o F  x.  (
d  e.  ( ZZ 
^m  B )  |->  ( k `  ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  ( h  u.  j
) ) ) ) ) ) )
174164, 173rexeqbidv 2762 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( h  u.  j )  ->  ( E. b  e.  (mzPoly `  a ) ( a 
C_  B  /\  (
( d  e.  ( ZZ  ^m  B ) 
|->  ( i `  (
d  |`  h ) ) )  o F  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 ) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B ) 
|->  ( k `  (
d  |`  j ) ) ) )  =  ( d  e.  ( ZZ 
^m  B )  |->  ( b `  ( d  |`  ( h  u.  j
) ) ) ) ) ) )
175171, 174anbi12d 691 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( h  u.  j )  ->  (
( E. b  e.  (mzPoly `  a )
( a  C_  B  /\  ( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  +  ( 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
) ) )  o F  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 ) ) )  o F  +  ( 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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  ( h  u.  j
) ) ) ) ) ) ) )
176175rspcev 2897 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) )  o F  +  ( 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
) ) )  o F  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 ) ) )  o F  +  ( 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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) ) )
17778, 144, 163, 176syl12anc 1180 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) ) )  o F  +  ( 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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) ) )
178177adantlrr 701 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) ) )  o F  +  ( 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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) ) )
179178adantrrr 705 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) )  o F  +  ( 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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) ) )
180 simplrr 737 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 741 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) ) ) )
182180, 181oveq12d 5892 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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  o F  +  g )  =  ( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  +  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) ) )
183182eqeq1d 2304 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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  o F  +  g )  =  ( d  e.  ( ZZ  ^m  B
)  |->  ( b `  ( d  |`  a
) ) )  <->  ( (
d  e.  ( ZZ 
^m  B )  |->  ( i `  ( d  |`  h ) ) )  o F  +  ( d  e.  ( ZZ 
^m  B )  |->  ( k `  ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) )
184183anbi2d 684 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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  o F  +  g )  =  ( d  e.  ( ZZ  ^m  B
)  |->  ( b `  ( d  |`  a
) ) ) )  <-> 
( a  C_  B  /\  ( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  +  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) ) )
185184rexbidv 2577 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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  o F  +  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
) ) )  o F  +  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) ) )
186180, 181oveq12d 5892 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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  o F  x.  g )  =  ( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) ) )
187186eqeq1d 2304 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B
)  |->  ( b `  ( d  |`  a
) ) )  <->  ( (
d  e.  ( ZZ 
^m  B )  |->  ( i `  ( d  |`  h ) ) )  o F  x.  (
d  e.  ( ZZ 
^m  B )  |->  ( k `  ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) )
188187anbi2d 684 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B
)  |->  ( b `  ( d  |`  a
) ) ) )  <-> 
( a  C_  B  /\  ( ( d  e.  ( ZZ  ^m  B
)  |->  ( i `  ( d  |`  h
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) ) )
189188rexbidv 2577 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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  o F  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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) ) )
190185, 189anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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  o F  +  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) )  /\  E. b  e.  (mzPoly `  a
) ( a  C_  B  /\  ( f  o F  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
) ) )  o F  +  ( 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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) ) ) )
191190rexbidv 2577 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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  o F  +  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) )  /\  E. b  e.  (mzPoly `  a
) ( a  C_  B  /\  ( f  o F  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 ) ) )  o F  +  ( 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
) ) )  o F  x.  ( d  e.  ( ZZ  ^m  B )  |->  ( k `
 ( d  |`  j ) ) ) )  =  ( d  e.  ( ZZ  ^m  B )  |->  ( b `
 ( d  |`  a ) ) ) ) ) ) )
192179, 191mpbird 223 . . . . . . . . . . . . 13  |-  ( ( ( ( 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  o F  +  g )  =  ( d  e.  ( ZZ 
^m  B )  |->  ( b `  ( d  |`  a ) ) ) )  /\  E. b  e.  (mzPoly `  a )
( a  C_  B  /\  ( f  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) ) ) )
193 r19.40 2704 . . . . . . . . . . . . 13  |-  ( E. a  e.  Fin  ( E. b  e.  (mzPoly `  a ) ( a 
C_  B  /\  (
f  o F  +  g )  =  ( d  e.  ( ZZ 
^m  B )  |->  ( b `  ( d  |`  a ) ) ) )  /\  E. b  e.  (mzPoly `  a )
( a  C_  B  /\  ( f  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) ) )  -> 
( E. a  e. 
Fin  E. b  e.  (mzPoly `  a ) ( a 
C_  B  /\  (
f  o F  +  g )  =  ( d  e.  ( ZZ 
^m  B )  |->  ( b `  ( d  |`  a ) ) ) )  /\  E. a  e.  Fin  E. b  e.  (mzPoly `  a )
( a  C_  B  /\  ( f  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) ) ) )
194192, 193syl 15 . . . . . . . . . . . 12  |-  ( ( ( ( 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  o F  +  g )  =  ( d  e.  ( ZZ 
^m  B )  |->  ( b `  ( d  |`  a ) ) ) )  /\  E. a  e.  Fin  E. b  e.  (mzPoly `  a )
( a  C_  B  /\  ( f  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) ) ) )
195194exp32 588 . . . . . . . . . . 11  |-  ( ( ( 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  o F  +  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) )  /\  E. a  e.  Fin  E. b  e.  (mzPoly `  a )
( a  C_  B  /\  ( f  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) ) ) ) ) )
196195rexlimdvv 2686 . . . . . . . . . 10  |-  ( ( ( 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  o F  +  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) )  /\  E. a  e.  Fin  E. b  e.  (mzPoly `  a )
( a  C_  B  /\  ( f  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) ) ) ) )
197196ex 423 . . . . . . . . 9  |-  ( ( 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  o F  +  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) )  /\  E. a  e.  Fin  E. b  e.  (mzPoly `  a )
( a  C_  B  /\  ( f  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) ) ) ) ) )
198197rexlimivv 2685 . . . . . . . 8  |-  ( 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  o F  +  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) )  /\  E. a  e.  Fin  E. b  e.  (mzPoly `  a )
( a  C_  B  /\  ( f  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) ) ) ) )
199198imp 418 . . . . . . 7  |-  ( ( 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  o F  +  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) )  /\  E. a  e.  Fin  E. b  e.  (mzPoly `  a )
( a  C_  B  /\  ( f  o F  x.  g )  =  ( d  e.  ( ZZ  ^m  B ) 
|->  ( b `  (
d  |`  a ) ) ) ) ) )
200199ad2ant2l 726 . . . . . 6  |-  ( ( ( 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.