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

Theorem mdetunilem9 18395
Description: Lemma for mdetuni 18397. (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 3777 . . . 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 5669 . . . . . . . 8  |-  (  _I  |`  N ) : N -1-1-onto-> N
4 f1of 5634 . . . . . . . 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 7219 . . . . . . . 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 18292 . . . . . . . . . . . . . . . 16  |-  ( y  e.  B  ->  y  e.  ( K  ^m  ( N  X.  N ) ) )
16 elmapi 7226 . . . . . . . . . . . . . . . 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 5737 . . . . . . . . . . . . . 14  |-  ( y  e.  B  ->  y  =  ( w  e.  ( N  X.  N
)  |->  ( y `  w ) ) )
1918fveq2d 5688 . . . . . . . . . . . . 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 2437 . . . . . . . . . . . . . 14  |-  ( N  X.  N )  =  ( N  X.  N
)
22 mpteq12 4364 . . . . . . . . . . . . . . 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 5688 . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . . . . 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 1761 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  z  ->  (
w  e.  a  <->  w  e.  z ) )
2928ifbid 3804 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  z  ->  if ( w  e.  a ,  .1.  ,  .0.  )  =  if ( w  e.  z ,  .1.  ,  .0.  ) )
3029mpteq2dv 4372 . . . . . . . . . . . . . . . . . 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 5688 . . . . . . . . . . . . . . . . 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 2445 . . . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  <. b ,  c
>.  ->  ( w  e.  a  <->  <. b ,  c
>.  e.  a ) )
3534ifbid 3804 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  <. b ,  c
>.  ->  if ( w  e.  a ,  .1.  ,  .0.  )  =  if ( <. b ,  c
>.  e.  a ,  .1.  ,  .0.  ) )
3635mpt2mpt 6177 . . . . . . . . . . . . . . . . . 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 7226 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  e.  ( N  ^m  N )  ->  a : N --> N )
3837adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  a : N
--> N )
39 ffn 5552 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a : N --> N  -> 
a  Fn  N )
4038, 39syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  a  Fn  N )
41403ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  a  Fn  N )
42 simp2 989 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  a  e.  ( N  ^m  N
) )  /\  b  e.  N  /\  c  e.  N )  ->  b  e.  N )
43 fnopfvb 5726 . . . . . . . . . . . . . . . . . . . . . 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 3804 . . . . . . . . . . . . . . . . . . 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 6145 . . . . . . . . . . . . . . . . . 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 2481 . . . . . . . . . . . . . . . . 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 5688 . . . . . . . . . . . . . . . 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 18394 . . . . . . . . . . . . . . . . 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 2469 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  a  e.  ( N  ^m  N ) )  ->  ( D `  ( w  e.  ( N  X.  N ) 
|->  if ( w  e.  a ,  .1.  ,  .0.  ) ) )  =  .0.  )
6333, 62chvarv 1958 . . . . . . . . . . . . . 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 2473 . . . . . . . . . . 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 2802 . . . . . . . . 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 7575 . . . . . . . . . . 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 2911 . . . . . . . . . . . . 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 2751 . . . . . . . . . . 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 3101 . . . . . . . . . 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 3368 . . . . . . . . 9  |-  ( N  X.  N )  C_  ( N  X.  N
)
79703ad2ant1 1009 . . . . . . . . . . 11  |-  ( (
ph  /\  ( N  X.  N )  C_  ( N  X.  N )  /\  -.  (/)  e.  Y )  ->  ( N  X.  N )  e.  Fin )
80 sseq1 3370 . . . . . . . . . . . . . 14  |-  ( a  =  (/)  ->  ( a 
C_  ( N  X.  N )  <->  (/)  C_  ( N  X.  N ) ) )
81803anbi2d 1294 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  ( (
ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  <->  ( ph  /\  (/)  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
) ) )
82 eleq1 2497 . . . . . . . . . . . . . 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 3370 . . . . . . . . . . . . . 14  |-  ( a  =  b  ->  (
a  C_  ( N  X.  N )  <->  b  C_  ( N  X.  N
) ) )
86853anbi2d 1294 . . . . . . . . . . . . 13  |-  ( a  =  b  ->  (
( ph  /\  a  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
)  <->  ( ph  /\  b  C_  ( N  X.  N )  /\  -.  (/) 
e.  Y ) ) )
87 eleq1 2497 . . . . . . . . . . . . . 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 3370 . . . . . . . . . . . . . 14  |-  ( a  =  ( b  u. 
{ c } )  ->  ( a  C_  ( N  X.  N
)  <->  ( b  u. 
{ c } ) 
C_  ( N  X.  N ) ) )
91903anbi2d 1294 . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . 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 3370 . . . . . . . . . . . . . 14  |-  ( a  =  ( N  X.  N )  ->  (
a  C_  ( N  X.  N )  <->  ( N  X.  N )  C_  ( N  X.  N ) ) )
96953anbi2d 1294 . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . 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 990 . . . . . . . . . . . 12  |-  ( (
ph  /\  (/)  C_  ( N  X.  N )  /\  -.  (/)  e.  Y )  ->  -.  (/)  e.  Y
)
101 id 22 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ph )
102 ssun1 3512 . . . . . . . . . . . . . . . 16  |-  b  C_  ( b  u.  {
c } )
103 sstr2 3356 . . . . . . . . . . . . . . . 16  |-  ( b 
C_  ( b  u. 
{ c } )  ->  ( ( b  u.  { c } )  C_  ( N  X.  N )  ->  b  C_  ( N  X.  N
) ) )
104102, 103ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( b  u.  { c } )  C_  ( N  X.  N )  -> 
b  C_  ( N  X.  N ) )
105 id 22 . . . . . . . . . . . . . . 15  |-  ( -.  (/)  e.  Y  ->  -.  (/) 
e.  Y )
106101, 104, 1053anim123i 1173 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  -.  (/) 
e.  Y )  -> 
( ph  /\  b  C_  ( N  X.  N
)  /\  -.  (/)  e.  Y
) )
107106imim1i 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 ) )
108 simpl1 991 . . . . . . . . . . . . . . . . . . . . . . . 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 )
109 simpl2 992 . . . . . . . . . . . . . . . . . . . . . . . 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
) )
110 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 )
11112, 13, 14matbas2i 18292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  e.  B  ->  a  e.  ( K  ^m  ( N  X.  N ) ) )
112 elmapi 7226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  e.  ( K  ^m  ( N  X.  N
) )  ->  a : ( N  X.  N ) --> K )
113111, 112syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  B  ->  a : ( N  X.  N ) --> K )
1141133ad2ant3 1011 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  a : ( N  X.  N ) --> K )
115114feqmptd 5737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  a  =  ( e  e.  ( N  X.  N
)  |->  ( a `  e ) ) )
116115reseq1d 5101 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
117543ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  R  e.  Ring )
118 rnggrp 16636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( R  e.  Ring  ->  R  e. 
Grp )
119117, 118syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  R  e.  Grp )
120119adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  R  e.  Grp )
121114adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  a : ( N  X.  N ) --> K )
122 simp2 989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  (
b  u.  { c } )  C_  ( N  X.  N ) )
123122unssbd 3527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  { c }  C_  ( N  X.  N ) )
124 vex 2969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  c  e. 
_V
125124snss 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( c  e.  ( N  X.  N )  <->  { c }  C_  ( N  X.  N ) )
126123, 125sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  c  e.  ( N  X.  N
) )
127 xp1st 6601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( c  e.  ( N  X.  N )  ->  ( 1st `  c )  e.  N )
128126, 127syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( 1st `  c )  e.  N )
129128snssd 4011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  { ( 1st `  c ) }  C_  N )
130 xpss1 4940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( { ( 1st `  c
) }  C_  N  ->  ( { ( 1st `  c ) }  X.  N )  C_  ( N  X.  N ) )
131129, 130syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( { ( 1st `  c
) }  X.  N
)  C_  ( N  X.  N ) )
132131sselda 3349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  e  e.  ( N  X.  N
) )
133121, 132ffvelrnd 5837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (
a `  e )  e.  K )
13413, 51rngidcl 16651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( R  e.  Ring  ->  .1.  e.  K )
135117, 134syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  .1.  e.  K )
13613, 50rng0cl 16652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( R  e.  Ring  ->  .0.  e.  K )
137117, 136syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  .0.  e.  K )
138135, 137ifcld 3825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  if ( e  e.  d ,  .1.  ,  .0.  )  e.  K )
139138adantr 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 )
140 eqid 2437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( -g `  R )  =  (
-g `  R )
14113, 52, 140grpnpcan 15606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
142120, 133, 139, 141syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
143142eqcomd 2442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) ) )
144143adantr 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.  ) ) )
145 iftrue 3790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) ) )
146 iftrue 3790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( e  =  c  ->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) )  =  if ( e  e.  d ,  .1.  ,  .0.  )
)
147145, 146oveq12d 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) ) )
148147adantl 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.  )
) )
149144, 148eqtr4d 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
15013, 52, 50grplid 15557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( R  e.  Grp  /\  ( a `  e
)  e.  K )  ->  (  .0.  .+  ( a `  e
) )  =  ( a `  e ) )
151120, 133, 150syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (  .0.  .+  ( a `  e ) )  =  ( a `  e
) )
152151eqcomd 2442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( { ( 1st `  c
) }  X.  N
) )  ->  (
a `  e )  =  (  .0.  .+  (
a `  e )
) )
153152adantr 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 ) ) )
154 iffalse 3792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( -.  e  =  c  ->  if ( e  =  c ,  ( ( a `
 e ) (
-g `  R ) if ( e  e.  d ,  .1.  ,  .0.  ) ) ,  .0.  )  =  .0.  )
155 iffalse 3792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( -.  e  =  c  ->  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `  e ) )  =  ( a `
 e ) )
156154, 155oveq12d 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
157156adantl 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
) ) )
158153, 157eqtr4d 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
159149, 158pm2.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 ) ) ) )
160159mpteq2dva 4371 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
161 snfi 7382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  { ( 1st `  c ) }  e.  Fin
16263ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  N  e.  Fin )
163 xpfi 7575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( { ( 1st `  c
) }  e.  Fin  /\  N  e.  Fin )  ->  ( { ( 1st `  c ) }  X.  N )  e.  Fin )
164161, 162, 163sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( { ( 1st `  c
) }  X.  N
)  e.  Fin )
165 ovex 6111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( a `  e ) ( -g `  R
) if ( e  e.  d ,  .1.  ,  .0.  ) )  e. 
_V
166 fvex 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 0g
`  R )  e. 
_V
16750, 166eqeltri 2507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  .0.  e.  _V
168165, 167ifex 3851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  if ( e  =  c ,  ( ( a `  e ) ( -g `  R ) if ( e  e.  d ,  .1.  ,  .0.  )
) ,  .0.  )  e.  _V
169168a1i 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 )
170 fvex 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 1r
`  R )  e. 
_V
17151, 170eqeltri 2507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  .1.  e.  _V
172171, 167ifex 3851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  if ( e  e.  d ,  .1.  ,  .0.  )  e.  _V
173 fvex 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a `
 e )  e. 
