:: by Roland Coghetto

::

:: Received March 27, 2018

:: Copyright (c) 2018 Association of Mizar Users

theorem Th01: :: BKMODEL1:1

for u, v, w being Element of (TOP-REAL 3)

for P1, P2, P3 being Element of (ProjectiveSpace (TOP-REAL 3)) st not u is zero & not v is zero & not w is zero & P1 = Dir u & P2 = Dir v & P3 = Dir w holds

( P1,P2,P3 are_collinear iff |{u,v,w}| = 0 )

for P1, P2, P3 being Element of (ProjectiveSpace (TOP-REAL 3)) st not u is zero & not v is zero & not w is zero & P1 = Dir u & P2 = Dir v & P3 = Dir w holds

( P1,P2,P3 are_collinear iff |{u,v,w}| = 0 )

proof end;

Lem01: for a, b, c, d being Real st a <> 0 & b <> 0 & a * d = b * c holds

ex e being Real st

( e = d / b & e = c / a & c = e * a & d = e * b )

proof end;

Lem02: for a, b, c, d being Real st a <> 0 & b = 0 & a * d = b * c holds

ex e being Real st

( c = e * a & d = e * b )

proof end;

theorem :: BKMODEL1:2

for a, b, c, d being Real st ( a <> 0 or b <> 0 ) & a * d = b * c holds

ex e being Real st

( c = e * a & d = e * b )

ex e being Real st

( c = e * a & d = e * b )

proof end;

theorem :: BKMODEL1:3

for a, b, c being Real st (a ^2) + (b ^2) = 1 & ((c * a) ^2) + ((c * b) ^2) = 1 & not c = 1 holds

c = - 1

c = - 1

proof end;

theorem :: BKMODEL1:7

for a, b, c, d being Real st (a ^2) + (b ^2) = 1 & (c ^2) + (d ^2) = 1 & (c * a) + (d * b) = 1 holds

b * c = a * d

b * c = a * d

proof end;

Lem03: for a being Real holds 1 + (a ^2) <> 0

proof end;

Lem04: for a, b being Real holds

( not a ^2 = 1 / b or a = 1 / (sqrt b) or a = (- 1) / (sqrt b) )

proof end;

theorem :: BKMODEL1:10

for a, b being Real holds

( not ((a * b) ^2) + (b ^2) = 1 or b = 1 / (sqrt (1 + (a ^2))) or b = (- 1) / (sqrt (1 + (a ^2))) )

( not ((a * b) ^2) + (b ^2) = 1 or b = 1 / (sqrt (1 + (a ^2))) or b = (- 1) / (sqrt (1 + (a ^2))) )

proof end;

Lem05: for z being non zero Complex holds ((1 / z) ^2) * (z ^2) = 1

proof end;

theorem :: BKMODEL1:11

for a, b being Real st a <> 0 & b ^2 = 1 + (a * a) holds

(((a * (1 / b)) * a) * ((- 1) / b)) + ((1 / b) * ((- 1) / b)) = - 1

(((a * (1 / b)) * a) * ((- 1) / b)) + ((1 / b) * ((- 1) / b)) = - 1

proof end;

theorem Th12: :: BKMODEL1:14

for a, b being Real

for g being positive Real holds

( (a ^2) + (b ^2) = g ^2 iff |[a,b]| in circle (0,0,g) )

for g being positive Real holds

( (a ^2) + (b ^2) = g ^2 iff |[a,b]| in circle (0,0,g) )

proof end;

Lem06: for a, b, c being Real holds ((a * b) ^2) + ((a * c) ^2) = (a ^2) * ((b ^2) + (c ^2))

;

theorem Th13: :: BKMODEL1:15

for a, b being Real st a <> 0 & - 1 < a & a < 1 & b = (2 + (sqrt (delta ((a * a),(- 2),1)))) / ((2 * a) * a) holds

