:: Axioms of Incidence
:: by Wojciech A. Trybulec
::
:: Copyright (c) 1990-2021 Association of Mizar Users

definition
attr c1 is strict ;
struct IncProjStr -> ;
aggr IncProjStr(# Points, Lines, Inc #) -> IncProjStr ;
sel Points c1 -> non empty set ;
sel Lines c1 -> non empty set ;
sel Inc c1 -> Relation of the Points of c1, the Lines of c1;
end;

definition
attr c1 is strict ;
struct IncStruct -> IncProjStr ;
aggr IncStruct(# Points, Lines, Planes, Inc, Inc2, Inc3 #) -> IncStruct ;
sel Planes c1 -> non empty set ;
sel Inc2 c1 -> Relation of the Points of c1, the Planes of c1;
sel Inc3 c1 -> Relation of the Lines of c1, the Planes of c1;
end;

definition
let S be IncProjStr ;
mode POINT of S is Element of the Points of S;
mode LINE of S is Element of the Lines of S;
end;

definition
let S be IncStruct ;
mode PLANE of S is Element of the Planes of S;
end;

:: Definitions of predicates 'on' and attributes 'linear', 'planar'
definition
let S be IncProjStr ;
let A be POINT of S;
let L be LINE of S;
pred A on L means :: INCSP_1:def 1
[A,L] in the Inc of S;
end;

:: deftheorem defines on INCSP_1:def 1 :
for S being IncProjStr
for A being POINT of S
for L being LINE of S holds
( A on L iff [A,L] in the Inc of S );

definition
let S be IncStruct ;
let A be POINT of S;
let P be PLANE of S;
pred A on P means :: INCSP_1:def 2
[A,P] in the Inc2 of S;
end;

:: deftheorem defines on INCSP_1:def 2 :
for S being IncStruct
for A being POINT of S
for P being PLANE of S holds
( A on P iff [A,P] in the Inc2 of S );

definition
let S be IncStruct ;
let L be LINE of S;
let P be PLANE of S;
pred L on P means :: INCSP_1:def 3
[L,P] in the Inc3 of S;
end;

:: deftheorem defines on INCSP_1:def 3 :
for S being IncStruct
for L being LINE of S
for P being PLANE of S holds
( L on P iff [L,P] in the Inc3 of S );

definition
let S be IncProjStr ;
let F be Subset of the Points of S;
let L be LINE of S;
pred F on L means :: INCSP_1:def 4
for A being POINT of S st A in F holds
A on L;
end;

:: deftheorem defines on INCSP_1:def 4 :
for S being IncProjStr
for F being Subset of the Points of S
for L being LINE of S holds
( F on L iff for A being POINT of S st A in F holds
A on L );

definition
let S be IncStruct ;
let F be Subset of the Points of S;
let P be PLANE of S;
pred F on P means :: INCSP_1:def 5
for A being POINT of S st A in F holds
A on P;
end;

:: deftheorem defines on INCSP_1:def 5 :
for S being IncStruct
for F being Subset of the Points of S
for P being PLANE of S holds
( F on P iff for A being POINT of S st A in F holds
A on P );

definition
let S be IncProjStr ;
let F be Subset of the Points of S;
attr F is linear means :: INCSP_1:def 6
ex L being LINE of S st F on L;
end;

:: deftheorem defines linear INCSP_1:def 6 :
for S being IncProjStr
for F being Subset of the Points of S holds
( F is linear iff ex L being LINE of S st F on L );

definition
let S be IncStruct ;
let F be Subset of the Points of S;
attr F is planar means :: INCSP_1:def 7
ex P being PLANE of S st F on P;
end;

:: deftheorem defines planar INCSP_1:def 7 :
for S being IncStruct
for F being Subset of the Points of S holds
( F is planar iff ex P being PLANE of S st F on P );

theorem Th1: :: INCSP_1:1
for S being IncProjStr
for L being LINE of S
for A, B being POINT of S holds
( {A,B} on L iff ( A on L & B on L ) )
proof end;

theorem Th2: :: INCSP_1:2
for S being IncProjStr
for L being LINE of S
for A, B, C being POINT of S holds
( {A,B,C} on L iff ( A on L & B on L & C on L ) )
proof end;

theorem Th3: :: INCSP_1:3
for S being IncStruct
for A, B being POINT of S
for P being PLANE of S holds
( {A,B} on P iff ( A on P & B on P ) )
proof end;

theorem Th4: :: INCSP_1:4
for S being IncStruct
for A, B, C being POINT of S
for P being PLANE of S holds
( {A,B,C} on P iff ( A on P & B on P & C on P ) )
proof end;

theorem Th5: :: INCSP_1:5
for S being IncStruct
for A, B, C, D being POINT of S
for P being PLANE of S holds
( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )
proof end;

theorem Th6: :: INCSP_1:6
for S being IncStruct
for L being LINE of S
for F, G being Subset of the Points of S st G c= F & F on L holds
G on L ;

theorem Th7: :: INCSP_1:7
for S being IncStruct
for P being PLANE of S
for F, G being Subset of the Points of S st G c= F & F on P holds
G on P ;

theorem Th8: :: INCSP_1:8
for S being IncStruct
for A being POINT of S
for L being LINE of S
for F being Subset of the Points of S holds
( ( F on L & A on L ) iff F \/ {A} on L )
proof end;

theorem Th9: :: INCSP_1:9
for S being IncStruct
for A being POINT of S
for P being PLANE of S
for F being Subset of the Points of S holds
( ( F on P & A on P ) iff F \/ {A} on P )
proof end;

theorem Th10: :: INCSP_1:10
for S being IncStruct
for L being LINE of S
for F, G being Subset of the Points of S holds
( F \/ G on L iff ( F on L & G on L ) )
proof end;

theorem Th11: :: INCSP_1:11
for S being IncStruct
for P being PLANE of S
for F, G being Subset of the Points of S holds
( F \/ G on P iff ( F on P & G on P ) )
proof end;

theorem :: INCSP_1:12
for S being IncStruct
for F, G being Subset of the Points of S st G c= F & F is linear holds
G is linear
proof end;

theorem :: INCSP_1:13
for S being IncStruct
for F, G being Subset of the Points of S st G c= F & F is planar holds
G is planar
proof end;

:: Introduction of mode IncSpace
definition
let S be IncProjStr ;
attr S is with_non-trivial_lines means :Def8: :: INCSP_1:def 8
for L being LINE of S ex A, B being POINT of S st
( A <> B & {A,B} on L );
attr S is linear means :Def9: :: INCSP_1:def 9
for A, B being POINT of S ex L being LINE of S st {A,B} on L;
attr S is up-2-rank means :Def10: :: INCSP_1:def 10
for A, B being POINT of S
for K, L being LINE of S st A <> B & {A,B} on K & {A,B} on L holds
K = L;
end;

:: deftheorem Def8 defines with_non-trivial_lines INCSP_1:def 8 :
for S being IncProjStr holds
( S is with_non-trivial_lines iff for L being LINE of S ex A, B being POINT of S st
( A <> B & {A,B} on L ) );

:: deftheorem Def9 defines linear INCSP_1:def 9 :
for S being IncProjStr holds
( S is linear iff for A, B being POINT of S ex L being LINE of S st {A,B} on L );

:: deftheorem Def10 defines up-2-rank INCSP_1:def 10 :
for S being IncProjStr holds
( S is up-2-rank iff for A, B being POINT of S
for K, L being LINE of S st A <> B & {A,B} on K & {A,B} on L holds
K = L );

definition
let S be IncStruct ;
attr S is with_non-empty_planes means :Def11: :: INCSP_1:def 11
for P being PLANE of S ex A being POINT of S st A on P;
attr S is planar means :Def12: :: INCSP_1:def 12
for A, B, C being POINT of S ex P being PLANE of S st {A,B,C} on P;
attr S is with_<=1_plane_per_3_pts means :Def13: :: INCSP_1:def 13
for A, B, C being POINT of S
for P, Q being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q holds
P = Q;
attr S is with_lines_inside_planes means :Def14: :: INCSP_1:def 14
for L being LINE of S
for P being PLANE of S st ex A, B being POINT of S st
( A <> B & {A,B} on L & {A,B} on P ) holds
L on P;
attr S is with_planes_intersecting_in_2_pts means :Def15: :: INCSP_1:def 15
for A being POINT of S
for P, Q being PLANE of S st A on P & A on Q holds
ex B being POINT of S st
( A <> B & B on P & B on Q );
attr S is up-3-dimensional means :Def16: :: INCSP_1:def 16
not for A, B, C, D being POINT of S holds {A,B,C,D} is planar ;
attr S is inc-compatible means :Def17: :: INCSP_1:def 17
for A being POINT of S
for L being LINE of S
for P being PLANE of S st A on L & L on P holds
A on P;
end;

:: deftheorem Def11 defines with_non-empty_planes INCSP_1:def 11 :
for S being IncStruct holds
( S is with_non-empty_planes iff for P being PLANE of S ex A being POINT of S st A on P );

:: deftheorem Def12 defines planar INCSP_1:def 12 :
for S being IncStruct holds
( S is planar iff for A, B, C being POINT of S ex P being PLANE of S st {A,B,C} on P );

:: deftheorem Def13 defines with_<=1_plane_per_3_pts INCSP_1:def 13 :
for S being IncStruct holds
( S is with_<=1_plane_per_3_pts iff for A, B, C being POINT of S
for P, Q being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q holds
P = Q );

:: deftheorem Def14 defines with_lines_inside_planes INCSP_1:def 14 :
for S being IncStruct holds
( S is with_lines_inside_planes iff for L being LINE of S
for P being PLANE of S st ex A, B being POINT of S st
( A <> B & {A,B} on L & {A,B} on P ) holds
L on P );

:: deftheorem Def15 defines with_planes_intersecting_in_2_pts INCSP_1:def 15 :
for S being IncStruct holds
( S is with_planes_intersecting_in_2_pts iff for A being POINT of S
for P, Q being PLANE of S st A on P & A on Q holds
ex B being POINT of S st
( A <> B & B on P & B on Q ) );

:: deftheorem Def16 defines up-3-dimensional INCSP_1:def 16 :
for S being IncStruct holds
( S is up-3-dimensional iff not for A, B, C, D being POINT of S holds {A,B,C,D} is planar );

:: deftheorem Def17 defines inc-compatible INCSP_1:def 17 :
for S being IncStruct holds
( S is inc-compatible iff for A being POINT of S
for L being LINE of S
for P being PLANE of S st A on L & L on P holds
A on P );

definition
let IT be IncStruct ;
attr IT is IncSpace-like means :: INCSP_1:def 18
( IT is with_non-trivial_lines & IT is linear & IT is up-2-rank & IT is with_non-empty_planes & IT is planar & IT is with_<=1_plane_per_3_pts & IT is with_lines_inside_planes & IT is with_planes_intersecting_in_2_pts & IT is up-3-dimensional & IT is inc-compatible );
end;

:: deftheorem defines IncSpace-like INCSP_1:def 18 :
for IT being IncStruct holds
( IT is IncSpace-like iff ( IT is with_non-trivial_lines & IT is linear & IT is up-2-rank & IT is with_non-empty_planes & IT is planar & IT is with_<=1_plane_per_3_pts & IT is with_lines_inside_planes & IT is with_planes_intersecting_in_2_pts & IT is up-3-dimensional & IT is inc-compatible ) );

registration
coherence
for b1 being IncStruct st b1 is IncSpace-like holds
( b1 is with_non-trivial_lines & b1 is linear & b1 is up-2-rank & b1 is with_non-empty_planes & b1 is planar & b1 is with_<=1_plane_per_3_pts & b1 is with_lines_inside_planes & b1 is with_planes_intersecting_in_2_pts & b1 is up-3-dimensional & b1 is inc-compatible )
;
end;

registration
existence
ex b1 being IncStruct st
( b1 is strict & b1 is IncSpace-like )
proof end;
end;

definition end;

:: Axioms of Incidence
theorem Th14: :: INCSP_1:14
for S being IncSpace
for L being LINE of S
for P being PLANE of S
for F being Subset of the Points of S st F on L & L on P holds
F on P by Def17;

:: Collinearity of points & coplanarity of points & lines
theorem Th15: :: INCSP_1:15
for S being IncSpace
for A, B being POINT of S holds {A,A,B} is linear
proof end;

theorem Th16: :: INCSP_1:16
for S being IncSpace
for A, B, C being POINT of S holds {A,A,B,C} is planar
proof end;

theorem Th17: :: INCSP_1:17
for S being IncSpace
for A, B, C, D being POINT of S st {A,B,C} is linear holds
{A,B,C,D} is planar
proof end;

theorem Th18: :: INCSP_1:18
for S being IncSpace
for A, B, C being POINT of S
for L being LINE of S st A <> B & {A,B} on L & not C on L holds
not {A,B,C} is linear
proof end;

theorem Th19: :: INCSP_1:19
for S being IncSpace
for A, B, C, D being POINT of S
for P being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & not D on P holds
not {A,B,C,D} is planar
proof end;

theorem :: INCSP_1:20
for S being IncSpace
for K, L being LINE of S st ( for P being PLANE of S holds
( not K on P or not L on P ) ) holds
K <> L
proof end;

Lm1: for S being IncSpace
for A being POINT of S
for L being LINE of S ex B being POINT of S st
( A <> B & B on L )

proof end;

theorem :: INCSP_1:21
for S being IncSpace
for L, L1, L2 being LINE of S st ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st
( A on L & A on L1 & A on L2 ) holds
L <> L1
proof end;

theorem :: INCSP_1:22
for S being IncSpace
for L, L1, L2 being LINE of S
for P being PLANE of S st L1 on P & L2 on P & not L on P & L1 <> L2 holds
for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q )
proof end;

:: Lines & planes
theorem Th23: :: INCSP_1:23
for S being IncSpace
for K, L being LINE of S st ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
( K on P & L on P )
proof end;

theorem :: INCSP_1:24
for S being IncSpace
for A, B being POINT of S st A <> B holds
ex L being LINE of S st
for K being LINE of S holds
( {A,B} on K iff K = L )
proof end;

theorem :: INCSP_1:25
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
ex P being PLANE of S st
for Q being PLANE of S holds
( {A,B,C} on Q iff P = Q )
proof end;

theorem Th26: :: INCSP_1:26
for S being IncSpace
for A being POINT of S
for L being LINE of S st not A on L holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
proof end;

theorem Th27: :: INCSP_1:27
for S being IncSpace
for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q )
proof end;

