MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mdetunilem9 Structured version   Unicode version

Theorem mdetunilem9 18989
Description: Lemma for mdetuni 18991. (Contributed by SO, 15-Jul-2018.)
Hypotheses
Ref Expression
mdetuni.a  |-  A  =  ( N Mat  R )
mdetuni.b  |-  B  =  ( Base `  A
)
mdetuni.k  |-  K  =  ( Base `  R
)
mdetuni.0g  |-  .0.  =  ( 0g `  R )
mdetuni.1r  |-  .1.  =  ( 1r `  R )
mdetuni.pg  |-  .+  =  ( +g  `  R )
mdetuni.tg  |-  .x.  =  ( .r `  R )
mdetuni.n  |-  ( ph  ->  N  e.  Fin )
mdetuni.r  |-  ( ph  ->  R  e.  Ring )
mdetuni.ff  |-  ( ph  ->  D : B --> K )
mdetuni.al  |-  ( ph  ->  A. x  e.  B  A. y  e.  N  A. z  e.  N  ( ( y  =/=  z  /\  A. w  e.  N  ( y
x w )  =  ( z x w ) )  ->  ( D `  x )  =  .0.  ) )
mdetuni.li  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. w  e.  N  ( ( ( x  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( ( D `  y
)  .+  ( D `  z ) ) ) )
mdetuni.sc  |-  ( ph  ->  A. x  e.  B  A. y  e.  K  A. z  e.  B  A. w  e.  N  ( ( ( x  |`  ( { w }  X.  N ) )  =  ( ( ( { w }  X.  N
)  X.  { y } )  oF  .x.  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( y  .x.  ( D `
 z ) ) ) )
mdetunilem9.id  |-  ( ph  ->  ( D `  ( 1r `  A ) )  =  .0.  )
mdetunilem9.y  |-  Y  =  { x  |  A. y  e.  B  A. z  e.  ( N  ^m  N ) ( A. w  e.  x  (
y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `
 y )  =  .0.  ) }
Assertion
Ref Expression
mdetunilem9  |-  ( ph  ->  D  =  ( B  X.  {  .0.  }
) )
Distinct variable groups:    ph, x, y, z, w    x, B, y, z, w    x, K, y, z, w    x, N, y, z, w    x, D, y, z, w    x,  .x. , y, z, w    x,  .+ , y, z, w    x,  .0. , y, z, w    x,  .1. , y, z, w    x, R, y, z, w    x, A, y, z, w
Allowed substitution hints:    Y( x, y, z, w)

Proof of Theorem mdetunilem9
Dummy variables  a 
b  c  d  e are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ral0 3915 . . . 4  |-  A. w  e.  (/)  ( a `  w )  =  if ( w  e.  (  _I  |`  N ) ,  .1.  ,  .0.  )
2 simpr 461 . . . . 5  |-  ( (
ph  /\  a  e.  B )  ->  a  e.  B )
3 f1oi 5837 . . . . . . . 8  |-  (  _I  |`  N ) : N -1-1-onto-> N
4 f1of 5802 . . . . . . . 8  |-  ( (  _I  |`  N ) : N -1-1-onto-> N  ->  (  _I  |`  N ) : N --> N )
53, 4mp1i 12 . . . . . . 7  |-  ( ph  ->  (  _I  |`  N ) : N --> N )
6 mdetuni.n . . . . . . . 8  |-  ( ph  ->  N  e.  Fin )
7 elmapg 7431 . . . . . . . 8  |-  ( ( N  e.  Fin  /\  N  e.  Fin )  ->  ( (  _I  |`  N )  e.  ( N  ^m  N )  <->  (  _I  |`  N ) : N --> N ) )
86, 6, 7syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( (  _I  |`  N )  e.  ( N  ^m  N )  <->  (  _I  |`  N ) : N --> N ) )
95, 8mpbird 232 . . . . . 6  |-  ( ph  ->  (  _I  |`  N )  e.  ( N  ^m  N ) )
109adantr 465 . . . . 5  |-  ( (
ph  /\  a  e.  B )  ->  (  _I  |`  N )  e.  ( N  ^m  N
) )
11 simplrl 759 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  ( N  ^m  N ) ) )  /\  A. w  e.  ( N  X.  N
) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  ) )  ->  y  e.  B )
12 mdetuni.a . . . . . . . . . . . . . . . . 17  |-  A  =  ( N Mat  R )
13 mdetuni.k . . . . . . . . . . . . . . . . 17  |-  K  =  ( Base `  R
)
14 mdetuni.b . . . . . . . . . . . . . . . . 17  |-  B  =  ( Base `  A
)
1512, 13, 14matbas2i 18791 . . . . . . . . . . . . . . . 16  |-  ( y  e.  B  ->  y  e.  ( K  ^m  ( N  X.  N ) ) )
16 elmapi 7438 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( K  ^m  ( N  X.  N
) )  ->  y : ( N  X.  N ) --> K )
1715, 16syl 16 . . . . . . . . . . . . . . 15  |-  ( y  e.  B  ->  y : ( N  X.  N ) --> K )
1817feqmptd 5907 . . . . . . . . . . . . . 14  |-  ( y  e.  B  ->  y  =  ( w  e.  ( N  X.  N
)  |->  ( y `  w ) ) )
1918fveq2d 5856 . . . . . . . . . . . . 13  |-  ( y  e.  B  ->  ( D `  y )  =  ( D `  ( w  e.  ( N  X.  N )  |->  ( y `  w ) ) ) )
2011, 19syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  ( N  ^m  N ) ) )  /\  A. w  e.  ( N  X.  N
) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  ) )  ->  ( D `  y )  =  ( D `  ( w  e.  ( N  X.  N )  |->  ( y `  w ) ) ) )
21 eqid 2441 . . . . . . . . . . . . . 14  |-  ( N  X.  N )  =  ( N  X.  N
)
22 mpteq12 4512 . . . . . . . . . . . . . . 15  |-  ( ( ( N  X.  N
)  =  ( N  X.  N )  /\  A. w  e.  ( N  X.  N ) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  ) )  -> 
( w  e.  ( N  X.  N ) 
|->  ( y `  w
) )  =  ( w  e.  ( N  X.  N )  |->  if ( w  e.  z ,  .1.  ,  .0.  ) ) )
2322fveq2d 5856 . . . . . . . . . . . . . 14  |-  ( ( ( N  X.  N
)  =  ( N  X.  N )  /\  A. w  e.  ( N  X.  N ) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  ) )  -> 
( D `  (
w  e.  ( N  X.  N )  |->  ( y `  w ) ) )  =  ( D `  ( w  e.  ( N  X.  N )  |->  if ( w  e.  z ,  .1.  ,  .0.  )
) ) )
2421, 23mpan 670 . . . . . . . . . . . . 13  |-  ( A. w  e.  ( N  X.  N ) ( y `
 w )  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `
 ( w  e.  ( N  X.  N
)  |->  ( y `  w ) ) )  =  ( D `  ( w  e.  ( N  X.  N )  |->  if ( w  e.  z ,  .1.  ,  .0.  ) ) ) )
2524adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  ( N  ^m  N ) ) )  /\  A. w  e.  ( N  X.  N
) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  ) )  ->  ( D `  ( w  e.  ( N  X.  N
)  |->  ( y `  w ) ) )  =  ( D `  ( w  e.  ( N  X.  N )  |->  if ( w  e.  z ,  .1.  ,  .0.  ) ) ) )
26 eleq1 2513 . . . . . . . . . . . . . . . . 17  |-  ( a  =  z  ->  (
a  e.  ( N  ^m  N )  <->  z  e.  ( N  ^m  N ) ) )
2726anbi2d 703 . . . . . . . . . . . . . . . 16  |-  ( a  =  z  ->  (
( ph  /\  a  e.  ( N  ^m  N
) )  <->  ( ph  /\  z  e.  ( N  ^m  N ) ) ) )
28 elequ2 1807 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  z  ->  (
w  e.  a  <->  w  e.  z ) )
2928ifbid 3944 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  z  ->  if ( w  e.  a ,  .1.  ,  .0.  )  =  if ( w  e.  z ,  .1.  ,  .0.  ) )
3029mpteq2dv 4520 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  z  ->  (
w  e.  ( N  X.  N )  |->  if ( w  e.  a ,  .1.  ,  .0.  ) )  =  ( w  e.  ( N  X.  N )  |->  if ( w  e.  z ,  .1.  ,  .0.  ) ) )
3130fveq2d 5856 . . . . . . . . . . . . . . . . 17  |-  ( a  =  z  ->  ( D `  ( w  e.  ( N  X.  N
)  |->  if ( w  e.  a ,  .1.  ,  .0.  ) ) )  =  ( D `  ( w  e.  ( N  X.  N )  |->  if ( w  e.  z ,  .1.  ,  .0.  ) ) ) )
3231eqeq1d 2443 . . . . . . . . . . . . . . . 16  |-  ( a  =  z  ->  (
( D `  (
w  e.  ( N  X.  N )  |->  if ( w  e.  a ,  .1.  ,  .0.  ) ) )  =  .0.  <->  ( D `  ( w  e.  ( N  X.  N )  |->  if ( w  e.  z ,  .1.  ,  .0.  ) ) )  =  .0.  ) )
3327, 32imbi12d 320 . . . . . . . . . . . . . . 15  |-  ( a  =  z  ->  (
( ( ph  /\  a  e.  ( N  ^m  N ) )  -> 
( D `  (
w  e.  ( N  X.  N )  |->  if ( w  e.  a ,  .1.  ,  .0.  ) ) )  =  .0.  )  <->  ( ( ph  /\  z  e.  ( N  ^m  N ) )  ->  ( D `  ( w  e.  ( N  X.  N ) 
|->  if ( w  e.  z ,  .1.  ,  .0.  ) ) )  =  .0.  ) ) )
34 eleq1 2513 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  <. b ,  c
>.  ->  ( w  e.  a  <->  <. b ,  c
>.  e.  a ) )
3534ifbid 3944 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  <. b ,  c
>.  ->  if ( w  e.  a ,  .1.  ,  .0.  )  =  if ( <. b ,  c
>.  e.  a ,  .1.  ,  .0.  ) )
3635mpt2mpt 6375 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ( N  X.  N )  |->  if ( w  e.  a ,  .1.  ,  .0.  )
)  =  ( b  e.  N ,  c  e.  N  |->  if (
<. b ,  c >.  e.  a ,  .1.  ,  .0.  ) )
37 elmapi 7438 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( N  ^m  N )  ->  a : N --> N )
3837adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  a : N
--> N )
39 ffn 5717 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a : N --> N  -> 
a  Fn  N )
4038, 39syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  a  Fn  N )
41403ad2ant1 1016 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  a  Fn  N )
42 simp2 996 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  b  e.  N )
43 fnopfvb 5895 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  Fn  N  /\  b  e.  N )  ->  ( ( a `  b )  =  c  <->  <. b ,  c >.  e.  a ) )
4441, 42, 43syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  (
( a `  b
)  =  c  <->  <. b ,  c >.  e.  a
) )
4544bicomd 201 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  ( <. b ,  c >.  e.  a  <->  ( a `  b )  =  c ) )
4645ifbid 3944 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  if ( <. b ,  c
>.  e.  a ,  .1.  ,  .0.  )  =  if ( ( a `  b )  =  c ,  .1.  ,  .0.  ) )
4746mpt2eq3dva 6342 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  ( b  e.  N ,  c  e.  N  |->  if ( <.
b ,  c >.  e.  a ,  .1.  ,  .0.  ) )  =  ( b  e.  N , 
c  e.  N  |->  if ( ( a `  b )  =  c ,  .1.  ,  .0.  ) ) )
4836, 47syl5eq 2494 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  ( w  e.  ( N  X.  N
)  |->  if ( w  e.  a ,  .1.  ,  .0.  ) )  =  ( b  e.  N ,  c  e.  N  |->  if ( ( a `
 b )  =  c ,  .1.  ,  .0.  ) ) )
