PROJRED1: Incidence Projective Space (a reduction theorem in a plane)

:: Incidence Projective Space (a reduction theorem in a plane)
:: by Eugeniusz Kusak and Wojciech Leo\'nczuk
::
:: Received October 16, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th1: :: PROJRED1:1

for IPP being IncProjSp
for A being LINE of IPP holds
not for a being POINT of IPP holds a on A

proof end;

theorem Th2: :: PROJRED1:2

for IPP being IncProjSp
for a being POINT of IPP holds
not for A being LINE of IPP holds a on A

proof end;

theorem Th3: :: PROJRED1:3

for IPP being IncProjSp
for A, B being LINE of IPP st A <> B holds
ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A )

proof end;

theorem :: PROJRED1:4

for IPP being IncProjSp
for a, b being POINT of IPP st a <> b holds
ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A )

proof end;

theorem :: PROJRED1:5

for IPP being IncProjSp
for a being POINT of IPP ex A, B, C being LINE of IPP st
( a on A & a on B & a on C & A <> B & B <> C & C <> A )

proof end;

theorem :: PROJRED1:6

for IPP being IncProjSp
for A, B being LINE of IPP ex a being POINT of IPP st
( not a on A & not a on B )

proof end;

theorem Th7: :: PROJRED1:7

for IPP being IncProjSp
for A being LINE of IPP ex a being POINT of IPP st a on A

proof end;

theorem Th8: :: PROJRED1:8

for IPP being IncProjSp
for a, b being POINT of IPP
for A being LINE of IPP ex c being POINT of IPP st
( c on A & c <> a & c <> b )

proof end;

theorem :: PROJRED1:9

for IPP being IncProjSp
for a, b being POINT of IPP ex A being LINE of IPP st
( not a on A & not b on A )

proof end;

theorem Th10: :: PROJRED1:10

for IPP being IncProjSp
for a, b, c, o being POINT of IPP
for A, B, P, Q being LINE of IPP st o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q holds
P <> Q

proof end;

theorem Th11: :: PROJRED1:11

for IPP being IncProjSp
for a, b, c being POINT of IPP
for A being LINE of IPP st {a,b,c} on A holds
( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A )

proof end;

theorem Th12: :: PROJRED1:12

for IPP being Desarguesian IncProjSp
for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of IPP
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IPP st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_distinct & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 holds
ex O being LINE of IPP st {r,s,t} on O

proof end;

Lm1: for IPP being IncProjSp
for a, b, c, d being POINT of IPP
for A, B being LINE of IPP st ex o being POINT of IPP st
( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_distinct holds
ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )

proof end;

theorem Th13: :: PROJRED1:13

for IPP being IncProjSp st ex A being LINE of IPP ex a, b, c, d being POINT of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_distinct ) holds
for B being LINE of IPP ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )

proof end;

Lm2: for IPP being Fanoian IncProjSp ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_distinct & d on A & c,d,p,q are_mutually_distinct )

proof end;

theorem :: PROJRED1:14

for IPP being Fanoian IncProjSp ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C )

proof end;

theorem :: PROJRED1:15

for IPP being Fanoian IncProjSp ex a being POINT of IPP ex A, B, C, D being LINE of IPP st
( a on A & a on B & a on C & a on D & A,B,C,D are_mutually_distinct )

proof end;

theorem Th16: :: PROJRED1:16

for IPP being Fanoian IncProjSp ex a, b, c, d being POINT of IPP ex A being LINE of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_distinct )

proof end;

theorem :: PROJRED1:17

for IPP being Fanoian IncProjSp
for B being LINE of IPP ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_distinct )

proof end;

definition

let IPP be 2-dimensional Desarguesian IncProjSp;
let K, L be LINE of IPP;
let p be POINT of IPP;
assume that
A1: not p on K and
A2: not p on L ;

func IncProj (K,p,L) -> PartFunc of the Points of IPP, the Points of IPP means :Def1: :: PROJRED1:def 1
( dom it c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom it iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( it . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines IncProj PROJRED1:def 1 :

theorem Th18: :: PROJRED1:18

for IPP being 2-dimensional Desarguesian IncProjSp
for p being POINT of IPP
for K being LINE of IPP st not p on K holds
for x being POINT of IPP st x on K holds
(IncProj (K,p,K)) . x = x

proof end;

theorem Th19: :: PROJRED1:19

for IPP being 2-dimensional Desarguesian IncProjSp
for p, x being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & x on K holds
(IncProj (K,p,L)) . x is POINT of IPP

proof end;

theorem Th20: :: PROJRED1:20

for IPP being 2-dimensional Desarguesian IncProjSp
for p, x, y being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x holds
y on L

proof end;

theorem :: PROJRED1:21

for IPP being 2-dimensional Desarguesian IncProjSp
for p, y being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & y in rng (IncProj (K,p,L)) holds
y on L

proof end;

theorem Th22: :: PROJRED1:22

for IPP being 2-dimensional Desarguesian IncProjSp
for p, q being POINT of IPP
for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds
( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) )

proof end;

theorem Th23: :: PROJRED1:23

for IPP being 2-dimensional Desarguesian IncProjSp
for p being POINT of IPP
for K, L being LINE of IPP
for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 holds
a1 = b1

proof end;

theorem Th24: :: PROJRED1:24

for IPP being 2-dimensional Desarguesian IncProjSp
for p, x being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & x on K & x on L holds
(IncProj (K,p,L)) . x = x

proof end;

theorem :: PROJRED1:25

for IPP being 2-dimensional Desarguesian IncProjSp
for c, p, q being POINT of IPP
for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R holds
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )

proof end;