:: Definitions of functions: Line, Plane
definition
let S be IncSpace;
let A, B be POINT of S;
assume A1: A <> B ;
func Line (A,B) -> LINE of S means :Def19: :: INCSP_1:def 19
{A,B} on it;
correctness
existence
ex b1 being LINE of S st {A,B} on b1
;
uniqueness
for b1, b2 being LINE of S st {A,B} on b1 & {A,B} on b2 holds
b1 = b2
;
by ;
end;

:: deftheorem Def19 defines Line INCSP_1:def 19 :
for S being IncSpace
for A, B being POINT of S st A <> B holds
for b4 being LINE of S holds
( b4 = Line (A,B) iff {A,B} on b4 );

definition
let S be IncSpace;
let A, B, C be POINT of S;
assume A1: not {A,B,C} is linear ;
func Plane (A,B,C) -> PLANE of S means :Def20: :: INCSP_1:def 20
{A,B,C} on it;
correctness
existence
ex b1 being PLANE of S st {A,B,C} on b1
;
uniqueness
for b1, b2 being PLANE of S st {A,B,C} on b1 & {A,B,C} on b2 holds
b1 = b2
;
by ;
end;

:: deftheorem Def20 defines Plane INCSP_1:def 20 :
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
for b5 being PLANE of S holds
( b5 = Plane (A,B,C) iff {A,B,C} on b5 );

