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
means :
Def4:
for
a,
b,
c,
d being
Element of holds
(
[[a,b],[c,d]] in it iff
a # d = b # c );
existence
ex b1 being Relation of st
for a, b, c, d being Element of holds
( [[a,b],[c,d]] in b1 iff a # d = b # c )
uniqueness
for b1, b2 being Relation of st ( for a, b, c, d being Element of holds
( [[a,b],[c,d]] in b1 iff a # d = b # c ) ) & ( for a, b, c, d being Element of 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 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,
a',
b',
c,
c' being
Element of st
a,
b ==> a',
b' &
a,
c ==> a',
c' holds
b,
c ==> b',
c'
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
for
ADG being
Uniquely_Two_Divisible_Group st ex
a,
b being
Element of st
a <> b holds
( ex
a,
b being
Element of st
a <> b & ( for
a,
b,
c being
Element of st
a,
b // c,
c holds
a = b ) & ( for
a,
b,
c,
d,
p,
q being
Element of st
a,
b // p,
q &
c,
d // p,
q holds
a,
b // c,
d ) & ( for
a,
b,
c being
Element of ex
d being
Element of st
a,
b // c,
d ) & ( for
a,
b,
c,
a',
b',
c' being
Element of st
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
c being
Element of ex
b being
Element of st
a,
b // b,
c ) & ( for
a,
b,
c,
b' being
Element of st
a,
b // b,
c &
a,
b' // b',
c holds
b = b' ) & ( for
a,
b,
c,
d being
Element of 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 st
a,
b // c,
c holds
a = b ) & ( for
a,
b,
c,
d,
p,
q being
Element of st
a,
b // p,
q &
c,
d // p,
q holds
a,
b // c,
d ) & ( for
a,
b,
c being
Element of ex
d being
Element of st
a,
b // c,
d ) & ( for
a,
b,
c,
a',
b',
c' being
Element of st
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
c being
Element of ex
b being
Element of st
a,
b // b,
c ) & ( for
a,
b,
c,
b' being
Element of st
a,
b // b,
c &
a,
b' // b',
c holds
b = b' ) & ( for
a,
b,
c,
d being
Element of 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 st
a,
b // c,
c holds
a = b ) & ( for
a,
b,
c,
d,
p,
q being
Element of st
a,
b // p,
q &
c,
d // p,
q holds
a,
b // c,
d ) & ( for
a,
b,
c being
Element of ex
d being
Element of st
a,
b // c,
d ) & ( for
a,
b,
c,
a',
b',
c' being
Element of st
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
c being
Element of ex
b being
Element of st
a,
b // b,
c ) & ( for
a,
b,
c,
b' being
Element of st
a,
b // b,
c &
a,
b' // b',
c holds
b = b' ) & ( for
a,
b,
c,
d being
Element of st
a,
b // c,
d holds
a,
c // b,
d ) ) );
theorem
for
AS being non
empty AffinStruct holds
( ( ex
a,
b being
Element of st
a <> b & ( for
a,
b,
c being
Element of st
a,
b // c,
c holds
a = b ) & ( for
a,
b,
c,
d,
p,
q being
Element of st
a,
b // p,
q &
c,
d // p,
q holds
a,
b // c,
d ) & ( for
a,
b,
c being
Element of ex
d being
Element of st
a,
b // c,
d ) & ( for
a,
b,
c,
a',
b',
c' being
Element of st
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
c being
Element of ex
b being
Element of st
a,
b // b,
c ) & ( for
a,
b,
c,
b' being
Element of st
a,
b // b,
c &
a,
b' // b',
c holds
b = b' ) & ( for
a,
b,
c,
d being
Element of st
a,
b // c,
d holds
a,
c // b,
d ) ) iff
AS is
AffVect )
by Def8, STRUCT_0:def 10;
theorem