:: 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-2011 Association of Mizar Users


begin

definition
let F be Field;
attr c2 is strict ;
struct SymStr of F -> RelStr , VectSpStr of F;
aggr SymStr(# carrier, addF, ZeroF, lmult, InternalRel #) -> SymStr of F;
end;

registration
let F be Field;
cluster non empty SymStr of F;
existence
not for b1 being SymStr of F holds b1 is empty
proof end;
end;

notation
let F be Field;
let S be SymStr of F;
let a, b be Element of S;
synonym a _|_ b for S <= a;
end;

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; :: 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 ) ) )

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}:]
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in mo or x in [:{0},{0}:] )
thus ( not x in mo or x in [:{0},{0}:] ) by A1; :: thesis: verum
end;
then reconsider mo = mo as Relation of {0} ;
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 )
proof end;

registration
let F be Field;
cluster non empty right_complementable Abelian add-associative right_zeroed SymStr of F;
existence
ex b1 being non empty SymStr of F st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable )
proof end;
end;

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 vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )

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}
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 vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) )

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 vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )

let 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 vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )

let 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 vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) )
assume A2: MPS = SymStr(# {0},md,o,mF,mo #) ; :: thesis: ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )
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 * 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 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 24;
then x * (y * v) = mF . (x,o) by A2, VECTSP_1:def 24;
hence (x * y) * v = x * (y * v) by A1, A5; :: thesis: 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 MPS ;
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; :: thesis: 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 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;
A18: o = 0. MPS by A2;
reconsider v = v as Element of MPS ;
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; :: thesis: verum
end;
(1_ F) * v = v
proof
set one1 = 1_ F;
A19: (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, A19, TARSKI:def 1; :: thesis: verum
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, A12, A3; :: thesis: verum
end;
hence ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) by VECTSP_1:def 26, VECTSP_1:def 27, VECTSP_1:def 28, VECTSP_1:def 29; :: thesis: verum
end;

Lm5: now
set CV = [:{0},{0}:];
let F be Field; :: thesis: for mF being Function of [: the carrier of F,{0}:],{0}
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 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 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 _|_ ) )

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 _|_ ) )

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 )
proof
let a, b be Element of MPS; :: thesis: ( b _|_ iff b = o )
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: b _|_
[a,b] = [c,d] by A6;
hence b _|_ by A2, A3, A7; :: thesis: verum
end;
( b _|_ implies b = o )
proof
assume b _|_ ; :: thesis: b = o
then ex c, d being Element of {0} st
( [a,b] = [c,d] & d = o ) by A3;
hence b = o by ZFMISC_1:33; :: thesis: verum
end;
hence ( b _|_ iff b = o ) by A5; :: thesis: verum
end;
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 _|_ ) )
proof
let a, b be Element of MPS; :: thesis: for l being Element of F st b _|_ holds
b _|_

let l be Element of F; :: thesis: ( b _|_ implies b _|_ )
assume b _|_ ; :: thesis: b _|_
then b = o by A4;
hence b _|_ by A4; :: thesis: verum
end;
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 _|_ ) )
proof
let a, b, c be Element of MPS; :: thesis: ( a _|_ & a _|_ implies a _|_ )
assume that
A8: a _|_ and
a _|_ ; :: thesis: a _|_
a = o by A4, A8;
hence a _|_ by A4; :: thesis: verum
end;
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 _|_
proof
let a, b, x be Element of MPS; :: thesis: ( not a _|_ implies ex k being Element of F st a _|_ )
assume A9: not a _|_ ; :: thesis: ex k being Element of F st a _|_
assume for k being Element of F holds not a _|_ ; :: thesis: contradiction
a <> o by A4, A9;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum
end;
let a, b, c be Element of MPS; :: thesis: ( b + c _|_ & c + a _|_ implies a + b _|_ )
assume that
b + c _|_ and
c + a _|_ ; :: thesis: a + b _|_
assume not a + b _|_ ; :: thesis: contradiction
then a + b <> o by A4;
hence contradiction by A2, TARSKI:def 1; :: thesis: verum
end;

