:: by Roland Coghetto

::

:: Received October 18, 2016

:: Copyright (c) 2016-2018 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 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*>

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)*>

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)

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*>*>

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 ) )

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 ) ) )

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 ) ) ) )

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)

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)

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

( ((a * u) + (b * v)) + (c * w) = 0. (TOP-REAL 3) & a <> 0 ) holds

|{u,v,w}| = 0

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

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 )

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 )

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 )

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*>*>

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)*>*>

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 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 )

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) ) )

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 :: 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

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

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 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 )

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))

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))

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 ) )

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

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 ) )

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 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 )

( |{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 )

( 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) )

( (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: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

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

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 )

( 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

|{q,r,s}| = 0

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 )

( |{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 )

( |{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 )

( |{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)*> )

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 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

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)*>

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*> @

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 )

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)*> )

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 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)*> )

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)*>*>

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 ;

<*<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>*> is FinSequence of 1 -tuples_on D

end;
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)*>*>;

<*<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>*> is FinSequence of 1 -tuples_on D

proof 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)*>*>;

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 :: 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

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 ;

<*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*> is FinSequence of D

end;
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)*>;

<*((p . 1) . 1),((p . 2) . 1),((p . 3) . 1)*> is FinSequence of D

proof 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)*>;

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)*>;

definition

let p be FinSequence of 1 -tuples_on REAL;

let a be Real;

assume A1: len p = 3 ;

ex b_{1} 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_{1} = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> )

for b_{1}, b_{2} 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_{1} = <*<*(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_{2} = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> ) holds

b_{1} = b_{2}
;

end;
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 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)*>*> );

ex b

( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b

proof end;

uniqueness for b

( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b

( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b

b

:: 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_{3} being FinSequence of 1 -tuples_on REAL holds

( b_{3} = a * p iff ex p1, p2, p3 being Real st

( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b_{3} = <*<*(a * p1)*>,<*(a * p2)*>,<*(a * p3)*>*> ) );

for p being FinSequence of 1 -tuples_on REAL

for a being Real st len p = 3 holds

for b

( b

( p1 = (p . 1) . 1 & p2 = (p . 2) . 1 & p3 = (p . 3) . 1 & b

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)

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

<*<*((p . 1) . 1)*>,<*((p . 2) . 1)*>,<*((p . 3) . 1)*>*> = p

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))*> )

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

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))*> )

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 :: 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> )

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)*>

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

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 )

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

for M being Matrix of m,1,F_Real holds M is FinSequence of 1 -tuples_on REAL

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)

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

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;

ex b_{1} 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_{1} . x = Dir v )

for b_{1}, b_{2} 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_{1} . 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_{2} . x = Dir v ) ) holds

b_{1} = b_{2}

end;
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 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 );

ex b

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

proof end;

uniqueness for b

( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & b

( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & b

b

proof end;

:: deftheorem DEF4 defines homography ANPROJ_8:def 4 :

for N being invertible Matrix of 3,F_Real

for b_{2} being Function of (ProjectiveSpace (TOP-REAL 3)),(ProjectiveSpace (TOP-REAL 3)) holds

( b_{2} = 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_{2} . x = Dir v ) );

for N being invertible Matrix of 3,F_Real

for b

( b

( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & b

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 )

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;