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
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;
ex mo being Relation of 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:]
then reconsider mo =
mo as
Relation of ;
take mo =
mo;
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;
verum
end;
Lm3:
for F being Field
for mF being Function of [:the carrier of F,X:],X
for mo being Relation of 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 )
Lm4:
now
let F be
Field;
for mF being Function of [:the carrier of F,X:],X st ( for a being Element of
for x being Element of X holds mF . [a,x] = o ) holds
for mo being Relation of
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr of F st MPS = SymStr(# X,md,o,mF,mo #) holds
MPS is VectSp-like let mF be
Function of
[:the carrier of F,X:],
X;
( ( for a being Element of
for x being Element of X holds mF . [a,x] = o ) implies for mo being Relation of
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr of F st MPS = SymStr(# X,md,o,mF,mo #) holds
MPS is VectSp-like )assume A1:
for
a being
Element of
for
x being
Element of
X holds
mF . [a,x] = o
;
for mo being Relation of
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr of F st MPS = SymStr(# X,md,o,mF,mo #) holds
MPS is VectSp-like let mo be
Relation of ;
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr of F st MPS = SymStr(# X,md,o,mF,mo #) holds
MPS is VectSp-like let MPS be non
empty right_complementable Abelian add-associative right_zeroed SymStr of
F;
( MPS = SymStr(# X,md,o,mF,mo #) implies MPS is VectSp-like )assume A2:
MPS = SymStr(#
X,
md,
o,
mF,
mo #)
;
MPS is VectSp-like
for
x,
y being
Element of
for
v,
w being
Element of 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 ;
for v, w being Element of 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 ;
( 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 24;
reconsider v =
v as
Element of ;
reconsider v =
v as
Element of ;
A5:
(x * y) * v = o
by A1, A2, A4;
reconsider v =
v as
Element of ;
A6:
mF . y,
v = o
by A1, A2;
reconsider v =
v as
Element of ;
y * v = o
by A2, A6, VECTSP_1:def 24;
then
x * (y * v) = mF . x,
o
by A2, VECTSP_1:def 24;
hence
(x * y) * v = x * (y * v)
by A1, A5;
verum
end;
A7:
x * (v + w) = (x * v) + (x * w)
proof
reconsider v =
v,
w =
w as
Element of ;
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 ;
x * (v + w) = mF . x,
o
by A2, A9, VECTSP_1:def 24;
then A10:
x * (v + w) = o
by A1;
reconsider w =
w as
Element of ;
reconsider v =
v as
Element of ;
A11:
mF . x,
v = o
by A1;
reconsider v =
v as
Element of ;
A12:
mF . x,
w = o
by A1;
reconsider w =
w as
Element of ;
A13:
x * w = o
by A2, A12, VECTSP_1:def 24;
x * v = o
by A2, A11, VECTSP_1:def 24;
hence
x * (v + w) = (x * v) + (x * w)
by A10, A13, A8, RLVECT_1:10;
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 24;
reconsider v =
v as
Element of ;
reconsider v =
v as
Element of ;
A16:
(x + y) * v = o
by A1, A2, A15;
reconsider v =
v as
Element of ;
A17:
mF . x,
v = o
by A1, A2;
reconsider v =
v as
Element of ;
A18:
x * v = o
by A2, A17, VECTSP_1:def 24;
reconsider v =
v as
Element of ;
A19:
mF . y,
v = o
by A1, A2;
A20:
o = 0. MPS
by A2, STRUCT_0:def 6;
reconsider v =
v as
Element of ;
y * v = o
by A2, A19, VECTSP_1:def 24;
hence
(x + y) * v = (x * v) + (y * v)
by A16, A18, A20, RLVECT_1:10;
verum
end;
(1_ F) * v = v
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;
verum
end;
hence
MPS is
VectSp-like
by VECTSP_1:def 26;
verum
end;
Lm5:
now
set CV =
[:X,X:];
let F be
Field;
for mF being Function of [:the carrier of F,X:],X
for mo being Relation of 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 of F st MPS = SymStr(# X,md,o,mF,mo #) holds
( ( for a, b, c, d being Element of st a <> 0. MPS & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds
ex p being Element of st
( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of
for l being Element of st b _|_ holds
b _|_ ) & ( for a, b, c being Element of st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of st not a _|_ holds
ex k being Element of st a _|_ ) & ( for a, b, c being Element of st b - c _|_ & c - a _|_ holds
a - b _|_ ) )let mF be
Function of
[:the carrier of F,X:],
X;
for mo being Relation of 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 of F st MPS = SymStr(# X,md,o,mF,mo #) holds
( ( for a, b, c, d being Element of st a <> 0. MPS & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds
ex p being Element of st
( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of
for l being Element of st b _|_ holds
b _|_ ) & ( for a, b, c being Element of st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of st not a _|_ holds
ex k being Element of st a _|_ ) & ( for a, b, c being Element of st b - c _|_ & c - a _|_ holds
a - b _|_ ) )let mo be
Relation of ;
( ( 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 of F st MPS = SymStr(# X,md,o,mF,mo #) holds
( ( for a, b, c, d being Element of st a <> 0. MPS & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds
ex p being Element of st
( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of
for l being Element of st b _|_ holds
b _|_ ) & ( for a, b, c being Element of st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of st not a _|_ holds
ex k being Element of st a _|_ ) & ( for a, b, c being Element of 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 ) ) )
;
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr of F st MPS = SymStr(# X,md,o,mF,mo #) holds
( ( for a, b, c, d being Element of st a <> 0. MPS & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds
ex p being Element of st
( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of
for l being Element of st b _|_ holds
b _|_ ) & ( for a, b, c being Element of st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of st not a _|_ holds
ex k being Element of st a _|_ ) & ( for a, b, c being Element of st b - c _|_ & c - a _|_ holds
a - b _|_ ) )let MPS be non
empty right_complementable Abelian add-associative right_zeroed SymStr of
F;
( MPS = SymStr(# X,md,o,mF,mo #) implies ( ( for a, b, c, d being Element of st a <> 0. MPS & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds
ex p being Element of st
( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of
for l being Element of st b _|_ holds
b _|_ ) & ( for a, b, c being Element of st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of st not a _|_ holds
ex k being Element of st a _|_ ) & ( for a, b, c being Element of st b - c _|_ & c - a _|_ holds
a - b _|_ ) ) )assume A2:
MPS = SymStr(#
X,
md,
o,
mF,
mo #)
;
( ( for a, b, c, d being Element of st a <> 0. MPS & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS holds
ex p being Element of st
( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( for a, b being Element of
for l being Element of st b _|_ holds
b _|_ ) & ( for a, b, c being Element of st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of st not a _|_ holds
ex k being Element of st a _|_ ) & ( for a, b, c being Element of 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 st
a <> 0. MPS &
b <> 0. MPS &
c <> 0. MPS &
d <> 0. MPS holds
ex
p being
Element of st
( not
a _|_ & not
b _|_ & not
c _|_ & not
d _|_ )
by A2, TARSKI:def 1;
( ( for a, b being Element of
for l being Element of st b _|_ holds
b _|_ ) & ( for a, b, c being Element of st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of st not a _|_ holds
ex k being Element of st a _|_ ) & ( for a, b, c being Element of st b - c _|_ & c - a _|_ holds
a - b _|_ ) )A3:
for
a,
b being
Element of 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 ;
( 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 9;
hence
(
b _|_ iff (
[a,b] in [:X,X:] & ex
c,
d being
Element of
X st
(
[a,b] = [c,d] &
d = o ) ) )
by A1;
verum
end;
A4:
for
a,
b being
Element of holds
(
b _|_ iff
b = o )
thus
for
a,
b being
Element of
for
l being
Element of st
b _|_ holds
b _|_
( ( for a, b, c being Element of st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of st not a _|_ holds
ex k being Element of st a _|_ ) & ( for a, b, c being Element of st b - c _|_ & c - a _|_ holds
a - b _|_ ) )
thus
for
a,
b,
c being
Element of st
a _|_ &
a _|_ holds
a _|_
( ( for a, b, x being Element of st not a _|_ holds
ex k being Element of st a _|_ ) & ( for a, b, c being Element of st b - c _|_ & c - a _|_ holds
a - b _|_ ) )
thus
for
a,
b,
x being
Element of st not
a _|_ holds
ex
k being
Element of st
a _|_
for a, b, c being Element of st b - c _|_ & c - a _|_ holds
a - b _|_
thus
for
a,
b,
c being
Element of st
b - c _|_ &
c - a _|_ holds
a - b _|_
verum
end;
:: deftheorem ORTSP_1:def 1 :
canceled;
:: deftheorem Def2 defines OrtSp-like ORTSP_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
canceled;
theorem
canceled;
theorem Th19:
theorem Th20:
theorem Th21:
theorem
:: deftheorem ORTSP_1:def 3 :
canceled;
:: deftheorem ORTSP_1:def 4 :
canceled;
:: deftheorem ORTSP_1:def 5 :
canceled;
:: deftheorem Def6 defines ProJ ORTSP_1:def 6 :
theorem
canceled;
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem
for
F being
Field for
S being
OrtSp of
F for
b,
a,
p,
c being
Element of st not
a _|_ &
a _|_ holds
(
ProJ a,
(b + p),
c = ProJ a,
b,
c &
ProJ a,
b,
(c + p) = ProJ a,
b,
c )
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
for
F being
Field for
S being
OrtSp of
F for
p,
a,
x,
q being
Element of 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)
theorem Th39:
for
F being
Field for
S being
OrtSp of
F for
p,
a,
x,
q,
b,
y being
Element of 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)
theorem Th40:
for
F being
Field for
S being
OrtSp of
F for
a,
p,
x,
y being
Element of st not
p _|_ & not
p _|_ & not
p _|_ holds
(ProJ p,a,x) * (ProJ x,p,y) = (ProJ p,a,y) * (ProJ y,p,x)
definition
let F be
Field;
let S be
OrtSp of
F;
let x,
y,
a,
b be
Element of ;
assume A1:
not
a _|_
;
func PProJ a,
b,
x,
y -> Element of
means :
Def7:
for
q being
Element of 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 st
( not
a _|_ & not
x _|_ )
it = 0. F if for
p being
Element of holds
(
a _|_ or
x _|_ )
;
existence
( ( ex p being Element of st
( not a _|_ & not x _|_ ) implies ex b1 being Element of st
for q being Element of st not a _|_ & not x _|_ holds
b1 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) & ( ( for p being Element of holds
( a _|_ or x _|_ ) ) implies ex b1 being Element of st b1 = 0. F ) )
uniqueness
for b1, b2 being Element of holds
( ( ex p being Element of st
( not a _|_ & not x _|_ ) & ( for q being Element of st not a _|_ & not x _|_ holds
b1 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) & ( for q being Element of st not a _|_ & not x _|_ holds
b2 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) implies b1 = b2 ) & ( ( for p being Element of holds
( a _|_ or x _|_ ) ) & b1 = 0. F & b2 = 0. F implies b1 = b2 ) )
consistency
for b1 being Element of st ex p being Element of st
( not a _|_ & not x _|_ ) & ( for p being Element of holds
( a _|_ or x _|_ ) ) holds
( ( for q being Element of st not a _|_ & not x _|_ holds
b1 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) iff b1 = 0. F )
;
end;
:: deftheorem Def7 defines PProJ ORTSP_1:def 7 :
for
F being
Field for
S being
OrtSp of
F for
x,
y,
a,
b being
Element of st not
a _|_ holds
for
b7 being
Element of holds
( ( ex
p being
Element of st
( not
a _|_ & not
x _|_ ) implies (
b7 = PProJ a,
b,
x,
y iff for
q being
Element of st not
a _|_ & not
x _|_ holds
b7 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) ) & ( ( for
p being
Element of holds
(
a _|_ or
x _|_ ) ) implies (
b7 = PProJ a,
b,
x,
y iff
b7 = 0. F ) ) );
theorem
canceled;
theorem
canceled;
theorem Th43:
theorem Th44:
theorem
theorem
theorem
for
F being
Field for
S being
OrtSp of
F for
b,
a,
x,
y,
z being
Element of st not
a _|_ holds
PProJ a,
b,
x,
(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z)