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

Theorem axlowdim 24390
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 uzuzle23 11146 . . . 4  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( ZZ>= `  2 )
)
2 0re 9613 . . . . 5  |-  0  e.  RR
32, 2axlowdimlem5 24375 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
41, 3syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
5 1re 9612 . . . . 5  |-  1  e.  RR
65, 2axlowdimlem5 24375 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
71, 6syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
82, 5axlowdimlem5 24375 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
91, 8syl 16 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
10 eqid 2457 . . . 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 } ) ) ) )
1110axlowdimlem15 24385 . . 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
) )
12 eqid 2457 . . . . . 6  |-  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )  =  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )
13 eqid 2457 . . . . . 6  |-  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) )
14 eqid 2457 . . . . . 6  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
1512, 13, 14, 2, 2axlowdimlem17 24387 . . . . 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 } ) ) >.
)
16 eqid 2457 . . . . . 6  |-  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
1712, 13, 16, 5, 2axlowdimlem17 24387 . . . . 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 } ) ) >.
)
18 eqid 2457 . . . . . 6  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
1912, 13, 18, 2, 5axlowdimlem17 24387 . . . . 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 } ) ) >.
)
20 1zzd 10916 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  1  e.  ZZ )
21 peano2zm 10928 . . . . . . . . . . . . . . 15  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
22213ad2ant2 1018 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  ( N  -  1 )  e.  ZZ )
23 2m1e1 10671 . . . . . . . . . . . . . . 15  |-  ( 2  -  1 )  =  1
24 2re 10626 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
25 3re 10630 . . . . . . . . . . . . . . . . . . . 20  |-  3  e.  RR
26 2lt3 10724 . . . . . . . . . . . . . . . . . . . 20  |-  2  <  3
2724, 25, 26ltleii 9724 . . . . . . . . . . . . . . . . . . 19  |-  2  <_  3
28 zre 10889 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ZZ  ->  N  e.  RR )
29 letr 9695 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR  /\  3  e.  RR  /\  N  e.  RR )  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
3024, 25, 29mp3an12 1314 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  RR  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
3128, 30syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ZZ  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
3227, 31mpani 676 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ZZ  ->  (
3  <_  N  ->  2  <_  N ) )
3332imp 429 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ZZ  /\  3  <_  N )  -> 
2  <_  N )
34333adant1 1014 . . . . . . . . . . . . . . . 16  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  2  <_  N )
35283ad2ant2 1018 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  N  e.  RR )
36 lesub1 10067 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  N  e.  RR  /\  1  e.  RR )  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
3724, 5, 36mp3an13 1315 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  RR  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
3835, 37syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
3934, 38mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
2  -  1 )  <_  ( N  - 
1 ) )
4023, 39syl5eqbrr 4490 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  1  <_  ( N  -  1 ) )
4120, 22, 403jca 1176 . . . . . . . . . . . . 13  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
1  e.  ZZ  /\  ( N  -  1
)  e.  ZZ  /\  1  <_  ( N  - 
1 ) ) )
42 eluz2 11112 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  3
)  <->  ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N ) )
43 eluz2 11112 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  ( N  -  1 )  e.  ZZ  /\  1  <_ 
( N  -  1 ) ) )
4441, 42, 433imtr4i 266 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ( ZZ>= `  1 )
)
45 eluzfz1 11718 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
4644, 45syl 16 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
4746adantr 465 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
48 eqeq1 2461 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
k  =  1  <->  1  =  1 ) )
49 oveq1 6303 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
k  +  1 )  =  ( 1  +  1 ) )
5049opeq1d 4225 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  <. (
k  +  1 ) ,  1 >.  =  <. ( 1  +  1 ) ,  1 >. )
5150sneqd 4044 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  { <. ( k  +  1 ) ,  1 >. }  =  { <. ( 1  +  1 ) ,  1
>. } )
5249sneqd 4044 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  { ( k  +  1 ) }  =  { ( 1  +  1 ) } )
5352difeq2d 3618 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 1 ... N
)  \  { (
k  +  1 ) } )  =  ( ( 1 ... N
)  \  { (
1  +  1 ) } ) )
5453xpeq1d 5031 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( ( 1 ... N )  \  {
( k  +  1 ) } )  X. 
{ 0 } )  =  ( ( ( 1 ... N ) 
\  { ( 1  +  1 ) } )  X.  { 0 } ) )
5551, 54uneq12d 3655 . . . . . . . . . . . 12  |-  ( k  =  1  ->  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( 1  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( 1  +  1 ) } )  X.  { 0 } ) ) )
5648, 55ifbieq2d 3969 . . . . . . . . . . 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 } ) ) ) )
57 snex 4697 . . . . . . . . . . . . 13  |-  { <. 3 ,  -u 1 >. }  e.  _V
58 ovex 6324 . . . . . . . . . . . . . . 15  |-  ( 1 ... N )  e. 
_V
59 difexg 4604 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { 3 } )  e.  _V )
6058, 59ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { 3 } )  e.  _V
61 snex 4697 . . . . . . . . . . . . . 14  |-  { 0 }  e.  _V
6260, 61xpex 6603 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { 3 } )  X.  {
0 } )  e. 
_V
6357, 62unex 6597 . . . . . . . . . . . 12  |-  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )  e.  _V
64 snex 4697 . . . . . . . . . . . . 13  |-  { <. ( 1  +  1 ) ,  1 >. }  e.  _V
65 difexg 4604 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { (
1  +  1 ) } )  e.  _V )
6658, 65ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { ( 1  +  1 ) } )  e.  _V
6766, 61xpex 6603 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } )  e. 
_V
6864, 67unex 6597 . . . . . . . . . . . 12  |-  ( {
<. ( 1  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) )  e.  _V
6963, 68ifex 4013 . . . . . . . . . . 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
7056, 10, 69fvmpt 5956 . . . . . . . . . 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 } ) ) ) )
7147, 70syl 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 } ) ) ) )
72 eqid 2457 . . . . . . . . . 10  |-  1  =  1
7372iftruei 3951 . . . . . . . . 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 } ) )
7471, 73syl6eq 2514 . . . . . . . 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 } ) ) )
7574opeq1d 4225 . . . . . . 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 } ) ) >. )
76 2eluzge1 11152 . . . . . . . . . . . . 13  |-  2  e.  ( ZZ>= `  1 )
77 fzss1 11747 . . . . . . . . . . . . 13  |-  ( 2  e.  ( ZZ>= `  1
)  ->  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) ) )
7876, 77ax-mp 5 . . . . . . . . . . . 12  |-  ( 2 ... ( N  - 
1 ) )  C_  ( 1 ... ( N  -  1 ) )
7978sseli 3495 . . . . . . . . . . 11  |-  ( i  e.  ( 2 ... ( N  -  1 ) )  ->  i  e.  ( 1 ... ( N  -  1 ) ) )
8079adantl 466 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  i  e.  ( 1 ... ( N  -  1 ) ) )
81 eqeq1 2461 . . . . . . . . . . . 12  |-  ( k  =  i  ->  (
k  =  1  <->  i  =  1 ) )
82 oveq1 6303 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  (
k  +  1 )  =  ( i  +  1 ) )
8382opeq1d 4225 . . . . . . . . . . . . . 14  |-  ( k  =  i  ->  <. (
k  +  1 ) ,  1 >.  =  <. ( i  +  1 ) ,  1 >. )
8483sneqd 4044 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  { <. ( k  +  1 ) ,  1 >. }  =  { <. ( i  +  1 ) ,  1
>. } )
8582sneqd 4044 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  { ( k  +  1 ) }  =  { ( i  +  1 ) } )
8685difeq2d 3618 . . . . . . . . . . . . . 14  |-  ( k  =  i  ->  (
( 1 ... N
)  \  { (
k  +  1 ) } )  =  ( ( 1 ... N
)  \  { (
i  +  1 ) } ) )
8786xpeq1d 5031 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  (
( ( 1 ... N )  \  {
( k  +  1 ) } )  X. 
{ 0 } )  =  ( ( ( 1 ... N ) 
\  { ( i  +  1 ) } )  X.  { 0 } ) )
8884, 87uneq12d 3655 . . . . . . . . . . . 12  |-  ( k  =  i  ->  ( { <. ( k  +  1 ) ,  1
>. }  u.  ( ( ( 1 ... N
)  \  { (
k  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) ) )
8981, 88ifbieq2d 3969 . . . . . . . . . . 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 } ) ) ) )
90 snex 4697 . . . . . . . . . . . . 13  |-  { <. ( i  +  1 ) ,  1 >. }  e.  _V
91 difexg 4604 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { (
i  +  1 ) } )  e.  _V )
9258, 91ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { ( i  +  1 ) } )  e.  _V
9392, 61xpex 6603 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } )  e. 
_V
9490, 93unex 6597 . . . . . . . . . . . 12  |-  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) )  e.  _V
9563, 94ifex 4013 . . . . . . . . . . 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
9689, 10, 95fvmpt 5956 . . . . . . . . . 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 } ) ) ) )
9780, 96syl 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 } ) ) ) )
98 1lt2 10723 . . . . . . . . . . . . . . . 16  |-  1  <  2
995, 24ltnlei 9722 . . . . . . . . . . . . . . . 16  |-  ( 1  <  2  <->  -.  2  <_  1 )
10098, 99mpbi 208 . . . . . . . . . . . . . . 15  |-  -.  2  <_  1
101100intnanr 915 . . . . . . . . . . . . . 14  |-  -.  (
2  <_  1  /\  1  <_  ( N  - 
1 ) )
102 eluzelz 11115 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ZZ )
103102, 21syl 16 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ZZ )
104 1z 10915 . . . . . . . . . . . . . . . 16  |-  1  e.  ZZ
105 2z 10917 . . . . . . . . . . . . . . . 16  |-  2  e.  ZZ
106 elfz 11703 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  ZZ  /\  2  e.  ZZ  /\  ( N  -  1 )  e.  ZZ )  -> 
( 1  e.  ( 2 ... ( N  -  1 ) )  <-> 
( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
107104, 105, 106mp3an12 1314 . . . . . . . . . . . . . . 15  |-  ( ( N  -  1 )  e.  ZZ  ->  (
1  e.  ( 2 ... ( N  - 
1 ) )  <->  ( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
108103, 107syl 16 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1  e.  ( 2 ... ( N  -  1 ) )  <->  ( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
109101, 108mtbiri 303 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  3
)  ->  -.  1  e.  ( 2 ... ( N  -  1 ) ) )
110 eleq1 2529 . . . . . . . . . . . . . 14  |-  ( i  =  1  ->  (
i  e.  ( 2 ... ( N  - 
1 ) )  <->  1  e.  ( 2 ... ( N  -  1 ) ) ) )
111110notbid 294 . . . . . . . . . . . . 13  |-  ( i  =  1  ->  ( -.  i  e.  (
2 ... ( N  - 
1 ) )  <->  -.  1  e.  ( 2 ... ( N  -  1 ) ) ) )
112109, 111syl5ibrcom 222 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  =  1  ->  -.  i  e.  ( 2 ... ( N  - 
1 ) ) ) )
113112con2d 115 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 2 ... ( N  -  1 ) )  ->  -.  i  =  1 ) )
114113imp 429 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  -.  i  =  1 )
115114iffalsed 3955 . . . . . . . . 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 } ) ) )
11697, 115eqtrd 2498 . . . . . . . 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 } ) ) )
117116opeq1d 4225 . . . . . . 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 } ) ) >.
)
11875, 117breq12d 4469 . . . . . 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 } ) ) >.
) )
11974opeq1d 4225 . . . . . . 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 } ) ) >. )
120116opeq1d 4225 . . . . . . 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 } ) ) >.
)
121119, 120breq12d 4469 . . . . . 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 } ) ) >.
) )
12246, 70syl 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 } ) ) ) )
123122, 73syl6eq 2514 . . . . . . . . 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 } ) ) )
124123opeq1d 4225 . . . . . . . 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 } ) ) >.
)
125124adantr 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 } ) ) >. )
126116opeq1d 4225 . . . . . . 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 } ) ) >.
)
127125, 126breq12d 4469 . . . . . 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 } ) ) >.
) )
128118, 121, 1273anbi123d 1299 . . . . 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 } ) ) >.
) ) )
12915, 17, 19, 128mpbir3and 1179 . . . 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 } ) ) >.
) )
130129ralrimiva 2871 . . 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 } ) ) >.
) )
13114, 16, 18axlowdimlem6 24376 . . . 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 } ) ) >. ) )
1321, 131syl 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 } ) ) >. ) )
133 opeq2 4220 . . . . . . . 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 } ) ) >.
)
134 opeq2 4220 . . . . . . . 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 } ) ) >.
)
135133, 134breq12d 4469 . . . . . . 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 } ) ) >.
) )
1361353anbi1d 1303 . . . . . 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 >.
) ) )
137136ralbidv 2896 . . . . 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 >.
) ) )
138 breq1 4459 . . . . . . 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 >. )
)
139 opeq2 4220 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. z ,  x >.  =  <. z ,  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >. )
140139breq2d 4468 . . . . . . 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 } ) ) >. )
)
141 opeq1 4219 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. x ,  y >.  =  <. ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  y >. )
142141breq2d 4468 . . . . . . 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 >. ) )
143138, 140, 1423orbi123d 1298 . . . . . 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 >. ) ) )
144143notbid 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 >. ) ) )
145137, 1443anbi23d 1302 . . . 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 >. ) ) ) )
146 opeq2 4220 . . . . . . . 8  |-  ( y  =  ( { <. 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
) ,  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
) ,  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) >.
)
147 opeq2 4220 . . . . . . . 8  |-  ( y  =  ( { <. 1 ,  1 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.