:: Homography in $\mathbbRP^2$
:: by Roland Coghetto
::
:: Copyright (c) 2016-2021 Association of Mizar Users

theorem Th1: :: ANPROJ_8:1
( [1,1] in [:(Seg 3),(Seg 3):] & [1,2] in [:(Seg 3),(Seg 3):] & [1,3] in [:(Seg 3),(Seg 3):] & [2,1] in [:(Seg 3),(Seg 3):] & [2,2] in [:(Seg 3),(Seg 3):] & [2,3] in [:(Seg 3),(Seg 3):] & [3,1] in [:(Seg 3),(Seg 3):] & [3,2] in [:(Seg 3),(Seg 3):] & [3,3] in [:(Seg 3),(Seg 3):] )
proof end;

theorem Th2: :: ANPROJ_8:2
( [1,1] in [:(Seg 3),(Seg 1):] & [2,1] in [:(Seg 3),(Seg 1):] & [3,1] in [:(Seg 3),(Seg 1):] )
proof end;

theorem Th3: :: ANPROJ_8:3
( [1,1] in [:(Seg 1),(Seg 3):] & [1,2] in [:(Seg 1),(Seg 3):] & [1,3] in [:(Seg 1),(Seg 3):] )
proof end;

theorem :: ANPROJ_8:4
for a, b, c being Real holds <*<*a*>,<*b*>,<*c*>*> is Matrix of 3,1,F_Real
proof end;

theorem Th4: :: ANPROJ_8:5
for a, b, c being Real
for N being Matrix of 3,1,F_Real st N = <*<*a*>,<*b*>,<*c*>*> holds
Col (N,1) = <*a,b,c*>
proof end;

theorem Th5: :: ANPROJ_8:6
for K being non empty multMagma
for a1, a2, a3, b1, b2, b3 being Element of K holds mlt (<*a1,a2,a3*>,<*b1,b2,b3*>) = <*(a1 * b1),(a2 * b2),(a3 * b3)*>
proof end;

theorem Th6: :: ANPROJ_8:7
for K being non empty right_complementable left_unital associative commutative Abelian add-associative right_zeroed doubleLoopStr
for a1, a2, a3, b1, b2, b3 being Element of K holds <*a1,a2,a3*> "*" <*b1,b2,b3*> = ((a1 * b1) + (a2 * b2)) + (a3 * b3)
proof end;

theorem Th7: :: ANPROJ_8:8
for M being Matrix of 3,F_Real
for N being Matrix of 3,1,F_Real st N = holds
M * N =
proof end;

theorem Th8: :: ANPROJ_8:9
for V being non trivial RealLinearSpace
for u, v, w being Element of V holds
( u,v,w are_LinDep iff ( u = v or u = w or v = w or {u,v,w} is linearly-dependent ) )
proof end;

theorem Th9: :: ANPROJ_8:10
for V being non trivial RealLinearSpace
for p, q, r being Element of () holds
( p,q,r are_collinear iff ex u, v, w being Element of V st
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ( u = v or u = w or v = w or {u,v,w} is linearly-dependent ) ) )
proof end;

theorem :: ANPROJ_8:11
for V being non trivial RealLinearSpace
for p, q, r being Element of () holds
( p,q,r are_collinear iff ex u, v, w being Element of V st
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) ) )
proof end;

theorem Th10: :: ANPROJ_8:12
for a, b, c being Real
for V being non trivial RealLinearSpace
for u, v, w being Element of V st a <> 0 & ((a * u) + (b * v)) + (c * w) = 0. V holds
u = (((- b) / a) * v) + (((- c) / a) * w)
proof end;

theorem Th11: :: ANPROJ_8:13
for a, b, c, d, e, f being Real st a <> 0 & ((a * b) + (c * d)) + (e * f) = 0 holds
b = (- ((c / a) * d)) - ((e / a) * f)
proof end;

