Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

A Construction of an Abstract Space of Congruence of Vectors

by
Grzegorz Lewandowski, and
Krzysztof Prazmowski

MML identifier: TDGROUP
[ Mizar article, MML identifier index ]

environ

vocabulary RLVECT_1, VECTSP_1, FUNCT_1, ARYTM_1, RELAT_1, ANALOAF, REALSET1,
TDGROUP, ARYTM_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, REAL_1, STRUCT_0,
ANALOAF, FUNCT_1, RELSET_1, BINOP_1, RLVECT_1, VECTSP_1, REALSET1;
constructors DOMAIN_1, ANALOAF, BINOP_1, REAL_1, MEMBERED, XBOOLE_0;
clusters ANALOAF, VECTSP_1, RELSET_1, STRUCT_0, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin

canceled;

theorem :: TDGROUP:2
for a being Element of G_Real holds
ex b being Element of G_Real st b + b = a;

theorem :: TDGROUP:3
for a being Element of G_Real st a + a = 0.G_Real holds
a = 0.G_Real;

definition let IT be non empty LoopStr;
attr IT is Two_Divisible means
:: TDGROUP:def 1
for a being Element of IT holds
ex b being Element of IT st b + b = a;
end;

definition
cluster G_Real -> Fanoian Two_Divisible;
end;

definition
right_zeroed right_complementable Abelian (non empty LoopStr);
end;

definition
mode Two_Divisible_Group is Two_Divisible add-associative right_zeroed
right_complementable Abelian (non empty LoopStr);
end;

definition
mode Uniquely_Two_Divisible_Group is Fanoian Two_Divisible add-associative
right_zeroed right_complementable Abelian (non empty LoopStr);
end;

canceled 3;

theorem :: TDGROUP:7
right_zeroed right_complementable Abelian (non empty LoopStr) holds
(AG is Uniquely_Two_Divisible_Group iff
(for a being Element of AG holds
(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));

reserve a,b,c,d,a',b',c',p,q for Element of ADG;
reserve x,y for set;

definition let ADG be non empty LoopStr;
let a,b be Element of ADG;
redefine func a+b;
synonym a # b;
end;

definition let ADG be non empty LoopStr;
canceled 2;

means
:: TDGROUP:def 4
for a,b,c,d being Element of ADG
holds [[a,b],[c,d]] in it iff a # d = b # c;
end;

definition let ADG be non empty LoopStr;
func AV(ADG) -> strict AffinStruct equals
:: TDGROUP:def 5
end;

definition let ADG be non empty LoopStr;
cluster AV ADG -> non empty;
end;

canceled;

theorem :: TDGROUP:9

pred a,b ==> c,d means
:: TDGROUP:def 6
[[a,b],[c,d]] in the CONGR of AV(ADG);
end;

theorem :: TDGROUP:10
a,b ==> c,d iff a # d = b # c;

theorem :: TDGROUP:11
ex a,b being Element of G_Real st a<>b;

theorem :: TDGROUP:12
ex ADG st ex a,b st a<>b;

theorem :: TDGROUP:13
a,b ==> c,c implies a=b;

theorem :: TDGROUP:14
a,b ==> p,q & c,d ==> p,q implies a,b ==> c,d;

theorem :: TDGROUP:15
ex d st (a,b ==> c,d);

theorem :: TDGROUP:16
a,b ==> a',b' & a,c ==> a',c' implies b,c ==> b',c';

theorem :: TDGROUP:17
ex b st (a,b ==> b,c);

theorem :: TDGROUP:18
a,b ==> b,c & a,b' ==> b',c implies b=b';

theorem :: TDGROUP:19
a,b ==> c,d implies a,c ==> b,d;

reserve AS for non empty AffinStruct;

theorem :: TDGROUP:20
(ex a,b being Element of ADG st a<>b) implies
( (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
:: 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;

definition
cluster strict non trivial AffVect-like (non empty AffinStruct);
end;

definition
mode AffVect is non trivial AffVect-like (non empty AffinStruct);
end;

theorem :: TDGROUP:21
for AS 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;

theorem :: TDGROUP:22
(ex a,b being Element of ADG st a<>b)