:: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski

::

:: Received November 23, 1989

:: Copyright (c) 1990-2021 Association of Mizar Users

reconsider X = {0} as non empty set ;

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

deffunc H

consider md being BinOp of X such that

Lm1: for x, y being Element of X holds md . (x,y) = H

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 ) ) )

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 S_{1}[ object ] 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 object holds

( x in mo iff ( x in [:X,X:] & S_{1}[x] ) )
from XBOOLE_0:sch 1();

mo c= [:X,X:] by A1;

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;
( $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 object holds

( x in mo iff ( x in [:X,X:] & S

mo c= [:X,X:] by A1;

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

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 )

proof end;

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 )

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 )

end;
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

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
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)

end;
( 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

A7:
x * (v + w) = (x * v) + (x * w)
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;
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

proof

A14:
(x + y) * v = (x * v) + (y * v)
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;
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

proof

(1_ F) * v = v
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;
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

proof

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
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;
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

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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_ ) )

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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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:] & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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:] & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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:] & ex a, b being Element of X st

( x = [a,b] & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_ ) ) )

assume 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 ) ) ) ; :: 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & 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 _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_ ) )

A3: for a, b being Element of MPS holds

( b _|_ iff ( [a,b] in [:X,X:] & ex c, d being Element of X st

( [a,b] = [c,d] & d = o ) ) )

( b _|_ iff b = o )

for l being Element of F st b _|_ holds

b _|_ :: thesis: ( ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_ ) )

a _|_ :: thesis: ( ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_ ) )

ex k being Element of F st a _|_ :: thesis: for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_

a - b _|_ :: thesis: verum

end;
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:] & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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:] & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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:] & ex a, b being Element of X st

( x = [a,b] & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_ ) ) )

assume 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 ) ) ) ; :: 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of MPS

for l being Element of F st b _|_ holds

b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & 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 & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds

ex p being Element of MPS st

( not a _|_ & not b _|_ & not c _|_ & 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 _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_ ) )

A3: for a, b being Element of MPS holds

( b _|_ iff ( [a,b] in [:X,X:] & ex c, d being Element of X st

( [a,b] = [c,d] & d = o ) ) )

proof

A4:
for a, b being Element of MPS holds
let a, b be Element of MPS; :: thesis: ( b _|_ iff ( [a,b] in [:X,X:] & ex c, d being Element of X st

( [a,b] = [c,d] & d = o ) ) )

( b _|_ iff [a,b] in mo ) by A2, ORDERS_2:def 5;

hence ( b _|_ iff ( [a,b] in [:X,X:] & ex c, d being Element of X st

( [a,b] = [c,d] & d = o ) ) ) by A1; :: thesis: verum

end;
( [a,b] = [c,d] & d = o ) ) )

( b _|_ iff [a,b] in mo ) by A2, ORDERS_2:def 5;

hence ( b _|_ iff ( [a,b] in [:X,X:] & ex c, d being Element of X st

( [a,b] = [c,d] & d = o ) ) ) by A1; :: thesis: verum

( b _|_ iff b = o )

proof

thus
for a, b being Element of MPS
let a, b be Element of MPS; :: thesis: ( b _|_ iff b = o )

A5: ( b = o implies b _|_ )

end;
A5: ( b = o implies b _|_ )

proof

( b _|_ implies b = o )
consider c, d being Element of MPS such that

A6: ( c = a & d = b ) ;

assume A7: b = o ; :: thesis: b _|_

[a,b] = [c,d] by A6;

hence b _|_ by A2, A3, A7; :: thesis: verum

end;
A6: ( c = a & d = b ) ;

assume A7: b = o ; :: thesis: b _|_

[a,b] = [c,d] by A6;

hence b _|_ by A2, A3, A7; :: thesis: verum

proof

hence
( b _|_ iff b = o )
by A5; :: thesis: verum
assume
b _|_
; :: thesis: b = o

then ex c, d being Element of X st

( [a,b] = [c,d] & d = o ) by A3;

hence b = o by XTUPLE_0:1; :: thesis: verum

end;
then ex c, d being Element of X st

( [a,b] = [c,d] & d = o ) by A3;

hence b = o by XTUPLE_0:1; :: thesis: verum

for l being Element of F st b _|_ holds

b _|_ :: thesis: ( ( for a, b, c being Element of MPS st a _|_ & a _|_ holds

a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_ ) )

proof

thus
for a, b, c being Element of MPS st a _|_ & a _|_ holds
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;
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

a _|_ :: thesis: ( ( for a, b, x being Element of MPS st not a _|_ holds

ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_ ) )