theorem Th12: :: ANPROJ_8:14
for u, v, w being Point of () st ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. () & a <> 0 ) holds
|{u,v,w}| = 0
proof end;

theorem Th13: :: ANPROJ_8:15
for n being Nat holds dom () = Seg n
proof end;

theorem Th14: :: ANPROJ_8:16
for A being Matrix of F_Real holds MXR2MXF () = A
proof end;

theorem Th15: :: ANPROJ_8:17
for A, B being Matrix of F_Real
for RA, RB being Matrix of REAL st A = RA & B = RB holds
A * B = RA * RB
proof end;

theorem :: ANPROJ_8:18
for n being Nat
for M being Matrix of n,REAL
for N being Matrix of n,F_Real st M = N holds
( M is invertible iff N is invertible )
proof end;

theorem Th16: :: ANPROJ_8:19
for p1, p2, p3, q1, q2, q3, r1, r2, r3 being Real holds <*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*> is Matrix of 3,F_Real
proof end;

theorem Th17: :: ANPROJ_8:20
for M being Matrix of 3,F_Real
for p1, p2, p3, q1, q2, q3, r1, r2, r3 being Real st M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*> holds
( M * (1,1) = p1 & M * (1,2) = q1 & M * (1,3) = r1 & M * (2,1) = p2 & M * (2,2) = q2 & M * (2,3) = r2 & M * (3,1) = p3 & M * (3,2) = q3 & M * (3,3) = r3 )
proof end;

theorem Th18: :: ANPROJ_8:21
for p, q, r being Point of ()
for M being Matrix of 3,F_Real st M = <*p,q,r*> holds
( M * (1,1) = p 1 & M * (1,2) = p 2 & M * (1,3) = p 3 & M * (2,1) = q 1 & M * (2,2) = q 2 & M * (2,3) = q 3 & M * (3,1) = r 1 & M * (3,2) = r 2 & M * (3,3) = r 3 )
proof end;

theorem Th19: :: ANPROJ_8:22
for M being Matrix of 3,F_Real
for p1, p2, p3, q1, q2, q3, r1, r2, r3 being Real st M = <*<*p1,q1,r1*>,<*p2,q2,r2*>,<*p3,q3,r3*>*> holds
M @ = <*<*p1,p2,p3*>,<*q1,q2,q3*>,<*r1,r2,r3*>*>
proof end;

theorem Th20: :: ANPROJ_8:23
for p, q, r being Point of ()
for M being Matrix of 3,F_Real st M = <*p,q,r*> holds
M @ = <*<*(p 1),(q 1),(r 1)*>,<*(p 2),(q 2),(r 2)*>,<*(p 3),(q 3),(r 3)*>*>
proof end;

theorem Th21: :: ANPROJ_8:24
for M being Matrix of 3,F_Real holds lines M = {(Line (M,1)),(Line (M,2)),(Line (M,3))}
proof end;

theorem Th22: :: ANPROJ_8:25
for p, q, r being Point of ()
for M being Matrix of 3,F_Real st M = <*<*(p 1),(p 2),(p 3)*>,<*(q 1),(q 2),(q 3)*>,<*(r 1),(r 2),(r 3)*>*> holds
( Line (M,1) = p & Line (M,2) = q & Line (M,3) = r )
proof end;

theorem :: ANPROJ_8:26
for M being Matrix of 3,F_Real
for x being object holds
( x in lines (M @) iff ex i being Nat st
( i in Seg 3 & x = Col (M,i) ) )
proof end;

