let N be invertible Matrix of 3,F_Real; :: thesis: 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
let NR be Matrix of 3,REAL; :: thesis: 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
let P, Q be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: 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
let u, v be non zero Element of (TOP-REAL 3); :: thesis: 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
let vfr, ufr be FinSequence of REAL ; :: thesis: 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
let a be non zero Real; :: thesis: ( P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = a * vfr implies (homography N) . P = Q )
assume A1: ( P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = a * vfr ) ; :: thesis: (homography N) . P = Q
A2: NR is invertible by A1, ANPROJ_8:18;
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
A3: ( P = Dir u1 & not u1 is zero & u1 = u1f & p1 = N * u1f & v1 = M2F p1 & not v1 is 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 being 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: ( not w1 is zero & not w2 is 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 :: thesis: ( not avfr is zero & not v is zero & are_Prop avfr,v )
thus not avfr is zero :: thesis: ( not v is zero & are_Prop avfr,v )
proof
assume avfr is zero ; :: thesis: contradiction
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, EUCLID_5:4; :: thesis: verum
end;
thus not v is zero ; :: thesis: are_Prop avfr,v
( a <> 0 & a * v = avfr ) by A1;
hence are_Prop avfr,v by ANPROJ_1:1; :: thesis: verum
end;
hence (homography N) . P = Q by A1, A3, A6, A13, ANPROJ_1:22; :: thesis: verum