begin
theorem
canceled;
theorem Th2:
theorem
:: deftheorem Def1 defines Two_Divisible TDGROUP:def 1 :
Lm1:
G_Real is Fanoian
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
definition
let ADG be non
empty addLoopStr ;
canceled;canceled;func CONGRD ADG -> Relation of
[:the carrier of ADG,the carrier of ADG:] means :
Def4:
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 )
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
end;
:: deftheorem TDGROUP:def 2 :
canceled;
:: deftheorem TDGROUP:def 3 :
canceled;
:: deftheorem Def4 defines CONGRD TDGROUP:def 4 :
:: deftheorem defines AV TDGROUP:def 5 :
theorem
canceled;
theorem
:: deftheorem Def6 defines ==> TDGROUP:def 6 :
theorem Th10:
theorem Th11:
theorem
theorem Th13:
theorem Th14:
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
theorem Th15:
theorem Th16:
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
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
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 ) )
definition
let IT be non
empty AffinStruct ;
canceled;attr IT is
AffVect-like means :
Def8:
( ( 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 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,
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 ) ) );
theorem
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 Def8, STRUCT_0:def 10;
theorem