theorem Th23: :: ANPROJ_8:27
for p, q, r being Point of () holds |{p,q,r}| = (((((((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))
proof end;

:: Grassmann-Pl\{?}ucker-Relation in rank 3
theorem :: ANPROJ_8:28
for p, q, r, s, t being Point of () holds ((|{p,q,r}| * |{p,s,t}|) - (|{p,q,s}| * |{p,r,t}|)) + (|{p,q,t}| * |{p,r,s}|) = 0
proof end;

theorem Th24: :: ANPROJ_8:29
for p, q, r being Point of () holds |{p,q,r}| = - |{p,r,q}|
proof end;

theorem Th25: :: ANPROJ_8:30
for p, q, r being Point of () holds |{p,q,r}| = - |{q,p,r}|
proof end;

theorem Th26: :: ANPROJ_8:31
for a being Real
for p, q, r being Point of () holds |{(a * p),q,r}| = a * |{p,q,r}|
proof end;

theorem Th27: :: ANPROJ_8:32
for a being Real
for p, q, r being Point of () holds |{p,(a * q),r}| = a * |{p,q,r}|
proof end;

theorem Th28: :: ANPROJ_8:33
for a being Real
for p, q, r being Point of () holds |{p,q,(a * r)}| = a * |{p,q,r}|
proof end;

theorem :: ANPROJ_8:34
for p, q, r being Point of ()
for M being Matrix of 3,F_Real st M = <*<*(p 1),(q 1),(r 1)*>,<*(p 2),(q 2),(r 2)*>,<*(p 3),(q 3),(r 3)*>*> holds
|{p,q,r}| = Det M
proof end;

theorem Th29: :: ANPROJ_8:35
for p, q, r being Point of ()
for M being Matrix of 3,F_Real st M = <*<*(p 1),(p 2),(p 3)*>,<*(q 1),(q 2),(q 3)*>,<*(r 1),(r 2),(r 3)*>*> holds
|{p,q,r}| = Det M
proof end;

theorem Th30: :: ANPROJ_8:36
for k being Nat
for M being Matrix of k,F_Real holds
( Det M = 0. F_Real iff the_rank_of M < k )
proof end;

theorem Th31: :: ANPROJ_8:37
for k being Nat
for M being Matrix of k,F_Real holds
( ( lines M is linearly-dependent or not M is without_repeated_line ) iff the_rank_of M < k )
proof end;

theorem Th32: :: ANPROJ_8:38
for k, m being Nat
for M being Matrix of k,m,F_Real holds Mx2Tran M is Function of (),()
proof end;

theorem Th33: :: ANPROJ_8:39
for k being Nat
for M being Matrix of k,F_Real holds Mx2Tran M is linear-transformation of (),()
proof end;

theorem Th34: :: ANPROJ_8:40
for p, q, r being Point of ()
for M being Matrix of 3,F_Real st M = <*<*(p 1),(p 2),(p 3)*>,<*(q 1),(q 2),(q 3)*>,<*(r 1),(r 2),(r 3)*>*> & the_rank_of M < 3 holds
ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. () & ( a <> 0 or b <> 0 or c <> 0 ) )
proof end;

theorem Th35: :: ANPROJ_8:41
for a, b, c being Real
for p, q, r being Point of () st ((a * p) + (b * q)) + (c * r) = 0. () & ( a <> 0 or b <> 0 or c <> 0 ) holds
|{p,q,r}| = 0
proof end;

theorem Th36: :: ANPROJ_8:42
for p, q, r being Point of () st |{p,q,r}| = 0 holds
ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. () & ( a <> 0 or b <> 0 or c <> 0 ) )
proof end;

theorem Th37: :: ANPROJ_8:43
for p, q, r being Point of () holds
( p,q,r are_LinDep iff |{p,q,r}| = 0 )
proof end;

theorem Th38: :: ANPROJ_8:44
for p, q being Point of () holds |(p,(p <X> q))| = 0
proof end;

theorem Th39: :: ANPROJ_8:45
for p, q being Point of () holds |(p,(q <X> p))| = 0
proof end;

theorem Th40: :: ANPROJ_8:46
for o, p, q, r being Point of () holds
( |{o,p,((o <X> p) <X> (q <X> r))}| = 0 & |{q,r,((o <X> p) <X> (q <X> r))}| = 0 )
proof end;

theorem Th41: :: ANPROJ_8:47
for o, p, q, r being Point of () holds
( o,p,(o <X> p) <X> (q <X> r) are_LinDep & q,r,(o <X> p) <X> (q <X> r) are_LinDep )
proof end;

theorem Th42: :: ANPROJ_8:48
for p being Point of () holds
( (0. ()) <X> p = 0. () & p <X> (0. ()) = 0. () )
proof end;

theorem :: ANPROJ_8:49
for p, q being Point of () holds |{p,q,(0. ())}| = 0
proof end;

theorem :: ANPROJ_8:50
for p, q, r being Point of () st p <X> q = 0. () & r = |[1,1,1]| holds
p,q,r are_LinDep
proof end;

theorem Th43: :: ANPROJ_8:51
for p, q being Point of () st not p is zero & not q is zero & p <X> q = 0. () holds
are_Prop p,q
proof end;

theorem Th44: :: ANPROJ_8:52
for p, q, r, s being non zero Point of () holds
( not (p <X> q) <X> (r <X> s) is zero or are_Prop p,q or are_Prop r,s or are_Prop p <X> q,r <X> s )
proof end;

theorem Th45: :: ANPROJ_8:53
for p, q being Point of () holds |{p,q,(p <X> q)}| = (|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|)
proof end;

theorem Th46: :: ANPROJ_8:54
for p, q being Point of () holds |((p <X> q),(p <X> q))| = (|(q,q)| * |(p,p)|) - (|(q,p)| * |(p,q)|)
proof end;

theorem Th47: :: ANPROJ_8:55
for p, q, r, s being Point of () st not p is zero & |(p,q)| = 0 & |(p,r)| = 0 & |(p,s)| = 0 holds
|{q,r,s}| = 0
proof end;

theorem :: ANPROJ_8:56
for p, q being Point of () holds |{p,q,(p <X> q)}| = |.(p <X> q).| ^2
proof end;

theorem :: ANPROJ_8:57
proof end;

theorem Th48: :: ANPROJ_8:58
for u, v, w, x being Element of () st not u is zero & not x is zero & Dir u = Dir x holds
( |{u,v,w}| = 0 iff |{x,v,w}| = 0 )
proof end;

theorem Th49: :: ANPROJ_8:59
for u, v, w, x being Element of () st not v is zero & not x is zero & Dir v = Dir x holds
( |{u,v,w}| = 0 iff |{u,x,w}| = 0 )
proof end;

theorem Th50: :: ANPROJ_8:60
for u, v, w, x being Element of () st not w is zero & not x is zero & Dir w = Dir x holds
( |{u,v,w}| = 0 iff |{u,v,x}| = 0 )
proof end;

theorem :: ANPROJ_8:61
( () . 1 = <e1> & () . 2 = <e2> & () . 3 = <e3> ) by ;

theorem :: ANPROJ_8:62
( Base_FinSeq (3,1) = <e1> & Base_FinSeq (3,2) = <e2> & Base_FinSeq (3,3) = <e3> ) by ;

theorem Th51: :: ANPROJ_8:63
for D being non empty set
for pr being FinSequence of D st len pr = 3 holds
( Col (<*pr*>,1) = <*(pr . 1)*> & Col (<*pr*>,2) = <*(pr . 2)*> & Col (<*pr*>,3) = <*(pr . 3)*> )
proof end;

theorem Th52: :: ANPROJ_8:64
( Col (,1) = <*1*> & Col (,2) = & Col (,3) = )
proof end;

theorem Th53: :: ANPROJ_8:65
( Col (,1) = & Col (,2) = <*1*> & Col (,3) = )
proof end;

theorem Th54: :: ANPROJ_8:66
( Col (,1) = & Col (,2) = & Col (,3) = <*1*> )
proof end;

theorem Th55: :: ANPROJ_8:67
( Col ((1. (F_Real,3)),1) = <*1,0,0*> & Col ((1. (F_Real,3)),2) = <*0,1,0*> & Col ((1. (F_Real,3)),3) = <*0,0,1*> )
proof end;

theorem Th56: :: ANPROJ_8:68
( Line ((1. (F_Real,3)),1) = <*1,0,0*> & Line ((1. (F_Real,3)),2) = <*0,1,0*> & Line ((1. (F_Real,3)),3) = <*0,0,1*> )
proof end;

theorem Th57: :: ANPROJ_8:69
proof end;

theorem Th58: :: ANPROJ_8:70
for k being Nat
for D being non empty set
for pf being FinSequence of D st k in dom pf holds
<*pf*> * (1,k) = pf . k
proof end;

theorem Th59: :: ANPROJ_8:71
for k being Nat
for D being non empty set
for pf being FinSequence of D st k in dom pf holds
Col (<*pf*>,k) = <*(pf . k)*>
proof end;

theorem :: ANPROJ_8:72
for D being non empty set
for pf being FinSequence of D
for pr being Element of REAL 3 st pf = pr holds
MXR2MXF () = <*pf*> @
proof end;

theorem Th60: :: ANPROJ_8:73
for p, q, r being Point of ()
for PQR being Matrix of 3,F_Real st PQR = <*<*(p 1),(p 2),(p 3)*>,<*(q 1),(q 2),(q 3)*>,<*(r 1),(r 2),(r 3)*>*> holds
( Line (PQR,1) = p & Line (PQR,2) = q & Line (PQR,3) = r )
proof end;

theorem :: ANPROJ_8:74
for p, q, r being Point of ()
for PQR being Matrix of 3,F_Real st PQR = <*<*(p 1),(p 2),(p 3)*>,<*(q 1),(q 2),(q 3)*>,<*(r 1),(r 2),(r 3)*>*> holds
( Col (PQR,1) = <*(p 1),(q 1),(r 1)*> & Col (PQR,2) = <*(p 2),(q 2),(r 2)*> & Col (PQR,3) = <*(p 3),(q 3),(r 3)*> )
proof end;

theorem Th61: :: ANPROJ_8:75
for D being non empty set
for pf being FinSequence of D holds width <*pf*> = len pf
proof end;

theorem Th62: :: ANPROJ_8:76
for D being non empty set
for pf being FinSequence of D st len pf = 3 holds
( Line ((<*pf*> @),1) = <*(pf . 1)*> & Line ((<*pf*> @),2) = <*(pf . 2)*> & Line ((<*pf*> @),3) = <*(pf . 3)*> )
proof end;

theorem Th63: :: ANPROJ_8:77
for D being non empty set
for pf being FinSequence of D st len pf = 3 holds
<*pf*> @ = <*<*(pf . 1)*>,<*(pf . 2)*>,<*(pf . 3)*>*>
proof end;

definition
let D be non empty set ;
let p be FinSequence of D;
assume A1: len p = 3 ;
func F2M p -> FinSequence of 1 -tuples_on D equals :DEF1: :: ANPROJ_8:def 1
<*<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>*>;
coherence
<*<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>*> is FinSequence of 1 -tuples_on D
proof end;
end;

:: deftheorem DEF1 defines F2M ANPROJ_8:def 1 :
for D being non empty set
for p being FinSequence of D st len p = 3 holds
F2M p = <*<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>*>;

theorem Th64: :: ANPROJ_8:78
for p being FinSequence of REAL st len p = 3 holds
len (F2M p) = 3
proof end;

theorem :: ANPROJ_8:79
for p being FinSequence of REAL st len p = 3 holds
p is 3 -element FinSequence of REAL
proof end;

theorem Th65: :: ANPROJ_8:80
for p being FinSequence of REAL st p = |[0,0,0]| holds
F2M p =
proof end;

theorem :: ANPROJ_8:81
for D being non empty set
for pf being FinSequence of D st len pf = 3 holds
<*(Col (<*pf*>,1)),(Col (<*pf*>,2)),(Col (<*pf*>,3))*> = F2M pf
proof end;

definition
let D be non empty set ;
let p be FinSequence of 1 -tuples_on D;
assume A1: len p = 3 ;
func M2F p -> FinSequence of D equals :DEF2: :: ANPROJ_8:def 2
<*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*>;
coherence
<*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*> is FinSequence of D
proof end;
end;

:: deftheorem DEF2 defines M2F ANPROJ_8:def 2 :
for D being non empty set
for p being FinSequence of 1 -tuples_on D st len p = 3 holds
M2F p = <*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*>;

theorem Th66: :: ANPROJ_8:82
for p being FinSequence of 1 -tuples_on REAL st len p = 3 holds
M2F p is Point of ()
proof end;

definition
let p be FinSequence of 1 -tuples_on REAL;
let a be Real;
assume A1: len p = 3 ;
func a * p -> FinSequence of 1 -tuples_on REAL means :DEF3: :: ANPROJ_8:def 3
ex p1, p2, p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & it = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> );
existence
ex b1 being FinSequence of 1 -tuples_on REAL ex p1, p2, p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b1 = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> )
proof end;
uniqueness
for b1, b2 being FinSequence of 1 -tuples_on REAL st ex p1, p2, p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b1 = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> ) & ex p1, p2, p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b2 = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> ) holds
b1 = b2
;
end;

