:: On Projections in Projective Planes. Part II
:: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Copyright (c) 1990-2018 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 b1 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 & b1 = IncProj (A,a,B) )
proof end;
end;

:: deftheorem Def3 defines Projection PROJRED2:def 3 :
for IPP being 2-dimensional Desarguesian IncProjSp
for b2 being PartFunc of the Points of IPP, the Points of IPP holds
( b2 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 & b2 = 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 ()
proof end;

theorem :: PROJRED2:11
for IPP being 2-dimensional Desarguesian IncProjSp
for A being LINE of IPP holds id () 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;