Copyright (c) 1989 Association of Mizar Users
environ
vocabulary VECTSP_1, BINOP_1, FUNCT_1, RELAT_1, SYMSP_1, RLVECT_1, ARYTM_1,
ORTSP_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, DOMAIN_1,
BINOP_1, STRUCT_0, RLVECT_1, VECTSP_1, RELSET_1, SYMSP_1;
constructors DOMAIN_1, BINOP_1, SYMSP_1, MEMBERED, XBOOLE_0;
clusters SYMSP_1, STRUCT_0, RELSET_1, SUBSET_1, VECTSP_1, MEMBERED, ZFMISC_1,
XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI;
theorems BINOP_1, VECTSP_1, TARSKI, RELSET_1, ZFMISC_1, SYMSP_1, RLVECT_1;
schemes BINOP_1, FUNCT_2, XBOOLE_0;
begin
::
:: 1. ORTHOGONAL VECTOR SPACE STRUCTURE
::
reserve F for Field;
reconsider X = {0} as non empty set;
reconsider o = 0 as Element of X by TARSKI:def 1;
deffunc F(Element of X,Element of X) = o;
consider md being BinOp of X such that
Lm1: for x,y being Element of X holds md.(x,y) = F(x,y) from BinOpLambda;
Lm2:
now let F;
set CV = [:X,X:];
defpred P[set] means ex a,b being Element of X st $1 = [a,b] & b = o;
consider mo being set such that A1:
for x being set holds x in mo iff
x in CV & P[x] from Separation;
mo c= CV
proof
let x be set;
thus thesis by A1;
end;
then reconsider mo as Relation of X by RELSET_1:def 1;
take mo;
thus for x being set holds x in mo iff
x in CV & ex a,b being Element of X
st x = [a,b] & b = o by A1;
end;
Lm3:
for mF being Function of [:(the carrier of F),(X):],(X),
mo being Relation of X
holds SymStr (# X,md,o,mF,mo #)
is Abelian add-associative right_zeroed right_complementable
proof
let mF be
Function of [:(the carrier of F),(X):],(X);
let mo be Relation of X;
set H = SymStr (# X,md,o,mF,mo #);
A1: for x,y being Element of H holds x+y = y+x
proof
let x,y be Element of H;
A2: y+x = md.(y,x) by RLVECT_1:5;
md.(x,y) = o & md.(y,x) = o by Lm1;
hence thesis by A2,RLVECT_1:5;
end;
A3: for x,y,z being Element of H holds (x+y)+z = x+(y+z)
proof
let x,y,z be Element of H;
A4: (x+y)+z = md.((x+y),z) by RLVECT_1:5;
x+(y+z) = md.(x,(y+z)) by RLVECT_1:5;
then A5: x+(y+z) = md.(x,md.(y,z)) by RLVECT_1:5;
reconsider x,y,z as Element of X;
md.(x,md.(y,z)) = o by Lm1;
hence thesis by A4,A5,Lm1;
end;
A6: for x being Element of H holds x+0.H = x
proof
let x be Element of H;
A7: x+0.H = md.(x,0.H) by RLVECT_1:5;
md.(x,0.H) = o by Lm1;
hence thesis by A7,TARSKI:def 1;
end;
for x being Element of H
ex y being Element of H st x+y = 0.H
proof
let x be Element of H;
A8: x+(-x) = md.(x,(-x)) by RLVECT_1:5;
A9: 0.H = o by RLVECT_1:def 2;
take -x;
thus thesis by A8,A9,Lm1;
end;
hence thesis by A1,A3,A6,VECTSP_1:7;
end;
Lm4:now let F;
let mF be Function of [:(the carrier of F),(X):],(X) such that
A1: for a being Element of F
for x being Element of X holds
mF.[a,x qua set] = o;
let mo be Relation of X;
let MPS be Abelian add-associative right_zeroed right_complementable
(non empty SymStr over F) such that
A2: MPS = SymStr (# X,md,o,mF,mo #);
thus MPS is VectSp-like
proof
for x,y being Element of F
for v,w being Element of MPS holds
x*(v+w) = x*v+x*w &
(x+y)*v = x*v+y*v &
(x*y)*v = x*(y*v) &
(1_ F)*v = v
proof
let x,y be Element of F;
let v,w be Element of MPS;
A3: x*(v+w) = x*v+x*w
proof
reconsider v,w as Element of MPS;
A4: v+w = md.(v,w) by A2,RLVECT_1:5;
reconsider v,w as Element of X by A2;
A5: md.(v,w) = o by Lm1;
reconsider v,w as Element of MPS;
A6: x*(v+w) = mF.(x,o) by A2,A4,A5,VECTSP_1:def 24;
mF.(x,o) = mF.[x,o] by BINOP_1:def 1;
then A7: x*(v+w) = o by A1,A6;
reconsider v as Element of MPS;
mF.(x,v) = mF.[x,v] by BINOP_1:def 1;
then A8: mF.(x,v qua set) = o by A1;
reconsider v as Element of MPS;
A9: x*v = o by A2,A8,VECTSP_1:def 24;
reconsider w as Element of MPS;
mF.(x,w) = mF.[x,w] by BINOP_1:def 1;
then A10: mF.(x,w qua set) = o by A1;
reconsider w as Element of MPS;
A11: x*w = o by A2,A10,VECTSP_1:def 24;
o = 0.MPS by A2,RLVECT_1:def 2;
hence thesis by A7,A9,A11,RLVECT_1:10;
end;
A12: (x+y)*v = x*v+y*v
proof
set z = x+y;
A13: z*v = mF.(z,v) by A2,VECTSP_1:def 24;
reconsider v as Element of MPS;
A14: mF.(z,v) = mF.[z,v] by BINOP_1:def 1;
reconsider v as Element of MPS;
A15: (x+y)*v = o by A1,A2,A13,A14;
reconsider v as Element of MPS;
mF.(x,v) = mF.[x,v] by BINOP_1:def 1;
then A16: mF.(x,v qua set) = o by A1,A2;
reconsider v as Element of MPS;
A17: x*v = o by A2,A16,VECTSP_1:def 24;
reconsider v as Element of MPS;
mF.(y,v) = mF.[y,v] by BINOP_1:def 1;
then A18: mF.(y,v qua set) = o by A1,A2;
reconsider v as Element of MPS;
A19: y*v = o by A2,A18,VECTSP_1:def 24;
o = 0.MPS by A2,RLVECT_1:def 2;
hence thesis by A15,A17,A19,RLVECT_1:10;
end;
A20: (x*y)*v = x*(y*v)
proof
set z = x*y;
A21: z*v = mF.(z,v) by A2,VECTSP_1:def 24;
reconsider v as Element of MPS;
A22: mF.(z,v) = mF.[z,v] by BINOP_1:def 1;
reconsider v as Element of MPS;
A23: (x*y)*v = o by A1,A2,A21,A22;
reconsider v as Element of MPS;
mF.(y,v) = mF.[y,v] by BINOP_1:def 1;
then A24: mF.(y,v qua set) = o by A1,A2;
reconsider v as Element of MPS;
y*v = o by A2,A24,VECTSP_1:def 24;
then A25: x*(y*v) = mF.(x,o) by A2,VECTSP_1:def 24;
mF.(x,o) = mF.[x,o] by BINOP_1:def 1;
hence thesis by A1,A23,A25;
end;
(1_ F)*v = v
proof
set one = 1_ F;
A26: one*v = mF.(one,v) by A2,VECTSP_1:def 24;
A27: mF.(one,v) = mF.[one,v] by BINOP_1:def 1;
reconsider v as Element of MPS;
mF.(one,v qua set) = o by A1,A2,A27;
hence thesis by A2,A26,TARSKI:def 1;
end;
hence thesis by A3,A12,A20;
end;
hence thesis by VECTSP_1:def 26;
end;
end;
Lm5:
now let F;
let mF be
Function of [:(the carrier of F),(X):],(X) such that
for a being Element of F
for x being Element of X holds
mF.[a,x qua set] = o;
set CV = [:X,X:];
let mo be Relation of X such that A1:
for x being set holds x in mo iff
x in CV & ex a,b being Element of X
st x = [a,b] & b = o;
let MPS be Abelian add-associative right_zeroed right_complementable
(non empty SymStr over F) such that
A2: MPS = SymStr (# X,md,o,mF,mo #);
A3: for a,b being Element of MPS holds
a _|_ b iff [a,b] in CV & ex c,d being Element of X
st [a,b] = [c,d] & d = o
proof
let a,b be Element of MPS;
a _|_ b iff [a,b] in mo by A2,SYMSP_1:def 1;
hence thesis by A1;
end;
A4: for a,b being Element of MPS holds
a _|_ b iff b = o
proof
let a,b be Element of MPS;
A5: a _|_ b implies b = o
proof
assume a _|_ b;
then ex c,d being Element of X st [a,b] = [c,d] &
d = o by A3;
hence thesis by ZFMISC_1:33;
end;
b = o implies a _|_ b
proof
assume A6: b = o;
consider c,d being Element of MPS such that A7: c = a &
d = b;
[a,b] = [c,d] by A7;
hence thesis by A2,A3,A6;
end;
hence thesis by A5;
end;
0.MPS = o by A2,TARSKI:def 1;
hence for a,b,c,d being Element of MPS
holds
(a <> 0.MPS & b <> 0.MPS &
c <> 0.MPS & d <> 0.MPS implies
(ex p being Element of MPS st
not p _|_ a & not p _|_ b & not p _|_ c & not p _|_ d)) by A2,TARSKI:def 1
;
thus for a,b being Element of MPS
for l being Element of F holds
(a _|_ b implies l*a _|_ b)
proof
let a,b be Element of MPS;
let l be Element of F;
assume a _|_ b;
then b = o by A4;
hence thesis by A4;
end;
thus for a,b,c being Element of MPS holds
(b _|_ a & c _|_ a implies b+c _|_ a)
proof
let a,b,c be Element of MPS;
assume b _|_ a & c _|_ a;
then a = o by A4;
hence thesis by A4;
end;
thus for a,b,x being Element of MPS holds
( not b _|_ a implies ex k being Element of F
st x-k*b _|_ a)
proof
let a,b,x be Element of MPS;
assume A8: not b _|_ a;
assume not thesis;
a <> o by A4,A8;
hence contradiction by A2,TARSKI:def 1;
end;
thus for a,b,c being Element of MPS holds
(a _|_ b-c & b _|_ c-a implies c _|_ a-b)
proof
let a,b,c be Element of MPS;
assume a _|_ b-c & b _|_ c-a;
assume not thesis;
then a-b <> o by A4;
hence contradiction by A2,TARSKI:def 1;
end;
end;
::
:: 2. ORTHOGONAL VECTOR SPACE
::
definition
let F;
let IT be Abelian add-associative right_zeroed right_complementable
(non empty SymStr over F);
canceled;
attr IT is OrtSp-like means
:Def2: for a,b,c,d,x being Element of IT
for l being Element of F holds
(a<>0.IT & b<>0.IT &
c <>0.IT & d<>0.IT implies
( ex p being Element of IT
st not p _|_ a & not p _|_ b & not p _|_ c & not p _|_ d)) &
(a _|_ b implies l*a _|_ b) &
( b _|_ a & c _|_ a implies b+c _|_ a ) &
(not b _|_ a implies
( ex k being Element of F st x-k*b _|_ a )) &
( a _|_ b-c & b _|_ c-a implies c _|_ a-b );
end;
definition let F;
cluster OrtSp-like VectSp-like strict
(Abelian add-associative right_zeroed right_complementable
(non empty SymStr over F));
existence
proof
deffunc F(Element of F,Element of X) = o;
consider mF being Function of [:(the carrier of F),X:],X
such that
A1: for a being Element of F
for x being Element of X holds mF.[a,x] = F(a,x) from Lambda2D;
consider mo being Relation of X such that
A2: for x being set holds x in mo iff
x in [:X,X:] & ex a,b being Element of X
st x = [a,b] & b = o by Lm2;
reconsider MPS = SymStr (# X,md,o,mF,mo #)
as Abelian add-associative right_zeroed right_complementable
(non empty SymStr over F)
by Lm3;
take MPS;
thus for a,b,c,d,x being Element of MPS
for l being Element of F holds
(a<>0.MPS & b<>0.MPS &
c <>0.MPS & d<>0.MPS implies
( ex p being Element of MPS
st not p _|_ a & not p _|_ b & not p _|_ c & not p _|_ d)) &
(a _|_ b implies l*a _|_ b) &
( b _|_ a & c _|_ a implies b+c _|_ a ) &
(not b _|_ a implies
( ex k being Element of F st x-k*b _|_ a )) &
( a _|_ b-c & b _|_ c-a implies c _|_ a-b ) by A1,A2,Lm5;
thus MPS is VectSp-like by A1,Lm4;
thus thesis;
end;
end;
definition let F;
mode OrtSp of F is OrtSp-like VectSp-like
(Abelian add-associative right_zeroed right_complementable
(non empty SymStr over F));
end;
reserve S for OrtSp of F;
reserve a,b,c,d,p,q,r,x,y,z for Element of S;
reserve k,l for Element of F;
canceled 10;
theorem
Th11: 0.S _|_ a
proof
set 0F = 0.F,0V = 0.S;
A1: now assume a _|_ a; then 0F*a _|_ a by Def2;
hence 0V _|_ a by VECTSP_1:59; end;
now assume not a _|_ a;
then consider m being Element of F
such that A2:(0V-m*a) _|_ a by Def2;
0F*(0V-m*a) _|_ a by A2,Def2;
hence 0V _|_ a by VECTSP_1:59; end;
hence thesis by A1;
end;
theorem
Th12: a _|_ b implies b _|_ a
proof
set 0V = 0.S;
assume a _|_ b;
then a _|_ (-(-b)) by RLVECT_1:30;
then a _|_ 0V+(-(-b)) by RLVECT_1:10;
then A1: a _|_ 0V-(-b) by RLVECT_1:def 11;
0V _|_ -b-a by Th11;
then -b _|_ a-0V by A1,Def2;
then -b _|_ a by VECTSP_1:65;
then (-1_ F)*(-b) _|_ a by Def2;
then -(-b) _|_ a by VECTSP_1:59;
hence thesis by RLVECT_1:30;
end;
theorem
Th13: not a _|_ b & c+a _|_ b implies not c _|_ b
proof
assume A1:not a _|_ b & c+a _|_ b;
assume not thesis;
then (-1_ F)*c _|_ b by Def2;
then -c _|_ b by VECTSP_1:59;
then -c+(c+a) _|_ b by A1,Def2;
then (c+(-c))+a _|_ b by RLVECT_1:def 6;
then 0.S+a _|_ b by RLVECT_1:16;
hence contradiction by A1,RLVECT_1:10;
end;
theorem
Th14: not b _|_ a & c _|_ a implies not b+c _|_ a
proof
assume A1:not b _|_ a & c _|_ a;
assume A2:not thesis;
(-1_ F)*c _|_ a by A1,Def2;
then -c _|_ a by VECTSP_1:59;
then (b+c)+(-c) _|_ a by A2,Def2;
then b+(c+(-c)) _|_ a by RLVECT_1:def 6;
then b+0.S _|_ a by RLVECT_1:16;
hence contradiction by A1,RLVECT_1:10;
end;
theorem
Th15: not b _|_ a & not l=0.F implies not l*b _|_ a & not b _|_ l*a
proof
set 1F = 1_ F;
assume A1: not b _|_ a & not l=0.F;
A2:now assume A3:l*b _|_ a;
consider k such that A4:l*k=1F by A1,VECTSP_1:def 20;
k*(l*b) _|_ a by A3,Def2;
then 1F*b _|_ a by A4,VECTSP_1:def 26;
hence contradiction by A1,VECTSP_1:def 26;
end;
now assume b _|_ l*a;
then A5:l*a _|_ b by Th12;
consider k such that A6:l*k=1F by A1,VECTSP_1:def 20;
k*(l*a) _|_ b by A5,Def2;
then 1F*a _|_ b by A6,VECTSP_1:def 26;
then a _|_ b by VECTSP_1:def 26;
hence contradiction by A1,Th12;
end;
hence thesis by A2;
end;
theorem
Th16: a _|_ b implies -a _|_ b
proof
assume a _|_ b;
then (-1_ F)*a _|_ b by Def2;
hence thesis by VECTSP_1:59;
end;
canceled 2;
theorem
Th19: a-b _|_ d & a-c _|_ d implies b-c _|_ d
proof
assume a-b _|_ d & a-c _|_ d;
then -(a-b) _|_ d & a-c _|_ d by Th16;
then -a+b _|_ d & a-c _|_ d by VECTSP_1:64;
then b+(-a)+(a-c) _|_ d by Def2;
then b+((-a)+(a-c)) _|_ d by RLVECT_1:def 6;
then b+(-a+(a+(-c))) _|_ d by RLVECT_1:def 11;
then b+((-a+a)+(-c)) _|_ d by RLVECT_1:def 6;
then b+((0.S)+(-c)) _|_ d by RLVECT_1:16;
then b+(-c) _|_ d by RLVECT_1:10;
hence thesis by RLVECT_1:def 11;
end;
theorem
Th20: not b _|_ a & x-k*b _|_ a & x-l*b _|_ a implies k = l
proof
set 1F = 1_ F;
assume A1:not b _|_ a & x-k*b _|_ a & x-l*b _|_ a;
assume A2:not thesis;
k*b-l*b _|_ a by A1,Th19;
then k*b+(-l*b) _|_ a by RLVECT_1:def 11;
then k*b+((-1F)*(l*b)) _|_ a by VECTSP_1:59;
then k*b+(((-1F)*l)*b) _|_ a by VECTSP_1:def 26;
then k*b+(-(l*(1F)))*b _|_ a by VECTSP_1:41;
then k*b+(-l)*b _|_ a by VECTSP_1:def 19;
then (k+(-l))*b _|_ a by VECTSP_1:def 26;
then (k+(-l))"*((k+(-l))*b) _|_ a by Def2;
then A3: ((k+(-l))"*(k+(-l)))*b _|_ a by VECTSP_1:def 26;
k-l<>0.F by A2,RLVECT_1:35;
then k+(-l)<>0.F by RLVECT_1:def 11;
then (1F)*b _|_ a by A3,VECTSP_1:def 22;
hence contradiction by A1,VECTSP_1:def 26;
end;
theorem
Th21: a _|_ a & b _|_ b implies a+b _|_ a-b
proof
set 0V = 0.S;
assume A1: a _|_ a & b _|_ b;
then (-1_ F)*a _|_ a by Def2;
then -a _|_ a by VECTSP_1:59;
then a _|_ -a by Th12;
then a _|_ 0V+(-a) by RLVECT_1:10;
then a _|_ (b+(-b))+(-a) by RLVECT_1:16;
then a _|_ b+(-b+(-a)) by RLVECT_1:def 6;
then a _|_ b+(-b-a) by RLVECT_1:def 11;
then a _|_ b+(-(b+a)) by VECTSP_1:64;
then A2: a _|_ b-(a+b) by RLVECT_1:def 11;
b _|_ b+0V by A1,RLVECT_1:10;
then b _|_ b+(a+(-a)) by RLVECT_1:16;
then b _|_ (b+a)+(-a) by RLVECT_1:def 6;
then b _|_ (a+b)-a by RLVECT_1:def 11;
hence thesis by A2,Def2;
end;
theorem
(1_ F+1_ F <> 0.F & (ex a st a<>0.S)) implies (ex b st not b _|_ b)
proof
set 1F = 1_ F,0V = 0.S;
assume that A1: 1_ F+1_ F<>0.F and A2: ex a st a<>0.S;
consider a such that A3: a<>0.S by A2;
assume A4: not thesis;
A5: for c,d holds c _|_ d
proof
let c,d;
A6: d _|_ d & c _|_ c by A4;
A7: d+c _|_ d+c by A4;
d+c _|_ d-c by A6,Th21;
then d-c _|_ d+c by Th12;
then (d+c)+(d-c) _|_ d+c by A7,Def2;
then (d+c)+((-c)+d) _|_ d+c by RLVECT_1:def 11;
then ((d+c)+(-c))+d _|_ d+c by RLVECT_1:def 6;
then (d+(c+(-c)))+d _|_ d+c by RLVECT_1:def 6;
then (d+0V)+d _|_ d+c by RLVECT_1:16;
then d+d _|_ d+c by RLVECT_1:10;
then (1F)*d+d _|_ d+c by VECTSP_1:def 26;
then (1F)*d+(1F)*d _|_ d+c by VECTSP_1:def 26;
then (1F+1F)*d _|_ d+c by VECTSP_1:def 26;
then (1F+1F)"*((1F+1F)*d) _|_ d+c by Def2;
then ((1F+1F)"*(1F+1F))*d _|_ d+c by VECTSP_1:def 26;
then (1F)*d _|_ d+c by A1,VECTSP_1:def 22;
then d _|_ d+c by VECTSP_1:def 26;
then A8: d+c _|_ d by Th12;
-d _|_ d by A6,Th16;
then -d+(d+c) _|_ d by A8,Def2;
then (-d+d)+c _|_ d by RLVECT_1:def 6;
then 0V+c _|_ d by RLVECT_1:16;
hence thesis by RLVECT_1:10;
end;
ex c st not c _|_ a & not c _|_ a & not c _|_ a & not c _|_ a by A3,Def2;
hence contradiction by A5;
end;
::
:: 5. ORTHOGONAL PROJECTION
::
definition let F,S,a,b,x;
assume A1: not b _|_ a;
canceled 3;
func ProJ(a,b,x) -> Element of F means
:Def6: for l being Element of F st x-l*b _|_ a
holds it = l;
existence
proof
consider k being Element of F such that
A2: x-k*b _|_ a by A1,Def2;
take k;
let l be Element of F;
assume x-l*b _|_ a;
hence thesis by A1,A2,Th20;
end;
uniqueness
proof
let l1,l2 be Element of F such that
A3: for l being Element of F st x-l*b _|_ a
holds l1 = l and
A4: for l being Element of F st x-l*b _|_ a
holds l2 = l;
consider k being Element of F such that
A5: x-k*b _|_ a by A1,Def2;
l1 = k by A3,A5;
hence thesis by A4,A5;
end;
end;
canceled;
theorem
Th24: not b _|_ a implies x-ProJ(a,b,x)*b _|_ a
proof
assume A1: not b _|_ a;
then ex l being Element of F st x-l*b _|_ a by Def2;
hence thesis by A1,Def6;
end;
theorem
Th25: not b _|_ a implies ProJ(a,b,l*x) = l*ProJ(a,b,x)
proof
assume A1: not b _|_ a;
set L = x-ProJ(a,b,x)*b;
A2: L _|_ a by A1,Th24;
l*L = l*x-l*(ProJ(a,b,x)*b) by VECTSP_1:70
.= l*x-(l*ProJ(a,b,x))*b by VECTSP_1:def 26;
then A3: l*x-(l*ProJ(a,b,x))*b _|_ a by A2,Def2;
l*x - ProJ(a,b,l*x)*b _|_ a by A1,Th24;
hence thesis by A1,A3,Th20;
end;
theorem
Th26: not b _|_ a implies ProJ(a,b,x+y) = ProJ(a,b,x) + ProJ(a,b,y)
proof
set 1F = 1_ F;
assume A1: not b _|_ a;
then A2: x-ProJ(a,b,x)*b _|_ a & y-ProJ(a,b,y)*b _|_ a by Th24;
set L = (x-ProJ(a,b,x)*b)+(y-ProJ(a,b,y)*b);
A3: now thus L = (x+(-ProJ(a,b,x)*b))+(y-ProJ(a,b,y)*b) by RLVECT_1:def 11
.= (x+(-ProJ(a,b,x)*b))+(y+(-ProJ(a,b,y)*b)) by RLVECT_1:def 11
.= (((-ProJ(a,b,x)*b)+x)+y)+(-ProJ(a,b,y)*b) by RLVECT_1:def 6
.= ((x+y)+(-ProJ(a,b,x)*b))+(-ProJ(a,b,y)*b) by RLVECT_1:def 6
.= (x+y)+((-ProJ(a,b,x)*b)+(-ProJ(a,b,y)*b)) by RLVECT_1:def 6
.= (x+y)+((1F)*(-ProJ(a,b,x)*b)+(-ProJ(a,b,y)*b)) by VECTSP_1:def 26
.= (x+y)+((1F)*(-ProJ(a,b,x)*b)+(1F)*(-ProJ
(a,b,y)*b)) by VECTSP_1:def 26
.= (x+y)+((1F)*((-ProJ(a,b,x))*b)+(1F)*(-ProJ(a,b,y)*b)) by VECTSP_1:68
.= (x+y)+((1F)*((-ProJ(a,b,x))*b)+(1F)*((-ProJ
(a,b,y))*b)) by VECTSP_1:68
.= (x+y)+(((1F)*(-ProJ(a,b,x)))*b+(1F)*((-ProJ
(a,b,y))*b)) by VECTSP_1:def 26
.= (x+y)+(((-ProJ(a,b,x))*(1F))*b+((1F)*(-ProJ(a,b,y)))*b) by VECTSP_1:
def 26
.= (x+y)+((-ProJ(a,b,x))*b+((-ProJ(a,b,y))*(1F))*b) by VECTSP_1:def 19
.= (x+y)+((-ProJ(a,b,x))*b+(-ProJ(a,b,y))*b) by VECTSP_1:def 19
.= (x+y)+((-ProJ(a,b,x))+(-ProJ(a,b,y)))*b by VECTSP_1:def 26
.= (x+y)+(-(ProJ(a,b,x)+ProJ(a,b,y)))*b by RLVECT_1:45
.= (x+y)-(ProJ(a,b,x)+ProJ(a,b,y))*b by VECTSP_1:68; end;
A4: L _|_ a by A2,Def2;
(x+y)-ProJ(a,b,x+y)*b _|_ a by A1,Th24;
hence thesis by A1,A3,A4,Th20;
end;
theorem
not b _|_ a & l <> 0.F implies ProJ(a,l*b,x) = l"*ProJ(a,b,x)
proof
assume A1: not b _|_ a & l <> 0.F;
then A2: x-ProJ(a,b,x)*b _|_ a by Th24;
A3: not l*b _|_ a by A1,Th15;
set L = x-ProJ(a,l*b,x)*(l*b);
A4: L _|_ a by A3,Th24;
L = x-(ProJ(a,l*b,x)*l)*b by VECTSP_1:def 26;
then ProJ(a,b,x)*l" = (ProJ(a,l*b,x)*l)*l" by A1,A2,A4,Th20;
then ProJ(a,b,x)*l" = ProJ(a,l*b,x)*(l*l") by VECTSP_1:def 16;
then l"*ProJ(a,b,x) = ProJ(a,l*b,x)*(1_ F) by A1,VECTSP_1:def 22;
hence thesis by VECTSP_1:def 19;
end;
theorem
Th28: not b _|_ a & l <> 0.F implies ProJ(l*a,b,x) = ProJ(a,b,x)
proof
assume A1: not b _|_ a & l <> 0.F;
then not b _|_ l*a by Th15;
then A2: x-ProJ(a,b,x)*b _|_ a & x-ProJ(l*a,b,x)*b _|_ l*a by A1,Th24;
then l*a _|_ x-ProJ(l*a,b,x)*b by Th12;
then l"*(l*a) _|_ x-ProJ(l*a,b,x)*b by Def2;
then (l"*l)*a _|_ x-ProJ(l*a,b,x)*b by VECTSP_1:def 26;
then 1_ F*a _|_ x-ProJ(l*a,b,x)*b by A1,VECTSP_1:def 22;
then a _|_ x-ProJ(l*a,b,x)*b by VECTSP_1:def 26;
then x-ProJ(l*a,b,x)*b _|_ a by Th12;
hence thesis by A1,A2,Th20;
end;
theorem
not b _|_ a & p _|_ a implies
ProJ(a,b+p,c) = ProJ(a,b,c) & ProJ(a,b,c+p) = ProJ(a,b,c)
proof
set 0V = 0.S;
assume A1: not b _|_ a & p _|_ a;
then not b+p _|_ a by Th14;
then A2: c-ProJ(a,b,c)*b _|_ a & c+p-ProJ(a,b,c+p)*b _|_ a &
c-ProJ(a,b+p,c)*(b+p) _|_ a by A1,Th24;
A3: ProJ(a,b+p,c)*p _|_ a by A1,Def2;
A4: -p _|_ a by A1,Th16;
c-(ProJ(a,b+p,c)*b+ProJ(a,b+p,c)*p) _|_ a by A2,VECTSP_1:def 26;
then c-ProJ(a,b+p,c)*b-ProJ(a,b+p,c)*p _|_ a by VECTSP_1:64;
then c-ProJ(a,b+p,c)*b-ProJ(a,b+p,c)*p+ProJ(a,b+p,c)*p _|_ a by A3,Def2;
then c+(-ProJ(a,b+p,c)*b)-ProJ(a,b+p,c)*p+ProJ(a,b+p,c)*p _|_
a by RLVECT_1:def 11;
then c+(-ProJ(a,b+p,c)*b)+(-ProJ(a,b+p,c)*p)+ProJ(a,b+p,c)*p _|_
a by RLVECT_1:def 11;
then c+(-ProJ(a,b+p,c)*b)+((-ProJ(a,b+p,c)*p)+ProJ(a,b+p,c)*p) _|_
a by RLVECT_1:def 6;
then c+(-ProJ(a,b+p,c)*b)+0V _|_ a by RLVECT_1:16;
then c+(-ProJ(a,b+p,c)*b) _|_ a by RLVECT_1:10;
then A5: c-ProJ(a,b+p,c)*b _|_ a by RLVECT_1:def 11;
-p+(p+c-ProJ(a,b,c+p)*b) _|_ a by A2,A4,Def2;
then -p+(p+c+(-ProJ(a,b,c+p)*b)) _|_ a by RLVECT_1:def 11;
then -p+(p+(c+(-ProJ(a,b,c+p)*b))) _|_ a by RLVECT_1:def 6;
then (-p+p)+(c+(-ProJ(a,b,c+p)*b)) _|_ a by RLVECT_1:def 6;
then 0V+(c+(-ProJ(a,b,c+p)*b)) _|_ a by RLVECT_1:16;
then c+(-ProJ(a,b,c+p)*b) _|_ a by RLVECT_1:10;
then c-ProJ(a,b,c+p)*b _|_ a by RLVECT_1:def 11;
hence thesis by A1,A2,A5,Th20;
end;
theorem
not b _|_ a & p _|_ b & p _|_ c implies ProJ(a+p,b,c) = ProJ(a,b,c)
proof
assume A1: not b _|_ a & p _|_ b & p _|_ c;
then not a _|_ b by Th12;
then not a+p _|_ b by A1,Th14;
then A2: not b _|_ a+p by Th12;
then A3: c-ProJ(a,b,c)*b _|_ a & c-ProJ(a+p,b,c)*b _|_ a+p by A1,Th24;
c _|_ p & b _|_ p by A1,Th12;
then c _|_ p & ProJ(a,b,c)*b _|_ p by Def2;
then c _|_ p & -(ProJ(a,b,c)*b) _|_ p by Th16;
then c+(-(ProJ(a,b,c)*b)) _|_ p by Def2;
then c-ProJ(a,b,c)*b _|_ p by RLVECT_1:def 11;
then A4: p _|_ c-ProJ(a,b,c)*b by Th12;
a _|_ c-ProJ(a,b,c)*b by A3,Th12;
then a+p _|_ c-ProJ(a,b,c)*b by A4,Def2;
then c-ProJ(a,b,c)*b _|_ a+p by Th12;
hence thesis by A2,A3,Th20;
end;
theorem
Th31: not b _|_ a & c-b _|_ a implies ProJ(a,b,c) = 1_ F
proof
assume A1: not b _|_ a & c-b _|_ a;
then A2: c-(1_ F)*b _|_ a by VECTSP_1:def 26;
c-ProJ(a,b,c)*b _|_ a by A1,Th24;
hence thesis by A1,A2,Th20;
end;
theorem
Th32: not b _|_ a implies ProJ(a,b,b) = 1_ F
proof
assume A1: not b _|_ a;
b+(-b) = 0.S by RLVECT_1:16;
then b-b = 0.S by RLVECT_1:def 11;
then b-b _|_ a by Th11;
hence thesis by A1,Th31;
end;
theorem
Th33: not b _|_ a implies ( x _|_ a iff ProJ(a,b,x) = 0.F )
proof
set 0F = 0.F;
set 0V = 0.S;
A1: now assume A2: not b _|_ a & x _|_ a;
then A3: x-ProJ(a,b,x)*b _|_ a by Th24;
x+0V _|_ a by A2,RLVECT_1:10;
then x+(-0V) _|_ a by RLVECT_1:25;
then x+(-(0F*b)) _|_ a by VECTSP_1:59;
then x-0F*b _|_ a by RLVECT_1:def 11;
hence ProJ(a,b,x) = 0.F by A2,A3,Th20;
end;
now assume not b _|_ a & ProJ(a,b,x) = 0.F;
then x-0F*b _|_ a by Th24;
then x-0V _|_ a by VECTSP_1:59;
then x+(-0V) _|_ a by RLVECT_1:def 11;
then x+0V _|_ a by RLVECT_1:25;
hence x _|_ a by RLVECT_1:10;
end;
hence thesis by A1;
end;
theorem
Th34: not b _|_ a & not q _|_ a implies ProJ(a,b,p)*ProJ(a,b,q)" = ProJ(a,q,p)
proof
assume A1: not b _|_ a & not q _|_ a;
then A2: p-ProJ(a,b,p)*b _|_ a & ProJ(a,q,p)*q-ProJ(a,b,ProJ(a,q,p)*q)*
b _|_ a &
p-ProJ(a,q,p)*q _|_ a by Th24;
then (p-ProJ(a,q,p)*q)+(ProJ(a,q,p)*q-ProJ(a,b,ProJ(a,q,p)*q)*b) _|_ a
by Def2;
then (p+(-ProJ(a,q,p)*q))+(ProJ(a,q,p)*q-(ProJ(a,b,ProJ(a,q,p)*q)*b)) _|_
a by RLVECT_1:def 11;
then (p+(-ProJ(a,q,p)*q))+(ProJ(a,q,p)*q+(-(ProJ(a,b,ProJ(a,q,p)*q))*b))
_|_ a by RLVECT_1:def 11;
then ((p+(-ProJ(a,q,p)*q))+(ProJ(a,q,p)*q))+(-(ProJ(a,b,ProJ(a,q,p)*q))*b)
_|_ a by RLVECT_1:def 6;
then (p+((-ProJ(a,q,p)*q)+(ProJ(a,q,p)*q))+(-(ProJ(a,b,ProJ(a,q,p)*q))*b))
_|_ a by RLVECT_1:def 6;
then p+0.S+(-(ProJ(a,b,ProJ(a,q,p)*q))*b) _|_ a by RLVECT_1:16;
then p+(-(ProJ(a,b,ProJ(a,q,p)*q))*b) _|_ a by RLVECT_1:10;
then p-(ProJ(a,b,ProJ(a,q,p)*q)*b) _|_ a by RLVECT_1:def 11;
then p-(ProJ(a,q,p)*ProJ(a,b,q))*b _|_ a by A1,Th25;
then A3: ProJ(a,q,p)*ProJ(a,b,q) = ProJ(a,b,p) by A1,A2,Th20;
A4: ProJ(a,b,q) <> 0.F by A1,Th33;
ProJ(a,q,p)*(ProJ(a,b,q)*ProJ(a,b,q)") = ProJ(a,b,p)*ProJ
(a,b,q)" by A3,VECTSP_1:def 16;
then ProJ(a,q,p)*1_ F = ProJ(a,b,p)*ProJ(a,b,q)" by A4,VECTSP_1:def 22;
hence thesis by VECTSP_1:def 19;
end;
theorem
Th35: not b _|_ a & not c _|_ a implies ProJ(a,b,c) = ProJ(a,c,b)"
proof
set 1F = 1_ F;
set 0F = 0.F;
assume A1: not b _|_ a & not c _|_ a;
then ProJ(a,b,b)*ProJ(a,b,c)" = ProJ(a,c,b) by Th34;
then ProJ(a,b,c)"*1F = ProJ(a,c,b) by A1,Th32;
then A2: ProJ(a,b,c)" = ProJ(a,c,b) by VECTSP_1:def 19;
A3: ProJ(a,c,b) <> 0F & ProJ(a,b,c) <> 0F by A1,Th33;
then 1F = ProJ(a,c,b)*ProJ(a,b,c) by A2,VECTSP_1:def 22;
then ProJ(a,c,b)" = ProJ(a,c,b)"*(ProJ(a,c,b)*ProJ(a,b,c)) by VECTSP_1:def 19
.= (ProJ(a,c,b)"*ProJ(a,c,b))*ProJ(a,b,c) by VECTSP_1:def 16
.= ProJ(a,b,c)*1F by A3,VECTSP_1:def 22;
hence thesis by VECTSP_1:def 19;
end;
theorem
Th36: not b _|_ a & b _|_ c+a implies ProJ(a,b,c) = -ProJ(c,b,a)
proof
set 1F = 1_ F;
assume A1: not b _|_ a & b _|_ c+a;
then not a _|_ b & c+a _|_ b by Th12;
then not c _|_ b by Th13;
then A2: not b _|_ c by Th12;
c-ProJ(a,b,c)*b _|_ a by A1,Th24;
then (-ProJ(a,b,c))*b+c _|_ a by VECTSP_1:68;
then (-1F)*((-ProJ(a,b,c))*b+c) _|_ a by Def2;
then (-1F)*((-ProJ(a,b,c))*b)+(-1F)*c _|_ a by VECTSP_1:def 26;
then ((-1F)*(-ProJ(a,b,c)))*b+(-1F)*c _|_ a by VECTSP_1:def 26;
then (ProJ(a,b,c)*(1F))*b+(-1F)*c _|_ a by VECTSP_1:42;
then ProJ(a,b,c)*b+(-1F)*c _|_ a by VECTSP_1:def 19;
then ProJ(a,b,c)*b+(-c) _|_ a by VECTSP_1:59;
then ProJ(a,b,c)*b-c _|_ a by RLVECT_1:def 11;
then a _|_ ProJ(a,b,c)*b-c by Th12;
then A3: -a _|_ ProJ(a,b,c)*b-c by Th16;
ProJ(a,b,c)*b _|_ c+a by A1,Def2;
then ProJ(a,b,c)*b _|_ c+(-(-a)) by RLVECT_1:30;
then ProJ(a,b,c)*b _|_ c-(-a) by RLVECT_1:def 11;
then c _|_ -a-ProJ(a,b,c)*b by A3,Def2;
then A4: -a-ProJ(a,b,c)*b _|_ c by Th12;
-a-ProJ(c,b,-a)*b _|_ c by A2,Th24;
then ProJ(a,b,c) = ProJ(c,b,-a) by A2,A4,Th20
.= ProJ(c,b,(-1F)*a) by VECTSP_1:59
.= (-1F)*ProJ(c,b,a) by A2,Th25
.= -(ProJ(c,b,a)*(1F)) by VECTSP_1:41;
hence thesis by VECTSP_1:def 19;
end;
theorem
Th37:not a _|_ b & not c _|_ b implies ProJ(c,b,a) = ProJ(b,a,c)"*ProJ(a,b,c)
proof
set 1F = 1_ F;
assume A1: not a _|_ b & not c _|_ b;
then A2: ProJ(b,a,c) <> 0.F by Th33;
A3: ProJ(b,a,c) <> 0.F by A1,Th33;
(-1F)*(ProJ(b,a,c)"*ProJ(b,a,c)) = (-1F)*(1F) by A2,VECTSP_1:def 22;
then ((-1F)*ProJ(b,a,c)")*ProJ(b,a,c) = (-1F)*(1F) by VECTSP_1:def 16;
then ((-1F)*ProJ(b,a,c)")*ProJ(b,a,c) = (-1F) by VECTSP_1:def 19;
then (-(ProJ(b,a,c)"*(1F)))*ProJ(b,a,c) = -1F by VECTSP_1:41;
then (-ProJ(b,a,c)")*ProJ(b,a,c) = -1F by VECTSP_1:def 19;
then ProJ(b,a,(-ProJ(b,a,c)")*c) = -1F by A1,Th25;
then (-ProJ(b,a,c)")*c-(-1F)*a _|_ b by A1,Th24;
then (-ProJ(b,a,c)")*c-(-a) _|_ b by VECTSP_1:59;
then (-ProJ(b,a,c)")*c+(-(-(a))) _|_ b by RLVECT_1:def 11;
then (-ProJ(b,a,c)")*c+a _|_ b by RLVECT_1:30;
then A4: b _|_ (-ProJ(b,a,c)")*c+a by Th12;
A5:not b _|_ a & not b _|_ c by A1,Th12;
then A6: ProJ(a,b,(-ProJ(b,a,c)")*c) = -ProJ((-ProJ
(b,a,c)")*c,b,a) by A4,Th36;
-ProJ(b,a,c)" <> 0.F by A3,VECTSP_1:74;
then ProJ(a,b,(-ProJ(b,a,c)")*c) = -ProJ(c,b,a) by A5,A6,Th28;
then (-ProJ(b,a,c)")*ProJ(a,b,c) = -ProJ(c,b,a) by A5,Th25;
then (-(ProJ(b,a,c)"*ProJ(a,b,c)))*(-1F) = (-ProJ
(c,b,a))*(-1F) by VECTSP_1:41;
then (ProJ(b,a,c)"*ProJ(a,b,c))*(1F) = (-ProJ(c,b,a))*(-1F) by VECTSP_1:42;
then (ProJ(b,a,c)"*ProJ(a,b,c))*(1F) = ProJ(c,b,a)*(1F) by VECTSP_1:42;
then ProJ(b,a,c)"*ProJ(a,b,c) = ProJ(c,b,a)*(1F) by VECTSP_1:def 19;
hence thesis by VECTSP_1:def 19;
end;
theorem
Th38: not p _|_ a & not p _|_ x & not q _|_ a & not q _|_ x implies
ProJ(a,q,p)*ProJ(p,a,x) = ProJ(q,a,x)*ProJ(x,q,p)
proof
set 0F = 0.F;
set 1F = 1_ F;
assume A1: not p _|_ a & not p _|_ x & not q _|_ a & not q _|_ x;
then A2: not a _|_ p & not x _|_ p & not a _|_ q & not x _|_ q by Th12;
then p <> 0.S & q <> 0.S & a <> 0.S & x <> 0.S by A1,Th11;
then consider r such that
A3: not r _|_ p & not r _|_ q & not r _|_ a & not r _|_ x by Def2;
A4: not p _|_ r & not q _|_ r & not a _|_ r & not x _|_ r by A3,Th12;
then A5: ProJ(r,q,p) <> 0F by Th33;
ProJ(a,q,p)*ProJ(p,a,x)*ProJ(q,a,x)" =
(ProJ(a,r,p)*ProJ(a,r,q)")*ProJ(p,a,x)*ProJ(q,a,x)" by A1,A3,Th34
.= (ProJ(a,r,p)*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,r,a)")*ProJ
(q,a,x)" by A2,A3,Th34
.= (ProJ(a,r,p)*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,r,a)")*ProJ
(q,x,a) by A2,Th35
.= (ProJ(a,r,p)*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,r,a)")*(ProJ(q,r,a)*ProJ
(q,r,x)")
by A2,A3,Th34
.= (ProJ(a,p,r)"*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,r,a)")*(ProJ(q,r,a)*ProJ
(q,r,x)")
by A1,A3,Th35
.= (ProJ(a,p,r)"*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,a,r))*(ProJ(q,r,a)*ProJ
(q,r,x)")
by A2,A3,Th35
.= (ProJ(a,p,r)"*ProJ(a,q,r))*(ProJ(p,r,x)*ProJ(p,a,r))*(ProJ(q,r,a)*ProJ
(q,r,x)")
by A1,A3,Th35
.= (ProJ(a,p,r)"*ProJ(a,q,r))*(ProJ(p,r,x)*ProJ(p,a,r))*(ProJ(q,a,r)"*ProJ
(q,r,x)")
by A2,A3,Th35
.= (ProJ(a,p,r)"*ProJ(a,q,r))*(ProJ(p,x,r)"*ProJ(p,a,r))*(ProJ(q,a,r)"*ProJ
(q,r,x)")
by A2,A3,Th35
.= (ProJ(p,x,r)"*ProJ(p,a,r))*(ProJ(a,p,r)"*ProJ(a,q,r))*(ProJ(q,a,r)"*ProJ
(q,x,r)) by A2,A3,Th35
.= ProJ(p,x,r)"*((ProJ(a,p,r)"*ProJ(a,q,r))*ProJ(p,a,r))*(ProJ(q,a,r)"*ProJ
(q,x,r)) by VECTSP_1:def 16
.= ProJ(p,x,r)"*((ProJ(a,p,r)"*ProJ(p,a,r))*ProJ(a,q,r))*(ProJ(q,a,r)"*ProJ
(q,x,r))
by VECTSP_1:def 16
.= ProJ(p,x,r)"*(ProJ(r,a,p)*ProJ(a,q,r))*(ProJ(q,a,r)"*ProJ
(q,x,r)) by A1,A3,Th37
.= (ProJ(p,x,r)"*ProJ(r,a,p))*ProJ(a,q,r)*(ProJ(q,a,r)"*ProJ
(q,x,r)) by VECTSP_1:def 16
.= (ProJ(p,x,r)"*ProJ(r,a,p))*(ProJ(a,q,r)*(ProJ(q,a,r)"*ProJ
(q,x,r))) by VECTSP_1:def 16
.= (ProJ(p,x,r)"*ProJ(r,a,p))*((ProJ(q,a,r)"*ProJ(a,q,r))*ProJ(q,x,r)) by
VECTSP_1:def 16
.= (ProJ(p,x,r)"*ProJ(r,a,p))*(ProJ(r,q,a)*ProJ(q,x,r)) by A2,A3,Th37
.= ProJ(p,x,r)"*(ProJ(r,a,p)*(ProJ(r,q,a)*ProJ(q,x,r))) by VECTSP_1:def 16
.= ProJ(p,x,r)"*((ProJ(r,a,p)*ProJ(r,q,a))*ProJ(q,x,r)) by VECTSP_1:def 16
.= ProJ(p,x,r)"*((ProJ(r,a,p)*ProJ(r,a,q)")*ProJ(q,x,r)) by A4,Th35
.= ProJ(p,x,r)"*(ProJ(r,q,p)*ProJ(q,x,r)) by A4,Th34
.= ProJ(p,r,x)*(ProJ(r,q,p)*ProJ(q,x,r)) by A2,A3,Th35
.= (ProJ(r,x,p)"*ProJ(x,r,p))*(ProJ(r,q,p)*ProJ(q,x,r)) by A4,Th37
.= (ProJ(r,x,p)"*ProJ(x,r,p))*(ProJ(r,q,p)*(ProJ(x,r,q)"*ProJ
(r,x,q))) by A1,A3,Th37
.= (ProJ(r,x,p)"*ProJ(x,r,p))*(ProJ(r,x,q)*(ProJ(r,q,p)*ProJ(x,r,q)")) by
VECTSP_1:def 16
.= ((ProJ(x,r,p)*ProJ(r,x,p)")*ProJ(r,x,q))*(ProJ(r,q,p)*ProJ(x,r,q)") by
VECTSP_1:def 16
.= (ProJ(x,r,p)*(ProJ(r,x,q)*ProJ(r,x,p)"))*(ProJ(r,q,p)*ProJ(x,r,q)") by
VECTSP_1:def 16
.= (ProJ(x,r,p)*ProJ(r,p,q))*(ProJ(r,q,p)*ProJ(x,r,q)") by A4,Th34
.= ProJ(x,r,p)*(ProJ(r,p,q)*(ProJ(r,q,p)*ProJ(x,r,q)")) by VECTSP_1:def 16
.= ProJ(x,r,p)*((ProJ(r,p,q)*ProJ(r,q,p))*ProJ(x,r,q)") by VECTSP_1:def 16
.= ProJ(x,r,p)*((ProJ(r,q,p)"*ProJ(r,q,p))*ProJ(x,r,q)") by A4,Th35
.= ProJ(x,r,p)*(ProJ(x,r,q)"*(1F)) by A5,VECTSP_1:def 22
.= ProJ(x,r,p)*ProJ(x,r,q)" by VECTSP_1:def 19
.= ProJ(x,q,p) by A1,A3,Th34;
then A6: (ProJ(q,a,x)*ProJ(q,a,x)")*(ProJ(a,q,p)*ProJ(p,a,x)) =
ProJ(q,a,x)*ProJ
(x,q,p) by VECTSP_1:def 16;
ProJ(q,a,x) <> 0F by A2,Th33;
then (ProJ(a,q,p)*ProJ(p,a,x))*(1F) = ProJ(q,a,x)*ProJ
(x,q,p) by A6,VECTSP_1:def 22;
hence thesis by VECTSP_1:def 19;
end;
theorem
Th39: not p _|_ a & not p _|_ x & not q _|_ a & not q _|_ x & not b _|_ a
implies
ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = ProJ(a,b,q)*ProJ(q,a,x)*ProJ(x,q,y)
proof
set 0F = 0.F;
set 1F = 1_ F;
assume A1: not p _|_ a & not p _|_ x & not q _|_ a & not q _|_ x &
not b _|_ a;
A2: now assume y _|_ x;
then ProJ(x,p,y) = 0F & ProJ(x,q,y) = 0F by A1,Th33;
then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F &
ProJ(a,b,q)*ProJ(q,a,x)*ProJ(x,q,y) = 0F by VECTSP_1:39;
hence thesis;
end;
now assume A3: not y _|_ x;
ProJ(a,q,p)*ProJ(p,a,x) = ProJ(x,q,p)*ProJ(q,a,x) by A1,Th38;
then (ProJ(a,b,p)*ProJ(a,b,q)")*ProJ(p,a,x) = ProJ(x,q,p)*ProJ
(q,a,x) by A1,Th34;
then (ProJ(a,b,q)"*ProJ(a,b,p))*ProJ(p,a,x) =
(ProJ(x,y,p)*ProJ(x,y,q)")*ProJ(q,a,x) by A1,A3,Th34;
then ProJ(a,b,q)*(ProJ(a,b,q)"*(ProJ(a,b,p)*ProJ(p,a,x))) =
ProJ(a,b,q)*((ProJ(x,y,p)*ProJ(x,y,q)")*ProJ
(q,a,x)) by VECTSP_1:def 16;
then A4: (ProJ(a,b,q)*ProJ(a,b,q)")*(ProJ(a,b,p)*ProJ(p,a,x)) =
ProJ(a,b,q)*((ProJ(x,y,p)*ProJ(x,y,q)")*ProJ
(q,a,x)) by VECTSP_1:def 16
;
ProJ(a,b,q) <> 0F by A1,Th33;
then (ProJ(a,b,p)*ProJ(p,a,x))*(1F) =
ProJ(a,b,q)*((ProJ(x,y,p)*ProJ(x,y,q)")*ProJ
(q,a,x)) by A4,VECTSP_1:def 22;
then ProJ(a,b,p)*ProJ(p,a,x) =
ProJ(a,b,q)*((ProJ(x,y,p)*ProJ(x,y,q)")*ProJ
(q,a,x)) by VECTSP_1:def 19
;
then ProJ(a,b,p)*ProJ(p,a,x) =
ProJ(a,b,q)*((ProJ(x,y,q)"*ProJ(x,p,y)")*ProJ
(q,a,x)) by A1,A3,Th35;
then ProJ(a,b,p)*ProJ(p,a,x) =
(ProJ(a,b,q)*(ProJ(x,y,q)"*ProJ(x,p,y)"))*ProJ
(q,a,x) by VECTSP_1:def 16;
then ProJ(a,b,p)*ProJ(p,a,x) =
ProJ(q,a,x)*((ProJ(a,b,q)*ProJ(x,y,q)")*ProJ
(x,p,y)") by VECTSP_1:def 16
;
then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) =
((ProJ(q,a,x)*(ProJ(a,b,q)*ProJ(x,y,q)"))*ProJ(x,p,y)")*ProJ
(x,p,y) by VECTSP_1:def 16;
then A5: ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) =
(ProJ(q,a,x)*(ProJ(a,b,q)*ProJ(x,y,q)"))*(ProJ(x,p,y)"*ProJ
(x,p,y)) by VECTSP_1:def 16;
ProJ(x,p,y) <> 0F by A1,A3,Th33;
then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) =
(ProJ(q,a,x)*(ProJ(a,b,q)*ProJ(x,y,q)"))*(1F) by A5,VECTSP_1:def 22;
then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) =
ProJ(q,a,x)*(ProJ(a,b,q)*ProJ(x,y,q)") by VECTSP_1:def 19;
then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) =
ProJ(q,a,x)*(ProJ(a,b,q)*ProJ(x,q,y)) by A1,A3,Th35;
hence thesis by VECTSP_1:def 16;
end;
hence thesis by A2;
end;
theorem
Th40: not a _|_ p & not x _|_ p & not y _|_ p implies
ProJ(p,a,x)*ProJ(x,p,y) = ProJ(p,a,y)*ProJ(y,p,x)
proof
set 0F = 0.F;
set 1F = 1_ F;
assume A1: not a _|_ p & not x _|_ p & not y _|_ p;
then A2: not a _|_ p & not x _|_ p & not y _|_ p & not p _|_ a &
not p _|_ x & not p _|_ y by Th12;
A3: now assume y _|_ x;
then y _|_ x & x _|_ y by Th12;
then ProJ(x,p,y) = 0F & ProJ(y,p,x) = 0F by A2,Th33;
then ProJ(p,a,x)*ProJ(x,p,y) = 0F & ProJ(p,a,y)*ProJ
(y,p,x) = 0F by VECTSP_1:39;
hence thesis;
end;
now assume A4: not y _|_ x;
then A5: not y _|_ x & not x _|_ y by Th12;
ProJ(p,a,y)*ProJ(p,a,x)" = ProJ(p,x,y) by A1,Th34;
then (ProJ(p,a,y)*ProJ(p,a,x)")*ProJ(p,a,x) =
(ProJ(x,y,p)"*ProJ(y,x,p))*ProJ(p,a,x) by A2,A4,Th37;
then A6: ProJ(p,a,y)*(ProJ(p,a,x)"*ProJ(p,a,x)) =
(ProJ(x,y,p)"*ProJ(y,x,p))*ProJ(p,a,x) by VECTSP_1:def 16;
ProJ(p,a,x) <> 0F by A1,Th33;
then ProJ(p,a,y)*(1F) =
(ProJ(x,y,p)"*ProJ(y,x,p))*ProJ(p,a,x) by A6,VECTSP_1:def 22;
then ProJ(p,a,y) = (ProJ(y,x,p)*ProJ(x,y,p)")*ProJ
(p,a,x) by VECTSP_1:def 19;
then ProJ(p,a,y) = ProJ(y,x,p)*(ProJ(x,y,p)"*ProJ
(p,a,x)) by VECTSP_1:def 16;
then ProJ(y,p,x)*ProJ(p,a,y) =
ProJ(y,p,x)*(ProJ(y,p,x)"*(ProJ(x,y,p)"*ProJ(p,a,x))) by A2,A5,Th35;
then A7: ProJ(y,p,x)*ProJ(p,a,y) =
(ProJ(y,p,x)*ProJ(y,p,x)")*(ProJ(x,y,p)"*ProJ
(p,a,x)) by VECTSP_1:def 16;
ProJ(y,p,x) <> 0F by A2,A5,Th33;
then ProJ(y,p,x)*ProJ(p,a,y) = (ProJ(x,y,p)"*ProJ(p,a,x))*(1F) by A7,
VECTSP_1:def 22
.= ProJ(x,y,p)"*ProJ(p,a,x) by VECTSP_1:def 19;
hence thesis by A2,A4,Th35;
end;
hence thesis by A3;
end;
::
:: 6. BILINEAR SYMMETRIC FORM
::
definition let F,S,x,y,a,b;
assume A1: not b _|_ a;
func PProJ(a,b,x,y) -> Element of F means
:Def7: for q st not q _|_ a & not q _|_ x holds
it = ProJ(a,b,q)*ProJ(q,a,x)*ProJ(x,q,y)
if ex p st (not p _|_ a & not p _|_ x) ,
it = 0.F if for p holds p _|_ a or p _|_ x;
existence
proof
thus (ex p st not p _|_ a & not p _|_ x) implies
ex IT being Element of F st
for q st not q _|_ a & not q _|_ x holds
IT = ProJ(a,b,q)*ProJ(q,a,x)*ProJ(x,q,y)
proof given p such that A2: not p _|_ a & not p _|_ x;
take ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y);
let q; assume not q _|_ a & not q _|_ x; hence
ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = ProJ(a,b,q)*ProJ(q,a,x)*ProJ
(x,q,y) by A1,A2,Th39;
end;
thus thesis;
end;
uniqueness
proof let IT1,IT2 be Element of F;
thus (ex p st not p _|_ a & not p _|_ x) &
(for q st not q _|_ a & not q _|_ x holds
IT1 = ProJ(a,b,q)*ProJ(q,a,x)*ProJ(x,q,y)) &
(for q st not q _|_ a & not q _|_ x holds
IT2 = ProJ(a,b,q)*ProJ(q,a,x)*ProJ(x,q,y))
implies IT1 = IT2
proof
given p such that A3: not p _|_ a & not p _|_ x;
assume that
A4: for q st not q _|_ a & not q _|_ x holds
IT1 = ProJ(a,b,q)*ProJ(q,a,x)*ProJ(x,q,y) and
A5: for q st not q _|_ a & not q _|_ x holds
IT2 = ProJ(a,b,q)*ProJ(q,a,x)*ProJ(x,q,y);
consider r such that A6: not r _|_ a & not r _|_ x by A3;
IT1 = ProJ(a,b,r)*ProJ(r,a,x)*ProJ(x,r,y) by A4,A6;
hence thesis by A5,A6;
end;
thus thesis;
end;
consistency;
end;
canceled 2;
theorem
Th43: not b _|_ a & x = 0.S implies PProJ(a,b,x,y) = 0.F
proof
assume A1: not b _|_ a & x = 0.S;
for p holds p _|_ a or p _|_ x
proof
let p;
x _|_ p by A1,Th11;
hence thesis by Th12;
end;
hence thesis by A1,Def7;
end;
Lm6: x _|_ 0.S
proof
0.S _|_ x by Th11;
hence thesis by Th12;
end;
theorem
Th44: not b _|_ a implies (PProJ(a,b,x,y) = 0.F iff y _|_ x)
proof
set 0F = 0.F;
assume A1: not b _|_ a;
then A2: a <> 0.S by Lm6;
A3: PProJ(a,b,x,y) = 0.F implies y _|_ x
proof
assume A4: PProJ(a,b,x,y) = 0.F;
A5: now assume A6: for p holds p _|_ a or p _|_ x;
x = 0.S
proof
assume not thesis;
then ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x
by A2,Def2;
hence contradiction by A6;
end;
hence thesis by Lm6; end;
now given p such that A7: not p _|_ a & not p _|_ x;
ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F by A1,A4,A7,Def7;
then ProJ(a,b,p)*ProJ(p,a,x) = 0F or ProJ(x,p,y) = 0F by VECTSP_1:44;
then A8: ProJ(a,b,p) = 0.F or ProJ(p,a,x) = 0.F or ProJ(x,p,y) = 0.F by
VECTSP_1:44;
now assume A9: ProJ(p,a,x) = 0.F;
not a _|_ p by A7,Th12;
then x _|_ p by A9,Th33;
hence contradiction by A7,Th12; end;
hence thesis by A1,A7,A8,Th33; end;
hence thesis by A5; end;
y _|_ x implies PProJ(a,b,x,y) = 0.F
proof
assume A10: y _|_ x;
A11: now assume x = 0.S;
then for p holds p _|_ a or p _|_ x by Lm6;
hence thesis by A1,Def7; end;
now assume x <> 0.S;
then ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x
by A2,Def2;
then consider p such that A12: not p _|_ a & not p _|_ x;
ProJ(x,p,y) = 0F by A10,A12,Th33;
then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0.F by VECTSP_1:39;
hence thesis by A1,A12,Def7; end;
hence thesis by A11; end;
hence thesis by A3;
end;
theorem
not b _|_ a implies PProJ(a,b,x,y) = PProJ(a,b,y,x)
proof
assume A1: not b _|_ a;
A2: now assume x _|_ y;
then y _|_ x & x _|_ y by Th12;
then PProJ(a,b,x,y) = 0.F & PProJ(a,b,y,x) = 0.F by A1,Th44;
hence thesis;
end;
now assume not x _|_ y;
then a <> 0.S & x <> 0.S & y <> 0.S by A1,Lm6,Th11;
then ex r st not r _|_ a & not r _|_ x & not r _|_ y & not r _|_ a by Def2
;
then consider r such that A3: not r _|_ a & not r _|_ x & not r _|_ y;
A4: not a _|_ b & not a _|_ r & not x _|_ r & not y _|_ r by A1,A3,Th12;
A5: PProJ(a,b,x,y) = ProJ(a,b,r)*ProJ(r,a,x)*ProJ(x,r,y) by A1,A3,Def7;
PProJ(a,b,y,x) = ProJ(a,b,r)*ProJ(r,a,y)*ProJ(y,r,x) by A1,A3,Def7;
then PProJ(a,b,y,x) = ProJ(a,b,r)*(ProJ(r,a,y)*ProJ
(y,r,x)) by VECTSP_1:def 16;
then PProJ(a,b,y,x) = ProJ(a,b,r)*(ProJ(r,a,x)*ProJ(x,r,y)) by A4,Th40;
hence thesis by A5,VECTSP_1:def 16;
end;
hence thesis by A2;
end;
theorem
not b _|_ a implies PProJ(a,b,x,l*y) = l*PProJ(a,b,x,y)
proof
set 0F = 0.F;
assume A1: not b _|_ a;
A2: now assume A3: x _|_ y;
then y _|_ x by Th12;
then l*y _|_ x by Def2;
then x _|_ y & y _|_ x & l*y _|_ x & x _|_ l*y by A3,Th12;
then l*PProJ(a,b,x,y) = l*0F & PProJ(a,b,x,l*y) = 0F by A1,Th44;
hence thesis by VECTSP_1:39;
end;
now assume not x _|_ y;
then a <> 0.S & x <> 0.S by A1,Lm6,Th11;
then ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by Def2
;
then consider p such that A4: not p _|_ a & not p _|_ x;
A5: PProJ(a,b,x,l*y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,l*y) by A1,A4,Def7;
A6: PProJ(a,b,x,y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) by A1,A4,Def7;
PProJ(a,b,x,l*y) = (l*ProJ(x,p,y))*(ProJ(a,b,p)*ProJ(p,a,x)) by A4,A5,
Th25
;
hence thesis by A6,VECTSP_1:def 16;
end;
hence thesis by A2;
end;
theorem
not b _|_ a implies PProJ(a,b,x,y+z) = PProJ(a,b,x,y) + PProJ(a,b,x,z)
proof
set 0F = 0.F;
assume A1: not b _|_ a;
A2: now assume x = 0.S;
then PProJ(a,b,x,y+z) = 0F & PProJ(a,b,x,y) = 0F & PProJ
(a,b,x,z) = 0F by A1,Th43;
hence thesis by RLVECT_1:10;
end;
now assume x <> 0.S;
then a <> 0.S & x <> 0.S by A1,Lm6;
then ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by Def2
;
then consider p such that A3: not p _|_ a & not p _|_ x;
A4: PProJ(a,b,x,y+z) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y+z) by A1,A3,Def7;
A5: PProJ(a,b,x,y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) by A1,A3,Def7;
A6: PProJ(a,b,x,z) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,z) by A1,A3,Def7;
ProJ(x,p,y+z) = ProJ(x,p,y) + ProJ(x,p,z) by A3,Th26;
hence thesis by A4,A5,A6,VECTSP_1:def 18;
end;
hence thesis by A2;
end;