:: 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; predA,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; proofend; 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) ) proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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) proofend; theorem :: PROJRED2:9 for IPP being 2-dimensional Desarguesian IncProjSp for f being Projection of IPP holds f " is Projection of IPP proofend; 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) proofend; theorem :: PROJRED2:11 for IPP being 2-dimensional Desarguesian IncProjSp for A being LINE of IPP holds id (CHAIN A) is Projection of IPP proofend; 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) proofend; 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) ) proofend; 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)) proofend; 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)) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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)) ) proofend; 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)) ) proofend; 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)) ) proofend; 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)) ) proofend; 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)) proofend; 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)) ) proofend; 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)) ) proofend; 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)) ) proofend; 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)) ) proofend;