:: 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-2012 Association of Mizar Users


begin

reconsider X = {0} as non empty set ;

reconsider o = 0 as Element of X by TARSKI:def_1;

deffunc H1( Element of X, 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) = H1(x,y) from BINOP_1:sch_4();

Lm2: now__::_thesis:_for_F_being_Field_ex_mo_being_Relation_of_X_st_
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_)_)_)
defpred S1[ set ] means  ex a, b being Element of X st
( $1 = [a,b] & b = o );
set CV = [:X,X:];
let F be Field; ::_thesis: ex mo being Relation of X st
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 ) ) )
consider mo being set  such that
A1: for x being set holds
( x in mo iff ( x in [:X,X:] & S1[x] ) ) from XBOOLE_0:sch_1();
 mo c= [:X,X:]
proof
let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in mo or x in [:X,X:] )
thus  ( not x in mo or x in [:X,X:] ) by A1; ::_thesis: verum
end;
then reconsider mo = mo as Relation of X ;
take mo = mo; ::_thesis: 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 ) ) )
thus  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 A1; ::_thesis: verum
end;

Lm3:  for F being Field
for mF being Function of [: the carrier of F,X:],X
for mo being Relation of X holds
( SymStr(# X,md,o,mF,mo #) is Abelian & SymStr(# X,md,o,mF,mo #) is add-associative & SymStr(# X,md,o,mF,mo #) is right_zeroed & SymStr(# X,md,o,mF,mo #) is right_complementable )
proofend;

Lm4: now__::_thesis:_for_F_being_Field
for_mF_being_Function_of_[:_the_carrier_of_F,X:],X_st_(_for_a_being_Element_of_F
for_x_being_Element_of_X_holds_mF_._[a,x]_=_o_)_holds_
for_mo_being_Relation_of_X
for_MPS_being_non_empty_right_complementable_Abelian_add-associative_right_zeroed_SymStr_over_F_st_MPS_=_SymStr(#_X,md,o,mF,mo_#)_holds_
(_MPS_is_vector-distributive_&_MPS_is_scalar-distributive_&_MPS_is_scalar-associative_&_MPS_is_scalar-unital_)
let F be Field; ::_thesis: for mF being Function of [: the carrier of F,X:],X st ( for a being Element of F
for x being Element of X holds mF . [a,x] = o ) holds
for mo being Relation of X
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# X,md,o,mF,mo #) holds
( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )
let mF be Function of [: the carrier of F,X:],X; ::_thesis: ( ( for a being Element of F
for x being Element of X holds mF . [a,x] = o ) implies for mo being Relation of X
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# X,md,o,mF,mo #) holds
( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) )
assume A1: for a being Element of F
for x being Element of X holds mF . [a,x] = o ; ::_thesis: for mo being Relation of X
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# X,md,o,mF,mo #) holds
( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )
let mo be Relation of X; ::_thesis: for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# X,md,o,mF,mo #) holds
( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )
let MPS be non empty right_complementable Abelian add-associative right_zeroed SymStr over F; ::_thesis: ( MPS = SymStr(# X,md,o,mF,mo #) implies ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) )
assume A2: MPS = SymStr(# X,md,o,mF,mo #) ; ::_thesis: ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )
 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; ::_thesis: 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 )
let v, w be Element of MPS; ::_thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ F) * v = v )
A3: (x * y) * v = x * (y * v)
proof
set z = x * y;
A4: (x * y) * v = mF . ((x * y),v) by A2, VECTSP_1:def_12;
reconsider v = v as Element of MPS ;
reconsider v = v as Element of MPS ;
A5: (x * y) * v = o by A1, A2, A4;
reconsider v = v as Element of MPS ;
A6: mF . (y,v) = o by A1, A2;
reconsider v = 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  (x * y) * v = x * (y * v) by A1, A5; ::_thesis: verum
end;
A7: x * (v + w) = (x * v) + (x * w)
proof
reconsider v = v, w = w as Element of MPS ;
A8: o = 0. MPS by A2, STRUCT_0:def_6;
reconsider v = v, w = w as Element of X by A2;
A9: md . (v,w) = o by Lm1;
reconsider v = v, w = 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 = w as Element of MPS ;
reconsider v = v as Element of MPS ;
A11: mF . (x,v) = o by A1;
reconsider v = v as Element of MPS ;
A12: mF . (x,w) = o by A1;
reconsider w = 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  x * (v + w) = (x * v) + (x * w) by A10, A13, A8, RLVECT_1:4; ::_thesis: verum
end;
A14: (x + y) * v = (x * v) + (y * v)
proof
set z = x + y;
A15: (x + y) * v = mF . ((x + y),v) by A2, VECTSP_1:def_12;
reconsider v = v as Element of MPS ;
reconsider v = v as Element of MPS ;
A16: (x + y) * v = o by A1, A2, A15;
reconsider v = v as Element of MPS ;
A17: mF . (x,v) = o by A1, A2;
reconsider v = v as Element of MPS ;
A18: x * v = o by A2, A17, VECTSP_1:def_12;
reconsider v = v as Element of MPS ;
A19: mF . (y,v) = o by A1, A2;
A20: o = 0. MPS by A2, STRUCT_0:def_6;
reconsider v = v as Element of MPS ;
 y * v = o by A2, A19, VECTSP_1:def_12;
hence  (x + y) * v = (x * v) + (y * v) by A16, A18, A20, RLVECT_1:4; ::_thesis: verum
end;
 (1_ F) * v = v
proof
set one1 = 1_ F;
A21: (1_ F) * v = mF . ((1_ F),v) by A2, VECTSP_1:def_12;
reconsider v = v as Element of MPS ;
 mF . ((1_ F),v) = o by A1, A2;
hence  (1_ F) * v = v by A2, A21, TARSKI:def_1; ::_thesis: verum
end;
hence  ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ F) * v = v ) by A7, A14, A3; ::_thesis: verum
end;
hence  ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) by VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17; ::_thesis: verum
end;

