ORTSP_1: Construction of a bilinear symmetric form in orthogonal vector space

Lm2: now :: thesis:

defpred S₁[ object ] means ex a, b being Element of X st
( $1 = [a,b] & b = o );
set CV = [:X,X:];
let F be Field; :: thesis:
consider mo being set such that
A1: for x being object holds
( x in mo iff ( x in [:X,X:] & S₁[x] ) ) from XBOOLE_0:sch 1();
mo c= [:X,X:] by A1;
then reconsider mo = mo as Relation of X ;
take mo = mo; :: thesis:
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:

end;

Lm4: now :: thesis:

let F be Field; :: thesis:
let mF be Function of [: the carrier of F,X:],X; :: thesis:
assume A1: for a being Element of F
for x being Element of X holds mF . [a,x] = o ; :: thesis:
let mo be Relation of X; :: thesis:
let MPS be non empty right_complementable Abelian add-associative right_zeroed SymStr over F; :: thesis:
assume A2: MPS = SymStr(# X,md,o,mF,mo #) ; :: thesis:
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:
let v, w be Element of MPS; :: thesis:
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:

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:

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:

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:

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:

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:

end;

Lm5: now :: thesis:

set CV = [:X,X:];
let F be Field; :: thesis:
let mF be Function of [: the carrier of F,X:],X; :: thesis:
let mo be Relation of X; :: thesis:
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:
let MPS be non empty right_complementable Abelian add-associative right_zeroed SymStr over F; :: thesis:
assume A2: MPS = SymStr(# X,md,o,mF,mo #) ; :: thesis:
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:
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

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

end;

A4: for a, b being Element of MPS holds
( b _|_ iff b = o )

proof

let a, b be Element of MPS; :: thesis:
A5: ( b = o implies b _|_ )

proof

consider c, d being Element of MPS such that
A6: ( c = a & d = b ) ;
assume A7: b = o ; :: thesis:
[a,b] = [c,d] by A6;
hence b _|_ by A2, A3, A7; :: thesis:

end;

( b _|_ implies b = o )

proof

assume b _|_ ; :: thesis:
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:

end;

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

end;

thus for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ :: thesis:

proof

let a, b be Element of MPS; :: thesis:
let l be Element of F; :: thesis:
assume b _|_ ; :: thesis:
then b = o by A4;
hence b _|_ by A4; :: thesis:

end;

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

proof

let a, b, c be Element of MPS; :: thesis:
assume that
A8: a _|_ and
a _|_ ; :: thesis:
a = o by A4, A8;
hence a _|_ by A4; :: thesis:

end;

thus for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ :: thesis:

proof

let a, b, x be Element of MPS; :: thesis:
assume A9: not a _|_ ; :: thesis:
assume for k being Element of F holds not a _|_ ; :: thesis:
a <> o by A4, A9;
hence contradiction by A2, TARSKI:def 1; :: thesis:

end;

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

proof

let a, b, c be Element of MPS; :: thesis:
assume that
b - c _|_ and
c - a _|_ ; :: thesis:
assume not a - b _|_ ; :: thesis:
then a - b <> o by A4;
hence contradiction by A2, TARSKI:def 1; :: thesis:

end;

definition

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

end;

:: deftheorem Def1 defines OrtSp-like ORTSP_1:def 1 :

theorem Th1: :: ORTSP_1:1

for F being Field
for S being OrtSp of F
for a being Element of S holds a _|_