:: Directed Geometrical Bundles and Their Analytical Representation
:: by Grzegorz Lewandowski, Krzysztof Pra\.zmowski and Bo\.zena Lewandowska
::
:: Received September 24, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ANALOAF, SUBSET_1, STRUCT_0, ZFMISC_1, TDGROUP, DIRAF,
BINOP_1, FUNCT_1, ALGSTR_0, SUPINF_2, ARYTM_3, RLVECT_1, ARYTM_1,
VECTSP_1, MCART_1, PBOOLE, RELAT_1, TARSKI, AFVECT0;
notations TARSKI, ZFMISC_1, SUBSET_1, STRUCT_0, ALGSTR_0, ANALOAF, TDGROUP,
FUNCT_1, FUNCT_2, XTUPLE_0, MCART_1, BINOP_1, RELAT_1, VECTSP_1,
RLVECT_1;
constructors BINOP_1, DOMAIN_1, TDGROUP, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1, TDGROUP,
RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
begin
definition
let IT be non empty AffinStruct;
attr IT is WeakAffVect-like means
:: AFVECT0:def 1
(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,d being Element of IT st a,b // c,d
holds a,c // b,d;
end;
registration
cluster strict WeakAffVect-like for non trivial AffinStruct;
end;
definition
mode WeakAffVect is WeakAffVect-like non trivial AffinStruct;
end;
registration
cluster AffVect-like -> WeakAffVect-like for non empty AffinStruct;
end;
reserve AFV for WeakAffVect;
reserve a,b,c,d,e,f,a9,b9,c9,d9,f9,p,q,r,o,x99 for Element of AFV;
::
:: Properties of Relation of Congruence of Vectors
::
theorem :: AFVECT0:1
a,b // a,b;
theorem :: AFVECT0:2
a,a // a,a;
theorem :: AFVECT0:3
a,b // c,d implies c,d // a,b;
theorem :: AFVECT0:4
a,b // a,c implies b = c;
theorem :: AFVECT0:5
a,b // c,d & a,b // c,d9 implies d = d9;
theorem :: AFVECT0:6
for a,b holds a,a // b,b;
theorem :: AFVECT0:7
a,b // c,d implies b,a // d,c;
theorem :: AFVECT0:8
a,b // c,d & a,c // b9,d implies b = b9;
theorem :: AFVECT0:9
b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 implies d = d9;
theorem :: AFVECT0:10
a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 implies d = d9;
theorem :: AFVECT0:11
a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 implies a,f
// a9,f9;
theorem :: AFVECT0:12
a,b // a9,b9 & a,c // c9,b9 implies b,c // c9,a9;
::
:: Relation of Maximal Distance
::
definition
let AFV;
let a,b;
pred MDist a,b means
:: AFVECT0:def 2
a,b // b,a & a <> b;
irreflexivity;
symmetry;
end;
theorem :: AFVECT0:13
ex a,b st a<>b & not MDist a,b;
theorem :: AFVECT0:14
MDist a,b & MDist a,c implies b = c or MDist b,c;
theorem :: AFVECT0:15
MDist a,b & a,b // c,d implies MDist c,d;
::
:: Midpoint Relation
::
definition
let AFV;
let a,b,c;
pred Mid a,b,c means
:: AFVECT0:def 3
a,b // b,c;
end;
theorem :: AFVECT0:16
Mid a,b,c implies Mid c,b,a;
theorem :: AFVECT0:17
Mid a,b,b iff a = b;
theorem :: AFVECT0:18
Mid a,b,a iff a = b or MDist a,b;
theorem :: AFVECT0:19
ex b st Mid a,b,c;
theorem :: AFVECT0:20
Mid a,b,c & Mid a,b9,c implies b =b9 or MDist b,b9;
theorem :: AFVECT0:21
ex c st Mid a,b,c;
theorem :: AFVECT0:22
Mid a,b,c & Mid a,b,c9 implies c = c9;
theorem :: AFVECT0:23
Mid a,b,c & MDist b,b9 implies Mid a,b9,c;
theorem :: AFVECT0:24
Mid a,b,c & Mid a,b9,c9 & MDist b,b9 implies c = c9;
theorem :: AFVECT0:25
Mid a,p,a9 & Mid b,p,b9 implies a,b // b9,a9;
theorem :: AFVECT0:26
Mid a,p,a9 & Mid b,q,b9 & MDist p,q implies a,b // b9,a9;
::
:: Point Symmetry
::
definition
let AFV;
let a,b;
func PSym(a,b) -> Element of AFV means
:: AFVECT0:def 4
Mid b,a,it;
end;
theorem :: AFVECT0:27
PSym(p,a) = b iff a,p // p,b;
theorem :: AFVECT0:28
PSym(p,a) = a iff a = p or MDist a,p;
theorem :: AFVECT0:29
PSym(p,PSym(p,a)) = a;
theorem :: AFVECT0:30
PSym(p,a) = PSym(p,b) implies a = b;
theorem :: AFVECT0:31
ex a st PSym(p,a) = b;
theorem :: AFVECT0:32
a,b // PSym(p,b),PSym(p,a);
theorem :: AFVECT0:33
a,b // c,d iff PSym(p,a),PSym(p,b) // PSym(p,c),PSym(p,d);
theorem :: AFVECT0:34
MDist a,b iff MDist PSym(p,a),PSym(p,b);
theorem :: AFVECT0:35
Mid a,b,c iff Mid PSym(p,a),PSym(p,b),PSym(p,c);
theorem :: AFVECT0:36
PSym(p,a) = PSym(q,a) iff p = q or MDist p,q;
theorem :: AFVECT0:37
PSym(q,PSym(p,PSym(q,a))) = PSym(PSym(q,p),a);
theorem :: AFVECT0:38
PSym(p,PSym(q,a)) = PSym(q,PSym(p,a)) iff p = q or MDist p,q or MDist
q,PSym(p,q);
theorem :: AFVECT0:39
PSym(p,PSym(q,PSym(r,a))) = PSym(r,PSym(q,PSym(p,a)));
theorem :: AFVECT0:40
ex d st PSym(a,PSym(b,PSym(c,p))) = PSym(d,p);
theorem :: AFVECT0:41
ex c st PSym(a,PSym(c,p)) = PSym(c,PSym(b,p));
::
:: Addition on the carrier
::
definition
let AFV,o;
let a,b;
func Padd(o,a,b) -> Element of AFV means
:: AFVECT0:def 5
o,a // b,it;
end;
notation
let AFV,o;
let a;
synonym Pcom(o,a) for PSym(o,a);
end;
definition
let AFV,o;
func Padd(o) -> BinOp of the carrier of AFV means
:: AFVECT0:def 6
for a,b holds it.(a ,b) = Padd(o,a,b);
end;
definition
let AFV,o;
func Pcom(o) -> UnOp of the carrier of AFV means
:: AFVECT0:def 7
for a holds it.a = Pcom(o,a);
end;
definition
let AFV,o;
func GroupVect(AFV,o) -> strict addLoopStr equals
:: AFVECT0:def 8
addLoopStr(#the carrier of
AFV,Padd(o),o#);
end;
registration
let AFV,o;
cluster GroupVect(AFV,o) -> non empty;
end;
theorem :: AFVECT0:42
the carrier of GroupVect(AFV,o) = the carrier of AFV & the addF of
GroupVect(AFV,o) = Padd(o) & 0.GroupVect(AFV,o) = o;
reserve a,b,c for Element of GroupVect(AFV,o);
theorem :: AFVECT0:43
for a,b being Element of GroupVect(AFV,o), a9,b9 being Element of AFV
st a=a9 & b=b9 holds a + b = (Padd(o)).(a9,b9);
registration
let AFV,o;
cluster GroupVect(AFV,o) -> Abelian add-associative right_zeroed
right_complementable;
end;
theorem :: AFVECT0:44
for a being Element of GroupVect(AFV,o), a9 being Element of AFV
st a=a9 holds -a = (Pcom(o)).a9;
theorem :: AFVECT0:45
0.GroupVect(AFV,o) = o;
reserve a,b for Element of GroupVect(AFV,o);
theorem :: AFVECT0:46
for a ex b st b + b = a;
registration
let AFV,o;
cluster GroupVect(AFV,o) -> Two_Divisible;
end;
::
:: Representation Theorem for Directed Geometrical Bundles
::
reserve AFV for AffVect,
o for Element of AFV;
theorem :: AFVECT0:47
for a being Element of GroupVect(AFV,o) st a + a = 0.(GroupVect(
AFV,o)) holds a = 0.(GroupVect(AFV,o));
registration
let AFV,o;
cluster GroupVect(AFV,o) -> Fanoian;
end;
registration
cluster strict non trivial for Uniquely_Two_Divisible_Group;
end;
definition
mode Proper_Uniquely_Two_Divisible_Group is non trivial
Uniquely_Two_Divisible_Group;
end;
theorem :: AFVECT0:48
GroupVect(AFV,o) is Proper_Uniquely_Two_Divisible_Group;
registration
let AFV,o;
cluster GroupVect(AFV,o) -> non trivial;
end;
theorem :: AFVECT0:49
for ADG being Proper_Uniquely_Two_Divisible_Group holds AV(ADG) is AffVect;
registration
let ADG be Proper_Uniquely_Two_Divisible_Group;
cluster AV(ADG) -> AffVect-like non trivial;
end;
theorem :: AFVECT0:50
for AFV being strict AffVect holds for o being Element of AFV
holds AFV = AV(GroupVect(AFV,o));
theorem :: AFVECT0:51
for AS being strict AffinStruct holds (AS is AffVect iff ex ADG being
Proper_Uniquely_Two_Divisible_Group st AS = AV(ADG) );
definition
let X,Y be non empty addLoopStr;
let f be Function of the carrier of X,the carrier of Y;
pred f is_Iso_of X,Y means
:: AFVECT0:def 9
f is one-to-one & rng(f) = the carrier of
Y & for a,b being Element of X holds f.(a+b) = (f.a)+(f.b) & f.(0.X) = 0.Y & f.
(-a) = -(f.a);
end;
definition
let X,Y be non empty addLoopStr;
pred X,Y are_Iso means
:: AFVECT0:def 10
ex f being Function of the carrier of X,the carrier of Y st f is_Iso_of X,Y;
end;
reserve ADG for Proper_Uniquely_Two_Divisible_Group;
reserve f for Function of the carrier of ADG,the carrier of ADG;
theorem :: AFVECT0:52
for o9 being Element of ADG, o being Element of AV(ADG) st (for
x being Element of ADG holds f.x = o9+x) & o=o9 holds for a,b being Element of
ADG holds f.(a+b) =(Padd(o)).(f.a,f.b) & f.(0.ADG) = 0.(GroupVect(AV(ADG),o)) &
f.(-a) = (Pcom(o)).(f.a);
theorem :: AFVECT0:53
for o9 being Element of ADG st (for b being Element of ADG holds
f.b = o9+b) holds f is one-to-one;
theorem :: AFVECT0:54
for o9 being Element of ADG, o being Element of AV(ADG) st (for
b being Element of ADG holds f.b = o9+b) holds rng(f) = the carrier of
GroupVect(AV(ADG),o);
theorem :: AFVECT0:55
for ADG being Proper_Uniquely_Two_Divisible_Group, o9 being Element of
ADG, o being Element of AV(ADG) st o=o9 holds ADG,GroupVect(AV(ADG),o) are_Iso;