4948fveq2d 5856 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  ( D `  ( w  e.  ( N  X.  N ) 
|->  if ( w  e.  a ,  .1.  ,  .0.  ) ) )  =  ( D `  (
b  e.  N , 
c  e.  N  |->  if ( ( a `  b )  =  c ,  .1.  ,  .0.  ) ) ) )
50 mdetuni.0g . . . . . . . . . . . . . . . . . 18  |-  .0.  =  ( 0g `  R )
51 mdetuni.1r . . . . . . . . . . . . . . . . . 18  |-  .1.  =  ( 1r `  R )
52 mdetuni.pg . . . . . . . . . . . . . . . . . 18  |-  .+  =  ( +g  `  R )
53 mdetuni.tg . . . . . . . . . . . . . . . . . 18  |-  .x.  =  ( .r `  R )
54 mdetuni.r . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  R  e.  Ring )
55 mdetuni.ff . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  D : B --> K )
56 mdetuni.al . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. x  e.  B  A. y  e.  N  A. z  e.  N  ( ( y  =/=  z  /\  A. w  e.  N  ( y
x w )  =  ( z x w ) )  ->  ( D `  x )  =  .0.  ) )
57 mdetuni.li . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. w  e.  N  ( ( ( x  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( ( D `  y
)  .+  ( D `  z ) ) ) )
58 mdetuni.sc . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. x  e.  B  A. y  e.  K  A. z  e.  B  A. w  e.  N  ( ( ( x  |`  ( { w }  X.  N ) )  =  ( ( ( { w }  X.  N
)  X.  { y } )  oF  .x.  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( y  .x.  ( D `
 z ) ) ) )
59 mdetunilem9.id . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D `  ( 1r `  A ) )  =  .0.  )
6012, 14, 13, 50, 51, 52, 53, 6, 54, 55, 56, 57, 58, 59mdetunilem8 18988 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  a : N
--> N )  ->  ( D `  ( b  e.  N ,  c  e.  N  |->  if ( ( a `  b )  =  c ,  .1.  ,  .0.  ) ) )  =  .0.  )
6137, 60sylan2 474 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  ( D `  ( b  e.  N ,  c  e.  N  |->  if ( ( a `
 b )  =  c ,  .1.  ,  .0.  ) ) )  =  .0.  )
