:: Homography in $\mathbbRP^2$
:: by Roland Coghetto
::
:: Received October 18, 2016
:: 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 = <*<*0*>,<*0*>,<*0*>*> holds
M * N = <*<*0*>,<*0*>,<*0*>*>

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 (ProjectiveSpace V) 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 (ProjectiveSpace V) 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 (TOP-REAL 3) st ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) & a <> 0 ) holds
|{u,v,w}| = 0

proof end;

theorem Th13: :: ANPROJ_8:15

for n being Nat holds dom (1_Rmatrix n) = Seg n

proof end;

theorem Th14: :: ANPROJ_8:16

for A being Matrix of F_Real holds MXR2MXF (MXF2MXR A) = 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 (TOP-REAL 3)
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 (TOP-REAL 3)
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 (TOP-REAL 3)
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 (TOP-REAL 3) 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 (TOP-REAL 3) 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 (TOP-REAL 3) holds |{p,q,r}| = - |{p,r,q}|

proof end;

theorem Th25: :: ANPROJ_8:30

for p, q, r being Point of (TOP-REAL 3) 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 (TOP-REAL 3) 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 (TOP-REAL 3) 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 (TOP-REAL 3) holds |{p,q,(a * r)}| = a * |{p,q,r}|

proof end;

theorem :: ANPROJ_8:34

for p, q, r being Point of (TOP-REAL 3)
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 (TOP-REAL 3)
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 (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL m))

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 (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL k))

proof end;

theorem Th34: :: ANPROJ_8:40

for p, q, r being Point of (TOP-REAL 3)
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. (TOP-REAL 3) & ( 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 (TOP-REAL 3) st ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( 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 (TOP-REAL 3) st |{p,q,r}| = 0 holds
ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) )

proof end;

theorem Th37: :: ANPROJ_8:43

for p, q, r being Point of (TOP-REAL 3) holds
( p,q,r are_LinDep iff |{p,q,r}| = 0 )

proof end;

theorem Th38: :: ANPROJ_8:44

for p, q being Point of (TOP-REAL 3) holds |(p,(p <X> q))| = 0

proof end;

theorem Th39: :: ANPROJ_8:45

for p, q being Point of (TOP-REAL 3) holds |(p,(q <X> p))| = 0

proof end;

theorem Th40: :: ANPROJ_8:46

for o, p, q, r being Point of (TOP-REAL 3) 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 (TOP-REAL 3) 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 (TOP-REAL 3) holds
( (0. (TOP-REAL 3)) <X> p = 0. (TOP-REAL 3) & p <X> (0. (TOP-REAL 3)) = 0. (TOP-REAL 3) )

proof end;

theorem :: ANPROJ_8:49

for p, q being Point of (TOP-REAL 3) holds |{p,q,(0. (TOP-REAL 3))}| = 0

proof end;

theorem :: ANPROJ_8:50

for p, q, r being Point of (TOP-REAL 3) st p <X> q = 0. (TOP-REAL 3) & r = |[1,1,1]| holds
p,q,r are_LinDep

proof end;

theorem Th43: :: ANPROJ_8:51

for p, q being Point of (TOP-REAL 3) st not p is zero & not q is zero & p <X> q = 0. (TOP-REAL 3) holds
are_Prop p,q

proof end;

theorem Th44: :: ANPROJ_8:52

for p, q, r, s being non zero Point of (TOP-REAL 3) 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 (TOP-REAL 3) 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 (TOP-REAL 3) 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 (TOP-REAL 3) 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 (TOP-REAL 3) holds |{p,q,(p <X> q)}| = |.(p <X> q).| ^2

proof end;

theorem :: ANPROJ_8:57

ProjectiveSpace (TOP-REAL 3) is CollProjectivePlane

proof end;

theorem Th48: :: ANPROJ_8:58

for u, v, w, x being Element of (TOP-REAL 3) 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 (TOP-REAL 3) 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 (TOP-REAL 3) 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_Rmatrix 3) . 1 = <e1> & (1_Rmatrix 3) . 2 = <e2> & (1_Rmatrix 3) . 3 = <e3> ) by MATRIXR2:77, MATRIXR2:78, EUCLID_8:def 1, EUCLID_8:def 2, EUCLID_8:def 3;