(((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0

(((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0

proof end;

Lem07: for a being Real st - 1 < a & a < 1 holds

ex b being Real st (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0

proof end;

theorem :: BKMODEL1:16

for a, b, c being Real st (a ^2) + (b ^2) = 1 & - 1 < c & c < 1 holds

ex d, e, f being Real st

( e = ((d * c) * a) + ((1 - d) * (- b)) & f = ((d * c) * b) + ((1 - d) * a) & (e ^2) + (f ^2) = d ^2 )

ex d, e, f being Real st

( e = ((d * c) * a) + ((1 - d) * (- b)) & f = ((d * c) * b) + ((1 - d) * a) & (e ^2) + (f ^2) = d ^2 )

proof end;

theorem :: BKMODEL1:17

for a, b, c, d being Real st (a ^2) + (b ^2) < 1 & (c ^2) + (d ^2) = 1 holds

(((a + c) / 2) ^2) + (((b + d) / 2) ^2) < 1

(((a + c) / 2) ^2) + (((b + d) / 2) ^2) < 1

proof end;

Lem08: for a, b, c being Real st 0 <= a & c <= 0 holds

0 <= delta (a,b,c)

proof end;

theorem :: BKMODEL1:18

for b being Real

for S, T being Element of REAL 2 st |.S.| ^2 <= 1 holds

0 <= delta ((Sum (sqr (T - S))),b,((Sum (sqr S)) - 1))

for S, T being Element of REAL 2 st |.S.| ^2 <= 1 holds

0 <= delta ((Sum (sqr (T - S))),b,((Sum (sqr S)) - 1))

proof end;

theorem :: BKMODEL1:20

for a, b, c, d being Real

for u, v, w being Element of (TOP-REAL 3) st u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds

|{u,v,w}| = 0

for u, v, w being Element of (TOP-REAL 3) st u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds

|{u,v,w}| = 0

proof end;

theorem Th19: :: BKMODEL1:21

for a being Real

for u, v being Element of (TOP-REAL 3) holds

( a * |(u,v)| = |((a * u),v)| & a * |(u,v)| = |(u,(a * v))| )

for u, v being Element of (TOP-REAL 3) holds

( a * |(u,v)| = |((a * u),v)| & a * |(u,v)| = |(u,(a * v))| )

proof end;

Lem09: for a11, a12, a13, a21, a22, a23, a31, a32, a33, b11, b12, b13, b21, b22, b23, b31, b32, b33 being Element of F_Real

for A, B being Matrix of 3,F_Real st A = <*<*a11,a12,a13*>,<*a21,a22,a23*>,<*a31,a32,a33*>*> & B = <*<*b11,b12,b13*>,<*b21,b22,b23*>,<*b31,b32,b33*>*> holds

( (A * B) * (1,1) = ((a11 * b11) + (a12 * b21)) + (a13 * b31) & (A * B) * (1,2) = ((a11 * b12) + (a12 * b22)) + (a13 * b32) & (A * B) * (1,3) = ((a11 * b13) + (a12 * b23)) + (a13 * b33) & (A * B) * (2,1) = ((a21 * b11) + (a22 * b21)) + (a23 * b31) & (A * B) * (2,2) = ((a21 * b12) + (a22 * b22)) + (a23 * b32) & (A * B) * (2,3) = ((a21 * b13) + (a22 * b23)) + (a23 * b33) & (A * B) * (3,1) = ((a31 * b11) + (a32 * b21)) + (a33 * b31) & (A * B) * (3,2) = ((a31 * b12) + (a32 * b22)) + (a33 * b32) & (A * B) * (3,3) = ((a31 * b13) + (a32 * b23)) + (a33 * b33) )

proof end;

theorem :: BKMODEL1:23

for a, b, c being Element of F_Real

for M, N being Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

( ((M @) * (N * M)) * (1,1) = (((a * (M * (1,1))) * (M * (1,1))) + ((b * (M * (2,1))) * (M * (2,1)))) + ((c * (M * (3,1))) * (M * (3,1))) & ((M @) * (N * M)) * (1,2) = (((a * (M * (1,1))) * (M * (1,2))) + ((b * (M * (2,1))) * (M * (2,2)))) + ((c * (M * (3,1))) * (M * (3,2))) & ((M @) * (N * M)) * (1,3) = (((a * (M * (1,1))) * (M * (1,3))) + ((b * (M * (2,1))) * (M * (2,3)))) + ((c * (M * (3,1))) * (M * (3,3))) & ((M @) * (N * M)) * (2,1) = (((a * (M * (1,2))) * (M * (1,1))) + ((b * (M * (2,2))) * (M * (2,1)))) + ((c * (M * (3,2))) * (M * (3,1))) & ((M @) * (N * M)) * (2,2) = (((a * (M * (1,2))) * (M * (1,2))) + ((b * (M * (2,2))) * (M * (2,2)))) + ((c * (M * (3,2))) * (M * (3,2))) & ((M @) * (N * M)) * (2,3) = (((a * (M * (1,2))) * (M * (1,3))) + ((b * (M * (2,2))) * (M * (2,3)))) + ((c * (M * (3,2))) * (M * (3,3))) & ((M @) * (N * M)) * (3,1) = (((a * (M * (1,3))) * (M * (1,1))) + ((b * (M * (2,3))) * (M * (2,1)))) + ((c * (M * (3,3))) * (M * (3,1))) & ((M @) * (N * M)) * (3,2) = (((a * (M * (1,3))) * (M * (1,2))) + ((b * (M * (2,3))) * (M * (2,2)))) + ((c * (M * (3,3))) * (M * (3,2))) & ((M @) * (N * M)) * (3,3) = (((a * (M * (1,3))) * (M * (1,3))) + ((b * (M * (2,3))) * (M * (2,3)))) + ((c * (M * (3,3))) * (M * (3,3))) )

for M, N being Matrix of 3,F_Real st N = <*<*a,0,0*>,<*0,b,0*>,<*0,0,c*>*> holds

( ((M @) * (N * M)) * (1,1) = (((a * (M * (1,1))) * (M * (1,1))) + ((b * (M * (2,1))) * (M * (2,1)))) + ((c * (M * (3,1))) * (M * (3,1))) & ((M @) * (N * M)) * (1,2) = (((a * (M * (1,1))) * (M * (1,2))) + ((b * (M * (2,1))) * (M * (2,2)))) + ((c * (M * (3,1))) * (M * (3,2))) & ((M @) * (N * M)) * (1,3) = (((a * (M * (1,1))) * (M * (1,3))) + ((b * (M * (2,1))) * (M * (2,3)))) + ((c * (M * (3,1))) * (M * (3,3))) & ((M @) * (N * M)) * (2,1) = (((a * (M * (1,2))) * (M * (1,1))) + ((b * (M * (2,2))) * (M * (2,1)))) + ((c * (M * (3,2))) * (M * (3,1))) & ((M @) * (N * M)) * (2,2) = (((a * (M * (1,2))) * (M * (1,2))) + ((b * (M * (2,2))) * (M * (2,2)))) + ((c * (M * (3,2))) * (M * (3,2))) & ((M @) * (N * M)) * (2,3) = (((a * (M * (1,2))) * (M * (1,3))) + ((b * (M * (2,2))) * (M * (2,3)))) + ((c * (M * (3,2))) * (M * (3,3))) & ((M @) * (N * M)) * (3,1) = (((a * (M * (1,3))) * (M * (1,1))) + ((b * (M * (2,3))) * (M * (2,1)))) + ((c * (M * (3,3))) * (M * (3,1))) & ((M @) * (N * M)) * (3,2) = (((a * (M * (1,3))) * (M * (1,2))) + ((b * (M * (2,3))) * (M * (2,2)))) + ((c * (M * (3,3))) * (M * (3,2))) & ((M @) * (N * M)) * (3,3) = (((a * (M * (1,3))) * (M * (1,3))) + ((b * (M * (2,3))) * (M * (2,3)))) + ((c * (M * (3,3))) * (M * (3,3))) )

proof end;

theorem :: BKMODEL1:24

for m, n being Nat

for M being Matrix of m,F_Real

for N being Matrix of m,n,F_Real st m > 0 holds

M * N is Matrix of m,n,F_Real

for M being Matrix of m,F_Real

for N being Matrix of m,n,F_Real st m > 0 holds

M * N is Matrix of m,n,F_Real

proof end;

theorem Th24: :: BKMODEL1:27

for D being non empty set

for d1, d2, d3 being Element of D holds <*<*d1,d2,d3*>*> is Matrix of 1,3,D

for d1, d2, d3 being Element of D holds <*<*d1,d2,d3*>*> is Matrix of 1,3,D

proof end;

theorem Th25: :: BKMODEL1:28

for D being non empty set

for d1, d2, d3 being Element of D holds <*<*d1*>,<*d2*>,<*d3*>*> is Matrix of 3,1,D

for d1, d2, d3 being Element of D holds <*<*d1*>,<*d2*>,<*d3*>*> is Matrix of 3,1,D

proof end;

theorem Th26: :: BKMODEL1:29

for D being non empty set

for A being Matrix of 1,3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>*>

for A being Matrix of 1,3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>*>

proof end;

theorem Th27: :: BKMODEL1:30

for D being non empty set

for B being Matrix of 3,1,D holds B = <*<*(B * (1,1))*>,<*(B * (2,1))*>,<*(B * (3,1))*>*>

for B being Matrix of 3,1,D holds B = <*<*(B * (1,1))*>,<*(B * (2,1))*>,<*(B * (3,1))*>*>

proof end;

theorem :: BKMODEL1:31

for D being non empty set

for A being Matrix of 1,3,D holds A @ = <*<*(A * (1,1))*>,<*(A * (1,2))*>,<*(A * (1,3))*>*>

for A being Matrix of 1,3,D holds A @ = <*<*(A * (1,1))*>,<*(A * (1,2))*>,<*(A * (1,3))*>*>

proof end;

theorem :: BKMODEL1:32

for D being non empty set

for A being Matrix of 1,3,D ex d1, d2, d3 being Element of D st A = <*<*d1,d2,d3*>*>

for A being Matrix of 1,3,D ex d1, d2, d3 being Element of D st A = <*<*d1,d2,d3*>*>

proof end;

theorem Th30: :: BKMODEL1:34

for M being Matrix of 3,F_Real

for MR being Matrix of 3,REAL

for v being Element of (TOP-REAL 3)

for uf being FinSequence of F_Real

for ufr being FinSequence of REAL

for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M holds

v = MR * ufr

for MR being Matrix of 3,REAL

for v being Element of (TOP-REAL 3)

for uf being FinSequence of F_Real

for ufr being FinSequence of REAL

for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & len uf = 3 & uf = ufr & MR = M holds

v = MR * ufr

proof end;

theorem Th31: :: BKMODEL1:35

for N being Matrix of 3,REAL

for uf being FinSequence of REAL st uf = 0. (TOP-REAL 3) holds

N * uf = 0. (TOP-REAL 3)

for uf being FinSequence of REAL st uf = 0. (TOP-REAL 3) holds

N * uf = 0. (TOP-REAL 3)

proof end;

theorem Th32: :: BKMODEL1:36

for N being Matrix of 3,REAL

for uf being FinSequence of REAL

for u being Element of (TOP-REAL 3) st N is invertible & u = uf & not u is zero holds

N * uf <> 0. (TOP-REAL 3)

for uf being FinSequence of REAL

for u being Element of (TOP-REAL 3) st N is invertible & u = uf & not u is zero holds

N * uf <> 0. (TOP-REAL 3)

proof end;

theorem :: BKMODEL1:37

for N being invertible Matrix of 3,F_Real

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 st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds

(homography N) . P = Q

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 st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds

(homography N) . P = Q

proof end;

theorem Th33: :: BKMODEL1:38

for N being invertible Matrix of 3,F_Real

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

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

proof end;

theorem Th34: :: BKMODEL1:39

for a, b being Element of F_Real

for p being FinSequence of REAL

for M being Matrix of 3,REAL st len p = 3 holds

|((a * p),(M * (b * p)))| = (a * b) * |(p,(M * p))|

for p being FinSequence of REAL

for M being Matrix of 3,REAL st len p = 3 holds

|((a * p),(M * (b * p)))| = (a * b) * |(p,(M * p))|

proof end;

theorem Th35: :: BKMODEL1:40

for a, b being Element of F_Real

for p being FinSequence of REAL

for M being Matrix of 3,REAL st len p = 3 holds

SumAll (QuadraticForm ((a * p),M,(b * p))) = (a * b) * (SumAll (QuadraticForm (p,M,p)))

for p being FinSequence of REAL

for M being Matrix of 3,REAL st len p = 3 holds

SumAll (QuadraticForm ((a * p),M,(b * p))) = (a * b) * (SumAll (QuadraticForm (p,M,p)))

proof end;

theorem :: BKMODEL1:42

for P, Q being Element of (TOP-REAL 2)

for r being Real holds

( P in Sphere (Q,r) iff P in circle ((Q . 1),(Q . 2),r) )

for r being Real holds

( P in Sphere (Q,r) iff P in circle ((Q . 1),(Q . 2),r) )

proof end;

theorem Th37: :: BKMODEL1:43

for u, v being non zero Element of (TOP-REAL 3) st Dir u = Dir v & u . 3 = v . 3 & v . 3 <> 0 holds

u = v

u = v

proof end;

theorem :: BKMODEL1:44

( not Dir101 , Dirm101 , Dir011 are_collinear & not Dir101 , Dirm101 , Dir010 are_collinear & not Dir101 , Dir011 , Dir010 are_collinear & not Dirm101 , Dir011 , Dir010 are_collinear )

proof end;

theorem Th39: :: BKMODEL1:46

for r, a, b, c, d, e, f, g, h, i being Element of F_Real

for M being Matrix of 3,F_Real st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds

r * M = <*<*(r * a),(r * b),(r * c)*>,<*(r * d),(r * e),(r * f)*>,<*(r * g),(r * h),(r * i)*>*>

for M being Matrix of 3,F_Real st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds

r * M = <*<*(r * a),(r * b),(r * c)*>,<*(r * d),(r * e),(r * f)*>,<*(r * g),(r * h),(r * i)*>*>

proof end;

theorem Th40: :: BKMODEL1:47

for a being Real

for ra2 being Element of F_Real st ra2 = a * a holds

(symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) = ra2 * (1. (F_Real,3))

for ra2 being Element of F_Real st ra2 = a * a holds

(symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) = ra2 * (1. (F_Real,3))

proof end;

theorem Th41: :: BKMODEL1:48

for a being non zero Real holds (symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 ((1 / a),(1 / a),(- (1 / a)),0,0,0)) = 1. (F_Real,3)

proof end;

theorem Th42: :: BKMODEL1:49

for a being non zero Real holds (symmetric_3 ((1 / a),(1 / a),(- (1 / a)),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) = 1. (F_Real,3)

proof end;

theorem :: BKMODEL1:51

for a being non zero Real

for N being Matrix of 3,F_Real st N = symmetric_3 (a,a,(- a),0,0,0) holds

N is invertible

for N being Matrix of 3,F_Real st N = symmetric_3 (a,a,(- a),0,0,0) holds

N is invertible

proof end;

theorem Th44: :: BKMODEL1:52

( symmetric_3 (1,1,(- 1),0,0,0) is invertible Matrix of 3,F_Real & (symmetric_3 (1,1,(- 1),0,0,0)) ~ = symmetric_3 (1,1,(- 1),0,0,0) )

proof end;

theorem :: BKMODEL1:53

for N being invertible Matrix of 3,F_Real

for N1 being Matrix of 3,F_Real

for M, NR being Matrix of 3,REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & N1 = M & NR = MXF2MXR (N ~) holds

((N @) * N1) * N = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~))

for N1 being Matrix of 3,F_Real

for M, NR being Matrix of 3,REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & N1 = M & NR = MXF2MXR (N ~) holds

((N @) * N1) * N = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~))

proof end;

theorem Th46: :: BKMODEL1:54

for n being Nat

for a being Element of F_Real

for ra being Real

for A being Matrix of n,F_Real

for rA being Matrix of n,REAL st a = ra & A = rA holds

a * A = ra * rA

for a being Element of F_Real

for ra being Real

for A being Matrix of n,F_Real

for rA being Matrix of n,REAL st a = ra & A = rA holds

a * A = ra * rA

proof end;

theorem Th47: :: BKMODEL1:55

for n being Nat

for a being Element of F_Real

for A, B being Matrix of n,F_Real st n > 0 holds

(a * A) * B = a * (A * B)

for a being Element of F_Real

for A, B being Matrix of n,F_Real st n > 0 holds

(a * A) * B = a * (A * B)

proof end;

theorem Th48: :: BKMODEL1:56

for a being Element of F_Real holds symmetric_3 (a,a,(- a),0,0,0) = a * (symmetric_3 (1,1,(- 1),0,0,0))

proof end;

theorem Th49: :: BKMODEL1:57

for a being Element of F_Real

for M being Matrix of 3,F_Real st M = symmetric_3 (a,a,(- a),0,0,0) holds

(M * M) * M = ((a * a) * a) * (symmetric_3 (1,1,(- 1),0,0,0))

for M being Matrix of 3,F_Real st M = symmetric_3 (a,a,(- a),0,0,0) holds

(M * M) * M = ((a * a) * a) * (symmetric_3 (1,1,(- 1),0,0,0))

proof end;

theorem Th50: :: BKMODEL1:58

for n being Nat

for a being Real

for M being Matrix of n,REAL

for x being FinSequence of REAL st n > 0 & len x = n holds

M * (a * x) = (a * M) * x

for a being Real

for M being Matrix of n,REAL

for x being FinSequence of REAL st n > 0 & len x = n holds

M * (a * x) = (a * M) * x

proof end;

theorem Th51: :: BKMODEL1:59

for n being Nat

for a being Real

for M being Matrix of n,REAL

for x being FinSequence of REAL st n > 0 & len x = n holds

a * (M * x) = (a * M) * x

for a being Real

for M being Matrix of n,REAL

for x being FinSequence of REAL st n > 0 & len x = n holds

a * (M * x) = (a * M) * x

proof end;

theorem Th52: :: BKMODEL1:60

for n being Nat

for N being Matrix of n,REAL st N is invertible holds

( N @ is invertible & Inv (N @) = (Inv N) @ )

for N being Matrix of n,REAL st N is invertible holds

( N @ is invertible & Inv (N @) = (Inv N) @ )

proof end;

theorem Th53: :: BKMODEL1:61

for ra being non zero Real

for N, O, M being Matrix of 3,3,REAL st N is invertible & M = ra * O & M = ((N @) * O) * N holds

(((Inv N) @) * O) * (Inv N) = (1 / ra) * O

for N, O, M being Matrix of 3,3,REAL st N is invertible & M = ra * O & M = ((N @) * O) * N holds

(((Inv N) @) * O) * (Inv N) = (1 / ra) * O

proof end;

theorem Th54: :: BKMODEL1:62

for ra being Real

for M, N being Matrix of 3,F_Real

for MR, NR being Matrix of 3,REAL st MR = M & NR = N & N is symmetric & MR = ra * NR holds

M is symmetric

for M, N being Matrix of 3,F_Real

for MR, NR being Matrix of 3,REAL st MR = M & NR = N & N is symmetric & MR = ra * NR holds

M is symmetric

proof end;

theorem Th55: :: BKMODEL1:63

for ra being Real

for O, M being Matrix of 3,REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O holds

( O * M = ra * (1_Rmatrix 3) & M * O = ra * (1_Rmatrix 3) )

for O, M being Matrix of 3,REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O holds

( O * M = ra * (1_Rmatrix 3) & M * O = ra * (1_Rmatrix 3) )

proof end;

theorem :: BKMODEL1:64

for ra being Real

for O, M being Matrix of 3,REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O holds

((((M @) * O) @) * O) * ((M @) * O) = (ra ^2) * O

for O, M being Matrix of 3,REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O holds

((((M @) * O) @) * O) * ((M @) * O) = (ra ^2) * O

proof end;

theorem :: BKMODEL1:65

for O, N being Matrix of 3,REAL holds ((((N @) * O) @) * O) * ((N @) * O) = ((O @) * ((N * O) * (N @))) * O

proof end;

theorem :: BKMODEL1:66

for NR, MR being Matrix of 3,REAL

for p1, p2, p3 being FinSequence of REAL st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & NR * p1 = MR * p1 & NR * p2 = MR * p2 & NR * p3 = MR * p3 holds

NR = MR

for p1, p2, p3 being FinSequence of REAL st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & NR * p1 = MR * p1 & NR * p2 = MR * p2 & NR * p3 = MR * p3 holds

NR = MR

proof end;

theorem Th56: :: BKMODEL1:67

for a being non zero Real

for u being Element of (TOP-REAL 3) st a * u = 0. (TOP-REAL 3) holds

u is zero

for u being Element of (TOP-REAL 3) st a * u = 0. (TOP-REAL 3) holds

u is zero

proof end;

theorem Th57: :: BKMODEL1:68

for u, v being non zero Element of (TOP-REAL 3)

for a, b being Real st ( a <> 0 or b <> 0 ) & (a * u) + (b * v) = 0. (TOP-REAL 3) holds

are_Prop u,v

for a, b being Real st ( a <> 0 or b <> 0 ) & (a * u) + (b * v) = 0. (TOP-REAL 3) holds

are_Prop u,v

proof end;

theorem :: BKMODEL1:69

for N being invertible Matrix of 3,F_Real

for P, Q, R being Point of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & (homography N) . P = Q & (homography N) . Q = P & P,Q,R are_collinear holds

(homography N) . ((homography N) . R) = R

for P, Q, R being Point of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & (homography N) . P = Q & (homography N) . Q = P & P,Q,R are_collinear holds

(homography N) . ((homography N) . R) = R

proof end;

theorem :: BKMODEL1:70

for n being Nat

for u, v being Element of (TOP-REAL n)

for a, b being Real st ((1 - a) * u) + (a * v) = ((1 - b) * v) + (b * u) holds

(1 - (a + b)) * u = (1 - (a + b)) * v

for u, v being Element of (TOP-REAL n)

for a, b being Real st ((1 - a) * u) + (a * v) = ((1 - b) * v) + (b * u) holds

(1 - (a + b)) * u = (1 - (a + b)) * v

proof end;

definition

ProjectiveSpace (TOP-REAL 3) is CollProjectivePlane by ANPROJ_8:57;

end;

func real_projective_plane -> CollProjectivePlane equals :: BKMODEL1:def 4

ProjectiveSpace (TOP-REAL 3);

coherence ProjectiveSpace (TOP-REAL 3);

ProjectiveSpace (TOP-REAL 3) is CollProjectivePlane by ANPROJ_8:57;

:: deftheorem defines real_projective_plane BKMODEL1:def 4 :

real_projective_plane = ProjectiveSpace (TOP-REAL 3);

real_projective_plane = ProjectiveSpace (TOP-REAL 3);

theorem :: BKMODEL1:72

for L being Element of ProjectiveLines real_projective_plane ex p, q being Point of real_projective_plane st

( p <> q & L = Line (p,q) )

( p <> q & L = Line (p,q) )

proof end;

theorem Th60: :: BKMODEL1:73

for L being LINE of (IncProjSp_of real_projective_plane) ex p, q being Point of real_projective_plane st

( p <> q & L = Line (p,q) )

( p <> q & L = Line (p,q) )

proof end;

theorem Th61: :: BKMODEL1:74

for R being POINT of (IncProjSp_of real_projective_plane)

for L being LINE of (IncProjSp_of real_projective_plane)

for p, q, r being Point of real_projective_plane st R = r & L = Line (p,q) holds

( R on L iff p,q,r are_collinear )

for L being LINE of (IncProjSp_of real_projective_plane)

for p, q, r being Point of real_projective_plane st R = r & L = Line (p,q) holds

( R on L iff p,q,r are_collinear )

proof end;

theorem :: BKMODEL1:77

for R being POINT of (IncProjSp_of real_projective_plane)

for L being LINE of (IncProjSp_of real_projective_plane)

for p, q being Point of real_projective_plane

for u, v, w being non zero Element of (TOP-REAL 3) st p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) holds

( R on L iff |{u,v,w}| = 0 )

for L being LINE of (IncProjSp_of real_projective_plane)

for p, q being Point of real_projective_plane

for u, v, w being non zero Element of (TOP-REAL 3) st p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) holds

( R on L iff |{u,v,w}| = 0 )

proof end;

theorem Th64: :: BKMODEL1:78

for u, v being non zero Element of (TOP-REAL 3)

for p, q being Element of (ProjectiveSpace (TOP-REAL 3)) st p <> q & p = Dir u & q = Dir v holds

not u <X> v is zero

for p, q being Element of (ProjectiveSpace (TOP-REAL 3)) st p <> q & p = Dir u & q = Dir v holds

not u <X> v is zero

proof end;

definition

let p, q be Point of real_projective_plane;

assume A1: p <> q ;

ex b_{1} being Point of real_projective_plane ex u, v being non zero Element of (TOP-REAL 3) st

( p = Dir u & q = Dir v & b_{1} = Dir (u <X> v) )

for b_{1}, b_{2} being Point of real_projective_plane st ex u, v being non zero Element of (TOP-REAL 3) st

( p = Dir u & q = Dir v & b_{1} = Dir (u <X> v) ) & ex u, v being non zero Element of (TOP-REAL 3) st

( p = Dir u & q = Dir v & b_{2} = Dir (u <X> v) ) holds

b_{1} = b_{2}

end;
assume A1: p <> q ;

func L2P (p,q) -> Point of real_projective_plane means :Def01: :: BKMODEL1:def 5

ex u, v being non zero Element of (TOP-REAL 3) st

( p = Dir u & q = Dir v & it = Dir (u <X> v) );

existence ex u, v being non zero Element of (TOP-REAL 3) st

( p = Dir u & q = Dir v & it = Dir (u <X> v) );

ex b

( p = Dir u & q = Dir v & b

proof end;

uniqueness for b

( p = Dir u & q = Dir v & b

( p = Dir u & q = Dir v & b

b

proof end;

:: deftheorem Def01 defines L2P BKMODEL1:def 5 :

for p, q being Point of real_projective_plane st p <> q holds

for b_{3} being Point of real_projective_plane holds

( b_{3} = L2P (p,q) iff ex u, v being non zero Element of (TOP-REAL 3) st

( p = Dir u & q = Dir v & b_{3} = Dir (u <X> v) ) );

for p, q being Point of real_projective_plane st p <> q holds

for b

( b

( p = Dir u & q = Dir v & b

theorem :: BKMODEL1:79

for p, q being Point of real_projective_plane st p <> q holds

( L2P (q,p) = L2P (p,q) & p <> L2P (p,q) )

( L2P (q,p) = L2P (p,q) & p <> L2P (p,q) )

proof end;

definition

let a, b, c, d, e, f be Real;

{ P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds

qfconic (a,b,c,d,e,f,u) is negative } is Subset of (ProjectiveSpace (TOP-REAL 3))

end;
func negative_conic (a,b,c,d,e,f) -> Subset of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL1:def 6

{ P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds

qfconic (a,b,c,d,e,f,u) is negative } ;

coherence { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds

qfconic (a,b,c,d,e,f,u) is negative } ;

{ P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds

qfconic (a,b,c,d,e,f,u) is negative } is Subset of (ProjectiveSpace (TOP-REAL 3))

proof end;

:: deftheorem defines negative_conic BKMODEL1:def 6 :

for a, b, c, d, e, f being Real holds negative_conic (a,b,c,d,e,f) = { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds

qfconic (a,b,c,d,e,f,u) is negative } ;

for a, b, c, d, e, f being Real holds negative_conic (a,b,c,d,e,f) = { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds

qfconic (a,b,c,d,e,f,u) is negative } ;

theorem :: BKMODEL1:81

for a, b, c, d, e, f being Real

for u1, u2 being non zero Element of (TOP-REAL 3) st Dir u1 = Dir u2 & qfconic (a,b,c,d,e,f,u1) is negative holds

qfconic (a,b,c,d,e,f,u2) is negative

for u1, u2 being non zero Element of (TOP-REAL 3) st Dir u1 = Dir u2 & qfconic (a,b,c,d,e,f,u1) is negative holds

qfconic (a,b,c,d,e,f,u2) is negative

proof end;

definition

conic (1,1,(- 1),0,0,0) is non empty Subset of (ProjectiveSpace (TOP-REAL 3))
end;

func absolute -> non empty Subset of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL1:def 7

conic (1,1,(- 1),0,0,0);

coherence conic (1,1,(- 1),0,0,0);

conic (1,1,(- 1),0,0,0) is non empty Subset of (ProjectiveSpace (TOP-REAL 3))

proof end;

theorem Th66: :: BKMODEL1:82

for u being non zero Element of (TOP-REAL 3)

for O being Matrix of 3,REAL

for P being Element of (ProjectiveSpace (TOP-REAL 3))

for p being FinSequence of REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p holds

( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )

for O being Matrix of 3,REAL

for P being Element of (ProjectiveSpace (TOP-REAL 3))

for p being FinSequence of REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & u = p holds

( P in absolute iff SumAll (QuadraticForm (p,O,p)) = 0 )

proof end;

theorem Th67: :: BKMODEL1:83

for u being non zero Element of (TOP-REAL 3)

for P being Element of absolute st P = Dir u holds

u . 3 <> 0

for P being Element of absolute st P = Dir u holds

u . 3 <> 0

proof end;

theorem Th68: :: BKMODEL1:84

for u being non zero Element of (TOP-REAL 3)

for P being Element of absolute st P = Dir u & u . 3 = 1 holds

|[(u . 1),(u . 2)]| in circle (0,0,1)

for P being Element of absolute st P = Dir u & u . 3 = 1 holds

|[(u . 1),(u . 2)]| in circle (0,0,1)

proof end;

theorem Th69: :: BKMODEL1:85

for u being non zero Element of (TOP-REAL 3)

for P being Point of (ProjectiveSpace (TOP-REAL 3)) st P = Dir u & u . 3 = 1 & |[(u . 1),(u . 2)]| in circle (0,0,1) holds

P is Element of absolute

for P being Point of (ProjectiveSpace (TOP-REAL 3)) st P = Dir u & u . 3 = 1 & |[(u . 1),(u . 2)]| in circle (0,0,1) holds

P is Element of absolute

proof end;

theorem :: BKMODEL1:86

definition

let P be Element of absolute ;

ex b_{1} being Element of circle (0,0,1) ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u . 3 = 1 & b_{1} = |[(u . 1),(u . 2)]| )

for b_{1}, b_{2} being Element of circle (0,0,1) st ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u . 3 = 1 & b_{1} = |[(u . 1),(u . 2)]| ) & ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u . 3 = 1 & b_{2} = |[(u . 1),(u . 2)]| ) holds

b_{1} = b_{2}

end;
func absolute_to_REAL2 P -> Element of circle (0,0,1) means :: BKMODEL1:def 8

ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u . 3 = 1 & it = |[(u . 1),(u . 2)]| );

existence ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u . 3 = 1 & it = |[(u . 1),(u . 2)]| );

ex b

( P = Dir u & u . 3 = 1 & b

proof end;

uniqueness for b

( P = Dir u & u . 3 = 1 & b

( P = Dir u & u . 3 = 1 & b

b

proof end;

:: deftheorem defines absolute_to_REAL2 BKMODEL1:def 8 :

for P being Element of absolute

for b_{2} being Element of circle (0,0,1) holds

( b_{2} = absolute_to_REAL2 P iff ex u being non zero Element of (TOP-REAL 3) st

( P = Dir u & u . 3 = 1 & b_{2} = |[(u . 1),(u . 2)]| ) );

for P being Element of absolute

for b

( b

( P = Dir u & u . 3 = 1 & b

definition

let u be non zero Element of (TOP-REAL 2);

assume A1: u in circle (0,0,1) ;

coherence

Dir |[(u . 1),(u . 2),1]| is Element of absolute

end;
assume A1: u in circle (0,0,1) ;

coherence

Dir |[(u . 1),(u . 2),1]| is Element of absolute

proof end;

:: deftheorem defines REAL2_to_absolute BKMODEL1:def 9 :

for u being non zero Element of (TOP-REAL 2) st u in circle (0,0,1) holds

REAL2_to_absolute u = Dir |[(u . 1),(u . 2),1]|;

for u being non zero Element of (TOP-REAL 2) st u in circle (0,0,1) holds

REAL2_to_absolute u = Dir |[(u . 1),(u . 2),1]|;

theorem Th70: :: BKMODEL1:88

for u being Element of (TOP-REAL 3) st qfconic (1,1,(- 1),0,0,0,u) = 0 & u . 3 = 1 holds

|[(u . 1),(u . 2)]| in Sphere ((0. (TOP-REAL 2)),1)

|[(u . 1),(u . 2)]| in Sphere ((0. (TOP-REAL 2)),1)

proof end;

theorem :: BKMODEL1:89

for P being Element of absolute ex u being non zero Element of (TOP-REAL 3) st

( ((u . 1) ^2) + ((u . 2) ^2) = 1 & u . 3 = 1 & P = Dir u )

( ((u . 1) ^2) + ((u . 2) ^2) = 1 & u . 3 = 1 & P = Dir u )

proof end;

theorem :: BKMODEL1:93

for ra being non zero Real

for O, N, M being invertible Matrix of 3,F_Real st O = symmetric_3 (1,1,(- 1),0,0,0) & M = symmetric_3 (ra,ra,(- ra),0,0,0) & M = ((N @) * O) * N & (homography M) .: absolute = absolute holds

(homography N) .: absolute = absolute

for O, N, M being invertible Matrix of 3,F_Real st O = symmetric_3 (1,1,(- 1),0,0,0) & M = symmetric_3 (ra,ra,(- ra),0,0,0) & M = ((N @) * O) * N & (homography M) .: absolute = absolute holds

(homography N) .: absolute = absolute

proof end;