The abstract of the Mizar article:

A Construction of Analytical Projective Space

by

Wojciech Leonczuk, and

Krzysztof Prazmowski

Received June 15, 1990

MML identifier: ANPROJ_1

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, RELAT_1, ARYTM_1, EQREL_1, SETFAM_1, REALSET1, COLLSP,
      ANPROJ_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REAL_1, EQREL_1, SETFAM_1,
      STRUCT_0, REALSET1, COLLSP, RLVECT_1, MCART_1;
 constructors REAL_1, EQREL_1, REALSET1, COLLSP, MCART_1, MEMBERED, XBOOLE_0;
 clusters COLLSP, RLVECT_1, RELSET_1, STRUCT_0, MEMBERED, ZFMISC_1, XBOOLE_0,
      PARTFUN1;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve V for RealLinearSpace;
reserve p,q,r,u,v,w,y,u1,v1,w1 for Element of V;
reserve a,b,c,d,a1,b1,c1,a2,b2,c2,a3,b3,c3,e,f for Real;

definition let V be RealLinearSpace, p be Element of V;
 redefine attr p is non-zero;
 synonym p is_Prop_Vect;
end;

definition let V,p,q;
 canceled;

 pred are_Prop p,q means
:: ANPROJ_1:def 2
  ex a,b st a*p = b*q & a<>0 & b<>0;
  reflexivity;
  symmetry;
end;

canceled 4;

theorem :: ANPROJ_1:5
 are_Prop p,q iff ex a st a<>0 & p = a*q;

theorem :: ANPROJ_1:6
 are_Prop p,u & are_Prop u,q implies are_Prop p,q;

theorem :: ANPROJ_1:7
 are_Prop p,0.V iff p = 0.V;

definition let V,u,v,w;
 pred u,v,w are_LinDep means
:: ANPROJ_1:def 3
  ex a,b,c st a*u + b*v + c*w = 0.V & (a<>0 or b<>0 or c <>0);
end;

canceled;

theorem :: ANPROJ_1:9
 are_Prop u,u1 & are_Prop v,v1 & are_Prop w,w1 & u,v,w are_LinDep implies
     u1,v1,w1 are_LinDep;

theorem :: ANPROJ_1:10
 u,v,w are_LinDep implies (u,w,v are_LinDep & v,u,w are_LinDep &
                w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep);

theorem :: ANPROJ_1:11
 v is_Prop_Vect & w is_Prop_Vect & not are_Prop v,w implies
                      (v,w,u are_LinDep iff ex a,b st u = a*v + b*w);

theorem :: ANPROJ_1:12
   not are_Prop p,q & a1*p + b1*q = a2*p + b2*q &
    p is_Prop_Vect & q is_Prop_Vect implies a1 = a2 & b1 = b2;

theorem :: ANPROJ_1:13
   not u,v,w are_LinDep & a1*u + b1*v + c1*w = a2*u + b2*v + c2*w
        implies a1 = a2 & b1 = b2 & c1 = c2;

theorem :: ANPROJ_1:14
 not are_Prop p,q & u = a1*p + b1*q & v = a2*p + b2*q & a1*b2 - a2*b1=0 &
 p is_Prop_Vect & q is_Prop_Vect implies (are_Prop u,v or u = 0.V or v = 0.V);

theorem :: ANPROJ_1:15
 (u = 0.V or v = 0.V or w = 0.V) implies u,v,w are_LinDep;

theorem :: ANPROJ_1:16
 (are_Prop u,v or are_Prop w,u or are_Prop v,w) implies w,u,v are_LinDep;

theorem :: ANPROJ_1:17
 not u,v,w are_LinDep implies
    ( u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect) &
                   (not are_Prop u,v & not are_Prop v,w & not are_Prop w,u);

theorem :: ANPROJ_1:18
 p + q = 0.V implies are_Prop p,q;

theorem :: ANPROJ_1:19
 not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w are_LinDep
    & p is_Prop_Vect & q is_Prop_Vect implies u,v,w are_LinDep;

theorem :: ANPROJ_1:20
   not u,v,w are_LinDep & u,v,p are_LinDep & v,w,q are_LinDep implies
      ex y st (u,w,y are_LinDep & p,q,y are_LinDep & y is_Prop_Vect);

theorem :: ANPROJ_1:21
   not are_Prop p,q & p is_Prop_Vect & q is_Prop_Vect implies for u,v ex y
  st y is_Prop_Vect & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y;

