let N be invertible Matrix of 3,F_Real; :: thesis: for p, q, r, s, t, u, np, nq, nr, ns being Element of real_projective_plane st p <> q & r <> s & np <> nq & nr <> ns & p,q,t are_collinear & r,s,t are_collinear & np = (homography N) . p & nq = (homography N) . q & nr = (homography N) . r & ns = (homography N) . s & np,nq,u are_collinear & nr,ns,u are_collinear & not u = (homography N) . t holds
Line (np,nq) = Line (nr,ns)
let p, q, r, s, t, u, np, nq, nr, ns be Element of real_projective_plane; :: thesis: ( p <> q & r <> s & np <> nq & nr <> ns & p,q,t are_collinear & r,s,t are_collinear & np = (homography N) . p & nq = (homography N) . q & nr = (homography N) . r & ns = (homography N) . s & np,nq,u are_collinear & nr,ns,u are_collinear & not u = (homography N) . t implies Line (np,nq) = Line (nr,ns) )
assume that
A0: ( p <> q & r <> s & np <> nq & nr <> ns ) and
A1: p,q,t are_collinear and
A2: r,s,t are_collinear and
A3: np = (homography N) . p and
A4: nq = (homography N) . q and
A5: nr = (homography N) . r and
A6: ns = (homography N) . s and
A7: np,nq,u are_collinear and
A8: nr,ns,u are_collinear ; :: thesis: ( u = (homography N) . t or Line (np,nq) = Line (nr,ns) )
A9: ( t in Line (p,q) & t in Line (r,s) & u in Line (np,nq) & u in Line (nr,ns) ) by A1, A2, A7, A8, COLLSP:11;
reconsider L1 = Line (p,q), L2 = Line (r,s), L3 = Line (np,nq), L4 = Line (nr,ns) as LINE of real_projective_plane by A0, COLLSP:def 7;
reconsider LL1 = L1, LL2 = L2, LL3 = L3, LL4 = L4 as LINE of (IncProjSp_of real_projective_plane) by INCPROJ:4;
reconsider t9 = t, u9 = u as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
A10: ( t9 on LL1 & t9 on LL2 & u9 on LL3 & u9 on LL4 ) by A9, INCPROJ:5;
reconsider nt = (homography N) . t as Element of real_projective_plane by FUNCT_2:5;
A11: ( nt in Line (np,nq) & nt in Line (nr,ns) ) by A1, A2, A3, A4, A5, A6, ANPROJ_8:102, COLLSP:11;
reconsider nt9 = nt as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
( nt9 on LL3 & nt9 on LL4 ) by A11, INCPROJ:5;
hence ( u = (homography N) . t or Line (np,nq) = Line (nr,ns) ) by A10, INCPROJ:8; :: thesis: verum