:: by Wojciech Skaba

::

:: Received May 9, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

:: deftheorem Def1 defines Relation3 COLLSP:def 1 :

for X, b_{2} being set holds

( b_{2} is Relation3 of X iff b_{2} c= [:X,X,X:] );

for X, b

( b

theorem Th1: :: COLLSP:1

for X being set holds

( X = {} or ex a being set st

( {a} = X or ex a, b being set st

( a <> b & a in X & b in X ) ) )

( X = {} or ex a being set st

( {a} = X or ex a, b being set st

( a <> b & a in X & b in X ) ) )

proof end;

definition

attr c_{1} is strict ;

struct CollStr -> 1-sorted ;

aggr CollStr(# carrier, Collinearity #) -> CollStr ;

sel Collinearity c_{1} -> Relation3 of the carrier of c_{1};

end;
struct CollStr -> 1-sorted ;

aggr CollStr(# carrier, Collinearity #) -> CollStr ;

sel Collinearity c

registration
end;

:: deftheorem defines are_collinear COLLSP:def 2 :

for CS being non empty CollStr

for a, b, c being Point of CS holds

( a,b,c are_collinear iff [a,b,c] in the Collinearity of CS );

for CS being non empty CollStr

for a, b, c being Point of CS holds

( a,b,c are_collinear iff [a,b,c] in the Collinearity of CS );

set Z = {1};

Lm1: 1 in {1}

by TARSKI:def 1;

Lm2: {[1,1,1]} c= [:{1},{1},{1}:]

proof end;

reconsider Z = {1} as non empty set ;

reconsider RR = {[1,1,1]} as Relation3 of Z by Def1, Lm2;

reconsider CLS = CollStr(# Z,RR #) as non empty CollStr ;

Lm3: now :: thesis: for a, b, c, p, q, r being Point of CLS holds

( ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) & ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) )

( ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) & ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) )

let a, b, c, p, q, r be Point of CLS; :: thesis: ( ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) & ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) )

A1: for z1, z2, z3 being Point of CLS holds [z1,z2,z3] in the Collinearity of CLS

thus ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) by A1; :: thesis: verum

end;
A1: for z1, z2, z3 being Point of CLS holds [z1,z2,z3] in the Collinearity of CLS

proof

hence
( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS )
; :: thesis: ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS )
let z1, z2, z3 be Point of CLS; :: thesis: [z1,z2,z3] in the Collinearity of CLS

A2: z3 = 1 by TARSKI:def 1;

( z1 = 1 & z2 = 1 ) by TARSKI:def 1;

hence [z1,z2,z3] in the Collinearity of CLS by A2, TARSKI:def 1; :: thesis: verum

end;
A2: z3 = 1 by TARSKI:def 1;

( z1 = 1 & z2 = 1 ) by TARSKI:def 1;

hence [z1,z2,z3] in the Collinearity of CLS by A2, TARSKI:def 1; :: thesis: verum

thus ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) by A1; :: thesis: verum

:: deftheorem Def3 defines reflexive COLLSP:def 3 :

for IT being non empty CollStr holds

( IT is reflexive iff for a, b, c being Point of IT st ( a = b or a = c or b = c ) holds

[a,b,c] in the Collinearity of IT );

for IT being non empty CollStr holds

( IT is reflexive iff for a, b, c being Point of IT st ( a = b or a = c or b = c ) holds

[a,b,c] in the Collinearity of IT );

definition

let IT be non empty CollStr ;

end;
attr IT is transitive means :Def4: :: COLLSP:def 4

for a, b, p, q, r being Point of IT st a <> b & [a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r] in the Collinearity of IT holds

[p,q,r] in the Collinearity of IT;

for a, b, p, q, r being Point of IT st a <> b & [a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r] in the Collinearity of IT holds

[p,q,r] in the Collinearity of IT;

:: deftheorem Def4 defines transitive COLLSP:def 4 :

for IT being non empty CollStr holds

( IT is transitive iff for a, b, p, q, r being Point of IT st a <> b & [a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r] in the Collinearity of IT holds

[p,q,r] in the Collinearity of IT );

for IT being non empty CollStr holds

( IT is transitive iff for a, b, p, q, r being Point of IT st a <> b & [a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r] in the Collinearity of IT holds

[p,q,r] in the Collinearity of IT );

registration

existence

ex b_{1} being non empty CollStr st

( b_{1} is strict & b_{1} is reflexive & b_{1} is transitive )

