:: TDGROUP semantic presentation

begin

theorem Th1: :: TDGROUP:1
for a being Element of G_Real ex b being Element of G_Real st b + b = a
proof
set G = G_Real ;
let a be Element of G_Real; ::_thesis: ex b being Element of G_Real st b + b = a
reconsider a = a as Element of REAL ;
reconsider b9 = a / 2 as Real ;
consider b being Element of G_Real such that
A1: b = b9 ;
 b + b = a by A1;
hence  ex b being Element of G_Real st b + b = a ; ::_thesis: verum
end;

theorem :: TDGROUP:2
for a being Element of G_Real st a + a = 0. G_Real holds
a = 0. G_Real ;

definition
let IT be non empty addLoopStr ;
attrIT 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 addLoopStr 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
let a be Element of G_Real; :: according to VECTSP_1:def_18 ::_thesis: ( not a # a = 0. G_Real or a = 0. G_Real )
assume  a + a = 0. G_Real ; ::_thesis: a = 0. G_Real
hence  a = 0. G_Real ; ::_thesis: verum
end;

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

registration
cluster non empty strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible for addLoopStr ;
existence
 ex b1 being non empty addLoopStr 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 right_complementable Abelian add-associative right_zeroed Two_Divisible addLoopStr ;
end;

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

theorem :: TDGROUP:3
for AG being non empty right_complementable Abelian add-associative right_zeroed addLoopStr 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_18;


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

definition
let ADG be non empty addLoopStr ;
func CONGRD ADG ->  Relation of [: the carrier of ADG, the carrier of ADG:] means :Def2: :: TDGROUP:def 2
 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
set X = the carrier of ADG;
set XX = [: the carrier of ADG, the carrier of ADG:];
defpred S1[ set , set ] means  ex a, b, c, d being Element of the carrier of ADG st
( $1 = [a,b] & $2 = [c,d] & a # d = b # c );
consider P being Relation of [: the carrier of ADG, the carrier of ADG:],[: the carrier of ADG, the carrier of ADG:] such that
A1: for x, y being set holds
( [x,y] in P iff ( x in [: the carrier of ADG, the carrier of ADG:] & y in [: the carrier of ADG, the carrier of ADG:] & S1[x,y] ) ) from RELSET_1:sch_1();
take  P ; ::_thesis: for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in P iff a # d = b # c )
let a, b, c, d be Element of the carrier of ADG; ::_thesis: ( [[a,b],[c,d]] in P iff a # d = b # c )
A2: ( [[a,b],[c,d]] in P implies a # d = b # c )
proof
assume  [[a,b],[c,d]] in P ; ::_thesis: a # d = b # c
then consider a9, b9, c9, d9 being Element of the carrier of ADG such that
A3: [a,b] = [a9,b9] and
A4: [c,d] = [c9,d9] and
A5: a9 # d9 = b9 # c9 by A1;
A6: c = c9 by A4, XTUPLE_0:1;
 ( a = a9 & b = b9 ) by A3, XTUPLE_0:1;
hence  a # d = b # c by A4, A5, A6, XTUPLE_0:1; ::_thesis: verum
end;
 ( [a,b] in [: the carrier of ADG, the carrier of ADG:] & [c,d] in [: the carrier of ADG, the carrier of ADG:] ) by ZFMISC_1:def_2;
hence  ( [[a,b],[c,d]] in P iff a # d = b # c ) by A1, A2; ::_thesis: verum
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
set X = the carrier of ADG;
set XX = [: the carrier of ADG, the carrier of ADG:];
let P, Q be Relation of [: the carrier of ADG, the carrier of ADG:]; ::_thesis: ( ( for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in P iff a # d = b # c ) ) & ( for a, b, c, d being Element of ADG holds
( [[a,b],[c,d]] in Q iff a # d = b # c ) ) implies P = Q )
assume that
A7: for a, b, c, d being Element of the carrier of ADG holds
( [[a,b],[c,d]] in P iff a # d = b # c ) and
A8: for a, b, c, d being Element of the carrier of ADG holds
( [[a,b],[c,d]] in Q iff a # d = b # c ) ; ::_thesis: P = Q
 for x, y being set holds
( [x,y] in P iff [x,y] in Q )
proof
let x, y be set ; ::_thesis: ( [x,y] in P iff [x,y] in Q )
A9: now__::_thesis:_(_[x,y]_in_Q_implies_[x,y]_in_P_)
assume A10: [x,y] in Q ; ::_thesis: [x,y] in P
then  x in [: the carrier of ADG, the carrier of ADG:] by ZFMISC_1:87;
then consider a, b being Element of ADG such that
A11: x = [a,b] by DOMAIN_1:1;
 y in [: the carrier of ADG, the carrier of ADG:] by A10, ZFMISC_1:87;
then consider c, d being Element of ADG such that
A12: y = [c,d] by DOMAIN_1:1;
 ( [x,y] in Q iff a # d = b # c ) by A8, A11, A12;
hence  [x,y] in P by A7, A10, A11, A12; ::_thesis: verum
end;
now__::_thesis:_(_[x,y]_in_P_implies_[x,y]_in_Q_)
assume A13: [x,y] in P ; ::_thesis: [x,y] in Q
then  x in [: the carrier of ADG, the carrier of ADG:] by ZFMISC_1:87;
then consider a, b being Element of ADG such that
A14: x = [a,b] by DOMAIN_1:1;
 y in [: the carrier of ADG, the carrier of ADG:] by A13, ZFMISC_1:87;
then consider c, d being Element of ADG such that
A15: y = [c,d] by DOMAIN_1:1;
 ( [x,y] in P iff a # d = b # c ) by A7, A14, A15;
hence  [x,y] in Q by A8, A13, A14, A15; ::_thesis: verum
end;
hence  ( [x,y] in P iff [x,y] in Q ) by A9; ::_thesis: verum
end;
hence  P = Q by RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines CONGRD TDGROUP:def_2_:_
 for ADG being non empty addLoopStr
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 addLoopStr ;
func AV ADG ->  strict AffinStruct  equals :: TDGROUP:def 3
 AffinStruct(# the carrier of ADG,(CONGRD ADG) #);
coherence
 AffinStruct(# the carrier of ADG,(CONGRD ADG) #) is strict AffinStruct ;
end;

:: deftheorem  defines AV TDGROUP:def_3_:_
 for ADG being non empty addLoopStr holds AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #);

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

theorem :: TDGROUP:4
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;
preda,b ==> c,d means :Def4: :: TDGROUP:def 4
[[a,b],[c,d]] in the CONGR of (AV ADG);
end;

:: deftheorem Def4 defines ==> TDGROUP:def_4_:_
 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 Th5: :: TDGROUP:5
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
let ADG be Uniquely_Two_Divisible_Group; ::_thesis: for a, b, c, d being Element of ADG holds
( a,b ==> c,d iff a # d = b # c )
let a, b, c, d be Element of ADG; ::_thesis: ( a,b ==> c,d iff a # d = b # c )
A1: the CONGR of (AV ADG) = CONGRD ADG ;
A2: now__::_thesis:_(_a,b_==>_c,d_implies_a_#_d_=_b_#_c_)
assume  a,b ==> c,d ; ::_thesis: a # d = b # c
then  [[a,b],[c,d]] in CONGRD ADG by A1, Def4;
hence  a # d = b # c by Def2; ::_thesis: verum
end;
now__::_thesis:_(_a_#_d_=_b_#_c_implies_a,b_==>_c,d_)
assume  a # d = b # c ; ::_thesis: a,b ==> c,d
then  [[a,b],[c,d]] in the CONGR of (AV ADG) by Def2;
hence  a,b ==> c,d by Def4; ::_thesis: verum
end;
hence  ( a,b ==> c,d iff a # d = b # c ) by A2; ::_thesis: verum
end;

theorem Th6: :: TDGROUP:6
ex a, b being Element of G_Real st a <> b
proof
 0 <> 1 ;
hence  ex a, b being Element of G_Real st a <> b ; ::_thesis: verum
end;

theorem :: TDGROUP:7
ex ADG being Uniquely_Two_Divisible_Group ex a, b being Element of ADG st a <> b by Th6;

theorem Th8: :: TDGROUP:8
for ADG being Uniquely_Two_Divisible_Group
for a, b, c being Element of ADG st a,b ==> c,c holds
a = b
proof
let ADG be Uniquely_Two_Divisible_Group; ::_thesis: for a, b, c being Element of ADG st a,b ==> c,c holds
a = b
let a, b, c be Element of ADG; ::_thesis: ( a,b ==> c,c implies a = b )
assume  a,b ==> c,c ; ::_thesis: a = b
then  a # c = b # c by Th5;
hence  a = b by RLVECT_1:8; ::_thesis: verum
end;

theorem Th9: :: TDGROUP:9
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
let ADG be Uniquely_Two_Divisible_Group; ::_thesis: 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
let a, b, p, q, c, d be Element of ADG; ::_thesis: ( a,b ==> p,q & c,d ==> p,q implies a,b ==> c,d )
assume that
A1: a,b ==> p,q and
A2: c,d ==> p,q ; ::_thesis: a,b ==> c,d
 a # q = b # p by A1, Th5;
then a + (q + d) = (b + p) + d by RLVECT_1:def_3
.= b + (p + d) by RLVECT_1:def_3
.= b + (c + q) by A2, Th5 ;
then (a + d) + q = b + (c + q) by RLVECT_1:def_3
.= (b + c) + q by RLVECT_1:def_3 ;
then  a + d = b + c by RLVECT_1:8;
hence  a,b ==> c,d by Th5; ::_thesis: verum
end;

theorem Th10: :: TDGROUP:10
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
let ADG be Uniquely_Two_Divisible_Group; ::_thesis: for a, b, c being Element of ADG ex d being Element of ADG st a,b ==> c,d
let a, b, c be Element of ADG; ::_thesis: ex d being Element of ADG st a,b ==> c,d
set d9 = (- a) + (b + c);
take  (- a) + (b + c) ; ::_thesis: a,b ==> c,(- a) + (b + c)
a + ((- a) + (b + c)) = (a + (- a)) + (b + c) by RLVECT_1:def_3
.= (0. ADG) + (b + c) by RLVECT_1:5
.= b + c by RLVECT_1:4 ;
hence  a,b ==> c,(- a) + (b + c) by Th5; ::_thesis: verum
end;

theorem Th11: :: TDGROUP:11
for ADG being Uniquely_Two_Divisible_Group
for a, b, a9, b9, c, c9 being Element of ADG st a,b ==> a9,b9 & a,c ==> a9,c9 holds
b,c ==> b9,c9
proof
let ADG be Uniquely_Two_Divisible_Group; ::_thesis: for a, b, a9, b9, c, c9 being Element of ADG st a,b ==> a9,b9 & a,c ==> a9,c9 holds
b,c ==> b9,c9
let a, b, a9, b9, c, c9 be Element of ADG; ::_thesis: ( a,b ==> a9,b9 & a,c ==> a9,c9 implies b,c ==> b9,c9 )
assume  ( a,b ==> a9,b9 & a,c ==> a9,c9 ) ; ::_thesis: b,c ==> b9,c9
then  ( a + b9 = b + a9 & a + c9 = c + a9 ) by Th5;
then b + (a9 + (a + c9)) = (c + a9) + (a + b9) by RLVECT_1:def_3
.= c + (a9 + (a + b9)) by RLVECT_1:def_3 ;
then b + ((a9 + a) + c9) = c + (a9 + (a + b9)) by RLVECT_1:def_3
.= c + ((a9 + a) + b9) by RLVECT_1:def_3 ;
then (b + c9) + (a9 + a) = c + (b9 + (a9 + a)) by RLVECT_1:def_3
.= (c + b9) + (a9 + a) by RLVECT_1:def_3 ;
then  b + c9 = c + b9 by RLVECT_1:8;
hence  b,c ==> b9,c9 by Th5; ::_thesis: verum
end;

theorem Th12: :: TDGROUP:12
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
let ADG be Uniquely_Two_Divisible_Group; ::_thesis: for a, c being Element of ADG ex b being Element of ADG st a,b ==> b,c
let a, c be Element of ADG; ::_thesis: ex b being Element of ADG st a,b ==> b,c
consider b being Element of ADG such that
A1: b + b = a + c by Def1;
take  b ; ::_thesis: a,b ==> b,c
thus  a,b ==> b,c by A1, Th5; ::_thesis: verum
end;

theorem Th13: :: TDGROUP:13
for ADG being Uniquely_Two_Divisible_Group
for a, b, c, b9 being Element of ADG st a,b ==> b,c & a,b9 ==> b9,c holds
b = b9
proof
let ADG be Uniquely_Two_Divisible_Group; ::_thesis: for a, b, c, b9 being Element of ADG st a,b ==> b,c & a,b9 ==> b9,c holds
b = b9
let a, b, c, b9 be Element of ADG; ::_thesis: ( a,b ==> b,c & a,b9 ==> b9,c implies b = b9 )
assume  ( a,b ==> b,c & a,b9 ==> b9,c ) ; ::_thesis: b = b9
then  ( a + c = b + b & a + c = b9 + b9 ) by Th5;
then (b + (- b9)) + b = (b9 + b9) + (- b9) by RLVECT_1:def_3
.= b9 + (b9 + (- b9)) by RLVECT_1:def_3
.= b9 + (0. ADG) by RLVECT_1:5
.= b9 by RLVECT_1:4 ;
then A1: (b + (- b9)) + (b + (- b9)) = b9 + (- b9) by RLVECT_1:def_3
.= 0. ADG by RLVECT_1:5 ;
b9 = (0. ADG) + b9 by RLVECT_1:4
.= (b + (- b9)) + b9 by A1, VECTSP_1:def_18
.= b + ((- b9) + b9) by RLVECT_1:def_3
.= b + (0. ADG) by RLVECT_1:5
.= b by RLVECT_1:4 ;
hence  b = b9 ; ::_thesis: verum
end;

theorem Th14: :: TDGROUP:14
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
let ADG be Uniquely_Two_Divisible_Group; ::_thesis: for a, b, c, d being Element of ADG st a,b ==> c,d holds
a,c ==> b,d
let a, b, c, d be Element of ADG; ::_thesis: ( a,b ==> c,d implies a,c ==> b,d )
assume  a,b ==> c,d ; ::_thesis: a,c ==> b,d
then  a + d = b + c by Th5;
hence  a,c ==> b,d by Th5; ::_thesis: verum
end;

theorem Th15: :: TDGROUP:15
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, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
proof
let ADG be Uniquely_Two_Divisible_Group; ::_thesis: ( ex a, b being Element of ADG st a <> b implies ( 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, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) ) )
set A = AV ADG;
assume  ex a, b being Element of ADG st a <> b ; ::_thesis: ( 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, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
hence  ex a, b being Element of (AV ADG) st a <> b ; ::_thesis: ( ( 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, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
A1: AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #) ;
A2: for a9, b9, c9, d9 being Element of (AV ADG)
for a, b, c, d being Element of ADG st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b ==> c,d iff a9,b9 // c9,d9 )
proof
let a9, b9, c9, d9 be Element of (AV ADG); ::_thesis: for a, b, c, d being Element of ADG st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b ==> c,d iff a9,b9 // c9,d9 )
let a, b, c, d be Element of ADG; ::_thesis: ( a = a9 & b = b9 & c = c9 & d = d9 implies ( a,b ==> c,d iff a9,b9 // c9,d9 ) )
assume A3: ( a = a9 & b = b9 & c = c9 & d = d9 ) ; ::_thesis: ( a,b ==> c,d iff a9,b9 // c9,d9 )
A4: now__::_thesis:_(_a9,b9_//_c9,d9_implies_a,b_==>_c,d_)
assume  a9,b9 // c9,d9 ; ::_thesis: a,b ==> c,d
then  [[a,b],[c,d]] in CONGRD ADG by A3, ANALOAF:def_2;
hence  a,b ==> c,d by A1, Def4; ::_thesis: verum
end;
now__::_thesis:_(_a,b_==>_c,d_implies_a9,b9_//_c9,d9_)
assume  a,b ==> c,d ; ::_thesis: a9,b9 // c9,d9
then  [[a,b],[c,d]] in CONGRD ADG by A1, Def4;
hence  a9,b9 // c9,d9 by A3, ANALOAF:def_2; ::_thesis: verum
end;
hence  ( a,b ==> c,d iff a9,b9 // c9,d9 ) by A4; ::_thesis: verum
end;
thus  for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b ::_thesis: ( ( 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, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
proof
let a, b, c be Element of (AV ADG); ::_thesis: ( a,b // c,c implies a = b )
assume A5: a,b // c,c ; ::_thesis: a = b
reconsider a9 = a, b9 = b, c9 = c as Element of ADG ;
 a9,b9 ==> c9,c9 by A2, A5;
hence  a = b by Th8; ::_thesis: verum
end;
thus  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 ::_thesis: ( ( 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, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
proof
let a, b, c, d, p, q be Element of (AV ADG); ::_thesis: ( a,b // p,q & c,d // p,q implies a,b // c,d )
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p, q9 = q as Element of ADG ;
assume  ( a,b // p,q & c,d // p,q ) ; ::_thesis: a,b // c,d
then  ( a9,b9 ==> p9,q9 & c9,d9 ==> p9,q9 ) by A2;
then  a9,b9 ==> c9,d9 by Th9;
hence  a,b // c,d by A2; ::_thesis: verum
end;
thus  for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d ::_thesis: ( ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
proof
let a, b, c be Element of (AV ADG); ::_thesis: ex d being Element of (AV ADG) st a,b // c,d
reconsider a9 = a, b9 = b, c9 = c as Element of ADG ;
consider d9 being Element of ADG such that
A6: a9,b9 ==> c9,d9 by Th10;
reconsider d = d9 as Element of (AV ADG) ;
take  d ; ::_thesis: a,b // c,d
thus  a,b // c,d by A2, A6; ::_thesis: verum
end;
thus  for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ::_thesis: ( ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
proof
let a, b, c, a9, b9, c9 be Element of (AV ADG); ::_thesis: ( a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
reconsider p = a, q = b, r = c, p9 = a9, q9 = b9, r9 = c9 as Element of ADG ;
assume  ( a,b // a9,b9 & a,c // a9,c9 ) ; ::_thesis: b,c // b9,c9
then  ( p,q ==> p9,q9 & p,r ==> p9,r9 ) by A2;
then  q,r ==> q9,r9 by Th11;
hence  b,c // b9,c9 by A2; ::_thesis: verum
end;
thus  for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ::_thesis: ( ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
proof
let a, c be Element of (AV ADG); ::_thesis: ex b being Element of (AV ADG) st a,b // b,c
reconsider a9 = a, c9 = c as Element of ADG ;
consider b9 being Element of ADG such that
A7: a9,b9 ==> b9,c9 by Th12;
reconsider b = b9 as Element of (AV ADG) ;
take  b ; ::_thesis: a,b // b,c
thus  a,b // b,c by A2, A7; ::_thesis: verum
end;
thus  for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ::_thesis: for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d
proof
let a, b, c, b9 be Element of (AV ADG); ::_thesis: ( a,b // b,c & a,b9 // b9,c implies b = b9 )
reconsider a9 = a, p = b, c9 = c, p9 = b9 as Element of ADG ;
assume  ( a,b // b,c & a,b9 // b9,c ) ; ::_thesis: b = b9
then  ( a9,p ==> p,c9 & a9,p9 ==> p9,c9 ) by A2;
hence  b = b9 by Th13; ::_thesis: verum
end;
thus  for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ::_thesis: verum
proof
let a, b, c, d be Element of (AV ADG); ::_thesis: ( a,b // c,d implies a,c // b,d )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of ADG ;
assume  a,b // c,d ; ::_thesis: a,c // b,d
then  a9,b9 ==> c9,d9 by A2;
then  a9,c9 ==> b9,d9 by Th14;
hence  a,c // b,d by A2; ::_thesis: verum
end;
end;

definition
let IT be non empty AffinStruct ;
attrIT is AffVect-like  means :Def5: :: TDGROUP:def 5
( ( 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, a9, b9, c9 being Element of IT st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, b, c, b9 being Element of IT st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of IT st a,b // c,d holds
a,c // b,d ) );
end;

:: deftheorem Def5 defines AffVect-like TDGROUP:def_5_:_
 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, a9, b9, c9 being Element of IT st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, b, c, b9 being Element of IT st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( 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 for AffinStruct ;
existence
 ex b1 being non trivial AffinStruct st
( b1 is strict & b1 is AffVect-like )
proof
consider ADG being Uniquely_Two_Divisible_Group such that
A1: ex a, b being Element of ADG st a <> b by Th6;
A2: ( ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) ) by A1, Th15;
A3: ( ( for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) ) by Th15;
A4: for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d by A1, Th15;
 ( ( 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 ) ) by A1, Th15;
then  ( not AV ADG is trivial & AV ADG is AffVect-like ) by A1, A2, A3, A4, Def5, STRUCT_0:def_10;
hence  ex b1 being non trivial AffinStruct st
( b1 is strict & b1 is AffVect-like ) ; ::_thesis: verum
end;
end;

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

theorem :: TDGROUP:16
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, a9, b9, c9 being Element of AS st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of AS ex b being Element of AS st a,b // b,c ) & ( for a, b, c, b9 being Element of AS st a,b // b,c & a,b9 // b9,c holds
b = b9 ) & ( for a, b, c, d being Element of AS st a,b // c,d holds
a,c // b,d ) ) iff AS is AffVect ) by Def5, STRUCT_0:def_10;

theorem :: TDGROUP:17
for ADG being Uniquely_Two_Divisible_Group st ex a, b being Element of ADG st a <> b holds
AV ADG is AffVect
proof
let ADG be Uniquely_Two_Divisible_Group; ::_thesis: ( ex a, b being Element of ADG st a <> b implies AV ADG is AffVect )
A1: ( ( for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b ) & ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c & a,b9 // b9,c holds
b = b9 ) ) by Th15;
assume A2: ex a, b being Element of ADG st a <> b ; ::_thesis: AV ADG is AffVect
then A3: ( ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 ) & ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) ) by Th15;
A4: for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d by A2, Th15;
 ( ( 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 ) ) by A2, Th15;
hence  AV ADG is AffVect by A2, A3, A1, A4, Def5, STRUCT_0:def_10; ::_thesis: verum
end;