Lm5: now__::_thesis:_for_F_being_Field
for_mF_being_Function_of_[:_the_carrier_of_F,X:],X
for_mo_being_Relation_of_X_st_(_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_)_)_)_)_holds_
for_MPS_being_non_empty_right_complementable_Abelian_add-associative_right_zeroed_SymStr_over_F_st_MPS_=_SymStr(#_X,md,o,mF,mo_#)_holds_
(_(_for_a,_b,_c,_d_being_Element_of_MPS_st_a_<>_0._MPS_&amp;_b_<>_0._MPS_&amp;_c_<>_0._MPS_&amp;_d_<>_0._MPS_holds_
ex_p_being_Element_of_MPS_st_
(_not_a__|__&amp;_not_b__|__&amp;_not_c__|__&amp;_not_d__|__)_)_&amp;_(_for_a,_b_being_Element_of_MPS
for_l_being_Element_of_F_st_b__|__holds_
b__|__)_&amp;_(_for_a,_b,_c_being_Element_of_MPS_st_a__|__&amp;_a__|__holds_
a__|__)_&amp;_(_for_a,_b,_x_being_Element_of_MPS_st_not_a__|__holds_
ex_k_being_Element_of_F_st_a__|__)_&amp;_(_for_a,_b,_c_being_Element_of_MPS_st_b_-_c__|__&amp;_c_-_a__|__holds_
a_-_b__|__)_)
set CV = [:X,X:];
let F be Field; ::_thesis: for mF being Function of [: the carrier of F,X:],X
for mo being Relation of X st ( for x being set holds
( x in mo iff ( x in [:X,X:] &amp; ex a, b being Element of X st
( x = [a,b] &amp; b = o ) ) ) ) holds
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# X,md,o,mF,mo #) holds
( ( for a, b, c, d being Element of MPS st a <> 0. MPS &amp; b <> 0. MPS &amp; c <> 0. MPS &amp; d <> 0. MPS holds
ex p being Element of MPS st
( not a _|_ &amp; not b _|_ &amp; not c _|_ &amp; not d _|_ ) ) &amp; ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) &amp; ( for a, b, c being Element of MPS st a _|_ &amp; a _|_ holds
a _|_ ) &amp; ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) &amp; ( for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_ ) )
let mF be Function of [: the carrier of F,X:],X; ::_thesis: for mo being Relation of X st ( for x being set holds
( x in mo iff ( x in [:X,X:] &amp; ex a, b being Element of X st
( x = [a,b] &amp; b = o ) ) ) ) holds
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# X,md,o,mF,mo #) holds
( ( for a, b, c, d being Element of MPS st a <> 0. MPS &amp; b <> 0. MPS &amp; c <> 0. MPS &amp; d <> 0. MPS holds
ex p being Element of MPS st
( not a _|_ &amp; not b _|_ &amp; not c _|_ &amp; not d _|_ ) ) &amp; ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) &amp; ( for a, b, c being Element of MPS st a _|_ &amp; a _|_ holds
a _|_ ) &amp; ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) &amp; ( for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_ ) )
let mo be Relation of X; ::_thesis: ( ( for x being set holds
( x in mo iff ( x in [:X,X:] &amp; ex a, b being Element of X st
( x = [a,b] &amp; b = o ) ) ) ) implies for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# X,md,o,mF,mo #) holds
( ( for a, b, c, d being Element of MPS st a <> 0. MPS &amp; b <> 0. MPS &amp; c <> 0. MPS &amp; d <> 0. MPS holds
ex p being Element of MPS st
( not a _|_ &amp; not b _|_ &amp; not c _|_ &amp; not d _|_ ) ) &amp; ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) &amp; ( for a, b, c being Element of MPS st a _|_ &amp; a _|_ holds
a _|_ ) &amp; ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) &amp; ( for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_ ) ) )
assume A1: for x being set holds
( x in mo iff ( x in [:X,X:] &amp; ex a, b being Element of X st
( x = [a,b] &amp; b = o ) ) ) ; ::_thesis: for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# X,md,o,mF,mo #) holds
( ( for a, b, c, d being Element of MPS st a <> 0. MPS &amp; b <> 0. MPS &amp; c <> 0. MPS &amp; d <> 0. MPS holds
ex p being Element of MPS st
( not a _|_ &amp; not b _|_ &amp; not c _|_ &amp; not d _|_ ) ) &amp; ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) &amp; ( for a, b, c being Element of MPS st a _|_ &amp; a _|_ holds
a _|_ ) &amp; ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) &amp; ( for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_ ) )
let MPS be non empty right_complementable Abelian add-associative right_zeroed SymStr over F; ::_thesis: ( MPS = SymStr(# X,md,o,mF,mo #) implies ( ( for a, b, c, d being Element of MPS st a <> 0. MPS &amp; b <> 0. MPS &amp; c <> 0. MPS &amp; d <> 0. MPS holds
ex p being Element of MPS st
( not a _|_ &amp; not b _|_ &amp; not c _|_ &amp; not d _|_ ) ) &amp; ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) &amp; ( for a, b, c being Element of MPS st a _|_ &amp; a _|_ holds
a _|_ ) &amp; ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) &amp; ( for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_ ) ) )
assume A2: MPS = SymStr(# X,md,o,mF,mo #) ; ::_thesis: ( ( for a, b, c, d being Element of MPS st a <> 0. MPS &amp; b <> 0. MPS &amp; c <> 0. MPS &amp; d <> 0. MPS holds
ex p being Element of MPS st
( not a _|_ &amp; not b _|_ &amp; not c _|_ &amp; not d _|_ ) ) &amp; ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) &amp; ( for a, b, c being Element of MPS st a _|_ &amp; a _|_ holds
a _|_ ) &amp; ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) &amp; ( for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_ ) )
 0. MPS = o by A2, TARSKI:def_1;
