Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

The abstract of the Mizar article:

Projective Spaces

by
Wojciech Leonczuk, and
Krzysztof Prazmowski

Received June 15, 1990

MML identifier: ANPROJ_2
[ Mizar article, MML identifier index ]


environ

 vocabulary RLVECT_1, ANPROJ_1, ARYTM_1, RELAT_1, FUNCT_2, FUNCT_1, FUNCSDOM,
      REALSET1, COLLSP, RELAT_2, INCSP_1, VECTSP_1, AFF_2, ANALOAF, ANPROJ_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, FUNCT_1, FUNCT_2, BINOP_1,
      DOMAIN_1, STRUCT_0, RLVECT_1, REAL_1, FRAENKEL, FUNCSDOM, COLLSP,
      ANPROJ_1;
 constructors DOMAIN_1, REAL_1, FUNCSDOM, ANPROJ_1, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, COLLSP, ANPROJ_1, STRUCT_0, RELSET_1, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve V for RealLinearSpace,
         o,p,q,r,s,u,v,w,y,y1,u1,v1,w1,u2,v2,w2 for Element of V,
         a,b,c,d,a1,b1,c1,d1,a2,b2,c2,d2,a3,b3,c3,d3 for Real,
         z for set;

theorem :: ANPROJ_2:1
 (for a,b,c st a*u + b*v + c*w = 0.V holds a = 0 & b = 0 & c = 0)
 implies u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect &
   not u,v,w are_LinDep & not are_Prop u,v;

theorem :: ANPROJ_2:2
 for u,v,u1,v1 holds
    ((for a,b,a1,b1 st a*u + b*v + a1*u1 + b1*v1 = 0.V holds
     a=0 & b=0 & a1=0 & b1=0) implies
 u is_Prop_Vect & v is_Prop_Vect & not are_Prop u,v & u1 is_Prop_Vect &
 v1 is_Prop_Vect & not are_Prop u1,v1 & not u,v,u1 are_LinDep &
                     not u1,v1,u are_LinDep);

theorem :: ANPROJ_2:3
(for w ex a,b,c st w = a*p + b*q + c*r) &
  (for a,b,c st a*p + b*q + c*r = 0.V holds a = 0 & b = 0 & c = 0) implies
(for u,u1 ex y st p,q,y are_LinDep & u,u1,y are_LinDep & y is_Prop_Vect);

theorem :: ANPROJ_2:4
 (for w ex a,b,c,d st w = a*p + b*q + c*r + d*s) &
 (for a,b,c,d st a*p + b*q + c*r + d*s = 0.V holds
  a = 0 & b = 0 & c = 0 & d = 0) implies
 (for u,v st u is_Prop_Vect & v is_Prop_Vect
    ex y,w st u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep &
     y is_Prop_Vect & w is_Prop_Vect);

theorem :: ANPROJ_2:5
  (for a,b,a1,b1 st a*u + b*v + a1*u1 + b1*v1 = 0.V holds
  a=0 & b=0 & a1=0 & b1=0) implies
      not ex y st y is_Prop_Vect & u,v,y are_LinDep & u1,v1,y are_LinDep;

::: > ANPROJ_3

::: < ANPROJ_4

definition let V,u,v,w;
 pred u,v,w are_Prop_Vect means
:: ANPROJ_2:def 1
  u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect;
end;

definition let V,u,v,w,u1,v1,w1;
 pred u,v,w,u1,v1,w1 lie_on_a_triangle means
:: ANPROJ_2:def 2
  u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep;
end;

definition let V,o,u,v,w,u2,v2,w2;
 pred o,u,v,w,u2,v2,w2 are_perspective means
:: ANPROJ_2:def 3
  o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep;
end;

theorem :: ANPROJ_2:6
 o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 &
 not are_Prop u,u2 & o,u,u2 are_Prop_Vect implies ((ex a1,b1 st b1*u2=o+a1*u
 & a1<>0 & b1<>0) & (ex a2,c2 st u2=c2*o+a2*u & c2<>0 & a2<>0));

theorem :: ANPROJ_2:7
 p,q,r are_LinDep & not are_Prop p,q & p,q,r are_Prop_Vect implies
      ex a,b st r = a*p + b*q;

theorem :: ANPROJ_2:8
o is_Prop_Vect & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect &
u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 are_perspective &
not are_Prop o,u2 & not are_Prop o,v2 & not are_Prop o,w2 &
not are_Prop u,u2 & not are_Prop v,v2 & not are_Prop w,w2 &
not o,u,v are_LinDep & not o,u,w are_LinDep & not o,v,w are_LinDep &
u,v,w,u1,v1,w1 lie_on_a_triangle & u2,v2,w2,u1,v1,w1 lie_on_a_triangle
              implies u1,v1,w1 are_LinDep;