definition
let F be Field;
let IT be non empty right_complementable Abelian add-associative right_zeroed SymStr of F;
attr IT is SymSp-like means :Def1: :: SYMSP_1:def 1
for a, b, c, x being Element of IT
for l being Element of F holds
( ( a <> 0. IT implies ex y being Element of IT st not a _|_ ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b + c _|_ & c + a _|_ implies a + b _|_ ) );
end;

:: deftheorem Def1 defines SymSp-like SYMSP_1:def 1 :
for F being Field
for IT being non empty right_complementable Abelian add-associative right_zeroed SymStr of F holds
( IT is SymSp-like iff for a, b, c, x being Element of IT
for l being Element of F holds
( ( a <> 0. IT implies ex y being Element of IT st not a _|_ ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b + c _|_ & c + a _|_ implies a + b _|_ ) ) );

registration
let F be Field;
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict SymSp-like SymStr of F;
existence
ex b1 being non empty right_complementable Abelian add-associative right_zeroed SymStr of F st
( b1 is SymSp-like & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is strict )
proof end;
end;

definition
let F be Field;
mode SymSp of F is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like SymStr of F;
end;

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
for F being Field
for S being SymSp of F
for a being Element of S holds a _|_
proof end;

theorem Th12: :: SYMSP_1:12
for F being Field
for S being SymSp of F
for a, b being Element of S st b _|_ holds
a _|_
proof end;

theorem Th13: :: SYMSP_1:13
for F being Field
for S being SymSp of F
for a, b, c being Element of S st not b _|_ & b _|_ holds
not b _|_
proof end;

theorem Th14: :: SYMSP_1:14
for F being Field
for S being SymSp of F
for b, a, c being Element of S st not a _|_ & a _|_ holds
not a _|_
proof end;

theorem Th15: :: SYMSP_1:15
for F being Field
for S being SymSp of F
for b, a being Element of S
for l being Element of F st not a _|_ & not l = 0. F holds
( not a _|_ & not l * a _|_ )
proof end;

theorem Th16: :: SYMSP_1:16
for F being Field
for S being SymSp of F
for a, b being Element of S st b _|_ holds
b _|_
proof end;

theorem :: SYMSP_1:17
canceled;

theorem :: SYMSP_1:18
canceled;

theorem Th19: :: SYMSP_1:19
for F being Field
for S being SymSp of F
for a, c, b being Element of S holds
( c _|_ or not c _|_ or not c _|_ )
proof end;

theorem Th20: :: SYMSP_1:20
for F being Field
for S being SymSp of F
for a9, a, b, b9 being Element of S st not a _|_ & b _|_ & not b _|_ & a _|_ holds
( not a _|_ & not b _|_ )
proof end;

theorem Th21: :: SYMSP_1:21
for F being Field
for S being SymSp of F
for a, b being Element of S st a <> 0. S & b <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ )
proof end;

theorem Th22: :: SYMSP_1:22
for F being Field
for S being SymSp of F
for a, b, c being Element of S st (1_ F) + (1_ F) <> 0. F & a <> 0. S & b <> 0. S & c <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
proof end;

theorem Th23: :: SYMSP_1:23
for F being Field
for S being SymSp of F
for a, b, d, c being Element of S st d _|_ & d _|_ holds
d _|_
proof end;

theorem Th24: :: SYMSP_1:24
for F being Field
for S being SymSp of F
for b, a, x being Element of S
for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds
k = l
proof end;

theorem Th25: :: SYMSP_1:25
for F being Field
for S being SymSp of F
for a being Element of S st (1_ F) + (1_ F) <> 0. F holds
a _|_
proof end;

definition
let F be Field;
let S be SymSp of F;
let a, b, x be Element of S;
assume A1: not a _|_ ;
canceled;
canceled;
canceled;
func ProJ (a,b,x) -> Element of F means :Def5: :: SYMSP_1:def 5
for l being Element of F st a _|_ holds
it = l;
existence
ex b1 being Element of F st
for l being Element of F st a _|_ holds
b1 = l
proof end;
uniqueness
for b1, b2 being Element of F st ( for l being Element of F st a _|_ holds
b1 = l ) & ( for l being Element of F st a _|_ holds
b2 = l ) holds
b1 = b2
proof end;
end;