definition
let S be IncSpace;
let A be POINT of S;
let L be LINE of S;
assume A1: not A on L ;
func Plane (A,L) -> PLANE of S means :Def21: :: INCSP_1:def 21
( A on it & L on it );
existence
ex b1 being PLANE of S st
( A on b1 & L on b1 )
proof end;
uniqueness
for b1, b2 being PLANE of S st A on b1 & L on b1 & A on b2 & L on b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines Plane INCSP_1:def 21 :
for S being IncSpace
for A being POINT of S
for L being LINE of S st not A on L holds
for b4 being PLANE of S holds
( b4 = Plane (A,L) iff ( A on b4 & L on b4 ) );

definition
let S be IncSpace;
let K, L be LINE of S;
assume that
A1: K <> L and
A2: ex A being POINT of S st
( A on K & A on L ) ;
func Plane (K,L) -> PLANE of S means :Def22: :: INCSP_1:def 22
( K on it & L on it );
existence
ex b1 being PLANE of S st
( K on b1 & L on b1 )
by ;
uniqueness
for b1, b2 being PLANE of S st K on b1 & L on b1 & K on b2 & L on b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines Plane INCSP_1:def 22 :
for S being IncSpace
for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
for b4 being PLANE of S holds
( b4 = Plane (K,L) iff ( K on b4 & L on b4 ) );

