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