:: Beltrami-Klein model, Part {IV}
:: 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 NAT_1, 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, TARSKI, XXREAL_0, PASCAL, SQUARE_1,
JGRAPH_6, RVSUM_1, FINSEQ_1, MATRIX_3, BKMODEL1, BKMODEL2,
BKMODEL3, RLTOPSP1, GTARSKI1, GTARSKI2, METRIC_1, EUCLID12,
CONVEX1, XXREAL_1, ALGSTR_4, BKMODEL4, GROUP_1;
notations GCD_1, RELSET_1, ORDINAL1, XCMPLX_0, PRE_TOPC, RVSUM_1, TARSKI,
XBOOLE_0, RLVECT_1, COLLSP, EUCLID_5, PASCAL, XXREAL_0, ANPROJ_9,
SQUARE_1, XREAL_0, JGRAPH_6, SUBSET_1, NUMBERS, FUNCT_1, FUNCT_2,
FINSEQ_1, STRUCT_0, ALGSTR_0, VECTSP_1, FINSEQ_2, EUCLID,
ANPROJ_1, MATRIX_6, LAPLACE, ANPROJ_8, MATRIX_1, MATRIX_3,
BKMODEL1, BKMODEL2, RLTOPSP1, GTARSKI1, METRIC_1, EUCLID12,
XXREAL_1, GTARSKI2, BKMODEL3;
constructors VECTSP_2, GCD_1, REALSET1, FINSEQ_4, LAPLACE, MATRPROB,
RELSET_1, MONOID_0, EUCLID_5, MATRIX13, ANPROJ_8, PASCAL,
SQUARE_1, BINOP_2, GTARSKI2, EUCLID12, CONVEX1, XXREAL_1,
BKMODEL3, MATRIX_3;
registrations MEMBERED, ORDINAL1, XXREAL_0, XBOOLE_0, ANPROJ_1, STRUCT_0,
VECTSP_1, REVROT_1, RELSET_1, XREAL_0, MONOID_0, EUCLID, VALUED_0,
MATRIX_6, SQUARE_1, XCMPLX_0, NUMBERS, TOPREAL9, TOPREALC, GTARSKI2,
RLTOPSP1, CONVEX1, BKMODEL3, RING_2, GCD_1;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions TARSKI, GTARSKI1;
equalities VECTSP_1, STRUCT_0, BKMODEL1, GTARSKI2, EUCLID, XCMPLX_0, BKMODEL3;
expansions TARSKI, STRUCT_0, XBOOLE_0, GTARSKI1;
theorems XREAL_0, LAPLACE, MATRIX_6, XREAL_1, EUCLID_5, ANPROJ_1, EUCLID,
XCMPLX_1, RVSUM_1, FINSEQ_1, FUNCT_1, FUNCT_2, ANPROJ_8, ANPROJ_9,
PASCAL, TARSKI, XBOOLE_0, SQUARE_1, TOPREAL9, EUCLID_2, FINSEQ_2,
BKMODEL1, BKMODEL2, GTARSKI1, GTARSKI2, RLTOPSP1, CONVEX1, XXREAL_1,
MATRIX_9, EUCLID12, GTARSKI3, BKMODEL3;
begin :: Preliminaries
theorem Th25:
for a,b being Real st a <> b holds 1 - (a / (a - b)) = - b / (a - b)
proof
let a,b be Real;
assume a <> b;
then a - b <> 0;
then 1 - (a / (a - b)) = (a - b) / (a - b) - a / (a - b) by XCMPLX_1:60
.= (a - b - a) / (a - b);
hence thesis;
end;
theorem
for a,b being Real st 0 < a * b holds 0 < a / b
proof
let a,b be Real;
assume
A1: 0 < a * b; then
A2: b <> 0; then
0 < b^2 by SQUARE_1:12;
then 0 / b^2 < (a * b) / b^2 by A1;
then 0 < (a * b) / (b * b) by SQUARE_1:def 1;
then 0 < (a / b) * (b / b) by XCMPLX_1:76;
then 0 < (a / b) * 1 by A2,XCMPLX_1:60;
hence thesis;
end;
theorem Th31:
for a,b,c being Real st 0 <= a <= 1 & 0 < b * c holds
0 <= (a * c) / ((1 - a) * b + a * c) <= 1
proof
let a,b,c be Real;
assume that
A1: 0 <= a <= 1 and
A2: 0 < b * c;
per cases by A2,XREAL_1:134;
suppose
A3: 0 < b & 0 < c;
B3: a - a <= 1 - a by A1,XREAL_1:9;
hence 0 <= (a * c) / ((1 - a) * b + a * c) by A1,A3;
0 + a * c <= (1 - a) * b + a * c by A3,B3,XREAL_1:6;
hence (a * c) / ((1 - a) * b + a * c) <= 1 by A1,A3,XREAL_1:183;
end;
suppose
A4: b < 0 & c < 0;
A5: a - a <= 1 - a by A1,XREAL_1:9;
hence 0 <= (a * c) / ((1 - a) * b + a * c) by A1,A4;
(1 - a) * b + a * c <= 0 + a * c by A4,A5,XREAL_1:6;
hence (a * c) / ((1 - a) * b + a * c) <= 1 by A1,A4,XREAL_1:184;
end;
end;
theorem Th32:
for a,b,c being Real st (1 - a) * b + a * c <> 0 holds
1 - ((a * c) / ((1 - a) * b + a * c)) =
(1 - a) * b / ((1 - a) * b + a * c)
proof
let a,b,c be Real;
set r = (1 - a) * b + a * c;
assume (1 - a) * b + a * c <> 0; then
1 - (a * c) / r = r / r - (a * c) / r by XCMPLX_1:60
.= (1 - a) * b / r;
hence thesis;
end;
theorem Th33:
for a,b,c,d being Real st b <> 0 holds
a * b / c * d / b = a * d / c
proof
let a,b,c,d be Real;
assume
A1: b <> 0;
a * b / c * d / b = a * ((d / c) * (b / b))
.= a * ((d / c) * 1) by A1,XCMPLX_1:60;
hence thesis;
end;
theorem Th35:
for u being Element of TOP-REAL 3 holds u = |[u.1,u.2,u.3]|
proof
let u be Element of TOP-REAL 3;
thus u = |[u`1,u`2,u`3]| by EUCLID_5:3
.= |[u.1,u`2,u`3]| by EUCLID_5:def 1
.= |[u.1,u.2,u`3]| by EUCLID_5:def 2
.= |[u.1,u.2,u.3]| by EUCLID_5:def 3;
end;
theorem Th01:
for P being Element of BK_model holds BK_to_REAL2 P in TarskiEuclid2Space
proof
let P be Element of BK_model;
the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 &
BK_to_REAL2 P in TOP-REAL 2 by GTARSKI1:def 13;
hence thesis by EUCLID:22;
end;
definition
let P be POINT of BK-model-Plane;
func BK_to_T2 P -> POINT of TarskiEuclid2Space means :Def01:
ex p be Element of BK_model st P = p &
it = BK_to_REAL2 p;
existence
proof
reconsider p = P as Element of BK_model;
BK_to_REAL2 p in TarskiEuclid2Space by Th01;
hence thesis;
end;
uniqueness;
end;
definition
let P be POINT of TarskiEuclid2Space;
assume
A1: Tn2TR P in inside_of_circle(0,0,1);
func T2_to_BK P -> POINT of BK-model-Plane means
:Def02:
ex u be non zero Element of TOP-REAL 3 st
it = Dir u & u`3 = 1 & Tn2TR P = |[u`1,u`2]|;
existence
proof
reconsider p = Tn2TR P as Element of inside_of_circle(0,0,1) by A1;
reconsider Q = REAL2_to_BK p as Element of BK_model;
consider P2 be Element of TOP-REAL 2 such that
A2: P2 = p and
A3: REAL2_to_BK p = Dir |[P2`1,P2`2,1]| by BKMODEL2:def 3;
reconsider u = |[P2`1,P2`2,1]| as non zero Element of TOP-REAL 3;
now
thus Q = Dir u by A3;
|[u`1,u`2,u`3]| = |[P2`1,P2`2,1]| by EUCLID_5:3;
then
A4: u`1 = P2`1 & u`2 = P2`2 & u`3 = 1 by FINSEQ_1:78;
thus u`3 = 1 by EUCLID_5:2;
thus p = |[u`1,u`2]| by A2,A4,EUCLID:53;
end;
hence thesis;
end;
uniqueness
proof
let P1,P2 be POINT of BK-model-Plane such that
A5: ex u be non zero Element of TOP-REAL 3 st
P1 = Dir u & u`3 = 1 & Tn2TR P = |[u`1,u`2]| and
A6: ex v be non zero Element of TOP-REAL 3 st
P2 = Dir v & v`3 = 1 & Tn2TR P = |[v`1,v`2]|;
consider u be non zero Element of TOP-REAL 3 such that
A7: P1 = Dir u and
A8: u`3 = 1 and
A9: Tn2TR P = |[u`1,u`2]| by A5;
consider v be non zero Element of TOP-REAL 3 such that
A10: P2 = Dir v and
A11: v`3 = 1 and
A12: Tn2TR P = |[v`1,v`2]| by A6;
A13: u`1 = v`1 & u`2 = v`2 by A9,A12,FINSEQ_1:77;
u = |[v`1,v`2,v`3]| by A13,A8,A11,EUCLID_5:3
.= v by EUCLID_5:3;
hence thesis by A7,A10;
end;
end;
theorem Th02:
for P being POINT of BK-model-Plane holds
Tn2TR BK_to_T2 P in inside_of_circle(0,0,1)
proof
let P be POINT of BK-model-Plane;
consider p be Element of BK_model such that
P = p and
A1: BK_to_T2 P = BK_to_REAL2 p by Def01;
reconsider Q = BK_to_T2 P as POINT of TarskiEuclid2Space;
thus thesis by A1;
end;
theorem
for P being POINT of BK-model-Plane holds T2_to_BK BK_to_T2 P = P
proof
let P be POINT of BK-model-Plane;
consider p be Element of BK_model such that
A1: P = p and
A2: BK_to_T2 P = BK_to_REAL2 p by Def01;
consider u be non zero Element of TOP-REAL 3 such that
A3: Dir u = p and
A4: u.3 = 1 and
A5: BK_to_REAL2 p = |[u.1,u.2]| by BKMODEL2:def 2;
reconsider Q = BK_to_T2 P as POINT of TarskiEuclid2Space;
consider v be non zero Element of TOP-REAL 3 such that
A6: T2_to_BK Q = Dir v and
A7: v`3 = 1 and
A8: Tn2TR Q = |[v`1,v`2]| by A2,Def02;
u.1 = v`1 & u.2 = v`2 by A8,A5,A2,FINSEQ_1:77; then
A9: u`1 = v`1 & u`2 = v`2 by EUCLID_5:def 1,def 2;
u = |[u`1,u`2,u`3]| by EUCLID_5:3
.= |[v`1,v`2,v`3]| by A4,A7,A9,EUCLID_5:def 3
.= v by EUCLID_5:3;
hence thesis by A1,A6,A3;
end;
theorem Th03:
for P being POINT of TarskiEuclid2Space st
Tn2TR P is Element of inside_of_circle(0,0,1) holds BK_to_T2 T2_to_BK P = P
proof
let P be POINT of TarskiEuclid2Space;
assume Tn2TR P is Element of inside_of_circle(0,0,1);
then consider u be non zero Element of TOP-REAL 3 such that
A1: T2_to_BK P = Dir u and
A2: u`3 = 1 and
A3: Tn2TR P = |[u`1,u`2]| by Def02;
reconsider Q9 = T2_to_BK P as Element of BK-model-Plane;
reconsider Q = T2_to_BK P as Element of BK_model;
consider p be Element of BK_model such that
A4: Q9 = p and
A5: BK_to_T2 Q9 = BK_to_REAL2 p by Def01;
consider v be non zero Element of TOP-REAL 3 such that
A6: Dir v = p and
A7: v.3 = 1 and
A8: BK_to_REAL2 p = |[v.1,v.2]| by BKMODEL2:def 2;
are_Prop u,v by A4,A6,A1,ANPROJ_1:22;
then consider a be Real such that a <> 0 and
A9: u = a * v by ANPROJ_1:1;
A10: 1 = a * v`3 by A2,A9,EUCLID_5:9
.= a * 1 by A7,EUCLID_5:def 3
.= a;
|[u`1,u`2,u`3]| = u by EUCLID_5:3
.= |[1 * v`1,1 * v`2,1 * v`3]| by A9,A10,EUCLID_5:7;
then u`1 = v`1 & u`2 = v`2 by FINSEQ_1:78;
then u`1 = v.1 & u`2 = v.2 by EUCLID_5:def 1,def 2;
hence thesis by A5,A8,A3;
end;
theorem Th04:
for P being Point of BK-model-Plane
for p being Element of BK_model st P = p holds
BK_to_T2 P = BK_to_REAL2 p & Tn2TR BK_to_T2 P = BK_to_REAL2 p
proof
let P be Point of BK-model-Plane;
let p be Element of BK_model;
assume
A1: P = p;
ex p be Element of BK_model st P = p &
BK_to_T2 P = BK_to_REAL2 p by Def01;
hence thesis by A1;
end;
theorem Th05:
for P,Q,R being Point of BK-model-Plane
for P2,Q2,R2 being POINT of TarskiEuclid2Space st
P2 = BK_to_T2 P & Q2 = BK_to_T2 Q & R2 = BK_to_T2 R
holds between P,Q,R iff between P2,Q2,R2
proof
let P,Q,R be Point of BK-model-Plane;
let P2,Q2,R2 be POINT of TarskiEuclid2Space;
assume that
A1: P2 = BK_to_T2 P and
A2: Q2 = BK_to_T2 Q and
A3: R2 = BK_to_T2 R;
reconsider p = P,q = Q, r = R as Element of BK_model;
A4: Tn2TR BK_to_T2 P = BK_to_REAL2 p &
Tn2TR BK_to_T2 Q = BK_to_REAL2 q &
Tn2TR BK_to_T2 R = BK_to_REAL2 r by Th04;
hereby
assume between P,Q,R;
then BK_to_REAL2 q in LSeg(BK_to_REAL2 p,BK_to_REAL2 r)
by BKMODEL3:def 7;
hence between P2,Q2,R2 by A4,A1,A2,A3,GTARSKI2:20;
end;
assume between P2,Q2,R2;
then Tn2TR BK_to_T2 Q in LSeg(Tn2TR BK_to_T2 P,Tn2TR BK_to_T2 R)
by A1,A2,A3,GTARSKI2:20;
hence between P,Q,R by A4,BKMODEL3:def 7;
end;
theorem Th06:
for P,Q being Element of TOP-REAL 2 st P <> Q holds
P.1 <> Q.1 or P.2 <> Q.2
proof
let P,Q be Element of TOP-REAL 2;
assume
A1: P <> Q;
assume P.1 = Q.1 & P.2 = Q.2;
then P`1 = Q`1 & P`2 = Q`2;
then P = |[Q`1,Q`2]| by EUCLID:53
.= Q by EUCLID:53;
hence contradiction by A1;
end;
theorem Th07:
for a,b being Real
for P,Q being Element of TOP-REAL 2 st P <> Q &
(1 - a) * P + a * Q = (1 - b) * P + b * Q holds
a = b
proof
let a,b be Real;
let P,Q be Element of TOP-REAL 2;
assume that
A1: P <> Q and
A2: (1 - a) * P + a * Q = (1 - b) * P + b * Q;
reconsider PR2 = P, QR2= Q as Element of REAL 2 by EUCLID:22;
reconsider R2 = (1-a)*PR2+a*QR2 as Element of TOP-REAL 2 by EUCLID:22;
per cases by A1,Th06;
suppose P.1 <> Q.1;
then
A3: QR2.1 - PR2.1 <> 0;
0 = R2.1 - R2.1
.= (R2 - R2).1 by RVSUM_1:27
.= ((b - a) * (QR2 - PR2)).1 by A2,EUCLID12:1
.= (b - a) * (QR2 - PR2).1 by RVSUM_1:44
.= (b - a) * (QR2.1 - PR2.1) by RVSUM_1:27;
then (b - a) = 0 by A3;
hence thesis;
end;
suppose P.2 <> Q.2; then
A4: QR2.2 - PR2.2 <> 0;
0 = R2.2 - R2.2
.= (R2 - R2).2 by RVSUM_1:27
.= ((b - a) * (QR2 - PR2)).2 by A2,EUCLID12:1
.= (b - a) * (QR2 - PR2).2 by RVSUM_1:44
.= (b - a) * (QR2.2 - PR2.2) by RVSUM_1:27;
then (b - a) = 0 by A4;
hence thesis;
end;
end;
theorem Th08:
for P,Q being Point of BK-model-Plane st Tn2TR BK_to_T2 P = Tn2TR BK_to_T2 Q
holds P = Q
proof
let P,Q be Point of BK-model-Plane;
assume
A1: Tn2TR BK_to_T2 P = Tn2TR BK_to_T2 Q;
reconsider p = P,q = Q as Element of BK_model;
Tn2TR BK_to_T2 P = BK_to_REAL2 p &
Tn2TR BK_to_T2 Q = BK_to_REAL2 q by Th04;
hence thesis by A1,BKMODEL2:4;
end;
definition
let P,Q,R be Point of BK-model-Plane;
assume that
A1: between P,Q,R and
A2: P <> R;
func length(P,Q,R) -> Real means
:Def03:
0 <= it <= 1 &
Tn2TR BK_to_T2 Q = (1 - it) * Tn2TR BK_to_T2 P + it * Tn2TR BK_to_T2 R;
existence
proof
reconsider P2 = BK_to_T2 P,Q2 = BK_to_T2 Q,R2 = BK_to_T2 R as
Point of TarskiEuclid2Space;
reconsider p = P,q = Q,r = R as Element of BK_model;
BK_to_T2 P = BK_to_REAL2 p & Tn2TR BK_to_T2 P = BK_to_REAL2 p &
BK_to_T2 Q = BK_to_REAL2 q & Tn2TR BK_to_T2 Q = BK_to_REAL2 q &
BK_to_T2 R = BK_to_REAL2 r & Tn2TR BK_to_T2 R = BK_to_REAL2 r by Th04;
then Tn2TR BK_to_T2 Q in LSeg(Tn2TR BK_to_T2 P,Tn2TR BK_to_T2 R)
by A1,BKMODEL3:def 7;
then consider r be Real such that
A3: 0 <= r and
A4: r <= 1 and
A5: Tn2TR BK_to_T2 Q = (1-r) * Tn2TR BK_to_T2 P + r * Tn2TR BK_to_T2 R
by RLTOPSP1:76;
take r;
thus thesis by A3,A4,A5;
end;
uniqueness by A2,Th07,Th08;
end;
theorem Th09:
for P,Q being Point of BK-model-Plane holds
between P,P,Q & between P,Q,Q
proof
let P,Q be Point of BK-model-Plane;
reconsider P2 = BK_to_T2 P,Q2 = BK_to_T2 Q as Point of TarskiEuclid2Space;
between P2,P2,Q2 by GTARSKI1:17;
hence between P,P,Q by Th05;
between P2,Q2,Q2 by GTARSKI1:14;
hence between P,Q,Q by Th05;
end;
theorem
for P,Q being Point of BK-model-Plane st P <> Q holds
length(P,P,Q) = 0 & length(P,Q,Q) = 1
proof
let P,Q be Point of BK-model-Plane;
assume
A1: P <> Q;
reconsider P2 = BK_to_T2 P,Q2 = BK_to_T2 Q as Point of TarskiEuclid2Space;
A2: between P,P,Q by Th09;
A3: between P,Q,Q by Th09;
reconsider r = 0 as Real;
now
thus 0 <= r <= 1;
thus (1 - r ) * Tn2TR BK_to_T2 P + r * Tn2TR BK_to_T2 Q
= |[ 1 * (Tn2TR BK_to_T2 P)`1, 1 * (Tn2TR BK_to_T2 P)`2 ]|
+ 0 * Tn2TR BK_to_T2 Q by EUCLID:57
.= |[ (Tn2TR BK_to_T2 P)`1, (Tn2TR BK_to_T2 P)`2 ]|
+ |[ 0 * (Tn2TR BK_to_T2 Q)`1, 0 * (Tn2TR BK_to_T2 Q)`2 ]|
by EUCLID:57
.= |[ (Tn2TR BK_to_T2 P)`1 + 0 , (Tn2TR BK_to_T2 P)`2 + 0 ]|
by EUCLID:56
.= Tn2TR BK_to_T2 P by EUCLID:53;
end;
hence length(P,P,Q) = 0 by A1,A2,Def03;
reconsider s = 1 as Real;
now
thus 0 <= s <= 1;
thus (1 - s ) * Tn2TR BK_to_T2 P + s * Tn2TR BK_to_T2 Q
= |[ 1 * (Tn2TR BK_to_T2 Q)`1, 1 * (Tn2TR BK_to_T2 Q)`2 ]|
+ 0 * Tn2TR BK_to_T2 P by EUCLID:57
.= |[ (Tn2TR BK_to_T2 Q)`1, (Tn2TR BK_to_T2 Q)`2 ]|
+ |[ 0 * (Tn2TR BK_to_T2 P)`1, 0 * (Tn2TR BK_to_T2 P)`2 ]|
by EUCLID:57
.= |[ (Tn2TR BK_to_T2 Q)`1 + 0 , (Tn2TR BK_to_T2 Q)`2 + 0 ]|
by EUCLID:56
.= Tn2TR BK_to_T2 Q by EUCLID:53;
end;
hence length(P,Q,Q) = 1 by A1,A3,Def03;
end;
theorem
for N being Matrix of 3,F_Real st
N = <* <* 2, 0, -1 *>,
<* 0, sqrt 3, 0 *>,
<* 1, 0, -2 *> *> holds
Det N = (-3) * sqrt 3 & N is invertible
proof
let N be Matrix of 3,F_Real;
assume
A1: N = <* <* 2, 0 ,-1 *>,
<* 0, sqrt 3, 0 *>,
<* 1, 0 ,-2 *> *>;
reconsider a = 2,b = 0,c = -1,d = 0,e = sqrt 3,f = 0,g = 1,h = 0,i = -2
as Element of F_Real by XREAL_0:def 1;
Det N = a*e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h by A1,MATRIX_9:46;
then Det N = (-3) * sqrt 3 & Det N <> 0.F_Real by SQUARE_1:24;
then A2: Det N = (-3) * sqrt 3 & Det N <> 0.F_Real by SQUARE_1:24;
then Det N is non zero;
then Det N is unital;
then N is invertible by LAPLACE:34;
hence thesis by A2, LAPLACE:34;
end;
theorem Th10:
for a11,a12,a13,a21,a22,a23,a31,a32,a33,
b11,b12,b13,b21,b22,b23,b31,b32,b33,
ab11,ab12,ab13,ab21,ab22,ab23,ab31,ab32,ab33 being Element of F_Real
for A,B being Matrix of 3,F_Real st
A = <* <* a11,a12,a13 *>,
<* a21,a22,a23 *>,
<* a31,a32,a33 *> *> &
B = <* <* b11,b12,b13 *>,
<* b21,b22,b23 *>,
<* b31,b32,b33 *> *> &
ab11 = a11 * b11 + a12 * b21 + a13 * b31 &
ab12 = a11 * b12 + a12 * b22 + a13 * b32 &
ab13 = a11 * b13 + a12 * b23 + a13 * b33 &
ab21 = a21 * b11 + a22 * b21 + a23 * b31 &
ab22 = a21 * b12 + a22 * b22 + a23 * b32 &
ab23 = a21 * b13 + a22 * b23 + a23 * b33 &
ab31 = a31 * b11 + a32 * b21 + a33 * b31 &
ab32 = a31 * b12 + a32 * b22 + a33 * b32 &
ab33 = a31 * b13 + a32 * b23 + a33 * b33 holds
A * B = <* <* ab11, ab12, ab13 *>,
<* ab21, ab22, ab23 *>,
<* ab31, ab32, ab33 *> *> by ANPROJ_9:6;
theorem Th11:
for N1,N2 being Matrix of 3,F_Real st
N1 = <* <* 2, 0, -1 *>,
<* 0, sqrt 3, 0 *>,
<* 1, 0, -2 *> *> &
N2 = <* <* 2/3, 0, -1/3 *>,
<* 0, 1/sqrt 3, 0 *>,
<* 1/3, 0, -2/3 *> *> holds
N1 * N2 = <* <* 1,0,0 *>,
<* 0,1,0 *>,
<* 0,0,1 *> *>
proof
let N1,N2 be Matrix of 3,F_Real;
assume that
A1: N1 = <* <* 2, 0, -1 *>,
<* 0, sqrt 3, 0 *>,
<* 1, 0, -2 *> *> and
A2: N2 = <* <* 2/3, 0, -1/3 *>,
<* 0, 1/sqrt 3, 0 *>,
<* 1/3, 0, -2/3 *> *>;
reconsider a = 2,b = 0,c = -1,d = 0, e = sqrt 3,f = 0,g = 1,h=0,i = -2,
a9 = 2/3,b9=0,c9 = - 1/3,d9=0,e9 = 1/sqrt 3,f9=0,g9 = 1/3,h9=0,i9 = -2/3
as Element of F_Real by XREAL_0:def 1;
reconsider n11 = a*a9+b*d9+c*g9, n12 = a*b9+b*e9+c*h9,
n13 = a*c9+b*f9+c*i9, n21 = d*a9+e*d9+f*g9,
n22 = d*b9+e*e9+f*h9, n23 = d*c9+e*f9+f*i9,
n31 = g*a9+h*d9+i*g9, n32 = g*b9+h*e9+i*h9,
n33 = g*c9+h*f9+i*i9 as Element of F_Real;
n11 = 1 & n12 = 0 & n13 = 0 & n21 = 0 &
n22 = 1 & n23 = 0 & n31 = 0 & n32 = 0 & n33 = 1
by SQUARE_1:24,XCMPLX_1:106;
hence thesis by A1,A2,Th10;
end;
theorem Th12:
for N1,N2 being Matrix of 3,F_Real st
N2 = <* <* 2, 0, -1 *>,
<* 0, sqrt 3, 0 *>,
<* 1, 0, -2 *> *> &
N1 = <* <* 2/3, 0, -1/3 *>,
<* 0, 1/sqrt 3, 0 *>,
<* 1/3, 0, -2/3 *> *> holds
N1 * N2 = <* <* 1,0,0 *>,
<* 0,1,0 *>,
<* 0,0,1 *> *>
proof
let N1,N2 be Matrix of 3,F_Real;
assume that
A1: N2 = <* <* 2, 0, -1 *>,
<* 0, sqrt 3, 0 *>,
<* 1, 0, -2 *> *> and
A2: N1 = <* <* 2/3, 0, -1/3 *>,
<* 0, 1/sqrt 3, 0 *>,
<* 1/3, 0, -2/3 *> *>;
reconsider a9 = 2,b9 = 0,c9 = -1,d9 = 0, e9 = sqrt 3,f9 = 0,g9 = 1,h9=0,
i9 = -2,a = 2/3,b=0,c = - 1/3,d=0,e = 1/sqrt 3,f=0,g = 1/3,h=0,i = -2/3
as Element of F_Real by XREAL_0:def 1;
reconsider n11 = a*a9+b*d9+c*g9, n12 = a*b9+b*e9+c*h9,
n13 = a*c9+b*f9+c*i9, n21 = d*a9+e*d9+f*g9,
n22 = d*b9+e*e9+f*h9, n23 = d*c9+e*f9+f*i9,
n31 = g*a9+h*d9+i*g9,n32 = g*b9+h*e9+i*h9,n33 = g*c9+h*f9+i*i9
as Element of F_Real;
n11 = 1 & n12 = 0 & n13 = 0 & n21 = 0 &
n22 = 1 & n23 = 0 & n31 = 0 & n32 = 0 & n33 = 1
by SQUARE_1:24,XCMPLX_1:106;
hence thesis by A1,A2,Th10;
end;
theorem Th13:
for N1,N2 being Matrix of 3,F_Real st
N1 = <* <* 2, 0, -1 *>,
<* 0, sqrt 3, 0 *>,
<* 1, 0, -2 *> *> &
N2 = <* <* 2/3, 0, -1/3 *>,
<* 0, 1/sqrt 3, 0 *>,
<* 1/3, 0, -2/3 *> *>
holds N1 is_reverse_of N2
proof
let N1,N2 be Matrix of 3,F_Real;
assume
A1: N1 = <* <* 2, 0, -1 *>,
<* 0, sqrt 3, 0 *>,
<* 1, 0, -2 *> *> &
N2 = <* <* 2/3, 0, -1/3 *>,
<* 0, 1/sqrt 3, 0 *>,
<* 1/3, 0, -2/3 *> *>;
N2 * N1 = 1.(F_Real,3) & N1 * N2 = 1.(F_Real,3) by A1,Th11,Th12,ANPROJ_9:1;
hence thesis by MATRIX_6:def 2;
end;
theorem Th14:
for N being invertible Matrix of 3,F_Real st
N = <* <* 2/3, 0 ,-1/3 *>,
<* 0, 1/sqrt 3, 0 *>,
<* 1/3, 0 ,-2/3 *> *> holds
homography(N).:absolute c= absolute
proof
let N be invertible Matrix of 3,F_Real;
assume
A1: N = <* <* 2/3, 0 ,-1/3 *>,
<* 0, 1/sqrt 3, 0 *>,
<* 1/3, 0 ,-2/3 *> *>;
reconsider a=2/3,b=0,c = -1/3,d=0,e=1/sqrt 3,f=0,g=1/3,h=0,i=-2/3
as Element of F_Real by XREAL_0:def 1;
homography(N).:absolute c= absolute
proof
let x be object;
assume x in homography(N).:absolute;
then consider y be object such that
A2: y in dom homography(N) and
A3: y in absolute and
A4: x = homography(N).y by FUNCT_1:def 6;
reconsider y as Point of ProjectiveSpace TOP-REAL 3 by A2;
consider yu be non zero Element of TOP-REAL 3 such that
A5: (yu.1)^2 + (yu.2)^2 = 1 and
A6: yu.3 = 1 and
A7: y = Dir yu by A3,BKMODEL1:89;
A8: yu`1 * yu`1 + yu`2 * yu`2 = yu.1 * yu`1 + yu`2 * yu`2
by EUCLID_5:def 1
.= yu.1 * yu.1 + yu`2 * yu`2 by EUCLID_5:def 1
.= yu.1 * yu.1 + yu.2 * yu`2 by EUCLID_5:def 2
.= yu.1 * yu.1 + yu.2 * yu.2 by EUCLID_5:def 2
.= (yu.1)^2 + yu.2 * yu.2 by SQUARE_1:def 1
.= 1 by A5,SQUARE_1:def 1;
A9: yu`3 * yu`3 = yu.3 * yu`3 by EUCLID_5:def 3
.= 1 by A6,EUCLID_5:def 3;
consider u,v be Element of TOP-REAL 3,
uf be FinSequence of F_Real,
p be FinSequence of 1-tuples_on REAL such that
A10: y = Dir u & u is not zero & u = uf & p = N * uf & v = M2F p &
v is not zero & homography(N).y = Dir v by ANPROJ_8:def 4;
are_Prop u,yu by A7,A10,ANPROJ_1:22;
then consider l be Real such that l <> 0 and
A11: u = l * yu by ANPROJ_1:1;
reconsider u1 = l * yu`1,u2 = l * yu`2,u3 = l * yu`3 as Element of F_Real
by XREAL_0:def 1;
uf = <* u1,u2,u3 *> by A11,A10,EUCLID_5:7;
then
v = <* a*u1+b*u2+c*u3,d*u1+e*u2+f*u3,g*u1+h*u2+i*u3 *> by A1,A10,PASCAL:8
.= <* (2/3) * u1 - (1/3) * u3, (1/sqrt 3) * u2,
(1/3) * u1 - (2/3) * u3 *>;
then v`1 = (2/3) * u1 - (1/3) * u3 & v`2 = (1 / sqrt 3) * u2 &
v`3 = (1/3) * u1 - (2/3) * u3 by EUCLID_5:2;
then
A12: v.1 = (2/3) * u1 - (1/3) * u3 & v.2 = (1/sqrt 3) * u2 &
v.3 = (1/3) * u1 - (2/3) * u3 by EUCLID_5:def 1,def 2,def 3;
set k = (1/3)*(1/3);
1 / sqrt 3 = sqrt 3 / 3 by BKMODEL3:10; then
A13: (1 / sqrt 3) * (1 / sqrt 3) = k * ((sqrt 3) * sqrt 3)
.= k * (sqrt (3 * 3)) by SQUARE_1:29
.= k * sqrt (3^2) by SQUARE_1:def 1
.= k * 3 by SQUARE_1:def 2;
A14: v.2 * v.2 = (1/sqrt 3) * (1/sqrt 3) * u2 * u2 by A12
.= k * 3 * u2 * u2 by A13;
reconsider P = homography(N).y as Point of ProjectiveSpace TOP-REAL 3;
qfconic(1,1,-1,0,0,0,v)=0
proof
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
.= k * (4 * u1 * u1 - 4 * u1 * u3 + u3 * u3) + k * 3 * u2 * u2
- k * (u1 * u1 - 4 * u1 * u3 + 4 * u3 * u3) by A12,A14
.= k * 3 * (l * l) * (yu`1 * yu`1 + yu`2 * yu`2 - yu`3 * yu`3)
.= 0 by A8,A9;
hence thesis;
end;
hence x in absolute by A4,A10,PASCAL:11;
end;
hence thesis;
end;
theorem
for N being invertible Matrix of 3,F_Real st
N = <* <* 2, 0 , -1 *>,
<* 0, sqrt 3, 0 *>,
<* 1, 0 , -2 *> *>
holds
homography(N).:absolute = absolute
proof
let N be invertible Matrix of 3,F_Real;
assume
A1: N = <* <* 2, 0 ,-1 *>,
<* 0, sqrt 3, 0 *>,
<* 1, 0 ,-2 *> *>;
reconsider a=2,b=0,c = -1,d=0,e=sqrt 3,f=0,g=1,h=0,i=-2
as Element of F_Real by XREAL_0:def 1;
A2: homography(N).:absolute c= absolute
proof
let x be object;
assume x in homography(N).:absolute;
then consider y be object such that
A3: y in dom homography(N) and
A4: y in absolute and
A5: x = homography(N).y by FUNCT_1:def 6;
reconsider y as Point of ProjectiveSpace TOP-REAL 3 by A3;
consider yu be non zero Element of TOP-REAL 3 such that
A6: (yu.1)^2 + (yu.2)^2 = 1 and
A7: yu.3 = 1 and
A8: y = Dir yu by A4,BKMODEL1:89;
A9: yu`1 * yu`1 + yu`2 * yu`2 = yu.1 * yu`1 + yu`2 * yu`2 by EUCLID_5:def 1
.= yu.1 * yu.1 + yu`2 * yu`2 by EUCLID_5:def 1
.= yu.1 * yu.1 + yu.2 * yu`2 by EUCLID_5:def 2
.= yu.1 * yu.1 + yu.2 * yu.2 by EUCLID_5:def 2
.= (yu.1)^2 + yu.2 * yu.2 by SQUARE_1:def 1
.= 1 by A6,SQUARE_1:def 1;
A10: yu`3 * yu`3 = yu.3 * yu`3 by EUCLID_5:def 3
.= 1 by A7,EUCLID_5:def 3;
consider u,v be Element of TOP-REAL 3,
uf be FinSequence of F_Real,
p be FinSequence of 1-tuples_on REAL
such that
A11: y = Dir u & u is not zero & u = uf & p = N * uf & v = M2F p &
v is not zero & homography(N).y = Dir v by ANPROJ_8:def 4;
are_Prop u,yu by A8,A11,ANPROJ_1:22;
then consider l be Real such that l <> 0 and
A12: u = l * yu by ANPROJ_1:1;
reconsider u1 = l * yu`1,u2 = l * yu`2,u3 = l * yu`3
as Element of F_Real by XREAL_0:def 1;
uf = <* u1,u2,u3 *> by A12,EUCLID_5:7,A11;
then v = <* a*u1+b*u2+c*u3,d*u1+e*u2+f*u3,g*u1+h*u2+i*u3 *>
by A1,A11,PASCAL:8
.= <* 2 * u1 - u3, (sqrt 3) * u2,u1 - 2 * u3 *>;
then v`1 = 2 * u1 - u3 & v`2 = (sqrt 3) * u2 & v`3 = u1 - 2 * u3
by EUCLID_5:2;
then
A13: v.1 = 2 * u1 - u3 & v.2 = (sqrt 3) * u2 & v.3 = u1 - 2 * u3
by EUCLID_5:def 1,def 2,def 3;
A14: v.1 * v.1 = (2 * u1 - u3)^2 by A13,SQUARE_1:def 1
.= (2 * u1)^2 - 2 * (2 * u1) * u3 + u3^2 by SQUARE_1:5
.= (2 * u1) * (2 * u1) - 2 * (2 * u1) * u3 + u3^2
by SQUARE_1:def 1
.= 4 * u1 * u1 - 4 * u1 * u3 + u3 * u3 by SQUARE_1:def 1;
A15: v.2 * v.2 = (sqrt 3) * (sqrt 3) * u2 * u2 by A13
.= sqrt (3 * 3) * u2 * u2 by SQUARE_1:29
.= sqrt (3^2) * u2 * u2 by SQUARE_1:def 1
.= 3 * u2 * u2 by SQUARE_1:def 2;
A16: v.3 * v.3 = (u1 - 2 * u3)^2 by A13,SQUARE_1:def 1
.= u1^2 - 2 * u1 * (2 * u3) + (2 * u3)^2 by SQUARE_1:5
.= u1 * u1 - 2 * 2 * u1 * u3 + (2 * u3)^2 by SQUARE_1:def 1
.= u1 * u1 - 2 * 2 * u1 * u3 + (2 * u3) * (2 * u3)
by SQUARE_1:def 1
.= u1 * u1 - 4 * u1 * u3 + 4 * u3 * u3;
reconsider P = homography(N).y as Point of ProjectiveSpace TOP-REAL 3;
qfconic(1,1,-1,0,0,0,v)=0
proof
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
.= (4 * u1 * u1 - 4 * u1 * u3 + u3 * u3) +
3 * u2 * u2 - (u1 * u1
- 4 * u1 * u3 + 4 * u3 * u3) by A14,A15,A16
.= 3 * (l * l) * (yu`1 * yu`1 + yu`2 * yu`2
- yu`3 * yu`3)
.= 0 by A9,A10;
hence thesis;
end;
hence x in absolute by A5,A11,PASCAL:11;
end;
absolute c= homography(N).:absolute
proof
let x be object;
assume
A17: x in absolute;
reconsider N1 = <* <* 2/3, 0 ,-1/3 *>,
<* 0, 1/sqrt 3, 0 *>,
<* 1/3, 0 ,-2/3 *> *> as Matrix of 3,F_Real
by ANPROJ_8:19;
N1 is_reverse_of N by A1,Th13;
then reconsider N1 as invertible Matrix of 3,F_Real by MATRIX_6:def 3;
A18: homography(N1).:absolute c= absolute by Th14;
dom homography(N1) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
then homography(N1).x in homography(N1).:absolute by A17,FUNCT_1:108;
then reconsider y = homography(N1).x as Element of absolute by A18;
A19: N * N1 = 1.(F_Real,3) by A1,Th11,ANPROJ_9:1;
now
dom homography(N) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
hence y in dom homography(N);
thus y in absolute;
reconsider P = x as Point of ProjectiveSpace TOP-REAL 3 by A17;
thus homography(N).y = homography(1.(F_Real,3)).P by A19,ANPROJ_9:13
.= x by ANPROJ_9:14;
end;
hence x in homography(N).:absolute by FUNCT_1:108;
end;
hence thesis by A2;
end;
theorem Th15:
for a,b,r being Real
for P,Q,R being Element of TOP-REAL 2 st
Q in LSeg(P,R) & P in inside_of_circle(a,b,r) & R in inside_of_circle(a,b,r)
holds Q in inside_of_circle(a,b,r)
proof
let a,b,r be Real;
let P,Q,R be Element of TOP-REAL 2;
assume that
A1: Q in LSeg(P,R) and
A2: P in inside_of_circle(a,b,r) and
A3: R in inside_of_circle(a,b,r);
consider s be Real such that
A4: 0 <= s & s <= 1 and
A5: Q = (1 - s)*P + s * R by A1,RLTOPSP1:76;
s in [. 0,1 .] by A4,XXREAL_1:1;
then s in ]. 0,1 .[ or s = 0 or s = 1 by XXREAL_1:5;
then per cases by XXREAL_1:4;
suppose
A6: 0 < s & s < 1;
Q = s * R + (1 - s)* P by A5;
hence thesis by A2,A3,A6,CONVEX1:def 2;
end;
suppose
s = 0;
then Q = P + 0 * R by A5,RVSUM_1:52
.= P by GTARSKI2:2;
hence thesis by A2;
end;
suppose s = 1;
then Q = R + 0 * P by A5,RVSUM_1:52
.= R by GTARSKI2:2;
hence thesis by A3;
end;
end;
theorem Th16:
for u,v being non zero Element of TOP-REAL 3 st
Dir u = Dir v & u.3 <> 0 & u.3 = v.3 holds u = v
proof
let u,v be non zero Element of TOP-REAL 3;
assume that
A1: Dir u = Dir v and
A2: u.3 <> 0 and
A3: u.3 = v.3;
are_Prop u,v by A1,ANPROJ_1:22;
then consider a be Real such that a <> 0 and
A4: u = a * v by ANPROJ_1:1;
u.3 = a * u.3 by A3,A4,RVSUM_1:44;
then a = 1 by A2,XCMPLX_1:7;
hence thesis by A4,RVSUM_1:52;
end;
theorem Th17:
for R being Element of ProjectiveSpace TOP-REAL 3
for P,Q being Element of BK_model
for u,v,w being non zero Element of TOP-REAL 3
for r being Real st 0 <= r <= 1 & P = Dir u &
Q = Dir v & R = Dir w & u.3 = 1 & v.3 = 1 &
w = r * u + (1 - r) * v holds R is Element of BK_model
proof
let R be Element of ProjectiveSpace TOP-REAL 3;
let P,Q be Element of BK_model;
let u,v,w be non zero Element of TOP-REAL 3;
let r be Real;
assume that
A1: 0 <= r <= 1 and
A2: P = Dir u & Q = Dir v & R = Dir w and
A3: u.3 = 1 & v.3 = 1 and
A4: w = r * u + (1 - r) * v;
reconsider ru = r * u,rv = (1 - r) * v as Element of REAL 3 by EUCLID:22;
A5: w.3 = ru.3 + rv.3 by A4,RVSUM_1:11
.= r * u.3 + rv.3 by RVSUM_1:44
.= r + (1 - r) * 1 by A3,RVSUM_1:44
.= 1;
consider u2 be non zero Element of TOP-REAL 3 such that
A6: Dir u2 = P & u2.3 = 1 & BK_to_REAL2 P = |[u2.1,u2.2]| by BKMODEL2:def 2;
A7: u = u2 by A2,A3,A6,Th16;
reconsider ru2 = |[u2.1,u2.2]| as Element of TOP-REAL 2;
consider v2 be non zero Element of TOP-REAL 3 such that
A8: Dir v2 = Q & v2.3 = 1 & BK_to_REAL2 Q = |[v2.1,v2.2]| by BKMODEL2:def 2;
A9: v = v2 by A2,A3,A8,Th16;
reconsider rv2 = |[v2.1,v2.2]| as Element of TOP-REAL 2;
reconsider rw = |[w.1,w.2]| as Element of TOP-REAL 2;
rw = r * ru2 + (1 - r) * rv2
proof
A10: w.1 = ru.1 + rv.1 by A4,RVSUM_1:11
.= r * u.1 + rv.1 by RVSUM_1:44
.= r * u2.1 + (1 - r) * v2.1 by A7,A9,RVSUM_1:44;
A13: w.2 = ru.2 + rv.2 by A4,RVSUM_1:11
.= r * u.2 + rv.2 by RVSUM_1:44
.= r * u2.2 + (1 - r) * v2.2 by A7,A9,RVSUM_1:44;
r * ru2 + (1 - r) * rv2 = |[r*u2.1,r*u2.2]| + (1 - r) * |[v2.1,v2.2]|
by EUCLID:58
.= |[r*u2.1,r*u2.2]| + |[(1-r)*v2.1,(1-r)*v2.2]|
by EUCLID:58;
hence thesis by A10,A13,EUCLID:56;
end;
then rw = (1 - r) * rv2 + r * ru2;
then rw in {(1 - r) * rv2 + r * ru2 where r is Real:0 <= r & r <= 1} by A1;
then rw in LSeg(rv2,ru2) by RLTOPSP1:def 2;
then reconsider rw as Element of inside_of_circle(0,0,1) by A6,A8,Th15;
consider RW2 be Element of TOP-REAL 2 such that
A11: RW2 = rw & REAL2_to_BK rw = Dir |[RW2`1,RW2`2,1]| by BKMODEL2:def 3;
A12: rw`1 = w.1 & rw`2 = w.2 by EUCLID:52;
w = |[w`1,w`2,w`3]| by EUCLID_5:3
.= |[w.1,w`2,w`3]| by EUCLID_5:def 1
.= |[w.1,w.2,w`3]| by EUCLID_5:def 2
.= |[w.1,w.2,w.3]| by EUCLID_5:def 3;
hence thesis by A2,A11,A5,A12;
end;
theorem Th18:
for N being invertible Matrix of 3,F_Real
for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
for P,Q being Point of ProjectiveSpace TOP-REAL 3
for u,v being non zero Element of TOP-REAL 3 st
N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & Q = Dir v & Q = homography(N).P & u.3 = 1
holds ex a being non zero Real st
v.1 = a * (n11 * u.1 + n12 * u.2 + n13) &
v.2 = a * (n21 * u.1 + n22 * u.2 + n23) &
v.3 = a * (n31 * u.1 + n32 * u.2 + n33)
proof
let N be invertible Matrix of 3,F_Real;
let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
let P,Q be Point of ProjectiveSpace TOP-REAL 3;
let u,v be non zero Element of TOP-REAL 3;
assume
A1: N = <* <* n11,n12,n13 *>, <* n21,n22,n23 *>, <* n31,n32,n33 *> *> &
P = Dir u & Q = Dir v & Q = homography(N).P & u.3 = 1;
consider u9,v9 be Element of TOP-REAL 3,
uf be FinSequence of F_Real,
p be FinSequence of 1-tuples_on REAL
such that
A2: P = Dir u9 & u9 is not zero & u9 = uf & p = N * uf & v9 = M2F p &
v9 is not zero & homography(N).P = Dir v9 by ANPROJ_8:def 4;
are_Prop u,u9 by A1,A2,ANPROJ_1:22;
then consider a be Real such that
A3: a <> 0 & u9 = a * u by ANPROJ_1:1;
A4: |[u9`1,u9`2,u9`3]| = u9 by EUCLID_5:3
.= |[ a * u`1,a * u`2, a * u`3 ]|
by A3,EUCLID_5:7
.= |[ a * u`1,a * u`2, a * u.3 ]| by EUCLID_5:def 3
.= |[ a * u`1,a * u`2, a]| by A1;
reconsider uf1=a*u`1,uf2=a*u`2,uf3=a as Element of F_Real by XREAL_0:def 1;
reconsider x1 = n11*u`1+n12*u`2+n13, x2 = n21*u`1+n22*u`2+n23,
x3 = n31*u`1+n32*u`2+n33 as Element of REAL by XREAL_0:def 1;
uf = <* uf1,uf2,uf3 *> by A2,A4,EUCLID_5:3;
then
A5: v9 = <* n11*uf1+n12*uf2+n13*uf3,
n21*uf1+n22*uf2+n23*uf3,
n31*uf1+n32*uf2+n33*uf3 *> by A1,A2,PASCAL:8
.= <* a*(n11*u`1+n12*u`2+n13),
a*(n21*u`1+n22*u`2+n23),
a*(n31*u`1+n32*u`2+n33) *>
.= a * |[x1,x2,x3]| by EUCLID_5:8;
are_Prop v,v9 by A1,A2,ANPROJ_1:22;
then consider b be Real such that
A6: b <> 0 and
A7: v = b * v9 by ANPROJ_1:1;
A8: v = b * |[a * x1,a * x2, a * x3]| by A7,A5,EUCLID_5:8
.= |[ b * (a * x1),b * (a * x2),b * (a * x3)]| by EUCLID_5:8
.= |[ (b * a) * (n11 * u`1 + n12 * u`2 + n13),
(b * a) * (n21 * u`1 + n22 * u`2 + n23),
(b * a) * (n31 * u`1 + n32 * u`2 + n33) ]|;
reconsider c = b * a as non zero Real by A3,A6;
take c;
v`1 = c * (n11 * u`1 + n12 * u`2 + n13) &
v`2 = c * (n21 * u`1 + n22 * u`2 + n23) &
v`3 = c * (n31 * u`1 + n32 * u`2 + n33)
by A8,EUCLID_5:2;
then v.1 = c * (n11 * u`1 + n12 * u`2 + n13) &
v.2 = c * (n21 * u`1 + n22 * u`2 + n23) &
v.3 = c * (n31 * u`1 + n32 * u`2 + n33)
by EUCLID_5:def 1,def 2,def 3;
then v.1 = c * (n11 * u.1 + n12 * u`2 + n13) &
v.2 = c * (n21 * u.1 + n22 * u`2 + n23) &
v.3 = c * (n31 * u.1 + n32 * u`2 + n33)
by EUCLID_5:def 1;
hence thesis by EUCLID_5:def 2;
end;
theorem Th19:
for N being invertible Matrix of 3,F_Real
for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
for P being Element of BK_model
for Q being Point of ProjectiveSpace TOP-REAL 3
for u,v being non zero Element of TOP-REAL 3 st
N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & Q = Dir v & Q = homography(N).P &
u.3 = 1 & v.3 = 1 holds n31 * u.1 + n32 * u.2 + n33 <> 0 &
v.1 = (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33) &
v.2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33)
proof
let N be invertible Matrix of 3,F_Real;
let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
let P be Element of BK_model;
let Q be Point of ProjectiveSpace TOP-REAL 3;
let u,v be non zero Element of TOP-REAL 3;
assume that
A1: N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> and
A2: P = Dir u and
A3: Q = Dir v and
A4: Q = homography(N).P and
A5: u.3 = 1 and
A6: v.3 = 1;
consider a be non zero Real such that
A7: v.1 = a * (n11 * u.1 + n12 * u.2 + n13) and
A8: v.2 = a * (n21 * u.1 + n22 * u.2 + n23) and
A9: v.3 = a * (n31 * u.1 + n32 * u.2 + n33) by A1,A2,A3, A4,A5,Th18;
thus n31 * u.1 + n32 * u.2 + n33 <> 0 by A6,A9;
reconsider nn = n31 * u.1 + n32 * u.2 + n33 as non zero Real by A6,A9;
a = 1 / nn by A6,A9,XCMPLX_1:73;
hence thesis by A7,A8;
end;
theorem Th20:
for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry
for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
for P being Element of BK_model
for u being non zero Element of TOP-REAL 3 st
h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & u.3 = 1 holds n31 * u.1 + n32 * u.2 + n33 <> 0
proof
let N be invertible Matrix of 3,F_Real;
let h be Element of SubGroupK-isometry;
let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
let P be Element of BK_model;
let u be non zero Element of TOP-REAL 3;
assume
A1: h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & u.3 = 1;
reconsider Q = homography(N).P as Point of ProjectiveSpace TOP-REAL 3;
reconsider Q = homography(N).P as Element of BK_model by A1,BKMODEL3:36;
ex v be non zero Element of TOP-REAL 3 st Q = Dir v & v.3 = 1 &
BK_to_REAL2 Q = |[v.1,v.2]| by BKMODEL2:def 2;
hence thesis by A1,Th19;
end;
theorem Th21:
for N being invertible Matrix of 3,F_Real
for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
for P being Element of absolute
for Q being Point of ProjectiveSpace TOP-REAL 3
for u,v being non zero Element of TOP-REAL 3 st
N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & Q = Dir v & Q = homography(N).P & u.3 = 1 & v.3 = 1
holds n31 * u.1 + n32 * u.2 + n33 <> 0 &
v.1 = (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33) &
v.2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33)
proof
let N be invertible Matrix of 3,F_Real;
let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
let P be Element of absolute;
let Q be Point of ProjectiveSpace TOP-REAL 3;
let u,v be non zero Element of TOP-REAL 3;
assume
A1: N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & Q = Dir v & Q = homography(N).P & u.3 = 1 & v.3 = 1;
consider a be non zero Real such that
A2: v.1 = a * (n11 * u.1 + n12 * u.2 + n13) and
A3: v.2 = a * (n21 * u.1 + n22 * u.2 + n23) and
A4: v.3 = a * (n31 * u.1 + n32 * u.2 + n33) by A1,Th18;
thus n31 * u.1 + n32 * u.2 + n33 <> 0 by A1,A4;
reconsider nn = n31 * u.1 + n32 * u.2 + n33 as non zero Real by A1,A4;
a = 1 / nn by A1,A4,XCMPLX_1:73;
hence thesis by A2,A3;
end;
theorem Th22:
for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry
for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
for P being Element of absolute
for u being non zero Element of TOP-REAL 3 st
h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & u.3 = 1 holds n31 * u.1 + n32 * u.2 + n33 <> 0
proof
let N be invertible Matrix of 3,F_Real;
let h be Element of SubGroupK-isometry;
let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
let P be Element of absolute;
let u be non zero Element of TOP-REAL 3;
assume
A1: h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & u.3 = 1;
reconsider Q = homography(N).P as Point of ProjectiveSpace TOP-REAL 3;
reconsider Q = homography(N).P as Element of absolute by A1,BKMODEL3:35;
ex v be non zero Element of TOP-REAL 3 st Q = Dir v & v.3 = 1 &
absolute_to_REAL2 Q = |[v.1,v.2]| by BKMODEL1:def 8;
hence thesis by A1,Th21;
end;
theorem Th23:
for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry
for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
for P being Element of BK_model
for u being non zero Element of TOP-REAL 3 st
h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & u.3 = 1 holds
homography(N).P = Dir |[
(n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33),
(n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33),
1 ]|
proof
let N be invertible Matrix of 3,F_Real;
let h be Element of SubGroupK-isometry;
let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
let P be Element of BK_model;
let u be non zero Element of TOP-REAL 3;
assume
A1: h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & u.3 = 1;
reconsider Q = homography(N).P as Element of BK_model by A1,BKMODEL3:36;
consider v be non zero Element of TOP-REAL 3 such that
A2: Q = Dir v & v.3 = 1 & BK_to_REAL2 Q = |[v.1,v.2]| by BKMODEL2:def 2;
n31 * u.1 + n32 * u.2 + n33 <> 0 &
v.1 = (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33) &
v.2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33)
by A2,A1,Th19;
then v`1 = (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33) &
v`2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33) &
v`3 = 1 by A2,EUCLID_5:def 1,def 2,def 3;
hence thesis by A2,EUCLID_5:3;
end;
theorem Th24:
for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry
for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
for P being Element of absolute
for u being non zero Element of TOP-REAL 3 st
h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
P = Dir u & u.3 = 1 holds
homography(N).P = Dir |[
(n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33),
(n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33),
1 ]|
proof
let N be invertible Matrix of 3,F_Real;
let h be Element of SubGroupK-isometry;
let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
let P be Element of absolute;
let u be non zero Element of TOP-REAL 3;
assume that
A1: h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> and
A2: P = Dir u & u.3 = 1;
reconsider Q = homography(N).P as Element of absolute by A1,BKMODEL3:35;
consider v be non zero Element of TOP-REAL 3 such that
A3: Q = Dir v & v.3 = 1 &
absolute_to_REAL2(Q) = |[v.1,v.2]| by BKMODEL1:def 8;
now
n31 * u.1 + n32 * u.2 + n33 <> 0 &
v.1 = (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33) &
v.2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33)
by A3,A2,A1,Th21;
hence v`1 = (n11 * u.1 + n12 * u.2 + n13) /
(n31 * u.1 + n32 * u.2 + n33) &
v`2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33) &
v`3 = 1 by A3,EUCLID_5:def 1,def 2,def 3;
thus homography(N).P = Dir |[v`1,v`2,v`3]| by A3,EUCLID_5:3;
end;
hence thesis;
end;
theorem Th26:
for A being Subset of TOP-REAL 3
for B being convex non empty Subset of TOP-REAL 2
for r being Real
for x being Element of TOP-REAL 3 st
A = {x where x is Element of TOP-REAL 3:|[x`1,x`2]| in B & x`3 = r}
holds A is non empty convex
proof
let A be Subset of TOP-REAL 3;
let B be convex non empty Subset of TOP-REAL 2;
let r be Real;
let x be Element of TOP-REAL 3;
assume
A1: A = {x where x is Element of TOP-REAL 3:|[x`1,x`2]| in B & x`3 = r};
A2: for z be Element of TOP-REAL 3 holds z in A iff |[z`1,z`2]| in B & z`3 = r
proof
let z be Element of TOP-REAL 3;
hereby
assume z in A;
then ex z9 be Element of TOP-REAL 3 st z = z9 & |[z9`1,z9`2]| in B &
z9`3 = r by A1;
hence |[z`1,z`2]| in B & z`3 = r;
end;
assume |[z`1,z`2]| in B & z`3 = r;
hence z in A by A1;
end;
set y = the Element of B;
reconsider z = |[y`1,y`2,r]| as Element of TOP-REAL 3;
z = |[z`1,z`2,z`3]| by EUCLID_5:3;
then
A3: z`1 = y`1 & z`2 = y`2 & z`3 = r by FINSEQ_1:78;
y in B;
then |[z`1,z`2]| in B & z`3 = r by A3,EUCLID:53;
then z in A by A1;
hence A is non empty;
now
let u,v be Element of TOP-REAL 3;
let s be Real;
assume that
A4: 0 < s < 1 and
A5: u in A and
A6: v in A;
reconsider w = s * u + (1 - s) * v as Element of TOP-REAL 3;
now
reconsider su = s * u,sv = (1 - s) * v as Element of TOP-REAL 3;
su = |[s * u`1,s * u`2,s * u`3]| &
sv = |[(1-s)*v`1,(1-s)*v`2,(1-s)*v`3]| by EUCLID_5:7;
then
A7: |[s * u`1 + (1-s)*v`1,s*u`2+(1-s)*v`2,s*u`3+(1-s)*v`3]|
= w by EUCLID_5:6
.= |[w`1,w`2,w`3]| by EUCLID_5:3;
then
A8: w`1 = s * u`1 + (1-s)*v`1 & w`2=s*u`2+(1-s)*v`2 & w`3=s*u`3+(1-s)*v`3
by FINSEQ_1:78;
u`3 = r & v`3 = r by A5,A6,A2;
hence w`3 = r by A7,FINSEQ_1:78;
reconsider u9 = |[u`1,u`2]|,v9 = |[v`1,v`2]|,w9 = |[w`1,w`2]|
as Element of TOP-REAL 2;
now
thus u9 in B & v9 in B by A2,A6,A5;
thus |[w`1,w`2]| = |[s*u`1,s*u`2]| + |[(1-s)*v`1,(1-s)*v`2]|
by A8,EUCLID:56
.= s * |[u`1,u`2]| + |[(1-s)*v`1,(1-s)*v`2]|
by EUCLID:58
.= s * u9 + (1 - s) * v9 by EUCLID:58;
end;
hence |[w`1,w`2]| in B by A4,CONVEX1:def 2;
end;
hence s * u + (1 - s) * v in A by A1;
end;
hence A is convex by CONVEX1:def 2;
end;
theorem Th27:
for n1,n2,n3 being Element of F_Real
for n,u being Element of TOP-REAL 3 st n = <* n1,n2,n3 *> &
u.3 = 1 holds |( n, u )| = n1 * u.1 + n2 * u.2 + n3
proof
let n1,n2,n3 be Element of F_Real;
let n,u be Element of TOP-REAL 3;
assume that
A1: n = <* n1,n2,n3 *> and
A2: u.3 = 1;
n = |[n`1,n`2,n`3]| by EUCLID_5:3;
then
A3: n`1 = n1 & n`2 = n2 & n`3 = n3 by A1,FINSEQ_1:78;
|( n, u )| = n1 * u`1 + n2 * u`2 + n3 * u`3 by A3,EUCLID_5:29
.= n1 * u.1 + n2 * u`2 + n3 * u`3 by EUCLID_5:def 1
.= n1 * u.1 + n2 * u.2 + n3 * u`3 by EUCLID_5:def 2
.= n1 * u.1 + n2 * u.2 + n3 * u.3 by EUCLID_5:def 3;
hence thesis by A2;
end;
theorem Th28:
for A being convex non empty Subset of TOP-REAL 3
for n,u,v being Element of TOP-REAL 3 st
(for w being Element of TOP-REAL 3 st w in A holds |( n,w )| <> 0) &
u in A & v in A holds 0 < |( n,u )| * |( n,v )|
proof
let A be convex non empty Subset of TOP-REAL 3;
let n,u,v be Element of TOP-REAL 3;
assume that
A1: for w be Element of TOP-REAL 3 st w in A holds |( n,w )| <> 0 and
A2: u in A & v in A;
set x = |( n,u )|,
y = |( n,v )|;
assume
A3: not 0 < |( n,u )| * |( n,v)|;
A4: x <> 0 & y <> 0 by A1,A2;
then
A5: 0 < x / (x - y) < 1 by A3,BKMODEL3:1;
reconsider l = x / (x - y) as non zero Real by A3,A4,BKMODEL3:1;
reconsider w = l * v + (1 - l) * u as Element of TOP-REAL 3;
x <> y
proof
assume x = y;
then l = 0 by XCMPLX_1:49;
hence contradiction;
end;
then
A6: 1 - l = - y / (x - y) by Th25;
|( n,w )| = 0
proof
|( n , w )| = |( n, l * v )| + |( n, (1 - l) * u)| by EUCLID_2:26
.= l * |(n , v)| + |( n, (1 - l) * u)| by EUCLID_2:19
.= x / (x - y) * y + (-y) / (x - y) * x by A6,EUCLID_2:19;
hence thesis;
end;
hence contradiction by A1,A2,A5,CONVEX1:def 2;
end;
theorem Th29:
for n31,n32,n33 being Element of F_Real
for u,v being Element of TOP-REAL 2 st u in inside_of_circle(0,0,1) &
v in inside_of_circle(0,0,1) &
(for w being Element of TOP-REAL 2 st w in inside_of_circle(0,0,1) holds
n31 * w.1 + n32 * w.2 + n33 <> 0) holds
0 < (n31 * u.1 + n32 * u.2 + n33) * (n31 * v.1 + n32 * v.2 + n33)
proof
let n31,n32,n33 be Element of F_Real;
let u,v be Element of TOP-REAL 2;
assume that
A1: u in inside_of_circle(0,0,1) and
A2: v in inside_of_circle(0,0,1) and
A3: for w be Element of TOP-REAL 2 st w in inside_of_circle(0,0,1) holds
n31 * w.1 + n32 * w.2 + n33 <> 0;
set B = inside_of_circle(0,0,1);
set A = {x where x is Element of TOP-REAL 3:|[x`1,x`2]| in B & x`3 = 1};
A c= the carrier of TOP-REAL 3
proof
let x be object;
assume x in A;
then ex y be Element of TOP-REAL 3 st x= y & |[y`1,y`2]| in B & y`3 = 1;
hence thesis;
end;
then reconsider A as Subset of TOP-REAL 3;
reconsider A as non empty convex Subset of TOP-REAL 3 by Th26;
reconsider n = |[ n31,n32,n33 ]|, u9 = |[u.1,u.2,1]|,v9 = |[v.1,v.2,1]|
as Element of TOP-REAL 3;
A4: |[u`1,u`2]| in B & |[v`1,v`2]| in B by A1,A2,EUCLID:53;
A5: u9`1 = u.1 & u9`2 = u.2 & u9`3 = 1 &
v9`1 = v.1 & v9`2 = v.2 & v9`3 = 1 by EUCLID_5:2;
A6: u9 in A & v9 in A by A5,A4;
A7:
now
let w be Element of TOP-REAL 3;
assume w in A;
then consider x be Element of TOP-REAL 3 such that
A8: w = x and
A9: |[x`1,x`2]| in B and
A10: x`3 = 1;
reconsider v = |[x`1,x`2]| as Element of TOP-REAL 2;
now
w.3 = 1 by A8,A10,EUCLID_5:def 3;
hence |(n,w)| = n31 * w.1 + n32 * w.2 + n33 by Th27;
thus w.1 = w`1 by EUCLID_5:def 1
.= v`1 by A8,EUCLID:52
.= v.1;
thus w.2 = w`2 by EUCLID_5:def 2
.= v`2 by A8,EUCLID:52
.= v.2;
end;
hence |(n,w)| <> 0 by A3,A9;
end;
now
n = <*n31,n32,n33*> & u9.3 = 1 by A5,EUCLID_5:def 3;
then |(n,u9)| = n31 * u9.1 + n32 * u9.2 + n33 by Th27;
then |(n,u9)| = n31 * u9`1 + n32 * u9.2 + n33 by EUCLID_5:def 1;
hence |(n,u9)| = n31 * u.1 + n32 * u.2 + n33 by A5,EUCLID_5:def 2;
n = <*n31,n32,n33*> & v9.3 = 1 by A5,EUCLID_5:def 3;
then |(n,v9)| = n31 * v9.1 + n32 * v9.2 + n33 by Th27;
then |(n,v9)| = n31 * v9`1 + n32 * v9.2 + n33 by EUCLID_5:def 1;
hence |(n,v9)| = n31 * v.1 + n32 * v.2 + n33 by A5,EUCLID_5:def 2;
end;
hence thesis by A7,A6,Th28;
end;
theorem Th30:
for n31,n32,n33 being Element of F_Real
for u,v being Element of TOP-REAL 2 st u in inside_of_circle(0,0,1) &
v in circle(0,0,1) &
(for w be Element of TOP-REAL 2 st w in closed_inside_of_circle(0,0,1) holds
n31 * w.1 + n32 * w.2 + n33 <> 0) holds
0 < (n31 * u.1 + n32 * u.2 + n33) * (n31 * v.1 + n32 * v.2 + n33)
proof
let n31,n32,n33 be Element of F_Real;
let u,v be Element of TOP-REAL 2;
assume that
A1: u in inside_of_circle(0,0,1) and
A2: v in circle(0,0,1) and
A3: for w be Element of TOP-REAL 2 st w in closed_inside_of_circle(0,0,1) holds
n31 * w.1 + n32 * w.2 + n33 <> 0;
set B = closed_inside_of_circle(0,0,1);
set A = {x where x is Element of TOP-REAL 3:|[x`1,x`2]| in B & x`3 = 1};
A c= the carrier of TOP-REAL 3
proof
let x be object;
assume x in A;
then ex y be Element of TOP-REAL 3 st x = y & |[y`1,y`2]| in B & y`3 = 1;
hence thesis;
end;
then reconsider A as Subset of TOP-REAL 3;
reconsider A as non empty convex Subset of TOP-REAL 3 by Th26;
reconsider n = |[ n31,n32,n33 ]|,
u9 = |[u.1,u.2,1]|,v9 = |[v.1,v.2,1]| as Element of TOP-REAL 3;
inside_of_circle(0,0,1) c= closed_inside_of_circle(0,0,1) &
circle(0,0,1) c= closed_inside_of_circle(0,0,1) by TOPREAL9:46,53;
then u in B & v in B by A1,A2;
then
A4: |[u`1,u`2]| in B & |[v`1,v`2]| in B by EUCLID:53;
A5: u9`1 = u.1 & u9`2 = u.2 & u9`3 = 1 &
v9`1 = v.1 & v9`2 = v.2 & v9`3 = 1 by EUCLID_5:2;
A6: u9 in A & v9 in A by A5,A4;
A7:
now
let w be Element of TOP-REAL 3;
assume w in A;
then consider x be Element of TOP-REAL 3 such that
A8: w = x and
A9: |[x`1,x`2]| in B and
A10: x`3 = 1;
reconsider v = |[x`1,x`2]| as Element of TOP-REAL 2;
now
w.3 = 1 by A8,A10,EUCLID_5:def 3;
hence |(n,w)| = n31 * w.1 + n32 * w.2 + n33 by Th27;
thus w.1 = w`1 by EUCLID_5:def 1
.= v`1 by A8,EUCLID:52
.= v.1;
thus w.2 = w`2 by EUCLID_5:def 2
.= v`2 by A8,EUCLID:52
.= v.2;
end;
hence |(n,w)| <> 0 by A3,A9;
end;
now
n = <*n31,n32,n33*> & u9.3 = 1 by A5,EUCLID_5:def 3;
then |(n,u9)| = n31 * u9.1 + n32 * u9.2 + n33 by Th27;
then |(n,u9)| = n31 * u9`1 + n32 * u9.2 + n33 by EUCLID_5:def 1;
hence |(n,u9)| = n31 * u.1 + n32 * u.2 + n33 by A5,EUCLID_5:def 2;
n = <*n31,n32,n33*> & v9.3 = 1 by A5,EUCLID_5:def 3;
then |(n,v9)| = n31 * v9.1 + n32 * v9.2 + n33 by Th27;
then |(n,v9)| = n31 * v9`1 + n32 * v9.2 + n33 by EUCLID_5:def 1;
hence |(n,v9)| = n31 * v.1 + n32 * v.2 + n33 by A5,EUCLID_5:def 2;
end;
hence thesis by A7,A6,Th28;
end;
theorem Th34:
for l,r being Real
for u,v,w being Element of TOP-REAL 3
for n11,n12,n13,n21,n22,n23,n31,n32,n33,nu1,nu2,nu3,nv1,
nv2,nv3,nw1,nw2,nw3 being Real st
nu3 <> 0 & nv3 <> 0 & nw3 <> 0 &
r = (l * nv3) / ((1 - l) * nu3 + l * nv3) &
(1 - l) * nu3 + l * nv3 <> 0 &
w = (1 - l) * u + l * v &
nu1 = n11 * u.1 + n12 * u.2 + n13 &
nu2 = n21 * u.1 + n22 * u.2 + n23 &
nu3 = n31 * u.1 + n32 * u.2 + n33 &
nv1 = n11 * v.1 + n12 * v.2 + n13 &
nv2 = n21 * v.1 + n22 * v.2 + n23 &
nv3 = n31 * v.1 + n32 * v.2 + n33 &
nw1 = n11 * w.1 + n12 * w.2 + n13 &
nw2 = n21 * w.1 + n22 * w.2 + n23 &
nw3 = n31 * w.1 + n32 * w.2 + n33 holds
(1 - r) * |[nu1 / nu3,nu2 / nu3,1]| + r * |[nv1 / nv3,nv2 / nv3,1]|
= |[nw1 / nw3,nw2 / nw3,1]|
proof
let l,r be Real;
let u,v,w be Element of TOP-REAL 3;
let n11,n12,n13,n21,n22,n23,n31,n32,n33,nu1,nu2,nu3,nv1,nv2,nv3,
nw1,nw2,nw3 be Real;
assume
A1: nu3 <> 0 & nv3 <> 0 & nw3 <> 0 &
r = (l * nv3) / ((1 - l) * nu3 + l * nv3) &
(1 - l) * nu3 + l * nv3 <> 0 &
w = (1 - l) * u + l * v &
nu1 = n11 * u.1 + n12 * u.2 + n13 &
nu2 = n21 * u.1 + n22 * u.2 + n23 &
nu3 = n31 * u.1 + n32 * u.2 + n33 &
nv1 = n11 * v.1 + n12 * v.2 + n13 &
nv2 = n21 * v.1 + n22 * v.2 + n23 &
nv3 = n31 * v.1 + n32 * v.2 + n33 &
nw1 = n11 * w.1 + n12 * w.2 + n13 &
nw2 = n21 * w.1 + n22 * w.2 + n23 &
nw3 = n31 * w.1 + n32 * w.2 + n33;
reconsider lu = (1 - l) * u, lv = l * v as Element of TOP-REAL 3;
reconsider ru = (1 - l) * u, rv = l * v as Element of REAL 3 by EUCLID:22;
A2:
now
thus (lu + lv).1 = ru.1 + rv.1 by RVSUM_1:11
.= lu.1 + lv.1;
thus (lu + lv).2 = ru.2 + rv.2 by RVSUM_1:11
.= lu.2 + lv.2;
thus (lu + lv).3 = ru.3 + rv.3 by RVSUM_1:11
.= lu.3 + lv.3;
end;
A3:
now
thus w.1 = (1-l) * u.1 + (l * v).1 by A1,A2,RVSUM_1:44
.= (1-l) * u.1 + l * v.1 by RVSUM_1:44;
thus w.2 = (1-l) * u.2 + (l * v).2 by A1,A2,RVSUM_1:44
.= (1-l) * u.2 + l * v.2 by RVSUM_1:44;
thus w.3 = (1-l) * u.3 + (l * v).3 by A1,A2,RVSUM_1:44
.= (1-l) * u.3 + l * v.3 by RVSUM_1:44;
end;
A4:
now
now
thus (1 - r) * nu1 / nu3 = ((1 - l) * nu3 /
((1 - l) * nu3 + l * nv3)) *
nu1 / nu3 by A1,Th32
.= (1 - l) * nu1 / ((1 - l) * nu3 + l * nv3)
by A1,Th33;
thus r * nv1 / nv3 = l * nv1 / ((1 - l) * nu3 + l * nv3) by A1,Th33;
end;
hence (1 - r) * nu1 / nu3 + r * nv1 / nv3 = ((1 - l) * nu1 + l * nv1) /
((1 - l) * nu3 + l * nv3)
.= nw1 / nw3 by A1,A3;
now
thus (1 - r) * nu2 / nu3 = ((1 - l) * nu3 /
((1 - l) * nu3 + l * nv3)) *
nu2 / nu3 by A1,Th32
.= (1 - l) * nu2 / ((1 - l) * nu3 + l * nv3)
by A1,Th33;
thus r * nv2 / nv3 = l * nv2 / ((1 - l) * nu3 + l * nv3) by A1,Th33;
end;
hence (1 - r) * nu2 / nu3 + r * nv2 / nv3
= ((1 - l) * nu2 + l * nv2) / ((1 - l) * nu3 + l * nv3)
.= nw2 / nw3 by A1,A3;
end;
(1 - r) * |[nu1 / nu3,nu2 / nu3,1]| + r * |[nv1 / nv3,nv2 / nv3,1]|
= |[ (1 - r) * (nu1 / nu3), (1 - r) * (nu2 / nu3), (1 - r) * 1 ]| +
r * |[nv1 / nv3,nv2 / nv3,1]| by EUCLID_5:8
.= |[ (1 - r) * nu1 / nu3, (1 - r) * nu2 / nu3, 1 - r ]|
+ |[r * (nv1 / nv3),r * (nv2 / nv3),r * 1]| by EUCLID_5:8
.= |[ (1 - r) * nu1 / nu3 + r * nv1 / nv3, (1 - r) * nu2 / nu3 +
r * nv2 / nv3 , 1 - r + r]| by EUCLID_5:6
.= |[ nw1 / nw3, nw2 / nw3, 1]| by A4;
hence thesis;
end;
theorem
for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry
for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
for P being Element of BK_model st h = homography(N) &
N = <* <* n11,n12,n13 *>, <* n21,n22,n23 *>, <* n31,n32,n33 *> *>
holds homography(N).P = Dir |[
(n11 * (BK_to_REAL2 P)`1 + n12 * (BK_to_REAL2 P)`2 + n13) /
(n31 * (BK_to_REAL2 P)`1 + n32 * (BK_to_REAL2 P)`2 + n33),
(n21 * (BK_to_REAL2 P)`1 + n22 * (BK_to_REAL2 P)`2 + n23) /
(n31 * (BK_to_REAL2 P)`1 + n32 * (BK_to_REAL2 P)`2 + n33),1 ]|
proof
let N be invertible Matrix of 3,F_Real;
let h be Element of SubGroupK-isometry;
let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
let P be Element of BK_model;
assume
A1: h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *>;
consider u be non zero Element of TOP-REAL 3 such that
A2: P = Dir u & u.3 = 1 & BK_to_REAL2 P = |[u.1,u.2]| by BKMODEL2:def 2;
(BK_to_REAL2 P)`1 = u.1 & (BK_to_REAL2 P)`2 = u.2 &
homography(N).P = Dir |[(n11 * u.1 + n12 * u.2 + n13) /
(n31 * u.1 + n32 * u.2 + n33),
(n21 * u.1 + n22 * u.2 + n23)
/ (n31 * u.1 + n32 * u.2 + n33),1 ]|
by A1,A2,Th23,EUCLID:52;
hence thesis;
end;
theorem Th36:
for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real
for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
for u2 being Element of TOP-REAL 2
st h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
u2 in inside_of_circle(0,0,1) holds n31 * u2.1 + n32 * u2.2 + n33 <> 0
proof
let h be Element of SubGroupK-isometry;
let N be invertible Matrix of 3,F_Real;
let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
let u2 be Element of TOP-REAL 2;
assume that
A1: h = homography(N) and
A2: N = <* <* n11,n12,n13 *>, <* n21,n22,n23 *>, <* n31,n32,n33 *> *> and
A3: u2 in inside_of_circle(0,0,1);
reconsider uic = u2 as Element of inside_of_circle(0,0,1) by A3;
consider Q be Element of TOP-REAL 2 such that
A4: Q = uic & REAL2_to_BK uic = Dir |[Q`1,Q`2,1]| by BKMODEL2:def 3;
reconsider P = REAL2_to_BK uic as Element of BK_model;
reconsider v = |[Q`1,Q`2,1]| as non zero Element of TOP-REAL 3;
A5: v.1 = v`1 by EUCLID_5:def 1
.= u2.1 by A4,EUCLID_5:2;
A6: v.2 = v`2 by EUCLID_5:def 2
.= u2.2 by A4,EUCLID_5:2;
now
thus P = Dir v by A4;
thus v.3 = v`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
end;
hence thesis by A5,A6,A1,A2,Th20;
end;
Lem01:
0^2 + 0^2 = 0
proof
0^2 + 0^2 = 0 * 0 + 0^2 by SQUARE_1:def 1
.= 0 * 0 by SQUARE_1:def 1;
hence thesis;
end;
theorem Th37:
for r being positive Real
for u being Element of TOP-REAL 2 st u in circle(0,0,r)
holds u is non zero
proof
let r be positive Real;
let u be Element of TOP-REAL 2;
assume
A1: u in circle(0,0,r);
assume u is zero;
then r^2 = 0 by A1,BKMODEL1:14,EUCLID:54,Lem01;
hence contradiction;
end;
theorem Th38:
for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real
for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
for u2 being Element of TOP-REAL 2
st h = homography(N) & N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> &
u2 in closed_inside_of_circle(0,0,1) holds n31 * u2.1 + n32 * u2.2 + n33 <> 0
proof
let h be Element of SubGroupK-isometry;
let N be invertible Matrix of 3,F_Real;
let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
let u2 be Element of TOP-REAL 2;
assume that
A1: h = homography(N) and
A2: N = <* <* n11,n12,n13 *>, <* n21,n22,n23 *>, <* n31,n32,n33 *> *> and
A3: u2 in closed_inside_of_circle(0,0,1);
u2 in inside_of_circle(0,0,1) \/ circle(0,0,1) by A3,TOPREAL9:55;
then per cases by XBOOLE_0:def 3;
suppose
u2 in inside_of_circle(0,0,1);
then reconsider uic = u2 as Element of inside_of_circle(0,0,1);
consider Q be Element of TOP-REAL 2 such that
A4: Q = uic & REAL2_to_BK uic = Dir |[Q`1,Q`2,1]| by BKMODEL2:def 3;
reconsider P = REAL2_to_BK uic as Element of BK_model;
reconsider v = |[Q`1,Q`2,1]| as non zero Element of TOP-REAL 3;
A5: v.1 = v`1 by EUCLID_5:def 1
.= u2.1 by A4,EUCLID_5:2;
A6: v.2 = v`2 by EUCLID_5:def 2
.= u2.2 by A4,EUCLID_5:2;
now
thus P = Dir v by A4;
thus v.3 = v`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
end;
hence thesis by A5,A6,A1,A2,Th20;
end;
suppose
A7: u2 in circle(0,0,1);
then reconsider u2 as non zero Element of TOP-REAL 2 by Th37;
reconsider P = REAL2_to_absolute u2 as Element of absolute;
reconsider v = |[u2.1,u2.2,1]| as non zero Element of TOP-REAL 3;
A8: v.1 = v`1 by EUCLID_5:def 1
.= u2.1 by EUCLID_5:2;
A9: v.2 = v`2 by EUCLID_5:def 2
.= u2.2 by EUCLID_5:2;
now
thus P is Element of absolute;
thus P = Dir v by A7,BKMODEL1:def 9;
thus v.3 = v`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
end;
hence thesis by A8,A9,A1,A2,Th22;
end;
end;
theorem Th39:
for a,b,c,d,e,f,r being Real st
(1 - r) * |[a,b,1]| + r * |[c,d,1]| = |[e,f,1]| holds
(1 - r) * |[a,b]| + r * |[c,d]| = |[e,f]|
proof
let a,b,c,d,e,f,r be Real;
assume (1 - r) * |[a,b,1]| + r * |[c,d,1]| = |[e,f,1]|;
then |[e,f,1]|=|[(1 - r) * a,(1 - r) * b,(1 - r) * 1]| + r * |[c,d,1]|
by EUCLID_5:8
.=|[(1 - r) * a,(1 - r) * b,(1 - r)]|
+ |[r * c,r * d,r * 1]| by EUCLID_5:8
.=|[(1 - r) * a + r * c,(1 - r) * b + r * d,1 - r + r]|
by EUCLID_5:6;
then e = (1 - r) * a + r * c & f = (1 - r) * b + r * d by FINSEQ_1:78;
then |[e,f]| = |[ (1 - r) * a, (1 - r) * b ]| + |[ r * c,r * d]|
by EUCLID:56
.= (1 - r) * |[a,b]| + |[r * c,r * d]| by EUCLID:58
.= (1 - r) * |[a,b]| + r * |[c,d]| by EUCLID:58;
hence thesis;
end;
theorem
for P,Q,R,P9,Q9,R9 being POINT of BK-model-Plane
for p,q,r,p9,q9,r9 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) &
between P,Q,R & P = p & Q = q & R = r & p9 = homography(N).p &
q9 = homography(N).q & r9 = homography(N).r &
P9 = p9 & Q9 = q9 & R9 = r9 holds between P9,Q9,R9
proof
let P,Q,R,P9,Q9,R9 be POINT of BK-model-Plane;
let p,q,r,p9,q9,r9 be Element of BK_model;
let h be Element of SubGroupK-isometry;
let N be invertible Matrix of 3,F_Real;
assume that
A1: h = homography(N) and
A2: between P,Q,R and
A3: P = p and
A4: Q = q and
A5: R = r and
A6: p9 = homography(N).p and
A7: q9 = homography(N).q and
A8: r9 = homography(N).r and
A9: P9 = p9 and
A10: Q9 = q9 and
A11: R9 = r9;
consider n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real such that
A12: N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> by PASCAL:3;
consider u be non zero Element of TOP-REAL 3 such that
A13: Dir u = p & u.3 = 1 & BK_to_REAL2 p = |[u.1,u.2]| by BKMODEL2:def 2;
consider v be non zero Element of TOP-REAL 3 such that
A14: Dir v = r & v.3 = 1 & BK_to_REAL2 r = |[v.1,v.2]| by BKMODEL2:def 2;
consider w be non zero Element of TOP-REAL 3 such that
A15: Dir w = q & w.3 = 1 & BK_to_REAL2 q = |[w.1,w.2]| by BKMODEL2:def 2;
reconsider nu1 = n11 * u.1 + n12 * u.2 + n13,
nu2 = n21 * u.1 + n22 * u.2 + n23,
nu3 = n31 * u.1 + n32 * u.2 + n33,
nv1 = n11 * v.1 + n12 * v.2 + n13,
nv2 = n21 * v.1 + n22 * v.2 + n23,
nv3 = n31 * v.1 + n32 * v.2 + n33,
nw1 = n11 * w.1 + n12 * w.2 + n13,
nw2 = n21 * w.1 + n22 * w.2 + n23,
nw3 = n31 * w.1 + n32 * w.2 + n33 as Real;
A16: BK_to_T2 P = BK_to_REAL2 p & Tn2TR BK_to_T2 P = BK_to_REAL2 p &
BK_to_T2 Q = BK_to_REAL2 q & Tn2TR BK_to_T2 Q = BK_to_REAL2 q &
BK_to_T2 R = BK_to_REAL2 r & Tn2TR BK_to_T2 R = BK_to_REAL2 r
by A3,A4,A5,Th04;
then Tn2TR BK_to_T2 Q in LSeg(Tn2TR BK_to_T2 P,Tn2TR BK_to_T2 R)
by A2,A3,A4,A5,BKMODEL3:def 7;
then consider l be Real such that
A17: 0 <= l & l <= 1 and
A18: Tn2TR BK_to_T2 Q = (1 - l) * Tn2TR BK_to_T2 P + l * Tn2TR BK_to_T2 R
by RLTOPSP1:76;
|[w.1,w.2]| = |[ (1 - l) * u.1, (1 - l) * u.2 ]| + l * |[v.1,v.2]|
by A18,A16,A13,A14,A15,EUCLID:58
.= |[ (1 - l) * u.1, (1 - l) * u.2 ]| + |[l * v.1,l * v.2]|
by EUCLID:58
.= |[ (1 - l) * u.1 + l * v.1, (1 - l) * u.2 + l * v.2]|
by EUCLID:56;
then
A19: w.1 = (1 - l) * u.1 + l * v.1 &
w.2 = (1 - l) * u.2 + l * v.2 by FINSEQ_1:77;
set r = (l * nv3) / ((1 - l) * nu3 + l * nv3);
now
thus w = |[w`1,w`2,w`3]| by EUCLID_5:3
.= |[w.1,w`2,w`3]| by EUCLID_5:def 1
.= |[w.1,w.2,w`3]| by EUCLID_5:def 2
.= |[(1 - l) * u.1 + l * v.1, (1 - l) * u.2 + l * v.2,
(1 - l) * 1 + l * 1]| by A15,A19,EUCLID_5:def 3
.= |[(1 -l) * u.1,(1 - l) * u.2,(1 - l) * 1]| +
|[ l * v.1,l * v.2, l * 1]| by EUCLID_5:6
.= (1 - l) * |[u.1,u.2,1]| +
|[ l * v.1,l * v.2, l * 1]| by EUCLID_5:8
.= (1 - l) * |[u.1,u.2,1]| +
l * |[v.1,v.2, 1]| by EUCLID_5:8
.= (1 - l) * u + l * |[v.1,v.2,v.3]| by A13,A14,Th35
.= (1 - l) * u + l * v by Th35;
thus nu3 <> 0 by A1,A12,A13,Th20;
thus nv3 <> 0 by A1,A12,A14,Th20;
thus
A20: nw3 <> 0 by A1,A12,A15,Th20;
thus nw3 = (1 - l) * nu3 + l * nv3 by A19;
thus (1 - l) * nu3 + l * nv3 <> 0 by A19,A20;
end;
then
A21: (1 - r) * |[nu1 / nu3,nu2 / nu3,1]| + r * |[nv1 / nv3,nv2 / nv3,1]|
= |[nw1 / nw3,nw2 / nw3,1]| by Th34;
A22: 0 <= r <= 1
proof
now
thus 0 <= l <= 1 by A17;
thus 0 < nu3 * nv3
proof
reconsider u1 = |[u.1,u.2]|, v1 = |[v.1,v.2]| as
Element of TOP-REAL 2;
A23: u1.1 = u1`1 .= u.1 by EUCLID:52;
A24: u1.2 = u1`2 .= u.2 by EUCLID:52;
A25: v1.1 = v1`1 .= v.1 by EUCLID:52;
A26: v1.2 = v1`2 .= v.2 by EUCLID:52;
reconsider m31 = n31, m32 = n32, m33 = n33 as Element of F_Real;
u1 in inside_of_circle(0,0,1) &
v1 in inside_of_circle(0,0,1) &
for w1 be Element of TOP-REAL 2 st
w1 in inside_of_circle(0,0,1) holds
m31 * w1.1 + m32 * w1.2 + m33 <> 0 by A13,A14,A1,A12,Th36;
hence thesis by A23,A24,A25,A26,Th29;
end;
end;
hence thesis by Th31;
end;
A27: BK_to_T2 P9 = BK_to_REAL2 p9 &
Tn2TR BK_to_T2 P9 = BK_to_REAL2 p9 &
BK_to_T2 Q9 = BK_to_REAL2 q9 &
Tn2TR BK_to_T2 Q9 = BK_to_REAL2 q9 &
BK_to_T2 R9 = BK_to_REAL2 r9 &
Tn2TR BK_to_T2 R9 = BK_to_REAL2 r9
by A9,A10,A11,Th04;
now
thus 0 <= r <= 1 by A22;
thus Tn2TR BK_to_T2 Q9 = (1 - r) * Tn2TR BK_to_T2 P9
+ r * Tn2TR BK_to_T2 R9
proof
reconsider u2 = |[nu1/nu3,nu2/nu3,1]|
as non zero Element of TOP-REAL 3;
consider u3 be non zero Element of TOP-REAL 3 such that
A28: Dir u3 = p9 & u3.3 = 1 & BK_to_REAL2 p9 = |[u3.1,u3.2]|
by BKMODEL2:def 2;
now
thus Dir u3 = Dir u2 by A28,A6,A1,A12,A13,Th23;
thus u2.3 = u2`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
hence u2.3 = u3.3 by A28;
end;
then u2 = u3 by BKMODEL1:43;
then
A29: BK_to_REAL2 p9 = |[u2`1,u2.2]| by A28,EUCLID_5:def 1
.= |[u2`1,u2`2]| by EUCLID_5:def 2
.= |[nu1/nu3,u2`2]| by EUCLID_5:2
.= |[nu1/nu3,nu2/nu3]| by EUCLID_5:2;
reconsider v2 = |[nv1/nv3,nv2/nv3,1]| as
non zero Element of TOP-REAL 3;
consider v3 be non zero Element of TOP-REAL 3 such that
A30: Dir v3 = r9 & v3.3 = 1 & BK_to_REAL2 r9 = |[v3.1,v3.2]|
by BKMODEL2:def 2;
now
thus Dir v3 = Dir v2 by A30,A1,A12,A14,Th23,A8;
thus v2.3 = v2`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
hence v2.3 = v3.3 by A30;
end;
then v2 = v3 by BKMODEL1:43;
then
A31: BK_to_REAL2 r9 = |[v2`1,v2.2]| by A30,EUCLID_5:def 1
.= |[v2`1,v2`2]| by EUCLID_5:def 2
.= |[nv1/nv3,v2`2]| by EUCLID_5:2
.= |[nv1/nv3,nv2/nv3]| by EUCLID_5:2;
reconsider w2 = |[nw1/nw3,nw2/nw3,1]|
as non zero Element of TOP-REAL 3;
consider w3 be non zero Element of TOP-REAL 3 such that
A32: Dir w3 = q9 & w3.3 = 1 & BK_to_REAL2 q9 = |[w3.1,w3.2]|
by BKMODEL2:def 2;
now
thus Dir w3 = Dir w2 by A32,A1,A12,A15,Th23,A7;
thus w2.3 = w2`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
hence w2.3 = w3.3 by A32;
end;
then w2 = w3 by BKMODEL1:43;
then BK_to_REAL2 q9 = |[w2`1,w2.2]| by A32,EUCLID_5:def 1
.= |[w2`1,w2`2]| by EUCLID_5:def 2
.= |[nw1/nw3,w2`2]| by EUCLID_5:2
.= |[nw1/nw3,nw2/nw3]| by EUCLID_5:2;
hence thesis by A27,A29,A31,Th39,A21;
end;
end;
then Tn2TR BK_to_T2 Q9 in {(1 - r) * Tn2TR BK_to_T2 P9
+ r * Tn2TR BK_to_T2 R9 where r is Real:0 <= r & r <= 1};
then Tn2TR BK_to_T2 Q9 in LSeg(Tn2TR BK_to_T2 P9,Tn2TR BK_to_T2 R9)
by RLTOPSP1:def 2;
hence thesis by A27,A9,A10,A11,BKMODEL3:def 7;
end;
definition
let P be Point of ProjectiveSpace TOP-REAL 3;
attr P is point_at_infty means
:Def04:
ex u being non zero Element of TOP-REAL 3 st
P = Dir u & u`3 = 0;
end;
theorem Th40:
for P being Point of ProjectiveSpace TOP-REAL 3 st
ex u being non zero Element of TOP-REAL 3 st
P = Dir u & u`3 <> 0 holds P is non point_at_infty
proof
let P be Point of ProjectiveSpace TOP-REAL 3;
given u be non zero Element of TOP-REAL 3 such that
A1: P = Dir u and
A2: u`3 <> 0;
now
let v be non zero Element of TOP-REAL 3;
assume P = Dir v;
then are_Prop u,v by A1,ANPROJ_1:22;
then consider a be Real such that
A3: a <> 0 and
A4: v = a * u by ANPROJ_1:1;
v`3 = a * u`3 by A4,EUCLID_5:9;
hence v`3 <> 0 by A2,A3;
end;
hence thesis;
end;
registration
cluster point_at_infty for Point of ProjectiveSpace TOP-REAL 3;
existence
proof
reconsider u = |[1,0,0]| as non zero Element of TOP-REAL 3;
reconsider P = Dir u as Point of ProjectiveSpace TOP-REAL 3 by ANPROJ_1:26;
take P;
u`3 = 0 by EUCLID_5:2;
hence thesis;
end;
cluster non point_at_infty for Point of ProjectiveSpace TOP-REAL 3;
correctness
proof
reconsider u = |[0,0,1]| as non zero Element of TOP-REAL 3;
reconsider P = Dir u as Point of ProjectiveSpace TOP-REAL 3 by ANPROJ_1:26;
take P;
now
let v be non zero Element of TOP-REAL 3;
assume P = Dir v;
then are_Prop u,v by ANPROJ_1:22;
then consider a be Real such that
A1: a <> 0 and
A2: v = a * u by ANPROJ_1:1;
v`3 = a * u`3 by A2,EUCLID_5:9
.= a * 1 by EUCLID_5:2
.= a;
hence v`3 <> 0 by A1;
end;
hence thesis;
end;
end;
definition
let P being non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
func RP3_to_REAL2 P -> Element of REAL 2 means
:Def05:
ex u being non zero Element of TOP-REAL 3 st P = Dir u & u`3 = 1 &
it = |[u`1,u`2]|;
existence
proof
consider u be Element of TOP-REAL 3 such that
A1: u is not zero and
A2: P = Dir u by ANPROJ_1:26;
A3: P is non point_at_infty;
reconsider v = |[u`1/u`3,u`2/u`3,1]| as non zero Element of TOP-REAL 3;
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]| by A1,A2,A3,XCMPLX_1:87
.= |[u`1,u`2,u`3]| by A1,A2,A3,XCMPLX_1:87
.= u by EUCLID_5:3;
then are_Prop u,v by A1,A2,A3,ANPROJ_1:1;
then
A4: P = Dir v by A2,A1,ANPROJ_1:22;
A5: v`3 = 1 by EUCLID_5:2;
|[v`1,v`2]| is Element of REAL 2 by EUCLID:22;
hence thesis by A4,A5;
end;
uniqueness
proof
let u,v be Element of REAL 2 such that
A6: ex w be non zero Element of TOP-REAL 3 st P = Dir w & w`3 = 1 &
u = |[w`1,w`2]| and
A7: ex w be non zero Element of TOP-REAL 3 st P = Dir w & w`3 = 1 &
v = |[w`1,w`2]|;
consider w1 be non zero Element of TOP-REAL 3 such that
A8: P = Dir w1 & w1`3 = 1 & u = |[w1`1,w1`2]| by A6;
consider w2 be non zero Element of TOP-REAL 3 such that
A9: P = Dir w2 & w2`3 = 1 & v = |[w2`1,w2`2]| by A7;
are_Prop w1,w2 by A8,A9,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A10: w1 = a * w2 by ANPROJ_1:1;
1 = a * w2`3 by A8,A10,EUCLID_5:9
.= a by A9;
then w1 = |[ 1 * w2`1,1 * w2`2,1 * w2`3]| by A10,EUCLID_5:7
.= w2 by EUCLID_5:3;
hence thesis by A8,A9;
end;
end;
definition
let P be non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
func RP3_to_T2 P -> Point of TarskiEuclid2Space equals
RP3_to_REAL2 P;
coherence
proof
the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
by GTARSKI1:def 13;
hence thesis;
end;
end;
theorem Th41:
for P,Q,R,P9,Q9,R9 being
non point_at_infty Element of ProjectiveSpace TOP-REAL 3
for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography(N) &
P in BK_model & Q in BK_model & R in absolute &
P9 = homography(N).P & Q9 = homography(N).Q & R9 = homography(N).R &
between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R holds
between RP3_to_T2 P9,RP3_to_T2 Q9,RP3_to_T2 R9
proof
let P,Q,R,P9,Q9,R9 be
non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
let h be Element of SubGroupK-isometry;
let N be invertible Matrix of 3,F_Real;
assume that
A1: h = homography(N) and
A2: P in BK_model and
A3: Q in BK_model and
A4: R in absolute and
A5: P9 = homography(N).P and
A6: Q9 = homography(N).Q and
A7: R9 = homography(N).R and
A8: between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R;
consider n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real such that
A9: N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> by PASCAL:3;
consider u be non zero Element of TOP-REAL 3 such that
A10: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
A11: |[u`1,u`2]| = |[u.1,u`2]| by EUCLID_5:def 1
.= |[u.1,u.2]| by EUCLID_5:def 2;
then
A12: P = Dir u & u.3 = 1 & RP3_to_REAL2 P = |[u.1,u.2]| by A10,EUCLID_5:def 3;
consider v be non zero Element of TOP-REAL 3 such that
A13: R = Dir v & v`3 = 1 & RP3_to_REAL2 R = |[v`1,v`2]| by Def05;
A14: |[v`1,v`2]| = |[v.1,v`2]| by EUCLID_5:def 1
.= |[v.1,v.2]| by EUCLID_5:def 2;
then
A15: R = Dir v & v.3 = 1 & RP3_to_REAL2 R = |[v.1,v.2]| by A13,EUCLID_5:def 3;
consider w be non zero Element of TOP-REAL 3 such that
A16: Q = Dir w & w`3 = 1 & RP3_to_REAL2 Q = |[w`1,w`2]| by Def05;
A17: |[w`1,w`2]| = |[w.1,w`2]| by EUCLID_5:def 1
.= |[w.1,w.2]| by EUCLID_5:def 2;
then
A18: Q = Dir w & w.3 = 1 & RP3_to_REAL2 Q = |[w.1,w.2]| by A16,EUCLID_5:def 3;
reconsider nu1 = n11 * u.1 + n12 * u.2 + n13,
nu2 = n21 * u.1 + n22 * u.2 + n23, nu3 = n31 * u.1 + n32 * u.2 + n33,
nv1 = n11 * v.1 + n12 * v.2 + n13, nv2 = n21 * v.1 + n22 * v.2 + n23,
nv3 = n31 * v.1 + n32 * v.2 + n33, nw1 = n11 * w.1 + n12 * w.2 + n13,
nw2 = n21 * w.1 + n22 * w.2 + n23, nw3 = n31 * w.1 + n32 * w.2 + n33
as Real;
Tn2TR RP3_to_T2 Q in LSeg(Tn2TR RP3_to_T2 P,Tn2TR RP3_to_T2 R)
by A8,GTARSKI2:20;
then consider l be Real such that
A19: 0 <= l & l <= 1 and
A20: Tn2TR RP3_to_T2 Q = (1 - l) * Tn2TR RP3_to_T2 P + l * Tn2TR RP3_to_T2 R
by RLTOPSP1:76;
|[w.1,w.2]| = |[ (1 - l) * u.1, (1 - l) * u.2 ]| + l * |[v.1,v.2]|
by A20,A11,A10,A14,A17,A16,A13,EUCLID:58
.= |[ (1 - l) * u.1, (1 - l) * u.2 ]| + |[l * v.1,l * v.2]|
by EUCLID:58
.= |[ (1 - l) * u.1 + l * v.1, (1 - l) * u.2 + l * v.2]|
by EUCLID:56;
then
A21: w.1 = (1 - l) * u.1 + l * v.1 & w.2 = (1 - l) * u.2 + l * v.2
by FINSEQ_1:77;
set r = (l * nv3) / ((1 - l) * nu3 + l * nv3);
now
thus w = |[w`1,w`2,w`3]| by EUCLID_5:3
.= |[w.1,w`2,w`3]| by EUCLID_5:def 1
.= |[(1 - l) * u.1 + l * v.1, (1 - l) * u.2 + l * v.2,
(1 - l) * 1 + l * 1]| by A16,A21,EUCLID_5:def 2
.= |[(1 -l) * u.1,(1 - l) * u.2,(1 - l) * 1]| +
|[ l * v.1,l * v.2, l * 1]| by EUCLID_5:6
.= (1 - l) * |[u.1,u.2,1]| +
|[ l * v.1,l * v.2, l * 1]| by EUCLID_5:8
.= (1 - l) * |[u.1,u.2,1]| +
l * |[v.1,v.2, 1]| by EUCLID_5:8
.= (1 - l) * u + l * |[v.1,v.2,v.3]| by A12,A15,Th35
.= (1 - l) * u + l * v by Th35;
thus nu3 <> 0 by A1,A2,A9,A12,Th20;
thus nv3 <> 0 by A1,A4,A9,A15,Th22;
thus
A22: nw3 <> 0 by A3,A1,A9,A18,Th20;
thus nw3 = (1 - l) * nu3 + l * nv3 by A21;
thus (1 - l) * nu3 + l * nv3 <> 0 by A22,A21;
end;
then
A23: (1 - r) * |[nu1 / nu3,nu2 / nu3,1]|
+ r * |[nv1 / nv3,nv2 / nv3,1]|
= |[nw1 / nw3,nw2 / nw3,1]| by Th34;
A24: 0 <= r <= 1
proof
now
thus 0 <= l <= 1 by A19;
thus 0 < nu3 * nv3
proof
reconsider u1 = |[u.1,u.2]|, v1 = |[v.1,v.2]| as
Element of TOP-REAL 2;
A25: u1.1 = u1`1 .= u.1 by EUCLID:52;
A26: u1.2 = u1`2 .= u.2 by EUCLID:52;
A27: v1.1 = v1`1 .= v.1 by EUCLID:52;
A28: v1.2 = v1`2 .= v.2 by EUCLID:52;
reconsider m31 = n31, m32 = n32, m33 = n33 as Element of F_Real;
now
reconsider PP = P as Element of BK_model by A2;
consider u3 be non zero Element of TOP-REAL 3 such that
A29: Dir u3 = PP & u3.3 = 1 & BK_to_REAL2 PP = |[u3.1,u3.2]|
by BKMODEL2:def 2;
u3 = u by A12,A29,Th16;
hence u1 in inside_of_circle(0,0,1) by A29;
thus v1 in circle(0,0,1) by A4,A15,BKMODEL1:84;
thus for w1 be Element of TOP-REAL 2 st
w1 in closed_inside_of_circle(0,0,1) holds
m31 * w1.1 + m32 * w1.2 + m33 <> 0 by A1,A9,Th38;
end;
hence thesis by A25,A26,A27,A28,Th30;
end;
end;
hence thesis by Th31;
end;
now
thus 0 <= r <= 1 by A24;
thus Tn2TR RP3_to_T2 Q9 = (1 - r) * Tn2TR RP3_to_T2 P9
+ r * Tn2TR RP3_to_T2 R9
proof
reconsider u2 = |[nu1/nu3,nu2/nu3,1]| as
non zero Element of TOP-REAL 3;
reconsider PP9 = P9 as
non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
consider u3 be non zero Element of TOP-REAL 3 such that
A30: PP9 = Dir u3 & u3`3 = 1 & RP3_to_REAL2 PP9 = |[u3`1,u3`2]| by Def05;
now
thus Dir u3 = Dir u2 by A1,A2,A9,A12,Th23,A5,A30;
thus u2.3 = u2`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
hence u2.3 = u3.3 by A30,EUCLID_5:def 3;
end;
then u2 = u3 by BKMODEL1:43;
then
A31: RP3_to_REAL2 P9 = |[nu1/nu3,u2`2]| by A30,EUCLID_5:2
.= |[nu1/nu3,nu2/nu3]| by EUCLID_5:2;
reconsider v2 = |[nv1/nv3,nv2/nv3,1]| as
non zero Element of TOP-REAL 3;
consider v3 be non zero Element of TOP-REAL 3 such that
A32: Dir v3= R9 & v3`3 = 1 & RP3_to_REAL2 R9 = |[v3`1,v3`2]| by Def05;
now
thus Dir v3 = Dir v2 by A15,A1,A4,A9,Th24,A7,A32;
thus v2.3 = v2`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
hence v2.3 = v3.3 by A32,EUCLID_5:def 3;
end;
then v2 = v3 by BKMODEL1:43;
then
A33: RP3_to_REAL2 R9 = |[nv1/nv3,v2`2]| by A32,EUCLID_5:2
.= |[nv1/nv3,nv2/nv3]| by EUCLID_5:2;
reconsider w2 = |[nw1/nw3,nw2/nw3,1]| as
non zero Element of TOP-REAL 3;
consider w3 be non zero Element of TOP-REAL 3 such that
A34: Dir w3= Q9 & w3`3 = 1 & RP3_to_REAL2 Q9 = |[w3`1,w3`2]| by Def05;
now
thus Dir w3 = Dir w2 by A3,A1,A9,A18,Th23,A6,A34;
thus w2.3 = w2`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
hence w2.3 = w3.3 by A34,EUCLID_5:def 3;
end;
then w2 = w3 by BKMODEL1:43;
then
A35: RP3_to_REAL2 Q9 = |[nw1/nw3,w2`2]| by A34,EUCLID_5:2
.= |[nw1/nw3,nw2/nw3]| by EUCLID_5:2;
RP3_to_REAL2 Q9 = (1 - r) * RP3_to_REAL2 P9 + r * RP3_to_REAL2 R9
proof
reconsider a = nu1/nu3, b = nu2/nu3, c = nv1/nv3, d = nv2/nv3,
e = nw1/nw3, f = nw2/nw3 as Real;
(1-r) * |[a,b]| + r * |[c,d]| = |[e,f]| by Th39,A23;
hence thesis by A31,A33,A35;
end;
hence thesis;
end;
end;
then Tn2TR RP3_to_T2 Q9 in {(1 - r) * Tn2TR RP3_to_T2 P9
+ r * Tn2TR RP3_to_T2 R9 where r is Real:0 <= r & r <= 1};
then Tn2TR RP3_to_T2 Q9 in LSeg(Tn2TR RP3_to_T2 P9,Tn2TR RP3_to_T2 R9)
by RLTOPSP1:def 2;
hence thesis by GTARSKI2:20;
end;
theorem Th42:
for a,b,c being Real
for u,v,w being Element of TOP-REAL 3
st a <> 0 & a + b + c = 0 &
a * u + b * v + c * w = 0.TOP-REAL 3 holds
u in Line(v,w)
proof
let a,b,c be Real;
let u,v,w be Element of TOP-REAL 3;
assume that
A1: a <> 0 and
A2: a + b + c = 0 and
A3: a * u + b * v + c * w = 0.TOP-REAL 3;
A4: u = ((-b)/a) * v + ((-c)/a) * w by A1,A3,ANPROJ_8:12;
reconsider r = (-c) / a as Real;
(1 - r) = a / a + c / a by A1,XCMPLX_1:60
.= (a + c) / a
.= (-b) / a by A2;
then u in the set of all (1 - r) * v + r * w where r is Real by A4;
hence thesis by RLTOPSP1:def 14;
end;
theorem Th43:
for P,Q,R being non point_at_infty Point of ProjectiveSpace TOP-REAL 3
for u,v,w being non zero Element of TOP-REAL 3 st
P = Dir u & Q = Dir v & R = Dir w &
u`3 = 1 & v`3 = 1 & w`3 = 1 holds
P,Q,R are_collinear iff u,v,w are_collinear
proof
let P,Q,R be non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
let u,v,w be non zero Element of TOP-REAL 3;
assume that
A1: P = Dir u & Q = Dir v & R = Dir w and
A2: u`3 = 1 & v`3 = 1 & w`3 = 1;
reconsider i = 3 as Nat;
hereby
assume P,Q,R are_collinear;
then consider u9,v9,w9 be Element of TOP-REAL 3 such that
A3: P = Dir u9 & Q = Dir v9 & R = Dir w9 &
u9 is not zero & v9 is not zero & w9 is not zero and
A4: ex a,b,c be Real st a*u9+b*v9+c*w9=0.TOP-REAL 3 &
(a <> 0 or b <> 0 or c <> 0) by ANPROJ_8:11;
A5: |{u9,v9,w9}| = 0 by A4,ANPROJ_8:41;
are_Prop u,u9 by A1,A3,ANPROJ_1:22;
then consider a be Real such that
A6: a <> 0 and
A7: u9 = a * u by ANPROJ_1:1;
are_Prop v,v9 by A1,A3,ANPROJ_1:22;
then consider b be Real such that
A8: b <> 0 and
A9: v9 = b * v by ANPROJ_1:1;
are_Prop w,w9 by A1,A3,ANPROJ_1:22;
then consider c be Real such that
A10: c <> 0 and
A11: w9 = c * w by ANPROJ_1:1;
reconsider d = a * (b * c) as non zero Real by A6,A8,A10;
0 = a * |{u,b * v,c * w}| by ANPROJ_8:31,A5,A7,A9,A11
.= a * (b * |{u,v,c * w}|) by ANPROJ_8:32
.= a * (b * (c * |{u,v,w}|)) by ANPROJ_8:33
.= d * |{u,v,w}|;
then |{u,v,w}| = 0;
then consider a,b,c be Real such that
A12: a * u + b * v + c * w = 0.TOP-REAL 3 and
A13: a <> 0 or b <> 0 or c <> 0 by ANPROJ_8:43,ANPROJ_1:def 2;
reconsider aubv = a * u + b * v,cw = c * w,au = a * u,
bv = b * v as Element of TOP-REAL 3;
A14: cw is Element of REAL 3 by EUCLID:22;
A15: aubv is Element of REAL 3 by EUCLID:22;
au is Element of REAL 3 & bv is Element of REAL 3 by EUCLID:22;
then
A16: aubv.3 = au.3 + bv.3 by RVSUM_1:11
.= a * u.3 + bv.3 by RVSUM_1:44
.= a * u.3 + b * v.3 by RVSUM_1:44;
A17: cw.3 = c * w.3 by RVSUM_1:44;
|[(aubv + cw)`1,(aubv + cw)`2,(aubv+cw)`3]| = |[0,0,0]|
by A12,EUCLID_5:3,4;
then
A18: 0 = (aubv + cw)`3 by FINSEQ_1:78
.= (aubv + cw).3 by EUCLID_5:def 3
.= aubv.3+cw.3 by A14,A15,RVSUM_1:11
.= a * u`3 + b * v.3 + c * w.3 by A16,A17,EUCLID_5:def 3
.= a * u`3 + b * v`3 + c * w.3 by EUCLID_5:def 3
.= a * u`3 + b * v`3 + c * w`3 by EUCLID_5:def 3
.= a + b + c by A2;
thus u,v,w are_collinear
proof
per cases by A13;
suppose
A19: a <> 0;
reconsider L = Line(v,w) as line of TOP-REAL 3;
u in L & v in L & w in L by A18,A12,Th42,A19,RLTOPSP1:72;
hence thesis by RLTOPSP1:def 16;
end;
suppose
A20: b <> 0;
A21: b * v + c * w + a * u = 0.TOP-REAL 3 by A12,RVSUM_1:15;
A22: b + c + a = 0 by A18;
reconsider L = Line(w,u) as line of TOP-REAL 3;
v in L & w in L & u in L by A22,A20,A21,Th42,RLTOPSP1:72;
hence thesis by RLTOPSP1:def 16;
end;
suppose
A23: c <> 0;
A24: c * w + a * u + b * v = 0.TOP-REAL 3 by A12,RVSUM_1:15;
A25: c + a + b = 0 by A18;
reconsider L = Line(u,v) as line of TOP-REAL 3;
w in L & u in L & v in L by A25,A23,A24,Th42,RLTOPSP1:72;
hence thesis by RLTOPSP1:def 16;
end;
end;
end;
assume u,v,w are_collinear;
then per cases by TOPREAL9:67;
suppose u in LSeg(v,w);
then consider r be Real such that 0 <= r & r <= 1 and
A26: u = (1 - r) * v + r * w by RLTOPSP1:76;
reconsider a = 1,b = r - 1,c = -r as Real;
1 * u + (r - 1) * v + (-r) * w = 0.TOP-REAL 3
proof
reconsider vw = v + w as Element of REAL 3 by EUCLID:22;
1 * u = (1 - r) * v + r * w by A26,RVSUM_1:52;
then 1 * u + (r - 1) * v + (-r) * w
= r * w + ((1 - r) * v + (r - 1) * v) + (-r) * w by RVSUM_1:15
.= r * w + ((1 - r) + (r - 1)) * v + (-r) * w by RVSUM_1:50
.= 0 * v + (r * w + (-r) * w) by RVSUM_1:15
.= 0 * v + (r + (-r)) * w by RVSUM_1:50
.= 0 * vw by RVSUM_1:51
.= i|->0 by RVSUM_1:53
.= 0.TOP-REAL 3 by EUCLID_5:4,FINSEQ_2:62;
hence thesis;
end;
hence thesis by A1,ANPROJ_8:11;
end;
suppose v in LSeg(w,u);
then consider r be Real such that 0 <= r & r <= 1 and
A27: v = (1 - r) * w + r * u by RLTOPSP1:76;
reconsider a = -r,b = 1,c = r - 1 as Real;
(-r) * u + 1 * v + (r - 1) * w = 0.TOP-REAL 3
proof
reconsider uw = u + w as Element of REAL 3 by EUCLID:22;
1 * v = (1 - r) * w + r * u by A27,RVSUM_1:52;
then (-r) * u + 1 * v + (r - 1) * w
= (-r) * u + r * u + (1 - r) * w + (r - 1) * w by RVSUM_1:15
.= ((-r) + r) * u + (1 - r) * w + (r - 1) * w by RVSUM_1:50
.= 0 * u + ((1 - r) * w + (r - 1) * w) by RVSUM_1:15
.= 0 * u + (((1 - r) + (r - 1)) * w) by RVSUM_1:50
.= 0 * uw by RVSUM_1:51
.= i|->0 by RVSUM_1:53
.= 0.TOP-REAL 3 by FINSEQ_2:62,EUCLID_5:4;
hence thesis;
end;
hence thesis by A1,ANPROJ_8:11;
end;
suppose w in LSeg(u,v);
then consider r be Real such that 0 <= r & r <= 1 and
A28: w = (1 - r) * u + r * v by RLTOPSP1:76;
reconsider a = r - 1,b = -r,c = 1 as Real;
(r - 1) * u + (-r) * v + 1 * w = 0.TOP-REAL 3
proof
reconsider vu = v + u as Element of REAL 3 by EUCLID:22;
1 * w = (1 - r) * u + r * v by A28,RVSUM_1:52;
then (r - 1) * u + (-r) * v + 1 * w
= (r - 1) * u + ((-r) * v + (r * v + (1 - r) * u)) by RVSUM_1:15
.= (r - 1) * u + ((-r) * v + r * v + (1 - r) * u) by RVSUM_1:15
.= (r - 1) * u + (((-r) + r) * v + (1 - r) * u) by RVSUM_1:50
.= 0 * v + ((r - 1) * u + (1 - r) * u) by RVSUM_1:15
.= 0 * v + (((r - 1) + (1 - r)) * u) by RVSUM_1:50
.= 0 * vu by RVSUM_1:51
.= i|->0 by RVSUM_1:53
.= 0.TOP-REAL 3 by FINSEQ_2:62,EUCLID_5:4;
hence thesis;
end;
hence thesis by A1,ANPROJ_8:11;
end;
end;
theorem Th44:
for u,v,w being Element of TOP-REAL 3 st u in LSeg(v,w) holds
|[u`1,u`2]| in LSeg ( |[v`1,v`2]| , |[w`1,w`2]| )
proof
let u,v,w be Element of TOP-REAL 3;
assume u in LSeg(v,w);
then consider r be Real such that
A1: 0 <= r and
A2: r <= 1 and
A3: u = (1 - r) * v + r * w by RLTOPSP1:76;
reconsider rv = (1 - r) * v,rw = r * w as Element of TOP-REAL 3;
rv = |[ (1 - r) * v`1, (1 - r) * v`2, (1 - r) * v`3 ]| &
rw = |[r * w`1,r * w`2, r * w`3]| by EUCLID_5:7;
then |[ (1 - r) * v`1 + r * w`1,
(1 - r) * v`2 + r * w`2,(1 - r) * v`3 + r * w`3 ]| = u by A3,EUCLID_5:6
.= |[u`1,u`2,u`3]|
by EUCLID_5:3;
then
A4: u`1 = (1 - r) * v`1 + r * w`1 &
u`2 = (1 - r) * v`2 + r *w`2 by FINSEQ_1:78;
reconsider u9 = |[u`1,u`2]|, v9 = |[v`1,v`2]|,
w9 = |[w`1,w`2]| as Element of TOP-REAL 2;
A5: u9`1 = u`1 & u9`2 = u`2 & v9`1 = v`1 & v9`2 = v`2 & w9`1 = w`1 &
w9`2 = w`2 by EUCLID:52;
reconsider rv9 = (1 - r) * v9, rw9 = r * w9 as Element of TOP-REAL 2;
rv9 = |[ (1 - r) * v9`1,(1 - r) * v9`2 ]| &
rw9 = |[ r * w9`1, r * w9`2 ]| by EUCLID:57;
then rv9 + rw9 = |[ u`1,u`2 ]| by A4,A5,EUCLID:56;
then u9 in {(1-r)*v9+r*w9 where r is Real : 0 <= r & r <= 1} by A1,A2;
hence thesis by RLTOPSP1:def 2;
end;
theorem Th45:
for u,v,w being Element of TOP-REAL 2 st u in LSeg(v,w) holds
|[u`1,u`2,1]| in LSeg(|[v`1,v`2,1]|,|[w`1,w`2,1]|)
proof
let u,v,w be Element of TOP-REAL 2;
assume u in LSeg(v,w);
then consider r be Real such that
A1: 0 <= r and
A2: r <= 1 and
A3: u = (1 - r) * v + r * w by RLTOPSP1:76;
reconsider u9 = |[u`1,u`2,1]|,
v9 = |[v`1,v`2,1]|,
w9 = |[w`1,w`2,1]| as Element of TOP-REAL 3;
reconsider rv = (1 - r) * v,
rw = r * w as Element of REAL 2 by EUCLID:22;
A4: rv.1 = (1 - r) * v.1 & rv.2 = (1 - r) * v.2 &
rw.1 = r * w.1 & rw.2 = r * w.2 by RVSUM_1:44;
A5: u`2 = (1 - r) * v.2 + r * w.2 by A4,A3,RVSUM_1:11;
reconsider rv9 = (1 - r) * v9,rw9 = r * w9 as Element of TOP-REAL 3;
u9 = (1 - r) * v9 + r * w9
proof
u9 = |[(1 - r) * v.1 + r * w.1,
(1 - r) * v.2 + r * w.2, (1 - r) * 1 + r * 1]|
by A5,A3,A4,RVSUM_1:11
.= |[(1 - r) * v.1,(1 - r) * v.2,(1 - r) * 1]|
+ |[r * w.1, r * w.2, r * 1]| by EUCLID_5:6
.= (1 - r) * |[v.1,v.2,1]|
+ |[r * w.1, r * w.2, r * 1]| by EUCLID_5:8
.= (1 - r) * |[v`1,v`2,1]|
+ r * |[w`1,w`2,1]| by EUCLID_5:8;
hence thesis;
end;
then u9 in {(1 - r) * v9 + r * w9 where r is Real: 0 <= r & r <= 1}
by A1,A2;
hence thesis by RLTOPSP1:def 2;
end;
theorem Th46:
for P,Q,R being non point_at_infty Point of ProjectiveSpace TOP-REAL 3
holds P,Q,R are_collinear iff Collinear RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R
proof
let P,Q,R be non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
reconsider p = RP3_to_T2 P,q = RP3_to_T2 Q,
r = RP3_to_T2 R as POINT of TarskiEuclid2Space;
consider u be non zero Element of TOP-REAL 3 such that
A1: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
consider v be non zero Element of TOP-REAL 3 such that
A2: Q = Dir v & v`3 = 1 & RP3_to_REAL2 Q = |[v`1,v`2]| by Def05;
consider w be non zero Element of TOP-REAL 3 such that
A3: R = Dir w & w`3 = 1 & RP3_to_REAL2 R = |[w`1,w`2]| by Def05;
hereby
assume
A4: P,Q,R are_collinear;
u,v,w are_collinear by A4,A1,A2,A3,Th43;
then per cases by TOPREAL9:67;
suppose u in LSeg(v,w);
then Tn2TR p in LSeg ( Tn2TR q, Tn2TR r ) by A1,A2,A3,Th44;
hence Collinear RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R by GTARSKI2:20;
end;
suppose v in LSeg(w,u);
then Tn2TR q in LSeg ( Tn2TR r, Tn2TR p ) by A1,A2,A3,Th44;
hence Collinear RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R by GTARSKI2:20;
end;
suppose w in LSeg(u,v);
then Tn2TR r in LSeg ( Tn2TR p, Tn2TR q ) by A1,A2,A3,Th44;
hence Collinear RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R by GTARSKI2:20;
end;
end;
assume Collinear RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R;
then
A5: Tn2TR q in LSeg( Tn2TR p, Tn2TR r) or
Tn2TR r in LSeg( Tn2TR q, Tn2TR p) or
Tn2TR p in LSeg( Tn2TR r, Tn2TR q) by GTARSKI2:20;
reconsider u1 = Tn2TR p, v1 = Tn2TR q,
w1 = Tn2TR r as Element of TOP-REAL 2;
reconsider u9 = |[u1`1,u1`2,1]|,v9 = |[v1`1,v1`2,1]|,
w9 = |[w1`1,w1`2,1]| as Element of TOP-REAL 3;
now
u1`1 = u`1 & u1`2 = u`2 & v1`1 = v`1 &
v1`2 = v`2 & w1`1 = w`1 & w1`2 = w`2 by A1,A2,A3,EUCLID:52;
hence Dir u9 = P & Dir v9 = Q & Dir w9 = R by A1,A2,A3,EUCLID_5:3;
thus u9`3 = 1 & v9`3 = 1 & w9`3 = 1 by EUCLID_5:2;
v9 in LSeg(u9,w9) or w9 in LSeg(v9,u9) or u9 in LSeg(w9,v9) by A5,Th45;
hence u9,v9,w9 are_collinear by TOPREAL9:67;
end;
hence P,Q,R are_collinear by Th43;
end;
theorem
for u,v,w being Element of TOP-REAL 2 st u,v,w are_collinear holds
|[u`1,u`2,1]|,|[v`1,v`2,1]|,|[w`1,w`2,1]| are_collinear
proof
let u,v,w be Element of TOP-REAL 2;
assume
A1: u,v,w are_collinear;
reconsider u1 = |[u`1,u`2,1]|, v1 = |[v`1,v`2,1]|,
w1 = |[w`1,w`2,1]| as non zero Point of TOP-REAL 3;
u in LSeg(v,w) or v in LSeg(w,u) or w in LSeg(u,v) by A1,TOPREAL9:67;
then u1 in LSeg(v1,w1) or v1 in LSeg(w1,u1) or w1 in LSeg(u1,v1) by Th45;
hence thesis by TOPREAL9:67;
end;
theorem Th47:
for P,Q,P1 being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
P in BK_model & Q in BK_model & P1 in absolute :::& P,Q,P1 are_collinear
holds
not between RP3_to_T2 Q,RP3_to_T2 P1,RP3_to_T2 P
proof
let P,Q,P1 be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
assume
A1: P in BK_model & Q in BK_model & P1 in absolute;
set P9 = RP3_to_T2 P, Q9 = RP3_to_T2 Q, P19 = RP3_to_T2 P1;
assume
A2: between Q9,P19,P9;
consider u be non zero Element of TOP-REAL 3 such that
A3: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
consider v be non zero Element of TOP-REAL 3 such that
A4: Q = Dir v & v`3 = 1 & RP3_to_REAL2 Q = |[v`1,v`2]| by Def05;
consider w1 be non zero Element of TOP-REAL 3 such that
A5: P1 = Dir w1 & w1`3 = 1 & RP3_to_REAL2 P1 = |[w1`1,w1`2]| by Def05;
A6: Tn2TR P19 in LSeg(Tn2TR Q9,Tn2TR P9) by A2,GTARSKI2:20;
reconsider u9 = Tn2TR P19, v9 = Tn2TR Q9,
w9 = Tn2TR P9 as Element of TOP-REAL 2;
|[u9`1,u9`2]| = |[w1`1,w1`2]| by A5,EUCLID:53;
then
A7: u9`1 = w1`1 & u9`2 = w1`2 by FINSEQ_1:77;
|[v9`1,v9`2]| = |[v`1,v`2]| by A4,EUCLID:53;
then
A8: v9`1 = v`1 & v9`2 = v`2 by FINSEQ_1:77;
|[w9`1,w9`2]| = |[u`1,u`2]| by A3,EUCLID:53;
then
A9: w9`1 = u`1 & w9`2 = u`2 by FINSEQ_1:77;
reconsider pu = |[u9`1,u9`2,1]|, pv = |[v9`1,v9`2,1]|,
pw = |[w9`1,w9`2,1]| as non zero Element of TOP-REAL 3;
pu in LSeg(pw,pv) by A6,Th45;
then consider r be Real such that
A10: 0 <= r & r <= 1 and
A11: pu = (1 - r) * pw + r * pv by RLTOPSP1:76;
now
thus Q = Dir pv by A4,A8,EUCLID_5:3;
thus P = Dir pw by A3,A9,EUCLID_5:3;
thus P1 = Dir pu by A5,A7,EUCLID_5:3;
thus pv.3 = pv`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
thus pw.3 = pw`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
thus pu = r * pv + (1 - r) * pw by A11;
end;
then P1 is Element of BK_model by A1,A10,Th17;
hence contradiction by A1,BKMODEL2:1,XBOOLE_0:def 4;
end;
definition
func Dir001 -> non point_at_infty Element of
ProjectiveSpace TOP-REAL 3 equals
Dir |[0,0,1]|;
coherence
proof
reconsider P = Dir |[0,0,1]| as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
for u be non zero Element of TOP-REAL 3 st P = Dir u holds u`3 <> 0
proof
let u be non zero Element of TOP-REAL 3;
assume P = Dir u;
then are_Prop u,|[0,0,1]| by ANPROJ_1:22;
then consider a be Real such that
A1: a <> 0 and
A2: u = a * |[0,0,1]| by ANPROJ_1:1;
u = |[ a * 0,a * 0,a * 1]| by A2,EUCLID_5:8;
hence thesis by A1,EUCLID_5:2;
end;
hence thesis by Def04;
end;
end;
definition
func Dir101 -> non point_at_infty Element of
ProjectiveSpace TOP-REAL 3 equals
Dir |[1,0,1]|;
coherence
proof
reconsider P = Dir |[1,0,1]| as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
for u be non zero Element of TOP-REAL 3 st P = Dir u holds u`3 <> 0
proof
let u be non zero Element of TOP-REAL 3;
assume P = Dir u;
then are_Prop u,|[1,0,1]| by ANPROJ_1:22;
then consider a be Real such that
A1: a <> 0 and
A2: u = a * |[1,0,1]| by ANPROJ_1:1;
u = |[ a * 1,a * 0,a * 1]| by A2,EUCLID_5:8;
hence thesis by A1,EUCLID_5:2;
end;
hence thesis by Def04;
end;
end;
theorem
for P,Q being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
P in absolute & Q in absolute
holds RP3_to_T2 Dir001, RP3_to_T2 P equiv RP3_to_T2 Dir001,RP3_to_T2 Q
proof
let P,Q be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
assume that
A1: P in absolute and
A2: Q in absolute;
reconsider p = RP3_to_T2 P, q = RP3_to_T2 Q,
r = RP3_to_T2 Dir001 as Element of TarskiEuclid2Space;
consider u be non zero Element of TOP-REAL 3 such that
A3: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
consider v be non zero Element of TOP-REAL 3 such that
A4: Q = Dir v & v`3 = 1 & RP3_to_REAL2 Q = |[v`1,v`2]| by Def05;
consider w be non zero Element of TOP-REAL 3 such that
A5: Dir001 = Dir w & w`3 = 1 & RP3_to_REAL2 Dir001 = |[w`1,w`2]| by Def05;
are_Prop |[0,0,1]|,w by A5,ANPROJ_1:22;
then consider a be Real such that a <> 0 and
A6: w = a * |[0,0,1]| by ANPROJ_1:1;
w = |[ a * 0, a * 0, a * 1]| by A6,EUCLID_5:8;
then
A8: w`1 = 0 & w`2 = 0 by EUCLID_5:2;
reconsider u1=u`1,u2=u`2,v1=v`1,v2=v`2,w1=w`1,w2=w`2 as Real;
now
A9: (Tn2TR RP3_to_T2 P)`1 = u`1 & (Tn2TR RP3_to_T2 P)`2 = u`2 &
(Tn2TR RP3_to_T2 Q)`1 = v`1 & (Tn2TR RP3_to_T2 Q)`2 = v`2 &
(Tn2TR RP3_to_T2 Dir001)`1 = w`1 & (Tn2TR RP3_to_T2 Dir001)`2 = w`2
by A3,A4,A5,EUCLID:52;
reconsider uP = |[u`1,u`2,1]| as non zero Element of TOP-REAL 3;
now
thus P in absolute by A1;
thus P = Dir uP by A3,EUCLID_5:3;
uP`3 = 1 by EUCLID_5:2;
hence uP.3 = 1 by EUCLID_5:def 3;
end;
then |[uP.1,uP.2]| in circle(0,0,1) by BKMODEL1:84;
then (uP.1)^2+(uP.2)^2 = 1 by BKMODEL1:13;
then (uP`1)^2+(uP.2)^2 = 1 by EUCLID_5:def 1;
then (uP`1)^2+(uP`2)^2 = 1 by EUCLID_5:def 2;
then (u`1)^2+(uP`2)^2 = 1 by EUCLID_5:2;
then
A10: (u`1)^2+(u`2)^2 = 1 by EUCLID_5:2;
reconsider vQ = |[v`1,v`2,1]| as non zero Element of TOP-REAL 3;
now
thus Q in absolute by A2;
thus Q = Dir vQ by A4,EUCLID_5:3;
vQ`3 = 1 by EUCLID_5:2;
hence vQ.3 = 1 by EUCLID_5:def 3;
end;
then |[vQ.1,vQ.2]| in circle(0,0,1) by BKMODEL1:84;
then (vQ.1)^2+(vQ.2)^2 = 1 by BKMODEL1:13;
then (vQ`1)^2+(vQ.2)^2 = 1 by EUCLID_5:def 1;
then (vQ`1)^2+(vQ`2)^2 = 1 by EUCLID_5:def 2;
then (v`1)^2+(vQ`2)^2 = 1 by EUCLID_5:2;
then
A11: (v`1)^2+(v`2)^2 = 1 by EUCLID_5:2;
now
thus dist(RP3_to_T2 Dir001,RP3_to_T2 P)
= sqrt((( 0 )-(u`1))^2+(( 0 )-(u`2))^2) by A9,A8,GTARSKI2:16
.= sqrt ((u`1)^2+(-u`2)^2) by SQUARE_1:3
.= 1 by A10,SQUARE_1:3,18;
thus dist(RP3_to_T2 Dir001,RP3_to_T2 Q)
= sqrt(((w`1)-(v`1))^2+((w`2)-(v`2))^2) by A9,GTARSKI2:16
.= sqrt ((v`1)^2+(-v`2)^2) by A8,SQUARE_1:3
.= 1 by A11,SQUARE_1:3,18;
end;
hence dist(RP3_to_T2 Dir001,RP3_to_T2 P)
= dist(RP3_to_T2 Dir001,RP3_to_T2 Q);
thus dist(RP3_to_T2 Dir001,RP3_to_T2 P)
= |. Tn2TR RP3_to_T2 Dir001 - Tn2TR RP3_to_T2 P .| by GTARSKI2:17;
thus dist(RP3_to_T2 Dir001,RP3_to_T2 Q)
= |. Tn2TR RP3_to_T2 Dir001 - Tn2TR RP3_to_T2 Q .| by GTARSKI2:17;
end;
hence thesis by GTARSKI2:18;
end;
theorem Th48:
for P,Q,R being non point_at_infty Element of ProjectiveSpace TOP-REAL 3
for u,v,w being non zero Element of TOP-REAL 3 st
P in absolute & Q in absolute & P <> Q & P = Dir u & Q = Dir v & R = Dir w &
u`3 = 1 & v`3 = 1 & w = |[ (u`1 + v`1) / 2,(u`2 + v`2) / 2,1]| holds
R in BK_model
proof
let P,Q,R be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
let u,v,w be non zero Element of TOP-REAL 3;
assume that
A1: P in absolute and
A2: Q in absolute and
A3: P <> Q and
A4: P = Dir u & Q = Dir v & R = Dir w and
A5: u`3 = 1 & v`3 = 1 and
A6: w = |[ (u`1 + v`1) / 2,(u`2 + v`2) / 2, 1]|;
A7: u.3 = 1 & v.3 = 1 by A5,EUCLID_5:def 3;
reconsider u9 = |[u.1,u.2]|,v9 = |[v.1,v.2]| as Element of TOP-REAL 2;
set M = the_midpoint_of_the_segment(u9,v9);
A8: w`1 = (u`1+v`1)*1/2 & w`2=(u`2+v`2)*1/2 by A6,EUCLID_5:2;
A9: M = 1/2 * (u9 + v9) by EUCLID12:29
.= 1/2 * |[u.1 + v.1,u.2 + v.2]| by EUCLID:56
.= |[(u.1+v.1)*1/2,(u.2+v.2)*1/2]| by EUCLID:58
.= |[(u`1+v.1)*1/2,(u.2+v.2)*1/2]| by EUCLID_5:def 1
.= |[(u`1+v.1)*1/2,(u`2+v.2)*1/2]| by EUCLID_5:def 2
.= |[(u`1+v`1)*1/2,(u`2+v.2)*1/2]| by EUCLID_5:def 1
.= |[w`1,w`2]| by A8,EUCLID_5:def 2;
u9 in circle(0,0,1) & v9 in circle(0,0,1) by A7,A1,A2,A4,BKMODEL1:84;
then
A10: LSeg(u9,v9) \ {u9,v9} c= inside_of_circle(0,0,1) by TOPREAL9:60;
u9 <> v9
proof
assume u9 = v9;
then u.1 = v.1 & u.2 = v.2 by FINSEQ_1:77;
then u`1 = v.1 & u`2 = v.2 by EUCLID_5:def 1,def 2;
then u`1 = v`1 & u`2 = v`2 by EUCLID_5:def 1,def 2;
then u = |[v`1,v`2,v`3]| by A5,EUCLID_5:3
.= v by EUCLID_5:3;
hence contradiction by A4,A3;
end;
then M <> u9 & M <> v9 by EUCLID12:32,33;
then
A11: not M in {u9,v9} by TARSKI:def 2;
M in LSeg(u9,v9) by EUCLID12:28;
then M in LSeg(u9,v9) \ {u9,v9} by A11,XBOOLE_0:def 5;
then reconsider rw = |[w`1,w`2]| as Element of inside_of_circle(0,0,1)
by A10,A9;
consider RW2 be Element of TOP-REAL 2 such that
A12: RW2 = rw & REAL2_to_BK rw = Dir |[RW2`1,RW2`2,1]| by BKMODEL2:def 3;
A13: rw`1 = w`1 & rw`2 = w`2 by EUCLID:52;
|[RW2`1,RW2`2,1]| = |[w`1,w`2,w`3]| by A12,A13,A6,EUCLID_5:2
.= w by EUCLID_5:3;
hence thesis by A12,A4;
end;
theorem Th49:
for R1,R2 being Point of TarskiEuclid2Space st
Tn2TR R1 in circle(0,0,1) & Tn2TR R2 in circle(0,0,1) & R1 <> R2 holds
ex P being Element of BK-model-Plane st between R1,BK_to_T2 P,R2
proof
let R1,R2 be Point of TarskiEuclid2Space;
assume
A1: Tn2TR R1 in circle(0,0,1) & Tn2TR R2 in circle(0,0,1) & R1 <> R2;
reconsider P = Tn2TR R1, Q = Tn2TR R2 as Element of TOP-REAL 2;
A2: P = |[P`1,P`2]| & Q = |[Q`1,Q`2]| by EUCLID:53;
reconsider w = |[ (P`1+Q`1)/2,(P`2+Q`2)/2 ]| as Element of TOP-REAL 2;
reconsider u9 = |[P`1,P`2,1]|,
v9 = |[Q`1,Q`2,1]| as non zero Element of TOP-REAL 3;
reconsider w9 = |[w`1,w`2,1]| as non zero Element of TOP-REAL 3;
reconsider P9 = Dir u9, Q9 = Dir v9,
R9 = Dir w9 as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
u9`3 = 1 & v9`3 = 1 by EUCLID_5:2;
then reconsider P9,Q9 as
non point_at_infty Point of ProjectiveSpace TOP-REAL 3 by Th40;
w9`3 <> 0 by EUCLID_5:2;
then reconsider R9 as
non point_at_infty Point of ProjectiveSpace TOP-REAL 3 by Th40;
reconsider R99 = RP3_to_T2 R9 as Point of TarskiEuclid2Space;
consider w99 be non zero Element of TOP-REAL 3 such that
A3: R9 = Dir w99 & w99`3 = 1 & RP3_to_REAL2 R9 = |[w99`1,w99`2]| by Def05;
A4: w9`1 = w`1 & w9`2 = w`2 by EUCLID_5:2;
w99.3 = 1 & w9`3 = 1 by A3,EUCLID_5:2,def 3;
then w99.3 = w9.3 & w9.3 <> 0 by EUCLID_5:def 3;
then
A5: w99 = w9 by A3,BKMODEL1:43;
A6: Tn2TR R99 = w by A3,A5,A4,EUCLID:53;
w = |[ P`1 / 2 + Q`1 / 2, P`2 / 2 + Q`2 / 2]|
.= |[ P`1/2 ,P`2/2]| + |[Q`1/2,Q`2/2]| by EUCLID:56
.= 1/2 * |[P`1,P`2]| + |[Q`1/2,Q`2/2]| by EUCLID:58
.= (1 - 1/2) * P + 1/2 * Q by A2,EUCLID:58;
then w in {(1-r)*P + r * Q where r is Real: 0 <= r & r <= 1};
then
A7: w in LSeg(Tn2TR R1,Tn2TR R2) by RLTOPSP1:def 2;
now
now
thus P9 = Dir u9;
u9`3 = 1 by EUCLID_5:2;
hence u9.3 = 1 by EUCLID_5:def 3;
thus |[P`1,P`2]| in circle(0,0,1) by A1,EUCLID:53;
u9`1 = P`1 & u9`2 = P`2 by EUCLID_5:2;
then P`1 = u9.1 & P`2 = u9.2 by EUCLID_5:def 1,def 2;
hence |[u9.1,u9.2]| in circle(0,0,1) by A1,EUCLID:53;
end;
then P9 is Element of absolute by BKMODEL1:86;
hence P9 in absolute;
now
thus Q9 = Dir v9;
v9`3 = 1 by EUCLID_5:2;
hence v9.3 = 1 by EUCLID_5:def 3;
v9`1 = Q`1 & v9`2 = Q`2 by EUCLID_5:2;
then Q`1 = v9.1 & Q`2 = v9.2 by EUCLID_5:def 1,def 2;
hence |[v9.1,v9.2]| in circle(0,0,1) by A1,EUCLID:53;
end;
then Q9 is Element of absolute by BKMODEL1:86;
hence Q9 in absolute;
thus P9 <> Q9
proof
assume
A8: P9 = Q9;
now
thus Dir u9 = Dir v9 by A8;
thus u9.3 = u9`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
thus v9.3 = v9`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
end;
then u9 = v9 by BKMODEL1:43;
then P`1 = Q`1 & P`2 = Q`2 by FINSEQ_1:78;
then |[P`1,P`2]| = Q by EUCLID:53;
hence contradiction by A1,EUCLID:53;
end;
thus u9`3 = 1 & v9`3 = 1 by EUCLID_5:2;
thus w9 = |[(u9`1+ v9`1)/2,(u9`2+v9`2)/2,1]|
proof
u9`1 = P`1 & v9`1 = Q`1 & u9`2 = P`2 & v9`2 = Q`2 &
w`1 = (P`1+Q`1)/2 & w`2 = (P`2+Q`2)/2 by EUCLID:52,EUCLID_5:2;
hence thesis;
end;
end;
then reconsider AR9 = R9 as Element of BK-model-Plane by Th48;
consider r be Element of BK_model such that
A9: AR9 = r and
A10: BK_to_T2 AR9 = BK_to_REAL2 r by Def01;
take AR9;
now
thus R99 = RP3_to_T2 R9;
consider x be non zero Element of TOP-REAL 3 such that
A11: Dir x = r & x.3 = 1 & BK_to_REAL2 r = |[x.1,x.2]| by BKMODEL2:def 2;
now
thus Dir x = Dir w9 by A11,A9;
thus x.3 <> 0 by A11;
w9.3 = w9`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
hence x.3 = w9.3 by A11;
end;
then x = w9 by Th16;
then BK_to_REAL2 r = |[w9`1,w9.2]| by A11,EUCLID_5:def 1
.= |[w`1,w`2]| by A4,EUCLID_5:def 2
.= w by EUCLID:53;
hence RP3_to_T2 R9 = BK_to_T2 AR9 by A3,A5,A4,EUCLID:53,A10;
end;
hence
between R1,BK_to_T2 AR9,R2 by A7,A6,GTARSKI2:20;
end;
theorem Th50:
for P,Q being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
RP3_to_T2 P = RP3_to_T2 Q holds P = Q
proof
let P,Q be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
assume
A1: RP3_to_T2 P = RP3_to_T2 Q;
consider u be non zero Element of TOP-REAL 3 such that
A2: P = Dir u and
A3: u`3 = 1 and
A4: RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
consider v be non zero Element of TOP-REAL 3 such that
A5: Q = Dir v and
A6: v`3 = 1 and
A7: RP3_to_REAL2 Q = |[v`1,v`2]| by Def05;
v`1 = u`1 & v`2 = u`2 & v`3 = u`3 by A1,A4,A7,A3,A6,FINSEQ_1:77;
then |[u`1,u`2,u`3]| = v by EUCLID_5:3;
hence thesis by A2,A5,EUCLID_5:3;
end;
theorem Th51:
for R1,R2 being non point_at_infty Element of ProjectiveSpace TOP-REAL 3
st R1 in absolute & R2 in absolute & R1 <> R2 holds
ex P being Element of BK-model-Plane st
between RP3_to_T2 R1,BK_to_T2 P,RP3_to_T2 R2
proof
let R1,R2 be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
assume that
A1: R1 in absolute & R2 in absolute and
A2: R1 <> R2;
consider u1 be non zero Element of TOP-REAL 3 such that
A3: R1 = Dir u1 and
A4: u1`3 = 1 and
A5: RP3_to_REAL2 R1 = |[u1`1,u1`2]| by Def05;
u1.3 = 1 by A4,EUCLID_5:def 3;
then |[u1.1,u1.2]| in circle(0,0,1) by A1,A3,BKMODEL1:84;
then
A6: |[u1`1,u1.2]| in circle(0,0,1) by EUCLID_5:def 1;
consider u2 be non zero Element of TOP-REAL 3 such that
A7: R2 = Dir u2 and
A8: u2`3 = 1 and
A9: RP3_to_REAL2 R2 = |[u2`1,u2`2]| by Def05;
u2.3 = 1 by A8,EUCLID_5:def 3;
then |[u2.1,u2.2]| in circle(0,0,1) by A1,A7,BKMODEL1:84;
then
A10: |[u2`1,u2.2]| in circle(0,0,1) by EUCLID_5:def 1;
reconsider P1 = RP3_to_T2 R1,
P2 = RP3_to_T2 R2 as Point of TarskiEuclid2Space;
Tn2TR P1 in circle(0,0,1) & Tn2TR P2 in circle(0,0,1) & P1 <> P2
by A2,Th50,A6,A5,A9,A10,EUCLID_5:def 2;
hence thesis by Th49;
end;
theorem Th52:
for P,Q,R being Point of TarskiEuclid2Space st between P,Q,R &
Tn2TR P in inside_of_circle(0,0,1) & Tn2TR R in inside_of_circle(0,0,1)
holds Tn2TR Q in inside_of_circle(0,0,1)
proof
let P,Q,R be Point of TarskiEuclid2Space;
assume that
A1: between P,Q,R and
A2: Tn2TR P in inside_of_circle(0,0,1) & Tn2TR R in inside_of_circle(0,0,1);
LSeg(Tn2TR P,Tn2TR R) c= inside_of_circle(0,0,1) by A2,RLTOPSP1:22;
hence thesis by A1,GTARSKI2:20;
end;
theorem Th53:
for P being non point_at_infty Element of ProjectiveSpace TOP-REAL 3
st P in absolute holds RP3_to_REAL2 P in circle(0,0,1)
proof
let P be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
assume
A1: P in absolute;
consider u be non zero Element of TOP-REAL 3 such that
A2: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
u.3 = 1 by A2,EUCLID_5:def 3;
then |[u.1,u.2]| in circle(0,0,1) by A1,A2,BKMODEL1:84;
then |[u`1,u.2]| in circle(0,0,1) by EUCLID_5:def 1;
hence thesis by A2,EUCLID_5:def 2;
end;
theorem
for P being non point_at_infty Element of ProjectiveSpace TOP-REAL 3
st P in BK_model holds RP3_to_REAL2 P in inside_of_circle(0,0,1)
proof
let P be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
assume 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
A1: Dir u = P1 & u.3 = 1 and
A2: BK_to_REAL2 P1 = |[u.1,u.2]| by BKMODEL2:def 2;
|[u`1,u.2]| is Element of inside_of_circle(0,0,1) by A2,EUCLID_5:def 1;
then
A3: |[u`1,u`2]| is Element of inside_of_circle(0,0,1) by EUCLID_5:def 2;
consider v be non zero Element of TOP-REAL 3 such that
A4: P = Dir v & v`3 = 1 & RP3_to_REAL2 P = |[v`1,v`2]| by Def05;
Dir v = Dir u & u.3 <> 0 & u.3 = v.3 by A1,A4,EUCLID_5:def 3;
then u = v by Th16;
hence thesis by A4,A3;
end;
theorem Th54:
for P being non point_at_infty Point of ProjectiveSpace TOP-REAL 3
for Q being Element of BK_model st P = Q holds RP3_to_REAL2 P = BK_to_REAL2 Q
proof
let P be non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
let Q be Element of BK_model;
assume
A1: P = Q;
consider u be non zero Element of TOP-REAL 3 such that
A2: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
consider v be non zero Element of TOP-REAL 3 such that
A3: Dir v = Q & v.3 = 1 & BK_to_REAL2 Q = |[v.1,v.2]| by BKMODEL2:def 2;
Dir v = Dir u & u.3 <> 0 & u.3 = v.3 by A1,A2,A3,EUCLID_5:def 3;
then u = v by Th16;
then BK_to_REAL2 Q = |[u`1,u.2]| by A3,EUCLID_5:def 1
.= |[u`1,u`2]| by EUCLID_5:def 2;
hence thesis by A2;
end;
theorem Th55:
for P,Q,R1,R2 being non point_at_infty Element of ProjectiveSpace
TOP-REAL 3 st P <> Q & P in BK_model & R1 in absolute &
R2 in absolute & between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R1 &
between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R2 holds R1 = R2
proof
let P,Q,R1,R2 be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
assume that
A1: P <> Q and
A2: P in BK_model and
A3: R1 in absolute and
A4: R2 in absolute and
A5: between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R1 and
A6: between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R2;
assume R1 <> R2;
then consider S be Element of BK-model-Plane such that
A7: between RP3_to_T2 R1,BK_to_T2 S,RP3_to_T2 R2 by A3,A4,Th51;
set p = RP3_to_T2 P, q = RP3_to_T2 Q, r1 = RP3_to_T2 R1,
r2 = RP3_to_T2 R2, s = BK_to_T2 S;
(between p,r1,r2 or between p,r2,r1) & between r1,s,r2 & between r2,s,r1
by A7,GTARSKI1:16,A1,A5,A6,Th50,GTARSKI3:56;
then per cases by GTARSKI1:19;
suppose
A8: between p,r1,s;
A9: RP3_to_REAL2 R1 in circle(0,0,1) by A3,Th53;
now
thus between p,r1,s by A8;
reconsider P9 = P as Element of BK_model by A2;
BK_to_REAL2 P9 = RP3_to_REAL2 P by Th54;
hence Tn2TR p in inside_of_circle(0,0,1);
thus Tn2TR s in inside_of_circle(0,0,1) by Th02;
end;
then Tn2TR r1 in inside_of_circle(0,0,1) by Th52;
then RP3_to_REAL2 R1 in inside_of_circle(0,0,1) /\ circle(0,0,1)
by A9,XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 7,TOPREAL9:54;
end;
suppose
A10: between p,r2,s;
A11: RP3_to_REAL2 R2 in circle(0,0,1) by A4,Th53;
now
thus between p,r2,s by A10;
reconsider P9 = P as Element of BK_model by A2;
reconsider P99 = P9 as POINT of BK-model-Plane;
BK_to_REAL2 P9 = RP3_to_REAL2 P by Th54;
hence Tn2TR p in inside_of_circle(0,0,1);
thus Tn2TR s in inside_of_circle(0,0,1) by Th02;
end;
then Tn2TR r2 in inside_of_circle(0,0,1) by Th52;
then RP3_to_REAL2 R2 in inside_of_circle(0,0,1) /\ circle(0,0,1)
by A11,XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 7,TOPREAL9:54;
end;
end;
theorem Th56:
for P,Q,P1,P2 being non point_at_infty Element of ProjectiveSpace
TOP-REAL 3 st P <> Q & P in BK_model & Q in BK_model & P1 in absolute &
P2 in absolute & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear
holds between RP3_to_T2 Q,RP3_to_T2 P,RP3_to_T2 P1 or
between RP3_to_T2 Q,RP3_to_T2 P,RP3_to_T2 P2
proof
let P,Q,P1,P2 be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
assume that
A1: P <> Q and
A2: P in BK_model and
A3: Q in BK_model and
A4: P1 in absolute and
A5: P2 in absolute and
A6: P1 <> P2 and
A7: P,Q,P1 are_collinear and
A8: P,Q,P2 are_collinear;
set P9 = RP3_to_T2 P, Q9 = RP3_to_T2 Q, P19 = RP3_to_T2 P1,
P29 = RP3_to_T2 P2;
Collinear P9,Q9,P19 & Collinear P9,Q9,P29 &
not between Q9,P19,P9 & not between Q9,P29,P9
by A2,A3,A4,A5,A7,A8,Th47,Th46;
hence thesis by A1,A2,A4,A5,A6,Th55,GTARSKI1:16;
end;
theorem Th57:
for P,Q being Element of BK_model st P <> Q holds
ex R being Element of absolute st
(for p,q,r being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
p = P & q = Q & r = R holds between RP3_to_T2 q,RP3_to_T2 p,RP3_to_T2 r)
proof
let P,Q be Element of BK_model;
assume
A1: P <> Q;
then consider P1,P2 be Element of absolute such that
A2: P1 <> P2 and
A3: P,Q,P1 are_collinear & P,Q,P2 are_collinear by BKMODEL2:20;
reconsider p = P,q = Q,p1 = P1,
p2 = P2 as Element of ProjectiveSpace TOP-REAL 3;
now
consider u be Element of TOP-REAL 3 such that
A4: u is not zero and
A5: p = Dir u by ANPROJ_1:26;
u.3 <> 0 by A4,A5,BKMODEL2:2;
then u`3 <> 0 by EUCLID_5:def 3;
hence p is non point_at_infty by A4,A5,Th40;
consider v be Element of TOP-REAL 3 such that
A6: v is not zero and
A7: q = Dir v by ANPROJ_1:26;
v.3 <> 0 by A6,A7,BKMODEL2:2;
then v`3 <> 0 by EUCLID_5:def 3;
hence q is non point_at_infty by A6,A7,Th40;
consider w be non zero Element of TOP-REAL 3 such that
A8: w.3 = 1 and
A9: p1 = Dir w by BKMODEL3:30;
w`3 <> 0 by A8,EUCLID_5:def 3;
hence p1 is non point_at_infty by A9,Th40;
consider x be non zero Element of TOP-REAL 3 such that
A10: x.3 = 1 and
A11: p2 = Dir x by BKMODEL3:30;
x`3 <> 0 by A10,EUCLID_5:def 3;
hence p2 is non point_at_infty by A11,Th40;
end;
then reconsider p,q,p1,p2 as
non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
per cases by A1,A2,A3,Th56;
suppose
A12: between RP3_to_T2 q,RP3_to_T2 p,RP3_to_T2 p1;
take P1;
thus thesis by A12;
end;
suppose
A13: between RP3_to_T2 q,RP3_to_T2 p,RP3_to_T2 p2;
take P2;
thus thesis by A13;
end;
end;
theorem Th58:
for P,Q being Element of BK_model st P <> Q holds
ex R being Element of absolute st
(for p,q,r being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
p = P & q = Q & r = R holds between RP3_to_T2 p,RP3_to_T2 q,RP3_to_T2 r)
proof
let P,Q be Element of BK_model;
assume P <> Q;
then consider R be Element of absolute such that
A1: (for p,q,r being non point_at_infty Element of ProjectiveSpace TOP-REAL 3
st p = Q & q = P & r = R holds
between RP3_to_T2 q,RP3_to_T2 p,RP3_to_T2 r) by Th57;
take R;
thus thesis by A1;
end;
theorem Th59:
Dir |[1,0,1]| is Element of absolute
proof
reconsider u = |[1,0,1]| as non zero Element of TOP-REAL 3;
reconsider P = Dir u as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
now
thus u.3 = u`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
now
thus u.1 = u`1 by EUCLID_5:def 1
.= 1 by EUCLID_5:2;
thus u.2 = u`2 by EUCLID_5:def 2
.= 0 by EUCLID_5:2;
end;
then u.1 * u.1 = 1 & u.2 * u.2 = 0;
then (u.1)^2 = 1 & (u.2)^2 = 0 by SQUARE_1:def 1;
then (u.1)^2 + (u.2)^2 = 1;
hence |[u.1,u.2]| in circle(0,0,1) by BKMODEL1:13;
end;
then P is Element of absolute by BKMODEL1:86;
hence thesis;
end;
theorem Th60:
for a,b being POINT of BK-model-Plane holds a,a equiv b,b
proof
let a,b be POINT of BK-model-Plane;
reconsider A = a, B = b as Element of BK_model;
reconsider P = Dir |[1,0,1]| as Element of absolute by Th59;
consider N be invertible Matrix of 3,F_Real such that
A1: homography(N).:absolute = absolute and
A2: (homography(N)).a = b and
(homography(N)).P = P by BKMODEL2:56;
homography(N) in the set of all homography(N) where
N is invertible Matrix of 3,F_Real;
then reconsider h = homography(N) as Element of EnsHomography3
by ANPROJ_9:def 1;
h is_K-isometry by A1,BKMODEL2:def 6;
then h in EnsK-isometry by BKMODEL2:def 7;
then reconsider h = homography(N) as Element of SubGroupK-isometry
by BKMODEL2:def 8;
ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st h = homography(N) &
homography(N).a = b & homography(N).a = b
proof
take h;
take N;
thus thesis by A2;
end;
hence thesis by BKMODEL3:def 8;
end;
theorem Th61:
for P being Element of BK_model holds
P is non point_at_infty Element of ProjectiveSpace TOP-REAL 3
proof
let P be Element of BK_model;
reconsider p = P as Element of ProjectiveSpace TOP-REAL 3;
consider u be Element of TOP-REAL 3 such that
P1: u is not zero and
P2: p = Dir u by ANPROJ_1:26;
u.3 <> 0 by P1,P2,BKMODEL2:2;
then u`3 <> 0 by EUCLID_5:def 3;
hence thesis by P1,P2,Th40;
end;
theorem Th62:
for P being Element of absolute holds
P is non point_at_infty Element of ProjectiveSpace TOP-REAL 3
proof
let P be Element of absolute;
consider u be non zero Element of TOP-REAL 3 such that
A1: u.3 = 1 and
A2: P = Dir u by BKMODEL3:30;
u`3 = 1 by A1,EUCLID_5:def 3;
hence thesis by A2,Th40;
end;
theorem Th63:
for P being Element of BK_model
for P9 being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
P = P9 holds RP3_to_REAL2 P9 = BK_to_REAL2 P
proof
let P be Element of BK_model;
let P9 be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
assume
A1: P = P9;
consider u be non zero Element of TOP-REAL 3 such that
A2: P9 = Dir u & u`3 = 1 & RP3_to_REAL2 P9 = |[u`1,u`2]| by Def05;
consider v be non zero Element of TOP-REAL 3 such that
A3: Dir v = P & v.3 = 1 & BK_to_REAL2 P = |[v.1,v.2]| by BKMODEL2:def 2;
Dir u = Dir v & u.3 = v.3 & u.3 <> 0 by A1,A2,A3,EUCLID_5:def 3;
then u = v by Th16;
then u`1 = v.1 & u`2 = v.2 by EUCLID_5:def 1,def 2;
hence thesis by A2,A3;
end;
theorem Th64:
for a, q, b, c being POINT of BK-model-Plane holds
ex x being POINT of BK-model-Plane st between q,a,x & a,x equiv b,c
proof
let A,Q,B,C be POINT of BK-model-Plane;
consider a be Element of BK_model such that
A1: A = a and
BK_to_T2 A = BK_to_REAL2 a by Def01;
consider q be Element of BK_model such that
A2: Q = q and
BK_to_T2 Q = BK_to_REAL2 q by Def01;
consider b be Element of BK_model such that
A3: B = b and
BK_to_T2 B = BK_to_REAL2 b by Def01;
consider c be Element of BK_model such that
A4: C = c and
BK_to_T2 C = BK_to_REAL2 c by Def01;
per cases;
suppose b <> c;
A5: for q1,a1,b1,c1 being POINT of BK-model-Plane st q1 <> a1 holds
ex x being POINT of BK-model-Plane st between q1,a1,x & a1,x equiv b1,c1
proof
let q1,a1,b1,c1 be POINT of BK-model-Plane;
assume
A6: q1 <> a1;
reconsider Q1 = q1, A1 = a1, B1 = b1, C1 = c1 as Element of BK_model;
reconsider pQ1=Q1,pA1=A1,pB1=B1,pC1=C1 as
non point_at_infty Element of ProjectiveSpace TOP-REAL 3 by Th61;
consider qaR be Element of absolute such that
A7: (for p,q,r being non point_at_infty Element of
ProjectiveSpace TOP-REAL 3 st p = q1 & q = a1 & r = qaR holds
between RP3_to_T2 p,RP3_to_T2 q,RP3_to_T2 r)
by A6,Th58;
reconsider pqaR = qaR as
non point_at_infty Element of ProjectiveSpace TOP-REAL 3 by Th62;
per cases;
suppose
A8: B1 = C1;
reconsider x = a1 as Element of BK_model;
reconsider x as POINT of BK-model-Plane;
take x;
Tn2TR BK_to_T2 a1 in LSeg(Tn2TR BK_to_T2 q1,Tn2TR BK_to_T2 x)
by RLTOPSP1:68;
then between BK_to_T2 q1,BK_to_T2 a1,BK_to_T2 x by GTARSKI2:20;
hence between q1,a1,x by Th05;
thus a1,x equiv b1,c1 by A8,Th60;
end;
suppose
A9: B1 <> C1;
consider bcP be Element of absolute such that
A10: (for p,q,r being non point_at_infty Element of ProjectiveSpace
TOP-REAL 3 st p = b1 & q = c1 & r = bcP holds
between RP3_to_T2 p,RP3_to_T2 q,RP3_to_T2 r) by A9,Th58;
reconsider pbcP = bcP as non point_at_infty Element of
ProjectiveSpace TOP-REAL 3 by Th62;
consider N be invertible Matrix of 3,F_Real such that
A11: homography(N).:absolute = absolute and
A12: (homography(N)).B1 = A1 and
A13: (homography(N)).bcP = qaR by BKMODEL2:56;
homography(N) in the set of all homography(N) where
N is invertible Matrix of 3,F_Real;
then reconsider h = homography(N) as Element of EnsHomography3
by ANPROJ_9:def 1;
h is_K-isometry by A11,BKMODEL2:def 6;
then h in EnsK-isometry by BKMODEL2:def 7;
then reconsider h = homography(N) as Element of SubGroupK-isometry
by BKMODEL2:def 8;
h = homography(N);
then reconsider x = (homography(N)).C1 as Element of BK_model
by BKMODEL3:36;
reconsider x as POINT of BK-model-Plane;
reconsider px = x as non point_at_infty Element of
ProjectiveSpace TOP-REAL 3 by Th61;
take x;
now
thus between q1,a1,x
proof
A14: between RP3_to_T2 pQ1,RP3_to_T2 pA1,RP3_to_T2 pqaR by A7;
between RP3_to_T2 pB1,RP3_to_T2 pC1,RP3_to_T2 pbcP &
h = homography(N) & pB1 in BK_model & pC1 in BK_model &
pbcP in absolute by A10;
then
A15: between RP3_to_T2 pA1,RP3_to_T2 px,RP3_to_T2 pqaR
by A12,A13,Th41;
set tq = RP3_to_T2 pQ1, ta = RP3_to_T2 pA1,
tx = RP3_to_T2 px, tr = RP3_to_T2 pqaR;
A16: between tq,ta,tx by A15,A14,GTARSKI3:17;
now
consider pp1 be Element of BK_model such that
A17: q1 = pp1 and
A18: BK_to_T2 q1 = BK_to_REAL2 pp1 by Def01;
consider pp2 be Element of BK_model such that
A19: a1 = pp2 and
A20: BK_to_T2 a1 = BK_to_REAL2 pp2 by Def01;
consider pp3 be Element of BK_model such that
A21: x = pp3 and
A22: BK_to_T2 x = BK_to_REAL2 pp3 by Def01;
thus tq = BK_to_T2 q1 by A17,A18,Th63;
thus ta = BK_to_T2 a1 by A19,A20,Th63;
thus tx = BK_to_T2 x by Th63,A21,A22;
end;
hence thesis by A16,Th05;
end;
ex h being Element of SubGroupK-isometry st
ex N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).a1 = b1 & homography(N).x = c1
proof
A23: h = homography(N);
reconsider M = N~ as invertible Matrix of 3,F_Real;
reconsider g = homography(M) as Element of SubGroupK-isometry
by A23,BKMODEL2:47;
take g;
ex N being invertible Matrix of 3,F_Real st
g = homography(N) & homography(N).a1 = b1 &
homography(N).x = c1
proof
take M;
thus thesis by A12,ANPROJ_9:15;
end;
hence thesis;
end;
hence a1,x equiv b1,c1 by BKMODEL3:def 8;
end;
hence thesis;
end;
end;
q = a implies ex x being POINT of BK-model-Plane st between Q,A,x &
A,x equiv B,C
proof
assume
A24: q = a;
consider Q3 be Element of BK_model such that
A25: a <> Q3 by BKMODEL3:11;
reconsider q3 = Q3 as Element of BK-model-Plane;
consider x be POINT of BK-model-Plane such that
between q3,A,x and
A26: A,x equiv B,C by A25,A1,A5;
take x;
between BK_to_T2 A,BK_to_T2 A,BK_to_T2 x by GTARSKI1:17;
hence thesis by A26,A1,A24,A2,Th05;
end;
hence thesis by A1,A2,A5;
end;
suppose
A27: b = c;
set X = A;
take X;
between BK_to_T2 Q,BK_to_T2 A,BK_to_T2 X by GTARSKI1:14;
hence between Q,A,X by Th05;
thus A,A equiv B,C by A27,A3,A4,Th60;
end;
end;
theorem Th65:
for P,Q being POINT of BK-model-Plane st BK_to_T2 P = BK_to_T2 Q holds P = Q
proof
let P,Q be POINT of BK-model-Plane;
assume
A1: BK_to_T2 P = BK_to_T2 Q;
(ex q be Element of BK_model st Q = q &
BK_to_T2 Q = BK_to_REAL2 q) &
(ex p be Element of BK_model st P = p &
BK_to_T2 P = BK_to_REAL2 p) by Def01;
hence thesis by A1,BKMODEL2:4;
end;
theorem
for a,b,r being Real
for P,Q,R being Element of TOP-REAL 2 st
P in inside_of_circle(a,b,r) & R in inside_of_circle(a,b,r) holds
LSeg(P,R) c= inside_of_circle(a,b,r) by Th15;
begin :: SegmentConstruction
theorem
BK-model-Plane is satisfying_SegmentConstruction by Th64;
begin :: BetweennessIdentity
theorem
BK-model-Plane is satisfying_BetweennessIdentity
proof
let P,Q be POINT of BK-model-Plane;
assume
A1: between P,Q,P;
reconsider P2 = BK_to_T2 P, Q2 = BK_to_T2 Q as POINT of TarskiEuclid2Space;
between P2,Q2,P2 by A1,Th05;
hence thesis by GTARSKI1:def 10,Th65;
end;
begin :: Pasch
theorem
BK-model-Plane is satisfying_Pasch
proof
let A,B,P,Q,Z be POINT of BK-model-Plane;
assume that
A1: between A,P,Z and
A2: between B,Q,Z;
reconsider a = A,b = B,p = P,q = Q,z = Z as Element of BK_model;
reconsider A2 = BK_to_T2 A, B2 = BK_to_T2 B, P2 = BK_to_T2 P,
Q2 = BK_to_T2 Q, Z2 = BK_to_T2 Z as POINT of TarskiEuclid2Space;
between A2,P2,Z2 & between B2,Q2,Z2 by A1,A2,Th05;
then consider X2 be POINT of TarskiEuclid2Space such that
A3: between P2,X2,B2 and
A4: between Q2,X2,A2 by GTARSKI1:def 11;
reconsider X = T2_to_BK X2 as POINT of BK-model-Plane;
A5: Tn2TR X2 in LSeg(Tn2TR P2,Tn2TR B2) by A3,GTARSKI2:20;
set P9 = Tn2TR P2, B9 = Tn2TR B2;
P9 in inside_of_circle(0,0,1) & B9 in inside_of_circle(0,0,1) by Th02;
then Tn2TR X2 is Element of inside_of_circle(0,0,1) by A5,Th15;
then X2 = BK_to_T2 X by Th03;
then between P,X,B & between Q,X,A by A3,A4,Th05;
hence thesis;
end;