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

Theorem mdetunilem9 19289
Description: Lemma for mdetuni 19291. (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 3922 . . . 4  |-  A. w  e.  (/)  ( a `  w )  =  if ( w  e.  (  _I  |`  N ) ,  .1.  ,  .0.  )
2 simpr 459 . . . . 5  |-  ( (
ph  /\  a  e.  B )  ->  a  e.  B )
3 f1oi 5833 . . . . . . . 8  |-  (  _I  |`  N ) : N -1-1-onto-> N
4 f1of 5798 . . . . . . . 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 )
76, 6elmapd 7426 . . . . . . 7  |-  ( ph  ->  ( (  _I  |`  N )  e.  ( N  ^m  N )  <->  (  _I  |`  N ) : N --> N ) )
85, 7mpbird 232 . . . . . 6  |-  ( ph  ->  (  _I  |`  N )  e.  ( N  ^m  N ) )
98adantr 463 . . . . 5  |-  ( (
ph  /\  a  e.  B )  ->  (  _I  |`  N )  e.  ( N  ^m  N
) )
10 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 )
11 mdetuni.a . . . . . . . . . . . . . . . . 17  |-  A  =  ( N Mat  R )
12 mdetuni.k . . . . . . . . . . . . . . . . 17  |-  K  =  ( Base `  R
)
13 mdetuni.b . . . . . . . . . . . . . . . . 17  |-  B  =  ( Base `  A
)
1411, 12, 13matbas2i 19091 . . . . . . . . . . . . . . . 16  |-  ( y  e.  B  ->  y  e.  ( K  ^m  ( N  X.  N ) ) )
15 elmapi 7433 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( K  ^m  ( N  X.  N
) )  ->  y : ( N  X.  N ) --> K )
1614, 15syl 16 . . . . . . . . . . . . . . 15  |-  ( y  e.  B  ->  y : ( N  X.  N ) --> K )
1716feqmptd 5901 . . . . . . . . . . . . . 14  |-  ( y  e.  B  ->  y  =  ( w  e.  ( N  X.  N
)  |->  ( y `  w ) ) )
1817fveq2d 5852 . . . . . . . . . . . . 13  |-  ( y  e.  B  ->  ( D `  y )  =  ( D `  ( w  e.  ( N  X.  N )  |->  ( y `  w ) ) ) )
1910, 18syl 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 ) ) ) )
20 eqid 2454 . . . . . . . . . . . . . 14  |-  ( N  X.  N )  =  ( N  X.  N
)
21 mpteq12 4518 . . . . . . . . . . . . . . 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.  ) ) )
2221fveq2d 5852 . . . . . . . . . . . . . 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.  )
) ) )
2320, 22mpan 668 . . . . . . . . . . . . 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.  ) ) ) )
2423adantl 464 . . . . . . . . . . . 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.  ) ) ) )
25 eleq1 2526 . . . . . . . . . . . . . . . . 17  |-  ( a  =  z  ->  (
a  e.  ( N  ^m  N )  <->  z  e.  ( N  ^m  N ) ) )
2625anbi2d 701 . . . . . . . . . . . . . . . 16  |-  ( a  =  z  ->  (
( ph  /\  a  e.  ( N  ^m  N
) )  <->  ( ph  /\  z  e.  ( N  ^m  N ) ) ) )
27 elequ2 1828 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  z  ->  (
w  e.  a  <->  w  e.  z ) )
2827ifbid 3951 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  z  ->  if ( w  e.  a ,  .1.  ,  .0.  )  =  if ( w  e.  z ,  .1.  ,  .0.  ) )
2928mpteq2dv 4526 . . . . . . . . . . . . . . . . . 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.  ) ) )
3029fveq2d 5852 . . . . . . . . . . . . . . . . 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.  ) ) ) )
3130eqeq1d 2456 . . . . . . . . . . . . . . . 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.  ) )
3226, 31imbi12d 318 . . . . . . . . . . . . . . 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.  ) ) )
33 eleq1 2526 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  <. b ,  c
>.  ->  ( w  e.  a  <->  <. b ,  c
>.  e.  a ) )
3433ifbid 3951 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  <. b ,  c
>.  ->  if ( w  e.  a ,  .1.  ,  .0.  )  =  if ( <. b ,  c
>.  e.  a ,  .1.  ,  .0.  ) )
3534mpt2mpt 6367 . . . . . . . . . . . . . . . . . 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.  ) )
36 elmapi 7433 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( N  ^m  N )  ->  a : N --> N )
3736adantl 464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  a : N
--> N )
38 ffn 5713 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a : N --> N  -> 
a  Fn  N )
3937, 38syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  a  Fn  N )
40393ad2ant1 1015 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  a  Fn  N )
41 simp2 995 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  b  e.  N )
42 fnopfvb 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  Fn  N  /\  b  e.  N )  ->  ( ( a `  b )  =  c  <->  <. b ,  c >.  e.  a ) )
4340, 41, 42syl2anc 659 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  (
( a `  b
)  =  c  <->  <. b ,  c >.  e.  a
) )
4443bicomd 201 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  ( <. b ,  c >.  e.  a  <->  ( a `  b )  =  c ) )
4544ifbid 3951 . . . . . . . . . . . . . . . . . . 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.  ) )
4645mpt2eq3dva 6334 . . . . . . . . . . . . . . . . . 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.  ) ) )
4735, 46syl5eq 2507 . . . . . . . . . . . . . . . . 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.  ) ) )
4847fveq2d 5852 . . . . . . . . . . . . . . . 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.  ) ) ) )
49 mdetuni.0g . . . . . . . . . . . . . . . . . 18  |-  .0.  =  ( 0g `  R )
50 mdetuni.1r . . . . . . . . . . . . . . . . . 18  |-  .1.  =  ( 1r `  R )
51 mdetuni.pg . . . . . . . . . . . . . . . . . 18  |-  .+  =  ( +g  `  R )
52 mdetuni.tg . . . . . . . . . . . . . . . . . 18  |-  .x.  =  ( .r `  R )
53 mdetuni.r . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  R  e.  Ring )
54 mdetuni.ff . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  D : B --> K )
55 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.  ) )
56 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 ) ) ) )
57 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 ) ) ) )
58 mdetunilem9.id . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D `  ( 1r `  A ) )  =  .0.  )
5911, 13, 12, 49, 50, 51, 52, 6, 53, 54, 55, 56, 57, 58mdetunilem8 19288 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  a : N
--> N )  ->  ( D `  ( b  e.  N ,  c  e.  N  |->  if ( ( a `  b )  =  c ,  .1.  ,  .0.  ) ) )  =  .0.  )
6036, 59sylan2 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  ( D `  ( b  e.  N ,  c  e.  N  |->  if ( ( a `
 b )  =  c ,  .1.  ,  .0.  ) ) )  =  .0.  )