::: > ANPROJ_4

::: < ANPROJ_6

definition let V,o,u,v,w,u2,v2,w2;
 pred o,u,v,w,u2,v2,w2 lie_on_an_angle means
:: ANPROJ_2:def 4
  not o,u,u2 are_LinDep & o,u,v are_LinDep & o,u,w are_LinDep &
   o,u2,v2 are_LinDep & o,u2,w2 are_LinDep;
end;

definition let V,o,u,v,w,u2,v2,w2;
 pred o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop means
:: ANPROJ_2:def 5
  not are_Prop o,v & not are_Prop o,w & not are_Prop o,v2 &
   not are_Prop o,w2 & not are_Prop u,v & not are_Prop u,w &
    not are_Prop u2,v2 & not are_Prop u2,w2 & not are_Prop v,w &
     not are_Prop v2,w2;
end;

theorem :: ANPROJ_2:9
o is_Prop_Vect & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect &
u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 lie_on_an_angle &
o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep &
u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep &
v,w2,u1 are_LinDep & w,v2,u1 are_LinDep implies u1,v1,w1 are_LinDep;

::: > ANPROJ_6

reserve A for non empty set;
reserve f,g,h,f1 for Element of Funcs(A,REAL);
reserve x1,x2,x3,x4 for Element of A;

