Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axlowdim Structured version   Unicode version

Theorem axlowdim 25892
Description: The general lower dimensional axiom. Take a dimension  N greater than or equal to three. Then, there are three non-colinear points in  N dimensional space that are equidistant from  N  -  1 distinct points. Derived from remarks in "Tarski's System of Geometry", by Alfred Tarski and Steven Givant, Bull. Symbolic Logic Volume 5, Number 2 (1999), 175-214. (Contributed by Scott Fenton, 22-Apr-2013.)
Assertion
Ref Expression
axlowdim  |-  ( N  e.  ( ZZ>= `  3
)  ->  E. p E. x  e.  ( EE `  N ) E. y  e.  ( EE
`  N ) E. z  e.  ( EE
`  N ) ( p : ( 1 ... ( N  - 
1 ) ) -1-1-> ( EE `  N )  /\  A. i  e.  ( 2 ... ( N  -  1 ) ) ( <. (
p `  1 ) ,  x >.Cgr <. ( p `  i ) ,  x >.  /\  <. ( p ` 
1 ) ,  y
>.Cgr <. ( p `  i ) ,  y
>.  /\  <. ( p ` 
1 ) ,  z
>.Cgr <. ( p `  i ) ,  z
>. )  /\  -.  (
x  Btwn  <. y ,  z >.  \/  y  Btwn  <. z ,  x >.  \/  z  Btwn  <. x ,  y >. )
) )
Distinct variable group:    i, N, p, x, y, z

Proof of Theorem axlowdim
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 2re 10061 . . . . . . . 8  |-  2  e.  RR
2 3re 10063 . . . . . . . 8  |-  3  e.  RR
3 2lt3 10135 . . . . . . . 8  |-  2  <  3
41, 2, 3ltleii 9188 . . . . . . 7  |-  2  <_  3
5 2z 10304 . . . . . . . 8  |-  2  e.  ZZ
6 3nn 10126 . . . . . . . . 9  |-  3  e.  NN
76nnzi 10297 . . . . . . . 8  |-  3  e.  ZZ
8 eluz 10491 . . . . . . . 8  |-  ( ( 2  e.  ZZ  /\  3  e.  ZZ )  ->  ( 3  e.  (
ZZ>= `  2 )  <->  2  <_  3 ) )
95, 7, 8mp2an 654 . . . . . . 7  |-  ( 3  e.  ( ZZ>= `  2
)  <->  2  <_  3
)
104, 9mpbir 201 . . . . . 6  |-  3  e.  ( ZZ>= `  2 )
11 uzss 10498 . . . . . 6  |-  ( 3  e.  ( ZZ>= `  2
)  ->  ( ZZ>= ` 
3 )  C_  ( ZZ>=
`  2 ) )
1210, 11ax-mp 8 . . . . 5  |-  ( ZZ>= ` 
3 )  C_  ( ZZ>=
`  2 )
1312sseli 3336 . . . 4  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( ZZ>= `  2 )
)
14 0re 9083 . . . . 5  |-  0  e.  RR
1514, 14axlowdimlem5 25877 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
1613, 15syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
17 1re 9082 . . . . 5  |-  1  e.  RR
1817, 14axlowdimlem5 25877 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
1913, 18syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
2014, 17axlowdimlem5 25877 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
2113, 20syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
22 eqid 2435 . . . 4  |-  ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) )  =  ( k  e.  ( 1 ... ( N  - 
1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. ( k  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( k  +  1 ) } )  X.  { 0 } ) ) ) )
2322axlowdimlem15 25887 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) : ( 1 ... ( N  -  1 ) )
-1-1-> ( EE `  N
) )
24 eqid 2435 . . . . . 6  |-  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )  =  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )
25 eqid 2435 . . . . . 6  |-  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) )
26 eqid 2435 . . . . . 6  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
2724, 25, 26, 14, 14axlowdimlem17 25889 . . . . 5  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  <. ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( { <. (
i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)
28 eqid 2435 . . . . . 6  |-  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
2924, 25, 28, 17, 14axlowdimlem17 25889 . . . . 5  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  <. ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( { <. (
i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)
30 eqid 2435 . . . . . 6  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
3124, 25, 30, 14, 17axlowdimlem17 25889 . . . . 5  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  <. ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( { <. (
i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)
32 1z 10303 . . . . . . . . . . . . . . 15  |-  1  e.  ZZ
3332a1i 11 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  1  e.  ZZ )
34 peano2zm 10312 . . . . . . . . . . . . . . 15  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
35343ad2ant2 979 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  ( N  -  1 )  e.  ZZ )
36 2m1e1 10087 . . . . . . . . . . . . . . 15  |-  ( 2  -  1 )  =  1
37 zre 10278 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ZZ  ->  N  e.  RR )
38 letr 9159 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR  /\  3  e.  RR  /\  N  e.  RR )  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
391, 2, 38mp3an12 1269 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  RR  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
4037, 39syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ZZ  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
414, 40mpani 658 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ZZ  ->  (
3  <_  N  ->  2  <_  N ) )
4241imp 419 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ZZ  /\  3  <_  N )  -> 
2  <_  N )
43423adant1 975 . . . . . . . . . . . . . . . 16  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  2  <_  N )
44373ad2ant2 979 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  N  e.  RR )
45 lesub1 9514 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  N  e.  RR  /\  1  e.  RR )  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
461, 17, 45mp3an13 1270 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  RR  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
4744, 46syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
4843, 47mpbid 202 . . . . . . . . . . . . . . 15  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
2  -  1 )  <_  ( N  - 
1 ) )
4936, 48syl5eqbrr 4238 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  1  <_  ( N  -  1 ) )
5033, 35, 493jca 1134 . . . . . . . . . . . . 13  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
1  e.  ZZ  /\  ( N  -  1
)  e.  ZZ  /\  1  <_  ( N  - 
1 ) ) )
51 eluz2 10486 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  3
)  <->  ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N ) )
52 eluz2 10486 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  ( N  -  1 )  e.  ZZ  /\  1  <_ 
( N  -  1 ) ) )
5350, 51, 523imtr4i 258 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ( ZZ>= `  1 )
)
54 eluzfz1 11056 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
5553, 54syl 16 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
5655adantr 452 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
57 eqeq1 2441 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
k  =  1  <->  1  =  1 ) )
58 oveq1 6080 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
k  +  1 )  =  ( 1  +  1 ) )
5958opeq1d 3982 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  <. (
k  +  1 ) ,  1 >.  =  <. ( 1  +  1 ) ,  1 >. )
6059sneqd 3819 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  { <. ( k  +  1 ) ,  1 >. }  =  { <. ( 1  +  1 ) ,  1
>. } )
6158sneqd 3819 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  { ( k  +  1 ) }  =  { ( 1  +  1 ) } )
6261difeq2d 3457 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 1 ... N
)  \  { (
k  +  1 ) } )  =  ( ( 1 ... N
)  \  { (
1  +  1 ) } ) )
6362xpeq1d 4893 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( ( 1 ... N )  \  {
( k  +  1 ) } )  X. 
{ 0 } )  =  ( ( ( 1 ... N ) 
\  { ( 1  +  1 ) } )  X.  { 0 } ) )
6460, 63uneq12d 3494 . . . . . . . . . . . 12  |-  ( k  =  1  ->  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( 1  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( 1  +  1 ) } )  X.  { 0 } ) ) )
6557, 64ifbieq2d 3751 . . . . . . . . . . 11  |-  ( k  =  1  ->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. ( k  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( k  +  1 ) } )  X.  { 0 } ) ) )  =  if ( 1  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( 1  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) ) ) )
66 snex 4397 . . . . . . . . . . . . 13  |-  { <. 3 ,  -u 1 >. }  e.  _V
67 ovex 6098 . . . . . . . . . . . . . . 15  |-  ( 1 ... N )  e. 
_V
68 difexg 4343 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { 3 } )  e.  _V )
6967, 68ax-mp 8 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { 3 } )  e.  _V
70 snex 4397 . . . . . . . . . . . . . 14  |-  { 0 }  e.  _V
7169, 70xpex 4982 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { 3 } )  X.  {
0 } )  e. 
_V
7266, 71unex 4699 . . . . . . . . . . . 12  |-  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )  e.  _V
73 snex 4397 . . . . . . . . . . . . 13  |-  { <. ( 1  +  1 ) ,  1 >. }  e.  _V
74 difexg 4343 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { (
1  +  1 ) } )  e.  _V )
7567, 74ax-mp 8 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { ( 1  +  1 ) } )  e.  _V
7675, 70xpex 4982 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } )  e. 
_V
7773, 76unex 4699 . . . . . . . . . . . 12  |-  ( {
<. ( 1  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) )  e.  _V
7872, 77ifex 3789 . . . . . . . . . . 11  |-  if ( 1  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( 1  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) ) )  e.  _V
7965, 22, 78fvmpt 5798 . . . . . . . . . 10  |-  ( 1  e.  ( 1 ... ( N  -  1 ) )  ->  (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
)  =  if ( 1  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( 1  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) ) ) )
8056, 79syl 16 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
)  =  if ( 1  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( 1  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) ) ) )
81 eqid 2435 . . . . . . . . . 10  |-  1  =  1
82 iftrue 3737 . . . . . . . . . 10  |-  ( 1  =  1  ->  if ( 1  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. ( 1  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( 1  +  1 ) } )  X.  { 0 } ) ) )  =  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) )
8381, 82ax-mp 8 . . . . . . . . 9  |-  if ( 1  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( 1  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) ) )  =  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )
8480, 83syl6eq 2483 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
)  =  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) )
8584opeq1d 3982 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  =  <. ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >. )
86 2nn 10125 . . . . . . . . . . . . . 14  |-  2  e.  NN
87 nnuz 10513 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  1 )
8886, 87eleqtri 2507 . . . . . . . . . . . . 13  |-  2  e.  ( ZZ>= `  1 )
89 fzss1 11083 . . . . . . . . . . . . 13  |-  ( 2  e.  ( ZZ>= `  1
)  ->  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) ) )
9088, 89ax-mp 8 . . . . . . . . . . . 12  |-  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) )
9190sseli 3336 . . . . . . . . . . 11  |-  ( i  e.  ( 2 ... ( N  -  1 ) )  ->  i  e.  ( 1 ... ( N  -  1 ) ) )
9291adantl 453 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  i  e.  ( 1 ... ( N  -  1 ) ) )
93 eqeq1 2441 . . . . . . . . . . . 12  |-  ( k  =  i  ->  (
k  =  1  <->  i  =  1 ) )
94 oveq1 6080 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  (
k  +  1 )  =  ( i  +  1 ) )
9594opeq1d 3982 . . . . . . . . . . . . . 14  |-  ( k  =  i  ->  <. (
k  +  1 ) ,  1 >.  =  <. ( i  +  1 ) ,  1 >. )
9695sneqd 3819 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  { <. ( k  +  1 ) ,  1 >. }  =  { <. ( i  +  1 ) ,  1
>. } )
9794sneqd 3819 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  { ( k  +  1 ) }  =  { ( i  +  1 ) } )
9897difeq2d 3457 . . . . . . . . . . . . . 14  |-  ( k  =  i  ->  (
( 1 ... N
)  \  { (
k  +  1 ) } )  =  ( ( 1 ... N
)  \  { (
i  +  1 ) } ) )
9998xpeq1d 4893 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  (
( ( 1 ... N )  \  {
( k  +  1 ) } )  X. 
{ 0 } )  =  ( ( ( 1 ... N ) 
\  { ( i  +  1 ) } )  X.  { 0 } ) )
10096, 99uneq12d 3494 . . . . . . . . . . . 12  |-  ( k  =  i  ->  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) )
10193, 100ifbieq2d 3751 . . . . . . . . . . 11  |-  ( k  =  i  ->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. ( k  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( k  +  1 ) } )  X.  { 0 } ) ) )  =  if ( i  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) ) ) )
102 snex 4397 . . . . . . . . . . . . 13  |-  { <. ( i  +  1 ) ,  1 >. }  e.  _V
103 difexg 4343 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { (
i  +  1 ) } )  e.  _V )
10467, 103ax-mp 8 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { ( i  +  1 ) } )  e.  _V
105104, 70xpex 4982 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } )  e. 
_V
106102, 105unex 4699 . . . . . . . . . . . 12  |-  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) )  e.  _V
10772, 106ifex 3789 . . . . . . . . . . 11  |-  if ( i  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( i  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) ) )  e.  _V
108101, 22, 107fvmpt 5798 . . . . . . . . . 10  |-  ( i  e.  ( 1 ... ( N  -  1 ) )  ->  (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
)  =  if ( i  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( i  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) ) ) )
10992, 108syl 16 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
)  =  if ( i  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( i  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) ) ) )
110 1lt2 10134 . . . . . . . . . . . . . . . 16  |-  1  <  2
11117, 1ltnlei 9186 . . . . . . . . . . . . . . . 16  |-  ( 1  <  2  <->  -.  2  <_  1 )
112110, 111mpbi 200 . . . . . . . . . . . . . . 15  |-  -.  2  <_  1
113112intnanr 882 . . . . . . . . . . . . . 14  |-  -.  (
2  <_  1  /\  1  <_  ( N  - 
1 ) )
114 eluzelz 10488 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ZZ )
115114, 34syl 16 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ZZ )
116 elfz 11041 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  ZZ  /\  2  e.  ZZ  /\  ( N  -  1 )  e.  ZZ )  -> 
( 1  e.  ( 2 ... ( N  -  1 ) )  <-> 
( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
11732, 5, 116mp3an12 1269 . . . . . . . . . . . . . . 15  |-  ( ( N  -  1 )  e.  ZZ  ->  (
1  e.  ( 2 ... ( N  - 
1 ) )  <->  ( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
118115, 117syl 16 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1  e.  ( 2 ... ( N  -  1 ) )  <->  ( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
119113, 118mtbiri 295 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  3
)  ->  -.  1  e.  ( 2 ... ( N  -  1 ) ) )
120 eleq1 2495 . . . . . . . . . . . . . 14  |-  ( i  =  1  ->  (
i  e.  ( 2 ... ( N  - 
1 ) )  <->  1  e.  ( 2 ... ( N  -  1 ) ) ) )
121120notbid 286 . . . . . . . . . . . . 13  |-  ( i  =  1  ->  ( -.  i  e.  (
2 ... ( N  - 
1 ) )  <->  -.  1  e.  ( 2 ... ( N  -  1 ) ) ) )
122119, 121syl5ibrcom 214 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  =  1  ->  -.  i  e.  ( 2 ... ( N  - 
1 ) ) ) )
123122con2d 109 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 2 ... ( N  -  1 ) )  ->  -.  i  =  1 ) )
124123imp 419 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  -.  i  =  1 )
125 iffalse 3738 . . . . . . . . . 10  |-  ( -.  i  =  1  ->  if ( i  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) )  =  ( { <. (
i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) )
126124, 125syl 16 . . . . . . . . 9  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  if ( i  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) )  =  ( { <. (
i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) )
127109, 126eqtrd 2467 . . . . . . . 8  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
)  =  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) ) )
128127opeq1d 3982 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  =  <. ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)
12985, 128breq12d 4217 . . . . . 6  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  <->  <.
( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( { <. (
i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
) )
13084opeq1d 3982 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  =  <. ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. 1 ,  1 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >. )
131127opeq1d 3982 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  =  <. ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)
132130, 131breq12d 4217 . . . . . 6  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  <->  <.
( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( { <. (
i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
) )
13355, 79syl 16 . . . . . . . . . 10  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( (
k  e.  ( 1 ... ( N  - 
1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. ( k  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( k  +  1 ) } )  X.  { 0 } ) ) ) ) `
 1 )  =  if ( 1  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( 1  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) ) ) )
134133, 83syl6eq 2483 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( (
k  e.  ( 1 ... ( N  - 
1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. ( k  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( k  +  1 ) } )  X.  { 0 } ) ) ) ) `
 1 )  =  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) )
