:: 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 :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies INCPROJ, INCSP_1, SUBSET_1, AFF_2, ANALOAF, PARTFUN1, PROJRED1, FUNCT_1, RELAT_1, TARSKI, ZFMISC_1, PROJRED2; notations TARSKI, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, RELSET_1, INCSP_1, INCPROJ, PARTFUN1, FUNCT_1, PROJRED1; constructors DOMAIN_1, PROJRED1, RELSET_1; registrations FUNCT_1, RELSET_1, INCPROJ; requirements SUBSET, BOOLE; begin reserve IPS for IncProjSp, z for POINT of IPS; definition let IPS; 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; definition let IPS; let Z be LINE of IPS; func CHAIN(Z) -> Subset of the Points of IPS equals :: PROJRED2:def 2 {z: z on Z}; end; reserve IPP for Desarguesian 2-dimensional IncProjSp, a,b,c,d,p,pp9,q,o,o9,o99 ,oo9 for POINT of IPP, r,s,x,y,o1,o2 for POINT of IPP, O1,O2,O3,O4,A,B,C,O,Q,Q1 ,Q2,Q3,R,S,X for LINE of IPP; definition let IPP; mode Projection of IPP -> PartFunc of the Points of IPP,the Points of IPP means :: PROJRED2:def 3 ex a,A,B st not a on A & not a on B & it = IncProj(A,a,B); end; theorem :: PROJRED2:1 A=B or B=C or C=A implies A,B,C are_concurrent; theorem :: PROJRED2:2 A,B,C are_concurrent implies 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 :: PROJRED2:3 not o on A & not o on B & y on B implies ex x st x on A & IncProj (A,o,B).x = y; theorem :: PROJRED2:4 not o on A & not o on B implies dom IncProj(A,o,B) = CHAIN(A); theorem :: PROJRED2:5 not o on A & not o on B implies rng IncProj(A,o,B) = CHAIN(B); theorem :: PROJRED2:6 for x being set holds x in CHAIN(A) iff ex a st x=a & a on A; theorem :: PROJRED2:7 not o on A & not o on B implies IncProj(A,o,B) is one-to-one; theorem :: PROJRED2:8 not o on A & not o on B implies IncProj(A,o,B)" = IncProj(B,o,A); theorem :: PROJRED2:9 for f being Projection of IPP holds f" is Projection of IPP; theorem :: PROJRED2:10 not o on A implies IncProj(A,o,A) = id CHAIN(A); theorem :: PROJRED2:11 id CHAIN(A) is Projection of IPP; theorem :: PROJRED2:12 not o on A & not o on B & not o on C implies IncProj(C,o,B)*IncProj(A, o,C) = IncProj(A,o,B); theorem :: PROJRED2:13 not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 & O1,O2,O3 are_concurrent & O1<>O3 implies ex o st not o on O1 & not o on O3 & IncProj(O2, o2,O3)*IncProj(O1,o1,O2) = IncProj(O1,o,O3); theorem :: PROJRED2:14 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 implies IncProj(C,b,B)*IncProj(A,a, C) = IncProj(Q,b,B)*IncProj(A,q,Q); theorem :: PROJRED2:15 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 implies IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b, B)*IncProj(A,q,Q); theorem :: PROJRED2:16 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 implies q<>a & q<>b & not q on A & not q on Q; theorem :: PROJRED2:17 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 implies not q on A & not q on Q & b<>q; theorem :: PROJRED2:18 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 implies Q<>A & Q<>C & not q on Q & not b on Q; theorem :: PROJRED2:19 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 implies not b on Q & not q on Q & A<>Q; theorem :: PROJRED2:20 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 implies ex q 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); theorem :: PROJRED2:21 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 implies ex q 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); theorem :: PROJRED2:22 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 implies IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,a,B)*IncProj(A,b,Q); theorem :: PROJRED2:23 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 implies ex Q 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); theorem :: PROJRED2:24 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 implies ex Q 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);