6148, 60eqtrd 2495 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  ( D `  ( w  e.  ( N  X.  N ) 
|->  if ( w  e.  a ,  .1.  ,  .0.  ) ) )  =  .0.  )
6232, 61chvarv 2019 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  ( N  ^m  N ) )  ->  ( D `  ( w  e.  ( N  X.  N ) 
|->  if ( w  e.  z ,  .1.  ,  .0.  ) ) )  =  .0.  )
6362adantrl 713 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  ( N  ^m  N
) ) )  -> 
( D `  (
w  e.  ( N  X.  N )  |->  if ( w  e.  z ,  .1.  ,  .0.  ) ) )  =  .0.  )
6463adantr 463 . . . . . . . . . . . 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.  )
6519, 24, 643eqtrd 2499 . . . . . . . . . . 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.  )
6665ex 432 . . . . . . . . . 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.  ) )
6766ralrimivva 2875 . . . . . . . . 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.  )
)
68 xpfi 7783 . . . . . . . . . . 11  |-  ( ( N  e.  Fin  /\  N  e.  Fin )  ->  ( N  X.  N
)  e.  Fin )
696, 6, 68syl2anc 659 . . . . . . . . . 10  |-  ( ph  ->  ( N  X.  N
)  e.  Fin )
70 raleq 3051 . . . . . . . . . . . . 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.  ) ) )
7170imbi1d 315 . . . . . . . . . . . 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.  ) ) )
72712ralbidv 2898 . . . . . . . . . . 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.  ) ) )
73 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.  ) }
7472, 73elab2g 3245 . . . . . . . . . 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.  ) ) )
7569, 74syl 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.  ) ) )
7667, 75mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( N  X.  N
)  e.  Y )
77 ssid 3508 . . . . . . . . 9  |-  ( N  X.  N )  C_  ( N  X.  N
)
78693ad2ant1 1015 . . . . . . . . . . 11  |-  ( (
ph  /\  ( N  X.  N )  C_  ( N  X.  N )  /\  -.  (/)  e.  Y )  ->  ( N  X.  N )  e.  Fin )
79 sseq1 3510 . . . . . . . . . . . . . 14  |-  ( a  =  (/)  ->  ( a 
C_  ( N  X.  N )  <->  (/)  C_  ( N  X.  N ) ) )
80793anbi2d 1302 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  ( (
ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  <->  ( ph  /\  (/)  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
) ) )
81 eleq1 2526 . . . . . . . . . . . . . 14  |-  ( a  =  (/)  ->  ( a  e.  Y  <->  (/)  e.  Y
) )
8281notbid 292 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  ( -.  a  e.  Y  <->  -.  (/)  e.  Y
) )
8380, 82imbi12d 318 . . . . . . . . . . . 12  |-  ( a  =  (/)  ->  ( ( ( ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  ->  -.  a  e.  Y )  <->  ( ( ph  /\  (/)  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  ->  -.  (/)  e.  Y ) ) )
84 sseq1 3510 . . . . . . . . . . . . . 14  |-  ( a  =  b  ->  (
a  C_  ( N  X.  N )  <->  b  C_  ( N  X.  N
) ) )
85843anbi2d 1302 . . . . . . . . . . . . 13  |-  ( a  =  b  ->  (
( ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  <->  ( ph  /\  b  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y ) ) )
86 eleq1 2526 . . . . . . . . . . . . . 14  |-  ( a  =  b  ->  (
a  e.  Y  <->  b  e.  Y ) )
8786notbid 292 . . . . . . . . . . . . 13  |-  ( a  =  b  ->  ( -.  a  e.  Y  <->  -.  b  e.  Y ) )
8885, 87imbi12d 318 . . . . . . . . . . . 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
) ) )
89 sseq1 3510 . . . . . . . . . . . . . 14  |-  ( a  =  ( b  u. 
{ c } )  ->  ( a  C_  ( N  X.  N
)  <->  ( b  u. 
{ c } ) 
C_  ( N  X.  N ) ) )
90893anbi2d 1302 . . . . . . . . . . . . 13  |-  ( a  =  ( b  u. 
{ c } )  ->  ( ( ph  /\  a  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  <->  ( ph  /\  ( b  u.  {
c } )  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
) ) )
91 eleq1 2526 . . . . . . . . . . . . . 14  |-  ( a  =  ( b  u. 
{ c } )  ->  ( a  e.  Y  <->  ( b  u. 
{ c } )  e.  Y ) )
9291notbid 292 . . . . . . . . . . . . 13  |-  ( a  =  ( b  u. 
{ c } )  ->  ( -.  a  e.  Y  <->  -.  ( b  u.  { c } )  e.  Y ) )
9390, 92imbi12d 318 . . . . . . . . . . . 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 ) ) )
94 sseq1 3510 . . . . . . . . . . . . . 14  |-  ( a  =  ( N  X.  N )  ->  (
a  C_  ( N  X.  N )  <->  ( N  X.  N )  C_  ( N  X.  N ) ) )
95943anbi2d 1302 . . . . . . . . . . . . 13  |-  ( a  =  ( N  X.  N )  ->  (
( ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  <->  ( ph  /\  ( N  X.  N
)  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y ) ) )
96 eleq1 2526 . . . . . . . . . . . . . 14  |-  ( a  =  ( N  X.  N )  ->  (
a  e.  Y  <->  ( N  X.  N )  e.  Y
) )
9796notbid 292 . . . . . . . . . . . . 13  |-  ( a  =  ( N  X.  N )  ->  ( -.  a  e.  Y  <->  -.  ( N  X.  N
)  e.  Y ) )
9895, 97imbi12d 318 . . . . . . . . . . . 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 ) ) )
99 simp3 996 . . . . . . . . . . . 12  |-  ( (
ph  /\  (/)  C_  ( N  X.  N )  /\  -.  (/)  e.  Y )  ->  -.  (/)  e.  Y
)
100 ssun1 3653 . . . . . . . . . . . . . . . 16  |-  b  C_  ( b  u.  {
c } )
101 sstr2 3496 . . . . . . . . . . . . . . . 16  |-  ( b 
C_  ( b  u. 
{ c } )  ->  ( ( b  u.  { c } )  C_  ( N  X.  N )  ->  b  C_  ( N  X.  N
) ) )
102100, 101ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( b  u.  { c } )  C_  ( N  X.  N )  -> 
b  C_  ( N  X.  N ) )
1031023anim2i 1181 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  -> 
( ph  /\  b  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
) )
104103imim1i 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 ) )
105 simpl1 997 . . . . . . . . . . . . . . . . . . . . . . . 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 )
106 simpl2 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.  ) ) )  -> 
( b  u.  {
c } )  C_  ( N  X.  N
) )
107 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 )
10811, 12, 13matbas2i 19091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  e.  B  ->  a  e.  ( K  ^m  ( N  X.  N ) ) )
109 elmapi 7433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  e.  ( K  ^m  ( N  X.  N
) )  ->  a : ( N  X.  N ) --> K )
110108, 109syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  B  ->  a : ( N  X.  N ) --> K )
1111103ad2ant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  a : ( N  X.  N ) --> K )
112111feqmptd 5901 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  a  =  ( e  e.  ( N  X.  N
)  |->  ( a `  e ) ) )
113112reseq1d 5261 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
114533ad2ant1 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  R  e.  Ring )
115 ringgrp 17398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( R  e.  Ring  ->  R  e. 
Grp )
116114, 115syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  R  e.  Grp )
117116adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  R  e.  Grp )
118111adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  a : ( N  X.  N ) --> K )
119 simp2 995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
b  u.  { c } )  C_  ( N  X.  N ) )
120119unssbd 3668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  { c }  C_  ( N  X.  N ) )
121 vex 3109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  c  e. 
_V
122121snss 4140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  e.  ( N  X.  N )  <->  { c }  C_  ( N  X.  N ) )
123120, 122sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  c  e.  ( N  X.  N
) )
124 xp1st 6803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( c  e.  ( N  X.  N )  ->  ( 1st `  c )  e.  N )
125123, 124syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( 1st `  c )  e.  N )
126125snssd 4161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  { ( 1st `  c ) }  C_  N )
127 xpss1 5099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( { ( 1st `  c
) }  C_  N  ->  ( { ( 1st `  c ) }  X.  N )  C_  ( N  X.  N ) )
128126, 127syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( { ( 1st `  c
) }  X.  N
)  C_  ( N  X.  N ) )
129128sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  e  e.  ( N  X.  N
) )
130118, 129ffvelrnd 6008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (
a `  e )  e.  K )
13112, 50ringidcl 17414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( R  e.  Ring  ->  .1.  e.  K )
132114, 131syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  .1.  e.  K )
13312, 49ring0cl 17415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( R  e.  Ring  ->  .0.  e.  K )
134114, 133syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  .0.  e.  K )
135132, 134ifcld 3972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  if ( e  e.  d ,  .1.  ,  .0.  )  e.  K )
136135adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
137 eqid 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -g `  R )  =  (
-g `  R )
13812, 51, 137grpnpcan 16329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
139117, 130, 136, 138syl3anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
140139eqcomd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) ) )
141140adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) ) )
142 iftrue 3935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) ) )
143 iftrue 3935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( e  =  c  ->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) )  =  if ( e  e.  d ,  .1.  ,  .0.  )
)
144142, 143oveq12d 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) ) )
145144adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  )
) )
146141, 145eqtr4d 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
14712, 51, 49grplid 16279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( R  e.  Grp  /\  ( a `  e
)  e.  K )  ->  (  .0.  .+  ( a `  e
) )  =  ( a `  e ) )
148117, 130, 147syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (  .0.  .+  ( a `  e ) )  =  ( a `  e
) )
149148eqcomd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (
a `  e )  =  (  .0.  .+  (
a `  e )
) )
150149adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
151 iffalse 3938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( -.  e  =  c  ->  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  =  .0.  )
152 iffalse 3938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( -.  e  =  c  ->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) )  =  ( a `
 e ) )
153151, 152oveq12d 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
154153adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
155150, 154eqtr4d 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
156146, 155pm2.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 ) ) ) )
157156mpteq2dva 4525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
158 snfi 7589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  { ( 1st `  c ) }  e.  Fin
15963ad2ant1 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  N  e.  Fin )
160 xpfi 7783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( { ( 1st `  c
) }  e.  Fin  /\  N  e.  Fin )  ->  ( { ( 1st `  c ) }  X.  N )  e.  Fin )
161158, 159, 160sylancr 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( { ( 1st `  c
) }  X.  N
)  e.  Fin )
162 ovex 6298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( a `  e ) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) )  e. 
_V
163 fvex 5858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 0g
`  R )  e. 
_V
16449, 163eqeltri 2538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  .0.  e.  _V
165162, 164ifex 3997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  )  e.  _V
166165a1i 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 )
167 fvex 5858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 1r
`  R )  e. 
_V
16850, 167eqeltri 2538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  .1.  e.  _V
169168, 164ifex 3997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  if ( e  e.  d ,  .1.  ,  .0.  )  e.  _V
170 fvex 5858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a `
 e )  e. 
_V
171169, 170ifex 3997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `
 e ) )  e.  _V
