:: Parallelity and Lines in Affine Spaces :: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received May 4, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition let AS be AffinSpace; let a, b, c be Element of AS; pred LIN a,b,c means :Def1: :: AFF_1:def 1 a,b // a,c; end; :: deftheorem Def1 defines LIN AFF_1:def_1_:_ for AS being AffinSpace for a, b, c being Element of AS holds ( LIN a,b,c iff a,b // a,c ); theorem Th1: :: AFF_1:1 for AS being AffinSpace for a being Element of AS ex b being Element of AS st a <> b proofend; theorem Th2: :: AFF_1:2 for AS being AffinSpace for x, y being Element of AS holds ( x,y // y,x & x,y // x,y ) proofend; Lm1: for AS being AffinSpace for x, y, z, t being Element of AS st x,y // z,t holds z,t // x,y proofend; theorem Th3: :: AFF_1:3 for AS being AffinSpace for x, y, z being Element of AS holds ( x,y // z,z & z,z // x,y ) proofend; Lm2: for AS being AffinSpace for x, y, z, t being Element of AS st x,y // z,t holds y,x // z,t proofend; Lm3: for AS being AffinSpace for x, y, z, t being Element of AS st x,y // z,t holds x,y // t,z proofend; theorem Th4: :: AFF_1:4 for AS being AffinSpace for x, y, z, t being Element of AS st x,y // z,t holds ( x,y // t,z & y,x // z,t & y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x ) proofend; theorem Th5: :: AFF_1:5 for AS being AffinSpace for a, b, x, y, z, t being Element of AS st a <> b & ( ( a,b // x,y & a,b // z,t ) or ( a,b // x,y & z,t // a,b ) or ( x,y // a,b & z,t // a,b ) or ( x,y // a,b & a,b // z,t ) ) holds x,y // z,t proofend; Lm4: for AS being AffinSpace for x, y, z being Element of AS st LIN x,y,z holds ( LIN x,z,y & LIN y,x,z ) proofend; theorem Th6: :: AFF_1:6 for AS being AffinSpace for x, y, z being Element of AS st LIN x,y,z holds ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x ) proofend; theorem Th7: :: AFF_1:7 for AS being AffinSpace for x, y being Element of AS holds ( LIN x,x,y & LIN x,y,y & LIN x,y,x ) proofend; theorem Th8: :: AFF_1:8 for AS being AffinSpace for x, y, z, t, u being Element of AS st x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u holds LIN z,t,u proofend; theorem Th9: :: AFF_1:9 for AS being AffinSpace for x, y, z, t being Element of AS st x <> y & LIN x,y,z & x,y // z,t holds LIN x,y,t proofend; theorem Th10: :: AFF_1:10 for AS being AffinSpace for x, y, z, t being Element of AS st LIN x,y,z & LIN x,y,t holds x,y // z,t proofend; theorem Th11: :: AFF_1:11 for AS being AffinSpace for u, z, x, y, w being Element of AS st u <> z & LIN x,y,u & LIN x,y,z & LIN u,z,w holds LIN x,y,w proofend; theorem Th12: :: AFF_1:12 for AS being AffinSpace holds not for x, y, z being Element of AS holds LIN x,y,z proofend; theorem :: AFF_1:13 for AS being AffinSpace for x, y being Element of AS st x <> y holds ex z being Element of AS st not LIN x,y,z proofend; theorem :: AFF_1:14 for AS being AffinSpace for o, a, b, b9 being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 holds b = b9 proofend; :: :: Definition of the Line joining two points :: definition let AS be AffinSpace; let a, b be Element of AS; func Line (a,b) -> Subset of AS means :Def2: :: AFF_1:def 2 for x being Element of AS holds ( x in it iff LIN a,b,x ); existence ex b1 being Subset of AS st for x being Element of AS holds ( x in b1 iff LIN a,b,x ) proofend; uniqueness for b1, b2 being Subset of AS st ( for x being Element of AS holds ( x in b1 iff LIN a,b,x ) ) & ( for x being Element of AS holds ( x in b2 iff LIN a,b,x ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines Line AFF_1:def_2_:_ for AS being AffinSpace for a, b being Element of AS for b4 being Subset of AS holds ( b4 = Line (a,b) iff for x being Element of AS holds ( x in b4 iff LIN a,b,x ) ); Lm5: for AS being AffinSpace for a, b being Element of AS holds Line (a,b) c= Line (b,a) proofend; definition let AS be AffinSpace; let a, b be Element of AS; :: original:Line redefine func Line (a,b) -> Subset of AS; commutativity for a, b being Element of AS holds Line (a,b) = Line (b,a) proofend; end; theorem Th15: :: AFF_1:15 for AS being AffinSpace for a, b being Element of AS holds ( a in Line (a,b) & b in Line (a,b) ) proofend; theorem Th16: :: AFF_1:16 for AS being AffinSpace for c, a, b, d being Element of AS st c in Line (a,b) & d in Line (a,b) & c <> d holds Line (c,d) c= Line (a,b) proofend; theorem Th17: :: AFF_1:17 for AS being AffinSpace for c, a, b, d being Element of AS st c in Line (a,b) & d in Line (a,b) & a <> b holds Line (a,b) c= Line (c,d) proofend; :: :: Definition of the Line :: definition let AS be AffinSpace; let A be Subset of AS; attrA is being_line means :Def3: :: AFF_1:def 3 ex a, b being Element of AS st ( a <> b & A = Line (a,b) ); end; :: deftheorem Def3 defines being_line AFF_1:def_3_:_ for AS being AffinSpace for A being Subset of AS holds ( A is being_line iff ex a, b being Element of AS st ( a <> b & A = Line (a,b) ) ); registration let AS be AffinSpace; cluster being_line for M2(K24( the carrier of AS)); existence ex b1 being Subset of AS st b1 is being_line proofend; end; Lm6: for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds A = Line (a,b) proofend; :: Otrzymujemy stad zasadnicze stwierdzenie, ze kazda prosta :: jest jednoznacznie wyznaczona przez swoje dowolne dwa punkty. theorem Th18: :: AFF_1:18 for AS being AffinSpace for a, b being Element of AS for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds A = C proofend; theorem Th19: :: AFF_1:19 for AS being AffinSpace for A being Subset of AS st A is being_line holds ex a, b being Element of AS st ( a in A & b in A & a <> b ) proofend; theorem Th20: :: AFF_1:20 for AS being AffinSpace for a being Element of AS for A being Subset of AS st A is being_line holds ex b being Element of AS st ( a <> b & b in A ) proofend; theorem Th21: :: AFF_1:21 for AS being AffinSpace for a, b, c being Element of AS holds ( LIN a,b,c iff ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) ) proofend; :: :: Definition of the parallelity between segments and lines :: definition let AS be AffinSpace; let a, b be Element of AS; let A be Subset of AS; preda,b // A means :Def4: :: AFF_1:def 4 ex c, d being Element of AS st ( c <> d & A = Line (c,d) & a,b // c,d ); end; :: deftheorem Def4 defines // AFF_1:def_4_:_ for AS being AffinSpace for a, b being Element of AS for A being Subset of AS holds ( a,b // A iff ex c, d being Element of AS st ( c <> d & A = Line (c,d) & a,b // c,d ) ); definition let AS be AffinSpace; let A, C be Subset of AS; predA // C means :Def5: :: AFF_1:def 5 ex a, b being Element of AS st ( A = Line (a,b) & a <> b & a,b // C ); end; :: deftheorem Def5 defines // AFF_1:def_5_:_ for AS being AffinSpace for A, C being Subset of AS holds ( A // C iff ex a, b being Element of AS st ( A = Line (a,b) & a <> b & a,b // C ) ); theorem Th22: :: AFF_1:22 for AS being AffinSpace for c, a, b, d being Element of AS st c in Line (a,b) & a <> b holds ( d in Line (a,b) iff a,b // c,d ) proofend; theorem Th23: :: AFF_1:23 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st A is being_line & a in A holds ( b in A iff a,b // A ) proofend; theorem :: AFF_1:24 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS holds ( a <> b & A = Line (a,b) iff ( A is being_line & a in A & b in A & a <> b ) ) by Def3, Lm6, Th15; theorem Th25: :: AFF_1:25 for AS being AffinSpace for a, b, x being Element of AS for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds x in A proofend; theorem Th26: :: AFF_1:26 for AS being AffinSpace for A being Subset of AS st ex a, b being Element of AS st a,b // A holds A is being_line proofend; theorem Th27: :: AFF_1:27 for AS being AffinSpace for c, d, a, b being Element of AS for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds ( a,b // A iff a,b // c,d ) proofend; theorem Th28: :: AFF_1:28 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st a,b // A holds ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) proofend; theorem Th29: :: AFF_1:29 for AS being AffinSpace for a, b being Element of AS st a <> b holds a,b // Line (a,b) proofend; theorem Th30: :: AFF_1:30 for AS being AffinSpace for a, b being Element of AS for A being being_line Subset of AS holds ( a,b // A iff ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) ) proofend; theorem :: AFF_1:31 for AS being AffinSpace for a, b, c, d being Element of AS for A being being_line Subset of AS st a,b // A & c,d // A holds a,b // c,d proofend; theorem Th32: :: AFF_1:32 for AS being AffinSpace for a, b, p, q being Element of AS for A being Subset of AS st a,b // A & a,b // p,q & a <> b holds p,q // A proofend; theorem Th33: :: AFF_1:33 for AS being AffinSpace for a being Element of AS for A being being_line Subset of AS holds a,a // A proofend; theorem Th34: :: AFF_1:34 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st a,b // A holds b,a // A proofend; theorem :: AFF_1:35 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st a,b // A & not a in A holds not b in A proofend; theorem Th36: :: AFF_1:36 for AS being AffinSpace for A, C being Subset of AS st A // C holds ( A is being_line & C is being_line ) proofend; theorem Th37: :: AFF_1:37 for AS being AffinSpace for A, C being Subset of AS holds ( A // C iff ex a, b, c, d being Element of AS st ( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) ) proofend; theorem Th38: :: AFF_1:38 for AS being AffinSpace for a, b, c, d being Element of AS for A, C being being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds ( A // C iff a,b // c,d ) proofend; theorem Th39: :: AFF_1:39 for AS being AffinSpace for a, b, c, d being Element of AS for A, C being Subset of AS st a in A & b in A & c in C & d in C & A // C holds a,b // c,d proofend; theorem :: AFF_1:40 for AS being AffinSpace for a, b being Element of AS for A, C being Subset of AS st a in A & b in A & A // C holds a,b // C proofend; theorem Th41: :: AFF_1:41 for AS being AffinSpace for A being being_line Subset of AS holds A // A proofend; definition let AS be AffinSpace; let A, B be being_line Subset of AS; :: original:// redefine predA // B; reflexivity for A being being_line Subset of AS holds (AS,b1,b1) by Th41; end; theorem Th42: :: AFF_1:42 for AS being AffinSpace for A, C being Subset of AS st A // C holds C // A proofend; definition let AS be AffinSpace; let A, C be Subset of AS; :: original:// redefine predA // C; symmetry for A, C being Subset of AS st (AS,b1,b2) holds (AS,b2,b1) by Th42; end; theorem Th43: :: AFF_1:43 for AS being AffinSpace for a, b being Element of AS for A, C being Subset of AS st a,b // A & A // C holds a,b // C proofend; Lm7: for AS being AffinSpace for A, C, D being Subset of AS st A // C & C // D holds A // D proofend; theorem :: AFF_1:44 for AS being AffinSpace for A, C, D being Subset of AS st ( ( A // C & C // D ) or ( A // C & D // C ) or ( C // A & C // D ) or ( C // A & D // C ) ) holds A // D by Lm7; theorem Th45: :: AFF_1:45 for AS being AffinSpace for p being Element of AS for A, C being Subset of AS st A // C & p in A & p in C holds A = C proofend; theorem :: AFF_1:46 for AS being AffinSpace for x, a, b being Element of AS for K being Subset of AS st x in K & not a in K & a,b // K & not a = b holds not LIN x,a,b proofend; theorem :: AFF_1:47 for AS being AffinSpace for a9, b9, p, a, b being Element of AS for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds a9 = b9 proofend; theorem :: AFF_1:48 for AS being AffinSpace for a, b, c, d being Element of AS for A being being_line Subset of AS st a in A & b in A & c in A & a <> b & a,b // c,d holds d in A proofend; theorem :: AFF_1:49 for AS being AffinSpace for a being Element of AS for A being being_line Subset of AS ex C being Subset of AS st ( a in C & A // C ) proofend; theorem :: AFF_1:50 for AS being AffinSpace for p being Element of AS for A, C, D being Subset of AS st A // C & A // D & p in C & p in D holds C = D by Lm7, Th45; :: :: Additional theorems :: theorem :: AFF_1:51 for AS being AffinSpace for a, b, c, d being Element of AS for A being Subset of AS st A is being_line & a in A & b in A & c in A & d in A holds a,b // c,d by Th39, Th41; theorem :: AFF_1:52 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st A is being_line & a in A & b in A holds a,b // A by Th23; theorem :: AFF_1:53 for AS being AffinSpace for a, b being Element of AS for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds A // C proofend; theorem Th54: :: AFF_1:54 for AS being AffinSpace for o, a, b, a9, b9 being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9 = b9 holds ( a9 = o & b9 = o ) proofend; theorem Th55: :: AFF_1:55 for AS being AffinSpace for o, a, b, b9, a9 being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a9,b9 & a9 = o holds b9 = o proofend; theorem :: AFF_1:56 for AS being AffinSpace for o, a, b, a9, b9, x being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & LIN o,b,x & a,b // a9,b9 & a,b // a9,x holds b9 = x proofend; theorem :: AFF_1:57 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds A = Line (a,b) by Lm6; theorem Th58: :: AFF_1:58 for AP being AffinPlane for A, C being Subset of AP st A is being_line & C is being_line & not A // C holds ex x being Element of AP st ( x in A & x in C ) proofend; theorem :: AFF_1:59 for AP being AffinPlane for a, b being Element of AP for A being Subset of AP st A is being_line & not a,b // A holds ex x being Element of AP st ( x in A & LIN a,b,x ) proofend; theorem :: AFF_1:60 for AP being AffinPlane for a, b, c, d being Element of AP st not a,b // c,d holds ex p being Element of AP st ( LIN a,b,p & LIN c,d,p ) proofend;