hence  for a, b, c, d being Element of MPS st a <> 0. MPS &amp; b <> 0. MPS &amp; c <> 0. MPS &amp; d <> 0. MPS holds
ex p being Element of MPS st
( not a _|_ &amp; not b _|_ &amp; not c _|_ &amp; not d _|_ ) by A2, TARSKI:def_1; ::_thesis: ( ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) &amp; ( for a, b, c being Element of MPS st a _|_ &amp; a _|_ holds
a _|_ ) &amp; ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) &amp; ( for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_ ) )
A3: for a, b being Element of MPS holds
( b _|_ iff ( [a,b] in [:X,X:] &amp; ex c, d being Element of X st
( [a,b] = [c,d] &amp; d = o ) ) )
proof
let a, b be Element of MPS; ::_thesis: ( b _|_ iff ( [a,b] in [:X,X:] &amp; ex c, d being Element of X st
( [a,b] = [c,d] &amp; d = o ) ) )
 ( b _|_ iff [a,b] in mo ) by A2, ORDERS_2:def_5;
hence  ( b _|_ iff ( [a,b] in [:X,X:] &amp; ex c, d being Element of X st
( [a,b] = [c,d] &amp; d = o ) ) ) by A1; ::_thesis: verum
end;
A4: for a, b being Element of MPS holds
( b _|_ iff b = o )
proof
let a, b be Element of MPS; ::_thesis: ( b _|_ iff b = o )
A5: ( b = o implies b _|_ )
proof
consider c, d being Element of MPS such that
A6: ( c = a &amp; d = b ) ;
assume A7: b = o ; ::_thesis: b _|_
 [a,b] = [c,d] by A6;
