:: SYMSP_1 semantic presentation

definition
let c1 be Field;
attr a2 is strict;
struct SymStr of c1 -> VectSpStr of a1;
aggr SymStr(# carrier, add, Zero, lmult, 2_arg_relation #) -> SymStr of a1;
sel 2_arg_relation c2 -> Relation of the carrier of a2;
end;

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

definition
let c1 be Field;
let c2 be SymStr of c1;
let c3, c4 be Element of c2;
pred c3 _|_ c4 means :Def1: :: SYMSP_1:def 1
[a3,a4] in the 2_arg_relation of a2;
end;

:: deftheorem Def1 defines _|_ SYMSP_1:def 1 :
for b1 being Field
for b2 being SymStr of b1
for b3, b4 being Element of b2 holds
( b3 _|_ b4 iff [b3,b4] in the 2_arg_relation of b2 );

set c1 = {0};

reconsider c2 = 0 as Element of {0} by TARSKI:def 1;

deffunc H1( Element of {0}, Element of {0}) -> Element of {0} = c2;

consider c3 being BinOp of {0} such that
Lemma2: for b1, b2 being Element of {0} holds c3 . b1,b2 = H1(b1,b2) from BINOP_1:sch 2();

E3: now
let c4 be Field;
set c5 = [:{0},{0}:];
defpred S1[ set ] means ex b1, b2 being Element of {0} st
( a1 = [b1,b2] & b2 = c2 );
consider c6 being set such that
E4: for b1 being set holds
( b1 in c6 iff ( b1 in [:{0},{0}:] & S1[b1] ) ) from XBOOLE_0:sch 1();
 c6 c= [:{0},{0}:]
proof
let c7 be set ; :: according to TARSKI:def 3
thus ( not c7 in c6 or c7 in [:{0},{0}:] ) by E4;
end;
then reconsider c7 = c6 as Relation of {0} by RELSET_1:def 1;
take c8 = c7;
thus for b1 being set holds
( b1 in c8 iff ( b1 in [:{0},{0}:] & ex b2, b3 being Element of {0} st
( b1 = [b2,b3] & b3 = c2 ) ) ) by E4;
end;

registration
let c4 be Field;
let c5 be non empty set ;
let c6 be BinOp of c5;
let c7 be Element of c5;
let c8 be Function of [:the carrier of c4,c5:],c5;
let c9 be Relation of c5;
cluster SymStr(# a2,a3,a4,a5,a6 #) -> non empty ;
coherence
not SymStr(# c5,c6,c7,c8,c9 #) is empty
proof end;
end;

Lemma4: for b1 being Field
for b2 being Function of [:the carrier of b1,{0}:],{0}
for b3 being Relation of {0} holds
( SymStr(# {0},c3,c2,b2,b3 #) is Abelian & SymStr(# {0},c3,c2,b2,b3 #) is add-associative & SymStr(# {0},c3,c2,b2,b3 #) is right_zeroed & SymStr(# {0},c3,c2,b2,b3 #) is right_complementable )
proof end;

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

E5: now
let c4 be Field;
let c5 be Function of [:the carrier of c4,{0}:],{0};
assume E6: for b1 being Element of c4
for b2 being Element of {0} holds c5 . [b1,b2] = c2 ;
let c6 be Relation of {0};
let c7 be non empty Abelian add-associative right_zeroed right_complementable SymStr of c4;
assume E7: c7 = SymStr(# {0},c3,c2,c5,c6 #) ;
thus c7 is VectSp-like
proof
for b1, b2 being Element of c4
for b3, b4 being Element of c7 holds
( b1 * (b3 + b4) = (b1 * b3) + (b1 * b4) & (b1 + b2) * b3 = (b1 * b3) + (b2 * b3) & (b1 * b2) * b3 = b1 * (b2 * b3) & (1. c4) * b3 = b3 )
proof
let c8, c9 be Element of c4;
let c10, c11 be Element of c7;
E8: c8 * (c10 + c11) = (c8 * c10) + (c8 * c11)
proof
E9: c10 + c11 = c3 . c10,c11 by E7, RLVECT_1:5;
reconsider c12 = c10, c13 = c11 as Element of {0} by E7;
E10: c3 . c12,c13 = c2 by Lemma2;
reconsider c14 = c12, c15 = c13 as Element of c7 ;
E11: c8 * (c14 + c15) = c5 . c8,c2 by E7, E9, E10, VECTSP_1:def 24;
E12: c8 * (c14 + c15) = c2 by E6, E11;
c5 . c8,c14 = c2 by E6;
then E13: c8 * c14 = c2 by E7, VECTSP_1:def 24;
c5 . c8,c15 = c2 by E6;
then E14: c8 * c15 = c2 by E7, VECTSP_1:def 24;
c2 = 0. c7 by E7, RLVECT_1:def 2;
hence c8 * (c10 + c11) = (c8 * c10) + (c8 * c11) by E12, E13, E14, RLVECT_1:10;
end;
E9: (c8 + c9) * c10 = (c8 * c10) + (c9 * c10)
proof
set c12 = c8 + c9;
E10: (c8 + c9) * c10 = c5 . (c8 + c9),c10 by E7, VECTSP_1:def 24;
reconsider c13 = c10 as Element of c7 ;
reconsider c14 = c13 as Element of c7 ;
E11: (c8 + c9) * c14 = c2 by E6, E7, E10;
reconsider c15 = c14 as Element of c7 ;
E12: c5 . c8,c15 = c2 by E6, E7;
reconsider c16 = c15 as Element of c7 ;
E13: c8 * c16 = c2 by E7, E12, VECTSP_1:def 24;
reconsider c17 = c16 as Element of c7 ;
E14: c5 . c9,c17 = c2 by E6, E7;
reconsider c18 = c17 as Element of c7 ;
E15: c9 * c18 = c2 by E7, E14, VECTSP_1:def 24;
c2 = 0. c7 by E7, RLVECT_1:def 2;
hence (c8 + c9) * c10 = (c8 * c10) + (c9 * c10) by E11, E13, E15, RLVECT_1:10;
end;
E10: (c8 * c9) * c10 = c8 * (c9 * c10)
proof
set c12 = c8 * c9;
E11: (c8 * c9) * c10 = c5 . (c8 * c9),c10 by E7, VECTSP_1:def 24;
reconsider c13 = c10 as Element of c7 ;
reconsider c14 = c13 as Element of c7 ;
E12: (c8 * c9) * c14 = c2 by E6, E7, E11;
reconsider c15 = c14 as Element of c7 ;
E13: c5 . c9,c15 = c2 by E6, E7;
reconsider c16 = c15 as Element of c7 ;
c9 * c16 = c2 by E7, E13, VECTSP_1:def 24;
then E14: c8 * (c9 * c16) = c5 . c8,c2 by E7, VECTSP_1:def 24;
thus (c8 * c9) * c10 = c8 * (c9 * c10) by E6, E12, E14;
end;
(1. c4) * c10 = c10
proof
set c12 = 1. c4;
E11: (1. c4) * c10 = c5 . (1. c4),c10 by E7, VECTSP_1:def 24;
reconsider c13 = c10 as Element of c7 ;
c5 . (1. c4),c13 = c2 by E6, E7;
hence (1. c4) * c10 = c10 by E7, E11, TARSKI:def 1;
end;
hence ( c8 * (c10 + c11) = (c8 * c10) + (c8 * c11) & (c8 + c9) * c10 = (c8 * c10) + (c9 * c10) & (c8 * c9) * c10 = c8 * (c9 * c10) & (1. c4) * c10 = c10 ) by E8, E9, E10;
end;
hence c7 is VectSp-like by VECTSP_1:def 26;
end;
end;

E6: now
let c4 be Field;
let c5 be Function of [:the carrier of c4,{0}:],{0};
assume for b1 being Element of c4
for b2 being Element of {0} holds c5 . [b1,b2] = c2 ;
set c6 = [:{0},{0}:];
let c7 be Relation of {0};
assume E7: for b1 being set holds
( b1 in c7 iff ( b1 in [:{0},{0}:] & ex b2, b3 being Element of {0} st
( b1 = [b2,b3] & b3 = c2 ) ) ) ;
let c8 be non empty Abelian add-associative right_zeroed right_complementable SymStr of c4;
assume E8: c8 = SymStr(# {0},c3,c2,c5,c7 #) ;
E9: for b1, b2 being Element of c8 holds
( b1 _|_ b2 iff ( [b1,b2] in [:{0},{0}:] & ex b3, b4 being Element of {0} st
( [b1,b2] = [b3,b4] & b4 = c2 ) ) )
proof
let c9, c10 be Element of c8;
( c9 _|_ c10 iff [c9,c10] in c7 ) by E8, Def1;
hence ( c9 _|_ c10 iff ( [c9,c10] in [:{0},{0}:] & ex b1, b2 being Element of {0} st
( [c9,c10] = [b1,b2] & b2 = c2 ) ) ) by E7;
end;
E10: for b1, b2 being Element of c8 holds
( b1 _|_ b2 iff b2 = c2 )
proof
let c9, c10 be Element of c8;
E11: ( c9 _|_ c10 implies c10 = c2 )
proof
assume c9 _|_ c10 ;
then ex b1, b2 being Element of {0} st
( [c9,c10] = [b1,b2] & b2 = c2 ) by E9;
hence c10 = c2 by ZFMISC_1:33;
end;
( c10 = c2 implies c9 _|_ c10 )
proof
assume E12: c10 = c2 ;
consider c11, c12 being Element of c8 such that
E13: ( c11 = c9 & c12 = c10 ) ;
[c9,c10] = [c11,c12] by E13;
hence c9 _|_ c10 by E8, E9, E12;
end;
hence ( c9 _|_ c10 iff c10 = c2 ) by E11;
end;
0. c8 = c2 by E8, TARSKI:def 1;
hence for b1 being Element of c8 st b1 <> 0. c8 holds
ex b2 being Element of c8 st not b2 _|_ b1 by E8, TARSKI:def 1;
thus for b1, b2 being Element of c8
for b3 being Element of c4 st b1 _|_ b2 holds
b3 * b1 _|_ b2
proof
let c9, c10 be Element of c8;
let c11 be Element of c4;
assume c9 _|_ c10 ;
then c10 = c2 by E10;
hence c11 * c9 _|_ c10 by E10;
end;
thus for b1, b2, b3 being Element of c8 st b2 _|_ b1 & b3 _|_ b1 holds
b2 + b3 _|_ b1
proof
let c9, c10, c11 be Element of c8;
assume ( c10 _|_ c9 & c11 _|_ c9 ) ;
then c9 = c2 by E10;
hence c10 + c11 _|_ c9 by E10;
end;
thus for b1, b2, b3 being Element of c8 st not b2 _|_ b1 holds
ex b4 being Element of c4 st b3 - (b4 * b2) _|_ b1
proof
let c9, c10, c11 be Element of c8;
assume E11: not c10 _|_ c9 ;
assume for b1 being Element of c4 holds not c11 - (b1 * c10) _|_ c9 ;
c9 <> c2 by E10, E11;
hence contradiction by E8, TARSKI:def 1;
end;
let c9, c10, c11 be Element of c8;
assume ( c9 _|_ c10 + c11 & c10 _|_ c11 + c9 ) ;
assume not c11 _|_ c9 + c10 ;
then c9 + c10 <> c2 by E10;
hence contradiction by E8, TARSKI:def 1;
end;

definition
let c4 be Field;
let c5 be non empty Abelian add-associative right_zeroed right_complementable SymStr of c4;
attr a2 is SymSp-like means :Def2: :: SYMSP_1:def 2
for b1, b2, b3, b4 being Element of a2
for b5 being Element of a1 holds
( ( b1 <> 0. a2 implies ex b6 being Element of a2 st not b6 _|_ b1 ) & ( b1 _|_ b2 implies b5 * b1 _|_ b2 ) & ( b2 _|_ b1 & b3 _|_ b1 implies b2 + b3 _|_ b1 ) & ( not b2 _|_ b1 implies ex b6 being Element of a1 st b4 - (b6 * b2) _|_ b1 ) & ( b1 _|_ b2 + b3 & b2 _|_ b3 + b1 implies b3 _|_ b1 + b2 ) );
end;

:: deftheorem Def2 defines SymSp-like SYMSP_1:def 2 :
for b1 being Field
for b2 being non empty Abelian add-associative right_zeroed right_complementable SymStr of b1 holds
( b2 is SymSp-like iff for b3, b4, b5, b6 being Element of b2
for b7 being Element of b1 holds
( ( b3 <> 0. b2 implies ex b8 being Element of b2 st not b8 _|_ b3 ) & ( b3 _|_ b4 implies b7 * b3 _|_ b4 ) & ( b4 _|_ b3 & b5 _|_ b3 implies b4 + b5 _|_ b3 ) & ( not b4 _|_ b3 implies ex b8 being Element of b1 st b6 - (b8 * b4) _|_ b3 ) & ( b3 _|_ b4 + b5 & b4 _|_ b5 + b3 implies b5 _|_ b3 + b4 ) ) );

registration
let c4 be Field;
cluster non empty Abelian add-associative right_zeroed right_complementable VectSp-like strict SymSp-like SymStr of a1;
existence
ex b1 being non empty Abelian add-associative right_zeroed right_complementable SymStr of c4 st
( b1 is SymSp-like & b1 is VectSp-like & b1 is strict )
proof end;
end;

definition
let c4 be Field;
mode SymSp of a1 is non empty Abelian add-associative right_zeroed right_complementable VectSp-like SymSp-like SymStr of a1;
end;

theorem Th1: :: SYMSP_1:1
canceled;

theorem Th2: :: SYMSP_1:2
canceled;

theorem Th3: :: SYMSP_1:3
canceled;

theorem Th4: :: SYMSP_1:4
canceled;

theorem Th5: :: SYMSP_1:5
canceled;

theorem Th6: :: SYMSP_1:6
canceled;

theorem Th7: :: SYMSP_1:7
canceled;

theorem Th8: :: SYMSP_1:8
canceled;

theorem Th9: :: SYMSP_1:9
canceled;

theorem Th10: :: SYMSP_1:10
canceled;

theorem Th11: :: SYMSP_1:11
for b1 being Field
for b2 being SymSp of b1
for b3 being Element of b2 holds 0. b2 _|_ b3
proof end;

theorem Th12: :: SYMSP_1:12
for b1 being Field
for b2 being SymSp of b1
for b3, b4 being Element of b2 st b3 _|_ b4 holds
b4 _|_ b3
proof end;

theorem Th13: :: SYMSP_1:13
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & b5 + b3 _|_ b4 holds
not b5 _|_ b4
proof end;

theorem Th14: :: SYMSP_1:14
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & b5 _|_ b4 holds
not b3 + b5 _|_ b4
proof end;

theorem Th15: :: SYMSP_1:15
for b1 being Field
for b2 being SymSp of b1
for b3, b4 being Element of b2
for b5 being Element of b1 st not b3 _|_ b4 & not b5 = 0. b1 holds
( not b5 * b3 _|_ b4 & not b3 _|_ b5 * b4 )
proof end;

theorem Th16: :: SYMSP_1:16
for b1 being Field
for b2 being SymSp of b1
for b3, b4 being Element of b2 st b3 _|_ b4 holds
- b3 _|_ b4
proof end;

theorem Th17: :: SYMSP_1:17
canceled;

theorem Th18: :: SYMSP_1:18
canceled;

theorem Th19: :: SYMSP_1:19
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 holds
( b3 _|_ b4 or not b3 + b5 _|_ b4 or not (((1. b1) + (1. b1)) * b3) + b5 _|_ b4 )
proof end;

theorem Th20: :: SYMSP_1:20
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & b3 _|_ b5 & not b6 _|_ b5 & b6 _|_ b4 holds
( not b3 + b6 _|_ b4 & not b3 + b6 _|_ b5 )
proof end;

theorem Th21: :: SYMSP_1:21
for b1 being Field
for b2 being SymSp of b1
for b3, b4 being Element of b2 st b3 <> 0. b2 & b4 <> 0. b2 holds
ex b5 being Element of b2 st
( not b5 _|_ b3 & not b5 _|_ b4 )
proof end;

theorem Th22: :: SYMSP_1:22
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 st (1. b1) + (1. b1) <> 0. b1 & b3 <> 0. b2 & b4 <> 0. b2 & b5 <> 0. b2 holds
ex b6 being Element of b2 st
( not b6 _|_ b3 & not b6 _|_ b4 & not b6 _|_ b5 )
proof end;

theorem Th23: :: SYMSP_1:23
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st b3 - b4 _|_ b5 & b3 - b6 _|_ b5 holds
b4 - b6 _|_ b5
proof end;

theorem Th24: :: SYMSP_1:24
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2
for b6, b7 being Element of b1 st not b3 _|_ b4 & b5 - (b6 * b3) _|_ b4 & b5 - (b7 * b3) _|_ b4 holds
b6 = b7
proof end;

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

definition
let c4 be Field;
let c5 be SymSp of c4;
let c6, c7, c8 be Element of c5;
assume E21: not c7 _|_ c6 ;
canceled;
canceled;
canceled;
func ProJ c3,c4,c5 -> Element of a1 means :Def6: :: SYMSP_1:def 6
for b1 being Element of a1 st a5 - (b1 * a4) _|_ a3 holds
a6 = b1;
existence
ex b1 being Element of c4 st
for b2 being Element of c4 st c8 - (b2 * c7) _|_ c6 holds
b1 = b2
proof end;
uniqueness
for b1, b2 being Element of c4 st ( for b3 being Element of c4 st c8 - (b3 * c7) _|_ c6 holds
b1 = b3 ) & ( for b3 being Element of c4 st c8 - (b3 * c7) _|_ c6 holds
b2 = b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 SYMSP_1:def 3 :
canceled;

:: deftheorem Def4 SYMSP_1:def 4 :
canceled;

:: deftheorem Def5 SYMSP_1:def 5 :
canceled;

:: deftheorem Def6 defines ProJ SYMSP_1:def 6 :
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 st not b4 _|_ b3 holds
for b6 being Element of b1 holds
( b6 = ProJ b3,b4,b5 iff for b7 being Element of b1 st b5 - (b7 * b4) _|_ b3 holds
b6 = b7 );

theorem Th26: :: SYMSP_1:26
canceled;

theorem Th27: :: SYMSP_1:27
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 holds
b5 - ((ProJ b4,b3,b5) * b3) _|_ b4
proof end;

theorem Th28: :: SYMSP_1:28
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2
for b6 being Element of b1 st not b3 _|_ b4 holds
ProJ b4,b3,(b6 * b5) = b6 * (ProJ b4,b3,b5)
proof end;

theorem Th29: :: SYMSP_1:29
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 holds
ProJ b4,b3,(b5 + b6) = (ProJ b4,b3,b5) + (ProJ b4,b3,b6)
proof end;

theorem Th30: :: SYMSP_1:30
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2
for b6 being Element of b1 st not b3 _|_ b4 & b6 <> 0. b1 holds
ProJ b4,(b6 * b3),b5 = (b6 " ) * (ProJ b4,b3,b5)
proof end;

theorem Th31: :: SYMSP_1:31
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2
for b6 being Element of b1 st not b3 _|_ b4 & b6 <> 0. b1 holds
ProJ (b6 * b4),b3,b5 = ProJ b4,b3,b5
proof end;

theorem Th32: :: SYMSP_1:32
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & b5 _|_ b4 holds
( ProJ b4,(b3 + b5),b6 = ProJ b4,b3,b6 & ProJ b4,b3,(b6 + b5) = ProJ b4,b3,b6 )
proof end;

theorem Th33: :: SYMSP_1:33
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & b5 _|_ b3 & b5 _|_ b6 holds
ProJ (b4 + b5),b3,b6 = ProJ b4,b3,b6
proof end;

theorem Th34: :: SYMSP_1:34
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & b5 - b3 _|_ b4 holds
ProJ b4,b3,b5 = 1. b1
proof end;

theorem Th35: :: SYMSP_1:35
for b1 being Field
for b2 being SymSp of b1
for b3, b4 being Element of b2 st not b3 _|_ b4 holds
ProJ b4,b3,b3 = 1. b1
proof end;

theorem Th36: :: SYMSP_1:36
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 holds
( b5 _|_ b4 iff ProJ b4,b3,b5 = 0. b1 )
proof end;

theorem Th37: :: SYMSP_1:37
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & not b5 _|_ b4 holds
(ProJ b4,b3,b6) * ((ProJ b4,b3,b5) " ) = ProJ b4,b5,b6
proof end;

theorem Th38: :: SYMSP_1:38
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & not b5 _|_ b4 holds
ProJ b4,b3,b5 = (ProJ b4,b5,b3) "
proof end;

theorem Th39: :: SYMSP_1:39
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & b3 _|_ b5 + b4 holds
ProJ b4,b3,b5 = ProJ b5,b3,b4
proof end;

theorem Th40: :: SYMSP_1:40
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & not b5 _|_ b4 holds
ProJ b5,b4,b3 = (- ((ProJ b4,b3,b5) " )) * (ProJ b3,b4,b5)
proof end;

theorem Th41: :: SYMSP_1:41
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st (1. b1) + (1. b1) <> 0. b1 & not b3 _|_ b4 & not b3 _|_ b5 & not b6 _|_ b4 & not b6 _|_ b5 holds
(ProJ b3,b4,b5) * (ProJ b6,b5,b4) = (ProJ b4,b3,b6) * (ProJ b5,b6,b3)
proof end;

theorem Th42: :: SYMSP_1:42
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st (1. b1) + (1. b1) <> 0. b1 & not b3 _|_ b4 & not b3 _|_ b5 & not b6 _|_ b4 & not b6 _|_ b5 holds
(ProJ b4,b6,b3) * (ProJ b3,b4,b5) = (ProJ b5,b6,b3) * (ProJ b6,b4,b5)
proof end;

theorem Th43: :: SYMSP_1:43
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6, b7, b8 being Element of b2 st (1. b1) + (1. b1) <> 0. b1 & not b3 _|_ b4 & not b3 _|_ b5 & not b6 _|_ b4 & not b6 _|_ b5 & not b7 _|_ b4 holds
((ProJ b4,b7,b3) * (ProJ b3,b4,b5)) * (ProJ b5,b3,b8) = ((ProJ b4,b7,b6) * (ProJ b6,b4,b5)) * (ProJ b5,b6,b8)
proof end;

theorem Th44: :: SYMSP_1:44
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & not b5 _|_ b4 & not b6 _|_ b4 holds
(ProJ b4,b3,b5) * (ProJ b5,b4,b6) = (- (ProJ b4,b3,b6)) * (ProJ b6,b4,b5)
proof end;

definition
let c4 be Field;
let c5 be SymSp of c4;
let c6, c7, c8, c9 be Element of c5;
assume that
E39: not c9 _|_ c8 and
E40: (1. c4) + (1. c4) <> 0. c4 ;
func PProJ c5,c6,c3,c4 -> Element of a1 means :Def7: :: SYMSP_1:def 7
for b1 being Element of a2 st not b1 _|_ a5 & not b1 _|_ a3 holds
a7 = ((ProJ a5,a6,b1) * (ProJ b1,a5,a3)) * (ProJ a3,b1,a4) if ex b1 being Element of a2 st
( not b1 _|_ a5 & not b1 _|_ a3 )
a7 = 0. a1 if for b1 being Element of a2 holds
( b1 _|_ a5 or b1 _|_ a3 )
;
existence
( ( ex b1 being Element of c5 st
( not b1 _|_ c8 & not b1 _|_ c6 ) implies ex b1 being Element of c4 st
for b2 being Element of c5 st not b2 _|_ c8 & not b2 _|_ c6 holds
b1 = ((ProJ c8,c9,b2) * (ProJ b2,c8,c6)) * (ProJ c6,b2,c7) ) & ( ( for b1 being Element of c5 holds
( b1 _|_ c8 or b1 _|_ c6 ) ) implies ex b1 being Element of c4 st b1 = 0. c4 ) )
proof end;
uniqueness
for b1, b2 being Element of c4 holds
( ( ex b3 being Element of c5 st
( not b3 _|_ c8 & not b3 _|_ c6 ) & ( for b3 being Element of c5 st not b3 _|_ c8 & not b3 _|_ c6 holds
b1 = ((ProJ c8,c9,b3) * (ProJ b3,c8,c6)) * (ProJ c6,b3,c7) ) & ( for b3 being Element of c5 st not b3 _|_ c8 & not b3 _|_ c6 holds
b2 = ((ProJ c8,c9,b3) * (ProJ b3,c8,c6)) * (ProJ c6,b3,c7) ) implies b1 = b2 ) & ( ( for b3 being Element of c5 holds
( b3 _|_ c8 or b3 _|_ c6 ) ) & b1 = 0. c4 & b2 = 0. c4 implies b1 = b2 ) )
proof end;
consistency
for b1 being Element of c4 st ex b2 being Element of c5 st
( not b2 _|_ c8 & not b2 _|_ c6 ) & ( for b2 being Element of c5 holds
( b2 _|_ c8 or b2 _|_ c6 ) ) holds
( ( for b2 being Element of c5 st not b2 _|_ c8 & not b2 _|_ c6 holds
b1 = ((ProJ c8,c9,b2) * (ProJ b2,c8,c6)) * (ProJ c6,b2,c7) ) iff b1 = 0. c4 ) ;
end;

:: deftheorem Def7 defines PProJ SYMSP_1:def 7 :
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st not b6 _|_ b5 & (1. b1) + (1. b1) <> 0. b1 holds
for b7 being Element of b1 holds
( ( ex b8 being Element of b2 st
( not b8 _|_ b5 & not b8 _|_ b3 ) implies ( b7 = PProJ b5,b6,b3,b4 iff for b8 being Element of b2 st not b8 _|_ b5 & not b8 _|_ b3 holds
b7 = ((ProJ b5,b6,b8) * (ProJ b8,b5,b3)) * (ProJ b3,b8,b4) ) ) & ( ( for b8 being Element of b2 holds
( b8 _|_ b5 or b8 _|_ b3 ) ) implies ( b7 = PProJ b5,b6,b3,b4 iff b7 = 0. b1 ) ) );

theorem Th45: :: SYMSP_1:45
canceled;

theorem Th46: :: SYMSP_1:46
canceled;

theorem Th47: :: SYMSP_1:47
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st (1. b1) + (1. b1) <> 0. b1 & not b3 _|_ b4 & b5 = 0. b2 holds
PProJ b4,b3,b5,b6 = 0. b1
proof end;

Lemma41: for b1 being Field
for b2 being SymSp of b1
for b3 being Element of b2 holds b3 _|_ 0. b2
proof end;

theorem Th48: :: SYMSP_1:48
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st (1. b1) + (1. b1) <> 0. b1 & not b3 _|_ b4 holds
( PProJ b4,b3,b5,b6 = 0. b1 iff b6 _|_ b5 )
proof end;

theorem Th49: :: SYMSP_1:49
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2 st (1. b1) + (1. b1) <> 0. b1 & not b3 _|_ b4 holds
PProJ b4,b3,b5,b6 = - (PProJ b4,b3,b6,b5)
proof end;

theorem Th50: :: SYMSP_1:50
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6 being Element of b2
for b7 being Element of b1 st (1. b1) + (1. b1) <> 0. b1 & not b3 _|_ b4 holds
PProJ b4,b3,b5,(b7 * b6) = b7 * (PProJ b4,b3,b5,b6)
proof end;

theorem Th51: :: SYMSP_1:51
for b1 being Field
for b2 being SymSp of b1
for b3, b4, b5, b6, b7 being Element of b2 st (1. b1) + (1. b1) <> 0. b1 & not b3 _|_ b4 holds
PProJ b4,b3,b5,(b6 + b7) = (PProJ b4,b3,b5,b6) + (PProJ b4,b3,b5,b7)
proof end;