:: A Construction of Analytical Projective Space
::  by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received June 15, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RLVECT_1, SUBSET_1, REAL_1, RELAT_1, CARD_1, SUPINF_2, ARYTM_3,
      ARYTM_1, XCMPLX_0, EQREL_1, STRUCT_0, SETFAM_1, ZFMISC_1, XBOOLE_0,
      COLLSP, TARSKI, ANPROJ_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, ORDINAL1, SUBSET_1, XCMPLX_0,
      XREAL_0, REAL_1, EQREL_1, SETFAM_1, NUMBERS, STRUCT_0, COLLSP, RLVECT_1,
      MCART_1;
 constructors REAL_1, EQREL_1, RLVECT_1, COLLSP, XTUPLE_0;
 registrations RELSET_1, STRUCT_0, RLVECT_1, COLLSP, XREAL_0, ORDINAL1;
 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,e,f for Real;

definition
  let V,p,q;

  pred are_Prop p,q means
:: ANPROJ_1:def 1

  ex a,b st a*p = b*q & a<>0 & b<>0;
  reflexivity;
  symmetry;
end;

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

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

theorem :: ANPROJ_1:3
  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 2

  ex a,b,c st a*u + b*v + c*w = 0.V & (a<>0 or b<>0 or c <>0);
end;

theorem :: ANPROJ_1:4
  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:5
  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:6
  v is not zero & w is not zero & not are_Prop v,w implies (v,w,u
  are_LinDep iff ex a,b st u = a*v + b*w);

theorem :: ANPROJ_1:7
  not are_Prop p,q & a1*p + b1*q = a2*p + b2*q & p is not zero & q is
  not zero implies a1 = a2 & b1 = b2;

theorem :: ANPROJ_1:8
  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:9
  not are_Prop p,q & u = a1*p + b1*q & v = a2*p + b2*q & a1*b2 -
a2*b1=0 & p is not zero & q is not zero implies (are_Prop u,v or u = 0.V or v =
  0.V);

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

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

theorem :: ANPROJ_1:12
  not u,v,w are_LinDep implies u is not zero & v is not zero & w
  is not zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u;

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

theorem :: ANPROJ_1:14
  not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w
  are_LinDep & p is not zero & q is not zero implies u,v,w are_LinDep;

theorem :: ANPROJ_1:15
  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 not zero;

theorem :: ANPROJ_1:16
  not are_Prop p,q & p is not zero & q is not zero implies for u,v ex y
  st y is not zero & u,v,y are_LinDep & not are_Prop u,y & not are_Prop v,y;

theorem :: ANPROJ_1:17
  not p,q,r are_LinDep implies for u,v st u is not zero & v is not zero
  & not are_Prop u,v ex y st y is not zero & not u,v,y are_LinDep;

theorem :: ANPROJ_1:18
  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 not
  zero & q is not zero & r is not zero 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 object;

definition

  let V;
  func Proportionality_as_EqRel_of V -> Equivalence_Relation of NonZero V
  means
:: ANPROJ_1:def 3

  for x,y holds [x,y] in it iff (x in NonZero V & y in NonZero V &
  ex u,v being Element of V st x=u & y=v & are_Prop u,v );
end;

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

theorem :: ANPROJ_1:20
  [u,v] in Proportionality_as_EqRel_of V iff u is not zero & v is
  not zero & are_Prop u,v;

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

definition
  let V;
  func ProjectivePoints(V) -> set means
:: ANPROJ_1:def 5

  ex Y being Subset-Family of NonZero V
  st Y = Class Proportionality_as_EqRel_of V & it = Y;
end;

registration
  cluster strict non trivial for RealLinearSpace;
end;

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

registration
  let V;
  cluster ProjectivePoints V -> non empty;
end;

theorem :: ANPROJ_1:21
  p is not zero implies Dir(p) is Element of ProjectivePoints(V);

theorem :: ANPROJ_1:22
  p is not zero & q is not zero implies (Dir(p) = Dir(q) iff are_Prop p,q);

definition

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

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

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

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

theorem :: ANPROJ_1:24
  [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 not zero & q is not zero & r is not
  zero & p,q,r are_LinDep;

theorem :: ANPROJ_1:25
  u is not zero & v is not zero & w is not zero implies ([Dir(u),Dir(v),
  Dir(w)] in the Collinearity of ProjectiveSpace(V) iff u,v,w are_LinDep);

theorem :: ANPROJ_1:26
  x is Element of ProjectiveSpace(V) iff ex u st u is not zero & x = Dir (u);