proof

thus
for a, b, x being Element of MPS st not a _|_ holds
let a, b, c be Element of MPS; :: thesis: ( a _|_ & a _|_ implies a _|_ )

assume that

A8: a _|_ and

a _|_ ; :: thesis: a _|_

a = o by A4, A8;

hence a _|_ by A4; :: thesis: verum

end;
assume that

A8: a _|_ and

a _|_ ; :: thesis: a _|_

a = o by A4, A8;

hence a _|_ by A4; :: thesis: verum

ex k being Element of F st a _|_ :: thesis: for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds

a - b _|_

proof

thus
for a, b, c being Element of MPS st b - c _|_ & c - a _|_ holds
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;
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

a - b _|_ :: thesis: verum

proof

let a, b, c be Element of MPS; :: thesis: ( b - c _|_ & 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;
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

:: 2. ORTHOGONAL VECTOR SPACE

definition

let F be Field;

let IT be non empty right_complementable Abelian add-associative right_zeroed SymStr over F;

end;
let IT be non empty right_complementable Abelian add-associative right_zeroed SymStr over F;

attr IT 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 & b <> 0. IT & c <> 0. IT & d <> 0. IT implies ex p being Element of IT st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b - c _|_ & c - a _|_ implies a - b _|_ ) );

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 a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b - c _|_ & c - a _|_ implies a - b _|_ ) );

:: 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 & b <> 0. IT & c <> 0. IT & d <> 0. IT implies ex p being Element of IT st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b - c _|_ & c - a _|_ implies a - b _|_ ) ) );

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 & b <> 0. IT & c <> 0. IT & d <> 0. IT implies ex p being Element of IT st

( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b - c _|_ & c - a _|_ implies a - b _|_ ) ) );

registration

let F be Field;

ex b_{1} being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st

( b_{1} is OrtSp-like & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is strict )

end;
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 b

( b

proof 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;
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;

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 _|_ & b _|_ holds

not b _|_

for S being OrtSp of F

for a, b, c being Element of S st not b _|_ & b _|_ holds

not b _|_

proof end;

theorem Th4: :: ORTSP_1:4

for F being Field

for S being OrtSp of F

for a, b, c being Element of S st not a _|_ & a _|_ holds

not a _|_

for S being OrtSp of F

for a, b, c being Element of S st not a _|_ & a _|_ holds

not a _|_

proof end;

theorem Th5: :: ORTSP_1:5

for F being Field

for S being OrtSp of F

for a, b being Element of S

for l being Element of F st not a _|_ & not l = 0. F holds

( not a _|_ & not l * a _|_ )

for S being OrtSp of F

for a, b being Element of S

for l being Element of F st not a _|_ & not l = 0. F holds

( not a _|_ & not l * a _|_ )

proof end;

theorem Th7: :: ORTSP_1:7

for F being Field

for S being OrtSp of F

for a, b, c, d being Element of S st d _|_ & d _|_ holds

d _|_

for S being OrtSp of F

for a, b, c, d being Element of S st d _|_ & d _|_ holds

d _|_

proof end;

theorem Th8: :: ORTSP_1:8

for F being Field

for S being OrtSp of F

for a, b, x being Element of S

for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds

k = l

for S being OrtSp of F

for a, b, x being Element of S

for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds

k = l

proof end;

theorem Th9: :: ORTSP_1:9

for F being Field

for S being OrtSp of F

for a, b being Element of S st a _|_ & b _|_ holds

a - b _|_

for S being OrtSp of F

for a, b being Element of S st a _|_ & b _|_ holds

a - b _|_

proof end;

theorem :: ORTSP_1:10

for F being Field

for S being OrtSp of F st (1_ F) + (1_ F) <> 0. F & ex a being Element of S st a <> 0. S holds

ex b being Element of S st not b _|_

for S being OrtSp of F st (1_ F) + (1_ F) <> 0. F & ex a being Element of S st a <> 0. S holds

ex b being Element of S st not b _|_

proof end;

:: 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 _|_ ;

ex b_{1} being Element of F st

for l being Element of F st a _|_ holds

b_{1} = l

for b_{1}, b_{2} being Element of F st ( for l being Element of F st a _|_ holds

b_{1} = l ) & ( for l being Element of F st a _|_ holds

b_{2} = l ) holds

b_{1} = b_{2}

end;
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 for l being Element of F st a _|_ holds

it = l;

ex b

for l being Element of F st a _|_ holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{6} being Element of F holds

( b_{6} = ProJ (a,b,x) iff for l being Element of F st a _|_ holds

b_{6} = l );

for F being Field

for S being OrtSp of F

for a, b, x being Element of S st not a _|_ holds

for b

( b

b

theorem Th12: :: ORTSP_1:12

for F being Field

for S being OrtSp of F

for a, b, 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))

