:: Beltrami-Klein model, Part {III}
:: by Roland Coghetto
::
:: Received December 30, 2019
:: Copyright (c) 2019-2026 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 TREES_1, MATRIX_6, 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, GROUP_1, MONOID_0, TARSKI,
XXREAL_0, PASCAL, INCPROJ, ZFMISC_1, SQUARE_1, JGRAPH_6, FINSEQ_1,
FUNCT_3, BKMODEL1, BKMODEL2, BKMODEL3, PBOOLE, BINOP_1, RLTOPSP1,
GTARSKI1;
notations BINOP_1, RELSET_1, ORDINAL1, XCMPLX_0, PRE_TOPC, TARSKI, GROUP_1,
XBOOLE_0, RLVECT_1, COLLSP, EUCLID_5, PASCAL, XXREAL_0, INCPROJ,
DOMAIN_1, INCSP_1, SQUARE_1, XREAL_0, JGRAPH_6, ZFMISC_1, SUBSET_1,
FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, ALGSTR_0, VECTSP_1, EUCLID,
ANPROJ_1, MATRIX_0, MATRIX_6, ANPROJ_8, MATRIX_1, MATRIX_3, QUIN_1,
BKMODEL1, BKMODEL2, RLTOPSP1, GTARSKI1;
constructors REALSET1, RELSET_1, MONOID_0, EUCLID_5, MATRIX13, ANPROJ_8,
PASCAL, SQUARE_1, QUIN_1, BKMODEL2, GTARSKI2, MATRIX_3;
registrations SUBSET_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, ANPROJ_9, SQUARE_1, XCMPLX_0, QUIN_1, TOPREALC;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions TARSKI, GROUP_1, GTARSKI1;
equalities ALGSTR_0, BKMODEL1, XCMPLX_0, SQUARE_1;
expansions STRUCT_0, XBOOLE_0, GTARSKI1;
theorems MATRIX_6, XREAL_1, EUCLID_5, ANPROJ_1, XCMPLX_1, RVSUM_1, FINSEQ_1,
MATRIX_3, FUNCT_1, FUNCT_2, ANPROJ_8, GROUP_1, INCPROJ, ANPROJ_9, PASCAL,
XBOOLE_0, SQUARE_1, COLLSP, MATRIX_0, ZFMISC_1, RELAT_1, HESSENBE,
BKMODEL1, BKMODEL2, QUIN_1, XXREAL_0, XTUPLE_0, RELSET_1;
schemes FUNCT_2, BINOP_1, BINOP_2, RELSET_1;
begin :: Preliminaries
theorem
for x,y being Real st x * y < 0 holds 0 < x / (x - y) < 1
proof
let x,y be Real;
assume
A1: x * y < 0;
then x <> 0 & y <> 0;
then per cases;
suppose
A2: x < 0;
then y > 0 by A1;
then x - y < x by XREAL_1:44;
hence thesis by A2,XREAL_1:190;
end;
suppose
A3: 0 < x;
then y < 0 by A1;
then x < x - y by XREAL_1:46;
hence thesis by A3,XREAL_1:189;
end;
end;
theorem Th02:
for a being non zero Real, b, r being Real
st r = sqrt (a^2 + b^2) holds
r is positive & (a / r)^2 + (b / r)^2 = 1
proof
let a be non zero Real;
let b,r be Real;
assume
A1: r = sqrt (a^2 + b^2);
thus r is positive by A1,SQUARE_1:25;
reconsider r as positive Real by A1,SQUARE_1:25;
(a / r)^2 = a^2 / r^2 & (b / r)^2 = b^2 / r^2 by XCMPLX_1:76;
then (a / r)^2 + (b / r)^2 = (a^2 + b^2) / r^2
.= r^2 / r^2 by A1,SQUARE_1:def 2
.= 1 by XCMPLX_1:60;
hence thesis;
end;
theorem Th03:
for a being non zero Real,
b,c,d,e being Real st
a * b = c - d * e holds
b^2 = (c^2/a^2) - 2 * ((c * d) / (a * a)) * e + (d^2 / a^2) * e^2
proof
let a be non zero Real;
let b,c,d,e be Real;
assume
A1: a * b = c - d * e;
b = (a * b) / a by XCMPLX_1:89
.= (c / a - (d * e) / a) by A1,XCMPLX_1:120
.= (c / a - (d / a) * e);
then b^2 = (c / a)^2 - 2 * (c / a) * ((d / a) * e) + ((d / a) * e)^2
.= (c^2 / a^2) - 2 * (c / a) * ((d / a) * e) + ((d / a)^2 * e^2)
by XCMPLX_1:76
.= (c^2 / a^2) - 2 * ((c / a) * (d / a)) * e + ((d^2 / a^2) * e^2)
by XCMPLX_1:76
.= (c^2 / a^2) - 2 * ((c * d) / (a * a)) * e + ((d^2 / a^2) * e^2)
by XCMPLX_1:76;
hence thesis;
end;
theorem Th04:
for a,b,c being Complex st a <> 0 holds (a^2 * b) * c / a^2 = b * c
proof
let a,b,c be Complex;
assume
A1: a <> 0;
(a^2 * b) * c / a^2 = b * a^2 * (c / a^2)
.= b * c by A1,XCMPLX_1:90;
hence thesis;
end;
theorem Th05:
for a,b,c being Complex st a <> 0 holds 2 * (a^2 * b) * c / a^2 = 2 * b * c
proof
let a,b,c be Complex;
assume a <> 0;
then (a^2 * b) * c / a^2 = b * c by Th04;
hence thesis;
end;
theorem Th07:
for a being Real st 1 < a holds 1 / a - 1 < 0
proof
let a be Real;
assume 1 < a;
then 1 / a < 1 / 1 by XREAL_1:76;
then 1 / a - 1 < 1 - 1 by XREAL_1:9;
hence thesis;
end;
theorem Th08:
for a,b being Real st 0 < a & 1 < b holds a / b - a < 0
proof
let a,b be Real;
assume that
A1: 0 < a and
A2: 1 < b;
A3: a / b - a = a * ( 1 / b - 1);
(1 / b - 1) < 0 by A2,Th07;
hence thesis by A1,A3;
end;
theorem Th09:
for a being non zero Real,
b,c,d being Real st
a^2 + c^2 = b^2 & 1 < b^2 holds
not ((b^2)^2 / a^2) - 2 * ((b^2 * c) / (a * a)) * d
+ (c^2 / a^2) * d^2 + d^2 = 1
proof
let a be non zero Real;
let b,c,d be Real;
assume that
A1: a^2 + c^2 = b^2 and
A2: 1 < b^2;
assume
A5: ((b^2)^2 / a^2) - 2 * ((b^2 * c) / (a * a)) * d
+ (c^2 / a^2) * d^2 + d^2 = 1;
c^2 / a^2 + 1 = c^2 / a^2 + (a^2 / a^2) by XCMPLX_1:60
.= b^2 / a^2 by A1;
then
A6: a^2 * (c^2 / a^2 + 1) = a^2 * b^2 / a^2 by XCMPLX_1:74
.= b^2 by XCMPLX_1:89;
A7: a^2 * (2 * ((b^2 * c) / (a * a))) = 2 * (a^2 * (b^2 * c) / (a * a))
.= 2 * (b^2 * c) by XCMPLX_1:89;
A8: (a^2) * ((b^2)^2 / a^2) - (a^2) * 1
= ((a^2) * (b^2)^2) / a^2 - (a^2) * 1
.= (b^2)^2 - a^2 by XCMPLX_1:89;
a^2 * 0 = a^2 * ((c^2 / a^2 + 1) * d^2 - 2 * ((b^2 * c) / (a * a)) * d
+ ((b^2)^2 / a^2) - 1) by A5;
then
A9: 0 = (a^2) * (c^2 / a^2 + 1) * d^2
- (a^2) * 2 * ((b^2 * c) / (a * a)) * d + (a^2) * ((b^2)^2 / a^2)
- (a^2) * 1;
A11: b <> 0 by A6;
A12: 0 = (b^2 * d^2 - 2 * (b^2 * c) * d + (b^2)^2 - a^2)/(b^2) by A9,A6,A7,A8
.= d^2 * b^2 / b^2 - 2 * (b^2 * c) * d / b^2
+ (b^2)^2 / b^2 - a^2 / b^2
.= d^2 - 2 * (b^2 * c) * d / b^2 + (b^2)^2 / b^2 - a^2 / b^2
by A6,XCMPLX_1:89
.= d^2 - 2 * c * d + (b^2)^2 / b^2 - a^2 / b^2 by A11,Th05
.= d^2 + (-2 * c) * d + b^2 - a^2 / b^2 by A6,XCMPLX_1:89
.= 1 * d^2 + (-2 * c) * d + (b^2 - a^2 / b^2);
reconsider c1 = 1, c2 = -2 * c, c3 = b^2 - a^2 / b^2 as Real;
A13:a^2 / b^2 - a^2 < 0 by A2,Th08;
delta(c1,c2,c3) < 0
proof
c2^2 - 4 * c1 * c3 = 4 * (c^2 - (b^2 - a^2 / b^2));
hence thesis by A1,A13,QUIN_1:def 1;
end;
hence contradiction by A12,QUIN_1:3;
end;
theorem Th10:
for a,b,c being Real st a * (- b) = c & a * c = b holds
c = 0 & b = 0
proof
let a,b,c be Real;
assume that
A1: a * (-b) = c and
A2: a * c = b;
a * (- a * c) = c by A1,A2; then
A3: (-a * a) * c = c;
thus c = 0
proof
assume c <> 0;
then - a^2 = 1 by A3,XCMPLX_1:7;
hence contradiction;
end;
hence b = 0 by A2;
end;
theorem
for a being positive Real holds (sqrt a) / a = 1 / sqrt a
proof
let a be positive Real;
a = sqrt (a^2) by SQUARE_1:def 2
.= sqrt a * sqrt a by SQUARE_1:29; then
(sqrt a) / a = sqrt a / sqrt a / sqrt a by XCMPLX_1:78;
hence thesis by XCMPLX_1:60,SQUARE_1:24;
end;
registration
let a be non zero Real;
let b,c be Real;
cluster |[a,b,c]| -> non zero for Element of TOP-REAL 3;
coherence
proof
now
assume |[a,b,c]| is zero;
then a = |[0,0,0]|`1 by EUCLID_5:2,4;
hence contradiction by EUCLID_5:2;
end;
hence thesis;
end;
cluster |[c,a,b]| -> non zero for Element of TOP-REAL 3;
coherence
proof
now
assume |[c,a,b]| is zero;
then a = |[0,0,0]|`2 by EUCLID_5:2,4;
hence contradiction by EUCLID_5:2;
end;
hence thesis;
end;
cluster |[b,c,a]| -> non zero for Element of TOP-REAL 3;
coherence
proof
now
assume |[b,c,a]| is zero;
then a = |[0,0,0]|`3 by EUCLID_5:2,4;
hence contradiction by EUCLID_5:2;
end;
hence thesis;
end;
end;
definition
let P be Element of real_projective_plane;
assume
A0: P in absolute \/ BK_model;
func #P -> non zero Element of TOP-REAL 3 means :Def01:
Dir it = P & it.3 = 1;
existence
proof
per cases by A0,XBOOLE_0:def 3;
suppose P in absolute;
then reconsider P1 = P as Element of absolute;
consider u be non zero Element of TOP-REAL 3 such that
A1: P1 = Dir u & u.3 = 1 and
absolute_to_REAL2(P1) = |[u.1,u.2]| by BKMODEL1:def 8;
take u;
thus thesis by A1;
end;
suppose P in BK_model;
then reconsider P1 = P as Element of BK_model;
consider u be non zero Element of TOP-REAL 3 such that
A2: Dir u = P1 & u.3 = 1 and
BK_to_REAL2 P1 = |[u.1,u.2]| by BKMODEL2:def 2;
take u;
thus thesis by A2;
end;
end;
uniqueness
proof
let u,v be non zero Element of TOP-REAL 3 such that
A3: Dir u = P & u.3 = 1 and
A4: Dir v = P & v.3 = 1 ;
are_Prop u,v by A3,A4,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A5: u = a * v by ANPROJ_1:1;
1 = a * v.3 by A5,A3,RVSUM_1:44
.= a by A4;
hence thesis by A5,RVSUM_1:52;
end;
end;
theorem Th11:
for P being Element of real_projective_plane holds
ex Q being Element of BK_model st P <> Q
proof
let P be Element of real_projective_plane;
per cases;
suppose
A1: #P = |[0,0,1]|;
reconsider u = |[0,1/2,1]| as non zero Element of TOP-REAL 3;
reconsider Q = Dir u as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
now
let v be Element of TOP-REAL 3;
assume v is non zero & Q = Dir v;
then are_Prop u,v by ANPROJ_1:22;
then consider a be Real such that
A2: a <> 0 and
A3: v = a * u by ANPROJ_1:1;
v = |[a * 0,a * (1/2),a * 1]| by A3,EUCLID_5:8
.= |[0,a/2,a]|; then
A4: v.1 = 0 & v.2 = a/2 & v.3 = a by FINSEQ_1:45;
qfconic(1,1,-1,0,0,0,v) = 1 * v.1 * v.1 + 1 * v.2 * v.2
+ (- 1) * v.3 * v.3
+ 0 * v.1 * v.2 + 0 * v.1 * v.3 + 0 * v.2 * v.3 by PASCAL:def 1
.= a^2 * (-3/4) by A4;
hence qfconic(1,1,-1,0,0,0,v) is negative by A2;
end;
then Q in {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(1,1,-1,0,0,0,u) is negative};
then reconsider Q as Element of BK_model
by BKMODEL2:def 1;
reconsider Q9 = Q as Element of real_projective_plane;
take Q;
Q <> P
proof
assume
A6: Q = P;
A7: Q9 = Dir u & u.3 = 1 by FINSEQ_1:45;
Q9 in absolute \/ BK_model by XBOOLE_0:def 3;
then |[0,0,1]| = |[0,1/2,1]| by A7,Def01,A6,A1;
hence contradiction by FINSEQ_1:78;
end;
hence thesis;
end;
suppose
A8: #P <> |[0,0,1]|;
reconsider u = |[0,0,1]| as non zero Element of TOP-REAL 3;
reconsider Q = Dir u as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
now
let v be Element of TOP-REAL 3;
assume v is non zero & Q = Dir v;
then are_Prop u,v by ANPROJ_1:22;
then consider a be Real such that
A9: a <> 0 and
A10: v = a * u by ANPROJ_1:1;
v = |[a * 0,a * 0,a * 1]| by A10,EUCLID_5:8
.= |[0,0,a]|; then
A11: v.1 = 0 & v.2 = 0 & v.3 = a by FINSEQ_1:45;
qfconic(1,1,-1,0,0,0,v) = 1 * v.1 * v.1 + 1 * v.2 * v.2
+ (- 1) * v.3 * v.3
+ 0 * v.1 * v.2 + 0 * v.1 * v.3 + 0 * v.2 * v.3 by PASCAL:def 1
.= a^2 * (-1) by A11;
hence qfconic(1,1,-1,0,0,0,v) is negative by A9;
end;
then Q in {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(1,1,-1,0,0,0,u) is negative};
then reconsider Q as Element of BK_model
by BKMODEL2:def 1;
reconsider Q9 = Q as Element of real_projective_plane;
take Q;
Q <> P
proof
assume
A13: Q = P;
A14: Q9 = Dir u & u.3 = 1 by FINSEQ_1:45;
Q9 in absolute \/ BK_model by XBOOLE_0:def 3;
hence contradiction by A14,A8,Def01,A13;
end;
hence thesis;
end;
end;
reserve P for Element of BK_model;
theorem
ex P1,P2 being Element of absolute st
P1 <> P2 & P1,P,P2 are_collinear
proof
consider Q be Element of BK_model such that
A1: P <> Q by Th11;
consider P1,P2 be Element of absolute such that
A2: P1 <> P2 and
A3: P,Q,P1 are_collinear and
A4: P,Q,P2 are_collinear by A1,BKMODEL2:20;
take P1,P2;
P,P1,P2 are_collinear by A1,A3,A4,COLLSP:6;
hence thesis by A2,COLLSP:4;
end;
theorem
for Q being Element of absolute holds
ex R being Element of BK_model st P <> R & P,Q,R are_collinear
proof
let Q be Element of absolute;
reconsider P1 = P,Q1 = Q as Element of real_projective_plane;
consider R1 be Element of real_projective_plane such that
A1: R1 in BK_model and
A2: P1 <> R1 and
A3: R1,P1,Q1 are_collinear by BKMODEL2:22;
reconsider R = R1 as Element of BK_model by A1;
take R;
thus thesis by A3,A2,HESSENBE:1;
end;
theorem Th12:
for L being LINE of IncProjSp_of real_projective_plane
st P in L holds ex P1,P2 being Element of absolute st P1 <> P2 &
P1 in L & P2 in L
proof
let L be LINE of IncProjSp_of real_projective_plane;
assume
A1: P in L;
consider Q be Element of ProjectiveSpace TOP-REAL 3 such that
A2: P <> Q and
A3: Q in L by BKMODEL2:8;
consider R be Element of absolute such that
A4: P,Q,R are_collinear by A2,BKMODEL2:19;
reconsider p = P,r = R as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
reconsider L9 = L as LINE of real_projective_plane by INCPROJ:4;
Line(P,Q) = L9 by A1,A2,A3,COLLSP:19;
then P in L9 & Q in L9 & R in L9 by A1,A3,A4,COLLSP:11;
then p on L & r on L by INCPROJ:5;
then consider p1,p2 be POINT of IncProjSp_of real_projective_plane,
P1,P2 be Element of real_projective_plane such that
A5: p1 = P1 and
A6: p2 = P2 and
A7: P1 <> P2 and
A8: P1 in absolute and
A9: P2 in absolute and
A10:p1 on L and
A11:p2 on L by BKMODEL2:23;
reconsider P1,P2 as Element of absolute by A8,A9;
take P1,P2;
P1 in L9 & P2 in L9 by A5,A6,A10,A11,INCPROJ:5;
hence thesis by A7;
end;
definition
let N be invertible Matrix of 3,F_Real;
func line_homography(N) -> Function of
the Lines of IncProjSp_of real_projective_plane,
the Lines of IncProjSp_of real_projective_plane means
:Def02:
for x being LINE of IncProjSp_of real_projective_plane holds
it.x = {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on x};
existence
proof
defpred P[object,object] means
ex x being LINE of IncProjSp_of real_projective_plane st
$1 = x & $2 = {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on x};
A1: for x being object st x in the Lines of IncProjSp_of real_projective_plane
ex y being object st y in the Lines of IncProjSp_of real_projective_plane
& P[x,y]
proof
let x be object;
assume x in the Lines of IncProjSp_of real_projective_plane;
then reconsider x9 = x as Element of
the Lines of IncProjSp_of real_projective_plane;
set y = {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on x9};
consider p,q be Point of real_projective_plane such that
A2: p <> q and
A3: x9 = Line(p,q) by COLLSP:def 7,INCPROJ:4;
reconsider p9 = homography(N).p,
q9 = homography(N).q as Point of real_projective_plane
by FUNCT_2:5;
A4: y = Line(p9,q9)
proof
A5: y c= Line(p9,q9)
proof
let x be object;
assume x in y;
then consider Px be POINT of IncProjSp_of real_projective_plane
such that
A6: x = homography(N).Px and
A7: Px on x9;
reconsider Px as Point of real_projective_plane by INCPROJ:3;
x9 is LINE of real_projective_plane by INCPROJ:4;
then
A8: Px in x9 by A7,INCPROJ:5;
reconsider p1 = p,q1 = q,r1 = Px,p2 = p9,q2 = q9 as
Point of ProjectiveSpace TOP-REAL 3;
homography(N).p1,homography(N).q1,homography(N).r1 are_collinear
by A8,A3,COLLSP:11,ANPROJ_8:102;
hence thesis by A6,COLLSP:11;
end;
Line(p9,q9) c= y
proof
let x be object;
assume x in Line(p9,q9);
then x in {p where p is Element of real_projective_plane:
p9,q9,p are_collinear} by COLLSP:def 5;
then consider x99 be Element of real_projective_plane such that
A9: x = x99 and
A10: p9,q9,x99 are_collinear;
reconsider p1 = p,q1 = q,r1 = x99, p2 = p9,q2 = q9 as
Point of ProjectiveSpace TOP-REAL 3;
reconsider r2 = homography(N~).r1 as
Point of ProjectiveSpace TOP-REAL 3;
reconsider r3 = r2 as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
A11: r1 = homography(N).r2 by ANPROJ_9:15;
A12: x9 is LINE of real_projective_plane by INCPROJ:4;
r2 in x9 by A3,A10,A11,ANPROJ_8:102,COLLSP:11;
then r3 on x9 by A12,INCPROJ:5;
hence thesis by A11,A9;
end;
hence thesis by A5;
end;
reconsider y9 = Line(p9,q9) as LINE of real_projective_plane
by A2,ANPROJ_9:16,COLLSP:def 7;
reconsider y = y9 as LINE of IncProjSp_of real_projective_plane
by INCPROJ:4;
y is Element of the Lines of IncProjSp_of real_projective_plane;
then reconsider y = {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on x9} as
Element of the Lines of IncProjSp_of real_projective_plane by A4;
take y;
thus thesis;
end;
consider f be Function of
(the Lines of IncProjSp_of real_projective_plane),
(the Lines of IncProjSp_of real_projective_plane) such that
A13: for x be object st x in the Lines of IncProjSp_of real_projective_plane
holds P[x,f.x] from FUNCT_2:sch 1(A1);
for x be LINE of IncProjSp_of real_projective_plane holds
f.x = {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on x}
proof
let x be LINE of IncProjSp_of real_projective_plane;
P[x,f.x] by A13;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let h1,h2 be Function of
(the Lines of IncProjSp_of real_projective_plane),
(the Lines of IncProjSp_of real_projective_plane) such that
A14: for x be LINE of IncProjSp_of real_projective_plane holds
h1.x = {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on x} and
A15: for x be LINE of IncProjSp_of real_projective_plane holds
h2.x = {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on x};
now
dom h1 = the Lines of IncProjSp_of real_projective_plane
by FUNCT_2:def 1;
hence dom h1 = dom h2 by FUNCT_2:def 1;
hereby
let x9 be object;
assume x9 in dom h1;
then reconsider y = x9 as LINE of IncProjSp_of real_projective_plane;
h1.y = {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on y} by A14
.= h2.y by A15;
hence h1.x9 = h2.x9;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
end;
reserve N,N1,N2 for invertible Matrix of 3,F_Real;
reserve l,l1,l2 for Element of the Lines of IncProjSp_of real_projective_plane;
theorem Th13:
(line_homography(N1)).((line_homography(N2)).l)
= (line_homography(N1 * N2)).l
proof
reconsider l2 = (line_homography(N2)).l as
LINE of IncProjSp_of real_projective_plane;
A1: l2 = {homography(N2).P where
P is POINT of IncProjSp_of real_projective_plane : P on l} by Def02;
A2: (line_homography(N1)).((line_homography(N2)).l) = {homography(N1).P where
P is POINT of IncProjSp_of real_projective_plane : P on l2} by Def02;
set X = {homography(N1).P where
P is POINT of IncProjSp_of real_projective_plane : P on l2},
Y = {homography(N1 * N2).P where
P is POINT of IncProjSp_of real_projective_plane : P on l};
{homography(N1).P where
P is POINT of IncProjSp_of real_projective_plane : P on l2}
= {homography(N1 * N2).P where
P is POINT of IncProjSp_of real_projective_plane : P on l}
proof
A3: X c= Y
proof
let x be object;
assume x in X;
then consider P be POINT of IncProjSp_of real_projective_plane
such that
A4: x = homography(N1).P and
A5: P on l2;
A6: P is Point of real_projective_plane by INCPROJ:3;
l2 is LINE of real_projective_plane by INCPROJ:4;
then P in {homography(N2).P where
P is POINT of IncProjSp_of real_projective_plane : P on l}
by A6,A1,A5,INCPROJ:5;
then consider P2 be POINT of IncProjSp_of real_projective_plane
such that
A7: P = homography(N2).P2 and
A8: P2 on l;
P2 is Point of real_projective_plane by INCPROJ:3;
then x = (homography(N1*N2)).P2 by A4,A7,ANPROJ_9:13;
hence thesis by A8;
end;
Y c= X
proof
let x be object;
assume x in Y;
then consider P be POINT of IncProjSp_of real_projective_plane
such that
A9: x = homography(N1*N2).P and
A10: P on l;
A11: P is Point of real_projective_plane by INCPROJ:3;
P is Element of ProjectiveSpace TOP-REAL 3 by INCPROJ:3;
then homography(N2).P is Point of real_projective_plane by FUNCT_2:5;
then reconsider P2 = homography(N2).P as
POINT of IncProjSp_of real_projective_plane by INCPROJ:3;
now
thus x = homography(N1).P2 by A11,A9,ANPROJ_9:13;
A12: P2 in l2 by A10,A1;
l2 is LINE of real_projective_plane by INCPROJ:4;
hence P2 on l2 by A12,INCPROJ:5;
end;
hence thesis;
end;
hence thesis by A3;
end;
hence thesis by A2,Def02;
end;
theorem Th14:
(line_homography(1.(F_Real,3))).l = l
proof
set X = {homography(1.(F_Real,3)).P where
P is POINT of IncProjSp_of real_projective_plane : P on l};
A1: X c= l
proof
let x be object;
assume x in X;
then consider P be POINT of IncProjSp_of real_projective_plane such that
A2: x = homography(1.(F_Real,3)).P and
A3: P on l;
A4: P is Point of real_projective_plane by INCPROJ:2;
then
A5: x = P by A2,ANPROJ_9:14;
l is LINE of real_projective_plane by INCPROJ:4;
hence thesis by A4,A3,A5,INCPROJ:5;
end;
l c= X
proof
let x be object;
assume
A6: x in l;
A7: l is LINE of real_projective_plane by INCPROJ:4;
l is Subset of real_projective_plane by INCPROJ:4;
then reconsider x9 = x as Point of real_projective_plane by A6;
reconsider l9 = l as LINE of IncProjSp_of real_projective_plane;
reconsider x99 = x9 as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
A8: x99 on l by A7,A6,INCPROJ:5;
homography(1.(F_Real,3)).x99 = x99 by ANPROJ_9:14;
hence thesis by A8;
end;
hence thesis by A1,Def02;
end;
theorem Th15:
(line_homography(N)).((line_homography(N~)).l) = l &
(line_homography(N~)).((line_homography(N)).l) = l
proof
A1: N~ is_reverse_of N by MATRIX_6:def 4;
thus (line_homography(N)).((line_homography(N~)).l)
= (line_homography(N * N~)).l by Th13
.= (line_homography(1.(F_Real,3))).l by A1,MATRIX_6:def 2
.= l by Th14;
thus (line_homography(N~)).((line_homography(N)).l)
= (line_homography(N~ * N)).l by Th13
.= (line_homography(1.(F_Real,3))).l by A1,MATRIX_6:def 2
.= l by Th14;
end;
theorem
(line_homography(N)).l1 = (line_homography(N)).l2 implies l1 = l2
proof
assume (line_homography(N)).l1 = (line_homography(N)).l2;
then l1 = (line_homography(N~)).((line_homography(N)).l2) by Th15
.= l2 by Th15;
hence thesis;
end;
definition
func EnsLineHomography3 -> set equals
the set of all line_homography(N) where N is invertible Matrix of 3,F_Real;
coherence;
end;
registration
cluster EnsLineHomography3 -> non empty;
coherence
proof
line_homography(1.(F_Real,3)) in EnsLineHomography3;
hence thesis;
end;
end;
definition
let h1,h2 be Element of EnsLineHomography3;
func h1 (*) h2 -> Element of EnsLineHomography3 means
:Def03:
ex N1,N2 being invertible Matrix of 3,F_Real st h1 = line_homography(N1) &
h2 = line_homography(N2) & it = line_homography(N1 * N2);
existence
proof
h1 in the set of all line_homography(N) where
N is invertible Matrix of 3,F_Real;
then consider N1 be invertible Matrix of 3,F_Real such that
A1: h1 = line_homography(N1);
h2 in the set of all line_homography(N) where
N is invertible Matrix of 3,F_Real;
then consider N2 be invertible Matrix of 3,F_Real such that
A2: h2 = line_homography(N2);
line_homography(N1 * N2) in EnsLineHomography3;
hence thesis by A1,A2;
end;
uniqueness
proof
let H1,H2 be Element of EnsLineHomography3 such that
A3: ex N1,N2 being invertible Matrix of 3,F_Real st h1 = line_homography(N1) &
h2 = line_homography(N2) & H1 = line_homography(N1 * N2) and
A4: ex N1,N2 being invertible Matrix of 3,F_Real st h1 = line_homography(N1) &
h2 = line_homography(N2) & H2 = line_homography(N1 * N2);
consider NA1,NA2 being invertible Matrix of 3,F_Real such that
A5: h1 = line_homography(NA1) and
A6: h2 = line_homography(NA2) and
A7: H1 = line_homography(NA1 * NA2) by A3;
consider NB1,NB2 being invertible Matrix of 3,F_Real such that
A8: h1 = line_homography(NB1) and
A9: h2 = line_homography(NB2) and
A10: H2 = line_homography(NB1 * NB2) by A4;
reconsider fH1 = H1,fH2 = H2 as
Function of (the Lines of IncProjSp_of real_projective_plane),
(the Lines of IncProjSp_of real_projective_plane) by A7,A10;
now
dom fH1 = the Lines of IncProjSp_of real_projective_plane
by FUNCT_2:def 1;
hence dom fH1 = dom fH2 by FUNCT_2:def 1;
thus for x be object st x in dom fH1 holds fH1.x = fH2.x
proof
let x be object;
assume x in dom fH1;
then reconsider P = x as Element of the Lines of
IncProjSp_of real_projective_plane;
fH1.x = (line_homography(NB1)).((line_homography(NB2)).P)
by A5,A6,A7,A8,A9,Th13
.= fH2.x by A10,Th13;
hence thesis;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
end;
theorem Th16:
for h1,h2 being Element of EnsLineHomography3 st
h1 = line_homography(N1) & h2 = line_homography(N2) holds
line_homography(N1 * N2) = h1 (*) h2
proof
let h1,h2 be Element of EnsLineHomography3;
assume that
A1: h1 = line_homography(N1) and
A2: h2 = line_homography(N2);
consider M1,M2 be invertible Matrix of 3,F_Real such that
A3: h1 = line_homography(M1) and
A4: h2 = line_homography(M2) and
A5: h1 (*) h2 = line_homography(M1 * M2) by Def03;
reconsider h12 = h1 (*) h2 as
Function of the Lines of IncProjSp_of real_projective_plane,
the Lines of IncProjSp_of real_projective_plane by A5;
now
dom line_homography(N1 * N2)
= the Lines of IncProjSp_of real_projective_plane
by FUNCT_2:def 1;
hence dom line_homography(N1 * N2) = dom h12 by FUNCT_2:def 1;
thus for x be object st x in dom line_homography(N1 * N2) holds
(line_homography(N1 * N2)).x = h12.x
proof
let x be object;
assume x in dom line_homography(N1 * N2);
then reconsider xf = x as
Element of the Lines of IncProjSp_of real_projective_plane;
(line_homography(N1 * N2)).xf
= (line_homography(N1)).((line_homography(N2)).xf)
by Th13
.= h12.xf by A3,A4,A5,A1,A2,Th13;
hence thesis;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
theorem Th17:
for x,y,z being Element of EnsLineHomography3 holds
(x (*) y) (*) z = x (*) (y (*) z)
proof
let x,y,z be Element of EnsLineHomography3;
x in EnsLineHomography3;
then consider Nx be invertible Matrix of 3,F_Real such that
A2: x = line_homography(Nx);
y in EnsLineHomography3;
then consider Ny be invertible Matrix of 3,F_Real such that
A3: y = line_homography(Ny);
z in EnsLineHomography3;
then consider Nz be invertible Matrix of 3,F_Real such that
A4: z = line_homography(Nz);
A5: width Nx = 3 & len Ny = 3 & width Ny = 3 & len Nz = 3 by MATRIX_0:24;
y (*) z = line_homography(Ny * Nz) by A3,A4,Th16; then
A6: (x (*) (y (*) z)) = line_homography(Nx * (Ny * Nz)) by A2,Th16
.= line_homography((Nx * Ny) * Nz) by A5,MATRIX_3:33;
x (*) y = line_homography(Nx * Ny) by A2,A3,Th16;
hence thesis by A6,A4,Th16;
end;
definition
func BinOpLineHomography3 -> BinOp of EnsLineHomography3 means :Def04:
for h1,h2 being Element of EnsLineHomography3 holds it.(h1,h2) = h1 (*) h2;
existence from BINOP_1:sch 4;
uniqueness from BINOP_2:sch 2;
end;
definition
func GroupLineHomography3 -> strict multMagma equals
multMagma(# EnsLineHomography3, BinOpLineHomography3 #);
coherence;
end;
set GLH3 = GroupLineHomography3;
Lm1:
now
let e be Element of GLH3 such that
A1: e = line_homography(1.(F_Real,3));
let h be Element of GLH3;
reconsider h1 = h,h2 = e as Element of EnsLineHomography3;
consider N1,N2 be invertible Matrix of 3,F_Real such that
A2: h1 = line_homography(N1) and
A3: h2 = line_homography(N2) and
A4: h1 (*) h2 = line_homography(N1 * N2) by Def03;
line_homography(N1 * N2) = line_homography(N1)
proof
dom line_homography(N1 * N2)
= the Lines of IncProjSp_of real_projective_plane
by FUNCT_2:def 1;
then
A5: dom line_homography(N1 * N2) = dom line_homography(N1) by FUNCT_2:def 1;
for x be object st x in dom line_homography(N1) holds
(line_homography(N1 * N2)).x = (line_homography(N1)).x
proof
let x be object;
assume x in dom line_homography(N1);
then reconsider xf = x as Element of
the Lines of IncProjSp_of real_projective_plane;
(line_homography(N1 * N2)).xf
= (line_homography(N1)).((line_homography(N2)).xf)
by Th13
.= (line_homography(N1)).xf by A1,A3,Th14;
hence thesis;
end;
hence thesis by A5,FUNCT_1:def 11;
end;
hence h * e = h by Def04,A2,A4;
consider N2,N1 be invertible Matrix of 3,F_Real such that
A6: h2 = line_homography(N2) and
A7: h1 = line_homography(N1) and
A8: h2 (*) h1 = line_homography(N2 * N1) by Def03;
line_homography(N2 * N1) = line_homography(N1)
proof
dom line_homography(N2 * N1)
= the Lines of IncProjSp_of real_projective_plane
by FUNCT_2:def 1;
then
A9: dom line_homography(N2 * N1) = dom line_homography(N1) by FUNCT_2:def 1;
for x be object st x in dom line_homography(N1) holds
(line_homography(N2 * N1)).x = (line_homography(N1)).x
proof
let x be object;
assume x in dom line_homography(N1);
then reconsider xf = x as Element of
the Lines of IncProjSp_of real_projective_plane;
(line_homography(N2 * N1)).xf
= (line_homography(N2)).((line_homography(N1)).xf) by Th13
.= (line_homography(N1)).xf by A1,A6,Th14;
hence thesis;
end;
hence thesis by A9,FUNCT_1:def 11;
end;
hence e * h = h by Def04,A7,A8;
end;
Lm2:
now
let e,h,g be Element of GLH3;
let N,Ng be invertible Matrix of 3,F_Real such that
A1: h = line_homography(N) and
A2: g = line_homography(Ng) and
A3: Ng = N~ and
A4: e = line_homography(1.(F_Real,3));
reconsider h1 = h as Element of EnsLineHomography3;
A5: Ng is_reverse_of N by A3,MATRIX_6:def 4;
reconsider g1 = g as Element of EnsLineHomography3;
consider N1,N2 be invertible Matrix of 3,F_Real such that
A6: h1 = line_homography(N1) and
A7: g1 = line_homography(N2) and
A8: h1 (*) g1 = line_homography(N1 * N2) by Def03;
line_homography(N1 * N2) = line_homography(N * Ng)
proof
now
dom line_homography(N1 * N2)
= the Lines of IncProjSp_of real_projective_plane
by FUNCT_2:def 1;
hence dom line_homography(N1 * N2) = dom line_homography(N * Ng)
by FUNCT_2:def 1;
thus for x be object st x in dom line_homography(N1 * N2) holds
(line_homography(N1 * N2)).x = (line_homography(N * Ng)).x
proof
let x be object;
assume x in dom line_homography(N1 * N2);
then reconsider xf = x as
Element of the Lines of IncProjSp_of real_projective_plane;
(line_homography(N1 * N2)).xf
= (line_homography(N)).((line_homography(Ng)).xf)
by Th13,A6,A1,A7,A2
.= (line_homography(N * Ng)).xf by Th13;
hence thesis;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
then h1 (*) g1 = e by A4,A8,A5,MATRIX_6:def 2;
hence h*g = e by Def04;
consider N1,N2 be invertible Matrix of 3,F_Real such that
A9: g1 = line_homography(N1) and
A10: h1 = line_homography(N2) and
A11: g1 (*) h1 = line_homography(N1 * N2) by Def03;
line_homography(N1 * N2) = line_homography(Ng * N)
proof
now
dom line_homography(N1 * N2)
= the Lines of IncProjSp_of real_projective_plane
by FUNCT_2:def 1;
hence dom line_homography(N1 * N2) = dom line_homography(Ng * N)
by FUNCT_2:def 1;
thus for x be object st x in dom line_homography(N1 * N2) holds
(line_homography(N1 * N2)).x = (line_homography(Ng * N)).x
proof
let x be object;
assume x in dom line_homography(N1 * N2);
then reconsider xf = x as
Element of the Lines of IncProjSp_of real_projective_plane;
(line_homography(N1 * N2)).xf
= (line_homography(Ng)).((line_homography(N)).xf)
by Th13,A9,A1,A10,A2
.= (line_homography(Ng * N)).xf by Th13;
hence thesis;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
then g1 (*) h1 = e by A11,A5,A4,MATRIX_6:def 2;
hence g*h = e by Def04;
end;
set e = line_homography(1.(F_Real,3));
e in EnsLineHomography3;
then reconsider e as Element of GLH3;
registration
cluster GroupLineHomography3 -> non empty associative Group-like;
coherence
proof
thus GLH3 is non empty;
thus GLH3 is associative
proof
let x,y,z be Element of GLH3;
reconsider xf=x,yf=y,zf=z as Element of EnsLineHomography3;
A7: x * y = xf (*) yf by Def04;
A8: (x * y) * z = (xf (*) yf) (*) zf by Def04,A7;
y * z = yf (*) zf by Def04;
then x * (y * z) = xf (*) (yf (*) zf) by Def04;
hence thesis by A8,Th17;
end;
take e;
let h be Element of GLH3;
thus h * e = h & e * h = h by Lm1;
h in EnsLineHomography3;
then consider N be invertible Matrix of 3,F_Real such that
A9: h = line_homography(N);
reconsider Ng = N~ as invertible Matrix of 3,F_Real;
line_homography(Ng) in EnsLineHomography3;
then reconsider g = line_homography(Ng) as Element of GLH3;
take g;
thus thesis by A9,Lm2;
end;
end;
theorem Th18:
1_GroupLineHomography3 = line_homography(1.(F_Real,3))
proof
for h being Element of GLH3 holds h * e = h & e * h = h by Lm1;
hence thesis by GROUP_1:4;
end;
theorem
for h,g being Element of GroupLineHomography3
for N,Ng being invertible Matrix of 3,F_Real st
h = line_homography(N) & g = line_homography(Ng) & Ng = N~
holds g = h"
proof
let h,g be Element of GLH3;
let N,Ng be invertible Matrix of 3,F_Real;
assume h = line_homography(N) & g = line_homography(Ng) & Ng = N~;
then h * g = 1_GLH3 & g * h = 1_GLH3 by Lm2,Th18;
hence g = h" by GROUP_1:def 5;
end;
reserve P for Point of ProjectiveSpace TOP-REAL 3,
l for LINE of IncProjSp_of real_projective_plane;
theorem Th19:
homography(N).P in l implies P in (line_homography(N~)).l
proof
assume
A1: homography(N).P in l;
reconsider P9 = homography(N).P as
POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
l is LINE of real_projective_plane by INCPROJ:4;
then
A2: P9 on l by A1,INCPROJ:5;
(line_homography(N~)).l = {homography(N~).P where
P is POINT of IncProjSp_of real_projective_plane : P on l} by Def02;
then homography(N~).P9 in (line_homography(N~)).l by A2;
hence thesis by ANPROJ_9:15;
end;
theorem
P in (line_homography(N)).l implies homography(N~).P in l
proof
assume P in (line_homography(N)).l;
then P in {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on l} by Def02;
then consider P9 be POINT of IncProjSp_of real_projective_plane
such that
A1: P = homography(N).P9 and
A2: P9 on l;
P9 is Element of real_projective_plane by INCPROJ:3;
then
A3: homography(N~).P = P9 by A1,ANPROJ_9:15;
l is LINE of real_projective_plane by INCPROJ:4;
hence thesis by A2,A3,INCPROJ:5;
end;
theorem Th20:
P in l iff homography(N).P in (line_homography(N)).l
proof
hereby
assume
A1: P in l;
reconsider P9 = P as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
l is LINE of real_projective_plane by INCPROJ:4;
then
A2: P9 on l by A1,INCPROJ:5;
(line_homography(N)).l = {homography(N).P where
P is POINT of IncProjSp_of real_projective_plane : P on l} by Def02;
hence homography(N).P in (line_homography(N)).l by A2;
end;
assume homography(N).P in (line_homography(N)).l;
then P in (line_homography(N~)).((line_homography(N)).l) by Th19;
hence P in l by Th15;
end;
theorem Th21:
for u,v,w being non zero Element of TOP-REAL 3 st
u`3 = 1 & v`1 = - u`2 & v`2 = u`1 & v`3 = 0 &
w`3 = 1 & |{ u,v,w }| = 0 holds
(u`1)^2 + (u`2)^2 - (u`1) * (w`1) - (u`2) * (w`2) = 0
proof
let u,v,w be non zero Element of TOP-REAL 3;
assume that
A1: u`3 = 1 and
A2: v`1 = - u`2 and
A3: v`2 = u`1 and
A4: v`3 = 0 and
A5: w`3 = 1 and
A6: |{ u,v,w }| = 0;
set p = u,q = v, r = w;
0 = p`1 * q`2 * r`3 - 1 *q`2*r`1 - p`1*q`3*r`2 + p`2*q`3*r`1
- p`2*q`1*r`3 + 1 *q`1*r`2 by A1,A6,ANPROJ_8:27
.= (p`1)^2 + (p`2)^2 - p`1 * r`1 - p`2 * r`2 by A2,A3,A4,A5;
hence thesis;
end;
theorem Th22:
for a being non zero Real
for b,c being Real holds a * |[b / a,c / a,1]| = |[b,c,a]|
proof
let a be non zero Real;
let b,c be Real;
a * |[b / a,c / a,1]| = |[a * (b / a), a * (c / a),a * 1]| by EUCLID_5:8
.= |[b , a * (c / a),a]| by XCMPLX_1:87
.= |[b, c ,a]| by XCMPLX_1:87;
hence thesis;
end;
theorem Th23:
for u,v,w being non zero Element of TOP-REAL 3 st
u`1 <> 0 & u`3 = 1 & v`1 = - u`2 & v`2 = u`1 & v`3 = 0 &
w`3 = 1 & |{ u,v,w }| = 0 & 1 < (u`1)^2 + (u`2)^2 holds
(w`1)^2 + (w`2)^2 <> 1
proof
let u,v,w be non zero Element of TOP-REAL 3;
assume that
A0: u`1 <> 0 and
A1: u`3 = 1 and
A2: v`1 = - u`2 and
A3: v`2 = u`1 and
A4: v`3 = 0 and
A5: w`3 = 1 and
A6: |{ u,v,w }| = 0 and
A7: 1 < (u`1)^2 + (u`2)^2;
A8: (u`1)^2 + (u`2)^2 - (u`1) * (w`1) - (u`2) * (w`2) = 0
by A1,A2,A3,A4,A5,A6,Th21;
assume
A9: (w`1)^2 + (w`2)^2 = 1;
reconsider x = w`1, y = w`2 as Real;
reconsider u1 = u`1 as non zero Real by A0;
reconsider r = sqrt ((u`1)^2 + (u`2)^2) as positive Real by A0,Th02;
reconsider u2 = u`2 as Real;
A10: r^2 = (u`1)^2 + (u`2)^2 by SQUARE_1:def 2;
then u1 * x = r^2 - u2 * y by A8;
then ((r^2)^2 / u1^2) - 2 * ((r^2 * u2) / (u1 * u1)) * y
+ (u2^2 / u1^2) * y^2 + y^2 = 1 by A9,Th03;
hence contradiction by A10,A7,Th09;
end;
theorem Th24:
for u,v,w being non zero Element of TOP-REAL 3 st
u`2 <> 0 & u`3 = 1 & v`1 = - u`2 & v`2 = u`1 & v`3 = 0 &
w`3 = 1 & |{ u,v,w }| = 0 & 1 < (u`1)^2 + (u`2)^2 holds
(w`1)^2 + (w`2)^2 <> 1
proof
let u,v,w be non zero Element of TOP-REAL 3;
assume that
A0: u`2 <> 0 and
A1: u`3 = 1 and
A2: v`1 = - u`2 and
A3: v`2 = u`1 and
A4: v`3 = 0 and
A5: w`3 = 1 and
A6: |{ u,v,w }| = 0 and
A7: 1 < (u`1)^2 + (u`2)^2;
A8: (u`1)^2 + (u`2)^2 - (u`1) * (w`1) - (u`2) * (w`2) = 0
by A1,A2,A3,A4,A5,A6,Th21;
assume
A9: (w`1)^2 + (w`2)^2 = 1;
reconsider x = w`1, y = w`2 as Real;
reconsider u2 = u`2 as non zero Real by A0;
reconsider r = sqrt ((u`1)^2 + (u`2)^2) as positive Real by A0,Th02;
reconsider u1 = u`1 as Real;
A10: r^2 = (u`1)^2 + (u`2)^2 by SQUARE_1:def 2;
u2 * y = r^2 - u1 * x by A8,SQUARE_1:def 2;
then ((r^2)^2 / u2^2) - 2 * ((r^2 * u1) / (u2 * u2)) * x
+ (u1^2 / u2^2) * x^2 + x^2 = 1 by A9,Th03;
hence contradiction by A10,A7,Th09;
end;
theorem Th25:
for P being Element of absolute holds
ex u being non zero Element of TOP-REAL 3 st u.3 = 1 & P = Dir u
proof
let P be Element of absolute;
consider u be Element of TOP-REAL 3 such that
A1: u is not zero and
A2: P = Dir u by ANPROJ_1:26;
u.3 <> 0 by A1,A2,BKMODEL1:83;
then
A3: u`3 <> 0 by EUCLID_5:def 3;
reconsider v = |[u`1/u`3,u`2/u`3,1]| as non zero Element of TOP-REAL 3;
take v;
thus v.3 = v`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
u`3 * v = |[u`3 * (u`1/u`3), u`3 * (u`2/u`3), u`3 * 1]| by EUCLID_5:8
.= |[ u`1,u`3 * (u`2/u`3), u`3 * 1]| by A3,XCMPLX_1:87
.= |[ u`1,u`2, u`3 * 1]| by A3,XCMPLX_1:87
.= u by EUCLID_5:3;
then are_Prop u,v by A3,ANPROJ_1:1;
hence P = Dir v by A1,A2,ANPROJ_1:22;
end;
theorem Th26:
for a,b,c,d being Real
for u,v being non zero Element of TOP-REAL 3 st u = |[a,b,1]| &
v = |[c,d,0]| holds Dir u <> Dir v
proof
let a,b,c,d be Real;
let u,v be non zero Element of TOP-REAL 3;
assume that
A1: u = |[a,b,1]| and
A2: v = |[c,d,0]|;
assume Dir u = Dir v;
then are_Prop u,v by ANPROJ_1:22;
then consider x be Real such that
x <> 0 and
A3: u = x * v by ANPROJ_1:1;
1 = (x * v)`3 by A3,A1,EUCLID_5:2
.= |[x * v`1,x * v`2,x * v`3]|`3 by EUCLID_5:7
.= x * v`3 by EUCLID_5:2
.= x * 0 by A2,EUCLID_5:2
.= 0;
hence contradiction;
end;
theorem Th27:
for u being non zero Element of TOP-REAL 3 st
(u.1)^2 + (u.2)^2 < 1 & u.3 = 1 holds Dir u is Element of BK_model
proof
let u be non zero Element of TOP-REAL 3;
assume that
A1: (u.1)^2 + (u.2)^2 < 1 and
A2: u.3 = 1;
reconsider P = Dir u as Point of ProjectiveSpace TOP-REAL 3 by ANPROJ_1:26;
now
let v be Element of TOP-REAL 3;
assume that
A3: v is non zero and
A4: P = Dir v;
qfconic(1,1,-1,0,0,0,u) = 1 * u.1 * u.1 + 1 * u.2 * u.2
+ (-1) * u.3 * u.3
+ 0 * u.1 * u.2 + 0 * u.1 * u.3 + 0 * u.2 * u.3 by PASCAL:def 1
.= (u.1)^2 + (u.2)^2 + (-1) by A2;
then qfconic(1,1,-1,0,0,0,u) < 1 + (-1) by A1,XREAL_1:8;
hence qfconic(1,1,-1,0,0,0,v) is negative by A3,A4,BKMODEL1:81;
end;
then P in {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(1,1,-1,0,0,0,u) is negative};
hence thesis by BKMODEL2:def 1;
end;
theorem Th28:
for a,b being Real st a^2 + b^2 <= 1 holds
Dir |[a,b,1]| in BK_model \/ absolute
proof
let a,b be Real;
assume a^2 + b^2 <= 1;
then per cases by XXREAL_0:1;
suppose
A1: a^2 + b^2 = 1;
reconsider u = |[a,b,1]| as non zero Element of TOP-REAL 3;
reconsider P = Dir u as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
now
B1: u.1 = u`1 by EUCLID_5:def 1
.= a by EUCLID_5:2;
u.2 = u`2 by EUCLID_5:def 2
.= b by EUCLID_5:2;
hence |[u.1,u.2]| in circle(0,0,1) by A1,B1,BKMODEL1:13;
thus u.3 = |[a,b,1]|`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
end;
then P is Element of absolute by BKMODEL1:86;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A2: a^2 + b^2 < 1;
reconsider w = |[a,b,1]| as non zero Element of TOP-REAL 3;
w`1 = a & w`2 = b & w`3 = 1 by EUCLID_5:2;
then w.1 = a & w.2 = b & w.3 = 1 by EUCLID_5:def 1,def 2,def 3;
then Dir |[a,b,1]| is Element of BK_model by A2,Th27;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem Th29:
not P in BK_model \/ absolute implies (ex l st P in l &
l misses absolute)
proof
assume
A1: not P in BK_model \/ absolute;
then
A2: not P in BK_model & not P in absolute by XBOOLE_0:def 3;
consider u9 be Element of TOP-REAL 3 such that
A3: u9 is not zero and
A4: P = Dir u9 by ANPROJ_1:26;
per cases;
suppose
A5: u9.3 = 0;
u9.1 <> 0 or u9.2 <> 0
proof
assume
A6: u9.1 = 0 & u9.2 = 0;
u9 = |[u9`1,u9`2,u9`3]| by EUCLID_5:3
.= |[0,u9`2,u9`3]| by A6,EUCLID_5:def 1
.= |[0,0,u9`3]| by A6,EUCLID_5:def 2
.= 0.TOP-REAL 3 by A5,EUCLID_5:def 3,4;
hence contradiction by A3;
end;
then per cases;
suppose
A7: u9.1 <> 0;
then reconsider v = |[-u9.2,u9.1,0]| as non zero Element of TOP-REAL 3;
reconsider Q = Dir v as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
P <> Q
proof
assume P = Q;
then are_Prop u9,v by A3,A4,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A9: u9 = a * v by ANPROJ_1:1;
A10: |[a * (- u9.2), a * u9.1,a * 0]|
= a * v by EUCLID_5:8
.= |[u9`1,u9`2,u9`3]| by A9,EUCLID_5:3;
now
thus a * (- u9.2) = |[u9`1,u9`2,u9`3]|`1 by A10,EUCLID_5:2
.= u9`1 by EUCLID_5:2
.= u9.1 by EUCLID_5:def 1;
thus a * u9.1 = |[u9`1,u9`2,u9`3]|`2 by A10,EUCLID_5:2
.= u9`2 by EUCLID_5:2
.= u9.2 by EUCLID_5:def 2;
end;
then u9.1 = 0 & u9.2 = 0 by Th10;
then u9`1 = 0 & u9`2 = 0 & u9`3 = 0 by A5,EUCLID_5:def 1,def 2,def 3;
hence contradiction by A3,EUCLID_5:3,4;
end;
then reconsider l9 = Line(P,Q) as LINE of real_projective_plane
by COLLSP:def 7;
reconsider l = l9 as Element of the Lines of
IncProjSp_of real_projective_plane by INCPROJ:4;
take l;
l misses absolute
proof
assume not l misses absolute;
then consider R be object such that
A11: R in l /\ absolute by XBOOLE_0:7;
A12: R in l & R in absolute by A11,XBOOLE_0:def 4;
reconsider R as Element of ProjectiveSpace TOP-REAL 3 by A11;
consider w be non zero Element of TOP-REAL 3 such that
A13: w.3 = 1 and
A14: R = Dir w by A12,Th25;
reconsider R9 = R as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
reconsider l2 = l as LINE of IncProjSp_of real_projective_plane;
A15: w`3 = 1 by A13,EUCLID_5:def 3;
A16: u9`3 = 0 by A5,EUCLID_5:def 3;
A17: v`1 = - u9.2 by EUCLID_5:2
.= -u9`2 by EUCLID_5:def 2;
A18: v`2 = u9.1 by EUCLID_5:2
.= u9`1 by EUCLID_5:def 1;
A19: v`3 = 0 by EUCLID_5:2;
R9 on l2 by A12,INCPROJ:5;
then |{u9,v,w}| = 0 by A3,A4,A14,BKMODEL1:77;
then 0 = u9`1 * v`2 * 1 - u9`3*v`2*w`1 - u9`1*v`3*w`2
+ u9`2*v`3*w`1 -
u9`2*v`1* 1 + u9`3*v`1*w`2 by A15,ANPROJ_8:27
.= (u9`1)^2 + (u9`2)^2 by A16,A17,A18,A19;
then u9`1 = 0 & u9`2 = 0;
hence contradiction by A7,EUCLID_5:def 1;
end;
hence thesis by COLLSP:10;
end;
suppose
A20: u9.2 <> 0;
then reconsider v = |[-u9.2,u9.1,0]| as non zero Element of TOP-REAL 3;
reconsider Q = Dir v as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
P <> Q
proof
assume P = Q;
then are_Prop u9,v by A3,A4,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A22: u9 = a * v by ANPROJ_1:1;
A23: |[a * (- u9.2), a * u9.1,a * 0]|
= a * v by EUCLID_5:8
.= |[u9`1,u9`2,u9`3]| by A22,EUCLID_5:3;
now
thus a * (- u9.2) = |[u9`1,u9`2,u9`3]|`1 by A23,EUCLID_5:2
.= u9`1 by EUCLID_5:2
.= u9.1 by EUCLID_5:def 1;
thus a * u9.1 = |[u9`1,u9`2,u9`3]|`2 by A23,EUCLID_5:2
.= u9`2 by EUCLID_5:2
.= u9.2 by EUCLID_5:def 2;
end;
then u9.1 = 0 & u9.2 = 0 by Th10;
then u9`1 = 0 & u9`2 = 0 & u9`3 = 0 by A5,EUCLID_5:def 1,def 2,def 3;
hence contradiction by A3,EUCLID_5:3,4;
end;
then reconsider l9 = Line(P,Q) as LINE of real_projective_plane
by COLLSP:def 7;
reconsider l = l9 as Element of the Lines of
IncProjSp_of real_projective_plane by INCPROJ:4;
take l;
l misses absolute
proof
assume not l misses absolute;
then consider R be object such that
A24: R in l /\ absolute by XBOOLE_0:7;
A25: R in l & R in absolute by A24,XBOOLE_0:def 4;
reconsider R as Element of ProjectiveSpace TOP-REAL 3 by A24;
consider w be non zero Element of TOP-REAL 3 such that
A26: w.3 = 1 and
A27: R = Dir w by A25,Th25;
reconsider R9 = R as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
reconsider l2 = l as LINE of IncProjSp_of real_projective_plane;
A28: w`3 = 1 by A26,EUCLID_5:def 3;
A29: u9`3 = 0 by A5,EUCLID_5:def 3;
A30: v`1 = - u9.2 by EUCLID_5:2
.= -u9`2 by EUCLID_5:def 2;
A31: v`2 = u9.1 by EUCLID_5:2
.= u9`1 by EUCLID_5:def 1;
A32: v`3 = 0 by EUCLID_5:2;
R9 on l2 by A25,INCPROJ:5;
then |{u9,v,w}| = 0 by A3,A4,A27,BKMODEL1:77;
then
0 = u9`1 * v`2 * 1 - u9`3*v`2*w`1 - u9`1*v`3*w`2
+ u9`2*v`3*w`1 -
u9`2*v`1* 1 + u9`3*v`1*w`2 by A28,ANPROJ_8:27
.= (u9`1)^2 + (u9`2)^2 by A29,A30,A31,A32;
then u9`1 = 0 & u9`2 = 0;
hence contradiction by A20,EUCLID_5:def 2;
end;
hence thesis by COLLSP:10;
end;
end;
suppose
A33: u9.3 <> 0;
reconsider u = |[u9.1 / u9.3, u9.2 / u9.3, 1]| as
non zero Element of TOP-REAL 3;
A34: u`3 = 1 by EUCLID_5:2;
then
A35: u.3 = 1 by EUCLID_5:def 3;
u9.3 * u = |[u9.1,u9.2,u9.3]| by A33,Th22
.= |[u9`1,u9.2,u9.3]| by EUCLID_5:def 1
.= |[u9`1,u9`2,u9.3]| by EUCLID_5:def 2
.= |[u9`1,u9`2,u9`3]| by EUCLID_5:def 3
.= u9 by EUCLID_5:3;
then
A36: are_Prop u,u9 by A33,ANPROJ_1:1;
then
A37: P = Dir u by A3,A4,ANPROJ_1:22;
u.1 <> 0 or u.2 <> 0
proof
assume
A38: u.1 = 0 & u.2 = 0;
now
let v be Element of TOP-REAL 3;
assume
A39: v is non zero;
assume P = Dir v;
then
A40: Dir u = Dir v by A36,A3,A4,ANPROJ_1:22;
now
thus 0 < (u.3)^2 by A35;
thus qfconic(1,1,-1,0,0,0,u) = 1 * u.1 * u.1 + 1 * u.2 * u.2
+ (-1) * u.3 * u.3 +
0 * u.1 * u.2 + 0 * u.1 * u.3 + 0 * u.2 * u.3 by PASCAL:def 1
.= (-1) * (u.3)^2 by A38;
end;
hence qfconic(1,1,-1,0,0,0,v) is negative by A39,A40,BKMODEL1:81;
end;
hence contradiction by A2,BKMODEL2:def 1;
end;
then per cases;
suppose
A41: u.1 <> 0;
then reconsider u1 = u.1 as non zero Real;
reconsider u2 = u.2 as Real;
reconsider v = |[-u2,u1,0]| as non zero Element of TOP-REAL 3;
reconsider Q = Dir v as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
reconsider l9 = Line(P,Q) as LINE of real_projective_plane
by Th26,A37,COLLSP:def 7;
reconsider l = l9 as Element of the Lines of
IncProjSp_of real_projective_plane by INCPROJ:4;
take l;
l misses absolute
proof
assume not l misses absolute;
then consider R be object such that
A42: R in l /\ absolute by XBOOLE_0:7;
A43: R in l & R in absolute by A42,XBOOLE_0:def 4;
reconsider R as Element of ProjectiveSpace TOP-REAL 3 by A42;
consider w be non zero Element of TOP-REAL 3 such that
A44: w.3 = 1 and
A45: R = Dir w by A43,Th25;
|[w.1,w.2]| in circle(0,0,1) by A43,A44,A45,BKMODEL1:84;
then (w.1)^2 + (w.2)^2 = 1 by BKMODEL1:13;
then (w`1)^2 + (w.2)^2 = 1 by EUCLID_5:def 1;
then
A46: (w`1)^2 + (w`2)^2 = 1 by EUCLID_5:def 2;
now
thus u`1 <> 0 by A41,EUCLID_5:def 1;
thus u`3 = 1 by EUCLID_5:2;
v`1 = -u2 by EUCLID_5:2;
hence v`1 = -u`2 by EUCLID_5:def 2;
v`2 = u.1 by EUCLID_5:2;
hence v`2 = u`1 by EUCLID_5:def 1;
thus v`3 = 0 by EUCLID_5:2;
thus w`3 = 1 by A44,EUCLID_5:def 3;
reconsider R9 = R as POINT of IncProjSp_of
real_projective_plane by INCPROJ:3;
reconsider l2 = l as LINE of IncProjSp_of real_projective_plane;
R9 on l2 by A43,INCPROJ:5;
hence |{u,v,w}| = 0 by A37,A45,BKMODEL1:77;
thus 1 < (u`1)^2 + (u`2)^2
proof
assume not 1 < (u`1)^2 + (u`2)^2;
then Dir |[u`1,u`2,1]| in BK_model \/ absolute by Th28;
hence contradiction by A37,A1,A34,EUCLID_5:3;
end;
end;
hence contradiction by A46,Th23;
end;
hence thesis by COLLSP:10;
end;
suppose
A47: u.2 <> 0;
then reconsider u2 = u.2 as non zero Real;
reconsider u1 = u.1 as Real;
reconsider v = |[-u2,u1,0]| as non zero Element of TOP-REAL 3;
reconsider Q = Dir v as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
reconsider l9 = Line(P,Q) as LINE of real_projective_plane
by A37,Th26,COLLSP:def 7;
reconsider l = l9 as Element of the Lines of IncProjSp_of
real_projective_plane by INCPROJ:4;
take l;
l misses absolute
proof
assume l meets absolute;
then consider R be object such that
A48: R in l /\ absolute by XBOOLE_0:7;
A49: R in l & R in absolute by A48,XBOOLE_0:def 4;
reconsider R as Element of ProjectiveSpace TOP-REAL 3 by A48;
consider w be non zero Element of TOP-REAL 3 such that
A50: w.3 = 1 and
A51: R = Dir w by A49,Th25;
|[w.1,w.2]| in circle(0,0,1) by A49,A50,A51,BKMODEL1:84;
then (w.1)^2 + (w.2)^2 = 1 by BKMODEL1:13;
then (w`1)^2 + (w.2)^2 = 1 by EUCLID_5:def 1;
then
A53: (w`1)^2 + (w`2)^2 = 1 by EUCLID_5:def 2;
now
thus u`2 <> 0 by A47,EUCLID_5:def 2;
thus u`3 = 1 by EUCLID_5:2;
v`1 = -u2 by EUCLID_5:2;
hence v`1 = -u`2 by EUCLID_5:def 2;
v`2 = u.1 by EUCLID_5:2;
hence v`2 = u`1 by EUCLID_5:def 1;
thus v`3 = 0 by EUCLID_5:2;
thus w`3 = 1 by A50,EUCLID_5:def 3;
reconsider R9 = R as POINT of IncProjSp_of
real_projective_plane by INCPROJ:3;
reconsider l2 = l as LINE of IncProjSp_of real_projective_plane;
R9 on l2 by A49,INCPROJ:5;
hence |{u,v,w}| = 0 by A37,A51,BKMODEL1:77;
thus 1 < (u`1)^2 + (u`2)^2
proof
assume not 1 < (u`1)^2 + (u`2)^2;
then Dir |[u`1,u`2,1]| in BK_model \/ absolute by Th28;
hence contradiction by A37,A1,EUCLID_5:3,A34;
end;
end;
hence contradiction by A53,Th24;
end;
hence thesis by COLLSP:10;
end;
end;
end;
theorem Th30:
for P being Point of real_projective_plane
for h being Element of SubGroupK-isometry,
N being invertible Matrix of 3,F_Real st h = homography(N) holds
P is Element of absolute iff homography(N).P is Element of absolute
proof
let P be Point of real_projective_plane;
let h be Element of SubGroupK-isometry;
let N be invertible Matrix of 3,F_Real;
assume
A1: h = homography(N);
h is Element of EnsK-isometry by BKMODEL2:def 8;
then
A2: homography(N).:absolute = absolute by A1,BKMODEL2:44;
homography(N~) is Element of SubGroupK-isometry by A1,BKMODEL2:47;
then homography(N~) is Element of EnsK-isometry by BKMODEL2:def 8;
then
A3: homography(N~).:absolute = absolute by BKMODEL2:44;
set hP = homography(N).P;
hereby
assume
A4: P is Element of absolute;
dom homography(N) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
hence homography(N).P is Element of absolute by A2,A4,FUNCT_1:108;
end;
assume
A5: homography(N).P is Element of absolute;
A6: dom homography(N~) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
homography(N~).hP in homography(N~).:absolute by A6,A5,FUNCT_1:108;
hence P is Element of absolute by A3,ANPROJ_9:15;
end;
theorem Th31:
for P being Element of BK_model
for h being Element of SubGroupK-isometry,
N being invertible Matrix of 3,F_Real st
h = homography(N) holds homography(N).P is Element of BK_model
proof
let P be Element of BK_model;
let h be Element of SubGroupK-isometry;
let N be invertible Matrix of 3,F_Real;
assume
A1: h = homography(N);
set hP = homography(N).P;
assume
A2: not hP is Element of BK_model;
not hP is Element of absolute
proof
assume hP is Element of absolute;
then P is Element of absolute by A1,Th30;
hence contradiction by XBOOLE_0:3,BKMODEL2:1;
end;
then not hP in BK_model \/ absolute by A2,XBOOLE_0:def 3;
then consider l such that
A3: hP in l and
A4: l misses absolute by Th29;
reconsider L = (line_homography(N~)).l as LINE of real_projective_plane
by INCPROJ:4;
reconsider L9 = L as LINE of IncProjSp_of real_projective_plane;
consider P1,P2 be Element of absolute such that
P1 <> P2 and
A5: P1 in L9 and
P2 in L9 by A3,Th19,Th12;
A6: homography(N).P1 is Element of absolute by A1,Th30;
homography(N).P1 in (line_homography(N)).L by A5,Th20;
then homography(N).P1 in l by Th15;
hence contradiction by A6,A4,XBOOLE_0:def 4;
end;
theorem
for P being Element of BK_model
for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography(N) holds
ex u being non zero Element of TOP-REAL 3 st homography(N).P = Dir u &
u.3 = 1
proof
let P be Element of BK_model;
let h be Element of SubGroupK-isometry;
let N be invertible Matrix of 3,F_Real;
assume h = homography(N);
then reconsider hP = homography(N).P as Element of BK_model by Th31;
ex u being non zero Element of TOP-REAL 3 st
Dir u = hP & u.3 = 1 & BK_to_REAL2 hP = |[u.1,u.2]| by BKMODEL2:def 2;
hence thesis;
end;
begin :: Beltrami-Klein model
definition
func BK-model-Betweenness -> Relation of
[: BK_model,BK_model:],BK_model means
for a,b,c being Element of BK_model holds [[a,b],c] in it iff
BK_to_REAL2 b in LSeg(BK_to_REAL2 a,BK_to_REAL2 c);
existence
proof
defpred P[object,object] means
ex a,b,c being Element of BK_model st $1 = [a,b] & $2 = c &
BK_to_REAL2 b in LSeg (BK_to_REAL2 a,BK_to_REAL2 c);
consider R be Relation of [: BK_model,BK_model :], BK_model such that
A1: for x being Element of [: BK_model,BK_model :],
y being Element of BK_model holds
[x,y] in R iff P[x,y] from RELSET_1:sch 2;
for a,b,c being Element of BK_model holds [[a,b],c] in R iff
BK_to_REAL2 b in LSeg(BK_to_REAL2 a,BK_to_REAL2 c)
proof
let a,b,c be Element of BK_model;
hereby
assume
A2: [[a,b],c] in R;
reconsider x = [a,b] as Element of [:BK_model,BK_model:];
consider a9,b9,c9 be Element of BK_model such that
A3: x = [a9,b9] and
A4: c = c9 and
A5: BK_to_REAL2 b9 in LSeg (BK_to_REAL2 a9,BK_to_REAL2 c9) by A2,A1;
a = a9 & b = b9 by A3,XTUPLE_0:1;
hence BK_to_REAL2 b in LSeg (BK_to_REAL2 a,BK_to_REAL2 c) by A4,A5;
end;
assume BK_to_REAL2 b in LSeg(BK_to_REAL2 a,BK_to_REAL2 c);
hence [[a,b],c] in R by A1;
end;
hence thesis;
end;
uniqueness
proof
let R1,R2 be Relation of [: BK_model,BK_model :],BK_model such that
A6: for a,b,c being Element of BK_model holds [[a,b],c] in R1 iff
BK_to_REAL2 b in LSeg(BK_to_REAL2 a,BK_to_REAL2 c) and
A7: for a,b,c being Element of BK_model holds [[a,b],c] in R2 iff
BK_to_REAL2 b in LSeg(BK_to_REAL2 a,BK_to_REAL2 c);
thus R1 = R2
proof
for a,b be object holds [a,b] in R1 iff [a,b] in R2
proof
let a,b be object;
hereby
assume
A8: [a,b] in R1;
then consider c,d be object such that
A9: [a,b] = [c,d] and
A10: c in [: BK_model,BK_model :] and
A11: d in BK_model by RELSET_1:2;
consider e,f be object such that
A12: e in BK_model and
A13: f in BK_model and
A14: c = [e,f] by A10,ZFMISC_1:def 2;
reconsider d,e,f as Element of BK_model by A12,A13,A11;
BK_to_REAL2 f in LSeg(BK_to_REAL2 e,BK_to_REAL2 d) by A6,A8,A9,A14;
hence [a,b] in R2 by A9,A7,A14;
end;
assume
A15: [a,b] in R2;
then consider c,d be object such that
A16: [a,b] = [c,d] and
A17: c in [: BK_model,BK_model :] and
A18: d in BK_model by RELSET_1:2;
consider e,f be object such that
A19: e in BK_model and
A20: f in BK_model and
A21: c = [e,f] by A17,ZFMISC_1:def 2;
reconsider d,e,f as Element of BK_model by A19,A20,A18;
BK_to_REAL2 f in LSeg(BK_to_REAL2 e,BK_to_REAL2 d) by A7,A15,A16,A21;
hence [a,b] in R1 by A16,A6,A21;
end;
hence thesis by RELAT_1:def 2;
end;
end;
end;
definition
func BK-model-Equidistance -> Relation of [: BK_model,BK_model :],
[: BK_model,BK_model :] means
:Def05:
for a,b,c,d being Element of BK_model holds [[a,b],[c,d]] in it iff
ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a = c & homography(N).b = d;
existence
proof
defpred P[object,object] means
ex a,b,c,d being Element of BK_model st $1 = [a,b] & $2 = [c,d] &
ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a = c & homography(N).b = d;
consider R be Relation of [: BK_model,BK_model :],
[: BK_model,BK_model :] such that
A1: for x being Element of [: BK_model,BK_model :],
y being Element of [: BK_model,BK_model :] holds
[x,y] in R iff P[x,y] from RELSET_1:sch 2;
for a,b,c,d being Element of BK_model holds [[a,b],[c,d]] in R iff
ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a = c & homography(N).b = d
proof
let a,b,c,d be Element of BK_model;
hereby
assume
A2: [[a,b],[c,d]] in R;
reconsider x = [a,b], y = [c,d] as Element of [: BK_model,BK_model :];
consider a9,b9,c9,d9 being Element of BK_model such that
A3: x = [a9,b9] & y = [c9,d9] &
ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a9 = c9 & homography(N).b9 = d9
by A2,A1;
a = a9 & b = b9 & c = c9 & d = d9 by A3,XTUPLE_0:1;
hence ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a = c & homography(N).b = d by A3;
end;
assume ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a = c & homography(N).b = d;
hence [[a,b],[c,d]] in R by A1;
end;
hence thesis;
end;
uniqueness
proof
let B1,B2 be Relation of [: BK_model,BK_model :], [: BK_model,BK_model :]
such that
A4: for a,b,c,d being Element of BK_model holds [[a,b],[c,d]] in B1 iff
ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a = c & homography(N).b = d and
A5: for a,b,c,d being Element of BK_model holds [[a,b],[c,d]] in B2 iff
ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a = c & homography(N).b = d;
thus B1 = B2
proof
for a,b be object holds [a,b] in B1 iff [a,b] in B2
proof
let a,b be object;
hereby
assume
A6: [a,b] in B1;
then
A7: a in [: BK_model,BK_model :] & b in [: BK_model,BK_model :]
by ZFMISC_1:87;
then consider a1,a2 be object such that
A8: a1 in BK_model and
A9: a2 in BK_model and
A10: a = [a1,a2] by ZFMISC_1:def 2;
consider b1,b2 be object such that
A11: b1 in BK_model and
A12: b2 in BK_model and
A13: b = [b1,b2] by A7,ZFMISC_1:def 2;
ex h be Element of SubGroupK-isometry st
ex N be invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a1 = b1 &
homography(N).a2 = b2 by A4,A11,A12,A8,A9,A10,A6,A13;
hence [a,b] in B2 by A10,A13,A5,A8,A9,A11,A12;
end;
assume
A14: [a,b] in B2;
then
A14bis: a in [: BK_model,BK_model :] &
b in [: BK_model,BK_model :] by ZFMISC_1:87;
then consider a1,a2 be object such that
A15: a1 in BK_model and
A16: a2 in BK_model and
A17: a = [a1,a2] by ZFMISC_1:def 2;
consider b1,b2 be object such that
A18: b1 in BK_model and
A19: b2 in BK_model and
A20: b = [b1,b2] by A14bis,ZFMISC_1:def 2;
ex h be Element of SubGroupK-isometry st
ex N be invertible Matrix of 3,F_Real st
h = homography(N) &
homography(N).a1 = b1 &
homography(N).a2 = b2 by A5,A18,A19,A15,A16,A17,A14,A20;
hence [a,b] in B1 by A17,A20,A4,A15,A16,A18,A19;
end;
hence thesis by RELAT_1:def 2;
end;
end;
end;
definition
func BK-model-Plane -> TarskiGeometryStruct equals
TarskiGeometryStruct(# BK_model, BK-model-Betweenness,
BK-model-Equidistance #);
coherence;
end;
begin :: CongruenceSymmetry
theorem
BK-model-Plane is satisfying_CongruenceSymmetry
proof
let P,Q be POINT of BK-model-Plane;
ex h be Element of SubGroupK-isometry,
N be invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).P = Q &
homography(N).Q = P by BKMODEL2:60;
hence P,Q equiv Q,P by Def05;
end;
begin :: CongruenceEquivalenceRelation
theorem
BK-model-Plane is satisfying_CongruenceEquivalenceRelation
proof
let P,Q,R,S,T,U be POINT of BK-model-Plane;
assume that
A1: P,Q equiv R,S and
A2: P,Q equiv T,U;
consider h1 be Element of SubGroupK-isometry such that
A3: ex N be invertible Matrix of 3,F_Real st
h1 = homography(N) & homography(N).P = R & homography(N).Q = S by A1,Def05;
consider N1 be invertible Matrix of 3,F_Real such that
A4: h1 = homography(N1) & homography(N1).P = R & homography(N1).Q = S by A3;
reconsider N3 = N1~ as invertible Matrix of 3,F_Real;
P in BK_model & Q in BK_model;
then
A5: homography(N3).R = P & homography(N3).S = Q by A4,ANPROJ_9:15;
reconsider h3 = homography(N3) as Element of SubGroupK-isometry
by A4,BKMODEL2:47;
consider h2 be Element of SubGroupK-isometry such that
A6: ex N being invertible Matrix of 3,F_Real st
h2 = homography(N) & homography(N).P = T & homography(N).Q = U by A2,Def05;
consider N2 be invertible Matrix of 3,F_Real such that
A7: h2 = homography(N2) & homography(N2).P = T & homography(N2).Q = U by A6;
reconsider N4 = N2 * N3 as invertible Matrix of 3,F_Real;
now
h2 * h3 is Element of SubGroupK-isometry;
hence homography(N4) is Element of SubGroupK-isometry by A7,BKMODEL2:46;
thus N4 is invertible Matrix of 3,F_Real;
R in BK_model & S in BK_model;
hence homography(N4).R = T & homography(N4).S = U by A5,A7,ANPROJ_9:13;
end;
hence R,S equiv T,U by Def05;
end;
begin :: CongruenceIdentity
theorem
BK-model-Plane is satisfying_CongruenceIdentity
proof
let P,Q,R be Point of BK-model-Plane;
assume P,Q equiv R,R;
then ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).P = R & homography(N).Q = R by Def05;
hence P = Q by BKMODEL2:62;
end;