:: Beltrami-Klein model, Part {II}
:: by Roland Coghetto
::
:: Received March 27, 2018
:: Copyright (c) 2018-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FVSUM_1, NAT_1, TREES_1, MATRIX_6, FINSEQ_2, COMPLEX1, REAL_1,
XCMPLX_0, ANPROJ_1, PENCIL_1, MCART_1, EUCLID_5, ALGSTR_0, ARYTM_1,
ARYTM_3, CARD_1, EUCLID, FUNCT_1, INCSP_1, MATRIX_1, NUMBERS, PRE_TOPC,
RELAT_1, STRUCT_0, SUBSET_1, SUPINF_2, VECTSP_1, XBOOLE_0, MESFUNC1,
ANPROJ_8, GROUP_1, MONOID_0, ANPROJ_9, TARSKI, XXREAL_0, PASCAL, INCPROJ,
ZFMISC_1, GROUP_2, SQUARE_1, JGRAPH_6, PROB_1, RVSUM_1, FINSEQ_1,
QC_LANG1, RELAT_2, MATRIXR1, MATRIXC1, MATRIX_3, FUNCT_3, CARD_3,
BKMODEL1, BKMODEL2, COLLSP;
notations GCD_1, FVSUM_1, RELSET_1, ORDINAL1, XCMPLX_0, PRE_TOPC,
RVSUM_1, TARSKI, GROUP_1, XBOOLE_0, RLVECT_1, COLLSP, EUCLID_5,
PASCAL, XXREAL_0, INCPROJ, DOMAIN_1, INCSP_1, ANPROJ_9, SQUARE_1,
XREAL_0, JGRAPH_6, TOPREAL9, ZFMISC_1, SUBSET_1, NUMBERS, FUNCT_1,
FUNCT_2, FINSEQ_1, STRUCT_0, ALGSTR_0, VECTSP_1, FINSEQ_2, EUCLID,
ANPROJ_1, MATRIX_0, MATRIX_6, LAPLACE, ANPROJ_8, GROUP_2,
MATRIX_1, MATRIX_3, MATRIXR1, MATRIXR2, MATRPROB, QUIN_1,
BKMODEL1;
constructors GROUP_1, VECTSP_2, GCD_1, REALSET1, MATRIXR2, FINSEQ_4, FVSUM_1,
LAPLACE, MATRPROB, GROUP_5, RELSET_1, MONOID_0, EUCLID_5,
MATRIX13, ANPROJ_8, PASCAL, INCPROJ, ANPROJ_9, SQUARE_1, TOPREAL9,
BINOP_2, QUIN_1, BKMODEL1, MATRIX_3;
registrations SUBSET_1, RVSUM_1, FUNCT_1, MEMBERED, FINSEQ_1, ORDINAL1,
XXREAL_0, GROUP_2, XBOOLE_0, ANPROJ_1, STRUCT_0, VECTSP_1, REVROT_1,
RELSET_1, XREAL_0, MONOID_0, EUCLID, VALUED_0, MATRIX_6, ANPROJ_2,
ANPROJ_9, SQUARE_1, XCMPLX_0, NUMBERS, MATRIX_0, TOPREAL9, QUIN_1,
MATRIX_3, RING_2, GCD_1;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions TARSKI;
equalities VECTSP_1, STRUCT_0, ALGSTR_0, JGRAPH_6, BKMODEL1, SQUARE_1;
expansions TARSKI, GROUP_2, STRUCT_0, XBOOLE_0, ZFMISC_1;
theorems XREAL_0, MATRIXR2, FINSEQ_3, EUCLID_8, LAPLACE, MATRIX_6, MATRIXR1,
MATRPROB, GROUP_2, XREAL_1, EUCLID_5, ANPROJ_1, EUCLID, XCMPLX_1,
RVSUM_1, FINSEQ_1, MATRIX_3, FUNCT_1, FUNCT_2, ANPROJ_8, GROUP_1,
INCPROJ, ANPROJ_9, PASCAL, TARSKI, XBOOLE_0, SQUARE_1, TOPREAL9,
JGRAPH_1, JGRAPH_3, EUCLID_2, COLLSP, MATRIX_0, FINSEQ_2, ZFMISC_1,
ENUMSET1, RELAT_1, EUCLID_4, HESSENBE, BKMODEL1;
begin :: Beltrami-Cayley-Klein disk model
definition
func BK_model -> non empty Subset of ProjectiveSpace TOP-REAL 3 equals
negative_conic(1,1,-1,0,0,0);
coherence
proof
reconsider u = |[0,0,1]| as non zero Element of TOP-REAL 3 by ANPROJ_9:10;
reconsider P = Dir u as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
qfconic(1,1,-1,0,0,0,u) is negative
proof
qfconic(1,1,-1,0,0,0,u) = 1 * u.1 * u.1 + 1 * u.2 * u.2
+ (-1) * u.3 * u.3 + 0 * u.1 * u.2
+ 0 * u.1 * u.3 + 0 * u.2 * u.3
by PASCAL:def 1
.= -1;
hence thesis;
end;
then for v being Element of TOP-REAL 3 st v is non zero & P = Dir v holds
qfconic(1,1,-1,0,0,0,v) is negative by BKMODEL1:81;
then P in {P where P is Point of ProjectiveSpace TOP-REAL 3:
for u being Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(1,1,-1,0,0,0,u) is negative};
hence thesis;
end;
end;
theorem Th01:
BK_model misses absolute
proof
assume not BK_model misses absolute;
then consider x be object such that
A1: x in BK_model /\ absolute by XBOOLE_0:def 1;
A2: x in BK_model & x in absolute by A1,XBOOLE_0:def 4;
x in {P where P is Point of ProjectiveSpace TOP-REAL 3:
for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(1,1,-1,0,0,0,u) = 0} by A2,PASCAL:def 2;
then consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A3: x = P and
A4: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(1,1,-1,0,0,0,u) = 0;
consider u be Element of TOP-REAL 3 such that
A5: u is non zero and
A6: P = Dir u by ANPROJ_1:26;
consider Q be Point of ProjectiveSpace TOP-REAL 3 such that
A7: x = Q and
A8: for u be Element of TOP-REAL 3 st u is non zero & Q = Dir u holds
qfconic(1,1,-1,0,0,0,u) is negative by A2;
qfconic(1,1,-1,0,0,0,u) = 0 &
qfconic(1,1,-1,0,0,0,u) is negative by A3,A4,A5,A6,A7,A8;
hence contradiction;
end;
theorem
for P being Element of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st
P = Dir u & P in BK_model holds u.3 <> 0
proof
let P be Element of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
assume that
A1: P = Dir u and
A2: P in BK_model;
assume
A3: u.3 = 0;
consider Q be Point of ProjectiveSpace TOP-REAL 3 such that
A4: P = Q and
A5: for u be Element of TOP-REAL 3 st u is non zero & Q = Dir u holds
qfconic(1,1,-1,0,0,0,u) is negative by A2;
A6: qfconic(1,1,-1,0,0,0,u) is negative by A1,A4,A5;
qfconic(1,1,-1,0,0,0,u) = 1 * u.1 * u.1 + 1 * u.2 * u.2
+ (- 1) * u.3 * u.3 + 0 * u.1 * u.2
+ 0 * u.1 * u.3 + 0 * u.2 * u.3
by PASCAL:def 1
.= (u.1)^2 + (u.2)^2 by A3;
then u.1 = 0 & u.2 = 0 by A6,BKMODEL1:19;
then u`1 = 0 & u`2 = 0 & u`3 = 0 by A3,EUCLID_5:def 1,def 2,def 3;
hence contradiction by EUCLID_5:3,4;
end;
definition
let P being Element of BK_model;
func BK_to_REAL2 P -> Element of inside_of_circle(0,0,1) means
:Def01:
ex u being non zero Element of TOP-REAL 3 st
Dir u = P & u.3 = 1 & it = |[u.1,u.2]|;
existence
proof
P in {P where P is Point of ProjectiveSpace TOP-REAL 3:
for u being Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(1,1,-1,0,0,0,u) is negative};
then consider Q be Point of ProjectiveSpace TOP-REAL 3 such that
A1: P = Q and
A2: for u being Element of TOP-REAL 3 st u is non zero & Q = Dir u holds
qfconic(1,1,-1,0,0,0,u) is negative;
consider u be Element of TOP-REAL 3 such that
A3: u is not zero and
A4: P = Dir u by ANPROJ_1:26;
reconsider u1 = u.1,u2 = u.2,u3 = u.3 as Real;
qfconic(1,1,-1,0,0,0,u) = 1 * u.1 * u.1 + 1 * u.2 * u.2
+ (-1) * u.3 * u.3 + 0 * u.1 * u.2
+ 0 * u.1 * u.2 + 0 * u.2 * u.3
by PASCAL:def 1
.= (u.1)^2 + (u.2)^2 - (u.3)^2;
then u1^2 + u2^2 - u3^2 < 0 by A1,A3,A4,A2; then
A5: u1^2 + u2^2 - u3^2 + u3^2 < 0 + u3^2 by XREAL_1:6;
A6: u.3 <> 0
proof
assume
A7: u.3 = 0;
A8: qfconic(1,1,-1,0,0,0,u) = 1 * u.1 * u.1 + 1 * u.2 * u.2
+ (-1) * u.3 * u.3 + 0 * u.1 * u.2
+ 0 * u.1 * u.2 + 0 * u.2 * u.3
by PASCAL:def 1
.= u1^2 + u2^2 by A7;
0^2 = 0;
then 0 <= u1^2 & 0 <= u2^2 by SQUARE_1:12;
hence contradiction by A1,A3,A4,A2,A8;
end;
reconsider k = 1/(u3^2) as Real;
0 < u3^2 by A6,SQUARE_1:12; then
A10: (u1^2 + u2^2) * k < u3^2 * k by A5,XREAL_1:68;
A11: u1^2 * k = (u1 / u3)^2 & u2^2 * k = (u2 / u3)^2 by BKMODEL1:12;
|[u.1 / u.3,u.2 / u.3, 1]| <> 0.TOP-REAL 3
proof
assume |[u.1 / u.3,u.2 / u.3, 1]| = 0.TOP-REAL 3;
then 1 = |[0,0,0]|`3 by EUCLID_5:2,4;
hence contradiction by EUCLID_5:2;
end;
then |[u.1 / u.3,u.2 / u.3, 1]| is non zero;
then reconsider v = |[u.1 / u.3,u.2 / u.3, 1]|
as non zero Element of TOP-REAL 3;
A14: u.3 * (u.1 / u.3) = u.1 & u.3 * (u.2 / u.3) = u.2 by A6,XCMPLX_1:87;
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.2,u.3]| by A14,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
.= u by EUCLID_5:3;
then are_Prop v,u by A6,ANPROJ_1:1; then
A15: P = Dir v by A3,A4,ANPROJ_1:22;
|[v.1,v.2]| in inside_of_circle(0,0,1)
proof
reconsider t = |[v.1,v.2]| as Element of TOP-REAL 2;
|. t - |[0,0]| .| < 1
proof
A16: |. t - |[0,0]| .| = |. |[v.1 - 0,v.2 - 0]| .| by EUCLID:62
.= |. t .|;
A17: v.1 = t`1 & v.2 = t`2 by EUCLID:52;
|. t .|^2 = (u1^2 * k) + (u2^2 * k) by A17,JGRAPH_1:29,A11;
then |. t .|^2 < 1^2 by A10,A6,XCMPLX_1:106;
hence thesis by A16,SQUARE_1:48;
end;
hence thesis;
end;
then reconsider w = |[v.1,v.2]| as Element of inside_of_circle(0,0,1);
take w;
v.3 = v`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
hence thesis by A15;
end;
uniqueness
proof
let P1,P2 be Element of inside_of_circle(0,0,1) such that
A18: ex u be non zero Element of TOP-REAL 3 st
Dir u = P & u.3 = 1 & P1 = |[u.1,u.2]| and
A19: ex u be non zero Element of TOP-REAL 3 st
Dir u = P & u.3 = 1 & P2 = |[u.1,u.2]|;
consider u be non zero Element of TOP-REAL 3 such that
A20: Dir u = P & u.3 = 1 & P1 = |[u.1,u.2]| by A18;
consider v be non zero Element of TOP-REAL 3 such that
A21: Dir v = P & v.3 = 1 & P2 = |[v.1,v.2]| by A19;
are_Prop u,v by A20,A21,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A22: u = a * v by ANPROJ_1:1;
1 = a * v.3 by A20,A22,RVSUM_1:44
.= a by A21;
then u = v by A22,RVSUM_1:52;
hence thesis by A20,A21;
end;
end;
definition
let Q being Element of inside_of_circle(0,0,1);
func REAL2_to_BK Q -> Element of BK_model means
:Def02:
ex P being Element of TOP-REAL 2 st P = Q & it = Dir |[P`1,P`2,1]|;
existence
proof
reconsider P = Q as Element of TOP-REAL 2;
A1: |. P - |[0,0]| .| = |. |[P`1,P`2]| - |[0,0]| .| by EUCLID:53
.= |. |[P`1 - 0,P`2 - 0]| .| by EUCLID:62
.= |. P .| by EUCLID:53;
1^2 = 1;
then |. P .|^2 < 1 by TOPREAL9:45,A1,SQUARE_1:16;
then (P`1)^2 + (P`2)^2 < 1 by JGRAPH_3:1; then
A2: (P`1)^2 + (P`2)^2 - 1 < 1 - 1 by XREAL_1:14;
A3: |[P`1,P`2,1]| is non zero by EUCLID_5:4,FINSEQ_1:78;
then reconsider R = Dir |[P`1,P`2,1]|
as Element of ProjectiveSpace TOP-REAL 3 by ANPROJ_1:26;
for u being Element of TOP-REAL 3 st u is non zero & R = Dir u holds
qfconic(1,1,-1,0,0,0,u) is negative
proof
let u be Element of TOP-REAL 3;
assume that
A4: u is non zero and
A5: R = Dir u;
are_Prop u,|[P`1,P`2,1]| by A3,A4,A5,ANPROJ_1:22;
then consider k be Real such that
A6: k <> 0 and
A7: u = k * |[P`1,P`2,1]| by ANPROJ_1:1;
|[P`1,P`2,1]|.1 = |[P`1,P`2,1]|`1 by EUCLID_5:def 1
.= P`1 by EUCLID_5:2;
then
A8: u.1 = k * P`1 by A7,RVSUM_1:44;
|[P`1,P`2,1]|.2 = |[P`1,P`2,1]|`2 by EUCLID_5:def 2
.= P`2 by EUCLID_5:2;
then
A9: u.2 = k * P`2 by A7,RVSUM_1:44;
|[P`1,P`2,1]|.3 = |[P`1,P`2,1]|`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
then
A10: u.3 = k * 1 by A7,RVSUM_1:44;
A11: qfconic(1,1,-1,0,0,0,u) = 1 * u.1 * u.1 + 1 * u.2 * u.2 +
(-1) * u.3 * u.3 + 0 * u.1 * u.2 +
0 * u.1 * u.3 + 0 * u.2 * 1 by PASCAL:def 1
.= k^2 * ((P`1)^2 + (P`2)^2 - 1) by A8,A9,A10;
0 < k^2 by A6,SQUARE_1:12;
hence thesis by A11,A2;
end;
then R in {P where P is Point of ProjectiveSpace TOP-REAL 3:
for u being Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(1,1,-1,0,0,0,u) is negative};
hence thesis;
end;
uniqueness;
end;
theorem
for P being Element of BK_model holds REAL2_to_BK BK_to_REAL2 P = P
proof
let P be Element of BK_model;
consider u be non zero Element of TOP-REAL 3 such that
A1: Dir u = P and
A2: u.3 = 1 and
A3: BK_to_REAL2 P = |[u.1,u.2]| by Def01;
consider Q be Element of TOP-REAL 2 such that
A4: Q = BK_to_REAL2 P and
A5: REAL2_to_BK BK_to_REAL2 P = Dir |[Q`1,Q`2,1]| by Def02;
A6: |[Q`1,Q`2,1]| is non zero by EUCLID_5:4,FINSEQ_1:78;
are_Prop |[Q`1,Q`2,1]|,u
proof
A7: Q`1 = u.1 & Q`2 = u.2 by A3,A4,EUCLID:52;
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;
hence thesis by A2,A7;
end;
hence thesis by A1,A5,A6,ANPROJ_1:22;
end;
theorem Th02:
for P,Q being Element of BK_model holds P = Q iff
BK_to_REAL2 P = BK_to_REAL2 Q
proof
let P,Q be Element of BK_model;
thus P = Q implies BK_to_REAL2 P = BK_to_REAL2 Q;
assume
A1: BK_to_REAL2 P = BK_to_REAL2 Q;
consider u be non zero Element of TOP-REAL 3 such that
A2: Dir u = P & u.3 = 1 & BK_to_REAL2 P = |[u.1,u.2]| by Def01;
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 Def01;
u.1 = v.1 & u.2 = v.2 & u.3 = v.3 by A1,A2,A3,FINSEQ_1:77;
then u`1 = v.1 & u`2 = v.2 & u`3 = v.3 by EUCLID_5:def 1,def 2,def 3; then
A4: u`1 = v`1 & u`2 = v`2 & u`3 = v`3 by EUCLID_5:def 1,def 2,def 3;
u = |[u`1,u`2,u`3]| & v = |[v`1,v`2,v`3]| by EUCLID_5:3;
hence thesis by A2,A3,A4;
end;
theorem
for Q being Element of inside_of_circle(0,0,1) holds
BK_to_REAL2 REAL2_to_BK Q = Q
proof
let Q be Element of inside_of_circle(0,0,1);
consider P be Element of TOP-REAL 2 such that
A1: P = Q and
A2: REAL2_to_BK Q = Dir |[P`1,P`2,1]| by Def02;
consider u be non zero Element of TOP-REAL 3 such that
A3: Dir u = REAL2_to_BK Q and
A4: u.3 = 1 and
A5: BK_to_REAL2 REAL2_to_BK Q = |[u.1,u.2]| by Def01;
|[P`1,P`2,1]| is non zero by EUCLID_5:4,FINSEQ_1:78;
then are_Prop |[P`1,P`2,1]|,u by A2,A3,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A6: |[P`1,P`2,1]| = a * u by ANPROJ_1:1;
A7: a = a * u.3 by A4
.= (a * u).3 by RVSUM_1:44
.= |[P`1,P`2,1]|`3 by A6,EUCLID_5:def 3
.= 1 by EUCLID_5:2;
A8: |[P`1,P`2,1]| = u by A7,RVSUM_1:52,A6; then
A9: P`1 = u`1 by EUCLID_5:2
.= u.1 by EUCLID_5:def 1;
P`2 = u`2 by A8,EUCLID_5:2
.= u.2 by EUCLID_5:def 2;
hence thesis by A9,A5,A1,EUCLID:53;
end;
theorem
for P,Q being Element of BK_model for P1,P2,P3 being Element of absolute st
P <> Q & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear &
P,Q,P3 are_collinear holds P3 = P1 or P3 = P2
proof
let P,Q being Element of BK_model;
let P1,P2,P3 being Element of absolute;
assume that
A1: P <> Q and
A2: P1 <> P2 and
A3: P,Q,P1 are_collinear and
A4: P,Q,P2 are_collinear and
A5: P,Q,P3 are_collinear;
P3 = P1 or P3 = P2
proof
assume P3 <> P1 & P3 <> P2;
then P1,P2,P3 are_mutually_distinct by A2;
hence contradiction by A1,A3,A4,A5,COLLSP:3,BKMODEL1:92;
end;
hence thesis;
end;
theorem Th03:
for P being Element of BK_model
for Q being Element of ProjectiveSpace TOP-REAL 3
for v being non zero Element of TOP-REAL 3 st P <> Q & Q = Dir v &
v.3 = 1 holds
ex P1 being Element of absolute st P,Q,P1 are_collinear
proof
let P be Element of BK_model;
let Q be Element of ProjectiveSpace TOP-REAL 3;
let v be non zero Element of TOP-REAL 3;
assume that
A1: P <> Q and
A2: Q = Dir v and
A3: v.3 = 1;
consider u be non zero Element of TOP-REAL 3 such that
A4: Dir u = P & u.3 = 1 & BK_to_REAL2 P = |[u.1,u.2]| by Def01;
reconsider s = |[u.1,u.2]|,
t = |[v.1,v.2]| as Point of TOP-REAL 2;
set a = 0,
b = 0,
r = 1;
reconsider S = s,
T = t,
X = |[a,b]| as Element of REAL 2 by EUCLID:22;
reconsider w1 = ((- (2 * |((t - s),(s - |[a,b]|))|))
+ (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),
((Sum (sqr (S - X))) - (r ^2))))))
/ (2 * (Sum (sqr (T - S)))) as Real;
A5: s <> t
proof
assume s = t;
then u.1 = v.1 & u.2 = v.2 by FINSEQ_1:77;
then u`1 = v.1 & u`2 = v.2 & u`3 = v.3
by EUCLID_5:def 1,def 2,def 3,A4,A3;
then
A6: u`1 = v`1 & u`2 = v`2 & u`3 = v`3 by EUCLID_5:def 1,def 2,def 3;
u = |[u`1,u`2,u`3]| by EUCLID_5:3
.= v by A6,EUCLID_5:3;
hence contradiction by A4,A1,A2;
end;
consider e1 be Point of (TOP-REAL 2) such that
A7: ( {e1} = (halfline (s,t)) /\ (circle (a,b,r)) &
e1 = ((1 - w1) * s) + (w1 * t)) by A5,A4,TOPREAL9:58;
reconsider f = |[e1`1,e1`2,1]| as Element of TOP-REAL 3;
f is non zero by FINSEQ_1:78,EUCLID_5:4;
then reconsider ee1 = f as non zero Element of TOP-REAL 3;
A8: s.1 = u.1 & s.2 = u.2 & t.1 = v.1 & t.2 = v.2;
reconsider P1 = Dir ee1 as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
1 * ee1 + (-(1 - w1)) * u + (- w1) * v = 0.TOP-REAL 3
proof
A9: 1 * ee1 = |[1 * ee1`1,1 * ee1`2, 1 * ee1`3 ]| by EUCLID_5:7
.= ee1 by EUCLID_5:3;
ee1 = (1 - w1) * u + w1 * v
proof
A10: (1 - w1) * s + (w1 * t) = |[((1 - w1) * s + (w1 * t))`1,
((1 - w1) * s + (w1 * t))`2]|
by EUCLID:53;
(1 - w1) * s + (w1 * t) = |[((1 - w1) * s)`1 + (w1 * t)`1,
((1 - w1) * s)`2 + (w1 * t)`2]|
by EUCLID:55
.= |[((1 - w1) * s).1 + (w1 * t)`1,
((1 - w1) * s)`2 + (w1 * t)`2]|
by EUCLID:def 9
.= |[((1 - w1) * s).1 + (w1 * t).1,
((1 - w1) * s)`2 + (w1 * t)`2]|
by EUCLID:def 9
.= |[((1 - w1) * s).1 + (w1 * t).1,
((1 - w1) * s).2 + (w1 * t)`2]|
by EUCLID:def 10
.= |[((1 - w1) * s).1 + (w1 * t).1,
((1 - w1) * s).2 + (w1 * t).2]|
by EUCLID:def 10
.= |[(1 - w1) * s.1 + (w1 * t).1,
((1 - w1) * s).2 + (w1 * t).2]|
by RVSUM_1:44
.= |[(1 - w1) * s.1 + w1 * t.1,
((1 - w1) * s).2 + (w1 * t).2]| by RVSUM_1:44
.= |[(1 - w1) * s.1 + w1 * t.1,
(1 - w1) * s.2 + (w1 * t).2]| by RVSUM_1:44
.= |[(1 - w1) * u.1 + w1 * v.1,
(1 - w1) * u.2 + w1 * v.2]|
by A8,RVSUM_1:44;
then
A11: e1`1 = (1 - w1) * u.1 + w1 * v.1 & e1`2 = (1 - w1) * u.2 + w1 * v.2
by A7,A10,FINSEQ_1:77;
(1 - w1) * u + w1 * v = |[ (1 - w1) * u.1 + w1 * v.1,
(1 - w1) * u.2 + w1 * v.2,
(1 - w1) * u.3 + w1 * v.3]|
proof
((1 - w1) * u)`1 = (1 - w1) * u`1 by EUCLID_5:9
.= (1 - w1) * u.1
by EUCLID_5:def 1;
then
A12: ((1 - w1) * u)`1 + (w1 * v)`1 = (1 - w1) * u.1 + (w1 * v).1
by EUCLID_5:def 1
.= (1 - w1) * u.1 + w1 * v.1
by RVSUM_1:44;
((1 - w1) * u)`2 = (1 - w1) * u`2 by EUCLID_5:9
.= (1 - w1) * u.2 by EUCLID_5:def 2;
then
A13: ((1 - w1) * u)`2 + (w1 * v)`2 = (1 - w1) * u.2 + (w1 * v).2
by EUCLID_5:def 2
.= (1 - w1) * u.2 + w1 * v.2
by RVSUM_1:44;
((1 - w1) * u)`3 = (1 - w1) * u`3 by EUCLID_5:9
.= (1 - w1) * u.3 by EUCLID_5:def 3;
then ((1 - w1) * u)`3 + (w1 * v)`3 = (1 - w1) * u.3 + (w1 * v).3
by EUCLID_5:def 3
.= (1 - w1) * u.3 + w1 * v.3
by RVSUM_1:44;
hence thesis by A12,A13,EUCLID_5:5;
end;
hence thesis by A11,A4,A3;
end;
then ee1 + (-(1 - w1)) * u + (-w1) * v
= (1 - w1) * u + w1 * v + ((-(1 - w1)) * u + (-w1) * v) by RVSUM_1:15
.= (1 - w1) * u + (w1 * v + ((-(1 - w1)) * u + (-w1) * v))
by RVSUM_1:15
.= (1 - w1) * u + ((-(1 - w1)) * u + (w1 * v + (-w1) * v))
by RVSUM_1:15
.= (((1 - w1) * u + (-(1 - w1)) * u)) + (w1 * v + (-w1) * v)
by RVSUM_1:15
.= 0.TOP-REAL 3 + (w1 * v + (-w1) * v) by BKMODEL1:4
.= 0.TOP-REAL 3 + 0.TOP-REAL 3 by BKMODEL1:4
.= |[0 + 0,0 + 0,0 + 0]| by EUCLID_5:4,6
.= 0.TOP-REAL 3 by EUCLID_5:4;
hence thesis by A9;
end;
then
A14: P1,P,Q are_collinear by A4,A2,ANPROJ_8:11;
e1 in {e1} by TARSKI:def 1;
then
A15: e1 in circle(0,0,1) by A7,XBOOLE_0:def 4;
now
thus |[ee1.1,ee1.2]| in circle(0,0,1) by A15,EUCLID:53;
thus ee1.3 = 1;
end;
then P1 is Element of absolute by BKMODEL1:86;
hence thesis by A14,COLLSP:8;
end;
theorem
for P being Element of BK_model
for L being LINE of IncProjSp_of real_projective_plane
holds ex Q being Element of ProjectiveSpace TOP-REAL 3 st P <> Q & Q in L
proof
let P be Element of BK_model;
let L be LINE of IncProjSp_of real_projective_plane;
consider p,q be Point of real_projective_plane such that
A2: p <> q and
A3: L = Line(p,q) by BKMODEL1:73;
P <> p or P <> q by A2;
hence thesis by A3,COLLSP:10;
end;
theorem Th04:
for a,b,c,d,e being Real
for u,v,w being Element of TOP-REAL 3 st
u = |[a,b,e]| & v = |[c,d,0]| & w = |[ a + c, b + d, e ]| holds
|{u,v,w}| = 0
proof
let a,b,c,d,e be Real;
let u,v,w be Element of TOP-REAL 3;
assume that
A1: u = |[a,b,e]| and
A2: v = |[c,d,0]| and
A3: w = |[ a + c, b + d, e]|;
A4: u`1 = a & u`2 = b & u`3 = e & v`1 = c & v`2 = d & v`3 = 0 &
w`1 = a + c & w`2 = b + d & w`3 = e by A1,A2,A3,EUCLID_5:2;
|{ u,v,w }| = u`1 * v`2 * w`3 - u`3*v`2*w`1 - u`1*v`3*w`2 + u`2*v`3*w`1
- u`2*v`1*w`3 + u`3*v`1*w`2 by ANPROJ_8:27
.= a * d * e - e * d * (a+c) - b * c * e + e * c * (b+d) by A4;
hence thesis;
end;
theorem Th05:
for a,b being Real for c being non zero Real holds
|[a,b,c]| is non zero Element of TOP-REAL 3
proof
let a,b be Real;
let c be non zero Real;
|[a,b,c]| is non zero by EUCLID_5:4,FINSEQ_1:78;
hence thesis;
end;
theorem Th06:
for u,v being Element of TOP-REAL 3 for a,b,c,d,e being Real st
u = |[a,b,c]| & v = |[d,e,0]| & are_Prop u,v holds c = 0
proof
let u,v be Element of TOP-REAL 3;
let a,b,c,d,e be Real;
assume that
A1: u = |[a,b,c]| and
A2: v = |[d,e,0]| and
A3: are_Prop u,v;
consider f be Real such that f <> 0 and
A5: |[a,b,c]| = f * |[d,e,0]| by A1,A2,A3,ANPROJ_1:1;
f * |[d,e,0]| = |[ f * d,f * e, f * 0]| by EUCLID_5:8;
then c = |[ f * d, f * e, f * 0]|`3 by A5,EUCLID_5:2
.= f * 0 by EUCLID_5:2;
hence thesis;
end;
theorem
for P,Q,R being Element of ProjectiveSpace TOP-REAL 3
for u,v,w being non zero Element of TOP-REAL 3 st
P = Dir u & Q = Dir v & R = Dir w & u`3 <> 0 & v`3 = 0 &
w = |[u`1 + v`1,u`2 + v`2, u`3]| holds R <> P & R <> Q
proof
let P,Q,R be Element of ProjectiveSpace TOP-REAL 3;
let u,v,w be non zero Element of TOP-REAL 3;
assume that
A1: P = Dir u and
A2: Q = Dir v and
A3: R = Dir w and
A4: u`3 <> 0 and
A5: v`3 = 0 and
A6: w = |[u`1 + v`1,u`2 + v`2, u`3]|;
hereby
assume R = P;
then are_Prop u,w by A1,A3,ANPROJ_1:22;
then consider a be Real such that a <> 0 and
A7: u = a * w by ANPROJ_1:1;
A8: |[u`1,u`2,u`3]| = u by EUCLID_5:3
.= |[a * w`1,a * w`2,a * w`3]| by A7,EUCLID_5:7;
then |[u`1,u`2,u`3]| = |[a * w`1,a * w`2, a * u`3]| by A6,EUCLID_5:2;
then u`3 = a * u`3 by FINSEQ_1:78;
then
A9: a = 1 by A4,XCMPLX_1:7;
w`1 = u`1 + v`1 & w`2 = u`2 + v`2 & w`3 = u`3 by A6,EUCLID_5:2;
then u`1 = u`1 + v`1 & u`2 = u`2 + v`2 by A8,A9,FINSEQ_1:78;
hence contradiction by A5,EUCLID_5:3,4;
end;
hereby
assume R = Q;
then are_Prop v,w by A2,A3,ANPROJ_1:22;
then consider b be Real such that
A11: b <> 0 and
A12: v = b * w by ANPROJ_1:1;
|[v`1,v`2,v`3]| = v by EUCLID_5:3
.= |[b * w`1,b * w`2,b * w`3]| by A12,EUCLID_5:7;
then |[v`1,v`2,v`3]| = |[b * w`1,b * w`2, b * u`3]| by A6,EUCLID_5:2;
hence contradiction by A4,A11,A5,FINSEQ_1:78;
end;
end;
theorem Th07:
for L being LINE of IncProjSp_of real_projective_plane
for P,Q being Element of ProjectiveSpace TOP-REAL 3 st
P <> Q & P in L & Q in L holds L = Line(P,Q)
proof
let L be LINE of IncProjSp_of real_projective_plane;
let P,Q be Element of ProjectiveSpace TOP-REAL 3;
assume that
A1: P <> Q and
A2: P in L and
A3: Q in L;
reconsider L9 = L as LINE of real_projective_plane by INCPROJ:4;
L9 = Line(P,Q) by A1,A2,A3,COLLSP:19;
hence thesis;
end;
theorem
for L being LINE of IncProjSp_of real_projective_plane
for P,Q being Element of ProjectiveSpace TOP-REAL 3
for u,v being non zero Element of TOP-REAL 3 st
P in L & Q in L &
P = Dir u & Q = Dir v & u`3 <> 0 & v`3 = 0 holds
P <> Q &
Dir |[u`1 + v`1, u`2 + v`2, u`3]| in L
proof
let L be LINE of IncProjSp_of real_projective_plane;
let P,Q be Element of ProjectiveSpace TOP-REAL 3;
let u,v be non zero Element of TOP-REAL 3;
assume that
A1: P in L and
A2: Q in L and
A3: P = Dir u and
A4: Q = Dir v and
A5: u`3 <> 0 and
A6: v`3 = 0;
thus
A7: P <> Q
proof
assume P = Q;
then
A8: are_Prop u,v by A3,A4,ANPROJ_1:22;
u = |[u`1,u`2,u`3]| & v = |[v`1,v`2,0]| by A6,EUCLID_5:3;
hence contradiction by A5,A8,Th06;
end;
reconsider w = |[u`1 + v`1,u`2 + v`2, u`3]|
as non zero Element of TOP-REAL 3 by A5,Th05;
reconsider R = Dir w as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
u = |[u`1,u`2,u`3]| & v = |[v`1,v`2,0]| by A6,EUCLID_5:3;
then |{u,v,w}| = 0 by Th04;
then P,Q,R are_collinear by A3,A4,BKMODEL1:1;
then R in Line(P,Q) by COLLSP:11;
hence thesis by A1,A2,A7,Th07;
end;
theorem Th08:
for u,v,w being Element of TOP-REAL 3 st v`3 = 0 &
w = |[u`1 + v`1,u`2 + v`2, u`3]| holds |{u,v,w}| = 0
proof
let u,v,w be Element of TOP-REAL 3;
assume that
A2: v`3 = 0 and
A3: w = |[u`1 + v`1,u`2 + v`2, u`3]|;
A4: |{ u,v,w }| = u`1 * v`2 * w`3 - u`3*v`2*w`1 - u`1*v`3*w`2 + u`2*v`3*w`1 -
u`2*v`1*w`3 + u`3*v`1*w`2 by ANPROJ_8:27
.= u`1 * v`2 * w`3 - u`3*v`2*w`1 - u`2*v`1*w`3 + u`3*v`1*w`2
by A2;
w`1 = u`1 + v`1 & w`2 = u`2 + v`2 & w`3 = u`3 by A3,EUCLID_5:2;
hence thesis by A4;
end;
theorem Th09:
for L being LINE of IncProjSp_of real_projective_plane
for P being Element of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3
st P = Dir u & P in L & u.3 <> 0 holds
ex Q being Element of ProjectiveSpace TOP-REAL 3 st
(ex v being non zero Element of TOP-REAL 3 st
Q = Dir v & Q in L & P <> Q & v.3 <> 0)
proof
let L be LINE of IncProjSp_of real_projective_plane;
let P be Element of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
assume that
A1: P = Dir u and
A2: P in L and
A3: u.3 <> 0;
assume
A4: not ex Q being Element of ProjectiveSpace TOP-REAL 3 st
(ex v being non zero Element of TOP-REAL 3 st
Q = Dir v & Q in L & P <> Q & v.3 <> 0);
consider p,q be Element of ProjectiveSpace TOP-REAL 3 such that
A5: p <> q and
A6: L = Line(p,q) by BKMODEL1:73;
consider up be Element of TOP-REAL 3 such that
A7: up is not zero and
A8: p = Dir up by ANPROJ_1:26;
consider vp be Element of TOP-REAL 3 such that
A9: vp is not zero and
A10: q = Dir vp by ANPROJ_1:26;
reconsider P9 = P as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
reconsider L9 = L as LINE of real_projective_plane by INCPROJ:4;
per cases;
suppose
A11: up`3 = 0 & vp`3 = 0;
per cases by A5;
suppose
A12: P <> p;
A13: u`3 <> 0 by A3,EUCLID_5:def 3;
|[u`1+up`1,u`2+up`2,u`3]| is non zero
proof
assume |[u`1+up`1,u`2+up`2,u`3]| is zero;
then u`3 = 0 by EUCLID_5:4,FINSEQ_1:78;
hence contradiction by A3,EUCLID_5:def 3;
end;
then
reconsider wp = |[u`1+up`1,u`2+up`2,u`3]| as
non zero Element of TOP-REAL 3;
reconsider R = Dir wp as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
A14: |{u,up,wp}| = 0 by A11,Th08;
now
thus R <> P
proof
assume R = P;
then are_Prop wp,u by A1,ANPROJ_1:22;
then consider a be Real such that a <> 0 and
A15: wp = a * u by ANPROJ_1:1;
a = 1 & up`1 = 0 & up`2 = 0
proof
A16: |[a * u`1,a * u`2, a * u`3 ]|
= |[u`1+up`1,u`2 + up`2,u`3]| by A15,EUCLID_5:7;
then a * u`1 = u`1 + up`1 & a * u`2 = u`2 + up`2 &
a * u`3 = u`3 by FINSEQ_1:78;
hence a = 1 by XCMPLX_1:7,A13;
then u`1 = u`1 + up`1 & u`2 = u`2 + up`2 by A16,FINSEQ_1:78;
hence thesis;
end;
hence contradiction by A7,A11,EUCLID_5:3,4;
end;
reconsider R2 = R as POINT of IncProjSp_of real_projective_plane
by INCPROJ:2;
now
L = Line(P,p)
proof
P in L & p in L & P <> p & L is LINE of real_projective_plane
by A6,A2,A12,COLLSP:10,INCPROJ:4;
hence thesis by COLLSP:19;
end;
hence R2 on L by A1,A7,A8,A14,BKMODEL1:77;
thus L is LINE of real_projective_plane by INCPROJ:4;
end;
hence R in L by INCPROJ:5;
thus wp.3 <> 0 by A13;
end;
hence contradiction by A4;
end;
suppose
A17: P <> q;
A18: u`3 <> 0 by A3,EUCLID_5:def 3;
|[u`1+vp`1,u`2+vp`2,u`3]| is non zero
proof
assume |[u`1+vp`1,u`2+vp`2,u`3]| is zero;
then u`3 = 0 by EUCLID_5:4,FINSEQ_1:78;
hence contradiction by A3,EUCLID_5:def 3;
end;
then reconsider wp = |[u`1 + vp`1,u`2 + vp`2,u`3]| as
non zero Element of TOP-REAL 3;
reconsider R = Dir wp as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
A19: |{u,vp,wp}| = 0 by A11,Th08;
now
thus R <> P
proof
assume R = P;
then are_Prop wp,u by A1,ANPROJ_1:22;
then consider a be Real such that a <> 0 and
A20: wp = a * u by ANPROJ_1:1;
a = 1 & vp`1 = 0 & vp`2 = 0
proof
|[a * u`1,a * u`2, a * u`3 ]|
= |[u`1+vp`1,u`2 + vp`2,u`3]| by A20,EUCLID_5:7;
then
A21: a * u`1 = u`1 + vp`1 & a * u`2 = u`2 + vp`2 &
a * u`3 = u`3 by FINSEQ_1:78;
hence a = 1 by XCMPLX_1:7,A18;
hence thesis by A21;
end;
hence contradiction by A11,A9,EUCLID_5:3,4;
end;
reconsider R2 = R as POINT of IncProjSp_of real_projective_plane
by INCPROJ:2;
now
L = Line(P,q)
proof
P in L & q in L & P <> q &
L is LINE of real_projective_plane
by A6,A2,COLLSP:10,A17,INCPROJ:4;
hence thesis by COLLSP:19;
end;
hence R2 on L by A1,A9,A10,A19,BKMODEL1:77;
thus L is LINE of real_projective_plane by INCPROJ:4;
end;
hence R in L by INCPROJ:5;
thus wp.3 <> 0 by A18;
end;
hence contradiction by A4;
end;
end;
suppose up`3 <> 0 or vp`3 <> 0;
then per cases;
suppose
A22: up`3 <> 0;
per cases;
suppose
A23: P = p;
per cases;
suppose
A24: vp`3 <> 0;
vp.3 = 0 by A9,A10,A23,A5,A4,A6,COLLSP:10;
hence contradiction by A24,EUCLID_5:def 3;
end;
suppose
A25: vp`3 = 0;
A26: u`3 <> 0 by A3,EUCLID_5:def 3;
|[u`1+vp`1,u`2+vp`2,u`3]| is non zero
proof
assume |[u`1+vp`1,u`2+vp`2,u`3]| is zero;
then u`3 = 0 by EUCLID_5:4,FINSEQ_1:78;
hence contradiction by A3,EUCLID_5:def 3;
end;
then reconsider wp = |[u`1 + vp`1,u`2 + vp`2,u`3]| as
non zero Element of TOP-REAL 3;
reconsider R = Dir wp as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
A27: |{u,vp,wp}| = 0 by A25,Th08;
now
thus R <> P
proof
assume R = P;
then are_Prop wp,u by A1,ANPROJ_1:22;
then consider a be Real such that a <> 0 and
A28: wp = a * u by ANPROJ_1:1;
a = 1 & vp`1 = 0 & vp`2 = 0
proof
|[a * u`1,a * u`2, a * u`3 ]|
= |[u`1+vp`1,u`2 + vp`2,u`3]| by A28,EUCLID_5:7;
then
A29: a * u`1 = u`1 + vp`1 & a * u`2 = u`2 + vp`2 &
a * u`3 = u`3 by FINSEQ_1:78;
hence a = 1 by XCMPLX_1:7,A26;
hence thesis by A29;
end;
hence contradiction by A25,EUCLID_5:3,4,A9;
end;
reconsider R2 = R as POINT of IncProjSp_of real_projective_plane
by INCPROJ:2;
R2 on L & L is LINE of real_projective_plane
by A6,A23,A1,A9,A10,A27,BKMODEL1:77,INCPROJ:4;
hence R in L by INCPROJ:5;
thus wp.3 <> 0 by A26;
end;
hence contradiction by A4;
end;
end;
suppose P <> p;
then up.3 = 0 by A8,A6,A4,A7,COLLSP:10;
hence contradiction by A22,EUCLID_5:def 3;
end;
end;
suppose
A30: vp`3 <> 0;
per cases;
suppose
A31: P = q;
per cases;
suppose
A32: up`3 <> 0;
up.3 = 0 by A7,A8,A31,A5,A4,A6,COLLSP:10;
hence contradiction by A32,EUCLID_5:def 3;
end;
suppose
A33: up`3 = 0;
A34: u`3 <> 0 by A3,EUCLID_5:def 3;
|[u`1+up`1,u`2+up`2,u`3]| is non zero
proof
assume |[u`1+up`1,u`2+up`2,u`3]| is zero;
then u`3 = 0 by EUCLID_5:4,FINSEQ_1:78;
hence contradiction by A3,EUCLID_5:def 3;
end;
then reconsider wp = |[u`1 + up`1,u`2 + up`2,u`3]| as
non zero Element of TOP-REAL 3;
reconsider R = Dir wp as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
A35: |{u,up,wp}| = 0 by A33,Th08;
now
thus R <> P
proof
assume R = P;
then are_Prop wp,u by A1,ANPROJ_1:22;
then consider a be Real such that a <> 0 and
A36: wp = a * u by ANPROJ_1:1;
a = 1 & up`1 = 0 & up`2 = 0
proof
|[a * u`1,a * u`2, a * u`3 ]| = |[u`1+up`1,u`2 + up`2,u`3]|
by A36,EUCLID_5:7;
then
A37: a * u`1 = u`1 + up`1 & a * u`2 = u`2 + up`2 &
a * u`3 = u`3 by FINSEQ_1:78;
hence a = 1 by XCMPLX_1:7,A34;
hence thesis by A37;
end;
hence contradiction by A33,EUCLID_5:3,4,A7;
end;
reconsider R2 = R as
POINT of IncProjSp_of real_projective_plane by INCPROJ:2;
now
L = Line(P,p)
proof
P in L & p in L & P <> p &
L is LINE of real_projective_plane
by A6,A31,A5,COLLSP:10,INCPROJ:4;
hence thesis by COLLSP:19;
end;
hence R2 on L by A1,A7,A8,A35,BKMODEL1:77;
thus L is LINE of real_projective_plane by INCPROJ:4;
end;
hence R in L by INCPROJ:5;
thus wp.3 <> 0 by A34;
end;
hence contradiction by A4;
end;
end;
suppose P <> q;
then vp.3 = 0 by A10,A6,COLLSP:10,A4,A9;
hence contradiction by A30,EUCLID_5:def 3;
end;
end;
end;
end;
theorem Th10:
for P being Element of BK_model
for L being LINE of IncProjSp_of real_projective_plane st P in L
holds ex Q being Element of ProjectiveSpace TOP-REAL 3 st
P <> Q & Q in L &
for u being non zero Element of TOP-REAL 3 st Q = Dir u holds u.3 <> 0
proof
let P be Element of BK_model;
let L be LINE of IncProjSp_of real_projective_plane;
assume
A1: P in L;
consider u be non zero Element of TOP-REAL 3 such that
A2: P = Dir u & u.3 = 1 and
BK_to_REAL2 P = |[u.1,u.2]| by Def01;
consider Q be Element of ProjectiveSpace TOP-REAL 3 such that
A3: (ex v be non zero Element of TOP-REAL 3 st
Q = Dir v & Q in L & P <> Q & v.3 <> 0) by A1,A2,Th09;
consider v be non zero Element of TOP-REAL 3 such that
A4: Q = Dir v & Q in L & P <> Q & v.3 <> 0 by A3;
take Q;
now
thus P <> Q & Q in L by A3;
thus for u being non zero Element of TOP-REAL 3 st Q = Dir u holds
u.3 <> 0
proof
let w be non zero Element of TOP-REAL 3;
assume Q = Dir w;
then are_Prop v,w by A4,ANPROJ_1:22;
then consider a be Real such that
A5: a <> 0 and
A6: v = a * w by ANPROJ_1:1;
a * w = |[ a * w`1, a * w`2, a * w`3 ]| by EUCLID_5:7;
then v`3 = a * w`3 by A6,EUCLID_5:2;
then w`3 = v`3 / a by A5,XCMPLX_1:89
.= v.3 / a by EUCLID_5:def 3;
hence w.3 <> 0 by A5,A4,EUCLID_5:def 3;
end;
end;
hence thesis;
end;
theorem Th11:
for u,v being non zero Element of TOP-REAL 3
for k being non zero Real st u = k * v holds
Dir u = Dir v
proof
let u,v be non zero Element of TOP-REAL 3;
let k be non zero Real;
assume u = k * v;
then are_Prop u,v by ANPROJ_1:1;
hence thesis by ANPROJ_1:22;
end;
theorem
for P being Element of BK_model
for Q being Element of ProjectiveSpace TOP-REAL 3
st P <> Q holds ex P1 being Element of absolute st
P,Q,P1 are_collinear
proof
let P be Element of BK_model;
let Q be Element of ProjectiveSpace TOP-REAL 3;
assume P <> Q;
then Line(P,Q) is LINE of real_projective_plane
by COLLSP:def 7;
then reconsider L = Line(P,Q) as
LINE of IncProjSp_of real_projective_plane by INCPROJ:4;
consider R be Element of ProjectiveSpace TOP-REAL 3 such that
A1: P <> R and
A2: R in L and
A3: for u be non zero Element of TOP-REAL 3 st R = Dir u holds u.3 <> 0
by COLLSP:10,Th10;
consider u be non zero Element of TOP-REAL 3 such that
A4: Dir u = P & u.3 = 1 & BK_to_REAL2 P = |[u.1,u.2]| by Def01;
consider v9 be Element of TOP-REAL 3 such that
A5: v9 is non zero and
A6: Dir v9 = R by ANPROJ_1:26;
A7: v9.3 <> 0 by A5,A6,A3;
then
A8: v9`3 <> 0 by EUCLID_5:def 3;
then reconsider k = 1 / v9`3 as non zero Real;
k * v9 is non zero
proof
assume k * v9 is zero;
then |[0,0,0]| = |[ k * v9`1, k * v9`2, k * v9`3 ]| by EUCLID_5:4,7;
then v9`3 = 0 by FINSEQ_1:78;
hence contradiction by A7,EUCLID_5:def 3;
end;
then reconsider v = k * v9 as non zero Element of TOP-REAL 3;
A9: Dir v = R & v.3 = 1
proof
thus Dir v = R by A6,A5,Th11;
A10: |[v`1,v`2,v`3]| = v by EUCLID_5:3
.= |[k * v9`1,k * v9`2, k * v9`3 ]| by EUCLID_5:7;
thus v.3 = v`3 by EUCLID_5:def 3
.= k * v9`3 by A10,FINSEQ_1:78
.= 1 by A8,XCMPLX_1:106;
end;
reconsider s = |[u.1,u.2]|, t = |[v.1,v.2]| as Point of TOP-REAL 2;
set a = 0, b = 0, r = 1;
reconsider S = s, T = t, X = |[a,b]| as Element of REAL 2 by EUCLID:22;
reconsider w1 = ((- (2 * |((t - s),(s - |[a,b]|))|)) +
(sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),
((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) as Real;
s <> t
proof
assume s = t;
then u.1 = v.1 & u.2 = v.2 & u.3 = v.3 by A4,A9,FINSEQ_1:77;
then u`1 = v.1 & u`2 = v.2 & u`3 = v.3 by EUCLID_5:def 1,def 2,def 3;
then
A11: u`1 = v`1 & u`2 = v`2 & u`3 = v`3 by EUCLID_5:def 1,def 2,def 3;
u = |[u`1,u`2,u`3]| by EUCLID_5:3
.= v by A11,EUCLID_5:3;
hence contradiction by A4,A9,A1;
end;
then consider e1 be Point of (TOP-REAL 2) such that
A12: ( {e1} = (halfline (s,t)) /\ (circle (a,b,r)) &
e1 = ((1 - w1) * s) + (w1 * t) ) by A4,TOPREAL9:58;
reconsider w2 = ((- (2 * |((s - t),(t - |[a,b]|))|)) +
(sqrt (delta ((Sum (sqr (S - T))),(2 * |((s - t),(t - |[a,b]|))|),
((Sum (sqr (T - X))) - (r ^2)))))) / (2 * (Sum (sqr (S - T)))) as Real;
reconsider f = |[e1`1,e1`2,1]| as Element of TOP-REAL 3;
f is non zero by FINSEQ_1:78,EUCLID_5:4;
then reconsider ee1 = f as non zero Element of TOP-REAL 3;
A13: s.1 = u.1 & s.2 = u.2 & t.1 = v.1 & t.2 = v.2;
reconsider P1 = Dir ee1 as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
1 * ee1 + (-(1 - w1)) * u + (- w1) * v = 0.TOP-REAL 3
proof
A14: 1 * ee1 = |[1 * ee1`1,1 * ee1`2, 1 * ee1`3 ]| by EUCLID_5:7
.= ee1 by EUCLID_5:3;
ee1 = (1 - w1) * u + w1 * v
proof
A15: (1 - w1) * s + (w1 * t) = |[((1 - w1) * s + (w1 * t))`1,
((1 - w1) * s + (w1 * t))`2]|
by EUCLID:53;
(1 - w1) * s + (w1 * t) = |[((1 - w1) * s)`1 + (w1 * t)`1,
((1 - w1) * s)`2 + (w1 * t)`2]| by EUCLID:55
.= |[((1 - w1) * s).1 + (w1 * t)`1,
((1 - w1) * s)`2 + (w1 * t)`2]| by EUCLID:def 9
.= |[((1 - w1) * s).1 + (w1 * t).1,
((1 - w1) * s)`2 + (w1 * t)`2]| by EUCLID:def 9
.= |[((1 - w1) * s).1 + (w1 * t).1,
((1 - w1) * s).2 + (w1 * t)`2]| by EUCLID:def 10
.= |[((1 - w1) * s).1 + (w1 * t).1,
((1 - w1) * s).2 + (w1 * t).2]| by EUCLID:def 10
.= |[(1 - w1) * s.1 + (w1 * t).1,
((1 - w1) * s).2 + (w1 * t).2]| by RVSUM_1:44
.= |[(1 - w1) * s.1 + w1 * t.1,
((1 - w1) * s).2 + (w1 * t).2]| by RVSUM_1:44
.= |[(1 - w1) * s.1 + w1 * t.1,
(1 - w1) * s.2 + (w1 * t).2]| by RVSUM_1:44
.= |[(1 - w1) * u.1 + w1 * v.1,
(1 - w1) * u.2 + w1 * v.2]| by A13,RVSUM_1:44;
then
A16: e1`1 = (1 - w1) * u.1 + w1 * v.1 & e1`2 = (1 - w1) * u.2 + w1 * v.2
by A12,A15,FINSEQ_1:77;
(1 - w1) * u + w1 * v = |[ (1 - w1) * u.1 + w1 * v.1,
(1 - w1) * u.2 + w1 * v.2,
(1 - w1) * u.3 + w1 * v.3]|
proof
((1 - w1) * u)`1 = (1 - w1) * u`1 by EUCLID_5:9
.= (1 - w1) * u.1 by EUCLID_5:def 1;
then
A17: ((1 - w1) * u)`1 + (w1 * v)`1 = (1 - w1) * u.1 + (w1 * v).1
by EUCLID_5:def 1
.= (1 - w1) * u.1 + w1 * v.1
by RVSUM_1:44;
((1 - w1) * u)`2 = (1 - w1) * u`2 by EUCLID_5:9
.= (1 - w1) * u.2 by EUCLID_5:def 2;
then
A18: ((1 - w1) * u)`2 + (w1 * v)`2 = (1 - w1) * u.2 + (w1 * v).2
by EUCLID_5:def 2
.= (1 - w1) * u.2 + w1 * v.2
by RVSUM_1:44;
((1 - w1) * u)`3 = (1 - w1) * u`3 by EUCLID_5:9
.= (1 - w1) * u.3 by EUCLID_5:def 3;
then ((1 - w1) * u)`3 + (w1 * v)`3 = (1 - w1) * u.3 + (w1 * v).3
by EUCLID_5:def 3
.= (1 - w1) * u.3 + w1 * v.3
by RVSUM_1:44;
hence thesis by A17,A18,EUCLID_5:5;
end;
hence thesis by A16,A4,A9;
end;
then ee1 + (-(1 - w1)) * u + (-w1) * v
= (1 - w1) * u + w1 * v + ((-(1 - w1)) * u + (-w1) * v) by RVSUM_1:15
.= (1 - w1) * u + (w1 * v + ((-(1 - w1)) * u + (-w1) * v)) by RVSUM_1:15
.= (1 - w1) * u + ((-(1 - w1)) * u + (w1 * v + (-w1) * v)) by RVSUM_1:15
.= (((1 - w1) * u + (-(1 - w1)) * u)) + (w1 * v + (-w1) * v)
by RVSUM_1:15
.= 0.TOP-REAL 3 + (w1 * v + (-w1) * v) by BKMODEL1:4
.= |[0,0,0]| + |[0,0,0]| by BKMODEL1:4,EUCLID_5:4
.= |[0 + 0,0 + 0,0 + 0]| by EUCLID_5:6
.= 0.TOP-REAL 3 by EUCLID_5:4;
hence thesis by A14;
end;
then
A19: P1,P,R are_collinear by A4,A9,ANPROJ_8:11;
e1 in {e1} by TARSKI:def 1; then
A20: e1 in circle(0,0,1) by A12,XBOOLE_0:def 4;
now
thus |[ee1.1,ee1.2]| in circle(0,0,1) by A20,EUCLID:53;
thus ee1.3 = 1;
end;
then
A22: P1 is Element of absolute by BKMODEL1:86;
A23: P,R,P1 are_collinear by COLLSP:8,A19;
P,Q,R are_collinear by A2,COLLSP:11;
then P,R,Q are_collinear by ANPROJ_8:57,HESSENBE:1;
hence thesis by A22,A23,A1,HESSENBE:2,ANPROJ_8:57;
end;
theorem Th12:
for P,Q being Element of BK_model st P <> Q holds
ex P1,P2 being Element of absolute st P1 <> P2 &
P,Q,P1 are_collinear & P,Q,P2 are_collinear
proof
let P,Q be Element of BK_model;
assume
A1: P <> Q;
consider u be non zero Element of TOP-REAL 3 such that
A2: Dir u = P & u.3 = 1 & BK_to_REAL2 P = |[u.1,u.2]| by Def01;
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 Def01;
reconsider s = |[u.1,u.2]|, t = |[v.1,v.2]| as Point of TOP-REAL 2;
set a = 0, b = 0, r = 1;
reconsider S = s, T = t, X = |[a,b]| as Element of REAL 2 by EUCLID:22;
reconsider w1 = ((- (2 * |((t - s),(s - |[a,b]|))|)) +
(sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),
((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) as Real;
consider e1 be Point of (TOP-REAL 2) such that
A4: ( {e1} = (halfline (s,t)) /\ (circle (a,b,r)) &
e1 = ((1 - w1) * s) + (w1 * t) ) by Th02,A1,A2,A3,TOPREAL9:58;
reconsider w2 = ((- (2 * |((s - t),(t - |[a,b]|))|)) +
(sqrt (delta ((Sum (sqr (S - T))),(2 * |((s - t),(t - |[a,b]|))|),
((Sum (sqr (T - X))) - (r ^2)))))) / (2 * (Sum (sqr (S - T)))) as Real;
consider e2 be Point of (TOP-REAL 2) such that
A5: ({e2} = (halfline (t,s)) /\ (circle (a,b,r)) &
e2 = ((1 - w2) * t) + (w2 * s) ) by Th02,A1,A2,A3,TOPREAL9:58;
reconsider f = |[e1`1,e1`2,1]| as Element of TOP-REAL 3;
f is non zero by FINSEQ_1:78,EUCLID_5:4;
then reconsider ee1 = f as non zero Element of TOP-REAL 3;
A6: s.1 = u.1 & s.2 = u.2 & t.1 = v.1 & t.2 = v.2;
reconsider P1 = Dir ee1 as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
1 * ee1 + (-(1 - w1)) * u + (- w1) * v = 0.TOP-REAL 3
proof
A7: 1 * ee1 = |[1 * ee1`1,1 * ee1`2, 1 * ee1`3 ]| by EUCLID_5:7
.= ee1 by EUCLID_5:3;
ee1 = (1 - w1) * u + w1 * v
proof
A8: (1 - w1) * s + (w1 * t) = |[((1 - w1) * s + (w1 * t))`1,
((1 - w1) * s + (w1 * t))`2]|
by EUCLID:53;
(1 - w1) * s + (w1 * t) = |[((1 - w1) * s)`1 + (w1 * t)`1,
((1 - w1) * s)`2 + (w1 * t)`2]| by EUCLID:55
.= |[((1 - w1) * s).1 + (w1 * t)`1,
((1 - w1) * s)`2 + (w1 * t)`2]| by EUCLID:def 9
.= |[((1 - w1) * s).1 + (w1 * t).1,
((1 - w1) * s)`2 + (w1 * t)`2]| by EUCLID:def 9
.= |[((1 - w1) * s).1 + (w1 * t).1,
((1 - w1) * s).2 + (w1 * t)`2]| by EUCLID:def 10
.= |[((1 - w1) * s).1 + (w1 * t).1,
((1 - w1) * s).2 + (w1 * t).2]| by EUCLID:def 10
.= |[(1 - w1) * s.1 + (w1 * t).1,
((1 - w1) * s).2 + (w1 * t).2]| by RVSUM_1:44
.= |[(1 - w1) * s.1 + w1 * t.1,
((1 - w1) * s).2 + (w1 * t).2]| by RVSUM_1:44
.= |[(1 - w1) * s.1 + w1 * t.1,
(1 - w1) * s.2 + (w1 * t).2]| by RVSUM_1:44
.= |[(1 - w1) * u.1 + w1 * v.1,
(1 - w1) * u.2 + w1 * v.2]| by A6,RVSUM_1:44;
then
A9: e1`1 = (1 - w1) * u.1 + w1 * v.1 & e1`2 = (1 - w1) * u.2 + w1 * v.2
by A4,A8,FINSEQ_1:77;
(1 - w1) * u + w1 * v = |[ (1 - w1) * u.1 + w1 * v.1,
(1 - w1) * u.2 + w1 * v.2,
(1 - w1) * u.3 + w1 * v.3]|
proof
((1 - w1) * u)`1 = (1 - w1) * u`1 by EUCLID_5:9
.= (1 - w1) * u.1 by EUCLID_5:def 1;
then
A10: ((1 - w1) * u)`1 + (w1 * v)`1 = (1 - w1) * u.1 + (w1 * v).1
by EUCLID_5:def 1
.= (1 - w1) * u.1 + w1 * v.1
by RVSUM_1:44;
((1 - w1) * u)`2 = (1 - w1) * u`2 by EUCLID_5:9
.= (1 - w1) * u.2 by EUCLID_5:def 2;
then
A11: ((1 - w1) * u)`2 + (w1 * v)`2 = (1 - w1) * u.2 + (w1 * v).2
by EUCLID_5:def 2
.= (1 - w1) * u.2 + w1 * v.2
by RVSUM_1:44;
((1 - w1) * u)`3 = (1 - w1) * u`3 by EUCLID_5:9
.= (1 - w1) * u.3 by EUCLID_5:def 3;
then ((1 - w1) * u)`3 + (w1 * v)`3 = (1 - w1) * u.3 + (w1 * v).3
by EUCLID_5:def 3
.= (1 - w1) * u.3 + w1 * v.3
by RVSUM_1:44;
hence thesis by A10,A11,EUCLID_5:5;
end;
hence thesis by A9,A2,A3;
end;
then ee1 + (-(1 - w1)) * u + (-w1) * v
= (1 - w1) * u + w1 * v + ((-(1 - w1)) * u + (-w1) * v) by RVSUM_1:15
.= (1 - w1) * u + (w1 * v + ((-(1 - w1)) * u + (-w1) * v)) by RVSUM_1:15
.= (1 - w1) * u + ((-(1 - w1)) * u + (w1 * v + (-w1) * v)) by RVSUM_1:15
.= (((1 - w1) * u + (-(1 - w1)) * u)) + (w1 * v + (-w1) * v)
by RVSUM_1:15
.= 0.TOP-REAL 3 + (w1 * v + (-w1) * v) by BKMODEL1:4
.= |[0,0,0]| + |[0,0,0]| by BKMODEL1:4,EUCLID_5:4
.= |[0 + 0,0 + 0,0 + 0]| by EUCLID_5:6
.= 0.TOP-REAL 3 by EUCLID_5:4;
hence thesis by A7;
end;
then
A12: P1,P,Q are_collinear by A2,A3,ANPROJ_8:11;
e1 in {e1} by TARSKI:def 1; then
A13: e1 in circle(0,0,1) by A4,XBOOLE_0:def 4;
now
thus |[ee1.1,ee1.2]| in circle(0,0,1) by A13,EUCLID:53;
thus ee1.3 = 1;
end;
then
A15: P1 is Element of absolute by BKMODEL1:86;
reconsider g = |[e2`1,e2`2,1]| as Element of TOP-REAL 3;
g is non zero by EUCLID_5:4,FINSEQ_1:78;
then reconsider ee2 = g as non zero Element of TOP-REAL 3;
reconsider P2 = Dir ee2 as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
1 * ee2 + (-(1 - w2)) * v + (- w2) * u = 0.TOP-REAL 3
proof
A16: 1 * ee2 = |[1 * ee2`1,1 * ee2`2, 1 * ee2`3 ]| by EUCLID_5:7
.= ee2 by EUCLID_5:3;
ee2 = (1 - w2) * v + w2 * u
proof
A17: (1 - w2) * t + (w2 * s)
= |[((1 - w2) * t + (w2 * s))`1, ((1 - w2) * t + (w2 * s))`2]|
by EUCLID:53;
(1 - w2) * t + (w2 * s)
= |[((1 - w2) * t)`1 + (w2 * s)`1, ((1 - w2) * t)`2 + (w2 * s)`2]|
by EUCLID:55
.= |[((1 - w2) * t).1 + (w2 * s)`1, ((1 - w2) * t)`2 + (w2 * s)`2]|
by EUCLID:def 9
.= |[((1 - w2) * t).1 + (w2 * s).1, ((1 - w2) * t)`2 + (w2 * s)`2]|
by EUCLID:def 9
.= |[((1 - w2) * t).1 + (w2 * s).1, ((1 - w2) * t).2 + (w2 * s)`2]|
by EUCLID:def 10
.= |[((1 - w2) * t).1 + (w2 * s).1, ((1 - w2) * t).2 + (w2 * s).2]|
by EUCLID:def 10
.= |[(1 - w2) * t.1 + (w2 * s).1, ((1 - w2) * t).2 + (w2 * s).2]|
by RVSUM_1:44
.= |[(1 - w2) * t.1 + w2 * s.1,((1 - w2) * t).2 + (w2 * s).2]|
by RVSUM_1:44
.= |[(1 - w2) * t.1 + w2 * s.1, (1 - w2) * t.2 + (w2 * s).2]|
by RVSUM_1:44
.= |[(1 - w2) * v.1 + w2 * u.1, (1 - w2) * v.2 + w2 * u.2]|
by A6,RVSUM_1:44;
then
A18: e2`1 = (1 - w2) * v.1 + w2 * u.1 &
e2`2 = (1 - w2) * v.2 + w2 * u.2 by A5,A17,FINSEQ_1:77;
(1 - w2) * v + w2 * u = |[ (1 - w2) * v.1 + w2 * u.1,
(1 - w2) * v.2 + w2 * u.2,
(1 - w2) * v.3 + w2 * u.3]|
proof
((1 - w2) * v)`1 = (1 - w2) * v`1 by EUCLID_5:9
.= (1 - w2) * v.1 by EUCLID_5:def 1;
then
A19: ((1 - w2) * v)`1 + (w2 * u)`1 = (1 - w2) * v.1 + (w2 * u).1
by EUCLID_5:def 1
.= (1 - w2) * v.1 + w2 * u.1
by RVSUM_1:44;
((1 - w2) * v)`2 = (1 - w2) * v`2 by EUCLID_5:9
.= (1 - w2) * v.2 by EUCLID_5:def 2; then
A20: ((1 - w2) * v)`2 + (w2 * u)`2 = (1 - w2) * v.2 + (w2 * u).2
by EUCLID_5:def 2
.= (1 - w2) * v.2 + w2 * u.2
by RVSUM_1:44;
((1 - w2) * v)`3 = (1 - w2) * v`3 by EUCLID_5:9
.= (1 - w2) * v.3 by EUCLID_5:def 3;
then ((1 - w2) * v)`3 + (w2 * u)`3 = (1 - w2) * v.3 + (w2 * u).3
by EUCLID_5:def 3
.= (1 - w2) * v.3 + w2 * u.3
by RVSUM_1:44;
hence thesis by EUCLID_5:5,A19,A20;
end;
hence thesis by A18,A2,A3;
end;
then ee2 + (-(1 - w2)) * v + (-w2) * u
= (1 - w2) * v + w2 * u + ((-(1 - w2)) * v + (-w2) * u)
by RVSUM_1:15
.= (1 - w2) * v + (w2 * u + ((-(1 - w2)) * v + (-w2) * u))
by RVSUM_1:15
.= (1 - w2) * v + ((-(1 - w2)) * v + (w2 * u + (-w2) * u))
by RVSUM_1:15
.= (((1 - w2) * v + (-(1 - w2)) * v)) + (w2 * u + (-w2) * u)
by RVSUM_1:15
.= 0.TOP-REAL 3 + (w2 * u + (-w2) * u) by BKMODEL1:4
.= 0.TOP-REAL 3 + 0.TOP-REAL 3 by BKMODEL1:4
.= |[0 + 0,0 + 0,0 + 0]| by EUCLID_5:4,6
.= 0.TOP-REAL 3 by EUCLID_5:4;
hence thesis by A16;
end;
then
A21: P2,Q,P are_collinear by A2,A3,ANPROJ_8:11;
e2 in (halfline (t,s)) /\ (circle (a,b,r)) by A5,TARSKI:def 1;
then
A22: e2 in circle(0,0,1) by XBOOLE_0:def 4;
now
thus |[ee2.1,ee2.2]| in circle(0,0,1) by A22,EUCLID:53;
thus ee2.3 = 1;
end;
then
A24: P2 is Element of absolute by BKMODEL1:86;
A25: P1 <> P2
proof
assume P1 = P2;
then are_Prop ee1,ee2 by ANPROJ_1:22;
then consider l be Real such that
l <> 0 and
A26: ee1 = l * ee2 by ANPROJ_1:1;
|[e1`1,e1`2,1]| = |[l * (e2`1),l * (e2`2), l * 1]| by A26,EUCLID_5:8;
then
A27: 1 = l * 1 & e1`1 = l * e2`1 & e1`2 = l * e2`2 by FINSEQ_1:78;
A28: e1 = |[e1`1,e1`2]| by EUCLID:53
.= e2 by A27,EUCLID:53;
(1 - (w1 + w2)) <> 0
proof
assume
A29: (1 - (w1 + w2)) = 0;
A30: 2 * Sum(sqr(S - T)) = 2 * Sum(sqr(T - S)) by BKMODEL1:6;
Sum sqr (S - T) is non zero
proof
assume
A31: Sum sqr (S - T) is zero;
Sum sqr (S - T) = |. S - T .|^2 by TOPREAL9:5;
then
A32: |. S - T .| = 0 by A31;
reconsider n = 2 as Nat;
S = T
proof
reconsider Sn = S,Tn = T as Element of n-tuples_on REAL
by EUCLID:def 1;
Sn = Sn - Tn + Tn by RVSUM_1:43
.= 0*n + Tn by A32,EUCLID:8
.= Tn by EUCLID_4:1;
hence thesis;
end;
then
A33: u.1 = v.1 & u.2 = v.2 & u.3 = v.3 by A2,A3,FINSEQ_1:77;
A34: |[u.1,u.2,u.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
.= u by EUCLID_5:3;
|[v.1,v.2,v.3]| = |[v`1,v.2,v.3]| by EUCLID_5:def 1
.= |[v`1,v`2,v.3]| by EUCLID_5:def 2
.= |[v`1,v`2,v`3]| by EUCLID_5:def 3
.= v by EUCLID_5:3;
hence contradiction by A1,A2,A3,A34,A33;
end;
then reconsider l = Sum (sqr(S - T)) as non zero Real;
A35: s - |[a,b]| = |[s`1,s`2]| - |[0,0]| by EUCLID:53
.= |[s`1 - 0,s`2 - 0 ]| by EUCLID:62
.= s by EUCLID:53;
A36: t - |[a,b]| = |[t`1,t`2]| - |[0,0]| by EUCLID:53
.= |[t`1 - 0,t`2 - 0 ]| by EUCLID:62
.= t by EUCLID:53;
A38: w1 + w2 = ((- (2 * |((t - s),s)|))
+ (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),s)|),
((Sum (sqr (S - X))) - (r ^2)))))) / (2 * l)
+((- (2 * |((s - t),t)|))
+ (sqrt (delta ((Sum (sqr (S - T))),(2 * |((s - t),t)|),
((Sum (sqr (T - X))) - (r ^2)))))) / (2 * l)
by A35,A36,BKMODEL1:6
.= ((- (2 * |((t - s),s)|))
+ ( sqrt (delta (l,(2 * |((t - s),s)|),(Sum sqr S - 1))))) / (2 * l)
+((- (2 * |((s - t),t)|)) + (sqrt (delta (l,(2 * |((s - t),t)|),
(Sum sqr T - 1))))) / (2 * l) by A35,A36,BKMODEL1:6;
reconsider l2 = - (2 * |((t - s),s)|),
l3 = - (2 * |((s - t),t)|),
l4 = Sum sqr S - 1,
l5 = Sum sqr T - 1 as Real;
reconsider l6 = sqrt delta(l,-l2,l4),
l7 = sqrt delta(l,-l3,l5),
l8 = 2 * l as Real;
0 <= |.S - T.|^2;
then
A39: 0 <= l by TOPREAL9:5;
|[u.1,u.2]| - |[0,0]| = |[ u.1 - 0, u.2 - 0 ]| by EUCLID:62
.= s;
then
A40: |. S .| < 1 by A2,TOPREAL9:45;
|[v.1,v.2]| - |[0,0]| = |[ v.1 - 0, v.2 - 0 ]| by EUCLID:62
.= t;
then |. T .| < 1 by A3,TOPREAL9:45;
then
A42: |.S.|^2 <= 1 & |.T.|^2 <= 1 by A40,XREAL_1:160;
then 0 <= delta(l,-l2,l4) & 0 <= delta(l,-l3,l5) by BKMODEL1:18,A30;
then
A43: 0 <= l6 & 0 <= l7 by SQUARE_1:def 2;
A44: l2 + l3 = l8
proof
|( t - s,s )| + |( s - t,t )| = |( t,s )| - |( s,s )|
+ |( s - t, t)|
by EUCLID_2:24
.= - |( s,s )| + |( t,s )|
+ (|( s,t )| - |(t, t)|)
by EUCLID_2:24
.= - ( |( s,s )| - 2 * |( t,s )|
+ |(t, t)|)
.= - |( s - t, s - t )| by EUCLID_2:31
.= - |. S - T .|^2 by EUCLID_2:36
.= - Sum sqr (S- T) by TOPREAL9:5;
hence thesis;
end;
w1 + w2 = l2 / l8 + l6 / l8 + (l3 + l7) / l8
by A38,XCMPLX_1:62
.= l2 / l8 + l6 / l8 + (l3 / l8 + l7 / l8) by XCMPLX_1:62
.= l2 / l8 + l3 / l8 + (l6 / l8 + l7 / l8)
.= l8 / l8 + (l6 / l8 + l7 / l8) by A44,XCMPLX_1:62
.= 1 + (l6 / l8 + l7 / l8) by XCMPLX_1:60;
then 0 = (l6 + l7) / l8 by A29,XCMPLX_1:62;
then l6 = 0 & l7 = 0 by A43;
then
A45: delta(l,-l2,l4) = 0 & delta(l,-l3,l5) = 0
by A42,BKMODEL1:18,A30,SQUARE_1:24;
l4 < 0
proof
|.S.| * |.S.| < 1 by A40,XREAL_1:162;
then |.S.|^2 - 1 < 1 - 1 by XREAL_1:14;
hence thesis by TOPREAL9:5;
end;
hence contradiction by A45,A39,BKMODEL1:5;
end;
then reconsider w1w2 = (1 - (w1 + w2)) as non zero Real;
w1w2 * s = w1w2 * t by A28,A4,A5,BKMODEL1:70;
then s = t by EUCLID_4:8;
then
A46: u.1 = v.1 & u.2 = v.2 & u.3 = v.3 by A2,A3,FINSEQ_1:77;
A47: |[u.1,u.2,u.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
.= u by EUCLID_5:3;
|[v.1,v.2,v.3]| = |[v`1,v.2,v.3]| by EUCLID_5:def 1
.= |[v`1,v`2,v.3]| by EUCLID_5:def 2
.= |[v`1,v`2,v`3]| by EUCLID_5:def 3
.= v by EUCLID_5:3;
hence contradiction by A1,A2,A3,A47,A46;
end;
A48: P,Q,P1 are_collinear by COLLSP:8,A12;
Q,P2,P are_collinear by A21,COLLSP:7;
then P2,P,Q are_collinear by COLLSP:8;
then P,Q,P2 are_collinear by COLLSP:8;
hence thesis by A15,A24,A25,A48;
end;
theorem Th13:
for P,Q,R being Element of real_projective_plane
for u,v,w being non zero Element of TOP-REAL 3
for a,b,c,d being Real st P in BK_model &
Q in absolute & P = Dir u & Q = Dir v & R = Dir w &
u = |[a,b,1]| & v = |[c,d,1]| & w = |[ (a + c) / 2,(b + d) / 2,1 ]| holds
R in BK_model & R <> P & P,R,Q are_collinear
proof
let P,Q,R being Element of real_projective_plane;
let u,v,w being non zero Element of TOP-REAL 3;
let a,b,c,d being Real;
assume that
A1: P in BK_model and
A2: Q in absolute and
A3: P = Dir u and
A4: Q = Dir v and
A5: R = Dir w and
A6: u = |[a,b,1]| and
A7: v = |[c,d,1]| and
A8: w = |[ (a+c)/2,(b+d)/2,1 ]|;
reconsider PBK = P as Element of BK_model by A1;
consider u2 being non zero Element of TOP-REAL 3 such that
A9: Dir u2 = PBK & u2.3 = 1 & BK_to_REAL2 PBK = |[u2.1,u2.2]| by Def01;
A10: u.3 = u`3 by EUCLID_5:def 3 .= 1 by A6,EUCLID_5:2; then
A11: u = u2 by A3,A9,BKMODEL1:43;
reconsider S = |[u.1,u.2]| as Element of TOP-REAL 2;
A12: |. S - |[0,0]| .| = |. |[S`1,S`2]| - |[0,0]| .| by EUCLID:53
.= |. |[S`1 - 0,S`2 - 0]| .| by EUCLID:62
.= |. S .| by EUCLID:53;
1^2 = 1;
then |. S .|^2 < 1 by A9,A11,TOPREAL9:45,A12,SQUARE_1:16;
then (S`1)^2 + (S`2)^2 < 1 by JGRAPH_3:1;
then (u.1)^2 + (S`2)^2 < 1 by EUCLID:52; then
A13: (u.1)^2 + (u.2)^2 < 1 by EUCLID:52;
u`1 = a & u`2 = b & v`1 = c & v`2 = d by A6,A7,EUCLID_5:2;
then
A14: u.1 = a & u.2 = b & v.1 = c & v.2 = d by EUCLID_5:def 1,def 2;
v`3 = 1 by A7,EUCLID_5:2;
then v.3 = 1 by EUCLID_5:def 3;
then |[v.1,v.2]| in circle(0,0,1) by A2,A4,BKMODEL1:84;
then consider pp be Point of TOP-REAL 2 such that
A15: |[v.1,v.2]| = pp and
A16: |. pp - |[0,0]| .| = 1;
1 = |. |[v.1 - 0,v.2 - 0]| .| by A15,A16,EUCLID:62
.= |. pp .| by A15;
then a17: 1^2 = (pp`1)^2 + (pp`2)^2 by JGRAPH_1:29
.= (v.1)^2 + (pp`2)^2 by A15,EUCLID:52
.= (v.1)^2 + (v.2)^2 by A15,EUCLID:52;
w`1 = (a+c)/2 & w`2 = (b+d)/2 by A8,EUCLID_5:2; then
A18: w.1 = (a+c)/2 & w.2 = (b+d)/2 by EUCLID_5:def 1,def 2;
reconsider R1 = |[ w.1,w.2 ]| as Element of TOP-REAL 2;
|. R1 - |[0,0]| .|^2 < 1
proof
A19: R1`1 = w.1 & R1`2 = w.2 by EUCLID:52;
|. R1 - |[0,0]| .|^2 = |. |[w.1 - 0, w.2 - 0 ]| .|^2 by EUCLID:62
.= (w.1)^2 + (w.2)^2 by A19,JGRAPH_1:29;
hence thesis by A18,BKMODEL1:17,A13,a17,A14;
end;
then |. R1 - |[0,0]| .| < 1 by SQUARE_1:52;
then R1 in inside_of_circle(0,0,1);
then reconsider R1 as Element of inside_of_circle(0,0,1);
consider PR1 be Element of TOP-REAL 2 such that
A20: PR1 = R1 and
A21: REAL2_to_BK R1 = Dir |[PR1`1,PR1`2,1]| by Def02;
A22: w.1 = w`1 & w.2 = w`2 & w`3 = 1 by A8,EUCLID_5:2;
PR1`1 = w.1 & PR1`2 = w.2 by A20,EUCLID:52; then
A23: REAL2_to_BK R1 = Dir w by A21,A22,EUCLID_5:3;
A24: P <> R
proof
assume
A25: P = R;
w.3 = w`3 by EUCLID_5:def 3
.= 1 by A8,EUCLID_5:2;
then
A26: u`1 = w`1 & u`2 = w`2 by A25,A3,A5,A10,BKMODEL1:43;
u`1 = a & w`1 = (a + c)/2 & u`2 = b & w`2 = (b + d)/2
by A6,A8,EUCLID_5:2;
hence contradiction by A26,A6,A7,A3,A4,A1,A2,Th01,XBOOLE_0:def 4;
end;
0 = |{u,v,w}| by A6,A7,A8,BKMODEL1:20
.= - |{u,w,v}| by ANPROJ_8:29;
hence thesis by A23,A24,A3,A4,A5,BKMODEL1:1;
end;
theorem Th14:
for P,Q being Element of real_projective_plane
st P in absolute & Q in BK_model
holds
ex R being Element of real_projective_plane st R in BK_model &
Q <> R & R,Q,P are_collinear
proof
let P,Q being Element of real_projective_plane;
assume that
A1: P in absolute and
A2: Q in BK_model;
reconsider QBK = Q as Element of BK_model by A2;
consider u be non zero Element of TOP-REAL 3 such that
(u.1)^2 + (u.2)^2 = 1 and
A3: u.3 = 1 and
A4: P = Dir u by A1,BKMODEL1:89;
consider v be non zero Element of TOP-REAL 3 such that
A5: Dir v = QBK & v.3 = 1 & BK_to_REAL2 QBK = |[v.1,v.2]| by Def01;
|[ (v.1 + u.1)/2,(v.2 + u.2)/2,1 ]| is non zero by EUCLID_5:4,FINSEQ_1:78;
then reconsider w = |[ (v.1 + u.1)/2,(v.2 + u.2)/2,1 ]| as
non zero Element of TOP-REAL 3;
reconsider R = Dir w as Element of real_projective_plane by ANPROJ_1:26;
take R;
now
u = |[u`1,u`2,u`3]| & v = |[v`1,v`2,v`3]| by EUCLID_5:3;
then u = |[u.1,u`2,u`3]| & v = |[v.1,v`2,v`3]|;
then u = |[u.1,u.2,u`3]| & v = |[v.1,v.2,v`3]|;
hence u = |[u.1,u.2,1]| & v = |[v.1,v.2,1]| by A3,A5;
end;
then R in BK_model & R <> Q & Q,R,P are_collinear by A1,A4,A5,Th13;
hence thesis by COLLSP:4;
end;
theorem Th15:
for L being LINE of IncProjSp_of real_projective_plane
for p ,q being POINT of IncProjSp_of real_projective_plane
for P,Q being Element of real_projective_plane st
p = P & q = Q &
P in BK_model & Q in absolute &
q on L & p on L holds
ex p1,p2 being POINT of IncProjSp_of real_projective_plane,
P1,P2 being Element of real_projective_plane st
p1 = P1 & p2 = P2 & P1 <> P2 &
P1 in absolute & P2 in absolute &
p1 on L & p2 on L
proof
let L being LINE of IncProjSp_of real_projective_plane;
let p ,q being POINT of IncProjSp_of real_projective_plane;
let P ,Q being Element of real_projective_plane;
assume that
A1: p = P and
A2: q = Q and
A3: P in BK_model and
A4: Q in absolute and
A5: q on L and
A6: p on L;
A7: P <> Q by Th01,A3,A4,XBOOLE_0:def 4;
reconsider l = L as LINE of real_projective_plane by INCPROJ:4;
A8: P in l by A1,A6,INCPROJ:5;
reconsider PBK = P as Element of BK_model by A3;
consider R being Element of real_projective_plane such that
A9: R in BK_model and
A10: P <> R and
A11: R,P,Q are_collinear by A3,A4,Th14;
reconsider r = R as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
consider LL be LINE of IncProjSp_of real_projective_plane such that
A12: r on LL & p on LL & q on LL by A1,A2,A11,INCPROJ:10;
L = LL by A1,A2,A5,A6,A12,A7,INCPROJ:8;
then R in l by A12,INCPROJ:5; then
A13: l = Line(P,R) by A8,A10,COLLSP:19;
reconsider RBK = R as Element of BK_model by A9;
consider P1,P2 be Element of absolute such that
A14: P1 <> P2 and
A15: PBK,RBK,P1 are_collinear and
A16: PBK,RBK,P2 are_collinear by A10,Th12;
reconsider PP1 = P1, PP2 = P2 as Element of real_projective_plane;
A17: PP1 in Line(P,R) & PP2 in Line(P,R) by A15,A16,COLLSP:11;
reconsider p1 = P1,p2 = P2 as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
p1 on L & p2 on L by A13,A17,INCPROJ:5;
hence thesis by A14;
end;
theorem Th16:
for P being Element of BK_model
for Q being Element of absolute holds
ex R being Element of absolute st Q <> R & Q,P,R are_collinear
proof
let P be Element of BK_model;
let Q be Element of absolute;
A1: P <> Q by XBOOLE_0:def 4,Th01;
reconsider p9 = P,q9 = Q as Element of real_projective_plane;
reconsider L9 = Line(p9,q9) as LINE of real_projective_plane
by A1,COLLSP:def 7;
reconsider L = L9 as LINE of IncProjSp_of real_projective_plane
by INCPROJ:4;
reconsider p = P,q = Q as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
p9 in L9 & q9 in L9 by COLLSP:10;
then p on L & q on L by INCPROJ:5;
then consider p1,p2 be POINT of IncProjSp_of real_projective_plane,
P1,P2 be Element of real_projective_plane such that
A2: p1 = P1 & p2 = P2 & P1 <> P2 &
P1 in absolute & P2 in absolute &
p1 on L & p2 on L by Th15;
reconsider p1,p2 as Element of real_projective_plane by INCPROJ:3;
A3: P1 in L9 & P2 in L9 by A2,INCPROJ:5;
then
A4: p9,q9,p1 are_collinear & p9,q9,p2 are_collinear & P1 <> P2 &
P1 in absolute & P2 in absolute by A2,COLLSP:11;
reconsider P1,P2 as Element of absolute by A2;
per cases;
suppose
A5: q9 = p1;
take P2;
now
thus Q <> P2 by A5,A2;
P,Q,P2 are_collinear by A3,COLLSP:11;
hence Q,P,P2 are_collinear by COLLSP:4;
end;
hence thesis;
end;
suppose q9 <> p1;
per cases;
suppose
A6: Q <> P2;
take P2;
P,Q,P2 are_collinear by A3,COLLSP:11;
hence thesis by A6,COLLSP:4;
end;
suppose
A7: Q = P2;
take P1;
thus thesis by A4,A7,A2,COLLSP:4;
end;
end;
end;
theorem Th17:
for P being Element of BK_model
for u being non zero Element of TOP-REAL 3 st
P = Dir u & u.3 = 1 holds (u.1)^2 + (u.2)^2 < 1
proof
let P be Element of BK_model;
let u be non zero Element of TOP-REAL 3;
assume that
A1: P = Dir u and
A2: u.3 = 1;
consider u2 be non zero Element of TOP-REAL 3 such that
A3: Dir u2 = P & u2.3 = 1 & BK_to_REAL2 P = |[u2.1,u2.2]| by Def01;
A4: u = u2 by A1,A2,A3,BKMODEL1:43;
reconsider S = |[u.1,u.2]| as Element of TOP-REAL 2;
A5: |. S - |[0,0]| .| = |. |[S`1,S`2]| - |[0,0]| .| by EUCLID:53
.= |. |[S`1 - 0,S`2 - 0]| .| by EUCLID:62
.= |. S .| by EUCLID:53;
1^2 = 1;
then |. S .|^2 < 1 by A4,A3,TOPREAL9:45,A5,SQUARE_1:16;
then (S`1)^2 + (S`2)^2 < 1 by JGRAPH_3:1;
then (u.1)^2 + (S`2)^2 < 1 by EUCLID:52;
hence thesis by EUCLID:52;
end;
theorem Th18:
for P1,P2 being Element of absolute
for Q being Element of BK_model
for u,v,w being non zero Element of TOP-REAL 3 st
Dir u = P1 & Dir v = P2 & Dir w = Q &
u.3 = 1 & v.3 = 1 & w.3 = 1 & v.1 = - u.1 & v.2 = - u.2 &
P1,Q,P2 are_collinear holds
ex a being Real st -1 < a < 1 & w.1 = a * u.1 & w.2 = a * u.2
proof
let P1,P2 be Element of absolute;
let Q be Element of BK_model;
let u,v,w be non zero Element of TOP-REAL 3;
assume that
A1: Dir u = P1 & Dir v = P2 & Dir w = Q and
A2: u.3 = 1 & v.3 = 1 & w.3 = 1 and
A3: v.1 = - u.1 & v.2 = - u.2 and
A4: P1,Q,P2 are_collinear;
u.1 = u`1 & u.2 = u`2 by EUCLID_5:def 1,def 2;
then
A6: u`3 = 1 & v`3 = 1 & w`3 = 1 & v`1 = - u`1 & v`2 = - u`2
by A2,A3,EUCLID_5:def 1,def 2,def 3;
P1,P2,Q are_collinear by A4,COLLSP:4; then
A7: 0 = |{ u,v,w }| by A1,BKMODEL1:1
.= u`1 * (-u`2) * 1 - 1 * (-u`2) * w`1 - u`1 * 1 * w`2
+ u`2 * 1 * w`1 - u`2 * (-u`1) * 1 + 1 * (-u`1) * w`2 by A6,ANPROJ_8:27
.= 2 * (u`2 * w`1 - u`1 * w`2);
consider u9 be non zero Element of TOP-REAL 3 such that
A8: (u9.1)^2 + (u9.2)^2 = 1 and
A9: u9.3 = 1 and
A10: P1 = Dir u9 by BKMODEL1:89;
A11: u = u9 by A9,A10,A1,A2,BKMODEL1:43;
not (u`1 = 0 & u`2 = 0)
proof
assume u`1 = 0 & u`2 = 0;
then u.1 = 0 & u.2 = 0 by EUCLID_5:def 1,def 2;
hence contradiction by A11,A8;
end;
then consider e be Real such that
A13: w`1 = e * u`1 & w`2 = e * u`2 by A7,BKMODEL1:2;
w.1 = e * u`1 & w.2 = e * u`2 by A13,EUCLID_5:def 1,def 2;
then
A14: w.1 = e * u.1 & w.2 = e * u.2 by EUCLID_5:def 1,def 2;
per cases;
suppose e = 0;
hence thesis by A14;
end;
suppose e <> 0;
(w.1)^2 + (w.2)^2 = w`1 * w.1 + w.2 * w.2 by EUCLID_5:def 1
.= w`1 * w`1 + w.2 * w.2 by EUCLID_5:def 1
.= w`1 * w`1 + w`2 * w.2 by EUCLID_5:def 2
.= w`1 * w`1 + w`2 * w`2 by EUCLID_5:def 2
.= e * e * (u`1 * u`1 + u`2 * u`2) by A13
.= e * e * (u.1 * u`1 + u`2 * u`2) by EUCLID_5:def 1
.= e * e * (u.1 * u.1 + u`2 * u`2) by EUCLID_5:def 1
.= e * e * (u.1 * u.1 + u.2 * u`2) by EUCLID_5:def 2
.= e * e * (u.1 * u.1 + u.2 * u.2) by EUCLID_5:def 2
.= e * e by A8,A11;
then e^2 < 1 by A1,A2,Th17;
then - 1 < e < 1 by SQUARE_1:52;
hence thesis by A14;
end;
end;
begin :: Tangent
definition
let P being Element of absolute;
func pole_infty P -> Element of real_projective_plane means
:Def03:
ex u being non zero Element of TOP-REAL 3 st P = Dir u & u.3 = 1 &
(u.1)^2 + (u.2)^2 = 1 & it = Dir |[- u.2,u.1,0]|;
existence
proof
consider u be non zero Element of TOP-REAL 3 such that
A1: (u.1)^2 + (u.2)^2 = 1 and
A2: u.3 = 1 and
A3: P = Dir u by BKMODEL1:89;
Dir |[-u.2,u.1,0]| is Element of real_projective_plane
by A1,BKMODEL1:91,ANPROJ_1:26;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let P1,P2 be Element of real_projective_plane such that
A4: ex u be non zero Element of TOP-REAL 3 st P = Dir u & u.3 = 1 &
(u.1)^2 + (u.2)^2 = 1 & P1 = Dir |[- u.2,u.1,0]| and
A5: ex u be non zero Element of TOP-REAL 3 st P = Dir u & u.3 = 1 &
(u.1)^2 + (u.2)^2 = 1 & P2 = Dir |[- u.2,u.1,0]|;
consider u1 be non zero Element of TOP-REAL 3 such that
A6: P = Dir u1 & u1.3 = 1 & (u1.1)^2 + (u1.2)^2 = 1 &
P1 = Dir |[- u1.2,u1.1,0]| by A4;
consider u2 being non zero Element of TOP-REAL 3 such that
A7: P = Dir u2 & u2.3 = 1 & (u2.1)^2 + (u2.2)^2 = 1 &
P2 = Dir |[- u2.2,u2.1,0]| by A5;
A8: |[-u2.2,u2.1,0]| is non zero by A7,BKMODEL1:91;
A9: |[-u1.2,u1.1,0]| is non zero by A6,BKMODEL1:91;
are_Prop u1,u2 by A6,A7,ANPROJ_1:22;
then consider a be Real such that
A10: a <> 0 and
A11: u2 = a * u1 by ANPROJ_1:1;
A12: - u2.2 = - a * u1.2 by A11,RVSUM_1:44
.= a * (- u1.2);
|[-u2.2,u2.1,0]| = |[ a * (- u1.2), a * u1.1 , a * 0]|
by A11,RVSUM_1:44,A12
.= a * |[- u1.2,u1.1,0]| by EUCLID_5:8;
then are_Prop |[-u2.2,u2.1,0]|,|[-u1.2,u1.1,0]| by A10,ANPROJ_1:1;
hence thesis by A8,A9,A6,A7,ANPROJ_1:22;
end;
end;
theorem Th19:
for P being Element of absolute holds P <> pole_infty P
proof
let P be Element of absolute;
assume
A1: P = pole_infty P;
consider u being non zero Element of TOP-REAL 3 such that
A2: P = Dir u & u.3 = 1 & (u.1)^2 + (u.2)^2 = 1 &
pole_infty P = Dir |[- u.2,u.1,0]| by Def03;
A3: |[-u.2,u.1,0]| is non zero by A2,BKMODEL1:91;
are_Prop u,|[-u.2,u.1,0]| by A1,A2,A3,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A4: u = a * |[-u.2,u.1,0]| by ANPROJ_1:1;
1 = a * (|[-u.2,u.1,0]|).3 by A2,A4,RVSUM_1:44
.= a * (|[-u.2,u.1,0]|)`3 by EUCLID_5:def 3
.= a * 0 by EUCLID_5:2
.= 0;
hence contradiction;
end;
theorem Th20:
for P1,P2 being Element of absolute st pole_infty P1 = pole_infty P2
holds P1 = P2 or (ex u being non zero Element of TOP-REAL 3 st
P1 = Dir u & P2 = Dir |[-u`1,-u`2,1]| & u`3 = 1)
proof
let P1,P2 be Element of absolute;
assume
A1: pole_infty P1 = pole_infty P2;
consider u1 be non zero Element of TOP-REAL 3 such that
A2: P1 = Dir u1 & u1.3 = 1 & (u1.1)^2 + (u1.2)^2 = 1 &
pole_infty P1 = Dir |[- u1.2,u1.1,0]| by Def03;
consider u2 be non zero Element of TOP-REAL 3 such that
A3: P2 = Dir u2 & u2.3 = 1 & (u2.1)^2 + (u2.2)^2 = 1 &
pole_infty P2 = Dir |[- u2.2,u2.1,0]| by Def03;
reconsider w1 = |[- u1.2,u1.1,0]| as non zero Element of TOP-REAL 3
by A2,BKMODEL1:91;
reconsider w2 = |[- u2.2,u2.1,0]| as non zero Element of TOP-REAL 3
by A3,BKMODEL1:91;
are_Prop w1,w2 by A1,A2,A3,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A5: w1 = a * w2 by ANPROJ_1:1;
a * w2 = |[ a * (- u2.2), a * u2.1, a * 0 ]| by EUCLID_5:8; then
A6: - u1.2 = a * (- u2.2) & u1.1 = a * u2.1 by A5,FINSEQ_1:78; then
A7: 1 = (a * u2.1) * (a * u2.1) + (a * u2.2)^2 by A2
.= a * a * (u2.1 * u2.1 + u2.2 * u2.2)
.= a^2 by A3;
A8: a = 1 implies P1 = P2
proof
assume a = 1;
then u1`1 = u2.1 & u1`2 = u2.2 & u1`3 = u2.3
by A2,A3,A6,EUCLID_5:def 1,def 2,def 3; then
A9: u1`1 = u2`1 & u1`2 = u2`2 & u1`3 = u2`3 by EUCLID_5:def 1,def 2,def 3;
u1 = |[u1`1,u1`2,u1`3]| by EUCLID_5:3
.= u2 by A9,EUCLID_5:3;
hence thesis by A2,A3;
end;
a = -1 implies ex u being non zero Element of TOP-REAL 3 st
P1 = Dir u & P2 = Dir |[-u`1,-u`2,1]| & u`3 = 1
proof
assume a = -1;
then u1`1 = - u2.1 & u1`2 = - u2.2 & u2`3 = 1
by A3,A6,EUCLID_5:def 1,def 2,def 3; then
A10: u1`1 = - u2`1 & u1`2 = - u2`2 & u2`3 = 1 by EUCLID_5:def 1,def 2;
take u1;
thus thesis by A10,EUCLID_5:3,A3,A2,EUCLID_5:def 3;
end;
hence thesis by A7,A8,SQUARE_1:41;
end;
definition
let P being Element of absolute;
func tangent P -> LINE of real_projective_plane means
:Def04:
ex p being Element of real_projective_plane st p = P &
it = Line(p,pole_infty P);
existence
proof
reconsider p = P as Element of real_projective_plane;
reconsider L = Line(p,pole_infty P) as LINE of real_projective_plane
by Th19,COLLSP:def 7;
take L;
thus thesis;
end;
uniqueness;
end;
theorem Th21:
for P being Element of absolute holds P in tangent P
proof
let P be Element of absolute;
ex p be Element of real_projective_plane st p = P &
tangent P = Line(p,pole_infty P) by Def04;
hence thesis by COLLSP:10;
end;
theorem Th22:
for P being Element of absolute holds tangent P /\ absolute = {P}
proof
let P be Element of absolute;
A1: {P} c= tangent P /\ absolute
proof
let x be object;
assume x in {P};
then x = P by TARSKI:def 1;
then x in tangent P & x in absolute by Th21;
hence x in tangent P /\ absolute by XBOOLE_0:def 4;
end;
tangent P /\ absolute c= {P}
proof
let x be object;
assume
A2: x in tangent P /\ absolute;
then reconsider y = x as Element of real_projective_plane;
consider p being Element of real_projective_plane such that
A3: p = P and
A4: tangent P = Line(p,pole_infty P) by Def04;
y in Line(p,pole_infty P) by A2,A4,XBOOLE_0:def 4;
then
A5: p,pole_infty P,y are_collinear by COLLSP:11;
consider u be Element of TOP-REAL 3 such that
A6: u is non zero and
A7: p = Dir u by ANPROJ_1:26;
consider v be non zero Element of TOP-REAL 3 such that
A8: P = Dir v & v.3 = 1 & (v.1)^2 + (v.2)^2 = 1 &
pole_infty P = Dir |[- v.2,v.1,0]| by Def03;
are_Prop u,v by A6,A7,A8,A3,ANPROJ_1:22;
then consider a be Real such that
A9: a <> 0 and
A10: u = a * v by ANPROJ_1:1;
A11: u`1 = u.1 by EUCLID_5:def 1
.= a * v.1 by A10,RVSUM_1:44;
A12: u`2 = u.2 by EUCLID_5:def 2
.= a * v.2 by A10,RVSUM_1:44;
A13: u`3 = u.3 by EUCLID_5:def 3
.= a * 1 by A8,A10,RVSUM_1:44
.= a;
y is Element of absolute by A2,XBOOLE_0:def 4;
then consider w be non zero Element of TOP-REAL 3 such that
A14: (w.1)^2 + (w.2)^2 = 1 and
A15: w.3 = 1 and
A16: y = Dir w by BKMODEL1:89;
A17: |[-v.2,v.1,0]|`1 = -v.2 & |[-v.2,v.1,0]|`2 = v.1 & |[-v.2,v.1,0]|`3 = 0
by EUCLID_5:2;
|[-v.2,v.1,0]| is non zero by A8,BKMODEL1:91;
then 0 = |{ u,|[-v.2,v.1,0]|,w }| by A5,A6,A7,A8,A16,BKMODEL1:1
.= u`1 * v.1 * w`3 - u`3 * v.1 *w`1 - u`1* 0 *w`2
+ u`2* 0 *w`1 - u`2*(-v.2)* w`3
+ u`3*(-v.2)* w`2 by A17,ANPROJ_8:27
.= u`1 * v.1 * w.3 - u`3 * v.1 *w`1 - u`2*(-v.2)*w`3
+ u`3*(-v.2)* w`2 by EUCLID_5:def 3
.= u`1 * v.1 * 1 - u`3 * v.1 *w`1 - u`2*(-v.2) * 1
+ u`3 *(-v.2)* w`2 by A15,EUCLID_5:def 3
.= a * (v.1 * v.1 + v.2 * v.2 - v.1 * w`1 - v.2 * w`2)
by A11,A12,A13
.= a * (1 - v.1 * w`1 - v.2 * w`2) by A8;
then 1 - v.1 * w`1 - v.2 * w`2 = 0 by A9; then
A18: 1 = v.1 * w`1 + v.2 * w`2
.= v.1 * w.1 + v.2 * w`2 by EUCLID_5:def 1
.= v.1 * w.1 + v.2 * w.2 by EUCLID_5:def 2;
then
A19: v.1 * w.2 = v.2 * w.1 by BKMODEL1:7,A14,A8;
x = P
proof
per cases;
suppose
A20: v.2 = 0;
then v.1 <> 0 by A8; then
A21: w.2 = 0 by A19,A20;
per cases by A20,A8,BKMODEL1:8;
suppose
A22: v.1 = 1;
per cases by A21,A14,BKMODEL1:8;
suppose w.1 = 1;
then w`1 = 1 & w`2 = 0 & w`3 = 1 & v`1 = 1 & v`2 = 0 & v`3 = 1
by A8,A20,A22,A19,A15,EUCLID_5:def 1,def 2,def 3;
then v = |[w`1,w`2,w`3]| by EUCLID_5:3
.= w by EUCLID_5:3;
hence x = P by A8,A16;
end;
suppose w.1 = -1;
hence x = P by A18,A20,A22;
end;
end;
suppose
A23: v.1 = -1;
per cases by A21,A14,BKMODEL1:8;
suppose w.1 = 1;
hence x = P by A18,A20,A23;
end;
suppose w.1 = -1;
then w`1 = -1 & w`2 = 0 & w`3 = 1 & v`1 = -1 & v`2 = 0 & v`3 = 1
by A23,A8,A20,A19,A15,EUCLID_5:def 1,def 2,def 3;
then v = |[w`1,w`2,w`3]| by EUCLID_5:3
.= w by EUCLID_5:3;
hence x = P by A8,A16;
end;
end;
end;
suppose
A24: v.2 <> 0;
per cases;
suppose
A25: v.1 = 0;
then per cases by A8,BKMODEL1:8;
suppose
A26: v.2 = 1;
A27: v.2 * w.1 = 0 * w.2 by A25,A18,BKMODEL1:7,A14,A8
.= 0;
then w.1 = 0 by A24;
then per cases by A14,BKMODEL1:8;
suppose w.2 = 1;
then
A28: w`1 = 0 & w`2 = 1 & w`3 = 1 & v`1 = 0 & v`2 = 1 & v`3 = 1
by A25,A26,A27,A8,A15,EUCLID_5:def 1,def 2,def 3;
v = |[w`1,w`2,w`3]| by A28,EUCLID_5:3
.= w by EUCLID_5:3;
hence x = P by A8,A16;
end;
suppose w.2 = -1;
hence x = P by A18,A25,A26;
end;
end;
suppose
A29: v.2 = -1;
A30: v.2 * w.1 = 0 * w.2 by A25,A18,BKMODEL1:7,A14,A8
.= 0;
then w.1 = 0 by A24;
then per cases by A14,BKMODEL1:8;
suppose w.2 = 1;
hence x = P by A18,A25,A29;
end;
suppose w.2 = -1;
then
A31: w`1 = 0 & w`2 = -1 & w`3 = 1 & v`1 = 0 & v`2 = -1 & v`3 = 1
by A29,A25,A30,A8,A15,EUCLID_5:def 1,def 2,def 3;
v = |[w`1,w`2,w`3]| by A31,EUCLID_5:3
.= w by EUCLID_5:3;
hence x = P by A8,A16;
end;
end;
end;
suppose v.1 <> 0;
then reconsider l = v.1 / v.2 as non zero Real by A24;
A32: l * v.2 = v.1 by XCMPLX_1:87,A24;
A33: l * w.2 = (v.1 * w.2) / v.2 by XCMPLX_1:74
.= (v.2 * w.1) / v.2 by A18,BKMODEL1:7,A14,A8
.= w.1 by XCMPLX_1:89,A24;
per cases by A32,A8,BKMODEL1:10;
suppose
A34: v.2 = 1 / sqrt(1+l^2);
per cases by A33,A14,BKMODEL1:10;
suppose w.2 = 1 / sqrt(1+l^2);
then w`1 = v.1 & w`2 = v.2 & w`3 = v.3
by A8,A15,A34,A32,A33,EUCLID_5:def 1,def 2,def 3;
then w`1 = v`1 & w`2 = v`2 & w`3 = v`3
by EUCLID_5:def 1,def 2,def 3;
then v = |[w`1,w`2,w`3]| by EUCLID_5:3
.= w by EUCLID_5:3;
hence x = P by A8,A16;
end;
suppose
A35: w.2 = (-1)/sqrt(1+l^2);
0 <= l^2 by SQUARE_1:12;
then
A36: (sqrt(1+l^2))^2 = 1 + l*l by SQUARE_1:def 2;
v.1 * w.1 + v.2 * w.2 = l * (1/sqrt(1+l^2)) * l
* ((-1)/sqrt(1+l^2)) + v.2 * w.2
by A34,A35,A32,A33
.= -1 by A34,A35,A36,BKMODEL1:11;
hence x = P by A18;
end;
end;
suppose
A37: v.2 = (-1) / sqrt(1+l^2);
per cases by A33,A14,BKMODEL1:10;
suppose
A38: w.2 = 1 / sqrt(1+l^2);
0 <= l^2 by SQUARE_1:12; then
A39: (sqrt(1+l^2))^2 = 1 + l*l by SQUARE_1:def 2;
v.1 * w.1 + v.2 * w.2 = l * (1/sqrt(1+l^2)) * l
* ((-1)/sqrt(1+l^2)) +
(1/sqrt(1+l^2)) * ((-1)/sqrt(1+l^2))
by A37,A38,A32,A33
.= -1 by A39,BKMODEL1:11;
hence x = P by A18;
end;
suppose w.2 = (-1) / sqrt(1+l^2);
then w`1 = v.1 & w`2 = v.2 & w`3 = v.3
by A8,A15,A37,A32,A33,EUCLID_5:def 1,def 2,def 3;
then w`1 = v`1 & w`2 = v`2 & w`3 = v`3
by EUCLID_5:def 1,def 2,def 3;
then v = |[w`1,w`2,w`3]| by EUCLID_5:3
.= w by EUCLID_5:3;
hence x = P by A8,A16;
end;
end;
end;
end;
end;
hence thesis by TARSKI:def 1;
end;
hence thesis by A1;
end;
theorem Th23:
for P1,P2 being Element of absolute st tangent P1 = tangent P2 holds P1 = P2
proof
let P1,P2 be Element of absolute;
assume
A1: tangent P1 = tangent P2;
absolute /\ tangent P1 = {P1} & absolute /\ tangent P2 = {P2} by Th22;
hence thesis by A1,ZFMISC_1:3;
end;
theorem Th24:
for P,Q being Element of absolute holds
ex R being Element of real_projective_plane st
R in tangent P & R in tangent Q
proof
let P,Q being Element of absolute;
reconsider pP = tangent P,pQ = tangent Q as
LINE of IncProjSp_of real_projective_plane by INCPROJ:4;
consider R being POINT of IncProjSp_of real_projective_plane such that
A1: R on pP and
A2: R on pQ by BKMODEL1:75,INCPROJ:def 9;
reconsider S = R as Element of real_projective_plane by INCPROJ:3;
S in tangent P & S in tangent Q by A1,A2,INCPROJ:5;
hence thesis;
end;
theorem Th25:
for P1,P2 being Element of absolute st P1 <> P2 holds
ex P being Element of real_projective_plane st tangent P1 /\ tangent P2 = {P}
proof
let P1,P2 be Element of absolute;
assume P1 <> P2;
then tangent P1 <> tangent P2 by Th23;
hence thesis by COLLSP:21,BKMODEL1:76;
end;
theorem Th26:
for M being Matrix of 3,REAL
for P being Element of absolute
for Q being Element of real_projective_plane
for u,v being non zero Element of TOP-REAL 3
for fp,fq being FinSequence of REAL st
M = symmetric_3(1,1,-1,0,0,0) &
P = Dir u & Q = Dir v &
u = fp & v = fq &
Q in tangent P holds SumAll QuadraticForm(fq,M,fp) = 0
proof
let M being Matrix of 3,REAL;
let P being Element of absolute;
let Q being Element of real_projective_plane;
let u,v being non zero Element of TOP-REAL 3;
let fp,fq being FinSequence of REAL;
assume that
A1: M = symmetric_3(1,1,-1,0,0,0) and
A2: P = Dir u and
A3: Q = Dir v and
A4: u = fp and
A5: v = fq and
A6: Q in tangent P;
consider p be Element of real_projective_plane such that
A7: p = P and
A8: tangent P = Line(p,pole_infty P) by Def04;
A9: p,pole_infty P,Q are_collinear by A6,A8,COLLSP:11;
consider w be non zero Element of TOP-REAL 3 such that
A10: P = Dir w & w.3 = 1 & (w.1)^2 + (w.2)^2 = 1 &
pole_infty P = Dir |[- w.2,w.1,0]| by Def03;
are_Prop w,u by A2,A10,ANPROJ_1:22;
then consider aa be Real such that
A11: aa <> 0 and
A12: w = aa * u by ANPROJ_1:1;
A13: w.1 = aa * u`1 & w.2 = aa * u`2 & w.3 = aa * u`3
proof
thus w.1 = aa * u.1 by A12,RVSUM_1:44
.= aa * u`1 by EUCLID_5:def 1;
thus w.2 = aa * u.2 by A12,RVSUM_1:44
.= aa * u`2 by EUCLID_5:def 2;
thus w.3 = aa * u.3 by A12,RVSUM_1:44
.= aa * u`3 by EUCLID_5:def 3;
end;
then 1 * w.1 = aa * u`1 & 1 * w.2 = aa * u`2 & 1 = aa * u`3 by A10;
then
A14: (aa * (1/aa)) * w.1 = aa * u`1 & (aa * (1/aa)) * w.2 = aa * u`2 &
(aa * (1/aa)) * 1 = aa * u`3 by A11,XCMPLX_1:106;
A16: 1 = aa^2 * (u`1 * u`1 + u`2 * u`2) by A13,A10;
A17: |[ -w.2,w.1,0]|`1 = - aa * u`2 & |[ -w.2,w.1,0]|`2 = aa * u`1 &
|[ -w.2,w.1,0]|`3 = 0 by A13,EUCLID_5:2;
|[-w.2,w.1,0]| is non zero by BKMODEL1:91,A10;
then 0 = |{u, |[-w.2,w.1,0]| ,v}| by A7,A10,A2,A3,A9,BKMODEL1:1
.= u`1 * |[-w.2,w.1,0]|`2 * v`3 - u`3*|[-w.2,w.1,0]|`2*v`1
- u`1*|[-w.2,w.1,0]|`3*v`2 + u`2*|[-w.2,w.1,0]|`3*v`1
- u`2*|[-w.2,w.1,0]|`1*v`3 + u`3*|[-w.2,w.1,0]|`1*v`2
by ANPROJ_8:27
.= aa * (u`1 * u`1 * v`3 - u`1 * u`3 * v`1 + u`2 * u`2 *v`3
- u`2 *u`3 * v`2) by A17;
then 0 = v`3 * (u`1 * u`1 + u`2 * u`2) - u`3 * (u`1 * v`1 + u`2 * v`2)
by A11
.= v`3 * (1/(aa^2)) - u`3 * (u`1 * v`1 + u`2 * v`2)
by A16,XCMPLX_1:73
.= v`3 * (1/(aa^2)) - (1/aa) * (u`1 * v`1 + u`2 * v`2)
by A14,A11,XCMPLX_1:5
.= v`3 * ((1/aa) * (1/aa)) - (1/aa) * (u`1 * v`1 + u`2 * v`2)
by XCMPLX_1:102
.= (1/aa) * (v`3 * (1/aa) - (u`1 * v`1 + u`2 * v`2));
then
A18: v`3 * (1/aa) - (u`1 * v`1 + u`2 * v`2) = 0 by A11;
A19: len fp = width M & len fq = len M & len fp = len M &
len fq = width M & len fp > 0 & len fq > 0
proof
len M = 3 & width M = 3 by MATRIX_0:24;
hence thesis by A5,FINSEQ_3:153,A4;
end;
then
A20: SumAll QuadraticForm(fq,M,fp) = |(fq * M,fp)| by MATRPROB:46
.= |(fq,M * fp)| by A19,MATRPROB:47;
A21: M * fp = Col(M * (ColVec2Mx fp),1) by MATRIXR1:def 11;
A22: fp is Element of REAL 3 by A4,EUCLID:22; then
A23: len fp = 3 by EUCLID_8:50;
reconsider fa = 1, fb = -1 ,z = 0 as Element of F_Real by XREAL_0:def 1;
A24: M = <* <* fa,z,z *>,
<* z,fa,z *>,
<* z,z,fb *> *> by A1,PASCAL:def 3;
reconsider fp1 = fp.1,fp2 = fp.2, fp3 = fp.3 as Element of F_Real
by XREAL_0:def 1;
A25: ColVec2Mx fp = MXR2MXF ColVec2Mx fp by MATRIXR1:def 1
.= <*fp*>@ by A22,ANPROJ_8:72
.= F2M fp by A22,ANPROJ_8:88,EUCLID_8:50
.= <* <* fp1 *>,<* fp2 *>, <* fp3 *> *> by A23,ANPROJ_8:def 1;
reconsider M1 = M as Matrix of 3,3,F_Real;
reconsider M2 = <* <* fp1 *>,<* fp2 *>, <* fp3 *> *>
as Matrix of 3,1,F_Real
by ANPROJ_8:4;
A26: for n,k,m be Nat for A be Matrix of n,k,F_Real
for B be Matrix of width A,m,F_Real
holds A*B is Matrix of len A,width B,F_Real;
A27: len M1 = 3 & width M2 = 1 by MATRIX_0:23;
width M1 = 3 by MATRIX_0:23; then
A28: M1 * M2 is Matrix of 3,1,F_Real by A26,A27;
A29: M * ColVec2Mx fp = M1 * M2 by A25,ANPROJ_8:17;
M * ColVec2Mx fp = M1 * M2 by A25,ANPROJ_8:17
.= <* <* fa * fp1 + z * fp2 + z * fp3 *> ,
<* z * fp1 + fa * fp2 + z * fp3 *>,
<* z * fp1 + z * fp2 + fb * fp3 *> *>
by A24,ANPROJ_9:7;
then SumAll QuadraticForm(fq,M,fp)
= |(v, |[ fp1,fp2,-fp3 ]| )| by A5,A20,A21,A28,A29,ANPROJ_8:5
.= v`1 * |[ fp1,fp2,-fp3 ]|`1 + v`2 * |[ fp1,fp2,-fp3 ]|`2
+ v`3 * |[ fp1,fp2,-fp3 ]|`3 by EUCLID_5:29
.= v`1 * fp1 + v`2 * |[ fp1,fp2,-fp3 ]|`2 + v`3 * |[ fp1,fp2,-fp3 ]|`3
by EUCLID_5:2
.= v`1 * fp1 + v`2 * fp2 + v`3 * |[ fp1,fp2,-fp3 ]|`3 by EUCLID_5:2
.= v`1 * fp1 + v`2 * fp2 + v`3 * (-fp3) by EUCLID_5:2
.= v`1 * u.1 + v`2 * u.2 - v`3 * u.3 by A4
.= v`1 * u`1 + v`2 * u.2 - v`3 * u.3 by EUCLID_5:def 1
.= v`1 * u`1 + v`2 * u`2 - v`3 * u.3 by EUCLID_5:def 2
.= v`1 * u`1 + v`2 * u`2 - v`3 * u`3 by EUCLID_5:def 3
.= 0 by A18,A14,A11,XCMPLX_1:5;
hence thesis;
end;
theorem Th27:
for P,Q,R being Element of absolute for P1,P2,P3,P4 being
Point of real_projective_plane st P,Q,R are_mutually_distinct &
P1 = P & P2 = Q & P3 = R & P4 in tangent P & P4 in tangent Q holds
not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear &
not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear
proof
let P,Q,R be Element of absolute;
let P1,P2,P3,P4 be Point of real_projective_plane;
assume that
A1: P,Q,R are_mutually_distinct and
A2: P1 = P & P2 = Q & P3 = R and
A3: P4 in tangent P and
A4: P4 in tangent Q;
A5: not P4 in absolute
proof
assume P4 in absolute;
then P4 in absolute /\ tangent P & P4 in absolute /\ tangent Q
by A3,A4,XBOOLE_0:def 4;
then P4 in {P} & P4 in {Q} by Th22;
then P4 = P & P4 = Q by TARSKI:def 1;
hence contradiction by A1;
end;
consider p being Element of real_projective_plane such that
A6: p = P and
A7: tangent P = Line(p,pole_infty P) by Def04;
A8: p,pole_infty P,P4 are_collinear by A3,A7,COLLSP:11;
A9: P4 <> p by A6,A5;
consider q being Element of real_projective_plane such that
A10: q = Q and
A11: tangent Q = Line(q,pole_infty Q) by Def04;
A12: P4 <> q by A10,A5;
A13: q,pole_infty Q,P4 are_collinear by A4,A11,COLLSP:11;
thus not P1,P2,P3 are_collinear by A1,A2,BKMODEL1:92;
thus not P1,P2,P4 are_collinear
proof
assume
A14: P1,P2,P4 are_collinear;
now
thus P4 <> p by A6,A5;
thus P4,p,p are_collinear by COLLSP:2;
p,P4,pole_infty P are_collinear by A8,COLLSP:4;
hence P4,p,pole_infty P are_collinear by COLLSP:7;
p,P4,q are_collinear by A14,A2,A6,A10,COLLSP:4;
hence P4,p,q are_collinear by COLLSP:4;
end;
then Q in tangent P by A10,A7,COLLSP:3,11;
then Q in absolute /\ tangent P by XBOOLE_0:def 4;
then Q in {P} by Th22;
hence contradiction by A1,TARSKI:def 1;
end;
thus not P1,P3,P4 are_collinear
proof
assume P1,P3,P4 are_collinear;
then
A15: p,P4,P3 are_collinear by A2,A6,COLLSP:4;
p,P4,pole_infty P are_collinear by A8,COLLSP:4;
then P3 in tangent P by A9,A15,A7,COLLSP:6,11;
then P3 in absolute /\ tangent P by A2,XBOOLE_0:def 4;
then P3 in {P} by Th22;
hence contradiction by A1,A2,TARSKI:def 1;
end;
thus not P2,P3,P4 are_collinear
proof
assume P2,P3,P4 are_collinear;
then
A16: q,P4,P3 are_collinear by A2,A10,COLLSP:4;
q,P4,pole_infty Q are_collinear by A13,COLLSP:4;
then P3 in tangent Q by A16,A12,A11,COLLSP:6,11;
then P3 in absolute /\ tangent Q by A2,XBOOLE_0:def 4;
then P3 in {Q} by Th22;
hence contradiction by A1,A2,TARSKI:def 1;
end;
end;
theorem
for P,Q being Element of absolute
for R being Element of real_projective_plane
for u,v,w being non zero Element of TOP-REAL 3 st P = Dir u & Q = Dir v &
R = Dir w & R in tangent P & R in tangent Q & u.3 = 1 & v.3 = 1 &
w.3 = 0 holds P = Q or (u.1 = -v.1 & u.2 = -v.2)
proof
let P,Q being Element of absolute;
let R being Element of real_projective_plane;
let u,v,w being non zero Element of TOP-REAL 3;
assume that
A1: P = Dir u & Q = Dir v & R = Dir w & R in tangent P &
R in tangent Q & u.3 = 1 & v.3 = 1 & w.3 = 0;
assume
A2: P <> Q;
|[u.1,u.2]| in circle(0,0,1) & |[v.1,v.2]| in circle(0,0,1)
by A1,BKMODEL1:84; then
A3: (u.1)^2 + (u.2)^2 = 1 & (v.1)^2 + (v.2)^2 = 1 by BKMODEL1:13;
reconsider M = symmetric_3(1,1,-1,0,0,0) as Matrix of 3,REAL;
reconsider fp = u, fq = v,fr = w as FinSequence of REAL by EUCLID:24;
reconsider fr1 = w`1,fr2 = w`2, fr3 = w`3 as Element of REAL
by XREAL_0:def 1;
A4: fr = <* fr1,fr2,fr3 *> by EUCLID_5:3;
A5: SumAll QuadraticForm(fr,M,fp) = 0 &
SumAll QuadraticForm(fr,M,fq) = 0 by A1,Th26;
u is Element of REAL 3 & v is Element of REAL 3 &
w is Element of REAL 3 by EUCLID:22; then
A6: len fp = 3 & len fq = 3 & len fr = 3 by EUCLID_8:50;
len fr = len M & len fp = width M & len fp > 0 &
len fq = width M & len fq > 0 by A6,MATRIX_0:24;
then
A7: |( fr, M * fp )| = 0 & |( fr, M * fq )| = 0 by A5,MATRPROB:44;
reconsider m1 = 1,m2 = 0,m3 = 0,m4 = 0,m5 = 1,m6 = 0,m7 = 0,
m8 = 0,m9 = -1 as Element of REAL by XREAL_0:def 1;
A8: M = <* <* m1,m2,m3 *>,
<* m4,m5,m6 *>,
<* m7,m8,m9 *> *> by PASCAL:def 3;
reconsider fp1 = u`1,fp2 = u`2,fp3 = u`3,
fq1 = v`1,fq2 = v`2, fq3 = v`3 as Element of REAL by XREAL_0:def 1;
A9: u.1 = fp1 & u.2 = fp2 & v.1 = fq1 & v.2 = fq2 &
fp3 = 1 & fq3 = 1 & fr3 = 0 by A1,EUCLID_5:def 1,def 2,def 3;
A10: fp = <*fp1,fp2,fp3*> & fq = <*fq1,fq2,fq3*> &
fr = <* fr1,fr2,fr3 *> by EUCLID_5:3;
then M * fp = <* 1 * fp1 + 0 * fp2 + 0 * fp3,
0 * fp1 + 1 * fp2 + 0 * fp3,
0 * fp1 + 0 * fp2 +(-1) * fp3 *> by A8,PASCAL:9
.= <* fp1,fp2,-fp3 *>;
then
A11: fr1 * fp1 + fr2 * fp2 + fr3 * (-fp3) = 0 by A7,A4,EUCLID_5:30;
M * fq = <* 1 * fq1 + 0 * fq2 + 0 * fq3,
0 * fq1 + 1 * fq2 + 0 * fq3,
0 * fq1 + 0 * fq2 +(-1) * fq3 *> by A10,A8,PASCAL:9
.= <* fq1,fq2,-fq3 *>;
then
A12: fr1 * fq1 + fr2 * fq2 + fr3 * (-fq3) = 0 by A7,A4,EUCLID_5:30;
A13: fr3 = 0 by A1,EUCLID_5:def 3;
per cases;
suppose
A14: fr2 = 0;
then fr1 <> 0 by A10,EUCLID_5:4,A1;
then
A15: fp1 = 0 & fq1 = 0 by A14,A13,A11,A12;
then (fp2 = 1 or fp2 = -1) & (fq2 = 1 or fq2 = -1) by SQUARE_1:41,A9,A3;
hence thesis by A1,A2,A15,A10;
end;
suppose
A16: fr2 <> 0;
fq1 * (fr1 * fp1 + fr2 * fp2) = 0 & fp1 * (fr1 * fq1 + fr2 * fq2) = 0
by A13,A11,A12;
then fr2 * (fq1 * fp2 - fp1 * fq2) = 0;
then
A17: fq1 * fp2 - fp1 * fq2 = 0 by A16;
per cases;
suppose
A18: fp2 = 0; then
fp1 = 0 or fq2 = 0 by A17; then
(fq1 = 1 or fq1 = -1) & (fp1 = 1 or fp1 = -1) by SQUARE_1:41,
A3,A9,A18;
hence thesis by A1,A2,A10,A17;
end;
suppose
A20: fp2 <> 0;
per cases;
suppose fp1 = 0;
hence thesis by A9,A11,A16,A20;
end;
suppose
A21: fp1 <> 0;
reconsider l = fq1 / fp1 as Real;
A22: l = fq2 / fp2
proof
fq1 = fq1 * (fp2 / fp2) by XCMPLX_1:88,A20
.= fp1 * fq2 / fp2 by A17,XCMPLX_1:74
.= fp1 * (fq2 / fp2) by XCMPLX_1:74;
hence thesis by A21,XCMPLX_1:89;
end;
then
A23: fq1 = l * fp1 & fq2 = l * fp2 by A21,A20,XCMPLX_1:87;
v.1 = l * fp1 & v.2 = l * fp2 by A22,A9,A21,A20,XCMPLX_1:87;
then l = 1 or l = -1 by A9,A3,BKMODEL1:3;
hence thesis by A1,A2,A10,A23;
end;
end;
end;
end;
theorem Th28:
for P being Element of absolute
for R being Element of real_projective_plane
for u being non zero Element of TOP-REAL 3 st
R in tangent P & R = Dir u & u.3 = 0 holds R = pole_infty P
proof
let P be Element of absolute;
let R be Element of real_projective_plane;
let u be non zero Element of TOP-REAL 3;
assume that
A1: R in tangent P and
A2: R = Dir u and
A3: u.3 = 0;
consider w be non zero Element of TOP-REAL 3 such that
A4: P = Dir w & w.3 = 1 & (w.1)^2 + (w.2)^2 = 1 &
pole_infty P = Dir |[- w.2,w.1,0]| by Def03;
consider v be non zero Element of TOP-REAL 3 such that
A5: (v.1)^2 + (v.2)^2 = 1 & v.3 = 1 & P = Dir v by BKMODEL1:89;
reconsider M = symmetric_3(1,1,-1,0,0,0) as Matrix of 3,REAL;
reconsider fp = v, fr = u as FinSequence of REAL by EUCLID:24;
reconsider fr1 = u`1,fr2 = u`2, fr3 = u`3 as Element of REAL
by XREAL_0:def 1;
A6: fr = <* fr1,fr2,fr3 *> by EUCLID_5:3;
A7: SumAll QuadraticForm(fr,M,fp) = 0 by A2,A1,A5,Th26;
u is Element of REAL 3 & v is Element of REAL 3 by EUCLID:22;
then
A8: len fp = 3 & len fr = 3 by EUCLID_8:50;
len M = 3 & width M = 3 by MATRIX_0:24; then
A9: |( fr, M * fp )| = 0 by A7,A8,MATRPROB:44;
reconsider m1 = 1,m2 = 0,m3 = 0,m4 = 0,m5 = 1,m6 = 0,m7 = 0,
m8 = 0,m9 = -1 as Element of REAL by XREAL_0:def 1;
A10: M = <* <* m1,m2,m3 *>,
<* m4,m5,m6 *>,
<* m7,m8,m9 *> *> by PASCAL:def 3;
reconsider fp1 = v`1,fp2 = v`2,fp3 = v`3 as Element of REAL
by XREAL_0:def 1;
A11: v.1 = fp1 & v.2 = fp2 & fp3 = 1 & fr3 = 0
by A3,A5,EUCLID_5:def 1,def 2,def 3;
A12: fp = <*fp1,fp2,fp3*> & fr = <* fr1,fr2,fr3 *> by EUCLID_5:3;
then M * fp = <* 1 * fp1 + 0 * fp2 + 0 * fp3,
0 * fp1 + 1 * fp2 + 0 * fp3,
0 * fp1 + 0 * fp2 +(-1) * fp3 *> by A10,PASCAL:9
.= <* fp1,fp2,-fp3 *>;
then
A13: fr1 * fp1 + fr2 * fp2 + fr3 * (-fp3) = 0
by A9,A6,EUCLID_5:30;
per cases;
suppose
A14: fr1 = 0;
then
A15: fr2 <> 0 by A12,EUCLID_5:4,A3;
then
A16: fp2 = 0 by A14,A11,A13;
A17: w.1 = v.1 by A4,A5,BKMODEL1:43
.= fp1 by EUCLID_5:def 1;
A18: w.2 = v.2 by A4,A5,BKMODEL1:43
.= 0 by A15,A14,A11,A13;
now
A19: fp1 <> 0 by A5,A16,A11;
thus |[0,fp1,0]| is non zero
by A5,A16,A11,FINSEQ_1:78,EUCLID_5:4;
thus are_Prop u, |[0,fp1,0]|
proof
u = |[ (fr2/fp1) * 0, (fr2/fp1) * fp1, (fr2/fp1) * 0 ]|
by A16,A11,A5,XCMPLX_1:87,A12,A14
.= (fr2/fp1) * |[ 0,fp1,0 ]| by EUCLID_5:8;
hence thesis by A15,A19,ANPROJ_1:1;
end;
end;
hence thesis by A2,ANPROJ_1:22,A4,A17,A18;
end;
suppose
A20: fr1 <> 0;
A21: fp2 <> 0
proof
assume
A22: fp2 = 0;
then fp1 = 0 by A13,A11,A20;
hence contradiction by A22,A11,A5;
end;
then
A23: fr2 = (fp1 * (-fr1)) / fp2 by A13,A11,XCMPLX_1:89
.= fp1 * ((-fr1) / fp2) by XCMPLX_1:74;
reconsider l = (-fr1)/fp2 as non zero Real by A20,A21;
A24: now
thus |[-fp2,fp1,0]| is non zero by A21,FINSEQ_1:78,EUCLID_5:4;
fr1 = - (-fr1)
.= - (l * fp2) by A21,XCMPLX_1:87;
then fr = |[ l * (- fp2), l * fp1, l * 0 ]|
by A23,A12,A3
.= l * |[ - fp2,fp1,0]| by EUCLID_5:8;
hence are_Prop u, |[ -fp2,fp1,0]| by ANPROJ_1:1;
end;
w = v by BKMODEL1:43,A4,A5;
hence thesis by A24,A2,ANPROJ_1:22,A4,A11;
end;
end;
theorem Th29:
for a being non zero Real
for N being invertible Matrix of 3,F_Real st N = symmetric_3(a,a,-a,0,0,0)
holds homography(N).:absolute = absolute
proof
let a be non zero Real;
let N be invertible Matrix of 3,F_Real;
assume
A1: N = symmetric_3(a,a,-a,0,0,0);
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: (homography(N)).y = x by FUNCT_1:def 6;
A6: rng homography(N) c= the carrier of ProjectiveSpace TOP-REAL 3
by RELAT_1:def 19;
reconsider y9 = y as Element of ProjectiveSpace TOP-REAL 3 by A3;
consider u9 be non zero Element of TOP-REAL 3 such that
A7: (u9.1)^2 + (u9.2)^2 = 1 & u9.3 = 1 & y = Dir u9 by A4,BKMODEL1:89;
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
A8: y9 = Dir u & u is not zero & u = uf & p = N * uf & v = M2F p &
v is not zero & (homography(N)).y9 = Dir v by ANPROJ_8:def 4;
reconsider x9 = x as Element of ProjectiveSpace TOP-REAL 3
by A5,A3,A6,FUNCT_1:3;
reconsider z1 = 0,z2 = a,z3 = -a as Element of F_Real by XREAL_0:def 1;
A9: N = <* <* z2,z1,z1 *> ,
<* z1,z2,z1 *>,
<* z1,z1,z3 *> *> by A1,PASCAL:def 3;
reconsider ux = u`1,uy = u`2,uz = u`3 as Element of F_Real
by XREAL_0:def 1;
<* ux,uy,uz *> = uf by A8,EUCLID_5:3; then
A10: p = <* <* z2 * ux + z1 * uy + z1 * uz *>,
<* z1 * ux + z2 * uy + z1 * uz *>,
<* z1 * ux + z1 * uy + z3 * uz *> *> &
v = <* z2 * ux + z1 * uy + z1 * uz ,
z1 * ux + z2 * uy + z1 * uz ,
z1 * ux + z1 * uy + z3 * uz *> by A8,A9,PASCAL:8;
are_Prop u9,u by A7,A8,ANPROJ_1:22;
then consider l be Real such that
A11: l <> 0 and
A12: u9 = l * u by ANPROJ_1:1;
A13: u9.1 = l * u.1 & u9.2 = l * u.2 & u9.3 = l * u.3 by A12,RVSUM_1:44;
reconsider w = |[ - u.1 * l, - u.2 * l, u.3 * l ]|
as Element of TOP-REAL 3;
A15: w is non zero
proof
assume w is zero;
then u.1 = 0 & u.2 = 0 & u.3 = 0 by A11,FINSEQ_1:78,EUCLID_5:4;
then u`1 = 0 & u`2 = 0 & u`3 = 0 by EUCLID_5:def 1,def 2,def 3;
hence contradiction by A8,EUCLID_5:3,4;
end;
A16: (-1) * w`1 = (-1) * (-u.1 * l) & (-1) * w`2 = (-1) * (-u.2 * l) &
(-1) * w`3 = (-1) * (u.3 * l) by EUCLID_5:2;
then (-1) * w`1 = 1 * u.1 * l & (-1) * w`2 = 1 * u.2 * l &
(-1) * w`3 = -1 * u.3 * l; then
A17: (-1) * w`1 = u`1 * l & (-1) * w`2 = u`2 * l &
(-1) * w`3 = -1 * u`3 * l by EUCLID_5:def 1,def 2,def 3;
now
thus -a / l <> 0 by A11;
(-a / l) * w`1 = v`1 & (-a / l) * w`2 = v`2 &
(-a / l) * w`3 = v`3
proof
thus (-a / l) * w`1
= (a / l) * ((-1) * w`1)
.= (a / l) * (u`1 * l) by A16,EUCLID_5:def 1
.= a * u`1 by A11,XCMPLX_1:90
.= v`1 by A10,EUCLID_5:2;
thus (-a / l) * w`2
= (a / l) * ((-1) * w`2)
.= (a / l) * (u`2 * l) by A16,EUCLID_5:def 2
.= a * u`2 by A11,XCMPLX_1:90
.= v`2 by A10,EUCLID_5:2;
thus (-a / l) * w`3
= - (a / l) * (u`3 * l) by A17
.= - a * u`3 by A11,XCMPLX_1:90
.= v`3 by A10,EUCLID_5:2;
end;
then |[v`1,v`2,v`3]|
= (-a / l) * |[w`1,w`2,w`3]| by EUCLID_5:8
.= (-a / l) * w by EUCLID_5:3;
hence v = (-a / l) * w by EUCLID_5:3;
end;
then are_Prop w,v by ANPROJ_1:1; then
A18: Dir w = Dir v by ANPROJ_1:22,A15,A8;
A19: (w.1)^2 + (w.2)^2 = 1^2 & w.3 = 1
proof
thus 1^2 = ((l * u`1) * (l * u.1)) + ((l * u.2) * (l * u.2))
by EUCLID_5:def 1,A13,A7
.= ((l * u`1) * (l * u`1)) + ((l * u.2) * (l * u.2)) by EUCLID_5:def 1
.= ((l * u`1) * (l * u`1)) + ((l * u`2) * (l * u.2)) by EUCLID_5:def 2
.= ((-1) * w`1) * ((-1) * w`1) + ((-1) * w`2) * ((-1) * w`2)
by A17,EUCLID_5:def 2
.= w`1 * w`1 + w`2 * w`2
.= w.1 * w`1 + w`2 * w`2 by EUCLID_5:def 1
.= w.1 * w.1 + w`2 * w`2 by EUCLID_5:def 1
.= w.1 * w.1 + w.2 * w`2 by EUCLID_5:def 2
.= (w.1)^2 + (w.2)^2 by EUCLID_5:def 2;
thus w.3 = 1 by A13,A7;
end;
then |[w.1,w.2]| in circle(0,0,1) by BKMODEL1:14;
then x9 is Element of absolute by A15,A18,A8,A5,A19,BKMODEL1:86;
hence thesis;
end;
absolute c= homography(N).:absolute
proof
let x be object;
assume x in absolute;
then consider u be non zero Element of TOP-REAL 3 such that
A20: (u.1)^2 + (u.2)^2 = 1 & u.3 = 1 & x = Dir u by BKMODEL1:89;
reconsider w = |[ u.1 / a,u.2 / a, - u.3 / a ]| as Element of TOP-REAL 3;
A21: w is non zero
proof
assume w is zero;
then u.1 = 0 & u.2 = 0 & u.3 = 0 by FINSEQ_1:78,EUCLID_5:4;
then u`1 = 0 & u`2 = 0 & u`3 = 0 by EUCLID_5:def 1,def 2,def 3;
hence contradiction by EUCLID_5:3,4;
end;
then reconsider P = Dir w as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
reconsider v = |[ -u.1,-u.2,u.3 ]| as Element of TOP-REAL 3;
A22: (-a) * (u.1 / a) = - a * (u.1 /a)
.= - u.1 by XCMPLX_1:87;
A23: (-a) * (u.2 / a) = - a * (u.2 /a)
.= - u.2 by XCMPLX_1:87;
A24: (-a) * (- u.3 / a) = a * (u.3 /a)
.= u.3 by XCMPLX_1:87;
A25: v is non zero by A20,FINSEQ_1:78,EUCLID_5:4;
v = (-a) * w by A22,A23,A24,EUCLID_5:8;
then are_Prop v,w by ANPROJ_1:1; then
A26: P = Dir v by A21,A25,ANPROJ_1:22;
A27: v.3 = 1 by A20;
|[v.1,v.2]| in circle(0,0,1)
proof
(v.1)^2 + (v.2)^2 = 1^2 by A20;
hence thesis by BKMODEL1:14;
end;
then reconsider P as Element of absolute by A26,A27,A25,BKMODEL1:86;
now
dom homography(N) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
hence P in dom homography(N);
consider u1,v1 be Element of TOP-REAL 3,
uf be FinSequence of F_Real,
p be FinSequence of 1-tuples_on REAL
such that
A31: P = Dir u1 & u1 is not zero & u1 = uf & p = N * uf & v1 = M2F p &
v1 is not zero & homography(N).P = Dir v1 by ANPROJ_8:def 4;
are_Prop u1,w by A21,A31,ANPROJ_1:22;
then consider l be Real such that
A32: l <> 0 and
A33: u1 = l * w by ANPROJ_1:1;
u1 = |[ l * (u.1 / a), l * (u.2 /a), l * (- u.3 / a)]|
by A33,EUCLID_5:8;
then
A34: u1`1 = l * (u.1 / a) & u1`2 = l * (u.2 / a) & u1`3 = l * (- u.3 / a)
by EUCLID_5:2;
reconsider z1 = 0,z2 = a,z3 = -a as Element of F_Real by XREAL_0:def 1;
A35: N = <* <* z2,z1,z1 *> ,
<* z1,z2,z1 *>,
<* z1,z1,z3 *> *> by A1,PASCAL:def 3;
reconsider ux = u1`1,uy = u1`2,uz = u1`3 as Element of F_Real
by XREAL_0:def 1;
A36: a * (l * (u.1 / a)) = l * (a * (u.1 / a))
.= l * u.1 by XCMPLX_1:87;
A37: a * (l * (u.2 / a)) = l * (a * (u.2 / a))
.= l * u.2 by XCMPLX_1:87;
A38: (-a) * (l * (- u.3 / a)) = l * (a * (u.3 / a))
.= l * u.3 by XCMPLX_1:87;
<* ux,uy,uz *> = uf by A31,EUCLID_5:3;
then p = <* <* z2 * ux + z1 * uy + z1 * uz *>,
<* z1 * ux + z2 * uy + z1 * uz *>,
<* z1 * ux + z1 * uy + z3 * uz *> *> &
v1 = <* z2 * ux + z1 * uy + z1 * uz ,
z1 * ux + z2 * uy + z1 * uz ,
z1 * ux + z1 * uy + z3 * uz *> by A31,A35,PASCAL:8;
then v1`1 = a * u1`1 & v1`2 = a * u1`2 & v1`3 = (-a) * u1`3
by EUCLID_5:2;
then v1`1 = l * u`1 & v1`2 = l * u`2 & v1`3 = l * u`3
by EUCLID_5:def 1,def 2,def 3,A34,A36,A37,A38;
then v1 = |[ l * u`1,l * u`2, l * u`3]| by EUCLID_5:3
.= l * |[u`1,u`2,u`3]| by EUCLID_5:8
.= l * u by EUCLID_5:3;
then are_Prop u,v1 by A32,ANPROJ_1:1;
hence x = homography(N).P by A20,A31,ANPROJ_1:22;
end;
hence thesis by FUNCT_1:def 6;
end;
hence thesis by A2;
end;
theorem
for ra being non zero Element of F_Real
for M,O being invertible Matrix of 3,F_Real st
O = symmetric_3(1,1,-1,0,0,0) & M = ra * O holds
homography(M).:absolute = absolute
proof
let ra be non zero Element of F_Real;
let M,O be invertible Matrix of 3,F_Real;
assume that
A1: O = symmetric_3(1,1,-1,0,0,0) and
A2: M = ra * O;
reconsider z1 = 1,z2 = -1,z3 = 0 as Element of F_Real by XREAL_0:def 1;
O = <* <* z1,z3,z3 *>,
<* z3,z1,z3 *>,
<* z3,z3,z2 *> *> by A1,PASCAL:def 3;
then ra * O = <* <* ra * z1,ra * z3,ra * z3 *>,
<* ra * z3,ra * z1,ra * z3 *>,
<* ra * z3,ra * z3,ra * z2 *> *> by BKMODEL1:46
.= <* <* ra, 0, 0 *>,
<* 0, ra, 0 *>,
<* 0, 0, -ra *> *>;
then
A3: M = symmetric_3(ra,ra,-ra,0,0,0) by A2,PASCAL:def 3;
ra <> 0
proof
assume ra = 0;
then Det M = 0.F_Real;
then Det M is non unital;
hence contradiction by LAPLACE:34;
end;
hence thesis by A3,Th29;
end;
theorem Th30:
for P being Element of absolute holds tangent P misses BK_model
proof
let P be Element of absolute;
assume not tangent P misses BK_model;
then consider x be object such that
A1: x in tangent P and
A2: x in BK_model by XBOOLE_0:3;
reconsider x as Element of real_projective_plane by A1;
reconsider L = tangent P as LINE of IncProjSp_of real_projective_plane
by INCPROJ:4;
reconsider ip = P,iq = x as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
P in tangent P & x in tangent P by A1,Th21;
then ip on L & iq on L by INCPROJ:5;
then consider p1,p2 be POINT of IncProjSp_of real_projective_plane,
P1,P2 be Element of real_projective_plane such that
A3: p1 = P1 and
A4: p2 = P2 and
A5: P1 <> P2 and
A6: P1 in absolute and
A7: P2 in absolute and
A8: p1 on L and
A9: p2 on L by A2,Th15;
P1 in L & P2 in L by A3,A4,A8,A9,INCPROJ:5;
then P1 in tangent P /\ absolute & P2 in tangent P /\ absolute
by A6,A7,XBOOLE_0:def 4;
then P1 in {P} & P2 in {P} by Th22;
then P1 = P & P2 = P by TARSKI:def 1;
hence contradiction by A5;
end;
theorem Th31:
for P,PP1,PP2 being Element of real_projective_plane
for P1,P2 being Element of absolute
for Q being Element of real_projective_plane st
P1 <> P2 & PP1 = P1 & PP2 = P2 &
P in BK_model & P,PP1,PP2 are_collinear &
Q in tangent P1 & Q in tangent P2 holds
ex R being Element of real_projective_plane st R in absolute &
P,Q,R are_collinear
proof
let P,PP1,PP2 being Element of real_projective_plane;
let P1,P2 being Element of absolute;
let Q being Element of real_projective_plane;
assume that
A1: P1 <> P2 and
A2: PP1 = P1 and
A3: PP2 = P2 and
A4: P in BK_model and
A5: P,PP1,PP2 are_collinear and
A6: Q in tangent P1 and
A7: Q in tangent P2;
A8: P <> Q
proof
assume P = Q;
then BK_model meets tangent P1 by A4,A6,XBOOLE_0:def 4;
hence contradiction by Th30;
end;
consider u be Element of TOP-REAL 3 such that
A9: u is non zero and
A10: Dir u = Q by ANPROJ_1:26;
per cases;
suppose
A11: u`3 <> 0;
reconsider v = |[ u`1/u`3,u`2/u`3, 1 ]| as
non zero Element of TOP-REAL 3 by BKMODEL1:41;
A13: u`3 * (u`1 / u`3) = u`1 & u`3 * (u`2 / u`3) = u`2
by A11,XCMPLX_1:87;
u`3 * v = |[ u`3 * (u`1/u`3),u`3 * (u`2/u`3), u`3 * 1]| by EUCLID_5:8
.= u by A13,EUCLID_5:3;
then are_Prop v,u by A11,ANPROJ_1:1;
then
A14: Dir v = Q & v.3 = 1 by A10,A9,ANPROJ_1:22;
reconsider PP = P as Element of BK_model by A4;
reconsider QQ = Q as Element of ProjectiveSpace TOP-REAL 3;
consider R be Element of absolute such that
A15: PP,QQ,R are_collinear by A8,A14,Th03;
reconsider R as Element of real_projective_plane;
take R;
thus thesis by A15;
end;
suppose u`3 = 0;
then
A16: u.3 = 0 by EUCLID_5:def 3;
then Q = pole_infty P1 & Q = pole_infty P2 by A6,A7,A9,A10,Th28;
then consider up be non zero Element of TOP-REAL 3 such that
A17: P1 = Dir up and
A18: P2 = Dir |[-up`1,-up`2,1]| and
A19: up`3 = 1 by A1,Th20;
consider up1 be non zero Element of TOP-REAL 3 such that
A20: (up1.1)^2 + (up1.2)^2 = 1 and
A21: up1.3 = 1 and
A22: P1 = Dir up1 by BKMODEL1:89;
up.3 = 1 by A19,EUCLID_5:def 3; then
A23: up = up1 by A17,A21,A22,BKMODEL1:43;
reconsider PP = P as Element of BK_model by A4;
consider w be non zero Element of TOP-REAL 3 such that
A24: Dir w = PP and
A25: w.3 = 1 and
BK_to_REAL2 PP = |[w.1,w.2]| by Def01;
reconsider up2 = |[-up`1,-up`2,1]| as non zero Element of TOP-REAL 3
by BKMODEL1:41;
P1 is Element of absolute & P2 is Element of absolute &
PP is Element of BK_model & up1 is non zero &
up2 is non zero & w is non zero & P1 = Dir up1 &
P2 = Dir up2 & PP = Dir w & up1.3 = 1 & up2.3 = 1 &
w.3 = 1 & up2.1 = - up1.1 & up2.2 = - up1.2 & P1,PP,P2 are_collinear
by A22,A18,A24,A21,A25,A23,A2,A3,A5,COLLSP:4,
EUCLID_5:def 1,def 2;
then consider a be Real such that
A29: -1 < a < 1 and
A30: w.1 = a * up1.1 & w.2 = a * up1.2 by Th18;
consider d,e,f be Real such that
A31: e = d * a * up1.1 + (1 - d) * (-up1.2) and
A32: f = d * a * up1.2 + (1 - d) * up1.1 and
A33: e^2 + f^2 = d^2 by A29,A20,BKMODEL1:16;
d <> 0 by A20,A31,A32,A33;
then |[e,f,d]| is non zero by FINSEQ_1:78,EUCLID_5:4;
then reconsider ur = |[e,f,d]| as non zero Element of TOP-REAL 3;
reconsider S = Dir ur as Element of real_projective_plane by ANPROJ_1:26;
take S;
A35: qfconic(1,1,-1,0,0,0,ur) = 0
proof
qfconic(1,1,-1,0,0,0,ur) = 1 * ur.1 * ur.1 + 1 * ur.2 * ur.2
+ (- 1) * ur.3 * ur.3 + 0 * ur.1 * ur.2
+ 0 * ur.1 * ur.3 + 0 * ur.2 * ur.3
by PASCAL:def 1
.= e^2 + f^2 - d^2;
hence thesis by A33;
end;
|{w,u,ur}| = 0
proof
consider u9 be non zero Element of TOP-REAL 3 such that
A39: P1 = Dir u9 & u9.3 = 1 & (u9.1)^2 + (u9.2)^2 = 1 &
pole_infty P1 = Dir |[- u9.2,u9.1,0]| by Def03;
up.3 = 1 by A19,EUCLID_5:def 3; then
A40: u9 = up by A39,A17,BKMODEL1:43;
A41: Q = Dir |[-up.2,up.1,0]| by A39,A40,A16,A6,A9,A10,Th28;
|[-up.2,up.1,0]| is non zero
proof
assume |[-up.2,up.1,0]| is zero;
then up1.1 = 0 & up1.2 = 0 by A23,FINSEQ_1:78,EUCLID_5:4;
hence contradiction by A20;
end;
then are_Prop u,|[-up.2,up.1,0]| by A41,A10,A9,ANPROJ_1:22;
then consider g be Real such that
g <> 0 and
A42: u = g * |[-up.2,up.1,0]| by ANPROJ_1:1;
|[u`1,u`2,u`3]| = u by EUCLID_5:3
.= |[ g * (-up.2), g * (up.1), g * 0]|
by A42,EUCLID_5:8;
then
A43: u`1 = g * (-up.2) & u`2 = g * (up.1) & u`3 = g * 0 by FINSEQ_1:78;
A44: w`3 = 1 by A25,EUCLID_5:def 3;
A45: w`1 = a * up1.1 & w`2 = a * up1.2 by A30,EUCLID_5:def 1,def 2;
ur`1 = e & ur`2 = f & ur`3 = d by EUCLID_5:2;
then |{w,u,ur}| = (a * up1.1) * (g * (up.1)) * d
- 1 * (g * up.1) * (d * a * up1.1 + (1 - d) * (-up1.2))
- (a * up1.1) * 0 * (d * a * up1.2 + (1 - d) * up1.1)
+ (a *up1.2) * 0 * (d * a * up1.1 + (1 - d) * (-up1.2))
- (a * up1.2) * (g * (-up.2)) * d
+ 1 * (g * (-up.2)) * (d * a * up1.2 + (1 - d) * up1.1)
by A43,A44,A45,A31,A32,ANPROJ_8:27
.= 0 by A23;
hence thesis;
end;
hence thesis by A35,PASCAL:11,A9,A24,A10,BKMODEL1:1;
end;
end;
theorem Th32:
for P,R,S being Element of real_projective_plane
for Q being Element of absolute st P in BK_model & R in tangent Q &
P,S,R are_collinear & R <> S holds Q <> S
proof
let P,R,S being Element of real_projective_plane;
let Q being Element of absolute;
assume that
A1: P in BK_model and
A2: R in tangent Q and
A3: P,S,R are_collinear and
A4: R <> S;
A5: S,R,P are_collinear by A3,COLLSP:8;
consider q be Element of real_projective_plane such that
A6: q = Q & tangent Q = Line(q,pole_infty Q) by Def04;
assume Q = S;
then q,pole_infty Q,S are_collinear & q,pole_infty Q,R are_collinear
by A2,Th21,A6,COLLSP:11;
then
A7: P in tangent Q by A5,A4,COLLSP:9,A6,COLLSP:11;
reconsider L = tangent Q as LINE of IncProjSp_of real_projective_plane
by INCPROJ:4;
reconsider ip = P,iq = Q as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
Q in tangent Q by Th21;
then ip on L & iq on L by A7,INCPROJ:5;
then consider p1,p2 be POINT of IncProjSp_of real_projective_plane,
P1,P2 be Element of real_projective_plane such that
A8: p1 = P1 & p2 = P2 & P1 <> P2 & P1 in absolute & P2 in absolute &
p1 on L & p2 on L by A1,Th15;
P1 in L & P2 in L by A8,INCPROJ:5;
then P1 in tangent Q /\ absolute & P2 in tangent Q /\ absolute
by A8,XBOOLE_0:def 4;
then P1 in {Q} & P2 in {Q} by Th22;
then P1 = Q & P2 = Q by TARSKI:def 1;
hence contradiction by A8;
end;
begin :: Sub-Group of K-isometry
definition
let h being Element of EnsHomography3;
pred h is_K-isometry means ex N being invertible Matrix of 3,F_Real st
h = homography(N) & (homography(N)).:absolute = absolute;
end;
theorem Th33:
for h being Element of EnsHomography3 st h = homography(1.(F_Real,3)) holds
h is_K-isometry
proof
let h be Element of EnsHomography3;
assume
A1: h = homography(1.(F_Real,3));
reconsider N = 1.(F_Real,3) as invertible Matrix of 3,F_Real;
h is_K-isometry
proof
A2: (homography(N)).:absolute c= absolute
proof
let x be object;
assume x in (homography(N)).:absolute;
then ex y be object st y in dom homography(N) & y in absolute &
(homography(N)).y = x by FUNCT_1:def 6;
hence thesis by ANPROJ_9:14;
end;
absolute c= (homography(N)).:absolute
proof
let x be object;
assume
A3: x in absolute;
then reconsider y = x as Point of ProjectiveSpace TOP-REAL 3;
A4: y = homography(N).y by ANPROJ_9:14;
dom homography(N) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
hence thesis by A4,A3,FUNCT_1:108;
end;
then absolute = (homography(N)).:absolute by A2;
hence thesis by A1;
end;
hence thesis;
end;
definition
func EnsK-isometry -> non empty Subset of EnsHomography3 equals
{h where h is Element of EnsHomography3: h is_K-isometry};
coherence
proof
set KI = {h where h is Element of EnsHomography3: h is_K-isometry};
KI c= EnsHomography3
proof
let x be object;
assume x in KI;
then ex h be Element of EnsHomography3 st x = h & h is_K-isometry;
hence thesis;
end;
then reconsider KI as Subset of EnsHomography3;
reconsider N = 1.(F_Real,3) as invertible Matrix of 3,F_Real;
homography(N) in the set of all homography(N)
where N is invertible Matrix of 3,F_Real;
then reconsider h = homography(N) as Element of EnsHomography3
by ANPROJ_9:def 1;
h is_K-isometry by Th33;
then h in KI;
hence thesis;
end;
end;
definition
func SubGroupK-isometry -> strict Subgroup of GroupHomography3 means
:Def05:
the carrier of it = EnsK-isometry;
existence
proof
set H = EnsK-isometry,
G = GroupHomography3;
reconsider N = 1.(F_Real,3) as invertible Matrix of 3,F_Real;
homography N in the set of all homography M where
M is invertible Matrix of 3,F_Real;
then reconsider idG = homography(1.(F_Real,3)) as
Element of GroupHomography3 by ANPROJ_9:def 1,def 4;
A1: 1_G = idG
proof
for g be Element of G holds idG * g = g & g * idG = g
proof
let g be Element of G;
g in EnsHomography3 by ANPROJ_9:def 4;
then consider N be invertible Matrix of 3,F_Real such that
A2: g = homography(N) by ANPROJ_9:def 1;
idG in EnsHomography3 & homography(N) in EnsHomography3
by ANPROJ_9:def 1;
then reconsider g1 = idG, g2 = homography(N) as
Element of EnsHomography3;
thus idG * g = g
proof
idG * g = g1 (*) g2 by A2,ANPROJ_9:def 3,def 4
.= homography(1.(F_Real,3) * N) by ANPROJ_9:18
.= g by A2,MATRIX_3:18;
hence thesis;
end;
thus g * idG = g
proof
g * idG = g2 (*) g1 by A2,ANPROJ_9:def 3,def 4
.= homography(N * 1.(F_Real,3)) by ANPROJ_9:18
.= g by A2,MATRIX_3:19;
hence thesis;
end;
end;
hence thesis by GROUP_1:def 4;
end;
A3: for g1,g2 be Element of G st g1 in H & g2 in H holds g1 * g2 in H
proof
let g1,g2 be Element of G;
assume that
A4: g1 in H and
A5: g2 in H;
consider h1 be Element of EnsHomography3 such that
A5BIS: g1 = h1 & h1 is_K-isometry by A4;
consider h2 be Element of EnsHomography3 such that
A6: g2 = h2 & h2 is_K-isometry by A5;
reconsider g3 = g1 * g2 as Element of EnsHomography3 by ANPROJ_9:def 4;
consider N1,N2 be invertible Matrix of 3,F_Real such that
A7: h1 = homography(N1) and
A8: h2 = homography(N2) and
A9: h1 (*) h2 = homography(N1 * N2) by ANPROJ_9:def 2;
A10: dom homography(N1) = the carrier of ProjectiveSpace TOP-REAL 3 &
dom homography(N2) = the carrier of ProjectiveSpace TOP-REAL 3 &
dom homography(N1*N2) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
A11: homography(N1*N2) .: absolute c= absolute
proof
let x be object;
assume x in homography(N1*N2).:absolute;
then consider y be object such that
A12: y in dom homography(N1*N2) and
A13: y in absolute and
A14: homography(N1*N2).y = x by FUNCT_1:def 6;
reconsider y as Point of ProjectiveSpace TOP-REAL 3 by A12;
dom homography(N2) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
then
A15: homography(N2).y in absolute by A13,A6,A8,FUNCT_1:108;
dom homography(N1) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
then homography(N1).((homography(N2)).y) in
(homography(N1)).:absolute by A15,FUNCT_1:108;
hence thesis by A5BIS,A7,A14,ANPROJ_9:13;
end;
absolute c= homography(N1*N2) .:absolute
proof
let x be object;
assume
A16: x in absolute;
then reconsider y = x as Point of ProjectiveSpace TOP-REAL 3;
consider z be object such that
A17: z in dom (homography(N1)) and
A18: z in absolute and
A19: y = (homography(N1)).z by A16,A5BIS,A7,FUNCT_1:def 6;
reconsider z as Point of ProjectiveSpace TOP-REAL 3 by A17;
consider t be object such that
A20: t in dom (homography(N2)) and
A21: t in absolute and
A22: z = (homography(N2)).t by A18,A6,A8,FUNCT_1:def 6;
reconsider t as Point of ProjectiveSpace TOP-REAL 3 by A20;
y = (homography(N1 * N2)).t by A22,A19,ANPROJ_9:13;
hence thesis by A10,A21,FUNCT_1:def 6;
end;
then homography(N1 * N2) .:absolute = absolute by A11;
then g3 is_K-isometry by A9,A5BIS,A6,ANPROJ_9:def 3,def 4;
hence thesis;
end;
for g be Element of G st g in H holds g" in H
proof
let g be Element of G;
assume g in H;
then consider h be Element of EnsHomography3 such that
A23: g = h & h is_K-isometry;
h in the set of all homography(N) where
N is invertible Matrix of 3,F_Real by ANPROJ_9:def 1;
then consider N be invertible Matrix of 3,F_Real such that
A24: h = homography(N);
reconsider h3 = g" as Element of EnsHomography3 by ANPROJ_9:def 4;
h3 in the set of all homography(N) where
N is invertible Matrix of 3,F_Real by ANPROJ_9:def 1;
then consider N3 be invertible Matrix of 3,F_Real such that
A25: h3 = homography(N3);
A26: h (*) h3 = g * g" by A23,ANPROJ_9:def 3,def 4
.= 1_G by GROUP_1:def 5;
A27: h3 (*) h = g" * g by A23,ANPROJ_9:def 3,def 4
.= 1_G by GROUP_1:def 5;
A28: homography(N * N3) = homography(1.(F_Real,3))
by A26,A1,A25,A24,ANPROJ_9:18;
A29: homography(N3 * N) = homography(1.(F_Real,3))
by A27,A1,A25,A24,ANPROJ_9:18;
A30: for P being Point of ProjectiveSpace TOP-REAL 3 holds
homography(N3~).P = homography(N).P
proof
let P be Point of ProjectiveSpace TOP-REAL 3;
(homography(N3)).(homography(N).P) = (homography(N3 * N)).P
by ANPROJ_9:13
.= P by A29,ANPROJ_9:14;
hence thesis by ANPROJ_9:15;
end;
A31: for P being Point of ProjectiveSpace TOP-REAL 3 holds
homography(N3).P = homography(N~).P
proof
let P be Point of ProjectiveSpace TOP-REAL 3;
(homography(N)).(homography(N3).P) = (homography(N * N3)).P
by ANPROJ_9:13
.= P by A28,ANPROJ_9:14;
hence thesis by ANPROJ_9:15;
end;
A32: dom homography(N) = the carrier of ProjectiveSpace TOP-REAL 3 &
dom homography(N3) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
homography(N3).:absolute = absolute
proof
A33: homography(N3).:absolute c= absolute
proof
let x be object;
assume x in homography(N3).:absolute;
then consider y be object such that
A34: y in dom homography(N3) and
A35: y in absolute and
A36: (homography(N3)).y = x by FUNCT_1:def 6;
reconsider y as Point of ProjectiveSpace TOP-REAL 3 by A34;
A37: y = (homography(N3~)).x by A36,ANPROJ_9:15;
(homography(N3)).y is Point of ProjectiveSpace TOP-REAL 3;
then reconsider z = x as Point of ProjectiveSpace TOP-REAL 3 by A36;
(homography(N)).z in absolute by A37,A30,A35;
then consider t be object such that
A38: t in dom homography(N) and
A39: t in absolute and
A40: homography(N).t = homography(N).z by A23,A24,FUNCT_1:def 6;
reconsider t as Point of ProjectiveSpace TOP-REAL 3 by A38;
t = homography(N~).(homography(N).t) by ANPROJ_9:15
.= z by A40,ANPROJ_9:15;
hence thesis by A39;
end;
absolute c= homography(N3).:absolute
proof
let x be object;
assume
A41: x in absolute;
then reconsider y = x as Point of ProjectiveSpace TOP-REAL 3;
consider z be Point of ProjectiveSpace TOP-REAL 3 such that
A42: z in absolute and
A43: homography(N).y = z by A32,FUNCT_1:108,A41,A23,A24;
reconsider z as Point of ProjectiveSpace TOP-REAL 3;
y = homography(N~).(homography(N).y) by ANPROJ_9:15
.= homography(N3).z by A43,A31;
hence thesis by A42,A32,FUNCT_1:def 6;
end;
hence thesis by A33;
end;
then h3 is_K-isometry by A25;
hence g" in H;
end;
hence thesis by ANPROJ_9:def 4,A3,GROUP_2:52;
end;
uniqueness
proof
let H1,H2 be strict Subgroup of GroupHomography3 such that
A44: the carrier of H1 = EnsK-isometry and
A45: the carrier of H2 = EnsK-isometry;
for g be object holds g in H1 iff g in H2 by A44,A45;
hence thesis;
end;
end;
theorem
for h being Element of EnsK-isometry
for N being invertible Matrix of 3,F_Real st
h = homography(N) holds homography(N).:absolute = absolute
proof
let h being Element of EnsK-isometry;
let N being invertible Matrix of 3,F_Real;
assume
A1: h = homography(N);
h in {h where h is Element of EnsHomography3: h is_K-isometry};
then consider g be Element of EnsHomography3 such that
A2: h = g and
A3: g is_K-isometry;
thus thesis by A1,A2,A3;
end;
theorem Th34:
homography(1.(F_Real,3)) = 1_GroupHomography3 &
homography(1.(F_Real,3)) = 1_SubGroupK-isometry
proof
set G = GroupHomography3;
homography(1.(F_Real,3)) in G by ANPROJ_9:def 1,def 4;
then reconsider e = homography(1.(F_Real,3)) as Element of G;
now
let h being Element of GroupHomography3;
h in EnsHomography3 by ANPROJ_9:def 4;
then consider N be invertible Matrix of 3,F_Real such that
A1: h = homography(N) by ANPROJ_9:def 1;
h in EnsHomography3 & e in EnsHomography3 by A1,ANPROJ_9:def 1;
then reconsider h1 = h, h2 = e as Element of EnsHomography3;
thus h * e = h1 (*) h2 by ANPROJ_9:def 3,def 4
.= homography(N * 1.(F_Real,3)) by A1,ANPROJ_9:18
.= h by A1,MATRIX_3:19;
thus e * h = h2 (*) h1 by ANPROJ_9:def 3,def 4
.= homography(1.(F_Real,3) * N) by A1,ANPROJ_9:18
.= h by A1,MATRIX_3:18;
end;
hence homography(1.(F_Real,3)) = 1_GroupHomography3 by GROUP_1:4;
hence thesis by GROUP_2:44;
end;
theorem Th35:
for N1,N2 being invertible Matrix of 3,F_Real
for h1,h2 being Element of SubGroupK-isometry st
h1 = homography(N1) & h2 = homography(N2) holds
h1 * h2 is Element of SubGroupK-isometry &
h1 * h2 = homography(N1 * N2)
proof
let N1,N2 being invertible Matrix of 3,F_Real;
let h1,h2 being Element of SubGroupK-isometry;
assume that
A1: h1 = homography(N1) and
A2: h2 = homography(N2);
thus h1 * h2 is Element of SubGroupK-isometry;
h1 in EnsHomography3 by A1,ANPROJ_9:def 1;
then reconsider hh1 = h1 as Element of EnsHomography3;
h2 in EnsHomography3 by A2,ANPROJ_9:def 1;
then reconsider hh2 = h2 as Element of EnsHomography3;
set G = GroupHomography3;
reconsider h1g = hh1, h2g = hh2 as Element of G by ANPROJ_9:def 4;
h1g * h2g = hh1 (*) hh2 by ANPROJ_9:def 3,def 4
.= homography(N1 * N2) by A1,A2,ANPROJ_9:18;
hence h1 * h2 = homography(N1 * N2) by GROUP_2:43;
end;
theorem Th36:
for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry st
h = homography(N) holds h" = homography(N~) &
homography(N~) is Element of SubGroupK-isometry
proof
let N being invertible Matrix of 3,F_Real;
let h being Element of SubGroupK-isometry;
assume
A1: h = homography(N);
then h in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h1 = h as Element of EnsHomography3;
homography(N~) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h2 = homography(N~) as Element of EnsHomography3;
set G = GroupHomography3;
reconsider h1g = h1, h2g = h2 as Element of G by ANPROJ_9:def 4;
A2: N is_reverse_of N~ by MATRIX_6:def 4;
A3: h1g * h2g = h1 (*) h2 by ANPROJ_9:def 3,def 4
.= homography(N * N~) by A1,ANPROJ_9:18
.= 1_G by A2,MATRIX_6:def 2,Th34;
h2g * h1g = h2 (*) h1 by ANPROJ_9:def 3,def 4
.= homography(N~ * N) by A1,ANPROJ_9:18
.= 1_G by A2,MATRIX_6:def 2,Th34;
then h2g = h1g" by A3,GROUP_1:5;
hence h" = homography(N~) by GROUP_2:48;
hence thesis;
end;
theorem Th37:
for s being Element of ProjectiveSpace TOP-REAL 3
for p,q,r being Element of absolute st p,q,r are_mutually_distinct &
s in tangent p /\ tangent q holds
ex N being invertible Matrix of 3,F_Real st
homography(N).:absolute = absolute &
(homography(N)).Dir101 = p &
(homography(N)).Dirm101 = q &
(homography(N)).Dir011 = r &
(homography(N)).Dir010 = s
proof
let s be Element of ProjectiveSpace TOP-REAL 3;
let p,q,r be Element of absolute;
assume that
A1: p,q,r are_mutually_distinct and
A2: s in tangent p /\ tangent q;
reconsider P1 = p,P2 = q,P3 = r,P4 = s as Point of real_projective_plane;
P4 in tangent p & P4 in tangent q by A2,XBOOLE_0:def 4;
then not P1,P2,P3 are_collinear &
not P1,P2,P4 are_collinear &
not P1,P3,P4 are_collinear &
not P2,P3,P4 are_collinear by A1,Th27;
then consider N be invertible Matrix of 3,F_Real such that
A3: (homography(N)).Dir101 = P1 and
A4: (homography(N)).Dirm101 = P2 and
A5: (homography(N)).Dir011 = P3 and
A6: (homography(N)).Dir010 = P4
by BKMODEL1:44,ANPROJ_9:31;
consider na,nb,nc,nd,ne,nf,ng,nh,ni be Element of F_Real such that
A7: N = <* <* na,nb,nc *>,
<* nd,ne,nf *>,
<* ng,nh,ni *> *> by PASCAL:3;
reconsider b = -1 as Element of F_Real by XREAL_0:def 1;
A8: b is non zero;
reconsider a = 1 as Element of F_Real;
a is non zero;
then reconsider a = 1,b = -1 as non zero Element of F_Real by A8;
reconsider N1 = <* <* a,0,0 *>,
<* 0,a,0 *>,
<* 0,0,b *> *> as invertible Matrix of 3,F_Real
by ANPROJ_9:9;
reconsider M = (N@) * N1 * N as invertible Matrix of 3,F_Real;
A9: N1 = symmetric_3(a,a,b,0,0,0) by PASCAL:def 3;
then
A10: M is symmetric by PASCAL:7,12;
consider va,vb,vc,vd,ve,vf,vg,vh,vi be Element of F_Real such that
A11: M = <* <* va,vb,vc *>,
<* vd,ve,vf *>,
<* vg,vh,vi *> *> by PASCAL:3;
A12: vb = vd & vc = vg & vh = vf by A10,A11,PASCAL:6;
reconsider ra = va,rb = vb, rc = vc, re = ve, rf = vf, ri = vi as Real;
A13: M = symmetric_3(ra,re,ri,rb,rc,rf) by A12,A11,PASCAL:def 3;
A14: p in conic(1,1,-1,0,0,0) & N~ is invertible;
reconsider NR = MXF2MXR(N~) as Matrix of 3,REAL by MATRIXR1:def 2;
A15: N1 = symmetric_3(1,1,-1,0/2,0/2,0/2) by PASCAL:def 3;
reconsider N2 = N1 as Matrix of 3,REAL;
A16: M = MXF2MXR((MXR2MXF(NR@))~) * N2 * MXF2MXR((MXR2MXF NR)~)
by A15,BKMODEL1:53;
A17: (homography(N~)).p = Dir101 by A3,ANPROJ_9:15;
A18: not(ra = 0 & re = 0 & ri = 0 & rb = 0 & rc = 0 & rf = 0) &
(homography(N~)).p in conic(ra,re,ri,2 * rb,2 * rc,2 * rf)
by A13,A14,A15,A16,PASCAL:16;
Dir101 in {P where P is Point of ProjectiveSpace TOP-REAL 3:
for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(ra,re,ri,2*rb,2*rc,2*rf,u) = 0} by A18,A17,PASCAL:def 2;
then consider Q be Point of ProjectiveSpace TOP-REAL 3 such that
A19: Dir101 = Q and
A20: for u be Element of TOP-REAL 3 st u is non zero & Q = Dir u holds
qfconic(ra,re,ri,2*rb,2*rc,2*rf,u) = 0;
A21: |[1,0,1]|.1 = 1 & |[1,0,1]|.2 = 0 & |[1,0,1]|.3 = 1;
qfconic(ra,re,ri,2*rb,2*rc,2*rf, |[1,0,1]|) = 0 by A19,A20,BKMODEL1:41;
then
A22: 0 = ra * 1 * 1 + re * 0 * 0 + ri * 1 * 1 + 2* rb * 1 * 0
+ 2* rc * 1 * 1 + 2 * rf * 0 * 1 by A21,PASCAL:def 1
.= ra + ri + 2 * rc;
A23:(homography(N~)).q = Dirm101 by A4,ANPROJ_9:15;
q in conic(1,1,-1,0,0,0) & N~ is invertible;
then
A25: not(ra = 0 & re = 0 & ri = 0 & rb = 0 & rc = 0 & rf = 0) &
(homography(N~)).q in conic(ra,re,ri,2 * rb,2 * rc,2 * rf)
by A13,PASCAL:16,A15,A16;
Dirm101 in {P where P is Point of ProjectiveSpace TOP-REAL 3:
for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(ra,re,ri,2*rb,2*rc,2*rf,u) = 0} by A23,A25,PASCAL:def 2;
then consider Q be Point of ProjectiveSpace TOP-REAL 3 such that
A26: Dirm101 = Q and
A27: for u be Element of TOP-REAL 3 st u is non zero & Q = Dir u holds
qfconic(ra,re,ri,2*rb,2*rc,2*rf,u) = 0;
A28: |[-1,0,1]|.1 = -1 & |[-1,0,1]|.2 = 0 & |[-1,0,1]|.3 = 1;
qfconic(ra,re,ri,2*rb,2*rc,2*rf, |[-1,0,1]|) = 0
by A26,A27,BKMODEL1:41;
then
A29: 0 = ra * (-1) * (-1) + re * 0 * 0 + ri * 1 * 1
+ 2* rb * (-1) * 0 + 2* rc * (-1) * 1 + 2 * rf * 0 * 1
by A28,PASCAL:def 1
.= ra + ri - 2 * rc;
A30: (homography(N~)).r = Dir011 by A5,ANPROJ_9:15;
r in conic(1,1,-1,0,0,0) & N~ is invertible;
then
A31: for fa,fb,fc,fe,fi,ff be Real for N1,M being Matrix of 3,REAL
for NR be Matrix of 3,REAL st N1 = symmetric_3(1,1,-1,0/2,0/2,0/2) &
NR = MXF2MXR (N~) &
M = MXF2MXR((MXR2MXF(NR@))~) * N1 * MXF2MXR((MXR2MXF NR)~) &
M = symmetric_3(fa,fe,fi,fb,fc,ff) holds
not(fa = 0 & fe = 0 & fi = 0 & fb = 0 & ff = 0 & fc = 0) &
(homography(N~)).r in conic(fa,fe,fi,2 * fb,2 * fc,2 * ff) by PASCAL:16;
not(ra = 0 & re = 0 & ri = 0 & rb = 0 & rc = 0 & rf = 0) &
(homography(N~)).r in conic(ra,re,ri,2 * rb,2 * rc,2 * rf)
by A9,A13,A31,A16;
then Dir011 in {P where P is Point of ProjectiveSpace TOP-REAL 3:
for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(ra,re,ri,2*rb,2*rc,2*rf,u) = 0} by A30,PASCAL:def 2;
then consider Q be Point of ProjectiveSpace TOP-REAL 3 such that
A32: Dir011 = Q and
A33: for u be Element of TOP-REAL 3 st u is non zero & Q = Dir u holds
qfconic(ra,re,ri,2*rb,2*rc,2*rf,u) = 0;
A34: |[0,1,1]|.1 = 0 & |[0,1,1]|.2 = 1 & |[0,1,1]|.3 = 1;
qfconic(ra,re,ri,2*rb,2*rc,2*rf, |[0,1,1]|) = 0 by A32,A33,BKMODEL1:41;
then
A35: 0 = ra * 0 * 0 + re * 1 * 1 + ri * 1 * 1 + 2* rb * 0 * 1
+ 2 * rc * 0 * 1 + 2 * rf * 1 * 1 by A34,PASCAL:def 1
.= re + ri + 2 * rf;
rc = 0 & ra = - ri & rb = 0 & rf = 0 & ra = re
proof
thus rc = 0 by A22,A29;
thus ra = - ri by A22,A29;
consider k1 be Element of TOP-REAL 3 such that
A36: k1 is non zero and
A37: P1 = Dir k1 by ANPROJ_1:26;
consider k1b be Element of TOP-REAL 3 such that
A38: k1b is non zero and
A39: P2 = Dir k1b by ANPROJ_1:26;
consider k2 be Element of TOP-REAL 3 such that
A40: k2 is non zero and
A41: P4 = Dir k2 by ANPROJ_1:26;
reconsider kf1 = k1,
kf1b = k1b,
kf2 =k2 as FinSequence of REAL by EUCLID:24;
A42: P4 in tangent p & N2 is Matrix of 3,REAL &
p is Element of absolute & Q is Element of real_projective_plane &
k1 is non zero Element of TOP-REAL 3 &
k2 is non zero Element of TOP-REAL 3 & kf1 is FinSequence of REAL &
kf2 is FinSequence of REAL &N2 = symmetric_3(1,1,-1,0,0,0) &
p = Dir k1 & P4 = Dir k2 & k1 = kf1 & k2 = kf2
by A2,XBOOLE_0:def 4,PASCAL:def 3,A36,A37,A40,A41;
A43: P4 in tangent q & N2 is Matrix of 3,REAL & p is Element of absolute &
k1b is non zero Element of TOP-REAL 3 &
k2 is non zero Element of TOP-REAL 3 & kf1b is FinSequence of REAL &
kf2 is FinSequence of REAL & N2 = symmetric_3(1,1,-1,0,0,0) &
q = Dir k1b & P4 = Dir k2 & k1b = kf1b & k2 = kf2
by A2,A38,A40,PASCAL:def 3,A39,A41,XBOOLE_0:def 4;
consider ua,va be Element of TOP-REAL 3,
ufa be FinSequence of F_Real,
pa be FinSequence of 1-tuples_on REAL
such that
A44: Dir101 = Dir ua & ua is not zero & ua = ufa & pa = N * ufa &
va = M2F pa & va is not zero &
homography(N).Dir101 = Dir va by ANPROJ_8:def 4;
are_Prop k1,va by A3,A37,A44,ANPROJ_1:22,A36;
then consider li be Real such that
A45: li <> 0 and
A46: k1 = li * va by ANPROJ_1:1;
A47: len (N * <*ufa*>@) = len N
proof
ufa in TOP-REAL 3 by A44; then
A48: ufa in REAL 3 by EUCLID:22;
then len ufa = 3 by EUCLID_8:50;
then width <*ufa*> = 3 by ANPROJ_8:75; then
A50: len (<*ufa*>@) = width <*ufa*> by MATRIX_0:29
.= len ufa by MATRIX_0:23;
width N = 3 by MATRIX_0:24
.= len (<*ufa*>@) by A50,A48,EUCLID_8:50;
hence thesis by MATRIX_3:def 4;
end;
A51: len pa = len N by A47,A44,LAPLACE:def 9
.= 3 by MATRIX_0:23;
then
A52: kf1 = M2F (li * pa) by A44,A46,ANPROJ_8:83;
consider ub,vb be Element of TOP-REAL 3,
ufb be FinSequence of F_Real,
pb be FinSequence of 1-tuples_on REAL
such that
A53: Dir010 = Dir ub & ub is not zero & ub = ufb & pb = N * ufb &
vb = M2F pb & vb is not zero & homography(N).Dir010 = Dir vb
by ANPROJ_8:def 4;
are_Prop ub,|[0,1,0]| by A53,ANPROJ_1:22,ANPROJ_9:def 6,10;
then consider lub be Real such that
A54: lub <> 0 and
A55: ub = lub * |[0,1,0]| by ANPROJ_1:1;
A56: ufb = |[ lub * 0,lub * 1,lub *0]| by A53,A55,EUCLID_5:8
.= |[0,lub,0]|;
lub in REAL by XREAL_0:def 1;
then reconsider MUFB = <* ufb *> as Matrix of 1,3,F_Real
by A56,BKMODEL1:27;
A57: now
len ufb = 3 by A56,FINSEQ_1:45;
then dom ufb = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
then 1 in dom ufb & 2 in dom ufb & 3 in dom ufb by ENUMSET1:def 1;
then MUFB*(1,1) = |[0,lub,0]|.1 & MUFB*(1,2) = |[0,lub,0]|.2 &
MUFB*(1,3) = |[0,lub,0]|.3 by A56,ANPROJ_8:70;
hence MUFB*(1,1) = 0 & MUFB*(1,2) = lub & MUFB*(1,3) = 0;
end;
are_Prop k2,vb by A41,A6,A53,ANPROJ_1:22,A40;
then consider lj be Real such that
A58: lj <> 0 and
A59: k2 = lj * vb by ANPROJ_1:1;
A60: len (N * <*ufb*>@) = len N
proof
ufb in TOP-REAL 3 by A53;
then
A61: ufb in REAL 3 by EUCLID:22;
then len ufb = 3 by EUCLID_8:50;
then width <*ufb*> = 3 by ANPROJ_8:75;
then
A61bis: len (<*ufb*>@) = width <*ufb*> by MATRIX_0:29
.= len ufb by MATRIX_0:23;
width N = 3 by MATRIX_0:24
.= len (<*ufb*>@) by A61,A61bis,EUCLID_8:50;
hence thesis by MATRIX_3:def 4;
end;
A62: len pb = len N by A60,A53,LAPLACE:def 9
.= 3 by MATRIX_0:23;
then
A63: M2F pb is Element of TOP-REAL 3 by ANPROJ_8:82; then
A64: M2F pb is Element of REAL 3 by EUCLID:22; then
A65: len M2F pb = 3 by EUCLID_8:50;
M2F pa is Element of TOP-REAL 3 by A51,ANPROJ_8:82;
then
A66: M2F pa is Element of REAL 3 by EUCLID:22; then
A67: len M2F pa = 3 by EUCLID_8:50;
A68: li * (N2 * (M2F pa )) = N2 * (li * M2F pa)
proof
width N2 = 3 by MATRIX_0:23;
hence thesis by A67,MATRIXR1:59;
end;
A69: len (li * (N2 * (M2F pa))) = 3 & len (N2 * (M2F pa)) = 3
proof
ColVec2Mx (M2F pa) = pa by A51,BKMODEL1:33;
then reconsider Mpa = pa as Matrix of REAL;
A70: len (N2 * (M2F pa))
= len (Col(N2 * (ColVec2Mx (M2F pa)),1)) by MATRIXR1:def 11
.= len (N2 * (ColVec2Mx (M2F pa))) by MATRIX_0:def 8
.= len (N2 * Mpa) by A51,BKMODEL1:33;
reconsider N2F = N2,MpaF = Mpa as Matrix of F_Real;
A71: width N2F = len Mpa by A51,MATRIX_0:23;
len(N2 * Mpa) = len(N2F * MpaF) by ANPROJ_8:17
.= len N2F by A71,MATRIX_3:def 4
.= 3 by MATRIX_0:23;
hence thesis by A70,RVSUM_1:117;
end;
then
A72: len M2F pb = len (N2 * ((M2F(li * pa)))) by A51,ANPROJ_8:83,A68,A65;
A73: len M2F pb = len (N2 * (M2F(pa))) by A69,A64,EUCLID_8:50;
A74: kf2 = M2F (lj * pb) by A59,A53,A62,ANPROJ_8:83;
A75: len M2F(lj * pb) = len N2 & len M2F(li * pa) = width N2 &
len M2F(li * pa) > 0
proof
A76: len N2 = 3 & width N2 = 3 by MATRIX_0:23;
consider p1,p2,p3 be Real such that
A77: p1 = (pb.1).1 & p2 = (pb.2).1 & p3 = (pb.3).1 &
lj * pb = <* <* lj * p1 *>, <* lj * p2 *> , <* lj * p3 *> *>
by A62,ANPROJ_8:def 3;
len (lj * pb) = 3 by A77,FINSEQ_1:45; then
A78: M2F (lj * pb) = <* ((lj * pb).1).1,
((lj * pb).2).1,
((lj * pb).3).1 *> by ANPROJ_8:def 2;
consider p1,p2,p3 be Real such that
A79: p1 = (pa.1).1 & p2 = (pa.2).1 & p3 = (pa.3).1 &
li * pa = <* <* li * p1 *>, <* li * p2 *> , <* li * p3 *> *>
by A51,ANPROJ_8:def 3;
len (li * pa) = 3 by A79,FINSEQ_1:45;
then M2F (li * pa) = <* ((li * pa).1).1,
((li * pa).2).1,
((li * pa).3).1 *> by ANPROJ_8:def 2;
hence thesis by A76,A78,FINSEQ_1:45;
end;
A80: 0 = SumAll QuadraticForm(M2F(lj * pb),N2,M2F(li * pa))
by A42,Th26,A52,A74
.= |( M2F(lj * pb), N2 * (M2F(li * pa)))| by A75,MATRPROB:44
.= |( lj * M2F pb, N2 * (M2F(li * pa)))| by A62,ANPROJ_8:83
.= lj * |( M2F pb, N2 * (M2F(li * pa)))| by A72,RVSUM_1:121
.= lj * |( M2F pb, li * (N2 * (M2F pa )) )| by A68,A51,ANPROJ_8:83
.= lj * (li * |( M2F pb, N2 * (M2F pa) )| ) by A73,RVSUM_1:121
.= (lj * li) * |( M2F pb, N2 * (M2F pa) )|;
A81: nb * (- na + nc) + ne * (- nd + nf) = nh * (- ng + ni)
proof
consider ua2,va2 be Element of TOP-REAL 3,
ufa2 be FinSequence of F_Real,
pa2 be FinSequence of 1-tuples_on REAL
such that
A82: Dirm101 = Dir ua2 & ua2 is not zero & ua2 = ufa2 &
pa2 = N * ufa2 & va2 = M2F pa2 &
va2 is not zero & homography(N).Dirm101 = Dir va2 by ANPROJ_8:def 4;
are_Prop k1b,va2 by A39,A4,A82,ANPROJ_1:22,A38;
then consider li2 be Real such that
A83: li2 <> 0 and
A84: k1b = li2 * va2 by ANPROJ_1:1;
A85: len (N * <*ufa2*>@) = len N
proof
ufa2 in TOP-REAL 3 by A82; then
A86: ufa2 in REAL 3 by EUCLID:22;
A87: len ufa2 = 3 by A86,EUCLID_8:50;
width <*ufa2*> = 3 by A87,ANPROJ_8:75; then
A88: len (<*ufa2*>@) = width <*ufa2*> by MATRIX_0:29
.= len ufa2 by MATRIX_0:23;
width N = 3 by MATRIX_0:24
.= len (<*ufa2*>@) by A88,A86,EUCLID_8:50;
hence thesis by MATRIX_3:def 4;
end;
A89: len pa2 = len N by A85,A82,LAPLACE:def 9
.= 3 by MATRIX_0:23;
A90: kf1b = M2F (li2 * pa2) by A82,A84,A89,ANPROJ_8:83;
M2F pa2 is Element of TOP-REAL 3 by A89,ANPROJ_8:82;
then
A91: M2F pa2 is Element of REAL 3 by EUCLID:22;
then
A92: len M2F pa2 = 3 by EUCLID_8:50;
A93: li2 * (N2 * (M2F pa2 )) = N2 * (li2 * M2F pa2)
proof
width N2 = 3 by MATRIX_0:23;
hence thesis by MATRIXR1:59,A92;
end;
A94: len (li2 * (N2 * (M2F pa2))) = 3 & len (N2 * (M2F pa2)) = 3
proof
ColVec2Mx (M2F pa2) = pa2 by A89,BKMODEL1:33;
then reconsider Mpa2 = pa2 as Matrix of REAL;
A95: len (N2 * (M2F pa2))
= len (Col(N2 * (ColVec2Mx (M2F pa2)),1)) by MATRIXR1:def 11
.= len (N2 * (ColVec2Mx (M2F pa2))) by MATRIX_0:def 8
.= len (N2 * Mpa2) by A89,BKMODEL1:33;
reconsider N2F2 = N2,MpaF2 = Mpa2 as Matrix of F_Real;
A96: width N2F2 = len Mpa2 by A89,MATRIX_0:23;
len(N2 * Mpa2) = len(N2F2 * MpaF2) by ANPROJ_8:17
.= len N2F2 by A96,MATRIX_3:def 4
.= 3 by MATRIX_0:23;
hence thesis by A95,RVSUM_1:117;
end;
then
A97: len M2F pb = len (N2 * ((M2F(li2 * pa2)))) by A89,ANPROJ_8:83,A93,A65;
A98: len M2F pb = len (N2 * (M2F(pa2))) by A94,A64,EUCLID_8:50;
A99: kf2 = M2F (lj * pb) by A59,A53,A62,ANPROJ_8:83;
A100: len M2F(lj * pb) = len N2 & len M2F(li2 * pa2) = width N2 &
len M2F(li2 * pa2) > 0
proof
A101: len N2 = 3 & width N2 = 3 by MATRIX_0:23;
consider p1,p2,p3 be Real such that
A102: p1 = (pb.1).1 & p2 = (pb.2).1 & p3 = (pb.3).1 &
lj * pb = <* <* lj * p1 *>, <* lj * p2 *> , <* lj * p3 *> *>
by A62,ANPROJ_8:def 3;
len (lj * pb) = 3 by A102,FINSEQ_1:45; then
A103: M2F (lj * pb) = <* ((lj * pb).1).1,
((lj * pb).2).1,
((lj * pb).3).1 *> by ANPROJ_8:def 2;
consider p1b,p2b,p3b be Real such that
A104: p1b = (pa2.1).1 & p2b = (pa2.2).1 & p3b = (pa2.3).1 &
li2 * pa2 = <* <* li2 * p1b *>,
<* li2 * p2b *> ,
<* li2 * p3b *> *> by A89,ANPROJ_8:def 3;
len (li2 * pa2) = 3 by A104,FINSEQ_1:45;
then M2F (li2 * pa2) = <* ((li2 * pa2).1).1,
((li2 * pa2).2).1,
((li2 * pa2).3).1 *> by ANPROJ_8:def 2;
hence thesis by A101,A103,FINSEQ_1:45;
end;
A105: 0 = SumAll QuadraticForm(M2F(lj * pb),N2,M2F(li2 * pa2))
by A43,Th26,A90,A99
.= |( M2F(lj * pb), N2 * (M2F(li2 * pa2)))| by A100,MATRPROB:44
.= |( lj * M2F pb, N2 * (M2F(li2 * pa2)))| by A62,ANPROJ_8:83
.= lj * |( M2F pb, N2 * (M2F(li2 * pa2)))| by A97,RVSUM_1:121
.= lj * |( M2F pb, li2 * (N2 * (M2F pa2 )) )| by A93,A89,ANPROJ_8:83
.= lj * (li2 * |( M2F pb, N2 * (M2F pa2) )| ) by A98,RVSUM_1:121
.= (lj * li2) * |( M2F pb, N2 * (M2F pa2) )|;
A106: M2F pa2 = <* (pa2.1).1,(pa2.2).1,(pa2.3).1 *> by A89,ANPROJ_8:def 2;
dom (M2F pa2) = Seg 3 by A91,EUCLID_8:50;
then (M2F pa2).1 in REAL & (M2F pa2).2 in REAL & (M2F pa2).3 in REAL
by FINSEQ_1:1,FINSEQ_2:11;
then reconsider s1 = (pa2.1).1,s2 = (pa2.2).1,s3=(pa2.3).1
as Element of REAL by A106;
A107: M2F pb = <* (pb.1).1,(pb.2).1,(pb.3).1 *> by A62,ANPROJ_8:def 2;
dom (M2F pb) = Seg 3 by A64,EUCLID_8:50;
then (M2F pb).1 in REAL & (M2F pb).2 in REAL & (M2F pb).3 in REAL
by FINSEQ_1:1,FINSEQ_2:11;
then reconsider t1 = (pb.1).1,t2 = (pb.2).1,t3 = (pb.3).1
as Element of F_Real by A107;
reconsider r1 = 1, r2 = 0, r3 = -1 as Element of F_Real by XREAL_0:def 1;
nb * (- na + nc) + ne * (- nd + nf) = nh * (- ng + ni)
proof
reconsider r1 = 1, r2 = 0, r3 = -1 as Element of F_Real
by XREAL_0:def 1;
A108: M2F pa2 = <* (pa2.1).1,(pa2.2).1,(pa2.3).1 *> by A89,ANPROJ_8:def 2;
dom (M2F pa2) = Seg 3 by A91,EUCLID_8:50;
then (M2F pa2).1 in REAL & (M2F pa2).2 in REAL & (M2F pa2).3 in REAL
by FINSEQ_1:1,FINSEQ_2:11;
then reconsider s1 = (pa2.1).1,s2 = (pa2.2).1,s3=(pa2.3).1
as Element of REAL by A108;
A109: M2F pb = <* (pb.1).1,(pb.2).1,(pb.3).1 *> by A62,ANPROJ_8:def 2;
dom (M2F pb) = Seg 3 by A64,EUCLID_8:50;
then (M2F pb).1 in REAL & (M2F pb).2 in REAL & (M2F pb).3 in REAL
by FINSEQ_1:1,FINSEQ_2:11;
then reconsider t1 = (pb.1).1,t2 = (pb.2).1,t3 = (pb.3).1
as Element of F_Real by A109;
M2F pa2 = <* s1,s2,s3 *> by A89,ANPROJ_8:def 2; then
A110: N2 * M2F pa2 = <* 1 * s1 + 0 * s2 + 0 * s3,
0 * s1 + 1 * s2 + 0 * s3,
0 * s1 + 0 * s2 + (-1) * s3 *> by PASCAL:9
.= <* s1,s2,-s3 *>;
M2F pb = <* t1,t2,t3 *> by A62,ANPROJ_8:def 2; then
A111: (M2F pb).1 = t1 &
(M2F pb).2 = t2 &
(M2F pb).3 = t3 &
<* s1,s2,-s3 *>.1 = s1 &
<* s1,s2,-s3 *>.2 = s2 &
<* s1,s2,-s3 *>.3 = -s3;
A112: M2F pb is Element of REAL 3 by A63,EUCLID:22;
A113: |[ s1,s2,-s3 ]| is Element of REAL 3 by EUCLID:22;
0 = |( M2F pb , <* s1,s2,-s3 *> )| by A110,A105,A83,A58
.= t1 * s1 + t2 * s2 + t3 * (-s3) by A112,A113,EUCLID_8:63,A111;
then
A114: t1 * s1 + t2 * s2 = t3 * s3;
|[-1,0,1]| is non zero by EUCLID_5:4,FINSEQ_1:78;
then are_Prop ua2,|[-1,0,1]| by A82,ANPROJ_1:22;
then consider lua2 be Real such that
A115: lua2 <> 0 and
A116: ua2 = lua2 * |[-1,0,1]| by ANPROJ_1:1;
A117: ua2 = |[ lua2 * (-1), lua2 * 0, lua2 * 1]| by A116,EUCLID_5:8
.= |[ - lua2,0,lua2]|;
reconsider za1 = - lua2,za2 = 0,za3 = lua2 as Element of F_Real
by XREAL_0:def 1;
lua2 in REAL & -lua2 in REAL by XREAL_0:def 1;
then reconsider MUFA = <* ufa2 *> as Matrix of 1,3,F_Real
by A117,A82,BKMODEL1:27;
now
len ufa2 = 3 by A117,A82,FINSEQ_1:45;
then dom ufa2 = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
then 1 in dom ufa2 & 2 in dom ufa2 & 3 in dom ufa2 by ENUMSET1:def 1;
then MUFA*(1,1) = |[- lua2,0,lua2]|.1 &
MUFA*(1,2) = |[ - lua2,0,lua2]|.2 &
MUFA*(1,3) = |[ - lua2,0,lua2]|.3 by A117,A82,ANPROJ_8:70;
hence MUFA*(1,1) = - lua2 &
MUFA*(1,2) = 0 &
MUFA*(1,3) = lua2;
end;
then
A119: (<* ufa2 *>)@ = <* <* - lua2 *>, <* 0 *>, <* lua2 *> *>
by BKMODEL1:31;
reconsider nlua2 = - lua2 as Element of F_Real by XREAL_0:def 1;
0 is Element of F_Real & lua2 is Element of F_Real by XREAL_0:def 1;
then reconsider MUFAT = <* <* nlua2 *>, <* 0 *>, <* lua2 *> *>
as Matrix of 3,1,F_Real by BKMODEL1:28;
A120: N * MUFAT is Matrix of 3,1,F_Real by BKMODEL1:24;
A121: N * ufa2 = N * MUFAT by A119,LAPLACE:def 9;
then N * ufa2 = <* <* (N * ufa2)*(1,1) *>,
<* (N * ufa2)*(2,1) *> ,
<* (N * ufa2)*(3,1) *> *> by A120,BKMODEL1:30;
then
A122: pa2.1 = <* (N * ufa2)*(1,1) *> & pa2.2 = <* (N * ufa2)*(2,1) *> &
pa2.3 = <* (N * ufa2)*(3,1) *> by A82;
N * MUFAT is Matrix of 3,1,F_Real by BKMODEL1:24;
then
A123: Indices (N * MUFAT) = [: Seg 3,Seg 1:] by MATRIX_0:23;
width N = 3 by MATRIX_0:24;
then
A124: width N = len MUFAT by MATRIX_0:23;
A125: Col(MUFAT,1) = <* za1,za2,za3 *> by ANPROJ_8:5;
A126: Line(N,1) = <* na,nb,nc *> &
Line(N,2) = <* nd,ne,nf *> &
Line(N,3) = <* ng,nh,ni *> by A7,ANPROJ_9:4;
(N * MUFAT)*(1,1) = Line(N,1) "*" Col(MUFAT,1) &
(N * MUFAT)*(2,1) = Line(N,2) "*" Col(MUFAT,1) &
(N * MUFAT)*(3,1) = Line(N,3) "*" Col(MUFAT,1)
by A123,A124,MATRIX_3:def 4,ANPROJ_8:2;
then (N * MUFAT)*(1,1) = na * za1 + nb * za2 + nc * za3 &
(N * MUFAT)*(2,1) = nd * za1 + ne * za2 + nf * za3 &
(N * MUFAT)*(3,1) = ng * za1 + nh * za2 + ni * za3
by A125,A126,ANPROJ_8:7;
then
A127: (pa2.1).1 = na * nlua2 + nc * lua2 &
(pa2.2).1 = nd * nlua2 + nf * lua2 &
(pa2.3).1 = ng * nlua2 + ni * lua2 by A121,A122;
reconsider z1 = 0,z2 = lub,z3 = 0 as Element of F_Real
by XREAL_0:def 1;
0 is Element of F_Real & lub is Element of F_Real by XREAL_0:def 1;
then
reconsider MUFBT = <* <* 0 *>, <* lub *>, <* 0 *> *>
as Matrix of 3,1,F_Real by BKMODEL1:28;
A128: N * MUFBT is Matrix of 3,1,F_Real by BKMODEL1:24;
A129: N * ufb = N * (<*ufb*>@) by LAPLACE:def 9
.= N * MUFBT by A57,BKMODEL1:31;
then N * ufb = <* <* (N * ufb)*(1,1) *>,
<* (N * ufb)*(2,1) *> ,
<* (N * ufb)*(3,1) *> *> by A128,BKMODEL1:30;
then
A130: pb.1 = <* (N * ufb)*(1,1) *> & pb.2 = <* (N * ufb)*(2,1) *> &
pb.3 = <* (N * ufb)*(3,1) *> by A53;
N * MUFBT is Matrix of 3,1,F_Real by BKMODEL1:24;
then
A131: Indices (N * MUFBT) = [: Seg 3,Seg 1:] by MATRIX_0:23;
width N = 3 by MATRIX_0:24; then
A132: width N = len MUFBT by MATRIX_0:23;
reconsider z1 = 0, z2 = lub, z3 = 0 as Element of F_Real
by XREAL_0:def 1;
A133: Col(MUFBT,1) = <* z1,z2,z3 *> by ANPROJ_8:5;
A134: Line(N,1) = <* na,nb,nc *> &
Line(N,2) = <* nd,ne,nf *> &
Line(N,3) = <* ng,nh,ni *> by ANPROJ_9:4,A7;
(N * MUFBT)*(1,1) = Line(N,1) "*" Col(MUFBT,1) &
(N * MUFBT)*(2,1) = Line(N,2) "*" Col(MUFBT,1) &
(N * MUFBT)*(3,1) = Line(N,3) "*" Col(MUFBT,1)
by A132,MATRIX_3:def 4,A131,ANPROJ_8:2;
then (N * MUFBT)*(1,1) = na * z1 + nb * z2 + nc * z3 &
(N * MUFBT)*(2,1) = nd * z1 + ne * z2 + nf * z3 &
(N * MUFBT)*(3,1) = ng * z1 + nh * z2 + ni * z3
by A133,A134,ANPROJ_8:7;
then (pb.1).1 = nb * lub & (pb.2).1 = ne * lub &
(pb.3).1 = nh * lub by A129,A130;
then (lua2 * lub) * (nb * (- na + nc)) +
(lua2 * lub) * (ne * (- nd + nf))
= (lua2 * lub ) * (nh * (- ng + ni))
by A127,A114;
then (lua2 * lub) * (nb * (- na + nc))
+ (lua2 * lub) * (ne * (- nd + nf))
- (lua2 * lub ) * (nh * (- ng + ni)) = 0;
then (lua2 * lub) * ((nb * (- na + nc))
+ (ne * (- nd + nf)) - (nh * (- ng + ni))) = 0;
then (nb * (- na + nc)) + (ne * (- nd + nf)) - (nh * (- ng + ni)) = 0
by A54,A115;
hence thesis;
end;
hence thesis;
end;
A136: nb * (na + nc) + ne * (nd + nf) = nh * (ng + ni)
proof
reconsider r1 = 1, r2 = 0, r3 = -1 as Element of F_Real by XREAL_0:def 1;
A137: M2F pa = <* (pa.1).1,(pa.2).1,(pa.3).1 *> by A51,ANPROJ_8:def 2;
dom (M2F pa) = Seg 3 by A66,EUCLID_8:50;
then (M2F pa).1 in REAL & (M2F pa).2 in REAL & (M2F pa).3 in REAL
by FINSEQ_1:1,FINSEQ_2:11;
then reconsider s1 = (pa.1).1,s2 = (pa.2).1,s3=(pa.3).1
as Element of REAL by A137;
A138: M2F pb = <* (pb.1).1,(pb.2).1,(pb.3).1 *> by A62,ANPROJ_8:def 2;
dom (M2F pb) = Seg 3 by A64,EUCLID_8:50;
then (M2F pb).1 in REAL & (M2F pb).2 in REAL & (M2F pb).3 in REAL
by FINSEQ_1:1,FINSEQ_2:11;
then reconsider t1 = (pb.1).1,t2 = (pb.2).1,t3 = (pb.3).1
as Element of F_Real by A138;
M2F pa = <* s1,s2,s3 *> by A51,ANPROJ_8:def 2;
then
A139: N2 * M2F pa
= <* 1 * s1 + 0 * s2 + 0 * s3,
0 * s1 + 1 * s2 + 0 * s3,
0 * s1 + 0 * s2 + (-1) * s3 *> by PASCAL:9
.= <* s1,s2,-s3 *>;
M2F pb = <* t1,t2,t3 *> by A62,ANPROJ_8:def 2; then
A140: (M2F pb).1 = t1 &
(M2F pb).2 = t2 &
(M2F pb).3 = t3 &
<* s1,s2,-s3 *>.1 = s1 &
<* s1,s2,-s3 *>.2 = s2 &
<* s1,s2,-s3 *>.3 = -s3;
A141: M2F pb is Element of REAL 3 by A63,EUCLID:22;
A142: |[ s1,s2,-s3 ]| is Element of REAL 3 by EUCLID:22;
0 = |( M2F pb , <* s1,s2,-s3 *> )| by A139,A80,A45,A58
.= t1 * s1 + t2 * s2 + t3 * (-s3)
by A141,A142,EUCLID_8:63,A140;
then
A143: t1 * s1 + t2 * s2 = t3 * s3;
|[1,0,1]| is non zero by EUCLID_5:4,FINSEQ_1:78;
then are_Prop ua,|[1,0,1]| by A44,ANPROJ_1:22;
then consider lua be Real such that
A145: lua <> 0 and
A146: ua = lua * |[1,0,1]| by ANPROJ_1:1;
A147: ua = |[ lua * 1, lua * 0, lua * 1]| by A146,EUCLID_5:8
.= |[lua,0,lua]|;
reconsider za1 = lua,za2 = 0,za3 = lua as Element of F_Real
by XREAL_0:def 1;
lua in REAL by XREAL_0:def 1;
then reconsider MUFA = <* ufa *> as Matrix of 1,3,F_Real
by A147,A44,BKMODEL1:27;
now
len ufa = 3 by A147,A44,FINSEQ_1:45;
then dom ufa = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
then 1 in dom ufa & 2 in dom ufa & 3 in dom ufa by ENUMSET1:def 1;
then MUFA*(1,1) = |[lua,0,lua]|.1 &
MUFA*(1,2) = |[lua,0,lua]|.2 &
MUFA*(1,3) = |[lua,0,lua]|.3 by A147,A44,ANPROJ_8:70;
hence MUFA*(1,1) = lua & MUFA*(1,2) = 0 & MUFA*(1,3) = lua;
end;
then
A148: (<* ufa *>)@ = <* <* lua *>, <* 0 *>, <* lua *> *>
by BKMODEL1:31;
0 is Element of F_Real & lua is Element of F_Real by XREAL_0:def 1;
then reconsider MUFAT = <* <* lua *>, <* 0 *>, <* lua *> *>
as Matrix of 3,1,F_Real by BKMODEL1:28;
A149: N * MUFAT is Matrix of 3,1,F_Real by BKMODEL1:24;
A150: N * ufa = N * MUFAT by A148,LAPLACE:def 9;
N * ufa = <* <* (N * ufa)*(1,1) *>,
<* (N * ufa)*(2,1) *> ,
<* (N * ufa)*(3,1) *> *> by A149,A150,BKMODEL1:30;
then pa.1 = <* (N * ufa)*(1,1) *> & pa.2 = <* (N * ufa)*(2,1) *> &
pa.3 = <* (N * ufa)*(3,1) *> by A44;
then
A152: (pa.1).1 = (N * MUFAT)*(1,1) & (pa.2).1 = (N * MUFAT)*(2,1) &
(pa.3).1 = (N * MUFAT)*(3,1) by A150;
N * MUFAT is Matrix of 3,1,F_Real by BKMODEL1:24;
then
A153: Indices (N * MUFAT) = [: Seg 3,Seg 1:] by MATRIX_0:23;
width N = 3 by MATRIX_0:24;
then
A154: width N = len MUFAT by MATRIX_0:23;
A155: Col(MUFAT,1) = <* za1,za2,za3 *> by ANPROJ_8:5;
A156: Line(N,1) = <* na,nb,nc *> &
Line(N,2) = <* nd,ne,nf *> &
Line(N,3) = <* ng,nh,ni *> by ANPROJ_9:4,A7;
(N * MUFAT)*(1,1) = Line(N,1) "*" Col(MUFAT,1) &
(N * MUFAT)*(2,1) = Line(N,2) "*" Col(MUFAT,1) &
(N * MUFAT)*(3,1) = Line(N,3) "*" Col(MUFAT,1)
by A154,MATRIX_3:def 4,A153,ANPROJ_8:2;
then
A157: (pa.1).1 = na * za1 + nb * za2 + nc * za3 &
(pa.2).1 = nd * za1 + ne * za2 + nf * za3 &
(pa.3).1 = ng * za1 + nh * za2 + ni * za3 by A152,A155,A156,ANPROJ_8:7;
reconsider z1 = 0,z2 = lub,z3 = 0 as Element of F_Real by XREAL_0:def 1;
0 is Element of F_Real & lub is Element of F_Real by XREAL_0:def 1;
then reconsider MUFBT = <* <* 0 *>, <* lub *>, <* 0 *> *>
as Matrix of 3,1,F_Real by BKMODEL1:28;
A158: N * MUFBT is Matrix of 3,1,F_Real by BKMODEL1:24;
A159: N * ufb = N * (<*ufb*>@) by LAPLACE:def 9
.= N * MUFBT by A57,BKMODEL1:31;
N * ufb = <* <* (N * ufb)*(1,1) *>,
<* (N * ufb)*(2,1) *>,
<* (N * ufb)*(3,1) *> *> by A158,A159,BKMODEL1:30;
then
A160: pb.1 = <* (N * ufb)*(1,1) *> & pb.2 = <* (N * ufb)*(2,1) *> &
pb.3 = <* (N * ufb)*(3,1) *> by A53;
N * MUFBT is Matrix of 3,1,F_Real by BKMODEL1:24;
then
A161: Indices (N * MUFBT) = [: Seg 3,Seg 1:] by MATRIX_0:23;
width N = 3 by MATRIX_0:24;
then
A162: width N = len MUFBT by MATRIX_0:23;
reconsider z1 = 0, z2 = lub, z3 = 0 as Element of F_Real
by XREAL_0:def 1;
A163: Col(MUFBT,1) = <* z1,z2,z3 *> by ANPROJ_8:5;
A164: Line(N,1) = <* na,nb,nc *> &
Line(N,2) = <* nd,ne,nf *> &
Line(N,3) = <* ng,nh,ni *> by ANPROJ_9:4,A7;
(N * MUFBT)*(1,1) = Line(N,1) "*" Col(MUFBT,1) &
(N * MUFBT)*(2,1) = Line(N,2) "*" Col(MUFBT,1) &
(N * MUFBT)*(3,1) = Line(N,3) "*" Col(MUFBT,1)
by A162,MATRIX_3:def 4,A161,ANPROJ_8:2;
then (N * MUFBT)*(1,1) = na * z1 + nb * z2 + nc * z3 &
(N * MUFBT)*(2,1) = nd * z1 + ne * z2 + nf * z3 &
(N * MUFBT)*(3,1) = ng * z1 + nh * z2 + ni * z3
by A163,A164,ANPROJ_8:7;
then (pb.1).1 = nb * lub & (pb.2).1 = ne * lub &
(pb.3).1 = nh * lub by A160,A159;
then (lua * lub) * (nb * (na + nc)) +
(lua * lub) * (ne * (nd + nf)) = (lua * lub ) * (nh * (ng + ni))
by A157,A143;
then (lua * lub) * (nb * (na + nc))
+ (lua * lub) * (ne * (nd + nf))
- (lua * lub ) * (nh * (ng + ni)) = 0;
then (lua * lub) * ((nb * (na + nc))
+ (ne * (nd + nf)) - (nh * (ng + ni))) = 0;
then (nb * (na + nc)) + (ne * (nd + nf)) - (nh * (ng + ni)) = 0
by A54,A145;
hence thesis;
end;
<* <* na,nb,nc *>,
<* nd,ne,nf *>,
<* ng,nh,ni *> *> = <* <* N*(1,1),N*(1,2),N*(1,3)*>,
<* N*(2,1),N*(2,2),N*(2,3)*>,
<* N*(3,1),N*(3,2),N*(3,3)*> *>
by A7,MATRIXR2:37;
then
A166: na = N*(1,1) & nb = N*(1,2) & nc = N*(1,3) &
nd = N*(2,1) & ne = N*(2,2) & nf = N*(2,3) &
ng = N*(3,1) & nh = N*(3,2) & ni = N*(3,3) by PASCAL:2;
width N > 0 by MATRIX_0:23;
then len N = 3 & len N1 = 3 & width N1 = 3 &
width (N@) = len N by MATRIX_0:29,23;
then
A167: <* <* ra,rb,rc *>,
<* rb,re,rf *>,
<* rc,rf,ri *> *> = N@ * (N1 * N) by A12,A11,MATRIX_3:33
.= <* <* (N@ * (N1 * N))*(1,1),
(N@ * (N1 * N))*(1,2),
(N@ * (N1 * N))*(1,3) *>,
<* (N@ * (N1 * N))*(2,1),
(N@ * (N1 * N))*(2,2),
(N@ * (N1 * N))*(2,3) *>,
<* (N@ * (N1 * N))*(3,1),
(N@ * (N1 * N))*(3,2),
(N@ * (N1 * N))*(3,3) *> *>
by MATRIXR2:37;
A168: (N@ * (N1 * N))*(1,1) = a * (N*(1,1)) * (N*(1,1))
+ a * (N*(2,1)) * (N*(2,1)) + b * (N*(3,1)) * (N*(3,1)) &
(N@ * (N1 * N))*(1,2) = a * (N*(1,1)) * (N*(1,2))
+ a * (N*(2,1)) * (N*(2,2)) + b * (N*(3,1)) * (N*(3,2)) &
(N@ * (N1 * N))*(1,3) = a * (N*(1,1)) * (N*(1,3))
+ a * (N*(2,1)) * (N*(2,3)) + b * (N*(3,1)) * (N*(3,3)) &
(N@ * (N1 * N))*(2,1) = a * (N*(1,2)) * (N*(1,1))
+ a * (N*(2,2)) * (N*(2,1)) + b * (N*(3,2)) * (N*(3,1)) &
(N@ * (N1 * N))*(2,2) = a * (N*(1,2)) * (N*(1,2))
+ a * (N*(2,2)) * (N*(2,2)) + b * (N*(3,2)) * (N*(3,2)) &
(N@ * (N1 * N))*(2,3) = a * (N*(1,2)) * (N*(1,3))
+ a * (N*(2,2)) * (N*(2,3)) + b * (N*(3,2)) * (N*(3,3)) &
(N@ * (N1 * N))*(3,1) = a * (N*(1,3)) * (N*(1,1))
+ a * (N*(2,3)) * (N*(2,1)) + b * (N*(3,3)) * (N*(3,1)) &
(N@ * (N1 * N))*(3,2) = a * (N*(1,3)) * (N*(1,2))
+ a * (N*(2,3)) * (N*(2,2)) + b * (N*(3,3)) * (N*(3,2)) &
(N@ * (N1 * N))*(3,3) = a * (N*(1,3)) * (N*(1,3))
+ a * (N*(2,3)) * (N*(2,3)) + b * (N*(3,3)) * (N*(3,3))
by BKMODEL1:23;
A169: ra = na * na + nd * nd - ng * ng &
rb = na * nb + nd * ne - ng * nh &
rc = na * nc + nd * nf - ng * ni &
rb = na * nb + nd * ne - ng * nh &
re = nb * nb + ne * ne - nh * nh &
rf = nb * nc + ne * nf - nh * ni &
rc = na * nc + nd * nf - ng * ni &
rf = nb * nc + ne * nf - nh * ni &
ri = nc * nc + nf * nf - ni * ni by A166,A167,PASCAL:2,A168;
A170: nb * na + nb * nc + ne * nd + ne * nf = nh * ng + nh * ni by A136;
- nb * na + nb * nc + -ne * nd + ne * nf = -nh * ng + nh * ni by A81;
hence thesis by A170,A169,A22,A29,A35;
end;
then
A170: M = symmetric_3(ra,ra,-ra,0,0,0) by A12,A11,PASCAL:def 3;
A171: ra <> 0
proof
assume ra = 0;
then Det M = 0.F_Real by A170,BKMODEL1:22;
then Det M is non unital;
hence contradiction by LAPLACE:34;
end;
then
A172: homography(M).:absolute = absolute by A170,Th29;
take N;
thus thesis by A9,A171,A172,A170,A3,A4,A5,A6,BKMODEL1:93;
end;
theorem Th38:
for p1,q1,r1,p2,q2,r2 being Element of absolute
for s1,s2 being Element of real_projective_plane st
p1,q1,r1 are_mutually_distinct &
p2,q2,r2 are_mutually_distinct &
s1 in tangent p1 /\ tangent q1 &
s2 in tangent p2 /\ tangent q2
holds ex N being invertible Matrix of 3,F_Real st
homography(N).:absolute = absolute &
(homography(N)).p1 = p2 & (homography(N)).q1 = q2 &
(homography(N)).r1 = r2 & (homography(N)).s1 = s2
proof
let p1,q1,r1,p2,q2,r2 be Element of absolute;
let s1,s2 be Element of real_projective_plane;
assume that
A1: p1,q1,r1 are_mutually_distinct and
A2: p2,q2,r2 are_mutually_distinct and
A3: s1 in tangent p1 /\ tangent q1 and
A4: s2 in tangent p2 /\ tangent q2;
consider N1 be invertible Matrix of 3,F_Real such that
A5: homography(N1).:absolute = absolute &
(homography(N1)).Dir101 = p1 &
(homography(N1)).Dirm101 = q1 &
(homography(N1)).Dir011 = r1 &
(homography(N1)).Dir010 = s1 by A1,A3,Th37;
consider N2 be invertible Matrix of 3,F_Real such that
A7: homography(N2).:absolute = absolute &
(homography(N2)).Dir101 = p2 &
(homography(N2)).Dirm101 = q2 &
(homography(N2)).Dir011 = r2 &
(homography(N2)).Dir010 = s2 by A2,A4,Th37;
reconsider N = N2 * N1~ as invertible Matrix of 3,F_Real;
A20: (homography(N)).p1 = (homography(N2)).((homography(N1~)).p1)
by ANPROJ_9:13
.= p2 by A5,A7,ANPROJ_9:15;
A21: (homography(N)).q1 = (homography(N2)).((homography(N1~)).q1)
by ANPROJ_9:13
.= q2 by A5,A7,ANPROJ_9:15;
A22: (homography(N)).r1 = (homography(N2)).((homography(N1~)).r1)
by ANPROJ_9:13
.= r2 by A5,A7,ANPROJ_9:15;
A23: (homography(N)).s1 = (homography(N2)).((homography(N1~)).s1)
by ANPROJ_9:13
.= s2 by A5,A7,ANPROJ_9:15;
homography(N1) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h1 = homography(N1) as Element of EnsHomography3;
h1 is_K-isometry by A5;
then h1 in EnsK-isometry;
then reconsider hsg1 = h1 as Element of SubGroupK-isometry by Def05;
homography(N2) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h2 = homography(N2) as Element of EnsHomography3;
h2 is_K-isometry by A7;
then h2 in EnsK-isometry;
then reconsider hsg2 = h2 as Element of SubGroupK-isometry by Def05;
homography(N1~) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h3 = homography(N1~) as Element of EnsHomography3;
A24: hsg1" = h3 by Th36;
set H = EnsK-isometry,
G = GroupHomography3;
reconsider hg1 = hsg1, hg2 = hsg2, hg3 = hsg1" as Element of G
by A24,ANPROJ_9:def 4;
reconsider hsg3 = h3 as Element of SubGroupK-isometry by A24;
reconsider h4 = hsg2 * hsg3 as Element of SubGroupK-isometry;
A25: h4 = hg2 * hg3 by A24,GROUP_2:43
.= h2 (*) h3 by A24,ANPROJ_9:def 3,def 4
.= homography N by ANPROJ_9:18;
h4 in the carrier of SubGroupK-isometry;
then h4 in EnsK-isometry by Def05;
then ex h be Element of EnsHomography3 st h4 = h & h is_K-isometry;
hence thesis by A20,A21,A22,A23,A25;
end;
theorem
for p1,q1,r1,p2,q2,r2 being Element of absolute st
p1,q1,r1 are_mutually_distinct &
p2,q2,r2 are_mutually_distinct
holds ex N being invertible Matrix of 3,F_Real st
homography(N).:absolute = absolute &
(homography(N)).p1 = p2 & (homography(N)).q1 = q2 &
(homography(N)).r1 = r2
proof
let p1,q1,r1,p2,q2,r2 be Element of absolute;
assume that
A1: p1,q1,r1 are_mutually_distinct and
A2: p2,q2,r2 are_mutually_distinct;
consider t be Element of real_projective_plane such that
A3: tangent p1 /\ tangent q1 = {t} by A1,Th25;
t in tangent p1 /\ tangent q1 by A3,TARSKI:def 1;
then consider N1 be invertible Matrix of 3,F_Real such that
A5: homography(N1).:absolute = absolute &
(homography(N1)).Dir101 = p1 &
(homography(N1)).Dirm101 = q1 &
(homography(N1)).Dir011 = r1 &
(homography(N1)).Dir010 = t by A1,Th37;
consider u be Element of real_projective_plane such that
A6: tangent q2 /\ tangent p2 = {u} by A2,Th25;
u in tangent p2 /\ tangent q2 by A6,TARSKI:def 1;
then consider N2 be invertible Matrix of 3,F_Real such that
A7: homography(N2).:absolute = absolute &
(homography(N2)).Dir101 = p2 &
(homography(N2)).Dirm101 = q2 &
(homography(N2)).Dir011 = r2 &
(homography(N2)).Dir010 = u by A2,Th37;
reconsider N = N2 * N1~ as invertible Matrix of 3,F_Real;
A20: (homography(N)).p1 = (homography(N2)).((homography(N1~)).p1)
by ANPROJ_9:13
.= p2 by A5,A7,ANPROJ_9:15;
A21: (homography(N)).q1 = (homography(N2)).((homography(N1~)).q1)
by ANPROJ_9:13
.= q2 by A5,A7,ANPROJ_9:15;
A22: (homography(N)).r1 = (homography(N2)).((homography(N1~)).r1)
by ANPROJ_9:13
.= r2 by A5,A7,ANPROJ_9:15;
homography(N1) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h1 = homography(N1) as Element of EnsHomography3;
h1 is_K-isometry by A5;
then h1 in EnsK-isometry;
then reconsider hsg1 = h1 as Element of SubGroupK-isometry by Def05;
homography(N2) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h2 = homography(N2) as Element of EnsHomography3;
h2 is_K-isometry by A7;
then h2 in EnsK-isometry;
then reconsider hsg2 = h2 as Element of SubGroupK-isometry by Def05;
homography(N1~) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h3 = homography(N1~) as Element of EnsHomography3;
A24: hsg1" = h3 by Th36;
set H = EnsK-isometry,
G = GroupHomography3;
reconsider hg1 = hsg1, hg2 = hsg2, hg3 = hsg1" as Element of G
by A24,ANPROJ_9:def 4;
reconsider hsg3 = h3 as Element of SubGroupK-isometry by A24;
reconsider h4 = hsg2 * hsg3 as Element of SubGroupK-isometry;
A25: h4 = hg2 * hg3 by A24,GROUP_2:43
.= h2 (*) h3 by A24,ANPROJ_9:def 3,def 4
.= homography N by ANPROJ_9:18;
h4 in the carrier of SubGroupK-isometry;
then h4 in EnsK-isometry by Def05;
then ex h be Element of EnsHomography3 st h4 = h & h is_K-isometry;
hence thesis by A20,A21,A22,A25;
end;
theorem Th39:
for CLSP being CollSp
for p,q,r,s being Element of CLSP st
Line(p,q) = Line(r,s) holds r,s,p are_collinear by COLLSP:10,11;
theorem Th40:
for CLSP being CollSp
for p,q being Element of CLSP holds Line(p,q) = Line(q,p)
proof
let CLSP be CollSp;
let p,q be Element of CLSP;
A1: Line(p,q) c= Line(q,p)
proof
let x be object;
assume x in Line(p,q);
then x in {y where y is Element of CLSP: p,q,y are_collinear}
by COLLSP:def 5;
then consider y be Element of CLSP such that
A2: y = x and
A3: p,q,y are_collinear;
q,p,y are_collinear by A3,COLLSP:4;
then y in {y where y is Element of CLSP: q,p,y are_collinear};
hence thesis by A2,COLLSP:def 5;
end;
Line(q,p) c= Line(p,q)
proof
let x be object;
assume x in Line(q,p);
then x in {y where y is Element of CLSP: q,p,y are_collinear}
by COLLSP:def 5;
then consider y be Element of CLSP such that
A4: y = x and
A5: q,p,y are_collinear;
p,q,y are_collinear by A5,COLLSP:4;
then y in {y where y is Element of CLSP: p,q,y are_collinear};
hence thesis by A4,COLLSP:def 5;
end;
hence thesis by A1;
end;
theorem Th41:
for N being invertible Matrix of 3,F_Real
for p,q,r,s being Element of ProjectiveSpace TOP-REAL 3 st
Line(homography(N).p,homography(N).q) = Line(homography(N).r,homography(N).s)
holds p,q,r are_collinear & p,q,s are_collinear &
r,s,p are_collinear & r,s,q are_collinear
proof
let N being invertible Matrix of 3,F_Real;
let p,q,r,s being Element of ProjectiveSpace TOP-REAL 3;
assume
A1: Line(homography(N).p,homography(N).q)
= Line(homography(N).r,homography(N).s);
hence p,q,r are_collinear by ANPROJ_8:102,Th39;
Line(homography(N).p,homography(N).q)
= Line(homography(N).s,homography(N).r) by A1,Th40;
hence p,q,s are_collinear by ANPROJ_8:102,Th39;
thus r,s,p are_collinear by A1,ANPROJ_8:102,Th39;
Line(homography(N).q,homography(N).p)
= Line(homography(N).r,homography(N).s) by A1,Th40;
hence r,s,q are_collinear by ANPROJ_8:102,Th39;
end;
theorem Th42:
for N being invertible Matrix of 3,F_Real
for p,q,r,s,t,u,np,nq,nr,ns being Element of real_projective_plane st
p <> q & r <> s & np <> nq & nr <> ns &
p,q,t are_collinear & r,s,t are_collinear &
np = homography(N).p & nq = homography(N).q &
nr = homography(N).r & ns = homography(N).s &
np,nq,u are_collinear & nr,ns,u are_collinear holds
u = homography(N).t or Line(np,nq) = Line(nr,ns)
proof
let N be invertible Matrix of 3,F_Real;
let p,q,r,s,t,u,np,nq,nr,ns being Element of real_projective_plane;
assume that
A0: p <> q & r <> s & np <> nq & nr <> ns and
A1: p,q,t are_collinear and
A2: r,s,t are_collinear and
A3: np = homography(N).p and
A4: nq = homography(N).q and
A5: nr = homography(N).r and
A6: ns = homography(N).s and
A7: np,nq,u are_collinear and
A8: nr,ns,u are_collinear;
A9: t in Line(p,q) & t in Line(r,s) & u in Line(np,nq) & u in Line(nr,ns)
by A1,A2,A7,A8,COLLSP:11;
reconsider L1 = Line(p,q),L2 = Line(r,s),L3 = Line(np,nq),
L4 = Line(nr,ns) as LINE of real_projective_plane
by A0,COLLSP:def 7;
reconsider LL1 = L1,LL2 = L2, LL3 = L3,
LL4 = L4 as LINE of IncProjSp_of real_projective_plane
by INCPROJ:4;
reconsider t9 = t,u9 = u as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
A10: t9 on LL1 & t9 on LL2 & u9 on LL3 & u9 on LL4 by A9,INCPROJ:5;
reconsider nt = homography(N).t as Element of real_projective_plane
by FUNCT_2:5;
A11: nt in Line(np,nq) & nt in Line(nr,ns)
by A1,A2,A3,A4,A5,A6,ANPROJ_8:102,COLLSP:11;
reconsider nt9 = nt as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
nt9 on LL3 & nt9 on LL4 by A11,INCPROJ:5;
hence thesis by A10,INCPROJ:8;
end;
theorem Th43:
for N being invertible Matrix of 3,F_Real
for p,q,r,s,t,u,np,nq,nr,ns being Element of real_projective_plane st
p <> q & r <> s & np <> nq & nr <> ns &
p,q,t are_collinear & r,s,t are_collinear &
np = homography(N).p & nq = homography(N).q &
nr = homography(N).r & ns = homography(N).s &
np,nq,u are_collinear & nr,ns,u are_collinear &
not p,q,r are_collinear holds u = homography(N).t
proof
let N be invertible Matrix of 3,F_Real;
let p,q,r,s,t,u,np,nq,nr,ns being Element of real_projective_plane;
assume that
A1: p <> q & r <> s & np <> nq & nr <> ns &
p,q,t are_collinear & r,s,t are_collinear &
np = homography(N).p & nq = homography(N).q &
nr = homography(N).r & ns = homography(N).s &
np,nq,u are_collinear & nr,ns,u are_collinear and
A2: not p,q,r are_collinear;
u = homography(N).t or Line(np,nq) = Line(nr,ns) by A1,Th42;
hence thesis by A1,A2,Th41;
end;
theorem
for p,q being Element of absolute
for a,b being Element of BK_model
holds ex N being invertible Matrix of 3,F_Real st
homography(N).:absolute = absolute &
(homography(N)).a = b & (homography(N)).p = q
proof
let p,q be Element of absolute;
let a,b be Element of BK_model;
consider p9 be Element of absolute such that
A1: p <> p9 and
A2: p,a,p9 are_collinear by Th16;
consider q9 be Element of absolute such that
A3: q <> q9 and
A4: q,b,q9 are_collinear by Th16;
consider t be Element of real_projective_plane such that
A5: tangent p /\ tangent p9 = {t} by A1,Th25;
A6: t in tangent p /\ tangent p9 by A5,TARSKI:def 1;
consider u be Element of real_projective_plane such that
A7: tangent q /\ tangent q9 = {u} by A3,Th25;
A8: u in tangent q /\ tangent q9 by A7,TARSKI:def 1;
reconsider a9 = a as Element of real_projective_plane;
p <> p9 & a in BK_model & a,p,p9 are_collinear &
t in tangent p & t in tangent p9 by A1,A2,A6,XBOOLE_0:def 4,COLLSP:4;
then consider Ra be Element of real_projective_plane such that
A9: Ra in absolute and
A10: a9,t,Ra are_collinear by Th31;
reconsider RRa = Ra as Element of absolute by A9;
reconsider b9 = b as Element of real_projective_plane;
q <> q9 & b in BK_model & b,q,q9 are_collinear &
u in tangent q & u in tangent q9 by A3,A4,A8,XBOOLE_0:def 4,COLLSP:4;
then consider Rb be Element of real_projective_plane such that
A11: Rb in absolute and
A12: b9,u,Rb are_collinear by Th31;
reconsider RRb = Rb as Element of absolute by A11;
A13: p,p9,Ra are_mutually_distinct
proof
now
consider ra be Element of real_projective_plane such that
A14: ra = Ra & tangent RRa = Line(ra,pole_infty RRa) by Def04;
thus p <> Ra
proof
assume p = Ra;
then t in Line(ra,pole_infty RRa) by A14,A6,XBOOLE_0:def 4;
then ra,pole_infty RRa,t are_collinear by COLLSP:11;
then
A15: ra,t,pole_infty RRa are_collinear by COLLSP:4;
A16: ra,t,a9 are_collinear by A14,A10,HESSENBE:1;
ra <> t
proof
assume ra = t;
then t in absolute & t in tangent p & t in tangent p9
by A14,A6,XBOOLE_0:def 4;
then t in tangent p /\ absolute & t in tangent p9 /\ absolute
by XBOOLE_0:def 4;
then t in {p} & t in {p9} by Th22;
then t = p & t = p9 by TARSKI:def 1;
hence contradiction by A1;
end;
then a in tangent RRa & a in BK_model by A16,A15,A14,COLLSP:6,11;
then tangent RRa meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30;
end;
thus p9 <> Ra
proof
assume p9 = Ra;
then t in Line(ra,pole_infty RRa) by A14,A6,XBOOLE_0:def 4;
then ra,pole_infty RRa,t are_collinear by COLLSP:11;
then
A17: ra,t,pole_infty RRa are_collinear by COLLSP:4;
A18: ra,t,a9 are_collinear by A14,A10,HESSENBE:1;
ra <> t
proof
assume ra = t;
then t in absolute & t in tangent p & t in tangent p9
by A14,A6,XBOOLE_0:def 4;
then t in tangent p /\ absolute & t in tangent p9 /\ absolute
by XBOOLE_0:def 4;
then t in {p} & t in {p9} by Th22;
then t = p & t = p9 by TARSKI:def 1;
hence contradiction by A1;
end;
then a in tangent RRa & a in BK_model by A18,A17,A14,COLLSP:6,11;
then tangent RRa meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30;
end;
end;
hence thesis by A1;
end;
now
now
consider rb be Element of real_projective_plane such that
A19: rb = Rb & tangent RRb = Line(rb,pole_infty RRb) by Def04;
thus q <> Rb
proof
assume q = Rb;
then u in Line(rb,pole_infty RRb) by A19,A8,XBOOLE_0:def 4;
then rb,pole_infty RRb,u are_collinear by COLLSP:11;
then
A20: rb,u,pole_infty RRb are_collinear by COLLSP:4;
A21: rb,u,b9 are_collinear by A19,A12,HESSENBE:1;
rb <> u
proof
assume rb = u;
then u in absolute & u in tangent q & u in tangent q9
by A19,A8,XBOOLE_0:def 4;
then u in tangent q /\ absolute & u in tangent q9 /\ absolute
by XBOOLE_0:def 4;
then u in {q} & u in {q9} by Th22;
then u = q & u = q9 by TARSKI:def 1;
hence contradiction by A3;
end;
then b in tangent RRb & b in BK_model by A21,A20,A19,COLLSP:6,11;
then tangent RRb meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30;
end;
thus q9 <> Rb
proof
assume q9 = Rb;
then u in Line(rb,pole_infty RRb) by A19,A8,XBOOLE_0:def 4;
then rb,pole_infty RRb,u are_collinear by COLLSP:11;
then
A22: rb,u,pole_infty RRb are_collinear by COLLSP:4;
A23: rb,u,b9 are_collinear by A19,A12,HESSENBE:1;
rb <> u
proof
assume rb = u;
then u in absolute & u in tangent q & u in tangent q9
by A19,A8,XBOOLE_0:def 4;
then u in tangent q /\ absolute & u in tangent q9 /\ absolute
by XBOOLE_0:def 4;
then u in {q} & u in {q9} by Th22;
then u = q & u = q9 by TARSKI:def 1;
hence contradiction by A3;
end;
then b in tangent RRb & b in BK_model by A23,A22,A19,COLLSP:6,11;
then tangent RRb meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30;
end;
end;
hence q,q9,Rb are_mutually_distinct by A3;
end;
then
consider N be invertible Matrix of 3,F_Real such that
A24: homography(N).:absolute = absolute and
A25: (homography(N)).p = q and
A26: (homography(N)).p9 = q9 and
A27: (homography(N)).Ra = Rb and
A28: (homography(N)).t = u by A9,A11,A6,A8,A13,Th38;
reconsider plp = p, plq = p9, plr = Ra, pls = t,
plt = a, np = q, nq = q9, nr = Rb, ns = u, nu = b
as Element of real_projective_plane;
now
thus plp <> plq by A1;
thus np <> nq by A3;
thus nr <> ns
proof
consider rb be Element of real_projective_plane such that
A29: rb = Rb & tangent RRb = Line(rb,pole_infty RRb) by Def04;
rb <> u
proof
assume rb = u;
then u in absolute & u in tangent q & u in tangent q9
by A29,A8,XBOOLE_0:def 4;
then u in tangent q /\ absolute & u in tangent q9 /\ absolute
by XBOOLE_0:def 4;
then u in {q} & u in {q9} by Th22;
then u = q & u = q9 by TARSKI:def 1;
hence contradiction by A3;
end;
hence thesis by A29;
end;
thus plr <> pls
proof
consider ra be Element of real_projective_plane such that
A30: ra = Ra & tangent RRa = Line(ra,pole_infty RRa) by Def04;
ra <> t
proof
assume ra = t;
then t in absolute & t in tangent p & t in tangent p9
by A30,A6,XBOOLE_0:def 4;
then t in tangent p /\ absolute & t in tangent p9 /\ absolute
by XBOOLE_0:def 4;
then t in {p} & t in {p9} by Th22;
then t = p & t = p9 by TARSKI:def 1;
hence contradiction by A1;
end;
hence thesis by A30;
end;
thus plp,plq,plt are_collinear by A2,COLLSP:4;
thus plr,pls,plt are_collinear by A10,HESSENBE:1;
thus np = homography(N).plp & nq = homography(N).plq &
nr = homography(N).plr & ns = homography(N).pls by A25,A26,A27,A28;
thus np,nq,nu are_collinear by A4,HESSENBE:1;
thus nr,ns,nu are_collinear by A12,HESSENBE:1;
thus not plp,plq,plr are_collinear
proof
assume plp,plq,plr are_collinear;
then p,p9,RRa are_collinear;
hence contradiction by A13,BKMODEL1:92;
end;
end;
then nu = homography(N).plt by Th43;
hence thesis by A24,A25;
end;
theorem
for p,q,r,s being Element of absolute st
p,q,r are_mutually_distinct & q,p,s are_mutually_distinct
holds ex N being invertible Matrix of 3,F_Real st
homography(N).:absolute = absolute &
(homography(N)).p = q & (homography(N)).q = p &
(homography(N)).r = s &
(for t being Element of real_projective_plane st
t in tangent p /\ tangent q holds (homography(N)).t = t)
proof
let p,q,r,s be Element of absolute;
assume that
A1: p,q,r are_mutually_distinct and
A2: q,p,s are_mutually_distinct;
consider t be Element of real_projective_plane such that
A3: tangent p /\ tangent q = {t} by A1,Th25;
A4: t in tangent p /\ tangent q by A3,TARSKI:def 1;
then consider N1 be invertible Matrix of 3,F_Real such that
A5: homography(N1).:absolute = absolute &
(homography(N1)).Dir101 = p &
(homography(N1)).Dirm101 = q &
(homography(N1)).Dir011 = r &
(homography(N1)).Dir010 = t by A1,Th37;
consider N2 be invertible Matrix of 3,F_Real such that
A7: homography(N2).:absolute = absolute &
(homography(N2)).Dir101 = q &
(homography(N2)).Dirm101 = p &
(homography(N2)).Dir011 = s &
(homography(N2)).Dir010 = t by A2,A4,Th37;
reconsider N = N2 * N1~ as invertible Matrix of 3,F_Real;
A20: (homography(N)).p = (homography(N2)).((homography(N1~)).p)
by ANPROJ_9:13
.= q by A5,A7,ANPROJ_9:15;
A21: (homography(N)).q = (homography(N2)).((homography(N1~)).q)
by ANPROJ_9:13
.= p by A5,A7,ANPROJ_9:15;
A22: (homography(N)).r = (homography(N2)).((homography(N1~)).r)
by ANPROJ_9:13
.= s by A5,A7,ANPROJ_9:15;
A23: (homography(N)).t = (homography(N2)).((homography(N1~)).t)
by ANPROJ_9:13
.= t by A5,A7,ANPROJ_9:15;
homography(N1) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h1 = homography(N1) as Element of EnsHomography3;
h1 is_K-isometry by A5;
then h1 in EnsK-isometry;
then reconsider hsg1 = h1 as Element of SubGroupK-isometry by Def05;
homography(N2) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h2 = homography(N2) as Element of EnsHomography3;
h2 is_K-isometry by A7;
then h2 in EnsK-isometry;
then reconsider hsg2 = h2 as Element of SubGroupK-isometry by Def05;
homography(N1~) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h3 = homography(N1~) as Element of EnsHomography3;
A24: hsg1" = h3 by Th36;
set H = EnsK-isometry,
G = GroupHomography3;
reconsider hg1 = hsg1, hg2 = hsg2, hg3 = hsg1" as Element of G
by A24,ANPROJ_9:def 4;
reconsider hsg3 = h3 as Element of SubGroupK-isometry by A24;
reconsider h4 = hsg2 * hsg3 as Element of SubGroupK-isometry;
A25: h4 = hg2 * hg3 by A24,GROUP_2:43
.= h2 (*) h3 by A24,ANPROJ_9:def 3,def 4
.= homography N by ANPROJ_9:18;
h4 in the carrier of SubGroupK-isometry;
then h4 in EnsK-isometry by Def05;
then consider h be Element of EnsHomography3 such that
A26: h4 = h and
A27: h is_K-isometry;
take N;
thus homography(N).:absolute = absolute by A25,A26,A27;
thus (homography(N)).p = q & (homography(N)).q = p &
(homography(N)).r = s by A20,A21,A22;
thus for t being Element of real_projective_plane st
t in tangent p /\ tangent q holds (homography(N)).t = t
proof
let v be Element of real_projective_plane;
assume v in tangent p /\ tangent q;
then v = t by A3,TARSKI:def 1;
hence thesis by A23;
end;
end;
theorem Th44:
for P,Q being Element of BK_model st P <> Q holds
ex P1,P2,P3,P4 being Element of absolute,
P5 being Element of ProjectiveSpace TOP-REAL 3 st
P1 <> P2 &
P,Q,P1 are_collinear & P,Q,P2 are_collinear &
P,P5,P3 are_collinear & Q,P5,P4 are_collinear &
P1,P2,P3 are_mutually_distinct &
P1,P2,P4 are_mutually_distinct &
P5 in tangent P1 /\ tangent P2
proof
let P,Q being 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 and
A4: P,Q,P2 are_collinear by Th12;
consider R be Element of real_projective_plane such that
A5: R in tangent P1 & R in tangent P2 by Th24;
consider u be Element of TOP-REAL 3 such that
A6: u is non zero and
A7: R = Dir u by ANPROJ_1:26;
per cases;
suppose u.3 = 0;
reconsider RR = R as Element of ProjectiveSpace TOP-REAL 3;
P,P1,P2 are_collinear by A1,A3,A4,COLLSP:6;
then consider PT1 be Element of ProjectiveSpace TOP-REAL 3 such that
A8: PT1 in absolute and
A9: P,RR,PT1 are_collinear by A2,A5,Th31;
Q,P,P1 are_collinear & Q,P,P2 are_collinear by A3,A4,COLLSP:4;
then Q,P1,P2 are_collinear by A1,COLLSP:6;
then consider PT2 be Element of ProjectiveSpace TOP-REAL 3 such that
A10: PT2 in absolute and
A11: Q,RR,PT2 are_collinear by A2,A5,Th31;
now
thus P,Q,P1 are_collinear by A3;
thus P,Q,P2 are_collinear by A4;
A12: PT1 <> RR
proof
assume PT1 = RR;
then PT1 in absolute /\ tangent P1 & PT1 in absolute /\ tangent P2
by A5,A8,XBOOLE_0:def 4;
then PT1 in {P1} & PT1 in {P2} by Th22;
then PT1 = P1 & PT1 = P2 by TARSKI:def 1;
hence contradiction by A2;
end;
A13: PT2 <> RR
proof
assume PT2 = RR;
then PT2 in absolute /\ tangent P1 & PT2 in absolute /\ tangent P2
by A5,A10,XBOOLE_0:def 4;
then PT2 in {P1} & PT2 in {P2} by Th22;
then PT2 = P1 & PT2 = P2 by TARSKI:def 1;
hence contradiction by A2;
end;
A14: P2 <> PT1
proof
P,PT1,RR are_collinear by A9,COLLSP:4;
hence thesis by A5,A12,Th32;
end;
P1 <> PT1
proof
assume
A15: P1 = PT1;
consider p1 be Element of real_projective_plane such that
A16: p1 = P1 & tangent P1 = Line(p1,pole_infty P1) by Def04;
reconsider pt1 = PT1,
rr = RR,
p = P as Element of real_projective_plane;
A17: p1,pole_infty P1,pt1 are_collinear &
p1,pole_infty P1,rr are_collinear
by A15,A5,Th21,A16,COLLSP:11;
rr,pt1,p are_collinear by A9,COLLSP:8;
then P in tangent P1 & P in BK_model by A12,A17,A16,COLLSP:9,11;
then tangent P1 meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30;
end;
hence P1,P2,PT1 are_mutually_distinct by A14,A2;
A18: P1 <> PT2
proof
Q,PT2,RR are_collinear by A11,COLLSP:4;
hence thesis by A5,A13,Th32;
end;
P2 <> PT2
proof
assume
A19: P2 = PT2;
consider p2 be Element of real_projective_plane such that
A20: p2 = P2 & tangent P2 = Line(p2,pole_infty P2) by Def04;
reconsider pt2 = PT2,
rr = RR,
q = Q as Element of real_projective_plane;
A21: p2,pole_infty P2,pt2 are_collinear &
p2,pole_infty P2,rr are_collinear
by A20,A19,A5,Th21,COLLSP:11;
rr,pt2,q are_collinear by A11,COLLSP:8;
then Q in tangent P2 & Q in BK_model by A20,A13,A21,COLLSP:9,11;
then tangent P2 meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30;
end;
hence P1,P2,PT2 are_mutually_distinct by A18,A2;
thus R in tangent P1 /\ tangent P2 by A5,XBOOLE_0:def 4;
thus P,RR,PT1 are_collinear by A9;
thus Q,RR,PT2 are_collinear by A11;
end;
hence thesis by A8,A10;
end;
suppose
A22: u.3 <> 0;
reconsider v = |[u.1 / u.3,u.2 / u.3,1]| as
non zero Element of TOP-REAL 3 by BKMODEL1:41;
A24: u.3 * (u.1 / u.3) = u.1 & u.3 * (u.2/u.3) = u.2 by A22,XCMPLX_1:87;
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.2,u.3 ]| by A24,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
.= u by EUCLID_5:3;
then are_Prop v,u by A22,ANPROJ_1:1;
then
A25: R = Dir v & v.3 = 1 by A6,A7,ANPROJ_1:22;
reconsider RR = R as Element of ProjectiveSpace TOP-REAL 3;
P <> RR
proof
assume P = RR;
then BK_model meets tangent P1 by A5,XBOOLE_0:def 4;
hence contradiction by Th30;
end;
then consider PT1 be Element of absolute such that
A26: P,RR,PT1 are_collinear by A25,Th03;
Q <> RR
proof
assume Q = RR;
then BK_model meets tangent P2 by A5,XBOOLE_0:def 4;
hence contradiction by Th30;
end;
then consider PT2 being Element of absolute such that
A27: Q,RR,PT2 are_collinear by A25,Th03;
now
thus P,Q,P1 are_collinear by A3;
thus P,Q,P2 are_collinear by A4;
A28: PT1 <> RR
proof
assume PT1 = RR;
then PT1 in absolute /\ tangent P1 & PT1 in absolute /\ tangent P2
by A5,XBOOLE_0:def 4;
then PT1 in {P1} & PT1 in {P2} by Th22;
then PT1 = P1 & PT1 = P2 by TARSKI:def 1;
hence contradiction by A2;
end;
A29: PT2 <> RR
proof
assume PT2 = RR;
then PT2 in absolute /\ tangent P1 & PT2 in absolute /\ tangent P2
by A5,XBOOLE_0:def 4;
then PT2 in {P1} & PT2 in {P2} by Th22;
then PT2 = P1 & PT2 = P2 by TARSKI:def 1;
hence contradiction by A2;
end;
A30: P2 <> PT1
proof
P,PT1,RR are_collinear by A26,COLLSP:4;
hence thesis by A5,A28,Th32;
end;
P1 <> PT1
proof
assume
A31: P1 = PT1;
consider p1 be Element of real_projective_plane such that
A32: p1 = P1 & tangent P1 = Line(p1,pole_infty P1) by Def04;
reconsider pt1 = PT1,
rr = RR,
p = P as Element of real_projective_plane;
A33: p1,pole_infty P1,pt1 are_collinear &
p1,pole_infty P1,rr are_collinear by A31,A5,Th21,A32,COLLSP:11;
rr,pt1,p are_collinear by A26,COLLSP:8;
then P in tangent P1 & P in BK_model by A28,A33,A32,COLLSP:9,11;
then tangent P1 meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30;
end;
hence P1,P2,PT1 are_mutually_distinct by A30,A2;
A34: P1 <> PT2
proof
Q,PT2,RR are_collinear by A27,COLLSP:4;
hence thesis by A5,A29,Th32;
end;
P2 <> PT2
proof
assume
A35: P2 = PT2;
consider p2 being Element of real_projective_plane such that
A36: p2 = P2 & tangent P2 = Line(p2,pole_infty P2) by Def04;
reconsider pt2 = PT2,
rr = RR,
q = Q as Element of real_projective_plane;
A37: p2,pole_infty P2,pt2 are_collinear &
p2,pole_infty P2,rr are_collinear by A35,A5,Th21,A36,COLLSP:11;
rr,pt2,q are_collinear by A27,COLLSP:8;
then Q in tangent P2 by A36,A29,A37,COLLSP:9,11;
then tangent P2 meets BK_model by XBOOLE_0:def 4;
hence contradiction by Th30;
end;
hence P1,P2,PT2 are_mutually_distinct by A34,A2;
thus RR in tangent P1 /\ tangent P2 by A5,XBOOLE_0:def 4;
thus P,RR,PT1 are_collinear by A26;
thus Q,RR,PT2 are_collinear by A27;
end;
hence thesis;
end;
end;
theorem Th45:
for P,Q being Element of BK_model st P <> Q holds
ex N being invertible Matrix of 3,F_Real st
(homography(N)).:absolute = absolute &
(homography(N)). P = Q & (homography(N)).Q = P &
(ex P1,P2 being Element of absolute st P1 <> P2 &
P,Q,P1 are_collinear & P,Q,P2 are_collinear &
homography(N).P1 = P2 & homography(N).P2 = P1)
proof
let P,Q being Element of BK_model;
assume
A1: P <> Q;
consider P1,P2,P3,P4 be Element of absolute,
P5 be Element of ProjectiveSpace TOP-REAL 3 such that
A2: P1 <> P2 and
A3: P,Q,P1 are_collinear and
A4: P,Q,P2 are_collinear and
A5: P,P5,P3 are_collinear and
A6: Q,P5,P4 are_collinear and
A7: P1,P2,P3 are_mutually_distinct and
A8: P1,P2,P4 are_mutually_distinct and
A9: P5 in tangent P1 /\ tangent P2 by A1,Th44;
consider N1 be invertible Matrix of 3,F_Real such that
A10: homography(N1).:absolute = absolute and
A11: (homography(N1)).Dir101 = P1 and
A12: (homography(N1)).Dirm101 = P2 and
A13: (homography(N1)).Dir011 = P3 and
A14: (homography(N1)).Dir010 = P5 by A7,A9,Th37;
P2,P1,P4 are_mutually_distinct by A8;
then consider N2 be invertible Matrix of 3,F_Real such that
A15: homography(N2).:absolute = absolute and
A16: (homography(N2)).Dir101 = P2 and
A17: (homography(N2)).Dirm101 = P1 and
A18: (homography(N2)).Dir011 = P4 and
A19: (homography(N2)).Dir010 = P5 by A9,Th37;
reconsider N = N2 * N1~ as invertible Matrix of 3,F_Real;
A20: (homography(N)).P1 = (homography(N2)).((homography(N1~)).P1)
by ANPROJ_9:13
.= P2 by A11,A16,ANPROJ_9:15;
A21: (homography(N)).P2 = (homography(N2)).((homography(N1~)).P2)
by ANPROJ_9:13
.= P1 by A12,A17,ANPROJ_9:15;
A22: (homography(N)).P3 = (homography(N2)).((homography(N1~)).P3)
by ANPROJ_9:13
.= P4 by A13,A18,ANPROJ_9:15;
A23: (homography(N)).P5 = (homography(N2)).((homography(N1~)).P5)
by ANPROJ_9:13
.= P5 by A14,A19,ANPROJ_9:15;
homography(N1) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h1 = homography(N1) as Element of EnsHomography3;
h1 is_K-isometry by A10;
then h1 in EnsK-isometry;
then reconsider hsg1 = h1 as Element of SubGroupK-isometry by Def05;
homography(N2) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h2 = homography(N2) as Element of EnsHomography3;
h2 is_K-isometry by A15;
then h2 in EnsK-isometry;
then reconsider hsg2 = h2 as Element of SubGroupK-isometry by Def05;
homography(N1~) in EnsHomography3 by ANPROJ_9:def 1;
then reconsider h3 = homography(N1~) as Element of EnsHomography3;
A24: hsg1" = h3 by Th36;
set H = EnsK-isometry,
G = GroupHomography3;
reconsider hg1 = hsg1, hg2 = hsg2, hg3 = hsg1" as Element of G
by A24,ANPROJ_9:def 4;
reconsider hsg3 = h3 as Element of SubGroupK-isometry by A24;
reconsider h4 = hsg2 * hsg3 as Element of SubGroupK-isometry;
A25: h4 = hg2 * hg3 by A24,GROUP_2:43
.= h2 (*) h3 by A24,ANPROJ_9:def 3,def 4
.= homography N by ANPROJ_9:18;
h4 in the carrier of SubGroupK-isometry;
then h4 in EnsK-isometry by Def05;
then consider h be Element of EnsHomography3 such that
A26: h4 = h and
A27: h is_K-isometry;
take N;
thus homography(N).:absolute = absolute by A25,A26,A27;
set NP = homography(N).P,
NQ = homography(N).Q,
NP1 = homography(N).P1,
NP2 = homography(N).P2,
NP3 = homography(N).P3,
NP4 = homography(N).P4,
NP5 = homography(N).P5;
A28: P,P1,P2 are_collinear by A1,A3,A4,ANPROJ_8:57,HESSENBE:2;
Q,P,P1 are_collinear & Q,P,P2 are_collinear by A3,A4,COLLSP:4;
then
A29: Q,P1,P2 are_collinear by A1,ANPROJ_8:57,HESSENBE:2;
thus homography(N).P = Q & homography(N).Q = P
proof
A30: NP <> NQ
proof
assume
A31: NP = NQ;
Q = homography(N~).NQ by ANPROJ_9:15
.= P by A31,ANPROJ_9:15;
hence contradiction by A1;
end;
A32: NP,NQ,NP1 are_collinear & NP,NQ,NP2 are_collinear &
NP,NP5,NP3 are_collinear & NQ,NP5,NP4 are_collinear
by A3,A4,A5,A6,ANPROJ_8:102;
then
A33: NP,NP1,NP2 are_collinear by ANPROJ_8:57,A30,HESSENBE:2;
A34: P1,P2,Q are_collinear by A29,ANPROJ_8:57,HESSENBE:1;
P5,P4,Q are_collinear by A6,ANPROJ_8:57,HESSENBE:1;
then
A35: Q in Line(P1,P2) & Q in Line(P5,P4) by A34,COLLSP:11;
then
A36: Q in Line(P1,P2) /\ Line(P5,P4) by XBOOLE_0:def 4;
P1,P2,NP are_collinear by A33,A20,A21,ANPROJ_8:57,HESSENBE:1;
then
A37: NP in Line(P1,P2) by COLLSP:11;
P5,P4,NP are_collinear by A32,A22,A23,ANPROJ_8:57,HESSENBE:1;
then NP in Line(P5,P4) by COLLSP:11;
then NP in Line(P5,P4) /\ Line(P1,P2) by A37,XBOOLE_0:def 4;
then
A39: {Q,NP} c= Line(P1,P2) /\ Line(P5,P4) by A36,ZFMISC_1:32;
P4 <> P5
proof
assume P4 = P5;
then P4 in tangent P1 & P4 in tangent P2 by A9,XBOOLE_0:def 4;
then P4 in tangent P1 /\ absolute & P4 in tangent P2 /\absolute
by XBOOLE_0:def 4;
then P4 in {P1} & P4 in {P2} by Th22;
then P4 = P1 & P4 = P2 by TARSKI:def 1;
hence contradiction by A2;
end;
then Line(P1,P2) is LINE of real_projective_plane &
Line(P5,P4) is LINE of real_projective_plane
by A2,COLLSP:def 7;
then
A41: Line(P1,P2) = Line (P5,P4) or Line(P1,P2) misses Line (P5,P4) or
ex p being Element of real_projective_plane st
Line(P1,P2) /\ Line(P5,P4) = {p}
by COLLSP:21;
Line(P1,P2) <> Line(P5,P4)
proof
assume Line(P1,P2) = Line(P5,P4);
then P4 in Line(P1,P2) by COLLSP:10;
hence contradiction by A8,COLLSP:11,BKMODEL1:92;
end;
then consider p be Element of real_projective_plane such that
A42: Line(P1,P2) /\ Line(P5,P4) = {p} by A35,A41,XBOOLE_0:def 4;
Q = p & NP = p by A42,A39,ZFMISC_1:20;
hence thesis by A28,A20,A21,A2,COLLSP:8,BKMODEL1:69;
end;
thus ex P1,P2 being Element of absolute st
P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear &
homography(N).P1 = P2 & homography(N).P2 = P1 by A2,A3,A4,A20,A21;
end;
begin :: Main lemmas
theorem
for P,Q being Element of BK_model holds
ex h being Element of SubGroupK-isometry,
N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).P = Q &
homography(N).Q = P
proof
let P,Q be Element of BK_model;
per cases;
suppose
A1: P = Q;
reconsider N = 1.(F_Real,3) as invertible Matrix of 3,F_Real;
homography(N) in the set of all homography(N)
where N is invertible Matrix of 3,F_Real;
then reconsider h = homography(N) as Element of EnsHomography3
by ANPROJ_9:def 1;
h is_K-isometry by Th33;
then h in EnsK-isometry;
then reconsider h as Element of SubGroupK-isometry by Def05;
take h;
homography(N).P = Q & homography(N).Q = P by A1,ANPROJ_9:14;
hence thesis;
end;
suppose P <> Q;
then consider N be invertible Matrix of 3,F_Real such that
A2: (homography(N)).:absolute = absolute and
A3: (homography(N)). P = Q and
A4: (homography(N)).Q = P and
(ex P1,P2 being Element of absolute st P1 <> P2 &
P,Q,P1 are_collinear & P,Q,P2 are_collinear &
homography(N).P1 = P2 & homography(N).P2 = P1)
by Th45;
homography(N) in the set of all homography(N)
where N is invertible Matrix of 3,F_Real;
then reconsider h = homography(N) as Element of EnsHomography3
by ANPROJ_9:def 1;
h is_K-isometry by A2;
then h in EnsK-isometry;
then reconsider h as Element of SubGroupK-isometry by Def05;
take h;
thus thesis by A3,A4;
end;
end;
theorem
for P,Q,R,S,T,U being Element of BK_model st
ex h1,h2 being Element of SubGroupK-isometry,
N1,N2 being invertible Matrix of 3,F_Real st
h1 = homography(N1) & h2 = homography(N2) &
homography(N1).P = R & homography(N1).Q = S &
homography(N2).R = T & homography(N2).S = U holds
ex h3 being Element of SubGroupK-isometry,
N3 being invertible Matrix of 3,F_Real st
h3 = homography(N3) & homography(N3).P = T &
homography(N3).Q = U
proof
let P,Q,R,S,T,U be Element of BK_model;
assume ex h1,h2 be Element of SubGroupK-isometry,
N1,N2 be invertible Matrix of 3,F_Real st
h1 = homography(N1) & h2 = homography(N2) &
homography(N1).P = R & homography(N1).Q = S &
homography(N2).R = T & homography(N2).S = U;
then consider h1,h2 be Element of SubGroupK-isometry,
N1,N2 be invertible Matrix of 3,F_Real such that
A1: h1 = homography(N1) & h2 = homography(N2) &
homography(N1).P = R & homography(N1).Q = S &
homography(N2).R = T & homography(N2).S = U;
reconsider N3 = N2 * N1 as invertible Matrix of 3,F_Real;
h2 * h1 = homography(N2 * N1) by A1,Th35;
then reconsider h3 = homography(N3) as Element of SubGroupK-isometry;
take h3;
homography(N3).P = T & homography(N3).Q = U by A1,ANPROJ_9:13;
hence thesis;
end;
theorem
for P,Q,R being Element of BK_model, h being Element of SubGroupK-isometry,
N being invertible Matrix of 3,F_Real st
h = homography(N) & homography(N).P = R & homography(N).Q = R holds
P = Q by ANPROJ_9:16;