begin
Lm1:
G_Real is Fanoian
definition
let ADG be non
empty addLoopStr ;
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;
theorem Th9:
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 Th11:
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 Th15:
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 ;
attr IT is
AffVect-like means :
Def5:
( ( 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 ) ) );
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 Def5, STRUCT_0:def 10;