:: Definitional theorems of functions: Line, Plane
theorem :: INCSP_1:28
for S being IncSpace
for A, B being POINT of S st A <> B holds
Line (A,B) = Line (B,A)
proof end;

theorem Th29: :: INCSP_1:29
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (A,C,B)
proof end;

theorem Th30: :: INCSP_1:30
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (B,A,C)
proof end;

theorem :: INCSP_1:31
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (B,C,A)
proof end;

theorem Th32: :: INCSP_1:32
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,A,B)
proof end;

theorem :: INCSP_1:33
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,B,A)
proof end;

theorem :: INCSP_1:34
for S being IncSpace
for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
Plane (K,L) = Plane (L,K)
proof end;

theorem Th35: :: INCSP_1:35
for S being IncSpace
for A, B, C being POINT of S st A <> B & C on Line (A,B) holds
{A,B,C} is linear
proof end;

theorem :: INCSP_1:36
for S being IncSpace
for A, B, C being POINT of S st A <> B & A <> C & {A,B,C} is linear holds
Line (A,B) = Line (A,C)
proof end;

theorem :: INCSP_1:37
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,(Line (A,B)))
proof end;

theorem :: INCSP_1:38
for S being IncSpace
for A, B, C, D being POINT of S st not {A,B,C} is linear & D on Plane (A,B,C) holds
{A,B,C,D} is planar
proof end;