hence  b _|_ by A2, A3, A7; ::_thesis: verum
end;
 ( b _|_ implies b = o )
proof
assume  b _|_ ; ::_thesis: b = o
then  ex c, d being Element of X st
( [a,b] = [c,d] &amp; d = o ) by A3;
hence  b = o by XTUPLE_0:1; ::_thesis: verum
end;
hence  ( b _|_ iff b = o ) by A5; ::_thesis: verum
end;
thus  for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ::_thesis: ( ( for a, b, c being Element of MPS st a _|_ &amp; a _|_ holds
a _|_ ) &amp; ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) &amp; ( for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_ ) )
proof
let a, b be Element of MPS; ::_thesis: for l being Element of F st b _|_ holds
b _|_
let l be Element of F; ::_thesis: ( b _|_ implies b _|_ )
assume  b _|_ ; ::_thesis: b _|_
then  b = o by A4;
hence  b _|_ by A4; ::_thesis: verum
end;
thus  for a, b, c being Element of MPS st a _|_ &amp; a _|_ holds
a _|_ ::_thesis: ( ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) &amp; ( for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_ ) )
proof
let a, b, c be Element of MPS; ::_thesis: ( a _|_ &amp; a _|_ implies a _|_ )
assume that
A8: a _|_ and
 a _|_ ; ::_thesis: a _|_
 a = o by A4, A8;
hence  a _|_ by A4; ::_thesis: verum
end;
thus  for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ::_thesis: for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_
proof
let a, b, x be Element of MPS; ::_thesis: ( not a _|_ implies ex k being Element of F st a _|_ )
assume A9: not a _|_ ; ::_thesis: ex k being Element of F st a _|_
assume  for k being Element of F holds not a _|_ ; ::_thesis: contradiction
 a <> o by A4, A9;
hence  contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
thus  for a, b, c being Element of MPS st b - c _|_ &amp; c - a _|_ holds
a - b _|_ ::_thesis: verum
proof
let a, b, c be Element of MPS; ::_thesis: ( b - c _|_ &amp; c - a _|_ implies a - b _|_ )
assume that
 b - c _|_ and
 c - a _|_ ; ::_thesis: a - b _|_