:: 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 :
for F being Field
for S being SymSp of F
for a, b, x being Element of S st not a _|_ holds
for b6 being Element of F holds
( b6 = ProJ (a,b,x) iff for l being Element of F st a _|_ holds
b6 = l );

theorem :: SYMSP_1:26
canceled;

theorem Th27: :: SYMSP_1:27
for F being Field
for S being SymSp of F
for b, a, x being Element of S st not a _|_ holds
a _|_
proof end;

theorem Th28: :: SYMSP_1:28
for F being Field
for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ holds
ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
proof end;

theorem Th29: :: SYMSP_1:29
for F being Field
for S being SymSp of F
for b, a, x, y being Element of S st not a _|_ holds
ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y))
proof end;

theorem :: SYMSP_1:30
for F being Field
for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
proof end;

theorem Th31: :: SYMSP_1:31
for F being Field
for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ ((l * a),b,x) = ProJ (a,b,x)
proof end;

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) )
proof end;

theorem Th33: :: SYMSP_1:33
for F being Field
for S being SymSp of F
for b, a, p, c being Element of S st not a _|_ & b _|_ & c _|_ holds
ProJ ((a + p),b,c) = ProJ (a,b,c)
proof end;

theorem Th34: :: SYMSP_1:34
for F being Field
for S being SymSp of F
for b, a, c being Element of S st not a _|_ & a _|_ holds
ProJ (a,b,c) = 1_ F
proof end;

theorem Th35: :: SYMSP_1:35
for F being Field
for S being SymSp of F
for b, a being Element of S st not a _|_ holds
ProJ (a,b,b) = 1_ F
proof end;

theorem Th36: :: SYMSP_1:36
for F being Field
for S being SymSp of F
for b, a, x being Element of S st not a _|_ holds
( a _|_ iff ProJ (a,b,x) = 0. F )
proof end;

theorem Th37: :: SYMSP_1:37
for F being Field
for S being SymSp of F
for b, a, q, p being Element of S st not a _|_ & not a _|_ holds
(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)
proof end;

theorem Th38: :: SYMSP_1:38
for F being Field
for S being SymSp of F
for b, a, c being Element of S st not a _|_ & not a _|_ holds
ProJ (a,b,c) = (ProJ (a,c,b)) "
proof end;

theorem Th39: :: SYMSP_1:39
for F being Field
for S being SymSp of F
for b, a, c being Element of S st not a _|_ & c + a _|_ holds
ProJ (a,b,c) = ProJ (c,b,a)
proof end;

theorem Th40: :: SYMSP_1:40
for F being Field
for S being SymSp of F
for a, b, c being Element of S st not b _|_ & not b _|_ holds
ProJ (c,b,a) = (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c))
proof end;

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 q _|_ holds
(ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
proof end;

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))
proof end;

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))
proof end;

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))
proof end;

definition
let F be Field;
let S be SymSp of F;
let x, y, a, b be Element of S;
assume A1: ( not a _|_ & (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 _|_ )
otherwise it = 0. F;
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 ) )
proof end;
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 ) )
proof end;
consistency
for b1 being Element of F holds verum
;
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
for F being Field
for S being SymSp of F
for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & x = 0. S holds
PProJ (a,b,x,y) = 0. F
proof end;

theorem Th48: :: SYMSP_1:48
for F being Field
for S being SymSp of F
for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
( PProJ (a,b,x,y) = 0. F iff x _|_ )
proof end;

theorem :: SYMSP_1:49
for F being Field
for S being SymSp of F
for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
proof end;

theorem :: SYMSP_1:50
for F being Field
for S being SymSp of F
for b, a, x, y being Element of S
for l being Element of F st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
proof end;

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))
proof end;