theorem :: ANPROJ_8:62

( Base_FinSeq (3,1) = <e1> & Base_FinSeq (3,2) = <e2> & Base_FinSeq (3,3) = <e3> ) by MATRIXR2:77, EUCLID_8:def 1, EUCLID_8:def 2, EUCLID_8:def 3;

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 (<*<e1>*>,1) = <*1*> & Col (<*<e1>*>,2) = <*0*> & Col (<*<e1>*>,3) = <*0*> )

proof end;

theorem Th53: :: ANPROJ_8:65

( Col (<*<e2>*>,1) = <*0*> & Col (<*<e2>*>,2) = <*1*> & Col (<*<e2>*>,3) = <*0*> )

proof end;

theorem Th54: :: ANPROJ_8:66

( Col (<*<e3>*>,1) = <*0*> & Col (<*<e3>*>,2) = <*0*> & Col (<*<e3>*>,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

( <*<e1>*> @ = <*<*1*>,<*0*>,<*0*>*> & <*<e2>*> @ = <*<*0*>,<*1*>,<*0*>*> & <*<e3>*> @ = <*<*0*>,<*0*>,<*1*>*> )

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 (ColVec2Mx pr) = <*pf*> @

proof end;

theorem Th60: :: ANPROJ_8:73

for p, q, r being Point of (TOP-REAL 3)
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 (TOP-REAL 3)
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 = <*<*0*>,<*0*>,<*0*>*>

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 (TOP-REAL 3)

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 b₁ 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 & b₁ = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> )

proof end;

uniqueness
for b₁, b₂ 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 & b₁ = <*<*(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 & b₂ = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> ) holds
b₁ = b₂ ;

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 b₃ being FinSequence of 1 -tuples_on REAL holds
( b₃ = a * p iff ex p1, p2, p3 being Real st
( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b₃ = <*<*(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

( <*<e1>*> @ = F2M <e1> & <*<e2>*> @ = F2M <e2> & <*<e3>*> @ = F2M <e3> )

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 * (<*p*> @) 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 (TOP-REAL 3)
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 (TOP-REAL 3)
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 (TOP-REAL 3)
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 (TOP-REAL 3)
for M being Matrix of 3,F_Real
for pm, qm, rm being Point of (TOP-REAL 3)
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 (TOP-REAL 3)
for uf being FinSequence of F_Real st u = uf & <*uf*> @ = <*<*0*>,<*0*>,<*0*>*> holds
u = 0. (TOP-REAL 3)

proof end;

theorem Th82: :: ANPROJ_8:101

for N being invertible Matrix of 3,F_Real
for u, mu being Element of (TOP-REAL 3)
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 (ProjectiveSpace (TOP-REAL 3)),(ProjectiveSpace (TOP-REAL 3)) means :DEF4: :: ANPROJ_8:def 4
for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) 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 b₁ being Function of (ProjectiveSpace (TOP-REAL 3)),(ProjectiveSpace (TOP-REAL 3)) st
for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) 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 & b₁ . x = Dir v )

proof end;

uniqueness
for b₁, b₂ being Function of (ProjectiveSpace (TOP-REAL 3)),(ProjectiveSpace (TOP-REAL 3)) st ( for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) 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 & b₁ . x = Dir v ) ) & ( for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) 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 & b₂ . x = Dir v ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DEF4 defines homography ANPROJ_8:def 4 :
for N being invertible Matrix of 3,F_Real
for b₂ being Function of (ProjectiveSpace (TOP-REAL 3)),(ProjectiveSpace (TOP-REAL 3)) holds
( b₂ = homography N iff for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) 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 & b₂ . x = Dir v ) );

theorem :: ANPROJ_8:102

for N being invertible Matrix of 3,F_Real
for p, q, r being Point of (ProjectiveSpace (TOP-REAL 3)) holds
( p,q,r are_collinear iff (homography N) . p,(homography N) . q,(homography N) . r are_collinear )

proof end;