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

Theorem axlowdim 23158
Description: The general lower dimension 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, Alfred Tarski and Steven Givant, Bulletin of 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 10383 . . . . . . . 8  |-  2  e.  RR
2 3re 10387 . . . . . . . 8  |-  3  e.  RR
3 2lt3 10481 . . . . . . . 8  |-  2  <  3
41, 2, 3ltleii 9489 . . . . . . 7  |-  2  <_  3
5 2z 10670 . . . . . . . 8  |-  2  e.  ZZ
6 3z 10671 . . . . . . . 8  |-  3  e.  ZZ
7 eluz 10866 . . . . . . . 8  |-  ( ( 2  e.  ZZ  /\  3  e.  ZZ )  ->  ( 3  e.  (
ZZ>= `  2 )  <->  2  <_  3 ) )
85, 6, 7mp2an 672 . . . . . . 7  |-  ( 3  e.  ( ZZ>= `  2
)  <->  2  <_  3
)
94, 8mpbir 209 . . . . . 6  |-  3  e.  ( ZZ>= `  2 )
10 uzss 10873 . . . . . 6  |-  ( 3  e.  ( ZZ>= `  2
)  ->  ( ZZ>= ` 
3 )  C_  ( ZZ>=
`  2 ) )
119, 10ax-mp 5 . . . . 5  |-  ( ZZ>= ` 
3 )  C_  ( ZZ>=
`  2 )
1211sseli 3347 . . . 4  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( ZZ>= `  2 )
)
13 0re 9378 . . . . 5  |-  0  e.  RR
1413, 13axlowdimlem5 23143 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
1512, 14syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
16 1re 9377 . . . . 5  |-  1  e.  RR
1716, 13axlowdimlem5 23143 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
1812, 17syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
1913, 16axlowdimlem5 23143 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
2012, 19syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
21 eqid 2438 . . . 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 } ) ) ) )
2221axlowdimlem15 23153 . . 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
) )
23 eqid 2438 . . . . . 6  |-  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )  =  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )
24 eqid 2438 . . . . . 6  |-  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) )
25 eqid 2438 . . . . . 6  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
2623, 24, 25, 13, 13axlowdimlem17 23155 . . . . 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 } ) ) >.
)
27 eqid 2438 . . . . . 6  |-  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
2823, 24, 27, 16, 13axlowdimlem17 23155 . . . . 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 } ) ) >.
)
29 eqid 2438 . . . . . 6  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
3023, 24, 29, 13, 16axlowdimlem17 23155 . . . . 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 } ) ) >.
)
31 1z 10668 . . . . . . . . . . . . . . 15  |-  1  e.  ZZ
3231a1i 11 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  1  e.  ZZ )
33 peano2zm 10680 . . . . . . . . . . . . . . 15  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
34333ad2ant2 1010 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  ( N  -  1 )  e.  ZZ )
35 2m1e1 10428 . . . . . . . . . . . . . . 15  |-  ( 2  -  1 )  =  1
36 zre 10642 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ZZ  ->  N  e.  RR )
37 letr 9460 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR  /\  3  e.  RR  /\  N  e.  RR )  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
381, 2, 37mp3an12 1304 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  RR  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
3936, 38syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ZZ  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
404, 39mpani 676 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ZZ  ->  (
3  <_  N  ->  2  <_  N ) )
4140imp 429 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ZZ  /\  3  <_  N )  -> 
2  <_  N )
42413adant1 1006 . . . . . . . . . . . . . . . 16  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  2  <_  N )
43363ad2ant2 1010 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  N  e.  RR )
44 lesub1 9825 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  N  e.  RR  /\  1  e.  RR )  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
451, 16, 44mp3an13 1305 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  RR  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
4643, 45syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
4742, 46mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
2  -  1 )  <_  ( N  - 
1 ) )
4835, 47syl5eqbrr 4321 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  1  <_  ( N  -  1 ) )
4932, 34, 483jca 1168 . . . . . . . . . . . . 13  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
1  e.  ZZ  /\  ( N  -  1
)  e.  ZZ  /\  1  <_  ( N  - 
1 ) ) )
50 eluz2 10859 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  3
)  <->  ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N ) )
51 eluz2 10859 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  ( N  -  1 )  e.  ZZ  /\  1  <_ 
( N  -  1 ) ) )
5249, 50, 513imtr4i 266 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ( ZZ>= `  1 )
)
53 eluzfz1 11450 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
5452, 53syl 16 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
5554adantr 465 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
56 eqeq1 2444 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
k  =  1  <->  1  =  1 ) )
57 oveq1 6093 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
k  +  1 )  =  ( 1  +  1 ) )
5857opeq1d 4060 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  <. (
k  +  1 ) ,  1 >.  =  <. ( 1  +  1 ) ,  1 >. )
5958sneqd 3884 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  { <. ( k  +  1 ) ,  1 >. }  =  { <. ( 1  +  1 ) ,  1
>. } )
6057sneqd 3884 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  { ( k  +  1 ) }  =  { ( 1  +  1 ) } )
6160difeq2d 3469 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 1 ... N
)  \  { (
k  +  1 ) } )  =  ( ( 1 ... N
)  \  { (
1  +  1 ) } ) )
6261xpeq1d 4858 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( ( 1 ... N )  \  {
( k  +  1 ) } )  X. 
{ 0 } )  =  ( ( ( 1 ... N ) 
\  { ( 1  +  1 ) } )  X.  { 0 } ) )
6359, 62uneq12d 3506 . . . . . . . . . . . 12  |-  ( k  =  1  ->  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( 1  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( 1  +  1 ) } )  X.  { 0 } ) ) )
6456, 63ifbieq2d 3809 . . . . . . . . . . 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 } ) ) ) )
65 snex 4528 . . . . . . . . . . . . 13  |-  { <. 3 ,  -u 1 >. }  e.  _V
66 ovex 6111 . . . . . . . . . . . . . . 15  |-  ( 1 ... N )  e. 
_V
67 difexg 4435 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { 3 } )  e.  _V )
6866, 67ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { 3 } )  e.  _V
69 snex 4528 . . . . . . . . . . . . . 14  |-  { 0 }  e.  _V
7068, 69xpex 6503 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { 3 } )  X.  {
0 } )  e. 
_V
7165, 70unex 6373 . . . . . . . . . . . 12  |-  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )  e.  _V
72 snex 4528 . . . . . . . . . . . . 13  |-  { <. ( 1  +  1 ) ,  1 >. }  e.  _V
73 difexg 4435 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { (
1  +  1 ) } )  e.  _V )
7466, 73ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { ( 1  +  1 ) } )  e.  _V
7574, 69xpex 6503 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } )  e. 
_V
7672, 75unex 6373 . . . . . . . . . . . 12  |-  ( {
<. ( 1  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) )  e.  _V
7771, 76ifex 3853 . . . . . . . . . . 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
7864, 21, 77fvmpt 5769 . . . . . . . . . 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 } ) ) ) )
7955, 78syl 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 } ) ) ) )
80 eqid 2438 . . . . . . . . . 10  |-  1  =  1
8180iftruei 3793 . . . . . . . . 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 } ) )
8279, 81syl6eq 2486 . . . . . . . 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 } ) ) )
8382opeq1d 4060 . . . . . . 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 } ) ) >. )
84 2nn 10471 . . . . . . . . . . . . . 14  |-  2  e.  NN
85 nnuz 10888 . . . . . . . . . . . . . 14  |-  NN  =  ( ZZ>= `  1 )
8684, 85eleqtri 2510 . . . . . . . . . . . . 13  |-  2  e.  ( ZZ>= `  1 )
87 fzss1 11489 . . . . . . . . . . . . 13  |-  ( 2  e.  ( ZZ>= `  1
)  ->  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) ) )
8886, 87ax-mp 5 . . . . . . . . . . . 12  |-  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) )
8988sseli 3347 . . . . . . . . . . 11  |-  ( i  e.  ( 2 ... ( N  -  1 ) )  ->  i  e.  ( 1 ... ( N  -  1 ) ) )
9089adantl 466 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  i  e.  ( 1 ... ( N  -  1 ) ) )
91 eqeq1 2444 . . . . . . . . . . . 12  |-  ( k  =  i  ->  (
k  =  1  <->  i  =  1 ) )
92 oveq1 6093 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  (
k  +  1 )  =  ( i  +  1 ) )
9392opeq1d 4060 . . . . . . . . . . . . . 14  |-  ( k  =  i  ->  <. (
k  +  1 ) ,  1 >.  =  <. ( i  +  1 ) ,  1 >. )
9493sneqd 3884 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  { <. ( k  +  1 ) ,  1 >. }  =  { <. ( i  +  1 ) ,  1
>. } )
9592sneqd 3884 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  { ( k  +  1 ) }  =  { ( i  +  1 ) } )
9695difeq2d 3469 . . . . . . . . . . . . . 14  |-  ( k  =  i  ->  (
( 1 ... N
)  \  { (
k  +  1 ) } )  =  ( ( 1 ... N
)  \  { (
i  +  1 ) } ) )
9796xpeq1d 4858 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  (
( ( 1 ... N )  \  {
( k  +  1 ) } )  X. 
{ 0 } )  =  ( ( ( 1 ... N ) 
\  { ( i  +  1 ) } )  X.  { 0 } ) )
9894, 97uneq12d 3506 . . . . . . . . . . . 12  |-  ( k  =  i  ->  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) )
9991, 98ifbieq2d 3809 . . . . . . . . . . 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 } ) ) ) )
100 snex 4528 . . . . . . . . . . . . 13  |-  { <. ( i  +  1 ) ,  1 >. }  e.  _V
101 difexg 4435 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { (
i  +  1 ) } )  e.  _V )
10266, 101ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { ( i  +  1 ) } )  e.  _V
103102, 69xpex 6503 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } )  e. 
_V
104100, 103unex 6373 . . . . . . . . . . . 12  |-  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) )  e.  _V
10571, 104ifex 3853 . . . . . . . . . . 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
10699, 21, 105fvmpt 5769 . . . . . . . . . 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 } ) ) ) )
10790, 106syl 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 } ) ) ) )
108 1lt2 10480 . . . . . . . . . . . . . . . 16  |-  1  <  2
10916, 1ltnlei 9487 . . . . . . . . . . . . . . . 16  |-  ( 1  <  2  <->  -.  2  <_  1 )
110108, 109mpbi 208 . . . . . . . . . . . . . . 15  |-  -.  2  <_  1
111110intnanr 906 . . . . . . . . . . . . . 14  |-  -.  (
2  <_  1  /\  1  <_  ( N  - 
1 ) )
112 eluzelz 10862 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ZZ )
113112, 33syl 16 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ZZ )
114 elfz 11435 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  ZZ  /\  2  e.  ZZ  /\  ( N  -  1 )  e.  ZZ )  -> 
( 1  e.  ( 2 ... ( N  -  1 ) )  <-> 
( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
11531, 5, 114mp3an12 1304 . . . . . . . . . . . . . . 15  |-  ( ( N  -  1 )  e.  ZZ  ->  (
1  e.  ( 2 ... ( N  - 
1 ) )  <->  ( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
116113, 115syl 16 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1  e.  ( 2 ... ( N  -  1 ) )  <->  ( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
117111, 116mtbiri 303 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  3
)  ->  -.  1  e.  ( 2 ... ( N  -  1 ) ) )
118 eleq1 2498 . . . . . . . . . . . . . 14  |-  ( i  =  1  ->  (
i  e.  ( 2 ... ( N  - 
1 ) )  <->  1  e.  ( 2 ... ( N  -  1 ) ) ) )
119118notbid 294 . . . . . . . . . . . . 13  |-  ( i  =  1  ->  ( -.  i  e.  (
2 ... ( N  - 
1 ) )  <->  -.  1  e.  ( 2 ... ( N  -  1 ) ) ) )
120117, 119syl5ibrcom 222 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  =  1  ->  -.  i  e.  ( 2 ... ( N  - 
1 ) ) ) )
121120con2d 115 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 2 ... ( N  -  1 ) )  ->  -.  i  =  1 ) )
122121imp 429 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  -.  i  =  1 )
123 iffalse 3794 . . . . . . . . . 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 } ) ) )
124122, 123syl 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 } ) ) )
125107, 124eqtrd 2470 . . . . . . . 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 } ) ) )
126125opeq1d 4060 . . . . . . 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 } ) ) >.
)
12783, 126breq12d 4300 . . . . . 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 } ) ) >.
) )
12882opeq1d 4060 . . . . . . 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 } ) ) >. )
129125opeq1d 4060 . . . . . . 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 } ) ) >.
)
130128, 129breq12d 4300 . . . . . 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 } ) ) >.
) )
13154, 78syl 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 } ) ) ) )
132131, 81syl6eq 2486 . . . . . . . . 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 } ) ) )
133132opeq1d 4060 . . . . . . . 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 } ) ) >.
)
134133adantr 465 . . . . . . 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 } ) ) >. )
135125opeq1d 4060 . . . . . . 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 } ) ) >.
)
136134, 135breq12d 4300 . . . . . 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 } ) ) >.
) )
137127, 130, 1363anbi123d 1289 . . . . 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 } ) ) >.
) ) )
13826, 28, 30, 137mpbir3and 1171 . . . 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 } ) ) >.
) )
139138ralrimiva 2794 . . 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 } ) ) >.
) )
14025, 27, 29axlowdimlem6 23144 . . . 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 } ) ) >. ) )
14112, 140syl 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 } ) ) >. ) )
142 opeq2 4055 . . . . . . . 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 } ) ) >.
)
143 opeq2 4055 . . . . . . . 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 } ) ) >.
)
144142, 143breq12d 4300 . . . . . . 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 } ) ) >.
) )
1451443anbi1d 1293 . . . . . 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 >.
) ) )
146145ralbidv 2730 . . . . 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 >.
) ) )
147 breq1 4290 . . . . . . 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 >. )
)
148 opeq2 4055 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. z ,  x >.  =  <. z ,  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >. )
149148breq2d 4299 . . . . . . 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 } ) ) >. )
)
150 opeq1 4054 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. x ,  y >.  =  <. ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  y >. )
151150breq2d 4299 . . . . . . 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 >. ) )
152147, 149, 1513orbi123d 1288 . . . . . 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 >. ) ) )
153152notbid 294 . . . . 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 >. ) ) )
154146, 1533anbi23d 1292 . . . 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 ,  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 >. ) ) ) )
155 opeq2 4055 . . . . . . . 8  |-  ( y  =  ( { <. 1 ,  1 >. , 
<. 2 ,  0