135134opeq1d 3982 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  3
)  ->  <. ( ( k  e.  ( 1 ... ( N  - 
1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. ( k  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( k  +  1 ) } )  X.  { 0 } ) ) ) ) `
 1 ) ,  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) >.  =  <. ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)
136135adantr 452 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  =  <. ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. 1 ,  0 >. , 
<. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >. )
137127opeq1d 3982 . . . . . . 7  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  =  <. ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)
138136, 137breq12d 4217 . . . . . 6  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  <->  <.
( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( { <. (
i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
) )
139129, 132, 1383anbi123d 1254 . . . . 5  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  (
( <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)  <->  ( <. ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( { <. (
i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  /\  <. ( { <. 3 ,  -u 1 >. }  u.  ( (
( 1 ... N
)  \  { 3 } )  X.  {
0 } ) ) ,  ( { <. 1 ,  1 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >.Cgr <. ( { <. ( i  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) ) ,  ( { <. 1 ,  1 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >.  /\  <. ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( { <. (
i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) ,  ( { <. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
) ) )
14027, 29, 31, 139mpbir3and 1137 . . . 4  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  ( <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
) )
141140ralrimiva 2781 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  A. i  e.  ( 2 ... ( N  -  1 ) ) ( <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
) )
14226, 28, 30axlowdimlem6 25878 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  -.  (
( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )  Btwn  <. ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) >.  \/  ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  Btwn  <.
( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  \/  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )  Btwn  <. ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  ( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) >. ) )
14313, 142syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  -.  (
( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )  Btwn  <. ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) >.  \/  ( { <. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  Btwn  <.
( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  \/  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )  Btwn  <. ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  ( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) ) >. ) )
144 opeq2 3977 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  x >.  = 
<. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)
145 opeq2 3977 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  x >.  = 
<. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)
146144, 145breq12d 4217 . . . . . . 7  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  ( <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  x >.Cgr <.
( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  x >.  <->  <. ( ( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
) )
1471463anbi1d 1258 . . . . . 6  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  (
( <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  x >.Cgr <.
( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  x >.  /\ 
<. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  y >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  y >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  z >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  z >.
)  <->  ( <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  y >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  y >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  z >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  z >.
) ) )
148147ralbidv 2717 . . . . 5  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  ( A. i  e.  (
2 ... ( N  - 
1 ) ) (
<. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  x >.Cgr <.
( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  x >.  /\ 
<. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  y >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  y >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  z >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  z >.
)  <->  A. i  e.  ( 2 ... ( N  -  1 ) ) ( <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  y >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  y >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  z >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  z >.
) ) )
149 breq1 4207 . . . . . . 7  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  (
x  Btwn  <. y ,  z >.  <->  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  Btwn  <. y ,  z >. )
)
150 opeq2 3977 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. z ,  x >.  =  <. z ,  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >. )
151150breq2d 4216 . . . . . . 7  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  (
y  Btwn  <. z ,  x >.  <->  y  Btwn  <. z ,  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >. )
)
152 opeq1 3976 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. x ,  y >.  =  <. ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  y >. )
153152breq2d 4216 . . . . . . 7  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  (
z  Btwn  <. x ,  y >.  <->  z  Btwn  <. ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  y >. ) )
154149, 151, 1533orbi123d 1253 . . . . . 6  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  (
( x  Btwn  <. y ,  z >.  \/  y  Btwn  <. z ,  x >.  \/  z  Btwn  <. x ,  y >. )  <->  ( ( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )  Btwn  <. y ,  z >.  \/  y  Btwn  <. z ,  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  \/  z  Btwn  <. ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  y >. ) ) )
155154notbid 286 . . . . 5  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  ( -.  ( x  Btwn  <. y ,  z >.  \/  y  Btwn  <. z ,  x >.  \/  z  Btwn  <. x ,  y >. )  <->  -.  ( ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  Btwn  <. y ,  z >.  \/  y  Btwn  <. z ,  ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  \/  z  Btwn  <. ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  y >. ) ) )
156148, 1553anbi23d 1257 . . . 4  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  (
( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) : ( 1 ... ( N  -  1 ) )
-1-1-> ( EE `  N
)  /\  A. i  e.  ( 2 ... ( N  -  1 ) ) ( <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  x >.Cgr <.
( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  x >.  /\ 
<. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  y >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  y >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  z >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  z >.
)  /\  -.  (
x  Btwn  <. y ,  z >.  \/  y  Btwn  <. z ,  x >.  \/  z  Btwn  <. x ,  y >. )
)  <->  ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) : ( 1 ... ( N  -  1 ) )
-1-1-> ( EE `  N
)  /\  A. i  e.  ( 2 ... ( N  -  1 ) ) ( <. (
( k  e.  ( 1 ... ( N  -  1 ) ) 
|->  if ( k  =  1 ,  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  y >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  y >.  /\  <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u 1 >. }  u.  ( ( ( 1 ... N )  \  { 3 } )  X.  { 0 } ) ) ,  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  1
) ,  z >.Cgr <. ( ( k  e.  ( 1 ... ( N  -  1 ) )  |->  if ( k  =  1 ,  ( { <. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) ) ,  ( {
<. ( k  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) ) ) ) `  i
) ,  z >.
)  /\  -.  (
( { <. 1