for S being OrtSp of F

for a, b, 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))

proof end;

theorem Th13: :: ORTSP_1:13

for F being Field

for S being OrtSp of F

for a, b, x, y being Element of S st not a _|_ holds

ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y))

for S being OrtSp of F

for a, b, x, y being Element of S st not a _|_ holds

ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y))

proof end;

theorem :: ORTSP_1:14

for F being Field

for S being OrtSp of F

for a, b, x being Element of S

for l being Element of F st not a _|_ & l <> 0. F holds

ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))

for S being OrtSp of F

for a, b, x being Element of S

for l being Element of F st not a _|_ & l <> 0. F holds

ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))

proof end;

theorem Th15: :: ORTSP_1:15

for F being Field

for S being OrtSp of F

for a, b, x being Element of S

for l being Element of F st not a _|_ & l <> 0. F holds

ProJ ((l * a),b,x) = ProJ (a,b,x)

for S being OrtSp of F

for a, b, x being Element of S

for l being Element of F st not a _|_ & l <> 0. F holds

ProJ ((l * a),b,x) = ProJ (a,b,x)

proof end;

theorem :: ORTSP_1:16

for F being Field

for S being OrtSp of F

for a, b, c, p being Element of S st not a _|_ & a _|_ holds

( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )

for S being OrtSp of F

for a, b, c, p being Element of S st not a _|_ & a _|_ holds

( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )

proof end;

theorem :: ORTSP_1:17

for F being Field

for S being OrtSp of F

for a, b, c, p being Element of S st not a _|_ & b _|_ & c _|_ holds

ProJ ((a + p),b,c) = ProJ (a,b,c)

for S being OrtSp of F

for a, b, c, p being Element of S st not a _|_ & b _|_ & c _|_ holds

ProJ ((a + p),b,c) = ProJ (a,b,c)

proof end;

theorem Th18: :: ORTSP_1:18

for F being Field

for S being OrtSp of F

for a, b, c being Element of S st not a _|_ & a _|_ holds

ProJ (a,b,c) = 1_ F

for S being OrtSp of F

for a, b, c being Element of S st not a _|_ & a _|_ holds

ProJ (a,b,c) = 1_ F

proof end;

theorem Th19: :: ORTSP_1:19

for F being Field

for S being OrtSp of F

for a, b being Element of S st not a _|_ holds

ProJ (a,b,b) = 1_ F

for S being OrtSp of F

for a, b being Element of S st not a _|_ holds

ProJ (a,b,b) = 1_ F

proof end;

theorem Th20: :: ORTSP_1:20

for F being Field

for S being OrtSp of F

for a, b, x being Element of S st not a _|_ holds

( a _|_ iff ProJ (a,b,x) = 0. F )

for S being OrtSp of F

for a, b, x being Element of S st not a _|_ holds

( a _|_ iff ProJ (a,b,x) = 0. F )

proof end;

theorem Th21: :: ORTSP_1:21

for F being Field

for S being OrtSp of F

for a, b, p, q being Element of S st not a _|_ & not a _|_ holds

(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)

for S being OrtSp of F

for a, b, p, q being Element of S st not a _|_ & not a _|_ holds

(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)

proof end;

theorem Th22: :: ORTSP_1:22

for F being Field

for S being OrtSp of F

for a, b, c being Element of S st not a _|_ & not a _|_ holds

ProJ (a,b,c) = (ProJ (a,c,b)) "

for S being OrtSp of F

for a, b, c being Element of S st not a _|_ & not a _|_ holds

ProJ (a,b,c) = (ProJ (a,c,b)) "

proof end;

theorem Th23: :: ORTSP_1:23

for F being Field

for S being OrtSp of F

for a, b, c being Element of S st not a _|_ & c + a _|_ holds

ProJ (a,b,c) = - (ProJ (c,b,a))

for S being OrtSp of F

for a, b, c being Element of S st not a _|_ & c + a _|_ holds

ProJ (a,b,c) = - (ProJ (c,b,a))

proof end;

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 _|_ & not b _|_ holds

ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c))

for S being OrtSp of F

for a, b, c being Element of S st not b _|_ & not b _|_ holds

ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c))

proof end;

theorem Th25: :: ORTSP_1:25

for F being Field

for S being OrtSp of F

for a, p, q, x being Element of S st not a _|_ & not x _|_ & not a _|_ & not x _|_ holds