6249, 61eqtrd 2482 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  ( D `  ( w  e.  ( N  X.  N ) 
|->  if ( w  e.  a ,  .1.  ,  .0.  ) ) )  =  .0.  )
6333, 62chvarv 1998 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  ( N  ^m  N ) )  ->  ( D `  ( w  e.  ( N  X.  N ) 
|->  if ( w  e.  z ,  .1.  ,  .0.  ) ) )  =  .0.  )
6463adantrl 715 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  ( N  ^m  N
) ) )  -> 
( D `  (
w  e.  ( N  X.  N )  |->  if ( w  e.  z ,  .1.  ,  .0.  ) ) )  =  .0.  )
6564adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  ( N  ^m  N ) ) )  /\  A. w  e.  ( N  X.  N
) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  ) )  ->  ( D `  ( w  e.  ( N  X.  N
)  |->  if ( w  e.  z ,  .1.  ,  .0.  ) ) )  =  .0.  )
6620, 25, 653eqtrd 2486 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  ( N  ^m  N ) ) )  /\  A. w  e.  ( N  X.  N
) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  ) )  ->  ( D `  y )  =  .0.  )
6766ex 434 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  ( N  ^m  N
) ) )  -> 
( A. w  e.  ( N  X.  N
) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `  y )  =  .0.  ) )
6867ralrimivva 2862 . . . . . . . . 9  |-  ( ph  ->  A. y  e.  B  A. z  e.  ( N  ^m  N ) ( A. w  e.  ( N  X.  N ) ( y `  w
)  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `  y
)  =  .0.  )
)
69 xpfi 7789 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  N  e.  Fin )  ->  ( N  X.  N
)  e.  Fin )
706, 6, 69syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( N  X.  N
)  e.  Fin )
71 raleq 3038 . . . . . . . . . . . . 13  |-  ( x  =  ( N  X.  N )  ->  ( A. w  e.  x  ( y `  w
)  =  if ( w  e.  z ,  .1.  ,  .0.  )  <->  A. w  e.  ( N  X.  N ) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  ) ) )
7271imbi1d 317 . . . . . . . . . . . 12  |-  ( x  =  ( N  X.  N )  ->  (
( A. w  e.  x  ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `  y )  =  .0.  )  <->  ( A. w  e.  ( N  X.  N
) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `  y )  =  .0.  ) ) )
73722ralbidv 2885 . . . . . . . . . . 11  |-  ( x  =  ( N  X.  N )  ->  ( A. y  e.  B  A. z  e.  ( N  ^m  N ) ( A. w  e.  x  ( y `  w
)  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `  y
)  =  .0.  )  <->  A. y  e.  B  A. z  e.  ( N  ^m  N ) ( A. w  e.  ( N  X.  N ) ( y `
 w )  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `
 y )  =  .0.  ) ) )
74 mdetunilem9.y . . . . . . . . . . 11  |-  Y  =  { x  |  A. y  e.  B  A. z  e.  ( N  ^m  N ) ( A. w  e.  x  (
y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `
 y )  =  .0.  ) }
