:: A Construction of an Abstract Space of Congruence of Vectors
:: by Grzegorz Lewandowski and Krzysztof Pra\.zmowski
::
:: Received May 23, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: TDGROUP:1
canceled;
theorem Th2: :: TDGROUP:2
theorem :: TDGROUP:3
:: deftheorem Def1 defines Two_Divisible TDGROUP:def 1 :
Lm1:
G_Real is Fanoian
theorem :: TDGROUP:4
canceled;
theorem :: TDGROUP:5
canceled;
theorem :: TDGROUP:6
canceled;
theorem :: TDGROUP:7
definition
let ADG be non
empty addLoopStr ;
canceled;canceled;func CONGRD ADG -> Relation of
[:the carrier of ADG,the carrier of ADG:] means :
Def4:
:: TDGROUP:def 4
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 :: TDGROUP:8
canceled;
theorem :: TDGROUP:9
:: deftheorem Def6 defines ==> TDGROUP:def 6 :
theorem Th10: :: TDGROUP:10
theorem Th11: :: TDGROUP:11
theorem :: TDGROUP:12
theorem Th13: :: TDGROUP:13
theorem Th14: :: TDGROUP:14
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: :: TDGROUP:15
theorem Th16: :: TDGROUP:16
for
ADG being
Uniquely_Two_Divisible_Group for
a,
b,
a',
b',
c,
c' being
Element of
ADG st
a,
b ==> a',
b' &
a,
c ==> a',
c' holds
b,
c ==> b',
c'
theorem Th17: :: TDGROUP:17
theorem Th18: :: TDGROUP:18
theorem Th19: :: TDGROUP:19
theorem Th20: :: TDGROUP:20
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,
a',
b',
c' being
Element of
(AV ADG) st
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
c being
Element of
(AV ADG) ex
b being
Element of
(AV ADG) st
a,
b // b,
c ) & ( for
a,
b,
c,
b' being
Element of
(AV ADG) st
a,
b // b,
c &
a,
b' // b',
c holds
b = b' ) & ( 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:
:: TDGROUP:def 8
( ( 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,
a',
b',
c' being
Element of
IT st
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
c being
Element of
IT ex
b being
Element of
IT st
a,
b // b,
c ) & ( for
a,
b,
c,
b' being
Element of
IT st
a,
b // b,
c &
a,
b' // b',
c holds
b = b' ) & ( 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,
a',
b',
c' being
Element of
IT st
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
c being
Element of
IT ex
b being
Element of
IT st
a,
b // b,
c ) & ( for
a,
b,
c,
b' being
Element of
IT st
a,
b // b,
c &
a,
b' // b',
c holds
b = b' ) & ( for
a,
b,
c,
d being
Element of
IT st
a,
b // c,
d holds
a,
c // b,
d ) ) );
theorem :: TDGROUP:21
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,
a',
b',
c' being
Element of
AS st
a,
b // a',
b' &
a,
c // a',
c' holds
b,
c // b',
c' ) & ( for
a,
c being
Element of
AS ex
b being
Element of
AS st
a,
b // b,
c ) & ( for
a,
b,
c,
b' being
Element of
AS st
a,
b // b,
c &
a,
b' // b',
c holds
b = b' ) & ( 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 :: TDGROUP:22