:: deftheorem DEF3 defines * ANPROJ_8:def 3 :
for p being FinSequence of 1 -tuples_on REAL
for a being Real st len p = 3 holds
for b3 being FinSequence of 1 -tuples_on REAL holds
( b3 = a * p iff ex p1, p2, p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b3 = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> ) );

theorem Th67: :: ANPROJ_8:83
for a being Real
for p being FinSequence of 1 -tuples_on REAL st len p = 3 holds
M2F (a * p) = a * (M2F p)
proof end;

theorem Th68: :: ANPROJ_8:84
for p being FinSequence of 1 -tuples_on REAL st len p = 3 holds
<*<*((p . 1) . 1)*>,<*((p . 2) . 1)*>,<*((p . 3) . 1)*>*> = p
proof end;

theorem Th69: :: ANPROJ_8:85
for p being FinSequence of 1 -tuples_on REAL st len p = 3 holds
F2M (M2F p) = p
proof end;

theorem Th70: :: ANPROJ_8:86
for p being FinSequence of REAL st len p = 3 holds
M2F (F2M p) = p
proof end;

theorem :: ANPROJ_8:87
proof end;

theorem :: ANPROJ_8:88
for D being non empty set
for p being FinSequence of D st len p = 3 holds
<*p*> @ = F2M p
proof end;

