let P1, P2, P3 be Point of (ProjectiveSpace (TOP-REAL 3)); ( not P1,P2,P3 are_collinear implies ex N being invertible Matrix of 3,F_Real st
( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 ) )
assume A1:
not P1,P2,P3 are_collinear
; ex N being invertible Matrix of 3,F_Real st
( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 )
consider u1 being Element of (TOP-REAL 3) such that
A2:
not u1 is zero
and
A3:
P1 = Dir u1
by ANPROJ_1:26;
consider u2 being Element of (TOP-REAL 3) such that
A4:
not u2 is zero
and
A5:
P2 = Dir u2
by ANPROJ_1:26;
consider u3 being Element of (TOP-REAL 3) such that
A6:
not u3 is zero
and
A7:
P3 = Dir u3
by ANPROJ_1:26;
A8:
|{u1,u2,u3}| <> 0
by ANPROJ_8:43, A1, A2, A3, A4, A5, A6, A7, ANPROJ_2:23;
reconsider pf = u1, qf = u2, rf = u3 as FinSequence of F_Real by RVSUM_1:145;
consider N being Matrix of 3,F_Real such that
A9:
N is invertible
and
A10:
N * pf = F2M <e1>
and
A11:
N * qf = F2M <e2>
and
A12:
N * rf = F2M <e3>
by A8, ANPROJ_8:94;
reconsider N = N as invertible Matrix of 3,F_Real by A9;
A13:
( len <e1> = 3 & len <e2> = 3 & len <e3> = 3 )
by EUCLID_8:50;
take
N
; ( (homography N) . P1 = Dir100 & (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 )
thus
(homography N) . P1 = Dir100
( (homography N) . P2 = Dir010 & (homography N) . P3 = Dir001 )proof
consider nu1,
nv1 being
Element of
(TOP-REAL 3),
u1f being
FinSequence of
F_Real,
p1 being
FinSequence of 1
-tuples_on REAL such that A14:
P1 = Dir nu1
and A15:
not
nu1 is
zero
and A16:
nu1 = u1f
and A17:
p1 = N * u1f
and A18:
nv1 = M2F p1
and A19:
not
nv1 is
zero
and A20:
(homography N) . P1 = Dir nv1
by ANPROJ_8:def 4;
are_Prop u1,
nu1
by A2, A3, A14, A15, ANPROJ_1:22;
then consider a being
Real such that A21:
a <> 0
and A22:
u1 = a * nu1
by ANPROJ_1:1;
reconsider b = 1
/ a as
Real ;
nu1 in TOP-REAL 3
;
then A23:
nu1 in REAL 3
by EUCLID:22;
width <*u1f*> =
len nu1
by A16, ANPROJ_8:75
.=
3
by A23, EUCLID_8:50
;
then A24:
len (<*u1f*> @) =
width <*u1f*>
by MATRIX_0:29
.=
len nu1
by ANPROJ_8:75, A16
.=
3
by A23, EUCLID_8:50
;
A25:
width N = len (<*u1f*> @)
by MATRIX_0:24, A24;
A26:
len (N * u1f) =
len (N * (<*u1f*> @))
by LAPLACE:def 9
.=
len N
by A25, MATRIX_3:def 4
.=
3
by MATRIX_0:24
;
len <e1> = 3
by EUCLID_8:def 1, FINSEQ_1:45;
then A27:
F2M <e1> = <*<*(<e1> . 1)*>,<*(<e1> . 2)*>,<*(<e1> . 3)*>*>
by ANPROJ_8:def 1;
reconsider s1 =
u1f . 1,
s2 =
u1f . 2,
s3 =
u1f . 3 as
Element of
F_Real by XREAL_0:def 1;
reconsider t1 =
u1 . 1,
t2 =
u1 . 2,
t3 =
u1 . 3 as
Element of
F_Real by XREAL_0:def 1;
A28:
(
(N * pf) . 1
= <*(<e1> . 1)*> &
(N * pf) . 2
= <*(<e1> . 2)*> &
(N * pf) . 3
= <*(<e1> . 3)*> )
by A10, A27, FINSEQ_1:45;
A29:
((N * pf) . 1) . 1 =
|[1,0,0]| . 1
by A28, FINSEQ_1:40, EUCLID_8:def 1
.=
|[1,0,0]| `1
by EUCLID_5:def 1
.=
1
by EUCLID_5:2
;
A30:
((N * pf) . 2) . 1 =
|[1,0,0]| . 2
by A28, FINSEQ_1:40, EUCLID_8:def 1
.=
|[1,0,0]| `2
by EUCLID_5:def 2
.=
0
by EUCLID_5:2
;
A31:
((N * pf) . 3) . 1 =
|[1,0,0]| . 3
by A28, FINSEQ_1:40, EUCLID_8:def 1
.=
|[1,0,0]| `3
by EUCLID_5:def 3
.=
0
by EUCLID_5:2
;
(
p1 . 1
= <*((N * (<*u1f*> @)) * (1,1))*> &
p1 . 2
= <*((N * (<*u1f*> @)) * (2,1))*> &
p1 . 3
= <*((N * (<*u1f*> @)) * (3,1))*> )
by A16, A17, FINSEQ_1:1, Lem02;
then reconsider p111 =
(p1 . 1) . 1,
p121 =
(p1 . 2) . 1,
p131 =
(p1 . 3) . 1 as
Real ;
A32:
(
p111 = b * ((Line (N,1)) "*" pf) &
p121 = b * ((Line (N,2)) "*" pf) &
p131 = b * ((Line (N,3)) "*" pf) )
by FINSEQ_1:1, A16, A17, A21, A22, Lem04;
A33:
a * p1 = N * pf
len <e1> = 3
by EUCLID_8:50;
then A38:
<e1> =
M2F (F2M <e1>)
by ANPROJ_8:86
.=
a * nv1
by A18, A33, A10, A26, A17, ANPROJ_8:83
;
( not
nv1 is
zero & not
a * nv1 is
zero &
are_Prop nv1,
a * nv1 )
by A19, A21, Th04, ANPROJ_1:1;
hence
(homography N) . P1 = Dir100
by A38, EUCLID_8:def 1, ANPROJ_1:22, A20;
verum
end;
thus
(homography N) . P2 = Dir010
(homography N) . P3 = Dir001 proof
consider nu2,
nv2 being
Element of
(TOP-REAL 3),
u2f being
FinSequence of
F_Real,
p2 being
FinSequence of 1
-tuples_on REAL such that A39:
P2 = Dir nu2
and A40:
not
nu2 is
zero
and A41:
nu2 = u2f
and A42:
p2 = N * u2f
and A43:
nv2 = M2F p2
and A44:
not
nv2 is
zero
and A45:
(homography N) . P2 = Dir nv2
by ANPROJ_8:def 4;
are_Prop u2,
nu2
by A4, A5, A39, A40, ANPROJ_1:22;
then consider a being
Real such that A46:
a <> 0
and A47:
u2 = a * nu2
by ANPROJ_1:1;
reconsider b = 1
/ a as
Real ;
nu2 in TOP-REAL 3
;
then A48:
nu2 in REAL 3
by EUCLID:22;
width <*u2f*> =
len nu2
by A41, ANPROJ_8:75
.=
3
by A48, EUCLID_8:50
;
then A49:
len (<*u2f*> @) =
width <*u2f*>
by MATRIX_0:29
.=
len nu2
by ANPROJ_8:75, A41
.=
3
by A48, EUCLID_8:50
;
A50:
width N = len (<*u2f*> @)
by MATRIX_0:24, A49;
A51:
len (N * u2f) =
len (N * (<*u2f*> @))
by LAPLACE:def 9
.=
len N
by A50, MATRIX_3:def 4
.=
3
by MATRIX_0:24
;
len <e2> = 3
by EUCLID_8:def 2, FINSEQ_1:45;
then A52:
F2M <e2> = <*<*(<e2> . 1)*>,<*(<e2> . 2)*>,<*(<e2> . 3)*>*>
by ANPROJ_8:def 1;
reconsider s1 =
u2f . 1,
s2 =
u2f . 2,
s3 =
u2f . 3 as
Element of
F_Real by XREAL_0:def 1;
reconsider t1 =
u2 . 1,
t2 =
u2 . 2,
t3 =
u2 . 3 as
Element of
F_Real by XREAL_0:def 1;
A53:
(
(N * qf) . 1
= <*(<e2> . 1)*> &
(N * qf) . 2
= <*(<e2> . 2)*> &
(N * qf) . 3
= <*(<e2> . 3)*> )
by A11, A52, FINSEQ_1:45;
A54:
((N * qf) . 1) . 1 =
|[0,1,0]| . 1
by A53, FINSEQ_1:40, EUCLID_8:def 2
.=
|[0,1,0]| `1
by EUCLID_5:def 1
.=
0
by EUCLID_5:2
;
A55:
((N * qf) . 2) . 1 =
|[0,1,0]| . 2
by A53, FINSEQ_1:40, EUCLID_8:def 2
.=
|[0,1,0]| `2
by EUCLID_5:def 2
.=
1
by EUCLID_5:2
;
A56:
((N * qf) . 3) . 1 =
|[0,1,0]| . 3
by A53, FINSEQ_1:40, EUCLID_8:def 2
.=
|[0,1,0]| `3
by EUCLID_5:def 3
.=
0
by EUCLID_5:2
;
(
p2 . 1
= <*((N * (<*u2f*> @)) * (1,1))*> &
p2 . 2
= <*((N * (<*u2f*> @)) * (2,1))*> &
p2 . 3
= <*((N * (<*u2f*> @)) * (3,1))*> )
by A41, A42, FINSEQ_1:1, Lem02;
then reconsider p211 =
(p2 . 1) . 1,
p221 =
(p2 . 2) . 1,
p231 =
(p2 . 3) . 1 as
Real ;
A57:
(
p211 = b * ((Line (N,1)) "*" qf) &
p221 = b * ((Line (N,2)) "*" qf) &
p231 = b * ((Line (N,3)) "*" qf) )
by FINSEQ_1:1, A41, A42, A46, A47, Lem04;
A58:
a * p2 = N * qf
proof
consider pp1,
pp2,
pp3 being
Real such that A59:
pp1 = (p2 . 1) . 1
and A60:
pp2 = (p2 . 2) . 1
and A61:
pp3 = (p2 . 3) . 1
and A62:
a * p2 = <*<*(a * pp1)*>,<*(a * pp2)*>,<*(a * pp3)*>*>
by A42, A51, ANPROJ_8:def 3;
now ( len (N * qf) = 3 & (N * qf) . 1 = <*(a * pp1)*> & (N * qf) . 2 = <*(a * pp2)*> & (N * qf) . 3 = <*(a * pp3)*> )thus
len (N * qf) = 3
by A11, A13, ANPROJ_8:78;
( (N * qf) . 1 = <*(a * pp1)*> & (N * qf) . 2 = <*(a * pp2)*> & (N * qf) . 3 = <*(a * pp3)*> )
(Line (N,1)) "*" qf = ((N * qf) . 1) . 1
by FINSEQ_1:1, Lem05;
hence
(N * qf) . 1
= <*(a * pp1)*>
by A59, FINSEQ_1:40, A53, A57, A54;
( (N * qf) . 2 = <*(a * pp2)*> & (N * qf) . 3 = <*(a * pp3)*> )thus
(N * qf) . 2
= <*(a * pp2)*>
(N * qf) . 3 = <*(a * pp3)*>
(Line (N,3)) "*" qf = ((N * qf) . 3) . 1
by FINSEQ_1:1, Lem05;
hence
(N * qf) . 3
= <*(a * pp3)*>
by A61, FINSEQ_1:40, A53, A57, A56;
verum end;
hence
a * p2 = N * qf
by A62, FINSEQ_1:45;
verum
end;
len <e2> = 3
by EUCLID_8:50;
then A63:
<e2> =
M2F (F2M <e2>)
by ANPROJ_8:86
.=
a * nv2
by A43, A58, A11, A51, A42, ANPROJ_8:83
;
( not
nv2 is
zero & not
a * nv2 is
zero &
are_Prop nv2,
a * nv2 )
by A44, A46, Th04, ANPROJ_1:1;
hence
(homography N) . P2 = Dir010
by A63, EUCLID_8:def 2, ANPROJ_1:22, A45;
verum
end;
thus
(homography N) . P3 = Dir001
verumproof
consider nu3,
nv3 being
Element of
(TOP-REAL 3),
u3f being
FinSequence of
F_Real,
p3 being
FinSequence of 1
-tuples_on REAL such that A64:
P3 = Dir nu3
and A65:
not
nu3 is
zero
and A66:
nu3 = u3f
and A67:
p3 = N * u3f
and A68:
nv3 = M2F p3
and A69:
not
nv3 is
zero
and A70:
(homography N) . P3 = Dir nv3
by ANPROJ_8:def 4;
are_Prop u3,
nu3
by A6, A7, A64, A65, ANPROJ_1:22;
then consider a being
Real such that A71:
a <> 0
and A72:
u3 = a * nu3
by ANPROJ_1:1;
reconsider b = 1
/ a as
Real ;
nu3 in TOP-REAL 3
;
then A73:
nu3 in REAL 3
by EUCLID:22;
width <*u3f*> =
len nu3
by A66, ANPROJ_8:75
.=
3
by A73, EUCLID_8:50
;
then A74:
len (<*u3f*> @) =
width <*u3f*>
by MATRIX_0:29
.=
len nu3
by ANPROJ_8:75, A66
.=
3
by A73, EUCLID_8:50
;
A75:
width N = len (<*u3f*> @)
by MATRIX_0:24, A74;
A76:
len (N * u3f) =
len (N * (<*u3f*> @))
by LAPLACE:def 9
.=
len N
by A75, MATRIX_3:def 4
.=
3
by MATRIX_0:24
;
len <e3> = 3
by EUCLID_8:def 3, FINSEQ_1:45;
then A77:
F2M <e3> = <*<*(<e3> . 1)*>,<*(<e3> . 2)*>,<*(<e3> . 3)*>*>
by ANPROJ_8:def 1;
reconsider s1 =
u3f . 1,
s2 =
u3f . 2,
s3 =
u3f . 3 as
Element of
F_Real by XREAL_0:def 1;
reconsider t1 =
u3 . 1,
t2 =
u3 . 2,
t3 =
u3 . 3 as
Element of
F_Real by XREAL_0:def 1;
A78:
(
(N * rf) . 1
= <*(<e3> . 1)*> &
(N * rf) . 2
= <*(<e3> . 2)*> &
(N * rf) . 3
= <*(<e3> . 3)*> )
by A12, A77, FINSEQ_1:45;
A79:
((N * rf) . 1) . 1 =
|[0,0,1]| . 1
by A78, FINSEQ_1:40, EUCLID_8:def 3
.=
|[0,0,1]| `1
by EUCLID_5:def 1
.=
0
by EUCLID_5:2
;
A80:
((N * rf) . 2) . 1 =
|[0,0,1]| . 2
by A78, FINSEQ_1:40, EUCLID_8:def 3
.=
|[0,0,1]| `2
by EUCLID_5:def 2
.=
0
by EUCLID_5:2
;
A81:
((N * rf) . 3) . 1 =
|[0,0,1]| . 3
by A78, FINSEQ_1:40, EUCLID_8:def 3
.=
|[0,0,1]| `3
by EUCLID_5:def 3
.=
1
by EUCLID_5:2
;
(
p3 . 1
= <*((N * (<*u3f*> @)) * (1,1))*> &
p3 . 2
= <*((N * (<*u3f*> @)) * (2,1))*> &
p3 . 3
= <*((N * (<*u3f*> @)) * (3,1))*> )
by A66, A67, FINSEQ_1:1, Lem02;
then reconsider p311 =
(p3 . 1) . 1,
p321 =
(p3 . 2) . 1,
p331 =
(p3 . 3) . 1 as
Real ;
A82:
(
p311 = b * ((Line (N,1)) "*" rf) &
p321 = b * ((Line (N,2)) "*" rf) &
p331 = b * ((Line (N,3)) "*" rf) )
by FINSEQ_1:1, A66, A67, A71, A72, Lem04;
A83:
a * p3 = N * rf
proof
consider pp1,
pp2,
pp3 being
Real such that A84:
pp1 = (p3 . 1) . 1
and A85:
pp2 = (p3 . 2) . 1
and A86:
pp3 = (p3 . 3) . 1
and A87:
a * p3 = <*<*(a * pp1)*>,<*(a * pp2)*>,<*(a * pp3)*>*>
by A67, A76, ANPROJ_8:def 3;
now ( len (N * rf) = 3 & (N * rf) . 1 = <*(a * pp1)*> & (N * rf) . 2 = <*(a * pp2)*> & (N * rf) . 3 = <*(a * pp3)*> )thus
len (N * rf) = 3
by A12, A13, ANPROJ_8:78;
( (N * rf) . 1 = <*(a * pp1)*> & (N * rf) . 2 = <*(a * pp2)*> & (N * rf) . 3 = <*(a * pp3)*> )
(Line (N,1)) "*" rf = ((N * rf) . 1) . 1
by FINSEQ_1:1, Lem05;
hence
(N * rf) . 1
= <*(a * pp1)*>
by A84, FINSEQ_1:40, A78, A82, A79;
( (N * rf) . 2 = <*(a * pp2)*> & (N * rf) . 3 = <*(a * pp3)*> )
(Line (N,2)) "*" rf = ((N * rf) . 2) . 1
by FINSEQ_1:1, Lem05;
hence
(N * rf) . 2
= <*(a * pp2)*>
by A85, FINSEQ_1:40, A78, A82, A80;
(N * rf) . 3 = <*(a * pp3)*>thus
(N * rf) . 3
= <*(a * pp3)*>
verum end;
hence
a * p3 = N * rf
by A87, FINSEQ_1:45;
verum
end;
len <e3> = 3
by EUCLID_8:50;
then A88:
<e3> =
M2F (F2M <e3>)
by ANPROJ_8:86
.=
a * nv3
by A68, A83, A12, A76, A67, ANPROJ_8:83
;
( not
nv3 is
zero & not
a * nv3 is
zero &
are_Prop nv3,
a * nv3 )
by A69, A71, Th04, ANPROJ_1:1;
hence
(homography N) . P3 = Dir001
by A88, EUCLID_8:def 3, ANPROJ_1:22, A70;
verum
end;