:: Projective {P}lanes :: by Micha{\l} Muzalewski :: :: Received July 28, 1994 :: Copyright (c) 1994-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 INCSP_1, INCPROJ, ZFMISC_1, ANALOAF, SUBSET_1, RELAT_1, PROJPL_1, RECDEF_2, PENCIL_1; notations ZFMISC_1, SUBSET_1, MCART_1, DOMAIN_1, INCSP_1, INCPROJ; constructors DOMAIN_1, INCPROJ; registrations INCPROJ; begin :: 1. PROJECTIVE SPACES reserve G for IncProjStr; reserve a,a1,a2,b,b1,b2,c,d,p,q,r for POINT of G; reserve A,B,C,D,M,N,P,Q,R for LINE of G; notation let G,a,P; antonym a|'P for a on P; end; definition let G,a,b,P; pred a,b|'P means :: PROJPL_1:def 1 a|'P & b|'P; end; definition let G,a,P,Q; pred a on P,Q means :: PROJPL_1:def 2 a on P & a on Q; end; definition let G,a,P,Q,R; pred a on P,Q,R means :: PROJPL_1:def 3 a on P & a on Q & a on R; end; theorem :: PROJPL_1:1 ({a,b} on P implies {b,a} on P) & ({a,b,c} on P implies {a,c,b} on P & {b,a,c} on P & {b,c,a} on P & {c,a,b} on P & {c,b,a} on P) & (a on P,Q implies a on Q,P) & (a on P,Q,R implies a on P,R,Q & a on Q,P,R & a on Q,R,P & a on R,P,Q & a on R,Q,P); definition let IT be IncProjStr; attr IT is configuration means :: PROJPL_1:def 4 for p,q being POINT of IT, P,Q being LINE of IT st p on P & q on P & p on Q & q on Q holds p = q or P = Q; end; theorem :: PROJPL_1:2 G is configuration iff for p,q,P,Q st {p,q} on P & {p,q} on Q holds p = q or P = Q; theorem :: PROJPL_1:3 G is configuration iff for p,q,P,Q st p on P,Q & q on P,Q holds p = q or P = Q; theorem :: PROJPL_1:4 G is IncProjSp iff G is configuration & (for p,q ex P st {p,q} on P) & (ex p,P st p|'P) & (for P ex a,b,c st a,b,c are_mutually_distinct & {a,b, c} on P) & for a,b,c,d,p,M,N,P,Q st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p|'P & p|'Q & M<>N holds ex q st q on P,Q; definition mode IncProjectivePlane is 2-dimensional IncProjSp; end; definition let G,a,b,c; pred a,b,c are_collinear means :: PROJPL_1:def 5 ex P st {a,b,c} on P; end; notation let G,a,b,c; antonym a,b,c is_a_triangle for a,b,c are_collinear; end; theorem :: PROJPL_1:5 a,b,c are_collinear iff ex P st a on P & b on P & c on P; theorem :: PROJPL_1:6 a,b,c is_a_triangle iff for P holds a|'P or b|'P or c|'P; definition let G,a,b,c,d; pred a,b,c,d is_a_quadrangle means :: PROJPL_1:def 6 a,b,c is_a_triangle & b,c,d is_a_triangle & c,d,a is_a_triangle & d,a,b is_a_triangle; end; theorem :: PROJPL_1:7 G is IncProjSp implies ex A,B st A<>B; theorem :: PROJPL_1:8 G is IncProjSp implies ex b,c st {b,c} on A & a,b,c are_mutually_distinct; theorem :: PROJPL_1:9 G is IncProjSp & A<>B implies ex b st b on A & b|'B & a<>b; theorem :: PROJPL_1:10 G is configuration & {a1,a2} on A & a1<>a2 & b|'A implies a1,a2, b is_a_triangle; theorem :: PROJPL_1:11 a,b,c are_collinear implies a,c,b are_collinear & b,a,c are_collinear & b,c,a are_collinear & c,a,b are_collinear & c,b,a are_collinear; theorem :: PROJPL_1:12 a,b,c is_a_triangle implies a,c,b is_a_triangle & b,a,c is_a_triangle & b,c,a is_a_triangle & c,a,b is_a_triangle & c,b,a is_a_triangle; theorem :: PROJPL_1:13 a,b,c,d is_a_quadrangle implies a,c,b,d is_a_quadrangle & b,a,c, d is_a_quadrangle & b,c,a,d is_a_quadrangle & c,a,b,d is_a_quadrangle & c,b,a,d is_a_quadrangle & a,b,d,c is_a_quadrangle & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle; theorem :: PROJPL_1:14 G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2|'B & b1 ,b2|'A & a1<>a2 & b1<>b2 implies a1,a2,b1,b2 is_a_quadrangle; theorem :: PROJPL_1:15 G is IncProjSp implies ex a,b,c,d st a,b,c,d is_a_quadrangle; definition let G be IncProjSp; mode Quadrangle of G -> Element of [:the Points of G,the Points of G,the Points of G,the Points of G:] means :: PROJPL_1:def 7 it`1_4,it`2_4,it`3_4,it`4_4 is_a_quadrangle; end; definition let G be IncProjSp, a,b be POINT of G; assume a <> b; func a*b -> LINE of G means :: PROJPL_1:def 8 {a,b} on it; end; theorem :: PROJPL_1:16 for G be IncProjSp, a,b be POINT of G, L be LINE of G st a <> b holds a on a*b & b on a*b & a*b = b*a & (a on L & b on L implies L = a*b); begin :: 2. PROJECTIVE PLANES theorem :: PROJPL_1:17 (ex a,b,c st a,b,c is_a_triangle) & (for p,q ex M st {p,q} on M) implies ex p,P st p|'P; theorem :: PROJPL_1:18 (ex a,b,c,d st a,b,c,d is_a_quadrangle) implies ex a,b,c st a,b, c is_a_triangle; theorem :: PROJPL_1:19 a,b,c is_a_triangle & {a,b} on P & {a,c} on Q implies P<>Q; theorem :: PROJPL_1:20 a,b,c,d is_a_quadrangle & {a,b} on P & {a,c} on Q & {a,d} on R implies P,Q,R are_mutually_distinct; theorem :: PROJPL_1:21 G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a|'A & p on A,P & q on A,Q & r on A,R implies p,q,r are_mutually_distinct; theorem :: PROJPL_1:22 G is configuration & (for p,q ex M st {p,q} on M) & (for P,Q ex a st a on P,Q) & (ex a,b,c,d st a,b,c,d is_a_quadrangle) implies for P ex a,b,c st a,b,c are_mutually_distinct & {a,b,c} on P; theorem :: PROJPL_1:23 G is IncProjectivePlane iff G is configuration & (for p,q ex M st {p,q} on M) & (for P,Q ex a st a on P,Q) & ex a,b,c,d st a,b,c,d is_a_quadrangle; reserve G for IncProjectivePlane; reserve a,q for POINT of G; reserve A,B for LINE of G; definition let G,A,B; assume A <> B; func A*B -> POINT of G means :: PROJPL_1:def 9 it on A,B; end; theorem :: PROJPL_1:24 A <> B implies A*B on A & A*B on B & A*B = B*A & (a on A & a on B implies a=A*B); theorem :: PROJPL_1:25 A<>B & a on A & q|'A & a<>A*B implies (q*a)*B on B & (q*a)*B|'A; begin :: 3. SOME USEFUL PROPOSITIONS reserve G for IncProjSp; reserve a,b,c,d for POINT of G; reserve P for LINE of G; theorem :: PROJPL_1:26 a,b,c is_a_triangle implies a,b,c are_mutually_distinct; theorem :: PROJPL_1:27 a,b,c,d is_a_quadrangle implies a,b,c,d are_mutually_distinct; reserve G for IncProjectivePlane; theorem :: PROJPL_1:28 for a,b,c,d being POINT of G st a*c = b*d holds a = c or b = d or c = d or a*c = c*d; theorem :: PROJPL_1:29 for a,b,c,d being POINT of G st a*c = b*d holds a = c or b = d or c = d or a on c*d; theorem :: PROJPL_1:30 for G being IncProjectivePlane, e,m,m9 being POINT of G, I being LINE of G st m on I & m9 on I & m<>m9 & e|'I holds m*e<>m9*e & e*m<>e*m9; theorem :: PROJPL_1:31 for G being IncProjectivePlane, e being POINT of G, I,L1,L2 being LINE of G st e on L1 & e on L2 & L1<>L2 & e|'I holds I*L1<>I*L2 & L1*I<>L2*I; theorem :: PROJPL_1:32 for G being IncProjSp, a,b,q,q1 being POINT of G st q on a*b & q on a* q1 & q<>a & q1<>a & a<>b holds q1 on a*b; theorem :: PROJPL_1:33 for G being IncProjSp, a,b,c being POINT of G st c on a*b & a<>c holds b on a*c; theorem :: PROJPL_1:34 for G being IncProjectivePlane, q1,q2,r1,r2 being POINT of G, H being LINE of G st r1<>r2 & r1 on H & r2 on H & q1|'H & q2|'H holds q1*r1<>q2*r2; theorem :: PROJPL_1:35 for a,b,c being POINT of G st a on b*c holds a=c or b=c or b on c*a; theorem :: PROJPL_1:36 for a,b,c being POINT of G st a on b*c holds b=a or b=c or c on b*a; theorem :: PROJPL_1:37 for e,x1,x2,p1,p2 being POINT of G for H,I being LINE of G st x1 on I & x2 on I & e |'I & x1<>x2 & p1<>e & p2 <>e & p1 on e*x1 & p2 on e*x2 holds ex r being POINT of G st r on p1*p2 & r on H & r<>e;