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

Theorem axlowdim 24589
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 9815 . . . . . . . 8  |-  2  e.  RR
2 3re 9817 . . . . . . . 8  |-  3  e.  RR
3 2lt3 9887 . . . . . . . 8  |-  2  <  3
41, 2, 3ltleii 8941 . . . . . . 7  |-  2  <_  3
5 2z 10054 . . . . . . . 8  |-  2  e.  ZZ
6 3nn 9878 . . . . . . . . 9  |-  3  e.  NN
76nnzi 10047 . . . . . . . 8  |-  3  e.  ZZ
8 eluz 10241 . . . . . . . 8  |-  ( ( 2  e.  ZZ  /\  3  e.  ZZ )  ->  ( 3  e.  (
ZZ>= `  2 )  <->  2  <_  3 ) )
95, 7, 8mp2an 653 . . . . . . 7  |-  ( 3  e.  ( ZZ>= `  2
)  <->  2  <_  3
)
104, 9mpbir 200 . . . . . 6  |-  3  e.  ( ZZ>= `  2 )
11 uzss 10248 . . . . . 6  |-  ( 3  e.  ( ZZ>= `  2
)  ->  ( ZZ>= ` 
3 )  C_  ( ZZ>=
`  2 ) )
1210, 11ax-mp 8 . . . . 5  |-  ( ZZ>= ` 
3 )  C_  ( ZZ>=
`  2 )
1312sseli 3176 . . . 4  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( ZZ>= `  2 )
)
14 0re 8838 . . . . 5  |-  0  e.  RR
1514, 14axlowdimlem5 24574 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
1613, 15syl 15 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
17 1re 8837 . . . . 5  |-  1  e.  RR
1817, 14axlowdimlem5 24574 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
1913, 18syl 15 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
2014, 17axlowdimlem5 24574 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
2113, 20syl 15 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
22 eqid 2283 . . . 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 24584 . . 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 2283 . . . . . 6  |-  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )  =  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )
25 eqid 2283 . . . . . 6  |-  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) )
26 eqid 2283 . . . . . 6  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
2724, 25, 26, 14, 14axlowdimlem17 24586 . . . . 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 2283 . . . . . 6  |-  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
2924, 25, 28, 17, 14axlowdimlem17 24586 . . . . 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 2283 . . . . . 6  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
3124, 25, 30, 14, 17axlowdimlem17 24586 . . . . 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 10053 . . . . . . . . . . . . . . 15  |-  1  e.  ZZ
3332a1i 10 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  1  e.  ZZ )
34 peano2zm 10062 . . . . . . . . . . . . . . 15  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
35343ad2ant2 977 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  ( N  -  1 )  e.  ZZ )
36 2cn 9816 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
37 ax-1cn 8795 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
38 1p1e2 9840 . . . . . . . . . . . . . . . 16  |-  ( 1  +  1 )  =  2
3936, 37, 37, 38subaddrii 9135 . . . . . . . . . . . . . . 15  |-  ( 2  -  1 )  =  1
40 zre 10028 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ZZ  ->  N  e.  RR )
41 letr 8914 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR  /\  3  e.  RR  /\  N  e.  RR )  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
421, 2, 41mp3an12 1267 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  RR  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
4340, 42syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ZZ  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
444, 43mpani 657 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ZZ  ->  (
3  <_  N  ->  2  <_  N ) )
4544imp 418 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ZZ  /\  3  <_  N )  -> 
2  <_  N )
46453adant1 973 . . . . . . . . . . . . . . . 16  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  2  <_  N )
47403ad2ant2 977 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  N  e.  RR )
48 lesub1 9268 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  N  e.  RR  /\  1  e.  RR )  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
491, 17, 48mp3an13 1268 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  RR  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
5047, 49syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
5146, 50mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
2  -  1 )  <_  ( N  - 
1 ) )
5239, 51syl5eqbrr 4057 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  1  <_  ( N  -  1 ) )
5333, 35, 523jca 1132 . . . . . . . . . . . . 13  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
1  e.  ZZ  /\  ( N  -  1
)  e.  ZZ  /\  1  <_  ( N  - 
1 ) ) )
54 eluz2 10236 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  3
)  <->  ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N ) )
55 eluz2 10236 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  ( N  -  1 )  e.  ZZ  /\  1  <_ 
( N  -  1 ) ) )
5653, 54, 553imtr4i 257 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ( ZZ>= `  1 )
)
57 eluzfz1 10803 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
5856, 57syl 15 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
5958adantr 451 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
60 eqeq1 2289 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
k  =  1  <->  1  =  1 ) )
61 oveq1 5865 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
k  +  1 )  =  ( 1  +  1 ) )
6261opeq1d 3802 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  <. (
k  +  1 ) ,  1 >.  =  <. ( 1  +  1 ) ,  1 >. )
6362sneqd 3653 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  { <. ( k  +  1 ) ,  1 >. }  =  { <. ( 1  +  1 ) ,  1
>. } )
6461sneqd 3653 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  { ( k  +  1 ) }  =  { ( 1  +  1 ) } )
6564difeq2d 3294 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 1 ... N
)  \  { (
k  +  1 ) } )  =  ( ( 1 ... N
)  \  { (
1  +  1 ) } ) )
6665xpeq1d 4712 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( ( 1 ... N )  \  {
( k  +  1 ) } )  X. 
{ 0 } )  =  ( ( ( 1 ... N ) 
\  { ( 1  +  1 ) } )  X.  { 0 } ) )
6763, 66uneq12d 3330 . . . . . . . . . . . 12  |-  ( k  =  1  ->  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( 1  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( 1  +  1 ) } )  X.  { 0 } ) ) )
6860, 67ifbieq2d 3585 . . . . . . . . . . 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 } ) ) ) )
69 snex 4216 . . . . . . . . . . . . 13  |-  { <. 3 ,  -u 1 >. }  e.  _V
70 ovex 5883 . . . . . . . . . . . . . . 15  |-  ( 1 ... N )  e. 
_V
71 difexg 4162 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { 3 } )  e.  _V )
7270, 71ax-mp 8 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { 3 } )  e.  _V
73 snex 4216 . . . . . . . . . . . . . 14  |-  { 0 }  e.  _V
7472, 73xpex 4801 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { 3 } )  X.  {
0 } )  e. 
_V
7569, 74unex 4518 . . . . . . . . . . . 12  |-  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )  e.  _V
76 snex 4216 . . . . . . . . . . . . 13  |-  { <. ( 1  +  1 ) ,  1 >. }  e.  _V
77 difexg 4162 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { (
1  +  1 ) } )  e.  _V )
7870, 77ax-mp 8 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { ( 1  +  1 ) } )  e.  _V
7978, 73xpex 4801 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } )  e. 
_V
8076, 79unex 4518 . . . . . . . . . . . 12  |-  ( {
<. ( 1  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) )  e.  _V
8175, 80ifex 3623 . . . . . . . . . . 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
8268, 22, 81fvmpt 5602 . . . . . . . . . 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 } ) ) ) )
8359, 82syl 15 . . . . . . . . 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 } ) ) ) )
84 eqid 2283 . . . . . . . . . 10  |-  1  =  1
85 iftrue 3571 . . . . . . . . . 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 } ) ) )
8684, 85ax-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 } ) )
8783, 86syl6eq 2331 . . . . . . . 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 } ) ) )
8887opeq1d 3802 . . . . . . 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 } ) ) >. )
89 2nn 9877 . . . . . . . . . . . . . 14  |-  2  e.  NN
90 nnuz 10263 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  1 )
9189, 90eleqtri 2355 . . . . . . . . . . . . 13  |-  2  e.  ( ZZ>= `  1 )
92 fzss1 10830 . . . . . . . . . . . . 13  |-  ( 2  e.  ( ZZ>= `  1
)  ->  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) ) )
9391, 92ax-mp 8 . . . . . . . . . . . 12  |-  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) )
9493sseli 3176 . . . . . . . . . . 11  |-  ( i  e.  ( 2 ... ( N  -  1 ) )  ->  i  e.  ( 1 ... ( N  -  1 ) ) )
9594adantl 452 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  i  e.  ( 1 ... ( N  -  1 ) ) )
96 eqeq1 2289 . . . . . . . . . . . 12  |-  ( k  =  i  ->  (
k  =  1  <->  i  =  1 ) )
97 oveq1 5865 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  (
k  +  1 )  =  ( i  +  1 ) )
9897opeq1d 3802 . . . . . . . . . . . . . 14  |-  ( k  =  i  ->  <. (
k  +  1 ) ,  1 >.  =  <. ( i  +  1 ) ,  1 >. )
9998sneqd 3653 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  { <. ( k  +  1 ) ,  1 >. }  =  { <. ( i  +  1 ) ,  1
>. } )
10097sneqd 3653 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  { ( k  +  1 ) }  =  { ( i  +  1 ) } )
101100difeq2d 3294 . . . . . . . . . . . . . 14  |-  ( k  =  i  ->  (
( 1 ... N
)  \  { (
k  +  1 ) } )  =  ( ( 1 ... N
)  \  { (
i  +  1 ) } ) )
102101xpeq1d 4712 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  (
( ( 1 ... N )  \  {
( k  +  1 ) } )  X. 
{ 0 } )  =  ( ( ( 1 ... N ) 
\  { ( i  +  1 ) } )  X.  { 0 } ) )
10399, 102uneq12d 3330 . . . . . . . . . . . 12  |-  ( k  =  i  ->  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) )
10496, 103ifbieq2d 3585 . . . . . . . . . . 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 } ) ) ) )
105 snex 4216 . . . . . . . . . . . . 13  |-  { <. ( i  +  1 ) ,  1 >. }  e.  _V
106 difexg 4162 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { (
i  +  1 ) } )  e.  _V )
10770, 106ax-mp 8 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { ( i  +  1 ) } )  e.  _V
108107, 73xpex 4801 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } )  e. 
_V
109105, 108unex 4518 . . . . . . . . . . . 12  |-  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) )  e.  _V
11075, 109ifex 3623 . . . . . . . . . . 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
111104, 22, 110fvmpt 5602 . . . . . . . . . 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 } ) ) ) )
11295, 111syl 15 . . . . . . . . 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 } ) ) ) )
113 1lt2 9886 . . . . . . . . . . . . . . . 16  |-  1  <  2
11417, 1ltnlei 8939 . . . . . . . . . . . . . . . 16  |-  ( 1  <  2  <->  -.  2  <_  1 )
115113, 114mpbi 199 . . . . . . . . . . . . . . 15  |-  -.  2  <_  1
116115intnanr 881 . . . . . . . . . . . . . 14  |-  -.  (
2  <_  1  /\  1  <_  ( N  - 
1 ) )
117 eluzelz 10238 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ZZ )
118117, 34syl 15 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ZZ )
119 elfz 10788 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  ZZ  /\  2  e.  ZZ  /\  ( N  -  1 )  e.  ZZ )  -> 
( 1  e.  ( 2 ... ( N  -  1 ) )  <-> 
( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
12032, 5, 119mp3an12 1267 . . . . . . . . . . . . . . 15  |-  ( ( N  -  1 )  e.  ZZ  ->  (
1  e.  ( 2 ... ( N  - 
1 ) )  <->  ( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
121118, 120syl 15 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1  e.  ( 2 ... ( N  -  1 ) )  <->  ( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
122116, 121mtbiri 294 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  3
)  ->  -.  1  e.  ( 2 ... ( N  -  1 ) ) )
123 eleq1 2343 . . . . . . . . . . . . . 14  |-  ( i  =  1  ->  (
i  e.  ( 2 ... ( N  - 
1 ) )  <->  1  e.  ( 2 ... ( N  -  1 ) ) ) )
124123notbid 285 . . . . . . . . . . . . 13  |-  ( i  =  1  ->  ( -.  i  e.  (
2 ... ( N  - 
1 ) )  <->  -.  1  e.  ( 2 ... ( N  -  1 ) ) ) )
125122, 124syl5ibrcom 213 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  =  1  ->  -.  i  e.  ( 2 ... ( N  - 
1 ) ) ) )
126125con2d 107 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 2 ... ( N  -  1 ) )  ->  -.  i  =  1 ) )
127126imp 418 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  -.  i  =  1 )
128 iffalse 3572 . . . . . . . . . 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 } ) ) )
129127, 128syl 15 . . . . . . . . 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 } ) ) )
130112, 129eqtrd 2315 . . . . . . . 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 } ) ) )
131130opeq1d 3802 . . . . . . 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 } ) ) >.
)
13288, 131breq12d 4036 . . . . . 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 } ) ) >.
) )
13387opeq1d 3802 . . . . . . 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 } ) ) >. )
134130opeq1d 3802 . . . . . . 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 } ) ) >.
)
135133, 134breq12d 4036 . . . . . 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 } ) ) >.
) )
13658, 82syl 15 . . . . . . . . . 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 } ) ) ) )
137136, 86syl6eq 2331 . . . . . . . . 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 } ) ) )
138137opeq1d 3802 . . . . . . . 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 } ) ) >.
)
139138adantr 451 . . . . . . 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 } ) ) >. )
140130opeq1d 3802 . . . . . . 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 } ) ) >.
)
141139, 140breq12d 4036 . . . . . 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 } ) ) >.
) )
142132, 135, 1413anbi123d 1252 . . . . 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 } ) ) >.
) ) )
14327, 29, 31, 142mpbir3and 1135 . . . 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 } ) ) >.
) )
144143ralrimiva 2626 . . 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 } ) ) >.
) )
14526, 28, 30axlowdimlem6 24575 . . . 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 } ) ) >. ) )
14613, 145syl 15 . . 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 } ) ) >. ) )
147 opeq2 3797 . . . . . . . 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 } ) ) >.
)
148 opeq2 3797 . . . . . . . 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 } ) ) >.
)
149147, 148breq12d 4036 . . . . . . 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 } ) ) >.
) )
1501493anbi1d 1256 . . . . . 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 >.
) ) )
151150ralbidv 2563 . . . . 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 >.
) ) )
152 breq1 4026 . . . . . . 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 >. )
)
153 opeq2 3797 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. z ,  x >.  =  <. z ,  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >. )
154153breq2d 4035 . . . . . . 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 } ) ) >. )
)
155 opeq1 3796 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. x ,  y >.  =  <. ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  y >. )
156155breq2d 4035 . . . . . . 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 >. ) )
157152, 154, 1563orbi123d 1251 . . . . . 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 >. ) ) )
158157notbid 285 . . . . 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 >. ) ) )
159151, 1583anbi23d 1255 . . . 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.