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

Theorem axlowdim 24990
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 11207 . . . 4  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( ZZ>= `  2 )
)
2 0re 9651 . . . . 5  |-  0  e.  RR
32, 2axlowdimlem5 24975 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
41, 3syl 17 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
5 1re 9650 . . . . 5  |-  1  e.  RR
65, 2axlowdimlem5 24975 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
71, 6syl 17 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  1 >. ,  <. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
82, 5axlowdimlem5 24975 . . . 4  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
91, 8syl 17 . . 3  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( { <. 1 ,  0 >. ,  <. 2 ,  1
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  e.  ( EE `  N ) )
10 eqid 2422 . . . 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 24985 . . 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 2422 . . . . . 6  |-  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )  =  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )
13 eqid 2422 . . . . . 6  |-  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) )  =  ( { <. ( i  +  1 ) ,  1 >. }  u.  ( ( ( 1 ... N )  \  { ( i  +  1 ) } )  X.  { 0 } ) )
14 eqid 2422 . . . . . 6  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  0 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
1512, 13, 14, 2, 2axlowdimlem17 24987 . . . . 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 2422 . . . . . 6  |-  ( {
<. 1 ,  1
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  1 >. ,  <. 2 ,  0 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
1712, 13, 16, 5, 2axlowdimlem17 24987 . . . . 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 2422 . . . . . 6  |-  ( {
<. 1 ,  0
>. ,  <. 2 ,  1 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) )  =  ( { <. 1 ,  0 >. ,  <. 2 ,  1 >. }  u.  ( ( 3 ... N )  X. 
{ 0 } ) )
1912, 13, 18, 2, 5axlowdimlem17 24987 . . . . 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 10976 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  1  e.  ZZ )
21 peano2zm 10988 . . . . . . . . . . . . . . 15  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
22213ad2ant2 1027 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  ( N  -  1 )  e.  ZZ )
23 2m1e1 10732 . . . . . . . . . . . . . . 15  |-  ( 2  -  1 )  =  1
24 2re 10687 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
25 3re 10691 . . . . . . . . . . . . . . . . . . . 20  |-  3  e.  RR
26 2lt3 10785 . . . . . . . . . . . . . . . . . . . 20  |-  2  <  3
2724, 25, 26ltleii 9765 . . . . . . . . . . . . . . . . . . 19  |-  2  <_  3
28 zre 10949 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ZZ  ->  N  e.  RR )
29 letr 9735 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR  /\  3  e.  RR  /\  N  e.  RR )  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
3024, 25, 29mp3an12 1350 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  RR  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
3128, 30syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ZZ  ->  (
( 2  <_  3  /\  3  <_  N )  ->  2  <_  N
) )
3227, 31mpani 680 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ZZ  ->  (
3  <_  N  ->  2  <_  N ) )
3332imp 430 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ZZ  /\  3  <_  N )  -> 
2  <_  N )
34333adant1 1023 . . . . . . . . . . . . . . . 16  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  2  <_  N )
35283ad2ant2 1027 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  N  e.  RR )
36 lesub1 10116 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  N  e.  RR  /\  1  e.  RR )  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
3724, 5, 36mp3an13 1351 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  RR  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
3835, 37syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
2  <_  N  <->  ( 2  -  1 )  <_ 
( N  -  1 ) ) )
3934, 38mpbid 213 . . . . . . . . . . . . . . 15  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
2  -  1 )  <_  ( N  - 
1 ) )
4023, 39syl5eqbrr 4458 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  1  <_  ( N  -  1 ) )
4120, 22, 403jca 1185 . . . . . . . . . . . . 13  |-  ( ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N )  ->  (
1  e.  ZZ  /\  ( N  -  1
)  e.  ZZ  /\  1  <_  ( N  - 
1 ) ) )
42 eluz2 11173 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  3
)  <->  ( 3  e.  ZZ  /\  N  e.  ZZ  /\  3  <_  N ) )
43 eluz2 11173 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  ( N  -  1 )  e.  ZZ  /\  1  <_ 
( N  -  1 ) ) )
4441, 42, 433imtr4i 269 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ( ZZ>= `  1 )
)
45 eluzfz1 11814 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
4644, 45syl 17 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
4746adantr 466 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  1  e.  ( 1 ... ( N  -  1 ) ) )
48 eqeq1 2426 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
k  =  1  <->  1  =  1 ) )
49 oveq1 6313 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
k  +  1 )  =  ( 1  +  1 ) )
5049opeq1d 4193 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  <. (
k  +  1 ) ,  1 >.  =  <. ( 1  +  1 ) ,  1 >. )
5150sneqd 4010 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  { <. ( k  +  1 ) ,  1 >. }  =  { <. ( 1  +  1 ) ,  1
>. } )
5249sneqd 4010 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  { ( k  +  1 ) }  =  { ( 1  +  1 ) } )
5352difeq2d 3583 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( 1 ... N
)  \  { (
k  +  1 ) } )  =  ( ( 1 ... N
)  \  { (
1  +  1 ) } ) )
5453xpeq1d 4876 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( ( 1 ... N )  \  {
( k  +  1 ) } )  X. 
{ 0 } )  =  ( ( ( 1 ... N ) 
\  { ( 1  +  1 ) } )  X.  { 0 } ) )
5551, 54uneq12d 3621 . . . . . . . . . . . 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 3936 . . . . . . . . . . 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 4662 . . . . . . . . . . . . 13  |-  { <. 3 ,  -u 1 >. }  e.  _V
58 ovex 6334 . . . . . . . . . . . . . . 15  |-  ( 1 ... N )  e. 
_V
59 difexg 4572 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { 3 } )  e.  _V )
6058, 59ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { 3 } )  e.  _V
61 snex 4662 . . . . . . . . . . . . . 14  |-  { 0 }  e.  _V
6260, 61xpex 6610 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { 3 } )  X.  {
0 } )  e. 
_V
6357, 62unex 6604 . . . . . . . . . . . 12  |-  ( {
<. 3 ,  -u
1 >. }  u.  (
( ( 1 ... N )  \  {
3 } )  X. 
{ 0 } ) )  e.  _V
64 snex 4662 . . . . . . . . . . . . 13  |-  { <. ( 1  +  1 ) ,  1 >. }  e.  _V
65 difexg 4572 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { (
1  +  1 ) } )  e.  _V )
6658, 65ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { ( 1  +  1 ) } )  e.  _V
6766, 61xpex 6610 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } )  e. 
_V
6864, 67unex 6604 . . . . . . . . . . . 12  |-  ( {
<. ( 1  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
1  +  1 ) } )  X.  {
0 } ) )  e.  _V
6963, 68ifex 3979 . . . . . . . . . . 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 5965 . . . . . . . . . 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 17 . . . . . . . . 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 2422 . . . . . . . . . 10  |-  1  =  1
7372iftruei 3918 . . . . . . . . 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 2479 . . . . . . . 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 4193 . . . . . . 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 11213 . . . . . . . . . . . . 13  |-  2  e.  ( ZZ>= `  1 )
77 fzss1 11845 . . . . . . . . . . . . 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 3460 . . . . . . . . . . 11  |-  ( i  e.  ( 2 ... ( N  -  1 ) )  ->  i  e.  ( 1 ... ( N  -  1 ) ) )
8079adantl 467 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  i  e.  ( 1 ... ( N  -  1 ) ) )
81 eqeq1 2426 . . . . . . . . . . . 12  |-  ( k  =  i  ->  (
k  =  1  <->  i  =  1 ) )
82 oveq1 6313 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  (
k  +  1 )  =  ( i  +  1 ) )
8382opeq1d 4193 . . . . . . . . . . . . . 14  |-  ( k  =  i  ->  <. (
k  +  1 ) ,  1 >.  =  <. ( i  +  1 ) ,  1 >. )
8483sneqd 4010 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  { <. ( k  +  1 ) ,  1 >. }  =  { <. ( i  +  1 ) ,  1
>. } )
8582sneqd 4010 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  { ( k  +  1 ) }  =  { ( i  +  1 ) } )
8685difeq2d 3583 . . . . . . . . . . . . . 14  |-  ( k  =  i  ->  (
( 1 ... N
)  \  { (
k  +  1 ) } )  =  ( ( 1 ... N
)  \  { (
i  +  1 ) } ) )
8786xpeq1d 4876 . . . . . . . . . . . . 13  |-  ( k  =  i  ->  (
( ( 1 ... N )  \  {
( k  +  1 ) } )  X. 
{ 0 } )  =  ( ( ( 1 ... N ) 
\  { ( i  +  1 ) } )  X.  { 0 } ) )
8884, 87uneq12d 3621 . . . . . . . . . . . 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 3936 . . . . . . . . . . 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 4662 . . . . . . . . . . . . 13  |-  { <. ( i  +  1 ) ,  1 >. }  e.  _V
91 difexg 4572 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { (
i  +  1 ) } )  e.  _V )
9258, 91ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( 1 ... N ) 
\  { ( i  +  1 ) } )  e.  _V
9392, 61xpex 6610 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } )  e. 
_V
9490, 93unex 6604 . . . . . . . . . . . 12  |-  ( {
<. ( i  +  1 ) ,  1 >. }  u.  ( (
( 1 ... N
)  \  { (
i  +  1 ) } )  X.  {
0 } ) )  e.  _V
9563, 94ifex 3979 . . . . . . . . . . 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 5965 . . . . . . . . . 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 17 . . . . . . . . 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 10784 . . . . . . . . . . . . . . . 16  |-  1  <  2
995, 24ltnlei 9763 . . . . . . . . . . . . . . . 16  |-  ( 1  <  2  <->  -.  2  <_  1 )
10098, 99mpbi 211 . . . . . . . . . . . . . . 15  |-  -.  2  <_  1
101100intnanr 923 . . . . . . . . . . . . . 14  |-  -.  (
2  <_  1  /\  1  <_  ( N  - 
1 ) )
102 eluzelz 11176 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ZZ )
103102, 21syl 17 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ZZ )
104 1z 10975 . . . . . . . . . . . . . . . 16  |-  1  e.  ZZ
105 2z 10977 . . . . . . . . . . . . . . . 16  |-  2  e.  ZZ
106 elfz 11798 . . . . . . . . . . . . . . . 16  |-  ( ( 1  e.  ZZ  /\  2  e.  ZZ  /\  ( N  -  1 )  e.  ZZ )  -> 
( 1  e.  ( 2 ... ( N  -  1 ) )  <-> 
( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
107104, 105, 106mp3an12 1350 . . . . . . . . . . . . . . 15  |-  ( ( N  -  1 )  e.  ZZ  ->  (
1  e.  ( 2 ... ( N  - 
1 ) )  <->  ( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
108103, 107syl 17 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1  e.  ( 2 ... ( N  -  1 ) )  <->  ( 2  <_  1  /\  1  <_  ( N  -  1 ) ) ) )
109101, 108mtbiri 304 . . . . . . . . . . . . 13  |-  ( N  e.  ( ZZ>= `  3
)  ->  -.  1  e.  ( 2 ... ( N  -  1 ) ) )
110 eleq1 2495 . . . . . . . . . . . . . 14  |-  ( i  =  1  ->  (
i  e.  ( 2 ... ( N  - 
1 ) )  <->  1  e.  ( 2 ... ( N  -  1 ) ) ) )
111110notbid 295 . . . . . . . . . . . . 13  |-  ( i  =  1  ->  ( -.  i  e.  (
2 ... ( N  - 
1 ) )  <->  -.  1  e.  ( 2 ... ( N  -  1 ) ) ) )
112109, 111syl5ibrcom 225 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  =  1  ->  -.  i  e.  ( 2 ... ( N  - 
1 ) ) ) )
113112con2d 118 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 2 ... ( N  -  1 ) )  ->  -.  i  =  1 ) )
114113imp 430 . . . . . . . . . 10  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 2 ... ( N  -  1 ) ) )  ->  -.  i  =  1 )
115114iffalsed 3922 . . . . . . . . 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 2463 . . . . . . . 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 4193 . . . . . . 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 4436 . . . . . 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 4193 . . . . . . 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 4193 . . . . . . 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 4436 . . . . . 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 17 . . . . . . . . . 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 2479 . . . . . . . . 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 4193 . . . . . . . 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 466 . . . . . . 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 4193 . . . . . . 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 4436 . . . . . 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 1335 . . . . 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 1188 . . . 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 2836 . . 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 24976 . . . 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 17 . . 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 4188 . . . . . . . 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 4188 . . . . . . . 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 4436 . . . . . . 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 1339 . . . . . 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 2861 . . . . 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 4426 . . . . . . 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 4188 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. z ,  x >.  =  <. z ,  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) ) >. )
140139breq2d 4435 . . . . . . 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 4187 . . . . . . . 8  |-  ( x  =  ( { <. 1 ,  0 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.  { 0 } ) )  ->  <. x ,  y >.  =  <. ( { <. 1 ,  0
>. ,  <. 2 ,  0 >. }  u.  (
( 3 ... N
)  X.  { 0 } ) ) ,  y >. )
142141breq2d 4435 . . . . . . 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 1334 . . . . . 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 295 . . . . 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 1338 . . . 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 4188 . . . . . . . 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 4188 . . . . . . . 8  |-  ( y  =  ( { <. 1 ,  1 >. , 
<. 2 ,  0
>. }  u.  ( ( 3 ... N )  X.