theorem :: ANPROJ_2:10
 ex f,g,h st
      (for z st z in A holds
      (z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
      (for z st z in A holds
      (z=x2 implies g.z = 1) & (z<>x2 implies g.z = 0)) &
      (for z st z in A holds
      (z=x3 implies h.z = 1) & (z<>x3 implies h.z = 0));

theorem :: ANPROJ_2:11
 (x1 in A & x2 in A & x3 in A & x1<>x2 & x1<>x3 & x2<>x3) &
      (for z st z in A holds
      (z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
      (for z st z in A holds
      (z=x2 implies g.z = 1) & (z<>x2 implies g.z = 0)) &
      (for z st z in A holds
      (z=x3 implies h.z = 1) & (z<>x3 implies h.z = 0)) implies
 (for a,b,c st (RealFuncAdd(A)).((RealFuncAdd(A)).
   ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
   (RealFuncExtMult(A)).[c,h]) = RealFuncZero(A)
   holds a=0 & b=0 & c = 0);

theorem :: ANPROJ_2:12
   x1 in A & x2 in A & x3 in A & x1<>x2 & x1<>x3 & x2<>x3 implies
 (ex f,g,h st
   for a,b,c st (RealFuncAdd(A)).((RealFuncAdd(A)).
   ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
   (RealFuncExtMult(A)).[c,h]) = RealFuncZero(A)
   holds a=0 & b=0 & c = 0);

theorem :: ANPROJ_2:13
 A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3 &
     (for z st z in A holds
       (z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
     (for z st z in A holds
      (z=x2 implies g.z = 1) & (z<>x2 implies g.z = 0)) &
     (for z st z in A holds
      (z=x3 implies h.z = 1) & (z<>x3 implies h.z = 0))
     implies for h' being Element of Funcs(A,REAL) holds
     (ex a,b,c st h' = (RealFuncAdd(A)).((RealFuncAdd(A)).
   ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
   (RealFuncExtMult(A)).[c,h]));

theorem :: ANPROJ_2:14
   A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3 implies ex f,g,h st
   (for h' being Element of Funcs(A,REAL) holds
     (ex a,b,c st h' =
     (RealFuncAdd(A)).((RealFuncAdd(A)).
   ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
   (RealFuncExtMult(A)).[c,h])));

theorem :: ANPROJ_2:15
  (A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3) implies (ex f,g,h st
   (for a,b,c st (RealFuncAdd(A)).((RealFuncAdd(A)).
   ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
   (RealFuncExtMult(A)).[c,h]) = RealFuncZero(A)
   holds a=0 & b=0 & c = 0) &
   (for h' being Element of Funcs(A,REAL) holds
     (ex a,b,c st h' =
     (RealFuncAdd(A)).((RealFuncAdd(A)).
   ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
   (RealFuncExtMult(A)).[c,h]))));

 theorem :: ANPROJ_2:16
ex V being non trivial RealLinearSpace st
    (ex u,v,w being Element of V st
     (for a,b,c st a*u + b*v + c*w = 0.V holds a=0 & b=0 & c = 0) &
     (for y being Element of V ex a,b,c st y = a*u + b*v + c*w));

theorem :: ANPROJ_2:17
 ex f,g,h,f1 st
      (for z st z in A holds
      (z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
      (for z st z in A holds
      (z=x2 implies g.z = 1) & (z<>x2 implies g.z = 0)) &
      (for z st z in A holds
      (z=x3 implies h.z = 1) & (z<>x3 implies h.z = 0)) &
      (for z st z in A holds
      (z=x4 implies f1.z = 1) & (z<>x4 implies f1.z = 0));

theorem :: ANPROJ_2:18
 (x1 in A & x2 in A & x3 in A & x4 in A &
      x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4) &
      (for z st z in A holds
      (z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
      (for z st z in A holds
      (z=x2 implies g.z = 1) & (z<>x2 implies g.z = 0)) &
      (for z st z in A holds
      (z=x3 implies h.z = 1) & (z<>x3 implies h.z = 0)) &
      (for z st z in A holds
      (z=x4 implies f1.z = 1) & (z<>x4 implies f1.z = 0))
      implies (for a,b,c,d st
 (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)).
 ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
 (RealFuncExtMult(A)).[c,h]),(RealFuncExtMult(A)).[d,f1]) = RealFuncZero(A)
        holds a=0 & b=0 & c = 0 & d=0);

theorem :: ANPROJ_2:19
   x1 in A & x2 in A & x3 in A & x4 in A &
     x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4 implies
 (ex f,g,h,f1 st for a,b,c,d st
  (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)).
  ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
  (RealFuncExtMult(A)).[c,h]),(RealFuncExtMult(A)).[d,f1]) = RealFuncZero(A)
   holds a = 0 & b = 0 & c = 0 & d = 0);

theorem :: ANPROJ_2:20
A = {x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4 &
     (for z st z in A holds
      (z=x1 implies f.z = 1) & (z<>x1 implies f.z = 0)) &
     (for z st z in A holds
      (z=x2 implies g.z = 1) & (z<>x2 implies g.z = 0)) &
     (for z st z in A holds
      (z=x3 implies h.z = 1) & (z<>x3 implies h.z = 0)) &
     (for z st z in A holds
      (z=x4 implies f1.z = 1) & (z<>x4 implies f1.z = 0))
     implies for h' being Element of Funcs(A,REAL) holds
     ( ex a,b,c,d st h' = (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)).
  ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
  (RealFuncExtMult(A)).[c,h]),(RealFuncExtMult(A)).[d,f1]) );

theorem :: ANPROJ_2:21
   A = {x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4
  implies ex f,g,h,f1 st
   (for h' being Element of Funcs(A,REAL) holds
     (ex a,b,c,d st h' = (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)).
       ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
       (RealFuncExtMult(A)).[c,h]),(RealFuncExtMult(A)).[d,f1]) ));

theorem :: ANPROJ_2:22
  (A = {x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4)
  implies ( ex f,g,h,f1 st
   (for a,b,c,d st (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)).
 ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
 (RealFuncExtMult(A)).[c,h]),(RealFuncExtMult(A)).[d,f1]) = RealFuncZero(A)
   holds a = 0 & b = 0 & c = 0 & d = 0) &
   (for h' being Element of Funcs(A,REAL) holds
     (ex a,b,c,d st h' = (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)).
       ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]),
       (RealFuncExtMult(A)).[c,h]),(RealFuncExtMult(A)).[d,f1]) )));

 theorem :: ANPROJ_2:23
 ex V being non trivial RealLinearSpace st
    (ex u,v,w,u1 being Element of V
      st (for a,b,c,d st a*u + b*v + c*w + d*u1 = 0.V holds
                            a = 0 & b = 0 & c = 0 & d = 0) &
     (for y being Element of V ex a,b,c,d st y = a*u + b*v + c*w + d*u1));

definition let IT be RealLinearSpace;
 attr IT is up-3-dimensional means
:: ANPROJ_2:def 6
  ex u,v,w1 being Element of IT st
   for a,b,c st a*u + b*v + c*w1 = 0.IT holds a = 0 & b = 0 & c = 0;
end;

definition cluster up-3-dimensional RealLinearSpace;
end;

definition cluster up-3-dimensional -> non trivial RealLinearSpace;
end;

definition let CS be non empty CollStr;
 redefine attr CS is reflexive means
:: ANPROJ_2:def 7

 for p,q,r being Element of CS holds
   p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear;
 attr CS is transitive means
:: ANPROJ_2:def 8

 for p,q,r,r1,r2 being Element of CS
   st p<>q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear
   holds r,r1,r2 is_collinear;