172171a1i 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 )
173 xp1st 6803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  e.  ( { ( 1st `  c ) }  X.  N )  ->  ( 1st `  e
)  e.  { ( 1st `  c ) } )
174 elsni 4041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 1st `  e )  e.  { ( 1st `  c ) }  ->  ( 1st `  e )  =  ( 1st `  c
) )
175 iftrue 3935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) )
176173, 174, 1753syl 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.  ) )
177176mpteq2ia 4521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) )
178177a1i 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.  )
) )
179 eqidd 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
180161, 166, 172, 178, 179offval2 6529 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
181157, 180eqtr4d 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
182128resmptd 5313 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
183128resmptd 5313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
184128resmptd 5313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
185183, 184oveq12d 6288 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
186181, 182, 1853eqtr4d 2505 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
187113, 186eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
188112reseq1d 5261 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
189 xp1st 6803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  e.  ( ( N 
\  { ( 1st `  c ) } )  X.  N )  -> 
( 1st `  e
)  e.  ( N 
\  { ( 1st `  c ) } ) )
190 eldifsni 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 1st `  e )  e.  ( N  \  { ( 1st `  c
) } )  -> 
( 1st `  e
)  =/=  ( 1st `  c ) )
191189, 190syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( e  e.  ( ( N 
\  { ( 1st `  c ) } )  X.  N )  -> 
( 1st `  e
)  =/=  ( 1st `  c ) )
192191neneqd 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( e  e.  ( ( N 
\  { ( 1st `  c ) } )  X.  N )  ->  -.  ( 1st `  e
)  =  ( 1st `  c ) )
193192adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  ->  -.  ( 1st `  e
)  =  ( 1st `  c ) )
194193iffalsed 3940 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
195194mpteq2dva 4525 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
196 difss 3617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N 
\  { ( 1st `  c ) } ) 
C_  N
197 xpss1 5099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  \  { ( 1st `  c ) } )  C_  N  ->  ( ( N  \  { ( 1st `  c
) } )  X.  N )  C_  ( N  X.  N ) )
198196, 197ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  \  { ( 1st `  c ) } )  X.  N
)  C_  ( N  X.  N )
199 resmpt 5311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
200198, 199mp1i 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 ) ) ) )
201 resmpt 5311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
202198, 201mp1i 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 ) ) )
203195, 200, 2023eqtr4rd 2506 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
204188, 203eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
205 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( e  =  c  ->  ( 1st `  e )  =  ( 1st `  c
) )
206193, 205nsyl 121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  ->  -.  e  =  c
)
207206iffalsed 3940 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
208207mpteq2dva 4525 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
209 resmpt 5311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
210198, 209mp1i 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 ) ) ) )
211208, 210, 2023eqtr4rd 2506 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
212188, 211eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
213135adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
214111ffvelrnda 6007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  ( a `  e )  e.  K
)
215213, 214ifcld 3972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
216 eqid 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
217215, 216fmptd 6031 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
218 fvex 5858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Base `  R )  e.  _V
21912, 218eqeltri 2538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  K  e. 
_V
22068anidms 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  Fin  ->  ( N  X.  N )  e. 
Fin )
221159, 220syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( N  X.  N )  e. 
Fin )
222 elmapg 7425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
223219, 221, 222sylancr 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
224217, 223mpbird 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 ) ) )
22511, 12matbas2 19090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( K  ^m  ( N  X.  N ) )  =  ( Base `  A
) )
226159, 114, 225syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( K  ^m  ( N  X.  N ) )  =  ( Base `  A
) )
227226, 13syl6eqr 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( K  ^m  ( N  X.  N ) )  =  B )
228224, 227eleqtrd 2544 . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
229 simp3 996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  a  e.  B )
230116adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  R  e.  Grp )
23112, 137grpsubcl 16317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
232230, 214, 213, 231syl3anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
233134adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  .0.  e.  K
)
234232, 233ifcld 3972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
235234, 214ifcld 3972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
236 eqid 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
237235, 236fmptd 6031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
238 elmapg 7425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
239219, 221, 238sylancr 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
240237, 239mpbird 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
) ) )
241240, 227eleqtrd 2544 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
242563ad2ant1 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
243 reseq1 5256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  a  ->  (
x  |`  ( { w }  X.  N ) )  =  ( a  |`  ( { w }  X.  N ) ) )
244243eqeq1d 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
245 reseq1 5256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  a  ->  (
x  |`  ( ( N 
\  { w }
)  X.  N ) )  =  ( a  |`  ( ( N  \  { w } )  X.  N ) ) )
246245eqeq1d 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  a  ->  (
( x  |`  (
( N  \  {
w } )  X.  N ) )  =  ( y  |`  (
( N  \  {
w } )  X.  N ) )  <->  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) ) ) )
247245eqeq1d 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  a  ->  (
( x  |`  (
( N  \  {
w } )  X.  N ) )  =  ( z  |`  (
( N  \  {
w } )  X.  N ) )  <->  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) ) )
248244, 246, 2473anbi123d 1297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
249 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  a  ->  ( D `  x )  =  ( D `  a ) )
250249eqeq1d 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  =  a  ->  (
( D `  x
)  =  ( ( D `  y ) 
.+  ( D `  z ) )  <->  ( D `  a )  =  ( ( D `  y
)  .+  ( D `  z ) ) ) )
251248, 250imbi12d 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
2522512ralbidv 2898 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
253 reseq1 5256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
254253oveq1d 6285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
255254eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
256 reseq1 5256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
257256eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
258255, 2573anbi12d 1298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
259 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
260259oveq1d 6285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
261260eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  ( e  e.  ( N  X.  N
)  |->  if ( ( 1st `  e )  =  ( 1st `  c
) ,  if ( e  =  c ,  ( ( a