bkmodel3.miz



    begin

    theorem :: BKMODEL3:1

    for x,y be Real st (x * y) < 0 holds 0 < (x / (x - y)) < 1

    proof

      let x,y be Real;

      assume

       A1: (x * y) < 0 ;

      then x <> 0 & y <> 0 ;

      per cases ;

        suppose

         A2: x < 0 ;

        then y > 0 by A1;

        then (x - y) < x by XREAL_1: 44;

        hence thesis by A2, XREAL_1: 190;

      end;

        suppose

         A3: 0 < x;

        then y < 0 by A1;

        then x < (x - y) by XREAL_1: 46;

        hence thesis by A3, XREAL_1: 189;

      end;

    end;

    theorem :: BKMODEL3:2

    

     Th02: for a be non zero Real, b,r be Real st r = ( sqrt ((a ^2 ) + (b ^2 ))) holds r is positive & (((a / r) ^2 ) + ((b / r) ^2 )) = 1

    proof

      let a be non zero Real;

      let b,r be Real;

      assume

       A1: r = ( sqrt ((a ^2 ) + (b ^2 )));

      thus r is positive by A1, SQUARE_1: 25;

      reconsider r as positive Real by A1, SQUARE_1: 25;

      ((a / r) ^2 ) = ((a ^2 ) / (r ^2 )) & ((b / r) ^2 ) = ((b ^2 ) / (r ^2 )) by XCMPLX_1: 76;

      

      then (((a / r) ^2 ) + ((b / r) ^2 )) = (((a ^2 ) + (b ^2 )) / (r ^2 ))

      .= ((r ^2 ) / (r ^2 )) by A1, SQUARE_1:def 2

      .= 1 by XCMPLX_1: 60;

      hence thesis;

    end;

    theorem :: BKMODEL3:3

    

     Th03: for a be non zero Real, b,c,d,e be Real st (a * b) = (c - (d * e)) holds (b ^2 ) = ((((c ^2 ) / (a ^2 )) - ((2 * ((c * d) / (a * a))) * e)) + (((d ^2 ) / (a ^2 )) * (e ^2 )))

    proof

      let a be non zero Real;

      let b,c,d,e be Real;

      assume

       A1: (a * b) = (c - (d * e));

      b = ((a * b) / a) by XCMPLX_1: 89

      .= ((c / a) - ((d * e) / a)) by A1, XCMPLX_1: 120

      .= ((c / a) - ((d / a) * e));

      

      then (b ^2 ) = ((((c / a) ^2 ) - ((2 * (c / a)) * ((d / a) * e))) + (((d / a) * e) ^2 ))

      .= ((((c ^2 ) / (a ^2 )) - ((2 * (c / a)) * ((d / a) * e))) + (((d / a) ^2 ) * (e ^2 ))) by XCMPLX_1: 76

      .= ((((c ^2 ) / (a ^2 )) - ((2 * ((c / a) * (d / a))) * e)) + (((d ^2 ) / (a ^2 )) * (e ^2 ))) by XCMPLX_1: 76

      .= ((((c ^2 ) / (a ^2 )) - ((2 * ((c * d) / (a * a))) * e)) + (((d ^2 ) / (a ^2 )) * (e ^2 ))) by XCMPLX_1: 76;

      hence thesis;

    end;

    theorem :: BKMODEL3:4

    

     Th04: for a,b,c be Complex st a <> 0 holds ((((a ^2 ) * b) * c) / (a ^2 )) = (b * c)

    proof

      let a,b,c be Complex;

      assume

       A1: a <> 0 ;

      ((((a ^2 ) * b) * c) / (a ^2 )) = ((b * (a ^2 )) * (c / (a ^2 )))

      .= (b * c) by A1, XCMPLX_1: 90;

      hence thesis;

    end;

    theorem :: BKMODEL3:5

    

     Th05: for a,b,c be Complex st a <> 0 holds (((2 * ((a ^2 ) * b)) * c) / (a ^2 )) = ((2 * b) * c)

    proof

      let a,b,c be Complex;

      assume a <> 0 ;

      then ((((a ^2 ) * b) * c) / (a ^2 )) = (b * c) by Th04;

      hence thesis;

    end;

    theorem :: BKMODEL3:6

    

     Th07: for a be Real st 1 < a holds ((1 / a) - 1) < 0

    proof

      let a be Real;

      assume 1 < a;

      then (1 / a) < (1 / 1) by XREAL_1: 76;

      then ((1 / a) - 1) < (1 - 1) by XREAL_1: 9;

      hence thesis;

    end;

    theorem :: BKMODEL3:7

    

     Th08: for a,b be Real st 0 < a & 1 < b holds ((a / b) - a) < 0

    proof

      let a,b be Real;

      assume that

       A1: 0 < a and

       A2: 1 < b;

      

       A3: ((a / b) - a) = (a * ((1 / b) - 1));

      ((1 / b) - 1) < 0 by A2, Th07;

      hence thesis by A1, A3;

    end;

    theorem :: BKMODEL3:8

    

     Th09: for a be non zero Real, b,c,d be Real st ((a ^2 ) + (c ^2 )) = (b ^2 ) & 1 < (b ^2 ) holds not ((((((b ^2 ) ^2 ) / (a ^2 )) - ((2 * (((b ^2 ) * c) / (a * a))) * d)) + (((c ^2 ) / (a ^2 )) * (d ^2 ))) + (d ^2 )) = 1

    proof

      let a be non zero Real;

      let b,c,d be Real;

      assume that

       A1: ((a ^2 ) + (c ^2 )) = (b ^2 ) and

       A2: 1 < (b ^2 );

      assume

       A5: ((((((b ^2 ) ^2 ) / (a ^2 )) - ((2 * (((b ^2 ) * c) / (a * a))) * d)) + (((c ^2 ) / (a ^2 )) * (d ^2 ))) + (d ^2 )) = 1;

      (((c ^2 ) / (a ^2 )) + 1) = (((c ^2 ) / (a ^2 )) + ((a ^2 ) / (a ^2 ))) by XCMPLX_1: 60

      .= ((b ^2 ) / (a ^2 )) by A1;

      

      then

       A6: ((a ^2 ) * (((c ^2 ) / (a ^2 )) + 1)) = (((a ^2 ) * (b ^2 )) / (a ^2 )) by XCMPLX_1: 74

      .= (b ^2 ) by XCMPLX_1: 89;

      

       A7: ((a ^2 ) * (2 * (((b ^2 ) * c) / (a * a)))) = (2 * (((a ^2 ) * ((b ^2 ) * c)) / (a * a)))

      .= (2 * ((b ^2 ) * c)) by XCMPLX_1: 89;

      

       A8: (((a ^2 ) * (((b ^2 ) ^2 ) / (a ^2 ))) - ((a ^2 ) * 1)) = ((((a ^2 ) * ((b ^2 ) ^2 )) / (a ^2 )) - ((a ^2 ) * 1))

      .= (((b ^2 ) ^2 ) - (a ^2 )) by XCMPLX_1: 89;

      ((a ^2 ) * 0 ) = ((a ^2 ) * (((((((c ^2 ) / (a ^2 )) + 1) * (d ^2 )) - ((2 * (((b ^2 ) * c) / (a * a))) * d)) + (((b ^2 ) ^2 ) / (a ^2 ))) - 1)) by A5;

      then

       A9: 0 = ((((((a ^2 ) * (((c ^2 ) / (a ^2 )) + 1)) * (d ^2 )) - ((((a ^2 ) * 2) * (((b ^2 ) * c) / (a * a))) * d)) + ((a ^2 ) * (((b ^2 ) ^2 ) / (a ^2 )))) - ((a ^2 ) * 1));

      

       A11: b <> 0 by A6;

      

       A12: 0 = ((((((b ^2 ) * (d ^2 )) - ((2 * ((b ^2 ) * c)) * d)) + ((b ^2 ) ^2 )) - (a ^2 )) / (b ^2 )) by A9, A6, A7, A8

      .= ((((((d ^2 ) * (b ^2 )) / (b ^2 )) - (((2 * ((b ^2 ) * c)) * d) / (b ^2 ))) + (((b ^2 ) ^2 ) / (b ^2 ))) - ((a ^2 ) / (b ^2 )))

      .= ((((d ^2 ) - (((2 * ((b ^2 ) * c)) * d) / (b ^2 ))) + (((b ^2 ) ^2 ) / (b ^2 ))) - ((a ^2 ) / (b ^2 ))) by A6, XCMPLX_1: 89

      .= ((((d ^2 ) - ((2 * c) * d)) + (((b ^2 ) ^2 ) / (b ^2 ))) - ((a ^2 ) / (b ^2 ))) by A11, Th05

      .= ((((d ^2 ) + (( - (2 * c)) * d)) + (b ^2 )) - ((a ^2 ) / (b ^2 ))) by A6, XCMPLX_1: 89

      .= (((1 * (d ^2 )) + (( - (2 * c)) * d)) + ((b ^2 ) - ((a ^2 ) / (b ^2 ))));

      reconsider c1 = 1, c2 = ( - (2 * c)), c3 = ((b ^2 ) - ((a ^2 ) / (b ^2 ))) as Real;

      

       A13: (((a ^2 ) / (b ^2 )) - (a ^2 )) < 0 by A2, Th08;

      ( delta (c1,c2,c3)) < 0

      proof

        ((c2 ^2 ) - ((4 * c1) * c3)) = (4 * ((c ^2 ) - ((b ^2 ) - ((a ^2 ) / (b ^2 )))));

        hence thesis by A1, A13, QUIN_1:def 1;

      end;

      hence contradiction by A12, QUIN_1: 3;

    end;

    theorem :: BKMODEL3:9

    

     Th10: for a,b,c be Real st (a * ( - b)) = c & (a * c) = b holds c = 0 & b = 0

    proof

      let a,b,c be Real;

      assume that

       A1: (a * ( - b)) = c and

       A2: (a * c) = b;

      (a * ( - (a * c))) = c by A1, A2;

      then

       A3: (( - (a * a)) * c) = c;

      thus c = 0

      proof

        assume c <> 0 ;

        then ( - (a ^2 )) = 1 by A3, XCMPLX_1: 7;

        hence contradiction;

      end;

      hence b = 0 by A2;

    end;

    theorem :: BKMODEL3:10

    for a be positive Real holds (( sqrt a) / a) = (1 / ( sqrt a))

    proof

      let a be positive Real;

      a = ( sqrt (a ^2 )) by SQUARE_1:def 2

      .= (( sqrt a) * ( sqrt a)) by SQUARE_1: 29;

      then (( sqrt a) / a) = ((( sqrt a) / ( sqrt a)) / ( sqrt a)) by XCMPLX_1: 78;

      hence thesis by XCMPLX_1: 60, SQUARE_1: 24;

    end;

    registration

      let a be non zero Real;

      let b,c be Real;

      cluster |[a, b, c]| -> non zero;

      coherence

      proof

        now

          assume |[a, b, c]| is zero;

          then a = ( |[ 0 , 0 , 0 ]| `1 ) by EUCLID_5: 2, EUCLID_5: 4;

          hence contradiction by EUCLID_5: 2;

        end;

        hence thesis;

      end;

      cluster |[c, a, b]| -> non zero;

      coherence

      proof

        now

          assume |[c, a, b]| is zero;

          then a = ( |[ 0 , 0 , 0 ]| `2 ) by EUCLID_5: 2, EUCLID_5: 4;

          hence contradiction by EUCLID_5: 2;

        end;

        hence thesis;

      end;

      cluster |[b, c, a]| -> non zero;

      coherence

      proof

        now

          assume |[b, c, a]| is zero;

          then a = ( |[ 0 , 0 , 0 ]| `3 ) by EUCLID_5: 2, EUCLID_5: 4;

          hence contradiction by EUCLID_5: 2;

        end;

        hence thesis;

      end;

    end

    definition

      let P be Element of real_projective_plane ;

      assume

       A0: P in ( absolute \/ BK_model );

      :: BKMODEL3:def1

      func # P -> non zero Element of ( TOP-REAL 3) means

      : Def01: ( Dir it ) = P & (it . 3) = 1;

      existence

      proof

        per cases by A0, XBOOLE_0:def 3;

          suppose P in absolute ;

          then

          reconsider P1 = P as Element of absolute ;

          consider u be non zero Element of ( TOP-REAL 3) such that

           A1: P1 = ( Dir u) & (u . 3) = 1 and ( absolute_to_REAL2 P1) = |[(u . 1), (u . 2)]| by BKMODEL1:def 8;

          take u;

          thus thesis by A1;

        end;

          suppose P in BK_model ;

          then

          reconsider P1 = P as Element of BK_model ;

          consider u be non zero Element of ( TOP-REAL 3) such that

           A2: ( Dir u) = P1 & (u . 3) = 1 and ( BK_to_REAL2 P1) = |[(u . 1), (u . 2)]| by BKMODEL2:def 2;

          take u;

          thus thesis by A2;

        end;

      end;

      uniqueness

      proof

        let u,v be non zero Element of ( TOP-REAL 3) such that

         A3: ( Dir u) = P & (u . 3) = 1 and

         A4: ( Dir v) = P & (v . 3) = 1;

         are_Prop (u,v) by A3, A4, ANPROJ_1: 22;

        then

        consider a be Real such that a <> 0 and

         A5: u = (a * v) by ANPROJ_1: 1;

        1 = (a * (v . 3)) by A5, A3, RVSUM_1: 44

        .= a by A4;

        hence thesis by A5, RVSUM_1: 52;

      end;

    end

    theorem :: BKMODEL3:11

    

     Th11: for P be Element of real_projective_plane holds ex Q be Element of BK_model st P <> Q

    proof

      let P be Element of real_projective_plane ;

      per cases ;

        suppose

         A1: ( # P) = |[ 0 , 0 , 1]|;

        reconsider u = |[ 0 , (1 / 2), 1]| as non zero Element of ( TOP-REAL 3);

        reconsider Q = ( Dir u) as Point of ( ProjectiveSpace ( TOP-REAL 3)) by ANPROJ_1: 26;

        now

          let v be Element of ( TOP-REAL 3);

          assume v is non zero & Q = ( Dir v);

          then are_Prop (u,v) by ANPROJ_1: 22;

          then

          consider a be Real such that

           A2: a <> 0 and

           A3: v = (a * u) by ANPROJ_1: 1;

          v = |[(a * 0 ), (a * (1 / 2)), (a * 1)]| by A3, EUCLID_5: 8

          .= |[ 0 , (a / 2), a]|;

          then

           A4: (v . 1) = 0 & (v . 2) = (a / 2) & (v . 3) = a by FINSEQ_1: 45;

          ( qfconic (1,1,( - 1), 0 , 0 , 0 ,v)) = (((((((1 * (v . 1)) * (v . 1)) + ((1 * (v . 2)) * (v . 2))) + ((( - 1) * (v . 3)) * (v . 3))) + (( 0 * (v . 1)) * (v . 2))) + (( 0 * (v . 1)) * (v . 3))) + (( 0 * (v . 2)) * (v . 3))) by PASCAL:def 1

          .= ((a ^2 ) * ( - (3 / 4))) by A4;

          hence ( qfconic (1,1,( - 1), 0 , 0 , 0 ,v)) is negative by A2;

        end;

        then Q in { P where P be Point of ( ProjectiveSpace ( TOP-REAL 3)) : for u be Element of ( TOP-REAL 3) st u is non zero & P = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) is negative };

        then

        reconsider Q as Element of BK_model by BKMODEL2:def 1;

        reconsider Q9 = Q as Element of real_projective_plane ;

        take Q;

        Q <> P

        proof

          assume

           A6: Q = P;

          

           A7: Q9 = ( Dir u) & (u . 3) = 1 by FINSEQ_1: 45;

          Q9 in ( absolute \/ BK_model ) by XBOOLE_0:def 3;

          then |[ 0 , 0 , 1]| = |[ 0 , (1 / 2), 1]| by A7, Def01, A6, A1;

          hence contradiction by FINSEQ_1: 78;

        end;

        hence thesis;

      end;

        suppose

         A8: ( # P) <> |[ 0 , 0 , 1]|;

        reconsider u = |[ 0 , 0 , 1]| as non zero Element of ( TOP-REAL 3);

        reconsider Q = ( Dir u) as Point of ( ProjectiveSpace ( TOP-REAL 3)) by ANPROJ_1: 26;

        now

          let v be Element of ( TOP-REAL 3);

          assume v is non zero & Q = ( Dir v);

          then are_Prop (u,v) by ANPROJ_1: 22;

          then

          consider a be Real such that

           A9: a <> 0 and

           A10: v = (a * u) by ANPROJ_1: 1;

          v = |[(a * 0 ), (a * 0 ), (a * 1)]| by A10, EUCLID_5: 8

          .= |[ 0 , 0 , a]|;

          then

           A11: (v . 1) = 0 & (v . 2) = 0 & (v . 3) = a by FINSEQ_1: 45;

          ( qfconic (1,1,( - 1), 0 , 0 , 0 ,v)) = (((((((1 * (v . 1)) * (v . 1)) + ((1 * (v . 2)) * (v . 2))) + ((( - 1) * (v . 3)) * (v . 3))) + (( 0 * (v . 1)) * (v . 2))) + (( 0 * (v . 1)) * (v . 3))) + (( 0 * (v . 2)) * (v . 3))) by PASCAL:def 1

          .= ((a ^2 ) * ( - 1)) by A11;

          hence ( qfconic (1,1,( - 1), 0 , 0 , 0 ,v)) is negative by A9;

        end;

        then Q in { P where P be Point of ( ProjectiveSpace ( TOP-REAL 3)) : for u be Element of ( TOP-REAL 3) st u is non zero & P = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) is negative };

        then

        reconsider Q as Element of BK_model by BKMODEL2:def 1;

        reconsider Q9 = Q as Element of real_projective_plane ;

        take Q;

        Q <> P

        proof

          assume

           A13: Q = P;

          

           A14: Q9 = ( Dir u) & (u . 3) = 1 by FINSEQ_1: 45;

          Q9 in ( absolute \/ BK_model ) by XBOOLE_0:def 3;

          hence contradiction by A14, A8, Def01, A13;

        end;

        hence thesis;

      end;

    end;

    reserve P for Element of BK_model ;

    theorem :: BKMODEL3:12

    ex P1,P2 be Element of absolute st P1 <> P2 & (P1,P,P2) are_collinear

    proof

      consider Q be Element of BK_model such that

       A1: P <> Q by Th11;

      consider P1,P2 be Element of absolute such that

       A2: P1 <> P2 and

       A3: (P,Q,P1) are_collinear and

       A4: (P,Q,P2) are_collinear by A1, BKMODEL2: 20;

      take P1, P2;

      (P,P1,P2) are_collinear by A1, A3, A4, COLLSP: 6;

      hence thesis by A2, COLLSP: 4;

    end;

    theorem :: BKMODEL3:13

    for Q be Element of absolute holds ex R be Element of BK_model st P <> R & (P,Q,R) are_collinear

    proof

      let Q be Element of absolute ;

      reconsider P1 = P, Q1 = Q as Element of real_projective_plane ;

      consider R1 be Element of real_projective_plane such that

       A1: R1 in BK_model and

       A2: P1 <> R1 and

       A3: (R1,P1,Q1) are_collinear by BKMODEL2: 22;

      reconsider R = R1 as Element of BK_model by A1;

      take R;

      thus thesis by A3, A2, HESSENBE: 1;

    end;

    theorem :: BKMODEL3:14

    

     Th12: for L be LINE of ( IncProjSp_of real_projective_plane ) st P in L holds ex P1,P2 be Element of absolute st P1 <> P2 & P1 in L & P2 in L

    proof

      let L be LINE of ( IncProjSp_of real_projective_plane );

      assume

       A1: P in L;

      consider Q be Element of ( ProjectiveSpace ( TOP-REAL 3)) such that

       A2: P <> Q and

       A3: Q in L by BKMODEL2: 8;

      consider R be Element of absolute such that

       A4: (P,Q,R) are_collinear by A2, BKMODEL2: 19;

      reconsider p = P, r = R as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

      reconsider L9 = L as LINE of real_projective_plane by INCPROJ: 4;

      ( Line (P,Q)) = L9 by A1, A2, A3, COLLSP: 19;

      then P in L9 & Q in L9 & R in L9 by A1, A3, A4, COLLSP: 11;

      then p on L & r on L by INCPROJ: 5;

      then

      consider p1,p2 be POINT of ( IncProjSp_of real_projective_plane ), P1,P2 be Element of real_projective_plane such that

       A5: p1 = P1 and

       A6: p2 = P2 and

       A7: P1 <> P2 and

       A8: P1 in absolute and

       A9: P2 in absolute and

       A10: p1 on L and

       A11: p2 on L by BKMODEL2: 23;

      reconsider P1, P2 as Element of absolute by A8, A9;

      take P1, P2;

      P1 in L9 & P2 in L9 by A5, A6, A10, A11, INCPROJ: 5;

      hence thesis by A7;

    end;

    definition

      let N be invertible Matrix of 3, F_Real ;

      :: BKMODEL3:def2

      func line_homography (N) -> Function of the Lines of ( IncProjSp_of real_projective_plane ), the Lines of ( IncProjSp_of real_projective_plane ) means

      : Def02: for x be LINE of ( IncProjSp_of real_projective_plane ) holds (it . x) = { (( homography N) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on x };

      existence

      proof

        defpred P[ object, object] means ex x be LINE of ( IncProjSp_of real_projective_plane ) st $1 = x & $2 = { (( homography N) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on x };

        

         A1: for x be object st x in the Lines of ( IncProjSp_of real_projective_plane ) holds ex y be object st y in the Lines of ( IncProjSp_of real_projective_plane ) & P[x, y]

        proof

          let x be object;

          assume x in the Lines of ( IncProjSp_of real_projective_plane );

          then

          reconsider x9 = x as Element of the Lines of ( IncProjSp_of real_projective_plane );

          set y = { (( homography N) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on x9 };

          consider p,q be Point of real_projective_plane such that

           A2: p <> q and

           A3: x9 = ( Line (p,q)) by COLLSP:def 7, INCPROJ: 4;

          reconsider p9 = (( homography N) . p), q9 = (( homography N) . q) as Point of real_projective_plane by FUNCT_2: 5;

          

           A4: y = ( Line (p9,q9))

          proof

            

             A5: y c= ( Line (p9,q9))

            proof

              let x be object;

              assume x in y;

              then

              consider Px be POINT of ( IncProjSp_of real_projective_plane ) such that

               A6: x = (( homography N) . Px) and

               A7: Px on x9;

              reconsider Px as Point of real_projective_plane by INCPROJ: 3;

              x9 is LINE of real_projective_plane by INCPROJ: 4;

              then

               A8: Px in x9 by A7, INCPROJ: 5;

              reconsider p1 = p, q1 = q, r1 = Px, p2 = p9, q2 = q9 as Point of ( ProjectiveSpace ( TOP-REAL 3));

              ((( homography N) . p1),(( homography N) . q1),(( homography N) . r1)) are_collinear by A8, A3, COLLSP: 11, ANPROJ_8: 102;

              hence thesis by A6, COLLSP: 11;

            end;

            ( Line (p9,q9)) c= y

            proof

              let x be object;

              assume x in ( Line (p9,q9));

              then x in { p where p be Element of real_projective_plane : (p9,q9,p) are_collinear } by COLLSP:def 5;

              then

              consider x99 be Element of real_projective_plane such that

               A9: x = x99 and

               A10: (p9,q9,x99) are_collinear ;

              reconsider p1 = p, q1 = q, r1 = x99, p2 = p9, q2 = q9 as Point of ( ProjectiveSpace ( TOP-REAL 3));

              reconsider r2 = (( homography (N ~ )) . r1) as Point of ( ProjectiveSpace ( TOP-REAL 3));

              reconsider r3 = r2 as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

              

               A11: r1 = (( homography N) . r2) by ANPROJ_9: 15;

              

               A12: x9 is LINE of real_projective_plane by INCPROJ: 4;

              r2 in x9 by A3, A10, A11, ANPROJ_8: 102, COLLSP: 11;

              then r3 on x9 by A12, INCPROJ: 5;

              hence thesis by A11, A9;

            end;

            hence thesis by A5;

          end;

          reconsider y9 = ( Line (p9,q9)) as LINE of real_projective_plane by A2, ANPROJ_9: 16, COLLSP:def 7;

          reconsider y = y9 as LINE of ( IncProjSp_of real_projective_plane ) by INCPROJ: 4;

          y is Element of the Lines of ( IncProjSp_of real_projective_plane );

          then

          reconsider y = { (( homography N) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on x9 } as Element of the Lines of ( IncProjSp_of real_projective_plane ) by A4;

          take y;

          thus thesis;

        end;

        consider f be Function of the Lines of ( IncProjSp_of real_projective_plane ), the Lines of ( IncProjSp_of real_projective_plane ) such that

         A13: for x be object st x in the Lines of ( IncProjSp_of real_projective_plane ) holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

        for x be LINE of ( IncProjSp_of real_projective_plane ) holds (f . x) = { (( homography N) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on x }

        proof

          let x be LINE of ( IncProjSp_of real_projective_plane );

           P[x, (f . x)] by A13;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let h1,h2 be Function of the Lines of ( IncProjSp_of real_projective_plane ), the Lines of ( IncProjSp_of real_projective_plane ) such that

         A14: for x be LINE of ( IncProjSp_of real_projective_plane ) holds (h1 . x) = { (( homography N) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on x } and

         A15: for x be LINE of ( IncProjSp_of real_projective_plane ) holds (h2 . x) = { (( homography N) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on x };

        now

          ( dom h1) = the Lines of ( IncProjSp_of real_projective_plane ) by FUNCT_2:def 1;

          hence ( dom h1) = ( dom h2) by FUNCT_2:def 1;

          hereby

            let x9 be object;

            assume x9 in ( dom h1);

            then

            reconsider y = x9 as LINE of ( IncProjSp_of real_projective_plane );

            (h1 . y) = { (( homography N) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on y } by A14

            .= (h2 . y) by A15;

            hence (h1 . x9) = (h2 . x9);

          end;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

    end

    reserve N,N1,N2 for invertible Matrix of 3, F_Real ;

    reserve l,l1,l2 for Element of the Lines of ( IncProjSp_of real_projective_plane );

    theorem :: BKMODEL3:15

    

     Th13: (( line_homography N1) . (( line_homography N2) . l)) = (( line_homography (N1 * N2)) . l)

    proof

      reconsider l2 = (( line_homography N2) . l) as LINE of ( IncProjSp_of real_projective_plane );

      

       A1: l2 = { (( homography N2) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l } by Def02;

      

       A2: (( line_homography N1) . (( line_homography N2) . l)) = { (( homography N1) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l2 } by Def02;

      set X = { (( homography N1) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l2 }, Y = { (( homography (N1 * N2)) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l };

      { (( homography N1) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l2 } = { (( homography (N1 * N2)) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l }

      proof

        

         A3: X c= Y

        proof

          let x be object;

          assume x in X;

          then

          consider P be POINT of ( IncProjSp_of real_projective_plane ) such that

           A4: x = (( homography N1) . P) and

           A5: P on l2;

          

           A6: P is Point of real_projective_plane by INCPROJ: 3;

          l2 is LINE of real_projective_plane by INCPROJ: 4;

          then P in { (( homography N2) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l } by A6, A1, A5, INCPROJ: 5;

          then

          consider P2 be POINT of ( IncProjSp_of real_projective_plane ) such that

           A7: P = (( homography N2) . P2) and

           A8: P2 on l;

          P2 is Point of real_projective_plane by INCPROJ: 3;

          then x = (( homography (N1 * N2)) . P2) by A4, A7, ANPROJ_9: 13;

          hence thesis by A8;

        end;

        Y c= X

        proof

          let x be object;

          assume x in Y;

          then

          consider P be POINT of ( IncProjSp_of real_projective_plane ) such that

           A9: x = (( homography (N1 * N2)) . P) and

           A10: P on l;

          

           A11: P is Point of real_projective_plane by INCPROJ: 3;

          P is Element of ( ProjectiveSpace ( TOP-REAL 3)) by INCPROJ: 3;

          then (( homography N2) . P) is Point of real_projective_plane by FUNCT_2: 5;

          then

          reconsider P2 = (( homography N2) . P) as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

          now

            thus x = (( homography N1) . P2) by A11, A9, ANPROJ_9: 13;

            

             A12: P2 in l2 by A10, A1;

            l2 is LINE of real_projective_plane by INCPROJ: 4;

            hence P2 on l2 by A12, INCPROJ: 5;

          end;

          hence thesis;

        end;

        hence thesis by A3;

      end;

      hence thesis by A2, Def02;

    end;

    theorem :: BKMODEL3:16

    

     Th14: (( line_homography ( 1. ( F_Real ,3))) . l) = l

    proof

      set X = { (( homography ( 1. ( F_Real ,3))) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l };

      

       A1: X c= l

      proof

        let x be object;

        assume x in X;

        then

        consider P be POINT of ( IncProjSp_of real_projective_plane ) such that

         A2: x = (( homography ( 1. ( F_Real ,3))) . P) and

         A3: P on l;

        

         A4: P is Point of real_projective_plane by INCPROJ: 2;

        then

         A5: x = P by A2, ANPROJ_9: 14;

        l is LINE of real_projective_plane by INCPROJ: 4;

        hence thesis by A4, A3, A5, INCPROJ: 5;

      end;

      l c= X

      proof

        let x be object;

        assume

         A6: x in l;

        

         A7: l is LINE of real_projective_plane by INCPROJ: 4;

        l is Subset of real_projective_plane by INCPROJ: 4;

        then

        reconsider x9 = x as Point of real_projective_plane by A6;

        reconsider l9 = l as LINE of ( IncProjSp_of real_projective_plane );

        reconsider x99 = x9 as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

        

         A8: x99 on l by A7, A6, INCPROJ: 5;

        (( homography ( 1. ( F_Real ,3))) . x99) = x99 by ANPROJ_9: 14;

        hence thesis by A8;

      end;

      hence thesis by A1, Def02;

    end;

    theorem :: BKMODEL3:17

    

     Th15: (( line_homography N) . (( line_homography (N ~ )) . l)) = l & (( line_homography (N ~ )) . (( line_homography N) . l)) = l

    proof

      

       A1: (N ~ ) is_reverse_of N by MATRIX_6:def 4;

      

      thus (( line_homography N) . (( line_homography (N ~ )) . l)) = (( line_homography (N * (N ~ ))) . l) by Th13

      .= (( line_homography ( 1. ( F_Real ,3))) . l) by A1, MATRIX_6:def 2

      .= l by Th14;

      

      thus (( line_homography (N ~ )) . (( line_homography N) . l)) = (( line_homography ((N ~ ) * N)) . l) by Th13

      .= (( line_homography ( 1. ( F_Real ,3))) . l) by A1, MATRIX_6:def 2

      .= l by Th14;

    end;

    theorem :: BKMODEL3:18

    (( line_homography N) . l1) = (( line_homography N) . l2) implies l1 = l2

    proof

      assume (( line_homography N) . l1) = (( line_homography N) . l2);

      

      then l1 = (( line_homography (N ~ )) . (( line_homography N) . l2)) by Th15

      .= l2 by Th15;

      hence thesis;

    end;

    definition

      :: BKMODEL3:def3

      func EnsLineHomography3 -> set equals the set of all ( line_homography N) where N be invertible Matrix of 3, F_Real ;

      coherence ;

    end

    registration

      cluster EnsLineHomography3 -> non empty;

      coherence

      proof

        ( line_homography ( 1. ( F_Real ,3))) in EnsLineHomography3 ;

        hence thesis;

      end;

    end

    definition

      let h1,h2 be Element of EnsLineHomography3 ;

      :: BKMODEL3:def4

      func h1 (*) h2 -> Element of EnsLineHomography3 means

      : Def03: ex N1,N2 be invertible Matrix of 3, F_Real st h1 = ( line_homography N1) & h2 = ( line_homography N2) & it = ( line_homography (N1 * N2));

      existence

      proof

        h1 in the set of all ( line_homography N) where N be invertible Matrix of 3, F_Real ;

        then

        consider N1 be invertible Matrix of 3, F_Real such that

         A1: h1 = ( line_homography N1);

        h2 in the set of all ( line_homography N) where N be invertible Matrix of 3, F_Real ;

        then

        consider N2 be invertible Matrix of 3, F_Real such that

         A2: h2 = ( line_homography N2);

        ( line_homography (N1 * N2)) in EnsLineHomography3 ;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let H1,H2 be Element of EnsLineHomography3 such that

         A3: ex N1,N2 be invertible Matrix of 3, F_Real st h1 = ( line_homography N1) & h2 = ( line_homography N2) & H1 = ( line_homography (N1 * N2)) and

         A4: ex N1,N2 be invertible Matrix of 3, F_Real st h1 = ( line_homography N1) & h2 = ( line_homography N2) & H2 = ( line_homography (N1 * N2));

        consider NA1,NA2 be invertible Matrix of 3, F_Real such that

         A5: h1 = ( line_homography NA1) and

         A6: h2 = ( line_homography NA2) and

         A7: H1 = ( line_homography (NA1 * NA2)) by A3;

        consider NB1,NB2 be invertible Matrix of 3, F_Real such that

         A8: h1 = ( line_homography NB1) and

         A9: h2 = ( line_homography NB2) and

         A10: H2 = ( line_homography (NB1 * NB2)) by A4;

        reconsider fH1 = H1, fH2 = H2 as Function of the Lines of ( IncProjSp_of real_projective_plane ), the Lines of ( IncProjSp_of real_projective_plane ) by A7, A10;

        now

          ( dom fH1) = the Lines of ( IncProjSp_of real_projective_plane ) by FUNCT_2:def 1;

          hence ( dom fH1) = ( dom fH2) by FUNCT_2:def 1;

          thus for x be object st x in ( dom fH1) holds (fH1 . x) = (fH2 . x)

          proof

            let x be object;

            assume x in ( dom fH1);

            then

            reconsider P = x as Element of the Lines of ( IncProjSp_of real_projective_plane );

            (fH1 . x) = (( line_homography NB1) . (( line_homography NB2) . P)) by A5, A6, A7, A8, A9, Th13

            .= (fH2 . x) by A10, Th13;

            hence thesis;

          end;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

    end

    theorem :: BKMODEL3:19

    

     Th16: for h1,h2 be Element of EnsLineHomography3 st h1 = ( line_homography N1) & h2 = ( line_homography N2) holds ( line_homography (N1 * N2)) = (h1 (*) h2)

    proof

      let h1,h2 be Element of EnsLineHomography3 ;

      assume that

       A1: h1 = ( line_homography N1) and

       A2: h2 = ( line_homography N2);

      consider M1,M2 be invertible Matrix of 3, F_Real such that

       A3: h1 = ( line_homography M1) and

       A4: h2 = ( line_homography M2) and

       A5: (h1 (*) h2) = ( line_homography (M1 * M2)) by Def03;

      reconsider h12 = (h1 (*) h2) as Function of the Lines of ( IncProjSp_of real_projective_plane ), the Lines of ( IncProjSp_of real_projective_plane ) by A5;

      now

        ( dom ( line_homography (N1 * N2))) = the Lines of ( IncProjSp_of real_projective_plane ) by FUNCT_2:def 1;

        hence ( dom ( line_homography (N1 * N2))) = ( dom h12) by FUNCT_2:def 1;

        thus for x be object st x in ( dom ( line_homography (N1 * N2))) holds (( line_homography (N1 * N2)) . x) = (h12 . x)

        proof

          let x be object;

          assume x in ( dom ( line_homography (N1 * N2)));

          then

          reconsider xf = x as Element of the Lines of ( IncProjSp_of real_projective_plane );

          (( line_homography (N1 * N2)) . xf) = (( line_homography N1) . (( line_homography N2) . xf)) by Th13

          .= (h12 . xf) by A3, A4, A5, A1, A2, Th13;

          hence thesis;

        end;

      end;

      hence thesis by FUNCT_1:def 11;

    end;

    theorem :: BKMODEL3:20

    

     Th17: for x,y,z be Element of EnsLineHomography3 holds ((x (*) y) (*) z) = (x (*) (y (*) z))

    proof

      let x,y,z be Element of EnsLineHomography3 ;

      x in EnsLineHomography3 ;

      then

      consider Nx be invertible Matrix of 3, F_Real such that

       A2: x = ( line_homography Nx);

      y in EnsLineHomography3 ;

      then

      consider Ny be invertible Matrix of 3, F_Real such that

       A3: y = ( line_homography Ny);

      z in EnsLineHomography3 ;

      then

      consider Nz be invertible Matrix of 3, F_Real such that

       A4: z = ( line_homography Nz);

      

       A5: ( width Nx) = 3 & ( len Ny) = 3 & ( width Ny) = 3 & ( len Nz) = 3 by MATRIX_0: 24;

      (y (*) z) = ( line_homography (Ny * Nz)) by A3, A4, Th16;

      

      then

       A6: (x (*) (y (*) z)) = ( line_homography (Nx * (Ny * Nz))) by A2, Th16

      .= ( line_homography ((Nx * Ny) * Nz)) by A5, MATRIX_3: 33;

      (x (*) y) = ( line_homography (Nx * Ny)) by A2, A3, Th16;

      hence thesis by A6, A4, Th16;

    end;

    definition

      :: BKMODEL3:def5

      func BinOpLineHomography3 -> BinOp of EnsLineHomography3 means

      : Def04: for h1,h2 be Element of EnsLineHomography3 holds (it . (h1,h2)) = (h1 (*) h2);

      existence from BINOP_1:sch 4;

      uniqueness from BINOP_2:sch 2;

    end

    definition

      :: BKMODEL3:def6

      func GroupLineHomography3 -> strict multMagma equals multMagma (# EnsLineHomography3 , BinOpLineHomography3 #);

      coherence ;

    end

    set GLH3 = GroupLineHomography3 ;

     Lm1:

    now

      let e be Element of GLH3 such that

       A1: e = ( line_homography ( 1. ( F_Real ,3)));

      let h be Element of GLH3;

      reconsider h1 = h, h2 = e as Element of EnsLineHomography3 ;

      consider N1,N2 be invertible Matrix of 3, F_Real such that

       A2: h1 = ( line_homography N1) and

       A3: h2 = ( line_homography N2) and

       A4: (h1 (*) h2) = ( line_homography (N1 * N2)) by Def03;

      ( line_homography (N1 * N2)) = ( line_homography N1)

      proof

        ( dom ( line_homography (N1 * N2))) = the Lines of ( IncProjSp_of real_projective_plane ) by FUNCT_2:def 1;

        then

         A5: ( dom ( line_homography (N1 * N2))) = ( dom ( line_homography N1)) by FUNCT_2:def 1;

        for x be object st x in ( dom ( line_homography N1)) holds (( line_homography (N1 * N2)) . x) = (( line_homography N1) . x)

        proof

          let x be object;

          assume x in ( dom ( line_homography N1));

          then

          reconsider xf = x as Element of the Lines of ( IncProjSp_of real_projective_plane );

          (( line_homography (N1 * N2)) . xf) = (( line_homography N1) . (( line_homography N2) . xf)) by Th13

          .= (( line_homography N1) . xf) by A1, A3, Th14;

          hence thesis;

        end;

        hence thesis by A5, FUNCT_1:def 11;

      end;

      hence (h * e) = h by Def04, A2, A4;

      consider N2,N1 be invertible Matrix of 3, F_Real such that

       A6: h2 = ( line_homography N2) and

       A7: h1 = ( line_homography N1) and

       A8: (h2 (*) h1) = ( line_homography (N2 * N1)) by Def03;

      ( line_homography (N2 * N1)) = ( line_homography N1)

      proof

        ( dom ( line_homography (N2 * N1))) = the Lines of ( IncProjSp_of real_projective_plane ) by FUNCT_2:def 1;

        then

         A9: ( dom ( line_homography (N2 * N1))) = ( dom ( line_homography N1)) by FUNCT_2:def 1;

        for x be object st x in ( dom ( line_homography N1)) holds (( line_homography (N2 * N1)) . x) = (( line_homography N1) . x)

        proof

          let x be object;

          assume x in ( dom ( line_homography N1));

          then

          reconsider xf = x as Element of the Lines of ( IncProjSp_of real_projective_plane );

          (( line_homography (N2 * N1)) . xf) = (( line_homography N2) . (( line_homography N1) . xf)) by Th13

          .= (( line_homography N1) . xf) by A1, A6, Th14;

          hence thesis;

        end;

        hence thesis by A9, FUNCT_1:def 11;

      end;

      hence (e * h) = h by Def04, A7, A8;

    end;

     Lm2:

    now

      let e,h,g be Element of GLH3;

      let N,Ng be invertible Matrix of 3, F_Real such that

       A1: h = ( line_homography N) and

       A2: g = ( line_homography Ng) and

       A3: Ng = (N ~ ) and

       A4: e = ( line_homography ( 1. ( F_Real ,3)));

      reconsider h1 = h as Element of EnsLineHomography3 ;

      

       A5: Ng is_reverse_of N by A3, MATRIX_6:def 4;

      reconsider g1 = g as Element of EnsLineHomography3 ;

      consider N1,N2 be invertible Matrix of 3, F_Real such that

       A6: h1 = ( line_homography N1) and

       A7: g1 = ( line_homography N2) and

       A8: (h1 (*) g1) = ( line_homography (N1 * N2)) by Def03;

      ( line_homography (N1 * N2)) = ( line_homography (N * Ng))

      proof

        now

          ( dom ( line_homography (N1 * N2))) = the Lines of ( IncProjSp_of real_projective_plane ) by FUNCT_2:def 1;

          hence ( dom ( line_homography (N1 * N2))) = ( dom ( line_homography (N * Ng))) by FUNCT_2:def 1;

          thus for x be object st x in ( dom ( line_homography (N1 * N2))) holds (( line_homography (N1 * N2)) . x) = (( line_homography (N * Ng)) . x)

          proof

            let x be object;

            assume x in ( dom ( line_homography (N1 * N2)));

            then

            reconsider xf = x as Element of the Lines of ( IncProjSp_of real_projective_plane );

            (( line_homography (N1 * N2)) . xf) = (( line_homography N) . (( line_homography Ng) . xf)) by Th13, A6, A1, A7, A2

            .= (( line_homography (N * Ng)) . xf) by Th13;

            hence thesis;

          end;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

      then (h1 (*) g1) = e by A4, A8, A5, MATRIX_6:def 2;

      hence (h * g) = e by Def04;

      consider N1,N2 be invertible Matrix of 3, F_Real such that

       A9: g1 = ( line_homography N1) and

       A10: h1 = ( line_homography N2) and

       A11: (g1 (*) h1) = ( line_homography (N1 * N2)) by Def03;

      ( line_homography (N1 * N2)) = ( line_homography (Ng * N))

      proof

        now

          ( dom ( line_homography (N1 * N2))) = the Lines of ( IncProjSp_of real_projective_plane ) by FUNCT_2:def 1;

          hence ( dom ( line_homography (N1 * N2))) = ( dom ( line_homography (Ng * N))) by FUNCT_2:def 1;

          thus for x be object st x in ( dom ( line_homography (N1 * N2))) holds (( line_homography (N1 * N2)) . x) = (( line_homography (Ng * N)) . x)

          proof

            let x be object;

            assume x in ( dom ( line_homography (N1 * N2)));

            then

            reconsider xf = x as Element of the Lines of ( IncProjSp_of real_projective_plane );

            (( line_homography (N1 * N2)) . xf) = (( line_homography Ng) . (( line_homography N) . xf)) by Th13, A9, A1, A10, A2

            .= (( line_homography (Ng * N)) . xf) by Th13;

            hence thesis;

          end;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

      then (g1 (*) h1) = e by A11, A5, A4, MATRIX_6:def 2;

      hence (g * h) = e by Def04;

    end;

    set e = ( line_homography ( 1. ( F_Real ,3)));

    e in EnsLineHomography3 ;

    then

    reconsider e as Element of GLH3;

    registration

      cluster GroupLineHomography3 -> non empty associative Group-like;

      coherence

      proof

        thus GLH3 is non empty;

        thus GLH3 is associative

        proof

          let x,y,z be Element of GLH3;

          reconsider xf = x, yf = y, zf = z as Element of EnsLineHomography3 ;

          

           A7: (x * y) = (xf (*) yf) by Def04;

          

           A8: ((x * y) * z) = ((xf (*) yf) (*) zf) by Def04, A7;

          (y * z) = (yf (*) zf) by Def04;

          then (x * (y * z)) = (xf (*) (yf (*) zf)) by Def04;

          hence thesis by A8, Th17;

        end;

        take e;

        let h be Element of GLH3;

        thus (h * e) = h & (e * h) = h by Lm1;

        h in EnsLineHomography3 ;

        then

        consider N be invertible Matrix of 3, F_Real such that

         A9: h = ( line_homography N);

        reconsider Ng = (N ~ ) as invertible Matrix of 3, F_Real ;

        ( line_homography Ng) in EnsLineHomography3 ;

        then

        reconsider g = ( line_homography Ng) as Element of GLH3;

        take g;

        thus thesis by A9, Lm2;

      end;

    end

    theorem :: BKMODEL3:21

    

     Th18: ( 1_ GroupLineHomography3 ) = ( line_homography ( 1. ( F_Real ,3)))

    proof

      for h be Element of GLH3 holds (h * e) = h & (e * h) = h by Lm1;

      hence thesis by GROUP_1: 4;

    end;

    theorem :: BKMODEL3:22

    for h,g be Element of GroupLineHomography3 holds for N,Ng be invertible Matrix of 3, F_Real st h = ( line_homography N) & g = ( line_homography Ng) & Ng = (N ~ ) holds g = (h " )

    proof

      let h,g be Element of GLH3;

      let N,Ng be invertible Matrix of 3, F_Real ;

      assume h = ( line_homography N) & g = ( line_homography Ng) & Ng = (N ~ );

      then (h * g) = ( 1_ GLH3) & (g * h) = ( 1_ GLH3) by Lm2, Th18;

      hence g = (h " ) by GROUP_1:def 5;

    end;

    reserve P for Point of ( ProjectiveSpace ( TOP-REAL 3)),

l for LINE of ( IncProjSp_of real_projective_plane );

    theorem :: BKMODEL3:23

    

     Th19: (( homography N) . P) in l implies P in (( line_homography (N ~ )) . l)

    proof

      assume

       A1: (( homography N) . P) in l;

      reconsider P9 = (( homography N) . P) as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

      l is LINE of real_projective_plane by INCPROJ: 4;

      then

       A2: P9 on l by A1, INCPROJ: 5;

      (( line_homography (N ~ )) . l) = { (( homography (N ~ )) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l } by Def02;

      then (( homography (N ~ )) . P9) in (( line_homography (N ~ )) . l) by A2;

      hence thesis by ANPROJ_9: 15;

    end;

    theorem :: BKMODEL3:24

    P in (( line_homography N) . l) implies (( homography (N ~ )) . P) in l

    proof

      assume P in (( line_homography N) . l);

      then P in { (( homography N) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l } by Def02;

      then

      consider P9 be POINT of ( IncProjSp_of real_projective_plane ) such that

       A1: P = (( homography N) . P9) and

       A2: P9 on l;

      P9 is Element of real_projective_plane by INCPROJ: 3;

      then

       A3: (( homography (N ~ )) . P) = P9 by A1, ANPROJ_9: 15;

      l is LINE of real_projective_plane by INCPROJ: 4;

      hence thesis by A2, A3, INCPROJ: 5;

    end;

    theorem :: BKMODEL3:25

    

     Th20: P in l iff (( homography N) . P) in (( line_homography N) . l)

    proof

      hereby

        assume

         A1: P in l;

        reconsider P9 = P as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

        l is LINE of real_projective_plane by INCPROJ: 4;

        then

         A2: P9 on l by A1, INCPROJ: 5;

        (( line_homography N) . l) = { (( homography N) . P) where P be POINT of ( IncProjSp_of real_projective_plane ) : P on l } by Def02;

        hence (( homography N) . P) in (( line_homography N) . l) by A2;

      end;

      assume (( homography N) . P) in (( line_homography N) . l);

      then P in (( line_homography (N ~ )) . (( line_homography N) . l)) by Th19;

      hence P in l by Th15;

    end;

    theorem :: BKMODEL3:26

    

     Th21: for u,v,w be non zero Element of ( TOP-REAL 3) st (u `3 ) = 1 & (v `1 ) = ( - (u `2 )) & (v `2 ) = (u `1 ) & (v `3 ) = 0 & (w `3 ) = 1 & |{u, v, w}| = 0 holds (((((u `1 ) ^2 ) + ((u `2 ) ^2 )) - ((u `1 ) * (w `1 ))) - ((u `2 ) * (w `2 ))) = 0

    proof

      let u,v,w be non zero Element of ( TOP-REAL 3);

      assume that

       A1: (u `3 ) = 1 and

       A2: (v `1 ) = ( - (u `2 )) and

       A3: (v `2 ) = (u `1 ) and

       A4: (v `3 ) = 0 and

       A5: (w `3 ) = 1 and

       A6: |{u, v, w}| = 0 ;

      set p = u, q = v, r = w;

       0 = ((((((((p `1 ) * (q `2 )) * (r `3 )) - ((1 * (q `2 )) * (r `1 ))) - (((p `1 ) * (q `3 )) * (r `2 ))) + (((p `2 ) * (q `3 )) * (r `1 ))) - (((p `2 ) * (q `1 )) * (r `3 ))) + ((1 * (q `1 )) * (r `2 ))) by A1, A6, ANPROJ_8: 27

      .= (((((p `1 ) ^2 ) + ((p `2 ) ^2 )) - ((p `1 ) * (r `1 ))) - ((p `2 ) * (r `2 ))) by A2, A3, A4, A5;

      hence thesis;

    end;

    theorem :: BKMODEL3:27

    

     Th22: for a be non zero Real holds for b,c be Real holds (a * |[(b / a), (c / a), 1]|) = |[b, c, a]|

    proof

      let a be non zero Real;

      let b,c be Real;

      (a * |[(b / a), (c / a), 1]|) = |[(a * (b / a)), (a * (c / a)), (a * 1)]| by EUCLID_5: 8

      .= |[b, (a * (c / a)), a]| by XCMPLX_1: 87

      .= |[b, c, a]| by XCMPLX_1: 87;

      hence thesis;

    end;

    theorem :: BKMODEL3:28

    

     Th23: for u,v,w be non zero Element of ( TOP-REAL 3) st (u `1 ) <> 0 & (u `3 ) = 1 & (v `1 ) = ( - (u `2 )) & (v `2 ) = (u `1 ) & (v `3 ) = 0 & (w `3 ) = 1 & |{u, v, w}| = 0 & 1 < (((u `1 ) ^2 ) + ((u `2 ) ^2 )) holds (((w `1 ) ^2 ) + ((w `2 ) ^2 )) <> 1

    proof

      let u,v,w be non zero Element of ( TOP-REAL 3);

      assume that

       A0: (u `1 ) <> 0 and

       A1: (u `3 ) = 1 and

       A2: (v `1 ) = ( - (u `2 )) and

       A3: (v `2 ) = (u `1 ) and

       A4: (v `3 ) = 0 and

       A5: (w `3 ) = 1 and

       A6: |{u, v, w}| = 0 and

       A7: 1 < (((u `1 ) ^2 ) + ((u `2 ) ^2 ));

      

       A8: (((((u `1 ) ^2 ) + ((u `2 ) ^2 )) - ((u `1 ) * (w `1 ))) - ((u `2 ) * (w `2 ))) = 0 by A1, A2, A3, A4, A5, A6, Th21;

      assume

       A9: (((w `1 ) ^2 ) + ((w `2 ) ^2 )) = 1;

      reconsider x = (w `1 ), y = (w `2 ) as Real;

      reconsider u1 = (u `1 ) as non zero Real by A0;

      reconsider r = ( sqrt (((u `1 ) ^2 ) + ((u `2 ) ^2 ))) as positive Real by A0, Th02;

      reconsider u2 = (u `2 ) as Real;

      

       A10: (r ^2 ) = (((u `1 ) ^2 ) + ((u `2 ) ^2 )) by SQUARE_1:def 2;

      then (u1 * x) = ((r ^2 ) - (u2 * y)) by A8;

      then ((((((r ^2 ) ^2 ) / (u1 ^2 )) - ((2 * (((r ^2 ) * u2) / (u1 * u1))) * y)) + (((u2 ^2 ) / (u1 ^2 )) * (y ^2 ))) + (y ^2 )) = 1 by A9, Th03;

      hence contradiction by A10, A7, Th09;

    end;

    theorem :: BKMODEL3:29

    

     Th24: for u,v,w be non zero Element of ( TOP-REAL 3) st (u `2 ) <> 0 & (u `3 ) = 1 & (v `1 ) = ( - (u `2 )) & (v `2 ) = (u `1 ) & (v `3 ) = 0 & (w `3 ) = 1 & |{u, v, w}| = 0 & 1 < (((u `1 ) ^2 ) + ((u `2 ) ^2 )) holds (((w `1 ) ^2 ) + ((w `2 ) ^2 )) <> 1

    proof

      let u,v,w be non zero Element of ( TOP-REAL 3);

      assume that

       A0: (u `2 ) <> 0 and

       A1: (u `3 ) = 1 and

       A2: (v `1 ) = ( - (u `2 )) and

       A3: (v `2 ) = (u `1 ) and

       A4: (v `3 ) = 0 and

       A5: (w `3 ) = 1 and

       A6: |{u, v, w}| = 0 and

       A7: 1 < (((u `1 ) ^2 ) + ((u `2 ) ^2 ));

      

       A8: (((((u `1 ) ^2 ) + ((u `2 ) ^2 )) - ((u `1 ) * (w `1 ))) - ((u `2 ) * (w `2 ))) = 0 by A1, A2, A3, A4, A5, A6, Th21;

      assume

       A9: (((w `1 ) ^2 ) + ((w `2 ) ^2 )) = 1;

      reconsider x = (w `1 ), y = (w `2 ) as Real;

      reconsider u2 = (u `2 ) as non zero Real by A0;

      reconsider r = ( sqrt (((u `1 ) ^2 ) + ((u `2 ) ^2 ))) as positive Real by A0, Th02;

      reconsider u1 = (u `1 ) as Real;

      

       A10: (r ^2 ) = (((u `1 ) ^2 ) + ((u `2 ) ^2 )) by SQUARE_1:def 2;

      (u2 * y) = ((r ^2 ) - (u1 * x)) by A8, SQUARE_1:def 2;

      then ((((((r ^2 ) ^2 ) / (u2 ^2 )) - ((2 * (((r ^2 ) * u1) / (u2 * u2))) * x)) + (((u1 ^2 ) / (u2 ^2 )) * (x ^2 ))) + (x ^2 )) = 1 by A9, Th03;

      hence contradiction by A10, A7, Th09;

    end;

    theorem :: BKMODEL3:30

    

     Th25: for P be Element of absolute holds ex u be non zero Element of ( TOP-REAL 3) st (u . 3) = 1 & P = ( Dir u)

    proof

      let P be Element of absolute ;

      consider u be Element of ( TOP-REAL 3) such that

       A1: not u is zero and

       A2: P = ( Dir u) by ANPROJ_1: 26;

      (u . 3) <> 0 by A1, A2, BKMODEL1: 83;

      then

       A3: (u `3 ) <> 0 by EUCLID_5:def 3;

      reconsider v = |[((u `1 ) / (u `3 )), ((u `2 ) / (u `3 )), 1]| as non zero Element of ( TOP-REAL 3);

      take v;

      

      thus (v . 3) = (v `3 ) by EUCLID_5:def 3

      .= 1 by EUCLID_5: 2;

      ((u `3 ) * v) = |[((u `3 ) * ((u `1 ) / (u `3 ))), ((u `3 ) * ((u `2 ) / (u `3 ))), ((u `3 ) * 1)]| by EUCLID_5: 8

      .= |[(u `1 ), ((u `3 ) * ((u `2 ) / (u `3 ))), ((u `3 ) * 1)]| by A3, XCMPLX_1: 87

      .= |[(u `1 ), (u `2 ), ((u `3 ) * 1)]| by A3, XCMPLX_1: 87

      .= u by EUCLID_5: 3;

      then are_Prop (u,v) by A3, ANPROJ_1: 1;

      hence P = ( Dir v) by A1, A2, ANPROJ_1: 22;

    end;

    theorem :: BKMODEL3:31

    

     Th26: for a,b,c,d be Real holds for u,v be non zero Element of ( TOP-REAL 3) st u = |[a, b, 1]| & v = |[c, d, 0 ]| holds ( Dir u) <> ( Dir v)

    proof

      let a,b,c,d be Real;

      let u,v be non zero Element of ( TOP-REAL 3);

      assume that

       A1: u = |[a, b, 1]| and

       A2: v = |[c, d, 0 ]|;

      assume ( Dir u) = ( Dir v);

      then are_Prop (u,v) by ANPROJ_1: 22;

      then

      consider x be Real such that x <> 0 and

       A3: u = (x * v) by ANPROJ_1: 1;

      1 = ((x * v) `3 ) by A3, A1, EUCLID_5: 2

      .= ( |[(x * (v `1 )), (x * (v `2 )), (x * (v `3 ))]| `3 ) by EUCLID_5: 7

      .= (x * (v `3 )) by EUCLID_5: 2

      .= (x * 0 ) by A2, EUCLID_5: 2

      .= 0 ;

      hence contradiction;

    end;

    theorem :: BKMODEL3:32

    

     Th27: for u be non zero Element of ( TOP-REAL 3) st (((u . 1) ^2 ) + ((u . 2) ^2 )) < 1 & (u . 3) = 1 holds ( Dir u) is Element of BK_model

    proof

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

      assume that

       A1: (((u . 1) ^2 ) + ((u . 2) ^2 )) < 1 and

       A2: (u . 3) = 1;

      reconsider P = ( Dir u) as Point of ( ProjectiveSpace ( TOP-REAL 3)) by ANPROJ_1: 26;

      now

        let v be Element of ( TOP-REAL 3);

        assume that

         A3: v is non zero and

         A4: P = ( Dir v);

        ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = (((((((1 * (u . 1)) * (u . 1)) + ((1 * (u . 2)) * (u . 2))) + ((( - 1) * (u . 3)) * (u . 3))) + (( 0 * (u . 1)) * (u . 2))) + (( 0 * (u . 1)) * (u . 3))) + (( 0 * (u . 2)) * (u . 3))) by PASCAL:def 1

        .= ((((u . 1) ^2 ) + ((u . 2) ^2 )) + ( - 1)) by A2;

        then ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) < (1 + ( - 1)) by A1, XREAL_1: 8;

        hence ( qfconic (1,1,( - 1), 0 , 0 , 0 ,v)) is negative by A3, A4, BKMODEL1: 81;

      end;

      then P in { P where P be Point of ( ProjectiveSpace ( TOP-REAL 3)) : for u be Element of ( TOP-REAL 3) st u is non zero & P = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) is negative };

      hence thesis by BKMODEL2:def 1;

    end;

    theorem :: BKMODEL3:33

    

     Th28: for a,b be Real st ((a ^2 ) + (b ^2 )) <= 1 holds ( Dir |[a, b, 1]|) in ( BK_model \/ absolute )

    proof

      let a,b be Real;

      assume ((a ^2 ) + (b ^2 )) <= 1;

      per cases by XXREAL_0: 1;

        suppose

         A1: ((a ^2 ) + (b ^2 )) = 1;

        reconsider u = |[a, b, 1]| as non zero Element of ( TOP-REAL 3);

        reconsider P = ( Dir u) as Point of ( ProjectiveSpace ( TOP-REAL 3)) by ANPROJ_1: 26;

        now

          

           B1: (u . 1) = (u `1 ) by EUCLID_5:def 1

          .= a by EUCLID_5: 2;

          (u . 2) = (u `2 ) by EUCLID_5:def 2

          .= b by EUCLID_5: 2;

          hence |[(u . 1), (u . 2)]| in ( circle ( 0 , 0 ,1)) by A1, B1, BKMODEL1: 13;

          

          thus (u . 3) = ( |[a, b, 1]| `3 ) by EUCLID_5:def 3

          .= 1 by EUCLID_5: 2;

        end;

        then P is Element of absolute by BKMODEL1: 86;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose

         A2: ((a ^2 ) + (b ^2 )) < 1;

        reconsider w = |[a, b, 1]| as non zero Element of ( TOP-REAL 3);

        (w `1 ) = a & (w `2 ) = b & (w `3 ) = 1 by EUCLID_5: 2;

        then (w . 1) = a & (w . 2) = b & (w . 3) = 1 by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

        then ( Dir |[a, b, 1]|) is Element of BK_model by A2, Th27;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    theorem :: BKMODEL3:34

    

     Th29: not P in ( BK_model \/ absolute ) implies (ex l st P in l & l misses absolute )

    proof

      assume

       A1: not P in ( BK_model \/ absolute );

      then

       A2: not P in BK_model & not P in absolute by XBOOLE_0:def 3;

      consider u9 be Element of ( TOP-REAL 3) such that

       A3: not u9 is zero and

       A4: P = ( Dir u9) by ANPROJ_1: 26;

      per cases ;

        suppose

         A5: (u9 . 3) = 0 ;

        (u9 . 1) <> 0 or (u9 . 2) <> 0

        proof

          assume

           A6: (u9 . 1) = 0 & (u9 . 2) = 0 ;

          u9 = |[(u9 `1 ), (u9 `2 ), (u9 `3 )]| by EUCLID_5: 3

          .= |[ 0 , (u9 `2 ), (u9 `3 )]| by A6, EUCLID_5:def 1

          .= |[ 0 , 0 , (u9 `3 )]| by A6, EUCLID_5:def 2

          .= ( 0. ( TOP-REAL 3)) by A5, EUCLID_5:def 3, EUCLID_5: 4;

          hence contradiction by A3;

        end;

        per cases ;

          suppose

           A7: (u9 . 1) <> 0 ;

          then

          reconsider v = |[( - (u9 . 2)), (u9 . 1), 0 ]| as non zero Element of ( TOP-REAL 3);

          reconsider Q = ( Dir v) as Point of ( ProjectiveSpace ( TOP-REAL 3)) by ANPROJ_1: 26;

          P <> Q

          proof

            assume P = Q;

            then are_Prop (u9,v) by A3, A4, ANPROJ_1: 22;

            then

            consider a be Real such that a <> 0 and

             A9: u9 = (a * v) by ANPROJ_1: 1;

            

             A10: |[(a * ( - (u9 . 2))), (a * (u9 . 1)), (a * 0 )]| = (a * v) by EUCLID_5: 8

            .= |[(u9 `1 ), (u9 `2 ), (u9 `3 )]| by A9, EUCLID_5: 3;

            now

              

              thus (a * ( - (u9 . 2))) = ( |[(u9 `1 ), (u9 `2 ), (u9 `3 )]| `1 ) by A10, EUCLID_5: 2

              .= (u9 `1 ) by EUCLID_5: 2

              .= (u9 . 1) by EUCLID_5:def 1;

              

              thus (a * (u9 . 1)) = ( |[(u9 `1 ), (u9 `2 ), (u9 `3 )]| `2 ) by A10, EUCLID_5: 2

              .= (u9 `2 ) by EUCLID_5: 2

              .= (u9 . 2) by EUCLID_5:def 2;

            end;

            then (u9 . 1) = 0 & (u9 . 2) = 0 by Th10;

            then (u9 `1 ) = 0 & (u9 `2 ) = 0 & (u9 `3 ) = 0 by A5, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

            hence contradiction by A3, EUCLID_5: 3, EUCLID_5: 4;

          end;

          then

          reconsider l9 = ( Line (P,Q)) as LINE of real_projective_plane by COLLSP:def 7;

          reconsider l = l9 as Element of the Lines of ( IncProjSp_of real_projective_plane ) by INCPROJ: 4;

          take l;

          l misses absolute

          proof

            assume not l misses absolute ;

            then

            consider R be object such that

             A11: R in (l /\ absolute ) by XBOOLE_0: 7;

            

             A12: R in l & R in absolute by A11, XBOOLE_0:def 4;

            reconsider R as Element of ( ProjectiveSpace ( TOP-REAL 3)) by A11;

            consider w be non zero Element of ( TOP-REAL 3) such that

             A13: (w . 3) = 1 and

             A14: R = ( Dir w) by A12, Th25;

            reconsider R9 = R as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

            reconsider l2 = l as LINE of ( IncProjSp_of real_projective_plane );

            

             A15: (w `3 ) = 1 by A13, EUCLID_5:def 3;

            

             A16: (u9 `3 ) = 0 by A5, EUCLID_5:def 3;

            

             A17: (v `1 ) = ( - (u9 . 2)) by EUCLID_5: 2

            .= ( - (u9 `2 )) by EUCLID_5:def 2;

            

             A18: (v `2 ) = (u9 . 1) by EUCLID_5: 2

            .= (u9 `1 ) by EUCLID_5:def 1;

            

             A19: (v `3 ) = 0 by EUCLID_5: 2;

            R9 on l2 by A12, INCPROJ: 5;

            then |{u9, v, w}| = 0 by A3, A4, A14, BKMODEL1: 77;

            

            then 0 = ((((((((u9 `1 ) * (v `2 )) * 1) - (((u9 `3 ) * (v `2 )) * (w `1 ))) - (((u9 `1 ) * (v `3 )) * (w `2 ))) + (((u9 `2 ) * (v `3 )) * (w `1 ))) - (((u9 `2 ) * (v `1 )) * 1)) + (((u9 `3 ) * (v `1 )) * (w `2 ))) by A15, ANPROJ_8: 27

            .= (((u9 `1 ) ^2 ) + ((u9 `2 ) ^2 )) by A16, A17, A18, A19;

            then (u9 `1 ) = 0 & (u9 `2 ) = 0 ;

            hence contradiction by A7, EUCLID_5:def 1;

          end;

          hence thesis by COLLSP: 10;

        end;

          suppose

           A20: (u9 . 2) <> 0 ;

          then

          reconsider v = |[( - (u9 . 2)), (u9 . 1), 0 ]| as non zero Element of ( TOP-REAL 3);

          reconsider Q = ( Dir v) as Point of ( ProjectiveSpace ( TOP-REAL 3)) by ANPROJ_1: 26;

          P <> Q

          proof

            assume P = Q;

            then are_Prop (u9,v) by A3, A4, ANPROJ_1: 22;

            then

            consider a be Real such that a <> 0 and

             A22: u9 = (a * v) by ANPROJ_1: 1;

            

             A23: |[(a * ( - (u9 . 2))), (a * (u9 . 1)), (a * 0 )]| = (a * v) by EUCLID_5: 8

            .= |[(u9 `1 ), (u9 `2 ), (u9 `3 )]| by A22, EUCLID_5: 3;

            now

              

              thus (a * ( - (u9 . 2))) = ( |[(u9 `1 ), (u9 `2 ), (u9 `3 )]| `1 ) by A23, EUCLID_5: 2

              .= (u9 `1 ) by EUCLID_5: 2

              .= (u9 . 1) by EUCLID_5:def 1;

              

              thus (a * (u9 . 1)) = ( |[(u9 `1 ), (u9 `2 ), (u9 `3 )]| `2 ) by A23, EUCLID_5: 2

              .= (u9 `2 ) by EUCLID_5: 2

              .= (u9 . 2) by EUCLID_5:def 2;

            end;

            then (u9 . 1) = 0 & (u9 . 2) = 0 by Th10;

            then (u9 `1 ) = 0 & (u9 `2 ) = 0 & (u9 `3 ) = 0 by A5, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

            hence contradiction by A3, EUCLID_5: 3, EUCLID_5: 4;

          end;

          then

          reconsider l9 = ( Line (P,Q)) as LINE of real_projective_plane by COLLSP:def 7;

          reconsider l = l9 as Element of the Lines of ( IncProjSp_of real_projective_plane ) by INCPROJ: 4;

          take l;

          l misses absolute

          proof

            assume not l misses absolute ;

            then

            consider R be object such that

             A24: R in (l /\ absolute ) by XBOOLE_0: 7;

            

             A25: R in l & R in absolute by A24, XBOOLE_0:def 4;

            reconsider R as Element of ( ProjectiveSpace ( TOP-REAL 3)) by A24;

            consider w be non zero Element of ( TOP-REAL 3) such that

             A26: (w . 3) = 1 and

             A27: R = ( Dir w) by A25, Th25;

            reconsider R9 = R as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

            reconsider l2 = l as LINE of ( IncProjSp_of real_projective_plane );

            

             A28: (w `3 ) = 1 by A26, EUCLID_5:def 3;

            

             A29: (u9 `3 ) = 0 by A5, EUCLID_5:def 3;

            

             A30: (v `1 ) = ( - (u9 . 2)) by EUCLID_5: 2

            .= ( - (u9 `2 )) by EUCLID_5:def 2;

            

             A31: (v `2 ) = (u9 . 1) by EUCLID_5: 2

            .= (u9 `1 ) by EUCLID_5:def 1;

            

             A32: (v `3 ) = 0 by EUCLID_5: 2;

            R9 on l2 by A25, INCPROJ: 5;

            then |{u9, v, w}| = 0 by A3, A4, A27, BKMODEL1: 77;

            

            then 0 = ((((((((u9 `1 ) * (v `2 )) * 1) - (((u9 `3 ) * (v `2 )) * (w `1 ))) - (((u9 `1 ) * (v `3 )) * (w `2 ))) + (((u9 `2 ) * (v `3 )) * (w `1 ))) - (((u9 `2 ) * (v `1 )) * 1)) + (((u9 `3 ) * (v `1 )) * (w `2 ))) by A28, ANPROJ_8: 27

            .= (((u9 `1 ) ^2 ) + ((u9 `2 ) ^2 )) by A29, A30, A31, A32;

            then (u9 `1 ) = 0 & (u9 `2 ) = 0 ;

            hence contradiction by A20, EUCLID_5:def 2;

          end;

          hence thesis by COLLSP: 10;

        end;

      end;

        suppose

         A33: (u9 . 3) <> 0 ;

        reconsider u = |[((u9 . 1) / (u9 . 3)), ((u9 . 2) / (u9 . 3)), 1]| as non zero Element of ( TOP-REAL 3);

        

         A34: (u `3 ) = 1 by EUCLID_5: 2;

        then

         A35: (u . 3) = 1 by EUCLID_5:def 3;

        ((u9 . 3) * u) = |[(u9 . 1), (u9 . 2), (u9 . 3)]| by A33, Th22

        .= |[(u9 `1 ), (u9 . 2), (u9 . 3)]| by EUCLID_5:def 1

        .= |[(u9 `1 ), (u9 `2 ), (u9 . 3)]| by EUCLID_5:def 2

        .= |[(u9 `1 ), (u9 `2 ), (u9 `3 )]| by EUCLID_5:def 3

        .= u9 by EUCLID_5: 3;

        then

         A36: are_Prop (u,u9) by A33, ANPROJ_1: 1;

        then

         A37: P = ( Dir u) by A3, A4, ANPROJ_1: 22;

        (u . 1) <> 0 or (u . 2) <> 0

        proof

          assume

           A38: (u . 1) = 0 & (u . 2) = 0 ;

          now

            let v be Element of ( TOP-REAL 3);

            assume

             A39: v is non zero;

            assume P = ( Dir v);

            then

             A40: ( Dir u) = ( Dir v) by A36, A3, A4, ANPROJ_1: 22;

            now

              thus 0 < ((u . 3) ^2 ) by A35;

              

              thus ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = (((((((1 * (u . 1)) * (u . 1)) + ((1 * (u . 2)) * (u . 2))) + ((( - 1) * (u . 3)) * (u . 3))) + (( 0 * (u . 1)) * (u . 2))) + (( 0 * (u . 1)) * (u . 3))) + (( 0 * (u . 2)) * (u . 3))) by PASCAL:def 1

              .= (( - 1) * ((u . 3) ^2 )) by A38;

            end;

            hence ( qfconic (1,1,( - 1), 0 , 0 , 0 ,v)) is negative by A39, A40, BKMODEL1: 81;

          end;

          hence contradiction by A2, BKMODEL2:def 1;

        end;

        per cases ;

          suppose

           A41: (u . 1) <> 0 ;

          then

          reconsider u1 = (u . 1) as non zero Real;

          reconsider u2 = (u . 2) as Real;

          reconsider v = |[( - u2), u1, 0 ]| as non zero Element of ( TOP-REAL 3);

          reconsider Q = ( Dir v) as Element of ( ProjectiveSpace ( TOP-REAL 3)) by ANPROJ_1: 26;

          reconsider l9 = ( Line (P,Q)) as LINE of real_projective_plane by Th26, A37, COLLSP:def 7;

          reconsider l = l9 as Element of the Lines of ( IncProjSp_of real_projective_plane ) by INCPROJ: 4;

          take l;

          l misses absolute

          proof

            assume not l misses absolute ;

            then

            consider R be object such that

             A42: R in (l /\ absolute ) by XBOOLE_0: 7;

            

             A43: R in l & R in absolute by A42, XBOOLE_0:def 4;

            reconsider R as Element of ( ProjectiveSpace ( TOP-REAL 3)) by A42;

            consider w be non zero Element of ( TOP-REAL 3) such that

             A44: (w . 3) = 1 and

             A45: R = ( Dir w) by A43, Th25;

             |[(w . 1), (w . 2)]| in ( circle ( 0 , 0 ,1)) by A43, A44, A45, BKMODEL1: 84;

            then (((w . 1) ^2 ) + ((w . 2) ^2 )) = 1 by BKMODEL1: 13;

            then (((w `1 ) ^2 ) + ((w . 2) ^2 )) = 1 by EUCLID_5:def 1;

            then

             A46: (((w `1 ) ^2 ) + ((w `2 ) ^2 )) = 1 by EUCLID_5:def 2;

            now

              thus (u `1 ) <> 0 by A41, EUCLID_5:def 1;

              thus (u `3 ) = 1 by EUCLID_5: 2;

              (v `1 ) = ( - u2) by EUCLID_5: 2;

              hence (v `1 ) = ( - (u `2 )) by EUCLID_5:def 2;

              (v `2 ) = (u . 1) by EUCLID_5: 2;

              hence (v `2 ) = (u `1 ) by EUCLID_5:def 1;

              thus (v `3 ) = 0 by EUCLID_5: 2;

              thus (w `3 ) = 1 by A44, EUCLID_5:def 3;

              reconsider R9 = R as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

              reconsider l2 = l as LINE of ( IncProjSp_of real_projective_plane );

              R9 on l2 by A43, INCPROJ: 5;

              hence |{u, v, w}| = 0 by A37, A45, BKMODEL1: 77;

              thus 1 < (((u `1 ) ^2 ) + ((u `2 ) ^2 ))

              proof

                assume not 1 < (((u `1 ) ^2 ) + ((u `2 ) ^2 ));

                then ( Dir |[(u `1 ), (u `2 ), 1]|) in ( BK_model \/ absolute ) by Th28;

                hence contradiction by A37, A1, A34, EUCLID_5: 3;

              end;

            end;

            hence contradiction by A46, Th23;

          end;

          hence thesis by COLLSP: 10;

        end;

          suppose

           A47: (u . 2) <> 0 ;

          then

          reconsider u2 = (u . 2) as non zero Real;

          reconsider u1 = (u . 1) as Real;

          reconsider v = |[( - u2), u1, 0 ]| as non zero Element of ( TOP-REAL 3);

          reconsider Q = ( Dir v) as Element of ( ProjectiveSpace ( TOP-REAL 3)) by ANPROJ_1: 26;

          reconsider l9 = ( Line (P,Q)) as LINE of real_projective_plane by A37, Th26, COLLSP:def 7;

          reconsider l = l9 as Element of the Lines of ( IncProjSp_of real_projective_plane ) by INCPROJ: 4;

          take l;

          l misses absolute

          proof

            assume l meets absolute ;

            then

            consider R be object such that

             A48: R in (l /\ absolute ) by XBOOLE_0: 7;

            

             A49: R in l & R in absolute by A48, XBOOLE_0:def 4;

            reconsider R as Element of ( ProjectiveSpace ( TOP-REAL 3)) by A48;

            consider w be non zero Element of ( TOP-REAL 3) such that

             A50: (w . 3) = 1 and

             A51: R = ( Dir w) by A49, Th25;

             |[(w . 1), (w . 2)]| in ( circle ( 0 , 0 ,1)) by A49, A50, A51, BKMODEL1: 84;

            then (((w . 1) ^2 ) + ((w . 2) ^2 )) = 1 by BKMODEL1: 13;

            then (((w `1 ) ^2 ) + ((w . 2) ^2 )) = 1 by EUCLID_5:def 1;

            then

             A53: (((w `1 ) ^2 ) + ((w `2 ) ^2 )) = 1 by EUCLID_5:def 2;

            now

              thus (u `2 ) <> 0 by A47, EUCLID_5:def 2;

              thus (u `3 ) = 1 by EUCLID_5: 2;

              (v `1 ) = ( - u2) by EUCLID_5: 2;

              hence (v `1 ) = ( - (u `2 )) by EUCLID_5:def 2;

              (v `2 ) = (u . 1) by EUCLID_5: 2;

              hence (v `2 ) = (u `1 ) by EUCLID_5:def 1;

              thus (v `3 ) = 0 by EUCLID_5: 2;

              thus (w `3 ) = 1 by A50, EUCLID_5:def 3;

              reconsider R9 = R as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

              reconsider l2 = l as LINE of ( IncProjSp_of real_projective_plane );

              R9 on l2 by A49, INCPROJ: 5;

              hence |{u, v, w}| = 0 by A37, A51, BKMODEL1: 77;

              thus 1 < (((u `1 ) ^2 ) + ((u `2 ) ^2 ))

              proof

                assume not 1 < (((u `1 ) ^2 ) + ((u `2 ) ^2 ));

                then ( Dir |[(u `1 ), (u `2 ), 1]|) in ( BK_model \/ absolute ) by Th28;

                hence contradiction by A37, A1, EUCLID_5: 3, A34;

              end;

            end;

            hence contradiction by A53, Th24;

          end;

          hence thesis by COLLSP: 10;

        end;

      end;

    end;

    theorem :: BKMODEL3:35

    

     Th30: for P be Point of real_projective_plane holds for h be Element of SubGroupK-isometry , N be invertible Matrix of 3, F_Real st h = ( homography N) holds P is Element of absolute iff (( homography N) . P) is Element of absolute

    proof

      let P be Point of real_projective_plane ;

      let h be Element of SubGroupK-isometry ;

      let N be invertible Matrix of 3, F_Real ;

      assume

       A1: h = ( homography N);

      h is Element of EnsK-isometry by BKMODEL2:def 8;

      then

       A2: (( homography N) .: absolute ) = absolute by A1, BKMODEL2: 44;

      ( homography (N ~ )) is Element of SubGroupK-isometry by A1, BKMODEL2: 47;

      then ( homography (N ~ )) is Element of EnsK-isometry by BKMODEL2:def 8;

      then

       A3: (( homography (N ~ )) .: absolute ) = absolute by BKMODEL2: 44;

      set hP = (( homography N) . P);

      hereby

        assume

         A4: P is Element of absolute ;

        ( dom ( homography N)) = the carrier of ( ProjectiveSpace ( TOP-REAL 3)) by FUNCT_2:def 1;

        hence (( homography N) . P) is Element of absolute by A2, A4, FUNCT_1: 108;

      end;

      assume

       A5: (( homography N) . P) is Element of absolute ;

      

       A6: ( dom ( homography (N ~ ))) = the carrier of ( ProjectiveSpace ( TOP-REAL 3)) by FUNCT_2:def 1;

      (( homography (N ~ )) . hP) in (( homography (N ~ )) .: absolute ) by A6, A5, FUNCT_1: 108;

      hence P is Element of absolute by A3, ANPROJ_9: 15;

    end;

    theorem :: BKMODEL3:36

    

     Th31: for P be Element of BK_model holds for h be Element of SubGroupK-isometry , N be invertible Matrix of 3, F_Real st h = ( homography N) holds (( homography N) . P) is Element of BK_model

    proof

      let P be Element of BK_model ;

      let h be Element of SubGroupK-isometry ;

      let N be invertible Matrix of 3, F_Real ;

      assume

       A1: h = ( homography N);

      set hP = (( homography N) . P);

      assume

       A2: not hP is Element of BK_model ;

       not hP is Element of absolute

      proof

        assume hP is Element of absolute ;

        then P is Element of absolute by A1, Th30;

        hence contradiction by XBOOLE_0: 3, BKMODEL2: 1;

      end;

      then not hP in ( BK_model \/ absolute ) by A2, XBOOLE_0:def 3;

      then

      consider l such that

       A3: hP in l and

       A4: l misses absolute by Th29;

      reconsider L = (( line_homography (N ~ )) . l) as LINE of real_projective_plane by INCPROJ: 4;

      reconsider L9 = L as LINE of ( IncProjSp_of real_projective_plane );

      consider P1,P2 be Element of absolute such that P1 <> P2 and

       A5: P1 in L9 and P2 in L9 by A3, Th19, Th12;

      

       A6: (( homography N) . P1) is Element of absolute by A1, Th30;

      (( homography N) . P1) in (( line_homography N) . L) by A5, Th20;

      then (( homography N) . P1) in l by Th15;

      hence contradiction by A6, A4, XBOOLE_0:def 4;

    end;

    theorem :: BKMODEL3:37

    for P be Element of BK_model holds for h be Element of SubGroupK-isometry holds for N be invertible Matrix of 3, F_Real st h = ( homography N) holds ex u be non zero Element of ( TOP-REAL 3) st (( homography N) . P) = ( Dir u) & (u . 3) = 1

    proof

      let P be Element of BK_model ;

      let h be Element of SubGroupK-isometry ;

      let N be invertible Matrix of 3, F_Real ;

      assume h = ( homography N);

      then

      reconsider hP = (( homography N) . P) as Element of BK_model by Th31;

      ex u be non zero Element of ( TOP-REAL 3) st ( Dir u) = hP & (u . 3) = 1 & ( BK_to_REAL2 hP) = |[(u . 1), (u . 2)]| by BKMODEL2:def 2;

      hence thesis;

    end;

    begin

    definition

      :: BKMODEL3:def7

      func BK-model-Betweenness -> Relation of [: BK_model , BK_model :], BK_model means for a,b,c be Element of BK_model holds [ [a, b], c] in it iff ( BK_to_REAL2 b) in ( LSeg (( BK_to_REAL2 a),( BK_to_REAL2 c)));

      existence

      proof

        defpred P[ object, object] means ex a,b,c be Element of BK_model st $1 = [a, b] & $2 = c & ( BK_to_REAL2 b) in ( LSeg (( BK_to_REAL2 a),( BK_to_REAL2 c)));

        consider R be Relation of [: BK_model , BK_model :], BK_model such that

         A1: for x be Element of [: BK_model , BK_model :], y be Element of BK_model holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

        for a,b,c be Element of BK_model holds [ [a, b], c] in R iff ( BK_to_REAL2 b) in ( LSeg (( BK_to_REAL2 a),( BK_to_REAL2 c)))

        proof

          let a,b,c be Element of BK_model ;

          hereby

            assume

             A2: [ [a, b], c] in R;

            reconsider x = [a, b] as Element of [: BK_model , BK_model :];

            consider a9,b9,c9 be Element of BK_model such that

             A3: x = [a9, b9] and

             A4: c = c9 and

             A5: ( BK_to_REAL2 b9) in ( LSeg (( BK_to_REAL2 a9),( BK_to_REAL2 c9))) by A2, A1;

            a = a9 & b = b9 by A3, XTUPLE_0: 1;

            hence ( BK_to_REAL2 b) in ( LSeg (( BK_to_REAL2 a),( BK_to_REAL2 c))) by A4, A5;

          end;

          assume ( BK_to_REAL2 b) in ( LSeg (( BK_to_REAL2 a),( BK_to_REAL2 c)));

          hence [ [a, b], c] in R by A1;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of [: BK_model , BK_model :], BK_model such that

         A6: for a,b,c be Element of BK_model holds [ [a, b], c] in R1 iff ( BK_to_REAL2 b) in ( LSeg (( BK_to_REAL2 a),( BK_to_REAL2 c))) and

         A7: for a,b,c be Element of BK_model holds [ [a, b], c] in R2 iff ( BK_to_REAL2 b) in ( LSeg (( BK_to_REAL2 a),( BK_to_REAL2 c)));

        thus R1 = R2

        proof

          for a,b be object holds [a, b] in R1 iff [a, b] in R2

          proof

            let a,b be object;

            hereby

              assume

               A8: [a, b] in R1;

              then

              consider c,d be object such that

               A9: [a, b] = [c, d] and

               A10: c in [: BK_model , BK_model :] and

               A11: d in BK_model by RELSET_1: 2;

              consider e,f be object such that

               A12: e in BK_model and

               A13: f in BK_model and

               A14: c = [e, f] by A10, ZFMISC_1:def 2;

              reconsider d, e, f as Element of BK_model by A12, A13, A11;

              ( BK_to_REAL2 f) in ( LSeg (( BK_to_REAL2 e),( BK_to_REAL2 d))) by A6, A8, A9, A14;

              hence [a, b] in R2 by A9, A7, A14;

            end;

            assume

             A15: [a, b] in R2;

            then

            consider c,d be object such that

             A16: [a, b] = [c, d] and

             A17: c in [: BK_model , BK_model :] and

             A18: d in BK_model by RELSET_1: 2;

            consider e,f be object such that

             A19: e in BK_model and

             A20: f in BK_model and

             A21: c = [e, f] by A17, ZFMISC_1:def 2;

            reconsider d, e, f as Element of BK_model by A19, A20, A18;

            ( BK_to_REAL2 f) in ( LSeg (( BK_to_REAL2 e),( BK_to_REAL2 d))) by A7, A15, A16, A21;

            hence [a, b] in R1 by A16, A6, A21;

          end;

          hence thesis by RELAT_1:def 2;

        end;

      end;

    end

    definition

      :: BKMODEL3:def8

      func BK-model-Equidistance -> Relation of [: BK_model , BK_model :], [: BK_model , BK_model :] means

      : Def05: for a,b,c,d be Element of BK_model holds [ [a, b], [c, d]] in it iff ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . a) = c & (( homography N) . b) = d;

      existence

      proof

        defpred P[ object, object] means ex a,b,c,d be Element of BK_model st $1 = [a, b] & $2 = [c, d] & ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . a) = c & (( homography N) . b) = d;

        consider R be Relation of [: BK_model , BK_model :], [: BK_model , BK_model :] such that

         A1: for x be Element of [: BK_model , BK_model :], y be Element of [: BK_model , BK_model :] holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

        for a,b,c,d be Element of BK_model holds [ [a, b], [c, d]] in R iff ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . a) = c & (( homography N) . b) = d

        proof

          let a,b,c,d be Element of BK_model ;

          hereby

            assume

             A2: [ [a, b], [c, d]] in R;

            reconsider x = [a, b], y = [c, d] as Element of [: BK_model , BK_model :];

            consider a9,b9,c9,d9 be Element of BK_model such that

             A3: x = [a9, b9] & y = [c9, d9] & ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . a9) = c9 & (( homography N) . b9) = d9 by A2, A1;

            a = a9 & b = b9 & c = c9 & d = d9 by A3, XTUPLE_0: 1;

            hence ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . a) = c & (( homography N) . b) = d by A3;

          end;

          assume ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . a) = c & (( homography N) . b) = d;

          hence [ [a, b], [c, d]] in R by A1;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let B1,B2 be Relation of [: BK_model , BK_model :], [: BK_model , BK_model :] such that

         A4: for a,b,c,d be Element of BK_model holds [ [a, b], [c, d]] in B1 iff ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . a) = c & (( homography N) . b) = d and

         A5: for a,b,c,d be Element of BK_model holds [ [a, b], [c, d]] in B2 iff ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . a) = c & (( homography N) . b) = d;

        thus B1 = B2

        proof

          for a,b be object holds [a, b] in B1 iff [a, b] in B2

          proof

            let a,b be object;

            hereby

              assume

               A6: [a, b] in B1;

              then

               A7: a in [: BK_model , BK_model :] & b in [: BK_model , BK_model :] by ZFMISC_1: 87;

              then

              consider a1,a2 be object such that

               A8: a1 in BK_model and

               A9: a2 in BK_model and

               A10: a = [a1, a2] by ZFMISC_1:def 2;

              consider b1,b2 be object such that

               A11: b1 in BK_model and

               A12: b2 in BK_model and

               A13: b = [b1, b2] by A7, ZFMISC_1:def 2;

              ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . a1) = b1 & (( homography N) . a2) = b2 by A4, A11, A12, A8, A9, A10, A6, A13;

              hence [a, b] in B2 by A10, A13, A5, A8, A9, A11, A12;

            end;

            assume

             A14: [a, b] in B2;

            then

             A14bis: a in [: BK_model , BK_model :] & b in [: BK_model , BK_model :] by ZFMISC_1: 87;

            then

            consider a1,a2 be object such that

             A15: a1 in BK_model and

             A16: a2 in BK_model and

             A17: a = [a1, a2] by ZFMISC_1:def 2;

            consider b1,b2 be object such that

             A18: b1 in BK_model and

             A19: b2 in BK_model and

             A20: b = [b1, b2] by A14bis, ZFMISC_1:def 2;

            ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . a1) = b1 & (( homography N) . a2) = b2 by A5, A18, A19, A15, A16, A17, A14, A20;

            hence [a, b] in B1 by A17, A20, A4, A15, A16, A18, A19;

          end;

          hence thesis by RELAT_1:def 2;

        end;

      end;

    end

    definition

      :: BKMODEL3:def9

      func BK-model-Plane -> TarskiGeometryStruct equals TarskiGeometryStruct (# BK_model , BK-model-Betweenness , BK-model-Equidistance #);

      coherence ;

    end

    begin

    theorem :: BKMODEL3:38

     BK-model-Plane is satisfying_CongruenceSymmetry

    proof

      let P,Q be POINT of BK-model-Plane ;

      ex h be Element of SubGroupK-isometry , N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . P) = Q & (( homography N) . Q) = P by BKMODEL2: 60;

      hence (P,Q) equiv (Q,P) by Def05;

    end;

    begin

    theorem :: BKMODEL3:39

     BK-model-Plane is satisfying_CongruenceEquivalenceRelation

    proof

      let P,Q,R,S,T,U be POINT of BK-model-Plane ;

      assume that

       A1: (P,Q) equiv (R,S) and

       A2: (P,Q) equiv (T,U);

      consider h1 be Element of SubGroupK-isometry such that

       A3: ex N be invertible Matrix of 3, F_Real st h1 = ( homography N) & (( homography N) . P) = R & (( homography N) . Q) = S by A1, Def05;

      consider N1 be invertible Matrix of 3, F_Real such that

       A4: h1 = ( homography N1) & (( homography N1) . P) = R & (( homography N1) . Q) = S by A3;

      reconsider N3 = (N1 ~ ) as invertible Matrix of 3, F_Real ;

      P in BK_model & Q in BK_model ;

      then

       A5: (( homography N3) . R) = P & (( homography N3) . S) = Q by A4, ANPROJ_9: 15;

      reconsider h3 = ( homography N3) as Element of SubGroupK-isometry by A4, BKMODEL2: 47;

      consider h2 be Element of SubGroupK-isometry such that

       A6: ex N be invertible Matrix of 3, F_Real st h2 = ( homography N) & (( homography N) . P) = T & (( homography N) . Q) = U by A2, Def05;

      consider N2 be invertible Matrix of 3, F_Real such that

       A7: h2 = ( homography N2) & (( homography N2) . P) = T & (( homography N2) . Q) = U by A6;

      reconsider N4 = (N2 * N3) as invertible Matrix of 3, F_Real ;

      now

        (h2 * h3) is Element of SubGroupK-isometry ;

        hence ( homography N4) is Element of SubGroupK-isometry by A7, BKMODEL2: 46;

        thus N4 is invertible Matrix of 3, F_Real ;

        R in BK_model & S in BK_model ;

        hence (( homography N4) . R) = T & (( homography N4) . S) = U by A5, A7, ANPROJ_9: 13;

      end;

      hence (R,S) equiv (T,U) by Def05;

    end;

    begin

    theorem :: BKMODEL3:40

     BK-model-Plane is satisfying_CongruenceIdentity

    proof

      let P,Q,R be Point of BK-model-Plane ;

      assume (P,Q) equiv (R,R);

      then ex h be Element of SubGroupK-isometry st ex N be invertible Matrix of 3, F_Real st h = ( homography N) & (( homography N) . P) = R & (( homography N) . Q) = R by Def05;

      hence P = Q by BKMODEL2: 62;

    end;