end;

definition let IT be non empty CollStr;
 attr IT is Vebleian means
:: ANPROJ_2:def 9

 for p,p1,p2,r,r1 being Element of IT st
   p,p1,r is_collinear & p1,p2,r1 is_collinear
  ex r2 being Element of IT st
            p,p2,r2 is_collinear & r,r1,r2 is_collinear;
 attr IT is at_least_3rank means
:: ANPROJ_2:def 10

 for p,q being Element of IT ex r being
   Element of IT st p<>r & q<>r & p,q,r is_collinear;
end;

reserve V for non trivial RealLinearSpace;
reserve u,v,w,y,u1,v1,w1,u2,w2 for Element of V;
reserve p,p1,p2,p3,q,q1,q2,q3,r,r1,r2,r3 for
                    Element of ProjectiveSpace(V);

theorem :: ANPROJ_2:24
 p,q,r is_collinear iff ex u,v,w st
  p = Dir(u) & q = Dir(v) & r = Dir(w) & u is_Prop_Vect & v is_Prop_Vect &
  w is_Prop_Vect & u,v,w are_LinDep;

definition let V;
 cluster ProjectiveSpace V -> reflexive transitive;
end;

theorem :: ANPROJ_2:25
 p,q,r is_collinear implies p,r,q is_collinear & q,p,r is_collinear &
   r,q,p is_collinear & r,p,q is_collinear & q,r,p is_collinear;

definition let V;
 cluster ProjectiveSpace(V) -> Vebleian;
end;

definition let V be up-3-dimensional RealLinearSpace;
  cluster ProjectiveSpace(V) -> proper;
end;

theorem :: ANPROJ_2:26
(ex u,v st for a,b st a*u + b*v = 0.V holds a = 0 & b = 0 ) implies
    ProjectiveSpace(V) is at_least_3rank;

definition let V be up-3-dimensional RealLinearSpace;
 cluster ProjectiveSpace(V) -> at_least_3rank;
end;

definition
 cluster transitive reflexive proper Vebleian at_least_3rank
               (non empty CollStr);
end;

definition
 mode CollProjectiveSpace is
   reflexive transitive Vebleian at_least_3rank proper (non empty CollStr);
end;

definition let IT be CollProjectiveSpace;
 attr IT is Fanoian means
:: ANPROJ_2:def 11
 for p1,r2,q,r1,q1,p,r being Element of IT holds
 (p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear &
   r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear &
   p,q,r is_collinear implies
 (p1,r2,q1 is_collinear or p1,r2,r1 is_collinear or p1,r1,q1 is_collinear
     or r2,r1,q1 is_collinear));

 attr IT is Desarguesian means
:: ANPROJ_2:def 12
   for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Element of IT
  st o<>q1 & p1<>q1 & o<>q2 & p2<>q2 & o<>q3 & p3<>q3 &
   not o,p1,p2 is_collinear
 & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear
 & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear &
 p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear &
 o,p2,q2 is_collinear & o,p3,q3 is_collinear holds r1,r2,r3 is_collinear;

 attr IT is Pappian means
:: ANPROJ_2:def 13
    for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Element of IT
   st o<>p2 & o<>p3 & p2<>p3 & p1<>p2 & p1<>p3 & o<>q2 & o<>q3 &
     q2<>q3 & q1<>q2 & q1<>q3 &
  not o,p1,q1 is_collinear & o,p1,p2 is_collinear & o,p1,p3 is_collinear
 & o,q1,q2 is_collinear & o,q1,q3 is_collinear & p1,q2,r3 is_collinear &
 q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear &
 p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds r1,r2,r3 is_collinear;
end;

definition let IT be CollProjectiveSpace;
 attr IT is 2-dimensional means
:: ANPROJ_2:def 14

  for p,p1,q,q1 being Element of IT
  ex r being Element of IT st p,p1,r is_collinear &
  q,q1,r is_collinear;
 antonym IT is up-3-dimensional;
end;

definition let IT be CollProjectiveSpace;
 attr IT is at_most-3-dimensional means
:: ANPROJ_2:def 15
 for p,p1,q,q1,r2 being Element of IT
  ex r,r1 being Element of IT st p,q,r is_collinear &
         p1,q1,r1 is_collinear & r2,r,r1 is_collinear;
end;

canceled;

theorem :: ANPROJ_2:28
 p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear &
  r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear &
  p,q,r is_collinear implies
(p1,r2,q1 is_collinear or p1,r2,r1 is_collinear or p1,r1,q1 is_collinear
    or r2,r1,q1 is_collinear);

