:: Directed Geometrical Bundles and Their Analytical Representation :: by Grzegorz Lewandowski, Krzysztof Pra\.zmowski and Bo\.zena Lewandowska :: :: Received September 24, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition let IT be non empty AffinStruct ; attrIT 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 for AffinStruct ; existence ex b1 being non trivial AffinStruct st ( b1 is strict & b1 is WeakAffVect-like ) proofend; end; definition mode WeakAffVect is non trivial WeakAffVect-like AffinStruct ; end; registration cluster non empty AffVect-like -> non empty WeakAffVect-like for AffinStruct ; coherence for b1 being non empty AffinStruct st b1 is AffVect-like holds b1 is WeakAffVect-like proofend; end; :: :: Properties of Relation of Congruence of Vectors :: theorem Th1: :: AFVECT0:1 for AFV being WeakAffVect for a, b being Element of AFV holds a,b // a,b proofend; theorem :: AFVECT0:2 for AFV being WeakAffVect for a being Element of AFV holds a,a // a,a by Th1; theorem Th3: :: AFVECT0:3 for AFV being WeakAffVect for a, b, c, d being Element of AFV st a,b // c,d holds c,d // a,b proofend; theorem Th4: :: AFVECT0:4 for AFV being WeakAffVect for a, b, c being Element of AFV st a,b // a,c holds b = c proofend; theorem Th5: :: AFVECT0:5 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 proofend; theorem Th6: :: AFVECT0:6 for AFV being WeakAffVect for a, b being Element of AFV holds a,a // b,b proofend; theorem Th7: :: AFVECT0:7 for AFV being WeakAffVect for a, b, c, d being Element of AFV st a,b // c,d holds b,a // d,c proofend; theorem :: AFVECT0:8 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 proofend; theorem :: AFVECT0:9 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 proofend; theorem :: AFVECT0:10 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 proofend; theorem :: AFVECT0:11 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 proofend; theorem Th12: :: AFVECT0:12 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 proofend; :: :: Relation of Maximal Distance :: 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 Th3; 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:13 for AFV being WeakAffVect ex a, b being Element of AFV st ( a <> b & not MDist a,b ) proofend; theorem :: AFVECT0:14 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 proofend; theorem :: AFVECT0:15 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 proofend; :: :: Midpoint Relation :: 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 Th16: :: AFVECT0:16 for AFV being WeakAffVect for a, b, c being Element of AFV st Mid a,b,c holds Mid c,b,a proofend; theorem :: AFVECT0:17 for AFV being WeakAffVect for a, b being Element of AFV holds ( Mid a,b,b iff a = b ) proofend; theorem Th18: :: AFVECT0:18 for AFV being WeakAffVect for a, b being Element of AFV holds ( Mid a,b,a iff ( a = b or MDist a,b ) ) proofend; theorem Th19: :: AFVECT0:19 for AFV being WeakAffVect for a, c being Element of AFV ex b being Element of AFV st Mid a,b,c proofend; theorem Th20: :: AFVECT0:20 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 proofend; theorem Th21: :: AFVECT0:21 for AFV being WeakAffVect for a, b being Element of AFV ex c being Element of AFV st Mid a,b,c proofend; theorem Th22: :: AFVECT0:22 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 proofend; theorem Th23: :: AFVECT0:23 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 proofend; theorem Th24: :: AFVECT0:24 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 proofend; theorem Th25: :: AFVECT0:25 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 proofend; theorem :: AFVECT0:26 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 proofend; :: :: Point Symmetry :: 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 Th21, Th22; 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:27 for AFV being WeakAffVect for p, a, b being Element of AFV holds ( PSym (p,a) = b iff a,p // p,b ) proofend; theorem Th28: :: AFVECT0:28 for AFV being WeakAffVect for p, a being Element of AFV holds ( PSym (p,a) = a iff ( a = p or MDist a,p ) ) proofend; theorem Th29: :: AFVECT0:29 for AFV being WeakAffVect for p, a being Element of AFV holds PSym (p,(PSym (p,a))) = a proofend; theorem Th30: :: AFVECT0:30 for AFV being WeakAffVect for p, a, b being Element of AFV st PSym (p,a) = PSym (p,b) holds a = b proofend; theorem :: AFVECT0:31 for AFV being WeakAffVect for p, b being Element of AFV ex a being Element of AFV st PSym (p,a) = b proofend; theorem Th32: :: AFVECT0:32 for AFV being WeakAffVect for a, b, p being Element of AFV holds a,b // PSym (p,b), PSym (p,a) proofend; theorem Th33: :: AFVECT0:33 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) ) proofend; theorem :: AFVECT0:34 for AFV being WeakAffVect for a, b, p being Element of AFV holds ( MDist a,b iff MDist PSym (p,a), PSym (p,b) ) proofend; theorem Th35: :: AFVECT0:35 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) ) proofend; theorem Th36: :: AFVECT0:36 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 ) ) proofend; theorem Th37: :: AFVECT0:37 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) proofend; theorem :: AFVECT0:38 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) ) ) proofend; theorem Th39: :: AFVECT0:39 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))))) proofend; theorem :: AFVECT0:40 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) proofend; theorem :: AFVECT0:41 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))) proofend; :: :: Addition on the carrier :: 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, Th5; 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 ) proofend; definition let AFV be WeakAffVect; let o be Element of AFV; func Padd o -> BinOp of the carrier of AFV means :Def6: :: AFVECT0:def 6 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) proofend; 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 proofend; end; :: deftheorem Def6 defines Padd AFVECT0:def_6_:_ 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 :Def7: :: AFVECT0:def 7 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) proofend; 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 proofend; end; :: deftheorem Def7 defines Pcom AFVECT0:def_7_:_ 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 8 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_8_:_ 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:42 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:43 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 proofend; 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) proofend; 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 proofend; 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 ) proofend; Lm6: for AFV being WeakAffVect for o being Element of AFV holds GroupVect (AFV,o) is right_complementable proofend; 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 Th44: :: AFVECT0:44 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 proofend; theorem :: AFVECT0:45 for AFV being WeakAffVect for o being Element of AFV holds 0. (GroupVect (AFV,o)) = o ; theorem Th46: :: AFVECT0:46 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 proofend; 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 proofend; end; theorem Th47: :: AFVECT0:47 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)) proofend; registration let AFV be AffVect; let o be Element of AFV; cluster GroupVect (AFV,o) -> strict Fanoian ; coherence GroupVect (AFV,o) is Fanoian proofend; end; registration cluster non empty non trivial strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible for addLoopStr ; existence ex b1 being Uniquely_Two_Divisible_Group st ( b1 is strict & not b1 is trivial ) proofend; end; definition mode Proper_Uniquely_Two_Divisible_Group is non trivial Uniquely_Two_Divisible_Group; end; theorem :: AFVECT0:48 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 Th49: :: AFVECT0:49 for ADG being Proper_Uniquely_Two_Divisible_Group holds AV ADG is AffVect proofend; 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 Th49; end; theorem Th50: :: AFVECT0:50 for AFV being strict AffVect for o being Element of AFV holds AFV = AV (GroupVect (AFV,o)) proofend; 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 ) proofend; definition let X, Y be non empty addLoopStr ; let f be Function of the carrier of X, the carrier of Y; predf is_Iso_of X,Y means :Def9: :: 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; :: deftheorem Def9 defines is_Iso_of AFVECT0:def_9_:_ 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 ; predX,Y are_Iso means :Def10: :: AFVECT0:def 10 ex f being Function of the carrier of X, the carrier of Y st f is_Iso_of X,Y; end; :: deftheorem Def10 defines are_Iso AFVECT0:def_10_:_ 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 Th52: :: AFVECT0:52 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) ) proofend; theorem Th53: :: AFVECT0:53 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 proofend; theorem Th54: :: AFVECT0:54 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)) proofend; theorem :: AFVECT0:55 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 proofend;