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

A Construction of Analytical Projective Space

by
Wojciech Leonczuk, and
Krzysztof Prazmowski

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));