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


begin

definition
let IPS be IncProjSp;
let A, B, C be LINE of IPS;
pred A,B,C are_concurrent means :Def1: :: PROJRED2:def 1
 ex o being Element of the Points of IPS st
( o on A & o on B & o on C );
end;

:: deftheorem Def1 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 )
proof end;

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

theorem Th14: :: PROJRED2:14
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, p, q, pp9 being POINT of IPP
for A, B, C, Q, O, O1, O2, O3 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, q, c, o, o99, d, o9, oo9 being POINT of IPP
for A, C, B, Q, O, O1, O2, O3 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, p, d, q, pp9 being POINT of IPP
for A, C, Q, B, O, O1, O2, O3 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, o, o99, d, o9, oo9, q being POINT of IPP
for A, C, B, Q, O, O1, O2, O3 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, q, c, p, d, pp9 being POINT of IPP
for A, C, B, O, Q, O1, O2, O3 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, q, c, o, o99, d, o9, oo9 being POINT of IPP
for A, C, B, O, Q, O1, O2, O3 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, Q, O 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, Q, O 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, Q, O 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, Q, O 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, s, r being POINT of IPP
for A, B, C, S, R, Q 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;