theorem :: INCSP_1:39
for S being IncSpace
for A, B, C being POINT of S
for L being LINE of S st not C on L & {A,B} on L & A <> B holds
Plane (C,L) = Plane (A,B,C)
proof end;

theorem :: INCSP_1:40
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane ((Line (A,B)),(Line (A,C)))
proof end;

Lm2: for S being IncSpace
for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )

proof end;

:: The fourth axiom of incidence
theorem Th41: :: INCSP_1:41
for S being IncSpace
for P being PLANE of S ex A, B, C being POINT of S st
( {A,B,C} on P & not {A,B,C} is linear )
proof end;

:: Fundamental existence theorems
theorem :: INCSP_1:42
for S being IncSpace
for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by Lm2;

theorem :: INCSP_1:43
for S being IncSpace
for A being POINT of S
for L being LINE of S ex B being POINT of S st
( A <> B & B on L ) by Lm1;

theorem Th44: :: INCSP_1:44
for S being IncSpace
for A, B being POINT of S
for P being PLANE of S st A <> B holds
ex C being POINT of S st
( C on P & not {A,B,C} is linear )
proof end;

theorem Th45: :: INCSP_1:45
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
ex D being POINT of S st not {A,B,C,D} is planar
proof end;

theorem Th46: :: INCSP_1:46
for S being IncSpace
for A being POINT of S
for P being PLANE of S ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )
proof end;

theorem Th47: :: INCSP_1:47
for S being IncSpace
for A, B being POINT of S st A <> B holds
ex C, D being POINT of S st not {A,B,C,D} is planar
proof end;

theorem :: INCSP_1:48
for S being IncSpace
for A being POINT of S holds
not for B, C, D being POINT of S holds {A,B,C,D} is planar
proof end;

theorem :: INCSP_1:49
for S being IncSpace
for A being POINT of S
for P being PLANE of S ex L being LINE of S st
( not A on L & L on P )
proof end;

theorem Th50: :: INCSP_1:50
for S being IncSpace
for A being POINT of S
for P being PLANE of S st A on P holds
ex L, L1, L2 being LINE of S st
( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )
proof end;

theorem :: INCSP_1:51
for S being IncSpace
for A being POINT of S ex L, L1, L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
proof end;

theorem :: INCSP_1:52
for S being IncSpace
for A being POINT of S
for L being LINE of S ex P being PLANE of S st
( A on P & not L on P )
proof end;

theorem :: INCSP_1:53
for S being IncSpace
for L being LINE of S
for P being PLANE of S ex A being POINT of S st
( A on P & not A on L )
proof end;

theorem :: INCSP_1:54
for S being IncSpace
for L being LINE of S ex K being LINE of S st
for P being PLANE of S holds
( not L on P or not K on P )
proof end;

theorem :: INCSP_1:55
for S being IncSpace
for L being LINE of S ex P, Q being PLANE of S st
( P <> Q & L on P & L on Q )
proof end;

:: Intersection of lines and planes
theorem :: INCSP_1:56
for S being IncSpace
for A, B being POINT of S
for L being LINE of S
for P being PLANE of S st not L on P & {A,B} on L & {A,B} on P holds
A = B by Def14;

theorem :: INCSP_1:57
for S being IncSpace
for P, Q being PLANE of S holds
( not P <> Q or for A being POINT of S holds
( not A on P or not A on Q ) or ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L ) )
proof end;