theorem Th72: :: ANPROJ_8:89
for D being non empty set
for pf being FinSequence of D holds Line (<*pf*>,1) = pf
proof end;

theorem Th73: :: ANPROJ_8:90
for D being non empty set
for M being Matrix of 3,1,D holds
( Line (M,1) = <*(M * (1,1))*> & Line (M,2) = <*(M * (2,1))*> & Line (M,3) = <*(M * (3,1))*> )
proof end;

theorem Th74: :: ANPROJ_8:91
for R being Ring
for N being Matrix of 3,R
for p being FinSequence of R st len p = 3 holds
N * () is 3,1 -size
proof end;

theorem Th75: :: ANPROJ_8:92
for R being Ring
for pf being FinSequence of R
for N being Matrix of 3,R st len pf = 3 holds
( Line ((N * (<*pf*> @)),1) = <*((N * (<*pf*> @)) * (1,1))*> & Line ((N * (<*pf*> @)),2) = <*((N * (<*pf*> @)) * (2,1))*> & Line ((N * (<*pf*> @)),3) = <*((N * (<*pf*> @)) * (3,1))*> )
proof end;

theorem Th76: :: ANPROJ_8:93
for D being non empty set
for pf being FinSequence of D holds Col ((<*pf*> @),1) = pf
proof end;

