begin
set X = {0 };
reconsider o = 0 as Element of {0 } by TARSKI:def 1;
deffunc H1( Element of {0 }, Element of {0 }) -> Element of {0 } = o;
consider md being BinOp of {0 } such that
Lm1:
for x, y being Element of {0 } holds md . x,y = H1(x,y)
from BINOP_1:sch 4();
Lm2:
now
defpred S1[
set ]
means ex
a,
b being
Element of
{0 } st
( $1
= [a,b] &
b = o );
set CV =
[:{0 },{0 }:];
let F be
Field;
ex mo being Relation of st
for x being set holds
( x in mo iff ( x in [:{0 },{0 }:] & ex a, b being Element of {0 } st
( x = [a,b] & b = o ) ) )consider mo being
set such that A1:
for
x being
set holds
(
x in mo iff (
x in [:{0 },{0 }:] &
S1[
x] ) )
from XBOOLE_0:sch 1();
mo c= [:{0 },{0 }:]
then reconsider mo =
mo as
Relation of ;
take mo =
mo;
for x being set holds
( x in mo iff ( x in [:{0 },{0 }:] & ex a, b being Element of {0 } st
( x = [a,b] & b = o ) ) )thus
for
x being
set holds
(
x in mo iff (
x in [:{0 },{0 }:] & ex
a,
b being
Element of
{0 } st
(
x = [a,b] &
b = o ) ) )
by A1;
verum
end;
registration
let F be
Field;
let X be non
empty set ;
let md be
BinOp of
X;
let o be
Element of
X;
let mF be
Function of
[:the carrier of F,X:],
X;
let mo be
Relation of ;
cluster SymStr(#
X,
md,
o,
mF,
mo #)
-> non
empty ;
coherence
not SymStr(# X,md,o,mF,mo #) is empty
;
end;
Lm3:
for F being Field
for mF being Function of [:the carrier of F,{0 }:],{0 }
for mo being Relation of holds
( SymStr(# {0 },md,o,mF,mo #) is Abelian & SymStr(# {0 },md,o,mF,mo #) is add-associative & SymStr(# {0 },md,o,mF,mo #) is right_zeroed & SymStr(# {0 },md,o,mF,mo #) is right_complementable )
Lm4:
now
let F be
Field;
for mF being Function of [:the carrier of F,{0 }:],{0 } st ( for a being Element of
for x being Element of {0 } 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(# {0 },md,o,mF,mo #) holds
MPS is VectSp-like let mF be
Function of
[:the carrier of F,{0 }:],
{0 };
( ( for a being Element of
for x being Element of {0 } 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(# {0 },md,o,mF,mo #) holds
MPS is VectSp-like )assume A1:
for
a being
Element of
for
x being
Element of
{0 } 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(# {0 },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(# {0 },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(# {0 },md,o,mF,mo #) implies MPS is VectSp-like )assume A2:
MPS = SymStr(#
{0 },
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
{0 } by A2;
A8:
md . v,
w = o
by Lm1;
reconsider v =
v,
w =
w as
Element of ;
x * (v + w) = mF . x,
o
by A2, A8, VECTSP_1:def 24;
then A9:
x * (v + w) = o
by A1;
mF . x,
v = o
by A1;
then A10:
x * v = o
by A2, VECTSP_1:def 24;
mF . x,
w = o
by A1;
then A11:
x * w = o
by A2, VECTSP_1:def 24;
o = 0. MPS
by A2;
hence
x * (v + w) = (x * v) + (x * w)
by A9, A10, A11, RLVECT_1:10;
verum
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 ;
reconsider v =
v as
Element of ;
A14:
(x + y) * v = o
by A1, A2, A13;
reconsider v =
v as
Element of ;
A15:
mF . x,
v = o
by A1, A2;
reconsider v =
v as
Element of ;
A16:
x * v = o
by A2, A15, VECTSP_1:def 24;
reconsider v =
v as
Element of ;
A17:
mF . y,
v = o
by A1, A2;
A18:
o = 0. MPS
by A2;
reconsider v =
v as
Element of ;
y * v = o
by A2, A17, VECTSP_1:def 24;
hence
(x + y) * v = (x * v) + (y * v)
by A14, A16, A18, 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, A12, A3;
verum
end;
hence
MPS is
VectSp-like
by VECTSP_1:def 26;
verum
end;
Lm5:
now
set CV =
[:{0 },{0 }:];
let F be
Field;
for mF being Function of [:the carrier of F,{0 }:],{0 }
for mo being Relation of st ( for x being set holds
( x in mo iff ( x in [:{0 },{0 }:] & ex a, b being Element of {0 } 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(# {0 },md,o,mF,mo #) holds
( ( for a being Element of st a <> 0. MPS holds
ex p being Element of st not a _|_ ) & ( 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,{0 }:],
{0 };
for mo being Relation of st ( for x being set holds
( x in mo iff ( x in [:{0 },{0 }:] & ex a, b being Element of {0 } 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(# {0 },md,o,mF,mo #) holds
( ( for a being Element of st a <> 0. MPS holds
ex p being Element of st not a _|_ ) & ( 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 [:{0 },{0 }:] & ex a, b being Element of {0 } 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(# {0 },md,o,mF,mo #) holds
( ( for a being Element of st a <> 0. MPS holds
ex p being Element of st not a _|_ ) & ( 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 [:{0 },{0 }:] & ex
a,
b being
Element of
{0 } st
(
x = [a,b] &
b = o ) ) )
;
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr of F st MPS = SymStr(# {0 },md,o,mF,mo #) holds
( ( for a being Element of st a <> 0. MPS holds
ex p being Element of st not a _|_ ) & ( 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(# {0 },md,o,mF,mo #) implies ( ( for a being Element of st a <> 0. MPS holds
ex p being Element of st not a _|_ ) & ( 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(#
{0 },
md,
o,
mF,
mo #)
;
( ( for a being Element of st a <> 0. MPS holds
ex p being Element of st not a _|_ ) & ( 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 being
Element of st
a <> 0. MPS holds
ex
p being
Element of st not
a _|_
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 [:{0 },{0 }:] & ex
c,
d being
Element of
{0 } st
(
[a,b] = [c,d] &
d = o ) ) )
proof
let a,
b be
Element of ;
( b _|_ iff ( [a,b] in [:{0 },{0 }:] & ex c, d being Element of {0 } 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 [:{0 },{0 }:] & ex
c,
d being
Element of
{0 } 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 _|_
let a,
b,
c be
Element of ;
( b + c _|_ & c + a _|_ implies a + b _|_ )assume that
b + c _|_
and
c + a _|_
;
a + b _|_ assume
not
a + b _|_
;
contradictionthen
a + b <> o
by A4;
hence
contradiction
by A2, TARSKI:def 1;
verum
end;
:: deftheorem Def1 defines SymSp-like SYMSP_1:def 1 :
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 Th22:
theorem Th23:
theorem Th24:
theorem Th25:
:: deftheorem SYMSP_1:def 2 :
canceled;
:: deftheorem SYMSP_1:def 3 :
canceled;
:: deftheorem SYMSP_1:def 4 :
canceled;
:: deftheorem Def5 defines ProJ SYMSP_1:def 5 :
theorem
canceled;
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
for
F being
Field for
S being
SymSp 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 Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
for
F being
Field for
S being
SymSp of
F for
a,
p,
q,
b being
Element of st
(1_ F) + (1_ F) <> 0. F & not
p _|_ & not
q _|_ & not
q _|_ holds
(ProJ a,p,q) * (ProJ b,q,p) = (ProJ p,a,b) * (ProJ q,b,a)
theorem Th42:
for
F being
Field for
S being
SymSp of
F for
p,
a,
x,
q being
Element of st
(1_ F) + (1_ F) <> 0. F & not
a _|_ & not
x _|_ & not
a _|_ & not
x _|_ holds
(ProJ a,q,p) * (ProJ p,a,x) = (ProJ x,q,p) * (ProJ q,a,x)
theorem Th43:
for
F being
Field for
S being
SymSp of
F for
p,
a,
x,
q,
b,
y being
Element of st
(1_ F) + (1_ F) <> 0. F & 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 Th44:
for
F being
Field for
S being
SymSp 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
SymSp of
F;
let x,
y,
a,
b be
Element of ;
assume A1:
( not
a _|_ &
(1_ F) + (1_ F) <> 0. F )
;
func PProJ a,
b,
x,
y -> Element of
means :
Def6:
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 Def6 defines PProJ SYMSP_1:def 6 :
for
F being
Field for
S being
SymSp of
F for
x,
y,
a,
b being
Element of st not
a _|_ &
(1_ F) + (1_ F) <> 0. F 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 Th47:
theorem Th48:
theorem
theorem
theorem
for
F being
Field for
S being
SymSp of
F for
b,
a,
x,
y,
z being
Element of st
(1_ F) + (1_ F) <> 0. F & not
a _|_ holds
PProJ a,
b,
x,
(y + z) = (PProJ a,b,x,y) + (PProJ a,b,x,z)