:: Construction of a bilinear symmetric form in orthogonal vector space
:: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski
::
:: Received November 23, 1989
:: 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 VECTSP_1, CARD_1, XBOOLE_0, SUBSET_1, BINOP_1, FUNCT_1, ZFMISC_1,
TARSKI, RELAT_1, STRUCT_0, SYMSP_1, RLVECT_1, ALGSTR_0, ARYTM_3,
SUPINF_2, ARYTM_1, GROUP_1, FUNCOP_1, ORTSP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1,
ORDINAL1, NUMBERS, DOMAIN_1, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1,
GROUP_1, VECTSP_1, RELSET_1, SYMSP_1;
constructors BINOP_1, DOMAIN_1, FUNCOP_1, SYMSP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1, SYMSP_1;
requirements SUBSET, BOOLE;
definitions ALGSTR_0;
equalities BINOP_1, ALGSTR_0;
expansions TARSKI;
theorems VECTSP_1, TARSKI, RLVECT_1, GROUP_1, FUNCOP_1, STRUCT_0, ORDERS_2,
XTUPLE_0;
schemes BINOP_1, 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 BINOP_1:sch 4;
Lm2: now
defpred P[object] means ex a,b being Element of X st $1 = [a,b] & b = o;
set CV = [:X,X:];
let F;
consider mo being set such that
A1: for x being object holds x in mo iff x in CV & P[x] from XBOOLE_0:sch 1;
mo c= CV
by A1;
then reconsider mo as Relation of X;
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 being Element of H holds x+0.H = x
proof
let x be Element of H;
md.(x,0.H) = o by Lm1;
hence thesis by TARSKI:def 1;
end;
A2: H is right_complementable
proof
let x be Element of H;
take -x;
0.H = o by STRUCT_0:def 6;
hence thesis by Lm1;
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;
reconsider x,y,z as Element of X;
md.(x,md.(y,z)) = o by Lm1;
hence thesis by Lm1;
end;
for x,y being Element of H holds x+y = y+x
proof
let x,y be Element of H;
md.(x,y) = o by Lm1;
hence thesis by Lm1;
end;
hence thesis by A3,A1,A2,RLVECT_1:def 2,def 3,def 4;
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 #);
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*y)*v = x*(y*v)
proof
set z = x*y;
A4: z*v = mF.(z,v) by A2,VECTSP_1:def 12;
reconsider v as Element of MPS;
reconsider v as Element of MPS;
A5: (x*y)*v = o by A1,A2,A4;
reconsider v as Element of MPS;
A6: mF.(y,v qua set) = o by A1,A2;
reconsider v as Element of MPS;
y*v = o by A2,A6,VECTSP_1:def 12;
then x*(y*v) = mF.(x,o) by A2,VECTSP_1:def 12;
hence thesis by A1,A5;
end;
A7: x*(v+w) = x*v+x*w
proof
reconsider v,w as Element of MPS;
A8: o = 0.MPS by A2,STRUCT_0:def 6;
reconsider v,w as Element of X by A2;
A9: md.(v,w) = o by Lm1;
reconsider v,w as Element of MPS;
x*(v+w) = mF.(x,o) by A2,A9,VECTSP_1:def 12;
then
A10: x*(v+w) = o by A1;
reconsider w as Element of MPS;
reconsider v as Element of MPS;
A11: mF.(x,v qua set) = o by A1;
reconsider v as Element of MPS;
A12: mF.(x,w qua set) = o by A1;
reconsider w as Element of MPS;
A13: x*w = o by A2,A12,VECTSP_1:def 12;
x*v = o by A2,A11,VECTSP_1:def 12;
hence thesis by A10,A13,A8,RLVECT_1:4;
end;
A14: (x+y)*v = x*v+y*v
proof
set z = x+y;
A15: z*v = mF.(z,v) by A2,VECTSP_1:def 12;
reconsider v as Element of MPS;
reconsider v as Element of MPS;
A16: (x+y)*v = o by A1,A2,A15;
reconsider v as Element of MPS;
A17: mF.(x,v qua set) = o by A1,A2;
reconsider v as Element of MPS;
A18: x*v = o by A2,A17,VECTSP_1:def 12;
reconsider v as Element of MPS;
A19: mF.(y,v qua set) = o by A1,A2;
A20: o = 0.MPS by A2,STRUCT_0:def 6;
reconsider v as Element of MPS;
y*v = o by A2,A19,VECTSP_1:def 12;
hence thesis by A16,A18,A20,RLVECT_1:4;
end;
(1_F)*v = v
proof
set one1 = 1_F;
A21: one1*v = mF.(one1,v) by A2,VECTSP_1:def 12;
reconsider v as Element of MPS;
mF.(one1,v qua set) = o by A1,A2;
hence thesis by A2,A21,TARSKI:def 1;
end;
hence thesis by A7,A14,A3;
end;
hence MPS is vector-distributive scalar-distributive scalar-associative
scalar-unital by VECTSP_1:def 14,def 15,def 16,def 17;
end;
Lm5: now
set CV = [:X,X:];
let F;
let mF be Function of [:(the carrier of F),(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 #);
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;
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,ORDERS_2:def 5;
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: b = o implies a _|_ b
proof
consider c,d being Element of MPS such that
A6: c = a & d = b;
assume
A7: b = o;
[a,b] = [c,d] by A6;
hence thesis by A2,A3,A7;
end;
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 XTUPLE_0:1;
end;
hence thesis by A5;
end;
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 that
A8: b _|_ a and
c _|_ a;
a = o by A4,A8;
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
A9: not b _|_ a;
assume not thesis;
a <> o by A4,A9;
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 that
a _|_ b-c and
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;
attr IT is OrtSp-like means
:Def1:
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;
registration
let F;
cluster OrtSp-like vector-distributive scalar-distributive
scalar-associative scalar-unital strict for
Abelian add-associative right_zeroed
right_complementable non empty SymStr over F;
existence
proof
reconsider mF = [:the carrier of F,X:] --> o as Function of [:the carrier
of F,X:],X;
consider mo being Relation of X such that
A1: 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,Lm5;
for a being Element of F for x being Element of X holds mF.[a,x] = o
by FUNCOP_1:7;
hence MPS is vector-distributive scalar-distributive scalar-associative
scalar-unital by Lm4;
thus thesis;
end;
end;
definition
let F;
mode OrtSp of F is OrtSp-like vector-distributive scalar-distributive
scalar-associative scalar-unital 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;
theorem Th1:
0.S _|_ a
proof
set 0F = 0.F,0V = 0.S;
A1: now
assume not a _|_ a;
then consider m being Element of F such that
A2: (0V-m*a) _|_ a by Def1;
0F*(0V-m*a) _|_ a by A2,Def1;
hence thesis by VECTSP_1:14;
end;
now
assume a _|_ a;
then 0F*a _|_ a by Def1;
hence thesis by VECTSP_1:14;
end;
hence thesis by A1;
end;
theorem Th2:
a _|_ b implies b _|_ a
proof
set 0V = 0.S;
assume a _|_ b;
then a _|_ (-(-b)) by RLVECT_1:17;
then
A1: a _|_ 0V-(-b) by RLVECT_1:4;
0V _|_ -b-a by Th1;
then -b _|_ a-0V by A1,Def1;
then -b _|_ a by VECTSP_1:18;
then (-1_F)*(-b) _|_ a by Def1;
then -(-b) _|_ a by VECTSP_1:14;
hence thesis by RLVECT_1:17;
end;
theorem Th3:
not a _|_ b & c+a _|_ b implies not c _|_ b
proof
assume that
A1: not a _|_ b and
A2: c+a _|_ b;
assume not thesis;
then (-1_F)*c _|_ b by Def1;
then -c _|_ b by VECTSP_1:14;
then -c+(c+a) _|_ b by A2,Def1;
then (c+(-c))+a _|_ b by RLVECT_1:def 3;
then 0.S+a _|_ b by RLVECT_1:5;
hence contradiction by A1,RLVECT_1:4;
end;
theorem Th4:
not b _|_ a & c _|_ a implies not b+c _|_ a
proof
assume that
A1: not b _|_ a and
A2: c _|_ a;
(-1_F)*c _|_ a by A2,Def1;
then
A3: -c _|_ a by VECTSP_1:14;
assume not thesis;
then (b+c)+(-c) _|_ a by A3,Def1;
then b+(c+(-c)) _|_ a by RLVECT_1:def 3;
then b+0.S _|_ a by RLVECT_1:5;
hence contradiction by A1,RLVECT_1:4;
end;
theorem Th5:
not b _|_ a & not l=0.F implies not l*b _|_ a & not b _|_ l*a
proof
set 1F = 1_F;
assume that
A1: not b _|_ a and
A2: not l=0.F;
A3: now
consider k such that
A4: k*l=1F by A2,VECTSP_1:def 9;
assume b _|_ l*a;
then l*a _|_ b by Th2;
then k*(l*a) _|_ b by Def1;
then 1F*a _|_ b by A4,VECTSP_1:def 16;
then a _|_ b;
hence contradiction by A1,Th2;
end;
now
consider k such that
A5: k*l=1F by A2,VECTSP_1:def 9;
assume l*b _|_ a;
then k*(l*b) _|_ a by Def1;
then 1F*b _|_ a by A5,VECTSP_1:def 16;
hence contradiction by A1;
end;
hence thesis by A3;
end;
theorem Th6:
a _|_ b implies -a _|_ b
proof
assume a _|_ b;
then (-1_F)*a _|_ b by Def1;
hence thesis by VECTSP_1:14;
end;
theorem Th7:
a-b _|_ d & a-c _|_ d implies b-c _|_ d
proof
assume that
A1: a-b _|_ d and
A2: a-c _|_ d;
-(a-b) _|_ d by A1,Th6;
then -a+b _|_ d by VECTSP_1:17;
then b+(-a)+(a-c) _|_ d by A2,Def1;
then b+(-a+(a+(-c))) _|_ d by RLVECT_1:def 3;
then b+((-a+a)+(-c)) _|_ d by RLVECT_1:def 3;
then b+((0.S)+(-c)) _|_ d by RLVECT_1:5;
hence thesis by RLVECT_1:4;
end;
theorem Th8:
not b _|_ a & x-k*b _|_ a & x-l*b _|_ a implies k = l
proof
set 1F = 1_F;
assume that
A1: not b _|_ a and
A2: x-k*b _|_ a & x-l*b _|_ a;
k*b-l*b _|_ a by A2,Th7;
then k*b+((-1F)*(l*b)) _|_ a by VECTSP_1:14;
then k*b+(((-1F)*l)*b) _|_ a by VECTSP_1:def 16;
then k*b+(-(l*(1F)))*b _|_ a by VECTSP_1:9;
then k*b+(-l)*b _|_ a;
then (k+(-l))*b _|_ a by VECTSP_1:def 15;
then (k+(-l))"*((k+(-l))*b) _|_ a by Def1;
then
A3: ((k+(-l))"*(k+(-l)))*b _|_ a by VECTSP_1:def 16;
assume not thesis;
then k-l<>0.F by RLVECT_1:21;
then (1F)*b _|_ a by A3,VECTSP_1:def 10;
hence contradiction by A1;
end;
theorem Th9:
a _|_ a & b _|_ b implies a+b _|_ a-b
proof
set 0V = 0.S;
assume that
A1: a _|_ a and
A2: b _|_ b;
(-1_F)*a _|_ a by A1,Def1;
then -a _|_ a by VECTSP_1:14;
then a _|_ -a by Th2;
then a _|_ 0V+(-a) by RLVECT_1:4;
then a _|_ (b+(-b))+(-a) by RLVECT_1:5;
then a _|_ b+(-b-a) by RLVECT_1:def 3;
then
A3: a _|_ b-(a+b) by VECTSP_1:17;
b _|_ b+0V by A2,RLVECT_1:4;
then b _|_ b+(a+(-a)) by RLVECT_1:5;
then b _|_ (a+b)-a by RLVECT_1:def 3;
hence thesis by A3,Def1;
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;
d _|_ d & c _|_ c by A4;
then d+c _|_ d-c by Th9;
then
A6: d-c _|_ d+c by Th2;
d+c _|_ d+c by A4;
then (d+c)+((-c)+d) _|_ d+c by A6,Def1;
then ((d+c)+(-c))+d _|_ d+c by RLVECT_1:def 3;
then (d+(c+(-c)))+d _|_ d+c by RLVECT_1:def 3;
then (d+0V)+d _|_ d+c by RLVECT_1:5;
then d+d _|_ d+c by RLVECT_1:4;
then (1F)*d+d _|_ d+c;
then (1F)*d+(1F)*d _|_ d+c;
then (1F+1F)*d _|_ d+c by VECTSP_1:def 15;
then (1F+1F)"*((1F+1F)*d) _|_ d+c by Def1;
then ((1F+1F)"*(1F+1F))*d _|_ d+c by VECTSP_1:def 16;
then (1F)*d _|_ d+c by A1,VECTSP_1:def 10;
then d _|_ d+c;
then
A7: d+c _|_ d by Th2;
-d _|_ d by A4,Th6;
then -d+(d+c) _|_ d by A7,Def1;
then (-d+d)+c _|_ d by RLVECT_1:def 3;
then 0V+c _|_ d by RLVECT_1:5;
hence thesis by RLVECT_1:4;
end;
ex c st not c _|_ a & not c _|_ a & not c _|_ a & not c _|_ a by A3,Def1;
hence contradiction by A5;
end;
:: 5. ORTHOGONAL PROJECTION
definition
let F,S,a,b,x;
assume
A1: not b _|_ a;
func ProJ(a,b,x) -> Element of F means
:Def2:
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,Def1;
take k;
let l be Element of F;
assume x-l*b _|_ a;
hence thesis by A1,A2,Th8;
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,Def1;
l1 = k by A3,A5;
hence thesis by A4,A5;
end;
end;
theorem Th11:
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 Def1;
hence thesis by A1,Def2;
end;
theorem Th12:
not b _|_ a implies ProJ(a,b,l*x) = l*ProJ(a,b,x)
proof
set L = x-ProJ(a,b,x)*b;
A1: l*L = l*x-l*(ProJ(a,b,x)*b) by VECTSP_1:23
.= l*x-(l*ProJ(a,b,x))*b by VECTSP_1:def 16;
assume
A2: not b _|_ a;
then
A3: l*x - ProJ(a,b,l*x)*b _|_ a by Th11;
L _|_ a by A2,Th11;
then l*x-(l*ProJ(a,b,x))*b _|_ a by A1,Def1;
hence thesis by A2,A3,Th8;
end;
theorem Th13:
not b _|_ a implies ProJ(a,b,x+y) = ProJ(a,b,x) + ProJ(a,b,y)
proof
set 1F = 1_F;
set L = (x-ProJ(a,b,x)*b)+(y-ProJ(a,b,y)*b);
A1: L = (x+(-ProJ(a,b,x)*b))+(y-ProJ(a,b,y)*b)
.= (x+(-ProJ(a,b,x)*b))+(y+(-ProJ(a,b,y)*b))
.= (((-ProJ(a,b,x)*b)+x)+y)+(-ProJ(a,b,y)*b) by RLVECT_1:def 3
.= ((x+y)+(-ProJ(a,b,x)*b))+(-ProJ(a,b,y)*b) by RLVECT_1:def 3
.= (x+y)+((-ProJ(a,b,x)*b)+(-ProJ(a,b,y)*b)) by RLVECT_1:def 3
.= (x+y)+((1F)*(-ProJ(a,b,x)*b)+(-ProJ(a,b,y)*b))
.= (x+y)+((1F)*(-ProJ(a,b,x)*b)+(1F)*(-ProJ (a,b,y)*b))
.= (x+y)+((1F)*((-ProJ(a,b,x))*b)+(1F)*(-ProJ(a,b,y)*b)) by VECTSP_1:21
.= (x+y)+((1F)*((-ProJ(a,b,x))*b)+(1F)*((-ProJ (a,b,y))*b)) by VECTSP_1:21
.= (x+y)+(((1F)*(-ProJ(a,b,x)))*b+(1F)*((-ProJ (a,b,y))*b))
.= (x+y)+(((-ProJ(a,b,x))*(1F))*b+((1F)*(-ProJ(a,b,y)))*b)
.= (x+y)+((-ProJ(a,b,x))*b+((-ProJ(a,b,y))*(1F))*b)
.= (x+y)+((-ProJ(a,b,x))*b+(-ProJ(a,b,y))*b)
.= (x+y)+((-ProJ(a,b,x))+(-ProJ(a,b,y)))*b by VECTSP_1:def 15
.= (x+y)+(-(ProJ(a,b,x)+ProJ(a,b,y)))*b by RLVECT_1:31
.= (x+y)-(ProJ(a,b,x)+ProJ(a,b,y))*b by VECTSP_1:21;
assume
A2: not b _|_ a;
then x-ProJ(a,b,x)*b _|_ a & y-ProJ(a,b,y)*b _|_ a by Th11;
then
A3: L _|_ a by Def1;
(x+y)-ProJ(a,b,x+y)*b _|_ a by A2,Th11;
hence thesis by A2,A1,A3,Th8;
end;
theorem
not b _|_ a & l <> 0.F implies ProJ(a,l*b,x) = l"*ProJ(a,b,x)
proof
assume that
A1: not b _|_ a and
A2: l <> 0.F;
set L = x-ProJ(a,l*b,x)*(l*b);
not l*b _|_ a by A1,A2,Th5;
then
A3: L _|_ a by Th11;
A4: L = x-(ProJ(a,l*b,x)*l)*b by VECTSP_1:def 16;
x-ProJ(a,b,x)*b _|_ a by A1,Th11;
then ProJ(a,b,x)*l" = (ProJ(a,l*b,x)*l)*l" by A1,A3,A4,Th8;
then ProJ(a,b,x)*l" = ProJ(a,l*b,x)*(l*l") by GROUP_1:def 3;
then l"*ProJ(a,b,x) = ProJ(a,l*b,x)*(1_F) by A2,VECTSP_1:def 10;
hence thesis;
end;
theorem Th15:
not b _|_ a & l <> 0.F implies ProJ(l*a,b,x) = ProJ(a,b,x)
proof
assume that
A1: not b _|_ a and
A2: l <> 0.F;
not b _|_ l*a by A1,A2,Th5;
then x-ProJ(l*a,b,x)*b _|_ l*a by Th11;
then l*a _|_ x-ProJ(l*a,b,x)*b by Th2;
then l"*(l*a) _|_ x-ProJ(l*a,b,x)*b by Def1;
then (l"*l)*a _|_ x-ProJ(l*a,b,x)*b by VECTSP_1:def 16;
then 1_F*a _|_ x-ProJ(l*a,b,x)*b by A2,VECTSP_1:def 10;
then a _|_ x-ProJ(l*a,b,x)*b;
then
A3: x-ProJ(l*a,b,x)*b _|_ a by Th2;
x-ProJ(a,b,x)*b _|_ a by A1,Th11;
hence thesis by A1,A3,Th8;
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 that
A1: not b _|_ a and
A2: p _|_ a;
not b+p _|_ a by A1,A2,Th4;
then c-ProJ(a,b+p,c)*(b+p) _|_ a by Th11;
then c-(ProJ(a,b+p,c)*b+ProJ(a,b+p,c)*p) _|_ a by VECTSP_1:def 14;
then
A3: c-ProJ(a,b+p,c)*b-ProJ(a,b+p,c)*p _|_ a by VECTSP_1:17;
c+p-ProJ(a,b,c+p)*b _|_ a & -p _|_ a by A1,A2,Th6,Th11;
then -p+(p+c+(-ProJ(a,b,c+p)*b)) _|_ a by Def1;
then -p+(p+(c+(-ProJ(a,b,c+p)*b))) _|_ a by RLVECT_1:def 3;
then (-p+p)+(c+(-ProJ(a,b,c+p)*b)) _|_ a by RLVECT_1:def 3;
then 0V+(c+(-ProJ(a,b,c+p)*b)) _|_ a by RLVECT_1:5;
then
A4: c-ProJ(a,b,c+p)*b _|_ a by RLVECT_1:4;
ProJ(a,b+p,c)*p _|_ a by A2,Def1;
then c+(-ProJ(a,b+p,c)*b)-ProJ(a,b+p,c)*p+ProJ(a,b+p,c)*p _|_ a by A3,Def1;
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 3;
then c+(-ProJ(a,b+p,c)*b)+0V _|_ a by RLVECT_1:5;
then
A5: c-ProJ(a,b+p,c)*b _|_ a by RLVECT_1:4;
c-ProJ(a,b,c)*b _|_ a by A1,Th11;
hence thesis by A1,A5,A4,Th8;
end;
theorem
not b _|_ a & p _|_ b & p _|_ c implies ProJ(a+p,b,c) = ProJ(a,b,c)
proof
assume that
A1: not b _|_ a and
A2: p _|_ b and
A3: p _|_ c;
b _|_ p by A2,Th2;
then ProJ(a,b,c)*b _|_ p by Def1;
then
A4: -(ProJ(a,b,c)*b) _|_ p by Th6;
c _|_ p by A3,Th2;
then c+(-(ProJ(a,b,c)*b)) _|_ p by A4,Def1;
then
A5: p _|_ c-ProJ(a,b,c)*b by Th2;
c-ProJ(a,b,c)*b _|_ a by A1,Th11;
then a _|_ c-ProJ(a,b,c)*b by Th2;
then a+p _|_ c-ProJ(a,b,c)*b by A5,Def1;
then
A6: c-ProJ(a,b,c)*b _|_ a+p by Th2;
not a _|_ b by A1,Th2;
then not a+p _|_ b by A2,Th4;
then
A7: not b _|_ a+p by Th2;
then c-ProJ(a+p,b,c)*b _|_ a+p by Th11;
hence thesis by A7,A6,Th8;
end;
theorem Th18:
not b _|_ a & c-b _|_ a implies ProJ(a,b,c) = 1_F
proof
assume that
A1: not b _|_ a and
A2: c-b _|_ a;
c-(1_F)*b _|_ a & c-ProJ(a,b,c)*b _|_ a by A1,A2,Th11;
hence thesis by A1,Th8;
end;
theorem Th19:
not b _|_ a implies ProJ(a,b,b) = 1_F
proof
A1: b-b = 0.S by RLVECT_1:5;
assume not b _|_ a;
hence thesis by A1,Th1,Th18;
end;
theorem Th20:
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 that
A2: not b _|_ a and
A3: x _|_ a;
x+0V _|_ a by A3,RLVECT_1:4;
then x+(-0V) _|_ a by RLVECT_1:12;
then
A4: x-0F*b _|_ a by VECTSP_1:14;
x-ProJ(a,b,x)*b _|_ a by A2,Th11;
hence ProJ(a,b,x) = 0.F by A2,A4,Th8;
end;
now
assume ( not b _|_ a)& ProJ(a,b,x) = 0.F;
then x-0F*b _|_ a by Th11;
then x+(-0V) _|_ a by VECTSP_1:14;
then x+0V _|_ a by RLVECT_1:12;
hence x _|_ a by RLVECT_1:4;
end;
hence thesis by A1;
end;
theorem Th21:
not b _|_ a & not q _|_ a implies ProJ(a,b,p)*ProJ(a,b,q)" = ProJ(a,q,p)
proof
assume that
A1: not b _|_ a and
A2: not q _|_ a;
ProJ(a,q,p)*q-ProJ(a,b,ProJ(a,q,p)*q)* b _|_ a & p-ProJ(a,q,p)*q _|_ a
by A1,A2,Th11;
then (p+(-ProJ(a,q,p)*q))+(ProJ(a,q,p)*q-(ProJ(a,b,ProJ(a,q,p)*q)*b)) _|_ a
by Def1;
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 3;
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 3;
then p+0.S+(-(ProJ(a,b,ProJ(a,q,p)*q))*b) _|_ a by RLVECT_1:5;
then p-(ProJ(a,b,ProJ(a,q,p)*q)*b) _|_ a by RLVECT_1:4;
then
A3: p-(ProJ(a,q,p)*ProJ(a,b,q))*b _|_ a by A1,Th12;
p-ProJ(a,b,p)*b _|_ a by A1,Th11;
then ProJ(a,q,p)*ProJ(a,b,q) = ProJ(a,b,p) by A1,A3,Th8;
then
A4: ProJ(a,q,p)*(ProJ(a,b,q)*ProJ(a,b,q)") = ProJ(a,b,p)*ProJ (a,b,q)" by
GROUP_1:def 3;
ProJ(a,b,q) <> 0.F by A1,A2,Th20;
then ProJ(a,q,p)*1_F = ProJ(a,b,p)*ProJ(a,b,q)" by A4,VECTSP_1:def 10;
hence thesis;
end;
theorem Th22:
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 that
A1: not b _|_ a and
A2: not c _|_ a;
A3: ProJ(a,c,b) <> 0F by A1,A2,Th20;
ProJ(a,b,b)*ProJ(a,b,c)" = ProJ(a,c,b) by A1,A2,Th21;
then ProJ(a,b,c)"*1F = ProJ(a,c,b) by A1,Th19;
then
A4: ProJ(a,b,c)" = ProJ(a,c,b);
ProJ(a,b,c) <> 0F by A1,A2,Th20;
then 1F = ProJ(a,c,b)*ProJ(a,b,c) by A4,VECTSP_1:def 10;
then ProJ(a,c,b)" = ProJ(a,c,b)"*(ProJ(a,c,b)*ProJ(a,b,c))
.= (ProJ(a,c,b)"*ProJ(a,c,b))*ProJ(a,b,c) by GROUP_1:def 3
.= ProJ(a,b,c)*1F by A3,VECTSP_1:def 10;
hence thesis;
end;
theorem Th23:
not b _|_ a & b _|_ c+a implies ProJ(a,b,c) = -ProJ(c,b,a)
proof
set 1F = 1_F;
assume that
A1: not b _|_ a and
A2: b _|_ c+a;
c-ProJ(a,b,c)*b _|_ a by A1,Th11;
then (-ProJ(a,b,c))*b+c _|_ a by VECTSP_1:21;
then (-1F)*((-ProJ(a,b,c))*b+c) _|_ a by Def1;
then (-1F)*((-ProJ(a,b,c))*b)+(-1F)*c _|_ a by VECTSP_1:def 14;
then ((-1F)*(-ProJ(a,b,c)))*b+(-1F)*c _|_ a by VECTSP_1:def 16;
then (ProJ(a,b,c)*(1F))*b+(-1F)*c _|_ a by VECTSP_1:10;
then ProJ(a,b,c)*b+(-1F)*c _|_ a;
then ProJ(a,b,c)*b-c _|_ a by VECTSP_1:14;
then a _|_ ProJ(a,b,c)*b-c by Th2;
then
A3: -a _|_ ProJ(a,b,c)*b-c by Th6;
ProJ(a,b,c)*b _|_ c+a by A2,Def1;
then ProJ(a,b,c)*b _|_ c-(-a) by RLVECT_1:17;
then c _|_ -a-ProJ(a,b,c)*b by A3,Def1;
then
A4: -a-ProJ(a,b,c)*b _|_ c by Th2;
( not a _|_ b)& c+a _|_ b by A1,A2,Th2;
then
A5: not c _|_ b by Th3;
then
A6: not b _|_ c by Th2;
then -a-ProJ(c,b,-a)*b _|_ c by Th11;
then ProJ(a,b,c) = ProJ(c,b,-a) by A6,A4,Th8
.= ProJ(c,b,(-1F)*a) by VECTSP_1:14
.= (-1F)*ProJ(c,b,a) by A5,Th2,Th12
.= -(ProJ(c,b,a)*(1F)) by VECTSP_1:9;
hence thesis;
end;
theorem Th24:
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 that
A1: not a _|_ b and
A2: not c _|_ b;
ProJ(b,a,c) <> 0.F by A1,A2,Th20;
then
A3: -ProJ(b,a,c)" <> 0.F by VECTSP_1:25;
ProJ(b,a,c) <> 0.F by A1,A2,Th20;
then (-1F)*(ProJ(b,a,c)"*ProJ(b,a,c)) = (-1F)*(1F) by VECTSP_1:def 10;
then ((-1F)*ProJ(b,a,c)")*ProJ(b,a,c) = (-1F)*(1F) by GROUP_1:def 3;
then ((-1F)*ProJ(b,a,c)")*ProJ(b,a,c) = (-1F);
then (-(ProJ(b,a,c)"*(1F)))*ProJ(b,a,c) = -1F by VECTSP_1:9;
then (-ProJ(b,a,c)")*ProJ(b,a,c) = -1F;
then ProJ(b,a,(-ProJ(b,a,c)")*c) = -1F by A1,Th12;
then (-ProJ(b,a,c)")*c-(-1F)*a _|_ b by A1,Th11;
then (-ProJ(b,a,c)")*c+(-(-(a))) _|_ b by VECTSP_1:14;
then (-ProJ(b,a,c)")*c+a _|_ b by RLVECT_1:17;
then
A4: b _|_ (-ProJ(b,a,c)")*c+a by Th2;
not b _|_ a by A1,Th2;
then ProJ(a,b,(-ProJ(b,a,c)")*c) = -ProJ((-ProJ (b,a,c)")*c,b,a) by A4,Th23;
then ProJ(a,b,(-ProJ(b,a,c)")*c) = -ProJ(c,b,a) by A2,A3,Th2,Th15;
then (-ProJ(b,a,c)")*ProJ(a,b,c) = -ProJ(c,b,a) by A1,Th2,Th12;
then (-(ProJ(b,a,c)"*ProJ(a,b,c)))*(-1F) = (-ProJ (c,b,a))*(-1F) by
VECTSP_1:9;
then (ProJ(b,a,c)"*ProJ(a,b,c))*(1F) = (-ProJ(c,b,a))*(-1F) by VECTSP_1:10;
then (ProJ(b,a,c)"*ProJ(a,b,c))*(1F) = ProJ(c,b,a)*(1F) by VECTSP_1:10;
then ProJ(b,a,c)"*ProJ(a,b,c) = ProJ(c,b,a)*(1F);
hence thesis;
end;
theorem Th25:
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 that
A1: not p _|_ a and
A2: not p _|_ x and
A3: not q _|_ a and
A4: not q _|_ x;
A5: p <> 0.S & q <> 0.S by A1,A3,Th1;
A6: not a _|_ p by A1,Th2;
a <> 0.S & x <> 0.S by A1,A2,Th1,Th2;
then consider r such that
A7: not r _|_ p and
A8: not r _|_ q and
A9: not r _|_ a and
A10: not r _|_ x by A5,Def1;
A11: not q _|_ r by A8,Th2;
A12: not x _|_ r by A10,Th2;
A13: not p _|_ r by A7,Th2;
then
A14: ProJ(r,q,p) <> 0F by A11,Th20;
A15: not a _|_ r by A9,Th2;
A16: not x _|_ q by A4,Th2;
A17: not x _|_ p by A2,Th2;
A18: not a _|_ q by A3,Th2;
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 A3,A9,Th21
.= (ProJ(a,r,p)*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,r,a)")*ProJ (q,a,x)"
by A6,A7,Th21
.= (ProJ(a,r,p)*ProJ(a,r,q)")*(ProJ(p,r,x)*ProJ(p,r,a)")*ProJ (q,x,a) by
A18,A16,Th22
.= (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 A16,A8,Th21
.= (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,A9,Th22
.= (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 A6,A7,Th22
.= (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 A3,A9,Th22
.= (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 A18,A8,Th22
.= (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 A17,A7,Th22
.= (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 A16,A8,Th22
.= 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 GROUP_1:def 3
.= 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 GROUP_1:def 3
.= ProJ(p,x,r)"*(ProJ(r,a,p)*ProJ(a,q,r))*(ProJ(q,a,r)"*ProJ (q,x,r)) by A1
,A9,Th24
.= (ProJ(p,x,r)"*ProJ(r,a,p))*ProJ(a,q,r)*(ProJ(q,a,r)"*ProJ (q,x,r)) by
GROUP_1:def 3
.= (ProJ(p,x,r)"*ProJ(r,a,p))*(ProJ(a,q,r)*(ProJ(q,a,r)"*ProJ (q,x,r)))
by GROUP_1:def 3
.= (ProJ(p,x,r)"*ProJ(r,a,p))*((ProJ(q,a,r)"*ProJ(a,q,r))*ProJ(q,x,r))
by GROUP_1:def 3
.= (ProJ(p,x,r)"*ProJ(r,a,p))*(ProJ(r,q,a)*ProJ(q,x,r)) by A18,A8,Th24
.= ProJ(p,x,r)"*(ProJ(r,a,p)*(ProJ(r,q,a)*ProJ(q,x,r))) by GROUP_1:def 3
.= ProJ(p,x,r)"*((ProJ(r,a,p)*ProJ(r,q,a))*ProJ(q,x,r)) by GROUP_1:def 3
.= ProJ(p,x,r)"*((ProJ(r,a,p)*ProJ(r,a,q)")*ProJ(q,x,r)) by A11,A15,Th22
.= ProJ(p,x,r)"*(ProJ(r,q,p)*ProJ(q,x,r)) by A11,A15,Th21
.= ProJ(p,r,x)*(ProJ(r,q,p)*ProJ(q,x,r)) by A17,A7,Th22
.= (ProJ(r,x,p)"*ProJ(x,r,p))*(ProJ(r,q,p)*ProJ(q,x,r)) by A13,A12,Th24
.= (ProJ(r,x,p)"*ProJ(x,r,p))*(ProJ(r,q,p)*(ProJ(x,r,q)"*ProJ (r,x,q)))
by A4,A10,Th24
.= (ProJ(r,x,p)"*ProJ(x,r,p))*(ProJ(r,x,q)*(ProJ(r,q,p)*ProJ(x,r,q)"))
by GROUP_1:def 3
.= ((ProJ(x,r,p)*ProJ(r,x,p)")*ProJ(r,x,q))*(ProJ(r,q,p)*ProJ(x,r,q)")
by GROUP_1:def 3
.= (ProJ(x,r,p)*(ProJ(r,x,q)*ProJ(r,x,p)"))*(ProJ(r,q,p)*ProJ(x,r,q)")
by GROUP_1:def 3
.= (ProJ(x,r,p)*ProJ(r,p,q))*(ProJ(r,q,p)*ProJ(x,r,q)") by A13,A12,Th21
.= ProJ(x,r,p)*(ProJ(r,p,q)*(ProJ(r,q,p)*ProJ(x,r,q)")) by GROUP_1:def 3
.= ProJ(x,r,p)*((ProJ(r,p,q)*ProJ(r,q,p))*ProJ(x,r,q)") by GROUP_1:def 3
.= ProJ(x,r,p)*((ProJ(r,q,p)"*ProJ(r,q,p))*ProJ(x,r,q)") by A13,A11,Th22
.= ProJ(x,r,p)*(ProJ(x,r,q)"*(1F)) by A14,VECTSP_1:def 10
.= ProJ(x,r,p)*ProJ(x,r,q)"
.= ProJ(x,q,p) by A4,A10,Th21;
then
A19: (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 GROUP_1:def 3;
ProJ(q,a,x) <> 0F by A18,A16,Th20;
then (ProJ(a,q,p)*ProJ(p,a,x))*(1F) = ProJ(q,a,x)*ProJ (x,q,p) by A19,
VECTSP_1:def 10;
hence thesis;
end;
theorem Th26:
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 that
A1: not p _|_ a and
A2: not p _|_ x and
A3: not q _|_ a and
A4: not q _|_ x and
A5: not b _|_ a;
A6: now
A7: ProJ(a,b,q) <> 0F by A3,A5,Th20;
assume
A8: not y _|_ x;
ProJ(a,q,p)*ProJ(p,a,x) = ProJ(x,q,p)*ProJ(q,a,x) by A1,A2,A3,A4,Th25;
then (ProJ(a,b,p)*ProJ(a,b,q)")*ProJ(p,a,x) = ProJ(x,q,p)*ProJ (q,a,x) by
A3,A5,Th21;
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 A4,A8,Th21;
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 GROUP_1:def 3;
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 GROUP_1:def 3;
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 A7,VECTSP_1:def 10;
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));
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 A2,A8,Th22;
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 GROUP_1:def 3;
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 GROUP_1:def 3;
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 GROUP_1:def 3;
then
A9: 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 GROUP_1:def 3;
ProJ(x,p,y) <> 0F by A2,A8,Th20;
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 A9,VECTSP_1:def 10;
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)");
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 A4,A8,Th22;
hence thesis by GROUP_1:def 3;
end;
now
assume
A10: y _|_ x;
then ProJ(x,p,y) = 0F by A2,Th20;
then
A11: ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F;
ProJ(x,q,y) = 0F by A4,A10,Th20;
hence thesis by A11;
end;
hence thesis by A6;
end;
theorem Th27:
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 that
A1: not a _|_ p and
A2: not x _|_ p and
A3: not y _|_ p;
A4: not p _|_ y by A3,Th2;
A5: not p _|_ x by A2,Th2;
A6: now
A7: ProJ(p,a,x) <> 0F by A1,A2,Th20;
assume
A8: not y _|_ x;
then
A9: not x _|_ y by Th2;
ProJ(p,a,y)*ProJ(p,a,x)" = ProJ(p,x,y) by A1,A2,Th21;
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 A5,A8,Th24;
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 GROUP_1:def 3;
then ProJ(p,a,y)*(1F) = (ProJ(x,y,p)"*ProJ(y,x,p))*ProJ(p,a,x) by A7,
VECTSP_1:def 10;
then ProJ(p,a,y) = (ProJ(y,x,p)*ProJ(x,y,p)")*ProJ (p,a,x);
then ProJ(p,a,y) = ProJ(y,x,p)*(ProJ(x,y,p)"*ProJ (p,a,x)) by GROUP_1:def 3
;
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 A4,A9,Th22;
then
A10: 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 GROUP_1:def 3;
ProJ(y,p,x) <> 0F by A4,A9,Th20;
then ProJ(y,p,x)*ProJ(p,a,y) = (ProJ(x,y,p)"*ProJ(p,a,x))*(1F) by A10,
VECTSP_1:def 10
.= ProJ(x,y,p)"*ProJ(p,a,x);
hence thesis by A5,A8,Th22;
end;
now
assume
A11: y _|_ x;
then ProJ(x,p,y) = 0F by A5,Th20;
then
A12: ProJ(p,a,x)*ProJ(x,p,y) = 0F;
x _|_ y by A11,Th2;
then ProJ(y,p,x) = 0F by A4,Th20;
hence thesis by A12;
end;
hence thesis by A6;
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
:Def3:
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
otherwise it = 0.F;
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 thesis by A1,A2,Th26;
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;
consider r such that
A4: ( not r _|_ a)& not r _|_ x by A3;
assume that
A5: for q st not q _|_ a & not q _|_ x holds IT1 = ProJ(a,b,q)*ProJ
(q,a,x)*ProJ(x,q,y) and
A6: for q st not q _|_ a & not q _|_ x holds IT2 = ProJ(a,b,q)*ProJ
(q,a,x)*ProJ(x,q,y);
IT1 = ProJ(a,b,r)*ProJ(r,a,x)*ProJ(x,r,y) by A5,A4;
hence thesis by A6,A4;
end;
thus thesis;
end;
consistency;
end;
theorem Th28:
not b _|_ a & x = 0.S implies PProJ(a,b,x,y) = 0.F
proof
assume that
A1: not b _|_ a and
A2: x = 0.S;
for p holds p _|_ a or p _|_ x by A2,Th1,Th2;
hence thesis by A1,Def3;
end;
theorem Th29:
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 Th1,Th2;
A3: PProJ(a,b,x,y) = 0.F implies y _|_ x
proof
assume
A4: PProJ(a,b,x,y) = 0.F;
A5: now
given p such that
A6: not p _|_ a and
A7: not p _|_ x;
A8: now
assume
A9: ProJ(p,a,x) = 0.F;
not a _|_ p by A6,Th2;
then x _|_ p by A9,Th20;
hence contradiction by A7,Th2;
end;
ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F by A1,A4,A6,A7,Def3;
then ProJ(a,b,p)*ProJ(p,a,x) = 0F or ProJ(x,p,y) = 0F by VECTSP_1:12;
then
ProJ(a,b,p) = 0.F or ProJ(p,a,x) = 0.F or ProJ(x,p,y) = 0.F by VECTSP_1:12;
hence thesis by A1,A6,A7,A8,Th20;
end;
now
assume
A10: 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,Def1;
hence contradiction by A10;
end;
hence thesis by Th1,Th2;
end;
hence thesis by A5;
end;
y _|_ x implies PProJ(a,b,x,y) = 0.F
proof
assume
A11: y _|_ x;
A12: now
assume x <> 0.S;
then
ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by A2,Def1;
then consider p such that
A13: not p _|_ a and
A14: not p _|_ x;
ProJ(x,p,y) = 0F by A11,A14,Th20;
then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0.F;
hence thesis by A1,A13,A14,Def3;
end;
now
assume x = 0.S;
then for p holds p _|_ a or p _|_ x by Th1,Th2;
hence thesis by A1,Def3;
end;
hence thesis by A12;
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 not x _|_ y;
then
A3: x <> 0.S & y <> 0.S by Th1,Th2;
a <> 0.S by A1,Th1,Th2;
then
ex r st not r _|_ a & not r _|_ x & not r _|_ y & not r _|_ a by A3,Def1;
then consider r such that
A4: not r _|_ a and
A5: not r _|_ x and
A6: not r _|_ y;
A7: not y _|_ r by A6,Th2;
PProJ(a,b,y,x) = ProJ(a,b,r)*ProJ(r,a,y)*ProJ(y,r,x) by A1,A4,A6,Def3;
then
A8: PProJ(a,b,y,x) = ProJ(a,b,r)*(ProJ(r,a,y)*ProJ (y,r,x)) by GROUP_1:def 3;
( not a _|_ r)& not x _|_ r by A4,A5,Th2;
then
A9: PProJ(a,b,y,x) = ProJ(a,b,r)*(ProJ(r,a,x)*ProJ(x,r,y)) by A7,A8,Th27;
PProJ(a,b,x,y) = ProJ(a,b,r)*ProJ(r,a,x)*ProJ(x,r,y) by A1,A4,A5,Def3;
hence thesis by A9,GROUP_1:def 3;
end;
now
assume x _|_ y;
then y _|_ x & PProJ(a,b,y,x) = 0.F by A1,Th2,Th29;
hence thesis by A1,Th29;
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 not x _|_ y;
then
A3: x <> 0.S by Th1;
a <> 0.S by A1,Th1,Th2;
then ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by A3
,Def1;
then consider p such that
A4: not p _|_ a and
A5: not p _|_ x;
PProJ(a,b,x,l*y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,l*y) by A1,A4,A5,Def3;
then
A6: PProJ(a,b,x,l*y) = (l*ProJ(x,p,y))*(ProJ(a,b,p)*ProJ(p,a,x)) by A5,Th12;
PProJ(a,b,x,y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) by A1,A4,A5,Def3;
hence thesis by A6,GROUP_1:def 3;
end;
now
assume
A7: x _|_ y;
then y _|_ x by Th2;
then l*y _|_ x by Def1;
then
A8: PProJ(a,b,x,l*y) = 0F by A1,Th29;
y _|_ x by A7,Th2;
then l*PProJ(a,b,x,y) = l*0F by A1,Th29;
hence thesis by A8;
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
A3: x <> 0.S;
a <> 0.S by A1,Th1,Th2;
then
ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by A3,Def1;
then consider p such that
A4: ( not p _|_ a)& not p _|_ x;
A5: PProJ(a,b,x,y+z) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y+z) & PProJ(a,b,
x,y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) by A1,A4,Def3;
PProJ(a,b,x,z) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,z) & ProJ(x,p,y+z)
= ProJ( x,p,y) + ProJ(x,p,z) by A1,A4,Def3,Th13;
hence thesis by A5,VECTSP_1:def 7;
end;
now
assume
A6: x = 0.S;
then
A7: PProJ (a,b,x,z) = 0F by A1,Th28;
PProJ(a,b,x,y+z) = 0F & PProJ(a,b,x,y) = 0F by A1,A6,Th28;
hence thesis by A7,RLVECT_1:4;
end;
hence thesis by A2;
end;