:: by Grzegorz Lewandowski and Krzysztof Pra\.zmowski

::

:: Received May 23, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let IT be non empty addLoopStr ;

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

for a being Element of IT ex b being Element of IT st b + b = a;

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

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

registration

ex b_{1} being non empty addLoopStr st

( b_{1} is strict & b_{1} is Fanoian & b_{1} is Two_Divisible & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is Abelian )
by Lm1;

end;

cluster non empty strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible for addLoopStr ;

existence ex b

( b

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;

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

definition

let ADG be non empty addLoopStr ;

ex b_{1} 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 b_{1} iff a # d = b # c )

for b_{1}, b_{2} 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 b_{1} iff a # d = b # c ) ) & ( for a, b, c, d being Element of ADG holds

( [[a,b],[c,d]] in b_{2} iff a # d = b # c ) ) holds

b_{1} = b_{2}

end;
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 for a, b, c, d being Element of ADG holds

( [[a,b],[c,d]] in it iff a # d = b # c );

ex b

for a, b, c, d being Element of ADG holds

( [[a,b],[c,d]] in b

proof end;

uniqueness for b

( [[a,b],[c,d]] in b

( [[a,b],[c,d]] in b

b

proof end;

:: deftheorem Def2 defines CONGRD TDGROUP:def 2 :

for ADG being non empty addLoopStr

for b_{2} being Relation of [: the carrier of ADG, the carrier of ADG:] holds

( b_{2} = CONGRD ADG iff for a, b, c, d being Element of ADG holds

( [[a,b],[c,d]] in b_{2} iff a # d = b # c ) );

for ADG being non empty addLoopStr

for b

( b

( [[a,b],[c,d]] in b

definition

let ADG be non empty addLoopStr ;

AffinStruct(# the carrier of ADG,(CONGRD ADG) #) is strict AffinStruct ;

end;
func AV ADG -> strict AffinStruct equals :: TDGROUP:def 3

AffinStruct(# the carrier of ADG,(CONGRD ADG) #);

coherence AffinStruct(# the carrier of ADG,(CONGRD ADG) #);

AffinStruct(# the carrier of ADG,(CONGRD ADG) #) is strict AffinStruct ;

:: deftheorem defines AV TDGROUP:def 3 :

for ADG being non empty addLoopStr holds AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #);

for ADG being non empty addLoopStr holds AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #);

theorem :: TDGROUP:4

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

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 )

for a, b, c, d being Element of ADG holds

( a,b ==> c,d iff a # d = b # c )

proof end;

theorem :: TDGROUP:7

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

for a, b, c being Element of ADG st a,b ==> c,c holds

a = b

proof 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

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

for a, b, c being Element of ADG ex d being Element of ADG st a,b ==> c,d

proof 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

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

for a, c being Element of ADG ex b being Element of ADG st a,b ==> b,c

proof 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

for a, b, c, b9 being Element of ADG st a,b ==> b,c & a,b9 ==> b9,c holds

b = b9

proof 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

for a, b, c, d being Element of ADG st a,b ==> c,d holds

a,c ==> b,d

proof 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 ) )

( 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 end;

definition

let IT be non empty AffinStruct ;

end;
attr IT 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 ) );

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

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

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

existence

ex b_{1} being non trivial AffinStruct st

( b_{1} is strict & b_{1} is AffVect-like )

end;
ex b

( b

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

( ( 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

AV ADG is AffVect

proof end;