7573, 74elab2g 3232 . . . . . . . . . 10  |-  ( ( N  X.  N )  e.  Fin  ->  (
( N  X.  N
)  e.  Y  <->  A. y  e.  B  A. z  e.  ( N  ^m  N
) ( A. w  e.  ( N  X.  N
) ( y `  w )  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `  y )  =  .0.  ) ) )
7670, 75syl 16 . . . . . . . . 9  |-  ( ph  ->  ( ( N  X.  N )  e.  Y  <->  A. y  e.  B  A. z  e.  ( N  ^m  N ) ( A. w  e.  ( N  X.  N ) ( y `
 w )  =  if ( w  e.  z ,  .1.  ,  .0.  )  ->  ( D `
 y )  =  .0.  ) ) )
7768, 76mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( N  X.  N
)  e.  Y )
78 ssid 3505 . . . . . . . . 9  |-  ( N  X.  N )  C_  ( N  X.  N
)
79703ad2ant1 1016 . . . . . . . . . . 11  |-  ( (
ph  /\  ( N  X.  N )  C_  ( N  X.  N )  /\  -.  (/)  e.  Y )  ->  ( N  X.  N )  e.  Fin )
80 sseq1 3507 . . . . . . . . . . . . . 14  |-  ( a  =  (/)  ->  ( a 
C_  ( N  X.  N )  <->  (/)  C_  ( N  X.  N ) ) )
81803anbi2d 1303 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  ( (
ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  <->  ( ph  /\  (/)  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
) ) )
82 eleq1 2513 . . . . . . . . . . . . . 14  |-  ( a  =  (/)  ->  ( a  e.  Y  <->  (/)  e.  Y
) )
8382notbid 294 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  ( -.  a  e.  Y  <->  -.  (/)  e.  Y
) )
8481, 83imbi12d 320 . . . . . . . . . . . 12  |-  ( a  =  (/)  ->  ( ( ( ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  ->  -.  a  e.  Y )  <->  ( ( ph  /\  (/)  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  ->  -.  (/)  e.  Y ) ) )
85 sseq1 3507 . . . . . . . . . . . . . 14  |-  ( a  =  b  ->  (
a  C_  ( N  X.  N )  <->  b  C_  ( N  X.  N
) ) )
86853anbi2d 1303 . . . . . . . . . . . . 13  |-  ( a  =  b  ->  (
( ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  <->  ( ph  /\  b  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y ) ) )
87 eleq1 2513 . . . . . . . . . . . . . 14  |-  ( a  =  b  ->  (
a  e.  Y  <->  b  e.  Y ) )
8887notbid 294 . . . . . . . . . . . . 13  |-  ( a  =  b  ->  ( -.  a  e.  Y  <->  -.  b  e.  Y ) )
8986, 88imbi12d 320 . . . . . . . . . . . 12  |-  ( a  =  b  ->  (
( ( ph  /\  a  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  ->  -.  a  e.  Y
)  <->  ( ( ph  /\  b  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  ->  -.  b  e.  Y
) ) )
90 sseq1 3507 . . . . . . . . . . . . . 14  |-  ( a  =  ( b  u. 
{ c } )  ->  ( a  C_  ( N  X.  N
)  <->  ( b  u. 
{ c } ) 
C_  ( N  X.  N ) ) )
91903anbi2d 1303 . . . . . . . . . . . . 13  |-  ( a  =  ( b  u. 
{ c } )  ->  ( ( ph  /\  a  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  <->  ( ph  /\  ( b  u.  {
c } )  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
) ) )
92 eleq1 2513 . . . . . . . . . . . . . 14  |-  ( a  =  ( b  u. 
{ c } )  ->  ( a  e.  Y  <->  ( b  u. 
{ c } )  e.  Y ) )
9392notbid 294 . . . . . . . . . . . . 13  |-  ( a  =  ( b  u. 
{ c } )  ->  ( -.  a  e.  Y  <->  -.  ( b  u.  { c } )  e.  Y ) )
9491, 93imbi12d 320 . . . . . . . . . . . 12  |-  ( a  =  ( b  u. 
{ c } )  ->  ( ( (
ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  ->  -.  a  e.  Y )  <->  ( ( ph  /\  ( b  u. 
{ c } ) 
C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  ->  -.  ( b  u.  {
c } )  e.  Y ) ) )
95 sseq1 3507 . . . . . . . . . . . . . 14  |-  ( a  =  ( N  X.  N )  ->  (
a  C_  ( N  X.  N )  <->  ( N  X.  N )  C_  ( N  X.  N ) ) )
96953anbi2d 1303 . . . . . . . . . . . . 13  |-  ( a  =  ( N  X.  N )  ->  (
( ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  <->  ( ph  /\  ( N  X.  N
)  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y ) ) )
97 eleq1 2513 . . . . . . . . . . . . . 14  |-  ( a  =  ( N  X.  N )  ->  (
a  e.  Y  <->  ( N  X.  N )  e.  Y
) )
9897notbid 294 . . . . . . . . . . . . 13  |-  ( a  =  ( N  X.  N )  ->  ( -.  a  e.  Y  <->  -.  ( N  X.  N
)  e.  Y ) )
9996, 98imbi12d 320 . . . . . . . . . . . 12  |-  ( a  =  ( N  X.  N )  ->  (
( ( ph  /\  a  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  ->  -.  a  e.  Y
)  <->  ( ( ph  /\  ( N  X.  N
)  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  ->  -.  ( N  X.  N
)  e.  Y ) ) )
100 simp3 997 . . . . . . . . . . . 12  |-  ( (
ph  /\  (/)  C_  ( N  X.  N )  /\  -.  (/)  e.  Y )  ->  -.  (/)  e.  Y
)
101 ssun1 3649 . . . . . . . . . . . . . . . 16  |-  b  C_  ( b  u.  {
c } )
102 sstr2 3493 . . . . . . . . . . . . . . . 16  |-  ( b 
C_  ( b  u. 
{ c } )  ->  ( ( b  u.  { c } )  C_  ( N  X.  N )  ->  b  C_  ( N  X.  N
) ) )
103101, 102ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( b  u.  { c } )  C_  ( N  X.  N )  -> 
b  C_  ( N  X.  N ) )
1041033anim2i 1182 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  -> 
( ph  /\  b  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
) )
105104imim1i 58 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  b  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  ->  -.  b  e.  Y )  ->  (
( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  -.  (/)  e.  Y )  ->  -.  b  e.  Y ) )
106 simpl1 998 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  ( b  u.  {
c } )  e.  Y )  /\  (
( a  e.  B  /\  d  e.  ( N  ^m  N ) )  /\  A. w  e.  b  ( a `  w )  =  if ( w  e.  d ,  .1.  ,  .0.  ) ) )  ->  ph )
107 simpl2 999 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  ( b  u.  {
c } )  e.  Y )  /\  (
( a  e.  B  /\  d  e.  ( N  ^m  N ) )  /\  A. w  e.  b  ( a `  w )  =  if ( w  e.  d ,  .1.  ,  .0.  ) ) )  -> 
( b  u.  {
c } )  C_  ( N  X.  N
) )
108 simprll 761 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  ( b  u.  {
c } )  e.  Y )  /\  (
( a  e.  B  /\  d  e.  ( N  ^m  N ) )  /\  A. w  e.  b  ( a `  w )  =  if ( w  e.  d ,  .1.  ,  .0.  ) ) )  -> 
a  e.  B )
10912, 13, 14matbas2i 18791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  e.  B  ->  a  e.  ( K  ^m  ( N  X.  N ) ) )
110 elmapi 7438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  e.  ( K  ^m  ( N  X.  N
) )  ->  a : ( N  X.  N ) --> K )
111109, 110syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  B  ->  a : ( N  X.  N ) --> K )
1121113ad2ant3 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  a : ( N  X.  N ) --> K )
113112feqmptd 5907 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  a  =  ( e  e.  ( N  X.  N
)  |->  ( a `  e ) ) )
114113reseq1d 5258 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
a  |`  ( { ( 1st `  c ) }  X.  N ) )  =  ( ( e  e.  ( N  X.  N )  |->  ( a `  e ) )  |`  ( {
( 1st `  c
) }  X.  N
) ) )
115543ad2ant1 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  R  e.  Ring )
116 ringgrp 17071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( R  e.  Ring  ->  R  e. 
Grp )
117115, 116syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  R  e.  Grp )
118117adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  R  e.  Grp )
119112adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  a : ( N  X.  N ) --> K )
120 simp2 996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
b  u.  { c } )  C_  ( N  X.  N ) )
121120unssbd 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  { c }  C_  ( N  X.  N ) )
122 vex 3096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  c  e. 
_V
123122snss 4135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  e.  ( N  X.  N )  <->  { c }  C_  ( N  X.  N ) )
124121, 123sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  c  e.  ( N  X.  N
) )
125 xp1st 6811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( c  e.  ( N  X.  N )  ->  ( 1st `  c )  e.  N )
126124, 125syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( 1st `  c )  e.  N )
127126snssd 4156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  { ( 1st `  c ) }  C_  N )
128 xpss1 5097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( { ( 1st `  c
) }  C_  N  ->  ( { ( 1st `  c ) }  X.  N )  C_  ( N  X.  N ) )
129127, 128syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( { ( 1st `  c
) }  X.  N
)  C_  ( N  X.  N ) )
130129sselda 3486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  e  e.  ( N  X.  N
) )
131119, 130ffvelrnd 6013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (
a `  e )  e.  K )
13213, 51ringidcl 17087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( R  e.  Ring  ->  .1.  e.  K )
133115, 132syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  .1.  e.  K )
13413, 50ring0cl 17088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( R  e.  Ring  ->  .0.  e.  K )
135115, 134syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  .0.  e.  K )
136133, 135ifcld 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  if ( e  e.  d ,  .1.  ,  .0.  )  e.  K )
137136adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  if ( e  e.  d ,  .1.  ,  .0.  )  e.  K )
138 eqid 2441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -g `  R )  =  (
-g `  R )
13913, 52, 138grpnpcan 15999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( R  e.  Grp  /\  ( a `  e
)  e.  K  /\  if ( e  e.  d ,  .1.  ,  .0.  )  e.  K )  ->  ( ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) )  .+  if ( e  e.  d ,  .1.  ,  .0.  ) )  =  ( a `  e ) )
140118, 131, 137, 139syl3anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (
( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
)  .+  if (
e  e.  d ,  .1.  ,  .0.  )
)  =  ( a `
 e ) )
141140eqcomd 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (
a `  e )  =  ( ( ( a `  e ) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) )  .+  if ( e  e.  d ,  .1.  ,  .0.  ) ) )
142141adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( b  u.  {
c } )  C_  ( N  X.  N
)  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c ) }  X.  N ) )  /\  e  =  c )  ->  ( a `  e
)  =  ( ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) )  .+  if ( e  e.  d ,  .1.  ,  .0.  ) ) )
143 iftrue 3928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( e  =  c  ->  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  =  ( (
a `  e )
( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) )
144 iftrue 3928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( e  =  c  ->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) )  =  if ( e  e.  d ,  .1.  ,  .0.  )
)
145143, 144oveq12d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  =  c  ->  ( if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  .+  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  =  ( ( ( a `  e ) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) )  .+  if ( e  e.  d ,  .1.  ,  .0.  ) ) )
146145adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( b  u.  {
c } )  C_  ( N  X.  N
)  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c ) }  X.  N ) )  /\  e  =  c )  ->  ( if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  .+  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  =  ( ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
)  .+  if (
e  e.  d ,  .1.  ,  .0.  )
) )
147142, 146eqtr4d 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  ( b  u.  {
c } )  C_  ( N  X.  N
)  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c ) }  X.  N ) )  /\  e  =  c )  ->  ( a `  e
)  =  ( if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  .+  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) )
14813, 52, 50grplid 15949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( R  e.  Grp  /\  ( a `  e
)  e.  K )  ->  (  .0.  .+  ( a `  e
) )  =  ( a `  e ) )
149118, 131, 148syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (  .0.  .+  ( a `  e ) )  =  ( a `  e
) )
150149eqcomd 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (
a `  e )  =  (  .0.  .+  (
a `  e )
) )
151150adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( b  u.  {
c } )  C_  ( N  X.  N
)  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c ) }  X.  N ) )  /\  -.  e  =  c
)  ->  ( a `  e )  =  (  .0.  .+  ( a `  e ) ) )
152 iffalse 3931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( -.  e  =  c  ->  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  =  .0.  )
153 iffalse 3931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( -.  e  =  c  ->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) )  =  ( a `
 e ) )
154152, 153oveq12d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( -.  e  =  c  -> 
( if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  .+  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  =  (  .0.  .+  ( a `  e ) ) )
155154adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  ( b  u.  {
c } )  C_  ( N  X.  N
)  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c ) }  X.  N ) )  /\  -.  e  =  c
)  ->  ( if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  .+  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  =  (  .0.  .+  ( a `  e
) ) )
156151, 155eqtr4d 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  ( b  u.  {
c } )  C_  ( N  X.  N
)  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c ) }  X.  N ) )  /\  -.  e  =  c
)  ->  ( a `  e )  =  ( if ( e  =  c ,  ( ( a `  e ) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  .+  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) )
157147, 156pm2.61dan 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (
a `  e )  =  ( if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  )  .+  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) )
158157mpteq2dva 4519 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  ( a `  e ) )  =  ( e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  ( if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  )  .+  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) ) )
159 snfi 7594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  { ( 1st `  c ) }  e.  Fin
16063ad2ant1 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  N  e.  Fin )
161 xpfi 7789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( { ( 1st `  c
) }  e.  Fin  /\  N  e.  Fin )  ->  ( { ( 1st `  c ) }  X.  N )  e.  Fin )
162159, 160, 161sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( { ( 1st `  c
) }  X.  N
)  e.  Fin )
163 ovex 6305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( a `  e ) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) )  e. 
_V
164 fvex 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 0g
`  R )  e. 
_V
16550, 164eqeltri 2525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  .0.  e.  _V
166163, 165ifex 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  )  e.  _V
167166a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  e.  _V )
168 fvex 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 1r
`  R )  e. 
_V
16951, 168eqeltri 2525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  .1.  e.  _V
170169, 165ifex 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  if ( e  e.  d ,  .1.  ,  .0.  )  e.  _V
171 fvex 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a `
 e )  e. 
_V
172170, 171ifex 3991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `
 e ) )  e.  _V
