Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
The abstract of the Mizar article:
-
- 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