assume  not a - b _|_ ; ::_thesis: contradiction
then  a - b <> o by A4;
hence  contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
end;

:: 2. ORTHOGONAL VECTOR SPACE
definition
let F be Field;
let IT be non empty right_complementable Abelian add-associative right_zeroed SymStr over F;
attrIT is OrtSp-like  means :Def1: :: ORTSP_1:def 1
 for a, b, c, d, x being Element of IT
for l being Element of F holds
( ( a <> 0. IT &amp; b <> 0. IT &amp; c <> 0. IT &amp; d <> 0. IT implies ex p being Element of IT st
( not a _|_ &amp; not b _|_ &amp; not c _|_ &amp; not d _|_ ) ) &amp; ( b _|_ implies b _|_ ) &amp; ( a _|_ &amp; a _|_ implies a _|_ ) &amp; ( not a _|_ implies ex k being Element of F st a _|_ ) &amp; ( b - c _|_ &amp; c - a _|_ implies a - b _|_ ) );
end;

:: deftheorem Def1 defines OrtSp-like ORTSP_1:def_1_:_
 for F being Field
for IT being non empty right_complementable Abelian add-associative right_zeroed SymStr over F holds
( IT is OrtSp-like iff for a, b, c, d, x being Element of IT
for l being Element of F holds
( ( a <> 0. IT &amp; b <> 0. IT &amp; c <> 0. IT &amp; d <> 0. IT implies ex p being Element of IT st
( not a _|_ &amp; not b _|_ &amp; not c _|_ &amp; not d _|_ ) ) &amp; ( b _|_ implies b _|_ ) &amp; ( a _|_ &amp; a _|_ implies a _|_ ) &amp; ( not a _|_ implies ex k being Element of F st a _|_ ) &amp; ( b - c _|_ &amp; c - a _|_ implies a - b _|_ ) ) );

registration
let F be Field;
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict OrtSp-like for SymStr over F;
existence
 ex b1 being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st
( b1 is OrtSp-like &amp; b1 is vector-distributive &amp; b1 is scalar-distributive &amp; b1 is scalar-associative &amp; b1 is scalar-unital &amp; b1 is strict )
proofend;
end;

definition
let F be Field;
mode OrtSp of F is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital OrtSp-like SymStr over F;
end;

theorem Th1: :: ORTSP_1:1
for F being Field
for S being OrtSp of F
for a being Element of S holds a _|_
proofend;

theorem Th2: :: ORTSP_1:2
for F being Field
for S being OrtSp of F
for a, b being Element of S st b _|_ holds
a _|_
proofend;

theorem Th3: :: ORTSP_1:3
for F being Field
for S being OrtSp of F
for a, b, c being Element of S st not b _|_ &amp; b _|_ holds
not b _|_
proofend;

theorem Th4: :: ORTSP_1:4
for F being Field
for S being OrtSp of F
for b, a, c being Element of S st not a _|_ &amp; a _|_ holds
not a _|_
proofend;

theorem Th5: :: ORTSP_1:5
for F being Field
for S being OrtSp of F
for b, a being Element of S
for l being Element of F st not a _|_ &amp; not l = 0. F holds
( not a _|_ &amp; not l * a _|_ )
proofend;

theorem Th6: :: ORTSP_1:6
for F being Field
for S being OrtSp of F
for a, b being Element of S st b _|_ holds
b _|_
proofend;

theorem Th7: :: ORTSP_1:7
for F being Field
for S being OrtSp of F
for a, b, d, c being Element of S st d _|_ &amp; d _|_ holds
d _|_
proofend;

theorem Th8: :: ORTSP_1:8
for F being Field
for S being OrtSp of F
for b, a, x being Element of S
for k, l being Element of F st not a _|_ &amp; a _|_ &amp; a _|_ holds
k = l
proofend;

