:: On Projections in Projective Planes. Part II
:: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received October 31, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let IPS be IncProjSp;
let A, B, C be LINE of IPS;

pred A,B,C are_concurrent means :: PROJRED2:def 1
ex o being Element of the Points of IPS st
( o on A & o on B & o on C );

end;

:: deftheorem defines are_concurrent PROJRED2:def 1 :
for IPS being IncProjSp
for A, B, C being LINE of IPS holds
( A,B,C are_concurrent iff ex o being Element of the Points of IPS st
( o on A & o on B & o on C ) );

definition

let IPS be IncProjSp;
let Z be LINE of IPS;

func CHAIN Z -> Subset of the Points of IPS equals :: PROJRED2:def 2
{ z where z is POINT of IPS : z on Z } ;

correctness
coherence
{ z where z is POINT of IPS : z on Z } is Subset of the Points of IPS;

proof end;

end;

:: deftheorem defines CHAIN PROJRED2:def 2 :
for IPS being IncProjSp
for Z being LINE of IPS holds CHAIN Z = { z where z is POINT of IPS : z on Z } ;

definition

let IPP be 2-dimensional Desarguesian IncProjSp;

mode Projection of IPP -> PartFunc of the Points of IPP, the Points of IPP means :Def3: :: PROJRED2:def 3
ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & it = IncProj (A,a,B) );

existence
ex b₁ being PartFunc of the Points of IPP, the Points of IPP ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & b₁ = IncProj (A,a,B) )

proof end;

end;

:: deftheorem Def3 defines Projection PROJRED2:def 3 :
for IPP being 2-dimensional Desarguesian IncProjSp
for b₂ being PartFunc of the Points of IPP, the Points of IPP holds
( b₂ is Projection of IPP iff ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & b₂ = IncProj (A,a,B) ) );

theorem Th1: :: PROJRED2:1

for IPP being 2-dimensional Desarguesian IncProjSp
for A, B, C being LINE of IPP st ( A = B or B = C or C = A ) holds
A,B,C are_concurrent

proof end;

theorem :: PROJRED2:2

for IPP being 2-dimensional Desarguesian IncProjSp
for A, B, C being LINE of IPP st A,B,C are_concurrent holds
( A,C,B are_concurrent & B,A,C are_concurrent & B,C,A are_concurrent & C,A,B are_concurrent & C,B,A are_concurrent ) ;

theorem Th3: :: PROJRED2:3

for IPP being 2-dimensional Desarguesian IncProjSp
for o, y being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B & y on B holds
ex x being POINT of IPP st
( x on A & (IncProj (A,o,B)) . x = y )

proof end;

theorem Th4: :: PROJRED2:4

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
dom (IncProj (A,o,B)) = CHAIN A

proof end;

theorem Th5: :: PROJRED2:5

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
rng (IncProj (A,o,B)) = CHAIN B

proof end;

theorem :: PROJRED2:6

for IPP being 2-dimensional Desarguesian IncProjSp
for A being LINE of IPP
for x being set holds
( x in CHAIN A iff ex a being POINT of IPP st
( x = a & a on A ) ) ;

theorem Th7: :: PROJRED2:7

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
IncProj (A,o,B) is one-to-one

proof end;

theorem Th8: :: PROJRED2:8

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
(IncProj (A,o,B)) " = IncProj (B,o,A)

proof end;

theorem :: PROJRED2:9

for IPP being 2-dimensional Desarguesian IncProjSp
for f being Projection of IPP holds f " is Projection of IPP

proof end;

theorem Th10: :: PROJRED2:10

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A being LINE of IPP st not o on A holds
IncProj (A,o,A) = id (CHAIN A)

proof end;

theorem :: PROJRED2:11

for IPP being 2-dimensional Desarguesian IncProjSp
for A being LINE of IPP holds id (CHAIN A) is Projection of IPP

proof end;

theorem :: PROJRED2:12

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)

