:: TDGROUP semantic presentation

theorem Th1: :: TDGROUP:1
canceled;

theorem Th2: :: TDGROUP:2
for b1 being Element of G_Real ex b2 being Element of G_Real st b2 + b2 = b1
proof end;

theorem Th3: :: TDGROUP:3
for b1 being Element of G_Real st b1 + b1 = 0. G_Real holds
b1 = 0. G_Real
proof end;

definition
let c1 be non empty LoopStr ;
attr a1 is Two_Divisible means :Def1: :: TDGROUP:def 1
for b1 being Element of a1 ex b2 being Element of a1 st b2 + b2 = b1;
end;

:: deftheorem Def1 defines Two_Divisible TDGROUP:def 1 :
for b1 being non empty LoopStr holds
( b1 is Two_Divisible iff for b2 being Element of b1 ex b3 being Element of b1 st b3 + b3 = b2 );

Lemma4: G_Real is Fanoian
proof end;

registration
cluster G_Real -> Fanoian Two_Divisible ;
coherence
( G_Real is Fanoian & G_Real is Two_Divisible ) by Def1, Lemma4, Th2;
end;

registration
cluster non empty strict Abelian add-associative right_zeroed right_complementable Fanoian Two_Divisible LoopStr ;
existence
ex b1 being non empty LoopStr st
( b1 is strict & b1 is Fanoian & b1 is Two_Divisible & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian ) by Lemma4;
end;

definition
mode Two_Divisible_Group is non empty Abelian add-associative right_zeroed right_complementable Two_Divisible LoopStr ;
end;

definition
mode Uniquely_Two_Divisible_Group is non empty Abelian add-associative right_zeroed right_complementable Fanoian Two_Divisible LoopStr ;
end;

theorem Th4: :: TDGROUP:4
canceled;

theorem Th5: :: TDGROUP:5
canceled;

theorem Th6: :: TDGROUP:6
canceled;

theorem Th7: :: TDGROUP:7
for b1 being non empty Abelian add-associative right_zeroed right_complementable LoopStr holds
( b1 is Uniquely_Two_Divisible_Group iff ( ( for b2 being Element of b1 ex b3 being Element of b1 st b3 + b3 = b2 ) & ( for b2 being Element of b1 st b2 + b2 = 0. b1 holds
b2 = 0. b1 ) ) ) by Def1, VECTSP_1:def 28;

notation
let c1 be non empty LoopStr ;
let c2, c3 be Element of c1;
synonym c2 # c3 for c2 + c3;
end;

