:: Fano-Desargues Parallelity Spaces :: by Eugeniusz Kusak and Wojciech Leo\'nczuk :: :: Received March 23, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for F being non empty right_complementable add-associative right_zeroed addLoopStr for a, b being Element of F st a - b = 0. F holds a = b proofend; Lm2: for F being non empty right_complementable add-associative right_zeroed addLoopStr for x, y being Element of F holds ( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) ) proofend; theorem Th1: :: PARSP_2:1 for F being Field holds MPS F is ParSp proofend; Lm3: for F being Field for e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds ( ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) iff ( ex K being Element of F st ( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ) proofend; theorem Th2: :: PARSP_2:2 for F being Field for a, b, c, d being Element of (MPS F) holds ( a,b '||' c,d iff ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st ( [a,b,c,d] = [e,f,g,h] & ( ex K being Element of F st ( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ) ) proofend; theorem Th3: :: PARSP_2:3 for F being Field for a, b, c being Element of (MPS F) for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] holds ( e <> f & e <> g & f <> g ) proofend; theorem Th4: :: PARSP_2:4 for F being Field for a, b, c being Element of (MPS F) for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] for K, L being Element of F st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K * ((e `1_3) - (f `1_3)) = L * ((e `1_3) - (g `1_3)) & K * ((e `2_3) - (f `2_3)) = L * ((e `2_3) - (g `2_3)) & K * ((e `3_3) - (f `3_3)) = L * ((e `3_3) - (g `3_3)) holds ( K = 0. F & L = 0. F ) proofend; Lm4: for F being non empty right_complementable add-associative right_zeroed addLoopStr for a, b, c being Element of F holds (b + a) - (c + a) = b - c proofend; Lm5: for F being Field for K, L, R being Element of F holds (K - L) - (R - L) = K - R proofend; Lm6: for F being Field for K, N, M, L, S being Element of F st (K * (N - M)) - (L * (N - S)) = S - M holds (K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S) proofend; Lm7: for F being Field for K, L, N, M being Element of F st K - L = N - M holds M = (L + N) - K proofend; theorem Th5: :: PARSP_2:5 for F being Field for a, b, c, d being Element of (MPS F) for e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d & [a,b,c,d] = [e,f,g,h] holds ( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) ) proofend; Lm8: for F being Field for L, K, R being Element of F st (L * K) - (L * R) = R + K holds (L - (1_ F)) * K = (L + (1_ F)) * R proofend; Lm9: for F being Field for L, K, N, R, S being Element of F st L * (K - N) = R - S & S = (K + N) - R holds (L - (1_ F)) * (R - N) = (L + (1_ F)) * (R - K) proofend; Lm10: for F being Field for K, L, M, N, R, S being Element of F st K = (L + M) - N & R = (L + S) - N holds (1_ F) * (M - S) = K - R proofend; theorem Th6: :: PARSP_2:6 for F being Field holds not for a, b, c being Element of (MPS F) holds a,b '||' a,c proofend; theorem Th7: :: PARSP_2:7 for F being Field for b, c, a, d being Element of (MPS F) st (1_ F) + (1_ F) <> 0. F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds a,b '||' a,c proofend; theorem Th8: :: PARSP_2:8 for F being Field for a, p, b, c, q, r being Element of (MPS F) st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds b,c '||' q,r proofend; :: 2. DEFINITION OF A FANO-DESARGUES SPACE definition let IT be ParSp; attrIT is FanodesSp-like means :Def1: :: PARSP_2:def 1 ( not for a, b, c being Element of IT holds a,b '||' a,c & ( for a, b, c, d being Element of IT st b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds a,b '||' a,c ) & ( for a, b, c, p, q, r being Element of IT st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds b,c '||' q,r ) ); end; :: deftheorem Def1 defines FanodesSp-like PARSP_2:def_1_:_ for IT being ParSp holds ( IT is FanodesSp-like iff ( not for a, b, c being Element of IT holds a,b '||' a,c & ( for a, b, c, d being Element of IT st b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds a,b '||' a,c ) & ( for a, b, c, p, q, r being Element of IT st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds b,c '||' q,r ) ) ); registration cluster non empty strict ParSp-like FanodesSp-like for ParStr ; existence ex b1 being ParSp st ( b1 is strict & b1 is FanodesSp-like ) proofend; end; definition mode FanodesSp is FanodesSp-like ParSp; end; :: 3. AXIOMS OF A FANO-DESARGUES PARALLELITY SPACE theorem Th9: :: PARSP_2:9 for FdSp being FanodesSp for p, q being Element of FdSp st p <> q holds ex r being Element of FdSp st not p,q '||' p,r proofend; definition let FdSp be FanodesSp; let a, b, c be Element of FdSp; preda,b,c is_collinear means :Def2: :: PARSP_2:def 2 a,b '||' a,c; end; :: deftheorem Def2 defines is_collinear PARSP_2:def_2_:_ for FdSp being FanodesSp for a, b, c being Element of FdSp holds ( a,b,c is_collinear iff a,b '||' a,c ); theorem Th10: :: PARSP_2:10 for FdSp being FanodesSp for a, b, c being Element of FdSp st a,b,c is_collinear holds ( a,c,b is_collinear & c,b,a is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear ) proofend; theorem Th11: :: PARSP_2:11 for FdSp being FanodesSp for a, b, c, p, q, r being Element of FdSp st not a,b,c is_collinear & a,b '||' p,q & a,c '||' p,r & p <> q & p <> r holds not p,q,r is_collinear proofend; theorem Th12: :: PARSP_2:12 for FdSp being FanodesSp for a, b, c being Element of FdSp st ( a = b or b = c or c = a ) holds a,b,c is_collinear proofend; theorem Th13: :: PARSP_2:13 for FdSp being FanodesSp for a, b, p, q, r being Element of FdSp st a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear holds p,q,r is_collinear proofend; theorem Th14: :: PARSP_2:14 for FdSp being FanodesSp for p, q being Element of FdSp st p <> q holds ex r being Element of FdSp st not p,q,r is_collinear proofend; theorem Th15: :: PARSP_2:15 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st a,b,c is_collinear & a,b,d is_collinear holds a,b '||' c,d proofend; theorem Th16: :: PARSP_2:16 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st not a,b,c is_collinear & a,b '||' c,d holds not a,b,d is_collinear proofend; theorem Th17: :: PARSP_2:17 for FdSp being FanodesSp for a, b, c, d, x being Element of FdSp st not a,b,c is_collinear & a,b '||' c,d & c <> d & a,b,x is_collinear holds not c,d,x is_collinear proofend; theorem :: PARSP_2:18 for FdSp being FanodesSp for o, a, b, x being Element of FdSp holds ( o,a,b is_collinear or not o,a,x is_collinear or not o,b,x is_collinear or o = x ) proofend; theorem :: PARSP_2:19 for FdSp being FanodesSp for o, a, b, p, q being Element of FdSp st o <> a & o <> b & o,a,b is_collinear & o,a,p is_collinear & o,b,q is_collinear holds a,b '||' p,q proofend; theorem :: PARSP_2:20 for FdSp being FanodesSp for a, b, c, d, p, q being Element of FdSp st not a,b '||' c,d & a,b,p is_collinear & a,b,q is_collinear & c,d,p is_collinear & c,d,q is_collinear holds p = q proofend; theorem :: PARSP_2:21 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st a <> b & a,b,c is_collinear & a,b '||' c,d holds a,c '||' b,d proofend; theorem :: PARSP_2:22 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st a <> b & a,b,c is_collinear & a,b '||' c,d holds c,b '||' c,d proofend; theorem :: PARSP_2:23 for FdSp being FanodesSp for o, a, c, b, p, q being Element of FdSp st not o,a,c is_collinear & o,a,b is_collinear & o,c,p is_collinear & o,c,q is_collinear & a,c '||' b,p & a,c '||' b,q holds p = q proofend; theorem :: PARSP_2:24 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st a <> b & a,b,c is_collinear & a,b,d is_collinear holds a,c,d is_collinear proofend; theorem :: PARSP_2:25 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st a,b,c is_collinear & a,c,d is_collinear & a <> c holds b,c,d is_collinear proofend; definition let FdSp be FanodesSp; let a, b, c, d be Element of FdSp; pred parallelogram a,b,c,d means :Def3: :: PARSP_2:def 3 ( not a,b,c is_collinear & a,b '||' c,d & a,c '||' b,d ); end; :: deftheorem Def3 defines parallelogram PARSP_2:def_3_:_ for FdSp being FanodesSp for a, b, c, d being Element of FdSp holds ( parallelogram a,b,c,d iff ( not a,b,c is_collinear & a,b '||' c,d & a,c '||' b,d ) ); theorem Th26: :: PARSP_2:26 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds ( a <> b & b <> c & c <> a & a <> d & b <> d & c <> d ) proofend; theorem Th27: :: PARSP_2:27 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear ) proofend; theorem Th28: :: PARSP_2:28 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear & not a,c,b is_collinear & not b,a,c is_collinear & not b,c,a is_collinear & not c,a,b is_collinear & not c,b,a is_collinear & not b,d,a is_collinear & not a,b,d is_collinear & not a,d,b is_collinear & not d,a,b is_collinear & not d,b,a is_collinear & not c,a,d is_collinear & not a,c,d is_collinear & not a,d,c is_collinear & not d,a,c is_collinear & not d,c,a is_collinear & not d,b,c is_collinear & not b,c,d is_collinear & not b,d,c is_collinear & not c,b,d is_collinear & not c,d,b is_collinear ) proofend; theorem Th29: :: PARSP_2:29 for FdSp being FanodesSp for a, b, c, d, x being Element of FdSp holds ( not parallelogram a,b,c,d or not a,b,x is_collinear or not c,d,x is_collinear ) proofend; theorem Th30: :: PARSP_2:30 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds parallelogram a,c,b,d proofend; theorem Th31: :: PARSP_2:31 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds parallelogram c,d,a,b proofend; theorem Th32: :: PARSP_2:32 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds parallelogram b,a,d,c proofend; theorem Th33: :: PARSP_2:33 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a ) proofend; theorem Th34: :: PARSP_2:34 for FdSp being FanodesSp for a, b, c being Element of FdSp st not a,b,c is_collinear holds ex d being Element of FdSp st parallelogram a,b,c,d proofend; theorem Th35: :: PARSP_2:35 for FdSp being FanodesSp for a, b, c, p, q being Element of FdSp st parallelogram a,b,c,p & parallelogram a,b,c,q holds p = q proofend; theorem Th36: :: PARSP_2:36 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds not a,d '||' b,c proofend; theorem Th37: :: PARSP_2:37 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds not parallelogram a,b,d,c proofend; theorem Th38: :: PARSP_2:38 for FdSp being FanodesSp for a, b being Element of FdSp st a <> b holds ex c being Element of FdSp st ( a,b,c is_collinear & c <> a & c <> b ) proofend; theorem Th39: :: PARSP_2:39 for FdSp being FanodesSp for a, p, b, q, c, r being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r holds b,c '||' q,r proofend; theorem Th40: :: PARSP_2:40 for FdSp being FanodesSp for b, q, c, a, p, r being Element of FdSp st not b,q,c is_collinear & parallelogram a,p,b,q & parallelogram a,p,c,r holds parallelogram b,q,c,r proofend; theorem Th41: :: PARSP_2:41 for FdSp being FanodesSp for a, b, c, p, q, r being Element of FdSp st a,b,c is_collinear & b <> c & parallelogram a,p,b,q & parallelogram a,p,c,r holds parallelogram b,q,c,r proofend; theorem Th42: :: PARSP_2:42 for FdSp being FanodesSp for a, p, b, q, c, r, d, s being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,q,d,s holds c,d '||' r,s proofend; theorem Th43: :: PARSP_2:43 for FdSp being FanodesSp for a, b being Element of FdSp st a <> b holds ex c, d being Element of FdSp st parallelogram a,b,c,d proofend; theorem :: PARSP_2:44 for FdSp being FanodesSp for a, d being Element of FdSp st a <> d holds ex b, c being Element of FdSp st parallelogram a,b,c,d proofend; definition let FdSp be FanodesSp; let a, b, r, s be Element of FdSp; preda,b congr r,s means :Def4: :: PARSP_2:def 4 ( ( a = b & r = s ) or ex p, q being Element of FdSp st ( parallelogram p,q,a,b & parallelogram p,q,r,s ) ); end; :: deftheorem Def4 defines congr PARSP_2:def_4_:_ for FdSp being FanodesSp for a, b, r, s being Element of FdSp holds ( a,b congr r,s iff ( ( a = b & r = s ) or ex p, q being Element of FdSp st ( parallelogram p,q,a,b & parallelogram p,q,r,s ) ) ); theorem Th45: :: PARSP_2:45 for FdSp being FanodesSp for a, b, c being Element of FdSp st a,a congr b,c holds b = c proofend; theorem :: PARSP_2:46 for FdSp being FanodesSp for a, b, c being Element of FdSp st a,b congr c,c holds a = b proofend; theorem :: PARSP_2:47 for FdSp being FanodesSp for a, b being Element of FdSp st a,b congr b,a holds a = b proofend; theorem Th48: :: PARSP_2:48 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st a,b congr c,d holds a,b '||' c,d proofend; theorem Th49: :: PARSP_2:49 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st a,b congr c,d holds a,c '||' b,d proofend; theorem Th50: :: PARSP_2:50 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st a,b congr c,d & not a,b,c is_collinear holds parallelogram a,b,c,d proofend; theorem Th51: :: PARSP_2:51 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds a,b congr c,d proofend; theorem Th52: :: PARSP_2:52 for FdSp being FanodesSp for a, b, c, d, r, s being Element of FdSp st a,b congr c,d & a,b,c is_collinear & parallelogram r,s,a,b holds parallelogram r,s,c,d proofend; theorem :: PARSP_2:53 for FdSp being FanodesSp for a, b, c, x, y being Element of FdSp st a,b congr c,x & a,b congr c,y holds x = y proofend; theorem :: PARSP_2:54 for FdSp being FanodesSp for a, b, c being Element of FdSp ex d being Element of FdSp st a,b congr c,d proofend; theorem Th55: :: PARSP_2:55 for FdSp being FanodesSp for a, b being Element of FdSp holds a,b congr a,b proofend; theorem Th56: :: PARSP_2:56 for FdSp being FanodesSp for r, s, a, b, c, d being Element of FdSp st r,s congr a,b & r,s congr c,d holds a,b congr c,d proofend; theorem :: PARSP_2:57 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st a,b congr c,d holds c,d congr a,b proofend; theorem :: PARSP_2:58 for FdSp being FanodesSp for a, b, c, d being Element of FdSp st a,b congr c,d holds b,a congr d,c proofend;