theorem :: ANPROJ_8:94
for p, q, r being Point of ()
for pf, qf, rf being FinSequence of F_Real st p = pf & q = qf & r = rf & |{p,q,r}| <> 0 holds
ex M being Matrix of 3,F_Real st
( M is invertible & M * pf = F2M <e1> & M * qf = F2M <e2> & M * rf = F2M <e3> )
proof end;

theorem Th77: :: ANPROJ_8:95
for p, q, r being Point of ()
for M, PQR being Matrix of 3,F_Real
for pf, qf, rf being FinSequence of F_Real
for pt, qt, rt being FinSequence of 1 -tuples_on REAL st PQR = <*<*(p 1),(q 1),(r 1)*>,<*(p 2),(q 2),(r 2)*>,<*(p 3),(q 3),(r 3)*>*> & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf holds
(M * PQR) @ = <*(M2F pt),(M2F qt),(M2F rt)*>
proof end;

theorem :: ANPROJ_8:96
for p, q, r being Point of ()
for M being Matrix of 3,F_Real
for pt, qt, rt being FinSequence of 1 -tuples_on REAL st M = <*(M2F pt),(M2F qt),(M2F rt)*> & Det M = 0 & M2F pt = p & M2F qt = q & M2F rt = r holds
|{p,q,r}| = 0
proof end;