theorem Th9: :: ORTSP_1:9
for F being Field
for S being OrtSp of F
for a, b being Element of S st a _|_ &amp; b _|_ holds
a - b _|_
proofend;

theorem :: ORTSP_1:10
for F being Field
for S being OrtSp of F st (1_ F) + (1_ F) <> 0. F &amp; ex a being Element of S st a <> 0. S holds
ex b being Element of S st not b _|_
proofend;

:: 5. ORTHOGONAL PROJECTION
definition
let F be Field;
let S be OrtSp of F;
let a, b, x be Element of S;
assume A1: not a _|_ ;
func ProJ (a,b,x) ->  Element of F means :Def2: :: ORTSP_1:def 2
 for l being Element of F st a _|_ holds
it = l;
existence
 ex b1 being Element of F st
for l being Element of F st a _|_ holds
b1 = l
proofend;
uniqueness
 for b1, b2 being Element of F st ( for l being Element of F st a _|_ holds
b1 = l ) &amp; ( for l being Element of F st a _|_ holds
b2 = l ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines ProJ ORTSP_1:def_2_:_
 for F being Field
for S being OrtSp of F
for a, b, x being Element of S st not a _|_ holds
for b6 being Element of F holds
( b6 = ProJ (a,b,x) iff for l being Element of F st a _|_ holds
b6 = l );

theorem Th11: :: ORTSP_1:11
for F being Field
for S being OrtSp of F
for b, a, x being Element of S st not a _|_ holds
a _|_
proofend;

theorem Th12: :: ORTSP_1:12
for F being Field
for S being OrtSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ holds
ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
proofend;

theorem Th13: :: ORTSP_1:13
for F being Field
for S being OrtSp of F
for b, a, x, y being Element of S st not a _|_ holds
ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y))
proofend;

theorem :: ORTSP_1:14
for F being Field
for S being OrtSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ &amp; l <> 0. F holds
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
proofend;

theorem Th15: :: ORTSP_1:15
for F being Field
for S being OrtSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ &amp; l <> 0. F holds
ProJ ((l * a),b,x) = ProJ (a,b,x)
proofend;

theorem :: ORTSP_1:16
for F being Field
for S being OrtSp of F
for b, a, p, c being Element of S st not a _|_ &amp; a _|_ holds
( ProJ (a,(b + p),c) = ProJ (a,b,c) &amp; ProJ (a,b,(c + p)) = ProJ (a,b,c) )
proofend;

theorem :: ORTSP_1:17
for F being Field
for S being OrtSp of F
for b, a, p, c being Element of S st not a _|_ &amp; b _|_ &amp; c _|_ holds
ProJ ((a + p),b,c) = ProJ (a,b,c)
proofend;

theorem Th18: :: ORTSP_1:18
for F being Field
for S being OrtSp of F
for b, a, c being Element of S st not a _|_ &amp; a _|_ holds
ProJ (a,b,c) = 1_ F
proofend;

theorem Th19: :: ORTSP_1:19
for F being Field
for S being OrtSp of F
for b, a being Element of S st not a _|_ holds
ProJ (a,b,b) = 1_ F
proofend;

theorem Th20: :: ORTSP_1:20
for F being Field
for S being OrtSp of F
for b, a, x being Element of S st not a _|_ holds
( a _|_ iff ProJ (a,b,x) = 0. F )
proofend;

theorem Th21: :: ORTSP_1:21
for F being Field
for S being OrtSp of F
for b, a, q, p being Element of S st not a _|_ &amp; not a _|_ holds
(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)
proofend;

theorem Th22: :: ORTSP_1:22
for F being Field
for S being OrtSp of F
for b, a, c being Element of S st not a _|_ &amp; not a _|_ holds
ProJ (a,b,c) = (ProJ (a,c,b)) "
proofend;

theorem Th23: :: ORTSP_1:23
for F being Field
for S being OrtSp of F
for b, a, c being Element of S st not a _|_ &amp; c + a _|_ holds
ProJ (a,b,c) = - (ProJ (c,b,a))
proofend;