end;
ex b

( b

proof end;

theorem Th3: :: COLLSP:3

for CLSP being CollSp

for a, b, p, q, r being Point of CLSP st a <> b & a,b,p are_collinear & a,b,q are_collinear & a,b,r are_collinear holds

p,q,r are_collinear by Def4;

for a, b, p, q, r being Point of CLSP st a <> b & a,b,p are_collinear & a,b,q are_collinear & a,b,r are_collinear holds

p,q,r are_collinear by Def4;

theorem Th4: :: COLLSP:4

for CLSP being CollSp

for a, b, c being Point of CLSP st a,b,c are_collinear holds

( b,a,c are_collinear & a,c,b are_collinear )

for a, b, c being Point of CLSP st a,b,c are_collinear holds

( b,a,c are_collinear & a,c,b are_collinear )

proof end;

theorem :: COLLSP:5

theorem Th6: :: COLLSP:6

for CLSP being CollSp

for a, b, c, d being Point of CLSP st a <> b & a,b,c are_collinear & a,b,d are_collinear holds

a,c,d are_collinear

for a, b, c, d being Point of CLSP st a <> b & a,b,c are_collinear & a,b,d are_collinear holds

a,c,d are_collinear

proof end;

theorem :: COLLSP:7

for CLSP being CollSp

for a, b, c being Point of CLSP st a,b,c are_collinear holds

b,a,c are_collinear by Th4;

for a, b, c being Point of CLSP st a,b,c are_collinear holds

b,a,c are_collinear by Th4;

theorem Th8: :: COLLSP:8

for CLSP being CollSp

for a, b, c being Point of CLSP st a,b,c are_collinear holds

b,c,a are_collinear

for a, b, c being Point of CLSP st a,b,c are_collinear holds

b,c,a are_collinear

proof end;

theorem Th9: :: COLLSP:9

for CLSP being CollSp

for a, b, p, q, r being Point of CLSP st p <> q & a,b,p are_collinear & a,b,q are_collinear & p,q,r are_collinear holds

a,b,r are_collinear

for a, b, p, q, r being Point of CLSP st p <> q & a,b,p are_collinear & a,b,q are_collinear & p,q,r are_collinear holds

a,b,r are_collinear

proof end;

:: *******************

:: * LINES *

:: *******************

:: * LINES *

:: *******************

definition

let CLSP be CollSp;

let a, b be Point of CLSP;

coherence

{ p where p is Point of CLSP : a,b,p are_collinear } is set ;

;

end;
let a, b be Point of CLSP;

func Line (a,b) -> set equals :: COLLSP:def 5

{ p where p is Point of CLSP : a,b,p are_collinear } ;

correctness { p where p is Point of CLSP : a,b,p are_collinear } ;

coherence

{ p where p is Point of CLSP : a,b,p are_collinear } is set ;

;

:: deftheorem defines Line COLLSP:def 5 :

for CLSP being CollSp

for a, b being Point of CLSP holds Line (a,b) = { p where p is Point of CLSP : a,b,p are_collinear } ;

for CLSP being CollSp

for a, b being Point of CLSP holds Line (a,b) = { p where p is Point of CLSP : a,b,p are_collinear } ;

theorem Th11: :: COLLSP:11

for CLSP being CollSp

for a, b, r being Point of CLSP holds

( a,b,r are_collinear iff r in Line (a,b) )

for a, b, r being Point of CLSP holds

( a,b,r are_collinear iff r in Line (a,b) )

proof end;

set Z = {1,2,3};

set RR = { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } ;

Lm4: { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } c= [:{1,2,3},{1,2,3},{1,2,3}:]

proof end;

reconsider Z = {1,2,3} as non empty set by ENUMSET1:def 1;

reconsider RR = { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } as Relation3 of Z by Def1, Lm4;

reconsider CLS = CollStr(# Z,RR #) as non empty CollStr ;

Lm5: for a, b, c being Point of CLS holds

( [a,b,c] in RR iff ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) )

proof end;

Lm6: for a, b, c, p, q, r being Point of CLS st a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS holds

[p,q,r] in the Collinearity of CLS

proof end;

Lm7: not for a, b, c being Point of CLS holds a,b,c are_collinear

proof end;

Lm8: CLS is CollSp

proof end;

definition

let IT be non empty CollStr ;

end;
attr IT is proper means :Def6: :: COLLSP:def 6

not for a, b, c being Point of IT holds a,b,c are_collinear ;

not for a, b, c being Point of IT holds a,b,c are_collinear ;

:: deftheorem Def6 defines proper COLLSP:def 6 :

for IT being non empty CollStr holds

( IT is proper iff not for a, b, c being Point of IT holds a,b,c are_collinear );

for IT being non empty CollStr holds

( IT is proper iff not for a, b, c being Point of IT holds a,b,c are_collinear );

registration
end;

theorem Th12: :: COLLSP:12

for CLSP being proper CollSp

for p, q being Point of CLSP st p <> q holds

ex r being Point of CLSP st not p,q,r are_collinear

for p, q being Point of CLSP st p <> q holds

ex r being Point of CLSP st not p,q,r are_collinear

proof end;

definition

let CLSP be proper CollSp;

ex b_{1} being set ex a, b being Point of CLSP st

( a <> b & b_{1} = Line (a,b) )

end;
mode LINE of CLSP -> set means :Def7: :: COLLSP:def 7

ex a, b being Point of CLSP st

( a <> b & it = Line (a,b) );

existence ex a, b being Point of CLSP st

( a <> b & it = Line (a,b) );

ex b

( a <> b & b

proof end;

:: deftheorem Def7 defines LINE COLLSP:def 7 :

for CLSP being proper CollSp

for b_{2} being set holds

( b_{2} is LINE of CLSP iff ex a, b being Point of CLSP st

( a <> b & b_{2} = Line (a,b) ) );

for CLSP being proper CollSp

for b

( b

( a <> b & b

theorem :: COLLSP:13

for CLSP being proper CollSp

for a, b being Point of CLSP st a = b holds

Line (a,b) = the carrier of CLSP

for a, b being Point of CLSP st a = b holds

Line (a,b) = the carrier of CLSP

proof end;

theorem :: COLLSP:14

for CLSP being proper CollSp

for P being LINE of CLSP ex a, b being Point of CLSP st

( a <> b & a in P & b in P )

for P being LINE of CLSP ex a, b being Point of CLSP st

( a <> b & a in P & b in P )

proof end;

theorem :: COLLSP:15

for CLSP being proper CollSp

for a, b being Point of CLSP st a <> b holds

ex P being LINE of CLSP st

( a in P & b in P )

for a, b being Point of CLSP st a <> b holds

ex P being LINE of CLSP st

( a in P & b in P )

proof end;

theorem Th16: :: COLLSP:16

for CLSP being proper CollSp

for p, q, r being Point of CLSP

for P being LINE of CLSP st p in P & q in P & r in P holds

p,q,r are_collinear

for p, q, r being Point of CLSP

for P being LINE of CLSP st p in P & q in P & r in P holds

p,q,r are_collinear

proof end;

Lm9: for CLSP being proper CollSp

for P being LINE of CLSP

for x being set st x in P holds

x is Point of CLSP

proof end;

theorem Th18: :: COLLSP:18

for CLSP being proper CollSp

for p, q being Point of CLSP

for P being LINE of CLSP st p <> q & p in P & q in P holds

Line (p,q) c= P

for p, q being Point of CLSP

for P being LINE of CLSP st p <> q & p in P & q in P holds

Line (p,q) c= P

proof end;

theorem Th19: :: COLLSP:19

for CLSP being proper CollSp

for p, q being Point of CLSP

for P being LINE of CLSP st p <> q & p in P & q in P holds

Line (p,q) = P

for p, q being Point of CLSP

for P being LINE of CLSP st p <> q & p in P & q in P holds

Line (p,q) = P

proof end;

theorem Th20: :: COLLSP:20

for CLSP being proper CollSp

for p, q being Point of CLSP

for P, Q being LINE of CLSP st p <> q & p in P & q in P & p in Q & q in Q holds

P = Q

for p, q being Point of CLSP

for P, Q being LINE of CLSP st p <> q & p in P & q in P & p in Q & q in Q holds

P = Q

proof end;

theorem :: COLLSP:21

for CLSP being proper CollSp

for P, Q being LINE of CLSP holds

( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} )

for P, Q being LINE of CLSP holds

( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} )

proof end;

theorem :: COLLSP:22

for CLSP being proper CollSp

for a, b being Point of CLSP st a <> b holds

Line (a,b) <> the carrier of CLSP

for a, b being Point of CLSP st a <> b holds

Line (a,b) <> the carrier of CLSP

proof end;

:: * COLLINEARITY *

:: *********************