173172a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) )  e.  _V )
174 xp1st 6811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  e.  ( { ( 1st `  c ) }  X.  N )  ->  ( 1st `  e
)  e.  { ( 1st `  c ) } )
175 elsni 4035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 1st `  e )  e.  { ( 1st `  c ) }  ->  ( 1st `  e )  =  ( 1st `  c
) )
176 iftrue 3928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 1st `  e )  =  ( 1st `  c
)  ->  if (
( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) )  =  if ( e  =  c ,  ( ( a `  e ) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) )
177174, 175, 1763syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( e  e.  ( { ( 1st `  c ) }  X.  N )  ->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) )  =  if ( e  =  c ,  ( ( a `  e ) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) )
178177mpteq2ia 4515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( e  e.  ( { ( 1st `  c ) }  X.  N ) 
|->  if ( ( 1st `  e )  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  =  ( e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) )
179178a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  =  ( e  e.  ( { ( 1st `  c ) }  X.  N )  |->  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  )
) )
180 eqidd 2442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  =  ( e  e.  ( { ( 1st `  c ) }  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `
 e ) ) ) )
181162, 167, 173, 179, 180offval2 6537 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  oF  .+  (
e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) )  =  ( e  e.  ( { ( 1st `  c ) }  X.  N ) 
|->  ( if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  .+  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) ) )
182158, 181eqtr4d 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  ( a `  e ) )  =  ( ( e  e.  ( { ( 1st `  c ) }  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  oF  .+  (
e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) ) )
183129resmptd 5311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  ( a `  e
) )  |`  ( { ( 1st `  c
) }  X.  N
) )  =  ( e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  ( a `  e ) ) )
184129resmptd 5311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  if ( ( 1st `  e )  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { ( 1st `  c
) }  X.  N
) )  =  ( e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) ) )
185129resmptd 5311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { ( 1st `  c ) }  X.  N ) )  =  ( e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) )
186184, 185oveq12d 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { ( 1st `  c ) }  X.  N ) )  oF  .+  ( ( e  e.  ( N  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { ( 1st `  c
) }  X.  N
) ) )  =  ( ( e  e.  ( { ( 1st `  c ) }  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  oF  .+  (
e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) ) )
187182, 183, 1863eqtr4d 2492 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  ( a `  e
) )  |`  ( { ( 1st `  c
) }  X.  N
) )  =  ( ( ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { ( 1st `  c ) }  X.  N ) )  oF  .+  ( ( e  e.  ( N  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { ( 1st `  c
) }  X.  N
) ) ) )
188114, 187eqtrd 2482 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
a  |`  ( { ( 1st `  c ) }  X.  N ) )  =  ( ( ( e  e.  ( N  X.  N ) 
|->  if ( ( 1st `  e )  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { ( 1st `  c
) }  X.  N
) )  oF  .+  ( ( e  e.  ( N  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `
 e ) ) )  |`  ( {
( 1st `  c
) }  X.  N
) ) ) )
189113reseq1d 5258 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
a  |`  ( ( N 
\  { ( 1st `  c ) } )  X.  N ) )  =  ( ( e  e.  ( N  X.  N )  |->  ( a `
 e ) )  |`  ( ( N  \  { ( 1st `  c
) } )  X.  N ) ) )
190 xp1st 6811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  e.  ( ( N 
\  { ( 1st `  c ) } )  X.  N )  -> 
( 1st `  e
)  e.  ( N 
\  { ( 1st `  c ) } ) )
191 eldifsni 4137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 1st `  e )  e.  ( N  \  { ( 1st `  c
) } )  -> 
( 1st `  e
)  =/=  ( 1st `  c ) )
192190, 191syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( e  e.  ( ( N 
\  { ( 1st `  c ) } )  X.  N )  -> 
( 1st `  e
)  =/=  ( 1st `  c ) )
193192neneqd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( e  e.  ( ( N 
\  { ( 1st `  c ) } )  X.  N )  ->  -.  ( 1st `  e
)  =  ( 1st `  c ) )
194193adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  ->  -.  ( 1st `  e
)  =  ( 1st `  c ) )
195194iffalsed 3933 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  ->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) )  =  ( a `  e
) )
196195mpteq2dva 4519 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( ( N  \  { ( 1st `  c ) } )  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  =  ( e  e.  ( ( N  \  { ( 1st `  c
) } )  X.  N )  |->  ( a `
 e ) ) )
197 difss 3613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N 
\  { ( 1st `  c ) } ) 
C_  N
198 xpss1 5097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  \  { ( 1st `  c ) } )  C_  N  ->  ( ( N  \  { ( 1st `  c
) } )  X.  N )  C_  ( N  X.  N ) )
199197, 198ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  \  { ( 1st `  c ) } )  X.  N
)  C_  ( N  X.  N )
200 resmpt 5309 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( N  \  {
( 1st `  c
) } )  X.  N )  C_  ( N  X.  N )  -> 
( ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( ( N  \  { ( 1st `  c
) } )  X.  N ) )  =  ( e  e.  ( ( N  \  {
( 1st `  c
) } )  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) ) )
201199, 200mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  if ( ( 1st `  e )  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  |`  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  =  ( e  e.  ( ( N  \  {
( 1st `  c
) } )  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) ) )
202 resmpt 5309 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( N  \  {
( 1st `  c
) } )  X.  N )  C_  ( N  X.  N )  -> 
( ( e  e.  ( N  X.  N
)  |->  ( a `  e ) )  |`  ( ( N  \  { ( 1st `  c
) } )  X.  N ) )  =  ( e  e.  ( ( N  \  {
( 1st `  c
) } )  X.  N )  |->  ( a `
 e ) ) )
203199, 202mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  ( a `  e
) )  |`  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  =  ( e  e.  ( ( N  \  {
( 1st `  c
) } )  X.  N )  |->  ( a `
 e ) ) )
204196, 201, 2033eqtr4rd 2493 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  ( a `  e
) )  |`  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  =  ( ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( ( N  \  { ( 1st `  c
) } )  X.  N ) ) )
205189, 204eqtrd 2482 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
a  |`  ( ( N 
\  { ( 1st `  c ) } )  X.  N ) )  =  ( ( e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( ( N  \  { ( 1st `  c
) } )  X.  N ) ) )
206 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( e  =  c  ->  ( 1st `  e )  =  ( 1st `  c
) )
207194, 206nsyl 121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  ->  -.  e  =  c
)
208207iffalsed 3933 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  ->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) )  =  ( a `
 e ) )
209208mpteq2dva 4519 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( ( N  \  { ( 1st `  c ) } )  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  =  ( e  e.  ( ( N  \  { ( 1st `  c
) } )  X.  N )  |->  ( a `
 e ) ) )
210 resmpt 5309 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( N  \  {
( 1st `  c
) } )  X.  N )  C_  ( N  X.  N )  -> 
( ( e  e.  ( N  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  |`  ( ( N  \  { ( 1st `  c
) } )  X.  N ) )  =  ( e  e.  ( ( N  \  {
( 1st `  c
) } )  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `
 e ) ) ) )
211199, 210mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  |`  ( ( N  \  { ( 1st `  c
) } )  X.  N ) )  =  ( e  e.  ( ( N  \  {
( 1st `  c
) } )  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `
 e ) ) ) )
212209, 211, 2033eqtr4rd 2493 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  ( a `  e
) )  |`  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  =  ( ( e  e.  ( N  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  |`  ( ( N  \  { ( 1st `  c
) } )  X.  N ) ) )
213189, 212eqtrd 2482 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
a  |`  ( ( N 
\  { ( 1st `  c ) } )  X.  N ) )  =  ( ( e  e.  ( N  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `
 e ) ) )  |`  ( ( N  \  { ( 1st `  c ) } )  X.  N ) ) )
214136adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  if ( e  e.  d ,  .1.  ,  .0.  )  e.  K
)
215112ffvelrnda 6012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  ( a `  e )  e.  K
)
216214, 215ifcld 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) )  e.  K )
217 eqid 2441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( e  e.  ( N  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `
 e ) ) )  =  ( e  e.  ( N  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `
 e ) ) )
218216, 217fmptd 6036 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( N  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) : ( N  X.  N ) --> K )
219 fvex 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Base `  R )  e.  _V
22013, 219eqeltri 2525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  K  e. 
_V
22169anidms 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  Fin  ->  ( N  X.  N )  e. 
Fin )
222160, 221syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( N  X.  N )  e. 
Fin )
223 elmapg 7431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( K  e.  _V  /\  ( N  X.  N
)  e.  Fin )  ->  ( ( e  e.  ( N  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  e.  ( K  ^m  ( N  X.  N
) )  <->  ( e  e.  ( N  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) : ( N  X.  N ) --> K ) )
224220, 222, 223sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  e.  ( K  ^m  ( N  X.  N
) )  <->  ( e  e.  ( N  X.  N
)  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) ) : ( N  X.  N ) --> K ) )
225218, 224mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( N  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  e.  ( K  ^m  ( N  X.  N ) ) )
22612, 13matbas2 18790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( K  ^m  ( N  X.  N ) )  =  ( Base `  A
) )
227160, 115, 226syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( K  ^m  ( N  X.  N ) )  =  ( Base `  A
) )
228227, 14syl6eqr 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( K  ^m  ( N  X.  N ) )  =  B )
229225, 228eleqtrd 2531 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( N  X.  N )  |->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) ) )  e.  B
)
230 simp3 997 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  a  e.  B )
231117adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  R  e.  Grp )
23213, 138grpsubcl 15987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( R  e.  Grp  /\  ( a `  e
)  e.  K  /\  if ( e  e.  d ,  .1.  ,  .0.  )  e.  K )  ->  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
)  e.  K )
233231, 215, 214, 232syl3anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) )  e.  K
)
234135adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  .0.  e.  K
)
235233, 234ifcld 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  e.  K
)
236235, 215ifcld 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) )  e.  K )
237 eqid 2441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  =  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )
238236, 237fmptd 6036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) ) : ( N  X.  N ) --> K )
239 elmapg 7431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( K  e.  _V  /\  ( N  X.  N
)  e.  Fin )  ->  ( ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  e.  ( K  ^m  ( N  X.  N
) )  <->  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) ) : ( N  X.  N ) --> K ) )
240220, 222, 239sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
( e  e.  ( N  X.  N ) 
|->  if ( ( 1st `  e )  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  e.  ( K  ^m  ( N  X.  N ) )  <-> 
( e  e.  ( N  X.  N ) 
|->  if ( ( 1st `  e )  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `  e
) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) ) : ( N  X.  N ) --> K ) )
241238, 240mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  e.  ( K  ^m  ( N  X.  N
) ) )
242241, 228eleqtrd 2531 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  e.  B )
243573ad2ant1 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. w  e.  N  ( (
( x  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( ( D `  y
)  .+  ( D `  z ) ) ) )
244 reseq1 5253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  a  ->  (
x  |`  ( { w }  X.  N ) )  =  ( a  |`  ( { w }  X.  N ) ) )
245244eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  a  ->  (
( x  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  <-> 
( a  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) ) ) )
246 reseq1 5253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  a  ->  (
x  |`  ( ( N 
\  { w }
)  X.  N ) )  =  ( a  |`  ( ( N  \  { w } )  X.  N ) ) )
247246eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  a  ->  (
( x  |`  (
( N  \  {
w } )  X.  N ) )  =  ( y  |`  (
( N  \  {
w } )  X.  N ) )  <->  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) ) ) )
248246eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  a  ->  (
( x  |`  (
( N  \  {
w } )  X.  N ) )  =  ( z  |`  (
( N  \  {
w } )  X.  N ) )  <->  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) ) )
249245, 247, 2483anbi123d 1298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  =  a  ->  (
( ( x  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  <->  ( ( a  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) ) ) )
250 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  a  ->  ( D `  x )  =  ( D `  a ) )
251250eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  =  a  ->  (
( D `  x
)  =  ( ( D `  y ) 
.+  ( D `  z ) )  <->  ( D `  a )  =  ( ( D `  y
)  .+  ( D `  z ) ) ) )
252249, 251imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  =  a  ->  (
( ( ( x  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( ( D `  y
)  .+  ( D `  z ) ) )  <-> 
( ( ( a  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  a )  =  ( ( D `  y
)  .+  ( D `  z ) ) ) ) )
2532522ralbidv 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  a  ->  ( A. z  e.  B  A. w  e.  N  ( ( ( x  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( x  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  x )  =  ( ( D `  y
)  .+  ( D `  z ) ) )  <->  A. z  e.  B  A. w  e.  N  ( ( ( a  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  ->  ( D `  a )  =  ( ( D `  y
)  .+  ( D `  z ) ) ) ) )
254 reseq1 5253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  ->  ( y  |`  ( { w }  X.  N ) )  =  ( ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { w }  X.  N ) ) )
255254oveq1d 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  ->  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  =  ( ( ( e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) ) )
256255eqeq2d 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  ->  ( ( a  |`  ( { w }  X.  N ) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  <-> 
( a  |`  ( { w }  X.  N ) )  =  ( ( ( e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) ) ) )
257 reseq1 5253 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  ->  ( y  |`  ( ( N  \  { w } )  X.  N ) )  =  ( ( e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( ( N  \  { w } )  X.  N ) ) )
258257eqeq2d 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  ->  ( ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  <-> 
( a  |`  (
( N  \  {
w } )  X.  N ) )  =  ( ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( ( N  \  { w } )  X.  N ) ) ) )
259256, 2583anbi12d 1299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  ->  ( ( ( a  |`  ( {
w }  X.  N
) )  =  ( ( y  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) )  <->  ( ( a  |`  ( { w }  X.  N ) )  =  ( ( ( e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( { w }  X.  N ) )  oF  .+  ( z  |`  ( { w }  X.  N ) ) )  /\  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( ( e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) )  |`  ( ( N  \  { w } )  X.  N ) )  /\  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) ) ) )
260 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  ->  ( D `  y )  =  ( D `  ( e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) ) ) )
261260oveq1d 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  ) ,  ( a `  e ) ) )  ->  ( ( D `
 y )  .+  ( D `  z ) )  =  ( ( D `  ( e  e.  ( N  X.  N )  |->  if ( ( 1st `  e
)  =  ( 1st `  c ) ,  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  ) ,  ( a `  e ) ) ) )  .+  ( D `
 z ) )