:: Beltrami-Klein Model, {P}art {I}
:: by Roland Coghetto
::
:: Received March 27, 2018
:: Copyright (c) 2018 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;