:: by Roland Coghetto

::

:: Received March 27, 2018

:: Copyright (c) 2018-2019 Association of Mizar Users

definition

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

func BK_model -> non empty Subset of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL2:def 1

negative_conic (1,1,(- 1),0,0,0);

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

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

proof end;

theorem :: BKMODEL2:2

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

for u being non zero Element of (TOP-REAL 3) st P = Dir u & P in BK_model holds

u . 3 <> 0

for u being non zero Element of (TOP-REAL 3) st P = Dir u & P in BK_model holds

u . 3 <> 0

proof end;

definition

let P be Element of BK_model ;

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

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

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

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

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

b_{1} = b_{2}

end;
func BK_to_REAL2 P -> Element of inside_of_circle (0,0,1) means :Def01: :: BKMODEL2:def 2

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

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

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

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

ex b

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

proof end;

uniqueness for b

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

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

b

proof end;

:: deftheorem Def01 defines BK_to_REAL2 BKMODEL2:def 2 :

for P being Element of BK_model

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

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

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

for P being Element of BK_model

for b

( b

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

definition

let Q be Element of inside_of_circle (0,0,1);

ex b_{1} being Element of BK_model ex P being Element of (TOP-REAL 2) st

( P = Q & b_{1} = Dir |[(P `1),(P `2),1]| )

for b_{1}, b_{2} being Element of BK_model st ex P being Element of (TOP-REAL 2) st

( P = Q & b_{1} = Dir |[(P `1),(P `2),1]| ) & ex P being Element of (TOP-REAL 2) st

( P = Q & b_{2} = Dir |[(P `1),(P `2),1]| ) holds

b_{1} = b_{2}
;

end;
func REAL2_to_BK Q -> Element of BK_model means :Def02: :: BKMODEL2:def 3

ex P being Element of (TOP-REAL 2) st

( P = Q & it = Dir |[(P `1),(P `2),1]| );

existence ex P being Element of (TOP-REAL 2) st

( P = Q & it = Dir |[(P `1),(P `2),1]| );

ex b

( P = Q & b

proof end;

uniqueness for b

( P = Q & b

( P = Q & b

b

:: deftheorem Def02 defines REAL2_to_BK BKMODEL2:def 3 :

for Q being Element of inside_of_circle (0,0,1)

for b_{2} being Element of BK_model holds

( b_{2} = REAL2_to_BK Q iff ex P being Element of (TOP-REAL 2) st

( P = Q & b_{2} = Dir |[(P `1),(P `2),1]| ) );

for Q being Element of inside_of_circle (0,0,1)

for b

( b

( P = Q & b

theorem :: BKMODEL2:6

for P, Q being Element of BK_model

for P1, P2, P3 being Element of absolute st P <> Q & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & P,Q,P3 are_collinear & not P3 = P1 holds

P3 = P2

for P1, P2, P3 being Element of absolute st P <> Q & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & P,Q,P3 are_collinear & not P3 = P1 holds

P3 = P2

proof end;

theorem Th03: :: BKMODEL2:7

for P being Element of BK_model

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

for v being non zero Element of (TOP-REAL 3) st P <> Q & Q = Dir v & v . 3 = 1 holds

ex P1 being Element of absolute st P,Q,P1 are_collinear

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

for v being non zero Element of (TOP-REAL 3) st P <> Q & Q = Dir v & v . 3 = 1 holds

ex P1 being Element of absolute st P,Q,P1 are_collinear

proof end;

theorem :: BKMODEL2:8

for P being Element of BK_model

for L being LINE of (IncProjSp_of real_projective_plane) ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st

( P <> Q & Q in L )

for L being LINE of (IncProjSp_of real_projective_plane) ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st

( P <> Q & Q in L )

proof end;

theorem Th04: :: BKMODEL2:9

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

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

|{u,v,w}| = 0

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

|{u,v,w}| = 0

proof end;

theorem Th06: :: BKMODEL2:11

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

for a, b, c, d, e being Real st u = |[a,b,c]| & v = |[d,e,0]| & are_Prop u,v holds

c = 0

for a, b, c, d, e being Real st u = |[a,b,c]| & v = |[d,e,0]| & are_Prop u,v holds

c = 0

proof end;

theorem :: BKMODEL2:12

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

for u, v, w being non zero Element of (TOP-REAL 3) st P = Dir u & Q = Dir v & R = Dir w & u `3 <> 0 & v `3 = 0 & w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| holds

( R <> P & R <> Q )

for u, v, w being non zero Element of (TOP-REAL 3) st P = Dir u & Q = Dir v & R = Dir w & u `3 <> 0 & v `3 = 0 & w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| holds

( R <> P & R <> Q )

proof end;

theorem Th07: :: BKMODEL2:13

for L being LINE of (IncProjSp_of real_projective_plane)

for P, Q being Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & P in L & Q in L holds

L = Line (P,Q)

for P, Q being Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & P in L & Q in L holds

L = Line (P,Q)

proof end;

theorem :: BKMODEL2:14

for L being LINE of (IncProjSp_of real_projective_plane)

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

for u, v being non zero Element of (TOP-REAL 3) st P in L & Q in L & P = Dir u & Q = Dir v & u `3 <> 0 & v `3 = 0 holds

( P <> Q & Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L )

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

for u, v being non zero Element of (TOP-REAL 3) st P in L & Q in L & P = Dir u & Q = Dir v & u `3 <> 0 & v `3 = 0 holds

( P <> Q & Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L )

proof end;

theorem Th08: :: BKMODEL2:15

for u, v, w being Element of (TOP-REAL 3) st v `3 = 0 & w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| holds

|{u,v,w}| = 0

|{u,v,w}| = 0

proof end;

theorem Th09: :: BKMODEL2:16

for L being LINE of (IncProjSp_of real_projective_plane)

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

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

ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) ex v being non zero Element of (TOP-REAL 3) st

( Q = Dir v & Q in L & P <> Q & v . 3 <> 0 )

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

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

ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) ex v being non zero Element of (TOP-REAL 3) st

( Q = Dir v & Q in L & P <> Q & v . 3 <> 0 )

proof end;

theorem Th10: :: BKMODEL2:17

for P being Element of BK_model

for L being LINE of (IncProjSp_of real_projective_plane) st P in L holds

ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st

( P <> Q & Q in L & ( for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds

u . 3 <> 0 ) )

for L being LINE of (IncProjSp_of real_projective_plane) st P in L holds

ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st

( P <> Q & Q in L & ( for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds

u . 3 <> 0 ) )

proof end;

theorem Th11: :: BKMODEL2:18

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

for k being non zero Real st u = k * v holds

Dir u = Dir v

for k being non zero Real st u = k * v holds

Dir u = Dir v

proof end;

theorem :: BKMODEL2:19

for P being Element of BK_model

for Q being Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q holds

ex P1 being Element of absolute st P,Q,P1 are_collinear

for Q being Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q holds

ex P1 being Element of absolute st P,Q,P1 are_collinear

proof end;

theorem Th12: :: BKMODEL2:20

for P, Q being Element of BK_model st P <> Q holds

ex P1, P2 being Element of absolute st

( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear )

ex P1, P2 being Element of absolute st

( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear )

proof end;

theorem Th13: :: BKMODEL2:21

for P, Q, R being Element of real_projective_plane

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

for a, b, c, d being Real st P in BK_model & Q in absolute & P = Dir u & Q = Dir v & R = Dir w & u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds

( R in BK_model & R <> P & P,R,Q are_collinear )

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

for a, b, c, d being Real st P in BK_model & Q in absolute & P = Dir u & Q = Dir v & R = Dir w & u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds

( R in BK_model & R <> P & P,R,Q are_collinear )

proof end;

theorem Th14: :: BKMODEL2:22

for P, Q being Element of real_projective_plane st P in absolute & Q in BK_model holds

ex R being Element of real_projective_plane st

( R in BK_model & Q <> R & R,Q,P are_collinear )

ex R being Element of real_projective_plane st

( R in BK_model & Q <> R & R,Q,P are_collinear )

proof end;

theorem Th15: :: BKMODEL2:23

for L being LINE of (IncProjSp_of real_projective_plane)

for p, q being POINT of (IncProjSp_of real_projective_plane)

for P, Q being Element of real_projective_plane st p = P & q = Q & P in BK_model & Q in absolute & q on L & p on L holds

ex p1, p2 being POINT of (IncProjSp_of real_projective_plane) ex P1, P2 being Element of real_projective_plane st

( p1 = P1 & p2 = P2 & P1 <> P2 & P1 in absolute & P2 in absolute & p1 on L & p2 on L )

for p, q being POINT of (IncProjSp_of real_projective_plane)

for P, Q being Element of real_projective_plane st p = P & q = Q & P in BK_model & Q in absolute & q on L & p on L holds

ex p1, p2 being POINT of (IncProjSp_of real_projective_plane) ex P1, P2 being Element of real_projective_plane st

( p1 = P1 & p2 = P2 & P1 <> P2 & P1 in absolute & P2 in absolute & p1 on L & p2 on L )

proof end;

theorem Th16: :: BKMODEL2:24

for P being Element of BK_model

for Q being Element of absolute ex R being Element of absolute st

( Q <> R & Q,P,R are_collinear )

for Q being Element of absolute ex R being Element of absolute st

( Q <> R & Q,P,R are_collinear )

proof end;

theorem Th17: :: BKMODEL2:25

for P being Element of BK_model

for u being non zero Element of (TOP-REAL 3) st P = Dir u & u . 3 = 1 holds

((u . 1) ^2) + ((u . 2) ^2) < 1

for u being non zero Element of (TOP-REAL 3) st P = Dir u & u . 3 = 1 holds

((u . 1) ^2) + ((u . 2) ^2) < 1

proof end;

theorem Th18: :: BKMODEL2:26

for P1, P2 being Element of absolute

for Q being Element of BK_model

for u, v, w being non zero Element of (TOP-REAL 3) st Dir u = P1 & Dir v = P2 & Dir w = Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 1 & v . 1 = - (u . 1) & v . 2 = - (u . 2) & P1,Q,P2 are_collinear holds

ex a being Real st

( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )

for Q being Element of BK_model

for u, v, w being non zero Element of (TOP-REAL 3) st Dir u = P1 & Dir v = P2 & Dir w = Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 1 & v . 1 = - (u . 1) & v . 2 = - (u . 2) & P1,Q,P2 are_collinear holds

ex a being Real st

( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )

proof end;

definition

let P be Element of absolute ;

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

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

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

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

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

b_{1} = b_{2}

end;
func pole_infty P -> Element of real_projective_plane means :Def03: :: BKMODEL2:def 4

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

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

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

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

ex b

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

proof end;

uniqueness for b

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

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

b

proof end;

:: deftheorem Def03 defines pole_infty BKMODEL2:def 4 :

for P being Element of absolute

for b_{2} being Element of real_projective_plane holds

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

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

for P being Element of absolute

for b

( b

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

theorem Th20: :: BKMODEL2:28

for P1, P2 being Element of absolute holds

( not pole_infty P1 = pole_infty P2 or P1 = P2 or ex u being non zero Element of (TOP-REAL 3) st

( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )

( not pole_infty P1 = pole_infty P2 or P1 = P2 or ex u being non zero Element of (TOP-REAL 3) st

( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )

proof end;

definition

let P be Element of absolute ;

ex b_{1} being LINE of real_projective_plane ex p being Element of real_projective_plane st

( p = P & b_{1} = Line (p,(pole_infty P)) )

for b_{1}, b_{2} being LINE of real_projective_plane st ex p being Element of real_projective_plane st

( p = P & b_{1} = Line (p,(pole_infty P)) ) & ex p being Element of real_projective_plane st

( p = P & b_{2} = Line (p,(pole_infty P)) ) holds

b_{1} = b_{2}
;

end;
func tangent P -> LINE of real_projective_plane means :Def04: :: BKMODEL2:def 5

ex p being Element of real_projective_plane st

( p = P & it = Line (p,(pole_infty P)) );

existence ex p being Element of real_projective_plane st

( p = P & it = Line (p,(pole_infty P)) );

ex b

( p = P & b

proof end;

uniqueness for b

( p = P & b

( p = P & b

b

:: deftheorem Def04 defines tangent BKMODEL2:def 5 :

for P being Element of absolute

for b_{2} being LINE of real_projective_plane holds

( b_{2} = tangent P iff ex p being Element of real_projective_plane st

( p = P & b_{2} = Line (p,(pole_infty P)) ) );

for P being Element of absolute

for b

( b

( p = P & b

theorem Th24: :: BKMODEL2:32

for P, Q being Element of absolute ex R being Element of real_projective_plane st

( R in tangent P & R in tangent Q )

( R in tangent P & R in tangent Q )

proof end;

theorem Th25: :: BKMODEL2:33

for P1, P2 being Element of absolute st P1 <> P2 holds

ex P being Element of real_projective_plane st (tangent P1) /\ (tangent P2) = {P}

ex P being Element of real_projective_plane st (tangent P1) /\ (tangent P2) = {P}

proof end;

theorem Th26: :: BKMODEL2:34

for M being Matrix of 3,REAL

for P being Element of absolute

for Q being Element of real_projective_plane

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

for fp, fq being FinSequence of REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & Q = Dir v & u = fp & v = fq & Q in tangent P holds

SumAll (QuadraticForm (fq,M,fp)) = 0

for P being Element of absolute

for Q being Element of real_projective_plane

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

for fp, fq being FinSequence of REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & Q = Dir v & u = fp & v = fq & Q in tangent P holds

SumAll (QuadraticForm (fq,M,fp)) = 0

proof end;

theorem Th27: :: BKMODEL2:35

for P, Q, R being Element of absolute

for P1, P2, P3, P4 being Point of real_projective_plane st P,Q,R are_mutually_distinct & P1 = P & P2 = Q & P3 = R & P4 in tangent P & P4 in tangent Q holds

( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear )

for P1, P2, P3, P4 being Point of real_projective_plane st P,Q,R are_mutually_distinct & P1 = P & P2 = Q & P3 = R & P4 in tangent P & P4 in tangent Q holds

( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear )

proof end;

theorem :: BKMODEL2:36

for P, Q being Element of absolute

for R being Element 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 & R in tangent P & R in tangent Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 0 & not P = Q holds

( u . 1 = - (v . 1) & u . 2 = - (v . 2) )

for R being Element 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 & R in tangent P & R in tangent Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 0 & not P = Q holds

( u . 1 = - (v . 1) & u . 2 = - (v . 2) )

proof end;

theorem Th28: :: BKMODEL2:37

for P being Element of absolute

for R being Element of real_projective_plane

for u being non zero Element of (TOP-REAL 3) st R in tangent P & R = Dir u & u . 3 = 0 holds

R = pole_infty P

for R being Element of real_projective_plane

for u being non zero Element of (TOP-REAL 3) st R in tangent P & R = Dir u & u . 3 = 0 holds

R = pole_infty P

proof end;

theorem Th29: :: BKMODEL2:38

for a being non zero Real

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

(homography N) .: absolute = absolute

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

(homography N) .: absolute = absolute

proof end;

theorem :: BKMODEL2:39

for ra being non zero Element of F_Real

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

(homography M) .: absolute = absolute

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

(homography M) .: absolute = absolute

proof end;

theorem Th31: :: BKMODEL2:41

for P, PP1, PP2 being Element of real_projective_plane

for P1, P2 being Element of absolute

for Q being Element of real_projective_plane st P1 <> P2 & PP1 = P1 & PP2 = P2 & P in BK_model & P,PP1,PP2 are_collinear & Q in tangent P1 & Q in tangent P2 holds

ex R being Element of real_projective_plane st

( R in absolute & P,Q,R are_collinear )

for P1, P2 being Element of absolute

for Q being Element of real_projective_plane st P1 <> P2 & PP1 = P1 & PP2 = P2 & P in BK_model & P,PP1,PP2 are_collinear & Q in tangent P1 & Q in tangent P2 holds

ex R being Element of real_projective_plane st

( R in absolute & P,Q,R are_collinear )

proof end;

theorem Th32: :: BKMODEL2:42

for P, R, S being Element of real_projective_plane

for Q being Element of absolute st P in BK_model & R in tangent Q & P,S,R are_collinear & R <> S holds

Q <> S

for Q being Element of absolute st P in BK_model & R in tangent Q & P,S,R are_collinear & R <> S holds

Q <> S

proof end;

definition

let h be Element of EnsHomography3 ;

end;
pred h is_K-isometry means :: BKMODEL2:def 6

ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) .: absolute = absolute );

ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) .: absolute = absolute );

:: deftheorem defines is_K-isometry BKMODEL2:def 6 :

for h being Element of EnsHomography3 holds

( h is_K-isometry iff ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) .: absolute = absolute ) );

for h being Element of EnsHomography3 holds

( h is_K-isometry iff ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) .: absolute = absolute ) );

definition

{ h where h is Element of EnsHomography3 : h is_K-isometry } is non empty Subset of EnsHomography3
end;

func EnsK-isometry -> non empty Subset of EnsHomography3 equals :: BKMODEL2:def 7

{ h where h is Element of EnsHomography3 : h is_K-isometry } ;

coherence { h where h is Element of EnsHomography3 : h is_K-isometry } ;

{ h where h is Element of EnsHomography3 : h is_K-isometry } is non empty Subset of EnsHomography3

proof end;

:: deftheorem defines EnsK-isometry BKMODEL2:def 7 :

EnsK-isometry = { h where h is Element of EnsHomography3 : h is_K-isometry } ;

EnsK-isometry = { h where h is Element of EnsHomography3 : h is_K-isometry } ;

definition

ex b_{1} being strict Subgroup of GroupHomography3 st the carrier of b_{1} = EnsK-isometry

for b_{1}, b_{2} being strict Subgroup of GroupHomography3 st the carrier of b_{1} = EnsK-isometry & the carrier of b_{2} = EnsK-isometry holds

b_{1} = b_{2}
end;

func SubGroupK-isometry -> strict Subgroup of GroupHomography3 means :Def05: :: BKMODEL2:def 8

the carrier of it = EnsK-isometry ;

existence the carrier of it = EnsK-isometry ;

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def05 defines SubGroupK-isometry BKMODEL2:def 8 :

for b_{1} being strict Subgroup of GroupHomography3 holds

( b_{1} = SubGroupK-isometry iff the carrier of b_{1} = EnsK-isometry );

for b

( b

theorem :: BKMODEL2:44

for h being Element of EnsK-isometry

for N being invertible Matrix of 3,F_Real st h = homography N holds

(homography N) .: absolute = absolute

for N being invertible Matrix of 3,F_Real st h = homography N holds

(homography N) .: absolute = absolute

proof end;

theorem Th34: :: BKMODEL2:45

( homography (1. (F_Real,3)) = 1_ GroupHomography3 & homography (1. (F_Real,3)) = 1_ SubGroupK-isometry )

proof end;

theorem Th35: :: BKMODEL2:46

for N1, N2 being invertible Matrix of 3,F_Real

for h1, h2 being Element of SubGroupK-isometry st h1 = homography N1 & h2 = homography N2 holds

( h1 * h2 is Element of SubGroupK-isometry & h1 * h2 = homography (N1 * N2) )

for h1, h2 being Element of SubGroupK-isometry st h1 = homography N1 & h2 = homography N2 holds

( h1 * h2 is Element of SubGroupK-isometry & h1 * h2 = homography (N1 * N2) )

proof end;

theorem Th36: :: BKMODEL2:47

for N being invertible Matrix of 3,F_Real

for h being Element of SubGroupK-isometry st h = homography N holds

( h " = homography (N ~) & homography (N ~) is Element of SubGroupK-isometry )

for h being Element of SubGroupK-isometry st h = homography N holds

( h " = homography (N ~) & homography (N ~) is Element of SubGroupK-isometry )

proof end;

theorem Th37: :: BKMODEL2:48

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

for p, q, r being Element of absolute st p,q,r are_mutually_distinct & s in (tangent p) /\ (tangent q) holds

ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . Dir101 = p & (homography N) . Dirm101 = q & (homography N) . Dir011 = r & (homography N) . Dir010 = s )

for p, q, r being Element of absolute st p,q,r are_mutually_distinct & s in (tangent p) /\ (tangent q) holds

ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . Dir101 = p & (homography N) . Dirm101 = q & (homography N) . Dir011 = r & (homography N) . Dir010 = s )

proof end;

theorem Th38: :: BKMODEL2:49

for p1, q1, r1, p2, q2, r2 being Element of absolute

for s1, s2 being Element of real_projective_plane st p1,q1,r1 are_mutually_distinct & p2,q2,r2 are_mutually_distinct & s1 in (tangent p1) /\ (tangent q1) & s2 in (tangent p2) /\ (tangent q2) holds

ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . p1 = p2 & (homography N) . q1 = q2 & (homography N) . r1 = r2 & (homography N) . s1 = s2 )

for s1, s2 being Element of real_projective_plane st p1,q1,r1 are_mutually_distinct & p2,q2,r2 are_mutually_distinct & s1 in (tangent p1) /\ (tangent q1) & s2 in (tangent p2) /\ (tangent q2) holds

ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . p1 = p2 & (homography N) . q1 = q2 & (homography N) . r1 = r2 & (homography N) . s1 = s2 )

proof end;

theorem :: BKMODEL2:50

for p1, q1, r1, p2, q2, r2 being Element of absolute st p1,q1,r1 are_mutually_distinct & p2,q2,r2 are_mutually_distinct holds

ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . p1 = p2 & (homography N) . q1 = q2 & (homography N) . r1 = r2 )

ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . p1 = p2 & (homography N) . q1 = q2 & (homography N) . r1 = r2 )

proof end;

theorem Th41: :: BKMODEL2:53

for N being invertible Matrix of 3,F_Real

for p, q, r, s being Element of (ProjectiveSpace (TOP-REAL 3)) st Line (((homography N) . p),((homography N) . q)) = Line (((homography N) . r),((homography N) . s)) holds

( p,q,r are_collinear & p,q,s are_collinear & r,s,p are_collinear & r,s,q are_collinear )

for p, q, r, s being Element of (ProjectiveSpace (TOP-REAL 3)) st Line (((homography N) . p),((homography N) . q)) = Line (((homography N) . r),((homography N) . s)) holds

( p,q,r are_collinear & p,q,s are_collinear & r,s,p are_collinear & r,s,q are_collinear )

proof end;

theorem Th42: :: BKMODEL2:54

for N being invertible Matrix of 3,F_Real

for p, q, r, s, t, u, np, nq, nr, ns being Element of real_projective_plane st p <> q & r <> s & np <> nq & nr <> ns & p,q,t are_collinear & r,s,t are_collinear & np = (homography N) . p & nq = (homography N) . q & nr = (homography N) . r & ns = (homography N) . s & np,nq,u are_collinear & nr,ns,u are_collinear & not u = (homography N) . t holds

Line (np,nq) = Line (nr,ns)

for p, q, r, s, t, u, np, nq, nr, ns being Element of real_projective_plane st p <> q & r <> s & np <> nq & nr <> ns & p,q,t are_collinear & r,s,t are_collinear & np = (homography N) . p & nq = (homography N) . q & nr = (homography N) . r & ns = (homography N) . s & np,nq,u are_collinear & nr,ns,u are_collinear & not u = (homography N) . t holds

Line (np,nq) = Line (nr,ns)

proof end;

theorem Th43: :: BKMODEL2:55

for N being invertible Matrix of 3,F_Real

for p, q, r, s, t, u, np, nq, nr, ns being Element of real_projective_plane st p <> q & r <> s & np <> nq & nr <> ns & p,q,t are_collinear & r,s,t are_collinear & np = (homography N) . p & nq = (homography N) . q & nr = (homography N) . r & ns = (homography N) . s & np,nq,u are_collinear & nr,ns,u are_collinear & not p,q,r are_collinear holds

u = (homography N) . t

for p, q, r, s, t, u, np, nq, nr, ns being Element of real_projective_plane st p <> q & r <> s & np <> nq & nr <> ns & p,q,t are_collinear & r,s,t are_collinear & np = (homography N) . p & nq = (homography N) . q & nr = (homography N) . r & ns = (homography N) . s & np,nq,u are_collinear & nr,ns,u are_collinear & not p,q,r are_collinear holds

u = (homography N) . t

proof end;

theorem :: BKMODEL2:56

for p, q being Element of absolute

for a, b being Element of BK_model ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . a = b & (homography N) . p = q )

for a, b being Element of BK_model ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . a = b & (homography N) . p = q )

proof end;

theorem :: BKMODEL2:57

for p, q, r, s being Element of absolute st p,q,r are_mutually_distinct & q,p,s are_mutually_distinct holds

ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . p = q & (homography N) . q = p & (homography N) . r = s & ( for t being Element of real_projective_plane st t in (tangent p) /\ (tangent q) holds

(homography N) . t = t ) )

ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . p = q & (homography N) . q = p & (homography N) . r = s & ( for t being Element of real_projective_plane st t in (tangent p) /\ (tangent q) holds

(homography N) . t = t ) )

proof end;

theorem Th44: :: BKMODEL2:58

for P, Q being Element of BK_model st P <> Q holds

ex P1, P2, P3, P4 being Element of absolute ex P5 being Element of (ProjectiveSpace (TOP-REAL 3)) st

( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & P,P5,P3 are_collinear & Q,P5,P4 are_collinear & P1,P2,P3 are_mutually_distinct & P1,P2,P4 are_mutually_distinct & P5 in (tangent P1) /\ (tangent P2) )

ex P1, P2, P3, P4 being Element of absolute ex P5 being Element of (ProjectiveSpace (TOP-REAL 3)) st

( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & P,P5,P3 are_collinear & Q,P5,P4 are_collinear & P1,P2,P3 are_mutually_distinct & P1,P2,P4 are_mutually_distinct & P5 in (tangent P1) /\ (tangent P2) )

proof end;

theorem Th45: :: BKMODEL2:59

for P, Q being Element of BK_model st P <> Q holds

ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . P = Q & (homography N) . Q = P & ex P1, P2 being Element of absolute st

( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & (homography N) . P1 = P2 & (homography N) . P2 = P1 ) )

ex N being invertible Matrix of 3,F_Real st

( (homography N) .: absolute = absolute & (homography N) . P = Q & (homography N) . Q = P & ex P1, P2 being Element of absolute st

( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & (homography N) . P1 = P2 & (homography N) . P2 = P1 ) )

proof end;

theorem :: BKMODEL2:60

for P, Q being Element of BK_model ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st

( h = homography N & (homography N) . P = Q & (homography N) . Q = P )

( h = homography N & (homography N) . P = Q & (homography N) . Q = P )

proof end;

theorem :: BKMODEL2:61

for P, Q, R, S, T, U being Element of BK_model st ex h1, h2 being Element of SubGroupK-isometry ex N1, N2 being invertible Matrix of 3,F_Real st

( h1 = homography N1 & h2 = homography N2 & (homography N1) . P = R & (homography N1) . Q = S & (homography N2) . R = T & (homography N2) . S = U ) holds

ex h3 being Element of SubGroupK-isometry ex N3 being invertible Matrix of 3,F_Real st

( h3 = homography N3 & (homography N3) . P = T & (homography N3) . Q = U )

( h1 = homography N1 & h2 = homography N2 & (homography N1) . P = R & (homography N1) . Q = S & (homography N2) . R = T & (homography N2) . S = U ) holds

ex h3 being Element of SubGroupK-isometry ex N3 being invertible Matrix of 3,F_Real st

( h3 = homography N3 & (homography N3) . P = T & (homography N3) . Q = U )

proof end;

theorem :: BKMODEL2:62

for P, Q, R being Element of BK_model

for h being Element of SubGroupK-isometry

for N being invertible Matrix of 3,F_Real st h = homography N & (homography N) . P = R & (homography N) . Q = R holds

P = Q by ANPROJ_9:16;

for h being Element of SubGroupK-isometry

for N being invertible Matrix of 3,F_Real st h = homography N & (homography N) . P = R & (homography N) . Q = R holds

P = Q by ANPROJ_9:16;