:: Beltrami-Klein Model, {P}art {I} :: by Roland Coghetto :: :: Received March 27, 2018 :: Copyright (c) 2018-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 COLLSP, PRALG_1, NAT_1, TREES_1, MATRIX_0, MATRIX_6, FINSEQ_2, COMPLEX1, REAL_1, XCMPLX_0, ANPROJ_1, PENCIL_1, MCART_1, EUCLID_5, ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, EUCLID, FUNCT_1, INCSP_1, MATRIX_1, NUMBERS, PRE_TOPC, RELAT_1, STRUCT_0, SUBSET_1, SUPINF_2, VECTSP_1, XBOOLE_0, MESFUNC1, ANPROJ_8, ANPROJ_9, RLVECT_3, TARSKI, XXREAL_0, PASCAL, INCPROJ, ANPROJ_2, ZFMISC_1, ANALOAF, SQUARE_1, JGRAPH_6, PROB_1, METRIC_1, RVSUM_1, PROJPL_1, FINSEQ_1, QC_LANG1, RELAT_2, MATRIXR1, MATRIXC1, MATRIX_3, MATRIXR2, FUNCT_3, CARD_3, TOPREALB, BKMODEL1; notations XTUPLE_0, RELSET_1, ORDINAL1, XCMPLX_0, PRE_TOPC, RVSUM_1, TARSKI, XBOOLE_0, RLVECT_1, COLLSP, EUCLID_5, PASCAL, XXREAL_0, INCPROJ, DOMAIN_1, INCSP_1, ANPROJ_2, RLVECT_3, ANPROJ_9, SQUARE_1, XREAL_0, JGRAPH_6, TOPREAL9, PROJPL_1, ZFMISC_1, SUBSET_1, NUMBERS, FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, ALGSTR_0, VECTSP_1, FINSEQ_2, EUCLID, ANPROJ_1, MATRIX_0, MATRIX_6, LAPLACE, ANPROJ_8, MATRIX_1, MATRIX_3, MATRIXR1, MATRIXR2, MATRPROB, QUIN_1, COMPLEX1, TOPREALB; constructors MATRIXR2, RANKNULL, FINSEQ_4, FVSUM_1, LAPLACE, MATRPROB, MONOID_0, EUCLID_5, MATRIX13, ANPROJ_8, PASCAL, INCPROJ, ANPROJ_2, RLVECT_3, ANPROJ_9, SQUARE_1, JGRAPH_6, TOPREAL9, BINOP_2, QUIN_1, BORSUK_7; registrations FUNCT_1, MEMBERED, FINSEQ_1, ORDINAL1, XXREAL_0, XBOOLE_0, ANPROJ_1, STRUCT_0, VECTSP_1, REVROT_1, RELSET_1, XREAL_0, MONOID_0, EUCLID, VALUED_0, MATRIX_6, ANPROJ_2, INCPROJ, ANPROJ_9, SQUARE_1, XCMPLX_0, NUMBERS, MATRIX_0, QUIN_1; requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE; begin :: Preliminaries reserve a,b,c,d,e,f for Real, g for positive Real, x,y for Complex, S,T for Element of REAL 2, u,v,w for Element of TOP-REAL 3; theorem :: BKMODEL1:1 for P1,P2,P3 being Element of ProjectiveSpace TOP-REAL 3 st u is non zero & v is non zero & w is non zero & P1 = Dir u & P2 = Dir v & P3 = Dir w holds (P1,P2,P3 are_collinear iff |{u,v,w}| = 0); theorem :: BKMODEL1:2 (a <> 0 or b <> 0) & a * d = b * c implies ex e st c = e * a & d = e * b; theorem :: BKMODEL1:3 a^2 + b^2 = 1 & (c * a)^2 + (c * b)^2 = 1 implies c = 1 or c = -1; theorem :: BKMODEL1:4 a * u + (-a) * u = 0.TOP-REAL 3; theorem :: BKMODEL1:5 0 <= a & c < 0 & delta(a,b,c) = 0 implies a = 0; theorem :: BKMODEL1:6 Sum sqr (T - S) = Sum sqr (S - T); theorem :: BKMODEL1:7 a^2 + b^2 = 1 & c^2 + d^2 = 1 & c * a + d * b = 1 implies b * c = a * d; theorem :: BKMODEL1:8 a^2 + b^2 = 1 & a = 0 implies b = 1 or b = -1; theorem :: BKMODEL1:9 0 <= a^2; theorem :: BKMODEL1:10 (a * b)^2 + b^2 = 1 implies b = 1 / sqrt(1 + a^2) or b = (-1) / sqrt(1 + a^2); theorem :: BKMODEL1:11 a <> 0 & b^2 = 1 + a * a implies a * (1/b) * a * ((-1)/b) + (1/b) * ((-1)/b) = -1; theorem :: BKMODEL1:12 a^2 * (1/(b^2)) = (a/b)^2; theorem :: BKMODEL1:13 a^2 + b^2 = 1 iff |[a,b]| in circle(0,0,1); theorem :: BKMODEL1:14 a^2 + b^2 = g^2 iff |[a,b]| in circle(0,0,g); theorem :: BKMODEL1:15 a <> 0 & -1 < a < 1 & b = (2 + sqrt delta(a * a,-2,1)) / (2 * a * a) implies (1 + a * a) * b * b - 2 * b + 1 - b * b = 0; theorem :: BKMODEL1:16 a^2 + b^2 = 1 & -1 < c < 1 implies ex d,e,f st e = d * c * a + (1 - d) * (-b) & f = d * c * b + (1 - d) * a & e^2 + f^2 = d^2; theorem :: BKMODEL1:17 a^2 + b^2 < 1 & c^2 + d^2 = 1 implies ((a + c)/2)^2 + ((b + d)/2)^2 < 1; theorem :: BKMODEL1:18 |. S .|^2 <= 1 implies 0 <= delta(Sum sqr (T - S),b,Sum sqr S - 1); theorem :: BKMODEL1:19 a^2 + b^2 is negative implies a = 0 & b = 0; theorem :: BKMODEL1:20 u = |[a,b,1]| & v = |[c,d,1]| & w = |[ (a + c)/2, (b + d)/2, 1]| implies |{u,v,w}| = 0; theorem :: BKMODEL1:21 a * |(u,v)| = |(a * u,v)| & a * |(u,v)| = |(u, a * v)|; reserve a,b,c for Element of F_Real, M,N for Matrix of 3,F_Real; theorem :: BKMODEL1:22 M = symmetric_3(0,0,0,0,0,0) implies Det M = 0.F_Real; theorem :: BKMODEL1:23 N = <* <* a,0,0 *>, <* 0,b,0 *>, <* 0,0,c *> *> implies (M@ * (N * M))*(1,1) = a * (M*(1,1)) * (M*(1,1)) + b * (M*(2,1)) * (M*(2,1)) + c * (M*(3,1)) * (M*(3,1)) & (M@ * (N * M))*(1,2) = a * (M*(1,1)) * (M*(1,2)) + b * (M*(2,1)) * (M*(2,2)) + c * (M*(3,1)) * (M*(3,2)) & (M@ * (N * M))*(1,3) = a * (M*(1,1)) * (M*(1,3)) + b * (M*(2,1)) * (M*(2,3)) + c * (M*(3,1)) * (M*(3,3)) & (M@ * (N * M))*(2,1) = a * (M*(1,2)) * (M*(1,1)) + b * (M*(2,2)) * (M*(2,1)) + c * (M*(3,2)) * (M*(3,1)) & (M@ * (N * M))*(2,2) = a * (M*(1,2)) * (M*(1,2)) + b * (M*(2,2)) * (M*(2,2)) + c * (M*(3,2)) * (M*(3,2)) & (M@ * (N * M))*(2,3) = a * (M*(1,2)) * (M*(1,3)) + b * (M*(2,2)) * (M*(2,3)) + c * (M*(3,2)) * (M*(3,3)) & (M@ * (N * M))*(3,1) = a * (M*(1,3)) * (M*(1,1)) + b * (M*(2,3)) * (M*(2,1)) + c * (M*(3,3)) * (M*(3,1)) & (M@ * (N * M))*(3,2) = a * (M*(1,3)) * (M*(1,2)) + b * (M*(2,3)) * (M*(2,2)) + c * (M*(3,3)) * (M*(3,2)) & (M@ * (N * M))*(3,3) = a * (M*(1,3)) * (M*(1,3)) + b * (M*(2,3)) * (M*(2,3)) + c * (M*(3,3)) * (M*(3,3)); theorem :: BKMODEL1:24 for m,n being Nat for M being Matrix of m,F_Real for N being Matrix of m,n,F_Real st m > 0 holds M * N is Matrix of m,n,F_Real; reserve D for non empty set; reserve d1,d2,d3 for Element of D; reserve A for Matrix of 1,3,D; reserve B for Matrix of 3,1,D; theorem :: BKMODEL1:25 for M being Matrix of 1,D holds M@ = M; theorem :: BKMODEL1:26 (A@) is (3,1)-size; theorem :: BKMODEL1:27 <* <* d1,d2,d3 *> *> is Matrix of 1,3,D; theorem :: BKMODEL1:28 <* <* d1 *> ,<* d2 *> ,<* d3 *> *> is Matrix of 3,1,D; theorem :: BKMODEL1:29 A = <* <* A*(1,1), A*(1,2), A*(1,3) *> *>; theorem :: BKMODEL1:30 B = <* <* B*(1,1) *> , <* B*(2,1) *>, <* B*(3,1) *> *>; theorem :: BKMODEL1:31 A@ = <* <* A*(1,1) *>, <* A*(1,2) *>, <* A*(1,3) *> *>; theorem :: BKMODEL1:32 ex d1,d2,d3 st A = <* <* d1,d2,d3 *> *>; theorem :: BKMODEL1:33 for p being FinSequence of 1-tuples_on REAL st len p = 3 holds ColVec2Mx M2F p = p; theorem :: BKMODEL1:34 for M being Matrix of 3,F_Real for MR being Matrix of 3,REAL for v being Element of TOP-REAL 3 for uf being FinSequence of F_Real for ufr being FinSequence of REAL for p being FinSequence of (1-tuples_on REAL) st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M holds v = MR * ufr; theorem :: BKMODEL1:35 for N being Matrix of 3,REAL for uf being FinSequence of REAL st uf = 0.TOP-REAL 3 holds N * uf = 0.TOP-REAL 3; theorem :: BKMODEL1:36 for N being Matrix of 3,REAL for uf being FinSequence of REAL for u being Element of TOP-REAL 3 st N is invertible & u = uf & u is non zero holds N * uf <> 0.TOP-REAL 3; theorem :: BKMODEL1:37 for N being invertible Matrix of 3,F_Real for NR being Matrix of 3,REAL for P,Q being Element of ProjectiveSpace TOP-REAL 3 for u,v being non zero Element of TOP-REAL 3 for vfr,ufr being FinSequence of REAL st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds homography(N).P = Q; theorem :: BKMODEL1:38 for N being invertible Matrix of 3,F_Real for NR being Matrix of 3,REAL for P,Q being Element of ProjectiveSpace TOP-REAL 3 for u,v being non zero Element of TOP-REAL 3 for vfr,ufr being FinSequence of REAL for a being non zero Real st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = a * vfr holds homography(N).P = Q; theorem :: BKMODEL1:39 for p being FinSequence of REAL for M being Matrix of 3,REAL st len p = 3 holds |( a * p, M * (b * p) )| = a * b * |(p, M * p)|; theorem :: BKMODEL1:40 for p being FinSequence of REAL for M being Matrix of 3,REAL st len p = 3 holds SumAll QuadraticForm (a * p,M,b * p) = a * b * SumAll QuadraticForm(p,M,p); theorem :: BKMODEL1:41 for a,b being Real holds |[a,b,1]| is non zero; theorem :: BKMODEL1:42 for P being Element of TOP-REAL 2,Q being Element of TOP-REAL 2,r being Real holds P in Sphere(Q,r) iff P in circle(Q.1,Q.2,r); reserve u,v for non zero Element of TOP-REAL 3; theorem :: BKMODEL1:43 Dir u = Dir v & u.3 = v.3 & v.3 <> 0 implies u = v; definition func Dir101 -> Point of ProjectiveSpace TOP-REAL 3 equals :: BKMODEL1:def 1 Dir |[ 1,0,1 ]|; end; definition func Dirm101 -> Point of ProjectiveSpace TOP-REAL 3 equals :: BKMODEL1:def 2 Dir |[-1,0,1]|; end; definition func Dir011 -> Point of ProjectiveSpace TOP-REAL 3 equals :: BKMODEL1:def 3 Dir |[0,1,1]|; end; theorem :: BKMODEL1:44 not Dir101,Dirm101,Dir011 are_collinear & not Dir101,Dirm101,Dir010 are_collinear & not Dir101,Dir011,Dir010 are_collinear & not Dirm101,Dir011,Dir010 are_collinear; theorem :: BKMODEL1:45 symmetric_3(1,1,1,0,0,0) = 1.(F_Real,3); theorem :: BKMODEL1:46 for r,a,b,c,d,e,f,g,h,i being Element of F_Real for M being Matrix of 3,F_Real st M = <* <* a,b,c *>, <* d,e,f *>, <* g,h,i *> *> holds r * M = <* <* r * a,r * b,r * c *>, <* r * d,r * e,r * f *>, <* r * g,r * h,r * i *> *>; theorem :: BKMODEL1:47 for a being Real for ra2 being Element of F_Real st ra2 = a * a holds symmetric_3(a,a,-a,0,0,0) * symmetric_3(a,a,-a,0,0,0) = ra2 * 1.(F_Real,3); theorem :: BKMODEL1:48 for a being non zero Real holds symmetric_3(a,a,-a,0,0,0) * symmetric_3(1/a,1/a,-1/a,0,0,0) = 1.(F_Real,3); theorem :: BKMODEL1:49 for a being non zero Real holds symmetric_3(1/a,1/a,-1/a,0,0,0) * symmetric_3(a,a,-a,0,0,0) = 1.(F_Real,3); theorem :: BKMODEL1:50 symmetric_3(1,1,-1,0,0,0) * symmetric_3(1,1,-1,0,0,0) = 1.(F_Real,3); theorem :: BKMODEL1:51 for a being non zero Real for N being Matrix of 3,F_Real st N = symmetric_3(a,a,-a,0,0,0) holds N is invertible; theorem :: BKMODEL1:52 symmetric_3(1,1,-1,0,0,0) is invertible Matrix of 3,F_Real & (symmetric_3(1,1,-1,0,0,0))~ = symmetric_3(1,1,-1,0,0,0); theorem :: BKMODEL1:53 for N being invertible Matrix of 3,F_Real for N1 being Matrix of 3,F_Real for M,NR being Matrix of 3,REAL st M = symmetric_3(1,1,-1,0,0,0) & N1 = M & NR = MXF2MXR(N~) holds (N@) * N1 * N = MXF2MXR((MXR2MXF(NR@))~) * M * MXF2MXR((MXR2MXF NR)~); theorem :: BKMODEL1:54 for n being Nat for a being Element of F_Real for ra being Real for A being Matrix of n,F_Real for rA being Matrix of n,REAL st a = ra & A = rA holds a * A = ra * rA; theorem :: BKMODEL1:55 for n being Nat for a being Element of F_Real for A,B being Matrix of n,F_Real st n > 0 holds (a * A) * B = a * (A * B); theorem :: BKMODEL1:56 symmetric_3(a,a,-a,0,0,0) = a * (symmetric_3(1,1,-1,0,0,0)); theorem :: BKMODEL1:57 M = symmetric_3(a,a,-a,0,0,0) implies M * M * M = (a * a * a) * symmetric_3(1,1,-1,0,0,0); theorem :: BKMODEL1:58 for n being Nat for a being Real for M being Matrix of n,REAL for x being FinSequence of REAL st n > 0 & len x = n holds M * (a * x) = (a * M) * x; theorem :: BKMODEL1:59 for n being Nat for a being Real for M being Matrix of n,REAL for x being FinSequence of REAL st n > 0 & len x = n holds a * (M * x) = (a * M) * x; theorem :: BKMODEL1:60 for n being Nat for N being Matrix of n,REAL st N is invertible holds N@ is invertible & Inv(N@) = (Inv(N))@; theorem :: BKMODEL1:61 for ra being non zero Real for N,O,M being Matrix of 3,3,REAL st N is invertible & M = ra * O & M = N@ * O * N holds Inv(N)@ * O * Inv(N) = 1/ra * O; theorem :: BKMODEL1:62 for ra being Real for M,N being Matrix of 3,F_Real for MR,NR being Matrix of 3,REAL st MR = M & NR = N & N is symmetric & MR = ra * NR holds M is symmetric; theorem :: BKMODEL1:63 for ra being Real for O,M being Matrix of 3,REAL st O = symmetric_3(1,1,-1,0,0,0) & M = ra * O holds O * M = ra * 1_Rmatrix(3) & M * O = ra * 1_Rmatrix(3); theorem :: BKMODEL1:64 for ra being Real for O,M being Matrix of 3,REAL st O = symmetric_3(1,1,-1,0,0,0) & M = ra * O holds (M@ * O)@ * O * (M@ * O) = ra^2 * O; theorem :: BKMODEL1:65 for O,N being Matrix of 3,REAL holds (N@ * O)@ * O * (N@ * O) = O@ * (N * O * N@) * O; theorem :: BKMODEL1:66 for NR,MR being Matrix of 3,REAL for p1,p2,p3 being FinSequence of REAL st p1 = <* 1,0,0 *> & p2 = <* 0,1,0 *> & p3 = <* 0,0,1 *> & NR * p1 = MR * p1 & NR * p2 = MR * p2 & NR * p3 = MR * p3 holds NR = MR; theorem :: BKMODEL1:67 for a being non zero Real for u being Element of TOP-REAL 3 st a * u = 0.TOP-REAL 3 holds u is zero; theorem :: BKMODEL1:68 for u,v being non zero Element of TOP-REAL 3 for a,b being Real st (a <> 0 or b <> 0) & a * u + b * v = 0.TOP-REAL 3 holds are_Prop u,v; theorem :: BKMODEL1:69 for N being invertible Matrix of 3,F_Real for P,Q,R being Point of ProjectiveSpace TOP-REAL 3 st P <> Q & homography(N).P = Q & homography(N).Q = P & P,Q,R are_collinear holds (homography(N)).((homography(N)).R) = R; theorem :: BKMODEL1:70 for n being Nat for u,v being Element of TOP-REAL n for a,b being Real st (1 - a) * u + (a * v) = (1 - b) * v + (b * u) holds (1 - (a + b)) * u = (1 - (a + b)) * v; theorem :: BKMODEL1:71 ProjectiveSpace TOP-REAL 3 is proper; definition func real_projective_plane -> non empty proper CollProjectivePlane equals :: BKMODEL1:def 4 ProjectiveSpace TOP-REAL 3; end; reserve P,Q,R for POINT of IncProjSp_of real_projective_plane, L for LINE of IncProjSp_of real_projective_plane, p,q,r for Point of real_projective_plane; theorem :: BKMODEL1:72 for L being Element of ProjectiveLines real_projective_plane holds ex p,q st p <> q & L = Line(p,q); theorem :: BKMODEL1:73 ex p,q st p <> q & L = Line(p,q); theorem :: BKMODEL1:74 R = r & L = Line(p,q) implies (R on L iff p,q,r are_collinear); theorem :: BKMODEL1:75 IncProjSp_of real_projective_plane is IncProjectivePlane; theorem :: BKMODEL1:76 for L1,L2 being LINE of real_projective_plane holds L1 meets L2; reserve u,v,w for non zero Element of TOP-REAL 3; theorem :: BKMODEL1:77 p = Dir u & q = Dir v & R = Dir w & L = Line(p,q) implies (R on L iff |{u,v,w}| = 0); theorem :: BKMODEL1:78 for p,q being Element of ProjectiveSpace TOP-REAL 3 st p <> q & p = Dir u & q = Dir v holds u v is non zero; definition let p,q be Point of real_projective_plane; assume p <> q; func L2P(p,q) -> Point of real_projective_plane means :: BKMODEL1:def 5 ex u,v being non zero Element of TOP-REAL 3 st p = Dir u & q = Dir v & it = Dir(u v); end; theorem :: BKMODEL1:79 for p,q being Point of real_projective_plane st p <> q holds L2P(q,p) = L2P(p,q) & p <> L2P(p,q); theorem :: BKMODEL1:80 for N being invertible Matrix of 3,F_Real holds dom homography(N) = ProjectivePoints TOP-REAL 3; begin :: Absolute definition let a,b,c,d,e,f be Real; ::: assume not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & f = 0); func negative_conic(a,b,c,d,e,f) -> Subset of ProjectiveSpace TOP-REAL 3 equals :: BKMODEL1:def 6 {P where P is Point of ProjectiveSpace TOP-REAL 3: for u being Element of TOP-REAL 3 st u is non zero & P = Dir u holds qfconic(a,b,c,d,e,f,u) is negative}; end; theorem :: BKMODEL1:81 for a,b,c,d,e,f being Real for u1,u2 being non zero Element of TOP-REAL 3 st Dir u1 = Dir u2 & qfconic(a,b,c,d,e,f,u1) is negative holds qfconic(a,b,c,d,e,f,u2) is negative; definition func absolute -> non empty Subset of ProjectiveSpace TOP-REAL 3 equals :: BKMODEL1:def 7 conic(1,1,-1,0,0,0); end; theorem :: BKMODEL1:82 for O being Matrix of 3,REAL for P being Element of ProjectiveSpace TOP-REAL 3 for p being FinSequence of REAL st O = symmetric_3(1,1,-1,0,0,0) & P = Dir u & u = p holds P in absolute iff SumAll QuadraticForm(p,O,p) = 0; theorem :: BKMODEL1:83 for P being Element of absolute st P = Dir u holds u.3 <> 0; theorem :: BKMODEL1:84 for P being Element of absolute st P = Dir u & u.3 = 1 holds |[u.1,u.2]| in circle(0,0,1); theorem :: BKMODEL1:85 for P being Point of ProjectiveSpace TOP-REAL 3 st P = Dir u & u.3 = 1 & |[u.1,u.2]| in circle(0,0,1) holds P is Element of absolute; theorem :: BKMODEL1:86 for P being Point of ProjectiveSpace TOP-REAL 3 for u being non zero Element of TOP-REAL 3 st P = Dir u & u.3 = 1 holds |[u.1,u.2]| in circle(0,0,1) iff P is Element of absolute; definition let P be Element of absolute; func absolute_to_REAL2(P) -> Element of circle(0,0,1) means :: BKMODEL1:def 8 ex u being non zero Element of TOP-REAL 3 st P = Dir u & u.3 = 1 & it = |[u.1,u.2]|; end; theorem :: BKMODEL1:87 the carrier of Tunit_circle(2) = circle(0,0,1); definition let u be non zero Element of TOP-REAL 2; assume u in circle(0,0,1); func REAL2_to_absolute(u) -> Element of absolute equals :: BKMODEL1:def 9 Dir |[u.1,u.2,1]|; end; theorem :: BKMODEL1:88 for u being Element of TOP-REAL 3 st qfconic(1,1,-1,0,0,0,u) = 0 & u.3 = 1 holds|[u.1,u.2]| in Sphere(0.TOP-REAL 2,1); theorem :: BKMODEL1:89 for P being Element of absolute holds ex u st (u.1)^2 + (u.2)^2 = 1 & u.3 = 1 & P = Dir u; theorem :: BKMODEL1:90 for P being Element of absolute ex Q being Element of absolute st P <> Q; theorem :: BKMODEL1:91 for a,b being Real st a^2 + b^2 = 1 holds |[-b,a,0]| is non zero; theorem :: BKMODEL1:92 for P,Q,R being Element of absolute st P,Q,R are_mutually_distinct holds not P,Q,R are_collinear; theorem :: BKMODEL1:93 for ra being non zero Real for O,N,M being invertible Matrix of 3,F_Real st O = symmetric_3(1,1,-1,0,0,0) & M = symmetric_3(ra,ra,-ra,0,0,0) & M = N@ * O * N & homography(M).:absolute = absolute holds homography(N).:absolute = absolute;