let N be invertible Matrix of 3,F_Real; ( N = <*<*(2 / 3),0,(- (1 / 3))*>,<*0,(1 / (sqrt 3)),0*>,<*(1 / 3),0,(- (2 / 3))*>*> implies (homography N) .: absolute c= absolute )
assume A1:
N = <*<*(2 / 3),0,(- (1 / 3))*>,<*0,(1 / (sqrt 3)),0*>,<*(1 / 3),0,(- (2 / 3))*>*>
; (homography N) .: absolute c= absolute
reconsider a = 2 / 3, b = 0 , c = - (1 / 3), d = 0 , e = 1 / (sqrt 3), f = 0 , g = 1 / 3, h = 0 , i = - (2 / 3) as Element of F_Real by XREAL_0:def 1;
(homography N) .: absolute c= absolute
proof
let x be
object ;
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 A2:
y in dom (homography N)
and A3:
y in absolute
and A4:
x = (homography N) . y
by FUNCT_1:def 6;
reconsider y =
y as
Point of
(ProjectiveSpace (TOP-REAL 3)) by A2;
consider yu being non
zero Element of
(TOP-REAL 3) such that A5:
((yu . 1) ^2) + ((yu . 2) ^2) = 1
and A6:
yu . 3
= 1
and A7:
y = Dir yu
by A3, BKMODEL1:89;
A8:
((yu `1) * (yu `1)) + ((yu `2) * (yu `2)) =
((yu . 1) * (yu `1)) + ((yu `2) * (yu `2))
by EUCLID_5:def 1
.=
((yu . 1) * (yu . 1)) + ((yu `2) * (yu `2))
by EUCLID_5:def 1
.=
((yu . 1) * (yu . 1)) + ((yu . 2) * (yu `2))
by EUCLID_5:def 2
.=
((yu . 1) * (yu . 1)) + ((yu . 2) * (yu . 2))
by EUCLID_5:def 2
.=
((yu . 1) ^2) + ((yu . 2) * (yu . 2))
by SQUARE_1:def 1
.=
1
by A5, SQUARE_1:def 1
;
A9:
(yu `3) * (yu `3) =
(yu . 3) * (yu `3)
by EUCLID_5:def 3
.=
1
by A6, EUCLID_5:def 3
;
consider u,
v being
Element of
(TOP-REAL 3),
uf being
FinSequence of
F_Real,
p being
FinSequence of 1
-tuples_on REAL such that A10:
(
y = Dir u & not
u is
zero &
u = uf &
p = N * uf &
v = M2F p & not
v is
zero &
(homography N) . y = Dir v )
by ANPROJ_8:def 4;
are_Prop u,
yu
by A7, A10, ANPROJ_1:22;
then consider l being
Real such that
l <> 0
and A11:
u = l * yu
by ANPROJ_1:1;
reconsider u1 =
l * (yu `1),
u2 =
l * (yu `2),
u3 =
l * (yu `3) as
Element of
F_Real by XREAL_0:def 1;
uf = <*u1,u2,u3*>
by A11, A10, EUCLID_5:7;
then v =
<*(((a * u1) + (b * u2)) + (c * u3)),(((d * u1) + (e * u2)) + (f * u3)),(((g * u1) + (h * u2)) + (i * u3))*>
by A1, A10, PASCAL:8
.=
<*(((2 / 3) * u1) - ((1 / 3) * u3)),((1 / (sqrt 3)) * u2),(((1 / 3) * u1) - ((2 / 3) * u3))*>
;
then
(
v `1 = ((2 / 3) * u1) - ((1 / 3) * u3) &
v `2 = (1 / (sqrt 3)) * u2 &
v `3 = ((1 / 3) * u1) - ((2 / 3) * u3) )
by EUCLID_5:2;
then A12:
(
v . 1
= ((2 / 3) * u1) - ((1 / 3) * u3) &
v . 2
= (1 / (sqrt 3)) * u2 &
v . 3
= ((1 / 3) * u1) - ((2 / 3) * u3) )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
set k =
(1 / 3) * (1 / 3);
1
/ (sqrt 3) = (sqrt 3) / 3
by BKMODEL3:10;
then A13:
(1 / (sqrt 3)) * (1 / (sqrt 3)) =
((1 / 3) * (1 / 3)) * ((sqrt 3) * (sqrt 3))
.=
((1 / 3) * (1 / 3)) * (sqrt (3 * 3))
by SQUARE_1:29
.=
((1 / 3) * (1 / 3)) * (sqrt (3 ^2))
by SQUARE_1:def 1
.=
((1 / 3) * (1 / 3)) * 3
by SQUARE_1:def 2
;
A14:
(v . 2) * (v . 2) =
(((1 / (sqrt 3)) * (1 / (sqrt 3))) * u2) * u2
by A12
.=
((((1 / 3) * (1 / 3)) * 3) * u2) * u2
by A13
;
reconsider P =
(homography N) . y as
Point of
(ProjectiveSpace (TOP-REAL 3)) ;
qfconic (1,1,
(- 1),
0,
0,
0,
v)
= 0
proof
qfconic (1,1,
(- 1),
0,
0,
0,
v) =
((((((1 * (v . 1)) * (v . 1)) + ((1 * (v . 2)) * (v . 2))) + (((- 1) * (v . 3)) * (v . 3))) + ((0 * (v . 1)) * (v . 2))) + ((0 * (v . 1)) * (v . 3))) + ((0 * (v . 2)) * (v . 3))
by PASCAL:def 1
.=
((((1 / 3) * (1 / 3)) * ((((4 * u1) * u1) - ((4 * u1) * u3)) + (u3 * u3))) + (((((1 / 3) * (1 / 3)) * 3) * u2) * u2)) - (((1 / 3) * (1 / 3)) * (((u1 * u1) - ((4 * u1) * u3)) + ((4 * u3) * u3)))
by A12, A14
.=
((((1 / 3) * (1 / 3)) * 3) * (l * l)) * ((((yu `1) * (yu `1)) + ((yu `2) * (yu `2))) - ((yu `3) * (yu `3)))
.=
0
by A8, A9
;
hence
qfconic (1,1,
(- 1),
0,
0,
0,
v)
= 0
;
verum
end;
hence
x in absolute
by A4, A10, PASCAL:11;
verum
end;
hence
(homography N) .: absolute c= absolute
; verum