:: Beltrami-Klein Model, {P}art {I}
:: 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 COLLSP, PRALG_1, NAT_1, TREES_1, MATRIX_0, MATRIX_6, FINSEQ_2,
COMPLEX1, REAL_1, XCMPLX_0, ANPROJ_1, PENCIL_1, MCART_1, EUCLID_5,
ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, EUCLID, FUNCT_1, INCSP_1, MATRIX_1,
NUMBERS, PRE_TOPC, RELAT_1, STRUCT_0, SUBSET_1, SUPINF_2, VECTSP_1,
XBOOLE_0, MESFUNC1, ANPROJ_8, ANPROJ_9, RLVECT_3, TARSKI, XXREAL_0,
PASCAL, INCPROJ, ANPROJ_2, ZFMISC_1, ANALOAF, SQUARE_1, JGRAPH_6, PROB_1,
METRIC_1, RVSUM_1, PROJPL_1, FINSEQ_1, QC_LANG1, RELAT_2, MATRIXR1,
MATRIXC1, MATRIX_3, MATRIXR2, FUNCT_3, CARD_3, TOPREALB, BKMODEL1;
notations XTUPLE_0, RELSET_1, ORDINAL1, XCMPLX_0, PRE_TOPC, RVSUM_1, TARSKI,
XBOOLE_0, RLVECT_1, COLLSP, EUCLID_5, PASCAL, XXREAL_0, INCPROJ,
DOMAIN_1, INCSP_1, ANPROJ_2, RLVECT_3, ANPROJ_9, SQUARE_1, XREAL_0,
JGRAPH_6, TOPREAL9, PROJPL_1, ZFMISC_1, SUBSET_1, NUMBERS, FUNCT_1,
FUNCT_2, FINSEQ_1, STRUCT_0, ALGSTR_0, VECTSP_1, FINSEQ_2, EUCLID,
ANPROJ_1, MATRIX_0, MATRIX_6, LAPLACE, ANPROJ_8, MATRIX_1, MATRIX_3,
MATRIXR1, MATRIXR2, MATRPROB, QUIN_1, COMPLEX1, TOPREALB;
constructors MATRIXR2, RANKNULL, FINSEQ_4, FVSUM_1, LAPLACE, MATRPROB,
MONOID_0, EUCLID_5, MATRIX13, ANPROJ_8, PASCAL, INCPROJ, ANPROJ_2,
RLVECT_3, ANPROJ_9, SQUARE_1, JGRAPH_6, TOPREAL9, BINOP_2, QUIN_1,
BORSUK_7, MATRIX_3;
registrations FUNCT_1, MEMBERED, FINSEQ_1, ORDINAL1, XXREAL_0, XBOOLE_0,
ANPROJ_1, STRUCT_0, VECTSP_1, REVROT_1, RELSET_1, XREAL_0, MONOID_0,
EUCLID, VALUED_0, MATRIX_6, ANPROJ_2, INCPROJ, ANPROJ_9, SQUARE_1,
XCMPLX_0, NUMBERS, MATRIX_0, QUIN_1, MATRIX_3;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions TARSKI;
equalities VECTSP_1, STRUCT_0, JGRAPH_6, SQUARE_1;
expansions TARSKI, STRUCT_0, XBOOLE_0, ZFMISC_1;
theorems XREAL_0, MATRIXR2, FINSEQ_3, EUCLID_8, MATRIX_6, MATRIXR1, MATRPROB,
XREAL_1, EUCLID_5, ANPROJ_1, ANPROJ_2, EUCLID, XCMPLX_1, RVSUM_1,
FINSEQ_1, MATRIX_3, FUNCT_1, FUNCT_2, ANPROJ_8, INCSP_1, INCPROJ,
ANPROJ_9, PASCAL, TARSKI, XBOOLE_0, SQUARE_1, COMPLEX1, TOPREAL9,
TOPGEN_5, EUCLID_2, COLLSP, MATRIX_0, FINSEQ_2, MATRIX13, ZFMISC_1,
ENUMSET1, XTUPLE_0, RELAT_1, MATRIX_9, MATRIX14, EUCLID_4, MATRIX_5,
QUIN_1, EUCLID_3, XXREAL_0, TOPREALB;
begin :: Preliminaries
reserve a,b,c,d,e,f for Real,
g for positive Real,
x,y for Complex,
S,T for Element of REAL 2,
u,v,w for Element of TOP-REAL 3;
theorem Th01:
for P1,P2,P3 being Element of ProjectiveSpace TOP-REAL 3 st
u is non zero & v is non zero & w is non zero &
P1 = Dir u & P2 = Dir v & P3 = Dir w holds
(P1,P2,P3 are_collinear iff |{u,v,w}| = 0)
proof
let P1,P2,P3 be Element of ProjectiveSpace TOP-REAL 3;
assume that
A1: u is non zero and
A2: v is non zero and
A3: w is non zero and
A4: P1 = Dir u and
A5: P2 = Dir v and
A6: P3 = Dir w;
hereby
assume P1,P2,P3 are_collinear;
then consider u9,v9,w9 be Element of TOP-REAL 3 such that
A7: P1 = Dir(u9) and
A8: P2 = Dir(v9) and
A9: P3 = Dir(w9) & u9 is not zero & v9 is not zero & w9 is not zero &
u9,v9,w9 are_LinDep by ANPROJ_2:23;
[ Dir u9,Dir v9,Dir w9 ] in the Collinearity of
ProjectiveSpace TOP-REAL 3 by A9,ANPROJ_1:25;
then u,v,w are_LinDep by A7,A8,A9,A1,A2,A3,A4,A5,A6,ANPROJ_1:25;
hence |{u,v,w}| = 0 by ANPROJ_8:43;
end;
thus thesis by A1,A2,A3,A4,A5,A6,ANPROJ_2:23,ANPROJ_8:43;
end;
Lem01:
a <> 0 & b <> 0 & a * d = b * c implies
ex e st e = d / b & e = c / a & c = e * a & d = e * b
proof
assume that
A1: a <> 0 and
A2: b <> 0 and
A3: a * d = b * c;
A4: c = (a * d) / b by A2,A3,XCMPLX_1:89
.= (d / b) * a by XCMPLX_1:74;
A5: d = (b * c) / a by A1,A3,XCMPLX_1:89
.= (c / a) * b by XCMPLX_1:74;
d / b = ((d / b) * a) / a by A1,XCMPLX_1:89
.= (b * c) / (b * a) by A3,XCMPLX_1:83
.= (b / b) / (a / c) by XCMPLX_1:84
.= 1 / (a / c) by A2,XCMPLX_1:60
.= c / a by XCMPLX_1:57;
hence thesis by A4,A5;
end;
Lem02:
a <> 0 & b = 0 & a * d = b * c implies
ex e st c = e * a & d = e * b
proof
assume that
A1: a <> 0 and
A2: b = 0 and
A3: a * d = b * c;
A4: c = (c / a) * a by A1,XCMPLX_1:87;
(c / a) * b = d by A1,A2,A3;
hence thesis by A4;
end;
theorem
(a <> 0 or b <> 0) & a * d = b * c implies
ex e st c = e * a & d = e * b
proof
assume that
A1: a <> 0 or b <> 0 and
A2: a * d = b * c;
per cases;
suppose
A3: a <> 0;
per cases;
suppose b = 0;
hence thesis by A1,A2,Lem02;
end;
suppose b <> 0;
then ex e st e = d / b & e = c / a & c = e * a & d = e * b
by A2,A3,Lem01;
hence thesis;
end;
end;
suppose
a = 0; then
ex e st d = e * b & c = e * a by A1,A2,Lem02;
hence thesis;
end;
end;
theorem
a^2 + b^2 = 1 & (c * a)^2 + (c * b)^2 = 1 implies c = 1 or c = -1
proof
assume that
A1: a^2 + b^2 = 1 and
A2: (c * a)^2 + (c * b)^2 = 1;
1 = (c * c) *(a^2 + b * b) by A2
.= c^2 by A1;
hence thesis by SQUARE_1:41;
end;
theorem
a * u + (-a) * u = 0.TOP-REAL 3
proof
a* u = |[ a * u`1,a * u`2 , a * u`3 ]| by EUCLID_5:7;
then a * u +(-a) * u = |[ a * u`1,a * u`2 , a * u`3 ]| +
|[ (-a) * u`1,(-a) * u`2 , (-a) * u`3 ]| by EUCLID_5:7
.= |[ a * u`1 + (-a) * u`1 ,a * u`2 + (-a) * u`2,
a * u`3 + (-a) *u`3 ]| by EUCLID_5:6
.= |[0,0,0]|;
hence thesis by EUCLID_5:4;
end;
theorem
0 <= a & c < 0 & delta(a,b,c) = 0 implies a = 0
proof
assume that
A1: 0 <= a and
A2: c < 0 and
A3: delta(a,b,c) = 0;
A4: b^2 - 4 * a * c = 0 by A3,QUIN_1:def 1;
0 <= b^2
proof
per cases;
suppose b = 0;
hence thesis;
end;
suppose 0 <> b;
hence thesis by SQUARE_1:12;
end;
end;
hence thesis by A1,A2,A4;
end;
theorem
Sum sqr (T - S) = Sum sqr (S - T)
proof
Sum (sqr (T - S)) = |. T - S .|^2 by TOPREAL9:5
.= |. S - T .|^2 by EUCLID:18;
hence thesis by TOPREAL9:5;
end;
theorem
a^2 + b^2 = 1 & c^2 + d^2 = 1 & c * a + d * b = 1 implies b * c = a * d
proof
assume that
A1: a^2 + b^2 = 1 and
A2: c^2 + d^2 = 1 and
A3: c * a + d * b = 1;
c^2 + d^2 = (c * a + d * b)^2 by A3,A2
.= c^2 * a^2 + 2 * (c * a) * (d * b) + d^2 * b^2;
then (1 - a^2) * c^2 + (1 - b^2) * d^2 - 2 * (c * a) * (d * b) = 0;
then (b * c)^2 + a^2 * d^2 - 2 * (c * a) * (d * b) = 0 by A1,SQUARE_1:9;
then ((b * c) - (a * d))^2 = 0;
then (b * c) - (a * d) = 0;
hence thesis;
end;
theorem
a^2 + b^2 = 1 & a = 0 implies b = 1 or b = -1
proof
assume that
A1: a^2 + b^2 = 1 and
A2: a = 0;
b^2 = 1^2 by A1,A2;
hence thesis by SQUARE_1:40;
end;
Lem03:
1 + a^2 <> 0
proof
assume
A1: 1 + a^2 = 0;
then a^2 = -1;
then a = 0 by SQUARE_1:12;
hence contradiction by A1;
end;
theorem Th07:
0 <= a^2
proof
per cases;
suppose a = 0;
hence thesis;
end;
suppose a <> 0;
hence thesis by SQUARE_1:12;
end;
end;
Lem04:
a^2 = 1 / b implies a = 1 / sqrt b or a = (-1) / sqrt b
proof
assume
A1: a^2 = 1 / b;
reconsider ib = 1/b as Real;
A2: 0 <= b by A1,Th07;
0 <= ib by A1,Th07;
then ib = (sqrt (1/b))^2 by SQUARE_1:def 2; then
A3: a = sqrt(1/b) or a = -sqrt(1/b) by A1,SQUARE_1:40;
- (sqrt 1)/ sqrt b = (-1) / sqrt b by XCMPLX_1:187;
hence thesis by A3,A2,SQUARE_1:30;
end;
theorem
(a * b)^2 + b^2 = 1 implies b = 1 / sqrt(1 + a^2) or
b = (-1) / sqrt(1 + a^2)
proof
assume a1: (a * b)^2 + b^2 = 1;
b^2 = (a^2 + 1) * b^2 / (a^2 + 1) by XCMPLX_1:89,Lem03
.= 1 / (a^2 + 1) by a1;
hence thesis by Lem04;
end;
Lem05:
for z being non zero Complex holds (1/z)^2 * z^2 = 1
proof
let z be non zero Complex;
(1/z)^2 * z^2 = (1/z) * ((1/z) * z) * z
.= (1/z) * 1 * z by XCMPLX_1:106
.= 1 by XCMPLX_1:106;
hence thesis;
end;
theorem
a <> 0 & b^2 = 1 + a * a implies
a * (1/b) * a * ((-1)/b) + (1/b) * ((-1)/b) = -1
proof
assume that
A1: a <> 0 and
A2: b^2 = 1 + a * a;
A3: b <> 0
proof
assume b = 0;
then a^2 = -1 by A2;
hence contradiction by A1,SQUARE_1:12;
end;
a * (1/b) * a * ((-1)/b) + (1/b) * ((-1)/b) = (1/b) * (((-1) * 1)/b)
* (a * a + 1)
.= (1/b) * ((-1) * (1/b))
* (a * a + 1) by XCMPLX_1:74
.= (-1) * ((1/b)^2 * b^2) by A2
.= (-1) * 1 by A3,Lem05;
hence thesis;
end;
theorem
a^2 * (1/(b^2)) = (a/b)^2
proof
a^2 * (1/(b^2)) = a * a * ((1/b) * (1/b)) by XCMPLX_1:102
.= a * (a * (1/b)) * (1/b)
.= a * ((a * 1)/b) * (1/b) by XCMPLX_1:74
.= (a/b) * (a *(1/b))
.= (a/b) * ((a * 1)/b) by XCMPLX_1:74
.= (a / b)^2;
hence thesis;
end;
theorem Th11:
a^2 + b^2 = 1 iff |[a,b]| in circle(0,0,1)
proof
hereby
assume
A1: a^2 + b^2 = 1;
reconsider p = |[a,b]| as Point of TOP-REAL 2;
|. p - |[0,0]| .| = 1
proof
|. p - |[0,0]| .|^2 = |. |[a - 0,b - 0]| .|^2 by EUCLID:62
.= 1 by A1,TOPGEN_5:9;
hence thesis by SQUARE_1:41;
end;
hence |[a,b]| in circle(0,0,1);
end;
assume
A2: |[a,b]| in circle(0,0,1);
thus a^2 + b^2 = |. |[a - 0,b - 0]| .|^2 by TOPGEN_5:9
.= |. |[a,b]| - |[0,0]| .|^2 by EUCLID:62
.= 1^2 by A2,TOPREAL9:43
.= 1;
end;
theorem Th12:
a^2 + b^2 = g^2 iff |[a,b]| in circle(0,0,g)
proof
hereby
assume
A1: a^2 + b^2 = g^2;
reconsider p = |[a,b]| as Point of TOP-REAL 2;
|. p - |[0,0]| .| = g
proof
A2: |. p - |[0,0]| .|^2 = |. |[a - 0,b - 0]| .|^2 by EUCLID:62
.= g^2 by A1,TOPGEN_5:9;
-g < 0;
hence thesis by A2,SQUARE_1:40;
end;
hence |[a,b]| in circle(0,0,g);
end;
assume
A3: |[a,b]| in circle(0,0,g);
thus a^2 + b^2 = |. |[a - 0,b - 0]| .|^2 by TOPGEN_5:9
.= |. |[a,b]| - |[0,0]| .|^2 by EUCLID:62
.= g^2 by A3,TOPREAL9:43;
end;
Lem06:
(a * b)^2 + (a * c)^2 = a^2 * (b^2 + c^2);
theorem Th13:
a <> 0 & -1 < a < 1 & b = (2 + sqrt delta(a * a,-2,1)) / (2 * a * a)
implies (1 + a * a) * b * b - 2 * b + 1 - b * b = 0
proof
assume that
A1: a <> 0 and
A2: -1 < a < 1 and
A3: b = (2 + sqrt delta(a * a,-2,1)) / (2 * a * a);
set x1 = (- (-2) - sqrt(delta(a * a,-2,1)))/(2 * (a * a)),
x2 = (- (-2) + sqrt(delta(a * a,-2,1)))/(2 * (a * a));
A4: 0 <= 1 - a^2
proof
a^2 * 1^2 <= 1 by A2,SQUARE_1:53;
then a^2 < 1 by A2,SQUARE_1:41,XXREAL_0:1;
then a^2 - a^2 < 1 - a^2 by XREAL_1:9;
hence thesis;
end;
delta(a * a,-2,1) >= 0
proof
delta(a * a,-2,1) = (-2)^2 - 4 * (a * a) * 1 by QUIN_1:def 1
.= 4 * (1 - a^2);
hence thesis by A4;
end; then
(a * a) * b^2 + (- 2) * b + 1 = (a * a) * (b - x1) * (x2 - x2)
by A3,A1,QUIN_1:16
.= 0;
hence thesis;
end;
Lem07:
-1 < a < 1 implies ex b st (1 + a * a) * b * b - 2 * b + 1 - b * b = 0
proof
assume
A1: -1 < a < 1;
per cases;
suppose
A2: a = 0;
set b = 1/2;
take b;
thus thesis by A2;
end;
suppose
A3: a <> 0;
take b = (2 + sqrt delta(a * a,-2,1)) / (2 * a * a);
thus thesis by A1,A3,Th13;
end;
end;
theorem
a^2 + b^2 = 1 & -1 < c < 1 implies ex d,e,f st
e = d * c * a + (1 - d) * (-b) &
f = d * c * b + (1 - d) * a & e^2 + f^2 = d^2
proof
assume that
A1: a^2 + b^2 = 1 and
A2: -1 < c < 1;
consider d be Real such that
A3: (1 + c * c) * d * d - 2 * d + 1 - d * d = 0 by A2,Lem07;
reconsider e = d * c * a + (1 - d) * (-b),
f = d * c * b + (1 - d) * a as Real;
e^2 + f^2 = (d * c)^2 * (a^2 + b^2) + (((1 - d) * b)^2 + ((1 - d) *a)^2)
.= (d * c)^2 * 1 + (1 - d)^2 * 1 by A1,Lem06
.= d^2 by A3;
hence thesis;
end;
theorem
a^2 + b^2 < 1 & c^2 + d^2 = 1 implies ((a + c)/2)^2 + ((b + d)/2)^2 < 1
proof
assume that
A1: a^2 + b^2 < 1 and
A2: c^2 + d^2 = 1;
reconsider u = |[a,b]|, v = |[c,d]| as Element of TOP-REAL 2;
A4: |. |( u,v )| .| <= |.u.| * |.v.| by EUCLID_2:51;
A5: |.u.|^2 < 1 & |.v.|^2 = 1 by A1,A2,TOPGEN_5:9;
A6: |(u,v)| = u`1 * v`1 + u`2 * v`2 by EUCLID_3:41
.= a * v`1 + u`2 * v`2 by EUCLID:52
.= a * v`1 + b * v`2 by EUCLID:52
.= a * c + b * v`2 by EUCLID:52
.= a * c + b * d by EUCLID:52;
|.u.|^2 * |.v.|^2 < 1 * 1 by A5;
then (|.u.| * |.v.|)^2 < 1;
then |.u.| * |.v.| < 1 by SQUARE_1:52; then
A7: |. |(u,v)| .| < 1 by XXREAL_0:2,A4;
|(u,v)| <= |. |(u,v)| .| by COMPLEX1:76;
then a * c + b * d < 1 by A6,A7,XXREAL_0:2;
then 2 * (a * c + b * d) < 2 * 1 by XREAL_1:68;
then (2 * a * c + 2 * b * d) + (a^2 + b^2) < 2 + 1 by A1,XREAL_1:8;
then (2 * a * c + 2 * b * d) + (a^2 + b^2) + 1 < 2 + 1 + 1 by XREAL_1:8;
then ((2 * a * c + 2 * b * d) + (a^2 + b^2) + 1)/4 < 4/4 by XREAL_1:74;
hence thesis by A2;
end;
Lem08:
0 <= a & c <= 0 implies 0 <= delta(a,b,c)
proof
assume that
A1: 0 <= a and
A2: c <= 0;
A3: delta(a,b,c) = b^2 - 4 * a * c by QUIN_1:def 1;
0 <= b * b
proof
per cases;
suppose b = 0;
hence thesis;
end;
suppose b <> 0;
then 0 < b^2 by SQUARE_1:12;
hence thesis;
end;
end;
hence thesis by A1,A2,A3;
end;
theorem
|. S .|^2 <= 1 implies 0 <= delta(Sum sqr (T - S),b,Sum sqr S - 1)
proof
assume |.S.|^2 <= 1;
then |.S.|^2 - 1 <= |.S.|^2 - |.S.|^2 by XREAL_1:10; then
A1: Sum sqr S - 1 <= 0 by TOPREAL9:5;
0 <= |.T-S.|^2;
then 0 <= Sum sqr (T - S) by TOPREAL9:5;
hence thesis by A1,Lem08;
end;
theorem
a^2 + b^2 is negative implies a = 0 & b = 0
proof
assume
A1: a^2 + b^2 is negative;
0 <= a * a & 0 <= b * b by XREAL_1:63;
hence thesis by A1;
end;
theorem
u = |[a,b,1]| & v = |[c,d,1]| & w = |[ (a + c)/2, (b + d)/2, 1]| implies
|{u,v,w}| = 0
proof
assume that
A1: u = |[a,b,1]| and
A2: v = |[c,d,1]| and
A3: w = |[ (a + c)/2, (b + d)/2, 1]|;
A4: u`1 = a & u`2 = b & u`3 = 1 & v`1 = c & v`2 = d & v`3 = 1 &
w`1 = (a + c)/2 & w`2 = (b + d)/2 & w`3 = 1 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 * 1 - 1 * d * ((a+c)/2) - a * 1 * (b + d)/2
+ b * 1 * (a + c)/2 - b * c * 1 + 1 * c * (b+d)/2 by A4;
hence thesis;
end;
theorem Th19:
a * |(u,v)| = |(a * u,v)| & a * |(u,v)| = |(u, a * v)|
proof
A1: a * u`1 = a * u.1 by EUCLID_5:def 1
.= (a * u).1 by RVSUM_1:44
.= (a * u)`1 by EUCLID_5:def 1;
A2: a * u`2 = a * u.2 by EUCLID_5:def 2
.= (a * u).2 by RVSUM_1:44
.= (a * u)`2 by EUCLID_5:def 2;
A3: a * u`3 = a * u.3 by EUCLID_5:def 3
.= (a * u).3 by RVSUM_1:44
.= (a * u)`3 by EUCLID_5:def 3;
thus a * |(u,v)| = a * (u`1*v`1 + u`2*v`2+u`3*v`3) by EUCLID_5:29
.= (a *u)`1 * v`1 + (a*u)`2 * v`2 + (a*u)`3 * v`3
by A1,A2,A3
.= |(a * u,v)| by EUCLID_5:29;
A4: a * v`1 = a * v.1 by EUCLID_5:def 1
.= (a * v).1 by RVSUM_1:44
.= (a * v)`1 by EUCLID_5:def 1;
A5: a * v`2 = a * v.2 by EUCLID_5:def 2
.= (a * v).2 by RVSUM_1:44
.= (a * v)`2 by EUCLID_5:def 2;
A6: a * v`3 = a * v.3 by EUCLID_5:def 3
.= (a * v).3 by RVSUM_1:44
.= (a * v)`3 by EUCLID_5:def 3;
thus a * |(u,v)| = a * (u`1*v`1 + u`2*v`2+u`3*v`3) by EUCLID_5:29
.= u`1 * (a * v)`1 + u`2 * (a * v)`2 + u`3 * (a * v)`3
by A4,A5,A6
.= |(u,a * v)| by EUCLID_5:29;
end;
reserve a,b,c for Element of F_Real,
M,N for Matrix of 3,F_Real;
theorem
M = symmetric_3(0,0,0,0,0,0) implies Det M = 0.F_Real
proof
assume
A1: M = symmetric_3(0,0,0,0,0,0);
reconsider z = 0 as Element of F_Real;
M = <* <* z,z,z *>,
<* z,z,z *>,
<* z,z,z *> *> by A1,PASCAL:def 3;
then Det M = z * z * z - z * z * z - z * z * z + z * z * z
- z * z * z + z * z * z by MATRIX_9:46;
hence thesis;
end;
Lem09:
for a11,a12,a13,a21,a22,a23,a31,a32,a33,
b11,b12,b13,b21,b22,b23,b31,b32,b33 being Element of F_Real
for A,B being Matrix of 3,F_Real st
A = <* <* a11,a12,a13 *>,
<* a21,a22,a23 *>,
<* a31,a32,a33 *> *> &
B = <* <* b11,b12,b13 *>,
<* b21,b22,b23 *>,
<* b31,b32,b33 *> *>
holds
(A * B)*(1,1) = a11 * b11 + a12 * b21 + a13 * b31 &
(A * B)*(1,2) = a11 * b12 + a12 * b22 + a13 * b32 &
(A * B)*(1,3) = a11 * b13 + a12 * b23 + a13 * b33 &
(A * B)*(2,1) = a21 * b11 + a22 * b21 + a23 * b31 &
(A * B)*(2,2) = a21 * b12 + a22 * b22 + a23 * b32 &
(A * B)*(2,3) = a21 * b13 + a22 * b23 + a23 * b33 &
(A * B)*(3,1) = a31 * b11 + a32 * b21 + a33 * b31 &
(A * B)*(3,2) = a31 * b12 + a32 * b22 + a33 * b32 &
(A * B)*(3,3) = a31 * b13 + a32 * b23 + a33 * b33
proof
let a11,a12,a13,a21,a22,a23,a31,a32,a33,
b11,b12,b13,b21,b22,b23,b31,b32,b33 be Element of F_Real;
let A,B be Matrix of 3,F_Real;
assume that
A1: A = <* <* a11,a12,a13 *>,
<* a21,a22,a23 *>,
<* a31,a32,a33 *> *> and
A2: B = <* <* b11,b12,b13 *>,
<* b21,b22,b23 *>,
<* b31,b32,b33 *> *>;
A3: A * B = <* <* a11 * b11 + a12 * b21 + a13 * b31,
a11 * b12 + a12 * b22 + a13 * b32,
a11 * b13 + a12 * b23 + a13 * b33 *>,
<* a21 * b11 + a22 * b21 + a23 * b31,
a21 * b12 + a22 * b22 + a23 * b32,
a21 * b13 + a22 * b23 + a23 * b33 *>,
<* a31 * b11 + a32 * b21 + a33 * b31,
a31 * b12 + a32 * b22 + a33 * b32,
a31 * b13 + a32 * b23 + a33 * b33 *> *>
by A1,A2,ANPROJ_9:6;
reconsider C = A * B as Matrix of 3,F_Real;
C = <* <* C*(1,1), C*(1,2), C*(1,3) *>,
<* C*(2,1), C*(2,2), C*(2,3) *>,
<* C*(3,1), C*(3,2), C*(3,3) *> *> by MATRIXR2:37;
hence thesis by A3,PASCAL:2;
end;
theorem
N = <* <* a,0,0 *>,
<* 0,b,0 *>,
<* 0,0,c *> *> implies
(M@ * (N * M))*(1,1) = a * (M*(1,1)) * (M*(1,1))
+ b * (M*(2,1)) * (M*(2,1)) + c * (M*(3,1)) * (M*(3,1)) &
(M@ * (N * M))*(1,2) = a * (M*(1,1)) * (M*(1,2))
+ b * (M*(2,1)) * (M*(2,2)) + c * (M*(3,1)) * (M*(3,2)) &
(M@ * (N * M))*(1,3) = a * (M*(1,1)) * (M*(1,3))
+ b * (M*(2,1)) * (M*(2,3)) + c * (M*(3,1)) * (M*(3,3)) &
(M@ * (N * M))*(2,1) = a * (M*(1,2)) * (M*(1,1))
+ b * (M*(2,2)) * (M*(2,1)) + c * (M*(3,2)) * (M*(3,1)) &
(M@ * (N * M))*(2,2) = a * (M*(1,2)) * (M*(1,2))
+ b * (M*(2,2)) * (M*(2,2)) + c * (M*(3,2)) * (M*(3,2)) &
(M@ * (N * M))*(2,3) = a * (M*(1,2)) * (M*(1,3))
+ b * (M*(2,2)) * (M*(2,3)) + c * (M*(3,2)) * (M*(3,3)) &
(M@ * (N * M))*(3,1) = a * (M*(1,3)) * (M*(1,1))
+ b * (M*(2,3)) * (M*(2,1)) + c * (M*(3,3)) * (M*(3,1)) &
(M@ * (N * M))*(3,2) = a * (M*(1,3)) * (M*(1,2))
+ b * (M*(2,3)) * (M*(2,2)) + c * (M*(3,3)) * (M*(3,2)) &
(M@ * (N * M))*(3,3) = a * (M*(1,3)) * (M*(1,3))
+ b * (M*(2,3)) * (M*(2,3)) + c * (M*(3,3)) * (M*(3,3))
proof
assume
A1: N = <* <* a,0,0 *>,
<* 0,b,0 *>,
<* 0,0,c *> *>;
reconsider a11 = a, a12 = 0, a13 = 0,
a21 = 0, a22 = b, a23 = 0,
a31 = 0, a32 = 0, a33 = c,
b11 = M*(1,1), b12 = M*(1,2), b13 = M*(1,3),
b21 = M*(2,1), b22 = M*(2,2), b23 = M*(2,3),
b31 = M*(3,1), b32 = M*(3,2), b33 = M*(3,3)
as Element of F_Real;
A2: M = <* <* b11,b12,b13 *>,
<* b21,b22,b23 *>,
<* b31,b32,b33 *> *> by MATRIXR2:37; then
A3: (N * M)*(1,1) = a11 * b11 + a12 * b21 + a13 * b31 &
(N * M)*(1,2) = a11 * b12 + a12 * b22 + a13 * b32 &
(N * M)*(1,3) = a11 * b13 + a12 * b23 + a13 * b33 &
(N * M)*(2,1) = a21 * b11 + a22 * b21 + a23 * b31 &
(N * M)*(2,2) = a21 * b12 + a22 * b22 + a23 * b32 &
(N * M)*(2,3) = a21 * b13 + a22 * b23 + a23 * b33 &
(N * M)*(3,1) = a31 * b11 + a32 * b21 + a33 * b31 &
(N * M)*(3,2) = a31 * b12 + a32 * b22 + a33 * b32 &
(N * M)*(3,3) = a31 * b13 + a32 * b23 + a33 * b33 by A1,Lem09;
reconsider c11 = a * b11, c12 = a * b12, c13 = a * b13,
c21 = b * b21, c22 = b * b22, c23 = b * b23,
c31 = c * b31, c32 = c * b32, c33 = c * b33
as Element of F_Real;
A4: N * M = <* <* c11, c12, c13 *>,
<* c21, c22, c23 *>,
<* c31, c32, c33 *> *> by A3,MATRIXR2:37;
M@ = <* <* b11,b21,b31 *>,
<* b12,b22,b32 *>,
<* b13,b23,b33 *> *> by A2,ANPROJ_8:22; then
(M@ * (N * M))*(1,1) = b11 * (a * b11) + b21 * (b * b21)
+ b31 * (c * b31) &
(M@ * (N * M))*(1,2) = b11 * (a * b12) + b21 * (b * b22)
+ b31 * (c * b32) &
(M@ * (N * M))*(1,3) = b11 * (a * b13) + b21 * (b * b23)
+ b31 * (c * b33) &
(M@ * (N * M))*(2,1) = b12 * (a * b11) + b22 * (b * b21)
+ b32 * (c * b31) &
(M@ * (N * M))*(2,2) = b12 * (a * b12) + b22 * (b * b22)
+ b32 * (c * b32) &
(M@ * (N * M))*(2,3) = b12 * (a * b13) + b22 * (b * b23)
+ b32 * (c * b33) &
(M@ * (N * M))*(3,1) = b13 * (a * b11) + b23 * (b * b21)
+ b33 * (c * b31) &
(M@ * (N * M))*(3,2) = b13 * (a * b12) + b23 * (b * b22)
+ b33 * (c * b32) &
(M@ * (N * M))*(3,3) = b13 * (a * b13) + b23 * (b * b23)
+ b33 * (c * b33) by A4,Lem09;
hence thesis;
end;
theorem
for m,n being Nat
for M being Matrix of m,F_Real
for N being Matrix of m,n,F_Real st m > 0 holds
M * N is Matrix of m,n,F_Real
proof
let m,n be Nat;
let M be Matrix of m,F_Real;
let N be Matrix of m,n,F_Real;
assume
A1: m > 0;
len N = m & width N = n by A1,MATRIX_0:23;
then width M = len N by A1,MATRIX_0:23;
then len(M * N) = len M & width(M * N) = width N by MATRIX_3:def 4;
then len(M * N) = m & width(M * N) = n by A1,MATRIX_0:23;
hence thesis by A1,MATRIX_0:20;
end;
reserve D for non empty set;
reserve d1,d2,d3 for Element of D;
reserve A for Matrix of 1,3,D;
reserve B for Matrix of 3,1,D;
theorem
for M being Matrix of 1,D holds M@ = M
proof
let M be Matrix of 1,D;
A1: M = <* <* M*(1,1) *> *> by MATRIX13:20;
Indices M = [: {1},{1} :] by MATRIX_0:24,FINSEQ_1:2;
then [1,1] in Indices M by ZFMISC_1:28;
then (M@)*(1,1) = M*(1,1) by MATRIX_0:def 6;
hence thesis by A1,MATRIX13:20;
end;
theorem Th23:
(A@) is (3,1)-size
proof
width A = 3 & len A = 1 by MATRIX_0:23; then
A1: len (A@) = 3 & width (A@) = 1 by MATRIX_0:29;
then consider s1 be FinSequence such that
A2: s1 in rng (A@) and
A3: len s1 = 1 by MATRIX_0:def 3;
consider n0 be Nat such that
A4: for x be object st x in rng (A@) holds ex s be FinSequence st s = x &
len s = n0 by MATRIX_0:def 1;
consider s be FinSequence such that
A5: s = s1 and
A6: len s = n0 by A2,A4;
for p be FinSequence of D st p in rng (A@) holds len p = 1
proof
let p be FinSequence of D;
assume
A7: p in rng (A@);
consider s be FinSequence such that
A8: s = p and
A9: len s = n0 by A7,A4;
thus thesis by A3,A5,A6,A8,A9;
end;
hence thesis by A1,MATRIX_0:def 2;
end;
theorem Th24:
<* <* d1,d2,d3 *> *> is Matrix of 1,3,D
proof
A1: <* d1,d2,d3 *> is FinSequence of D by FINSEQ_2:14;
len <* d1,d2,d3 *> = 3 by FINSEQ_1:45;
hence thesis by A1,MATRIX_0:11;
end;
theorem Th25:
<* <* d1 *> ,<* d2 *> ,<* d3 *> *> is Matrix of 3,1,D
proof
reconsider p = <* d1 *>, q = <* d2 *>, r = <* d3 *> as FinSequence of D;
len p = 1 & len q = 1 & len r = 1 by FINSEQ_1:40;
hence thesis by MATRIXR2:34;
end;
theorem Th26:
A = <* <* A*(1,1), A*(1,2), A*(1,3) *> *>
proof
reconsider B = <* <* A*(1,1), A*(1,2), A*(1,3) *> *> as Matrix of 1,3,D
by Th24;
A1: len A=1 & width A=3 by MATRIX_0:23;
A2: for i,j being Nat st [i,j] in Indices A holds A*(i,j) = B*(i,j)
proof
let i,j be Nat;
A3: Indices B=[: Seg 1,Seg 3 :] by MATRIX_0:23;
A4: Indices A=[: Seg 1,Seg 3 :] by MATRIX_0:23;
assume
A5: [i,j] in Indices A;
then i in {1} by A4,ZFMISC_1:87,FINSEQ_1:2; then
A6: i = 1 by TARSKI:def 1;
j in {1,2,3} by A4,A5,ZFMISC_1:87,FINSEQ_3:1;
then per cases by A6,ENUMSET1:def 1;
suppose
A7: [i,j] = [1,1];
then consider p be FinSequence of D such that
A8: p = B.1 and
A9: B*(1,1) = p.1 by A3,A4,A5,MATRIX_0:def 5;
i= 1 & j = 1 by A7,XTUPLE_0:1;
hence thesis by A8,A9;
end;
suppose
A11: [i,j] = [1,2];
then consider p being FinSequence of D such that
A12: p = B.1 and
A13: B*(1,2) = p.2 by A3,A4,A5,MATRIX_0:def 5;
i = 1 & j = 2 by A11,XTUPLE_0:1;
hence thesis by A12,A13;
end;
suppose
A15: [i,j] = [1,3];
then consider p being FinSequence of D such that
A16: p = B.1 and
A17: B*(1,3) = p.3 by A3,A4,A5,MATRIX_0:def 5;
i = 1 & j = 3 by A15,XTUPLE_0:1;
hence thesis by A16,A17;
end;
end;
len B = 1 & width B = 3 by MATRIX_0:23;
hence thesis by A1,A2,MATRIX_0:21;
end;
theorem Th27:
B = <* <* B*(1,1) *> , <* B*(2,1) *>, <* B*(3,1) *> *>
proof
reconsider C = <* <* B*(1,1) *> , <* B*(2,1)*> , <* B*(3,1) *> *> as
Matrix of 3,1,D by Th25;
A1: len B = 3 & width B = 1 by MATRIX_0:23;
A2: for i,j being Nat st [i,j] in Indices B holds B*(i,j) = C*(i,j)
proof
let i,j be Nat;
A3: Indices C = [: Seg 3,Seg 1 :] by MATRIX_0:23;
A4: Indices B = [: Seg 3,Seg 1 :] by MATRIX_0:23;
assume
A5: [i,j] in Indices B;
then i in Seg 3 & j in Seg 1 by A4,ZFMISC_1:87;
then (i = 1 or i = 2 or i = 3) & j = 1
by FINSEQ_1:2,FINSEQ_3:1,ENUMSET1:def 1,TARSKI:def 1;
then per cases;
suppose
A6: [i,j] = [1,1];
then consider p being FinSequence of D such that
A7: p = C.1 and
A8: C*(1,1) = p.1 by A3,A4,A5,MATRIX_0:def 5;
i= 1 & j = 1 by A6,XTUPLE_0:1;
hence thesis by A7,A8;
end;
suppose
A10: [i,j] = [2,1];
then consider p being FinSequence of D such that
A11: p = C.2 and
A12: C*(2,1) = p.1 by A3,A4,A5,MATRIX_0:def 5;
i = 2 & j = 1 by A10,XTUPLE_0:1;
hence thesis by A11,A12;
end;
suppose
A14: [i,j] = [3,1];
then consider p being FinSequence of D such that
A15: p = C.3 and
A16: C*(3,1) = p.1 by A3,A4,A5,MATRIX_0:def 5;
i = 3 & j = 1 by A14,XTUPLE_0:1;
hence thesis by A15,A16;
end;
end;
len C = 3 & width C = 1 by MATRIX_0:23;
hence thesis by A1,A2,MATRIX_0:21;
end;
theorem
A@ = <* <* A*(1,1) *>, <* A*(1,2) *>, <* A*(1,3) *> *>
proof
A1: A@ is Matrix of 3,1,D by Th23;
[1,1] in Indices A & [1,2] in Indices A & [1,3] in Indices A
by MATRIX_0:31;
then (A@)*(1,1) = A*(1,1) & (A@)*(2,1) = A*(1,2) & (A@)*(3,1) = A*(1,3)
by MATRIX_0:def 6;
hence thesis by A1,Th27;
end;
theorem
ex d1,d2,d3 st A = <* <* d1,d2,d3 *> *>
proof
A = <* <* A*(1,1), A*(1,2), A*(1,3) *> *> by Th26;
hence thesis;
end;
theorem
for p being FinSequence of 1-tuples_on REAL st len p = 3 holds
ColVec2Mx M2F p = p
proof
let p be FinSequence of 1-tuples_on REAL;
assume
A1: len p = 3;
then
A2: M2F p = <* (p.1).1,(p.2).1,(p.3).1 *> by ANPROJ_8:def 2; then
A3: len (M2F p) = 3 by FINSEQ_1:45;
A4: len (M2F p) > 0 by A2,FINSEQ_1:45; then
A5: len(ColVec2Mx M2F p) = len (M2F p) by MATRIXR1:def 9
.= 3 by A2,FINSEQ_1:45;
width (ColVec2Mx M2F p) = 1 & ColVec2Mx M2F p is Matrix of REAL
by A4,MATRIXR1:def 9; then
A6: ColVec2Mx M2F p is Matrix of 3,1,F_Real by A5,MATRIX_0:20;
set A = ColVec2Mx M2F p;
A = <* <* A*(1,1) *> , <* A*(2,1) *>, <* A*(3,1) *> *> by A6,Th27;
then
A7: A.1 = <* A*(1,1) *> & A.2 = <* A*(2,1) *> & A.3 = <* A*(3,1) *>;
dom M2F p = Seg 3 by A3,FINSEQ_1:def 3;
then 1 in dom M2F p & 2 in dom M2F p & 3 in dom M2F p by FINSEQ_1:1;
then A.1 = <* (M2F p).1 *> & A.2 = <* (M2F p).2 *> &
A.3 = <* (M2F p).3 *> by A4,MATRIXR1:def 9;
then A = <* <* (M2F p).1 *> , <* (M2F p).2 *>, <* (M2F p).3 *> *>
by A6,Th27,A7
.= F2M (M2F p) by A3,ANPROJ_8:def 1
.= p by A1,ANPROJ_8:85;
hence thesis;
end;
theorem Th30:
for M being Matrix of 3,F_Real
for MR being Matrix of 3,REAL
for v being Element of TOP-REAL 3
for uf being FinSequence of F_Real
for ufr being FinSequence of REAL
for p being FinSequence of (1-tuples_on REAL)
st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M
holds v = MR * ufr
proof
let M be Matrix of 3,F_Real;
let MR be Matrix of 3,REAL;
let v be Element of TOP-REAL 3;
let uf be FinSequence of F_Real;
let ufr be FinSequence of REAL;
let p be FinSequence of (1-tuples_on REAL);
assume that
A1: p = M * uf and
A2: v = M2F p and
A3: len uf = 3 and
A4: uf = ufr and
A5: MR = M;
consider a,b,c,d,e,f,g,h,i be Element of F_Real such that
A6: M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *> by PASCAL:3;
uf is Element of REAL 3 by A3,EUCLID_8:2;
then uf in REAL 3;
then uf in TOP-REAL 3 by EUCLID:22;
then consider t1,t2,t3 be Real such that
A7: uf = <* t1,t2,t3 *> by EUCLID_5:1;
reconsider x = t1, y = t2, z = t3 as Element of F_Real by XREAL_0:def 1;
v = <* a * x + b * y + c * z ,
d * x + e * y + f * z ,
g * x + h * y + i * z *> by PASCAL:8,A1,A2,A6,A7;
hence thesis by A7,A4,A5,A6,PASCAL:9;
end;
theorem Th31:
for N being Matrix of 3,REAL for uf being FinSequence of REAL st
uf = 0.TOP-REAL 3 holds N * uf = 0.TOP-REAL 3
proof
let N be Matrix of 3,REAL;
let uf be FinSequence of REAL;
assume
A1: uf = 0.TOP-REAL 3;
reconsider M = N as Matrix of 3,F_Real;
consider n1,n2,n3,n4,n5,n6,n7,n8,n9 be Element of F_Real such that
A2: M = <* <* n1,n2,n3 *>,
<* n4,n5,n6 *>,
<* n7,n8,n9 *> *> by PASCAL:3;
reconsider r1 =n1,r2 = n2, r3 = n3,
r4 = n4, r5 = n5, r6 = n6,
r7 = n7, r8 = n8, r9 = n9 as Element of REAL;
reconsider z = 0.TOP-REAL 3 as Element of TOP-REAL 3;
reconsider p = <* 0,0,0 *> as FinSequence of REAL by EUCLID:24,EUCLID_5:4;
reconsider z1 = z`1, z2 = z`2, z3 = z`3 as Element of REAL
by XREAL_0:def 1;
z = <* 0,0,0 *> & z = <* z1,z2,z3 *> by EUCLID_5:3,4; then
A3: z1 = 0 & z2 = 0 & z3 = 0 by FINSEQ_1:78;
|[z`1,z`2,z`3]| = p by EUCLID_5:3,4;
then N * uf = <* r1 * z1 + r2 * z2 + r3 * z3 ,
r4 * z1 + r5 * z2 + r6 * z3 ,
r7 * z1 + r8 * z2 + r9 * z3 *>
by A2,A1,EUCLID_5:4,PASCAL:9
.= 0.TOP-REAL 3 by A3,EUCLID_5:4;
hence thesis;
end;
theorem Th32:
for N being Matrix of 3,REAL
for uf being FinSequence of REAL
for u being Element of TOP-REAL 3
st N is invertible & u = uf & u is non zero
holds N * uf <> 0.TOP-REAL 3
proof
let N be Matrix of 3,REAL;
let uf be FinSequence of REAL;
let u be Element of TOP-REAL 3;
assume
A1: N is invertible & u = uf & u is non zero;
then dom uf = Seg 3 by FINSEQ_1:89; then
A2: len uf = 3 by FINSEQ_1:def 3;
assume
A3: N * uf = 0.TOP-REAL 3;
A4: (Inv N) * N = 1_Rmatrix(3) & (Inv N) * N = 1_Rmatrix(3)
by A1,MATRIXR2:def 6;
width N = 3 & len N = 3 & width Inv(N) = 3 by MATRIX_0:24;
then Inv(N) * (N * uf) = (Inv(N) * N) * uf by A2,MATRIXR2:59
.= uf by A4,A2,MATRIXR2:86;
hence contradiction by A3,A1,Th31;
end;
theorem
for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL
for P,Q being Element of ProjectiveSpace TOP-REAL 3
for u,v being non zero Element of TOP-REAL 3
for vfr,ufr being FinSequence of REAL
st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds
homography(N).P = Q
proof
let N be invertible Matrix of 3,F_Real;
let NR be Matrix of 3,REAL;
let P,Q be Element of ProjectiveSpace TOP-REAL 3;
let u,v be non zero Element of TOP-REAL 3;
let vfr,ufr be FinSequence of REAL;
assume
A1: P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr;
consider u1,v1 being Element of TOP-REAL 3,
u1f being FinSequence of F_Real,
p1 being FinSequence of 1-tuples_on REAL such that
A2: P = Dir u1 & u1 is not zero & u1 = u1f & p1 = N * u1f & v1 = M2F p1 &
v1 is not zero & (homography(N)).P = Dir v1 by ANPROJ_8:def 4;
reconsider u1fr = u1f as FinSequence of REAL;
u1 in TOP-REAL 3;
then u1 in REAL 3 by EUCLID:22; then
A3: len u1fr = 3 by A2,EUCLID_8:50; then
A4: v1 = NR * u1fr by A1,A2,Th30;
are_Prop u,u1 by A1,A2,ANPROJ_1:22;
then consider a be Real such that
A5: a <> 0 and
A6: u = a * u1 by ANPROJ_1:1;
A7: width NR = 3 by MATRIX_0:23;
A8: width NR = len u1fr & len u1fr > 0 by A3,MATRIX_0:23;
A9: len NR = 3 by MATRIX_0:24;
u in TOP-REAL 3;
then u in REAL 3 by EUCLID:22;
then width NR = len ufr & len ufr > 0 by A7,A1,EUCLID_8:50;
then len (NR * ufr) = 3 & len (NR * u1fr) = 3
by A9,A3,MATRIX_0:23,MATRIXR1:61;
then NR * ufr is Element of REAL 3 & NR * u1fr is Element of REAL 3
by EUCLID_8:2;
then reconsider w1 = NR * ufr,w2 = NR * u1fr as Element of TOP-REAL 3
by EUCLID:22;
w1 = a * w2 by A8,A1,A2,A6,MATRIXR1:59;
then are_Prop w1,w2 by A5,ANPROJ_1:1;
hence thesis by A1,A2,A4,ANPROJ_1:22;
end;
theorem Th33:
for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL
for P,Q being Element of ProjectiveSpace TOP-REAL 3
for u,v being non zero Element of TOP-REAL 3
for vfr,ufr being FinSequence of REAL
for a being non zero Real
st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR &
NR * ufr = a * vfr holds homography(N).P = Q
proof
let N be invertible Matrix of 3,F_Real;
let NR be Matrix of 3,REAL;
let P,Q be Element of ProjectiveSpace TOP-REAL 3;
let u,v be non zero Element of TOP-REAL 3;
let vfr,ufr be FinSequence of REAL;
let a be non zero Real;
assume
A1: P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = a * vfr;
A2: NR is invertible by A1,ANPROJ_8:18;
consider u1,v1 be Element of TOP-REAL 3,
u1f be FinSequence of F_Real,
p1 be FinSequence of 1-tuples_on REAL such that
A3: P = Dir u1 & u1 is not zero & u1 = u1f & p1 = N * u1f & v1 = M2F p1 &
v1 is not zero & (homography(N)).P = Dir v1 by ANPROJ_8:def 4;
reconsider u1fr = u1f as FinSequence of REAL;
u1 in TOP-REAL 3; then
A4: u1 in REAL 3 by EUCLID:22; then
A5: len u1fr = 3 by A3,EUCLID_8:50; then
A6: v1 = NR * u1fr by A1,A3,Th30;
are_Prop u,u1 by A1,A3,ANPROJ_1:22;
then consider b be Real such that
A7: b <> 0 and
A8: u = b * u1 by ANPROJ_1:1;
A9: width NR = 3 by MATRIX_0:23; then
A10: width NR = len u1fr & len u1fr > 0 by A4,A3,EUCLID_8:50;
A11: len NR = 3 by MATRIX_0:24;
u in TOP-REAL 3;
then u in REAL 3 by EUCLID:22;
then len ufr = 3 by A1,EUCLID_8:50;
then len (NR * ufr) = 3 & len (NR * u1fr) = 3
by MATRIX_0:23,A11,A10,MATRIXR1:61;
then NR * ufr is Element of REAL 3 & NR * u1fr is Element of REAL 3
by EUCLID_8:2;
then reconsider w1 = NR * ufr,w2 = NR * u1fr as Element of TOP-REAL 3
by EUCLID:22;
A12: w1 is not zero & w2 is not zero by A1,A3,A2,Th32;
w1 = b * w2 by A1,A3,A8,A9,A5,MATRIXR1:59;
then are_Prop w1,w2 by A7,ANPROJ_1:1; then
A13: Dir w1 = Dir w2 by A12,ANPROJ_1:22;
v in TOP-REAL 3;
then v in REAL 3 by EUCLID:22;
then len vfr = 3 by A1,EUCLID_8:50;
then len (a * vfr) = 3 by RVSUM_1:117;
then a * vfr is Element of REAL 3 by EUCLID_8:2;
then reconsider avfr = a * vfr as Element of TOP-REAL 3 by EUCLID:22;
now
thus avfr is not zero
proof
assume avfr is zero;
then a * v = |[0,0,0]| by A1,EUCLID_5:4;
then |[ a * v`1,a * v`2, a * v`3 ]| = |[ 0,0,0 ]| by EUCLID_5:7;
then v`1 = 0 & v`2 = 0 & v`3 = 0 by FINSEQ_1:78;
hence contradiction by EUCLID_5:3,4;
end;
thus v is not zero;
a <> 0 & a * v = avfr by A1;
hence are_Prop avfr,v by ANPROJ_1:1;
end;
hence thesis by A1,A3,A6,A13,ANPROJ_1:22;
end;
theorem Th34:
for p being FinSequence of REAL
for M being Matrix of 3,REAL st len p = 3
holds |( a * p, M * (b * p) )| = a * b * |(p, M * p)|
proof
let p be FinSequence of REAL;
let M be Matrix of 3,REAL;
assume
A1: len p = 3;
A2: width M = 3 & len M = 3 by MATRIX_0:23;
A3: len (b * p) = 3 by A1,RVSUM_1:117;
A4: p is Element of REAL 3 by A1,EUCLID_8:2;
A5: p * M = Line((LineVec2Mx p) * M,1) by MATRIXR1:def 12;
A6: width (MXR2MXF LineVec2Mx p) = width LineVec2Mx p by MATRIXR1:def 1
.= len p by MATRIXR1:def 10
.= len MXR2MXF M by A1,MATRIX_0:23;
(LineVec2Mx p) * M = MXF2MXR ((MXR2MXF LineVec2Mx p) * MXR2MXF M)
by MATRIXR1:def 6
.= ((MXR2MXF LineVec2Mx p) * MXR2MXF M)
by MATRIXR1:def 2;
then width ((LineVec2Mx p) * M) = width (MXR2MXF M) by A6,MATRIX_3:def 4
.= width M by MATRIXR1:def 1;
then len Line((LineVec2Mx p)*M,1) = width M by MATRIX_0:def 7;
then
A7: p * M is Element of REAL 3 by A5,MATRIX_0:23,EUCLID_8:2;
len (b * p) > 0 by A1,RVSUM_1:117; then
A8: len ColVec2Mx (b * p) = len (b * p) by MATRIXR1:def 9
.= 3 by A1,RVSUM_1:117;
A9: width MXR2MXF M = 3 by MATRIX_0:23
.= len MXR2MXF (ColVec2Mx (b * p)) by A8,MATRIXR1:def 1;
len (M * (b * p)) = len (Col(M * (ColVec2Mx (b * p)),1)) by MATRIXR1:def 11
.= len (M * (ColVec2Mx (b * p))) by MATRIX_0:def 8
.= len (MXF2MXR (MXR2MXF M * MXR2MXF (ColVec2Mx (b * p))))
by MATRIXR1:def 6
.= len (MXR2MXF M * MXR2MXF (ColVec2Mx (b * p)))
by MATRIXR1:def 2
.= len (MXR2MXF M) by A9,MATRIX_3:def 4
.= 3 by MATRIX_0:23;
then M * (b * p) is Element of REAL 3 by EUCLID_8:2;
then |( a * p, M * (b * p) )| = a * |( M * (b * p), p )| by A4,EUCLID_4:21
.= a * |( p * M, b * p)|
by MATRPROB:47,A2,A3,A1
.= a * ( b * |(p , p * M)| )
by EUCLID_4:21,A4,A7
.= (a * b) * |( p * M, p)|
.= (a * b) * |( M * p, p )|
by A2,A1,MATRPROB:47;
hence thesis;
end;
theorem Th35:
for p being FinSequence of REAL
for M being Matrix of 3,REAL st len p = 3 holds
SumAll QuadraticForm (a * p,M,b * p) = a * b * SumAll QuadraticForm(p,M,p)
proof
let p be FinSequence of REAL;
let M be Matrix of 3,REAL;
assume
A1: len p = 3;
A2: len M = 3 & width M = 3 by MATRIX_0:23; then
A3: len (a * p) = len M by A1,RVSUM_1:117;
len (b * p) = width M & len (b * p) > 0 by A1,A2,RVSUM_1:117; then
A4: SumAll QuadraticForm (a * p,M,b * p) = |( a * p, M * (b * p) )|
by A3,MATRPROB:44;
len p = len M & len p = width M & len p > 0 by A1,MATRIX_0:23;
then SumAll QuadraticForm(p,M,p) = |( p, M * p )| by MATRPROB:44;
hence thesis by A4,A1,Th34;
end;
theorem Th36:
for a,b being Real holds |[a,b,1]| is non zero by EUCLID_5:4,FINSEQ_1:78;
theorem
for P being Element of TOP-REAL 2,Q being Element of TOP-REAL 2,r being
Real holds P in Sphere(Q,r) iff P in circle(Q.1,Q.2,r)
proof
let P be Element of TOP-REAL 2,
Q be Element of TOP-REAL 2,
r be Real;
hereby
assume P in Sphere(Q,r);
then P in Sphere(|[Q`1,Q`2]|,r) by EUCLID:53;
then P in Sphere(|[Q.1,Q`2]|,r) by EUCLID:def 9;
then P in Sphere(|[Q.1,Q.2]|,r) by EUCLID:def 10;
hence P in circle(Q.1,Q.2,r) by TOPREAL9:52;
end;
assume P in circle(Q.1,Q.2,r);
then P in Sphere(|[Q.1,Q.2]|,r) by TOPREAL9:52;
then P in Sphere(|[Q`1,Q.2]|,r) by EUCLID:def 9;
then P in Sphere(|[Q`1,Q`2]|,r) by EUCLID:def 10;
hence thesis by EUCLID:53;
end;
reserve u,v for non zero Element of TOP-REAL 3;
theorem Th37:
Dir u = Dir v & u.3 = v.3 & v.3 <> 0 implies u = v
proof
assume that
A1: Dir u = Dir v and
A2: u.3 = v.3 and
A3: v.3 <> 0;
are_Prop u,v by A1,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A4: u = a * v by ANPROJ_1:1;
reconsider b = 1 - a, c = v.3 as Real;
A5: |[u`1,u`2,u`3]| = a * v by A4,EUCLID_5:3
.= |[ a * v`1,a*v`2,a*v`3]| by EUCLID_5:7;
v.3 = u`3 by A2,EUCLID_5:def 3
.= a*v`3 by A5,FINSEQ_1:78
.= a * v.3 by EUCLID_5:def 3;
then (1 - a) * v.3 = 0 & c = v.3;
then b = 0 by A3;
then u = |[ 1 * v`1,1 * v`2, 1 * v`3]| by A4,EUCLID_5:7
.= v by EUCLID_5:3;
hence thesis;
end;
definition
func Dir101 -> Point of ProjectiveSpace TOP-REAL 3 equals Dir |[ 1,0,1 ]|;
coherence
proof
reconsider u = |[1,0,1]| as Element of TOP-REAL 3;
u is not zero by EUCLID_5:4,FINSEQ_1:78;
hence thesis by ANPROJ_1:26;
end;
end;
definition
func Dirm101 -> Point of ProjectiveSpace TOP-REAL 3 equals
Dir |[-1,0,1]|;
coherence
proof
reconsider u = |[-1,0,1]| as Element of TOP-REAL 3;
u is not zero by EUCLID_5:4,FINSEQ_1:78;
hence thesis by ANPROJ_1:26;
end;
end;
definition
func Dir011 -> Point of ProjectiveSpace TOP-REAL 3 equals
Dir |[0,1,1]|;
coherence
proof
reconsider u = |[0,1,1]| as Element of TOP-REAL 3;
u is not zero by EUCLID_5:4,FINSEQ_1:78;
hence thesis by ANPROJ_1:26;
end;
end;
theorem
not Dir101,Dirm101,Dir011 are_collinear &
not Dir101,Dirm101,Dir010 are_collinear &
not Dir101,Dir011,Dir010 are_collinear &
not Dirm101,Dir011,Dir010 are_collinear
proof
thus not Dir101,Dirm101,Dir011 are_collinear
proof
assume
A1: Dir101,Dirm101,Dir011 are_collinear;
set p = |[1,0,1]|, q = |[-1,0,1]|, r = |[0,1,1]|;
A2: p`1 = 1 & p`2 = 0 & p`3 = 1 & q`1 = -1 & q`2 = 0 & q`3 = 1 &
r`1 = 0 & r`2 = 1 & r`3 = 1 by EUCLID_5:2;
p is non zero & q is non zero & r is non zero by EUCLID_5:4,FINSEQ_1:78;
then 0 = |{p,q,r}| by A1,Th01
.= 1 * 0 * 1 - 1 * 0 * 0 - 1 * 1 * 1 + 0 * 1 * 0
- 0 * (-1) * 1 + 1 * (-1) * 1 by A2,ANPROJ_8:27
.= -2;
hence contradiction;
end;
thus not Dir101,Dirm101,Dir010 are_collinear
proof
assume
A3: Dir101,Dirm101,Dir010 are_collinear;
set p = |[1,0,1]|, q = |[-1,0,1]|, r = |[0,1,0]|;
A4: p`1 = 1 & p`2 = 0 & p`3 = 1 & q`1 = -1 & q`2 = 0 & q`3 = 1 &
r`1 = 0 & r`2 = 1 & r`3 = 0 by EUCLID_5:2;
p is non zero & q is non zero & r is non zero by EUCLID_5:4,FINSEQ_1:78;
then 0 = |{p,q,r}| by A3,ANPROJ_9:def 6,Th01
.= 1 * 0 * 0 - 1 * 0 * 0 - 1 * 1 * 1 + 0 * 1 * 0
- 0 * (-1) * 0 + 1 * (-1) * 1 by A4,ANPROJ_8:27
.= -2;
hence contradiction;
end;
thus not Dir101,Dir011,Dir010 are_collinear
proof
assume
A5: Dir101,Dir011,Dir010 are_collinear;
set p = |[1,0,1]|, q = |[0,1,1]|, r = |[0,1,0]|;
A6: p`1 = 1 & p`2 = 0 & p`3 = 1 & q`1 = 0 & q`2 = 1 & q`3 = 1 &
r`1 = 0 & r`2 = 1 & r`3 = 0 by EUCLID_5:2;
p is non zero & q is non zero & r is non zero by EUCLID_5:4,FINSEQ_1:78;
then 0 = |{p,q,r}| by A5,ANPROJ_9:def 6,Th01
.= p`1 * q`2 * r`3 - p`3*q`2*r`1 - p`1*q`3*r`2 + p`2*q`3*r`1 -
p`2*q`1*r`3 + p`3*q`1*r`2 by ANPROJ_8:27
.= -1 by A6;
hence contradiction;
end;
thus not Dirm101,Dir011,Dir010 are_collinear
proof
assume
A7: Dirm101,Dir011,Dir010 are_collinear;
set p = |[-1,0,1]|, q = |[0,1,1]|, r = |[0,1,0]|;
A8: p`1 = -1 & p`2 = 0 & p`3 = 1 & q`1 = 0 & q`2 = 1 & q`3 = 1 &
r`1 = 0 & r`2 = 1 & r`3 = 0 by EUCLID_5:2;
p is non zero & q is non zero & r is non zero by EUCLID_5:4,FINSEQ_1:78;
then 0 = |{p,q,r}| by A7,ANPROJ_9:def 6,Th01
.= p`1 * q`2 * r`3 - p`3*q`2*r`1 - p`1*q`3*r`2 + p`2*q`3*r`1 -
p`2*q`1*r`3 + p`3*q`1*r`2 by ANPROJ_8:27
.= 1 by A8;
hence contradiction;
end;
end;
theorem
symmetric_3(1,1,1,0,0,0) = 1.(F_Real,3) by PASCAL:def 3,ANPROJ_9:1;
theorem Th39:
for r,a,b,c,d,e,f,g,h,i being Element of F_Real
for M being Matrix of 3,F_Real st
M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *>
holds
r * M = <* <* r * a,r * b,r * c *>,
<* r * d,r * e,r * f *>,
<* r * g,r * h,r * i *> *>
proof
let r,a,b,c,d,e,f,g,h,i be Element of F_Real;
let M be Matrix of 3,F_Real;
assume
A1: M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *>;
A3: Indices M = [: Seg 3, Seg 3:] by MATRIX_0:23;
reconsider b11 = (r * M)*(1,1), b12 = (r * M)*(1,2), b13 = (r * M)*(1,3),
b21 = (r * M)*(2,1), b22 = (r * M)*(2,2), b23 = (r * M)*(2,3),
b31 = (r * M)*(3,1), b32 = (r * M)*(3,2), b33 = (r * M)*(3,3)
as Element of F_Real;
M = <* <* M*(1,1), M*(1,2), M*(1,3) *>,
<* M*(2,1), M*(2,2), M*(2,3) *>,
<* M*(3,1), M*(3,2), M*(3,3) *> *> by MATRIXR2:37;
then
A4: a = M*(1,1) & b = M*(1,2) & c = M*(1,3) &
d = M*(2,1) & e = M*(2,2)& f = M*(2,3) &
g = M*(3,1) & h = M*(3,2) & i = M*(3,3) by A1,PASCAL:2;
b11 = r * (M*(1,1)) & b12 = r * (M*(1,2)) & b13 = r * (M*(1,3)) &
b21 = r * (M*(2,1)) & b22 = r * (M*(2,2)) & b23 = r * (M*(2,3)) &
b31 = r * (M*(3,1)) & b32 = r * (M*(3,2)) & b33 = r * (M*(3,3))
by A3,ANPROJ_8:1,MATRIX_3:def 5;
hence thesis by A4,MATRIXR2:37;
end;
theorem Th40:
for a being Real
for ra2 being Element of F_Real st ra2 = a * a holds
symmetric_3(a,a,-a,0,0,0) * symmetric_3(a,a,-a,0,0,0) = ra2 * 1.(F_Real,3)
proof
let a be Real;
let ra2 be Element of F_Real;
assume
A1: ra2 = a * a;
reconsider zone = 1,z1 = 0, z2 = a,z3 = -a as Element of F_Real
by XREAL_0:def 1;
symmetric_3(a,a,-a,0,0,0) = <* <* z2, z1, z1 *>,
<* z1, z2, z1 *>,
<* z1, z1, z3 *> *> by PASCAL:def 3;
then
symmetric_3(a,a,-a,0,0,0) * symmetric_3(a,a,-a,0,0,0)
= <* <* z2 * z2 + z1 * z1 + z1 * z1, z2 * z1 + z1 * z2 + z1 * z1,
z2 * z1 + z1 * z1 + z1 * z3 *>,
<* z1 * z2 + z2 * z1 + z1 * z1, z1 * z1 + z2 * z2 + z1 * z1,
z1 * z1 + z2 * z1 + z1 * z3 *>,
<* z1 * z2 + z1 * z1 + z3 * z1, z1 * z1 + z1 * z2 + z3 * z1,
z1 * z1 + z1 * z1 + z3 * z3 *> *> by ANPROJ_9:6
.= <* <* ra2 * zone,ra2 * z1,ra2 * z1 *>,
<* ra2 * z1,ra2 * zone,ra2 * z1 *>,
<* ra2 * z1,ra2 * z1, ra2 * zone *> *> by A1
.= ra2 * 1.(F_Real,3) by Th39,ANPROJ_9:1;
hence thesis;
end;
theorem Th41:
for a being non zero Real holds
symmetric_3(a,a,-a,0,0,0) * symmetric_3(1/a,1/a,-1/a,0,0,0) = 1.(F_Real,3)
proof
let a be non zero Real;
reconsider z1 = 0, z2 = a,z3 = -a as Element of F_Real by XREAL_0:def 1;
A1: symmetric_3(a,a,-a,0,0,0) = <* <* z2, z1, z1 *>,
<* z1, z2, z1 *>,
<* z1, z1, z3 *> *> by PASCAL:def 3;
A2: z2 * (1/z2) = 1 & z3 * (1/z3) = 1 by XCMPLX_1:106;
reconsider y1 = z1,y2 = 1/z2, y3 = 1/z3 as Element of F_Real
by XREAL_0:def 1;
A3: symmetric_3(y2,y2,y3,y1,y1,y1) = <* <* 1/z2, z1, z1 *>,
<* z1, 1/z2, z1 *>,
<* z1, z1, 1/z3 *> *>
by PASCAL:def 3;
symmetric_3(a,a,-a,0,0,0) * symmetric_3(1/a,1/a,-1/a,0,0,0)
= symmetric_3(z2,z2,z3,z1,z1,z1) * symmetric_3(y2,y2,y3,y1,y1,y1)
by XCMPLX_1:188
.= <* <* z2 * y2 + z1 * y1 + z1 * y1,
z2 * y1 + z1 * y2 + z1 * y1,
z2 * y1 + z1 * y1 + z1 * y3 *>,
<* z1 * y2 + z2 * y1 + z1 * y1,
z1 * y1 + z2 * y2 + z1 * y1,
z1 * y1 + z2 * y1 + z1 * y3 *>,
<* z1 * y2 + z1 * y1 + z3 * y1,
z1 * y1 + z1 * y2 + z3 * y1,
z1 * y1 + z1 * y1 + z3 * y3 *> *> by A1,A3,ANPROJ_9:6
.= <* <* 1,0,0 *>,
<* 0,1,0 *>,
<* 0,0,1 *> *> by A2;
hence thesis by ANPROJ_9:1;
end;
theorem Th42:
for a being non zero Real holds
symmetric_3(1/a,1/a,-1/a,0,0,0) * symmetric_3(a,a,-a,0,0,0) = 1.(F_Real,3)
proof
let a be non zero Real;
reconsider b = 1 / a as non zero Real;
1 / b = a by XCMPLX_1:56;
hence thesis by Th41;
end;
theorem Th43:
symmetric_3(1,1,-1,0,0,0) * symmetric_3(1,1,-1,0,0,0) = 1.(F_Real,3)
proof
reconsider a = 1 as non zero Real;
-1 / a = -1;
hence thesis by Th41;
end;
theorem
for a being non zero Real
for N being Matrix of 3,F_Real st N = symmetric_3(a,a,-a,0,0,0) holds
N is invertible
proof
let a be non zero Real;
let N be Matrix of 3,F_Real;
assume
A1: N = symmetric_3(a,a,-a,0,0,0);
symmetric_3(a,a,-a,0,0,0) * symmetric_3(1/a,1/a,-1/a,0,0,0)
= 1.(F_Real,3) &
symmetric_3(1/a,1/a,-1/a,0,0,0) * symmetric_3(a,a,-a,0,0,0)
= 1.(F_Real,3) by Th41,Th42;
hence thesis by A1,MATRIX_6:def 2,def 3;
end;
theorem Th44:
symmetric_3(1,1,-1,0,0,0) is invertible Matrix of 3,F_Real &
(symmetric_3(1,1,-1,0,0,0))~ = symmetric_3(1,1,-1,0,0,0)
proof
A1: symmetric_3(1,1,-1,0,0,0) is_reverse_of symmetric_3(1,1,-1,0,0,0)
by Th43,MATRIX_6:def 2;
thus symmetric_3(1,1,-1,0,0,0) is invertible Matrix of 3,F_Real
by Th43,MATRIX_6:def 2,MATRIX_6:def 3;
hence (symmetric_3(1,1,-1,0,0,0))~ = symmetric_3(1,1,-1,0,0,0)
by A1,MATRIX_6:def 4;
end;
theorem
for N being invertible Matrix of 3,F_Real
for N1 being Matrix of 3,F_Real
for M,NR being Matrix of 3,REAL st
M = symmetric_3(1,1,-1,0,0,0) &
N1 = M &
NR = MXF2MXR(N~) holds
(N@) * N1 * N = MXF2MXR((MXR2MXF(NR@))~) * M * MXF2MXR((MXR2MXF NR)~)
proof
let N be invertible Matrix of 3,F_Real;
let N1 be Matrix of 3,F_Real;
let M,NR be Matrix of 3,REAL;
assume that
A1: M = symmetric_3(1,1,-1,0,0,0) and
A2: N1 = M and
A3: NR = MXF2MXR(N~);
reconsider b = -1 as Element of F_Real by XREAL_0:def 1;
A4: 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 A4;
reconsider N1 as invertible Matrix of 3,F_Real by A1,A2,Th44;
reconsider M1 = (N@) * N1 * N as invertible Matrix of 3,F_Real;
reconsider N2 = N1 as Matrix of 3,REAL;
A6: MXF2MXR((MXR2MXF NR)~) = (MXR2MXF NR)~ by MATRIXR1:def 2
.= (N~)~ by A3,ANPROJ_8:16
.= N by MATRIX_6:16;
A7: MXF2MXR((MXR2MXF(NR@))~) = N@
proof
A8: MXF2MXR((MXR2MXF(NR@))~) = (MXR2MXF(NR@))~ by MATRIXR1:def 2;
MXR2MXF (NR@) = NR@ by MATRIXR1:def 1;
then MXF2MXR((MXR2MXF(NR@))~) = ((N~)@)~ by A8,A3,MATRIXR1:def 2
.= (N@)~~ by MATRIX_6:13;
hence thesis by MATRIX_6:16;
end;
(N@) * N1 = MXF2MXR((MXR2MXF(NR@))~) * N2 by A7,ANPROJ_8:17;
hence thesis by A2,A6,ANPROJ_8:17;
end;
theorem Th46:
for n being Nat for a being Element of F_Real
for ra being Real for A being Matrix of n,F_Real
for rA being Matrix of n,REAL st
a = ra & A = rA holds
a * A = ra * rA
proof
let n be Nat;
let a be Element of F_Real;
let ra be Real;
let A be Matrix of n,F_Real;
let rA be Matrix of n,REAL;
assume that
A1: a = ra and
A2: A = rA;
ra * rA = MXF2MXR( a * MXR2MXF rA) by A1,MATRIXR1:def 7
.= MXF2MXR( a * A) by A2,MATRIXR1:def 1;
hence thesis by MATRIXR1:def 2;
end;
theorem Th47:
for n being Nat
for a being Element of F_Real
for A,B being Matrix of n,F_Real st n > 0 holds
(a * A) * B = a * (A * B)
proof
let n be Nat;
let a be Element of F_Real;
let A,B be Matrix of n,F_Real;
assume
A1: n > 0;
A2: width A = n & len A = n & width B = n & len B = n by MATRIX_0:24;
reconsider ra = a as Real;
reconsider rA = A, rB = B as Matrix of n,REAL;
A3: rA * rB = A * B by ANPROJ_8:17;
a * A = ra * rA by Th46;
then (a * A) * B = (ra * rA) * rB by ANPROJ_8:17
.= ra * (rA * rB) by A2,A1,MATRIXR1:41
.= a * (A * B) by A3,Th46;
hence thesis;
end;
theorem Th48:
symmetric_3(a,a,-a,0,0,0) = a * (symmetric_3(1,1,-1,0,0,0))
proof
reconsider z0 = 0, z1 = 1, z2 = -1 as Element of F_Real by XREAL_0:def 1;
symmetric_3(1,1,-1,0,0,0) = <* <* z1,z0,z0 *>,
<* z0,z1,z0 *>,
<* z0,z0,z2 *> *> by PASCAL:def 3;
then a * (symmetric_3(1,1,-1,0,0,0)) = <* <* a * z1, a * z0 ,a * z0 *>,
<* a * z0,a * z1, a * z0 *>,
<* a * z0,a * z0,a * z2 *> *>
by Th39;
hence thesis by PASCAL:def 3;
end;
theorem Th49:
M = symmetric_3(a,a,-a,0,0,0) implies
M * M * M = (a * a * a) * symmetric_3(1,1,-1,0,0,0)
proof
assume
A1: M = symmetric_3(a,a,-a,0,0,0);
reconsider ra2 = a * a as Element of F_Real;
M * M * M = (ra2 * 1.(F_Real,3)) * M by A1,Th40
.= ra2 * (1.(F_Real,3) * M) by Th47
.= ra2 * M by MATRIX_3:18
.= ra2 * (a * symmetric_3(1,1,-1,0,0,0)) by A1,Th48
.= (a * a * a) * symmetric_3(1,1,-1,0,0,0) by MATRIX_5:11;
hence thesis;
end;
theorem Th50:
for n being Nat for a being Real
for M being Matrix of n,REAL for x being FinSequence of REAL st
n > 0 & len x = n holds M * (a * x) = (a * M) * x
proof
let n be Nat;
let a be Real;
let M be Matrix of n,REAL;
let x be FinSequence of REAL;
assume that
A1: n > 0 and
A2: len x = n;
width M = n & len M = n by MATRIX_0:24; then
A3: width M = len ColVec2Mx x & len M > 0 & len ColVec2Mx x > 0 &
width ColVec2Mx x > 0 by A1,A2,MATRIXR1:def 9;
(a * M) * x = Col((a * M) * ColVec2Mx x, 1) by MATRIXR1:def 11
.= Col( a * (M * ColVec2Mx x),1) by A3,MATRIXR1:41
.= Col( M * (a * ColVec2Mx x),1) by A3,MATRIXR1:40
.= Col( M * (ColVec2Mx (a * x)),1) by A1,A2,MATRIXR1:47
.= M * (a * x) by MATRIXR1:def 11;
hence thesis;
end;
theorem Th51:
for n being Nat
for a being Real
for M being Matrix of n,REAL
for x being FinSequence of REAL st n > 0 & len x = n holds
a * (M * x) = (a * M) * x
proof
let n be Nat;
let a be Real;
let M be Matrix of n,REAL;
let x be FinSequence of REAL;
assume that
A1: n > 0 and
A2: len x = n;
width M = n by MATRIX_0:24;
then M * (a * x) = a * (M * x) by A1,A2,MATRIXR1:59;
hence thesis by A1,A2,Th50;
end;
theorem Th52:
for n being Nat for N being Matrix of n,REAL st
N is invertible holds N@ is invertible & Inv(N@) = (Inv(N))@
proof
let n be Nat;
let N be Matrix of n,REAL;
assume
A1: N is invertible;
then (N * Inv(N))@ = (1_Rmatrix(n))@ by MATRIXR2:def 6
.= 1_Rmatrix(n) by MATRIXR2:64; then
A2: (Inv(N)@) * N@ = 1_Rmatrix(n) by MATRIXR2:30;
(Inv(N) * N)@ = (1_Rmatrix(n))@ by A1,MATRIXR2:def 6
.= 1_Rmatrix(n) by MATRIXR2:64; then
A3: (N@ * Inv(N)@) = 1_Rmatrix(n) by MATRIXR2:30; then
N@ is invertible by A2,MATRIXR2:def 5;
hence thesis by A2,A3,MATRIXR2:def 6;
end;
theorem Th53:
for ra being non zero Real
for N,O,M being Matrix of 3,3,REAL st N is invertible &
M = ra * O & M = N@ * O * N holds Inv(N)@ * O * Inv(N) = 1/ra * O
proof
let ra be non zero Real;
let N,O,M be Matrix of 3,3,REAL;
assume that
A1: N is invertible and
A3: M = ra * O and
A4: M = N@ * O * N;
reconsider NI = Inv(N), NIT = (Inv(N))@ as Matrix of 3,3,REAL;
A5: (Inv(N))@ = Inv(N@) & N@ is invertible by A1,Th52;
A6: len NI = 3 & width NI = 3 & width (O * N) = 3 & len (O * N) = 3
by MATRIX_0:24;
reconsider ira = 1/ra as Real;
reconsider NTON = N@ * O * N as Matrix of REAL;
A7: len NTON = 3 by MATRIX_0:24;
A8: width(NI@) = 3 by MATRIX_0:24;
O = 1 * O by MATRIXR1:32
.= (1/ra * ra) * O by XCMPLX_1:87
.= ira * (N@ * O * N) by A3,A4,MATRIXR2:11;
then NI@ * O * NI = ira * (NI@ * (N@ * O * N)) * NI by A8,A7,MATRIXR1:40
.= ira * (NIT * (N@ * (O * N))) * NI by MATRIXR2:27
.= ira * ((NIT * N@) * (O * N)) * NI by MATRIXR2:27
.= ira * (1_Rmatrix(3) * (O * N)) * NI
by A5,MATRIXR2:def 6
.= ira * (O * N) * NI by MATRIXR2:70
.= ira * (O * N * NI) by A6,MATRIXR1:41
.= ira * (O * (N * NI)) by MATRIXR2:27
.= ira * (O * 1_Rmatrix(3)) by A1,MATRIXR2:def 6
.= ira * O by MATRIXR2:71;
hence thesis;
end;
theorem Th54:
for ra being Real for M,N being Matrix of 3,F_Real
for MR,NR being Matrix of 3,REAL st MR = M & NR = N &
N is symmetric & MR = ra * NR holds M is symmetric
proof
let ra be Real;
let M,N be Matrix of 3,F_Real;
let MR,NR be Matrix of 3,REAL;
assume that
A1: MR = M & NR = N and
A2: N is symmetric and
A3: MR = ra * NR;
width NR > 0 by MATRIX_0:23;
then M@ = ra * NR@ by A1,A3,MATRIXR1:30
.= M by A1,A2,A3,MATRIX_6:def 5;
hence thesis by MATRIX_6:def 5;
end;
theorem Th55:
for ra being Real for O,M being Matrix of 3,REAL
st O = symmetric_3(1,1,-1,0,0,0) & M = ra * O holds
O * M = ra * 1_Rmatrix(3) & M * O = ra * 1_Rmatrix(3)
proof
let ra be Real;
let O,M be Matrix of 3,REAL;
assume that
A1: O = symmetric_3(1,1,-1,0,0,0) and
A2: M = ra * O;
1_Rmatrix(3) = MXF2MXR 1.(F_Real,3) by MATRIXR2:def 2; then
A3: MXR2MXF 1_Rmatrix(3) = 1.(F_Real,3) by ANPROJ_8:16;
A4: O * O = symmetric_3(1,1,-1,0,0,0) * symmetric_3(1,1,-1,0,0,0)
by A1,ANPROJ_8:17
.= 1_Rmatrix(3) by Th43,A3,MATRIXR1:def 1;
len O = 3 & width O = 3 by MATRIX_0:23;
hence thesis by A4,A2,MATRIXR1:40,41;
end;
theorem
for ra being Real for O,M being Matrix of 3,REAL
st O = symmetric_3(1,1,-1,0,0,0) & M = ra * O holds
(M@ * O)@ * O * (M@ * O) = ra^2 * O
proof
let ra be Real;
let O,M be Matrix of 3,REAL;
assume that
A1: O = symmetric_3(1,1,-1,0,0,0) and
A2: M = ra * O;
reconsider O1 = O as Matrix of 3,F_Real;
A3: O@ = O by A1,PASCAL:12,MATRIX_6:def 5;
reconsider MR = M as Matrix of 3,F_Real;
A4: MR is symmetric by Th54,A2,A1,PASCAL:12;
A5: (ra * 1_Rmatrix(3)) * O * (ra * 1_Rmatrix(3)) = (ra^2) * O
proof
reconsider z1 = 1,z2 = -1,z3 = 0 as Element of F_Real by XREAL_0:def 1;
A6: O = <* <* z1,z3,z3 *>,
<* z3,z1,z3 *>,
<* z3,z3,z2 *> *> by A1,PASCAL:def 3;
reconsider ea = ra as Element of F_Real by XREAL_0:def 1;
A7: ra * 1_Rmatrix(3) = MXF2MXR (ea * (MXR2MXF 1_Rmatrix(3)))
by MATRIXR1:def 7
.= MXF2MXR (ea * (MXR2MXF MXF2MXR 1.(F_Real,3)))
by MATRIXR2:def 2
.= MXF2MXR (ea * 1.(F_Real,3)) by ANPROJ_8:16
.= ea * (1.(F_Real,3)) by MATRIXR1:def 2
.= <* <* ea * z1 ,ea * z3 ,ea * z3 *> ,
<* ea * z3,ea * z1,ea * z3 *>,
<* ea * z3, ea * z3,ea * z1 *> *>
by ANPROJ_9:1,Th39
.= <* <* ea,z3,z3 *> ,<* z3,ea,z3 *>,<* z3,z3,ea *> *>;
then reconsider RA1R = ra * 1_Rmatrix(3) as Matrix of 3,F_Real
by ANPROJ_8:19;
reconsider ea2 = ra * ra as Element of F_Real by XREAL_0:def 1;
reconsider z4 = ea * z2 as Element of F_Real;
A8: RA1R * O1 = <* <* ea * z1 + z3 * z3 + z3 * z3,
ea * z3 + z3 * z1 + z3 * z3,
ea * z3 + z3 * z3 + z3 * z2 *>,
<* z3 * z1 + ea * z3 + z3 * z3,
z3 * z3 + ea * z1 + z3 * z3,
z3 * z3 + ea * z3 + z3 * z2 *>,
<* z3 * z1 + z3 * z3 + ea * z3,
z3 * z3 + z3 * z1 + ea * z3,
z3 * z3 + z3 * z3 + ea * z2 *> *> by A7,A6,ANPROJ_9:6
.= <* <* ea,z3,z3 *>,
<* z3,ea,z3 *>,
<* z3,z3,z4 *> *>;
A9: (RA1R * O1) * RA1R = <* <* ea * ea + z3 * z3 + z3 * z3,
ea * z3 + z3 * ea + z3 * z3,
ea * z3 + z3 * z3 + z3 * ea *>,
<* z3 * ea + ea * z3 + z3 * z3,
z3 * z3 + ea * ea + z3 * z3,
z3 * z3 + ea * z3 + z3 * ea *>,
<* z3 * ea + z3 * z3 + z4 * z3,
z3 * z3 + z3 * ea + z4 * z3,
z3 * z3 + z3 * z3 + z4 * ea *> *>
by A8,A7,ANPROJ_9:6
.= <* <* ea * ea,z3,z3 *>,
<* z3,ea * ea,z3 *>,
<* z3,z3,z4 * ea *> *>;
A10: (ra * 1_Rmatrix(3)) * O = RA1R * O1 by ANPROJ_8:17;
(ra^2) * O = MXF2MXR (ea2 * MXR2MXF O) by MATRIXR1:def 7
.= ea2 * MXR2MXF O by MATRIXR1:def 2
.= <* <* ea2 * z1,ea2 * z3,ea2 * z3 *>,
<* ea2 * z3,ea2 * z1,ea2 * z3 *>,
<* ea2 * z3,ea2 * z3,ea2 * z2 *> *>
by A6,Th39,MATRIXR1:def 1;
hence thesis by A10,A9,ANPROJ_8:17;
end;
(M@ * O)@ * O * (M@ * O) = (M * O)@ * O * (M@ * O) by A4,MATRIX_6:def 5
.= (M * O)@ * O * (M * O) by A4,MATRIX_6:def 5
.= (O@ * M@) * O * (M * O) by MATRIXR2:30
.= (O * M) * O * (M * O) by A3,A4,MATRIX_6:def 5
.= (ra * 1_Rmatrix(3)) * O * (M * O) by A1,A2,Th55
.= (ra^2) * O by A1,A2,A5,Th55;
hence thesis;
end;
theorem
for O,N being Matrix of 3,REAL holds
(N@ * O)@ * O * (N@ * O) = O@ * (N * O * N@) * O
proof
let O,N be Matrix of 3,REAL;
(N@ * O)@ * O * (N@ * O) = (O@ * N@@) * O * (N@ * O) by MATRIXR2:30
.= (O@ * N) * O * (N@ * O) by MATRIXR2:29
.= (O@ * (N * O)) * (N@ * O) by MATRIXR2:27
.= (O@ * ((N * O) * (N@ * O))) by MATRIXR2:27
.= O@ * (((N * O) * N@) * O) by MATRIXR2:27;
hence thesis by MATRIXR2:27;
end;
theorem
for NR,MR being Matrix of 3,REAL
for p1,p2,p3 being FinSequence of REAL st
p1 = <* 1,0,0 *> & p2 = <* 0,1,0 *> & p3 = <* 0,0,1 *> &
NR * p1 = MR * p1 & NR * p2 = MR * p2 & NR * p3 = MR * p3
holds NR = MR
proof
let NR,MR be Matrix of 3,REAL;
let p1,p2,p3 be FinSequence of REAL;
assume that
A1: p1 = <* 1,0,0 *> & p2 = <* 0,1,0 *> & p3 = <* 0,0,1 *> and
A2: NR * p1 = MR * p1 and
A3: NR * p2 = MR * p2 and
A4: NR * p3 = MR * p3;
reconsider N = NR, M = MR as Matrix of 3,F_Real;
consider n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real such that
A5: N = <* <* n11,n12,n13 *>,
<* n21,n22,n23 *>,
<* n31,n32,n33 *> *> by PASCAL:3;
consider m11,m12,m13,m21,m22,m23,m31,m32,m33 be Element of F_Real such that
A6: M = <* <* m11,m12,m13 *>,
<* m21,m22,m23 *>,
<* m31,m32,m33 *> *> by PASCAL:3;
reconsider rn11 = n11, rn12 = n12, rn13 = n13,
rn21 = n21, rn22 = n22, rn23 = n23,
rn31 = n31, rn32 = n32, rn33 = n33 as Element of REAL;
reconsider rm11 = m11, rm12 = m12, rm13 = m13,
rm21 = m21, rm22 = m22, rm23 = m23,
rm31 = m31, rm32 = m32, rm33 = m33 as Element of REAL;
|[1,0,0]| in TOP-REAL 3;
then reconsider q1 = <* 1,0,0 *> as FinSequence of REAL by EUCLID:24;
reconsider z1 = q1.1, z2 = q1.2, z3 = q1.3 as Element of REAL
by XREAL_0:def 1;
NR = <* <* rn11,rn12,rn13 *>,
<* rn21,rn22,rn23 *>,
<* rn31,rn32,rn33 *> *> & q1 = <* z1,z2,z3 *>
by A5;
then
A10: NR * q1 = <* rn11 * z1 + rn12 * z2 + rn13 * z3,
rn21 * z1 + rn22 * z2 + rn23 * z3,
rn31 * z1 + rn32 * z2 + rn33 * z3 *> by PASCAL:9
.= <* rn11,rn21,rn31 *>;
MR = <* <* rm11,rm12,rm13 *>,
<* rm21,rm22,rm23 *>,
<* rm31,rm32,rm33 *> *> & q1 = <* z1,z2,z3 *> by A6;
then MR * q1 = <* rm11 * z1 + rm12 * z2 + rm13 * z3,
rm21 * z1 + rm22 * z2 + rm23 * z3,
rm31 * z1 + rm32 * z2 + rm33 * z3 *> by PASCAL:9
.= <* rm11,rm21,rm31 *>;
then
A11: rn11 = rm11 & rn21 = rm21 & rn31 = rm31 by A10,A2,A1,FINSEQ_1:78;
|[0,1,0]| in TOP-REAL 3;
then reconsider q1 = <* 0,1,0 *> as FinSequence of REAL by EUCLID:24;
reconsider z1 = q1.1, z2 = q1.2, z3 = q1.3 as Element of REAL
by XREAL_0:def 1;
NR = <* <* rn11,rn12,rn13 *>,
<* rn21,rn22,rn23 *>,
<* rn31,rn32,rn33 *> *> & q1 = <* z1,z2,z3 *>
by A5;
then
A15: NR * q1 = <* rn11 * z1 + rn12 * z2 + rn13 * z3,
rn21 * z1 + rn22 * z2 + rn23 * z3,
rn31 * z1 + rn32 * z2 + rn33 * z3 *> by PASCAL:9
.= <* rn12,rn22,rn32 *>;
MR = <* <* rm11,rm12,rm13 *>,
<* rm21,rm22,rm23 *>,
<* rm31,rm32,rm33 *> *> & q1 = <* z1,z2,z3 *>
by A6;
then MR * q1 = <* rm11 * z1 + rm12 * z2 + rm13 * z3,
rm21 * z1 + rm22 * z2 + rm23 * z3,
rm31 * z1 + rm32 * z2 + rm33 * z3 *> by PASCAL:9
.= <* rm12,rm22,rm32 *>;
then
A16: rn12 = rm12 & rn22 = rm22 & rn32 = rm32 by A15,A3,A1,FINSEQ_1:78;
|[0,0,1]| in TOP-REAL 3;
then reconsider q1 = <* 0,0,1 *> as FinSequence of REAL by EUCLID:24;
reconsider z1 = q1.1, z2 = q1.2, z3 = q1.3 as Element of REAL
by XREAL_0:def 1;
NR = <* <* rn11,rn12,rn13 *>,
<* rn21,rn22,rn23 *>,
<* rn31,rn32,rn33 *> *> & q1 = <* z1,z2,z3 *>
by A5;
then
A20: NR * q1 = <* rn11 * z1 + rn12 * z2 + rn13 * z3,
rn21 * z1 + rn22 * z2 + rn23 * z3,
rn31 * z1 + rn32 * z2 + rn33 * z3 *> by PASCAL:9
.= <* rn13,rn23,rn33 *>;
MR = <* <* rm11,rm12,rm13 *>,
<* rm21,rm22,rm23 *>,
<* rm31,rm32,rm33 *> *> & q1 = <* z1,z2,z3 *>
by A6;
then MR * q1 = <* rm11 * z1 + rm12 * z2 + rm13 * z3,
rm21 * z1 + rm22 * z2 + rm23 * z3,
rm31 * z1 + rm32 * z2 + rm33 * z3 *> by PASCAL:9
.= <* rm13,rm23,rm33 *>;
then rn13 = rm13 & rn23 = rm23 & rn33 = rm33 by A20,A4,A1,FINSEQ_1:78;
hence thesis by A11,A16,A5,A6;
end;
theorem Th56:
for a being non zero Real
for u being Element of TOP-REAL 3 st a * u = 0.TOP-REAL 3
holds u is zero
proof
let a be non zero Real;
let u be Element of TOP-REAL 3;
assume a * u = 0.TOP-REAL 3;
then |[ a * u`1, a * u`2,a * u`3 ]| = |[0,0,0]| by EUCLID_5:4,7;
then u`1 = 0 & u`2 = 0 & u`3 = 0 by FINSEQ_1:78;
hence thesis by EUCLID_5:3,4;
end;
theorem Th57:
for u,v being non zero Element of TOP-REAL 3
for a,b being Real st (a <> 0 or b <> 0) & a * u + b * v = 0.TOP-REAL 3
holds are_Prop u,v
proof
let u,v be non zero Element of TOP-REAL 3;
let a,b be Real;
assume that
A1: a <> 0 or b <> 0 and
A2: a * u + b * v = 0.TOP-REAL 3;
reconsider n = 3 as Nat;
reconsider au = a * u, bv = b * v as Element of TOP-REAL 3;
consider c be Real such that
A3: c <> 0 and
A4: au = c * bv by A2,ANPROJ_1:1,13;
A5: a <> 0 & b <> 0
proof
assume a = 0 or b = 0;
then per cases;
suppose
A6: a = 0;
u in TOP-REAL 3;
then u in REAL 3 by EUCLID:22; then
A7: 0 * u = 0*n by EUCLID_4:3;
bv in TOP-REAL 3;
then bv in REAL 3 by EUCLID:22;
then 0*n + bv = bv by EUCLID_4:1;
hence contradiction by A1,A6,A2,A7,Th56;
end;
suppose
A8: b = 0;
v in TOP-REAL 3;
then v in REAL 3 by EUCLID:22; then
A9: 0 * v = 0*n by EUCLID_4:3;
au in TOP-REAL 3;
then au in REAL 3 by EUCLID:22;
then au + 0*n = au by EUCLID_4:1;
hence contradiction by A1,A8,A2,A9,Th56;
end;
end;
u = 1 * u by RVSUM_1:52
.= (1/a * a) * u by A5,XCMPLX_1:106
.= (1/a) * (c * (b * v)) by A4,RVSUM_1:49
.= ((1/a * c) * (b * v)) by RVSUM_1:49
.= (1/a * c * b) * v by RVSUM_1:49;
hence thesis by A3,A5,ANPROJ_1:1;
end;
theorem
for N being invertible Matrix of 3,F_Real
for P,Q,R being Point of ProjectiveSpace TOP-REAL 3 st P <> Q &
homography(N).P = Q & homography(N).Q = P & P,Q,R are_collinear holds
(homography(N)).((homography(N)).R) = R
proof
let N be invertible Matrix of 3,F_Real;
let P,Q,R be Point of ProjectiveSpace TOP-REAL 3;
assume that
A1: P <> Q and
A2: homography(N).P = Q and
A3: homography(N).Q = P and
A4: P,Q,R are_collinear;
reconsider NR = MXF2MXR N as Matrix of 3,REAL by MATRIXR1:def 2;
consider u1,v1 be Element of TOP-REAL 3,
u1f be FinSequence of F_Real,
p1 be FinSequence of 1-tuples_on REAL such that
A5: P = Dir u1 & u1 is not zero & u1 = u1f & p1 = N * u1f & v1 = M2F p1 &
v1 is not zero & (homography(N)).P = Dir v1 by ANPROJ_8:def 4;
consider u2,v2 be Element of TOP-REAL 3,
u2f be FinSequence of F_Real,
p2 be FinSequence of 1-tuples_on REAL such that
A6: Q = Dir u2 & u2 is not zero & u2 = u2f & p2 = N * u2f & v2 = M2F p2 &
v2 is not zero & (homography(N)).Q = Dir v2 by ANPROJ_8:def 4;
reconsider u1fr = u1f, u2fr = u2f as FinSequence of REAL;
u1 in TOP-REAL 3 & u2 in TOP-REAL 3; then
A7: u1 in REAL 3 & u2 in REAL 3 by EUCLID:22; then
A8: len u1 = 3 & len u2 = 3 by EUCLID_8:50;
consider u3 be Element of TOP-REAL 3 such that
A9: u3 is not zero and
A10: R = Dir u3 by ANPROJ_1:26;
reconsider uf3r = u3 as FinSequence of REAL by EUCLID:24;
A11: are_Prop v2,u1 & are_Prop v1,u2 by A2,A3,A5,A6,ANPROJ_1:22;
then consider l1 be Real such that
A12: l1 <> 0 and
A13: v2 = l1 * u1 by ANPROJ_1:1;
consider l2 be Real such that
A14: l2 <> 0 and
A15: v1 = l2 * u2 by A11,ANPROJ_1:1;
A16: width NR = 3 & len NR = 3 & len u2fr = 3 & len u1fr = 3
by A7,EUCLID_8:50,A5,A6,MATRIX_0:24;
A17: width NR = len u2fr & len u2fr > 0 & width NR = len u1fr &
len u1fr > 0 by A8,A5,A6,MATRIX_0:24;
reconsider l = l1 * l2 as non zero Real by A12,A14;
A18: (NR * NR) * u1fr = NR * (NR * u1fr) by A16,MATRIXR2:59
.= NR * (l2 * u2fr) by A5,A6,A8,MATRIXR1:def 2,Th30,A15
.= l2 * (NR * u2fr) by A17,MATRIXR2:53
.= l2 * (l1 * u1fr) by A5,A6,A8,MATRIXR1:def 2,Th30,A13
.= l * u1fr by RVSUM_1:49;
A19: (NR * NR) * u2fr = NR * (NR * u2fr) by A16,MATRIXR2:59
.= NR * (l1 * u1fr) by A5,A6,A8,MATRIXR1:def 2,Th30,A13
.= l1 * (NR * u1fr) by A17,MATRIXR2:53
.= l1 * (l2 * u2fr) by A5,A6,A8,MATRIXR1:def 2,Th30,A15
.= l * u2fr by RVSUM_1:49;
|{u1,u2,u3}| = 0 by A4,A5,A6,A9,A10,Th01;
then consider a,b,c be Real such that
A20: a * u1 + b * u2 + c * u3 = 0.(TOP-REAL 3) & ((a <> 0) or
(b <> 0) or (c <> 0)) by ANPROJ_8:42;
A21: c <> 0
proof
assume
A22: c = 0;
reconsider bu2 = b * u2 as Element of REAL 3 by EUCLID:22;
reconsider n = 3 as Nat;
u3 in TOP-REAL 3; then
u3 in REAL 3 by EUCLID:22;
then bu2 + 0 * u3 = bu2 + 0*n by EUCLID_4:3
.= bu2 by EUCLID_4:1;
then a * u1 + b * u2 = 0.TOP-REAL 3 by A20,A22,RVSUM_1:15;
then are_Prop u1,u2 by A20,A22,A5,A6,Th57;
hence contradiction by A1,A5,A6,ANPROJ_1:22;
end;
A23: a * u1 + b * u2 + c * u3 = c * u3 + a * u1 + b * u2 by RVSUM_1:15;
reconsider d = (-a)/c, e = (-b)/c as Real;
A24: u3 = d * u1 + e * u2 by A23,A20,A21,ANPROJ_8:12;
reconsider u4fr = d * u1 + e * u2 as FinSequence of REAL;
reconsider NRNR = NR * NR as Matrix of 3,REAL;
u3 in TOP-REAL 3;
then u3 in REAL 3 by EUCLID:22; then
A25: len u4fr = width NR & width NR = len NR & len u4fr > 0 & len NR > 0
by A16,A24,EUCLID_8:50;
A26: len u1fr = 3 & len u2fr = 3 & width NR = 3 & len NR = 3
by A5,A6,A7,EUCLID_8:50,MATRIX_0:24;
len (d * u1fr) = 3 & len (e * u2fr) = 3 by RVSUM_1:117,A5,A6,A8;
then
A27: len (d * u1fr) = len (e * u2fr) & width NR = len (d * u1fr) &
len (d * u1fr) > 0 & len NR > 0 by MATRIX_0:24;
len (NR * u1fr) = 3 & len (NR * u2fr) = 3 by A26,MATRIXR1:61;
then
A28: len (d * (NR * u1fr)) = 3 & len (e * (NR * u2fr)) = 3 & width NR = 3 &
len NR = 3 by MATRIX_0:24,RVSUM_1:117;
A29: width NR = len (NR * u1fr) & len (NR * u1fr) > 0 by A26,MATRIXR1:61;
A30: width NR = len (NR * u2fr) & len (NR * u2fr) > 0 by A26,MATRIXR1:61;
A31: (NR * NR) * uf3r = (NR * NR) * u4fr by A23,A20,A21,ANPROJ_8:12
.= NR * (NR * (d * u1fr + e * u2fr))
by A5,A6,A25,MATRIXR2:59
.= NR * (NR * (d * u1fr) + NR * (e * u2fr))
by MATRIXR1:57,A27
.= NR * (d * (NR * u1fr) + NR * (e * u2fr))
by MATRIXR1:59,A26
.= NR * (d * (NR * u1fr) + e * (NR * u2fr))
by MATRIXR1:59,A26
.= NR * (d * (NR * u1fr)) + NR * (e * (NR * u2fr))
by MATRIXR1:57,A28
.= d * (NR * (NR * u1fr)) + NR * (e * (NR * u2fr))
by MATRIXR1:59,A29
.= d * (NR * (NR * u1fr)) + e * (NR * (NR * u2fr))
by MATRIXR1:59,A30
.= d * ((NR * NR) * u1fr) + e * (NR * (NR * u2fr))
by A16,MATRIXR2:59
.= d * (l * u1fr) + e * ((NR * NR) * u2fr)
by A18,A16,MATRIXR2:59
.= (d * l) * u1fr + e * (l * u2fr) by A19,RVSUM_1:49
.= (d * l) * u1fr + (e * l) * u2fr by RVSUM_1:49
.= l * (d * u1fr) + (l * e) * u2fr by RVSUM_1:49
.= l * (d * u1fr) + l * (e * u2fr) by RVSUM_1:49
.= l * (d * u1 + e * u2) by A5,A6,RVSUM_1:51
.= l * uf3r by A23,A20,A21,ANPROJ_8:12;
N = NR by MATRIXR1:def 2;
then (homography(N * N)).R = R by A31,A9,A10,Th33,ANPROJ_8:17;
hence thesis by ANPROJ_9:13;
end;
theorem
for n being Nat
for u,v being Element of TOP-REAL n
for a,b being Real st
(1 - a) * u + (a * v) = (1 - b) * v + (b * u)
holds (1 - (a + b)) * u = (1 - (a + b)) * v
proof
let n be Nat;
let u,v be Element of TOP-REAL n;
let a,b be Real;
assume
A1: (1 - a) * u + (a * v) = (1 - b) * v + (b * u);
reconsider ru = u ,rv = v as Element of REAL n by EUCLID:22;
A2: (1 - a) * ru + a * rv - a * rv = (1 - a) * ru
proof
(1 - a) * ru in REAL n & a * rv in REAL n;
then reconsider t1 = (1 - a) * u,
t2 = a * v as Element of n-tuples_on REAL
by EUCLID:def 1;
(1 - a) * ru + a * rv - a * rv = t1 + t2 - t2
.= t1 by RVSUM_1:42;
hence thesis;
end;
A3: (1 - b) * rv - a * rv + b * ru - b * ru = (1 - b) * rv - a * rv
proof
reconsider t1 = (1 - b) * rv - a * rv,
t2 = b * ru as Element of n-tuples_on REAL by EUCLID:def 1;
(1 - b) * rv - a * rv + b * ru - b * ru = t1 + t2 - t2
.= t1 by RVSUM_1:42;
hence thesis;
end;
(1 - a) * ru = (1 - b) * rv + b * ru + -( a * rv) by A1,A2,RVSUM_1:31
.= ((1 - b) * rv + - (a * rv)) + (b * ru) by RVSUM_1:15;
then (1 - a) * ru - b * ru = (1 - b) * rv - a * rv by A3,RVSUM_1:31;
then (1 - a) * ru + - (b * ru) = (1 - b) * rv - a * rv by RVSUM_1:31
.= (1 - b) * rv + -(a * rv) by RVSUM_1:31;
then (1 - a) * ru + (-1) * (b * ru) = (1 - b) * rv + -(a * rv)
by RVSUM_1:54;
then (1 - a) * ru + ((-1) * b) * ru = (1 - b) * rv + -(a * rv)
by RVSUM_1:49;
then ((1 - a) + (-1) * b) * ru = (1 - b) * rv + -(a * rv) by RVSUM_1:50;
then (1 - a - b) * ru = (1 - b) * rv + ((-1) *(a * rv)) by RVSUM_1:54
.= (1 - b) * rv + ((-1) * a) * rv by RVSUM_1:49
.= ((1 - b) + (-1) * a) * rv by RVSUM_1:50;
hence thesis;
end;
theorem
ProjectiveSpace TOP-REAL 3 is proper by ANPROJ_8:57;
definition
func real_projective_plane -> non empty proper
CollProjectivePlane equals ProjectiveSpace TOP-REAL 3;
coherence by ANPROJ_8:57;
end;
reserve P,Q,R for POINT of IncProjSp_of real_projective_plane,
L for LINE of IncProjSp_of real_projective_plane,
p,q,r for Point of real_projective_plane;
theorem
for L being Element of ProjectiveLines real_projective_plane holds
ex p,q st p <> q & L = Line(p,q)
proof
let L be Element of ProjectiveLines real_projective_plane;
L in ProjectiveLines real_projective_plane;
then L in {B where B is Subset of real_projective_plane:
B is LINE of real_projective_plane} by INCPROJ:def 1;
then ex B be Subset of real_projective_plane st L = B &
B is LINE of real_projective_plane;
hence thesis by COLLSP:def 7;
end;
theorem Th60:
ex p,q st p <> q & L = Line(p,q)
proof
L in the Lines of IncProjSp_of real_projective_plane;
then L in ProjectiveLines real_projective_plane by INCPROJ:2;
then L in {B where B is Subset of real_projective_plane:
B is LINE of real_projective_plane} by INCPROJ:def 1;
then ex B be Subset of real_projective_plane st L = B &
B is LINE of real_projective_plane;
hence thesis by COLLSP:def 7;
end;
theorem Th61:
R = r & L = Line(p,q) implies (R on L iff p,q,r are_collinear)
proof
assume
A1: R = r & L = Line(p,q);
hereby
assume R on L;
then [R,L] in the Inc of IncProjSp_of real_projective_plane
by INCSP_1:def 1;
then [R,L] in Proj_Inc real_projective_plane by INCPROJ:2;
then R in the carrier of real_projective_plane &
L in ProjectiveLines real_projective_plane & ex Y be set
st L = Y & R in Y by INCPROJ:def 2;
hence p,q,r are_collinear by A1,COLLSP:11;
end;
assume
A2: p,q,r are_collinear;
now
R is Point of real_projective_plane by INCPROJ:3;
hence R in the carrier of real_projective_plane;
L is Element of ProjectiveLines real_projective_plane
by INCPROJ:1,INCPROJ:4;
hence L in ProjectiveLines real_projective_plane;
thus ex Y be set st L = Y & R in Y by A2,A1,COLLSP:11;
end;
then [R,L] in Proj_Inc real_projective_plane by INCPROJ:def 2;
then [R,L] in the Inc of IncProjSp_of real_projective_plane by INCPROJ:2;
hence R on L by INCSP_1:def 1;
end;
theorem Th62:
IncProjSp_of real_projective_plane is IncProjectivePlane
proof
IncProjSp_of real_projective_plane is 2-dimensional
proof
for M,N being LINE of IncProjSp_of real_projective_plane
ex q being POINT of IncProjSp_of real_projective_plane st
q on M & q on N
proof
let M,N be LINE of IncProjSp_of real_projective_plane;
consider p1,q1 be Point of real_projective_plane such that
p1 <> q1 and
A1: M = Line(p1,q1) by Th60;
consider p2,q2 be Point of real_projective_plane such that
p2 <> q2 and
A2: N = Line(p2,q2) by Th60;
consider q be Element of real_projective_plane such that
A3: p1,q1,q are_collinear and
A4: p2,q2,q are_collinear by ANPROJ_2:def 14;
reconsider Q = q as POINT of IncProjSp_of real_projective_plane
by INCPROJ:3;
take Q;
thus thesis by A1,A2,A3,A4,Th61;
end;
hence thesis by INCPROJ:def 9;
end;
hence thesis;
end;
theorem
for L1,L2 being LINE of real_projective_plane holds L1 meets L2
proof
let L1,L2 be LINE of real_projective_plane;
reconsider LI1 = L1,LI2 = L2 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 LI1 and
A2: R on LI2 by Th62,INCPROJ:def 9;
reconsider S = R as Element of real_projective_plane by INCPROJ:3;
S in LI1 & S in LI2 by A1,A2,INCPROJ:5;
hence thesis by XBOOLE_0:def 4;
end;
reserve u,v,w for non zero Element of TOP-REAL 3;
theorem
p = Dir u & q = Dir v & R = Dir w & L = Line(p,q) implies
(R on L iff |{u,v,w}| = 0)
proof
assume that
A1: p = Dir u and
A2: q = Dir v and
A3: R = Dir w and
A4: L = Line(p,q);
reconsider r = Dir w as Point of real_projective_plane by ANPROJ_1:26;
hereby
assume R on L;
then p,q,r are_collinear by A3,A4,Th61;
then consider u1,v1,w1 be Element of TOP-REAL 3 such that
A5: p = Dir u1 and
A6: q = Dir v1 and
A7: r = Dir w1 and
A8: u1 is non zero & v1 is non zero & w1 is non zero and
A9: u1 = v1 or u1 = w1 or v1 = w1 or
{u1,v1,w1} is linearly-dependent by ANPROJ_8:10;
u1,v1,w1 are_LinDep by A9,ANPROJ_8:9;
then |{u1,v1,w1}| = 0 by ANPROJ_8:43;
then |{u,v1,w1}| = 0 by A1,A5,A8,ANPROJ_8:58;
then |{u,v,w1}| = 0 by A2,A6,A8,ANPROJ_8:59;
hence |{u,v,w}| = 0 by A8,A7,ANPROJ_8:60;
end;
assume |{u,v,w}| = 0;
then u = v or u = w or v = w or {u,v,w} is linearly-dependent
by ANPROJ_8:9,ANPROJ_8:43;
then p,q,r are_collinear by A1,A2,ANPROJ_8:10;
hence R on L by A3,A4,Th61;
end;
theorem Th64:
for p,q being Element of ProjectiveSpace TOP-REAL 3 st p <> q & p = Dir u &
q = Dir v holds u <X> v is non zero
proof
let p,q be Element of ProjectiveSpace TOP-REAL 3;
assume that
A1: p <> q & p = Dir u & q = Dir v;
assume u <X> v is zero;
then are_Prop u,v by ANPROJ_8:51;
hence contradiction by A1,ANPROJ_1:22;
end;
definition
let p,q be Point of real_projective_plane;
assume
A1: p <> q;
func L2P(p,q) -> Point of real_projective_plane means
:Def01:
ex u,v being non zero Element of TOP-REAL 3 st p = Dir u & q = Dir v & it =
Dir(u <X> v);
existence
proof
consider u be Element of TOP-REAL 3 such that
A2: u is not zero & p = Dir u by ANPROJ_1:26;
consider v be Element of TOP-REAL 3 such that
A3: v is not zero & q = Dir v by ANPROJ_1:26;
reconsider u,v as non zero Element of TOP-REAL 3 by A2,A3;
u <X> v is non zero by A1,A2,A3,Th64;
then Dir (u <X> v) is Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
hence thesis by A2,A3;
end;
uniqueness
proof
let P1,P2 be Point of real_projective_plane such that
A4: ex u,v being non zero Element of TOP-REAL 3 st p = Dir u &
q = Dir v & P1 = Dir(u <X> v) and
A5: ex u,v being non zero Element of TOP-REAL 3 st p = Dir u &
q = Dir v & P2 = Dir(u <X> v);
consider u1,v1 being non zero Element of TOP-REAL 3 such that
A6: p = Dir u1 & q = Dir v1 & P1 = Dir(u1 <X> v1) by A4;
consider u2,v2 being non zero Element of TOP-REAL 3 such that
A7: p = Dir u2 & q = Dir v2 & P2 = Dir(u2 <X> v2) by A5;
A8: u1 <X> v1 is non zero & u2 <X> v2 is non zero by A1,A6,A7,Th64;
A9: are_Prop u1,u2 & are_Prop v1,v2 by A6,A7,ANPROJ_1:22;
then consider a be Real such that
A10: a <> 0 & u1 = a * u2 by ANPROJ_1:1;
consider b be Real such that
A11: b <> 0 & v1 = b * v2 by A9,ANPROJ_1:1;
u1 <X> v1 = (b * (a * u2)) <X> v2 by A10,A11,EUCLID_5:16
.= ((a * b) * u2) <X> v2 by RVSUM_1:49
.= (a * b) * (u2 <X> v2) by EUCLID_5:16;
then are_Prop u1 <X> v1, u2 <X> v2 by A10,A11,ANPROJ_1:1;
hence P1 = P2 by A6,A7,A8,ANPROJ_1:22;
end;
end;
theorem
for p,q being Point of real_projective_plane st p <> q holds
L2P(q,p) = L2P(p,q) & p <> L2P(p,q)
proof
let p,q be Point of real_projective_plane;
assume
A1: p <> q;
then consider u1,v1 be non zero Element of TOP-REAL 3 such that
A2: p = Dir u1 and
A3: q = Dir v1 and
A4: L2P(p,q) = Dir(u1 <X> v1) by Def01;
consider u2,v2 be non zero Element of TOP-REAL 3 such that
A5: q = Dir u2 and
A6: p = Dir v2 and
A7: L2P(q,p) = Dir(u2 <X> v2) by A1,Def01;
are_Prop u1,v2 by A2,A6,ANPROJ_1:22;
then consider a be Real such that
A8: a <> 0 and
A9: u1 = a * v2 by ANPROJ_1:1;
are_Prop u2,v1 by A3,A5,ANPROJ_1:22;
then consider b be Real such that
A10: b <> 0 and
A11: v1 = b * u2 by ANPROJ_1:1;
(a * v2) <X> (b * u2) = (-a * b) *(u2 <X> v2)
proof
reconsider p1 = a * v2,p2 = b * u2 as Element of TOP-REAL 3;
A12: p1`1 = (a * v2).1 by EUCLID_5:def 1
.= a * v2.1 by RVSUM_1:44;
A13: p1`2 = (a * v2).2 by EUCLID_5:def 2
.= a * v2.2 by RVSUM_1:44;
A14: p1`3 = (a * v2).3 by EUCLID_5:def 3
.= a * v2.3 by RVSUM_1:44;
A15: p2`1 = (b * u2).1 by EUCLID_5:def 1
.= b * u2.1 by RVSUM_1:44;
A16: p2`2 = (b * u2).2 by EUCLID_5:def 2
.= b * u2.2 by RVSUM_1:44;
A17: p2`3 = (b * u2).3 by EUCLID_5:def 3
.= b * u2.3 by RVSUM_1:44;
A18: (a * v2) <X> (b * u2) = |[ (a * v2.2) * (b * u2.3)
-(a * v2.3) * (b * u2.2),
(a * v2.3) * (b * u2.1)
-(a * v2.1) * (b * u2.3),
(a * v2.1) * (b * u2.2)
- (a * v2.2) * (b * u2.1) ]|
by A12,A13,A14,A15,A16,A17,EUCLID_5:def 4;
u2`1 = u2.1 & u2`2 = u2.2 & u2`3 = u2.3 & v2`1 = v2.1 &
v2`2 = v2.2 & v2`3 = v2.3 by EUCLID_5:def 1,def 2,def 3;
then (-a * b) * (u2 <X> v2) = (-a * b) *
|[ (u2.2*v2.3)-(u2.3*v2.2),
(u2.3*v2.1)-(u2.1*v2.3),
(u2.1*v2.2)-(u2.2*v2.1) ]| by EUCLID_5:def 4
.= |[ (-a * b) * ((u2.2*v2.3)
-(u2.3*v2.2)),(-a * b)
* ((u2.3*v2.1)-(u2.1*v2.3)),
(-a * b) * ((u2.1*v2.2)-(u2.2*v2.1)) ]|
by EUCLID_5:8;
hence thesis by A18;
end;
then
A19: are_Prop u1 <X> v1,u2 <X> v2 by A8,A10,A9,A11,ANPROJ_1:1;
A20: u1 <X> v1 is non zero
proof
assume u1 <X> v1 is zero;
then are_Prop u1,v1 by ANPROJ_8:51;
hence contradiction by A1,A2,A3,ANPROJ_1:22;
end;
u2 <X> v2 is non zero
proof
assume u2 <X> v2 is zero;
then are_Prop u2,v2 by ANPROJ_8:51;
hence contradiction by A1,A5,A6,ANPROJ_1:22;
end;
hence L2P(q,p) = L2P(p,q) by A19,A20,A4,A7,ANPROJ_1:22;
thus p <> L2P(p,q)
proof
assume p = L2P(p,q);
then are_Prop u1,u1 <X> v1 by A2,A4,A20,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A21: u1 = a * (u1 <X> v1) by ANPROJ_1:1;
|(u1,a * (u1 <X> v1) )| = a * |(u1,u1 <X> v1)| by Th19
.= a * 0 by ANPROJ_8:44
.= 0;
then u1 = 0.TOP-REAL 3 by A21,EUCLID_2:43;
hence contradiction;
end;
end;
theorem
for N being invertible Matrix of 3,F_Real holds
dom homography(N) = ProjectivePoints TOP-REAL 3
proof
let N be invertible Matrix of 3,F_Real;
dom homography(N) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
hence thesis by ANPROJ_1:23;
end;
begin :: Absolute
definition
let a,b,c,d,e,f be Real;
::: assume not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & f = 0);
func negative_conic(a,b,c,d,e,f) -> Subset of ProjectiveSpace TOP-REAL 3
equals
{P where P is Point of ProjectiveSpace TOP-REAL 3:
for u being Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a,b,c,d,e,f,u) is negative};
coherence
proof
set C = {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(a,b,c,d,e,f,u) is negative};
C c= the carrier of ProjectiveSpace TOP-REAL 3
proof
let x be object;
assume x in C;
then ex P be Point of ProjectiveSpace TOP-REAL 3 st x = P &
for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a,b,c,d,e,f,u) is negative;
hence thesis;
end;
hence thesis;
end;
end;
theorem
for a,b,c,d,e,f being Real for u1,u2 being non zero Element of TOP-REAL 3
st Dir u1 = Dir u2 & qfconic(a,b,c,d,e,f,u1) is negative holds
qfconic(a,b,c,d,e,f,u2) is negative
proof
let a,b,c,d,e,f be Real;
let u1,u2 be non zero Element of TOP-REAL 3;
assume that
A1: Dir u1 = Dir u2 and
A2: qfconic(a,b,c,d,e,f,u1) is negative;
are_Prop u2,u1 by A1,ANPROJ_1:22;
then consider g be Real such that
A3: g <> 0 and
A4: u2 = g * u1 by ANPROJ_1:1;
A5: u2.1 = g * u1.1 & u2.2 = g * u1.2 & u2.3 = g * u1.3 by A4,RVSUM_1:44;
0 < g^2 by A3,SQUARE_1:12;
then reconsider g2 = g * g as positive Real;
qfconic(a,b,c,d,e,f,u2) = a * u2.1 * u2.1 + b * u2.2 * u2.2
+ c * u2.3 * u2.3 + d * u2.1 * u2.2
+ e * u2.1 * u2.3 + f * u2.2 * u2.3
by PASCAL:def 1
.= g2 * (a * u1.1 * u1.1 + b * u1.2 * u1.2
+ c * u1.3 * u1.3 + d * u1.1 * u1.2
+ e * u1.1 * u1.3 + f * u1.2 * u1.3) by A5
.= g2 * qfconic(a,b,c,d,e,f,u1) by PASCAL:def 1;
hence thesis by A2;
end;
definition
func absolute -> non empty Subset of ProjectiveSpace TOP-REAL 3 equals
conic(1,1,-1,0,0,0);
coherence
proof
Dir101 in conic(1,1,-1,0,0,0)
proof
Dir101 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) = 0}
proof
now
let u be Element of TOP-REAL 3;
assume
A1: u is non zero & Dir101 = Dir u;
|[1,0,1]| is non zero by EUCLID_5:4,FINSEQ_1:78;
then are_Prop u,|[1,0,1]| by A1,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A2: u = a * |[1,0,1]| by ANPROJ_1:1;
u = |[a * 1,a * 0,a * 1]| by A2,EUCLID_5:8
.= |[a,0,a]|;
then u`1 = a & u`2 = 0 & u`3 = a by EUCLID_5:2;
then
A3: u.1 = a & u.2 = 0 & u.3 = a by EUCLID_5:def 1,def 2,def 3;
thus qfconic(1,1,-1,0,0,0,u) = 1 * u.1 * u.1 + 1 * u.2 * u.2
+ (- 1) * u.3 * u.3 + 0 * u.1 * u.2
+ 0 * u.1 * u.3 + 0 * u.2 * u.3
by PASCAL:def 1
.= 0 by A3;
end;
hence thesis;
end;
hence thesis by PASCAL:def 2;
end;
hence thesis;
end;
end;
theorem Th66:
for O being Matrix of 3,REAL
for P being Element of ProjectiveSpace TOP-REAL 3
for p being FinSequence of REAL st
O = symmetric_3(1,1,-1,0,0,0) & P = Dir u & u = p
holds P in absolute iff SumAll QuadraticForm(p,O,p) = 0
proof
let O be Matrix of 3,REAL;
let P be Element of ProjectiveSpace TOP-REAL 3;
let p be FinSequence of REAL;
assume
A1: O = symmetric_3(1,1,-1,0,0,0) & P = Dir u & u = p;
hereby
assume P in absolute;
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) = 0} by PASCAL:def 2;
then consider Q being Point of ProjectiveSpace TOP-REAL 3 such that
A2: P = Q and
A3: 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) = 0;
consider u1 be Element of TOP-REAL 3 such that
A4: u1 is non zero and
A5: Q = Dir u1 by ANPROJ_1:26;
reconsider p1 = u1 as FinSequence of REAL by EUCLID:24;
A6: SumAll QuadraticForm(p1,O,p1) = qfconic(1,1,-1,2 * 0,2 * 0, 2 * 0,u1)
by A1,PASCAL:13
.= 0 by A3,A4,A5;
are_Prop u1,u by A2,A5,A1,A4,ANPROJ_1:22;
then consider a be Real such that
A7: a <> 0 and
A8: u1 = a * u by ANPROJ_1:1;
reconsider fa = a as Element of F_Real by XREAL_0:def 1;
u is Element of REAL 3 by EUCLID:22;
then len p = 3 by A1,EUCLID_8:50;
then SumAll QuadraticForm(p1,O,p1)
= fa * fa * SumAll QuadraticForm(p,O,p) by A1,A8,Th35;
hence SumAll QuadraticForm(p,O,p) = 0 by A7,A6;
end;
assume SumAll QuadraticForm(p,O,p) = 0;
then 0 = qfconic(1,1,-1,2 * 0,2 * 0, 2 * 0,u) by A1,PASCAL:13
.= qfconic(1,1,-1,0,0, 0,u);
then 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) = 0 by A1,PASCAL:10;
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) = 0};
hence P in absolute by PASCAL:def 2;
end;
theorem Th67:
for P being Element of absolute st P = Dir u holds u.3 <> 0
proof
let P be Element of absolute;
assume
A1: P = Dir u;
P in conic(1,1,-1,0,0,0);
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) = 0} by PASCAL:def 2;
then consider Q be Point of ProjectiveSpace TOP-REAL 3 such that
A2: P = Q and
A3: 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) = 0;
A4: qfconic(1,1,-1,0,0,0,u) = 0 by A1,A2,A3;
thus u.3 <> 0
proof
assume
A5: u.3 = 0;
A6: 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 = 0 by A4,PASCAL:def 1;
reconsider u1 = u.1, u2 = u.2 as Real;
u1 ^2 + u2 ^2 = 0 by A5,A6;
then u1 = 0 & u2 = 0 by COMPLEX1:1;
then u`1 = 0 & u`2 = 0 & u`3 = 0 by A5,EUCLID_5:def 1,def 2,def 3;
hence contradiction by EUCLID_5:3,4;
end;
end;
theorem Th68:
for P being Element of absolute st P = Dir u & u.3 = 1 holds
|[u.1,u.2]| in circle(0,0,1)
proof
let P be Element of absolute;
assume that
A1: P = Dir u and
A2: u.3 = 1;
P in conic(1,1,-1,0,0,0);
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) = 0} by PASCAL:def 2;
then consider Q be Point of ProjectiveSpace TOP-REAL 3 such that
A3: P = Q and
A4: 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) = 0;
qfconic(1,1,-1,0,0,0,u) = 0 by A1,A3,A4;
then
A5: 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 = 0 by PASCAL:def 1;
reconsider u1 = u.1, u2 = u.2 as Real;
u1^2 + u2^2 = 1 by A2,A5;
hence thesis by Th11;
end;
theorem Th69:
for P being Point of ProjectiveSpace TOP-REAL 3 st
P = Dir u & u.3 = 1 & |[u.1,u.2]| in circle(0,0,1) holds
P is Element of absolute
proof
let P be Point of ProjectiveSpace TOP-REAL 3;
assume that
A1: P = Dir u and
A2: u.3 = 1 and
A3: |[u.1,u.2]| in circle(0,0,1);
reconsider u1 = u.1, u2 = u.2, u3 = u.3 as Real;
A4: u1^2 + u2^2 = |. |[u1 - 0,u2 - 0]| .|^2 by TOPGEN_5:9
.= |. |[u1,u2]| - |[0,0]| .|^2 by EUCLID:62
.= 1^2 by A3,TOPREAL9:43
.= 1;
now
let v be Element of TOP-REAL 3;
assume that
A5: v is non zero and
A6: P = Dir v;
are_Prop u,v by A1,A5,A6,ANPROJ_1:22;
then consider a be Real such that
A7: a <> 0 and
A8: u = a * v by ANPROJ_1:1;
reconsider v1 = v.1, v2 = v.2,v3 = v.3 as Real;
u1 = a * v1 & u2 = a * v2 & u3 = a * v3 by A8,RVSUM_1:44;
then
A9: v1 = u1 / a & v2 = u2 / a & v3 = u3 / a by A7,XCMPLX_1:89;
qfconic(1,1,-1,0,0,0,v)
= 1 * v1 * v1 + 1 * v2 * v2 + (-1) * v3 * v3 + 0 * v1 * v2
+ 0 * v1 * v3 + 0 * v2 * v3 by PASCAL:def 1
.= (u1 / a) * (u1 / a) + (u2 / a) * (u2 / a) - (u3 / a) * (u3 / a)
by A9
.= 1/a * u1 * (u1 / a) + (u2 / a) * (u2 / a) - (u3 / a) * (u3 / a)
by XCMPLX_1:99
.= 1/a * u1 * (1/a * u1) + (u2 / a) * (u2 / a) - (u3 / a) * (u3 / a)
by XCMPLX_1:99
.= ((1/a) * (1/a)) * u1 * u1 + 1 / a * u2 * (u2 / a)
- (u3 / a) * (u3 / a) by XCMPLX_1:99
.= ((1/a) * (1/a)) * u1 * u1 + 1 / a * u2 * (1/a * u2)
- (u3 / a) * (u3 / a) by XCMPLX_1:99
.= ((1/a) * (1/a)) * u1 * u1 + ((1 / a) * (1 / a)) * u2 * u2
- 1/a * u3 * (u3 / a) by XCMPLX_1:99
.= ((1/a) * (1/a)) * u1 * u1 + ((1 / a) * (1 / a)) * u2 * u2
- 1/a * u3 * (1/a * u3) by XCMPLX_1:99
.= ((1/a) * (1/a)) * (u1^2 + u2 * u2 - u3 * u3)
.= 0 by A2,A4;
hence qfconic(1,1,-1,0,0,0,v)=0;
end;
then P in {P where P is Point of ProjectiveSpace TOP-REAL 3:
for u being Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(1,1,-1,0,0,0,u) = 0};
hence thesis by PASCAL:def 2;
end;
theorem
for P being Point of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st
P = Dir u & u.3 = 1 holds
|[u.1,u.2]| in circle(0,0,1) iff P is Element of absolute by Th68,Th69;
definition
let P be Element of absolute;
func absolute_to_REAL2(P) -> Element of circle(0,0,1) means
ex u being non zero Element of TOP-REAL 3 st P = Dir u &
u.3 = 1 & it = |[u.1,u.2]|;
existence
proof
consider u be Element of TOP-REAL 3 such that
A1: u is non zero and
A2: P = Dir u by ANPROJ_1:26;
u.3 <> 0 by A1,A2,Th67;
then
A3: u`3 <> 0 by EUCLID_5:def 3;
then reconsider r = 1/u`3 as non zero Real;
reconsider v = |[u`1/u`3,u`2/u`3,1]| as non zero Element of TOP-REAL 3
by Th36;
r * u = 1/u`3 * |[u`1,u`2,u`3]| by EUCLID_5:3
.= |[1/u`3 * u`1,1/u`3 * u`2,1/u`3 * u`3]| by EUCLID_5:8
.= |[u`1/u`3,1/u`3 * u`2,1/u`3 * u`3]| by XCMPLX_1:99
.= |[u`1/u`3,u`2/u`3,1/u`3 * u`3]| by XCMPLX_1:99
.= |[u`1/u`3 ,u`2/u`3, u`3/u`3 ]| by XCMPLX_1:99
.= v by A3,XCMPLX_1:60;
then are_Prop u,v by ANPROJ_1:1;
then
A4: P = Dir v by A1,A2,ANPROJ_1:22;
A5: v.3 = v`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
then |[v.1,v.2]| in circle(0,0,1) by A4,Th68;
hence thesis by A4,A5;
end;
uniqueness
proof
let u1,u2 be Element of circle(0,0,1) such that
A6: ex u being non zero Element of TOP-REAL 3 st P = Dir u & u.3 = 1 &
u1 = |[u.1,u.2]| and
A7: ex v being non zero Element of TOP-REAL 3 st P = Dir v & v.3 = 1 &
u2 = |[v.1,v.2]|;
consider u being non zero Element of TOP-REAL 3 such that
A8: P = Dir u & u.3 = 1 & u1 = |[u.1,u.2]| by A6;
consider v being non zero Element of TOP-REAL 3 such that
A9: P = Dir v & v.3 = 1 & u2 = |[v.1,v.2]| by A7;
|[u`1,u`2,u`3]| = u by EUCLID_5:3
.= v by A8,A9,Th37
.= |[v`1,v`2,v`3]| by EUCLID_5:3;
then u`1 = v`1 & u`2 = v`2 & u`3 = v`3 by FINSEQ_1:78;
then u.1 = v`1 & u.2 = v`2 by EUCLID_5:def 1,def 2;
then u.1 = v.1 & u.2 = v.2 by EUCLID_5:def 1,def 2;
hence thesis by A8,A9;
end;
end;
theorem
the carrier of Tunit_circle(2) = circle(0,0,1)
proof
A1: the carrier of Tunit_circle(2) c= circle(0,0,1)
proof
let u be object;
assume u in the carrier of Tunit_circle(2);
then u in the carrier of Tcircle(0.TOP-REAL 2,1) by TOPREALB:def 7;
then u in Sphere(0.TOP-REAL 2,1) by TOPREALB:9;
hence thesis by EUCLID:54,TOPREAL9:52;
end;
circle(0,0,1) c= the carrier of Tunit_circle(2)
proof
let u be object;
assume u in circle(0,0,1);
then u in Sphere(0.TOP-REAL 2,1) by TOPREAL9:52,EUCLID:54;
then u in the carrier of Tcircle(0.TOP-REAL 2,1) by TOPREALB:9;
hence thesis by TOPREALB:def 7;
end;
hence thesis by A1;
end;
definition
let u be non zero Element of TOP-REAL 2;
assume
A1: u in circle(0,0,1);
func REAL2_to_absolute(u) -> Element of absolute equals Dir |[u.1,u.2,1]|;
coherence
proof
|[u`1,u`2]| in circle(0,0,1) by A1,EUCLID:53; then
A2: |[u.1,u`2]| in circle(0,0,1) by EUCLID:def 9;
reconsider v = |[u.1,u.2,1]| as non zero Element of TOP-REAL 3 by Th36;
reconsider P = Dir v as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
A3: |[v.1,v.2]| in circle(0,0,1) by A2,EUCLID:def 10;
v.3 = v`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
then P is Element of absolute by A3,Th69;
hence thesis;
end;
end;
theorem Th70:
for u being Element of TOP-REAL 3 st qfconic(1,1,-1,0,0,0,u) = 0 & u.3 = 1
holds|[u.1,u.2]| in Sphere(0.TOP-REAL 2,1)
proof
let u be Element of TOP-REAL 3;
assume that
A1: qfconic(1,1,-1,0,0,0,u) = 0 and
A2: u.3 = 1;
0 = 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 A1,PASCAL:def 1
.= (u.1)^2 + (u.2)^2 - 1 by A2;
then |[u.1,u.2]| in circle(0,0,1) by Th11;
hence thesis by EUCLID:54,TOPREAL9:52;
end;
theorem
for P being Element of absolute holds
ex u st (u.1)^2 + (u.2)^2 = 1 & u.3 = 1 & P = Dir u
proof
let P be Element of absolute;
consider u be Element of TOP-REAL 3 such that
A1: u is non zero and
A2: Dir u = P by ANPROJ_1:26;
reconsider v1 = u.1/u.3,v2 = u.2/u.3 as Real;
reconsider v = |[v1,v2,1]| as Element of TOP-REAL 3;
A3: v.3 = v`3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2;
A4: v is non zero by EUCLID_5:4,FINSEQ_1:78;
u.3 * v = |[ u.3 * v1, u.3 * v2, u.3 * 1]| by EUCLID_5:8
.= |[u.1,u.3 * v2,u.3]| by A1,A2,Th67,XCMPLX_1:87
.= |[u.1,u.2,u.3]| by A1,A2,Th67,XCMPLX_1:87
.= |[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;
then are_Prop u,v by A1,A2,Th67,ANPROJ_1:1;
then
A5: Dir v = Dir u by A1,A4,ANPROJ_1:22;
|[v.1,v.2]| in circle(0,0,1) by A2,A3,A4,A5,Th68;
then (v.1)^2 + (v.2)^2 = 1^2 by Th12
.= 1;
hence thesis by A2,A3,A4,A5;
end;
theorem
for P being Element of absolute ex Q being Element of absolute st P <> Q
proof
let P be Element of absolute;
P in conic(1,1,-1,0,0,0);
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) = 0} by PASCAL:def 2;
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) = 0;
consider u be Element of TOP-REAL 3 such that
A3: u is non zero and
A4: Dir u = P by ANPROJ_1:26;
A5: qfconic(1,1,-1,0,0,0,u) = 0 by A1,A2,A3,A4;
A6: u.3 <> 0 by A3,A4,Th67;
|[u.1,u.2,-u.3]| is non zero
proof
assume |[u.1,u.2,-u.3]| is zero;
then u.3 = 0 by EUCLID_5:4,FINSEQ_1:78;
hence contradiction by A3,A4,Th67;
end;
then reconsider v = |[u.1,u.2,-u.3]| as non zero Element of TOP-REAL 3;
reconsider R = Dir v as Element of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
take R;
A7: R <> P
proof
assume R = P;
then are_Prop v,u by A3,A4,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A8: v = a * u by ANPROJ_1:1;
A9: -u.3 = v`3 by EUCLID_5:2
.= (a * u).3 by A8,EUCLID_5:def 3
.= a * u.3 by RVSUM_1:44;
(a + 1) * u.3 = 0 by A9;
then a + 1 = 0 by A6; then
A10: a = -1;
A11: u.1 = v`1 by EUCLID_5:2
.= (a * u).1 by A8,EUCLID_5:def 1
.= a * u.1 by RVSUM_1:44;
A12: u.2 = v`2 by EUCLID_5:2
.= (a * u).2 by A8,EUCLID_5:def 2
.= a * u.2 by RVSUM_1:44;
0 = 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 A5,PASCAL:def 1
.= (-1) * (u.3)^2 by A11,A10,A12;
hence contradiction by A6;
end;
for w be Element of TOP-REAL 3 st w is non zero & R = Dir w holds
qfconic(1,1,-1,0,0,0,w) = 0
proof
let w be Element of TOP-REAL 3;
assume that
A13: w is non zero and
A14: R = Dir w;
are_Prop v,w by A13,A14,ANPROJ_1:22;
then consider b be Real such that
b <> 0 and
A15: w = b * v by ANPROJ_1:1;
A16: w.1 = b * v.1 by A15,RVSUM_1:44
.= b * v`1 by EUCLID_5:def 1
.= b * u.1 by EUCLID_5:2;
A17: w.2 = b * v.2 by A15,RVSUM_1:44
.= b * v`2 by EUCLID_5:def 2
.= b * u.2 by EUCLID_5:2;
A18: w.3 = b * v.3 by A15,RVSUM_1:44
.= b * v`3 by EUCLID_5:def 3
.= b * (-u.3) by EUCLID_5:2;
qfconic(1,1,-1,0,0,0,w) = 1 * w.1 * w.1 + 1 * w.2 * w.2
+ (-1) * w.3 * w.3 + 0 * w.1 * w.2
+ 0 * w.1 * w.3 + 0 * w.2 * w.3
by PASCAL:def 1
.= b * b * (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 A16,A17,A18
.= b * b * qfconic(1,1,-1,0,0,0,u) by PASCAL:def 1
.= 0 by A5;
hence thesis;
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) = 0};
hence thesis by A7,PASCAL:def 2;
end;
theorem
for a,b being Real st a^2 + b^2 = 1 holds |[-b,a,0]| is non zero
proof
let a,b be Real;
assume
A1: a^2 + b^2 = 1;
assume |[-b,a,0]| is zero;
then -b = 0 & a = 0 by EUCLID_5:4,FINSEQ_1:78;
hence contradiction by A1;
end;
theorem
for P,Q,R being Element of absolute st P,Q,R are_mutually_distinct holds
not P,Q,R are_collinear
proof
let P,Q,R be Element of absolute;
assume
A1: P,Q,R are_mutually_distinct;
consider up be Element of TOP-REAL 3 such that
A2: up is non zero and
A3: P = Dir up by ANPROJ_1:26;
consider uq be Element of TOP-REAL 3 such that
A4: uq is non zero and
A5: Q = Dir uq by ANPROJ_1:26;
consider ur be Element of TOP-REAL 3 such that
A6: ur is non zero and
A7: R = Dir ur by ANPROJ_1:26;
reconsider up1 = up`1,up2 = up`2,up3 = up`3,
uq1 = uq`1,uq2 = uq`2,uq3 = uq`3,
ur1 = ur`1,ur2 = ur`2,ur3 = ur`3 as Real;
up.3 <> 0 & uq.3 <> 0 & ur.3 <> 0 by A2,A3,A4,A5,A6,A7,Th67;
then
A8: up3 <> 0 & uq3 <> 0 & ur3 <> 0 by EUCLID_5:def 3;
reconsider vp1 = up1 / up3,vp2 = up2 / up3, vq1 = uq1 / uq3,
vq2 = uq2 / uq3, vr1 = ur1 / ur3,vr2 = ur2 / ur3 as Real;
reconsider vp = |[ vp1,vp2,1 ]|, vq = |[ vq1,vq2,1 ]|,
vr = |[ vr1,vr2,1 ]| as non zero Element of TOP-REAL 3
by Th36;
A9: vp`3 = 1 & vq`3 = 1 & vr`3 = 1 by EUCLID_5:2;
A10: vp.3 = 1 & vq.3 = 1 & vr.3 = 1;
A11: P = Dir vp & Q = Dir vq & R = Dir vr
proof
thus P = Dir vp
proof
are_Prop up,vp
proof
up3 * vp = |[up3 * (up1/ up3),up3 * (up2 / up3),up3 * 1]|
by EUCLID_5:8
.= |[up1,up3 * (up2 / up3),up3 * 1]| by A8,XCMPLX_1:87
.= |[up1,up2,up3 * 1]| by A8,XCMPLX_1:87
.= up by EUCLID_5:3;
hence thesis by A8,ANPROJ_1:1;
end;
hence thesis by A2,A3,ANPROJ_1:22;
end;
thus Q = Dir vq
proof
are_Prop uq,vq
proof
uq3 * vq = |[uq3 * (uq1/ uq3),uq3 * (uq2 / uq3),uq3 * 1]|
by EUCLID_5:8
.= |[uq1,uq3 * (uq2 / uq3),uq3 * 1]| by A8,XCMPLX_1:87
.= |[uq1,uq2,uq3 * 1]| by A8,XCMPLX_1:87
.= uq by EUCLID_5:3;
hence thesis by A8,ANPROJ_1:1;
end;
hence thesis by A4,A5,ANPROJ_1:22;
end;
thus R = Dir vr
proof
are_Prop ur,vr
proof
ur3 * vr = |[ur3 * (ur1/ ur3),ur3 * (ur2 / ur3),ur3 * 1]|
by EUCLID_5:8
.= |[ur1,ur3 * (ur2 / ur3),ur3 * 1]| by A8,XCMPLX_1:87
.= |[ur1,ur2,ur3 * 1]| by A8,XCMPLX_1:87
.= ur by EUCLID_5:3;
hence thesis by A8,ANPROJ_1:1;
end;
hence thesis by A6,A7,ANPROJ_1:22;
end;
end;
assume P,Q,R are_collinear;
then consider tp,tq,tr be Element of TOP-REAL 3 such that
A12: P = Dir(tp) & Q = Dir(tq) & R = Dir(tr) and
A13: tp is not zero & tq is not zero & tr is not zero and
A14: ex a1,b1,c1 be Real st a1*tp + b1*tq + c1*tr = 0.TOP-REAL 3 &
(a1<>0 or b1<>0 or c1<>0) by ANPROJ_8:11;
consider a1,b1,c1 be Real such that
A15: a1 * tp + b1 * tq + c1 * tr = 0.TOP-REAL 3 and
A16: (a1<>0 or b1<>0 or c1<>0) by A14;
A17: are_Prop tp,vp & are_Prop tq,vq & are_Prop tr,vr
by A12,A13,A11,ANPROJ_1:22;
consider lp be Real such that
A18: lp <> 0 and
A19: tp = lp * vp by A17,ANPROJ_1:1;
consider lq be Real such that
A20: lq <> 0 and
A21: tq = lq * vq by A17,ANPROJ_1:1;
consider lr be Real such that
A22: lr <> 0 and
A23: tr = lr * vr by A17,ANPROJ_1:1;
reconsider A = |[vp`1,vp`2]|, B = |[vq`1,vq`2]|,
C = |[vr`1,vr`2]| as Element of TOP-REAL 2;
A24: B.1 = B`1 by EUCLID:def 9
.= vq`1 by EUCLID:52
.= vq.1 by EUCLID_5:def 1;
A25: B.2 = B`2 by EUCLID:def 10
.= vq`2 by EUCLID:52
.= vq.2 by EUCLID_5:def 2;
A26: C.1 = C`1 by EUCLID:def 9
.= vr`1 by EUCLID:52
.= vr.1 by EUCLID_5:def 1;
A27: C.2 = C`2 by EUCLID:def 10
.= vr`2 by EUCLID:52
.= vr.2 by EUCLID_5:def 2;
A28: A.1 = A`1 by EUCLID:def 9
.= vp`1 by EUCLID:52
.= vp.1 by EUCLID_5:def 1;
A29: A.2 = A`2 by EUCLID:def 10
.= vp`2 by EUCLID:52
.= vp.2 by EUCLID_5:def 2;
A30: A <> B
proof
assume A = B;
then
A30BIS: vp`1 = vq`1 & vp`2 = vq`2 by FINSEQ_1:77;
vp = |[vp`1,vp`2,vp`3]| by EUCLID_5:3
.= vq by A9,A30BIS,EUCLID_5:3;
hence contradiction by A11,A1;
end;
A31: A <> C
proof
assume A = C;
then
A31BIS: vp`1 = vr`1 & vp`2 = vr`2 by FINSEQ_1:77;
vp = |[vp`1,vp`2,vp`3]| by EUCLID_5:3
.= vr by A9,A31BIS,EUCLID_5:3;
hence contradiction by A11,A1;
end;
A32: B <> C
proof
assume B = C;
then
A32BIS: vq`1 = vr`1 & vq`2 = vr`2 by FINSEQ_1:77;
vq = |[vq`1,vq`2,vq`3]| by EUCLID_5:3
.= vr by A9,A32BIS,EUCLID_5:3;
hence contradiction by A11,A1;
end;
A34: A in Sphere(0.TOP-REAL 2,1)
proof
A35: qfconic(1,1,-1,0,0,0,vp) = 0
proof
P in conic(1,1,-1,0,0,0);
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) = 0} by PASCAL:def 2;
then ex PP be Point of ProjectiveSpace TOP-REAL 3 st P = PP & for u
being Element of TOP-REAL 3 st u is non zero & PP = Dir u holds
qfconic(1,1,-1,0,0,0,u) = 0;
hence thesis by A11;
end;
vp.1 = vp`1 & vp.2 = vp`2 by EUCLID_5:def 1,def 2;
hence A in Sphere(0.TOP-REAL 2,1) by A35,A10,Th70;
end;
A36: qfconic(1,1,-1,0,0,0,vq) = 0
proof
Q in conic(1,1,-1,0,0,0);
then Q in {P where P is Point of ProjectiveSpace TOP-REAL 3:
for u being Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(1,1,-1,0,0,0,u) = 0} by PASCAL:def 2;
then ex QP be Point of ProjectiveSpace TOP-REAL 3 st
Q = QP & for u being Element of TOP-REAL 3 st u is non zero &
QP = Dir u holds qfconic(1,1,-1,0,0,0,u) = 0;
hence thesis by A11;
end;
vq.1 = vq`1 & vq.2 = vq`2 by EUCLID_5:def 1,def 2; then
A37: B in Sphere(0.TOP-REAL 2,1) by A36,A10,Th70;
A38: C in Sphere(0.TOP-REAL 2,1)
proof
A39: qfconic(1,1,-1,0,0,0,vr) = 0
proof
R in conic(1,1,-1,0,0,0);
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) = 0} by PASCAL:def 2;
then ex RP be Point of ProjectiveSpace TOP-REAL 3 st R = RP &
for u being Element of TOP-REAL 3 st u is non zero &
RP = Dir u holds
qfconic(1,1,-1,0,0,0,u) = 0;
hence thesis by A11;
end;
vr.1 = vr`1 & vr.2 = vr`2 by EUCLID_5:def 1,def 2;
hence C in Sphere(0.TOP-REAL 2,1) by A39,A10,Th70;
end;
A40: halfline(B,C) /\ Sphere(0.TOP-REAL 2,1) = {B,C} &
halfline(C,B) /\ Sphere(0.TOP-REAL 2,1) = {C,B} &
halfline(A,C) /\ Sphere(0.TOP-REAL 2,1) = {A,C} &
halfline(C,A) /\ Sphere(0.TOP-REAL 2,1) = {C,A} &
halfline(A,B) /\ Sphere(0.TOP-REAL 2,1) = {A,B} &
halfline(B,A) /\ Sphere(0.TOP-REAL 2,1) = {B,A}
by A37,A38,A34,TOPREAL9:36;
per cases by A16;
suppose a1 <> 0; then
A41: lp * vp = ((-b1)/a1) * (lq * vq) + ((-c1)/a1) * (lr * vr)
by A19,A21,A23,A15,ANPROJ_8:12
.= ((-b1)/a1)*lq * vq + ((-c1)/a1) * (lr * vr) by RVSUM_1:49
.= ((-b1)/a1)*lq * vq + ((-c1)/a1)*lr * vr by RVSUM_1:49;
reconsider m1 = 1/lp * (((-b1)/a1) * lq),
m2 = 1/lp * (((-c1)/a1)* lr) as Real;
1 = lp / lp by A18,XCMPLX_1:60
.= 1/lp * lp by XCMPLX_1:99; then
A42: vp = (1/lp * lp) * vp by RVSUM_1:52
.= 1/lp * (((-b1)/a1)*lq * vq + ((-c1)/a1)*lr * vr) by A41,RVSUM_1:49
.= 1/lp * (((-b1)/a1)*lq * vq) + 1/lp * (((-c1)/a1)*lr * vr)
by RVSUM_1:51
.= 1/lp * (((-b1)/a1)*lq) * vq + 1/lp * (((-c1)/a1)*lr * vr)
by RVSUM_1:49
.= m1 * vq + m2 * vr by RVSUM_1:49;
A43: m1 = 1 - m2
proof
m1 * vq + m2 * vr = |[m1 * vq`1,m1 * vq`2,m1 * vq`3]| + m2 * vr
by EUCLID_5:7
.= |[m1 * vq`1,m1 * vq`2,m1 * vq`3]|
+ |[m2 * vr`1,m2 * vr`2,m2 * vr`3]| by EUCLID_5:7
.= |[m1 * vq`1 + m2 * vr`1,
m1 * vq`2 + m2 * vr`2,
m1 * vq`3 + m2 * vr`3]| by EUCLID_5:6;
then vp`3 = m1 * vq`3 + m2 * vr`3 by A42,EUCLID_5:14;
hence thesis by A9;
end;
per cases;
suppose
A44: 0 <= m2;
A45: A in halfline(B,C)
proof
reconsider tu = (1-m2)*vq, tv = m2*vr as Element of TOP-REAL 3;
A46: ((1 - m2) * vq).1 = (1-m2) * vq.1 by RVSUM_1:44;
A47: tu`1 = tu.1 & tv`1 = tv.1 by EUCLID_5:def 1;
A48: A`1 = vp`1 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`1 by A43,A42,EUCLID_5:5
.= tu.1 + tv.1 by A47,EUCLID_5:2
.= (1-m2) * B.1 + m2 * C.1 by A46,RVSUM_1:44,A24,A26;
A49: ((1 - m2) * vq).2 = (1-m2) * vq.2 by RVSUM_1:44;
A50: tu`2 = tu.2 & tv`2 = tv.2 by EUCLID_5:def 2;
A51: A`2 = vp`2 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`2 by A43,A42,EUCLID_5:5
.= tu.2 + tv.2 by A50,EUCLID_5:2
.= (1-m2) * B.2 + m2 * C.2 by A49,A25,A27,RVSUM_1:44;
A = |[(1-m2)*B.1 + m2 * C.1,(1-m2)*B.2+m2 * C.2]|
by A48,A51,EUCLID:53
.= |[(1-m2) * B.1,(1-m2)*B.2]| + |[m2 * C.1,m2 * C.2]| by EUCLID:56
.= (1 - m2) * |[B.1,B.2]| + |[m2 * C.1,m2 * C.2]| by EUCLID:58
.= (1 - m2) * B + m2 * C by EUCLID:58;
hence thesis by A44,TOPREAL9:26;
end;
A in halfline(B,C) /\ Sphere(0.TOP-REAL 2,1)
by A45,A34,XBOOLE_0:def 4;
hence contradiction by A30,A31,A40,TARSKI:def 2;
end;
suppose
A54: m2 < 0;
set m3 = 1 - m2;
A in halfline(C,B)
proof
reconsider tu = (1-m3)*vr, tv = m3*vq as Element of TOP-REAL 3;
A55: ((1 - m3) * vr).1 = (1-m3) * vr.1 by RVSUM_1:44;
A56: tu`1 = tu.1 & tv`1 = tv.1 by EUCLID_5:def 1;
A56b: A`1 = vp`1 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`1 by A43,A42,EUCLID_5:5
.= tu.1 + tv.1 by EUCLID_5:2,A56
.= (1-m3) * C.1 + m3 * B.1 by A24,A26,A55,RVSUM_1:44;
A57: ((1 - m3) * vr).2 = (1-m3) * vr.2 by RVSUM_1:44;
A58: tu`2 = tu.2 & tv`2 = tv.2 by EUCLID_5:def 2;
A59: A`2 = vp`2 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`2 by A43,A42,EUCLID_5:5
.= tu`2 + tv`2 by EUCLID_5:2
.= (1-m3) * C.2 + m3 * B.2 by A57,A58,RVSUM_1:44,A25,A27;
A = |[(1-m3)*C.1 + m3 * B.1,(1-m3)*C.2+m3 * B.2]|
by A56b,A59,EUCLID:53
.= |[(1-m3) * C.1,(1-m3)*C.2]| + |[m3 * B.1,m3 * B.2]| by EUCLID:56
.= (1 - m3) * |[C.1,C.2]| + |[m3 * B.1,m3 * B.2]| by EUCLID:58
.= (1 - m3) * C + m3 * B by EUCLID:58;
hence thesis by A54,TOPREAL9:26;
end;
then A in {C,B} by A40,A34,XBOOLE_0:def 4;
hence contradiction by A30,A31,TARSKI:def 2;
end;
end;
suppose
A62: b1 <> 0;
b1 * tq + a1 * tp + c1 * tr = 0.TOP-REAL 3 by A15;
then
A63: lq * vq = ((-a1)/b1) * (lp * vp) + ((-c1)/b1) * (lr * vr)
by A19,A21,A23,A62,ANPROJ_8:12
.= ((-a1)/b1)*lp * vp + ((-c1)/b1) * (lr * vr) by RVSUM_1:49
.= ((-a1)/b1)*lp * vp + ((-c1)/b1)*lr * vr by RVSUM_1:49;
reconsider m1 = 1/lq * (((-a1)/b1) * lp), m2 = 1/lq * (((-c1)/b1)* lr)
as Real;
1 = lq / lq by A20,XCMPLX_1:60
.= 1/lq * lq by XCMPLX_1:99; then
A65: vq = (1/lq * lq) * vq by RVSUM_1:52
.= 1/lq * (((-a1)/b1)*lp * vp + ((-c1)/b1)*lr * vr) by A63,RVSUM_1:49
.= 1/lq * (((-a1)/b1)*lp * vp) + 1/lq * (((-c1)/b1)*lr * vr)
by RVSUM_1:51
.= 1/lq * (((-a1)/b1)*lp) * vp + 1/lq * (((-c1)/b1)*lr * vr)
by RVSUM_1:49
.= m1 * vp + m2 * vr by RVSUM_1:49;
A66: m1 = 1 - m2
proof
m1 * vp + m2 * vr = |[m1 * vp`1,m1 * vp`2,
m1 * vp`3]| + m2 * vr by EUCLID_5:7
.= |[m1 * vp`1,m1 * vp`2,m1 * vp`3]|
+ |[m2 * vr`1,m2 * vr`2,m2 * vr`3]| by EUCLID_5:7
.= |[m1 * vp`1 + m2 * vr`1, m1 * vp`2 + m2 * vr`2,
m1 * vp`3 + m2 * vr`3]| by EUCLID_5:6;
then 1 = m1 * 1 + m2 * 1 by A9,A65,EUCLID_5:14;
hence thesis;
end;
per cases;
suppose
A67: 0 <= m2;
B in halfline(A,C)
proof
reconsider tu = (1-m2)*vp, tv = m2*vr as Element of TOP-REAL 3;
A68: ((1 - m2) * vp).1 = (1-m2) * vp.1 by RVSUM_1:44;
A69: tu`1 = tu.1 & tv`1 = tv.1 by EUCLID_5:def 1;
A70: B`1 = vq`1 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`1 by A66,A65,EUCLID_5:5
.= tu`1 + tv`1 by EUCLID_5:2
.= (1-m2) * A.1 + m2 * C.1 by A26,A28,A68,A69,RVSUM_1:44;
A71: ((1 - m2) * vp).2 = (1-m2) * vp.2 by RVSUM_1:44;
A72: tu`2 = tu.2 & tv`2 = tv.2 by EUCLID_5:def 2;
A73: B`2 = vq`2 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`2 by A66,A65,EUCLID_5:5
.= tu`2 + tv`2 by EUCLID_5:2
.= (1-m2) * A.2 + m2 * C.2 by A27,A29,A71,A72,RVSUM_1:44;
B = |[(1-m2)*A.1 + m2 * C.1,(1-m2)*A.2+m2 * C.2]|
by A70,A73,EUCLID:53
.= |[(1-m2) * A.1,(1-m2)*A.2]| + |[m2 * C.1,m2 * C.2]| by EUCLID:56
.= (1 - m2) * |[A.1,A.2]| + |[m2 * C.1,m2 * C.2]| by EUCLID:58
.= (1 - m2) * A + m2 * C by EUCLID:58;
hence thesis by A67,TOPREAL9:26;
end;
then B in {A,C} by A40,A37,XBOOLE_0:def 4;
hence contradiction by A30,A32,TARSKI:def 2;
end;
suppose
A76: m2 < 0;
set m3 = 1 - m2;
B in halfline(C,A)
proof
reconsider tu = (1-m3)*vr, tv = m3*vp as Element of TOP-REAL 3;
A77: ((1 - m3) * vr).1 = (1-m3) * vr.1 by RVSUM_1:44;
A78: tu`1 = tu.1 & tv`1 = tv.1 by EUCLID_5:def 1;
A79: B`1 = vq`1 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`1 by EUCLID_5:5,A66,A65
.= tu`1 + tv`1 by EUCLID_5:2
.= (1-m3) * C.1 + m3 * A.1 by A26,A28,A77,A78,RVSUM_1:44;
A80: ((1 - m3) * vr).2 = (1-m3) * vr.2 by RVSUM_1:44;
A81: tu`2 = tu.2 & tv`2 = tv.2 by EUCLID_5:def 2;
A82: B`2 = vq`2 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`2 by A66,A65,EUCLID_5:5
.= tu`2 + tv`2 by EUCLID_5:2
.= (1-m3) * C.2 + m3 * A.2 by A27,A29,A80,A81,RVSUM_1:44;
B = |[(1-m3)*C.1 + m3 * A.1,(1-m3)*C.2+m3 * A.2]|
by A79,A82,EUCLID:53
.= |[(1-m3) * C.1,(1-m3)*C.2]| + |[m3 * A.1,m3 * A.2]| by EUCLID:56
.= (1 - m3) * |[C.1,C.2]| + |[m3 * A.1,m3 * A.2]| by EUCLID:58
.= (1 - m3) * C + m3 * A by EUCLID:58;
hence thesis by A76,TOPREAL9:26;
end;
then B in {C,A} by A40,A37,XBOOLE_0:def 4;
hence contradiction by A30,A32,TARSKI:def 2;
end;
end;
suppose
A85: c1 <> 0;
c1 * tr + a1 * tp + b1 * tq = 0.TOP-REAL 3 by A15,RVSUM_1:15;
then
A86: lr * vr = ((-a1)/c1) * (lp * vp) + ((-b1)/c1) * (lq * vq)
by A19,A21,A23,A85,ANPROJ_8:12
.= ((-a1)/c1)*lp * vp + ((-b1)/c1) * (lq * vq) by RVSUM_1:49
.= ((-a1)/c1)*lp * vp + ((-b1)/c1)* lq * vq by RVSUM_1:49;
reconsider m1 = 1/lr * (((-a1)/c1) * lp),
m2 = 1/lr * (((-b1)/c1)* lq) as Real;
1 = lr / lr by A22,XCMPLX_1:60
.= 1/lr * lr by XCMPLX_1:99; then
A87: vr = (1/lr * lr) * vr by RVSUM_1:52
.= 1/lr * (((-a1)/c1)*lp * vp + ((-b1)/c1)*lq * vq) by A86,RVSUM_1:49
.= 1/lr * (((-a1)/c1)*lp * vp) + 1/lr * (((-b1)/c1)*lq * vq)
by RVSUM_1:51
.= 1/lr * (((-a1)/c1)*lp) * vp + 1/lr * (((-b1)/c1)*lq * vq)
by RVSUM_1:49
.= m1 * vp + m2 * vq by RVSUM_1:49;
A88: m1 = 1 - m2
proof
m1 * vp + m2 * vq = |[m1 * vp`1,m1 * vp`2,m1 * vp`3]| + m2 * vq
by EUCLID_5:7
.= |[m1 * vp`1,m1 * vp`2,m1 * vp`3]|
+ |[m2 * vq`1,m2 * vq`2,m2 * vq`3]| by EUCLID_5:7
.= |[m1 * vp`1 + m2 * vq`1,
m1 * vp`2 + m2 * vq`2,
m1 * vp`3 + m2 * vq`3]| by EUCLID_5:6;
then 1 = m1 * 1 + m2 * 1 by A87,EUCLID_5:14,A9;
hence thesis;
end;
per cases;
suppose
A89: 0 <= m2;
C in halfline(A,B)
proof
reconsider tu = (1-m2)*vp, tv = m2*vq as Element of TOP-REAL 3;
A90: ((1 - m2) * vp).1 = (1-m2) * vp.1 by RVSUM_1:44;
A91: tu`1 = tu.1 & tv`1 = tv.1 by EUCLID_5:def 1;
A92: C`1 = vr`1 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`1 by A88,A87,EUCLID_5:5
.= tu.1 + tv.1 by A91,EUCLID_5:2
.= (1-m2) * A.1 + m2 * B.1 by A24,A28,A90,RVSUM_1:44;
A93: ((1 - m2) * vp).2 = (1-m2) * vp.2 by RVSUM_1:44;
A94: tu`2 = tu.2 & tv`2 = tv.2 by EUCLID_5:def 2;
A95: C`2 = vr`2 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`2 by A88,A87,EUCLID_5:5
.= tu`2 + tv`2 by EUCLID_5:2
.= (1-m2) * A.2 + m2 * B.2 by A25,A29,A93,A94,RVSUM_1:44;
C = |[C`1,C`2]| by EUCLID:53
.= |[(1-m2) * A.1,(1-m2)*A.2]| + |[m2 * B.1,m2 * B.2]|
by A92,A95,EUCLID:56
.= (1 - m2) * |[A.1,A.2]| + |[m2 * B.1,m2 * B.2]| by EUCLID:58
.= (1 - m2) * A + m2 * B by EUCLID:58;
hence thesis by A89,TOPREAL9:26;
end;
then C in {A,B} by A40,A38,XBOOLE_0:def 4;
hence contradiction by A31,A32,TARSKI:def 2;
end;
suppose
A98: m2 < 0;
set m3 = 1 - m2;
C in halfline(B,A)
proof
reconsider tu = (1-m3)*vq, tv = m3*vp as Element of TOP-REAL 3;
A99: ((1 - m3) * vq).1 = (1-m3) * vq.1 by RVSUM_1:44;
A100: tu`1 = tu.1 & tv`1 = tv.1 by EUCLID_5:def 1;
A101: C`1 = vr`1 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`1 by A88,A87,EUCLID_5:5
.= tu.1 + tv.1 by A100,EUCLID_5:2
.= (1-m3) * B.1 + m3 * A.1 by A24,A28,A99,RVSUM_1:44;
A102: ((1 - m3) * vq).2 = (1-m3) * vq.2 by RVSUM_1:44;
A103: tu`2 = tu.2 & tv`2 = tv.2 by EUCLID_5:def 2;
A104: C`2 = vr`2 by EUCLID:52
.= |[tu`1+tv`1,tu`2+tv`2,tu`3+tv`3]|`2 by A88,A87,EUCLID_5:5
.= tu`2 + tv`2 by EUCLID_5:2
.= (1-m3) * B.2 + m3 * A.2 by A25,A29,A102,A103,RVSUM_1:44;
C = |[(1-m3)*B.1 + m3 * A.1,(1-m3)*B.2+m3 * A.2]|
by A101,A104,EUCLID:53
.= |[(1-m3) * B.1,(1-m3)*B.2]| + |[m3 * A.1,m3 * A.2]| by EUCLID:56
.= (1 - m3) * |[B.1,B.2]| + |[m3 * A.1,m3 * A.2]| by EUCLID:58
.= (1 - m3) * B + m3 * A by EUCLID:58;
hence thesis by A98,TOPREAL9:26;
end;
then C in {B,A} by A40,A38,XBOOLE_0:def 4;
hence contradiction by A31,A32,TARSKI:def 2;
end;
end;
end;
theorem
for ra being non zero Real
for O,N,M being invertible Matrix of 3,F_Real st
O = symmetric_3(1,1,-1,0,0,0) & M = symmetric_3(ra,ra,-ra,0,0,0) &
M = N@ * O * N & homography(M).:absolute = absolute
holds homography(N).:absolute = absolute
proof
let ra be non zero Real;
let O,N,M be invertible Matrix of 3,F_Real;
assume that
A1: O = symmetric_3(1,1,-1,0,0,0) and
A2: M = symmetric_3(ra,ra,-ra,0,0,0) and
A4: M = N@ * O * N and
A5: homography(M).:absolute = absolute;
reconsider O1 = O as Matrix of 3,REAL;
A6: len O1 = 3 & width O1 = 3 by MATRIX_0:24;
A7: homography(N).:absolute c= absolute
proof
let x be object;assume x in homography(N).:absolute;
then consider y be object such that
A8: y in dom homography(N) and
A9: y in absolute and
A10: (homography(N)).y = x by FUNCT_1:def 6;
A11: 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 A8;
consider z be object such that
A12: z in dom homography(M) and
A13: z in absolute and
A14: (homography(M)).z = y by A9,A5,FUNCT_1:def 6;
reconsider z9 = z as Element of ProjectiveSpace TOP-REAL 3 by A12;
A15: x = (homography(N)).(homography(M).z9) by A14,A10
.= (homography(N*M)).z by ANPROJ_9:13;
reconsider NM = N * M as invertible Matrix of 3,F_Real;
reconsider NMR = NM as Matrix of 3,REAL;
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
A16: z9 = Dir u & u is not zero & u = uf & p = NM * uf & v = M2F p &
v is not zero & (homography(NM)).z9 = Dir v by ANPROJ_8:def 4;
reconsider u1 = u as FinSequence of REAL by EUCLID:24;
u is Element of REAL 3 by EUCLID:22; then
A17: len u1 = 3 by EUCLID_8:50;
reconsider x9 = x as Element of ProjectiveSpace TOP-REAL 3
by A10,A11,A8,FUNCT_1:3;
consider u9 be Element of TOP-REAL 3 such that
A18: u9 is not zero and
A19: x9 = Dir u9 by ANPROJ_1:26;
reconsider uf9 = u9 as FinSequence of REAL by EUCLID:24;
u9 is Element of REAL 3 by EUCLID:22;
then len uf9 = 3 by EUCLID_8:50; then
A20: len uf9 = len O1 & len uf9 = width O1 & len uf9 > 0 by MATRIX_0:24;
are_Prop u9,v by A19,A18,A16,ANPROJ_1:22,A15;
then consider b be Real such that
b <> 0 and
A21: u9 = b * v by ANPROJ_1:1;
reconsider vf = v as FinSequence of REAL by EUCLID:24;
A22: v is Element of REAL 3 by EUCLID:22; then
A23: len vf = 3 by EUCLID_8:50;
A24: width O1 = len vf & len vf > 0 by A6,A22,EUCLID_8:50;
|( uf9, O1 * uf9 )| = 0
proof
width O1 = len vf & len vf > 0 by A23,MATRIX_0:24; then
A25: len (O1 * vf) = len O1 by MATRIXR1:61
.= 3 by MATRIX_0:24; then
A26: len vf = len (b * (O1 * vf)) by A23,RVSUM_1:117;
A27: len vf = len (O1 * vf) by A25,A22,EUCLID_8:50;
A28: |( uf9, O1 * uf9 )| = |( b * vf, b * (O1 * vf) )|
by A21,A24,MATRIXR1:59
.= b * |( vf, b * (O1 * vf) )| by A26,RVSUM_1:121
.= b * (b * |(O1 * vf, vf)| ) by A27,RVSUM_1:121;
|( vf, O1 * vf )| = 0
proof
A29: len N > 0 & width N > 0 by MATRIX_0:24;
A30: (N@ * O * N)@ = (N@ * (N@ * O)@) by MATRIX14:30
.= (N@ * (O@ * N@@)) by MATRIX14:30
.= (N@ * (O@ * N)) by A29,MATRIX_0:57;
A31: len N = 3 & width N = 3 & len M = 3 & width M = 3 by MATRIX_0:24;
A32: len (O * (N * M)) = 3 by MATRIX_0:24;
A33: len O = 3 & width O = 3 & len N = 3 by MATRIX_0:24; then
A34: width (N@) = len O & width O = len N by MATRIX_0:24;
A35: width M = len (N@) & width (N@) = len (O * (N * M))
by A31,A32,MATRIX_0:29;
A36: width (N@) = len O & width O = len (N * M) by MATRIX_0:24,A33;
A37: width (N@ * O) = len N & width N = len M by A31,MATRIX_0:24;
A38: width M = 3 & len M = 3 by MATRIX_0:24;
reconsider ra3 = ra * ra * ra as Element of F_Real by XREAL_0:def 1;
reconsider ea = ra as Element of F_Real by XREAL_0:def 1;
A39: M = symmetric_3(ea,ea,-ea,0,0,0) by A2;
O1 * NMR = O * (N * M) by ANPROJ_8:17; then
A40: NMR@ * (O1 * NMR) = (N * M)@ * (O * (N * M)) by ANPROJ_8:17
.= ((N@ * (O@ * N)) * N@) * (O * (N * (N@ * O * N)))
by A30,A4,A31,MATRIX_3:22
.= ((N@ * (O * N)) * N@) * (O * (N * (N@ * O * N)))
by A1,PASCAL:12,MATRIX_6:def 5
.= (M * N@) * (O * (N * (N@ * O * N)))
by A4,A34,MATRIX_3:33
.= (M * ((N@) * (O * (N * M))))
by A4,A35,MATRIX_3:33
.= M * ((N@ * O) * (N * M)) by A36,MATRIX_3:33
.= M * ((N@ * O * N) * M) by A37,MATRIX_3:33
.= M * M * M by A4,A38,MATRIX_3:33
.= (ea * ea * ea) * symmetric_3(1,1,-1,0,0,0)
by A39,Th49
.= ra3 * O1 by Th46,A1;
reconsider ONMRUF9 = O1 * (NMR * u1) as FinSequence of REAL;
A41: u is Element of REAL 3 by EUCLID:22; then
A42: len u1 = 3 by EUCLID_8:50;
A43: width (NMR@) = 3 by MATRIX_0:24;
A44: width NMR = 3 & len NMR = 3 by MATRIX_0:24;
A45: len u1 = width (O1 * NMR) & len (O1 * NMR) = width (NMR@) &
len (O1 * NMR) > 0 & len u1 > 0 by A42,A43,MATRIX_0:24;
len u1 = width NMR & width O1 = len NMR & len u1 > 0 &
len NMR > 0 by A41,EUCLID_8:50,A44,MATRIX_0:24; then
A46: (NMR@) * (O1 * (NMR * u1)) = (NMR@) * ((O1 * NMR) * u1)
by MATRIXR2:59
.= (ra3 * O1) * u1
by A40,A45,MATRIXR2:59;
width O1 = len u1 & len u1 > 0 by A42,MATRIX_0:24;
then len (O1 * u1) = len O1 by MATRIXR1:61
.= 3 by MATRIX_0:24;
then
A47: len u1 = len (O1 * u1) by A41,EUCLID_8:50;
A48: len O1 = 3 by MATRIX_0:24;
width NMR = 3 by MATRIX_0:24; then
A49: len (NMR * u1) = len NMR by A42,MATRIXR1:61
.= 3 by MATRIX_0:24; then
A50: width O1 = len (NMR * u1) by MATRIX_0:24;
A51: len ONMRUF9 = len NMR & len u1 = width NMR & len u1 > 0 &
len ONMRUF9 > 0
by A44,A41,EUCLID_8:50,A49,A48,A50,MATRIXR1:61;
consider s1,s2,s3,s4,s5,s6,s7,s8,s9 be Element of F_Real such that
A52: NM = <* <* s1,s2,s3 *>,
<* s4,s5,s6 *>,
<* s7,s8,s9 *> *> by PASCAL:3;
consider t1,t2,t3 be Real such that
A53: u = <* t1,t2,t3 *> by EUCLID_5:1;
reconsider et1 = t1, et2 = t2, et3 = t3 as Element of F_Real
by XREAL_0:def 1;
A54: vf = <* s1 * et1 + s2 * et2 + s3 * et3,
s4 * et1 + s5 * et2 + s6 * et3,
s7 * et1 + s8 * et2 + s9 * et3 *>
by A16,A52,A53,PASCAL:8;
reconsider rs1 = s1, rs2 = s2, rs3 = s3,
rs4 = s4, rs5 = s5, rs6 = s6,
rs7 = s7, rs8 = s8, rs9 = s9 as Element of REAL;
reconsider rt1 = t1, rt2 = t2, rt3 = t3 as Element of REAL
by XREAL_0:def 1;
NMR * u1 = <* rs1 * rt1 + rs2 * rt2 + rs3 * rt3,
rs4 * rt1 + rs5 * rt2 + rs6 * rt3,
rs7 * rt1 + rs8 * rt2 + rs9 * rt3 *>
by A53,A52,PASCAL:9; then
A55: |( vf, O1 * vf )| = |( u1, NMR@ * ONMRUF9 )|
by A54,A51,MATRPROB:48
.= |( u1, ra3 * (O1 * u1) )|
by A17,A46,Th51
.= ra3 * |( u1, O1 * u1 )| by RVSUM_1:121,A47;
A56: len u1 = len O1 & len u1 = width O1 & len u1 > 0
by A42,MATRIX_0:24;
0 = SumAll QuadraticForm(u1,O1,u1) by A16,A13,A1,Th66
.= |( u1, O1 * u1)| by A56,MATRPROB:44;
hence thesis by A55;
end;
hence thesis by A28;
end;
then SumAll QuadraticForm(uf9,O1,uf9) = 0 by A20,MATRPROB:44;
hence thesis by A18,A19,A1,Th66;
end;
absolute c= homography(N).:absolute
proof
let x be object;
assume
A57: x in absolute;
then x 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) = 0} by PASCAL:def 2;
then consider Q being Point of ProjectiveSpace TOP-REAL 3 such that
A58: x = Q and
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) = 0;
reconsider P = homography(N~).Q as
Element of ProjectiveSpace TOP-REAL 3;
A59: homography(N).P = x by A58,ANPROJ_9:15;
consider u2,v2 be Element of TOP-REAL 3,
uf2 be FinSequence of F_Real,
p2 be FinSequence of 1-tuples_on REAL such that
A60: Q = Dir u2 & u2 is not zero & u2 = uf2 & p2 = (N~) * uf2 &
v2 = M2F p2 & v2 is not zero & (homography(N~)).Q = Dir v2
by ANPROJ_8:def 4;
reconsider vf2 = v2 as FinSequence of REAL by EUCLID:24;
v2 in TOP-REAL 3;
then v2 in REAL 3 by EUCLID:22;
then len vf2 = 3 by EUCLID_8:50; then
A61: len vf2 = len O1 & len vf2 = width O1 & len vf2 > 0 by MATRIX_0:24;
|( vf2, O1 * vf2 )| = 0
proof
reconsider uf3 = uf2 as FinSequence of REAL;
A62: len O1 = 3 & width O1 = 3 by MATRIX_0:24;
u2 in TOP-REAL 3; then
A63: u2 in REAL 3 by EUCLID:22; then
A64: len uf2 = 3 by A60,EUCLID_8:50;
A65: len uf3 = len O1 by A63,A62,A60,EUCLID_8:50;
A66: SumAll QuadraticForm(uf3,O1,uf3) = 0
by A1,A58,A57,A60,Th66;
A67: len (O1 * uf3) = len uf3 by A62,A65,MATRIXR1:61;
reconsider NR = N as Matrix of 3,REAL;
reconsider NI = N~ as Matrix of 3,3,REAL;
A68: N~ is_reverse_of N by MATRIX_6:def 4;
A69: NI * NR = (N~) * N by ANPROJ_8:17
.= 1.(F_Real,3) by A68,MATRIX_6:def 2
.= MXF2MXR 1.(F_Real,3) by MATRIXR1:def 2
.= 1_Rmatrix(3) by MATRIXR2:def 2;
A70: NR * NI = N * (N~) by ANPROJ_8:17
.= 1.(F_Real,3) by A68,MATRIX_6:def 2
.= MXF2MXR 1.(F_Real,3) by MATRIXR1:def 2
.= 1_Rmatrix(3) by MATRIXR2:def 2;
then NR is invertible by A69,MATRIXR2:def 5; then
A71: Inv(NR) = NI by A69,A70,MATRIXR2:def 6;
reconsider ea = ra as Element of F_Real by XREAL_0:def 1;
M = symmetric_3(ea,ea,-ea,0,0,0) by A2; then
A72: M = ea * O by A1,Th48
.= ea * MXR2MXF O1 by MATRIXR1:def 1
.= MXF2MXR (ea * MXR2MXF O1) by MATRIXR1:def 2
.= ra * O1 by MATRIXR1:def 7;
N@ * O = NR@ * O1 by ANPROJ_8:17; then
A73: M = NR@ * O1 * NR by A4,ANPROJ_8:17;
width (NI@ * O1) = 3 by MATRIXR2:4; then
A75: len uf3 = width NI & width (NI@ * O1) = len NI &
len uf3 > 0 & len NI > 0 by A64,MATRIX_0:24;
width NI = len uf3 & len uf3 > 0 & len NI = 3 by A64,MATRIX_0:24;
then
A76: len (NI * uf3) = 3 & width O1 = 3 & len O1 = 3 &
width (NI@) = 3 by MATRIX_0:24,MATRIXR1:61;
width NI = len uf3 & len uf3 > 0 by A64,MATRIX_0:24;
then len (NI * uf3) = len NI by MATRIXR1:61
.= 3 by MATRIX_0:24;
then width O1 = len (NI * uf3) & len (NI * uf3) > 0 by MATRIX_0:24;
then len (O1 * (NI * uf3)) = len O1 by MATRIXR1:61
.= 3 by MATRIX_0:24; then
A77: len (O1 * (NI * uf3)) = len NI & len uf3 = width NI &
len uf3 > 0 & len (O1 * (NI * uf3)) > 0 by A64,MATRIX_0:24;
vf2 = NI * uf3
proof
consider s1,s2,s3,s4,s5,s6,s7,s8,s9 be Element of F_Real such that
A78: N~ = <* <* s1,s2,s3 *>,
<* s4,s5,s6 *>,
<* s7,s8,s9 *> *> by PASCAL:3;
consider t1,t2,t3 be Real such that
A79: u2 = <* t1,t2,t3 *> by EUCLID_5:1;
reconsider et1 = t1, et2 = t2, et3 = t3 as Element of F_Real
by XREAL_0:def 1;
vf2 = <* s1 * et1 + s2 * et2 + s3 * et3,
s4 * et1 + s5 * et2 + s6 * et3,
s7 * et1 + s8 * et2 + s9 * et3 *>
by A60,A78,A79,PASCAL:8;
hence thesis by A78,A79,A60,PASCAL:9;
end;
then |( vf2, O1 * vf2 )| = |( uf3, NI@ * (O1 * (NI * uf3)) )|
by A77,MATRPROB:48
.= |( uf3, (NI@ * O1) * (NI * uf3) )|
by A76,MATRIXR2:59
.= |( uf3, (NI@ * O1 * NI) * uf3 )|
by A75,MATRIXR2:59
.= |( uf3, (1/ra * O1) * uf3 )|
by A73,A69,A70,MATRIXR2:def 5,A72,Th53,A71
.= |( (1/ra) * (O1 * uf3), uf3 )|
by A64,Th51
.= 1/ra * |( O1 * uf3, uf3 )|
by A67,RVSUM_1:121
.= 1/ra * 0
by A66,A62,A65,MATRPROB:44
.= 0;
hence thesis;
end;
then SumAll QuadraticForm(vf2,O1,vf2) = 0 by A61,MATRPROB:44;
then
A80: P in absolute by A1,A60,Th66;
dom homography(N) = the carrier of ProjectiveSpace TOP-REAL 3
by FUNCT_2:def 1;
hence thesis by A59,A80,FUNCT_1:def 6;
end;
hence thesis by A7;
end;