proof end;

theorem :: PROJRED2:13

for IPP being 2-dimensional Desarguesian IncProjSp
for o1, o2 being POINT of IPP
for O1, O2, O3 being LINE of IPP st not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 & O1,O2,O3 are_concurrent & O1 <> O3 holds
ex o being POINT of IPP st
( not o on O1 & not o on O3 & (IncProj (O2,o2,O3)) * (IncProj (O1,o1,O2)) = IncProj (O1,o,O3) ) by PROJRED1:25;

theorem Th14: :: PROJRED2:14

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, p, pp9, q being POINT of IPP
for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & c on A & c on C & c on Q & not b on Q & A <> Q & a on O & b on O & not B,C,O are_concurrent & d on C & d on B & a on O1 & d on O1 & p on A & p on O1 & q on O & q on O2 & p on O2 & pp9 on O2 & d on O3 & b on O3 & pp9 on O3 & pp9 on Q & q <> a & not q on A & not q on Q holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))

proof end;

theorem Th15: :: PROJRED2:15

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, q, o, o9, o99, oo9 being POINT of IPP
for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & b <> q & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))

proof end;

theorem Th16: :: PROJRED2:16

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, p, pp9, q being POINT of IPP
for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 holds
( q <> a & q <> b & not q on A & not q on Q )

proof end;

theorem Th17: :: PROJRED2:17

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, q, o, o9, o99, oo9 being POINT of IPP
for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds
( not q on A & not q on Q & b <> q )

proof end;

theorem Th18: :: PROJRED2:18

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, p, pp9, q being POINT of IPP
for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on C & not q on A & not A,B,C are_concurrent & not B,C,O are_concurrent & a <> b & b <> q & q <> a & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 holds
( Q <> A & Q <> C & not q on Q & not b on Q )

proof end;

theorem Th19: :: PROJRED2:19

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, q, o, o9, o99, oo9 being POINT of IPP
for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on B & not b on C & not q on A & not A,B,C are_concurrent & a <> b & b <> q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds
( not b on Q & not q on Q & A <> Q )

proof end;

Lm1: for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, O, Q being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & not B,C,O are_concurrent holds
ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )

proof end;

Lm2: for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, O, Q being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & B,C,O are_concurrent holds
ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )

proof end;

theorem Th20: :: PROJRED2:20

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, O, Q being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O holds
ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )

proof end;

theorem :: PROJRED2:21

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, O, Q being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & B,C,Q are_concurrent & not a on Q & B <> Q & a <> b & a on O & b on O holds
ex q being POINT of IPP st
( q on O & not q on B & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,q,B)) * (IncProj (A,a,Q)) )

proof end;

theorem :: PROJRED2:22

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, r, s being POINT of IPP
for A, B, C, Q, R, S being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not a on B & not b on A & c on A & c on C & d on B & d on C & a on S & d on S & c on R & b on R & s on A & s on S & r on B & r on R & s on Q & r on Q & not A,B,C are_concurrent holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,a,B)) * (IncProj (A,b,Q))

proof end;

Lm3: for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & c on A & c on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not A,B,C are_concurrent & not B,C,O are_concurrent holds
ex Q being LINE of IPP st
( c on Q & not b on Q & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )

proof end;

Lm4: for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & c on A & c on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not A,B,C are_concurrent & B,C,O are_concurrent holds
ex Q being LINE of IPP st
( c on Q & not b on Q & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )

proof end;

theorem Th23: :: PROJRED2:23

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not A,B,C are_concurrent holds
ex Q being LINE of IPP st
( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )

proof end;

theorem :: PROJRED2:24

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & a <> b & a on O & b on O & q on O & not q on B & q <> a & not A,B,C are_concurrent holds
ex Q being LINE of IPP st
( B,C,Q are_concurrent & not a on Q & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,q,B)) * (IncProj (A,a,Q)) )

proof end;