bkmodel4.miz
begin
theorem ::
BKMODEL4:1
Th25: for a,b be
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 ::
BKMODEL4:2
for a,b be
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 ::
BKMODEL4:3
Th31: for a,b,c be
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 ::
BKMODEL4:4
Th32: for a,b,c be
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 ::
BKMODEL4:5
Th33: for a,b,c,d be
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 ::
BKMODEL4:6
Th35: for u be
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 ::
BKMODEL4:7
Th01: for P be
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 ;
::
BKMODEL4:def1
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));
::
BKMODEL4:def2
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 ::
BKMODEL4:8
Th02: for P be
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 ::
BKMODEL4:9
for P be
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,
EUCLID_5: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 ::
BKMODEL4:10
Th03: for P be
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,
EUCLID_5:def 2;
hence thesis by
A5,
A8,
A3;
end;
theorem ::
BKMODEL4:11
Th04: for P be
Point of
BK-model-Plane holds for p be
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 ::
BKMODEL4:12
Th05: for P,Q,R be
Point of
BK-model-Plane holds for P2,Q2,R2 be
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 ::
BKMODEL4:13
Th06: for P,Q be
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 ::
BKMODEL4:14
Th07: for a,b be
Real holds for P,Q be
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 ::
BKMODEL4:15
Th08: for P,Q be
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;
::
BKMODEL4:def3
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 ::
BKMODEL4:16
Th09: for P,Q be
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 ::
BKMODEL4:17
for P,Q be
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 ::
BKMODEL4:18
for N be
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;
hence thesis by
LAPLACE: 34;
end;
theorem ::
BKMODEL4:19
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 be
Element of
F_Real holds for A,B be
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 ::
BKMODEL4:20
Th11: for N1,N2 be
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 ::
BKMODEL4:21
Th12: for N1,N2 be
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 ::
BKMODEL4:22
Th13: for N1,N2 be
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 ::
BKMODEL4:23
Th14: for N be
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) & not u is
zero & u
= uf & p
= (N
* uf) & v
= (
M2F p) & not v is
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,
EUCLID_5:def 2,
EUCLID_5: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 ::
BKMODEL4:24
for N be
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) & not u is
zero & u
= uf & p
= (N
* uf) & v
= (
M2F p) & not v is
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,
EUCLID_5:def 2,
EUCLID_5: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 ::
BKMODEL4:25
Th15: for a,b,r be
Real holds for P,Q,R be
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;
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 ::
BKMODEL4:26
Th16: for u,v be 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 ::
BKMODEL4:27
Th17: for R be
Element of (
ProjectiveSpace (
TOP-REAL 3)) holds for P,Q be
Element of
BK_model holds for u,v,w be non
zero
Element of (
TOP-REAL 3) holds for r be
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 be
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 ::
BKMODEL4:28
Th18: for N be
invertible
Matrix of 3,
F_Real holds for n11,n12,n13,n21,n22,n23,n31,n32,n33 be
Element of
F_Real holds for P,Q be
Point of (
ProjectiveSpace (
TOP-REAL 3)) holds for u,v be 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 be 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) & not u9 is
zero & u9
= uf & p
= (N
* uf) & v9
= (
M2F p) & not v9 is
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,
EUCLID_5:def 2,
EUCLID_5: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 ::
BKMODEL4:29
Th19: for N be
invertible
Matrix of 3,
F_Real holds for n11,n12,n13,n21,n22,n23,n31,n32,n33 be
Element of
F_Real holds for P be
Element of
BK_model holds for Q be
Point of (
ProjectiveSpace (
TOP-REAL 3)) holds for u,v be 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 ::
BKMODEL4:30
Th20: for N be
invertible
Matrix of 3,
F_Real holds for h be
Element of
SubGroupK-isometry holds for n11,n12,n13,n21,n22,n23,n31,n32,n33 be
Element of
F_Real holds for P be
Element of
BK_model holds for u be 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 ::
BKMODEL4:31
Th21: for N be
invertible
Matrix of 3,
F_Real holds for n11,n12,n13,n21,n22,n23,n31,n32,n33 be
Element of
F_Real holds for P be
Element of
absolute holds for Q be
Point of (
ProjectiveSpace (
TOP-REAL 3)) holds for u,v be 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 ::
BKMODEL4:32
Th22: for N be
invertible
Matrix of 3,
F_Real holds for h be
Element of
SubGroupK-isometry holds for n11,n12,n13,n21,n22,n23,n31,n32,n33 be
Element of
F_Real holds for P be
Element of
absolute holds for u be 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 ::
BKMODEL4:33
Th23: for N be
invertible
Matrix of 3,
F_Real holds for h be
Element of
SubGroupK-isometry holds for n11,n12,n13,n21,n22,n23,n31,n32,n33 be
Element of
F_Real holds for P be
Element of
BK_model holds for u be 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,
EUCLID_5:def 2,
EUCLID_5:def 3;
hence thesis by
A2,
EUCLID_5: 3;
end;
theorem ::
BKMODEL4:34
Th24: for N be
invertible
Matrix of 3,
F_Real holds for h be
Element of
SubGroupK-isometry holds for n11,n12,n13,n21,n22,n23,n31,n32,n33 be
Element of
F_Real holds for P be
Element of
absolute holds for u be 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,
EUCLID_5:def 2,
EUCLID_5:def 3;
thus ((
homography N)
. P)
= (
Dir
|[(v
`1 ), (v
`2 ), (v
`3 )]|) by
A3,
EUCLID_5: 3;
end;
hence thesis;
end;
theorem ::
BKMODEL4:35
Th26: for A be
Subset of (
TOP-REAL 3) holds for B be
convex non
empty
Subset of (
TOP-REAL 2) holds for r be
Real holds for x be
Element of (
TOP-REAL 3) st A
= { x where x be
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 be
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 ::
BKMODEL4:36
Th27: for n1,n2,n3 be
Element of
F_Real holds for n,u be
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 ::
BKMODEL4:37
Th28: for A be
convex non
empty
Subset of (
TOP-REAL 3) holds for n,u,v be
Element of (
TOP-REAL 3) st (for w be
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 ::
BKMODEL4:38
Th29: for n31,n32,n33 be
Element of
F_Real holds for u,v be
Element of (
TOP-REAL 2) st u
in (
inside_of_circle (
0 ,
0 ,1)) & v
in (
inside_of_circle (
0 ,
0 ,1)) & (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 ) 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 be
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 ::
BKMODEL4:39
Th30: for n31,n32,n33 be
Element of
F_Real holds for u,v be
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 be
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,
TOPREAL9: 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 ::
BKMODEL4:40
Th34: for l,r be
Real holds for u,v,w be
Element of (
TOP-REAL 3) holds for n11,n12,n13,n21,n22,n23,n31,n32,n33,nu1,nu2,nu3,nv1,nv2,nv3,nw1,nw2,nw3 be
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 ::
BKMODEL4:41
for N be
invertible
Matrix of 3,
F_Real holds for h be
Element of
SubGroupK-isometry holds for n11,n12,n13,n21,n22,n23,n31,n32,n33 be
Element of
F_Real holds for P be
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 ::
BKMODEL4:42
Th36: for h be
Element of
SubGroupK-isometry holds for N be
invertible
Matrix of 3,
F_Real holds for n11,n12,n13,n21,n22,n23,n31,n32,n33 be
Element of
F_Real holds for u2 be
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 ::
BKMODEL4:43
Th37: for r be
positive
Real holds for u be
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 ::
BKMODEL4:44
Th38: for h be
Element of
SubGroupK-isometry holds for N be
invertible
Matrix of 3,
F_Real holds for n11,n12,n13,n21,n22,n23,n31,n32,n33 be
Element of
F_Real holds for u2 be
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;
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 ::
BKMODEL4:45
Th39: for a,b,c,d,e,f,r be
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 ::
BKMODEL4:46
for P,Q,R,P9,Q9,R9 be
POINT of
BK-model-Plane holds for p,q,r,p9,q9,r9 be
Element of
BK_model holds for h be
Element of
SubGroupK-isometry holds for N be
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 be
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));
::
BKMODEL4:def4
attr P is
point_at_infty means
:
Def04: ex u be non
zero
Element of (
TOP-REAL 3) st P
= (
Dir u) & (u
`3 )
=
0 ;
end
theorem ::
BKMODEL4:47
Th40: for P be
Point of (
ProjectiveSpace (
TOP-REAL 3)) st ex u be 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 be non
point_at_infty
Point of (
ProjectiveSpace (
TOP-REAL 3));
::
BKMODEL4:def5
func
RP3_to_REAL2 P ->
Element of (
REAL 2) means
:
Def05: ex u be 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: not u is
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));
::
BKMODEL4:def6
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 ::
BKMODEL4:48
Th41: for P,Q,R,P9,Q9,R9 be non
point_at_infty
Element of (
ProjectiveSpace (
TOP-REAL 3)) holds for h be
Element of
SubGroupK-isometry holds for N be
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 be
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 ::
BKMODEL4:49
Th42: for a,b,c be
Real holds for u,v,w be
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 be
Real by
A4;
hence thesis by
RLTOPSP1:def 14;
end;
theorem ::
BKMODEL4:50
Th43: for P,Q,R be non
point_at_infty
Point of (
ProjectiveSpace (
TOP-REAL 3)) holds for u,v,w be 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) & not u9 is
zero & not v9 is
zero & not w9 is
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,
EUCLID_5: 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 ;
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 ::
BKMODEL4:51
Th44: for u,v,w be
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 be
Real :
0
<= r & r
<= 1 } by
A1,
A2;
hence thesis by
RLTOPSP1:def 2;
end;
theorem ::
BKMODEL4:52
Th45: for u,v,w be
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 be
Real :
0
<= r & r
<= 1 } by
A1,
A2;
hence thesis by
RLTOPSP1:def 2;
end;
theorem ::
BKMODEL4:53
Th46: for P,Q,R be 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;
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 ::
BKMODEL4:54
for u,v,w be
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 ::
BKMODEL4:55
Th47: for P,Q,P1 be non
point_at_infty
Element of (
ProjectiveSpace (
TOP-REAL 3)) st P
in
BK_model & Q
in
BK_model & P1
in
absolute 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
::
BKMODEL4:def7
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
::
BKMODEL4:def8
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 ::
BKMODEL4:56
for P,Q be 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,
SQUARE_1: 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,
SQUARE_1: 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 ::
BKMODEL4:57
Th48: for P,Q,R be non
point_at_infty
Element of (
ProjectiveSpace (
TOP-REAL 3)) holds for u,v,w be 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,
EUCLID_5:def 2;
then (u
`1 )
= (v
`1 ) & (u
`2 )
= (v
`2 ) by
EUCLID_5:def 1,
EUCLID_5: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,
EUCLID12: 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 ::
BKMODEL4:58
Th49: for R1,R2 be
Point of
TarskiEuclid2Space st (
Tn2TR R1)
in (
circle (
0 ,
0 ,1)) & (
Tn2TR R2)
in (
circle (
0 ,
0 ,1)) & R1
<> R2 holds ex P be
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,
EUCLID_5: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 be
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,
EUCLID_5: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,
EUCLID_5: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 ::
BKMODEL4:59
Th50: for P,Q be 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 ::
BKMODEL4:60
Th51: for R1,R2 be non
point_at_infty
Element of (
ProjectiveSpace (
TOP-REAL 3)) st R1
in
absolute & R2
in
absolute & R1
<> R2 holds ex P be
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 ::
BKMODEL4:61
Th52: for P,Q,R be
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 ::
BKMODEL4:62
Th53: for P be 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 ::
BKMODEL4:63
for P be 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 ::
BKMODEL4:64
Th54: for P be non
point_at_infty
Point of (
ProjectiveSpace (
TOP-REAL 3)) holds for Q be
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 ::
BKMODEL4:65
Th55: for P,Q,R1,R2 be 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;
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 ::
BKMODEL4:66
Th56: for P,Q,P1,P2 be 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 ::
BKMODEL4:67
Th57: for P,Q be
Element of
BK_model st P
<> Q holds ex R be
Element of
absolute st (for p,q,r be 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: not u is
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: not v is
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 ::
BKMODEL4:68
Th58: for P,Q be
Element of
BK_model st P
<> Q holds ex R be
Element of
absolute st (for p,q,r be 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 be 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 ::
BKMODEL4:69
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 ::
BKMODEL4:70
Th60: for a,b be
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 be
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 be
Element of
SubGroupK-isometry st ex N be
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 ::
BKMODEL4:71
Th61: for P be
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: not u is
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 ::
BKMODEL4:72
Th62: for P be
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 ::
BKMODEL4:73
Th63: for P be
Element of
BK_model holds for P9 be 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,
EUCLID_5:def 2;
hence thesis by
A2,
A3;
end;
theorem ::
BKMODEL4:74
Th64: for a,q,b,c be
POINT of
BK-model-Plane holds ex x be
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 be
POINT of
BK-model-Plane st q1
<> a1 holds ex x be
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 be 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 be 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 be
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 be
Element of
SubGroupK-isometry st ex N be
invertible
Matrix of 3,
F_Real st h
= (
homography N) & ((
homography N)
. a1)
= b1 & ((
homography N)
. 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 be
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 be
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 ::
BKMODEL4:75
Th65: for P,Q be
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 ::
BKMODEL4:76
for a,b,r be
Real holds for P,Q,R be
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
theorem ::
BKMODEL4:77
BK-model-Plane is
satisfying_SegmentConstruction by
Th64;
begin
theorem ::
BKMODEL4:78
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
theorem ::
BKMODEL4:79
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;