_V
174172, 173ifex 3851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  if ( e  =  c ,  if ( e  e.  d ,  .1.  ,  .0.  ) ,  ( a `
 e ) )  e.  _V
175174a1i 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 )
176 xp1st 6601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  e.  ( { ( 1st `  c ) }  X.  N )  ->  ( 1st `  e
)  e.  { ( 1st `  c ) } )
177 elsni 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 1st `  e )  e.  { ( 1st `  c ) }  ->  ( 1st `  e )  =  ( 1st `  c
) )
178 iftrue 3790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) )
179176, 177, 1783syl 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.  ) )
180179mpteq2ia 4367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ) )
181180a1i 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.  )
) )
182 eqidd 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
183164, 169, 175, 181, 182offval2 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
184160, 183eqtr4d 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
185 resmpt 5149 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( { ( 1st `  c
) }  X.  N
)  C_  ( N  X.  N )  ->  (
( e  e.  ( N  X.  N ) 
|->  ( a `  e
) )  |`  ( { ( 1st `  c
) }  X.  N
) )  =  ( e  e.  ( { ( 1st `  c
) }  X.  N
)  |->  ( a `  e ) ) )
186131, 185syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
187 resmpt 5149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( { ( 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 ) ) )  |`  ( { ( 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 ) ) ) )
188131, 187syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
189 resmpt 5149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( { ( 1st `  c
) }  X.  N
)  C_  ( N  X.  N )  ->  (
( 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 ) ) ) )
190131, 189syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
191188, 190oveq12d 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
192184, 186, 1913eqtr4d 2479 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
193116, 192eqtrd 2469 . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
194115reseq1d 5101 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
195 xp1st 6601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  e.  ( ( N 
\  { ( 1st `  c ) } )  X.  N )  -> 
( 1st `  e
)  e.  ( N 
\  { ( 1st `  c ) } ) )
196 eldifsni 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 1st `  e )  e.  ( N  \  { ( 1st `  c
) } )  -> 
( 1st `  e
)  =/=  ( 1st `  c ) )
197195, 196syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( e  e.  ( ( N 
\  { ( 1st `  c ) } )  X.  N )  -> 
( 1st `  e
)  =/=  ( 1st `  c ) )
198197neneqd 2618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( e  e.  ( ( N 
\  { ( 1st `  c ) } )  X.  N )  ->  -.  ( 1st `  e
)  =  ( 1st `  c ) )
199198adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  ->  -.  ( 1st `  e
)  =  ( 1st `  c ) )
200 iffalse 3792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( -.  ( 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 ) )  =  ( a `  e
) )
201199, 200syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
202201mpteq2dva 4371 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
203 difss 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N 
\  { ( 1st `  c ) } ) 
C_  N
204 xpss1 4940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  \  { ( 1st `  c ) } )  C_  N  ->  ( ( N  \  { ( 1st `  c
) } )  X.  N )  C_  ( N  X.  N ) )
205203, 204ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  \  { ( 1st `  c ) } )  X.  N
)  C_  ( N  X.  N )
206 resmpt 5149 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
207205, 206mp1i 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 ) ) ) )
208 resmpt 5149 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
209205, 208mp1i 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 ) ) )
210202, 207, 2093eqtr4rd 2480 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
211194, 210eqtrd 2469 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
212 fveq2 5684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( e  =  c  ->  ( 1st `  e )  =  ( 1st `  c
) )
213199, 212nsyl 121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  (
( N  \  {
( 1st `  c
) } )  X.  N ) )  ->  -.  e  =  c
)
214213, 155syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
215214mpteq2dva 4371 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
216 resmpt 5149 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
217205, 216mp1i 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 ) ) ) )
218215, 217, 2093eqtr4rd 2480 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
219194, 218eqtrd 2469 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
220138adantr 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
)
221114ffvelrnda 5836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  ( a `  e )  e.  K
)
222220, 221ifcld 3825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
223 eqid 2437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
224222, 223fmptd 5860 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
225 fvex 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( Base `  R )  e.  _V
22613, 225eqeltri 2507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  K  e. 
_V
22769anidms 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  Fin  ->  ( N  X.  N )  e. 
Fin )
228162, 227syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( N  X.  N )  e. 
Fin )
229 elmapg 7219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
230226, 228, 229sylancr 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 ) )
231224, 230mpbird 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 ) ) )
23212, 13matbas2 18291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( N  e.  Fin  /\  R  e.  Ring )  -> 
( K  ^m  ( N  X.  N ) )  =  ( Base `  A
) )
233162, 117, 232syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( K  ^m  ( N  X.  N ) )  =  ( Base `  A
) )
234233, 14syl6eqr 2487 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  ( K  ^m  ( N  X.  N ) )  =  B )
235231, 234eleqtrd 2513 . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
236 simp3 990 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( b  u.  { c } ) 
C_  ( N  X.  N )  /\  a  e.  B )  ->  a  e.  B )
237119adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  R  e.  Grp )
23813, 140grpsubcl 15595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
239237, 221, 220, 238syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
240137adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  (
b  u.  { c } )  C_  ( N  X.  N )  /\  a  e.  B )  /\  e  e.  ( N  X.  N ) )  ->  .0.  e.  K
)
241239, 240ifcld 3825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
242241, 221ifcld 3825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
243 eqid 2437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
244242, 243fmptd 5860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
245 elmapg 7219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
246226, 228, 245sylancr 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 ) )
247244, 246mpbird 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
) ) )
248247, 234eleqtrd 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
249573ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
250 reseq1 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  a  ->  (
x  |`  ( { w }  X.  N ) )  =  ( a  |`  ( { w }  X.  N ) ) )
251250eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
252 reseq1 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  a  ->  (
x  |`  ( ( N 
\  { w }
)  X.  N ) )  =  ( a  |`  ( ( N  \  { w } )  X.  N ) ) )
253252eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  a  ->  (
( x  |`  (
( N  \  {
w } )  X.  N ) )  =  ( y  |`  (
( N  \  {
w } )  X.  N ) )  <->  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( y  |`  ( ( N  \  { w } )  X.  N ) ) ) )
254252eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  a  ->  (
( x  |`  (
( N  \  {
w } )  X.  N ) )  =  ( z  |`  (
( N  \  {
w } )  X.  N ) )  <->  ( a  |`  ( ( N  \  { w } )  X.  N ) )  =  ( z  |`  ( ( N  \  { w } )  X.  N ) ) ) )
255251, 253, 2543anbi123d 1289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
256 fveq2 5684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  a  ->  ( D `  x )  =  ( D `  a ) )
257256eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  =  a  ->  (
( D `  x
)  =  ( ( D `  y ) 
.+  ( D `  z ) )  <->  ( D `  a )  =  ( ( D `  y
)  .+  ( D `  z ) ) ) )
258255, 257imbi12d 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 ) ) ) ) )
2592582ralbidv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
260 reseq1 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
261260oveq1d 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
262261eqeq2d 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
263 reseq1 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
264263eqeq2d 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
265262, 2643anbi12d 1290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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