:: ORTSP_1 semantic presentation

Lm2: now

let F be Field; :: thesis:
set CV = [:X,X:];
defpred S₁[ set ] means ex a, b being Element of X st
( $1 = [a,b] & b = o );
consider mo being set such that
A1: for x being set holds
( x in mo iff ( x in [:X,X:] & S₁[x] ) ) from XBOOLE_0:sch 1( [:X,X:] );
mo c= [:X,X:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
thus ( not x in mo or x in [:X,X:] ) by A1; :: thesis:

end;

then reconsider mo = mo as Relation of X by RELSET_1:def 1;
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

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 Abelian add-associative right_zeroed right_complementable SymStr of F; :: thesis:
assume A2: MPS = SymStr(# X,md,o,mF,mo #) ; :: thesis:
thus MPS is VectSp-like :: thesis:

proof

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

proof

reconsider v = v, w = w as Element of MPS ;
A4: v + w = md . v,w by A2, RLVECT_1:5;
reconsider v = v, w = w as Element of X by A2;
A5: md . v,w = o by Lm1;
reconsider v = v, w = w as Element of MPS ;
A6: x * (v + w) = mF . x,o by A2, A4, A5, VECTSP_1:def 24;
A7: x * (v + w) = o by A1, A6;
reconsider v = v as Element of MPS ;
A8: mF . x,v = o by A1;
reconsider v = v as Element of MPS ;
A9: x * v = o by A2, A8, VECTSP_1:def 24;
reconsider w = w as Element of MPS ;
A10: mF . x,w = o by A1;
reconsider w = w as Element of MPS ;
A11: x * w = o by A2, A10, VECTSP_1:def 24;
o = 0. MPS by A2, RLVECT_1:def 2;
hence x * (v + w) = (x * v) + (x * w) by A7, A9, A11, RLVECT_1:10; :: thesis:

end;

A12: (x + y) * v = (x * v) + (y * v)

proof

set z = x + y;
A13: (x + y) * v = mF . (x + y),v by A2, VECTSP_1:def 24;
reconsider v = v as Element of MPS ;
reconsider v = v as Element of MPS ;
A14: (x + y) * v = o by A1, A2, A13;
reconsider v = v as Element of MPS ;
A15: mF . x,v = o by A1, A2;
reconsider v = v as Element of MPS ;
A16: x * v = o by A2, A15, VECTSP_1:def 24;
reconsider v = v as Element of MPS ;
A17: mF . y,v = o by A1, A2;
reconsider v = v as Element of MPS ;
A18: y * v = o by A2, A17, VECTSP_1:def 24;
o = 0. MPS by A2, RLVECT_1:def 2;
hence (x + y) * v = (x * v) + (y * v) by A14, A16, A18, RLVECT_1:10; :: thesis:

end;

A19: (x * y) * v = x * (y * v)

proof

set z = x * y;
A20: (x * y) * v = mF . (x * y),v by A2, VECTSP_1:def 24;
reconsider v = v as Element of MPS ;
reconsider v = v as Element of MPS ;
A21: (x * y) * v = o by A1, A2, A20;
reconsider v = v as Element of MPS ;
A22: mF . y,v = o by A1, A2;
reconsider v = v as Element of MPS ;
y * v = o by A2, A22, VECTSP_1:def 24;
then A23: x * (y * v) = mF . x,o by A2, VECTSP_1:def 24;
thus (x * y) * v = x * (y * v) by A1, A21, A23; :: thesis:

end;

(1. F) * v = v

proof

set one = 1. F;
A24: (1. F) * v = mF . (1. F),v by A2, VECTSP_1:def 24;
reconsider v = v as Element of MPS ;
mF . (1. F),v = o by A1, A2;
hence (1. F) * v = v by A2, A24, 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 A3, A12, A19; :: thesis:

end;

hence MPS is VectSp-like by VECTSP_1:def 26; :: thesis:

end;

Lm5: now

let F be Field; :: thesis:
let mF be Function of [:the carrier of F,X:],X; :: thesis:
assume for a being Element of F
for x being Element of X holds mF . [a,x] = o ; :: thesis:
set CV = [:X,X:];
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 Abelian add-associative right_zeroed right_complementable SymStr of F; :: thesis:
assume A2: MPS = SymStr(# X,md,o,mF,mo #) ; :: thesis:
A3: for a, b being Element of MPS holds
( a _|_ 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:
( a _|_ b iff [a,b] in mo ) by A2, SYMSP_1:def 1;
hence ( a _|_ 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
( a _|_ b iff b = o )

proof

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

proof

assume a _|_ b ; :: thesis:
then ex c, d being Element of X st
( [a,b] = [c,d] & d = o ) by A3;
hence b = o by ZFMISC_1:33; :: thesis:

end;

( b = o implies a _|_ b )

proof

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

end;

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

end;

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 p _|_ a & not p _|_ b & not p _|_ c & not p _|_ d ) by A2, TARSKI:def 1; :: thesis:
thus for a, b being Element of MPS
for l being Element of F st a _|_ b holds
l * a _|_ b :: thesis:

proof

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

end;

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

proof

let a, b, c be Element of MPS; :: thesis:
assume ( b _|_ a & c _|_ a ) ; :: thesis:
then a = o by A4;
hence b + c _|_ a by A4; :: thesis:

end;

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

proof

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

end;

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

proof

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

end;

definition

end;

definition

let F be Field;
let S be OrtSp of F;
let a, b, x be Element of S;
assume A1: not b _|_ a ;
canceled;
canceled;
canceled;
func ProJ a,b,x -> Element of F means :Def6: :: ORTSP_1:def 6
for l being Element of F st x - (l * b) _|_ a holds
it = l;
existence

proof end;

uniqueness

proof end;

end;

definition

let F be Field;
let S be OrtSp of F;
let x, y, a, b be Element of S;
assume A1: not b _|_ a ;
func PProJ a,b,x,y -> Element of F means :Def7: :: ORTSP_1:def 7
for q being Element of S st not q _|_ a & not q _|_ x holds
it = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) if ex p being Element of S st
( not p _|_ a & not p _|_ x )
it = 0. F if for p being Element of S holds
( p _|_ a or p _|_ x )
;
existence

proof end;

uniqueness

proof end;

consistency ;

end;