(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (ProJ (x,q,p))

for S being OrtSp of F

for a, p, q, x being Element of S st not a _|_ & not x _|_ & not a _|_ & not x _|_ holds

(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (ProJ (x,q,p))

proof end;

theorem Th26: :: ORTSP_1:26

for F being Field

for S being OrtSp of F

for a, b, p, q, x, y being Element of S st not a _|_ & not x _|_ & not a _|_ & not x _|_ & 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))

for S being OrtSp of F

for a, b, p, q, x, y being Element of S st not a _|_ & not x _|_ & not a _|_ & not x _|_ & 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))

proof end;

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 _|_ & not p _|_ & not p _|_ holds

(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))

for S being OrtSp of F

for a, p, x, y being Element of S st not p _|_ & not p _|_ & not p _|_ holds

(ProJ (p,a,x)) * (ProJ (x,p,y)) = (ProJ (p,a,y)) * (ProJ (y,p,x))

proof end;

:: 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 _|_ ;

( ( ex p being Element of S st

( not a _|_ & not x _|_ ) implies ex b_{1} being Element of F st

for q being Element of S st not a _|_ & not x _|_ holds

b_{1} = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) & ( ( for p being Element of S holds

( a _|_ or x _|_ ) ) implies ex b_{1} being Element of F st b_{1} = 0. F ) )

for b_{1}, b_{2} being Element of F holds

( ( ex p being Element of S st

( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds

b_{1} = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) & ( for q being Element of S st not a _|_ & not x _|_ holds

b_{2} = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) implies b_{1} = b_{2} ) & ( ( for p being Element of S holds

( a _|_ or x _|_ ) ) & b_{1} = 0. F & b_{2} = 0. F implies b_{1} = b_{2} ) )

for b_{1} being Element of F holds verum
;

end;
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 _|_ & 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 _|_ & not x _|_ )

otherwise it = 0. F;

existence for q being Element of S st not a _|_ & 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 _|_ & not x _|_ )

otherwise it = 0. F;

( ( ex p being Element of S st

( not a _|_ & not x _|_ ) implies ex b

for q being Element of S st not a _|_ & not x _|_ holds

b

( a _|_ or x _|_ ) ) implies ex b

proof end;

uniqueness for b

( ( ex p being Element of S st

( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds

b

b

( a _|_ or x _|_ ) ) & b

proof end;

consistency for b

:: 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 b_{7} being Element of F holds

( ( ex p being Element of S st

( not a _|_ & not x _|_ ) implies ( b_{7} = PProJ (a,b,x,y) iff for q being Element of S st not a _|_ & not x _|_ holds

b_{7} = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) ) & ( ( for p being Element of S holds

( a _|_ or x _|_ ) ) implies ( b_{7} = PProJ (a,b,x,y) iff b_{7} = 0. F ) ) );

for F being Field

for S being OrtSp of F

for x, y, a, b being Element of S st not a _|_ holds

for b

( ( ex p being Element of S st

( not a _|_ & not x _|_ ) implies ( b

b

( a _|_ or x _|_ ) ) implies ( b

theorem Th28: :: ORTSP_1:28

for F being Field

for S being OrtSp of F

for a, b, x, y being Element of S st not a _|_ & x = 0. S holds

PProJ (a,b,x,y) = 0. F

for S being OrtSp of F

for a, b, x, y being Element of S st not a _|_ & x = 0. S holds

PProJ (a,b,x,y) = 0. F

proof end;

theorem Th29: :: ORTSP_1:29

for F being Field

for S being OrtSp of F

for a, b, x, y being Element of S st not a _|_ holds

( PProJ (a,b,x,y) = 0. F iff x _|_ )

for S being OrtSp of F

for a, b, x, y being Element of S st not a _|_ holds

( PProJ (a,b,x,y) = 0. F iff x _|_ )

proof end;

theorem :: ORTSP_1:30

for F being Field

for S being OrtSp of F

for a, b, x, y being Element of S st not a _|_ holds

PProJ (a,b,x,y) = PProJ (a,b,y,x)

for S being OrtSp of F

for a, b, x, y being Element of S st not a _|_ holds

PProJ (a,b,x,y) = PProJ (a,b,y,x)

proof end;

theorem :: ORTSP_1:31

for F being Field

for S being OrtSp of F

for a, b, 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))

for S being OrtSp of F

for a, b, 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))

proof end;

theorem :: ORTSP_1:32

for F being Field

for S being OrtSp of F

for a, b, 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))

for S being OrtSp of F

for a, b, 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))

proof end;