:: A Construction of an Abstract Space of Congruence of Vectors
:: by Grzegorz Lewandowski and Krzysztof Pra\.zmowski
::
:: Received May 23, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: TDGROUP:1
for a being Element of G_Real ex b being Element of G_Real st b + b = a
proofend;

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
proofend;

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

theorem Th6: :: TDGROUP:6
ex a, b being Element of G_Real st a <> b
proofend;

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
proofend;

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 &amp; c,d ==> p,q holds
a,b ==> c,d
proofend;

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
proofend;

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 &amp; a,c ==> a9,c9 holds
b,c ==> b9,c9
proofend;

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
proofend;

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 &amp; a,b9 ==> b9,c holds
b = b9
proofend;

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
proofend;

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 &amp; ( for a, b, c being Element of (AV ADG) st a,b // c,c holds
a = b ) &amp; ( for a, b, c, d, p, q being Element of (AV ADG) st a,b // p,q &amp; c,d // p,q holds
a,b // c,d ) &amp; ( for a, b, c being Element of (AV ADG) ex d being Element of (AV ADG) st a,b // c,d ) &amp; ( for a, b, c, a9, b9, c9 being Element of (AV ADG) st a,b // a9,b9 &amp; a,c // a9,c9 holds
b,c // b9,c9 ) &amp; ( for a, c being Element of (AV ADG) ex b being Element of (AV ADG) st a,b // b,c ) &amp; ( for a, b, c, b9 being Element of (AV ADG) st a,b // b,c &amp; a,b9 // b9,c holds
b = b9 ) &amp; ( for a, b, c, d being Element of (AV ADG) st a,b // c,d holds
a,c // b,d ) )
proofend;

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 ) &amp; ( for a, b, c, d, p, q being Element of IT st a,b // p,q &amp; c,d // p,q holds
a,b // c,d ) &amp; ( for a, b, c being Element of IT ex d being Element of IT st a,b // c,d ) &amp; ( for a, b, c, a9, b9, c9 being Element of IT st a,b // a9,b9 &amp; a,c // a9,c9 holds
b,c // b9,c9 ) &amp; ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) &amp; ( for a, b, c, b9 being Element of IT st a,b // b,c &amp; a,b9 // b9,c holds
b = b9 ) &amp; ( 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 ) &amp; ( for a, b, c, d, p, q being Element of IT st a,b // p,q &amp; c,d // p,q holds
a,b // c,d ) &amp; ( for a, b, c being Element of IT ex d being Element of IT st a,b // c,d ) &amp; ( for a, b, c, a9, b9, c9 being Element of IT st a,b // a9,b9 &amp; a,c // a9,c9 holds
b,c // b9,c9 ) &amp; ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) &amp; ( for a, b, c, b9 being Element of IT st a,b // b,c &amp; a,b9 // b9,c holds
b = b9 ) &amp; ( 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 &amp; b1 is AffVect-like )
proofend;
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 &amp; ( for a, b, c being Element of AS st a,b // c,c holds
a = b ) &amp; ( for a, b, c, d, p, q being Element of AS st a,b // p,q &amp; c,d // p,q holds
a,b // c,d ) &amp; ( for a, b, c being Element of AS ex d being Element of AS st a,b // c,d ) &amp; ( for a, b, c, a9, b9, c9 being Element of AS st a,b // a9,b9 &amp; a,c // a9,c9 holds
b,c // b9,c9 ) &amp; ( for a, c being Element of AS ex b being Element of AS st a,b // b,c ) &amp; ( for a, b, c, b9 being Element of AS st a,b // b,c &amp; a,b9 // b9,c holds
b = b9 ) &amp; ( 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
proofend;