:: Directed Geometrical Bundles and Their Analytical Representation
:: by Grzegorz Lewandowski, Krzysztof Pra\.zmowski and Bo\.zena Lewandowska
::
:: Received September 24, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users


begin

definition
let IT be non empty AffinStruct ;
attr IT is WeakAffVect-like means :Def1: :: 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;

:: deftheorem Def1 defines WeakAffVect-like AFVECT0:def 1 :
for IT being non empty AffinStruct holds
( IT is WeakAffVect-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, d being Element of IT st a,b // c,d holds
a,c // b,d ) ) );

registration
cluster non empty non trivial strict WeakAffVect-like AffinStruct ;
existence
ex b1 being non empty AffinStruct st
( b1 is strict & not b1 is trivial & b1 is WeakAffVect-like )
proof end;
end;

definition
mode WeakAffVect is non empty non trivial WeakAffVect-like AffinStruct ;
end;

registration
cluster non empty AffVect-like -> non empty WeakAffVect-like AffinStruct ;
coherence
for b1 being non empty AffinStruct st b1 is AffVect-like holds
b1 is WeakAffVect-like
proof end;
end;

theorem :: AFVECT0:1
canceled;

theorem Th2: :: AFVECT0:2
for AFV being WeakAffVect
for a, b being Element of AFV holds a,b // a,b
proof end;

theorem :: AFVECT0:3
for AFV being WeakAffVect
for a being Element of AFV holds a,a // a,a by Th2;

theorem Th4: :: AFVECT0:4
for AFV being WeakAffVect
for a, b, c, d being Element of AFV st a,b // c,d holds
c,d // a,b
proof end;

theorem Th5: :: AFVECT0:5
for AFV being WeakAffVect
for a, b, c being Element of AFV st a,b // a,c holds
b = c
proof end;

theorem Th6: :: AFVECT0:6
for AFV being WeakAffVect
for a, b, c, d, d9 being Element of AFV st a,b // c,d & a,b // c,d9 holds
d = d9
proof end;

theorem Th7: :: AFVECT0:7
for AFV being WeakAffVect
for a, b being Element of AFV holds a,a // b,b
proof end;

theorem Th8: :: AFVECT0:8
for AFV being WeakAffVect
for a, b, c, d being Element of AFV st a,b // c,d holds
b,a // d,c
proof end;

theorem :: AFVECT0:9
for AFV being WeakAffVect
for a, b, c, d, b9 being Element of AFV st a,b // c,d & a,c // b9,d holds
b = b9
proof end;

theorem :: AFVECT0:10
for AFV being WeakAffVect
for b, c, b9, c9, a, d, d9 being Element of AFV st b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 holds
d = d9
proof end;

theorem :: AFVECT0:11
for AFV being WeakAffVect
for a, b, a9, b9, c, d, d9 being Element of AFV st a,b // a9,b9 & c,d // b,a & c,d9 // b9,a9 holds
d = d9
proof end;

theorem :: AFVECT0:12
for AFV being WeakAffVect
for a, b, a9, b9, c, d, c9, d9, f, f9 being Element of AFV st a,b // a9,b9 & c,d // c9,d9 & b,f // c,d & b9,f9 // c9,d9 holds
a,f // a9,f9
proof end;

theorem Th13: :: AFVECT0:13
for AFV being WeakAffVect
for a, b, a9, b9, c, c9 being Element of AFV st a,b // a9,b9 & a,c // c9,b9 holds
b,c // c9,a9
proof end;

definition
let AFV be WeakAffVect;
let a, b be Element of AFV;
pred MDist a,b means :Def2: :: AFVECT0:def 2
( a,b // b,a & a <> b );
irreflexivity
for a being Element of AFV holds
( not a,a // a,a or not a <> a )
;
symmetry
for a, b being Element of AFV st a,b // b,a & a <> b holds
( b,a // a,b & b <> a )
by Th4;
end;

:: deftheorem Def2 defines MDist AFVECT0:def 2 :
for AFV being WeakAffVect
for a, b being Element of AFV holds
( MDist a,b iff ( a,b // b,a & a <> b ) );

theorem :: AFVECT0:14
canceled;

theorem :: AFVECT0:15
canceled;

theorem :: AFVECT0:16
for AFV being WeakAffVect ex a, b being Element of AFV st
( a <> b & not MDist a,b )
proof end;

theorem :: AFVECT0:17
canceled;

theorem :: AFVECT0:18
for AFV being WeakAffVect
for a, b, c being Element of AFV st MDist a,b & MDist a,c & not b = c holds
MDist b,c
proof end;

theorem :: AFVECT0:19
for AFV being WeakAffVect
for a, b, c, d being Element of AFV st MDist a,b & a,b // c,d holds
MDist c,d
proof end;

definition
let AFV be WeakAffVect;
let a, b, c be Element of AFV;
pred Mid a,b,c means :Def3: :: AFVECT0:def 3
a,b // b,c;
end;

:: deftheorem Def3 defines Mid AFVECT0:def 3 :
for AFV being WeakAffVect
for a, b, c being Element of AFV holds
( Mid a,b,c iff a,b // b,c );

theorem :: AFVECT0:20
canceled;

theorem Th21: :: AFVECT0:21
for AFV being WeakAffVect
for a, b, c being Element of AFV st Mid a,b,c holds
Mid c,b,a
proof end;

theorem :: AFVECT0:22
for AFV being WeakAffVect
for a, b being Element of AFV holds
( Mid a,b,b iff a = b )
proof end;

theorem Th23: :: AFVECT0:23
for AFV being WeakAffVect
for a, b being Element of AFV holds
( Mid a,b,a iff ( a = b or MDist a,b ) )
proof end;

theorem Th24: :: AFVECT0:24
for AFV being WeakAffVect
for a, c being Element of AFV ex b being Element of AFV st Mid a,b,c
proof end;

theorem Th25: :: AFVECT0:25
for AFV being WeakAffVect
for a, b, c, b9 being Element of AFV st Mid a,b,c & Mid a,b9,c & not b = b9 holds
MDist b,b9
proof end;

theorem Th26: :: AFVECT0:26
for AFV being WeakAffVect
for a, b being Element of AFV ex c being Element of AFV st Mid a,b,c
proof end;

theorem Th27: :: AFVECT0:27
for AFV being WeakAffVect
for a, b, c, c9 being Element of AFV st Mid a,b,c & Mid a,b,c9 holds
c = c9
proof end;

theorem Th28: :: AFVECT0:28
for AFV being WeakAffVect
for a, b, c, b9 being Element of AFV st Mid a,b,c & MDist b,b9 holds
Mid a,b9,c
proof end;

theorem Th29: :: AFVECT0:29
for AFV being WeakAffVect
for a, b, c, b9, c9 being Element of AFV st Mid a,b,c & Mid a,b9,c9 & MDist b,b9 holds
c = c9
proof end;

theorem Th30: :: AFVECT0:30
for AFV being WeakAffVect
for a, p, a9, b, b9 being Element of AFV st Mid a,p,a9 & Mid b,p,b9 holds
a,b // b9,a9
proof end;

theorem :: AFVECT0:31
for AFV being WeakAffVect
for a, p, a9, b, q, b9 being Element of AFV st Mid a,p,a9 & Mid b,q,b9 & MDist p,q holds
a,b // b9,a9
proof end;

definition
let AFV be WeakAffVect;
let a, b be Element of AFV;
func PSym (a,b) -> Element of AFV means :Def4: :: AFVECT0:def 4
Mid b,a,it;
correctness
existence
ex b1 being Element of AFV st Mid b,a,b1
;
uniqueness
for b1, b2 being Element of AFV st Mid b,a,b1 & Mid b,a,b2 holds
b1 = b2
;
by Th26, Th27;
end;

:: deftheorem Def4 defines PSym AFVECT0:def 4 :
for AFV being WeakAffVect
for a, b, b4 being Element of AFV holds
( b4 = PSym (a,b) iff Mid b,a,b4 );

theorem :: AFVECT0:32
canceled;

theorem :: AFVECT0:33
for AFV being WeakAffVect
for p, a, b being Element of AFV holds
( PSym (p,a) = b iff a,p // p,b )
proof end;

theorem :: AFVECT0:34
canceled;

theorem Th35: :: AFVECT0:35
for AFV being WeakAffVect
for p, a being Element of AFV holds
( PSym (p,a) = a iff ( a = p or MDist a,p ) )
proof end;

theorem Th36: :: AFVECT0:36
for AFV being WeakAffVect
for p, a being Element of AFV holds PSym (p,(PSym (p,a))) = a
proof end;

theorem Th37: :: AFVECT0:37
for AFV being WeakAffVect
for p, a, b being Element of AFV st PSym (p,a) = PSym (p,b) holds
a = b
proof end;

theorem :: AFVECT0:38
for AFV being WeakAffVect
for p, b being Element of AFV ex a being Element of AFV st PSym (p,a) = b
proof end;

theorem Th39: :: AFVECT0:39
for AFV being WeakAffVect
for a, b, p being Element of AFV holds a,b // PSym (p,b), PSym (p,a)
proof end;

theorem Th40: :: AFVECT0:40
for AFV being WeakAffVect
for a, b, c, d, p being Element of AFV holds
( a,b // c,d iff PSym (p,a), PSym (p,b) // PSym (p,c), PSym (p,d) )
proof end;

theorem :: AFVECT0:41
for AFV being WeakAffVect
for a, b, p being Element of AFV holds
( MDist a,b iff MDist PSym (p,a), PSym (p,b) )
proof end;

theorem Th42: :: AFVECT0:42
for AFV being WeakAffVect
for a, b, c, p being Element of AFV holds
( Mid a,b,c iff Mid PSym (p,a), PSym (p,b), PSym (p,c) )
proof end;

theorem Th43: :: AFVECT0:43
for AFV being WeakAffVect
for p, a, q being Element of AFV holds
( PSym (p,a) = PSym (q,a) iff ( p = q or MDist p,q ) )
proof end;

theorem Th44: :: AFVECT0:44
for AFV being WeakAffVect
for q, p, a being Element of AFV holds PSym (q,(PSym (p,(PSym (q,a))))) = PSym ((PSym (q,p)),a)
proof end;

theorem :: AFVECT0:45
for AFV being WeakAffVect
for p, q, a being Element of AFV holds
( PSym (p,(PSym (q,a))) = PSym (q,(PSym (p,a))) iff ( p = q or MDist p,q or MDist q, PSym (p,q) ) )
proof end;

theorem Th46: :: AFVECT0:46
for AFV being WeakAffVect
for p, q, r, a being Element of AFV holds PSym (p,(PSym (q,(PSym (r,a))))) = PSym (r,(PSym (q,(PSym (p,a)))))
proof end;

theorem :: AFVECT0:47
for AFV being WeakAffVect
for a, b, c, p being Element of AFV ex d being Element of AFV st PSym (a,(PSym (b,(PSym (c,p))))) = PSym (d,p)
proof end;

theorem :: AFVECT0:48
for AFV being WeakAffVect
for a, p, b being Element of AFV ex c being Element of AFV st PSym (a,(PSym (c,p))) = PSym (c,(PSym (b,p)))
proof end;

definition
let AFV be WeakAffVect;
let o, a, b be Element of AFV;
func Padd (o,a,b) -> Element of AFV means :Def5: :: AFVECT0:def 5
o,a // b,it;
correctness
existence
ex b1 being Element of AFV st o,a // b,b1
;
uniqueness
for b1, b2 being Element of AFV st o,a // b,b1 & o,a // b,b2 holds
b1 = b2
;
by Def1, Th6;
end;

:: deftheorem Def5 defines Padd AFVECT0:def 5 :
for AFV being WeakAffVect
for o, a, b, b5 being Element of AFV holds
( b5 = Padd (o,a,b) iff o,a // b,b5 );

notation
let AFV be WeakAffVect;
let o, a be Element of AFV;
synonym Pcom (o,a) for PSym (o,a);
end;

Lm1: for AFV being WeakAffVect
for o, a, b being Element of AFV holds
( Pcom (o,a) = b iff a,o // o,b )
proof end;

definition
let AFV be WeakAffVect;
let o be Element of AFV;
canceled;
func Padd o -> BinOp of the carrier of AFV means :Def7: :: AFVECT0:def 7
for a, b being Element of AFV holds it . (a,b) = Padd (o,a,b);
existence
ex b1 being BinOp of the carrier of AFV st
for a, b being Element of AFV holds b1 . (a,b) = Padd (o,a,b)
proof end;
uniqueness
for b1, b2 being BinOp of the carrier of AFV st ( for a, b being Element of AFV holds b1 . (a,b) = Padd (o,a,b) ) & ( for a, b being Element of AFV holds b2 . (a,b) = Padd (o,a,b) ) holds
b1 = b2
proof end;
end;

:: deftheorem AFVECT0:def 6 :
canceled;

:: deftheorem Def7 defines Padd AFVECT0:def 7 :
for AFV being WeakAffVect
for o being Element of AFV
for b3 being BinOp of the carrier of AFV holds
( b3 = Padd o iff for a, b being Element of AFV holds b3 . (a,b) = Padd (o,a,b) );

definition
let AFV be WeakAffVect;
let o be Element of AFV;
func Pcom o -> UnOp of the carrier of AFV means :Def8: :: AFVECT0:def 8
for a being Element of AFV holds it . a = Pcom (o,a);
existence
ex b1 being UnOp of the carrier of AFV st
for a being Element of AFV holds b1 . a = Pcom (o,a)
proof end;
uniqueness
for b1, b2 being UnOp of the carrier of AFV st ( for a being Element of AFV holds b1 . a = Pcom (o,a) ) & ( for a being Element of AFV holds b2 . a = Pcom (o,a) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Pcom AFVECT0:def 8 :
for AFV being WeakAffVect
for o being Element of AFV
for b3 being UnOp of the carrier of AFV holds
( b3 = Pcom o iff for a being Element of AFV holds b3 . a = Pcom (o,a) );

definition
let AFV be WeakAffVect;
let o be Element of AFV;
func GroupVect (AFV,o) -> strict addLoopStr equals :: AFVECT0:def 9
addLoopStr(# the carrier of AFV,(Padd o),o #);
correctness
coherence
addLoopStr(# the carrier of AFV,(Padd o),o #) is strict addLoopStr
;
;
end;

:: deftheorem defines GroupVect AFVECT0:def 9 :
for AFV being WeakAffVect
for o being Element of AFV holds GroupVect (AFV,o) = addLoopStr(# the carrier of AFV,(Padd o),o #);

registration
let AFV be WeakAffVect;
let o be Element of AFV;
cluster GroupVect (AFV,o) -> non empty strict ;
coherence
not GroupVect (AFV,o) is empty
;
end;

theorem :: AFVECT0:49
canceled;

theorem :: AFVECT0:50
canceled;

theorem :: AFVECT0:51
canceled;

theorem :: AFVECT0:52
canceled;

theorem :: AFVECT0:53
canceled;

theorem :: AFVECT0:54
canceled;

theorem :: AFVECT0:55
for AFV being WeakAffVect
for o being Element of AFV holds
( the carrier of (GroupVect (AFV,o)) = the carrier of AFV & the addF of (GroupVect (AFV,o)) = Padd o & 0. (GroupVect (AFV,o)) = o ) ;

theorem :: AFVECT0:56
canceled;

theorem :: AFVECT0:57
for AFV being WeakAffVect
for o being Element of AFV
for a, b being Element of (GroupVect (AFV,o))
for a9, b9 being Element of AFV st a = a9 & b = b9 holds
a + b = (Padd o) . (a9,b9) ;

Lm2: for AFV being WeakAffVect
for o being Element of AFV
for a, b being Element of (GroupVect (AFV,o)) holds a + b = b + a
proof end;

Lm3: for AFV being WeakAffVect
for o being Element of AFV
for a, b, c being Element of (GroupVect (AFV,o)) holds (a + b) + c = a + (b + c)
proof end;

Lm4: for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) holds a + (0. (GroupVect (AFV,o))) = a
proof end;

Lm5: for AFV being WeakAffVect
for o being Element of AFV holds
( GroupVect (AFV,o) is Abelian & GroupVect (AFV,o) is add-associative & GroupVect (AFV,o) is right_zeroed )
proof end;

Lm6: for AFV being WeakAffVect
for o being Element of AFV holds GroupVect (AFV,o) is right_complementable
proof end;

registration
let AFV be WeakAffVect;
let o be Element of AFV;
cluster GroupVect (AFV,o) -> strict right_complementable Abelian add-associative right_zeroed ;
coherence
( GroupVect (AFV,o) is Abelian & GroupVect (AFV,o) is add-associative & GroupVect (AFV,o) is right_zeroed & GroupVect (AFV,o) is right_complementable )
by Lm5, Lm6;
end;

theorem Th58: :: AFVECT0:58
for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect (AFV,o))
for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9
proof end;

theorem :: AFVECT0:59
for AFV being WeakAffVect
for o being Element of AFV holds 0. (GroupVect (AFV,o)) = o ;

theorem :: AFVECT0:60
canceled;

theorem :: AFVECT0:61
canceled;

theorem :: AFVECT0:62
canceled;

theorem :: AFVECT0:63
canceled;

theorem :: AFVECT0:64
canceled;

theorem :: AFVECT0:65
canceled;

theorem Th66: :: AFVECT0:66
for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) ex b being Element of (GroupVect (AFV,o)) st b + b = a
proof end;

registration
let AFV be WeakAffVect;
let o be Element of AFV;
cluster GroupVect (AFV,o) -> strict Two_Divisible ;
coherence
GroupVect (AFV,o) is Two_Divisible
proof end;
end;

theorem Th67: :: AFVECT0:67
for AFV being AffVect
for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) st a + a = 0. (GroupVect (AFV,o)) holds
a = 0. (GroupVect (AFV,o))
proof end;

registration
let AFV be AffVect;
let o be Element of AFV;
cluster GroupVect (AFV,o) -> strict Fanoian ;
coherence
GroupVect (AFV,o) is Fanoian
proof end;
end;

registration
cluster non empty non trivial strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr ;
existence
ex b1 being Uniquely_Two_Divisible_Group st
( b1 is strict & not b1 is trivial )
proof end;
end;

definition
mode Proper_Uniquely_Two_Divisible_Group is non trivial Uniquely_Two_Divisible_Group;
end;

theorem :: AFVECT0:68
canceled;

theorem :: AFVECT0:69
for AFV being AffVect
for o being Element of AFV holds GroupVect (AFV,o) is Proper_Uniquely_Two_Divisible_Group ;

registration
let AFV be AffVect;
let o be Element of AFV;
cluster GroupVect (AFV,o) -> non trivial strict ;
coherence
not GroupVect (AFV,o) is trivial
;
end;

theorem Th70: :: AFVECT0:70
for ADG being Proper_Uniquely_Two_Divisible_Group holds AV ADG is AffVect
proof end;

registration
let ADG be Proper_Uniquely_Two_Divisible_Group;
cluster AV ADG -> non trivial AffVect-like ;
coherence
( AV ADG is AffVect-like & not AV ADG is trivial )
by Th70;
end;

theorem Th71: :: AFVECT0:71
for AFV being strict AffVect
for o being Element of AFV holds AFV = AV (GroupVect (AFV,o))
proof end;

theorem :: AFVECT0:72
for AS being strict AffinStruct holds
( AS is AffVect iff ex ADG being Proper_Uniquely_Two_Divisible_Group st AS = AV ADG )
proof 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 :Def10: :: AFVECT0:def 10
( 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;

:: deftheorem Def10 defines is_Iso_of AFVECT0:def 10 :
for X, Y being non empty addLoopStr
for f being Function of the carrier of X, the carrier of Y holds
( f is_Iso_of X,Y iff ( 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) ) ) ) );

definition
let X, Y be non empty addLoopStr ;
pred X,Y are_Iso means :Def11: :: AFVECT0:def 11
ex f being Function of the carrier of X, the carrier of Y st f is_Iso_of X,Y;
end;

:: deftheorem Def11 defines are_Iso AFVECT0:def 11 :
for X, Y being non empty addLoopStr holds
( X,Y are_Iso iff ex f being Function of the carrier of X, the carrier of Y st f is_Iso_of X,Y );

theorem :: AFVECT0:73
canceled;

theorem :: AFVECT0:74
canceled;

theorem Th75: :: AFVECT0:75
for ADG being Proper_Uniquely_Two_Divisible_Group
for f being Function of the carrier of ADG, the carrier of ADG
for o9 being Element of ADG
for 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 end;

theorem Th76: :: AFVECT0:76
for ADG being Proper_Uniquely_Two_Divisible_Group
for f being Function of the carrier of ADG, the carrier of ADG
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 end;

theorem Th77: :: AFVECT0:77
for ADG being Proper_Uniquely_Two_Divisible_Group
for f being Function of the carrier of ADG, the carrier of ADG
for o9 being Element of ADG
for 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 end;

theorem :: AFVECT0:78
for ADG being Proper_Uniquely_Two_Divisible_Group
for o9 being Element of ADG
for o being Element of (AV ADG) st o = o9 holds
ADG, GroupVect ((AV ADG),o) are_Iso
proof end;