:: Construction of a bilinear antisymmetric form in symplectic 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, ORDERS_2, STRUCT_0, ALGSTR_0, BINOP_1, SUBSET_1,
FUNCT_1, ZFMISC_1, RELAT_1, XBOOLE_0, XXREAL_0, CARD_1, TARSKI, RLVECT_1,
SUPINF_2, ARYTM_1, ARYTM_3, GROUP_1, MESFUNC1, SYMSP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_2, DOMAIN_1, ORDINAL1,
NUMBERS, STRUCT_0, ORDERS_2, ALGSTR_0, RLVECT_1, BINOP_1, GROUP_1,
VECTSP_1, RELSET_1;
constructors BINOP_1, DOMAIN_1, RLVECT_1, VECTSP_1, ORDERS_2, GROUP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1;
requirements SUBSET, BOOLE;
definitions STRUCT_0, RLVECT_1, ALGSTR_0;
equalities STRUCT_0, ALGSTR_0;
expansions TARSKI;
theorems VECTSP_1, TARSKI, RLVECT_1, GROUP_1, ORDERS_2, XTUPLE_0;
schemes BINOP_1, XBOOLE_0;
begin :: 1. SYMPLECTIC VECTOR SPACE STRUCTURE
reserve F for Field;
definition
let F;
struct (RelStr,ModuleStr over F) SymStr over F (# carrier -> set, addF ->
BinOp of the carrier, ZeroF -> Element of the carrier, lmult -> Function of [:
the carrier of F, the carrier:], the carrier, InternalRel -> Relation of the
carrier #);
end;
registration
let F;
cluster non empty for SymStr over F;
existence
proof
set X = the non empty set,a = the BinOp of X,Z = the Element of X,l =the
Function of [:the carrier of F, X:], X,r = the Relation of X;
take SymStr(#X,a,Z,l,r#);
thus the carrier of SymStr(#X,a,Z,l,r#) is non empty;
end;
end;
notation
let F;
let S be SymStr over F;
let a,b be Element of S;
synonym a _|_ b for a <= b;
end;
set X = {0};
reconsider o = 0 as Element of {0} by TARSKI:def 1;
deffunc F(Element of {0},Element of {0}) = o;
consider md being BinOp of {0} such that
Lm1: for x,y being Element of {0} 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;
registration
let F;
let X be non empty set, md be BinOp of X, o be Element of X, mF be Function
of [:the carrier of F, X:], X, mo be Relation of X;
cluster SymStr (# X,md,o,mF,mo #) -> non empty;
coherence;
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 #);
thus H is Abelian
proof
let x,y be Element of H;
reconsider x,y as Element of X;
md.(x,y) = o by Lm1;
hence thesis by Lm1;
end;
thus H is add-associative
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;
thus H is right_zeroed
proof
let x be Element of H;
reconsider x as Element of X;
md.(x,0.H) = o by Lm1;
hence thesis by TARSKI:def 1;
end;
let x be Element of H;
take -x;
thus thesis by Lm1;
end;
registration
let F;
cluster Abelian add-associative right_zeroed right_complementable for
non empty
SymStr over F;
existence
proof
set mo = the Relation of X;
set mF = the Function of [:the carrier of F,X:],X;
SymStr (# X,md,o,mF,mo #) is Abelian add-associative right_zeroed
right_complementable by Lm3;
hence thesis;
end;
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) = 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) = 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 X by A2;
A8: md.(v,w) = o by Lm1;
reconsider v,w as Element of MPS;
x*(v+w) = mF.(x,o) by A2,A8,VECTSP_1:def 12;
then
A9: x*(v+w) = o by A1;
mF.(x,v) = o by A1;
then
A10: x*v = o by A2,VECTSP_1:def 12;
mF.(x,w) = o by A1;
then
A11: x*w = o by A2,VECTSP_1:def 12;
o = 0.MPS by A2;
hence thesis by A9,A10,A11,RLVECT_1:4;
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 12;
reconsider v as Element of MPS;
reconsider v as Element of MPS;
A14: (x+y)*v = o by A1,A2,A13;
reconsider v as Element of MPS;
A15: mF.(x,v) = o by A1,A2;
reconsider v as Element of MPS;
A16: x*v = o by A2,A15,VECTSP_1:def 12;
reconsider v as Element of MPS;
A17: mF.(y,v) = o by A1,A2;
A18: o = 0.MPS by A2;
reconsider v as Element of MPS;
y*v = o by A2,A17,VECTSP_1:def 12;
hence thesis by A14,A16,A18,RLVECT_1:4;
end;
(1_F)*v = v
proof
set one1 = 1_F;
A19: one1*v = mF.(one1,v) by A2,VECTSP_1:def 12;
reconsider v as Element of MPS;
mF.(one1,v) = o by A1,A2;
hence thesis by A2,A19,TARSKI:def 1;
end;
hence thesis by A7,A12,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 #);
thus for a being Element of MPS holds (a <> 0.MPS implies ex p being Element
of MPS st not p _|_ a ) 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;
let a,b,c be Element of MPS;
assume that
a _|_ b+c and
b _|_ c+a;
assume not c _|_ a+b;
then a+b <> o by A4;
hence contradiction by A2,TARSKI:def 1;
end;
:: 2. SYMPLECTIC VECTOR SPACE
definition
let F;
let IT be Abelian add-associative right_zeroed right_complementable non
empty SymStr over F;
attr IT is SymSp-like means
:Def1:
for a,b,c,x being Element of IT for l
being Element of F holds (a<>(0.IT) implies ex y being Element of IT st not y
_|_ a ) & (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 SymSp-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
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 BINOP_1:sch 4;
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,x being Element of MPS for l being Element of F holds (a<>(
0.MPS) implies ex y being Element of MPS st not y _|_ a ) & (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 A2,Lm5;
thus MPS is vector-distributive scalar-distributive scalar-associative
scalar-unital by A1,Lm4;
thus thesis;
end;
end;
definition
let F;
mode SymSp of F is SymSp-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 SymSp of F;
reserve a,b,c,d,a9,b9,p,q,r,s,x,y,z for Element of S;
reserve k,l for Element of F;
theorem Th1:
0.S _|_ a
proof
set 0V = 0.S, 0F = 0.F;
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
A1: a _|_ 0V+b by RLVECT_1:4;
0V _|_ b+a by Th1;
then b _|_ a+0V by A1,Def1;
hence thesis by RLVECT_1:4;
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:
not a _|_ c implies not a+b _|_ c or not (1_F+1_F)*a+b _|_ c
proof
set 1F = 1_F;
assume
A1: not a _|_ c;
assume
A2: not thesis;
then (1F*a+1_F*a)+b _|_ c by VECTSP_1:def 15;
then (a+1F*a)+b _|_ c;
then (a+a)+b _|_ c;
then a+(a+b) _|_ c by RLVECT_1:def 3;
hence contradiction by A1,A2,Th4;
end;
theorem Th8:
not a9 _|_ a & a9 _|_ b & not b9 _|_ b & b9 _|_ a implies not a9
+b9 _|_ a & not a9+b9 _|_ b
proof
set 0V = 0.S;
assume that
A1: not a9 _|_ a and
A2: a9 _|_ b and
A3: not b9 _|_ b and
A4: b9 _|_ a;
assume not thesis;
then
a9+b9 _|_ a & (-(1_F))*b9 _|_ a or a9+b9 _|_ b & (-(1_F))*a9 _|_ b by A2,A4
,Def1;
then a9+b9 _|_ a & -b9 _|_ a or a9+b9 _|_ b & -a9 _|_ b by VECTSP_1:14;
then (a9+b9)+(-b9) _|_ a or -a9+(a9+b9) _|_ b by Def1;
then a9+(b9+(-b9)) _|_ a or (-a9+a9)+b9 _|_ b by RLVECT_1:def 3;
then a9+0V _|_ a or 0V+b9 _|_ b by RLVECT_1:5;
hence contradiction by A1,A3,RLVECT_1:4;
end;
theorem Th9:
a<>0.S & b<>0.S implies ex p st not p _|_ a & not p _|_ b
proof
assume that
A1: a<>0.S and
A2: b<>0.S;
consider a9 such that
A3: not a9 _|_ a by A1,Def1;
now
consider b9 such that
A4: not b9 _|_ b by A2,Def1;
assume
A5: a9 _|_ b;
now
assume b9 _|_ a;
then ( not a9+b9 _|_ a)& not a9+b9 _|_ b by A3,A5,A4,Th8;
hence thesis;
end;
hence thesis by A4;
end;
hence thesis by A3;
end;
theorem Th10:
1_F+1_F<>0.F & a<>0.S & b<>0.S & c <>0.S implies ex p st not p
_|_ a & not p _|_ b & not p _|_ c
proof
assume that
A1: 1_F+1_F<>0.F and
A2: a<>0.S and
A3: b<>0.S and
A4: c <>0.S;
consider r such that
A5: not r _|_ a and
A6: not r _|_ b by A2,A3,Th9;
consider s such that
A7: not s _|_ a and
A8: not s _|_ c by A2,A4,Th9;
now
assume that
A9: r _|_ c and
A10: s _|_ b;
A11: now
(1_F+1_F)*r _|_ c by A9,Def1;
then
A12: not (1_F+1_F)*r+s _|_ c by A8,Th4;
not (1_F+1_F)*r _|_ b by A1,A6,Th5;
then
A13: not (1_F+1_F)*r+s _|_ b by A10,Th4;
assume not (1_F+1_F)*r+s _|_ a;
hence thesis by A13,A12;
end;
now
assume
A14: not r+s _|_ a;
( not r+s _|_ b)& not r+s _|_ c by A6,A8,A9,A10,Th4;
hence thesis by A14;
end;
hence thesis by A5,A11,Th7;
end;
hence thesis by A5,A6,A7,A8;
end;
theorem Th11:
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 Th12:
not b _|_ a & x-k*b _|_ a & x-l*b _|_ a implies k = l
proof
assume that
A1: not b _|_ a and
A2: x-k*b _|_ a & x-l*b _|_ a;
set 1F=1_F;
k*b-l*b _|_ a by A2,Th11;
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 Th13:
1_F+1_F<>0.F implies a _|_ a
proof
set 1F = 1_F;
assume
A1: 1_F+1_F<>0.F;
now
assume a <> 0.S;
then consider c such that
A2: not c _|_ a by Def1;
consider k such that
A3: a-k*c _|_ a by A2,Def1;
a _|_ a+(-k*c) by A3,Th2;
then -k*c _|_ a+a by Def1;
then -k*c _|_ a+(1F)*a;
then -k*c _|_ (1F)*a+(1F)*a;
then (-1F)*(k*c) _|_ (1F)*a+(1F)*a by VECTSP_1:14;
then (-1F)*(k*c) _|_ ((1F)+(1F))*a by VECTSP_1:def 15;
then ((-1F)*k)*c _|_ ((1F)+(1F))*a by VECTSP_1:def 16;
then (-(k*(1F)))*c _|_ ((1F)+(1F))*a by VECTSP_1:9;
then (-k)*c _|_ ((1_F)+(1F))*a;
then ((1_F)+(1_F))*a _|_ (-k)*c by Th2;
then ((1_F)+(1_F))"*(((1_F)+(1_F))*a) _|_ (-k)*c by Def1;
then a _|_ (-k)*c by A1,VECTSP_1:20;
then
A4: (-k)*c _|_ a by Th2;
a+(-k)*c _|_ a by A3,VECTSP_1:21;
hence thesis by A4,Th4;
end;
hence thesis by Th1;
end;
:: 5. ORTHOGONAL PROJECTION
definition
let F;
let 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,Th12;
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 Th14:
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 Th15:
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 Th14;
L _|_ a by A2,Th14;
then l*x-(l*ProJ(a,b,x))*b _|_ a by A1,Def1;
hence thesis by A2,A3,Th12;
end;
theorem Th16:
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 = (((-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 Th14;
then
A3: L _|_ a by Def1;
(x+y)-ProJ(a,b,x+y)*b _|_ a by A2,Th14;
hence thesis by A2,A3,A1,Th12;
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 Th14;
A4: L = x-(ProJ(a,l*b,x)*l)*b by VECTSP_1:def 16;
x-ProJ(a,b,x)*b _|_ a by A1,Th14;
then ProJ(a,b,x)*l" = (ProJ(a,l*b,x)*l)*l" by A1,A3,A4,Th12;
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 Th18:
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 Th14;
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,Th14;
hence thesis by A1,A3,Th12;
end;
theorem Th19:
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 Th14;
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,Th14;
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,Th14;
hence thesis by A1,A5,A4,Th12;
end;
theorem Th20:
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,Th14;
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 Th14;
hence thesis by A7,A6,Th12;
end;
theorem Th21:
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,Th14;
hence thesis by A1,Th12;
end;
theorem Th22:
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,Th21;
end;
theorem Th23:
not b _|_ a implies ( x _|_ a iff ProJ(a,b,x) = 0.F )
proof
set 0F = 0.F, 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,Th14;
hence ProJ(a,b,x) = 0.F by A2,A4,Th12;
end;
now
assume ( not b _|_ a)& ProJ(a,b,x) = 0.F;
then x-0F*b _|_ a by Th14;
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 Th24:
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,Th14;
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,Th15;
p-ProJ(a,b,p)*b _|_ a by A1,Th14;
then ProJ(a,q,p)*ProJ(a,b,q) = ProJ(a,b,p) by A1,A3,Th12;
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,Th23;
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 Th25:
not b _|_ a & not c _|_ a implies ProJ(a,b,c) = ProJ(a,c,b)"
proof
set 1F = 1_F, 0F = 0.F;
assume that
A1: not b _|_ a and
A2: not c _|_ a;
A3: ProJ(a,c,b) <> 0F by A1,A2,Th23;
ProJ(a,b,b)*ProJ(a,b,c)" = ProJ(a,c,b) by A1,A2,Th24;
then ProJ(a,b,c)"*1F = ProJ(a,c,b) by A1,Th22;
then
A4: ProJ(a,b,c)" = ProJ(a,c,b);
ProJ(a,b,c) <> 0F by A1,A2,Th23;
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 Th26:
not b _|_ a & b _|_ c+a implies ProJ(a,b,c) = ProJ(c,b,a)
proof
assume that
A1: not b _|_ a and
A2: b _|_ c+a;
ProJ(a,b,c)*b _|_ c+a by A2,Def1;
then
A3: -ProJ(a,b,c)*b _|_ c+a by Th6;
c-ProJ(a,b,c)*b _|_ a by A1,Th14;
then a _|_ -ProJ(a,b,c)*b+c by Th2;
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 not c _|_ b by Th3;
then
A5: not b _|_ c by Th2;
then a-ProJ(c,b,a)*b _|_ c by Th14;
hence thesis by A5,A4,Th12;
end;
theorem Th27:
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;
A3: ProJ(b,a,c) <> 0.F by A1,A2,Th23;
then
A4: -ProJ(b,a,c)" <> 0.F by VECTSP_1:25;
(-1F)*(ProJ(b,a,c)"*ProJ(b,a,c)) = (-1F)*(1F) by A3,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,Th15;
then (-ProJ(b,a,c)")*c-(-1F)*a _|_ b by A1,Th14;
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
A5: 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 A5,Th26;
then ProJ(a,b,(-ProJ(b,a,c)")*c) = ProJ(c,b,a) by A2,A4,Th2,Th18;
hence thesis by A1,Th2,Th15;
end;
theorem Th28:
1_F+1_F<>0.F & not a _|_ p & not a _|_ q & not b _|_ q implies
ProJ(a,p,q)*ProJ(b,q,p) = ProJ(p,a,b)*ProJ(q,b,a)
proof
assume that
A1: 1_F+1_F<>0.F and
A2: not a _|_ p and
A3: not a _|_ q and
A4: not b _|_ q;
A5: now
assume that
A6: p _|_ q and
A7: a _|_ b;
not q _|_ b by A4,Th2;
then
A8: ProJ(b,q,p) = ProJ (b,q,p+a) by A7,Th19;
A9: not p+a _|_ q by A3,A6,Th4;
then
A10: ProJ(b,q,p+a) = (-ProJ(q,p+a,b)")*ProJ(p+a,q,b) by A4,Th27;
A11: a _|_ a by A1,Th13;
A12: not p _|_ a by A2,Th2;
then
A13: ProJ(a,p,q) = ProJ(a,p+a,q) by A11,Th19;
not p+a _|_ a by A12,A11,Th4;
then
A14: not a _|_ p+a by Th2;
A15: not q _|_ p+a by A9,Th2;
then ProJ(a,p+a,q) = (-ProJ(p+a,q,a)")*ProJ(q,p+a,a) by A14,Th27;
then
ProJ(a,p,q)*ProJ(b,q,p) = ((ProJ(q,p+a,a)*(-ProJ(p+a,q,a)"))*(-ProJ(q
,p+a,b)"))*ProJ (p+a,q,b) by A13,A8,A10,GROUP_1:def 3
.= (ProJ(q,p+a,a)*((-ProJ(p+a,q,a)")*(-ProJ(q,p+a,b)")))*ProJ (p+a,q,b
) by GROUP_1:def 3
.= (ProJ(q,p+a,a)*(ProJ(q,p+a,b)"*ProJ(p+a,q,a)"))*ProJ(p+a,q,b) by
VECTSP_1:10
.= ((ProJ(q,p+a,a)*ProJ(q,p+a,b)")*ProJ(p+a,q,a)")*ProJ (p+a,q,b) by
GROUP_1:def 3
.= (ProJ(q,b,a)*ProJ(p+a,q,a)")*ProJ(p+a,q,b) by A4,A9,Th24
.= ProJ(q,b,a)*(ProJ(p+a,q,b)*ProJ(p+a,q,a)") by GROUP_1:def 3
.= ProJ(q,b,a)*ProJ(p+a,a,b) by A14,A15,Th24
.= ProJ(q,b,a)*ProJ(p,a,b) by A2,A7,A11,Th20;
hence thesis;
end;
A16: now
assume
A17: not a _|_ b;
A18: not q _|_ b by A4,Th2;
then
A19: ProJ(q,b,a) = (-ProJ(b,a,q)")*ProJ(a,b,q) by A17,Th27;
A20: not p _|_ a by A2,Th2;
A21: not b _|_ a by A17,Th2;
then ProJ(p,a,b) = (-ProJ(a,b,p)")*ProJ(b,a,p) by A20,Th27;
then
ProJ(p,a,b)*ProJ(q,b,a) = ((ProJ(b,a,p)*(-ProJ(a,b,p)"))*(-ProJ(b,a,q
)"))*ProJ (a,b,q) by A19,GROUP_1:def 3
.= (ProJ(b,a,p)*((-ProJ(a,b,p)")*(-ProJ(b,a,q)")))*ProJ (a,b,q) by
GROUP_1:def 3
.= (ProJ(b,a,p)*(ProJ(b,a,q)"*ProJ(a,b,p)"))*ProJ(a,b,q) by VECTSP_1:10
.= ((ProJ(b,a,p)*ProJ(b,a,q)")*ProJ(a,b,p)")*ProJ(a,b,q) by GROUP_1:def 3
.= (ProJ(b,q,p)*ProJ(a,b,p)")*ProJ(a,b,q) by A17,A18,Th24
.= ProJ(b,q,p)*(ProJ(a,b,q)*ProJ(a,b,p)") by GROUP_1:def 3
.= ProJ(b,q,p)*ProJ(a,p,q) by A21,A20,Th24;
hence thesis;
end;
now
assume
A22: not p _|_ q;
then
A23: ProJ(b,q,p) = (-(ProJ(q,p,b)"))*ProJ(p,q,b) by A4,Th27;
A24: not q _|_ p by A22,Th2;
then ProJ(a,p,q) = (-ProJ(p,q,a)")*ProJ(q,p,a) by A2,Th27;
then
ProJ(a,p,q)*ProJ(b,q,p) = ((ProJ(q,p,a)*(-ProJ(p,q,a)"))*(-ProJ(q,p,b
)"))*ProJ(p,q,b) by A23,GROUP_1:def 3
.= (ProJ(q,p,a)*((-ProJ(p,q,a)")*(-ProJ(q,p,b)")))*ProJ (p,q,b) by
GROUP_1:def 3
.= (ProJ(q,p,a)*(ProJ(q,p,b)"*ProJ(p,q,a)"))*ProJ(p,q,b) by VECTSP_1:10
.= ((ProJ(q,p,a)*ProJ(q,p,b)")*ProJ(p,q,a)")*ProJ(p,q,b) by GROUP_1:def 3
.= (ProJ(q,b,a)*ProJ(p,q,a)")*ProJ(p,q,b) by A4,A22,Th24
.= ProJ(q,b,a)*(ProJ(p,q,b)*ProJ(p,q,a)") by GROUP_1:def 3
.= ProJ(q,b,a)*ProJ(p,a,b) by A2,A24,Th24;
hence thesis;
end;
hence thesis by A16,A5;
end;
theorem Th29:
1_F+1_F<>0.F & not p _|_ a & not p _|_ x & not q _|_ a & not q
_|_ x implies ProJ(a,q,p)*ProJ(p,a,x) = ProJ(x,q,p)*ProJ(q,a,x)
proof
set 0F = 0.F, 1F = 1_F;
assume that
A1: 1_F+1_F<>0.F and
A2: not p _|_ a and
A3: not p _|_ x and
A4: not q _|_ a and
A5: not q _|_ x;
A6: ( not a _|_ q)& not x _|_ q by A4,A5,Th2;
ProJ(p,a,x)*ProJ(q,x,a) = ProJ(a,p,q)*ProJ(x,q,p) by A1,A2,A3,A5,Th28;
then ProJ(p,a,x)*ProJ(q,x,a) = ProJ(a,q,p)"*ProJ(x,q,p) by A2,A4,Th25;
then
A7: ProJ(a,q,p)*(ProJ(p,a,x)*ProJ(q,x,a)) = (ProJ(a,q,p)*ProJ(a,q,p)")*ProJ
(x,q,p) by GROUP_1:def 3;
ProJ(a,q,p) <> 0F by A2,A4,Th23;
then ProJ(a,q,p)*(ProJ(p,a,x)*ProJ(q,x,a)) = ProJ (x,q,p)*(1F) by A7,
VECTSP_1:def 10;
then ProJ(a,q,p)*(ProJ(p,a,x)*ProJ(q,x,a)) = ProJ(x,q,p);
then (ProJ(a,q,p)*ProJ(p,a,x))*ProJ(q,x,a) = ProJ(x,q,p) by GROUP_1:def 3;
then (ProJ(a,q,p)*ProJ(p,a,x))*ProJ(q,a,x)" = ProJ(x,q,p) by A6,Th25;
then
A8: (ProJ(a,q,p)*ProJ(p,a,x))*(ProJ(q,a,x)"*ProJ(q,a,x)) = ProJ(x,q,p)*ProJ
(q,a,x) by GROUP_1:def 3;
ProJ(q,a,x) <> 0F by A6,Th23;
then (ProJ(a,q,p)*ProJ(p,a,x))*(1F) = ProJ(x,q,p)*ProJ (q,a,x) by A8,
VECTSP_1:def 10;
hence thesis;
end;
theorem Th30:
1_F+1_F<>0.F & 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, 1F = 1_F;
assume that
A1: 1_F+1_F<>0.F & 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,Th23;
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,Th29;
then (ProJ(a,b,p)*ProJ(a,b,q)")*ProJ(p,a,x) = ProJ(x,q,p)*ProJ (q,a,x) by
A3,A5,Th24;
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,Th24;
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,Th25;
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,Th23;
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,Th25;
hence thesis by GROUP_1:def 3;
end;
now
assume
A10: y _|_ x;
then ProJ(x,p,y) = 0F by A2,Th23;
then
A11: ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F;
ProJ(x,q,y) = 0F by A4,A10,Th23;
hence thesis by A11;
end;
hence thesis by A6;
end;
theorem Th31:
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, 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,Th23;
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,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 A5,A8,Th27;
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,Th25;
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,Th23;
then ProJ(y,p,x)*ProJ(p,a,y) = ((-ProJ(x,y,p)")*ProJ(p,a,x))*(1F) by A10,
VECTSP_1:def 10;
then ProJ(p,a,y)*ProJ(y,p,x) = (-ProJ(x,y,p)")*ProJ(p,a,x);
then -(ProJ(p,a,y)*ProJ(y,p,x)) = -(-ProJ(x,y,p)"*ProJ (p,a,x)) by
VECTSP_1:9;
then -(ProJ(p,a,y)*ProJ(y,p,x)) = ProJ(x,y,p)"*ProJ(p,a,x) by RLVECT_1:17;
then (-ProJ(p,a,y))*ProJ(y,p,x) = ProJ(x,y,p)"*ProJ(p,a,x) by VECTSP_1:9;
hence thesis by A5,A8,Th25;
end;
now
assume
A11: y _|_ x;
then ProJ(x,p,y) = 0F by A5,Th23;
then
A12: ProJ(p,a,x)*ProJ(x,p,y) = 0F;
x _|_ y by A11,Th2;
then ProJ(y,p,x) = 0F by A4,Th23;
hence thesis by A12;
end;
hence thesis by A6;
end;
:: 6. BILINEAR ANTISYMMETRIC FORM
definition
let F,S,x,y,a,b;
assume
A1: ( not b _|_ a)& 1_F+1_F<>0.F;
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,Th30;
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 Th32:
1_F+1_F<>0.F & not b _|_ a & x=0.S implies PProJ(a,b,x,y) = 0.F
proof
assume that
A1: 1_F+1_F<>0.F & 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 Th33:
1_F+1_F<>0.F & not b _|_ a implies (PProJ(a,b,x,y) = 0.F iff y _|_ x)
proof
set 0F = 0.F;
assume that
A1: 1_F+1_F<>0.F and
A2: not b _|_ a;
A3: a<>0.S by A2,Th1,Th2;
A4: PProJ(a,b,x,y) = 0.F implies y _|_ x
proof
assume
A5: PProJ(a,b,x,y) = 0.F;
A6: now
given p such that
A7: not p _|_ a and
A8: not p _|_ x;
A9: now
assume
A10: ProJ(p,a,x) = 0.F;
not a _|_ p by A7,Th2;
then x _|_ p by A10,Th23;
hence contradiction by A8,Th2;
end;
ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0F by A1,A2,A5,A7,A8,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 A2,A7,A8,A9,Th23;
end;
now
assume for p holds p _|_ a or p _|_ x;
then x = 0.S by A3,Th9;
hence thesis by Th1,Th2;
end;
hence thesis by A6;
end;
y _|_ x implies PProJ(a,b,x,y) = 0.F
proof
assume
A11: y _|_ x;
A12: now
assume x<>0.S;
then consider p such that
A13: not p _|_ a and
A14: not p _|_ x by A3,Th9;
ProJ(x,p,y) = 0F by A11,A14,Th23;
then ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) = 0.F;
hence thesis by A1,A2,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,A2,Def3;
end;
hence thesis by A12;
end;
hence thesis by A4;
end;
theorem
1_F+1_F<>0.F & not b _|_ a implies PProJ(a,b,x,y) = -PProJ(a,b,y,x)
proof
set 0F = 0.F, 1F = 1_F;
assume that
A1: 1_F+1_F<>0.F and
A2: not b _|_ a;
A3: now
assume not x _|_ y;
then
A4: x <> 0.S & y <> 0.S by Th1,Th2;
a <> 0.S by A2,Th1,Th2;
then consider r such that
A5: not r _|_ a and
A6: not r _|_ x and
A7: not r _|_ y by A1,A4,Th10;
A8: not y _|_ r by A7,Th2;
PProJ(a,b,y,x) = ProJ(a,b,r)*ProJ(r,a,y)*ProJ(y,r,x) by A1,A2,A5,A7,Def3;
then
A9: 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 A5,A6,Th2;
then PProJ(a,b,y,x) = ProJ(a,b,r)*((-(ProJ(r,a,x)))*ProJ (x,r,y)) by A8,A9
,Th31;
then PProJ(a,b,y,x) = ((-(ProJ(r,a,x)))*ProJ(a,b,r))*ProJ (x,r,y) by
GROUP_1:def 3;
then PProJ(a,b,y,x) = (-ProJ(r,a,x)*ProJ(a,b,r))*ProJ (x,r,y) by VECTSP_1:9
;
then (-1F)*PProJ(a,b,y,x) = (-1F)*(-ProJ(a,b,r)*ProJ(r,a,x)*ProJ (x,r,y))
by VECTSP_1:9;
then
-(PProJ(a,b,y,x)*(1F)) = (-1F)*(-ProJ(a,b,r)*ProJ(r,a,x)*ProJ (x,r,y)
) by VECTSP_1:9;
then -PProJ(a,b,y,x) = (-1F)*(-ProJ(a,b,r)*ProJ(r,a,x)*ProJ (x,r,y));
then
A10: -PProJ(a,b,y,x) = (ProJ(a,b,r)*ProJ(r,a,x)*ProJ (x,r,y))*(1F) by
VECTSP_1:10;
PProJ(a,b,x,y) = ProJ(a,b,r)*ProJ(r,a,x)*ProJ(x,r,y) by A1,A2,A5,A6,Def3;
hence thesis by A10;
end;
now
assume
A11: x _|_ y;
then (-1F)*PProJ(a,b,y,x) = (-1F)*0F by A1,A2,Th33;
then -(PProJ (a,b,y,x)*(1F)) = (-1F)*0F by VECTSP_1:9;
then
A12: -PProJ(a,b,y,x) = (-1F)*0F;
y _|_ x by A11,Th2;
then PProJ(a,b,x,y) = 0F by A1,A2,Th33;
hence thesis by A12;
end;
hence thesis by A3;
end;
theorem
1_F+1_F<>0.F & not b _|_ a implies PProJ(a,b,x,l*y) = l*PProJ(a,b,x,y)
proof
set 0F = 0.F;
assume that
A1: 1_F+1_F<>0.F and
A2: not b _|_ a;
A3: now
assume not x _|_ y;
then
A4: x <> 0.S by Th1;
a <> 0.S by A2,Th1,Th2;
then consider p such that
A5: not p _|_ a and
A6: not p _|_ x by A4,Th9;
PProJ(a,b,x,l*y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ (x,p,l*y) by A1,A2,A5,A6
,Def3;
then
A7: PProJ(a,b,x,l*y) = (l*ProJ(x,p,y))*(ProJ(a,b,p)*ProJ(p,a,x)) by A6,Th15;
PProJ(a,b,x,y) = ProJ(a,b,p)*ProJ(p,a,x)*ProJ(x,p,y) by A1,A2,A5,A6,Def3;
hence thesis by A7,GROUP_1:def 3;
end;
now
assume
A8: x _|_ y;
then y _|_ x by Th2;
then l*y _|_ x by Def1;
then
A9: PProJ(a,b,x,l*y) = 0F by A1,A2,Th33;
y _|_ x by A8,Th2;
then l*PProJ(a,b,x,y) = l*0F by A1,A2,Th33;
hence thesis by A9;
end;
hence thesis by A3;
end;
theorem
1_F+1_F<>0.F & not b _|_ a implies PProJ(a,b,x,y+z) = PProJ(a,b,x,y) +
PProJ (a,b,x,z)
proof
assume that
A1: 1_F+1_F<>0.F and
A2: not b _|_ a;
A3: now
assume
A4: x <> 0.S;
a <> 0.S by A2,Th1,Th2;
then consider p such that
A5: ( not p _|_ a)& not p _|_ x by A4,Th9;
A6: 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,A2,A5,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,A2,A5,Def3,Th16;
hence thesis by A6,VECTSP_1:def 7;
end;
set 0F = 0.F;
now
assume
A7: x = 0.S;
then
A8: PProJ (a,b,x,z) = 0F by A1,A2,Th32;
PProJ(a,b,x,y+z) = 0F & PProJ(a,b,x,y) = 0F by A1,A2,A7,Th32;
hence thesis by A8,RLVECT_1:4;
end;
hence thesis by A3;
end;