theorem Th78: :: ANPROJ_8:97
for p, q, r being Point of ()
for M being Matrix of 3,F_Real
for pm, qm, rm being Point of ()
for pt, qt, rt being FinSequence of 1 -tuples_on REAL
for pf, qf, rf being FinSequence of F_Real st M is invertible & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf & M2F pt = pm & M2F qt = qm & M2F rt = rm holds
( |{p,q,r}| = 0 iff |{pm,qm,rm}| = 0 )
proof end;

theorem Th79: :: ANPROJ_8:98
for m being Nat st 0 < m holds
for M being Matrix of m,1,F_Real holds M is FinSequence of 1 -tuples_on REAL
proof end;

theorem Th80: :: ANPROJ_8:99
for uf being FinSequence of F_Real st len uf = 3 holds
<*uf*> @ = (1. (F_Real,3)) * (<*uf*> @)
proof end;

theorem Th81: :: ANPROJ_8:100
for u being Element of ()
for uf being FinSequence of F_Real st u = uf & <*uf*> @ = holds
u = 0. ()
proof end;

theorem Th82: :: ANPROJ_8:101
for N being invertible Matrix of 3,F_Real
for u, mu being Element of ()
for uf being FinSequence of F_Real
for ut being FinSequence of 1 -tuples_on REAL st not u is zero & u = uf & ut = N * uf & mu = M2F ut holds
not mu is zero
proof end;

definition
let N be invertible Matrix of 3,F_Real;
func homography N -> Function of (),() means :DEF4: :: ANPROJ_8:def 4
for x being Point of () ex u, v being Element of () ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & it . x = Dir v );
existence
ex b1 being Function of (),() st
for x being Point of () ex u, v being Element of () ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & b1 . x = Dir v )
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for x being Point of () ex u, v being Element of () ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & b1 . x = Dir v ) ) & ( for x being Point of () ex u, v being Element of () ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & b2 . x = Dir v ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DEF4 defines homography ANPROJ_8:def 4 :
for N being invertible Matrix of 3,F_Real
for b2 being Function of (),() holds
( b2 = homography N iff for x being Point of () ex u, v being Element of () ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & b2 . x = Dir v ) );

theorem :: ANPROJ_8:102
for N being invertible Matrix of 3,F_Real
for p, q, r being Point of () holds
( p,q,r are_collinear iff () . p,() . q,() . r are_collinear )
proof end;