theorem :: ANPROJ_1:22
   not p,q,r are_LinDep implies
     for u,v st u is_Prop_Vect & v is_Prop_Vect & not are_Prop u,v
     ex y st y is_Prop_Vect & not u,v,y are_LinDep;

theorem :: ANPROJ_1:23
   u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep &
  v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep &
  p is_Prop_Vect & q is_Prop_Vect & r is_Prop_Vect
  implies
(u,v,y are_LinDep or u,v,w are_LinDep or u,w,y are_LinDep or v,w,y are_LinDep);

reserve x,y,z for set;

definition let V;
  func Proper_Vectors_of V means
:: ANPROJ_1:def 4
     for u being set holds (u in it iff u<>0.V & u is Element of V);
end;

canceled 2;

theorem :: ANPROJ_1:26
 for u holds (u in Proper_Vectors_of V iff u is_Prop_Vect);

definition let V; func
 Proportionality_as_EqRel_of V -> Equivalence_Relation of Proper_Vectors_of V
 means
:: ANPROJ_1:def 5
  for x,y holds [x,y] in it iff
    (x in Proper_Vectors_of V & y in Proper_Vectors_of V
       & ex u,v being Element of V st x=u & y=v & are_Prop u,v );
end;

canceled;

theorem :: ANPROJ_1:28
   [x,y] in Proportionality_as_EqRel_of V implies
                          (x is Element of V & y is Element of V);

theorem :: ANPROJ_1:29
 [u,v] in Proportionality_as_EqRel_of V iff
                    ( u is_Prop_Vect & v is_Prop_Vect & are_Prop u,v );

definition let V; let v;
  func Dir(v) -> Subset of Proper_Vectors_of V equals
:: ANPROJ_1:def 6
    Class(Proportionality_as_EqRel_of V,v);
end;

definition let V;
 func ProjectivePoints(V) means
:: ANPROJ_1:def 7
   ex Y being Subset-Family of Proper_Vectors_of V st
         Y = Class Proportionality_as_EqRel_of V & it = Y;
end;

definition let V be non empty ZeroStr;
 redefine attr V is trivial means
:: ANPROJ_1:def 8
   for u being Element of V holds u = 0.V;
end;

definition
 cluster strict non trivial RealLinearSpace;
end;

canceled 3;

theorem :: ANPROJ_1:33
   for V being RealLinearSpace holds (V is non trivial RealLinearSpace iff
   ex u being Element of V st u in Proper_Vectors_of V);

reserve V for non trivial RealLinearSpace;
reserve p,q,r,u,v,w for Element of V;

definition let V;
 cluster Proper_Vectors_of V -> non empty;

 cluster ProjectivePoints V -> non empty;
end;

theorem :: ANPROJ_1:34
 p is_Prop_Vect implies Dir(p) is Element of ProjectivePoints(V);

theorem :: ANPROJ_1:35
 p is_Prop_Vect & q is_Prop_Vect implies (Dir(p) = Dir(q) iff are_Prop p,q);

definition let V;
 func ProjectiveCollinearity(V) -> Relation3 of ProjectivePoints(V) means
:: ANPROJ_1:def 9
  for x,y,z being set holds ([x,y,z] in it iff
   ex p,q,r st x = Dir(p) & y = Dir(q) & z = Dir(r) &
     p is_Prop_Vect & q is_Prop_Vect & r is_Prop_Vect & p,q,r are_LinDep);
end;

definition let V;
 func ProjectiveSpace(V) -> strict CollStr equals
:: ANPROJ_1:def 10
  CollStr (# ProjectivePoints(V),ProjectiveCollinearity(V) #);
end;

definition let V;
 cluster ProjectiveSpace V -> non empty;
end;

canceled 3;

theorem :: ANPROJ_1:39
for V holds
 ((the carrier of ProjectiveSpace(V)) = ProjectivePoints(V) &
 (the Collinearity of ProjectiveSpace(V)) = ProjectiveCollinearity(V));

theorem :: ANPROJ_1:40
   [x,y,z] in the Collinearity of ProjectiveSpace(V) implies (ex p,q,r st
  x = Dir(p) & y = Dir(q) & z = Dir(r) & p is_Prop_Vect & q is_Prop_Vect &
  r is_Prop_Vect & p,q,r are_LinDep)
;

theorem :: ANPROJ_1:41
u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect implies
 ([Dir(u),Dir(v),Dir(w)] in the Collinearity of ProjectiveSpace(V) iff
    u,v,w are_LinDep);

theorem :: ANPROJ_1:42
  x is Element of ProjectiveSpace(V) iff
 (ex u st u is_Prop_Vect & x = Dir(u));