:: Directed Geometrical Bundles and Their Analytical Representation
:: by Grzegorz Lewandowski, Krzysztof Pra\.zmowski and Bo\.zena Lewandowska
::
:: Received September 24, 1990
:: Copyright (c) 1990-2018 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;
definitions RLVECT_1, ALGSTR_0;
equalities STRUCT_0, BINOP_1, ALGSTR_0;
expansions STRUCT_0;
theorems DOMAIN_1, TDGROUP, FUNCT_1, FUNCT_2, MCART_1, RELAT_1, TARSKI,
RLVECT_1, ANALOAF, XBOOLE_0, VECTSP_1, STRUCT_0;
schemes BINOP_1, FUNCT_2;
begin
definition
let IT be non empty AffinStruct;
attr IT is WeakAffVect-like means
:Def1:
(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;
existence
proof
set AFV = the strict AffVect;
reconsider AS = AFV as non empty AffinStruct;
A1: ( 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 by TDGROUP:16;
A2: ( for a,c being Element of AS ex b being Element of AS st a,b // b,c)&
for a,b,c,d being Element of AS st a,b // c,d holds a,c // b,d by TDGROUP:16;
( 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 by
TDGROUP:16;
then AS is WeakAffVect-like by A1,A2;
hence thesis;
end;
end;
definition
mode WeakAffVect is WeakAffVect-like non trivial AffinStruct;
end;
registration
cluster AffVect-like -> WeakAffVect-like for non empty AffinStruct;
coherence
by TDGROUP:def 5;
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 Th1:
a,b // a,b
proof
ex d st a,b // b,d by Def1;
hence thesis by Def1;
end;
theorem
a,a // a,a by Th1;
theorem Th3:
a,b // c,d implies c,d // a,b
proof
assume
A1: a,b // c,d;
c,d // c,d by Th1;
hence thesis by A1,Def1;
end;
theorem Th4:
a,b // a,c implies b = c
proof
assume a,b // a,c;
then a,a // b,c by Def1;
then b,c // a,a by Th3;
hence thesis by Def1;
end;
theorem Th5:
a,b // c,d & a,b // c,d9 implies d = d9
proof
assume a,b // c,d & a,b // c,d9;
then c,d // a,b & c,d9 // a,b by Th3;
then c,d // c,d9 by Def1;
hence thesis by Th4;
end;
theorem Th6:
for a,b holds a,a // b,b
proof
let a,b;
consider p such that
A1: a,a // b,p by Def1;
b,p // a,a by A1,Th3;
hence thesis by A1,Def1;
end;
theorem Th7:
a,b // c,d implies b,a // d,c
proof
assume
A1: a,b // c,d;
a,a // c,c by Th6;
hence thesis by A1,Def1;
end;
theorem
a,b // c,d & a,c // b9,d implies b = b9
proof
assume that
A1: a,b // c,d and
A2: a,c // b9,d;
a,c // b,d by A1,Def1;
then b,d // a,c by Th3;
then
A3: d,b // c,a by Th7;
b9,d // a,c by A2,Th3;
then d,b9 // c,a by Th7;
then d,b // d,b9 by A3,Def1;
hence thesis by Th4;
end;
theorem
b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 implies d = d9
proof
assume that
A1: b,c // b9,c9 and
A2: a,d // b,c and
A3: a,d9 // b9,c9;
b9,c9 // b,c by A1,Th3;
then a,d // b9,c9 by A2,Def1;
then a,d // a,d9 by A3,Def1;
hence thesis by Th4;
end;
theorem
a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 implies d = d9
proof
assume that
A1: a,b // a9,b9 and
A2: c,d // b,a and
A3: c,d9 // b9,a9;
a9,b9 // a,b by A1,Th3;
then b9,a9 // b,a by Th7;
then c,d // b9,a9 by A2,Def1;
then c,d // c,d9 by A3,Def1;
hence thesis by Th4;
end;
theorem
a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 implies a,f
// a9,f9
proof
assume that
A1: a,b // a9,b9 and
A2: c,d // c9,d9 and
A3: b,f // c,d and
A4: b9,f9 // c9,d9;
b9,f9 // c,d by A2,A4,Def1;
then
A5: b,f // b9,f9 by A3,Def1;
b,a // b9,a9 by A1,Th7;
hence thesis by A5,Def1;
end;
theorem Th12:
a,b // a9,b9 & a,c // c9,b9 implies b,c // c9,a9
proof
assume that
A1: a,b // a9,b9 and
A2: a,c // c9,b9;
consider d such that
A3: c9,b9 // a9,d by Def1;
a9,d // c9,b9 by A3,Th3;
then a,c // a9,d by A2,Def1;
then
A4: b,c // b9,d by A1,Def1;
c9,a9 // b9,d by A3,Def1;
hence thesis by A4,Def1;
end;
::
:: Relation of Maximal Distance
::
definition
let AFV;
let a,b;
pred MDist a,b means
a,b // b,a & a <> b;
irreflexivity;
symmetry by Th3;
end;
theorem
ex a,b st a<>b & not MDist a,b
proof
consider p,q such that
A1: p <> q by STRUCT_0:def 10;
now
consider r such that
A2: p,r // r,q by Def1;
A3: now
A4: now
assume MDist p,r;
then
A5: p,r // r,p;
r,q // p,r by A2,Th3;
then q,r // r,p by Th7;
then p,r // q,r by A5,Def1;
hence thesis by A1,Th4,Th7;
end;
assume p <> r;
hence thesis by A4;
end;
now
assume
A6: p = r;
then r,q // p,p by A2,Th3;
hence thesis by A1,A6,Def1;
end;
hence thesis by A3;
end;
hence thesis;
end;
theorem
MDist a,b & MDist a,c implies b = c or MDist b,c
proof
assume that
A1: MDist a,b and
A2: MDist a,c;
A3: a,b // b,a by A1;
A4: a,c // c,a by A2;
consider d such that
A5: c,a // b,d by Def1;
b,d // c,a by A5,Th3;
then a,c // b,d by A4,Def1;
then
A6: b,c // a,d by A3,Def1;
c,b // a,d by A5,Def1;
then b,c // c,b by A6,Def1;
hence thesis;
end;
theorem
MDist a,b & a,b // c,d implies MDist c,d
proof
assume that
A1: MDist a,b and
A2: a,b // c,d;
A3: a,b // b,a by A1;
A4: c,d // a,b by A2,Th3;
then d,c // b,a by Th7;
then d,c // a,b by A3,Def1;
then c,d // d,c by A4,Def1;
then c <> d implies thesis;
hence thesis by A1,A2,Def1;
end;
::
:: Midpoint Relation
::
definition
let AFV;
let a,b,c;
pred Mid a,b,c means
:Def3:
a,b // b,c;
end;
theorem Th16:
Mid a,b,c implies Mid c,b,a
proof
assume Mid a,b,c;
then a,b // b,c;
then b,a // c,b by Th7;
then c,b // b,a by Th3;
hence thesis;
end;
theorem
Mid a,b,b iff a = b
by Def1,Th6;
theorem Th18:
Mid a,b,a iff a = b or MDist a,b
by Th6;
theorem Th19:
ex b st Mid a,b,c
proof
consider b such that
A1: a,b // b,c by Def1;
Mid a,b,c by A1;
hence thesis;
end;
theorem Th20:
Mid a,b,c & Mid a,b9,c implies b =b9 or MDist b,b9
proof
assume that
A1: Mid a,b,c and
A2: Mid a,b9,c;
A3: a,b // b,c by A1;
consider d such that
A4: b9,c // b,d by Def1;
A5: b,d // b9,c by A4,Th3;
then b,b9 // d,c by Def1;
then
A6: b9,b // c,d by Th7;
a,b9 // b9,c by A2;
then a,b9 // b,d by A5,Def1;
then b,b9 // c,d by A3,Def1;
then b,b9 // b9,b by A6,Def1;
hence thesis;
end;
theorem Th21:
ex c st Mid a,b,c
proof
consider c such that
A1: a,b // b,c by Def1;
Mid a,b,c by A1;
hence thesis;
end;
theorem Th22:
Mid a,b,c & Mid a,b,c9 implies c = c9
proof
assume that
A1: Mid a,b,c and
A2: Mid a,b,c9;
a,b // b,c9 by A2;
then
A3: b,c9 // a,b by Th3;
a,b // b,c by A1;
then b,c // a,b by Th3;
then b,c // b,c9 by A3,Def1;
hence thesis by Th4;
end;
theorem Th23:
Mid a,b,c & MDist b,b9 implies Mid a,b9,c
proof
assume that
A1: Mid a,b,c and
A2: MDist b,b9;
A3: b,b9 // b9,b by A2;
a,b // b,c by A1;
then
A4: b,a // c,b by Th7;
consider d such that
A5: b9,b // c,d by Def1;
c,d // b9,b by A5,Th3;
then b,b9 // c,d by A3,Def1;
then
A6: a,b9 // b,d by A4,Def1;
b9,c // b,d by A5,Def1;
then a,b9 // b9,c by A6,Def1;
hence thesis;
end;
theorem Th24:
Mid a,b,c & Mid a,b9,c9 & MDist b,b9 implies c = c9
proof
assume that
A1: Mid a,b,c and
A2: Mid a,b9,c9 and
A3: MDist b,b9;
Mid a,b9,c by A1,A3,Th23;
hence thesis by A2,Th22;
end;
theorem Th25:
Mid a,p,a9 & Mid b,p,b9 implies a,b // b9,a9
proof
assume that
A1: Mid a,p,a9 and
A2: Mid b,p,b9;
consider d such that
A3: b9,p // a9,d by Def1;
a,p // p,a9 by A1;
then
A4: p,a // a9,p by Th7;
b,p // p,b9 by A2;
then
A5: p,b // b9,p by Th7;
a9,d // b9,p by A3,Th3;
then p,b // a9,d by A5,Def1;
then
A6: a,b // p,d by A4,Def1;
b9,a9 // p,d by A3,Def1;
hence thesis by A6,Def1;
end;
theorem
Mid a,p,a9 & Mid b,q,b9 & MDist p,q implies a,b // b9,a9
proof
assume that
A1: Mid a,p,a9 and
A2: Mid b,q,b9 and
A3: MDist p,q;
Mid a,q,a9 by A1,A3,Th23;
hence thesis by A2,Th25;
end;
::
:: Point Symmetry
::
definition
let AFV;
let a,b;
func PSym(a,b) -> Element of AFV means
:Def4:
Mid b,a,it;
correctness by Th21,Th22;
end;
theorem
PSym(p,a) = b iff a,p // p,b by Def3,Def4;
theorem Th28:
PSym(p,a) = a iff a = p or MDist a,p
proof
A1: now
assume a = p or MDist a,p;
then Mid a,p,a by Th18;
hence PSym(p,a) = a by Def4;
end;
now
assume PSym(p,a) = a;
then Mid a,p,a by Def4;
hence a = p or MDist a,p;
end;
hence thesis by A1;
end;
theorem Th29:
PSym(p,PSym(p,a)) = a
proof
Mid a,p,PSym(p,a) by Def4;
then Mid PSym(p,a),p,a by Th16;
hence thesis by Def4;
end;
theorem Th30:
PSym(p,a) = PSym(p,b) implies a = b
proof
assume
A1: PSym(p,a) = PSym(p,b);
PSym(p,PSym(p,a)) = a by Th29;
hence thesis by A1,Th29;
end;
theorem
ex a st PSym(p,a) = b
proof
PSym(p,PSym(p,b)) = b by Th29;
hence thesis;
end;
theorem Th32:
a,b // PSym(p,b),PSym(p,a)
proof
Mid a,p,PSym(p,a) & Mid b,p,PSym(p,b) by Def4;
hence thesis by Th25;
end;
theorem Th33:
a,b // c,d iff PSym(p,a),PSym(p,b) // PSym(p,c),PSym(p,d)
proof
A1: now
assume
A2: PSym(p,a),PSym(p,b) // PSym(p,c),PSym(p,d);
d,c // PSym(p,c),PSym(p,d) by Th32;
then d,c // PSym(p,a),PSym(p,b) by A2,Def1;
then
A3: c,d // PSym(p,b),PSym(p,a) by Th7;
a,b // PSym(p,b),PSym(p,a) by Th32;
hence a,b // c,d by A3,Def1;
end;
now
A4: PSym(p,b),PSym(p,a) // a,b by Th3,Th32;
assume
A5: a,b // c,d;
PSym(p,d),PSym(p,c) // c,d by Th3,Th32;
then PSym(p,d),PSym(p,c) // a,b by A5,Def1;
then PSym(p,b),PSym(p,a) // PSym(p,d),PSym(p,c) by A4,Def1;
hence PSym(p,a),PSym(p,b) // PSym(p,c),PSym(p,d) by Th7;
end;
hence thesis by A1;
end;
theorem
MDist a,b iff MDist PSym(p,a),PSym(p,b)
by Th30,Th33;
theorem Th35:
Mid a,b,c iff Mid PSym(p,a),PSym(p,b),PSym(p,c)
by Th33;
theorem Th36:
PSym(p,a) = PSym(q,a) iff p = q or MDist p,q
proof
A1: now
assume
A2: MDist p,q;
Mid a,p,PSym(p,a) & Mid a,q,PSym(q,a) by Def4;
hence PSym(p,a) = PSym(q,a) by A2,Th24;
end;
now
assume
A3: PSym(p,a) = PSym(q,a);
Mid a,p,PSym(p,a) & Mid a,q,PSym(q,a) by Def4;
hence p = q or MDist p,q by A3,Th20;
end;
hence thesis by A1;
end;
theorem Th37:
PSym(q,PSym(p,PSym(q,a))) = PSym(PSym(q,p),a)
proof
Mid PSym(q,a),p,PSym(p,PSym(q,a)) by Def4;
then Mid PSym(q,PSym(q,a)),PSym(q,p),PSym(q,PSym(p,PSym(q,a))) by Th35;
then PSym(q,PSym(p,PSym(q,a)))=PSym(PSym(q,p),PSym(q,PSym(q,a))) by Def4;
hence thesis by Th29;
end;
theorem
PSym(p,PSym(q,a)) = PSym(q,PSym(p,a)) iff p = q or MDist p,q or MDist
q,PSym(p,q)
proof
A1: now
assume PSym(p,PSym(q,a))=PSym(q,PSym(p,a));
then PSym(p,PSym(q,PSym(p,a)))=PSym(q,a) by Th29;
then PSym(PSym(p,q),a)=PSym(q,a) by Th37;
then q=PSym(p,q) or MDist q,PSym(p,q) by Th36;
then
A2: Mid q,p,q or MDist q,PSym(p,q) by Def4;
hence p = q or MDist q,p or MDist q,PSym(p,q);
thus p = q or MDist p,q or MDist q,PSym(p,q) by A2,Th18;
end;
now
assume p = q or MDist p,q or MDist q,PSym(p,q);
then Mid q,p,q or MDist q,PSym(p,q) by Th18;
then PSym(PSym(p,q),a)=PSym(q,a) by Def4,Th36;
then PSym(p,PSym(q,PSym(p,a)))=PSym(q,a) by Th37;
hence PSym(p,PSym(q,a))=PSym(q,PSym(p,a)) by Th29;
end;
hence thesis by A1;
end;
theorem Th39:
PSym(p,PSym(q,PSym(r,a))) = PSym(r,PSym(q,PSym(p,a)))
proof
p,a // PSym(r,a),PSym(r,p) & PSym(q,PSym(r,p)),PSym(q,PSym(r,a)) //
PSym(r,a ),PSym(r,p) by Th3,Th32;
then
A1: p,a // PSym(q,PSym(r,p)),PSym(q,PSym(r,a)) by Def1;
p,a // PSym(p,a),PSym(p,p) & PSym(q,PSym(p,p)),PSym(q,PSym(p,a)) //
PSym(p,a ),PSym(p,p) by Th3,Th32;
then
A2: p,a // PSym(q,PSym(p,p)),PSym(q,PSym(p,a)) by Def1;
PSym(q,p),PSym(r,p) // PSym(r,PSym(r,p)),PSym(r,PSym(q,p)) by Th32;
then PSym(q,p),PSym(r,p) // p,PSym(r,PSym(q,p)) by Th29;
then
A3: p,PSym(r,PSym(q,p)) // PSym(q,p),PSym(r,p) by Th3;
PSym(q,PSym(r,p)),p // PSym(q,p),PSym(q,PSym(q,PSym(r,p))) by Th32;
then PSym(q,PSym(r,p)),p // PSym(q,p),PSym(r,p) by Th29;
then PSym(q,PSym(r,p)),p // p,PSym(r,PSym(q,p)) by A3,Def1;
then Mid PSym(q,PSym(r,p)),p,PSym(r,PSym(q,p));
then PSym(p,PSym(q,PSym(r,p))) = PSym(r,PSym(q,p)) by Def4;
then
A4: PSym(p,PSym(q,PSym(r,p))) = PSym(r,PSym(q,PSym(p,p))) by Th28;
PSym(r,PSym(q,PSym(p,a))),PSym(r,PSym(q,PSym(p,p))) // PSym(q,PSym(p,p)
),PSym(q,PSym(p,a)) by Th3,Th32;
then
A5: PSym(r,PSym(q,PSym(p,a))),PSym(r,PSym(q,PSym(p,p))) // p,a by A2,Def1;
PSym(p,PSym(q,PSym(r,a))),PSym(p,PSym(q,PSym(r,p))) // PSym(q,PSym(r,p)
),PSym(q,PSym(r,a)) by Th3,Th32;
then PSym(p,PSym(q,PSym(r,a))),PSym(p,PSym(q,PSym(r,p))) // p,a by A1,Def1;
then PSym(p,PSym(q,PSym(r,a))),PSym(p,PSym(q,PSym(r,p))) // PSym(r,PSym(q,
PSym(p,a))),PSym(p,PSym(q,PSym(r,p))) by A4,A5,Def1;
hence thesis by Th4,Th7;
end;
theorem
ex d st PSym(a,PSym(b,PSym(c,p))) = PSym(d,p)
proof
consider e such that
A1: Mid a,e,c by Th19;
consider d such that
A2: Mid b,e,d by Th21;
c = PSym(e,a) by A1,Def4;
then PSym(c,PSym(d,p)) = PSym(PSym(e,a),PSym(PSym(e,b),p)) by A2,Def4
.= PSym(PSym(e,a),PSym(e,PSym(b,PSym(e,p)))) by Th37
.= PSym(e,PSym(a,PSym(e,PSym(e,PSym(b,PSym(e,p)))))) by Th37
.= PSym(e,PSym(a,PSym(b,PSym(e,p)))) by Th29
.= PSym(e,PSym(e,PSym(b,PSym(a,p)))) by Th39
.= PSym(b,PSym(a,p)) by Th29;
then PSym(d,p) = PSym(c,PSym(b,PSym(a,p))) by Th29;
hence thesis by Th39;
end;
theorem
ex c st PSym(a,PSym(c,p)) = PSym(c,PSym(b,p))
proof
consider c such that
A1: Mid a,c,b by Th19;
PSym(b,p) = PSym(PSym(c,a),p) by A1,Def4
.= PSym(c,PSym(a,(PSym(c,p)))) by Th37;
then PSym(c,PSym(b,p)) = PSym(a,(PSym(c,p))) by Th29;
hence thesis;
end;
::
:: Addition on the carrier
::
definition
let AFV,o;
let a,b;
func Padd(o,a,b) -> Element of AFV means
:Def5:
o,a // b,it;
correctness by Def1,Th5;
end;
notation
let AFV,o;
let a;
synonym Pcom(o,a) for PSym(o,a);
end;
Lm1: Pcom(o,a) = b iff a,o // o,b by Def4,Def3;
definition
let AFV,o;
func Padd(o) -> BinOp of the carrier of AFV means
:Def6:
for a,b holds it.(a ,b) = Padd(o,a,b);
existence
proof
deffunc F(Element of AFV, Element of AFV) = Padd(o,$1,$2);
consider O being BinOp of the carrier of AFV such that
A1: for a,b holds O.(a,b) = F(a,b) from BINOP_1:sch 4;
take O;
thus thesis by A1;
end;
uniqueness
proof
set X = the carrier of AFV;
let o1,o2 be BinOp of the carrier of AFV such that
A2: for a,b holds o1.(a,b) = Padd(o,a,b) and
A3: for a,b holds o2.(a,b) = Padd(o,a,b);
for x being Element of [:X,X:] holds o1.x = o2.x
proof
let x be Element of [:X,X:];
consider x1,x2 being Element of X such that
A4: x = [x1,x2] by DOMAIN_1:1;
o1.x = o1.(x1,x2) by A4
.= Padd(o,x1,x2) by A2
.= o2.(x1,x2) by A3
.= o2.x by A4;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let AFV,o;
func Pcom(o) -> UnOp of the carrier of AFV means
:Def7:
for a holds it.a = Pcom(o,a);
existence
proof
deffunc F(Element of AFV) = Pcom(o,$1);
consider O being UnOp of the carrier of AFV such that
A1: for a holds O.a = F(a) from FUNCT_2:sch 4;
take O;
thus thesis by A1;
end;
uniqueness
proof
set X = the carrier of AFV;
let o1,o2 be UnOp of the carrier of AFV such that
A2: for a holds o1.a = Pcom(o,a) and
A3: for a holds o2.a = Pcom(o,a);
for x being Element of X holds o1.x = o2.x
proof
let x be Element of X;
o1.x = Pcom(o,x) by A2
.= o2.x by A3;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let AFV,o;
func GroupVect(AFV,o) -> strict addLoopStr equals
addLoopStr(#the carrier of
AFV,Padd(o),o#);
correctness;
end;
registration
let AFV,o;
cluster GroupVect(AFV,o) -> non empty;
coherence;
end;
theorem
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
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);
Lm2: a+b = b+a
proof
reconsider a9=a,b9=b as Element of AFV;
reconsider c9=(a+b) as Element of AFV;
c9= Padd(o,a9,b9) by Def6;
then o,a9 // b9,c9 by Def5;
then o,b9 // a9,c9 by Def1;
then c9 = Padd(o,b9,a9) by Def5
.= b + a by Def6;
hence thesis;
end;
Lm3: (a+b)+c = a+(b+c)
proof
reconsider a9=a,b9=b,c9=c as Element of AFV;
set p= b+c,q=a+b;
reconsider p9=p,q9=q as Element of AFV;
reconsider x9=(a+p) ,y9=(q+c) as Element of AFV;
consider x99 such that
A1: x9,p9 // c9,x99 by Def1;
x9= Padd(o,a9,p9) by Def6;
then o,a9 // p9,x9 by Def5;
then
A2: a9,o // x9,p9 by Th7;
c9,x99 // x9,p9 by A1,Th3;
then
A3: a9,o // c9,x99 by A2,Def1;
q9= Padd(o,a9,b9) by Def6;
then o,a9 // b9,q9 by Def5;
then o,b9 // a9,q9 by Def1;
then
A4: a9,q9 // o,b9 by Th3;
p9= Padd(o,b9,c9) by Def6;
then o,b9 // c9,p9 by Def5;
then c9,p9 // o,b9 by Th3;
then a9,q9 // c9,p9 by A4,Def1;
then
A5: q9,o // p9,x99 by A3,Def1;
x9,c9 // p9,x99 by A1,Def1;
then q9,o // x9,c9 by A5,Def1;
then o,q9 // c9,x9 by Th7;
then
A6: c9,x9 // o,q9 by Th3;
y9= Padd(o,q9,c9) by Def6;
then o,q9 // c9,y9 by Def5;
then c9,y9 // o,q9 by Th3;
then c9,y9 // c9,x9 by A6,Def1;
hence thesis by Th4;
end;
Lm4: a + (0.(GroupVect(AFV,o))) = a
proof
reconsider a9=a as Element of AFV;
reconsider x9=(a + (0.(GroupVect(AFV,o)))) as Element of AFV;
x9= Padd(o,a9,o) by Def6;
then o,a9 // o,x9 by Def5;
hence thesis by Th4;
end;
Lm5: GroupVect(AFV,o) is Abelian add-associative right_zeroed
proof
thus for a,b holds a+b = b+a by Lm2;
thus for a,b,c holds (a+b)+c = a+(b+c) by Lm3;
thus for a holds a + 0.GroupVect(AFV,o) = a by Lm4;
end;
Lm6: GroupVect(AFV,o) is right_complementable
proof
let s be Element of GroupVect(AFV,o);
reconsider s9 = s as Element of AFV;
reconsider t = (Pcom(o)).s9 as Element of GroupVect(AFV,o);
take t;
Pcom(o,o) = o by Th28;
then o,s9 // Pcom(o,s9),o by Th32;
then
A1: Padd(o,s9,Pcom(o,s9)) = o by Def5;
thus s + t = (Padd(o)).(s9,(Pcom(o,s9))) by Def7
.= 0.GroupVect(AFV,o) by A1,Def6;
end;
registration
let AFV,o;
cluster GroupVect(AFV,o) -> Abelian add-associative right_zeroed
right_complementable;
coherence by Lm5,Lm6;
end;
theorem Th44:
for a being Element of GroupVect(AFV,o), a9 being Element of AFV
st a=a9 holds -a = (Pcom(o)).a9
proof
let a be Element of GroupVect(AFV,o), a9 be Element of AFV;
assume
A1: a=a9;
reconsider aa = (Pcom(o)).a9 as Element of GroupVect(AFV,o);
Pcom(o,o) = o & o,a9 // Pcom(o,a9),Pcom(o,o) by Th28,Th32;
then
A2: Padd(o,a9,Pcom(o,a9)) = o by Def5;
a + aa = (Padd(o)).(a,(Pcom(o,a9))) by Def7
.= 0.GroupVect(AFV,o) by A1,A2,Def6;
hence thesis by RLVECT_1:def 10;
end;
theorem
0.GroupVect(AFV,o) = o;
reserve a,b for Element of GroupVect(AFV,o);
theorem Th46:
for a ex b st b + b = a
proof
let a;
reconsider a99=a as Element of AFV;
consider b9 being Element of AFV such that
A1: o,b9 // b9,a99 by Def1;
reconsider b=b9 as Element of GroupVect(AFV,o);
a99 = Padd(o,b9,b9) by A1,Def5
.= b+b by Def6;
hence thesis;
end;
registration
let AFV,o;
cluster GroupVect(AFV,o) -> Two_Divisible;
coherence
proof
for a ex b st b + b = a by Th46;
hence thesis by TDGROUP:def 1;
end;
end;
::
:: Representation Theorem for Directed Geometrical Bundles
::
reserve AFV for AffVect,
o for Element of AFV;
theorem Th47:
for a being Element of GroupVect(AFV,o) st a + a = 0.(GroupVect(
AFV,o)) holds a = 0.(GroupVect(AFV,o))
proof
let a be Element of GroupVect(AFV,o) such that
A1: a + a = 0.(GroupVect(AFV,o));
reconsider a99=a as Element of AFV;
o = Padd(o,a99,a99) by A1,Def6;
then
A2: o,a99 // a99,o by Def5;
o,o // o,o by Th1;
hence thesis by A2,TDGROUP:16;
end;
registration
let AFV,o;
cluster GroupVect(AFV,o) -> Fanoian;
coherence
proof
for a being Element of GroupVect(AFV,o) st a + a = 0.(GroupVect(AFV,o)
) holds a = 0.(GroupVect(AFV,o)) by Th47;
hence thesis by VECTSP_1:def 18;
end;
end;
registration
cluster strict non trivial for Uniquely_Two_Divisible_Group;
existence
proof
set X = G_Real;
X is non trivial by TDGROUP:6;
hence thesis;
end;
end;
definition
mode Proper_Uniquely_Two_Divisible_Group is non trivial
Uniquely_Two_Divisible_Group;
end;
theorem
GroupVect(AFV,o) is Proper_Uniquely_Two_Divisible_Group;
registration
let AFV,o;
cluster GroupVect(AFV,o) -> non trivial;
coherence;
end;
theorem Th49:
for ADG being Proper_Uniquely_Two_Divisible_Group holds AV(ADG) is AffVect
proof
let ADG be Proper_Uniquely_Two_Divisible_Group;
ex a,b being Element of ADG st a<>b by STRUCT_0:def 10;
hence thesis by TDGROUP:17;
end;
registration
let ADG be Proper_Uniquely_Two_Divisible_Group;
cluster AV(ADG) -> AffVect-like non trivial;
coherence by Th49;
end;
theorem Th50:
for AFV being strict AffVect holds for o being Element of AFV
holds AFV = AV(GroupVect(AFV,o))
proof
let AFV be strict AffVect;
let o be Element of AFV;
set X = GroupVect(AFV,o);
now
let x,y be object;
set xy = [x,y];
A1: now
set V = the carrier of AFV;
assume
A2: xy in the CONGR of AFV;
set VV = [:V,V:];
xy`2 = y;
then
A3: y in VV by A2,MCART_1:10;
then
A4: y = [y`1,y`2] by MCART_1:21;
xy`1 = x;
then
A5: x in VV by A2,MCART_1:10;
then reconsider
x1 = x`1, x2 = x`2, y1 = y`1, y2 = y`2 as Element of AFV by A3,MCART_1:10
;
reconsider x19 = x1, x29 = x2, y19 = y1, y29 = y2 as Element of X;
A6: x = [x`1,x`2] by A5,MCART_1:21;
then
A7: x1,x2 // y1,y2 by A2,A4,ANALOAF:def 2;
x19 # y29 = x29 # y19
proof
reconsider z1=x19#y29,z2=x29#y19 as Element of AFV;
z1 = Padd(o,x1,y2) by Def6;
then o,x1 // y2,z1 by Def5;
then x1,o // z1,y2 by Th7;
then
A8: o,x2 // y1,z1 by A7,Th12;
z2 = Padd(o,x2,y1) by Def6;
hence thesis by A8,Def5;
end;
hence [x,y] in CONGRD(X) by A6,A4,TDGROUP:def 2;
end;
now
set V = the carrier of X;
assume
A9: xy in CONGRD(X);
set VV = [:V,V:];
xy`2 = y;
then
A10: y in VV by A9,MCART_1:10;
then
A11: y = [y`1,y`2] by MCART_1:21;
xy`1 = x;
then
A12: x in VV by A9,MCART_1:10;
then reconsider
x19 = x`1, x29 = x`2, y19 = y`1, y29 = y`2 as Element of X by A10,
MCART_1:10;
set z19 = x19 # y29, z29 = x29 # y19;
reconsider x1 = x19, x2 = x29, y1 = y19, y2 = y29 as Element of AFV;
reconsider z1=z19,z2=z29 as Element of AFV;
A13: z2 = Padd(o,x2,y1) by Def6;
z1 = Padd(o,x1,y2) by Def6;
then
A14: o,x1 // y2,z1 by Def5;
A15: x = [x`1,x`2] by A12,MCART_1:21;
then z19=z29 by A9,A11,TDGROUP:def 2;
then o,x2 // y1,z1 by A13,Def5;
then x1,x2 // y1,y2 by A14,Th12;
hence xy in the CONGR of AFV by A15,A11,ANALOAF:def 2;
end;
hence [x,y] in CONGRD(X) iff [x,y] in the CONGR of AFV by A1;
end;
then the carrier of AV(X) = the carrier of AFV & CONGRD(X) = the CONGR of
AFV by RELAT_1:def 2,TDGROUP:4;
hence thesis by TDGROUP:4;
end;
theorem
for AS being strict AffinStruct holds (AS is AffVect iff ex ADG being
Proper_Uniquely_Two_Divisible_Group st AS = AV(ADG) )
proof
let AS be strict AffinStruct;
now
assume AS is AffVect;
then reconsider AS9 = AS as AffVect;
set o = the Element of AS9;
take ADG = GroupVect(AS9,o);
AS9 = AV(ADG) by Th50;
hence ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV(ADG);
end;
hence thesis;
end;
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
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
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 Th52:
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)
proof
let o9 be Element of ADG, o be Element of AV(ADG);
assume that
A1: for x being Element of ADG holds f.x = o9+x and
A2: o=o9;
let a,b be Element of ADG;
set a9=f.a,b9=f.b;
A3: AV(ADG) = AffinStruct(#the carrier of ADG,CONGRD(ADG)#) by TDGROUP:def 3;
then reconsider a99=a9,b99=b9 as Element of AV(ADG);
thus f.(a+b) =(Padd(o)).((f.a),(f.b))
proof
A4: ((Padd(o)).((f.a),(f.b))) = Padd(o,a99,b99) by Def6;
then reconsider c99= (Padd(o)).((f.a),(f.b)) as Element of AV( ADG);
reconsider c9=c99 as Element of ADG by A3;
o,a99 // b99,c99 by A4,Def5;
then [[o9,a9],[b9,c9]] in CONGRD(ADG) by A2,A3,ANALOAF:def 2;
then
A5: o9+c9 = a9+b9 by TDGROUP:def 2;
a9 = o9+a & b9 = o9+b by A1;
then o9+c9 = (o9+((a+o9)+b)) by A5,RLVECT_1:def 3
.= o9+(o9+(a+b)) by RLVECT_1:def 3;
then c9 = o9+(a+b) by RLVECT_1:8
.= f.(a+b) by A1;
hence thesis;
end;
f.(0.ADG) = o9+(0.ADG) by A1
.= 0.(GroupVect(AV(ADG),o)) by A2,RLVECT_1:4;
hence f.(0.ADG) = 0.(GroupVect(AV(ADG),o));
thus f.(-a) = (Pcom(o)).(f.a)
proof
A6: ((Pcom(o)).(f.a)) = Pcom(o,a99) by Def7;
then reconsider c99 = (Pcom(o)).(f.a) as Element of AV(ADG);
reconsider c9=c99 as Element of ADG by A3;
a99,o // o,c99 by A6,Lm1;
then [[a9,o9],[o9,c9]] in CONGRD(ADG) by A2,A3,ANALOAF:def 2;
then a9+c9 = o9+o9 by TDGROUP:def 2;
then
A7: o9+o9 = (o9+a)+c9 by A1
.= o9+(a+c9) by RLVECT_1:def 3;
f.(-a) = o9+(-a) by A1
.= (c9+a)+(-a) by A7,RLVECT_1:8
.= c9+(a+(-a)) by RLVECT_1:def 3
.= c9+(0.ADG) by RLVECT_1:5
.= c9 by RLVECT_1:4;
hence thesis;
end;
end;
theorem Th53:
for o9 being Element of ADG st (for b being Element of ADG holds
f.b = o9+b) holds f is one-to-one
proof
let o9 be Element of ADG such that
A1: for b being Element of ADG holds f.b = o9+b;
now
let x1,x2 be object such that
A2: x1 in dom(f) & x2 in dom(f) and
A3: f.x1 = f.x2;
reconsider x19=x1,x29=x2 as Element of ADG by A2,FUNCT_2:def 1;
o9+x29 = f.x19 by A1,A3
.= o9+x19 by A1;
hence x1=x2 by RLVECT_1:8;
end;
hence thesis by FUNCT_1:def 4;
end;
theorem Th54:
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)
proof
set X = the carrier of ADG;
A1: X = dom(f) by FUNCT_2:def 1;
let o9 be Element of ADG, o be Element of AV(ADG) such that
A2: for b being Element of ADG holds f.b = o9+b;
now
let y be object;
assume y in X;
then reconsider y9=y as Element of X;
set x9=y9-o9;
f.x9 = o9+((-o9)+y9) by A2
.= (o9+(-o9))+y9 by RLVECT_1:def 3
.= y9+(0.ADG) by RLVECT_1:5
.= y by RLVECT_1:4;
hence y in rng(f) by A1,FUNCT_1:def 3;
end;
then
A3: X c= rng(f) by TARSKI:def 3;
rng(f) c= X & X = the carrier of GroupVect(AV(ADG),o) by RELAT_1:def 19
,TDGROUP:4;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem
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
proof
let ADG be Proper_Uniquely_Two_Divisible_Group, o9 be Element of ADG, o be
Element of AV(ADG) such that
A1: o=o9;
set AS = AV(ADG);
set X = the carrier of ADG,Z=GroupVect(AS,o);
set T = the carrier of GroupVect(AS,o);
deffunc F(Element of X) = o9+$1;
consider g being UnOp of X such that
A2: for a being Element of X holds g.a = F(a) from FUNCT_2:sch 4;
X = T by TDGROUP:4;
then reconsider f = g as Function of X,T;
A3: now
let a,b be Element of ADG;
reconsider fa = f.a as Element of AV(ADG);
thus f.(a+b) = (f.a)+(f.b) by A1,A2,Th52;
thus f.(0.ADG) = 0.Z by A1,A2,Th52;
thus f.(-a) = (Pcom(o)).fa by A1,A2,Th52
.= -(f.a) by Th44;
end;
f is one-to-one & rng(f) = T by A2,Th53,Th54;
then f is_Iso_of ADG,Z by A3;
hence thesis;
end;