:: by Eugeniusz Kusak and Wojciech Leo\'nczuk

::

:: Received October 16, 1990

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

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 )

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 )

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 )

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 )

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 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 )

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 )

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

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 )

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

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 )

( 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 )

( 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 )

( 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 )

( 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 )

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 ;

ex b_{1} being PartFunc of the Points of IPP, the Points of IPP st

( dom b_{1} c= the Points of IPP & ( for x being POINT of IPP holds

( x in dom b_{1} iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds

( b_{1} . x = y iff ex X being LINE of IPP st

( p on X & x on X & y on X ) ) ) )

for b_{1}, b_{2} being PartFunc of the Points of IPP, the Points of IPP st dom b_{1} c= the Points of IPP & ( for x being POINT of IPP holds

( x in dom b_{1} iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds

( b_{1} . x = y iff ex X being LINE of IPP st

( p on X & x on X & y on X ) ) ) & dom b_{2} c= the Points of IPP & ( for x being POINT of IPP holds

( x in dom b_{2} iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds

( b_{2} . x = y iff ex X being LINE of IPP st

( p on X & x on X & y on X ) ) ) holds

b_{1} = b_{2}

end;
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 ( 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 ) ) ) );

ex b

( dom b

( x in dom b

( b

( p on X & x on X & y on X ) ) ) )

proof end;

uniqueness for b

( x in dom b

( b

( p on X & x on X & y on X ) ) ) & dom b

( x in dom b

( b

( p on X & x on X & y on X ) ) ) holds

b

proof end;

:: deftheorem Def1 defines IncProj PROJRED1:def 1 :

for IPP being 2-dimensional Desarguesian IncProjSp

for K, L being LINE of IPP

for p being POINT of IPP st not p on K & not p on L holds

for b_{5} being PartFunc of the Points of IPP, the Points of IPP holds

( b_{5} = IncProj (K,p,L) iff ( dom b_{5} c= the Points of IPP & ( for x being POINT of IPP holds

( x in dom b_{5} iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds

( b_{5} . x = y iff ex X being LINE of IPP st

( p on X & x on X & y on X ) ) ) ) );

for IPP being 2-dimensional Desarguesian IncProjSp

for K, L being LINE of IPP

for p being POINT of IPP st not p on K & not p on L holds

for b

( b

( x in dom b

( b

( p on X & x on X & y on X ) ) ) ) );

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

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

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

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

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)) )

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

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

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) )

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;