let ra be 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
let O, N, M be invertible Matrix of 3,F_Real; ( 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 implies (homography N) .: absolute = absolute )
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
; (homography N) .: 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 ;
TARSKI:def 3 ( not x in (homography N) .: absolute or x in absolute )
assume
x in (homography N) .: absolute
;
x in absolute
then consider y being
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 being
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 being
Element of
(TOP-REAL 3),
uf being
FinSequence of
F_Real,
p being
FinSequence of 1
-tuples_on REAL such that A16:
(
z9 = Dir u & not
u is
zero &
u = uf &
p = NM * uf &
v = M2F p & not
v is
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 being
Element of
(TOP-REAL 3) such that A18:
not
u9 is
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 being
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 being
Element of
F_Real such that A52:
NM = <*<*s1,s2,s3*>,<*s4,s5,s6*>,<*s7,s8,s9*>*>
by PASCAL:3;
consider t1,
t2,
t3 being
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
|(vf,(O1 * vf))| = 0
by A55;
verum
end;
hence
|(uf9,(O1 * uf9))| = 0
by A28;
verum
end;
then
SumAll (QuadraticForm (uf9,O1,uf9)) = 0
by A20, MATRPROB:44;
hence
x in absolute
by A18, A19, A1, Th66;
verum
end;
absolute c= (homography N) .: absolute
proof
let x be
object ;
TARSKI:def 3 ( not x in absolute or x in (homography N) .: absolute )
assume A57:
x in absolute
;
x in (homography N) .: absolute
then
x in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is 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 not
u is
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 being
Element of
(TOP-REAL 3),
uf2 being
FinSequence of
F_Real,
p2 being
FinSequence of 1
-tuples_on REAL such that A60:
(
Q = Dir u2 & not
u2 is
zero &
u2 = uf2 &
p2 = (N ~) * uf2 &
v2 = M2F p2 & not
v2 is
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 being
Element of
F_Real such that A78:
N ~ = <*<*s1,s2,s3*>,<*s4,s5,s6*>,<*s7,s8,s9*>*>
by PASCAL:3;
consider t1,
t2,
t3 being
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
vf2 = NI * uf3
by A78, A79, A60, PASCAL:9;
verum
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
|(vf2,(O1 * vf2))| = 0
;
verum
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
x in (homography N) .: absolute
by A59, A80, FUNCT_1:def 6;
verum
end;
hence
(homography N) .: absolute = absolute
by A7; verum