theorem Th24: :: ORTSP_1:24
for F being Field
for S being OrtSp of F
for a, b, c being Element of S st not b _|_ &amp; not b _|_ holds
ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c))
proofend;

theorem Th25: :: ORTSP_1:25
for F being Field
for S being OrtSp of F
for p, a, x, q being Element of S st not a _|_ &amp; not x _|_ &amp; not a _|_ &amp; not x _|_ holds
(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (ProJ (x,q,p))
proofend;

theorem Th26: :: ORTSP_1:26
for F being Field
for S being OrtSp of F
for p, a, x, q, b, y being Element of S st not a _|_ &amp; not x _|_ &amp; not a _|_ &amp; not x _|_ &amp; not a _|_ holds
((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
proofend;

theorem Th27: :: ORTSP_1:27
for F being Field
for S being OrtSp of F
for a, p, x, y being Element of S st not p _|_ &amp; not p _|_ &amp; not p _|_ holds
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))
proofend;

:: 6. BILINEAR SYMMETRIC FORM
definition
let F be Field;
let S be OrtSp of F;
let x, y, a, b be Element of S;
assume A1: not a _|_ ;
func PProJ (a,b,x,y) ->  Element of F means :Def3: :: ORTSP_1:def 3
 for q being Element of S st not a _|_ &amp; not x _|_ holds
it = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) if  ex p being Element of S st
( not a _|_ &amp; not x _|_ )
otherwise it = 0. F;
existence
 ( ( ex p being Element of S st
( not a _|_ &amp; not x _|_ ) implies ex b1 being Element of F st
for q being Element of S st not a _|_ &amp; not x _|_ holds
b1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) &amp; ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies ex b1 being Element of F st b1 = 0. F ) )
proofend;
uniqueness
 for b1, b2 being Element of F holds
( ( ex p being Element of S st
( not a _|_ &amp; not x _|_ ) &amp; ( for q being Element of S st not a _|_ &amp; not x _|_ holds
b1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) &amp; ( for q being Element of S st not a _|_ &amp; not x _|_ holds
b2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) implies b1 = b2 ) &amp; ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) &amp; b1 = 0. F &amp; b2 = 0. F implies b1 = b2 ) )
proofend;
consistency
 for b1 being Element of F holds verum ;
end;

:: deftheorem Def3 defines PProJ ORTSP_1:def_3_:_
 for F being Field
for S being OrtSp of F
for x, y, a, b being Element of S st not a _|_ holds
for b7 being Element of F holds
( ( ex p being Element of S st
( not a _|_ &amp; not x _|_ ) implies ( b7 = PProJ (a,b,x,y) iff for q being Element of S st not a _|_ &amp; not x _|_ holds
b7 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) ) &amp; ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies ( b7 = PProJ (a,b,x,y) iff b7 = 0. F ) ) );

theorem Th28: :: ORTSP_1:28
for F being Field
for S being OrtSp of F
for b, a, x, y being Element of S st not a _|_ &amp; x = 0. S holds
PProJ (a,b,x,y) = 0. F
proofend;

theorem Th29: :: ORTSP_1:29
for F being Field
for S being OrtSp of F
for b, a, x, y being Element of S st not a _|_ holds
( PProJ (a,b,x,y) = 0. F iff x _|_ )
proofend;

theorem :: ORTSP_1:30
for F being Field
for S being OrtSp of F
for b, a, x, y being Element of S st not a _|_ holds
PProJ (a,b,x,y) = PProJ (a,b,y,x)
proofend;

theorem :: ORTSP_1:31
for F being Field
for S being OrtSp of F
for b, a, x, y being Element of S
for l being Element of F st not a _|_ holds
PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
proofend;

theorem :: ORTSP_1:32
for F being Field
for S being OrtSp of F
for b, a, x, y, z being Element of S st not a _|_ holds
PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
proofend;