:: Construction of a bilinear antisymmetric form in symplectic vector space
:: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski
::
:: Received November 23, 1989
:: Copyright (c) 1990 Association of Mizar Users
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
let F be
Field;
:: thesis: ex mo being Relation of {0 } 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 ) ) )set CV =
[:{0 },{0 }:];
defpred S1[
set ]
means ex
a,
b being
Element of
{0 } st
( $1
= [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
{0 } by RELSET_1:def 1;
take mo =
mo;
:: thesis: 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;
:: thesis: 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
X;
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 {0 } 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;
:: thesis: for mF being Function of [:the carrier of F,{0 }:],{0 } st ( for a being Element of F
for x being Element of {0 } holds mF . a,x = o ) holds
for mo being Relation of {0 }
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-likelet mF be
Function of
[:the carrier of F,{0 }:],
{0 };
:: thesis: ( ( for a being Element of F
for x being Element of {0 } holds mF . a,x = o ) implies for mo being Relation of {0 }
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
F for
x being
Element of
{0 } holds
mF . a,
x = o
;
:: thesis: for mo being Relation of {0 }
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-likelet mo be
Relation of
{0 };
:: thesis: 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-likelet MPS be non
empty right_complementable Abelian add-associative right_zeroed SymStr of
F;
:: thesis: ( MPS = SymStr(# {0 },md,o,mF,mo #) implies MPS is VectSp-like )assume A2:
MPS = SymStr(#
{0 },
md,
o,
mF,
mo #)
;
:: thesis: MPS is VectSp-likethus
MPS is
VectSp-like
:: thesis: verum
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: 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 * (v + w) = (x * v) + (x * w)
proof
reconsider v =
v,
w =
w as
Element of
{0 } by A2;
A4:
md . v,
w = o
by Lm1;
reconsider v =
v,
w =
w as
Element of
MPS ;
x * (v + w) = mF . x,
o
by A2, A4, VECTSP_1:def 24;
then A5:
x * (v + w) = o
by A1;
mF . x,
v = o
by A1;
then A6:
x * v = o
by A2, VECTSP_1:def 24;
mF . x,
w = o
by A1;
then A7:
x * w = o
by A2, VECTSP_1:def 24;
o = 0. MPS
by A2;
hence
x * (v + w) = (x * v) + (x * w)
by A5, A6, A7, RLVECT_1:10;
:: thesis: verum
end;
A8:
(x + y) * v = (x * v) + (y * v)
proof
set z =
x + y;
A9:
(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 ;
A10:
(x + y) * v = o
by A1, A2, A9;
reconsider v =
v as
Element of
MPS ;
A11:
mF . x,
v = o
by A1, A2;
reconsider v =
v as
Element of
MPS ;
A12:
x * v = o
by A2, A11, VECTSP_1:def 24;
reconsider v =
v as
Element of
MPS ;
A13:
mF . y,
v = o
by A1, A2;
reconsider v =
v as
Element of
MPS ;
A14:
y * v = o
by A2, A13, VECTSP_1:def 24;
o = 0. MPS
by A2;
hence
(x + y) * v = (x * v) + (y * v)
by A10, A12, A14, RLVECT_1:10;
:: thesis: verum
end;
A15:
(x * y) * v = x * (y * v)
proof
set z =
x * y;
A16:
(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 ;
A17:
(x * y) * v = o
by A1, A2, A16;
reconsider v =
v as
Element of
MPS ;
A18:
mF . y,
v = o
by A1, A2;
reconsider v =
v as
Element of
MPS ;
y * v = o
by A2, A18, 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, A17;
:: thesis: 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 A3, A8, A15;
:: thesis: verum
end;
hence
MPS is
VectSp-like
by VECTSP_1:def 26;
:: thesis: verum
end;
end;
Lm5:
now
let F be
Field;
:: thesis: for mF being Function of [:the carrier of F,{0 }:],{0 } st ( for a being Element of F
for x being Element of {0 } holds mF . a,x = o ) holds
for mo being Relation of {0 } 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 MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( 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,{0 }:],
{0 };
:: thesis: ( ( for a being Element of F
for x being Element of {0 } holds mF . a,x = o ) implies for mo being Relation of {0 } 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 MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( 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
for
a being
Element of
F for
x being
Element of
{0 } holds
mF . a,
x = o
;
:: thesis: for mo being Relation of {0 } 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 MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( 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 =
[:{0 },{0 }:];
let mo be
Relation of
{0 };
:: thesis: ( ( 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 MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( 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 [:{0 },{0 }:] & ex
a,
b being
Element of
{0 } st
(
x = [a,b] &
b = o ) ) )
;
:: thesis: 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 MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( 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 of
F;
:: thesis: ( MPS = SymStr(# {0 },md,o,mF,mo #) implies ( ( for a being Element of MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( 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(#
{0 },
md,
o,
mF,
mo #)
;
:: thesis: ( ( for a being Element of MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( 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 [:{0 },{0 }:] & ex
c,
d being
Element of
{0 } st
(
[a,b] = [c,d] &
d = o ) ) )
proof
let a,
b be
Element of
MPS;
:: thesis: ( 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;
:: thesis: verum
end;
A4:
for
a,
b being
Element of
MPS holds
(
b _|_ iff
b = o )
thus
for
a being
Element of
MPS st
a <> 0. MPS holds
ex
p being
Element of
MPS st not
a _|_
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 _|_ ) )thus
for
a,
b being
Element of
MPS 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 _|_ ) )
thus
for
a,
b,
c being
Element of
MPS st
a _|_ &
a _|_ holds
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 _|_ ) )
thus
for
a,
b,
x being
Element of
MPS st not
a _|_ holds
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 _|_
let a,
b,
c be
Element of
MPS;
:: thesis: ( b + c _|_ & c + a _|_ implies a + b _|_ )assume
(
b + c _|_ &
c + a _|_ )
;
:: thesis: a + b _|_ assume
not
a + b _|_
;
:: thesis: contradictionthen
a + b <> o
by A4;
hence
contradiction
by A2, TARSKI:def 1;
:: thesis: verum
end;
:: deftheorem Def1 defines SymSp-like SYMSP_1:def 1 :
theorem :: SYMSP_1:1
canceled;
theorem :: SYMSP_1:2
canceled;
theorem :: SYMSP_1:3
canceled;
theorem :: SYMSP_1:4
canceled;
theorem :: SYMSP_1:5
canceled;
theorem :: SYMSP_1:6
canceled;
theorem :: SYMSP_1:7
canceled;
theorem :: SYMSP_1:8
canceled;
theorem :: SYMSP_1:9
canceled;
theorem :: SYMSP_1:10
canceled;
theorem Th11: :: SYMSP_1:11
theorem Th12: :: SYMSP_1:12
theorem Th13: :: SYMSP_1:13
theorem Th14: :: SYMSP_1:14
theorem Th15: :: SYMSP_1:15
theorem Th16: :: SYMSP_1:16
theorem :: SYMSP_1:17
canceled;
theorem :: SYMSP_1:18
canceled;
theorem Th19: :: SYMSP_1:19
theorem Th20: :: SYMSP_1:20
theorem Th21: :: SYMSP_1:21
theorem Th22: :: SYMSP_1:22
theorem Th23: :: SYMSP_1:23
theorem Th24: :: SYMSP_1:24
theorem Th25: :: SYMSP_1:25
:: 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 :: SYMSP_1:26
canceled;
theorem Th27: :: SYMSP_1:27
theorem Th28: :: SYMSP_1:28
theorem Th29: :: SYMSP_1:29
theorem :: SYMSP_1:30
theorem Th31: :: SYMSP_1:31
theorem Th32: :: SYMSP_1:32
for
F being
Field for
S being
SymSp of
F for
b,
a,
p,
c 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 )
theorem Th33: :: SYMSP_1:33
theorem Th34: :: SYMSP_1:34
theorem Th35: :: SYMSP_1:35
theorem Th36: :: SYMSP_1:36
theorem Th37: :: SYMSP_1:37
theorem Th38: :: SYMSP_1:38
theorem Th39: :: SYMSP_1:39
theorem Th40: :: SYMSP_1:40
theorem Th41: :: SYMSP_1:41
for
F being
Field for
S being
SymSp of
F for
a,
p,
q,
b being
Element of
S st
(1_ F) + (1_ F) <> 0. F & not
p _|_ & not
q _|_ & not
p _|_ & not
q _|_ holds
(ProJ a,p,q) * (ProJ b,q,p) = (ProJ p,a,b) * (ProJ q,b,a)
theorem Th42: :: SYMSP_1:42
for
F being
Field for
S being
SymSp of
F for
p,
a,
x,
q being
Element of
S 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: :: SYMSP_1:43
for
F being
Field for
S being
SymSp of
F for
p,
a,
x,
q,
b,
y being
Element of
S 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: :: SYMSP_1:44
for
F being
Field for
S being
SymSp 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)
definition
let F be
Field;
let S be
SymSp of
F;
let x,
y,
a,
b be
Element of
S;
assume that A1:
not
a _|_
and A2:
(1_ F) + (1_ F) <> 0. F
;
func PProJ a,
b,
x,
y -> Element of
F means :
Def6:
:: SYMSP_1:def 6
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 _|_ )
it = 0. F if for
p being
Element of
S holds
(
a _|_ or
x _|_ )
;
existence
( ( ex p being Element of S st
( not a _|_ & not x _|_ ) implies ex b1 being Element of F st
for q being Element of S st not a _|_ & not x _|_ holds
b1 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) & ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies ex b1 being Element of F st b1 = 0. F ) )
uniqueness
for b1, b2 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
b1 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) & ( for q being Element of S 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 S holds
( a _|_ or x _|_ ) ) & b1 = 0. F & b2 = 0. F implies b1 = b2 ) )
consistency
for b1 being Element of F st ex p being Element of S st
( not a _|_ & not x _|_ ) & ( for p being Element of S holds
( a _|_ or x _|_ ) ) holds
( ( for q being Element of S 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
S st not
a _|_ &
(1_ F) + (1_ F) <> 0. F holds
for
b7 being
Element of
F holds
( ( ex
p being
Element of
S st
( not
a _|_ & not
x _|_ ) implies (
b7 = PProJ a,
b,
x,
y iff for
q being
Element of
S st not
a _|_ & not
x _|_ holds
b7 = ((ProJ a,b,q) * (ProJ q,a,x)) * (ProJ x,q,y) ) ) & ( ( for
p being
Element of
S holds
(
a _|_ or
x _|_ ) ) implies (
b7 = PProJ a,
b,
x,
y iff
b7 = 0. F ) ) );
theorem :: SYMSP_1:45
canceled;
theorem :: SYMSP_1:46
canceled;
theorem Th47: :: SYMSP_1:47
theorem Th48: :: SYMSP_1:48
theorem :: SYMSP_1:49
theorem :: SYMSP_1:50
theorem :: SYMSP_1:51
for
F being
Field for
S being
SymSp of
F for
b,
a,
x,
y,
z being
Element of
S 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)