definition
let c1 be non empty LoopStr ;
canceled;
canceled;
func CONGRD c1 -> Relation of [:the carrier of a1,the carrier of a1:] means :Def4: :: TDGROUP:def 4
for b1, b2, b3, b4 being Element of a1 holds
( [[b1,b2],[b3,b4]] in a2 iff b1 # b4 = b2 # b3 );
existence
ex b1 being Relation of [:the carrier of c1,the carrier of c1:] st
for b2, b3, b4, b5 being Element of c1 holds
( [[b2,b3],[b4,b5]] in b1 iff b2 # b5 = b3 # b4 )
proof end;
uniqueness
for b1, b2 being Relation of [:the carrier of c1,the carrier of c1:] st ( for b3, b4, b5, b6 being Element of c1 holds
( [[b3,b4],[b5,b6]] in b1 iff b3 # b6 = b4 # b5 ) ) & ( for b3, b4, b5, b6 being Element of c1 holds
( [[b3,b4],[b5,b6]] in b2 iff b3 # b6 = b4 # b5 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 TDGROUP:def 2 :
canceled;

:: deftheorem Def3 TDGROUP:def 3 :
canceled;

:: deftheorem Def4 defines CONGRD TDGROUP:def 4 :
for b1 being non empty LoopStr
for b2 being Relation of [:the carrier of b1,the carrier of b1:] holds
( b2 = CONGRD b1 iff for b3, b4, b5, b6 being Element of b1 holds
( [[b3,b4],[b5,b6]] in b2 iff b3 # b6 = b4 # b5 ) );

definition
let c1 be non empty LoopStr ;
func AV c1 -> strict AffinStruct equals :: TDGROUP:def 5
 AffinStruct(# the carrier of a1,(CONGRD a1) #);
coherence
AffinStruct(# the carrier of c1,(CONGRD c1) #) is strict AffinStruct ;
end;

:: deftheorem Def5 defines AV TDGROUP:def 5 :
for b1 being non empty LoopStr holds AV b1 = AffinStruct(# the carrier of b1,(CONGRD b1) #);

registration
let c1 be non empty LoopStr ;
cluster AV a1 -> non empty strict ;
coherence
not AV c1 is empty
proof end;
end;

theorem Th8: :: TDGROUP:8
canceled;

theorem Th9: :: TDGROUP:9
for b1 being Uniquely_Two_Divisible_Group holds
( the carrier of (AV b1) = the carrier of b1 & the CONGR of (AV b1) = CONGRD b1 ) ;

definition
let c1 be Uniquely_Two_Divisible_Group;
let c2, c3, c4, c5 be Element of c1;
pred c2,c3 ==> c4,c5 means :Def6: :: TDGROUP:def 6
[[a2,a3],[a4,a5]] in the CONGR of (AV a1);
end;

:: deftheorem Def6 defines ==> TDGROUP:def 6 :
for b1 being Uniquely_Two_Divisible_Group
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 ==> b4,b5 iff [[b2,b3],[b4,b5]] in the CONGR of (AV b1) );

theorem Th10: :: TDGROUP:10
for b1 being Uniquely_Two_Divisible_Group
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 ==> b4,b5 iff b2 # b5 = b3 # b4 )
proof end;

theorem Th11: :: TDGROUP:11
ex b1, b2 being Element of G_Real st b1 <> b2
proof end;

theorem Th12: :: TDGROUP:12
ex b1 being Uniquely_Two_Divisible_Groupex b2, b3 being Element of b1 st b2 <> b3 by Th11;

theorem Th13: :: TDGROUP:13
for b1 being Uniquely_Two_Divisible_Group
for b2, b3, b4 being Element of b1 st b2,b3 ==> b4,b4 holds
b2 = b3
proof end;

theorem Th14: :: TDGROUP:14
for b1 being Uniquely_Two_Divisible_Group
for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 ==> b4,b5 & b6,b7 ==> b4,b5 holds
b2,b3 ==> b6,b7
proof end;

theorem Th15: :: TDGROUP:15
for b1 being Uniquely_Two_Divisible_Group
for b2, b3, b4 being Element of b1 ex b5 being Element of b1 st b2,b3 ==> b4,b5
proof end;

theorem Th16: :: TDGROUP:16
for b1 being Uniquely_Two_Divisible_Group
for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 ==> b4,b5 & b2,b6 ==> b4,b7 holds
b3,b6 ==> b5,b7
proof end;

theorem Th17: :: TDGROUP:17
for b1 being Uniquely_Two_Divisible_Group
for b2, b3 being Element of b1 ex b4 being Element of b1 st b2,b4 ==> b4,b3
proof end;

theorem Th18: :: TDGROUP:18
for b1 being Uniquely_Two_Divisible_Group
for b2, b3, b4, b5 being Element of b1 st b2,b3 ==> b3,b4 & b2,b5 ==> b5,b4 holds
b3 = b5
proof end;

theorem Th19: :: TDGROUP:19
for b1 being Uniquely_Two_Divisible_Group
for b2, b3, b4, b5 being Element of b1 st b2,b3 ==> b4,b5 holds
b2,b4 ==> b3,b5
proof end;

theorem Th20: :: TDGROUP:20
for b1 being Uniquely_Two_Divisible_Group st ex b2, b3 being Element of b1 st b2 <> b3 holds
( ex b2, b3 being Element of (AV b1) st b2 <> b3 & ( for b2, b3, b4 being Element of (AV b1) st b2,b3 // b4,b4 holds
b2 = b3 ) & ( for b2, b3, b4, b5, b6, b7 being Element of (AV b1) st b2,b3 // b6,b7 & b4,b5 // b6,b7 holds
b2,b3 // b4,b5 ) & ( for b2, b3, b4 being Element of (AV b1) ex b5 being Element of (AV b1) st b2,b3 // b4,b5 ) & ( for b2, b3, b4, b5, b6, b7 being Element of (AV b1) st b2,b3 // b5,b6 & b2,b4 // b5,b7 holds
b3,b4 // b6,b7 ) & ( for b2, b3 being Element of (AV b1) ex b4 being Element of (AV b1) st b2,b4 // b4,b3 ) & ( for b2, b3, b4, b5 being Element of (AV b1) st b2,b3 // b3,b4 & b2,b5 // b5,b4 holds
b3 = b5 ) & ( for b2, b3, b4, b5 being Element of (AV b1) st b2,b3 // b4,b5 holds
b2,b4 // b3,b5 ) )
proof end;

definition
let c1 be non empty AffinStruct ;
canceled;
attr a1 is AffVect-like means :Def8: :: TDGROUP:def 8
( ( for b1, b2, b3 being Element of a1 st b1,b2 // b3,b3 holds
b1 = b2 ) & ( for b1, b2, b3, b4, b5, b6 being Element of a1 st b1,b2 // b5,b6 & b3,b4 // b5,b6 holds
b1,b2 // b3,b4 ) & ( for b1, b2, b3 being Element of a1 ex b4 being Element of a1 st b1,b2 // b3,b4 ) & ( for b1, b2, b3, b4, b5, b6 being Element of a1 st b1,b2 // b4,b5 & b1,b3 // b4,b6 holds
b2,b3 // b5,b6 ) & ( for b1, b2 being Element of a1 ex b3 being Element of a1 st b1,b3 // b3,b2 ) & ( for b1, b2, b3, b4 being Element of a1 st b1,b2 // b2,b3 & b1,b4 // b4,b3 holds
b2 = b4 ) & ( for b1, b2, b3, b4 being Element of a1 st b1,b2 // b3,b4 holds
b1,b3 // b2,b4 ) );
end;

:: deftheorem Def7 TDGROUP:def 7 :
canceled;

:: deftheorem Def8 defines AffVect-like TDGROUP:def 8 :
for b1 being non empty AffinStruct holds
( b1 is AffVect-like iff ( ( for b2, b3, b4 being Element of b1 st b2,b3 // b4,b4 holds
b2 = b3 ) & ( for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 // b6,b7 & b4,b5 // b6,b7 holds
b2,b3 // b4,b5 ) & ( for b2, b3, b4 being Element of b1 ex b5 being Element of b1 st b2,b3 // b4,b5 ) & ( for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 // b5,b6 & b2,b4 // b5,b7 holds
b3,b4 // b6,b7 ) & ( for b2, b3 being Element of b1 ex b4 being Element of b1 st b2,b4 // b4,b3 ) & ( for b2, b3, b4, b5 being Element of b1 st b2,b3 // b3,b4 & b2,b5 // b5,b4 holds
b3 = b5 ) & ( for b2, b3, b4, b5 being Element of b1 st b2,b3 // b4,b5 holds
b2,b4 // b3,b5 ) ) );

registration
cluster non empty non trivial strict AffVect-like AffinStruct ;
existence
ex b1 being non empty AffinStruct st
( b1 is strict & not b1 is trivial & b1 is AffVect-like )
proof end;
end;

definition
mode AffVect is non empty non trivial AffVect-like AffinStruct ;
end;

theorem Th21: :: TDGROUP:21
for b1 being non empty AffinStruct holds
( ( ex b2, b3 being Element of b1 st b2 <> b3 & ( for b2, b3, b4 being Element of b1 st b2,b3 // b4,b4 holds
b2 = b3 ) & ( for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 // b6,b7 & b4,b5 // b6,b7 holds
b2,b3 // b4,b5 ) & ( for b2, b3, b4 being Element of b1 ex b5 being Element of b1 st b2,b3 // b4,b5 ) & ( for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 // b5,b6 & b2,b4 // b5,b7 holds
b3,b4 // b6,b7 ) & ( for b2, b3 being Element of b1 ex b4 being Element of b1 st b2,b4 // b4,b3 ) & ( for b2, b3, b4, b5 being Element of b1 st b2,b3 // b3,b4 & b2,b5 // b5,b4 holds
b3 = b5 ) & ( for b2, b3, b4, b5 being Element of b1 st b2,b3 // b4,b5 holds
b2,b4 // b3,b5 ) ) iff b1 is AffVect ) by Def8, REALSET2:def 7;

theorem Th22: :: TDGROUP:22
for b1 being Uniquely_Two_Divisible_Group st ex b2, b3 being Element of b1 st b2 <> b3 holds
AV b1 is AffVect
proof end;