:: Projective Spaces
:: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received June 15, 1990
:: Copyright (c) 1990-2026 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, ARYTM_3, SUPINF_2, CARD_1,
XCMPLX_0, ANPROJ_1, ARYTM_1, XBOOLE_0, FUNCT_2, NUMBERS, FUNCT_1,
FUNCSDOM, ZFMISC_1, INCSP_1, COLLSP, RELAT_2, VECTSP_1, AFF_2, ANALOAF,
ANPROJ_2, FUNCT_7, PENCIL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, FUNCT_2,
BINOP_1, DOMAIN_1, XCMPLX_0, XREAL_0, STRUCT_0, RLVECT_1, REAL_1,
FUNCSDOM, COLLSP, ANPROJ_1;
constructors DOMAIN_1, REAL_1, FUNCSDOM, BINOP_2, ANPROJ_1, RELSET_1,
VALUED_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, STRUCT_0, COLLSP,
ANPROJ_1, XREAL_0, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions COLLSP, ANPROJ_1;
equalities BINOP_1, FUNCSDOM, RLVECT_1, STRUCT_0, ALGSTR_0;
expansions COLLSP, ANPROJ_1, STRUCT_0;
theorems RLVECT_1, FUNCT_2, FUNCSDOM, COLLSP, ANPROJ_1, ENUMSET1, XCMPLX_0,
XCMPLX_1, FUNCOP_1, STRUCT_0, XREAL_0;
schemes FUNCT_2;
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 Th1:
(for a,b,c st a*u + b*v + c*w = 0.V holds a = 0 & b = 0 & c = 0)
implies u is not zero & v is not zero & w is not zero & not u,v,w are_LinDep &
not are_Prop u,v
proof
assume
A1: for a,b,c st a*u + b*v + c*w = 0.V holds a=0 & b=0 & c = 0;
A2: now
assume not v is not zero;
then
A3: v = 0.V;
0.V = 0.V + 0.V by RLVECT_1:4
.= 0.V + 0.V + 0.V by RLVECT_1:4
.= 0.V + 1*v + 0.V by A3,RLVECT_1:def 8
.= 0*u + 1*v + 0.V by RLVECT_1:10
.= 0*u + 1*v + 0*w by RLVECT_1:10;
hence contradiction by A1;
end;
A4: now
assume not w is not zero;
then
A5: w = 0.V;
0.V = 0.V + 0.V by RLVECT_1:4
.= 0.V + 0.V + 0.V by RLVECT_1:4
.= 0.V + 0.V + 1*w by A5,RLVECT_1:def 8
.= 0*u + 0.V + 1*w by RLVECT_1:10
.= 0*u + 0*v + 1*w by RLVECT_1:10;
hence contradiction by A1;
end;
now
assume not u is not zero;
then
A6: u = 0.V;
0.V = 0.V + 0.V by RLVECT_1:4
.= 0.V + 0.V + 0.V by RLVECT_1:4
.= 1*u + 0.V + 0.V by A6,RLVECT_1:def 8
.= 1*u + 0*v + 0.V by RLVECT_1:10
.= 1*u + 0*v + 0*w by RLVECT_1:10;
hence contradiction by A1;
end;
hence u is not zero & v is not zero & w is not zero by A2,A4;
thus not u,v,w are_LinDep by A1;
hence thesis by ANPROJ_1:12;
end;
Lm1: (for a,b st a*u + b*v = 0.V holds a = 0 & b = 0 ) implies u is not zero &
v is not zero & not are_Prop u,v
proof
assume
A1: for a,b st a*u + b*v = 0.V holds a=0 & b=0;
A2: now
assume not v is not zero;
then
A3: v = 0.V;
0.V = 0.V + 0.V by RLVECT_1:4
.= 0.V + 1*v by A3,RLVECT_1:def 8
.= 0*u + 1*v by RLVECT_1:10;
hence contradiction by A1;
end;
now
assume not u is not zero;
then
A4: u = 0.V;
0.V = 0.V + 0.V by RLVECT_1:4
.= 1*u + 0.V by A4,RLVECT_1:def 8
.= 1*u + 0*v by RLVECT_1:10;
hence contradiction by A1;
end;
hence u is not zero & v is not zero by A2;
given a,b such that
A5: a*u = b*v and
A6: a<>0 and
b<>0;
0.V = a*u - b*v by A5,RLVECT_1:15
.= a*u + b*(-v) by RLVECT_1:25
.= a*u + (-b)*v by RLVECT_1:24;
hence contradiction by A1,A6;
end;
theorem Th2:
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 not zero & v is not zero &
not are_Prop u,v & u1 is not zero & v1 is not zero & not are_Prop u1,v1 & not u
,v,u1 are_LinDep & not u1,v1,u are_LinDep)
proof
let u,v,u1,v1;
assume
A1: 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;
A2: now
let d1,d2,d3;
assume d1*u + d2*v + d3*u1 = 0.V;
then 0.V = d1*u + d2*v + d3*u1 + 0.V by RLVECT_1:4
.= d1*u + d2*v + d3*u1 + 0*v1 by RLVECT_1:10;
hence d1=0 & d2=0 & d3=0 by A1;
end;
now
let d1,d2,d3;
assume d1*u1 + d2*v1 + d3*u = 0.V;
then 0.V = d3*u + d1*u1 + d2*v1 by RLVECT_1:def 3
.= d3*u + 0.V + d1*u1 + d2*v1 by RLVECT_1:4
.= d3*u + 0*v + d1*u1 + d2*v1 by RLVECT_1:10;
hence d1=0 & d2=0 & d3=0 by A1;
end;
hence thesis by A2,Th1;
end;
Lm2: a*(b*v+c*w+d*u) = (a*b)*v+(a*c)*w+(a*d)*u
proof
thus (a*b)*v+(a*c)*w+(a*d)*u = a*(b*v)+(a*c)*w+(a*d)*u by RLVECT_1:def 7
.= a*(b*v)+a*(c*w)+(a*d)*u by RLVECT_1:def 7
.= a*(b*v+c*w)+(a*d)*u by RLVECT_1:def 5
.= a*(b*v+c*w)+a*(d*u) by RLVECT_1:def 7
.= a*(b*v+c*w+d*u) by RLVECT_1:def 5;
end;
Lm3: (u+v+w) + (u1+v1+w1) = (u+u1)+(v+v1)+(w+w1)
proof
thus (u+u1)+(v+v1)+(w+w1) = u1+(u+(v+v1))+(w+w1) by RLVECT_1:def 3
.= u1+((u+v)+v1)+(w+w1) by RLVECT_1:def 3
.= (u1+v1)+(u+v)+(w+w1) by RLVECT_1:def 3
.= (u1+v1)+((u+v)+(w+w1)) by RLVECT_1:def 3
.= (u1+v1)+(u+v+w+w1) by RLVECT_1:def 3
.= (u+v+w) + (u1+v1+w1) by RLVECT_1:def 3;
end;
theorem Th3:
(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 not zero
proof
assume that
A1: for w ex a,b,c st w = a*p + b*q + c*r and
A2: for a,b,c st a*p + b*q + c*r = 0.V holds a = 0 & b = 0 & c = 0;
let u,u1;
consider a,b,c such that
A3: u = a*p + b*q + c*r by A1;
consider a1,b1,c1 such that
A4: u1 = a1*p + b1*q + c1*r by A1;
A5: a3*u + b3*u1 = (a3*a + b3*a1)*p + (a3*b + b3*b1)*q + (a3*c + b3*c1)*r
proof
a3*u = (a3*a)*p + (a3*b)*q + (a3*c)*r by A3,Lm2;
hence
a3*u + b3*u1 = ((a3*a)*p + (a3*b)*q + (a3*c)*r) + ((b3*a1)*p + (b3*b1
)*q + (b3*c1)*r) by A4,Lm2
.= ((a3*a)*p + (b3*a1)*p) + ((a3*b)*q + (b3*b1)*q) + ((a3*c)*r + (b3*
c1)*r) by Lm3
.= (a3*a + b3*a1)*p + ((a3*b)*q + (b3*b1)*q) + ((a3*c)*r + (b3*c1)*r)
by RLVECT_1:def 6
.= (a3*a + b3*a1)*p + (a3*b + b3*b1)*q + ((a3*c)*r + (b3*c1)*r) by
RLVECT_1:def 6
.= (a3*a + b3*a1)*p + (a3*b + b3*b1)*q + (a3*c + b3*c1)*r by
RLVECT_1:def 6;
end;
A6: q is not zero by A2,Th1;
A7: now
A8: now
assume not u1 is not zero;
then u1 = 0.V;
then p,q,q are_LinDep & u,u1,q are_LinDep by ANPROJ_1:10,11;
hence thesis by A6;
end;
A9: now
assume not u is not zero;
then u = 0.V;
then p,q,q are_LinDep & u,u1,q are_LinDep by ANPROJ_1:10,11;
hence thesis by A6;
end;
A10: now
assume are_Prop u,u1;
then p,q,q are_LinDep & u,u1,q are_LinDep by ANPROJ_1:11;
hence thesis by A6;
end;
assume are_Prop u,u1 or not u is not zero or not u1 is not zero;
hence thesis by A10,A9,A8;
end;
A11: p is not zero & not are_Prop p,q by A2,Th1;
A12: now
assume that
A13: not are_Prop u,u1 and
A14: u is not zero and
A15: u1 is not zero and
A16: c <> 0;
A17: now
set a3 = 1,b3 = -(c*c1");
set y = a3*u + b3*u1;
assume
A18: c1 <> 0;
then c1"<>0 by XCMPLX_1:202;
then
A19: c*c1" <> 0 by A16,XCMPLX_1:6;
A20: y is not zero
proof
assume not y is not zero;
then 0.V = 1*u + (-(c*c1"))*u1
.= 1*u + (c*c1")*(-u1) by RLVECT_1:24
.= 1*u + -((c*c1")*u1) by RLVECT_1:25;
then -1*u = -((c*c1")*u1) by RLVECT_1:def 10;
then 1*u = (c*c1")*u1 by RLVECT_1:18;
hence contradiction by A13,A19;
end;
a3*c + b3*c1 = c + (-c)*(c1"*c1) .= c + (-c)*1 by A18,XCMPLX_0:def 7
.= 0;
then y = (a3*a + b3*a1)*p + (a3*b + b3*b1)*q + 0*r by A5
.= (a3*a + b3*a1)*p + (a3*b + b3*b1)*q + 0.V by RLVECT_1:10
.= (a3*a + b3*a1)*p + (a3*b + b3*b1)*q by RLVECT_1:4;
then
A21: p,q,y are_LinDep by A6,A11,ANPROJ_1:6;
u,u1,y are_LinDep by A13,A14,A15,ANPROJ_1:6;
hence thesis by A20,A21;
end;
now
set a3 = 0,b3 = 1;
set y = a3*u + b3*u1;
A22: y = 0*u + u1 by RLVECT_1:def 8
.= 0.V + u1 by RLVECT_1:10
.= u1 by RLVECT_1:4;
assume c1 = 0;
then a3*c + b3*c1 = 0;
then y = (a3*a + b3*a1)*p + (a3*b + b3*b1)*q + 0*r by A5
.= (a3*a + b3*a1)*p + (a3*b + b3*b1)*q + 0.V by RLVECT_1:10
.= (a3*a + b3*a1)*p + (a3*b + b3*b1)*q by RLVECT_1:4;
then
A23: p,q,y are_LinDep by A6,A11,ANPROJ_1:6;
u,u1,y are_LinDep by A13,A14,A15,ANPROJ_1:6;
hence thesis by A15,A22,A23;
end;
hence thesis by A17;
end;
now
assume that
A24: not are_Prop u,u1 and
A25: u is not zero and
A26: u1 is not zero and
A27: c = 0;
now
set a3 = 1,b3 = 0;
set y = a3*u + b3*u1;
A28: y = u + 0*u1 by RLVECT_1:def 8
.= u + 0.V by RLVECT_1:10
.= u by RLVECT_1:4;
a3*c + b3*c1 = 0 by A27;
then y = (a3*a + b3*a1)*p + (a3*b + b3*b1)*q + 0*r by A5
.= (a3*a + b3*a1)*p + (a3*b + b3*b1)*q + 0.V by RLVECT_1:10
.= (a3*a + b3*a1)*p + (a3*b + b3*b1)*q by RLVECT_1:4;
then
A29: p,q,y are_LinDep by A6,A11,ANPROJ_1:6;
u,u1,y are_LinDep by A24,A25,A26,ANPROJ_1:6;
hence thesis by A25,A28,A29;
end;
hence thesis;
end;
hence thesis by A7,A12;
end;
Lm4: a*(b*v+c*w+d*u+d1*y) = (a*b)*v+(a*c)*w+(a*d)*u+(a*d1)*y
proof
thus (a*b)*v+(a*c)*w+(a*d)*u+(a*d1)*y = a*(b*v)+(a*c)*w+(a*d)*u+ (a*d1)*y by
RLVECT_1:def 7
.= a*(b*v)+a*(c*w)+(a*d)*u+(a*d1)*y by RLVECT_1:def 7
.= a*(b*v+c*w)+(a*d)*u+(a*d1)*y by RLVECT_1:def 5
.= a*(b*v+c*w)+a*(d*u)+(a*d1)*y by RLVECT_1:def 7
.= a*(b*v+c*w)+a*(d*u)+a*(d1*y) by RLVECT_1:def 7
.= a*(b*v+c*w+d*u)+a*(d1*y) by RLVECT_1:def 5
.= a*(b*v+c*w+d*u+d1*y) by RLVECT_1:def 5;
end;
Lm5: (u+v+w+y) + (u1+v1+w1+y1) = (u+u1)+(v+v1)+(w+w1)+(y+y1)
proof
thus (u+u1)+(v+v1)+(w+w1)+(y+y1) = u1+(u+(v+v1))+(w+w1)+(y+y1) by
RLVECT_1:def 3
.= u1+((u+v)+v1)+(w+w1)+(y+y1) by RLVECT_1:def 3
.= (u1+v1)+(u+v)+(w+w1)+(y+y1) by RLVECT_1:def 3
.= (u1+v1)+((u+v)+(w+w1))+(y+y1) by RLVECT_1:def 3
.= (u1+v1)+(u+v+w+w1)+(y+y1) by RLVECT_1:def 3
.= (u1+v1+w1)+(u+v+w)+(y+y1) by RLVECT_1:def 3
.= (u+v+w)+((u1+v1+w1)+(y+y1)) by RLVECT_1:def 3
.= (u+v+w)+(y+(y1+(u1+v1+w1))) by RLVECT_1:def 3
.= (u+v+w+y)+(u1+v1+w1+y1) by RLVECT_1:def 3;
end;
Lm6: a*(b*v+c*w+d*u) = (a*b)*v+(a*c)*w+(a*d)*u
proof
thus (a*b)*v+(a*c)*w+(a*d)*u = a*(b*v)+(a*c)*w+(a*d)*u by RLVECT_1:def 7
.= a*(b*v)+a*(c*w)+(a*d)*u by RLVECT_1:def 7
.= a*(b*v+c*w)+(a*d)*u by RLVECT_1:def 5
.= a*(b*v+c*w)+a*(d*u) by RLVECT_1:def 7
.= a*(b*v+c*w+d*u) by RLVECT_1:def 5;
end;
Lm7: y = a1*p + b1*w & w = a*p + b*q + c*r implies y = (a1 + b1*a)*p + (b1*b)*
q + (b1*c)*r
proof
assume y = a1*p + b1*w & w = a*p + b*q + c*r;
hence y = a1*p + ((b1*a)*p + (b1*b)*q + (b1*c)*r) by Lm6
.= a1*p + ((b1*a)*p + ((b1*b)*q + (b1*c)*r)) by RLVECT_1:def 3
.= (a1*p + (b1*a)*p) + ((b1*b)*q + (b1*c)*r) by RLVECT_1:def 3
.= (a1+b1*a)*p + ((b1*b)*q + (b1*c)*r) by RLVECT_1:def 6
.= (a1 + b1*a)*p + (b1*b)*q + (b1*c)*r by RLVECT_1:def 3;
end;
theorem Th4:
(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 not zero & v is not zero ex y,w st u,v,w are_LinDep & q,r,y
are_LinDep & p,w,y are_LinDep & y is not zero & w is not zero
proof
assume that
A1: for w ex a,b,c,d st w = a*p + b*q + c*r + d*s and
A2: 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;
A3: p is not zero by A2,Th2;
let u,v such that
A4: u is not zero and
A5: v is not zero;
consider a1,b1,c1,d1 such that
A6: u = a1*p + b1*q + c1*r + d1*s by A1;
not p,q,r are_LinDep by A2,Th2;
then
A7: not are_Prop q,r by ANPROJ_1:11;
A8: q is not zero by A2,Th2;
consider a2,b2,c2,d2 such that
A9: v = a2*p + b2*q + c2*r + d2*s by A1;
A10: a3*u + b3*v = (a3*a1 + b3*a2)*p + (a3*b1 + b3*b2)*q + (a3*c1 + b3*c2)*r
+ (a3*d1 + b3*d2)*s
proof
a3*u = (a3*a1)*p + (a3*b1)*q + (a3*c1)*r + (a3*d1)*s by A6,Lm4;
hence
a3*u + b3*v = ((a3*a1)*p + (a3*b1)*q + (a3*c1)*r + (a3*d1)*s) + ((b3*
a2)*p + (b3*b2)*q + (b3*c2)*r + (b3*d2)*s) by A9,Lm4
.= ((a3*a1)*p + (b3*a2)*p) + ((a3*b1)*q + (b3*b2)*q) + ((a3*c1)*r + (
b3*c2)*r) + ((a3*d1)*s + (b3*d2)*s) by Lm5
.= (a3*a1+b3*a2)*p + ((a3*b1)*q + (b3*b2)*q) + ((a3*c1)*r + (b3*c2)*r)
+ ((a3*d1)*s + (b3*d2)*s) by RLVECT_1:def 6
.= (a3*a1+b3*a2)*p + (a3*b1+b3*b2)*q + ((a3*c1)*r + (b3*c2)*r) + ((a3*
d1)*s + (b3*d2)*s) by RLVECT_1:def 6
.= (a3*a1+b3*a2)*p + (a3*b1+b3*b2)*q + (a3*c1+ b3*c2)*r + ((a3*d1)*s +
(b3*d2)*s) by RLVECT_1:def 6
.= (a3*a1+b3*a2)*p + (a3*b1+b3*b2)*q + (a3*c1+b3*c2)*r + (a3*d1+b3*d2)
*s by RLVECT_1:def 6;
end;
A11: r is not zero by A2,Th2;
A12: now
assume
A13: not are_Prop u,v;
ex w st (w is not zero & u,v,w are_LinDep & ex A,B,C being Real
st w = A*p + B*q + C*r)
proof
A14: now
set a3 = -d2*d1",b3=1, w = a3*u+b3*v;
assume that
A15: d1<>0 and
A16: d2<>0;
set A = a3*a1 + b3*a2, B = a3*b1 + b3*b2, C = a3*c1 + b3*c2;
A17: A<>0 or B<>0 or C<>0
proof
A18: d2*d1" <> 0
proof
assume not thesis;
then d1"=0 by A16,XCMPLX_1:6;
hence contradiction by A15,XCMPLX_1:202;
end;
A19: d2*d1"*d1 = d2*(d1"*d1) .= d2*1 by A15,XCMPLX_0:def 7
.= d2;
assume
A20: not thesis;
then
A21: --d2*d1"*c1 = c2;
--d2*d1"*a1 = a2 & --d2*d1"*b1 = b2 by A20;
then (d2*d1")*u = v by A6,A9,A21,A19,Lm4;
hence contradiction by A13,A18,ANPROJ_1:1;
end;
a3*d1 + b3*d2 = -d2*(d1"*d1) + d2 .= -d2*1 + d2 by A15,XCMPLX_0:def 7
.= 0;
then
A22: w = (a3*a1 + b3*a2)*p + (a3*b1 + b3*b2)*q + (a3*c1 + b3*c2 )*r +
0*s by A10
.= (a3*a1 + b3*a2)*p + (a3*b1 + b3*b2)*q + (a3*c1 + b3*c2)*r + 0.V
by RLVECT_1:10
.= (a3*a1 + b3*a2)*p + (a3*b1 + b3*b2)*q + (a3*c1 + b3*c2)*r by
RLVECT_1:4;
then
A23: w = A*p+B*q+C*r+0.V by RLVECT_1:4
.= A*p+B*q+C*r+0*s by RLVECT_1:10;
A24: w is not zero
by A2,A23,A17;
u,v,w are_LinDep by A4,A5,A13,ANPROJ_1:6;
hence thesis by A22,A24;
end;
A25: now
assume
A26: d2=0;
take w = v;
A27: u,v,w are_LinDep by ANPROJ_1:11;
w = a2*p + b2*q + c2*r + 0.V by A9,A26,RLVECT_1:10
.= a2*p + b2*q + c2*r by RLVECT_1:4;
hence thesis by A5,A27;
end;
now
assume
A28: d1=0;
take w = u;
A29: u,v,w are_LinDep by ANPROJ_1:11;
w = a1*p + b1*q + c1*r + 0.V by A6,A28,RLVECT_1:10
.= a1*p + b1*q + c1*r by RLVECT_1:4;
hence thesis by A4,A29;
end;
hence thesis by A25,A14;
end;
then consider w such that
A30: w is not zero and
A31: u,v,w are_LinDep and
A32: ex A,B,C being Real st w = A*p + B*q + C*r;
consider A,B,C being Real such that
A33: w = A*p + B*q + C*r by A32;
A34: now
set b = 1, a = -A;
set y = a*p + b*w;
A35: y = (a+b*A)*p + (b*B)*q + (b*C)*r by A33,Lm7
.= 0.V + (1*B)*q + (1*C)*r by RLVECT_1:10
.= B*q + C*r by RLVECT_1:4;
assume
A36: not are_Prop p,w;
then
A37: p,w,y are_LinDep by A3,A30,ANPROJ_1:6;
A38: B<>0 or C<>0
proof
assume not thesis;
then
A39: w = A*p + 0.V + 0*r by A33,RLVECT_1:10
.= A*p + 0.V + 0.V by RLVECT_1:10
.= A*p + 0.V by RLVECT_1:4
.= A*p by RLVECT_1:4;
A<>0
by A39,RLVECT_1:10,A30;
hence contradiction by A36,A39,ANPROJ_1:1;
end;
A40: y is not zero
proof
assume not thesis;
then 0.V = B*q + C*r by A35
.= 0.V + B*q + C*r by RLVECT_1:4
.= 0*p + B*q + C*r by RLVECT_1:10
.= 0*p + B*q + C*r + 0.V by RLVECT_1:4
.= 0*p + B*q + C*r + 0*s by RLVECT_1:10;
hence contradiction by A2,A38;
end;
q,r,y are_LinDep by A8,A11,A7,A35,ANPROJ_1:6;
hence thesis by A30,A31,A40,A37;
end;
now
assume are_Prop p,w;
then q,r,q are_LinDep & p,w,q are_LinDep by ANPROJ_1:11;
hence thesis by A8,A30,A31;
end;
hence thesis by A34;
end;
now
assume are_Prop u,v;
then
A41: u,v,p are_LinDep by ANPROJ_1:11;
q,r,q are_LinDep & p,p,q are_LinDep by ANPROJ_1:11;
hence thesis by A3,A8,A41;
end;
hence thesis by A12;
end;
theorem Th5:
(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 not zero & u,v,y are_LinDep & u1,v1,y
are_LinDep
proof
assume
A1: 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;
then
A2: not are_Prop u,v by Th2;
assume not thesis;
then consider y such that
A3: y is not zero and
A4: u,v,y are_LinDep and
A5: u1,v1,y are_LinDep;
u is not zero & v is not zero by A1,Th2;
then consider a,b such that
A6: y = a*u + b*v by A4,A2,ANPROJ_1:6;
A7: not are_Prop u1,v1 by A1,Th2;
u1 is not zero & v1 is not zero by A1,Th2;
then consider a1,b1 such that
A8: y = a1*u1 + b1*v1 by A5,A7,ANPROJ_1:6;
0.V = (a*u + b*v) - (a1*u1 + b1*v1) by A6,A8,RLVECT_1:15
.= (a*u + b*v) + (-1)*(a1*u1 + b1*v1) by RLVECT_1:16
.= (a*u + b*v) + ((-1)*(a1*u1) + (-1)*(b1*v1)) by RLVECT_1:def 5
.= (a*u + b*v) + (((-1)*a1)*u1 + (-1)*(b1*v1)) by RLVECT_1:def 7
.= (a*u + b*v) + (((-1)*a1)*u1 + ((-1)*b1)*v1) by RLVECT_1:def 7
.= a*u + b*v + ((-1)*a1)*u1 + ((-1)*b1)*v1 by RLVECT_1:def 3;
then a=0 & b=0 by A1;
then y = 0.V + 0*v by A6,RLVECT_1:10
.= 0.V + 0.V by RLVECT_1:10
.= 0.V by RLVECT_1:4;
hence contradiction by A3;
end;
definition
let V,u,v,w;
pred u,v,w are_Prop_Vect means
u is not zero & v is not zero & w is not zero;
end;
definition
let V,u,v,w,u1,v1,w1;
pred u,v,w,u1,v1,w1 lie_on_a_triangle means
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
o,u,u2 are_LinDep & o,v, v2 are_LinDep & o,w,w2 are_LinDep;
end;
Lm8: -(a*o) = (-a)*o
proof
thus -(a*o) = a*(-o) by RLVECT_1:25
.= (-a)*o by RLVECT_1:24;
end;
theorem Th6:
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
proof
assume that
A1: o,u,u2 are_LinDep and
A2: not are_Prop o,u and
A3: not are_Prop o,u2 and
A4: not are_Prop u,u2 and
A5: o,u,u2 are_Prop_Vect;
consider a,b,c such that
A6: a*o + b*u + c*u2 = 0.V and
A7: a<>0 or b<>0 or c <>0 by A1;
u is not zero by A5;
then
A8: u <> 0.V;
u2 is not zero by A5;
then
A9: u2 <>0.V;
o is not zero by A5;
then
A10: o <> 0.V;
A11: a<>0 & b<>0 & c <>0
proof
A12: now
assume
A13: b = 0;
then 0.V = a*o + 0.V + c*u2 by A6,RLVECT_1:10
.= a*o + c*u2 by RLVECT_1:4;
then a*o = -c*u2 by RLVECT_1:6
.= c*(-u2) by RLVECT_1:25;
then
A14: a*o = (-c)*u2 by RLVECT_1:24;
A15: a<>0 & c <>0
proof
A16: now
assume
A17: c = 0;
then 0.V = a*o + 0*u + 0.V by A6,A13,RLVECT_1:10
.= a*o + 0*u by RLVECT_1:4
.= a*o + 0.V by RLVECT_1:10
.= a*o by RLVECT_1:4;
hence contradiction by A7,A10,A13,A17,RLVECT_1:11;
end;
A18: now
assume
A19: a = 0;
then 0.V = 0.V + 0*u + c*u2 by A6,A13,RLVECT_1:10
.= 0*u + c*u2 by RLVECT_1:4
.= 0.V + c*u2 by RLVECT_1:10
.= c*u2 by RLVECT_1:4;
hence contradiction by A7,A9,A13,A19,RLVECT_1:11;
end;
assume not thesis;
hence contradiction by A18,A16;
end;
then -c <>0;
hence contradiction by A3,A15,A14;
end;
A20: now
assume
A21: a = 0;
then 0.V = 0.V + b*u + c*u2 by A6,RLVECT_1:10
.= b*u + c*u2 by RLVECT_1:4;
then b*u = -c*u2 by RLVECT_1:6
.= c*(-u2) by RLVECT_1:25;
then
A22: b*u = (-c)*u2 by RLVECT_1:24;
A23: b<>0 & c <>0
proof
A24: now
assume
A25: c = 0;
then 0.V = 0.V + b*u + 0*u2 by A6,A21,RLVECT_1:10
.= b*u + 0*u2 by RLVECT_1:4
.= b*u + 0.V by RLVECT_1:10
.= b*u by RLVECT_1:4;
hence contradiction by A7,A8,A21,A25,RLVECT_1:11;
end;
A26: now
assume
A27: b = 0;
then 0.V = 0.V + 0*u + c*u2 by A6,A21,RLVECT_1:10
.= 0*u + c*u2 by RLVECT_1:4
.= 0.V + c*u2 by RLVECT_1:10
.= c*u2 by RLVECT_1:4;
hence contradiction by A7,A9,A21,A27,RLVECT_1:11;
end;
assume not thesis;
hence contradiction by A26,A24;
end;
then -c <>0;
hence contradiction by A4,A23,A22;
end;
A28: now
assume
A29: c = 0;
then 0.V = a*o + b*u + 0.V by A6,RLVECT_1:10
.= a*o + b*u by RLVECT_1:4;
then a*o = -b*u by RLVECT_1:6
.= b*(-u) by RLVECT_1:25;
then
A30: a*o = (-b)*u by RLVECT_1:24;
A31: a<>0 & b<>0
proof
A32: now
assume
A33: b = 0;
then 0.V = a*o + 0*u + 0.V by A6,A29,RLVECT_1:10
.= a*o + 0*u by RLVECT_1:4
.= a*o + 0.V by RLVECT_1:10
.= a*o by RLVECT_1:4;
hence contradiction by A7,A10,A29,A33,RLVECT_1:11;
end;
A34: now
assume
A35: a = 0;
then 0.V = 0.V + b*u + 0*u2 by A6,A29,RLVECT_1:10
.= b*u + 0*u2 by RLVECT_1:4
.= b*u + 0.V by RLVECT_1:10
.= b*u by RLVECT_1:4;
hence contradiction by A7,A8,A29,A35,RLVECT_1:11;
end;
assume not thesis;
hence contradiction by A34,A32;
end;
then -b<>0;
hence contradiction by A2,A31,A30;
end;
assume not thesis;
hence contradiction by A20,A12,A28;
end;
then
A36: c" <> 0 by XCMPLX_1:202;
a" <> 0 by A11,XCMPLX_1:202;
then
A37: a"*b <> 0 & -(a"*c) <> 0 by A11,XCMPLX_1:6;
a"*(-c*u2) = a"*(a*o + b*u) by A6,RLVECT_1:6
.= a"*(a*o) + a"*(b*u) by RLVECT_1:def 5
.= (a"*a)*o + a"*(b*u) by RLVECT_1:def 7
.= (a"*a)*o + (a"*b)*u by RLVECT_1:def 7
.= 1*o + (a"*b)*u by A11,XCMPLX_0:def 7
.= o + (a"*b)*u by RLVECT_1:def 8;
then o + (a"*b)*u = a"*(c*(-u2)) by RLVECT_1:25
.= (a"*c)*(-u2) by RLVECT_1:def 7
.= (-(a"*c))*u2 by RLVECT_1:24;
hence ex a1,b1 st b1*u2=o+a1*u & a1<>0 & b1<>0 by A37;
-b <> 0 by A11;
then
A38: (c"*(-b)) <> 0 by A36,XCMPLX_1:6;
c*u2 = -(a*o + b*u) by A6,RLVECT_1:def 10
.= -(a*o) + (-(b*u)) by RLVECT_1:31
.= (-a)*o + (-(b*u)) by Lm8
.= (-a)*o + (-b)*u by Lm8;
then c"*(c*u2) = c"*((-a)*o) + c"*((-b)*u) by RLVECT_1:def 5
.= (c"*(-a))*o + c"*((-b)*u) by RLVECT_1:def 7
.= (c"*(-a))*o + (c"*(-b))*u by RLVECT_1:def 7;
then
A39: (c"*(-a))*o + (c"*(-b))*u = (c"*c)*u2 by RLVECT_1:def 7
.= 1*u2 by A11,XCMPLX_0:def 7
.= u2 by RLVECT_1:def 8;
-a <> 0 by A11;
then (c"*(-a)) <> 0 by A36,XCMPLX_1:6;
hence thesis by A39,A38;
end;
theorem Th7:
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
proof
assume that
A1: p,q,r are_LinDep and
A2: not are_Prop p,q and
A3: p,q,r are_Prop_Vect;
consider a,b,c such that
A4: a*p + b*q + c*r = 0.V and
A5: a<>0 or b<>0 or c <>0 by A1;
q is not zero by A3;
then
A6: q <> 0.V;
p is not zero by A3;
then
A7: p <> 0.V;
A8: c <>0
proof
assume
A9: not thesis;
then 0.V = a*p + b*q + 0.V by A4,RLVECT_1:10
.= a*p + b*q by RLVECT_1:4;
then
A10: a*p = -(b*q) by RLVECT_1:6
.= (-b)*q by Lm8;
A11: a<>0 & b<>0
proof
A12: now
assume
A13: b = 0;
then 0.V =a*p + 0.V + 0*r by A4,A9,RLVECT_1:10
.= a*p + 0.V + 0.V by RLVECT_1:10
.= a*p + 0.V by RLVECT_1:4
.= a*p by RLVECT_1:4;
hence contradiction by A7,A5,A9,A13,RLVECT_1:11;
end;
A14: now
assume
A15: a = 0;
then 0.V = 0.V + b*q + 0*r by A4,A9,RLVECT_1:10
.= 0.V + b*q + 0.V by RLVECT_1:10
.= b*q + 0.V by RLVECT_1:4
.= b*q by RLVECT_1:4;
hence contradiction by A6,A5,A9,A15,RLVECT_1:11;
end;
assume not thesis;
hence contradiction by A14,A12;
end;
then -b <> 0;
hence contradiction by A2,A11,A10;
end;
c*r = -(a*p + b*q) by A4,RLVECT_1:def 10
.= -(a*p) + (-(b*q)) by RLVECT_1:31
.= (-a)*p + (-(b*q)) by Lm8
.= (-a)*p + (-b)*q by Lm8;
then c"*(c*r) = c"*((-a)*p) + c"*((-b)*q) by RLVECT_1:def 5
.= (c"*(-a))*p + c"*((-b)*q) by RLVECT_1:def 7
.= (c"*(-a))*p + (c"*(-b))*q by RLVECT_1:def 7;
then (c"*(-a))*p + (c"*(-b))*q = (c"*c)*r by RLVECT_1:def 7
.= 1*r by A8,XCMPLX_0:def 7
.= r by RLVECT_1:def 8;
hence thesis;
end;
Lm9: b1*u2=w2 & b1 <> 0 implies are_Prop u2,w2
proof
assume that
A1: b1*u2=w2 and
A2: b1 <> 0;
b1*u2 = 1*w2 by A1,RLVECT_1:def 8;
hence thesis by A2;
end;
Lm10: q = o + a*p & r = o + b*s & are_Prop q,r & a<>0 implies o,p,s are_LinDep
proof
assume that
A1: q = o + a*p & r = o + b*s & are_Prop q,r and
A2: a<>0;
consider A being Real such that
A <> 0 and
A3: o + a*p = A*(o + b*s) by A1,ANPROJ_1:1;
o + a*p = A*o + A*(b*s) by A3,RLVECT_1:def 5
.= A*o + (A*b)*s by RLVECT_1:def 7;
then -(A*o) + (o + a*p) = (-(A*o) + A*o) + (A*b)*s by RLVECT_1:def 3
.= 0.V + (A*b)*s by RLVECT_1:5
.= (A*b)*s by RLVECT_1:4;
then (-(A*o) + o) + a*p = (A*b)*s by RLVECT_1:def 3;
then (A*b)*s = ((-A)*o + o) + a*p by Lm8
.= ((-A)*o + 1*o) + a*p by RLVECT_1:def 8
.= (-A+1)*o + a*p by RLVECT_1:def 6;
then (-A+1)*o + a*p + (-((A*b)*s)) = 0.V by RLVECT_1:5;
then 0.V = (-A+1)*o + a*p + (-(A*b))*s by Lm8;
hence thesis by A2;
end;
Lm11: a*p = q & a <> 0 & p is not zero implies q is not zero
by RLVECT_1:11;
Lm12: for A,B being Real
holds ( r = A*u2 + B*v2 & u2 = o + a1*u & v2 = o + a2
*v implies r = (A + B)*o + (A*a1)*u + (B*a2)*v )
proof
let A,B be Real;
assume r = A*u2 + B*v2 & u2 = o + a1*u & v2 = o + a2 *v;
hence r = A*o + A*(a1*u) + B*(o + a2*v) by RLVECT_1:def 5
.= A*o + A*(a1*u) + (B*o + B*(a2*v)) by RLVECT_1:def 5
.= A*o + (A*a1)*u + (B*o + B*(a2*v)) by RLVECT_1:def 7
.= A*o + (A*a1)*u + (B*o + (B*a2)*v) by RLVECT_1:def 7
.= (A*o + (A*a1)*u + B*o) + (B*a2)*v by RLVECT_1:def 3
.= A*o + B*o + (A*a1)*u + (B*a2)*v by RLVECT_1:def 3
.= (A + B)*o + (A*a1)*u + (B*a2)*v by RLVECT_1:def 6;
end;
Lm13: r = a*p + b*q implies r = 0*o + a*p + b*q
proof
assume r = a*p + b*q;
hence r = 0.V + a*p + b*q by RLVECT_1:4
.= 0*o + a*p + b*q by RLVECT_1:10;
end;
Lm14: 0*p + 0*q = 0.V
proof
thus 0*p + 0*q = 0.V + 0*q by RLVECT_1:10
.= 0*q by RLVECT_1:4
.= 0.V by RLVECT_1:10;
end;
Lm15: 0*o + (b*a2)*v + ((-b)*a3)*w = b*(a2*v - a3*w)
proof
thus 0*o + (b*a2)*v + ((-b)*a3)*w = 0.V + (b*a2)*v + ((-b)*a3)*w by
RLVECT_1:10
.= (b*a2)*v + ((-b)*a3)*w by RLVECT_1:4
.= b*(a2*v) + (b*(-a3))*w by RLVECT_1:def 7
.= b*(a2*v) + b*((-a3)*w) by RLVECT_1:def 7
.= b*(a2*v) + b*(-(a3*w)) by Lm8
.= b*(a2*v - a3*w) by RLVECT_1:def 5;
end;
theorem Th8:
o is not zero & 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
proof
assume that
A1: o is not zero and
A2: u,v,w are_Prop_Vect and
A3: u2,v2,w2 are_Prop_Vect and
A4: u1,v1,w1 are_Prop_Vect and
A5: o,u,v,w,u2,v2,w2 are_perspective and
A6: not are_Prop o,u2 and
A7: not are_Prop o,v2 and
A8: not are_Prop o,w2 and
A9: not are_Prop u,u2 and
A10: not are_Prop v,v2 and
A11: not are_Prop w,w2 and
A12: not o,u,v are_LinDep and
A13: not o,u,w are_LinDep and
A14: not o,v,w are_LinDep and
A15: u,v,w,u1,v1,w1 lie_on_a_triangle and
A16: u2,v2,w2,u1,v1,w1 lie_on_a_triangle;
A17: w is not zero by A2;
A18: o,w,w2 are_LinDep & not are_Prop w,o by A5,A13,ANPROJ_1:11;
A19: w2 is not zero by A3;
then o,w,w2 are_Prop_Vect by A1,A17;
then consider a3,b3 such that
A20: b3*w2=o+a3*w and
a3<>0 and
A21: b3<>0 by A8,A11,A18,Th6;
A22: u is not zero by A2;
A23: v is not zero by A2;
A24: o,v,v2 are_LinDep & not are_Prop o,v by A5,A12,ANPROJ_1:11;
A25: o,u,u2 are_LinDep & not are_Prop o,u by A5,A12,ANPROJ_1:11;
A26: u2 is not zero by A3;
then o,u,u2 are_Prop_Vect by A1,A22;
then consider a1,b1 such that
A27: b1*u2=o+a1*u and
A28: a1<>0 and
A29: b1<>0 by A6,A9,A25,Th6;
A30: v2 is not zero by A3;
then o,v,v2 are_Prop_Vect by A1,A23;
then consider a2,b2 such that
A31: b2*v2=o+a2*v and
A32: a2<>0 and
A33: b2<>0 by A7,A10,A24,Th6;
set u29 = o+a1*u, v29 = o+a2*v, w29 = o+a3*w;
A34: are_Prop v2,v29 by A31,A33,Lm9;
A35: v29 is not zero by A30,A31,A33,Lm11;
A36: are_Prop w2,w29 by A20,A21,Lm9;
A37: u,v,w1 are_LinDep & not are_Prop u,v by A12,A15,ANPROJ_1:12;
A38: w1 is not zero by A4;
then u,v,w1 are_Prop_Vect by A22,A23;
then consider c3,d3 such that
A39: w1 = c3*u + d3*v by A37,Th7;
A40: are_Prop u2,u29 by A27,A29,Lm9;
A41: v,w,u1 are_LinDep & not are_Prop v,w by A14,A15,ANPROJ_1:12;
A42: u1 is not zero by A4;
then v,w,u1 are_Prop_Vect by A23,A17;
then consider c1,d1 such that
A43: u1 = c1*v + d1*w by A41,Th7;
v2,w2,u1 are_LinDep by A16;
then
A44: v29,w29,u1 are_LinDep by A34,A36,ANPROJ_1:4;
A45: not are_Prop v29,w29 by A14,A32,Lm10;
A46: w29 is not zero by A19,A20,A21,Lm11;
then v29,w29,u1 are_Prop_Vect by A42,A35;
then consider A1,B1 being Real such that
A47: u1 = A1*v29 + B1*w29 by A44,A45,Th7;
A48: u,w,v1 are_LinDep & not are_Prop u,w by A13,A15,ANPROJ_1:12;
A49: v1 is not zero by A4;
then u,w,v1 are_Prop_Vect by A22,A17;
then consider c2,d2 such that
A50: v1 = c2*u + d2*w by A48,Th7;
A51: u1 = (A1 + B1)*o + (A1*a2)*v + (B1*a3)*w by A47,Lm12;
u2,v2,w1 are_LinDep by A16;
then
A52: u29,v29,w1 are_LinDep by A40,A34,ANPROJ_1:4;
A53: not are_Prop u29,v29 by A12,A28,Lm10;
A54: u29 is not zero by A26,A27,A29,Lm11;
then u29,v29,w1 are_Prop_Vect by A38,A35;
then consider A3,B3 being Real such that
A55: w1 = A3*u29 + B3*v29 by A52,A53,Th7;
u2,w2,v1 are_LinDep by A16;
then
A56: u29,w29,v1 are_LinDep by A40,A36,ANPROJ_1:4;
A57: not are_Prop u29,w29 by A13,A28,Lm10;
A58: w1 = (A3 + B3)*o + (A3*a1)*u + (B3*a2)*v by A55,Lm12;
u29,w29,v1 are_Prop_Vect by A49,A54,A46;
then consider A2,B2 being Real such that
A59: v1 = A2*u29 + B2*w29 by A56,A57,Th7;
A60: v1 = (A2 + B2)*o + (A2*a1)*u + (B2*a3)*w by A59,Lm12;
w1 = 0*o + c3*u + d3*v by A39,Lm13;
then
A61: A3 + B3 = 0 by A12,A58,ANPROJ_1:8;
u1 = 0*o + c1*v + d1*w by A43,Lm13;
then
A62: A1 + B1 = 0 by A14,A51,ANPROJ_1:8;
v1 = 0*o + c2*u + d2*w by A50,Lm13;
then
A63: A2 + B2 = 0 by A13,A60,ANPROJ_1:8;
then
A64: A1 <> 0 & A2 <> 0 & A3 <> 0 by A42,A47,A62,A49,A59,A38,A55,A61,Lm14;
set u19 = a2*v - a3*w, v19 = a1*u - a3*w, w19 = a1*u - a2*v;
B1 = -A1 by A62;
then u1 = A1*u19 by A51,Lm15;
then
A65: are_Prop u19,u1 by A64,Lm9;
B3 = -A3 by A61;
then w1 = A3*w19 by A58,Lm15;
then
A66: are_Prop w19,w1 by A64,Lm9;
B2 = -A2 by A63;
then v1 = A2*v19 by A60,Lm15;
then
A67: are_Prop v19,v1 by A64,Lm9;
1*u19 + (-1)*v19 + 1*w19 = u19 + (-1)*v19 + 1*w19 by RLVECT_1:def 8
.= u19 + (-1)*v19 + w19 by RLVECT_1:def 8
.= u19 + (-v19) + w19 by RLVECT_1:16
.= (a2*v + (-(a3*w))) + (a3*w + (-(a1*u)) ) + (a1*u - a2*v) by RLVECT_1:33
.= a2*v + (-(a3*w)) + a3*w + (-(a1*u)) + (a1*u + (-(a2*v))) by
RLVECT_1:def 3
.= a2*v + ((-(a3*w)) + a3*w) + (-(a1*u)) + (a1*u + (-(a2*v))) by
RLVECT_1:def 3
.= a2*v + 0.V + (-(a1*u)) + (a1*u + (-(a2*v))) by RLVECT_1:5
.= a2*v + (-(a1*u)) + (a1*u + (-(a2*v))) by RLVECT_1:4
.= a2*v + ((-(a1*u)) + (a1*u + (-(a2*v)))) by RLVECT_1:def 3
.= a2*v + ((-(a1*u)) + a1*u + (-(a2*v))) by RLVECT_1:def 3
.= a2*v + (0.V + (-(a2*v))) by RLVECT_1:5
.= a2*v + (-(a2*v)) by RLVECT_1:4
.= 0.V by RLVECT_1:5;
then u19,v19,w19 are_LinDep;
hence thesis by A65,A67,A66,ANPROJ_1:4;
end;
definition
let V,o,u,v,w,u2,v2,w2;
pred o,u,v,w,u2,v2,w2 lie_on_an_angle means
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
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;
Lm16: b1*u2=w2 & b1 <> 0 implies are_Prop u2,w2
proof
assume that
A1: b1*u2=w2 and
A2: b1 <> 0;
b1*u2 = 1*w2 by A1,RLVECT_1:def 8;
hence thesis by A2;
end;
Lm17: not are_Prop p,q & y = a*q & a <> 0 implies not are_Prop p,y
proof
assume that
A1: not are_Prop p,q and
A2: y = a*q & a <> 0;
assume not thesis;
then consider b such that
A3: b <> 0 & p = b*y by ANPROJ_1:1;
p = (b*a)*q & b*a <> 0 by A2,A3,RLVECT_1:def 7,XCMPLX_1:6;
hence contradiction by A1,ANPROJ_1:1;
end;
Lm18: w1 = a*u + b*v2 & v2 = o + c2*u2 implies w1 = b*o + a*u + (b*c2)*u2
proof
assume w1 = a*u + b*v2 & v2 = o + c2*u2;
hence w1 = a*u + (b*o + b*(c2*u2)) by RLVECT_1:def 5
.= a*u + b*o + b*(c2*u2) by RLVECT_1:def 3
.= b*o + a*u + (b*c2)*u2 by RLVECT_1:def 7;
end;
Lm19: w1 = a*u2 + b*v1 & v1 = o + a2*u implies w1 = b*o + (b*a2)*u + a*u2
proof
assume w1 = a*u2 + b*v1 & v1 = o + a2*u;
hence w1 = b*o + a*u2 + (b*a2)*u by Lm18
.= b*o + (b*a2)*u + a*u2 by RLVECT_1:def 3;
end;
Lm20: a*p = q & a <> 0 & p is not zero implies q is not zero
by RLVECT_1:11;
Lm21: not are_Prop p,q & y = a*q & a <> 0 & s = b*p & b <> 0 implies not
are_Prop s,y
proof
assume that
A1: not are_Prop p,q and
A2: y = a*q & a <> 0 and
A3: s = b*p & b <> 0;
assume not thesis;
then consider c such that
A4: c <> 0 & s = c*y by ANPROJ_1:1;
s = (c*a)*q & c*a <> 0 by A2,A4,RLVECT_1:def 7,XCMPLX_1:6;
hence contradiction by A1,A3;
end;
Lm22: for A,B being Real
holds ( r = A*u2 + B*v2 & u2 = o + a1*u & v2 = o + a2
*v implies r = (A + B)*o + (A*a1)*u + (B*a2)*v )
proof
let A,B be Real;
assume r = A*u2 + B*v2 & u2 = o + a1*u & v2 = o + a2 *v;
hence r = A*o + A*(a1*u) + B*(o + a2*v) by RLVECT_1:def 5
.= A*o + A*(a1*u) + (B*o + B*(a2*v)) by RLVECT_1:def 5
.= A*o + (A*a1)*u + (B*o + B*(a2*v)) by RLVECT_1:def 7
.= A*o + (A*a1)*u + (B*o + (B*a2)*v) by RLVECT_1:def 7
.= (A*o + (A*a1)*u + B*o) + (B*a2)*v by RLVECT_1:def 3
.= A*o + B*o + (A*a1)*u + (B*a2)*v by RLVECT_1:def 3
.= (A + B)*o + (A*a1)*u + (B*a2)*v by RLVECT_1:def 6;
end;
Lm23: a2<>a3 & c2<>0 implies a3*c2 - a2*c2 <> 0
proof
assume that
A1: a2<>a3 and
A2: c2<>0;
a3*c2 - a2*c2 = (a3 - a2)*c2 & a3 - a2 <> 0 by A1;
hence thesis by A2,XCMPLX_1:6;
end;
Lm24: for A1,A19,B1,B19 being Real
holds ( A1 + B1 = A19 + B19 & A1*a2 = A19*
a3 & B1*c3 = B19*c2 & a2<>a3 & c2<>0 implies A1 = (a3*c3 - a3*c2)*(a3*c2 - a2*
c2)"*B1 )
proof
let A1,A19,B1,B19 be Real;
assume that
A1: A1 + B1 = A19 + B19 and
A2: A1*a2 = A19*a3 & B1*c3 = B19*c2 and
A3: a2<>a3 & c2<>0;
A4: A1*(a3*c2) + B1*(a3*c2) = (A19 + B19)*(a3*c2) by A1,XCMPLX_1:8;
A1*(a2*c2) = A19*a3*c2 & B1*(c3*a3) = B19*c2*a3 by A2,XCMPLX_1:4;
then B1*(a3*c3 - a3*c2) = A1*(a3*c2-a2*c2) by A4;
then
A5: A1*((a3*c2-a2*c2)*(a3*c2-a2*c2)") = B1*(a3*c3 - a3*c2)*(a3*c2-a2*c2)"
by XCMPLX_1:4;
a3*c2 - a2*c2 <> 0 by A3,Lm23;
then A1*1 = B1*(a3*c3 - a3*c2)*(a3*c2 -a2*c2)" by A5,XCMPLX_0:def 7;
hence thesis;
end;
Lm25: for B1 being Real
st c2<>0 & a2<>a3 & B1 <> 0 holds B1*(a3*c2 - a2*c2)" <> 0
proof
let B1 be Real;
assume that
A1: c2<>0 & a2<>a3 and
A2: B1 <> 0;
(a3*c2 - a2*c2)" <> 0 by A1,Lm23,XCMPLX_1:202;
hence thesis by A2,XCMPLX_1:6;
end;
Lm26: for A1,B1 being Real
holds ( A1 = (a3*c3 - a3*c2)*(a3*c2 - a2*c2)"*B1 &
c2<>0 & a2<>a3 & u1 = (A1 + B1)*o + (A1*a2)*u + (B1*c3)*u2 implies u1 = (B1*(a3
*c2 - a2*c2)")*((a3*c3 - a2*c2)*o + ((a2*a3)*(c3 - c2))*u + ((c2*c3)*(a3 - a2))
*u2) )
proof
let A1,B1 be Real;
assume that
A1: A1 = (a3*c3 - a3*c2)*(a3*c2 - a2*c2)"*B1 and
A2: c2<>0 & a2<>a3 and
A3: u1 = (A1 + B1)*o + (A1*a2)*u + (B1*c3)*u2;
A4: (a3*c2 - a2*c2) <> 0 by A2,Lm23;
A5: (B1*c3)*u2 = (B1*1*c3)*u2
.= (B1*((a3*c2 - a2*c2)"*(a3*c2 - a2*c2))*c3)*u2 by A4,XCMPLX_0:def 7
.= ((B1*(a3*c2 - a2*c2)")*((c3*c2)*(a3 - a2)))*u2
.= (B1*(a3*c2 - a2*c2)")*(((c2*c3)*(a3 - a2))*u2) by RLVECT_1:def 7;
A6: ((a3*c3 - a3*c2)*(a3*c2 - a2*c2)"*B1*a2)*u = ((B1*(a3*c2 - a2*c2)")*((a2
*a3)*(c3 - c2)))*u
.= (B1*(a3*c2 - a2*c2)")*(((a2*a3)*(c3 - c2))*u) by RLVECT_1:def 7;
((a3*c3 - a3*c2)*(a3*c2 - a2*c2)"*B1 + B1*1)*o = ((a3*c3 - a3*c2)*(B1*(
a3*c2 - a2*c2)") + B1*((a3*c2 - a2*c2)"*(a3*c2 - a2*c2)))*o by A4,
XCMPLX_0:def 7
.= ((B1*(a3*c2 - a2*c2)")*(a3*c3 + - a3*c2 + a3*c2 - a2*c2))*o
.= (B1*(a3*c2 - a2*c2)")*((a3*c3 - a2*c2)*o) by RLVECT_1:def 7;
hence u1 = (B1*(a3*c2 - a2*c2)")*((a3*c3 - a2*c2)*o + ((a2*a3)*(c3 - c2))*u)
+ (B1*(a3*c2 - a2*c2)")* (((c2*c3)*(a3 - a2))*u2) by A1,A3,A6,A5,
RLVECT_1:def 5
.= (B1*(a3*c2 - a2*c2)")*((a3*c3 - a2* c2)*o + ((a2*a3)*(c3 - c2))*u + (
(c2*c3)*(a3 - a2))*u2) by RLVECT_1:def 5;
end;
Lm27: (p+q+r) + (u+u2+u1) = (p+u)+(q+u2)+(r+u1)
proof
thus (p+u)+(q+u2)+(r+u1) = u+(p+(q+u2))+(r+u1) by RLVECT_1:def 3
.= u+((p+q)+u2)+(r+u1) by RLVECT_1:def 3
.= (u+u2)+(p+q)+(r+u1) by RLVECT_1:def 3
.= (u+u2)+((p+q)+(r+u1)) by RLVECT_1:def 3
.= (u+u2)+(p+q+r+u1) by RLVECT_1:def 3
.= (p+q+r) + (u+u2+u1) by RLVECT_1:def 3;
end;
Lm28: for C2,C3 being Real
holds ( u1 = (a3*c3 - a2*c2)*o + ((a2*a3)*(c3 - c2)
)*u + ((c2*c3)*(a3 - a2))*u2 & v1 = o + a3*u + c3*u2 & w2 = o + a2*u + c2*u2 &
C2 + C3 = a2*c2 - a3*c3 & C2*a3 + C3*a2 = (a2*a3)*(c2 - c3) & C2*c3 + C3*c2 = (
c2*c3)*(a2 - a3) implies 1*u1 + C2*v1 + C3*w2 = 0.V )
proof
let C2,C3 be Real such that
A1: u1 = (a3*c3 - a2*c2)*o + ((a2*a3)*(c3 - c2))*u + ((c2*c3)*(a3 - a2))
*u2 and
A2: v1 = o + a3*u + c3*u2 & w2 = o + a2*u + c2*u2 and
A3: C2 + C3 = a2*c2 - a3*c3 & C2*a3 + C3*a2 = (a2*a3)*(c2 - c3) & C2*c3
+ C3 *c2 = (c2*c3)*(a2 - a3);
A4: 1*u1 + C2*v1 + C3*w2 = u1 + C2*v1 + C3*w2 by RLVECT_1:def 8
.= u1 + (C2*v1 + C3*w2) by RLVECT_1:def 3;
C2*v1 + C3*w2 = C2*(o + a3*u) + C2*(c3*u2) + C3*(o + a2*u + c2*u2) by A2,
RLVECT_1:def 5
.= C2*o + C2*(a3*u) + C2*(c3*u2) + C3*(o + a2*u + c2*u2) by RLVECT_1:def 5
.= C2*o + C2*(a3*u) + C2*(c3*u2) + (C3*(o + a2*u) + C3*(c2*u2)) by
RLVECT_1:def 5
.= C2*o + C2*(a3*u) + C2*(c3*u2) + (C3*o + C3* (a2*u) + C3*(c2*u2)) by
RLVECT_1:def 5
.= (C2*o + C3*o) + (C2*(a3*u) + C3* (a2*u)) + (C2*(c3*u2) + C3*(c2*u2))
by Lm27
.= (C2 + C3)*o + (C2*(a3*u) + C3*(a2*u)) + (C2*(c3*u2) + C3*(c2*u2)) by
RLVECT_1:def 6
.= (C2 + C3)*o + ((C2*a3)*u + C3*(a2*u)) + (C2*(c3*u2) + C3*(c2*u2)) by
RLVECT_1:def 7
.= (C2 + C3)*o + ((C2*a3)*u + (C3*a2)*u) + (C2*(c3*u2) + C3*(c2*u2)) by
RLVECT_1:def 7
.= (C2 + C3)*o + ((C2*a3)*u + (C3*a2)*u) + ((C2*c3)*u2 + C3*(c2*u2)) by
RLVECT_1:def 7
.= (C2 + C3)*o + ((C2*a3)*u + (C3*a2)*u) + ((C2*c3)*u2 + (C3*c2)*u2) by
RLVECT_1:def 7
.= (C2 + C3)*o + (C2*a3 + C3*a2)*u + ((C2*c3)*u2 + (C3*c2)*u2) by
RLVECT_1:def 6
.= (a2*c2 - a3*c3)*o + ((a2*a3)*(c2 - c3))*u + ((c2*c3)*(a2 - a3))*u2 by A3
,RLVECT_1:def 6;
hence
1*u1 + C2*v1 + C3*w2 = ((a3*c3 - a2*c2)*o + (a2*c2 - a3*c3)*o) + (((a2*
a3)*(c3 - c2))*u + ((a2*a3)*(c2 - c3))*u) + (((c2*c3)*(a3 - a2))*u2 + ((c2*c3)*
(a2 - a3))*u2) by A1,A4,Lm27
.= ((a3*c3 - a2*c2 + (a2*c2 - a3*c3))*o) + (((a2*a3)*(c3 - c2))*u + ((a2
*a3)*(c2 - c3))*u) + (((c2*c3)*(a3 - a2))*u2 + ((c2*c3)*(a2 - a3))*u2) by
RLVECT_1:def 6
.= (a3*c3 - a2*c2 + (a2*c2 - a3*c3))*o + ((a2*a3)*(c3 - c2) + (a2*a3)*(
c2 - c3))*u + (((c2*c3)*(a3 - a2))*u2 + ((c2*c3)*(a2 - a3))*u2) by
RLVECT_1:def 6
.= (a3*c3 + -a2*c2 + a2*c2 + -a3*c3)*o + ((a2*a3)*(c3 - c2) + (a2*a3)*(
c2 - c3))*u + ((c2*c3)*(a3 - a2) + (c2*c3)*(a2 - a3))*u2 by RLVECT_1:def 6
.= 0.V + ((a2*a3)*(c3 - c2) + (a2*a3)*(c2 - c3))*u + ((c2*c3)*(a3 - a2)
+ (c2* c3)*(a2 - a3))*u2 by RLVECT_1:10
.= 0*u + ((c2*c3)*(a3 - a2) + -((c2*c3)* (a3 - a2)))*u2 by RLVECT_1:4
.= 0.V + 0*u2 by RLVECT_1:10
.= 0.V + 0.V by RLVECT_1:10
.= 0.V by RLVECT_1:4;
end;
Lm29: for A3,A39,B3,B39 being Real
holds ( w2 = o + a2*u + c2*u2 & w1 = B3*o +
A3*u + (B3*c2)*u2 & B3 = B39 & A3 = B39*a2 implies w1 = B3*w2 )
proof
let A3,A39,B3,B39 be Real;
assume that
A1: w2 = o + a2*u + c2*u2 and
A2: w1 = B3*o + A3*u + (B3*c2)*u2 & B3 = B39 & A3 = B39*a2;
thus w1 = B3*o + B3*(a2*u) + (B3*c2)*u2 by A2,RLVECT_1:def 7
.= B3*o + B3*(a2*u) + B3*(c2*u2) by RLVECT_1:def 7
.= B3*(o + a2*u) + B3*(c2*u2) by RLVECT_1:def 5
.= B3*w2 by A1,RLVECT_1:def 5;
end;
theorem Th9:
o is not zero & 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
proof
assume that
A1: o is not zero and
A2: u,v,w are_Prop_Vect and
A3: u2,v2,w2 are_Prop_Vect and
A4: u1,v1,w1 are_Prop_Vect and
A5: o,u,v,w,u2,v2,w2 lie_on_an_angle and
A6: o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop and
A7: u,v2,w1 are_LinDep and
A8: u2,v,w1 are_LinDep and
A9: u,w2,v1 are_LinDep and
A10: w,u2,v1 are_LinDep and
A11: v,w2,u1 are_LinDep and
A12: w,v2,u1 are_LinDep;
A13: u is not zero by A2;
A14: not are_Prop u2,v2 by A6;
A15: not are_Prop o,v by A6;
A16: not are_Prop u,v by A6;
A17: o,u2,v2 are_LinDep by A5;
A18: ( not are_Prop o,w2)& not are_Prop u2,w2 by A6;
A19: u2 is not zero by A3;
A20: ( not are_Prop o,w)& not are_Prop u,w by A6;
A21: o,u,w are_LinDep by A5;
A22: not are_Prop o,v2 by A6;
A23: o,u2,w2 are_LinDep by A5;
A24: not o,u,u2 are_LinDep by A5;
then
A25: not are_Prop o,u by ANPROJ_1:12;
A26: w is not zero by A2;
then o,u,w are_Prop_Vect by A1,A13;
then consider a3,b3 such that
A27: b3*w=o+a3*u and
a3<>0 and
A28: b3<>0 by A21,A20,A25,Th6;
A29: not are_Prop u2,o by A24,ANPROJ_1:12;
A30: w2 is not zero by A3;
then o,u2,w2 are_Prop_Vect by A1,A19;
then consider c3,d3 such that
A31: d3*w2=o+c3*u2 and
c3<>0 and
A32: d3<>0 by A23,A18,A29,Th6;
A33: o,u,v are_LinDep by A5;
A34: v2 is not zero by A3;
then o,u2,v2 are_Prop_Vect by A1,A19;
then consider c2,d2 such that
A35: d2*v2=o+c2*u2 and
A36: c2<>0 and
A37: d2<>0 by A17,A22,A14,A29,Th6;
A38: v is not zero by A2;
then o,u,v are_Prop_Vect by A1,A13;
then consider a2,b2 such that
A39: b2*v=o+a2*u and
a2<>0 and
A40: b2<>0 by A33,A15,A16,A25,Th6;
set v9 = o+a2*u, w9 = o+a3*u, v29 = o+c2*u2, w29 = o+c3*u2;
A41: v29 is not zero by A34,A35,A37,Lm20;
A42: v9 is not zero by A38,A39,A40,Lm20;
A43: w9 is not zero by A26,A27,A28,Lm20;
A44: w29 is not zero by A30,A31,A32,Lm20;
A45: are_Prop w2,w29 by A31,A32,Lm16;
then
A46: u,w29,v1 are_LinDep by A9,ANPROJ_1:4;
A47: are_Prop v,v9 by A39,A40,Lm16;
then
A48: v9,w29,u1 are_LinDep by A11,A45,ANPROJ_1:4;
A49: are_Prop v2,v29 by A35,A37,Lm16;
then
A50: u,v29,w1 are_LinDep by A7,ANPROJ_1:4;
A51: are_Prop w,w9 by A27,A28,Lm16;
then
A52: w9,v29,u1 are_LinDep by A12,A49,ANPROJ_1:4;
not are_Prop u,v2
proof
assume not thesis;
then o,u2,u are_LinDep by A17,ANPROJ_1:4;
hence contradiction by A24,ANPROJ_1:5;
end;
then not are_Prop u,v29 by A35,A37,Lm17;
then consider A3,B3 being Real such that
A53: w1 = A3*u + B3*v29 by A13,A50,A41,ANPROJ_1:6;
not o,u2,v are_LinDep
proof
assume not thesis;
then
A54: o,v,u2 are_LinDep by ANPROJ_1:5;
o,v,u are_LinDep & o,v,o are_LinDep by A33,ANPROJ_1:5,11;
hence contradiction by A1,A38,A24,A15,A54,ANPROJ_1:14;
end;
then not are_Prop v,w2 by A23,ANPROJ_1:4;
then not are_Prop v9,w29 by A39,A40,A31,A32,Lm21;
then consider A1,B1 being Real such that
A55: u1 = A1*v9 + B1*w29 by A42,A44,A48,ANPROJ_1:6;
not o,u,v2 are_LinDep
proof
assume not thesis;
then
A56: o,v2,u are_LinDep by ANPROJ_1:5;
o,v2,u2 are_LinDep & o,v2,o are_LinDep by A17,ANPROJ_1:5,11;
hence contradiction by A1,A34,A24,A22,A56,ANPROJ_1:14;
end;
then not are_Prop v2,w by A21,ANPROJ_1:4;
then not are_Prop w9,v29 by A27,A28,A35,A37,Lm21;
then consider A19,B19 being Real such that
A57: u1 = A19*w9 + B19*v29 by A41,A43,A52,ANPROJ_1:6;
A58: u1 = (A1 + B1)*o + (A1*a2)*u + (B1*c3)*u2 by A55,Lm22;
A59: not are_Prop v2,w2 by A6;
A60: not are_Prop v,w by A6;
A61: not are_Prop v9,w9 & not are_Prop v29,w29
proof
A62: now
assume are_Prop v29,w29;
then are_Prop v2,w29 by A49,ANPROJ_1:2;
hence contradiction by A59,A45,ANPROJ_1:2;
end;
A63: now
assume are_Prop v9,w9;
then are_Prop v,w9 by A47,ANPROJ_1:2;
hence contradiction by A60,A51,ANPROJ_1:2;
end;
assume not thesis;
hence contradiction by A63,A62;
end;
not are_Prop u,w2
proof
assume not thesis;
then o,u2,u are_LinDep by A23,ANPROJ_1:4;
hence contradiction by A24,ANPROJ_1:5;
end;
then not are_Prop u,w29 by A31,A32,Lm17;
then consider A2,B2 being Real such that
A64: v1 = A2*u + B2*w29 by A13,A44,A46,ANPROJ_1:6;
u2,w,v1 are_LinDep by A10;
then
A65: u2,w9,v1 are_LinDep by A51,ANPROJ_1:4;
not are_Prop u2,w by A24,A21,ANPROJ_1:4;
then not are_Prop u2,w9 by A27,A28,Lm17;
then consider A29,B29 being Real such that
A66: v1 = A29*u2 + B29*w9 by A19,A43,A65,ANPROJ_1:6;
A67: v1 = B2*o + A2*u + (B2*c3)*u2 by A64,Lm18;
A68: u2,v9,w1 are_LinDep by A8,A47,ANPROJ_1:4;
not are_Prop u2,v by A24,A33,ANPROJ_1:4;
then not are_Prop u2,v9 by A39,A40,Lm17;
then consider A39,B39 being Real such that
A69: w1 = A39*u2 + B39*v9 by A19,A68,A42,ANPROJ_1:6;
A70: w1 = B3*o + A3*u + (B3*c2)*u2 by A53,Lm18;
v1 = B29*o + (B29*a3)*u + A29*u2 by A66,Lm19;
then
A71: B2 = B29 & A2 = B29*a3 by A24,A67,ANPROJ_1:8;
w1 = B39*o + (B39*a2)*u + A39*u2 by A69,Lm19;
then
A72: B3 = B39 & A3 = B39*a2 by A24,A70,ANPROJ_1:8;
A73: u1 = (A19 + B19)*o + (A19*a3)*u + (B19*c2)*u2 by A57,Lm22;
then
A74: B1*c3 = B19*c2 by A24,A58,ANPROJ_1:8;
A1 + B1 = A19 + B19 & A1*a2 = A19*a3 by A24,A58,A73,ANPROJ_1:8;
then
A75: A1 = (a3*c3 - a3*c2)*(a3*c2 - a2*c2)"*B1 by A36,A61,A74,Lm24;
set v19 = o + a3*u + c3*u2;
set C2 = a2*c2, C3 = -(a3* c3);
set u19 = (a3*c3 - a2*c2)*o + ((a2*a3)*(c3 - c2))*u + ((c2*c3)*(a3 - a2))*u2;
set w19 = o + a2*u + c2*u2;
A76: C2*c3 + C3*c2 = (c2*c3)*(a2 - a3);
C2 + C3 = a2*c2 - a3*c3 & C2*a3 + C3*a2 = (a2*a3)*(c2 - c3);
then 1*u19 + C2*v19 + C3*w19 = 0.V by A76,Lm28;
then
A77: u19,v19,w19 are_LinDep;
A78: v1 is not zero by A4;
A79: B2 <> 0
proof
assume not thesis;
then v1 = 0.V + 0*w29 by A64,A71,RLVECT_1:10
.= 0.V + 0.V by RLVECT_1:10
.= 0.V by RLVECT_1:4;
hence contradiction by A78;
end;
v1 = B2*v19 by A67,A71,Lm29;
then
A80: are_Prop v19,v1 by A79,Lm16;
A81: w1 is not zero by A4;
A82: B3 <> 0
proof
assume not thesis;
then w1 = 0.V + 0*v29 by A53,A72,RLVECT_1:10
.= 0.V + 0.V by RLVECT_1:10
.= 0.V by RLVECT_1:4;
hence contradiction by A81;
end;
w1 = B3*w19 by A70,A72,Lm29;
then
A83: are_Prop w19,w1 by A82,Lm16;
A84: u1 is not zero by A4;
A85: B1<>0
proof
assume not thesis;
then u1 = 0.V + 0*w29 by A55,A75,RLVECT_1:10
.= 0.V + 0.V by RLVECT_1:10
.= 0.V by RLVECT_1:4;
hence contradiction by A84;
end;
u1 = (B1*(a3*c2 - a2*c2)")*((a3*c3 - a2*c2)*o + ((a2*a3)*(c3 - c2))*u
+ ((c2*c3)*(a3 - a2))*u2) by A36,A61,A58,A75,Lm26;
then are_Prop u19,u1 by A36,A61,A85,Lm16,Lm25;
hence thesis by A83,A80,A77,ANPROJ_1:4;
end;
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 Th10:
ex f st f.x1 = 1 & for z st z in A & z<>x1 holds f.z = 0
proof
deffunc G(object) = In(0,REAL);
deffunc F(object) = 1;
defpred P[object] means $1 = x1;
A1: for z being object st z in A
holds (P[z] implies F(z) in REAL) & (not P[z] implies G(
z) in REAL) by XREAL_0:def 1;
consider f being Function of A,REAL such that
A2: for z being object st z in A
holds (P[z] implies f.z = F(z)) & (not P[z] implies
f.z = G(z)) from FUNCT_2:sch 5(A1);
reconsider f as Element of Funcs(A,REAL) by FUNCT_2:8;
take f;
thus thesis by A2;
end;
theorem Th11:
x1<>x2 & x1<>x3 & x2<>x3 & f.x1 = 1 & (for z st z in A holds(z<>
x1 implies f.z = 0)) & g.x2 = 1 & (for z st z in A holds(z<>x2 implies g.z = 0)
) & h.x3 = 1 & (for z st z in A holds(z<>x3 implies h.z = 0)) implies
for a,b,c being Real
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
proof
set RM = RealFuncExtMult(A), RA = RealFuncAdd(A);
assume that
A1: x1<>x2 and
A2: x1<>x3 and
A3: x2<>x3 and
A4: f.x1 = 1 and
A5: for z st z in A holds(z<>x1 implies f.z = 0) and
A6: g.x2 = 1 and
A7: for z st z in A holds(z<>x2 implies g.z = 0) and
A8: h.x3 = 1 and
A9: for z st z in A holds(z<>x3 implies h.z = 0);
A10: f.x2=0 & h.x2=0 by A1,A3,A5,A9;
let a,b,c be Real;
assume
A11: RA.(RA.(RM.[a,f],RM.[b,g]),RM.[c,h]) = RealFuncZero(A);
reconsider a,b,c as Element of REAL by XREAL_0:def 1;
A12: 0 = (RA.(RA.(RM.[a,f],RM.[b,g]), RM.[c,h])).x2 by FUNCOP_1:7,A11
.= (RA.(RM.[a,f],RM.[b,g])).x2 + (RM.[c,h]).x2 by FUNCSDOM:1
.= ((RM.[a,f]).x2) + ((RM.[b,g]).x2) + (RM.[c,h]).x2 by FUNCSDOM:1
.= ((RM.[a,f]).x2) + ((RM.[b,g]).x2) + c*(h.x2) by FUNCSDOM:4
.= ((RM.[a,f]).x2) + b*(g.x2) + c*(h.x2) by FUNCSDOM:4
.= a*0 + b*1 + c*0 by A6,A10,FUNCSDOM:4
.= b;
A13: g.x1=0 & h.x1=0 by A1,A2,A7,A9;
A14: f.x3=0 & g.x3=0 by A2,A3,A5,A7;
A15: 0 = (RA.(RA.(RM.[a,f],RM.[b,g]), RM.[c,h])).x3 by A11,FUNCOP_1:7
.= (RA.(RM.[a,f],RM.[b,g])).x3 + (RM.[c,h]).x3 by FUNCSDOM:1
.= ((RM.[a,f]).x3) + ((RM.[b,g]).x3) + (RM.[c,h]).x3 by FUNCSDOM:1
.= ((RM.[a,f]).x3) + ((RM.[b,g]).x3) + c*(h.x3) by FUNCSDOM:4
.= ((RM.[a,f]).x3) + b*(g.x3) + c*(h.x3) by FUNCSDOM:4
.= a*0 + b*0 + c*1 by A8,A14,FUNCSDOM:4
.= c;
0 = (RA.(RA.(RM.[a,f],RM.[b,g]),RM.[c,h])).x1 by A11,FUNCOP_1:7
.= (RA.(RM.[a,f],RM.[b,g])).x1 + (RM.[c,h]).x1 by FUNCSDOM:1
.= ((RM.[a,f]).x1) + ((RM.[b,g]).x1) + (RM.[c,h]).x1 by FUNCSDOM:1
.= ((RM.[a,f]).x1) + ((RM.[b,g]).x1) + c*(h.x1) by FUNCSDOM:4
.= ((RM.[a,f]).x1) + b*(g.x1) + c*(h.x1) by FUNCSDOM:4
.= a*1 + b*0 + c*0 by A4,A13,FUNCSDOM:4
.= a;
hence thesis by A12,A15;
end;
theorem
x1<>x2 & x1<>x3 & x2<>x3 implies ex f,g,h st
for a,b,c being Real 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
proof
assume
A1: x1<>x2 & x1<>x3 & x2<>x3;
consider f such that
A2: f.x1 = 1 & for z st z in A holds (z<>x1 implies f.z = 0) by Th10;
consider h such that
A3: h.x3 = 1 & for z st z in A holds(z<>x3 implies h.z = 0) by Th10;
consider g such that
A4: g.x2 = 1 & for z st z in A holds(z<>x2 implies g.z = 0) by Th10;
take f,g,h;
let a,b,c be Real;
assume (RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(
RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h]) = RealFuncZero(A);
hence thesis by A1,A2,A4,A3,Th11;
end;
theorem Th13:
A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3 & f.x1 = 1 & (for z st
z in A holds (z<>x1 implies f.z = 0)) & g.x2 = 1 & (for z st z in A holds (z<>
x2 implies g.z = 0)) & h.x3 = 1 & (for z st z in A holds (z<>x3 implies h.z = 0
)) implies for h9 being Element of Funcs(A,REAL) holds
ex a,b,c being Real st h9 = (
RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult
(A)).[b,g]), (RealFuncExtMult(A)).[c,h])
proof
assume that
A1: A = {x1,x2,x3} and
A2: x1<>x2 and
A3: x1<>x3 and
A4: x2<>x3 and
A5: f.x1 = 1 and
A6: for z st z in A holds(z<>x1 implies f.z = 0) and
A7: g.x2 = 1 and
A8: for z st z in A holds(z<>x2 implies g.z = 0) and
A9: h.x3 = 1 and
A10: for z st z in A holds(z<>x3 implies h.z = 0);
A11: g.x1=0 & h.x1=0 by A2,A3,A8,A10;
A12: f.x2=0 & h.x2=0 by A2,A4,A6,A10;
let h9 be Element of Funcs(A,REAL);
take a = h9.x1, b = h9.x2, c = h9.x3;
A13: f.x3=0 & g.x3=0 by A3,A4,A6,A8;
now
let x be Element of A;
A14: x = x1 or x = x2 or x = x3 by A1,ENUMSET1:def 1;
A15: ((RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(
RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h])).x2 = ((RealFuncAdd(A))
. ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g])).x2 + ((
RealFuncExtMult(A)).[c,h]).x2 by FUNCSDOM:1
.= (((RealFuncExtMult(A)).[a,f]).x2) + (((RealFuncExtMult(A)).[b,g]).
x2) + ((RealFuncExtMult(A)).[c,h]).x2 by FUNCSDOM:1
.= (((RealFuncExtMult(A)).[a,f]).x2) + (((RealFuncExtMult(A)).[b,g]).
x2) + c*(h.x2) by FUNCSDOM:4
.= (((RealFuncExtMult(A)).[a,f]).x2) + b*(g.x2) + c*(h.x2) by FUNCSDOM:4
.= a*0 + b*1 + c*0 by A7,A12,FUNCSDOM:4
.= h9.x2;
A16: ((RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(
RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h])).x3 = ((RealFuncAdd(A))
. ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g])).x3 + ((
RealFuncExtMult(A)).[c,h]).x3 by FUNCSDOM:1
.= (((RealFuncExtMult(A)).[a,f]).x3) + (((RealFuncExtMult(A)).[b,g]).
x3) + ((RealFuncExtMult(A)).[c,h]).x3 by FUNCSDOM:1
.= (((RealFuncExtMult(A)).[a,f]).x3) + (((RealFuncExtMult(A)).[b,g]).
x3) + c*(h.x3) by FUNCSDOM:4
.= (((RealFuncExtMult(A)).[a,f]).x3) + b*(g.x3) + c*(h.x3) by FUNCSDOM:4
.= a*0 + b*0 + c*1 by A9,A13,FUNCSDOM:4
.= h9.x3;
((RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(
RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h])).x1 = ((RealFuncAdd(A))
. ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g])).x1 + ((
RealFuncExtMult(A)).[c,h]).x1 by FUNCSDOM:1
.= (((RealFuncExtMult(A)).[a,f]).x1) + (((RealFuncExtMult(A)).[b,g]).
x1) + ((RealFuncExtMult(A)).[c,h]).x1 by FUNCSDOM:1
.= (((RealFuncExtMult(A)).[a,f]).x1) + (((RealFuncExtMult(A)).[b,g]).
x1) + c*(h.x1) by FUNCSDOM:4
.= (((RealFuncExtMult(A)).[a,f]).x1) + b*(g.x1) + c*(h.x1) by FUNCSDOM:4
.= a*1 + b*0 + c*0 by A5,A11,FUNCSDOM:4
.= h9.x1;
hence
h9.x = ((RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,
f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h])).x by A14,A15
,A16;
end;
hence thesis by FUNCT_2:63;
end;
theorem
A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3 implies ex f,g,h st for h9
being Element of Funcs(A,REAL)
ex a,b,c being Real st h9 = (RealFuncAdd(A)).((
RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (
RealFuncExtMult(A)).[c,h])
proof
assume
A1: A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3;
consider f such that
A2: f.x1 = 1 & for z st z in A holds(z<>x1 implies f.z =0) by Th10;
consider h such that
A3: h.x3 = 1 & for z st z in A holds(z<>x3 implies h.z = 0) by Th10;
consider g such that
A4: g.x2 = 1 & for z st z in A holds(z<>x2 implies g.z = 0) by Th10;
take f,g,h;
let h9 be Element of Funcs(A,REAL);
thus thesis by A1,A2,A4,A3,Th13;
end;
theorem Th15:
A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3 implies ex f,g,h st (
for a,b,c being Real
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 h9 being Element of Funcs(A,REAL)
ex a,b,c being Real st h9
= (RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(
RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h])
proof
assume
A1: A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3;
consider f such that
A2: f.x1 = 1 & for z st z in A holds(z<>x1 implies f.z =0) by Th10;
consider h such that
A3: h.x3 = 1 & for z st z in A holds(z<>x3 implies h.z = 0) by Th10;
consider g such that
A4: g.x2 = 1 & for z st z in A holds(z<>x2 implies g.z = 0) by Th10;
take f,g,h;
thus thesis by A1,A2,A4,A3,Th11,Th13;
end;
Lm30: ex A,x1,x2,x3 st A={x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3
proof
reconsider A={0,1,2} as non empty set;
take A;
reconsider x1=0,x2=1,x3=2 as Element of A by ENUMSET1:def 1;
take x1,x2,x3;
thus thesis;
end;
theorem Th16:
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
proof
consider A,x1,x2,x3 such that
A1: A={x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3 by Lm30;
set V = RealVectSpace(A);
consider f,g,h such that
A2: for a,b,c being Real
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 and
A3: for h9 being Element of Funcs(A,REAL)
ex a,b,c being Real st h9 = (
RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult
(A)).[b,g]), (RealFuncExtMult(A)).[c,h]) by A1,Th15;
reconsider u=f, v=g, w = h as Element of V;
for a,b,c st a*u + b*v + c*w = 0.V holds a=0 & b=0 & c = 0
by A2;
then u is not zero by Th1;
then
A4: u <> 0.V;
A5: for y being Element of V ex a,b,c st y = a*u + b*v + c*w
proof
let y be Element of V;
reconsider h9=y as Element of Funcs(A,REAL);
consider a,b,c being Real such that
A6: h9 = (RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,
f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h]) by A3;
h9 = a*u + b*v + c*w by A6;
hence thesis;
end;
reconsider V as non trivial RealLinearSpace by A4,STRUCT_0:def 18;
take V;
reconsider u,v,w as Element of V;
take u,v,w;
thus for a,b,c st a*u + b*v + c*w = 0.V holds a=0 & b=0 & c = 0
by A2;
let y be Element of V;
ex a,b,c st y = a*u + b*v + c*w by A5;
hence thesis;
end;
theorem Th17:
x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4 & f.x1 = 1 &
(for z st z in A holds(z<>x1 implies f.z = 0)) & g.x2 = 1 & (for z st z in A
holds(z<>x2 implies g.z = 0)) & h.x3 = 1 & (for z st z in A holds(z<>x3 implies
h.z = 0)) & f1.x4 = 1 & (for z st z in A holds(z<>x4 implies f1.z = 0)) implies
for a,b,c,d being Real
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
proof
set RM = RealFuncExtMult(A), RA = RealFuncAdd(A);
assume that
A1: x1<>x2 and
A2: x1<>x3 and
A3: x1<>x4 and
A4: x2<>x3 and
A5: x2<>x4 and
A6: x3<>x4 and
A7: f.x1 = 1 and
A8: for z st z in A holds(z<>x1 implies f.z = 0) and
A9: g.x2 = 1 and
A10: for z st z in A holds(z<>x2 implies g.z = 0) and
A11: h.x3 = 1 and
A12: for z st z in A holds(z<>x3 implies h.z = 0) and
A13: f1.x4 = 1 and
A14: for z st z in A holds(z<>x4 implies f1.z = 0);
A15: f.x2=0 & h.x2=0 by A1,A4,A8,A12;
A16: g.x1=0 & h.x1=0 by A1,A2,A10,A12;
A17: f1.x1=0 by A3,A14;
A18: f1.x2=0 by A5,A14;
let a,b,c,d be Real;
assume
A19: RA.(RA.(RA.(RM.[a,f],RM.[b,g]),RM.[c,h]),RM.[d,f1]) = RealFuncZero( A);
reconsider a,b,c,d as Element of REAL by XREAL_0:def 1;
A20: 0 = (RA.(RA.(RA.(RM.[a,f],RM.[b,g]),RM.[c,h]),RM.[d,f1])).x2
by FUNCOP_1:7,A19
.= (RA.(RA.(RM.[a,f],RM.[b,g]),RM.[c,h])).x2 + (RM.[d,f1]).x2 by FUNCSDOM:1
.= (RA.(RM.[a,f],RM.[b,g])).x2 + (RM.[c,h]).x2 + (RM.[d,f1]).x2 by
FUNCSDOM:1
.= (RM.[a,f]).x2 + (RM.[b,g]).x2 + (RM.[c,h]).x2 + (RM.[d,f1]).x2 by
FUNCSDOM:1
.= (RM.[a,f]).x2 + (RM.[b,g]).x2 + (RM.[c,h]).x2 + d*(f1.x2) by FUNCSDOM:4
.= (RM.[a,f]).x2 + (RM.[b,g]).x2 + c*(h.x2) + d*(f1.x2) by FUNCSDOM:4
.= (RM.[a,f]).x2 + b*(g.x2) + c*(h.x2) + d*(f1.x2) by FUNCSDOM:4
.= a*0 + b*1 + c*0 + d*0 by A9,A15,A18,FUNCSDOM:4
.= b;
A21: f.x4=0 & g.x4=0 by A3,A5,A8,A10;
A22: h.x4=0 by A6,A12;
A23: f.x3=0 & g.x3=0 by A2,A4,A8,A10;
A24: f1.x3=0 by A6,A14;
A25: 0 = (RA.(RA.(RA.(RM.[a,f],RM.[b,g]),RM.[c,h]),RM.[d,f1])).x4 by A19,
FUNCOP_1:7
.= (RA.(RA.(RM.[a,f],RM.[b,g]),RM.[c,h])).x4 + (RM.[d,f1]).x4 by FUNCSDOM:1
.= (RA.(RM.[a,f], RM.[b,g])).x4 + (RM.[c,h]).x4 + (RM.[d,f1]).x4 by
FUNCSDOM:1
.= (RM.[a,f]).x4 + (RM.[b,g]).x4 + (RM.[c,h]).x4 + (RM.[d,f1]).x4 by
FUNCSDOM:1
.= (RM.[a,f]).x4 + (RM.[b,g]).x4 + (RM.[c,h]).x4 + d*(f1.x4) by FUNCSDOM:4
.= (RM.[a,f]).x4 + (RM.[b,g]).x4 + c*(h.x4) + d*(f1.x4) by FUNCSDOM:4
.= (RM.[a,f]).x4 + b*(g.x4) + c*(h.x4) + d*(f1.x4) by FUNCSDOM:4
.= a*0 + b*0 + c*0 + d*1 by A13,A21,A22,FUNCSDOM:4
.= d;
A26: 0 = (RA.(RA.(RA.(RM.[a,f],RM.[b,g]),RM.[c,h]),RM.[d,f1])).x3 by A19,
FUNCOP_1:7
.= (RA.(RA.(RM.[a,f], RM.[b,g]),RM.[c,h])).x3 + (RM.[d,f1]).x3 by
FUNCSDOM:1
.= (RA.(RM.[a,f],RM.[b,g])).x3 + (RM.[c,h]).x3 + (RM.[d,f1]).x3 by
FUNCSDOM:1
.= (RM.[a,f]).x3 + (RM.[b,g]).x3 + (RM.[c,h]).x3 + (RM.[d,f1]).x3 by
FUNCSDOM:1
.= (RM.[a,f]).x3 + (RM.[b,g]).x3 + (RM.[c,h]).x3 + d*(f1.x3) by FUNCSDOM:4
.= (RM.[a,f]).x3 + (RM.[b,g]).x3 + c*(h.x3) + d*(f1.x3) by FUNCSDOM:4
.= (RM.[a,f]).x3 + b*(g.x3) + c*(h.x3) + d*(f1.x3) by FUNCSDOM:4
.= a*0 + b*0 + c*1 + d*0 by A11,A23,A24,FUNCSDOM:4
.= c;
0 = (RA.(RA.(RA.(RM.[a,f],RM.[b,g]),RM.[c,h]),RM.[d,f1])).x1 by A19,
FUNCOP_1:7
.= (RA.(RA.(RM.[a,f],RM.[b,g]),RM.[c,h])).x1 + (RM.[d,f1]).x1 by FUNCSDOM:1
.= (RA.(RM.[a,f],RM.[b,g])).x1 + (RM.[c,h]).x1 + (RM.[d,f1]).x1 by
FUNCSDOM:1
.= (RM.[a,f]).x1 + (RM.[b,g]).x1 + (RM.[c,h]).x1 + (RM.[d,f1]).x1 by
FUNCSDOM:1
.= (RM.[a,f]).x1 + (RM.[b,g]).x1 + (RM.[c,h]).x1 + d*(f1.x1) by FUNCSDOM:4
.= (RM.[a,f]).x1 + (RM.[b,g]).x1 + c*(h.x1) + d*(f1.x1) by FUNCSDOM:4
.= (RM.[a,f]).x1 + b*(g.x1) + c*(h.x1) + d*(f1.x1) by FUNCSDOM:4
.= a*1 + b*0 + c*0 + d*0 by A7,A16,A17,FUNCSDOM:4
.= a;
hence thesis by A20,A26,A25;
end;
theorem
x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4 implies ex f,g,h,
f1 st for a,b,c,d being Real
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
proof
assume
A1: x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4;
consider f such that
A2: f.x1 = 1 & for z st z in A holds(z<>x1 implies f.z = 0) by Th10;
consider f1 such that
A3: f1.x4 = 1 & for z st z in A holds(z<>x4 implies f1.z = 0) by Th10;
consider h such that
A4: h.x3 = 1 & for z st z in A holds(z<>x3 implies h.z = 0) by Th10;
consider g such that
A5: g.x2 = 1 & for z st z in A holds(z<>x2 implies g.z = 0) by Th10;
take f,g,h,f1;
let a,b,c,d be Real;
assume (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((
RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,
h]),(RealFuncExtMult(A)).[d,f1]) = RealFuncZero(A);
hence thesis by A1,A2,A5,A4,A3,Th17;
end;
theorem Th19:
A = {x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 &
x3<>x4 & f.x1 = 1 & (for z st z in A holds(z<>x1 implies f.z = 0)) & g.x2 = 1 &
(for z st z in A holds(z<>x2 implies g.z = 0)) & h.x3 = 1 & (for z st z in A
holds(z<>x3 implies h.z = 0)) & f1.x4 = 1 & (for z st z in A holds(z<>x4
implies f1.z = 0)) implies for h9 being Element of Funcs(A,REAL)
ex a,b,c ,d being Real
st h9 = (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((
RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,
h]),(RealFuncExtMult(A)).[d,f1])
proof
assume that
A1: A = {x1,x2,x3,x4} and
A2: x1<>x2 and
A3: x1<>x3 and
A4: x1<>x4 and
A5: x2<>x3 and
A6: x2<>x4 and
A7: x3<>x4 and
A8: f.x1 = 1 and
A9: for z st z in A holds(z<>x1 implies f.z = 0) and
A10: g.x2 = 1 and
A11: for z st z in A holds(z<>x2 implies g.z = 0) and
A12: h.x3 = 1 and
A13: for z st z in A holds(z<>x3 implies h.z = 0) and
A14: f1.x4 = 1 and
A15: for z st z in A holds(z<>x4 implies f1.z = 0);
A16: f.x4=0 & g.x4=0 by A4,A6,A9,A11;
A17: f1.x3=0 by A7,A15;
A18: f1.x2=0 by A6,A15;
A19: f.x2=0 & h.x2=0 by A2,A5,A9,A13;
A20: f1.x1=0 by A4,A15;
A21: g.x1=0 & h.x1=0 by A2,A3,A11,A13;
A22: h.x4=0 by A7,A13;
let h9 be Element of Funcs(A,REAL);
take a = h9.x1, b = h9.x2, c = h9.x3, d = h9.x4;
A23: f.x3=0 & g.x3=0 by A3,A5,A9,A11;
now
let x be Element of A;
A24: x = x1 or x = x2 or x = x3 or x = x4 by A1,ENUMSET1:def 2;
A25: ((RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((
RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,
h]),(RealFuncExtMult(A)).[d,f1])).x2 = ((RealFuncAdd(A)).((RealFuncAdd(A)).((
RealFuncExtMult(A)).[a,f], (RealFuncExtMult(A)).[b,g]),(RealFuncExtMult(A)).[c,
h])).x2 + ((RealFuncExtMult(A)).[d,f1]).x2 by FUNCSDOM:1
.= ((RealFuncAdd(A)).((RealFuncExtMult(A)).[a,f], (RealFuncExtMult(A))
.[b,g])).x2 + ((RealFuncExtMult(A)).[c,h]).x2 + ((RealFuncExtMult(A)).[d,f1]).
x2 by FUNCSDOM:1
.= ((RealFuncExtMult(A)).[a,f]).x2 + ((RealFuncExtMult(A)).[b,g]).x2 +
((RealFuncExtMult(A)).[c,h]).x2 + ((RealFuncExtMult(A)).[d,f1]).x2 by
FUNCSDOM:1
.= ((RealFuncExtMult(A)).[a,f]).x2 + ((RealFuncExtMult(A)).[b,g]).x2 +
((RealFuncExtMult(A)).[c,h]).x2 + d*(f1.x2) by FUNCSDOM:4
.= ((RealFuncExtMult(A)).[a,f]).x2 + ((RealFuncExtMult(A)).[b,g]).x2 +
c*(h.x2) + d*(f1.x2) by FUNCSDOM:4
.= ((RealFuncExtMult(A)).[a,f]).x2 + b*(g.x2) + c*(h.x2) + d*(f1.x2)
by FUNCSDOM:4
.= a*0 + b*1 + c*0 + d*0 by A10,A19,A18,FUNCSDOM:4
.= h9.x2;
A26: ((RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((
RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,
h]),(RealFuncExtMult(A)).[d,f1])).x4 = ((RealFuncAdd(A)).((RealFuncAdd(A)).((
RealFuncExtMult(A)).[a,f], (RealFuncExtMult(A)).[b,g]),(RealFuncExtMult(A)).[c,
h])).x4 + ((RealFuncExtMult(A)).[d,f1]).x4 by FUNCSDOM:1
.= ((RealFuncAdd(A)).((RealFuncExtMult(A)).[a,f], (RealFuncExtMult(A))
.[b,g])).x4 + ((RealFuncExtMult(A)).[c,h]).x4 + ((RealFuncExtMult(A)).[d,f1]).
x4 by FUNCSDOM:1
.= ((RealFuncExtMult(A)).[a,f]).x4 + ((RealFuncExtMult(A)).[b,g]).x4 +
((RealFuncExtMult(A)).[c,h]).x4 + ((RealFuncExtMult(A)).[d,f1]).x4 by
FUNCSDOM:1
.= ((RealFuncExtMult(A)).[a,f]).x4 + ((RealFuncExtMult(A)).[b,g]).x4 +
((RealFuncExtMult(A)).[c,h]).x4 + d*(f1.x4) by FUNCSDOM:4
.= ((RealFuncExtMult(A)).[a,f]).x4 + ((RealFuncExtMult(A)).[b,g]).x4 +
c*(h.x4) + d*(f1.x4) by FUNCSDOM:4
.= ((RealFuncExtMult(A)).[a,f]).x4 + b*(g.x4) + c*(h.x4) + d*(f1.x4)
by FUNCSDOM:4
.= a*0 + b*0 + c*0 + d*1 by A14,A16,A22,FUNCSDOM:4
.= h9.x4;
A27: ((RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((
RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,
h]),(RealFuncExtMult(A)).[d,f1])).x3 = ((RealFuncAdd(A)).((RealFuncAdd(A)).((
RealFuncExtMult(A)).[a,f], (RealFuncExtMult(A)).[b,g]),(RealFuncExtMult(A)).[c,
h])).x3 + ((RealFuncExtMult(A)).[d,f1]).x3 by FUNCSDOM:1
.= ((RealFuncAdd(A)).((RealFuncExtMult(A)).[a,f], (RealFuncExtMult(A))
.[b,g])).x3 + ((RealFuncExtMult(A)).[c,h]).x3 + ((RealFuncExtMult(A)).[d,f1]).
x3 by FUNCSDOM:1
.= ((RealFuncExtMult(A)).[a,f]).x3 + ((RealFuncExtMult(A)).[b,g]).x3 +
((RealFuncExtMult(A)).[c,h]).x3 + ((RealFuncExtMult(A)).[d,f1]).x3 by
FUNCSDOM:1
.= ((RealFuncExtMult(A)).[a,f]).x3 + ((RealFuncExtMult(A)).[b,g]).x3 +
((RealFuncExtMult(A)).[c,h]).x3 + d*(f1.x3) by FUNCSDOM:4
.= ((RealFuncExtMult(A)).[a,f]).x3 + ((RealFuncExtMult(A)).[b,g]).x3 +
c*(h.x3) + d*(f1.x3) by FUNCSDOM:4
.= ((RealFuncExtMult(A)).[a,f]).x3 + b*(g.x3) + c*(h.x3) + d*(f1.x3)
by FUNCSDOM:4
.= a*0 + b*0 + c*1 + d*0 by A12,A23,A17,FUNCSDOM:4
.= h9.x3;
((RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((
RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,
h]),(RealFuncExtMult(A)).[d,f1])).x1 = ((RealFuncAdd(A)).((RealFuncAdd(A)).((
RealFuncExtMult(A)).[a,f], (RealFuncExtMult(A)).[b,g]),(RealFuncExtMult(A)).[c,
h])).x1 + ((RealFuncExtMult(A)).[d,f1]).x1 by FUNCSDOM:1
.= ((RealFuncAdd(A)).((RealFuncExtMult(A)).[a,f], (RealFuncExtMult(A))
.[b,g])).x1 + ((RealFuncExtMult(A)).[c,h]).x1 + ((RealFuncExtMult(A)).[d,f1]).
x1 by FUNCSDOM:1
.= ((RealFuncExtMult(A)).[a,f]).x1 + ((RealFuncExtMult(A)).[b,g]).x1 +
((RealFuncExtMult(A)).[c,h]).x1 + ((RealFuncExtMult(A)).[d,f1]).x1 by
FUNCSDOM:1
.= ((RealFuncExtMult(A)).[a,f]).x1 + ((RealFuncExtMult(A)).[b,g]).x1 +
((RealFuncExtMult(A)).[c,h]).x1 + d*(f1.x1) by FUNCSDOM:4
.= ((RealFuncExtMult(A)).[a,f]).x1 + ((RealFuncExtMult(A)).[b,g]).x1 +
c*(h.x1) + d*(f1.x1) by FUNCSDOM:4
.= ((RealFuncExtMult(A)).[a,f]).x1 + b*(g.x1) + c*(h.x1) + d*(f1.x1)
by FUNCSDOM:4
.= a*1 + b*0 + c*0 + d*0 by A8,A21,A20,FUNCSDOM:4
.= h9.x1;
hence h9.x = ((RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((
RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,
h]),(RealFuncExtMult(A)).[d,f1])).x by A24,A25,A27,A26;
end;
hence thesis by FUNCT_2:63;
end;
theorem
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 h9 being Element of Funcs(A,REAL)
ex a,b,c,d being Real
st h9 = (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((
RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,
h]),(RealFuncExtMult(A)).[d,f1])
proof
assume
A1: A = {x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3 <>x4;
consider f such that
A2: f.x1 = 1 & for z st z in A holds(z<>x1 implies f.z =0) by Th10;
consider f1 such that
A3: f1.x4 = 1 & for z st z in A holds(z<>x4 implies f1.z = 0) by Th10;
consider h such that
A4: h.x3 = 1 & for z st z in A holds(z<>x3 implies h.z = 0) by Th10;
consider g such that
A5: g.x2 = 1 & for z st z in A holds(z<>x2 implies g.z = 0) by Th10;
take f,g,h,f1;
let h9 be Element of Funcs(A,REAL);
thus thesis by A1,A2,A5,A4,A3,Th19;
end;
theorem Th21:
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 being Real 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 h9 being Element of Funcs(A,REAL)
ex a,b,c,d being Real
st h9 = (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((
RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,
h]),(RealFuncExtMult(A)).[d,f1])
proof
assume
A1: A = {x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3 <>x4;
consider f such that
A2: f.x1 = 1 & for z st z in A holds(z<>x1 implies f.z = 0) by Th10;
consider f1 such that
A3: f1.x4 = 1 & for z st z in A holds(z<>x4 implies f1.z = 0) by Th10;
consider h such that
A4: h.x3 = 1 & for z st z in A holds(z<>x3 implies h.z = 0) by Th10;
consider g such that
A5: g.x2 = 1 & for z st z in A holds(z<>x2 implies g.z = 0) by Th10;
take f,g,h,f1;
thus thesis by A1,A2,A5,A4,A3,Th17,Th19;
end;
Lm31: ex A,x1,x2,x3,x4 st A={x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3
& x2<>x4 & x3<>x4
proof
reconsider A={0,1,2,3} as non empty set;
take A;
reconsider x1=0,x2=1,x3=2,x4=3 as Element of A by ENUMSET1:def 2;
take x1,x2,x3,x4;
thus thesis;
end;
theorem Th22:
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
proof
consider A,x1,x2,x3,x4 such that
A1: A={x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3 <>
x4 by Lm31;
set V = RealVectSpace(A);
consider f,g,h,f1 such that
A2: for a,b,c,d being Real
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 and
A3: for h9 being Element of Funcs(A,REAL)
ex a,b,c,d being Real st h9 = (
RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f
],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h]),(RealFuncExtMult(A))
.[d,f1]) by A1,Th21;
reconsider u = f, v = g, w = h, u1 = f1 as Element of V;
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
by A2;
then u is not zero by Th2;
then
A4: u <> 0.V;
A5: for y being Element of V ex a,b,c,d st y = a*u + b*v + c*w + d*u1
proof
let y be Element of V;
reconsider h9=y as Element of Funcs(A,REAL);
consider a,b,c,d being Real such that
A6: h9 = (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). ((
RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,
h]),(RealFuncExtMult(A)).[d,f1]) by A3;
h9 = a * u + b*v + c*w + d*u1 by A6;
hence thesis;
end;
reconsider V as non trivial RealLinearSpace by A4,STRUCT_0:def 18;
take V;
reconsider u,v,w,u1 as Element of V;
take u,v,w,u1;
thus 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
by A2;
let y be Element of V;
ex a,b,c,d st y = a*u + b*v + c*w + d*u1 by A5;
hence thesis;
end;
definition
let IT be RealLinearSpace;
attr IT is up-3-dimensional means
:Def6:
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;
registration
cluster up-3-dimensional for RealLinearSpace;
existence by Th16,Def6;
end;
registration
cluster up-3-dimensional -> non trivial for RealLinearSpace;
coherence
proof
let V be RealLinearSpace;
given u,v,w1 being Element of V such that
A1: for a,b,c st a*u + b*v + c*w1 = 0.V holds a = 0 & b = 0 & c = 0;
now
assume w1 = 0.V;
then
A2: 0.V = 1*w1 by RLVECT_1:10;
0.V = 0*u & 0.V = 0*v by RLVECT_1:10;
then 0.V = 0*u + 0*v by RLVECT_1:4
.= 0*u + 0*v + 1*w1 by A2,RLVECT_1:4;
hence contradiction by A1;
end;
hence thesis;
end;
end;
definition
let CS be non empty CollStr;
redefine attr CS is reflexive means :: redefines reflexive (COLLSP, definition)
:Def7:
for p,q,r being Element of CS
holds p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear;
compatibility
proof
thus CS is reflexive implies
for p,q,r be Element of CS holds p,q,p are_collinear &
p,p,q are_collinear & p,q,q are_collinear;
assume
A1: for p,q,r being Element of CS holds p,q,p are_collinear & p,p,q
are_collinear & p,q,q are_collinear;
let p,q,r be Element of CS such that
A2: p=q or p=r or q=r;
per cases by A2;
suppose
p=q;
then p,q,r are_collinear by A1;
hence thesis;
end;
suppose
p=r;
then p,q,r are_collinear by A1;
hence thesis;
end;
suppose
q=r;
then p,q,r are_collinear by A1;
hence thesis;
end;
end;
redefine attr CS is transitive means :: redefines transitive (COLLSP, definition)
:Def8:
for p,q,r,r1,r2 being Element of CS st p
<>q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear
holds r,r1,r2 are_collinear;
compatibility
proof
thus CS is transitive implies
for p,q,r,r1,r2 be Element of CS st p<>q &
p,q,r are_collinear & p,q,r1 are_collinear &
p,q,r2 are_collinear holds r,r1,r2 are_collinear;
assume
A3: for p,q,r,r1,r2 being Element of CS st p<>q & p,q,r are_collinear
& p,q,r1 are_collinear & p,q,r2 are_collinear holds r,r1,r2 are_collinear;
let p,q,r,r1,r2 be Element of CS such that
A4: p<>q and
A5: [p,q,r] in the Collinearity of CS & [p,q,r1] in the Collinearity of CS and
A6: [p,q,r2] in the Collinearity of CS;
A7: p,q,r2 are_collinear by A6;
p,q,r are_collinear & p,q,r1 are_collinear by A5;
then r,r1,r2 are_collinear by A3,A4,A7;
hence thesis;
end;
end;
definition
let IT be non empty CollStr;
attr IT is Vebleian means
:Def9:
for p,p1,p2,r,r1 being Element of IT st p,
p1,r are_collinear & p1,p2,r1 are_collinear ex r2 being Element of IT
st p,p2,r2 are_collinear & r,r1,r2 are_collinear;
attr IT is at_least_3rank means
:Def10:
for p,q being Element of IT ex r
being Element of IT st p<>r & q<>r & p,q,r are_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 Th23:
p,q,r are_collinear iff ex u,v,w st p = Dir(u) & q = Dir(v) & r =
Dir(w) & u is not zero & v is not zero & w is not zero & u,v,w are_LinDep
by ANPROJ_1:24,ANPROJ_1:25;
Lm32: ProjectiveSpace(V) is reflexive
proof
let p,q;
consider u such that
A1: u is not zero & p = Dir(u) by ANPROJ_1:26;
consider v such that
A2: v is not zero & q = Dir(v) by ANPROJ_1:26;
A3: u,v,v are_LinDep by ANPROJ_1:11;
u,v,u are_LinDep & u,u,v are_LinDep by ANPROJ_1:11;
hence thesis by A1,A2,A3,Th23;
end;
Lm33: ProjectiveSpace(V) is transitive
proof
let p,q,r,r1,r2;
assume that
A1: p<>q and
A2: p,q,r are_collinear and
A3: p,q,r1 are_collinear and
A4: p,q,r2 are_collinear;
consider u1,v1,w1 such that
A5: p = Dir(u1) and
A6: q = Dir(v1) and
A7: r = Dir(w1) and
A8: u1 is not zero and
A9: v1 is not zero and
A10: w1 is not zero and
A11: u1,v1,w1 are_LinDep by A2,Th23;
consider v such that
A12: v is not zero and
A13: q = Dir(v) by ANPROJ_1:26;
A14: are_Prop v1,v by A12,A13,A6,A9,ANPROJ_1:22;
consider u3,v3,w3 being Element of V such that
A15: p = Dir(u3) and
A16: q = Dir(v3) and
A17: r2 = Dir(w3) and
A18: u3 is not zero and
A19: v3 is not zero and
A20: w3 is not zero and
A21: u3,v3,w3 are_LinDep by A4,Th23;
A22: are_Prop v3,v by A12,A13,A16,A19,ANPROJ_1:22;
consider u2,v2,w2 being Element of V such that
A23: p = Dir(u2) and
A24: q = Dir(v2) and
A25: r1 = Dir(w2) and
A26: u2 is not zero and
A27: v2 is not zero and
A28: w2 is not zero and
A29: u2,v2,w2 are_LinDep by A3,Th23;
A30: are_Prop v2,v by A12,A13,A24,A27,ANPROJ_1:22;
consider u such that
A31: u is not zero and
A32: p = Dir(u) by ANPROJ_1:26;
are_Prop u1,u by A31,A32,A5,A8,ANPROJ_1:22;
then
A33: u,v,w1 are_LinDep by A11,A14,ANPROJ_1:4;
are_Prop u3,u by A31,A32,A15,A18,ANPROJ_1:22;
then
A34: u,v,w3 are_LinDep by A21,A22,ANPROJ_1:4;
are_Prop u2,u by A31,A32,A23,A26,ANPROJ_1:22;
then
A35: u,v,w2 are_LinDep by A29,A30,ANPROJ_1:4;
not are_Prop u,v by A1,A31,A32,A12,A13,ANPROJ_1:22;
then w1,w2,w3 are_LinDep by A31,A12,A33,A35,A34,ANPROJ_1:14;
hence thesis by A7,A10,A25,A28,A17,A20,Th23;
end;
registration
let V;
cluster ProjectiveSpace V -> reflexive transitive;
coherence by Lm32,Lm33;
end;
theorem Th24:
p,q,r are_collinear implies p,r,q are_collinear & q,p,r
are_collinear & r,q,p are_collinear & r,p,q are_collinear &
q,r,p are_collinear
proof
assume p,q,r are_collinear;
then consider u,v,w such that
A1: p = Dir(u) & q = Dir(v) & r = Dir(w) & u is not zero & v is not zero
& w is not zero and
A2: u,v,w are_LinDep by Th23;
A3: w,v,u are_LinDep & w,u,v are_LinDep by A2,ANPROJ_1:5;
A4: v,w,u are_LinDep by A2,ANPROJ_1:5;
u,w,v are_LinDep & v,u,w are_LinDep by A2,ANPROJ_1:5;
hence thesis by A1,A3,A4,Th23;
end;
Lm34: p,p1,p2 are_collinear & p,p1,r are_collinear & p1,p2,r1 are_collinear
implies ex r2 st p,p2,r2 are_collinear & r,r1,r2 are_collinear
proof
assume that
A1: p,p1,p2 are_collinear and
A2: p,p1,r are_collinear and
A3: p1,p2,r1 are_collinear;
A4: now
A5: now
assume
A6: p1<>p;
take r;
A7: r,r1,r are_collinear by Def7;
p,p1,p are_collinear by Def7;
then p,p2,r are_collinear by A1,A2,A6,Def8;
hence thesis by A7;
end;
A8: now
assume
A9: p1<>p2;
take r1;
A10: r,r1,r1 are_collinear by Def7;
p1,p2,p are_collinear & p1,p2,p2 are_collinear by A1,Def7,Th24;
then p,p2,r1 are_collinear by A3,A9,Def8;
hence thesis by A10;
end;
assume p<>p2;
hence thesis by A5,A8;
end;
now
assume p=p2;
then
A11: p,p2,r are_collinear by Def7;
take r;
r,r1,r are_collinear by Def7;
hence thesis by A11;
end;
hence thesis by A4;
end;
Lm35: not p,p1,p2 are_collinear & p,p1,r are_collinear & p1,p2,r1 are_collinear
implies ex r2 st p,p2,r2 are_collinear & r,r1,r2 are_collinear
proof
assume that
A1: not p,p1,p2 are_collinear and
A2: p,p1,r are_collinear and
A3: p1,p2,r1 are_collinear;
consider u,v,t being Element of V such that
A4: p = Dir(u) and
A5: p1 = Dir(v) and
A6: r = Dir(t) and
A7: u is not zero and
A8: v is not zero and
A9: t is not zero and
A10: u,v,t are_LinDep by A2,Th23;
consider v1,w,s being Element of V such that
A11: p1 = Dir(v1) and
A12: p2 = Dir(w) and
A13: r1 = Dir(s) and
A14: v1 is not zero and
A15: w is not zero and
A16: s is not zero and
A17: v1,w,s are_LinDep by A3,Th23;
are_Prop v1,v by A5,A8,A11,A14,ANPROJ_1:22;
then
A18: v,w,s are_LinDep by A17,ANPROJ_1:4;
not u,v,w are_LinDep by A1,A4,A5,A7,A8,A12,A15,Th23;
then consider y such that
A19: u,w,y are_LinDep & t,s,y are_LinDep and
A20: y is not zero by A10,A18,ANPROJ_1:15;
reconsider r2 = Dir(y) as Element of ProjectiveSpace(V) by A20,ANPROJ_1:26;
take r2;
thus thesis by A4,A6,A7,A9,A12,A13,A15,A16,A19,A20,Th23;
end;
Lm36: ProjectiveSpace(V) is Vebleian
proof
let p,p1,p2,r,r1;
assume
A1: p,p1,r are_collinear & p1,p2,r1 are_collinear;
then p,p1,p2 are_collinear implies thesis by Lm34;
hence thesis by A1,Lm35;
end;
registration
let V;
cluster ProjectiveSpace(V) -> Vebleian;
coherence by Lm36;
end;
Lm37: V is up-3-dimensional implies ProjectiveSpace(V) is proper
proof
given u,v,w such that
A1: for a,b,c st a*u + b*v + c*w = 0.V holds a = 0 & b = 0 & c = 0;
A2: not u,v,w are_LinDep by A1;
A3: w is not zero by A1,Th1;
A4: u is not zero & v is not zero by A1,Th1;
then reconsider
p = Dir(u),q = Dir(v),r = Dir(w) as Element of ProjectiveSpace(V)
by A3,ANPROJ_1:26;
take p,q,r;
assume p,q,r are_collinear;
then [Dir(u),Dir(v),Dir(w)] in the Collinearity of ProjectiveSpace(V);
hence contradiction by A4,A3,A2,ANPROJ_1:25;
end;
registration
let V be up-3-dimensional RealLinearSpace;
cluster ProjectiveSpace(V) -> proper;
coherence by Lm37;
end;
theorem Th25:
(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
proof
given u,v such that
A1: for a,b st a*u + b*v = 0.V holds a = 0 & b = 0;
A2: not are_Prop u,v by A1,Lm1;
let p,q;
consider y such that
A3: y is not zero & p = Dir(y) by ANPROJ_1:26;
consider w such that
A4: w is not zero & q = Dir(w) by ANPROJ_1:26;
u is not zero & v is not zero by A1,Lm1;
then consider z being Element of V such that
A5: z is not zero and
A6: y,w,z are_LinDep and
A7: not are_Prop y,z and
A8: not are_Prop w,z by A2,ANPROJ_1:16;
reconsider r = Dir(z) as Element of ProjectiveSpace(V) by A5,ANPROJ_1:26;
take r;
thus p<>r by A3,A5,A7,ANPROJ_1:22;
thus q<>r by A4,A5,A8,ANPROJ_1:22;
thus thesis by A3,A4,A5,A6,Th23;
end;
Lm38: V is up-3-dimensional implies ProjectiveSpace(V) is at_least_3rank
proof
given u,v,w1 such that
A1: for a,b,c st a*u + b*v + c*w1 = 0.V holds a = 0 & b = 0 & c = 0;
now
let a,b;
assume a*u + b*v =0.V;
then 0.V = a*u + b*v + 0.V by RLVECT_1:4
.= a*u + b*v + 0*w1 by RLVECT_1:10;
hence a = 0 & b = 0 by A1;
end;
hence thesis by Th25;
end;
registration
let V be up-3-dimensional RealLinearSpace;
cluster ProjectiveSpace(V) -> at_least_3rank;
coherence by Lm38;
end;
registration
cluster transitive reflexive proper Vebleian at_least_3rank for non empty
CollStr;
existence
proof
set V0 = the up-3-dimensional RealLinearSpace;
take ProjectiveSpace(V0);
thus thesis;
end;
end;
definition
mode CollProjectiveSpace is reflexive transitive Vebleian at_least_3rank
proper non empty CollStr;
end;
definition
let IT be non empty CollStr;
attr IT is Fanoian means
for p1,r2,q,r1,q1,p,r being Element of IT
holds (p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear &
r2, q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear &
p,q,r are_collinear
implies (p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1,
q1 are_collinear or r2,r1,q1 are_collinear));
attr IT is Desarguesian means
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
are_collinear & not o,p1,p3 are_collinear & not o,p2,p3 are_collinear &
p1,p2,r3
are_collinear & q1,q2,r3 are_collinear & p2,p3,r1 are_collinear & q2,q3,r1
are_collinear & p1,p3,r2 are_collinear & q1,q3,r2 are_collinear & o,p1,q1
are_collinear & o,p2,q2 are_collinear & o,p3,q3 are_collinear holds r1,r2,r3
are_collinear;
attr IT is Pappian means
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 are_collinear & o,p1,p2 are_collinear & o,p1,p3
are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3
are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2
are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear holds
r1,r2,r3
are_collinear;
end;
definition
let IT be CollProjectiveSpace;
attr IT is 2-dimensional means
:Def14:
for p,p1,q,q1 being Element of IT ex
r being Element of IT st p,p1,r are_collinear & q,q1,r are_collinear;
end;
notation
let IT be CollProjectiveSpace;
antonym IT is up-3-dimensional for IT is 2-dimensional;
end;
definition
let IT be CollProjectiveSpace;
attr IT is at_most-3-dimensional means
for p,p1,q,q1,r2 being
Element of IT ex r,r1 being Element of IT st p,q,r are_collinear & p1,q1,r1
are_collinear & r2,r,r1 are_collinear;
end;
theorem Th26:
p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p
are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r
are_collinear & p,q,r are_collinear implies
(p1,r2,q1 are_collinear or p1,r2,r1
are_collinear or p1,r1,q1 are_collinear or r2,r1,q1 are_collinear)
proof
assume that
A1: p1,r2,q are_collinear and
A2: r1,q1,q are_collinear and
A3: p1,r1,p are_collinear and
A4: r2,q1,p are_collinear and
A5: p1,q1,r are_collinear and
A6: r2,r1,r are_collinear and
A7: p,q,r are_collinear;
consider u1,w1,x being Element of V such that
A8: p1 = Dir(u1) and
A9: r1 = Dir(w1) and
A10: p = Dir(x) and
A11: u1 is not zero and
A12: w1 is not zero and
A13: x is not zero and
A14: u1,w1,x are_LinDep by A3,Th23;
consider u,v,z being Element of V such that
A15: p1 = Dir(u) and
A16: r2 = Dir(v) and
A17: q = Dir(z) and
A18: u is not zero and
A19: v is not zero and
A20: z is not zero and
A21: u,v,z are_LinDep by A1,Th23;
consider w,y,z1 being Element of V such that
A22: r1 = Dir(w) and
A23: q1 = Dir(y) and
A24: q = Dir(z1) and
A25: w is not zero and
A26: y is not zero and
A27: z1 is not zero and
A28: w,y,z1 are_LinDep by A2,Th23;
A29: are_Prop w1,w by A22,A25,A9,A12,ANPROJ_1:22;
are_Prop z1,z by A17,A20,A24,A27,ANPROJ_1:22;
then
A30: w,y,z are_LinDep by A28,ANPROJ_1:4;
consider x2,z2,t2 being Element of V such that
A31: p = Dir(x2) and
A32: q = Dir(z2) and
A33: r = Dir(t2) and
A34: x2 is not zero and
A35: z2 is not zero and
A36: t2 is not zero and
A37: x2,z2,t2 are_LinDep by A7,Th23;
A38: are_Prop x2,x by A10,A13,A31,A34,ANPROJ_1:22;
consider u2,y2,t being Element of V such that
A39: p1 = Dir(u2) and
A40: q1 = Dir(y2) and
A41: r = Dir(t) and
A42: u2 is not zero and
A43: y2 is not zero and
A44: t is not zero and
A45: u2,y2,t are_LinDep by A5,Th23;
A46: are_Prop y2,y by A23,A26,A40,A43,ANPROJ_1:22;
A47: are_Prop t2,t by A41,A44,A33,A36,ANPROJ_1:22;
are_Prop z2,z by A17,A20,A32,A35,ANPROJ_1:22;
then
A48: x,z,t are_LinDep by A37,A38,A47,ANPROJ_1:4;
are_Prop u2,u by A15,A18,A39,A42,ANPROJ_1:22;
then
A49: u,y,t are_LinDep by A45,A46,ANPROJ_1:4;
consider v2,w2,t1 being Element of V such that
A50: r2 = Dir(v2) and
A51: r1 = Dir(w2) and
A52: r = Dir(t1) and
A53: v2 is not zero and
A54: w2 is not zero and
A55: t1 is not zero and
A56: v2,w2,t1 are_LinDep by A6,Th23;
A57: are_Prop t1,t by A41,A44,A52,A55,ANPROJ_1:22;
are_Prop u1,u by A15,A18,A8,A11,ANPROJ_1:22;
then
A58: u,w,x are_LinDep by A14,A29,ANPROJ_1:4;
consider v1,y1,x1 being Element of V such that
A59: r2 = Dir(v1) and
A60: q1 = Dir(y1) and
A61: p = Dir(x1) and
A62: v1 is not zero and
A63: y1 is not zero and
A64: x1 is not zero and
A65: v1,y1,x1 are_LinDep by A4,Th23;
A66: are_Prop x1,x by A10,A13,A61,A64,ANPROJ_1:22;
A67: are_Prop w2,w by A22,A25,A51,A54,ANPROJ_1:22;
are_Prop v2,v by A16,A19,A50,A53,ANPROJ_1:22;
then
A68: v,w,t are_LinDep by A56,A67,A57,ANPROJ_1:4;
A69: are_Prop y1,y by A23,A26,A60,A63,ANPROJ_1:22;
are_Prop v1,v by A16,A19,A59,A62,ANPROJ_1:22;
then v,y,x are_LinDep by A65,A69,A66,ANPROJ_1:4;
then u,v,y are_LinDep or u,v,w are_LinDep or u,w,y are_LinDep or v,w,y
are_LinDep by A20,A21,A13,A44,A30,A58,A49,A68,A48,ANPROJ_1:18;
hence thesis by A15,A16,A18,A19,A22,A23,A25,A26,Th23;
end;
Lm39: for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace(V) is
Fanoian
by Th26;
Lm40: for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace(V) is
Desarguesian
proof
let V be up-3-dimensional RealLinearSpace;
let o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be Element of ProjectiveSpace(V);
assume that
A1: o<>q1 and
A2: p1<>q1 and
A3: o<>q2 and
A4: p2<>q2 and
A5: o<>q3 and
A6: p3<>q3 and
A7: not o,p1,p2 are_collinear and
A8: ( not o,p1,p3 are_collinear)& not o,p2,p3 are_collinear and
A9: p1,p2,r3 are_collinear and
A10: q1,q2,r3 are_collinear and
A11: p2,p3,r1 are_collinear and
A12: q2,q3,r1 are_collinear and
A13: p1,p3,r2 are_collinear and
A14: q1,q3,r2 are_collinear and
A15: o,p1,q1 are_collinear and
A16: o,p2,q2 are_collinear and
A17: o,p3,q3 are_collinear;
consider q19,q29,r399 being Element of V such that
A18: q1 = Dir(q19) and
A19: q2 = Dir(q29) and
A20: r3 = Dir(r399) and
A21: q19 is not zero and
A22: q29 is not zero and
A23: r399 is not zero and
A24: q19,q29,r399 are_LinDep by A10,Th23;
consider q299,q39,r199 being Element of V such that
A25: q2 = Dir(q299) and
A26: q3 = Dir(q39) and
A27: r1 = Dir(r199) and
A28: q299 is not zero and
A29: q39 is not zero and
A30: r199 is not zero and
A31: q299,q39,r199 are_LinDep by A12,Th23;
A32: are_Prop q299,q29 by A19,A22,A25,A28,ANPROJ_1:22;
consider p299,p39,r19 being Element of V such that
A33: p2 = Dir(p299) and
A34: p3 = Dir(p39) and
A35: r1 = Dir(r19) and
A36: p299 is not zero and
A37: p39 is not zero and
A38: r19 is not zero and
A39: p299,p39,r19 are_LinDep by A11,Th23;
A40: not are_Prop p39,q39 by A6,A34,A37,A26,A29,ANPROJ_1:22;
are_Prop r199,r19 by A35,A38,A27,A30,ANPROJ_1:22;
then
A41: q29,q39,r19 are_LinDep by A31,A32,ANPROJ_1:4;
consider p199,p399,r29 being Element of V such that
A42: p1 = Dir(p199) and
A43: p3 = Dir(p399) and
A44: r2 = Dir(r29) and
A45: p199 is not zero and
A46: p399 is not zero and
A47: r29 is not zero and
A48: p199,p399,r29 are_LinDep by A13,Th23;
A49: are_Prop p399,p39 by A34,A37,A43,A46,ANPROJ_1:22;
consider o9 being Element of V such that
A50: o9 is not zero and
A51: o = Dir(o9) by ANPROJ_1:26;
A52: not are_Prop o9,q39 by A5,A50,A51,A26,A29,ANPROJ_1:22;
consider p19,p29,r39 being Element of V such that
A53: p1 = Dir(p19) and
A54: p2 = Dir(p29) and
A55: r3 = Dir(r39) and
A56: p19 is not zero and
A57: p29 is not zero and
A58: r39 is not zero and
A59: p19,p29,r39 are_LinDep by A9,Th23;
A60: ( not are_Prop p19,q19)& not are_Prop p29,q29 by A2,A4,A53,A54,A56,A57,A18
,A19,A21,A22,ANPROJ_1:22;
A61: ( not are_Prop o9,q19)& not are_Prop o9,q29 by A1,A3,A50,A51,A18,A19,A21
,A22,ANPROJ_1:22;
consider o999,p2999,q2999 being Element of V such that
A62: o = Dir(o999) and
A63: p2 = Dir(p2999) and
A64: q2 = Dir(q2999) and
A65: o999 is not zero and
A66: p2999 is not zero and
A67: q2999 is not zero and
A68: o999,p2999,q2999 are_LinDep by A16,Th23;
A69: are_Prop q2999,q29 by A19,A22,A64,A67,ANPROJ_1:22;
A70: are_Prop o999,o9 by A50,A51,A62,A65,ANPROJ_1:22;
are_Prop p2999,p29 by A54,A57,A63,A66,ANPROJ_1:22;
then
A71: o9,p29,q29 are_LinDep by A68,A70,A69,ANPROJ_1:4;
consider q199,q399,r299 being Element of V such that
A72: q1 = Dir(q199) and
A73: q3 = Dir(q399) and
A74: r2 = Dir(r299) and
A75: q199 is not zero and
A76: q399 is not zero and
A77: r299 is not zero and
A78: q199,q399,r299 are_LinDep by A14,Th23;
A79: are_Prop q199,q19 by A18,A21,A72,A75,ANPROJ_1:22;
A80: not o9,p19,p29 are_LinDep by A7,A50,A51,A53,A54,A56,A57,Th23;
are_Prop r399,r39 by A55,A58,A20,A23,ANPROJ_1:22;
then
A81: q19,q29,r39 are_LinDep by A24,ANPROJ_1:4;
A82: are_Prop q399,q39 by A26,A29,A73,A76,ANPROJ_1:22;
consider o9999,p3999,q3999 being Element of V such that
A83: o = Dir(o9999) and
A84: p3 = Dir(p3999) and
A85: q3 = Dir(q3999) and
A86: o9999 is not zero and
A87: p3999 is not zero and
A88: q3999 is not zero and
A89: o9999,p3999,q3999 are_LinDep by A17,Th23;
A90: are_Prop q3999,q39 by A26,A29,A85,A88,ANPROJ_1:22;
are_Prop p299,p29 by A54,A57,A33,A36,ANPROJ_1:22;
then
A91: p29,p39,r19 are_LinDep by A39,ANPROJ_1:4;
are_Prop p199,p19 by A53,A56,A42,A45,ANPROJ_1:22;
then p19,p39,r29 are_LinDep by A48,A49,ANPROJ_1:4;
then
A92: p19,p29,p39,r19,r29,r39 lie_on_a_triangle by A59,A91;
A93: q19,q29,q39 are_Prop_Vect by A21,A22,A29;
consider o99,p1999,q1999 being Element of V such that
A94: o = Dir(o99) and
A95: p1 = Dir(p1999) and
A96: q1 = Dir(q1999) and
A97: o99 is not zero and
A98: p1999 is not zero and
A99: q1999 is not zero and
A100: o99,p1999,q1999 are_LinDep by A15,Th23;
A101: are_Prop q1999,q19 by A18,A21,A96,A99,ANPROJ_1:22;
A102: ( not o9,p19,p39 are_LinDep)& not o9,p29,p39 are_LinDep by A8,A50,A51,A53
,A54,A56,A57,A34,A37,Th23;
A103: p19,p29,p39 are_Prop_Vect by A56,A57,A37;
A104: are_Prop o9999,o9 by A50,A51,A83,A86,ANPROJ_1:22;
are_Prop p3999,p39 by A34,A37,A84,A87,ANPROJ_1:22;
then
A105: o9,p39,q39 are_LinDep by A89,A104,A90,ANPROJ_1:4;
A106: are_Prop o99,o9 by A50,A51,A94,A97,ANPROJ_1:22;
are_Prop p1999,p19 by A53,A56,A95,A98,ANPROJ_1:22;
then o9,p19,q19 are_LinDep by A100,A106,A101,ANPROJ_1:4;
then
A107: o9,p19,p29,p39,q19,q29,q39 are_perspective by A71,A105;
are_Prop r299,r29 by A44,A47,A74,A77,ANPROJ_1:22;
then q19,q39,r29 are_LinDep by A78,A79,A82,ANPROJ_1:4;
then
A108: q19,q29,q39,r19,r29,r39 lie_on_a_triangle by A81,A41;
r19,r29,r39 are_Prop_Vect by A58,A38,A47;
then r19,r29,r39 are_LinDep by A50,A61,A52,A60,A40,A103,A93,A107,A80,A102,A92
,A108,Th8;
hence thesis by A55,A58,A35,A38,A44,A47,Th23;
end;
Lm41: for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace(V) is
Pappian
proof
let V be up-3-dimensional RealLinearSpace;
let o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be Element of ProjectiveSpace V;
assume that
A1: o<>p2 and
A2: o<>p3 and
A3: p2<>p3 and
A4: p1<>p2 and
A5: p1<>p3 and
A6: o<>q2 and
A7: o<>q3 and
A8: q2<>q3 and
A9: q1<>q2 and
A10: q1<>q3 and
A11: not o,p1,q1 are_collinear and
A12: o,p1,p2 are_collinear and
A13: o,p1,p3 are_collinear and
A14: o,q1,q2 are_collinear and
A15: o,q1,q3 are_collinear and
A16: p1,q2,r3 are_collinear and
A17: q1,p2,r3 are_collinear and
A18: p1,q3,r2 are_collinear and
A19: p3,q1,r2 are_collinear and
A20: p2,q3,r1 are_collinear and
A21: p3,q2,r1 are_collinear;
consider o999,q19,q29 being Element of V such that
A22: o = Dir(o999) and
A23: q1 = Dir(q19) and
A24: q2 = Dir(q29) and
A25: o999 is not zero and
A26: q19 is not zero and
A27: q29 is not zero and
A28: o999,q19,q29 are_LinDep by A14,Th23;
A29: not are_Prop q19,q29 by A9,A23,A24,A26,A27,ANPROJ_1:22;
consider o9999,q199,q39 being Element of V such that
A30: o = Dir(o9999) and
A31: q1 = Dir(q199) and
A32: q3 = Dir(q39) and
A33: o9999 is not zero and
A34: q199 is not zero and
A35: q39 is not zero and
A36: o9999,q199,q39 are_LinDep by A15,Th23;
A37: are_Prop q199,q19 by A23,A26,A31,A34,ANPROJ_1:22;
consider o99,p199,p39 being Element of V such that
A38: o = Dir(o99) & p1 = Dir(p199) and
A39: p3 = Dir(p39) and
A40: o99 is not zero & p199 is not zero and
A41: p39 is not zero and
A42: o99,p199,p39 are_LinDep by A13,Th23;
consider o9,p19,p29 being Element of V such that
A43: o = Dir(o9) and
A44: p1 = Dir(p19) and
A45: p2 = Dir(p29) and
A46: o9 is not zero and
A47: p19 is not zero and
A48: p29 is not zero and
A49: o9,p19,p29 are_LinDep by A12,Th23;
A50: ( not are_Prop o9,p39)& not are_Prop p19,p39 by A2,A5,A43,A44,A46,A47,A39
,A41,ANPROJ_1:22;
A51: ( not are_Prop q19,q39)& not are_Prop q29,q39 by A8,A10,A23,A24,A26,A27
,A32,A35,ANPROJ_1:22;
A52: not are_Prop p29,p39 by A3,A45,A48,A39,A41,ANPROJ_1:22;
A53: not are_Prop o9,q39 by A7,A43,A46,A32,A35,ANPROJ_1:22;
A54: not are_Prop o9,q29 by A6,A43,A46,A24,A27,ANPROJ_1:22;
( not are_Prop o9,p29)& not are_Prop p19,p29 by A1,A4,A43,A44,A45,A46,A47,A48
,ANPROJ_1:22;
then
A55: o9,p19,p29,p39,q19,q29,q39 are_half_mutually_not_Prop by A54,A53,A50,A29
,A52,A51;
consider q1999,p2999,r399 being Element of V such that
A56: q1 = Dir(q1999) and
A57: p2 = Dir(p2999) and
A58: r3 = Dir(r399) and
A59: q1999 is not zero and
A60: p2999 is not zero and
A61: r399 is not zero and
A62: q1999,p2999,r399 are_LinDep by A17,Th23;
A63: are_Prop q1999,q19 by A23,A26,A56,A59,ANPROJ_1:22;
consider p29999,q3999,r19 being Element of V such that
A64: p2 = Dir(p29999) and
A65: q3 = Dir(q3999) and
A66: r1 = Dir(r19) and
A67: p29999 is not zero and
A68: q3999 is not zero and
A69: r19 is not zero and
A70: p29999,q3999,r19 are_LinDep by A20,Th23;
A71: are_Prop q3999,q39 by A32,A35,A65,A68,ANPROJ_1:22;
are_Prop o999,o9 by A43,A46,A22,A25,ANPROJ_1:22;
then
A72: o9,q19,q29 are_LinDep by A28,ANPROJ_1:4;
are_Prop o9999,o9 by A43,A46,A30,A33,ANPROJ_1:22;
then
A73: o9,q19,q39 are_LinDep by A36,A37,ANPROJ_1:4;
are_Prop o99,o9 & are_Prop p199,p19 by A43,A44,A46,A47,A38,A40,ANPROJ_1:22;
then
A74: o9,p19,p39 are_LinDep by A42,ANPROJ_1:4;
not o9,p19,q19 are_LinDep by A11,A43,A44,A46,A47,A23,A26,Th23;
then
A75: o9,p19,p29,p39,q19,q29,q39 lie_on_an_angle by A49,A74,A72,A73;
consider p19999,q399,r29 being Element of V such that
A76: p1 = Dir(p19999) and
A77: q3 = Dir(q399) and
A78: r2 = Dir(r29) and
A79: p19999 is not zero and
A80: q399 is not zero and
A81: r29 is not zero and
A82: p19999,q399,r29 are_LinDep by A18,Th23;
A83: are_Prop q399,q39 by A32,A35,A77,A80,ANPROJ_1:22;
consider p3999,q29999,r199 being Element of V such that
A84: p3 = Dir(p3999) and
A85: q2 = Dir(q29999) and
A86: r1 = Dir(r199) and
A87: p3999 is not zero and
A88: q29999 is not zero and
A89: r199 is not zero and
A90: p3999,q29999,r199 are_LinDep by A21,Th23;
A91: are_Prop p3999,p39 by A39,A41,A84,A87,ANPROJ_1:22;
A92: are_Prop q29999,q29 by A24,A27,A85,A88,ANPROJ_1:22;
are_Prop r199,r19 by A66,A69,A86,A89,ANPROJ_1:22;
then
A93: p39,q29,r19 are_LinDep by A90,A91,A92,ANPROJ_1:4;
A94: q19,q29,q39 are_Prop_Vect by A26,A27,A35;
A95: p19,p29,p39 are_Prop_Vect by A47,A48,A41;
are_Prop p29999,p29 by A45,A48,A64,A67,ANPROJ_1:22;
then
A96: p29,q39,r19 are_LinDep by A70,A71,ANPROJ_1:4;
consider p399,q1999,r299 being Element of V such that
A97: p3 = Dir(p399) and
A98: q1 = Dir(q1999) and
A99: r2 = Dir(r299) and
A100: p399 is not zero and
A101: q1999 is not zero and
A102: r299 is not zero and
A103: p399,q1999,r299 are_LinDep by A19,Th23;
A104: are_Prop q1999,q19 by A23,A26,A98,A101,ANPROJ_1:22;
are_Prop p19999,p19 by A44,A47,A76,A79,ANPROJ_1:22;
then
A105: p19,q39,r29 are_LinDep by A82,A83,ANPROJ_1:4;
consider p1999,q2999,r39 being Element of V such that
A106: p1 = Dir(p1999) and
A107: q2 = Dir(q2999) and
A108: r3 = Dir(r39) and
A109: p1999 is not zero and
A110: q2999 is not zero and
A111: r39 is not zero and
A112: p1999,q2999,r39 are_LinDep by A16,Th23;
A113: are_Prop q2999,q29 by A24,A27,A107,A110,ANPROJ_1:22;
A114: are_Prop p2999,p29 by A45,A48,A57,A60,ANPROJ_1:22;
are_Prop r399,r39 by A108,A111,A58,A61,ANPROJ_1:22;
then
A115: q19,p29,r39 are_LinDep by A62,A63,A114,ANPROJ_1:4;
are_Prop p1999,p19 by A44,A47,A106,A109,ANPROJ_1:22;
then
A116: p19,q29,r39 are_LinDep by A112,A113,ANPROJ_1:4;
A117: are_Prop p399,p39 by A39,A41,A97,A100,ANPROJ_1:22;
are_Prop r299,r29 by A78,A81,A99,A102,ANPROJ_1:22;
then
A118: p39,q19,r29 are_LinDep by A103,A117,A104,ANPROJ_1:4;
r19,r29,r39 are_Prop_Vect by A111,A81,A69;
then r19,r29,r39 are_LinDep by A46,A75,A55,A95,A94,A116,A115,A105,A118,A96
,A93,Th9;
hence thesis by A108,A111,A78,A81,A66,A69,Th23;
end;
registration
let V be up-3-dimensional RealLinearSpace;
::$N Desargues' Theorem
::$L https://en.wikipedia.org/wiki/Desargues's_theorem Desargues' Theorem
cluster ProjectiveSpace V -> Fanoian Desarguesian Pappian;
coherence by Lm39,Lm40,Lm41;
end;
theorem Th27:
(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
are_collinear & r1,r2,q are_collinear)
proof
given p,q,r being Element of V such that
A1: for a,b,c st a*p + b*q + c*r = 0.V holds a=0 & b=0 & c = 0 and
A2: for y ex a,b,c st y = a*p + b*q + c*r;
A3: p is not zero & q is not zero by A1,Th1;
then reconsider x1=Dir(p),x2=Dir(q) as Element of ProjectiveSpace(V) by
ANPROJ_1:26;
take x1,x2;
not are_Prop p,q by A1,Th1;
hence x1<>x2 by A3,ANPROJ_1:22;
let r1,r2;
consider u such that
A4: u is not zero & r1 = Dir(u) by ANPROJ_1:26;
consider u1 such that
A5: u1 is not zero & r2 = Dir(u1) by ANPROJ_1:26;
consider y such that
A6: p,q,y are_LinDep and
A7: u,u1,y are_LinDep and
A8: y is not zero by A1,A2,Th3;
reconsider q = Dir(y) as Element of ProjectiveSpace(V) by A8,ANPROJ_1:26;
take q;
thus x1,x2,q are_collinear by A3,A6,A8,Th23;
thus thesis by A4,A5,A7,A8,Th23;
end;
theorem Th28:
(ex x1,x2 being Element of ProjectiveSpace(V) st (x1<>x2 & for
r1,r2 ex q st x1,x2,q are_collinear & r1,r2,q are_collinear)) implies
for p,p1,q,
q1 ex r st p,p1,r are_collinear & q,q1,r are_collinear
proof
given x1,x2 being Element of ProjectiveSpace(V) such that
A1: x1<>x2 and
A2: for r1,r2 ex q st x1,x2,q are_collinear & r1,r2,q are_collinear;
let p,p1,q,q1;
consider p3 being Element of ProjectiveSpace(V) such that
A3: x1,x2,p3 are_collinear and
A4: p,p1,p3 are_collinear by A2;
consider q3 being Element of ProjectiveSpace(V) such that
A5: x1,x2,q3 are_collinear and
A6: q,q1,q3 are_collinear by A2;
consider s2 being Element of ProjectiveSpace(V) such that
A7: x1,x2,s2 are_collinear and
A8: p,q,s2 are_collinear by A2;
A9: s2,p,q are_collinear by A8,Th24;
consider s4 being Element of ProjectiveSpace(V) such that
A10: x1,x2,s4 are_collinear and
A11: p,q1,s4 are_collinear by A2;
A12: s4,q1,p are_collinear by A11,Th24;
p3,s2,q3 are_collinear by A1,A3,A5,A7,Def8;
then consider s3 being Element of ProjectiveSpace(V) such that
A13: p3,p,s3 are_collinear and
A14: q3,q,s3 are_collinear by A9,Def9;
consider s being Element of ProjectiveSpace(V) such that
A15: x1,x2,s are_collinear and
A16: p1,q1,s are_collinear by A2;
q3,s4,p3 are_collinear by A1,A3,A5,A10,Def8;
then consider s5 being Element of ProjectiveSpace(V) such that
A17: q3,q1,s5 are_collinear and
A18: p3,p,s5 are_collinear by A12,Def9;
A19: p1,s,q1 are_collinear by A16,Th24;
consider s6 being Element of ProjectiveSpace(V) such that
A20: x1,x2,s6 are_collinear and
A21: p1,q,s6 are_collinear by A2;
A22: s6,p1,q are_collinear by A21,Th24;
p3,s6,q3 are_collinear by A1,A3,A5,A20,Def8;
then consider s7 being Element of ProjectiveSpace(V) such that
A23: p3,p1,s7 are_collinear and
A24: q3,q,s7 are_collinear by A22,Def9;
s,p3,q3 are_collinear by A1,A3,A5,A15,Def8;
then consider s1 being Element of ProjectiveSpace(V) such that
A25: p1,p3,s1 are_collinear and
A26: q1,q3,s1 are_collinear by A19,Def9;
A27: now
A28: now
A29: q3,q1,s1 are_collinear by A26,Th24;
assume that
A30: p3<>p1 and
A31: q3<>q1;
q3,q1,q are_collinear & q3,q1,q1 are_collinear by A6,Def7,Th24;
then
A32: q,q1,s1 are_collinear by A31,A29,Def8;
take s1;
A33: p3,p1,s1 are_collinear by A25,Th24;
p3,p1,p are_collinear & p3,p1,p1 are_collinear by A4,Def7,Th24;
then p,p1,s1 are_collinear by A30,A33,Def8;
hence thesis by A32;
end;
A34: now
assume that
A35: p3<>p and
A36: q3<>q;
take s3;
q3,q,q are_collinear & q3,q,q1 are_collinear by A6,Def7,Th24;
then
A37: q,q1,s3 are_collinear by A14,A36,Def8;
p3,p,p are_collinear & p3,p,p1 are_collinear by A4,Def7,Th24;
then p,p1,s3 are_collinear by A13,A35,Def8;
hence thesis by A37;
end;
A38: now
assume that
A39: p3<>p1 and
A40: q3<>q;
take s7;
q3,q,q are_collinear & q3,q,q1 are_collinear by A6,Def7,Th24;
then
A41: q,q1,s7 are_collinear by A24,A40,Def8;
p3,p1,p are_collinear & p3,p1,p1 are_collinear by A4,Def7,Th24;
then p,p1,s7 are_collinear by A23,A39,Def8;
hence thesis by A41;
end;
A42: now
assume that
A43: p3<>p and
A44: q3<>q1;
take s5;
q3,q1,q are_collinear & q3,q1,q1 are_collinear by A6,Def7,Th24;
then
A45: q,q1,s5 are_collinear by A17,A44,Def8;
p3,p,p are_collinear & p3,p,p1 are_collinear by A4,Def7,Th24;
then p,p1,s5 are_collinear by A18,A43,Def8;
hence thesis by A45;
end;
assume p<>p1 & q<>q1;
hence thesis by A34,A42,A38,A28;
end;
now
A46: now
assume
A47: p=p1;
take q3;
p,p1,q3 are_collinear by A47,Def7;
hence thesis by A6;
end;
A48: now
assume
A49: q=q1;
take p3;
q,q1,p3 are_collinear by A49,Def7;
hence thesis by A4;
end;
assume p = p1 or q = q1;
hence thesis by A48,A46;
end;
hence thesis by A27;
end;
theorem Th29:
(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
proof
given u,v,w such that
A1: for a,b,c st a*u + b*v + c*w = 0.V holds a=0 & b=0 & c = 0 and
A2: for y ex a,b,c st y = a*u + b*v + c*w;
reconsider V9 = V as up-3-dimensional RealLinearSpace by A1,Def6;
take ProjectiveSpace(V9);
ex x1,x2 being Element of ProjectiveSpace(V) st (x1<>x2 & for r1,r2 ex q
st x1,x2,q are_collinear & r1,r2,q are_collinear) by A1,A2,Th27;
then for p,p1,q,q1 ex r st p,p1,r are_collinear & q,q1,r are_collinear
by Th28;
hence thesis;
end;
Lm42: (ex y,u,v,w st (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 V is up-3-dimensional
proof
given y,u,v,w such that
A1: 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;
take y,u,v;
let a,b,a1;
assume a*y + b*u + a1*v = 0.V;
then 0.V = a*y + b*u + a1*v + 0.V by RLVECT_1:4
.= a*y + b*u + a1*v + 0*w by RLVECT_1:10;
hence thesis by A1;
end;
Lm43: (ex y,u,v,w st (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 ProjectiveSpace(V) is proper at_least_3rank
proof
given y,u,v,w such that
A1: 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;
V is up-3-dimensional by A1,Lm42;
hence thesis;
end;
theorem Th30:
(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 are_collinear & for r1,r2
ex q3,r3 st
r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear
proof
given y,u,v,w such that
A1: for w1 ex a,b,a1,b1 st w1 = a*y + b*u + a1*v + b1*w and
A2: 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;
A3: u is not zero & v is not zero by A2,Th2;
A4: y is not zero by A2,Th2;
then reconsider
p = Dir(y),q1 = Dir(u),q2 = Dir(v) as Element of
ProjectiveSpace(V) by A3,ANPROJ_1:26;
take p,q1,q2;
not y,u,v are_LinDep by A2,Th2;
then not p,q1,q2 are_collinear by A4,A3,ANPROJ_1:25;
hence not p,q1,q2 are_collinear;
let r1,r2;
consider u1 such that
A5: u1 is not zero and
A6: r1 = Dir(u1) by ANPROJ_1:26;
consider u2 such that
A7: u2 is not zero and
A8: r2 = Dir(u2) by ANPROJ_1:26;
consider w1,w2 such that
A9: u1,u2,w2 are_LinDep and
A10: u,v,w1 are_LinDep and
A11: y,w2,w1 are_LinDep and
A12: w1 is not zero and
A13: w2 is not zero by A1,A2,A5,A7,Th4;
reconsider q3 = Dir(w1),r3 = Dir(w2) as Element of
ProjectiveSpace(V) by A12,A13,ANPROJ_1:26;
take q3,r3;
thus r1,r2,r3 are_collinear by A5,A6,A7,A8,A9,A13,Th23;
thus q1,q2,q3 are_collinear by A3,A10,A12,Th23;
thus thesis by A4,A11,A12,A13,Th23;
end;
Lm44: for x,d,b,b9,d9,q being Element of ProjectiveSpace(V) st not q,b,d
are_collinear & b,d,x are_collinear & q,b9,b are_collinear &
q,d9,d are_collinear
holds ex o being Element of ProjectiveSpace(V) st b9,d9,o are_collinear & q,x,o
are_collinear
proof
let x,d,b,b9,d9,q be Element of ProjectiveSpace(V);
assume that
A1: not q,b,d are_collinear and
A2: b,d,x are_collinear and
A3: q,b9,b are_collinear and
A4: q,d9,d are_collinear;
A5: b9,q,b are_collinear by A3,Th24;
A6: b<>d by A1,Def7;
A7: now
A8: b,b9,q are_collinear by A3,Th24;
consider z being Element of ProjectiveSpace(V) such that
A9: b9,d9,z are_collinear and
A10: b,d,z are_collinear by A4,A5,Def9;
A11: z,b9,b9 are_collinear by Def7;
b,d,b are_collinear by Def7;
then z,b,x are_collinear by A2,A6,A10,Def8;
then consider
o being Element of ProjectiveSpace(V) such that
A12: z,b9,o are_collinear and
A13: x,q,o are_collinear by A8,Def9;
A14: q,x,o are_collinear by A13,Th24;
assume
A15: b <> b9;
A16: z<>b9
proof
assume not thesis;
then
A17: b,b9,d are_collinear by A10,Th24;
b,b9,q are_collinear & b,b9,b are_collinear by A3,Def7,Th24;
hence contradiction by A1,A15,A17,Def8;
end;
z,b9,d9 are_collinear by A9,Th24;
then b9,d9,o are_collinear by A12,A16,A11,Def8;
hence thesis by A14;
end;
now
assume b = b9;
then
A18: d,b9,x are_collinear by A2,Th24;
d9,d,q are_collinear by A4,Th24;
then consider
o being Element of ProjectiveSpace(V) such that
A19: d9,b9,o are_collinear and
A20: q,x,o are_collinear by A18,Def9;
b9,d9,o are_collinear by A19,Th24;
hence thesis by A20;
end;
hence thesis by A7;
end;
reserve x,z,x1,y1,z1,x2,x3,y2,z2,p4,q4 for Element of ProjectiveSpace(V);
theorem Th31:
ProjectiveSpace(V) is proper at_least_3rank & (ex p,q1,q2 st not
p,q1,q2 are_collinear & (for r1,r2 ex q3,r3 st r1,r2,r3 are_collinear &
q1,q2,q3
are_collinear & p,r3,q3 are_collinear)) implies
ex CS being CollProjectiveSpace
st CS = ProjectiveSpace(V) & CS is at_most-3-dimensional
proof
assume that
A1: ProjectiveSpace(V) is proper and
A2: for p,q holds ex r st p<>r & q<>r & p,q,r are_collinear;
defpred P[Element of ProjectiveSpace(V), Element of ProjectiveSpace(V),
Element of ProjectiveSpace(V)] means for y1,y2 ex x2,x1 st y1,y2,x1
are_collinear & $2,$3,x2 are_collinear & $1,x1,x2 are_collinear;
A3: for p,q1,q2 st q1,q2,p are_collinear holds P[p,q1,q2]
proof
let p,q1,q2 such that
A4: q1,q2,p are_collinear;
now
let y1,y2;
y1,y2,y2 are_collinear & p,y2,p are_collinear by Def7;
hence
ex x2,x1 st y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & p,x1,x2
are_collinear by A4;
end;
hence thesis;
end;
A5: for q,q1,q2,p1,p2,x st P[q,q1,q2] & not q1,q2,q are_collinear & q1,q2,x
are_collinear & not p1,p2,q are_collinear & p1,p2,x are_collinear
holds P[q,p1,p2]
proof
let q,q1,q2,p1,p2,x;
assume that
A6: P[q,q1,q2] and
A7: not q1,q2,q are_collinear and
A8: q1,q2,x are_collinear and
A9: not p1,p2,q are_collinear and
A10: p1,p2,x are_collinear;
A11: q1<>q2 by A7,Def7;
A12: p1<>p2 by A9,Def7;
now
let y1,y2;
A13: now
ex a being Element of ProjectiveSpace(V) st p1,p2,a are_collinear
& x<>a
proof
A14: now
assume
A15: x<>p2;
take p2;
p1,p2,p2 are_collinear by Def7;
hence thesis by A15;
end;
now
assume
A16: x<>p1;
take p1;
p1,p2,p1 are_collinear by Def7;
hence thesis by A16;
end;
hence thesis by A9,A14,Def7;
end;
then consider x1 such that
A17: p1,p2,x1 are_collinear and
A18: x<>x1;
consider b,b9 being Element of ProjectiveSpace(V) such that
A19: y1,y2,b9 are_collinear and
A20: q1,q2,b are_collinear and
A21: q,b9,b are_collinear by A6;
assume
A22: y1<>y2;
ex a being Element of ProjectiveSpace(V) st y1,y2,a are_collinear
& b9<>a
proof
A23: now
assume
A24: b9<>y2;
take y2;
y1,y2,y2 are_collinear by Def7;
hence thesis by A24;
end;
now
assume
A25: b9<>y1;
take y1;
y1,y2,y1 are_collinear by Def7;
hence thesis by A25;
end;
hence thesis by A22,A23;
end;
then consider x3 such that
A26: b9<>x3 and
A27: y1,y2,x3 are_collinear;
consider d,d9 being Element of ProjectiveSpace(V) such that
A28: x1,x3,d9 are_collinear and
A29: q1,q2,d are_collinear and
A30: q,d9,d are_collinear by A6;
A31: b,d,x are_collinear by A8,A11,A20,A29,Def8;
A32: now
assume
A33: b<>d;
not q,b,d are_collinear
proof
q1,q2,q2 are_collinear by Def7;
then
A34: b,d,q2 are_collinear by A11,A20,A29,Def8;
assume not thesis;
then
A35: b,d,q are_collinear by Th24;
q1,q2,q1 are_collinear by Def7;
then b,d,q1 are_collinear by A11,A20,A29,Def8;
hence contradiction by A7,A33,A35,A34,Def8;
end;
then consider o being Element of ProjectiveSpace(V) such that
A36: b9,d9,o are_collinear and
A37: q,x,o are_collinear by A21,A30,A31,Lm44;
A38: o,x,q are_collinear by A37,Th24;
d9,x3,x1 are_collinear by A28,Th24;
then consider z1 such that
A39: b9,x3,z1 are_collinear and
A40: o,x1,z1 are_collinear by A36,Def9;
x1,o,z1 are_collinear by A40,Th24;
then consider z2 such that
A41: x1,x,z2 are_collinear and
A42: z1,q,z2 are_collinear by A38,Def9;
A43: q,z1,z2 are_collinear by A42,Th24;
p1,p2,p2 are_collinear by Def7;
then
A44: x1,x,p2 are_collinear by A10,A12,A17,Def8;
y1,y2,y2 are_collinear by Def7;
then
A45: b9,x3,y2 are_collinear by A22,A19,A27,Def8;
p1,p2,p1 are_collinear by Def7;
then x1,x,p1 are_collinear by A10,A12,A17,Def8;
then
A46: p1,p2,z2 are_collinear by A18,A41,A44,Def8;
y1,y2,y1 are_collinear by Def7;
then b9,x3,y1 are_collinear by A22,A19,A27,Def8;
then y1,y2,z1 are_collinear by A26,A39,A45,Def8;
hence ex z2,z1 st y1,y2,z1 are_collinear & p1,p2,z2 are_collinear &
q,
z1,z2 are_collinear by A46,A43;
end;
now
assume b=d;
then
A47: b,q,d9 are_collinear by A30,Th24;
y1,y2,y2 are_collinear by Def7;
then
A48: b9,x3,y2 are_collinear by A22,A19,A27,Def8;
A49: d9,x3,x1 are_collinear by A28,Th24;
b,q,b9 are_collinear & b,q,q are_collinear by A21,Def7,Th24;
then b9,d9,q are_collinear by A7,A20,A47,Def8;
then consider z1 such that
A50: b9,x3,z1 are_collinear and
A51: q,x1,z1 are_collinear by A49,Def9;
A52: q,z1,x1 are_collinear by A51,Th24;
y1,y2,y1 are_collinear by Def7;
then b9,x3,y1 are_collinear by A22,A19,A27,Def8;
then y1,y2,z1 are_collinear by A26,A50,A48,Def8;
hence ex z2,z1 st y1,y2,z1 are_collinear & p1,p2,z2 are_collinear &
q,
z1,z2 are_collinear by A17,A52;
end;
hence
ex z2,z1 st y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,
z2 are_collinear by A32;
end;
now
assume y1=y2;
then
A53: y1,y2,q are_collinear by Def7;
p1,p2,p1 are_collinear & q,q,p1 are_collinear by Def7;
hence
ex z2,z1 st y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,
z2 are_collinear by A53;
end;
hence
ex z2,z1 st y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2
are_collinear by A13;
end;
hence thesis;
end;
A54: for q1,q2,p1,p2,q st not q1,q2,q are_collinear & not p1,p2,q
are_collinear & (not ex x st (q1,q2,x are_collinear & p1,p2,x are_collinear))
ex
q3,p3 st p1,p2,p3 are_collinear & q1,q2,q3 are_collinear & not q3,p3,q
are_collinear
proof
let q1,q2,p1,p2,q such that
A55: not q1,q2,q are_collinear and
A56: not p1,p2,q are_collinear and
not ex x st (q1,q2,x are_collinear & p1,p2,x are_collinear);
A57: q<>q1 by A55,Def7;
A58: not q1,p1,q are_collinear or not q1,p2,q are_collinear
proof
assume not thesis;
then
A59: q,q1,p1 are_collinear & q,q1,p2 are_collinear by Th24;
q,q1,q are_collinear by Def7;
hence contradiction by A56,A57,A59,Def8;
end;
A60: p1,p2,p2 are_collinear by Def7;
q1,q2,q1 are_collinear & p1,p2,p1 are_collinear by Def7;
hence thesis by A60,A58;
end;
A61: for q,q1,q2,p1,p2 st P[q,q1,q2] & not q1,q2,q are_collinear & not p1,p2
,q are_collinear &
not ex x st (q1,q2,x are_collinear & p1,p2,x are_collinear)
holds P[q,p1,p2]
proof
let q,q1,q2,p1,p2;
assume that
A62: P[q,q1,q2] and
A63: not q1,q2,q are_collinear and
A64: not p1,p2,q are_collinear and
A65: not ex x st (q1,q2,x are_collinear & p1,p2,x are_collinear);
consider q3,p3 such that
A66: p1,p2,p3 are_collinear and
A67: q1,q2,q3 are_collinear and
A68: not q3,p3,q are_collinear by A54,A63,A64,A65;
q3,p3,q3 are_collinear by Def7;
then
A69: P[q,q3,p3] by A5,A62,A63,A67,A68;
q3,p3,p3 are_collinear by Def7;
hence thesis by A5,A64,A66,A68,A69;
end;
A70: for q,q1,q2 st P[q,q1,q2] & not q1,q2,q are_collinear holds for p1,p2
holds P[q,p1,p2]
proof
let q,q1,q2 such that
A71: ( P[q,q1,q2])& not q1,q2,q are_collinear;
let p1,p2;
A72: not p1,p2,q are_collinear & (not ex x st q1,q2,x are_collinear & p1,p2
,x are_collinear) implies P[q,p1,p2] by A61,A71;
not p1,p2,q are_collinear & (ex x st q1,q2,x are_collinear & p1,p2,x
are_collinear) implies P[q,p1,p2] by A5,A71;
hence thesis by A3,A72;
end;
reconsider CS = ProjectiveSpace(V) as CollProjectiveSpace by A1,A2,Def10;
given p,q1,q2 such that
A73: not p,q1,q2 are_collinear and
A74: for r1,r2 ex q3,r3 st r1,r2,r3 are_collinear & q1,q2,q3 are_collinear
& p,r3,q3 are_collinear;
take CS;
A75: for q,q1,q2,x,q3 st P[q,q1,q2] & not q1,q2,q are_collinear & q1,q2,x
are_collinear & q,q3,x are_collinear holds P[q3,q1,q2]
proof
let q,q1,q2,x,q3 such that
A76: P[q,q1,q2] and
A77: not q1,q2,q are_collinear and
A78: q1,q2,x are_collinear and
A79: q,q3,x are_collinear;
now
let y1,y2;
consider z2,z1 such that
A80: y1,y2,z1 are_collinear and
A81: q1,q2,z2 are_collinear and
A82: q,z1,z2 are_collinear by A76;
A83: now
q3,q,x are_collinear by A79,Th24;
then consider x2 such that
A84: q3,z1,x2 are_collinear and
A85: x,z2,x2 are_collinear by A82,Def9;
A86: q1<>q2 by A77,Def7;
q1,q2,q2 are_collinear by Def7;
then
A87: x,z2,q2 are_collinear by A78,A81,A86,Def8;
q1,q2,q1 are_collinear by Def7;
then
A88: x,z2,q1 are_collinear by A78,A81,A86,Def8;
assume x<>z2;
then q1,q2,x2 are_collinear by A85,A88,A87,Def8;
hence
ex x2,x1 st y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1
,x2 are_collinear by A80,A84;
end;
now
A89: q,x,q3 are_collinear & q,x,x are_collinear by A79,Def7,Th24;
assume
A90: x=z2;
then q,x,z1 are_collinear by A82,Th24;
then q3,z1,z2 are_collinear by A77,A78,A90,A89,Def8;
hence
ex x2,x1 st y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1
,x2 are_collinear by A80,A81;
end;
hence ex x2,x1 st y1,y2,x1 are_collinear & q1,q2,x2 are_collinear &
q3,x1,
x2 are_collinear by A83;
end;
hence thesis;
end;
A91: for q,p holds ((for q1,q2 holds P[q,q1,q2]) implies ex p1,p2 st P[p,p1
,p2] & not p1,p2,p are_collinear )
proof
let q,p such that
A92: for q1,q2 holds P[q,q1,q2];
consider x1 such that
A93: p<>x1 and
A94: q<>x1 and
A95: p,q,x1 are_collinear by A2;
consider x2 such that
A96: not p,x1,x2 are_collinear by A1,A93,COLLSP:12;
A97: not x1,x2,q are_collinear
proof
assume not thesis;
then
A98: q,x1,x2 are_collinear by Th24;
q,x1,x1 are_collinear & q,x1,p are_collinear by A95,Def7,Th24;
hence contradiction by A94,A96,A98,Def8;
end;
A99: x1,x2,x1 are_collinear by Def7;
A100: not x1,x2,p are_collinear by A96,Th24;
A101: P[q,x1,x2] by A92;
q,p,x1 are_collinear by A95,Th24;
then P[p,x1,x2] by A75,A97,A99,A101;
hence thesis by A100;
end;
A102: for x,y1,z holds P[x,y1,z]
proof
let x,y1,z;
not q1,q2,p are_collinear by A73,Th24;
then for p1,p2 holds P[p,p1,p2] by A74,A70;
then ex r1,r2 st P[x,r1,r2] & not r1,r2,x are_collinear by A91;
hence thesis by A70;
end;
for p4,p1,q,q4,r2 ex r,r1 st p4,q,r are_collinear & p1,q4,r1
are_collinear & r2,r,r1 are_collinear
proof
let p4,p1,q,q4,r2;
ex r1,r st p4,q,r are_collinear & p1,q4,r1 are_collinear & r2,r,r1
are_collinear by A102;
hence thesis;
end;
hence thesis;
end;
theorem Th32:
(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
proof
given y,u,v,w such that
A1: ( 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;
ProjectiveSpace(V) is proper at_least_3rank & ex p,q1,q2 st not p,q1,q2
are_collinear & for r1,r2 ex q3,r3 st r1,r2,r3 are_collinear & q1,q2,q3
are_collinear & p,r3,q3 are_collinear by A1,Lm43,Th30;
hence thesis by Th31;
end;
theorem Th33:
(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
proof
given u,v,u1,v1 such that
A1: 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;
V is up-3-dimensional by A1,Lm42;
then reconsider CS = ProjectiveSpace(V) as CollProjectiveSpace;
take CS;
thus CS = ProjectiveSpace(V);
A2: u1 is not zero & v1 is not zero by A1,Th2;
A3: u is not zero & v is not zero by A1,Th2;
then reconsider p=Dir(u),p1=Dir(v),q=Dir(u1),q1=Dir(v1) as Element of CS by
A2,ANPROJ_1:26;
take p,p1,q,q1;
thus not ex r being Element of CS st (p,p1,r are_collinear & q,q1,r
are_collinear)
proof
assume not thesis;
then consider r being Element of CS such that
A4: p,p1,r are_collinear and
A5: q,q1,r are_collinear;
consider y such that
A6: y is not zero and
A7: r=Dir(y) by ANPROJ_1:26;
[q,q1,r] in the Collinearity of ProjectiveSpace(V) by A5;
then
A8: u1,v1,y are_LinDep by A2,A6,A7,ANPROJ_1:25;
[p,p1,r] in the Collinearity of ProjectiveSpace(V) by A4;
then u,v,y are_LinDep by A3,A6,A7,ANPROJ_1:25;
hence contradiction by A1,A6,A8,Th5;
end;
end;
theorem Th34:
(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
proof
assume 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;
then
(ex CS1 being CollProjectiveSpace st CS1 = ProjectiveSpace (V) & CS1 is
up-3-dimensional )& ex CS2 being CollProjectiveSpace st CS2 = ProjectiveSpace (
V) & CS2 is at_most-3-dimensional by Th32,Th33;
hence thesis;
end;
registration
cluster strict Fanoian Desarguesian Pappian 2-dimensional
for CollProjectiveSpace;
existence
proof
consider V being non trivial RealLinearSpace such that
A1: 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 by Th16;
reconsider V as up-3-dimensional RealLinearSpace by A1,Def6;
take CS = ProjectiveSpace(V);
thus CS is strict Fanoian Desarguesian Pappian;
ex CS1 being CollProjectiveSpace st CS1 = ProjectiveSpace (V) & CS1 is
2-dimensional by A1,Th29;
hence thesis;
end;
cluster strict Fanoian Desarguesian Pappian at_most-3-dimensional
up-3-dimensional for CollProjectiveSpace;
existence
proof
consider V being non trivial RealLinearSpace such that
A2: 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 by Th22;
reconsider V as up-3-dimensional RealLinearSpace by A2,Lm42;
take CS = ProjectiveSpace(V);
thus CS is strict Fanoian Desarguesian Pappian;
ex CS being CollProjectiveSpace st CS = ProjectiveSpace(V) & CS is
up-3-dimensional at_most-3-dimensional by A2,Th34;
hence thesis;
end;
end;
definition
mode CollProjectivePlane is 2-dimensional CollProjectiveSpace;
end;
theorem
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 are_collinear & q,q1,r
are_collinear)
proof
let CS be non empty CollStr;
thus CS is 2-dimensional CollProjectiveSpace implies 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 are_collinear & q,q1,r are_collinear by Def14;
assume that
A1: CS is at_least_3rank proper CollSp and
A2: for p,p1,q,q1 being Element of CS ex r being Element of CS st p,p1,r
are_collinear & q,q1,r are_collinear;
CS is Vebleian
by A2;
hence thesis by A1,A2,Def14;
end;