definition let V be up-3-dimensional RealLinearSpace;
 cluster ProjectiveSpace V -> Fanoian Desarguesian Pappian;
end;

theorem :: ANPROJ_2:29
(ex u,v,w st
     (for a,b,c st a*u + b*v + c*w = 0.V holds a=0 & b=0 & c = 0) &
     (for y ex a,b,c st y = a*u + b*v + c*w)) implies
    (ex x1,x2 being Element of ProjectiveSpace(V) st
     (x1<>x2 & for r1,r2 ex q st
         x1,x2,q is_collinear & r1,r2,q is_collinear));

theorem :: ANPROJ_2:30
(ex x1,x2 being Element of ProjectiveSpace(V) st
     (x1<>x2 & for r1,r2 ex q st
         x1,x2,q is_collinear & r1,r2,q is_collinear)) implies
  (for p,p1,q,q1 ex r st p,p1,r is_collinear & q,q1,r is_collinear);

theorem :: ANPROJ_2:31
(ex u,v,w st
     (for a,b,c st a*u + b*v + c*w = 0.V holds a=0 & b=0 & c = 0) &
     (for y ex a,b,c st y = a*u + b*v + c*w)) implies
      ex CS being CollProjectiveSpace
       st CS = ProjectiveSpace(V) & CS is 2-dimensional;

theorem :: ANPROJ_2:32
(ex y,u,v,w st
 (for w1 ex a,b,a1,b1 st w1 = a*y + b*u + a1*v + b1*w) &
 (for a,b,a1,b1 st a*y + b*u + a1*v + b1*w = 0.V holds
  a=0 & b=0 & a1=0 & b1=0)) implies (ex p,q1,q2 st not p,q1,q2 is_collinear &
  (for r1,r2 ex q3,r3
  st r1,r2,r3 is_collinear & q1,q2,q3 is_collinear & p,r3,q3 is_collinear));

reserve x,z,x1,y1,z1,x2,x3,y2,z2,p4,q4
                for Element of ProjectiveSpace(V);

theorem :: ANPROJ_2:33
 ProjectiveSpace(V) is proper at_least_3rank &
(ex p,q1,q2 st not p,q1,q2 is_collinear & (for r1,r2 ex q3,r3
  st r1,r2,r3 is_collinear & q1,q2,q3 is_collinear & p,r3,q3 is_collinear))
  implies ex CS being CollProjectiveSpace st
   CS = ProjectiveSpace(V) & CS is at_most-3-dimensional;

theorem :: ANPROJ_2:34
(ex y,u,v,w st
 (for w1 ex a,b,c,c1 st w1 = a*y + b*u + c*v + c1*w) &
 (for a,b,a1,b1 st a*y + b*u + a1*v + b1*w = 0.V holds
  a=0 & b=0 & a1=0 & b1=0)) implies
   ex CS being CollProjectiveSpace st
   CS = ProjectiveSpace(V) & CS is at_most-3-dimensional;

theorem :: ANPROJ_2:35
 (ex u,v,u1,v1 st
   (for a,b,a1,b1 st a*u + b*v + a1*u1 + b1*v1 = 0.V holds
          a=0 & b=0 & a1=0 & b1=0)) implies
   ex CS being CollProjectiveSpace st
    CS = ProjectiveSpace(V) & CS is non 2-dimensional;

theorem :: ANPROJ_2:36
 (ex u,v,u1,v1 st
 (for w ex a,b,a1,b1 st w = a*u + b*v + a1*u1 + b1*v1) &
   (for a,b,a1,b1 st a*u + b*v + a1*u1 + b1*v1 = 0.V holds
          a=0 & b=0 & a1=0 & b1=0)) implies
   ex CS being CollProjectiveSpace st CS = ProjectiveSpace(V) &
       CS is up-3-dimensional at_most-3-dimensional;

definition
 cluster strict Fanoian Desarguesian Pappian 2-dimensional CollProjectiveSpace;

 cluster strict Fanoian Desarguesian Pappian at_most-3-dimensional
         up-3-dimensional CollProjectiveSpace;
end;

definition
 mode CollProjectivePlane is 2-dimensional CollProjectiveSpace;
end;

theorem :: ANPROJ_2:37
  for CS being non empty CollStr holds
   CS is 2-dimensional CollProjectiveSpace iff
   (CS is at_least_3rank proper CollSp &
     for p,p1,q,q1 being Element of CS
     ex r being Element of CS st p,p1,r is_collinear &
      q,q1,r is_collinear);


Back to top