:: Parallelity and Lines in Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received May 4, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies DIRAF, SUBSET_1, ANALOAF, INCSP_1, STRUCT_0, TARSKI, AFF_1;
notations TARSKI, STRUCT_0, ANALOAF, DIRAF;
constructors DIRAF;
registrations STRUCT_0;
requirements SUBSET, BOOLE;
definitions TARSKI;
theorems DIRAF, TARSKI, XBOOLE_0, SUBSET_1;
schemes SUBSET_1;
begin
reserve AS for AffinSpace;
reserve a,a9,b,b9,c,d,o,p,q,r,s,x,y,z,t,u,w for Element of AS;
definition
let AS,a,b,c;
pred LIN a,b,c means
a,b // a,c;
end;
::$CT
theorem Th1:
x,y // y,x & x,y // x,y by DIRAF:40;
Lm1: x,y // z,t implies z,t // x,y
proof
assume
A1: x,y // z,t;
now
assume
A2: x<>y;
x,y // x,y by Th1;
hence thesis by A1,A2,DIRAF:40;
end;
hence thesis by DIRAF:40;
end;
theorem Th2:
x,y // z,z & z,z // x,y by Lm1,DIRAF:40;
Lm2: x,y // z,t implies y,x // z,t
proof
assume
A1: x,y // z,t;
x,y // y,x by Th1;
then y,x // z,t or x=y by A1,DIRAF:40;
hence thesis by Th2;
end;
Lm3: x,y // z,t implies x,y // t,z
proof
assume x,y // z,t;
then z,t // x,y by Lm1;
then t,z // x,y by Lm2;
hence thesis by Lm1;
end;
theorem Th3:
x,y // z,t implies 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
proof
assume
A1: x,y // z,t;
hence x,y // t,z & y,x // z,t by Lm2,Lm3;
hence y,x // t,z by Lm2;
thus z,t // x,y by A1,Lm1;
hence z,t // y,x & t,z // x,y by Lm2,Lm3;
hence thesis by Lm3;
end;
theorem Th4:
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 ) implies x,y // z,t
proof
assume that
A1: a<>b and
A2: 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;
A3: a,b // z,t by A2,Th3;
a,b // x,y by A2,Th3;
hence thesis by A1,A3,DIRAF:40;
end;
Lm4: LIN x,y,z implies LIN x,z,y & LIN y,x,z
by DIRAF:40,Th3;
theorem Th5:
LIN x,y,z implies LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x
proof
assume LIN x,y,z;
hence LIN x,z,y & LIN y,x,z by Lm4;
hence LIN y,z,x & LIN z,x,y by Lm4;
hence thesis by Lm4;
end;
theorem Th6:
LIN x,x,y & LIN x,y,y & LIN x,y,x by Th1,Th2;
theorem Th7:
x<>y & LIN x,y,z & LIN x,y,t & LIN x,y,u implies LIN z,t,u
proof
assume that
A1: x<>y and
A2: LIN x,y,z and
A3: LIN x,y,t and
A4: LIN x,y,u;
A5: now
A6: x,y // x,z by A2;
x,y // x,u by A4;
then x,z // x,u by A1,A6,Th4;
then
A7: z,x // z,u by DIRAF:40;
x,y // x,t by A3;
then x,z // x,t by A1,A6,Th4;
then
A8: z,x // z,t by DIRAF:40;
assume x<>z;
then z,t // z,u by A8,A7,Th4;
hence thesis;
end;
x=z implies thesis by A1,A3,A4,Th4;
hence thesis by A5;
end;
theorem Th8:
x<>y & LIN x,y,z & x,y // z,t implies LIN x,y,t
proof
assume that
A1: x<>y and
A2: LIN x,y,z and
A3: x,y // z,t;
now
x,y // x,z by A2;
then x,z // z,t by A1,A3,Th4;
then z,x // z,t by Th3;
then LIN z,x,t;
then
A4: LIN x,z,t by Th5;
assume
A5: z<>x;
A6: LIN x,z,x by Th6;
LIN x,z,y by A2,Th5;
hence thesis by A5,A4,A6,Th7;
end;
hence thesis by A3;
end;
theorem Th9:
LIN x,y,z & LIN x,y,t implies x,y // z,t
proof
assume that
A1: LIN x,y,z and
A2: LIN x,y,t;
now
A3: x,y // x,t by A2;
A4: x,y // x,z by A1;
assume x<>y;
then x,z // x,t by A4,A3,Th4;
then z,x // z,t by DIRAF:40;
then x,z // z,t by Th3;
hence thesis by A4,A3,Th4;
end;
hence thesis by Th2;
end;
theorem Th10:
u<>z & LIN x,y,u & LIN x,y,z & LIN u,z,w implies LIN x,y,w
proof
assume that
A1: u<>z and
A2: LIN x,y,u and
A3: LIN x,y,z and
A4: LIN u,z,w;
now
assume
A5: x<>y;
LIN x,y,x by Th6;
then
A6: LIN z,u,x by A2,A3,A5,Th7;
LIN x,y,y by Th6;
then
A7: LIN z,u,y by A2,A3,A5,Th7;
LIN z,u,w by A4,Th5;
hence thesis by A1,A7,A6,Th7;
end;
hence thesis by Th6;
end;
theorem Th11:
ex x,y,z st not LIN x,y,z
proof
consider x,y,z such that
A1: not x,y // x,z by DIRAF:40;
not LIN x,y,z by A1;
hence thesis;
end;
theorem
x<>y implies ex z st not LIN x,y,z
proof
assume
A1: x<>y;
consider a,b,c such that
A2: not LIN a,b,c by Th11;
assume
A3: not thesis;
then
A4: LIN x,y,b;
A5: LIN x,y,c by A3;
LIN x,y,a by A3;
hence contradiction by A1,A2,A4,A5,Th7;
end;
theorem
not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 implies b=b9
proof
assume that
A1: not LIN o,a,b and
A2: LIN o,b,b9 and
A3: a,b // a,b9;
LIN a,b,b9 by A3;
then
A4: LIN b,b9,a by Th5;
A5: LIN b,b9,b by Th6;
assume
A6: b<>b9;
LIN b,b9,o by A2,Th5;
hence contradiction by A1,A6,A4,A5,Th7;
end;
::
:: Definition of the Line joining two points
::
definition
let AS,a,b;
func Line(a,b) -> Subset of AS means
:Def2:
for x holds x in it iff LIN a,b,x;
existence
proof
defpred P[set] means for y st y = $1 holds LIN a,b,y;
consider X being Subset of AS such that
A1: for x being set holds x in X iff x in the carrier of AS & P[x]
from SUBSET_1:sch 1;
take X;
let x;
thus x in X implies LIN a,b,x by A1;
assume LIN a,b,x;
then for y st y = x holds LIN a,b,y;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of AS such that
A2: for x holds x in X1 iff LIN a,b,x and
A3: for x holds x in X2 iff LIN a,b,x;
for x being object holds x in X1 iff x in X2 by A2,A3;
hence thesis by TARSKI:2;
end;
end;
reserve A,C,D,K for Subset of AS;
Lm5: Line(a,b) c= Line(b,a)
proof
let x be object;
assume
A1: x in Line(a,b);
then reconsider x9=x as Element of AS;
LIN a,b,x9 by A1,Def2;
then LIN b,a,x9 by Th5;
hence x in Line(b,a) by Def2;
end;
definition
let AS,a,b;
redefine func Line(a,b); :: redefines Line (AFF_1, definition)
commutativity
proof let a,b;
A1: Line(b,a) c= Line(a,b) by Lm5;
Line(a,b) c= Line(b,a) by Lm5;
hence thesis by A1,XBOOLE_0:def 10;
end;
end;
theorem Th14:
a in Line(a,b) & b in Line(a,b)
proof
A1: LIN a,b,b by Th6;
LIN a,b,a by Th6;
hence thesis by A1,Def2;
end;
theorem Th15:
c in Line(a,b) & d in Line(a,b) & c <>d implies Line(c,d) c= Line(a,b)
proof
assume that
A1: c in Line(a,b) and
A2: d in Line(a,b) and
A3: c <>d;
A4: LIN a,b,d by A2,Def2;
A5: LIN a,b,c by A1,Def2;
let x be object;
assume
A6: x in Line(c,d);
then reconsider x9=x as Element of AS;
LIN c,d,x9 by A6,Def2;
then LIN a,b,x9 by A3,A5,A4,Th10;
hence x in Line(a,b) by Def2;
end;
theorem Th16:
c in Line(a,b) & d in Line(a,b) & a<>b implies Line(a,b) c= Line (c,d)
proof
assume that
A1: c in Line(a,b) and
A2: d in Line(a,b) and
A3: a<>b;
A4: LIN a,b,d by A2,Def2;
A5: LIN a,b,c by A1,Def2;
let x be object;
assume
A6: x in Line(a,b);
then reconsider x9=x as Element of AS;
LIN a,b,x9 by A6,Def2;
then LIN c,d,x9 by A3,A5,A4,Th7;
hence x in Line(c,d) by Def2;
end;
::
:: Definition of the Line
::
definition let AS,A;
attr A is being_line means :Def3:
ex a,b st a <> b & A = Line(a,b);
end;
registration let AS;
cluster being_line for Subset of AS;
existence
proof
set a = the Element of AS;
consider b being Element of AS such that
A1: a <> b by SUBSET_1:50;
take Line(a,b);
thus thesis by A1;
end;
end;
Lm6: A is being_line & a in A & b in A & a<>b implies A=Line(a,b)
proof
assume that
A1: A is being_line and
A2: a in A and
A3: b in A and
A4: a<>b;
A5: ex p,q st p<>q & A=Line(p,q) by A1;
then
A6: A c= Line(a,b) by A2,A3,Th16;
Line(a,b) c= A by A2,A3,A4,A5,Th15;
hence thesis by A6,XBOOLE_0:def 10;
end;
:: Otrzymujemy stad zasadnicze stwierdzenie, ze kazda prosta
:: jest jednoznacznie wyznaczona przez swoje dowolne dwa punkty.
theorem Th17:
A is being_line & C is being_line & a in A & b in A & a in C & b in C
implies a=b or A=C
proof
assume that
A1: A is being_line and
A2: C is being_line and
A3: a in A and
A4: b in A and
A5: a in C and
A6: b in C;
assume
A7: a<>b;
then A=Line(a,b) by A1,A3,A4,Lm6;
hence thesis by A2,A5,A6,A7,Lm6;
end;
theorem Th18:
A is being_line implies ex a,b st a in A & b in A & a<>b
proof
assume A is being_line;
then consider a,b such that
A1: a<>b and
A2: A=Line(a,b);
A3: b in A by A2,Th14;
a in A by A2,Th14;
hence thesis by A1,A3;
end;
theorem Th19:
A is being_line implies ex b st a<>b & b in A
proof
assume A is being_line;
then consider p,q such that
A1: p in A and
A2: q in A and
A3: p<>q by Th18;
a=p implies a<>q & q in A by A2,A3;
hence thesis by A1;
end;
theorem Th20:
LIN a,b,c iff ex A st A is being_line & a in A & b in A & c in A
proof
A1: LIN a,b,c implies ex A st A is being_line & a in A & b in A & c in A
proof
assume
A2: LIN a,b,c;
A3: now
set A=Line(a,b);
A4: a in A by Th14;
A5: b in A by Th14;
assume a<>b;
then
A6: A is being_line;
c in A by A2,Def2;
hence thesis by A6,A4,A5;
end;
A7: now
set A=Line(a,c);
A8: c in A by Th14;
assume a<>c;
then
A9: A is being_line;
LIN a,c,b by A2,Th5;
then
A10: b in A by Def2;
a in A by Th14;
hence thesis by A9,A10,A8;
end;
now
consider x such that
A11: a<>x by SUBSET_1:50;
set A=Line(a,x);
A12: a in A by Th14;
assume that
A13: a=b and
A14: a=c;
A is being_line by A11;
hence thesis by A13,A14,A12;
end;
hence thesis by A3,A7;
end;
(ex A st A is being_line & a in A & b in A & c in A) implies LIN a,b,c
proof
given A such that
A15: A is being_line and
A16: a in A and
A17: b in A and
A18: c in A;
consider p,q such that
A19: p<>q and
A20: A=Line(p,q) by A15;
A21: LIN p,q,b by A17,A20,Def2;
A22: LIN p,q,c by A18,A20,Def2;
LIN p,q,a by A16,A20,Def2;
hence thesis by A19,A21,A22,Th7;
end;
hence thesis by A1;
end;
::
:: Definition of the parallelity between segments and lines
::
definition
let AS,a,b,A;
pred a,b // A means
ex c,d st c <>d & A=Line(c,d) & a,b // c,d;
end;
definition
let AS,A,C;
pred A // C means
ex a,b st A=Line(a,b) & a<>b & a,b // C;
end;
theorem Th21:
c in Line(a,b) & a<>b implies (d in Line(a,b) iff a,b // c,d)
proof
assume that
A1: c in Line(a,b) and
A2: a<>b;
A3: LIN a,b,c by A1,Def2;
thus d in Line(a,b) implies a,b // c,d
proof
assume d in Line(a,b);
then LIN a,b,d by Def2;
hence thesis by A3,Th9;
end;
assume a,b // c,d;
then LIN a,b,d by A2,A3,Th8;
hence thesis by Def2;
end;
theorem Th22:
A is being_line & a in A implies (b in A iff a,b // A)
proof
assume that
A1: A is being_line and
A2: a in A;
consider p,q such that
A3: p<>q and
A4: A=Line(p,q) by A1;
hereby assume b in A;
then p,q // a,b by A2,A3,A4,Th21;
then a,b // p,q by Th3;
hence a,b // A by A3,A4;
end;
assume a,b // A;
then consider p,q such that
A5: p<>q and
A6: A=Line(p,q) and
A7: a,b // p,q;
p,q // a,b by A7,Th3;
hence b in A by A2,A5,A6,Th21;
end;
theorem
a<>b & A=Line(a,b) iff A is being_line & a in A & b in A & a<>b by Lm6
,Th14;
theorem Th24:
A is being_line & a in A & b in A & a<>b & LIN a,b,x implies x in A
proof
assume that
A1: A is being_line and
A2: a in A and
A3: b in A and
A4: a<>b and
A5: LIN a,b,x;
A=Line(a,b) by A1,A2,A3,A4,Lm6;
hence thesis by A5,Def2;
end;
theorem
(ex a,b st a,b // A) implies A is being_line;
theorem Th26:
c in A & d in A & A is being_line & c <>d implies (a,b // A iff a,b // c,d)
proof
assume that
A1: c in A and
A2: d in A and
A3: A is being_line and
A4: c <>d;
thus a,b // A implies a,b // c,d
proof
assume a,b // A;
then consider p,q such that
A5: p<>q and
A6: A=Line(p,q) and
A7: a,b // p,q;
p,q // c,d by A1,A2,A5,A6,Th21;
hence thesis by A5,A7,Th4;
end;
assume
A8: a,b // c,d;
A=Line(c,d) by A1,A2,A3,A4,Lm6;
hence thesis by A4,A8;
end;
theorem Th27:
a,b // A implies ex c,d st c <>d & c in A & d in A & a,b // c,d
proof
assume a,b // A;
then consider c,d such that
A1: c <>d and
A2: A=Line(c,d) and
A3: a,b // c,d;
A4: d in A by A2,Th14;
c in A by A2,Th14;
hence thesis by A1,A3,A4;
end;
theorem Th28:
a<>b implies a,b // Line(a,b) by Th1;
theorem Th29:
for A be being_line Subset of AS holds
(a,b // A iff ex c,d st c <>d & c in A & d in A & a,b // c,d )
proof
A1: a,b // A implies ex c,d st c <>d & c in A & d in A & a,b // c,d by Th27;
let A be being_line Subset of AS;
(ex c,d st c <>d & c in A & d in A & a,b // c,d) implies a,b // A
proof
assume ex c,d st c <>d & c in A & d in A & a,b // c,d;
then consider c,d such that
A2: c <>d and
A3: c in A and
A4: d in A and
A5: a,b // c,d;
A=Line(c,d) by A2,A3,A4,Lm6;
hence thesis by A2,A5;
end;
hence thesis by A1;
end;
theorem
for A be being_line Subset of AS st a,b // A & c,d // A holds a,b // c,d
proof
let A be being_line Subset of AS;
assume that
A1: a,b // A and
A2: c,d // A;
consider p,q such that
A3: p<>q and
A4: A=Line(p,q) and
A5: a,b // p,q by A1;
A6: q in A by A4,Th14;
p in A by A4,Th14;
then c,d // p,q by A2,A3,A6,Th26;
hence thesis by A3,A5,Th4;
end;
theorem Th31:
a,b // A & a,b // p,q & a<>b implies p,q // A
proof
assume that
A1: a,b // A and
A2: a,b // p,q and
A3: a<>b;
A4: A is being_line by A1;
then consider c,d such that
A5: c <>d and
A6: c in A and
A7: d in A and
A8: a,b // c,d by A1,Th29;
p,q // c,d by A2,A3,A8,Th4;
hence thesis by A4,A5,A6,A7,Th29;
end;
theorem Th32:
for A be being_line Subset of AS holds a,a // A
proof
let A be being_line Subset of AS;
consider p,q such that
A1: p<>q and
A2: A=Line(p,q) by Def3;
a,a // p,q by Th2;
hence thesis by A1,A2;
end;
theorem Th33:
a,b // A implies b,a // A
proof
assume
A1: a,b // A;
a<>b implies thesis by A1,Th1,Th31;
hence thesis by A1;
end;
theorem
a,b // A & not a in A implies not b in A
proof
assume that
A1: a,b // A and
A2: not a in A and
A3: b in A;
A4: b,a // A by A1,Th33;
A is being_line by A1;
hence contradiction by A2,A3,A4,Th22;
end;
theorem Th35:
A // C implies A is being_line & C is being_line
proof
assume A // C;
then ex a,b st A=Line(a,b) & a<>b & a,b // C;
hence thesis;
end;
theorem Th36:
A // C iff ex a,b,c,d st a<>b & c <>d & a,b // c,d & A=Line(a,b)
& C=Line(c,d)
proof
thus A // C implies
ex a,b,c,d st a<>b & c <>d & a,b // c,d & A=Line(a,b) & C=Line(c,d)
proof
assume A // C;
then consider a,b such that
A1: A=Line(a,b) and
A2: a<>b and
A3: a,b // C;
ex c,d st c <>d & C=Line(c,d) & a,b // c,d by A3;
hence thesis by A1,A2;
end;
given a,b,c,d such that
A4: a<>b and
A5: c <>d and
A6: a,b // c,d and
A7: A=Line(a,b) and
A8: C=Line(c,d);
a,b // C by A5,A6,A8;
hence thesis by A4,A7;
end;
theorem Th37:
for A, C be 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)
proof
let A, C be being_line Subset of AS;
assume that
A1: a in A and
A2: b in A and
A3: c in C and
A4: d in C and
A5: a<>b and
A6: c <>d;
thus A // C implies a,b // c,d
proof
assume A // C;
then consider p,q,r,s such that
A7: p<>q and
A8: r<>s and
A9: p,q // r,s and
A10: A=Line(p,q) and
A11: C=Line(r,s) by Th36;
p,q // a,b by A1,A2,A7,A10,Th21; then
A12: a,b // r,s by A7,A9,Th4;
r,s // c,d by A3,A4,A8,A11,Th21;
hence thesis by A8,A12,Th4;
end;
A13: C=Line(c,d) by A3,A4,A6,Lm6;
assume
A14: a,b // c,d;
A=Line(a,b) by A1,A2,A5,Lm6;
hence thesis by A5,A6,A14,A13,Th36;
end;
theorem Th38:
a in A & b in A & c in C & d in C & A // C implies a,b // c,d
proof
assume that
A1: a in A and
A2: b in A and
A3: c in C and
A4: d in C and
A5: A // C;
now
A6: C is being_line by A5,Th35;
assume that
A7: a<>b and
A8: c <>d;
A is being_line by A5;
hence thesis by A1,A2,A3,A4,A5,A7,A8,A6,Th37;
end;
hence thesis by Th2;
end;
theorem
a in A & b in A & A // C implies a,b // C
proof
assume that
A1: a in A and
A2: b in A and
A3: A // C;
A4: C is being_line by A3,Th35;
now
consider p,q such that
A5: p in C and
A6: q in C and
A7: p<>q by A4,Th18;
A8: C=Line(p,q) by A4,A5,A6,A7,Lm6;
a,b // p,q by A1,A2,A3,A5,A6,Th38;
hence thesis by A7,A8;
end;
hence thesis;
end;
theorem Th40:
for A being being_line Subset of AS holds A // A
proof
let A be being_line Subset of AS;
consider a,b such that
A1: a<>b and
A2: A=Line(a,b) by Def3;
a,b // a,b by Th1;
hence thesis by A1,A2,Th36;
end;
definition let AS; let A,B be being_line Subset of AS;
redefine pred A // B; :: redefines // (AFF_1, definition)
reflexivity by Th40;
end;
theorem Th41:
A // C implies C // A
proof
assume A // C;
then consider a,b,c,d such that
A1: a<>b and
A2: c <>d and
A3: a,b // c,d and
A4: A=Line(a,b) and
A5: C=Line(c,d) by Th36;
c,d // a,b by A3,Th3;
hence thesis by A1,A2,A4,A5,Th36;
end;
definition let AS,A,C;
redefine pred A // C; :: redefines // (AFF_1, definition)
symmetry by Th41;
end;
theorem Th42:
a,b // A & A // C implies a,b // C
proof
assume that
A1: a,b // A and
A2: A // C;
consider p,q,c,d such that
A3: p<>q and
A4: c <>d and
A5: p,q // c,d and
A6: A=Line(p,q) and
A7: C=Line(c,d) by A2,Th36;
A8: q in A by A6,Th14;
A9: A is being_line by A2;
p in A by A6,Th14;
then a,b // p,q by A1,A3,A8,A9,Th26;
then a,b // c,d by A3,A5,Th4;
hence thesis by A4,A7;
end;
Lm7: A // C & C // D implies A // D
proof
assume that
A1: A // C and
A2: C // D;
consider a,b,c,d such that
A3: a<>b and
A4: c <>d and
A5: a,b // c,d and
A6: A=Line(a,b) and
A7: C=Line(c,d) by A1,Th36;
A8: C is being_line by A2;
A9: d in C by A7,Th14;
A10: D is being_line by A2,Th35;
then consider p,q such that
A11: p<>q and
A12: D=Line(p,q);
A13: p in D by A12,Th14;
A14: q in D by A12,Th14;
c in C by A7,Th14;
then c,d // p,q by A2,A4,A8,A10,A11,A13,A14,A9,Th37;
then a,b // p,q by A4,A5,Th4;
hence thesis by A3,A6,A11,A12,Th36;
end;
theorem
( A // C & C // D or A // C & D // C or C // A & C // D or C // A & D
// C ) implies A // D by Lm7;
theorem Th44:
A // C & p in A & p in C implies A=C
proof
assume that
A1: A // C and
A2: p in A and
A3: p in C;
A4: for A,C,p holds A // C & p in A & p in C implies A c= C
proof
let A,C,p;
assume that
A5: A // C and
A6: p in A and
A7: p in C;
A8: C is being_line by A5,Th35;
A9: A is being_line by A5;
let x be object;
assume
A10: x in A;
then reconsider x9=x as Element of AS;
now
consider q such that
A11: p<>q and
A12: q in C by A8,Th19;
assume
A13: x9<>p;
then A=Line(p,x9) by A6,A9,A10,Lm6;
then p,x9 // C by A5,A13,Th28,Th42;
then p,x9 // p,q by A7,A8,A11,A12,Th26;
then p,q // p,x9 by Th3;
then
A14: LIN p,q,x9;
C=Line(p,q) by A7,A8,A11,A12,Lm6;
hence x in C by A14,Def2;
end;
hence x in C by A7;
end;
then
A15: C c= A by A1,A2,A3;
A c= C by A1,A2,A3,A4;
hence thesis by A15,XBOOLE_0:def 10;
end;
theorem
x in K & not a in K & a,b // K implies (a=b or not LIN x,a,b)
proof
assume that
A1: x in K and
A2: not a in K and
A3: a,b // K;
set A=Line(a,b);
assume that
A4: a<>b and
A5: LIN x,a,b;
LIN a,b,x by A5,Th5;
then
A6: x in A by Def2;
A7: a in A by Th14;
A // K by A3,A4;
hence contradiction by A1,A2,A6,A7,Th44;
end;
theorem
a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a=b
implies a9=b9
proof
assume that
A1: a9,b9 // K and
A2: LIN p,a,a9 and
A3: LIN p,b,b9 and
A4: p in K and
A5: not a in K and
A6: a=b;
set A=Line(p,a);
A7: b9 in A by A3,A6,Def2;
A8: p in A by Th14;
A9: a9 in A by A2,Def2;
assume
A10: a9<>b9;
A is being_line by A4,A5;
then A=Line(a9,b9) by A9,A7,A10,Lm6;
then A // K by A1,A10;
then A=K by A4,A8,Th44;
hence contradiction by A5,Th14;
end;
theorem
for A be 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
proof
let A be being_line Subset of AS;
assume that
A1: a in A and
A2: b in A and
A3: c in A and
A4: a<>b and
A5: a,b // c,d;
now
set C=Line(c,d);
A6: c in C by Th14;
A7: d in C by Th14;
assume
A8: c <>d;
then C is being_line;
then A // C by A1,A2,A4,A5,A8,A6,A7,Th37;
hence thesis by A3,A6,A7,Th44;
end;
hence thesis by A3;
end;
theorem
for A be being_line Subset of AS ex C st a in C & A // C
proof
let A be being_line Subset of AS;
consider p,q such that
A1: p<>q and
A2: A=Line(p,q) by Def3;
consider b such that
A3: p,q // a,b and
A4: a<>b by DIRAF:40;
set C=Line(a,b);
A5: a in C by Th14;
A // C by A1,A2,A3,A4,Th36;
hence thesis by A5;
end;
theorem
A // C & A // D & p in C & p in D implies C=D by Lm7,Th44;
::
:: Additional theorems
::
theorem
A is being_line & a in A & b in A & c in A & d in A implies a,b // c,d
by Th38,Th40;
theorem
A is being_line & a in A & b in A implies a,b // A by Th22;
theorem
a,b // A & a,b // C & a<>b implies A // C
proof
assume that
A1: a,b // A and
A2: a,b // C and
A3: a<>b;
A4: C is being_line by A2;
then consider p,q such that
A5: p<>q and
A6: p in C and
A7: q in C and
A8: a,b // p,q by A2,Th29;
A9: A is being_line by A1;
then consider c,d such that
A10: c <>d and
A11: c in A and
A12: d in A and
A13: a,b // c,d by A1,Th29;
c,d // p,q by A3,A13,A8,Th4;
hence thesis by A9,A4,A10,A11,A12,A5,A6,A7,Th37;
end;
theorem Th53:
not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9=b9 implies a9=o & b9=o
proof
assume that
A1: not LIN o,a,b and
A2: LIN o,a,a9 and
A3: LIN o,b,b9 and
A4: a9=b9;
set A=Line(o,a), C=Line(o,b);
A5: o in A by Th14;
A6: o<>b by A1,Th6;
then
A7: C is being_line;
A8: o<>a by A1,Th6;
then
A9: A is being_line;
A10: a in A by Th14;
then
A11: a9 in A by A2,A8,A9,A5,Th24;
A12: b in C by Th14;
A13: o in C by Th14;
then
A14: b9 in C by A3,A6,A7,A12,Th24;
A<>C by A1,A9,A5,A10,A12,Th20;
hence thesis by A4,A9,A7,A5,A13,A14,A11,Th17;
end;
theorem Th54:
not LIN o,a,b & LIN o,b,b9 & a,b // a9,b9 & a9=o implies b9=o
proof
assume that
A1: not LIN o,a,b and
A2: LIN o,b,b9 and
A3: a,b // a9,b9 and
A4: a9=o;
A5: now
assume a,b // a9,b;
then b,a // b,a9 by Th3;
then LIN b,a,a9;
hence contradiction by A1,A4,Th5;
end;
a9,b // a9,b9 by A2,A4;
hence thesis by A3,A4,A5,Th4;
end;
theorem
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 implies b9=x
proof
assume that
A1: not LIN o,a,b and
A2: LIN o,a,a9 and
A3: LIN o,b,b9 and
A4: LIN o,b,x and
A5: a,b // a9,b9 and
A6: a,b // a9,x;
set A=Line(o,a), C=Line(o,b), P=Line(a9,b9);
A7: a9 in P by Th14;
assume
A8: b9<>x;
A9: a9<>b9
proof
assume
A10: a9=b9;
then a9=o by A1,A2,A3,Th53;
hence contradiction by A1,A4,A6,A8,A10,Th54;
end;
then
A11: P is being_line;
A12: o<>b by A1,Th6;
then
A13: C is being_line;
A14: b9 in P by Th14;
a<>b by A1,Th6;
then a9,b9 // a9,x by A5,A6,Th4;
then LIN a9,b9,x;
then
A15: x in P by A9,A11,A7,A14,Th24;
A16: b in C by Th14;
A17: o in C by Th14;
then
A18: x in C by A4,A12,A13,A16,Th24;
b9 in C by A3,A12,A13,A17,A16,Th24;
then
A19: a9 in C by A8,A13,A11,A7,A14,A18,A15,Th17;
A20: o<>a by A1,Th6;
then
A21: A is being_line;
A22: a9<>o
proof
assume
A23: a9=o;
then b9=o by A1,A3,A5,Th54;
hence contradiction by A1,A4,A6,A8,A23,Th54;
end;
A24: o in A by Th14;
A25: a in A by Th14;
then a9 in A by A2,A20,A21,A24,Th24;
then b in A by A22,A21,A13,A24,A17,A16,A19,Th17;
hence contradiction by A1,A21,A24,A25,Th20;
end;
theorem
for a,b,A holds A is being_line & a in A & b in A & a<>b implies
A = Line(a,b) by Lm6;
::
:: Facts about Affine Plane
::
reserve AP for AffinPlane;
reserve a,b,c,d,x,p,q for Element of AP;
reserve A,C for Subset of AP;
theorem Th57:
A is being_line & C is being_line & not A // C implies
ex x st x in A & x in C
proof
assume that
A1: A is being_line and
A2: C is being_line and
A3: not A // C;
consider a,b such that
A4: a<>b and
A5: A=Line(a,b) by A1;
consider c,d such that
A6: c <>d and
A7: C=Line(c,d) by A2;
not a,b // c,d by A3,A4,A5,A6,A7,Th36;
then consider x such that
A8: a,b // a,x and
A9: c,d // c,x by DIRAF:46;
LIN c,d,x by A9;
then
A10: x in C by A7,Def2;
LIN a,b,x by A8;
then x in A by A5,Def2;
hence thesis by A10;
end;
theorem
A is being_line & not a,b // A implies ex x st x in A & LIN a,b,x
proof
assume that
A1: A is being_line and
A2: not a,b // A;
set C=Line(a,b);
A3: not C // A
proof
A4: b in C by Th14;
assume C // A;
then consider p,q such that
A5: C=Line(p,q) and
A6: p<>q and
A7: p,q // A;
a in C by Th14;
then p,q // a,b by A5,A6,A4,Th21;
hence contradiction by A2,A6,A7,Th31;
end;
a<>b by A1,A2,Th32;
then C is being_line;
then consider x such that
A8: x in C and
A9: x in A by A1,A3,Th57;
LIN a,b,x by A8,Def2;
hence thesis by A9;
end;
theorem
not a,b // c,d implies ex p st LIN a,b,p & LIN c,d,p
proof
assume not a,b // c,d;
then consider p such that
A1: a,b // a,p and
A2: c,d // c,p by DIRAF:46;
A3: LIN c,d,p by A2;
LIN a,b,p by A1;
hence thesis by A3;
end;