:: TDGROUP semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: TDGROUP:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: TDGROUP:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Element of G_Real ex b being Element of G_Real st b + b = a
proof end;

theorem Th3: :: TDGROUP:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Element of G_Real st a + a = 0. G_Real holds
a = 0. G_Real
proof end;

definition
let IT be non empty LoopStr ;
attr IT is Two_Divisible means :Def1: :: TDGROUP:def 1
for a being Element of IT ex b being Element of IT st b + b = a;
end;

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

Lm1: 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, Lm1, 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 Lm1;
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 :: TDGROUP:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TDGROUP:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TDGROUP:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TDGROUP:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AG being non empty Abelian add-associative right_zeroed right_complementable LoopStr holds
( AG is Uniquely_Two_Divisible_Group iff ( ( for a being Element of AG ex b being Element of AG st b + b = a ) & ( for a being Element of AG st a + a = 0. AG holds
a = 0. AG ) ) ) by Def1, VECTSP_1:def 28;

notation
let ADG be non empty LoopStr ;
let a, b be Element of ADG;
synonym a # b for a + b;
end;

definition
let ADG be non empty LoopStr ;
canceled;
canceled;
func CONGRD ADG -> Relation of [:the carrier of ADG,the carrier of ADG:] means :Def4: :: TDGROUP:def 4
for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in it iff a # d = b # c );
existence
ex b1 being Relation of [:the carrier of ADG,the carrier of ADG:] st
for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in b1 iff a # d = b # c )
proof end;
uniqueness
for b1, b2 being Relation of [:the carrier of ADG,the carrier of ADG:] st ( for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in b1 iff a # d = b # c ) ) & ( for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in b2 iff a # d = b # c ) ) holds
b1 = b2
proof end;
end;

:: deftheorem TDGROUP:def 2 :
canceled;

:: deftheorem TDGROUP:def 3 :
canceled;

:: deftheorem Def4 defines CONGRD TDGROUP:def 4 :
for ADG being non empty LoopStr
for b2 being Relation of [:the carrier of ADG,the carrier of ADG:] holds
( b2 = CONGRD ADG iff for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in b2 iff a # d = b # c ) );

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

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

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

theorem :: TDGROUP:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TDGROUP:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group holds
( the carrier of (AV ADG) = the carrier of ADG & the CONGR of (AV ADG) = CONGRD ADG ) ;

definition
let ADG be Uniquely_Two_Divisible_Group;
let a, b, c, d be Element of ADG;
pred a,b ==> c,d means :Def6: :: TDGROUP:def 6
[[a,b],[c,d]] in the CONGR of (AV ADG);
end;

:: deftheorem Def6 defines ==> TDGROUP:def 6 :
for ADG being Uniquely_Two_Divisible_Group
for a, b, c, d being Element of ADG holds
( a,b ==> c,d iff [[a,b],[c,d]] in the CONGR of (AV ADG) );

theorem Th10: :: TDGROUP:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group
for a, b, c, d being Element of ADG holds
( a,b ==> c,d iff a # d = b # c )
proof end;

theorem Th11: :: TDGROUP:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex a, b being Element of G_Real st a <> b
proof end;

theorem :: TDGROUP:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex ADG being Uniquely_Two_Divisible_Group ex a, b being Element of ADG st a <> b by Th11;

theorem Th13: :: TDGROUP:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group
for a, b, c being Element of ADG st a,b ==> c,c holds
a = b
proof end;

theorem Th14: :: TDGROUP:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group
for a, b, p, q, c, d being Element of ADG st a,b ==> p,q & c,d ==> p,q holds
a,b ==> c,d
proof end;

theorem Th15: :: TDGROUP:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group
for a, b, c being Element of ADG ex d being Element of ADG st a,b ==> c,d
proof end;

theorem Th16: :: TDGROUP:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group
for a, b, a', b', c, c' being Element of ADG st a,b ==> a',b' & a,c ==> a',c' holds
b,c ==> b',c'
proof end;

theorem Th17: :: TDGROUP:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group
for a, c being Element of ADG ex b being Element of ADG st a,b ==> b,c
proof end;

theorem Th18: :: TDGROUP:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group
for a, b, c, b' being Element of ADG st a,b ==> b,c & a,b' ==> b',c holds
b = b'
proof end;

theorem Th19: :: TDGROUP:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group
for a, b, c, d being Element of ADG st a,b ==> c,d holds
a,c ==> b,d
proof end;

theorem Th20: :: TDGROUP:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group st ex a, b being Element of ADG st a <> b holds
( ex a, b being Element of (AV ADG) st a <> b & ( for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b ) & ( for a, b, c, d, p, q being Element of (AV ADG) st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d ) & ( for a, b, c, a', b', c' being Element of (AV ADG) st a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b' being Element of (AV ADG) st a,b // b,c & a,b' // b',c holds
b = b' ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
proof end;

definition
let IT be non empty AffinStruct ;
canceled;
attr IT is AffVect-like means :Def8: :: TDGROUP:def 8
( ( for a, b, c being Element of IT st a,b // c,c holds
a = b ) & ( for a, b, c, d, p, q being Element of IT st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, b, c being Element of IT ex d being Element of IT st a,b // c,d ) & ( for a, b, c, a', b', c' being Element of IT st a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, b, c, b' being Element of IT st a,b // b,c & a,b' // b',c holds
b = b' ) & ( for a, b, c, d being Element of IT st a,b // c,d holds
a,c // b,d ) );
end;

:: deftheorem TDGROUP:def 7 :
canceled;

:: deftheorem Def8 defines AffVect-like TDGROUP:def 8 :
for IT being non empty AffinStruct holds
( IT is AffVect-like iff ( ( for a, b, c being Element of IT st a,b // c,c holds
a = b ) & ( for a, b, c, d, p, q being Element of IT st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, b, c being Element of IT ex d being Element of IT st a,b // c,d ) & ( for a, b, c, a', b', c' being Element of IT st a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, b, c, b' being Element of IT st a,b // b,c & a,b' // b',c holds
b = b' ) & ( for a, b, c, d being Element of IT st a,b // c,d holds
a,c // b,d ) ) );

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 :: TDGROUP:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for AS being non empty AffinStruct holds
( ( ex a, b being Element of AS st a <> b & ( for a, b, c being Element of AS st a,b // c,c holds
a = b ) & ( for a, b, c, d, p, q being Element of AS st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, b, c being Element of AS ex d being Element of AS st a,b // c,d ) & ( for a, b, c, a', b', c' being Element of AS st a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a, c being Element of AS ex b being Element of AS st a,b // b,c ) & ( for a, b, c, b' being Element of AS st a,b // b,c & a,b' // b',c holds
b = b' ) & ( for a, b, c, d being Element of AS st a,b // c,d holds
a,c // b,d ) ) iff AS is AffVect ) by Def8, REALSET2:def 7;

theorem :: TDGROUP:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ADG being Uniquely_Two_Divisible_Group st ex a, b being Element of ADG st a <> b holds
AV ADG is AffVect
proof end;