bkmodel1.miz



    begin

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

g for positive Real,

x,y for Complex,

S,T for Element of ( REAL 2),

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

    theorem :: BKMODEL1:1

    

     Th01: for P1,P2,P3 be Element of ( ProjectiveSpace ( TOP-REAL 3)) st u is non zero & v is non zero & w is non zero & P1 = ( Dir u) & P2 = ( Dir v) & P3 = ( Dir w) holds ((P1,P2,P3) are_collinear iff |{u, v, w}| = 0 )

    proof

      let P1,P2,P3 be Element of ( ProjectiveSpace ( TOP-REAL 3));

      assume that

       A1: u is non zero and

       A2: v is non zero and

       A3: w is non zero and

       A4: P1 = ( Dir u) and

       A5: P2 = ( Dir v) and

       A6: P3 = ( Dir w);

      hereby

        assume (P1,P2,P3) are_collinear ;

        then

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

         A7: P1 = ( Dir u9) and

         A8: P2 = ( Dir v9) and

         A9: P3 = ( Dir w9) & not u9 is zero & not v9 is zero & not w9 is zero & (u9,v9,w9) are_LinDep by ANPROJ_2: 23;

         [( Dir u9), ( Dir v9), ( Dir w9)] in the Collinearity of ( ProjectiveSpace ( TOP-REAL 3)) by A9, ANPROJ_1: 25;

        then (u,v,w) are_LinDep by A7, A8, A9, A1, A2, A3, A4, A5, A6, ANPROJ_1: 25;

        hence |{u, v, w}| = 0 by ANPROJ_8: 43;

      end;

      thus thesis by A1, A2, A3, A4, A5, A6, ANPROJ_2: 23, ANPROJ_8: 43;

    end;

    

     Lem01: a <> 0 & b <> 0 & (a * d) = (b * c) implies ex e st e = (d / b) & e = (c / a) & c = (e * a) & d = (e * b)

    proof

      assume that

       A1: a <> 0 and

       A2: b <> 0 and

       A3: (a * d) = (b * c);

      

       A4: c = ((a * d) / b) by A2, A3, XCMPLX_1: 89

      .= ((d / b) * a) by XCMPLX_1: 74;

      

       A5: d = ((b * c) / a) by A1, A3, XCMPLX_1: 89

      .= ((c / a) * b) by XCMPLX_1: 74;

      (d / b) = (((d / b) * a) / a) by A1, XCMPLX_1: 89

      .= ((b * c) / (b * a)) by A3, XCMPLX_1: 83

      .= ((b / b) / (a / c)) by XCMPLX_1: 84

      .= (1 / (a / c)) by A2, XCMPLX_1: 60

      .= (c / a) by XCMPLX_1: 57;

      hence thesis by A4, A5;

    end;

    

     Lem02: a <> 0 & b = 0 & (a * d) = (b * c) implies ex e st c = (e * a) & d = (e * b)

    proof

      assume that

       A1: a <> 0 and

       A2: b = 0 and

       A3: (a * d) = (b * c);

      

       A4: c = ((c / a) * a) by A1, XCMPLX_1: 87;

      ((c / a) * b) = d by A1, A2, A3;

      hence thesis by A4;

    end;

    theorem :: BKMODEL1:2

    (a <> 0 or b <> 0 ) & (a * d) = (b * c) implies ex e st c = (e * a) & d = (e * b)

    proof

      assume that

       A1: a <> 0 or b <> 0 and

       A2: (a * d) = (b * c);

      per cases ;

        suppose

         A3: a <> 0 ;

        per cases ;

          suppose b = 0 ;

          hence thesis by A1, A2, Lem02;

        end;

          suppose b <> 0 ;

          then ex e st e = (d / b) & e = (c / a) & c = (e * a) & d = (e * b) by A2, A3, Lem01;

          hence thesis;

        end;

      end;

        suppose a = 0 ;

        then ex e st d = (e * b) & c = (e * a) by A1, A2, Lem02;

        hence thesis;

      end;

    end;

    theorem :: BKMODEL1:3

    ((a ^2 ) + (b ^2 )) = 1 & (((c * a) ^2 ) + ((c * b) ^2 )) = 1 implies c = 1 or c = ( - 1)

    proof

      assume that

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

       A2: (((c * a) ^2 ) + ((c * b) ^2 )) = 1;

      1 = ((c * c) * ((a ^2 ) + (b * b))) by A2

      .= (c ^2 ) by A1;

      hence thesis by SQUARE_1: 41;

    end;

    theorem :: BKMODEL1:4

    ((a * u) + (( - a) * u)) = ( 0. ( TOP-REAL 3))

    proof

      (a * u) = |[(a * (u `1 )), (a * (u `2 )), (a * (u `3 ))]| by EUCLID_5: 7;

      

      then ((a * u) + (( - a) * u)) = ( |[(a * (u `1 )), (a * (u `2 )), (a * (u `3 ))]| + |[(( - a) * (u `1 )), (( - a) * (u `2 )), (( - a) * (u `3 ))]|) by EUCLID_5: 7

      .= |[((a * (u `1 )) + (( - a) * (u `1 ))), ((a * (u `2 )) + (( - a) * (u `2 ))), ((a * (u `3 )) + (( - a) * (u `3 )))]| by EUCLID_5: 6

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

      hence thesis by EUCLID_5: 4;

    end;

    theorem :: BKMODEL1:5

     0 <= a & c < 0 & ( delta (a,b,c)) = 0 implies a = 0

    proof

      assume that

       A1: 0 <= a and

       A2: c < 0 and

       A3: ( delta (a,b,c)) = 0 ;

      

       A4: ((b ^2 ) - ((4 * a) * c)) = 0 by A3, QUIN_1:def 1;

       0 <= (b ^2 )

      proof

        per cases ;

          suppose b = 0 ;

          hence thesis;

        end;

          suppose 0 <> b;

          hence thesis by SQUARE_1: 12;

        end;

      end;

      hence thesis by A1, A2, A4;

    end;

    theorem :: BKMODEL1:6

    ( Sum ( sqr (T - S))) = ( Sum ( sqr (S - T)))

    proof

      ( Sum ( sqr (T - S))) = ( |.(T - S).| ^2 ) by TOPREAL9: 5

      .= ( |.(S - T).| ^2 ) by EUCLID: 18;

      hence thesis by TOPREAL9: 5;

    end;

    theorem :: BKMODEL1:7

    ((a ^2 ) + (b ^2 )) = 1 & ((c ^2 ) + (d ^2 )) = 1 & ((c * a) + (d * b)) = 1 implies (b * c) = (a * d)

    proof

      assume that

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

       A2: ((c ^2 ) + (d ^2 )) = 1 and

       A3: ((c * a) + (d * b)) = 1;

      ((c ^2 ) + (d ^2 )) = (((c * a) + (d * b)) ^2 ) by A3, A2

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

      then ((((1 - (a ^2 )) * (c ^2 )) + ((1 - (b ^2 )) * (d ^2 ))) - ((2 * (c * a)) * (d * b))) = 0 ;

      then ((((b * c) ^2 ) + ((a ^2 ) * (d ^2 ))) - ((2 * (c * a)) * (d * b))) = 0 by A1, SQUARE_1: 9;

      then (((b * c) - (a * d)) ^2 ) = 0 ;

      then ((b * c) - (a * d)) = 0 ;

      hence thesis;

    end;

    theorem :: BKMODEL1:8

    ((a ^2 ) + (b ^2 )) = 1 & a = 0 implies b = 1 or b = ( - 1)

    proof

      assume that

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

       A2: a = 0 ;

      (b ^2 ) = (1 ^2 ) by A1, A2;

      hence thesis by SQUARE_1: 40;

    end;

    

     Lem03: (1 + (a ^2 )) <> 0

    proof

      assume

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

      then (a ^2 ) = ( - 1);

      then a = 0 by SQUARE_1: 12;

      hence contradiction by A1;

    end;

    theorem :: BKMODEL1:9

    

     Th07: 0 <= (a ^2 )

    proof

      per cases ;

        suppose a = 0 ;

        hence thesis;

      end;

        suppose a <> 0 ;

        hence thesis by SQUARE_1: 12;

      end;

    end;

    

     Lem04: (a ^2 ) = (1 / b) implies a = (1 / ( sqrt b)) or a = (( - 1) / ( sqrt b))

    proof

      assume

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

      reconsider ib = (1 / b) as Real;

      

       A2: 0 <= b by A1, Th07;

       0 <= ib by A1, Th07;

      then ib = (( sqrt (1 / b)) ^2 ) by SQUARE_1:def 2;

      then

       A3: a = ( sqrt (1 / b)) or a = ( - ( sqrt (1 / b))) by A1, SQUARE_1: 40;

      ( - (( sqrt 1) / ( sqrt b))) = (( - 1) / ( sqrt b)) by XCMPLX_1: 187, SQUARE_1: 18;

      hence thesis by A3, A2, SQUARE_1: 30, SQUARE_1: 18;

    end;

    theorem :: BKMODEL1:10

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

    proof

      assume

       a1: (((a * b) ^2 ) + (b ^2 )) = 1;

      (b ^2 ) = ((((a ^2 ) + 1) * (b ^2 )) / ((a ^2 ) + 1)) by XCMPLX_1: 89, Lem03

      .= (1 / ((a ^2 ) + 1)) by a1;

      hence thesis by Lem04;

    end;

    

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

    proof

      let z be non zero Complex;

      (((1 / z) ^2 ) * (z ^2 )) = (((1 / z) * ((1 / z) * z)) * z)

      .= (((1 / z) * 1) * z) by XCMPLX_1: 106

      .= 1 by XCMPLX_1: 106;

      hence thesis;

    end;

    theorem :: BKMODEL1:11

    a <> 0 & (b ^2 ) = (1 + (a * a)) implies ((((a * (1 / b)) * a) * (( - 1) / b)) + ((1 / b) * (( - 1) / b))) = ( - 1)

    proof

      assume that

       A1: a <> 0 and

       A2: (b ^2 ) = (1 + (a * a));

      

       A3: b <> 0

      proof

        assume b = 0 ;

        then (a ^2 ) = ( - 1) by A2;

        hence contradiction by A1, SQUARE_1: 12;

      end;

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

      .= (((1 / b) * (( - 1) * (1 / b))) * ((a * a) + 1)) by XCMPLX_1: 74

      .= (( - 1) * (((1 / b) ^2 ) * (b ^2 ))) by A2

      .= (( - 1) * 1) by A3, Lem05;

      hence thesis;

    end;

    theorem :: BKMODEL1:12

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

    proof

      ((a ^2 ) * (1 / (b ^2 ))) = ((a * a) * ((1 / b) * (1 / b))) by XCMPLX_1: 102

      .= ((a * (a * (1 / b))) * (1 / b))

      .= ((a * ((a * 1) / b)) * (1 / b)) by XCMPLX_1: 74

      .= ((a / b) * (a * (1 / b)))

      .= ((a / b) * ((a * 1) / b)) by XCMPLX_1: 74

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

      hence thesis;

    end;

    theorem :: BKMODEL1:13

    

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

    proof

      hereby

        assume

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

        reconsider p = |[a, b]| as Point of ( TOP-REAL 2);

         |.(p - |[ 0 , 0 ]|).| = 1

        proof

          ( |.(p - |[ 0 , 0 ]|).| ^2 ) = ( |. |[(a - 0 ), (b - 0 )]|.| ^2 ) by EUCLID: 62

          .= 1 by A1, TOPGEN_5: 9;

          hence thesis by SQUARE_1: 41;

        end;

        hence |[a, b]| in ( circle ( 0 , 0 ,1));

      end;

      assume

       A2: |[a, b]| in ( circle ( 0 , 0 ,1));

      

      thus ((a ^2 ) + (b ^2 )) = ( |. |[(a - 0 ), (b - 0 )]|.| ^2 ) by TOPGEN_5: 9

      .= ( |.( |[a, b]| - |[ 0 , 0 ]|).| ^2 ) by EUCLID: 62

      .= (1 ^2 ) by A2, TOPREAL9: 43

      .= 1;

    end;

    theorem :: BKMODEL1:14

    

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

    proof

      hereby

        assume

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

        reconsider p = |[a, b]| as Point of ( TOP-REAL 2);

         |.(p - |[ 0 , 0 ]|).| = g

        proof

          

           A2: ( |.(p - |[ 0 , 0 ]|).| ^2 ) = ( |. |[(a - 0 ), (b - 0 )]|.| ^2 ) by EUCLID: 62

          .= (g ^2 ) by A1, TOPGEN_5: 9;

          ( - g) < 0 ;

          hence thesis by A2, SQUARE_1: 40;

        end;

        hence |[a, b]| in ( circle ( 0 , 0 ,g));

      end;

      assume

       A3: |[a, b]| in ( circle ( 0 , 0 ,g));

      

      thus ((a ^2 ) + (b ^2 )) = ( |. |[(a - 0 ), (b - 0 )]|.| ^2 ) by TOPGEN_5: 9

      .= ( |.( |[a, b]| - |[ 0 , 0 ]|).| ^2 ) by EUCLID: 62

      .= (g ^2 ) by A3, TOPREAL9: 43;

    end;

    

     Lem06: (((a * b) ^2 ) + ((a * c) ^2 )) = ((a ^2 ) * ((b ^2 ) + (c ^2 )));

    theorem :: BKMODEL1:15

    

     Th13: a <> 0 & ( - 1) < a < 1 & b = ((2 + ( sqrt ( delta ((a * a),( - 2),1)))) / ((2 * a) * a)) implies ((((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b)) = 0

    proof

      assume that

       A1: a <> 0 and

       A2: ( - 1) < a < 1 and

       A3: b = ((2 + ( sqrt ( delta ((a * a),( - 2),1)))) / ((2 * a) * a));

      set x1 = ((( - ( - 2)) - ( sqrt ( delta ((a * a),( - 2),1)))) / (2 * (a * a))), x2 = ((( - ( - 2)) + ( sqrt ( delta ((a * a),( - 2),1)))) / (2 * (a * a)));

      

       A4: 0 <= (1 - (a ^2 ))

      proof

        ((a ^2 ) * (1 ^2 )) <= 1 by A2, SQUARE_1: 53;

        then (a ^2 ) < 1 by A2, SQUARE_1: 41, XXREAL_0: 1;

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

        hence thesis;

      end;

      ( delta ((a * a),( - 2),1)) >= 0

      proof

        ( delta ((a * a),( - 2),1)) = ((( - 2) ^2 ) - ((4 * (a * a)) * 1)) by QUIN_1:def 1

        .= (4 * (1 - (a ^2 )));

        hence thesis by A4;

      end;

      

      then ((((a * a) * (b ^2 )) + (( - 2) * b)) + 1) = (((a * a) * (b - x1)) * (x2 - x2)) by A3, A1, QUIN_1: 16

      .= 0 ;

      hence thesis;

    end;

    

     Lem07: ( - 1) < a < 1 implies ex b st ((((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b)) = 0

    proof

      assume

       A1: ( - 1) < a < 1;

      per cases ;

        suppose

         A2: a = 0 ;

        set b = (1 / 2);

        take b;

        thus thesis by A2;

      end;

        suppose

         A3: a <> 0 ;

        take b = ((2 + ( sqrt ( delta ((a * a),( - 2),1)))) / ((2 * a) * a));

        thus thesis by A1, A3, Th13;

      end;

    end;

    theorem :: BKMODEL1:16

    ((a ^2 ) + (b ^2 )) = 1 & ( - 1) < c < 1 implies ex d, e, f st e = (((d * c) * a) + ((1 - d) * ( - b))) & f = (((d * c) * b) + ((1 - d) * a)) & ((e ^2 ) + (f ^2 )) = (d ^2 )

    proof

      assume that

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

       A2: ( - 1) < c < 1;

      consider d be Real such that

       A3: ((((((1 + (c * c)) * d) * d) - (2 * d)) + 1) - (d * d)) = 0 by A2, Lem07;

      reconsider e = (((d * c) * a) + ((1 - d) * ( - b))), f = (((d * c) * b) + ((1 - d) * a)) as Real;

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

      .= ((((d * c) ^2 ) * 1) + (((1 - d) ^2 ) * 1)) by A1, Lem06

      .= (d ^2 ) by A3;

      hence thesis;

    end;

    theorem :: BKMODEL1:17

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

    proof

      assume that

       A1: ((a ^2 ) + (b ^2 )) < 1 and

       A2: ((c ^2 ) + (d ^2 )) = 1;

      reconsider u = |[a, b]|, v = |[c, d]| as Element of ( TOP-REAL 2);

      

       A4: |. |(u, v)|.| <= ( |.u.| * |.v.|) by EUCLID_2: 51;

      

       A5: ( |.u.| ^2 ) < 1 & ( |.v.| ^2 ) = 1 by A1, A2, TOPGEN_5: 9;

      

       A6: |(u, v)| = (((u `1 ) * (v `1 )) + ((u `2 ) * (v `2 ))) by EUCLID_3: 41

      .= ((a * (v `1 )) + ((u `2 ) * (v `2 ))) by EUCLID: 52

      .= ((a * (v `1 )) + (b * (v `2 ))) by EUCLID: 52

      .= ((a * c) + (b * (v `2 ))) by EUCLID: 52

      .= ((a * c) + (b * d)) by EUCLID: 52;

      (( |.u.| ^2 ) * ( |.v.| ^2 )) < (1 * 1) by A5;

      then (( |.u.| * |.v.|) ^2 ) < 1;

      then ( |.u.| * |.v.|) < 1 by SQUARE_1: 52;

      then

       A7: |. |(u, v)|.| < 1 by XXREAL_0: 2, A4;

       |(u, v)| <= |. |(u, v)|.| by COMPLEX1: 76;

      then ((a * c) + (b * d)) < 1 by A6, A7, XXREAL_0: 2;

      then (2 * ((a * c) + (b * d))) < (2 * 1) by XREAL_1: 68;

      then ((((2 * a) * c) + ((2 * b) * d)) + ((a ^2 ) + (b ^2 ))) < (2 + 1) by A1, XREAL_1: 8;

      then (((((2 * a) * c) + ((2 * b) * d)) + ((a ^2 ) + (b ^2 ))) + 1) < ((2 + 1) + 1) by XREAL_1: 8;

      then ((((((2 * a) * c) + ((2 * b) * d)) + ((a ^2 ) + (b ^2 ))) + 1) / 4) < (4 / 4) by XREAL_1: 74;

      hence thesis by A2;

    end;

    

     Lem08: 0 <= a & c <= 0 implies 0 <= ( delta (a,b,c))

    proof

      assume that

       A1: 0 <= a and

       A2: c <= 0 ;

      

       A3: ( delta (a,b,c)) = ((b ^2 ) - ((4 * a) * c)) by QUIN_1:def 1;

       0 <= (b * b)

      proof

        per cases ;

          suppose b = 0 ;

          hence thesis;

        end;

          suppose b <> 0 ;

          then 0 < (b ^2 ) by SQUARE_1: 12;

          hence thesis;

        end;

      end;

      hence thesis by A1, A2, A3;

    end;

    theorem :: BKMODEL1:18

    ( |.S.| ^2 ) <= 1 implies 0 <= ( delta (( Sum ( sqr (T - S))),b,(( Sum ( sqr S)) - 1)))

    proof

      assume ( |.S.| ^2 ) <= 1;

      then (( |.S.| ^2 ) - 1) <= (( |.S.| ^2 ) - ( |.S.| ^2 )) by XREAL_1: 10;

      then

       A1: (( Sum ( sqr S)) - 1) <= 0 by TOPREAL9: 5;

       0 <= ( |.(T - S).| ^2 );

      then 0 <= ( Sum ( sqr (T - S))) by TOPREAL9: 5;

      hence thesis by A1, Lem08;

    end;

    theorem :: BKMODEL1:19

    ((a ^2 ) + (b ^2 )) is negative implies a = 0 & b = 0

    proof

      assume

       A1: ((a ^2 ) + (b ^2 )) is negative;

       0 <= (a * a) & 0 <= (b * b) by XREAL_1: 63;

      hence thesis by A1;

    end;

    theorem :: BKMODEL1:20

    u = |[a, b, 1]| & v = |[c, d, 1]| & w = |[((a + c) / 2), ((b + d) / 2), 1]| implies |{u, v, w}| = 0

    proof

      assume that

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

       A2: v = |[c, d, 1]| and

       A3: w = |[((a + c) / 2), ((b + d) / 2), 1]|;

      

       A4: (u `1 ) = a & (u `2 ) = b & (u `3 ) = 1 & (v `1 ) = c & (v `2 ) = d & (v `3 ) = 1 & (w `1 ) = ((a + c) / 2) & (w `2 ) = ((b + d) / 2) & (w `3 ) = 1 by A1, A2, A3, EUCLID_5: 2;

       |{u, v, w}| = ((((((((u `1 ) * (v `2 )) * (w `3 )) - (((u `3 ) * (v `2 )) * (w `1 ))) - (((u `1 ) * (v `3 )) * (w `2 ))) + (((u `2 ) * (v `3 )) * (w `1 ))) - (((u `2 ) * (v `1 )) * (w `3 ))) + (((u `3 ) * (v `1 )) * (w `2 ))) by ANPROJ_8: 27

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

      hence thesis;

    end;

    theorem :: BKMODEL1:21

    

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

    proof

      

       A1: (a * (u `1 )) = (a * (u . 1)) by EUCLID_5:def 1

      .= ((a * u) . 1) by RVSUM_1: 44

      .= ((a * u) `1 ) by EUCLID_5:def 1;

      

       A2: (a * (u `2 )) = (a * (u . 2)) by EUCLID_5:def 2

      .= ((a * u) . 2) by RVSUM_1: 44

      .= ((a * u) `2 ) by EUCLID_5:def 2;

      

       A3: (a * (u `3 )) = (a * (u . 3)) by EUCLID_5:def 3

      .= ((a * u) . 3) by RVSUM_1: 44

      .= ((a * u) `3 ) by EUCLID_5:def 3;

      

      thus (a * |(u, v)|) = (a * ((((u `1 ) * (v `1 )) + ((u `2 ) * (v `2 ))) + ((u `3 ) * (v `3 )))) by EUCLID_5: 29

      .= (((((a * u) `1 ) * (v `1 )) + (((a * u) `2 ) * (v `2 ))) + (((a * u) `3 ) * (v `3 ))) by A1, A2, A3

      .= |((a * u), v)| by EUCLID_5: 29;

      

       A4: (a * (v `1 )) = (a * (v . 1)) by EUCLID_5:def 1

      .= ((a * v) . 1) by RVSUM_1: 44

      .= ((a * v) `1 ) by EUCLID_5:def 1;

      

       A5: (a * (v `2 )) = (a * (v . 2)) by EUCLID_5:def 2

      .= ((a * v) . 2) by RVSUM_1: 44

      .= ((a * v) `2 ) by EUCLID_5:def 2;

      

       A6: (a * (v `3 )) = (a * (v . 3)) by EUCLID_5:def 3

      .= ((a * v) . 3) by RVSUM_1: 44

      .= ((a * v) `3 ) by EUCLID_5:def 3;

      

      thus (a * |(u, v)|) = (a * ((((u `1 ) * (v `1 )) + ((u `2 ) * (v `2 ))) + ((u `3 ) * (v `3 )))) by EUCLID_5: 29

      .= ((((u `1 ) * ((a * v) `1 )) + ((u `2 ) * ((a * v) `2 ))) + ((u `3 ) * ((a * v) `3 ))) by A4, A5, A6

      .= |(u, (a * v))| by EUCLID_5: 29;

    end;

    reserve a,b,c for Element of F_Real ,

M,N for Matrix of 3, F_Real ;

    theorem :: BKMODEL1:22

    M = ( symmetric_3 ( 0 , 0 , 0 , 0 , 0 , 0 )) implies ( Det M) = ( 0. F_Real )

    proof

      assume

       A1: M = ( symmetric_3 ( 0 , 0 , 0 , 0 , 0 , 0 ));

      reconsider z = 0 as Element of F_Real ;

      M = <* <*z, z, z*>, <*z, z, z*>, <*z, z, z*>*> by A1, PASCAL:def 3;

      then ( Det M) = (((((((z * z) * z) - ((z * z) * z)) - ((z * z) * z)) + ((z * z) * z)) - ((z * z) * z)) + ((z * z) * z)) by MATRIX_9: 46;

      hence thesis;

    end;

    

     Lem09: for a11,a12,a13,a21,a22,a23,a31,a32,a33,b11,b12,b13,b21,b22,b23,b31,b32,b33 be Element of F_Real holds for A,B be Matrix of 3, F_Real st A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*> & B = <* <*b11, b12, b13*>, <*b21, b22, b23*>, <*b31, b32, b33*>*> holds ((A * B) * (1,1)) = (((a11 * b11) + (a12 * b21)) + (a13 * b31)) & ((A * B) * (1,2)) = (((a11 * b12) + (a12 * b22)) + (a13 * b32)) & ((A * B) * (1,3)) = (((a11 * b13) + (a12 * b23)) + (a13 * b33)) & ((A * B) * (2,1)) = (((a21 * b11) + (a22 * b21)) + (a23 * b31)) & ((A * B) * (2,2)) = (((a21 * b12) + (a22 * b22)) + (a23 * b32)) & ((A * B) * (2,3)) = (((a21 * b13) + (a22 * b23)) + (a23 * b33)) & ((A * B) * (3,1)) = (((a31 * b11) + (a32 * b21)) + (a33 * b31)) & ((A * B) * (3,2)) = (((a31 * b12) + (a32 * b22)) + (a33 * b32)) & ((A * B) * (3,3)) = (((a31 * b13) + (a32 * b23)) + (a33 * b33))

    proof

      let a11,a12,a13,a21,a22,a23,a31,a32,a33,b11,b12,b13,b21,b22,b23,b31,b32,b33 be Element of F_Real ;

      let A,B be Matrix of 3, F_Real ;

      assume that

       A1: A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*> and

       A2: B = <* <*b11, b12, b13*>, <*b21, b22, b23*>, <*b31, b32, b33*>*>;

      

       A3: (A * B) = <* <*(((a11 * b11) + (a12 * b21)) + (a13 * b31)), (((a11 * b12) + (a12 * b22)) + (a13 * b32)), (((a11 * b13) + (a12 * b23)) + (a13 * b33))*>, <*(((a21 * b11) + (a22 * b21)) + (a23 * b31)), (((a21 * b12) + (a22 * b22)) + (a23 * b32)), (((a21 * b13) + (a22 * b23)) + (a23 * b33))*>, <*(((a31 * b11) + (a32 * b21)) + (a33 * b31)), (((a31 * b12) + (a32 * b22)) + (a33 * b32)), (((a31 * b13) + (a32 * b23)) + (a33 * b33))*>*> by A1, A2, ANPROJ_9: 6;

      reconsider C = (A * B) as Matrix of 3, F_Real ;

      C = <* <*(C * (1,1)), (C * (1,2)), (C * (1,3))*>, <*(C * (2,1)), (C * (2,2)), (C * (2,3))*>, <*(C * (3,1)), (C * (3,2)), (C * (3,3))*>*> by MATRIXR2: 37;

      hence thesis by A3, PASCAL: 2;

    end;

    theorem :: BKMODEL1:23

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

    proof

      assume

       A1: N = <* <*a, 0 , 0 *>, <* 0 , b, 0 *>, <* 0 , 0 , c*>*>;

      reconsider a11 = a, a12 = 0 , a13 = 0 , a21 = 0 , a22 = b, a23 = 0 , a31 = 0 , a32 = 0 , a33 = c, b11 = (M * (1,1)), b12 = (M * (1,2)), b13 = (M * (1,3)), b21 = (M * (2,1)), b22 = (M * (2,2)), b23 = (M * (2,3)), b31 = (M * (3,1)), b32 = (M * (3,2)), b33 = (M * (3,3)) as Element of F_Real ;

      

       A2: M = <* <*b11, b12, b13*>, <*b21, b22, b23*>, <*b31, b32, b33*>*> by MATRIXR2: 37;

      then

       A3: ((N * M) * (1,1)) = (((a11 * b11) + (a12 * b21)) + (a13 * b31)) & ((N * M) * (1,2)) = (((a11 * b12) + (a12 * b22)) + (a13 * b32)) & ((N * M) * (1,3)) = (((a11 * b13) + (a12 * b23)) + (a13 * b33)) & ((N * M) * (2,1)) = (((a21 * b11) + (a22 * b21)) + (a23 * b31)) & ((N * M) * (2,2)) = (((a21 * b12) + (a22 * b22)) + (a23 * b32)) & ((N * M) * (2,3)) = (((a21 * b13) + (a22 * b23)) + (a23 * b33)) & ((N * M) * (3,1)) = (((a31 * b11) + (a32 * b21)) + (a33 * b31)) & ((N * M) * (3,2)) = (((a31 * b12) + (a32 * b22)) + (a33 * b32)) & ((N * M) * (3,3)) = (((a31 * b13) + (a32 * b23)) + (a33 * b33)) by A1, Lem09;

      reconsider c11 = (a * b11), c12 = (a * b12), c13 = (a * b13), c21 = (b * b21), c22 = (b * b22), c23 = (b * b23), c31 = (c * b31), c32 = (c * b32), c33 = (c * b33) as Element of F_Real ;

      

       A4: (N * M) = <* <*c11, c12, c13*>, <*c21, c22, c23*>, <*c31, c32, c33*>*> by A3, MATRIXR2: 37;

      (M @ ) = <* <*b11, b21, b31*>, <*b12, b22, b32*>, <*b13, b23, b33*>*> by A2, ANPROJ_8: 22;

      then (((M @ ) * (N * M)) * (1,1)) = (((b11 * (a * b11)) + (b21 * (b * b21))) + (b31 * (c * b31))) & (((M @ ) * (N * M)) * (1,2)) = (((b11 * (a * b12)) + (b21 * (b * b22))) + (b31 * (c * b32))) & (((M @ ) * (N * M)) * (1,3)) = (((b11 * (a * b13)) + (b21 * (b * b23))) + (b31 * (c * b33))) & (((M @ ) * (N * M)) * (2,1)) = (((b12 * (a * b11)) + (b22 * (b * b21))) + (b32 * (c * b31))) & (((M @ ) * (N * M)) * (2,2)) = (((b12 * (a * b12)) + (b22 * (b * b22))) + (b32 * (c * b32))) & (((M @ ) * (N * M)) * (2,3)) = (((b12 * (a * b13)) + (b22 * (b * b23))) + (b32 * (c * b33))) & (((M @ ) * (N * M)) * (3,1)) = (((b13 * (a * b11)) + (b23 * (b * b21))) + (b33 * (c * b31))) & (((M @ ) * (N * M)) * (3,2)) = (((b13 * (a * b12)) + (b23 * (b * b22))) + (b33 * (c * b32))) & (((M @ ) * (N * M)) * (3,3)) = (((b13 * (a * b13)) + (b23 * (b * b23))) + (b33 * (c * b33))) by A4, Lem09;

      hence thesis;

    end;

    theorem :: BKMODEL1:24

    for m,n be Nat holds for M be Matrix of m, F_Real holds for N be Matrix of m, n, F_Real st m > 0 holds (M * N) is Matrix of m, n, F_Real

    proof

      let m,n be Nat;

      let M be Matrix of m, F_Real ;

      let N be Matrix of m, n, F_Real ;

      assume

       A1: m > 0 ;

      ( len N) = m & ( width N) = n by A1, MATRIX_0: 23;

      then ( width M) = ( len N) by A1, MATRIX_0: 23;

      then ( len (M * N)) = ( len M) & ( width (M * N)) = ( width N) by MATRIX_3:def 4;

      then ( len (M * N)) = m & ( width (M * N)) = n by A1, MATRIX_0: 23;

      hence thesis by A1, MATRIX_0: 20;

    end;

    reserve D for non empty set;

    reserve d1,d2,d3 for Element of D;

    reserve A for Matrix of 1, 3, D;

    reserve B for Matrix of 3, 1, D;

    theorem :: BKMODEL1:25

    for M be Matrix of 1, D holds (M @ ) = M

    proof

      let M be Matrix of 1, D;

      

       A1: M = <* <*(M * (1,1))*>*> by MATRIX13: 20;

      ( Indices M) = [: {1}, {1}:] by MATRIX_0: 24, FINSEQ_1: 2;

      then [1, 1] in ( Indices M) by ZFMISC_1: 28;

      then ((M @ ) * (1,1)) = (M * (1,1)) by MATRIX_0:def 6;

      hence thesis by A1, MATRIX13: 20;

    end;

    theorem :: BKMODEL1:26

    

     Th23: (A @ ) is 3, 1 -size

    proof

      ( width A) = 3 & ( len A) = 1 by MATRIX_0: 23;

      then

       A1: ( len (A @ )) = 3 & ( width (A @ )) = 1 by MATRIX_0: 29;

      then

      consider s1 be FinSequence such that

       A2: s1 in ( rng (A @ )) and

       A3: ( len s1) = 1 by MATRIX_0:def 3;

      consider n0 be Nat such that

       A4: for x be object st x in ( rng (A @ )) holds ex s be FinSequence st s = x & ( len s) = n0 by MATRIX_0:def 1;

      consider s be FinSequence such that

       A5: s = s1 and

       A6: ( len s) = n0 by A2, A4;

      for p be FinSequence of D st p in ( rng (A @ )) holds ( len p) = 1

      proof

        let p be FinSequence of D;

        assume

         A7: p in ( rng (A @ ));

        consider s be FinSequence such that

         A8: s = p and

         A9: ( len s) = n0 by A7, A4;

        thus thesis by A3, A5, A6, A8, A9;

      end;

      hence thesis by A1, MATRIX_0:def 2;

    end;

    theorem :: BKMODEL1:27

    

     Th24: <* <*d1, d2, d3*>*> is Matrix of 1, 3, D

    proof

      

       A1: <*d1, d2, d3*> is FinSequence of D by FINSEQ_2: 14;

      ( len <*d1, d2, d3*>) = 3 by FINSEQ_1: 45;

      hence thesis by A1, MATRIX_0: 11;

    end;

    theorem :: BKMODEL1:28

    

     Th25: <* <*d1*>, <*d2*>, <*d3*>*> is Matrix of 3, 1, D

    proof

      reconsider p = <*d1*>, q = <*d2*>, r = <*d3*> as FinSequence of D;

      ( len p) = 1 & ( len q) = 1 & ( len r) = 1 by FINSEQ_1: 40;

      hence thesis by MATRIXR2: 34;

    end;

    theorem :: BKMODEL1:29

    

     Th26: A = <* <*(A * (1,1)), (A * (1,2)), (A * (1,3))*>*>

    proof

      reconsider B = <* <*(A * (1,1)), (A * (1,2)), (A * (1,3))*>*> as Matrix of 1, 3, D by Th24;

      

       A1: ( len A) = 1 & ( width A) = 3 by MATRIX_0: 23;

      

       A2: for i,j be Nat st [i, j] in ( Indices A) holds (A * (i,j)) = (B * (i,j))

      proof

        let i,j be Nat;

        

         A3: ( Indices B) = [:( Seg 1), ( Seg 3):] by MATRIX_0: 23;

        

         A4: ( Indices A) = [:( Seg 1), ( Seg 3):] by MATRIX_0: 23;

        assume

         A5: [i, j] in ( Indices A);

        then i in {1} by A4, ZFMISC_1: 87, FINSEQ_1: 2;

        then

         A6: i = 1 by TARSKI:def 1;

        j in {1, 2, 3} by A4, A5, ZFMISC_1: 87, FINSEQ_3: 1;

        per cases by A6, ENUMSET1:def 1;

          suppose

           A7: [i, j] = [1, 1];

          then

          consider p be FinSequence of D such that

           A8: p = (B . 1) and

           A9: (B * (1,1)) = (p . 1) by A3, A4, A5, MATRIX_0:def 5;

          

           A10: (B . 1) = <*(A * (1,1)), (A * (1,2)), (A * (1,3))*> by FINSEQ_1: 40;

          i = 1 & j = 1 by A7, XTUPLE_0: 1;

          hence thesis by A10, A8, A9, FINSEQ_1: 45;

        end;

          suppose

           A11: [i, j] = [1, 2];

          then

          consider p be FinSequence of D such that

           A12: p = (B . 1) and

           A13: (B * (1,2)) = (p . 2) by A3, A4, A5, MATRIX_0:def 5;

          

           A14: (B . 1) = <*(A * (1,1)), (A * (1,2)), (A * (1,3))*> by FINSEQ_1: 40;

          i = 1 & j = 2 by A11, XTUPLE_0: 1;

          hence thesis by A14, A12, A13, FINSEQ_1: 45;

        end;

          suppose

           A15: [i, j] = [1, 3];

          then

          consider p be FinSequence of D such that

           A16: p = (B . 1) and

           A17: (B * (1,3)) = (p . 3) by A3, A4, A5, MATRIX_0:def 5;

          

           A18: (B . 1) = <*(A * (1,1)), (A * (1,2)), (A * (1,3))*> by FINSEQ_1: 40;

          i = 1 & j = 3 by A15, XTUPLE_0: 1;

          hence thesis by A18, A16, A17, FINSEQ_1: 45;

        end;

      end;

      ( len B) = 1 & ( width B) = 3 by MATRIX_0: 23;

      hence thesis by A1, A2, MATRIX_0: 21;

    end;

    theorem :: BKMODEL1:30

    

     Th27: B = <* <*(B * (1,1))*>, <*(B * (2,1))*>, <*(B * (3,1))*>*>

    proof

      reconsider C = <* <*(B * (1,1))*>, <*(B * (2,1))*>, <*(B * (3,1))*>*> as Matrix of 3, 1, D by Th25;

      

       A1: ( len B) = 3 & ( width B) = 1 by MATRIX_0: 23;

      

       A2: for i,j be Nat st [i, j] in ( Indices B) holds (B * (i,j)) = (C * (i,j))

      proof

        let i,j be Nat;

        

         A3: ( Indices C) = [:( Seg 3), ( Seg 1):] by MATRIX_0: 23;

        

         A4: ( Indices B) = [:( Seg 3), ( Seg 1):] by MATRIX_0: 23;

        assume

         A5: [i, j] in ( Indices B);

        then i in ( Seg 3) & j in ( Seg 1) by A4, ZFMISC_1: 87;

        then (i = 1 or i = 2 or i = 3) & j = 1 by FINSEQ_1: 2, FINSEQ_3: 1, ENUMSET1:def 1, TARSKI:def 1;

        per cases ;

          suppose

           A6: [i, j] = [1, 1];

          then

          consider p be FinSequence of D such that

           A7: p = (C . 1) and

           A8: (C * (1,1)) = (p . 1) by A3, A4, A5, MATRIX_0:def 5;

          

           A9: (C . 1) = <*(B * (1,1))*> by FINSEQ_1: 45;

          i = 1 & j = 1 by A6, XTUPLE_0: 1;

          hence thesis by A9, A7, A8, FINSEQ_1: 40;

        end;

          suppose

           A10: [i, j] = [2, 1];

          then

          consider p be FinSequence of D such that

           A11: p = (C . 2) and

           A12: (C * (2,1)) = (p . 1) by A3, A4, A5, MATRIX_0:def 5;

          

           A13: (C . 2) = <*(B * (2,1))*> by FINSEQ_1: 45;

          i = 2 & j = 1 by A10, XTUPLE_0: 1;

          hence thesis by A13, A11, A12, FINSEQ_1: 40;

        end;

          suppose

           A14: [i, j] = [3, 1];

          then

          consider p be FinSequence of D such that

           A15: p = (C . 3) and

           A16: (C * (3,1)) = (p . 1) by A3, A4, A5, MATRIX_0:def 5;

          

           A17: (C . 3) = <*(B * (3,1))*> by FINSEQ_1: 45;

          i = 3 & j = 1 by A14, XTUPLE_0: 1;

          hence thesis by A17, A15, A16, FINSEQ_1: 40;

        end;

      end;

      ( len C) = 3 & ( width C) = 1 by MATRIX_0: 23;

      hence thesis by A1, A2, MATRIX_0: 21;

    end;

    theorem :: BKMODEL1:31

    (A @ ) = <* <*(A * (1,1))*>, <*(A * (1,2))*>, <*(A * (1,3))*>*>

    proof

      

       A1: (A @ ) is Matrix of 3, 1, D by Th23;

       [1, 1] in ( Indices A) & [1, 2] in ( Indices A) & [1, 3] in ( Indices A) by MATRIX_0: 31;

      then ((A @ ) * (1,1)) = (A * (1,1)) & ((A @ ) * (2,1)) = (A * (1,2)) & ((A @ ) * (3,1)) = (A * (1,3)) by MATRIX_0:def 6;

      hence thesis by A1, Th27;

    end;

    theorem :: BKMODEL1:32

    ex d1, d2, d3 st A = <* <*d1, d2, d3*>*>

    proof

      A = <* <*(A * (1,1)), (A * (1,2)), (A * (1,3))*>*> by Th26;

      hence thesis;

    end;

    theorem :: BKMODEL1:33

    for p be FinSequence of (1 -tuples_on REAL ) st ( len p) = 3 holds ( ColVec2Mx ( M2F p)) = p

    proof

      let p be FinSequence of (1 -tuples_on REAL );

      assume

       A1: ( len p) = 3;

      then

       A2: ( M2F p) = <*((p . 1) . 1), ((p . 2) . 1), ((p . 3) . 1)*> by ANPROJ_8:def 2;

      then

       A3: ( len ( M2F p)) = 3 by FINSEQ_1: 45;

      

       A4: ( len ( M2F p)) > 0 by A2, FINSEQ_1: 45;

      

      then

       A5: ( len ( ColVec2Mx ( M2F p))) = ( len ( M2F p)) by MATRIXR1:def 9

      .= 3 by A2, FINSEQ_1: 45;

      ( width ( ColVec2Mx ( M2F p))) = 1 & ( ColVec2Mx ( M2F p)) is Matrix of REAL by A4, MATRIXR1:def 9;

      then

       A6: ( ColVec2Mx ( M2F p)) is Matrix of 3, 1, F_Real by A5, MATRIX_0: 20;

      set A = ( ColVec2Mx ( M2F p));

      A = <* <*(A * (1,1))*>, <*(A * (2,1))*>, <*(A * (3,1))*>*> by A6, Th27;

      then

       A7: (A . 1) = <*(A * (1,1))*> & (A . 2) = <*(A * (2,1))*> & (A . 3) = <*(A * (3,1))*> by FINSEQ_1: 45;

      ( dom ( M2F p)) = ( Seg 3) by A3, FINSEQ_1:def 3;

      then 1 in ( dom ( M2F p)) & 2 in ( dom ( M2F p)) & 3 in ( dom ( M2F p)) by FINSEQ_1: 1;

      then (A . 1) = <*(( M2F p) . 1)*> & (A . 2) = <*(( M2F p) . 2)*> & (A . 3) = <*(( M2F p) . 3)*> by A4, MATRIXR1:def 9;

      

      then A = <* <*(( M2F p) . 1)*>, <*(( M2F p) . 2)*>, <*(( M2F p) . 3)*>*> by A6, Th27, A7

      .= ( F2M ( M2F p)) by A3, ANPROJ_8:def 1

      .= p by A1, ANPROJ_8: 85;

      hence thesis;

    end;

    theorem :: BKMODEL1:34

    

     Th30: for M be Matrix of 3, F_Real holds for MR be Matrix of 3, REAL holds for v be Element of ( TOP-REAL 3) holds for uf be FinSequence of F_Real holds for ufr be FinSequence of REAL holds for p be FinSequence of (1 -tuples_on REAL ) st p = (M * uf) & v = ( M2F p) & ( len uf) = 3 & uf = ufr & MR = M holds v = (MR * ufr)

    proof

      let M be Matrix of 3, F_Real ;

      let MR be Matrix of 3, REAL ;

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

      let uf be FinSequence of F_Real ;

      let ufr be FinSequence of REAL ;

      let p be FinSequence of (1 -tuples_on REAL );

      assume that

       A1: p = (M * uf) and

       A2: v = ( M2F p) and

       A3: ( len uf) = 3 and

       A4: uf = ufr and

       A5: MR = M;

      consider a,b,c,d,e,f,g,h,i be Element of F_Real such that

       A6: M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*> by PASCAL: 3;

      uf is Element of ( REAL 3) by A3, EUCLID_8: 2;

      then uf in ( REAL 3);

      then uf in ( TOP-REAL 3) by EUCLID: 22;

      then

      consider t1,t2,t3 be Real such that

       A7: uf = <*t1, t2, t3*> by EUCLID_5: 1;

      reconsider x = t1, y = t2, z = t3 as Element of F_Real by XREAL_0:def 1;

      v = <*(((a * x) + (b * y)) + (c * z)), (((d * x) + (e * y)) + (f * z)), (((g * x) + (h * y)) + (i * z))*> by PASCAL: 8, A1, A2, A6, A7;

      hence thesis by A7, A4, A5, A6, PASCAL: 9;

    end;

    theorem :: BKMODEL1:35

    

     Th31: for N be Matrix of 3, REAL holds for uf be FinSequence of REAL st uf = ( 0. ( TOP-REAL 3)) holds (N * uf) = ( 0. ( TOP-REAL 3))

    proof

      let N be Matrix of 3, REAL ;

      let uf be FinSequence of REAL ;

      assume

       A1: uf = ( 0. ( TOP-REAL 3));

      reconsider M = N as Matrix of 3, F_Real ;

      consider n1,n2,n3,n4,n5,n6,n7,n8,n9 be Element of F_Real such that

       A2: M = <* <*n1, n2, n3*>, <*n4, n5, n6*>, <*n7, n8, n9*>*> by PASCAL: 3;

      reconsider r1 = n1, r2 = n2, r3 = n3, r4 = n4, r5 = n5, r6 = n6, r7 = n7, r8 = n8, r9 = n9 as Element of REAL ;

      reconsider z = ( 0. ( TOP-REAL 3)) as Element of ( TOP-REAL 3);

      reconsider p = <* 0 , 0 , 0 *> as FinSequence of REAL by EUCLID: 24, EUCLID_5: 4;

      reconsider z1 = (z `1 ), z2 = (z `2 ), z3 = (z `3 ) as Element of REAL by XREAL_0:def 1;

      z = <* 0 , 0 , 0 *> & z = <*z1, z2, z3*> by EUCLID_5: 3, EUCLID_5: 4;

      then

       A3: z1 = 0 & z2 = 0 & z3 = 0 by FINSEQ_1: 78;

       |[(z `1 ), (z `2 ), (z `3 )]| = p by EUCLID_5: 3, EUCLID_5: 4;

      

      then (N * uf) = <*(((r1 * z1) + (r2 * z2)) + (r3 * z3)), (((r4 * z1) + (r5 * z2)) + (r6 * z3)), (((r7 * z1) + (r8 * z2)) + (r9 * z3))*> by A2, A1, EUCLID_5: 4, PASCAL: 9

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

      hence thesis;

    end;

    theorem :: BKMODEL1:36

    

     Th32: for N be Matrix of 3, REAL holds for uf be FinSequence of REAL holds for u be Element of ( TOP-REAL 3) st N is invertible & u = uf & u is non zero holds (N * uf) <> ( 0. ( TOP-REAL 3))

    proof

      let N be Matrix of 3, REAL ;

      let uf be FinSequence of REAL ;

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

      assume

       A1: N is invertible & u = uf & u is non zero;

      then ( dom uf) = ( Seg 3) by FINSEQ_1: 89;

      then

       A2: ( len uf) = 3 by FINSEQ_1:def 3;

      assume

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

      

       A4: (( Inv N) * N) = ( 1_Rmatrix 3) & (( Inv N) * N) = ( 1_Rmatrix 3) by A1, MATRIXR2:def 6;

      ( width N) = 3 & ( len N) = 3 & ( width ( Inv N)) = 3 by MATRIX_0: 24;

      

      then (( Inv N) * (N * uf)) = ((( Inv N) * N) * uf) by A2, MATRIXR2: 59

      .= uf by A4, A2, MATRIXR2: 86;

      hence contradiction by A3, A1, Th31;

    end;

    theorem :: BKMODEL1:37

    for N be invertible Matrix of 3, F_Real holds for NR be Matrix of 3, REAL holds for P,Q be Element of ( ProjectiveSpace ( TOP-REAL 3)) holds for u,v be non zero Element of ( TOP-REAL 3) holds for vfr,ufr be FinSequence of REAL st P = ( Dir u) & Q = ( Dir v) & u = ufr & v = vfr & N = NR & (NR * ufr) = vfr holds (( homography N) . P) = Q

    proof

      let N be invertible Matrix of 3, F_Real ;

      let NR be Matrix of 3, REAL ;

      let P,Q be Element of ( ProjectiveSpace ( TOP-REAL 3));

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

      let vfr,ufr be FinSequence of REAL ;

      assume

       A1: P = ( Dir u) & Q = ( Dir v) & u = ufr & v = vfr & N = NR & (NR * ufr) = vfr;

      consider u1,v1 be Element of ( TOP-REAL 3), u1f be FinSequence of F_Real , p1 be FinSequence of (1 -tuples_on REAL ) such that

       A2: P = ( Dir u1) & not u1 is zero & u1 = u1f & p1 = (N * u1f) & v1 = ( M2F p1) & not v1 is zero & (( homography N) . P) = ( Dir v1) by ANPROJ_8:def 4;

      reconsider u1fr = u1f as FinSequence of REAL ;

      u1 in ( TOP-REAL 3);

      then u1 in ( REAL 3) by EUCLID: 22;

      then

       A3: ( len u1fr) = 3 by A2, EUCLID_8: 50;

      then

       A4: v1 = (NR * u1fr) by A1, A2, Th30;

       are_Prop (u,u1) by A1, A2, ANPROJ_1: 22;

      then

      consider a be Real such that

       A5: a <> 0 and

       A6: u = (a * u1) by ANPROJ_1: 1;

      

       A7: ( width NR) = 3 by MATRIX_0: 23;

      

       A8: ( width NR) = ( len u1fr) & ( len u1fr) > 0 by A3, MATRIX_0: 23;

      

       A9: ( len NR) = 3 by MATRIX_0: 24;

      u in ( TOP-REAL 3);

      then u in ( REAL 3) by EUCLID: 22;

      then ( width NR) = ( len ufr) & ( len ufr) > 0 by A7, A1, EUCLID_8: 50;

      then ( len (NR * ufr)) = 3 & ( len (NR * u1fr)) = 3 by A9, A3, MATRIX_0: 23, MATRIXR1: 61;

      then (NR * ufr) is Element of ( REAL 3) & (NR * u1fr) is Element of ( REAL 3) by EUCLID_8: 2;

      then

      reconsider w1 = (NR * ufr), w2 = (NR * u1fr) as Element of ( TOP-REAL 3) by EUCLID: 22;

      w1 = (a * w2) by A8, A1, A2, A6, MATRIXR1: 59;

      then are_Prop (w1,w2) by A5, ANPROJ_1: 1;

      hence thesis by A1, A2, A4, ANPROJ_1: 22;

    end;

    theorem :: BKMODEL1:38

    

     Th33: for N be invertible Matrix of 3, F_Real holds for NR be Matrix of 3, REAL holds for P,Q be Element of ( ProjectiveSpace ( TOP-REAL 3)) holds for u,v be non zero Element of ( TOP-REAL 3) holds for vfr,ufr be FinSequence of REAL holds for a be non zero Real st P = ( Dir u) & Q = ( Dir v) & u = ufr & v = vfr & N = NR & (NR * ufr) = (a * vfr) holds (( homography N) . P) = Q

    proof

      let N be invertible Matrix of 3, F_Real ;

      let NR be Matrix of 3, REAL ;

      let P,Q be Element of ( ProjectiveSpace ( TOP-REAL 3));

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

      let vfr,ufr be FinSequence of REAL ;

      let a be non zero Real;

      assume

       A1: P = ( Dir u) & Q = ( Dir v) & u = ufr & v = vfr & N = NR & (NR * ufr) = (a * vfr);

      

       A2: NR is invertible by A1, ANPROJ_8: 18;

      consider u1,v1 be Element of ( TOP-REAL 3), u1f be FinSequence of F_Real , p1 be FinSequence of (1 -tuples_on REAL ) such that

       A3: P = ( Dir u1) & not u1 is zero & u1 = u1f & p1 = (N * u1f) & v1 = ( M2F p1) & not v1 is zero & (( homography N) . P) = ( Dir v1) by ANPROJ_8:def 4;

      reconsider u1fr = u1f as FinSequence of REAL ;

      u1 in ( TOP-REAL 3);

      then

       A4: u1 in ( REAL 3) by EUCLID: 22;

      then

       A5: ( len u1fr) = 3 by A3, EUCLID_8: 50;

      then

       A6: v1 = (NR * u1fr) by A1, A3, Th30;

       are_Prop (u,u1) by A1, A3, ANPROJ_1: 22;

      then

      consider b be Real such that

       A7: b <> 0 and

       A8: u = (b * u1) by ANPROJ_1: 1;

      

       A9: ( width NR) = 3 by MATRIX_0: 23;

      then

       A10: ( width NR) = ( len u1fr) & ( len u1fr) > 0 by A4, A3, EUCLID_8: 50;

      

       A11: ( len NR) = 3 by MATRIX_0: 24;

      u in ( TOP-REAL 3);

      then u in ( REAL 3) by EUCLID: 22;

      then ( len ufr) = 3 by A1, EUCLID_8: 50;

      then ( len (NR * ufr)) = 3 & ( len (NR * u1fr)) = 3 by MATRIX_0: 23, A11, A10, MATRIXR1: 61;

      then (NR * ufr) is Element of ( REAL 3) & (NR * u1fr) is Element of ( REAL 3) by EUCLID_8: 2;

      then

      reconsider w1 = (NR * ufr), w2 = (NR * u1fr) as Element of ( TOP-REAL 3) by EUCLID: 22;

      

       A12: not w1 is zero & not w2 is zero by A1, A3, A2, Th32;

      w1 = (b * w2) by A1, A3, A8, A9, A5, MATRIXR1: 59;

      then are_Prop (w1,w2) by A7, ANPROJ_1: 1;

      then

       A13: ( Dir w1) = ( Dir w2) by A12, ANPROJ_1: 22;

      v in ( TOP-REAL 3);

      then v in ( REAL 3) by EUCLID: 22;

      then ( len vfr) = 3 by A1, EUCLID_8: 50;

      then ( len (a * vfr)) = 3 by RVSUM_1: 117;

      then (a * vfr) is Element of ( REAL 3) by EUCLID_8: 2;

      then

      reconsider avfr = (a * vfr) as Element of ( TOP-REAL 3) by EUCLID: 22;

      now

        thus not avfr is zero

        proof

          assume avfr is zero;

          then (a * v) = |[ 0 , 0 , 0 ]| by A1, EUCLID_5: 4;

          then |[(a * (v `1 )), (a * (v `2 )), (a * (v `3 ))]| = |[ 0 , 0 , 0 ]| by EUCLID_5: 7;

          then (v `1 ) = 0 & (v `2 ) = 0 & (v `3 ) = 0 by FINSEQ_1: 78;

          hence contradiction by EUCLID_5: 3, EUCLID_5: 4;

        end;

        thus not v is zero;

        a <> 0 & (a * v) = avfr by A1;

        hence are_Prop (avfr,v) by ANPROJ_1: 1;

      end;

      hence thesis by A1, A3, A6, A13, ANPROJ_1: 22;

    end;

    theorem :: BKMODEL1:39

    

     Th34: for p be FinSequence of REAL holds for M be Matrix of 3, REAL st ( len p) = 3 holds |((a * p), (M * (b * p)))| = ((a * b) * |(p, (M * p))|)

    proof

      let p be FinSequence of REAL ;

      let M be Matrix of 3, REAL ;

      assume

       A1: ( len p) = 3;

      

       A2: ( width M) = 3 & ( len M) = 3 by MATRIX_0: 23;

      

       A3: ( len (b * p)) = 3 by A1, RVSUM_1: 117;

      

       A4: p is Element of ( REAL 3) by A1, EUCLID_8: 2;

      

       A5: (p * M) = ( Line ((( LineVec2Mx p) * M),1)) by MATRIXR1:def 12;

      

       A6: ( width ( MXR2MXF ( LineVec2Mx p))) = ( width ( LineVec2Mx p)) by MATRIXR1:def 1

      .= ( len p) by MATRIXR1:def 10

      .= ( len ( MXR2MXF M)) by A1, MATRIX_0: 23;

      (( LineVec2Mx p) * M) = ( MXF2MXR (( MXR2MXF ( LineVec2Mx p)) * ( MXR2MXF M))) by MATRIXR1:def 6

      .= (( MXR2MXF ( LineVec2Mx p)) * ( MXR2MXF M)) by MATRIXR1:def 2;

      

      then ( width (( LineVec2Mx p) * M)) = ( width ( MXR2MXF M)) by A6, MATRIX_3:def 4

      .= ( width M) by MATRIXR1:def 1;

      then ( len ( Line ((( LineVec2Mx p) * M),1))) = ( width M) by MATRIX_0:def 7;

      then

       A7: (p * M) is Element of ( REAL 3) by A5, MATRIX_0: 23, EUCLID_8: 2;

      ( len (b * p)) > 0 by A1, RVSUM_1: 117;

      

      then

       A8: ( len ( ColVec2Mx (b * p))) = ( len (b * p)) by MATRIXR1:def 9

      .= 3 by A1, RVSUM_1: 117;

      

       A9: ( width ( MXR2MXF M)) = 3 by MATRIX_0: 23

      .= ( len ( MXR2MXF ( ColVec2Mx (b * p)))) by A8, MATRIXR1:def 1;

      ( len (M * (b * p))) = ( len ( Col ((M * ( ColVec2Mx (b * p))),1))) by MATRIXR1:def 11

      .= ( len (M * ( ColVec2Mx (b * p)))) by MATRIX_0:def 8

      .= ( len ( MXF2MXR (( MXR2MXF M) * ( MXR2MXF ( ColVec2Mx (b * p)))))) by MATRIXR1:def 6

      .= ( len (( MXR2MXF M) * ( MXR2MXF ( ColVec2Mx (b * p))))) by MATRIXR1:def 2

      .= ( len ( MXR2MXF M)) by A9, MATRIX_3:def 4

      .= 3 by MATRIX_0: 23;

      then (M * (b * p)) is Element of ( REAL 3) by EUCLID_8: 2;

      

      then |((a * p), (M * (b * p)))| = (a * |((M * (b * p)), p)|) by A4, EUCLID_4: 21

      .= (a * |((p * M), (b * p))|) by MATRPROB: 47, A2, A3, A1

      .= (a * (b * |(p, (p * M))|)) by EUCLID_4: 21, A4, A7

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

      .= ((a * b) * |((M * p), p)|) by A2, A1, MATRPROB: 47;

      hence thesis;

    end;

    theorem :: BKMODEL1:40

    

     Th35: for p be FinSequence of REAL holds for M be Matrix of 3, REAL st ( len p) = 3 holds ( SumAll ( QuadraticForm ((a * p),M,(b * p)))) = ((a * b) * ( SumAll ( QuadraticForm (p,M,p))))

    proof

      let p be FinSequence of REAL ;

      let M be Matrix of 3, REAL ;

      assume

       A1: ( len p) = 3;

      

       A2: ( len M) = 3 & ( width M) = 3 by MATRIX_0: 23;

      then

       A3: ( len (a * p)) = ( len M) by A1, RVSUM_1: 117;

      ( len (b * p)) = ( width M) & ( len (b * p)) > 0 by A1, A2, RVSUM_1: 117;

      then

       A4: ( SumAll ( QuadraticForm ((a * p),M,(b * p)))) = |((a * p), (M * (b * p)))| by A3, MATRPROB: 44;

      ( len p) = ( len M) & ( len p) = ( width M) & ( len p) > 0 by A1, MATRIX_0: 23;

      then ( SumAll ( QuadraticForm (p,M,p))) = |(p, (M * p))| by MATRPROB: 44;

      hence thesis by A4, A1, Th34;

    end;

    theorem :: BKMODEL1:41

    

     Th36: for a,b be Real holds |[a, b, 1]| is non zero by EUCLID_5: 4, FINSEQ_1: 78;

    theorem :: BKMODEL1:42

    for P be Element of ( TOP-REAL 2), Q be Element of ( TOP-REAL 2), r be Real holds P in ( Sphere (Q,r)) iff P in ( circle ((Q . 1),(Q . 2),r))

    proof

      let P be Element of ( TOP-REAL 2), Q be Element of ( TOP-REAL 2), r be Real;

      hereby

        assume P in ( Sphere (Q,r));

        then P in ( Sphere ( |[(Q `1 ), (Q `2 )]|,r)) by EUCLID: 53;

        then P in ( Sphere ( |[(Q . 1), (Q `2 )]|,r)) by EUCLID:def 9;

        then P in ( Sphere ( |[(Q . 1), (Q . 2)]|,r)) by EUCLID:def 10;

        hence P in ( circle ((Q . 1),(Q . 2),r)) by TOPREAL9: 52;

      end;

      assume P in ( circle ((Q . 1),(Q . 2),r));

      then P in ( Sphere ( |[(Q . 1), (Q . 2)]|,r)) by TOPREAL9: 52;

      then P in ( Sphere ( |[(Q `1 ), (Q . 2)]|,r)) by EUCLID:def 9;

      then P in ( Sphere ( |[(Q `1 ), (Q `2 )]|,r)) by EUCLID:def 10;

      hence thesis by EUCLID: 53;

    end;

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

    theorem :: BKMODEL1:43

    

     Th37: ( Dir u) = ( Dir v) & (u . 3) = (v . 3) & (v . 3) <> 0 implies u = v

    proof

      assume that

       A1: ( Dir u) = ( Dir v) and

       A2: (u . 3) = (v . 3) and

       A3: (v . 3) <> 0 ;

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

      then

      consider a be Real such that a <> 0 and

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

      reconsider b = (1 - a), c = (v . 3) as Real;

      

       A5: |[(u `1 ), (u `2 ), (u `3 )]| = (a * v) by A4, EUCLID_5: 3

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

      (v . 3) = (u `3 ) by A2, EUCLID_5:def 3

      .= (a * (v `3 )) by A5, FINSEQ_1: 78

      .= (a * (v . 3)) by EUCLID_5:def 3;

      then ((1 - a) * (v . 3)) = 0 & c = (v . 3);

      then b = 0 by A3;

      

      then u = |[(1 * (v `1 )), (1 * (v `2 )), (1 * (v `3 ))]| by A4, EUCLID_5: 7

      .= v by EUCLID_5: 3;

      hence thesis;

    end;

    definition

      :: BKMODEL1:def1

      func Dir101 -> Point of ( ProjectiveSpace ( TOP-REAL 3)) equals ( Dir |[1, 0 , 1]|);

      coherence

      proof

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

         not u is zero by EUCLID_5: 4, FINSEQ_1: 78;

        hence thesis by ANPROJ_1: 26;

      end;

    end

    definition

      :: BKMODEL1:def2

      func Dirm101 -> Point of ( ProjectiveSpace ( TOP-REAL 3)) equals ( Dir |[( - 1), 0 , 1]|);

      coherence

      proof

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

         not u is zero by EUCLID_5: 4, FINSEQ_1: 78;

        hence thesis by ANPROJ_1: 26;

      end;

    end

    definition

      :: BKMODEL1:def3

      func Dir011 -> Point of ( ProjectiveSpace ( TOP-REAL 3)) equals ( Dir |[ 0 , 1, 1]|);

      coherence

      proof

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

         not u is zero by EUCLID_5: 4, FINSEQ_1: 78;

        hence thesis by ANPROJ_1: 26;

      end;

    end

    theorem :: BKMODEL1:44

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

    proof

      thus not ( Dir101 , Dirm101 , Dir011 ) are_collinear

      proof

        assume

         A1: ( Dir101 , Dirm101 , Dir011 ) are_collinear ;

        set p = |[1, 0 , 1]|, q = |[( - 1), 0 , 1]|, r = |[ 0 , 1, 1]|;

        

         A2: (p `1 ) = 1 & (p `2 ) = 0 & (p `3 ) = 1 & (q `1 ) = ( - 1) & (q `2 ) = 0 & (q `3 ) = 1 & (r `1 ) = 0 & (r `2 ) = 1 & (r `3 ) = 1 by EUCLID_5: 2;

        p is non zero & q is non zero & r is non zero by EUCLID_5: 4, FINSEQ_1: 78;

        

        then 0 = |{p, q, r}| by A1, Th01

        .= (((((((1 * 0 ) * 1) - ((1 * 0 ) * 0 )) - ((1 * 1) * 1)) + (( 0 * 1) * 0 )) - (( 0 * ( - 1)) * 1)) + ((1 * ( - 1)) * 1)) by A2, ANPROJ_8: 27

        .= ( - 2);

        hence contradiction;

      end;

      thus not ( Dir101 , Dirm101 , Dir010 ) are_collinear

      proof

        assume

         A3: ( Dir101 , Dirm101 , Dir010 ) are_collinear ;

        set p = |[1, 0 , 1]|, q = |[( - 1), 0 , 1]|, r = |[ 0 , 1, 0 ]|;

        

         A4: (p `1 ) = 1 & (p `2 ) = 0 & (p `3 ) = 1 & (q `1 ) = ( - 1) & (q `2 ) = 0 & (q `3 ) = 1 & (r `1 ) = 0 & (r `2 ) = 1 & (r `3 ) = 0 by EUCLID_5: 2;

        p is non zero & q is non zero & r is non zero by EUCLID_5: 4, FINSEQ_1: 78;

        

        then 0 = |{p, q, r}| by A3, ANPROJ_9:def 6, Th01

        .= (((((((1 * 0 ) * 0 ) - ((1 * 0 ) * 0 )) - ((1 * 1) * 1)) + (( 0 * 1) * 0 )) - (( 0 * ( - 1)) * 0 )) + ((1 * ( - 1)) * 1)) by A4, ANPROJ_8: 27

        .= ( - 2);

        hence contradiction;

      end;

      thus not ( Dir101 , Dir011 , Dir010 ) are_collinear

      proof

        assume

         A5: ( Dir101 , Dir011 , Dir010 ) are_collinear ;

        set p = |[1, 0 , 1]|, q = |[ 0 , 1, 1]|, r = |[ 0 , 1, 0 ]|;

        

         A6: (p `1 ) = 1 & (p `2 ) = 0 & (p `3 ) = 1 & (q `1 ) = 0 & (q `2 ) = 1 & (q `3 ) = 1 & (r `1 ) = 0 & (r `2 ) = 1 & (r `3 ) = 0 by EUCLID_5: 2;

        p is non zero & q is non zero & r is non zero by EUCLID_5: 4, FINSEQ_1: 78;

        

        then 0 = |{p, q, r}| by A5, ANPROJ_9:def 6, Th01

        .= ((((((((p `1 ) * (q `2 )) * (r `3 )) - (((p `3 ) * (q `2 )) * (r `1 ))) - (((p `1 ) * (q `3 )) * (r `2 ))) + (((p `2 ) * (q `3 )) * (r `1 ))) - (((p `2 ) * (q `1 )) * (r `3 ))) + (((p `3 ) * (q `1 )) * (r `2 ))) by ANPROJ_8: 27

        .= ( - 1) by A6;

        hence contradiction;

      end;

      thus not ( Dirm101 , Dir011 , Dir010 ) are_collinear

      proof

        assume

         A7: ( Dirm101 , Dir011 , Dir010 ) are_collinear ;

        set p = |[( - 1), 0 , 1]|, q = |[ 0 , 1, 1]|, r = |[ 0 , 1, 0 ]|;

        

         A8: (p `1 ) = ( - 1) & (p `2 ) = 0 & (p `3 ) = 1 & (q `1 ) = 0 & (q `2 ) = 1 & (q `3 ) = 1 & (r `1 ) = 0 & (r `2 ) = 1 & (r `3 ) = 0 by EUCLID_5: 2;

        p is non zero & q is non zero & r is non zero by EUCLID_5: 4, FINSEQ_1: 78;

        

        then 0 = |{p, q, r}| by A7, ANPROJ_9:def 6, Th01

        .= ((((((((p `1 ) * (q `2 )) * (r `3 )) - (((p `3 ) * (q `2 )) * (r `1 ))) - (((p `1 ) * (q `3 )) * (r `2 ))) + (((p `2 ) * (q `3 )) * (r `1 ))) - (((p `2 ) * (q `1 )) * (r `3 ))) + (((p `3 ) * (q `1 )) * (r `2 ))) by ANPROJ_8: 27

        .= 1 by A8;

        hence contradiction;

      end;

    end;

    theorem :: BKMODEL1:45

    ( symmetric_3 (1,1,1, 0 , 0 , 0 )) = ( 1. ( F_Real ,3)) by PASCAL:def 3, ANPROJ_9: 1;

    theorem :: BKMODEL1:46

    

     Th39: for r,a,b,c,d,e,f,g,h,i be Element of F_Real holds for M be Matrix of 3, F_Real st M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*> holds (r * M) = <* <*(r * a), (r * b), (r * c)*>, <*(r * d), (r * e), (r * f)*>, <*(r * g), (r * h), (r * i)*>*>

    proof

      let r,a,b,c,d,e,f,g,h,i be Element of F_Real ;

      let M be Matrix of 3, F_Real ;

      assume

       A1: M = <* <*a, b, c*>, <*d, e, f*>, <*g, h, i*>*>;

      ( len M) = 3 & ( width M) = 3 by MATRIX_0: 23;

      then ( len (r * M)) = 3 & ( width (r * M)) = 3 by MATRIX_3:def 5;

      then

       A2: (r * M) is Matrix of 3, 3, F_Real by MATRIX_0: 20;

      

       A3: ( Indices M) = [:( Seg 3), ( Seg 3):] by MATRIX_0: 23;

      reconsider b11 = ((r * M) * (1,1)), b12 = ((r * M) * (1,2)), b13 = ((r * M) * (1,3)), b21 = ((r * M) * (2,1)), b22 = ((r * M) * (2,2)), b23 = ((r * M) * (2,3)), b31 = ((r * M) * (3,1)), b32 = ((r * M) * (3,2)), b33 = ((r * M) * (3,3)) as Element of F_Real ;

      M = <* <*(M * (1,1)), (M * (1,2)), (M * (1,3))*>, <*(M * (2,1)), (M * (2,2)), (M * (2,3))*>, <*(M * (3,1)), (M * (3,2)), (M * (3,3))*>*> by MATRIXR2: 37;

      then

       A4: a = (M * (1,1)) & b = (M * (1,2)) & c = (M * (1,3)) & d = (M * (2,1)) & e = (M * (2,2)) & f = (M * (2,3)) & g = (M * (3,1)) & h = (M * (3,2)) & i = (M * (3,3)) by A1, PASCAL: 2;

      b11 = (r * (M * (1,1))) & b12 = (r * (M * (1,2))) & b13 = (r * (M * (1,3))) & b21 = (r * (M * (2,1))) & b22 = (r * (M * (2,2))) & b23 = (r * (M * (2,3))) & b31 = (r * (M * (3,1))) & b32 = (r * (M * (3,2))) & b33 = (r * (M * (3,3))) by A3, ANPROJ_8: 1, MATRIX_3:def 5;

      hence thesis by A4, A2, MATRIXR2: 37;

    end;

    theorem :: BKMODEL1:47

    

     Th40: for a be Real holds for ra2 be Element of F_Real st ra2 = (a * a) holds (( symmetric_3 (a,a,( - a), 0 , 0 , 0 )) * ( symmetric_3 (a,a,( - a), 0 , 0 , 0 ))) = (ra2 * ( 1. ( F_Real ,3)))

    proof

      let a be Real;

      let ra2 be Element of F_Real ;

      assume

       A1: ra2 = (a * a);

      reconsider zone = 1, z1 = 0 , z2 = a, z3 = ( - a) as Element of F_Real by XREAL_0:def 1;

      ( symmetric_3 (a,a,( - a), 0 , 0 , 0 )) = <* <*z2, z1, z1*>, <*z1, z2, z1*>, <*z1, z1, z3*>*> by PASCAL:def 3;

      

      then (( symmetric_3 (a,a,( - a), 0 , 0 , 0 )) * ( symmetric_3 (a,a,( - a), 0 , 0 , 0 ))) = <* <*(((z2 * z2) + (z1 * z1)) + (z1 * z1)), (((z2 * z1) + (z1 * z2)) + (z1 * z1)), (((z2 * z1) + (z1 * z1)) + (z1 * z3))*>, <*(((z1 * z2) + (z2 * z1)) + (z1 * z1)), (((z1 * z1) + (z2 * z2)) + (z1 * z1)), (((z1 * z1) + (z2 * z1)) + (z1 * z3))*>, <*(((z1 * z2) + (z1 * z1)) + (z3 * z1)), (((z1 * z1) + (z1 * z2)) + (z3 * z1)), (((z1 * z1) + (z1 * z1)) + (z3 * z3))*>*> by ANPROJ_9: 6

      .= <* <*(ra2 * zone), (ra2 * z1), (ra2 * z1)*>, <*(ra2 * z1), (ra2 * zone), (ra2 * z1)*>, <*(ra2 * z1), (ra2 * z1), (ra2 * zone)*>*> by A1

      .= (ra2 * ( 1. ( F_Real ,3))) by Th39, ANPROJ_9: 1;

      hence thesis;

    end;

    theorem :: BKMODEL1:48

    

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

    proof

      let a be non zero Real;

      reconsider z1 = 0 , z2 = a, z3 = ( - a) as Element of F_Real by XREAL_0:def 1;

      

       A1: ( symmetric_3 (a,a,( - a), 0 , 0 , 0 )) = <* <*z2, z1, z1*>, <*z1, z2, z1*>, <*z1, z1, z3*>*> by PASCAL:def 3;

      

       A2: (z2 * (1 / z2)) = 1 & (z3 * (1 / z3)) = 1 by XCMPLX_1: 106;

      reconsider y1 = z1, y2 = (1 / z2), y3 = (1 / z3) as Element of F_Real by XREAL_0:def 1;

      

       A3: ( symmetric_3 (y2,y2,y3,y1,y1,y1)) = <* <*(1 / z2), z1, z1*>, <*z1, (1 / z2), z1*>, <*z1, z1, (1 / z3)*>*> by PASCAL:def 3;

      (( symmetric_3 (a,a,( - a), 0 , 0 , 0 )) * ( symmetric_3 ((1 / a),(1 / a),( - (1 / a)), 0 , 0 , 0 ))) = (( symmetric_3 (z2,z2,z3,z1,z1,z1)) * ( symmetric_3 (y2,y2,y3,y1,y1,y1))) by XCMPLX_1: 188

      .= <* <*(((z2 * y2) + (z1 * y1)) + (z1 * y1)), (((z2 * y1) + (z1 * y2)) + (z1 * y1)), (((z2 * y1) + (z1 * y1)) + (z1 * y3))*>, <*(((z1 * y2) + (z2 * y1)) + (z1 * y1)), (((z1 * y1) + (z2 * y2)) + (z1 * y1)), (((z1 * y1) + (z2 * y1)) + (z1 * y3))*>, <*(((z1 * y2) + (z1 * y1)) + (z3 * y1)), (((z1 * y1) + (z1 * y2)) + (z3 * y1)), (((z1 * y1) + (z1 * y1)) + (z3 * y3))*>*> by A1, A3, ANPROJ_9: 6

      .= <* <*1, 0 , 0 *>, <* 0 , 1, 0 *>, <* 0 , 0 , 1*>*> by A2;

      hence thesis by ANPROJ_9: 1;

    end;

    theorem :: BKMODEL1:49

    

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

    proof

      let a be non zero Real;

      reconsider b = (1 / a) as non zero Real;

      (1 / b) = a by XCMPLX_1: 56;

      hence thesis by Th41;

    end;

    theorem :: BKMODEL1:50

    

     Th43: (( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) * ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 ))) = ( 1. ( F_Real ,3))

    proof

      reconsider a = 1 as non zero Real;

      ( - (1 / a)) = ( - 1);

      hence thesis by Th41;

    end;

    theorem :: BKMODEL1:51

    for a be non zero Real holds for N be Matrix of 3, F_Real st N = ( symmetric_3 (a,a,( - a), 0 , 0 , 0 )) holds N is invertible

    proof

      let a be non zero Real;

      let N be Matrix of 3, F_Real ;

      assume

       A1: N = ( symmetric_3 (a,a,( - a), 0 , 0 , 0 ));

      (( symmetric_3 (a,a,( - a), 0 , 0 , 0 )) * ( symmetric_3 ((1 / a),(1 / a),( - (1 / a)), 0 , 0 , 0 ))) = ( 1. ( F_Real ,3)) & (( symmetric_3 ((1 / a),(1 / a),( - (1 / a)), 0 , 0 , 0 )) * ( symmetric_3 (a,a,( - a), 0 , 0 , 0 ))) = ( 1. ( F_Real ,3)) by Th41, Th42;

      hence thesis by A1, MATRIX_6:def 2, MATRIX_6:def 3;

    end;

    theorem :: BKMODEL1:52

    

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

    proof

      

       A1: ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) is_reverse_of ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) by Th43, MATRIX_6:def 2;

      thus ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) is invertible Matrix of 3, F_Real by Th43, MATRIX_6:def 2, MATRIX_6:def 3;

      hence (( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) ~ ) = ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) by A1, MATRIX_6:def 4;

    end;

    theorem :: BKMODEL1:53

    for N be invertible Matrix of 3, F_Real holds for N1 be Matrix of 3, F_Real holds for M,NR be Matrix of 3, REAL st M = ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) & N1 = M & NR = ( MXF2MXR (N ~ )) holds (((N @ ) * N1) * N) = ((( MXF2MXR (( MXR2MXF (NR @ )) ~ )) * M) * ( MXF2MXR (( MXR2MXF NR) ~ )))

    proof

      let N be invertible Matrix of 3, F_Real ;

      let N1 be Matrix of 3, F_Real ;

      let M,NR be Matrix of 3, REAL ;

      assume that

       A1: M = ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) and

       A2: N1 = M and

       A3: NR = ( MXF2MXR (N ~ ));

      reconsider b = ( - 1) as Element of F_Real by XREAL_0:def 1;

      

       A4: b is non zero;

      reconsider a = 1 as Element of F_Real ;

      a is non zero;

      then

      reconsider a = 1, b = ( - 1) as non zero Element of F_Real by A4;

      reconsider N1 as invertible Matrix of 3, F_Real by A1, A2, Th44;

      reconsider M1 = (((N @ ) * N1) * N) as invertible Matrix of 3, F_Real ;

      reconsider N2 = N1 as Matrix of 3, REAL ;

      

       A6: ( MXF2MXR (( MXR2MXF NR) ~ )) = (( MXR2MXF NR) ~ ) by MATRIXR1:def 2

      .= ((N ~ ) ~ ) by A3, ANPROJ_8: 16

      .= N by MATRIX_6: 16;

      

       A7: ( MXF2MXR (( MXR2MXF (NR @ )) ~ )) = (N @ )

      proof

        

         A8: ( MXF2MXR (( MXR2MXF (NR @ )) ~ )) = (( MXR2MXF (NR @ )) ~ ) by MATRIXR1:def 2;

        ( MXR2MXF (NR @ )) = (NR @ ) by MATRIXR1:def 1;

        

        then ( MXF2MXR (( MXR2MXF (NR @ )) ~ )) = (((N ~ ) @ ) ~ ) by A8, A3, MATRIXR1:def 2

        .= (((N @ ) ~ ) ~ ) by MATRIX_6: 13;

        hence thesis by MATRIX_6: 16;

      end;

      ((N @ ) * N1) = (( MXF2MXR (( MXR2MXF (NR @ )) ~ )) * N2) by A7, ANPROJ_8: 17;

      hence thesis by A2, A6, ANPROJ_8: 17;

    end;

    theorem :: BKMODEL1:54

    

     Th46: for n be Nat holds for a be Element of F_Real holds for ra be Real holds for A be Matrix of n, F_Real holds for rA be Matrix of n, REAL st a = ra & A = rA holds (a * A) = (ra * rA)

    proof

      let n be Nat;

      let a be Element of F_Real ;

      let ra be Real;

      let A be Matrix of n, F_Real ;

      let rA be Matrix of n, REAL ;

      assume that

       A1: a = ra and

       A2: A = rA;

      (ra * rA) = ( MXF2MXR (a * ( MXR2MXF rA))) by A1, MATRIXR1:def 7

      .= ( MXF2MXR (a * A)) by A2, MATRIXR1:def 1;

      hence thesis by MATRIXR1:def 2;

    end;

    theorem :: BKMODEL1:55

    

     Th47: for n be Nat holds for a be Element of F_Real holds for A,B be Matrix of n, F_Real st n > 0 holds ((a * A) * B) = (a * (A * B))

    proof

      let n be Nat;

      let a be Element of F_Real ;

      let A,B be Matrix of n, F_Real ;

      assume

       A1: n > 0 ;

      

       A2: ( width A) = n & ( len A) = n & ( width B) = n & ( len B) = n by MATRIX_0: 24;

      reconsider ra = a as Real;

      reconsider rA = A, rB = B as Matrix of n, REAL ;

      

       A3: (rA * rB) = (A * B) by ANPROJ_8: 17;

      (a * A) = (ra * rA) by Th46;

      

      then ((a * A) * B) = ((ra * rA) * rB) by ANPROJ_8: 17

      .= (ra * (rA * rB)) by A2, A1, MATRIXR1: 41

      .= (a * (A * B)) by A3, Th46;

      hence thesis;

    end;

    theorem :: BKMODEL1:56

    

     Th48: ( symmetric_3 (a,a,( - a), 0 , 0 , 0 )) = (a * ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )))

    proof

      reconsider z0 = 0 , z1 = 1, z2 = ( - 1) as Element of F_Real by XREAL_0:def 1;

      ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) = <* <*z1, z0, z0*>, <*z0, z1, z0*>, <*z0, z0, z2*>*> by PASCAL:def 3;

      then (a * ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 ))) = <* <*(a * z1), (a * z0), (a * z0)*>, <*(a * z0), (a * z1), (a * z0)*>, <*(a * z0), (a * z0), (a * z2)*>*> by Th39;

      hence thesis by PASCAL:def 3;

    end;

    theorem :: BKMODEL1:57

    

     Th49: M = ( symmetric_3 (a,a,( - a), 0 , 0 , 0 )) implies ((M * M) * M) = (((a * a) * a) * ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )))

    proof

      assume

       A1: M = ( symmetric_3 (a,a,( - a), 0 , 0 , 0 ));

      reconsider ra2 = (a * a) as Element of F_Real ;

      ((M * M) * M) = ((ra2 * ( 1. ( F_Real ,3))) * M) by A1, Th40

      .= (ra2 * (( 1. ( F_Real ,3)) * M)) by Th47

      .= (ra2 * M) by MATRIX_3: 18

      .= (ra2 * (a * ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )))) by A1, Th48

      .= (((a * a) * a) * ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 ))) by MATRIX_5: 11;

      hence thesis;

    end;

    theorem :: BKMODEL1:58

    

     Th50: for n be Nat holds for a be Real holds for M be Matrix of n, REAL holds for x be FinSequence of REAL st n > 0 & ( len x) = n holds (M * (a * x)) = ((a * M) * x)

    proof

      let n be Nat;

      let a be Real;

      let M be Matrix of n, REAL ;

      let x be FinSequence of REAL ;

      assume that

       A1: n > 0 and

       A2: ( len x) = n;

      ( width M) = n & ( len M) = n by MATRIX_0: 24;

      then

       A3: ( width M) = ( len ( ColVec2Mx x)) & ( len M) > 0 & ( len ( ColVec2Mx x)) > 0 & ( width ( ColVec2Mx x)) > 0 by A1, A2, MATRIXR1:def 9;

      ((a * M) * x) = ( Col (((a * M) * ( ColVec2Mx x)),1)) by MATRIXR1:def 11

      .= ( Col ((a * (M * ( ColVec2Mx x))),1)) by A3, MATRIXR1: 41

      .= ( Col ((M * (a * ( ColVec2Mx x))),1)) by A3, MATRIXR1: 40

      .= ( Col ((M * ( ColVec2Mx (a * x))),1)) by A1, A2, MATRIXR1: 47

      .= (M * (a * x)) by MATRIXR1:def 11;

      hence thesis;

    end;

    theorem :: BKMODEL1:59

    

     Th51: for n be Nat holds for a be Real holds for M be Matrix of n, REAL holds for x be FinSequence of REAL st n > 0 & ( len x) = n holds (a * (M * x)) = ((a * M) * x)

    proof

      let n be Nat;

      let a be Real;

      let M be Matrix of n, REAL ;

      let x be FinSequence of REAL ;

      assume that

       A1: n > 0 and

       A2: ( len x) = n;

      ( width M) = n by MATRIX_0: 24;

      then (M * (a * x)) = (a * (M * x)) by A1, A2, MATRIXR1: 59;

      hence thesis by A1, A2, Th50;

    end;

    theorem :: BKMODEL1:60

    

     Th52: for n be Nat holds for N be Matrix of n, REAL st N is invertible holds (N @ ) is invertible & ( Inv (N @ )) = (( Inv N) @ )

    proof

      let n be Nat;

      let N be Matrix of n, REAL ;

      assume

       A1: N is invertible;

      

      then ((N * ( Inv N)) @ ) = (( 1_Rmatrix n) @ ) by MATRIXR2:def 6

      .= ( 1_Rmatrix n) by MATRIXR2: 64;

      then

       A2: ((( Inv N) @ ) * (N @ )) = ( 1_Rmatrix n) by MATRIXR2: 30;

      ((( Inv N) * N) @ ) = (( 1_Rmatrix n) @ ) by A1, MATRIXR2:def 6

      .= ( 1_Rmatrix n) by MATRIXR2: 64;

      then

       A3: ((N @ ) * (( Inv N) @ )) = ( 1_Rmatrix n) by MATRIXR2: 30;

      then (N @ ) is invertible by A2, MATRIXR2:def 5;

      hence thesis by A2, A3, MATRIXR2:def 6;

    end;

    theorem :: BKMODEL1:61

    

     Th53: for ra be non zero Real holds for N,O,M be Matrix of 3, 3, REAL st N is invertible & M = (ra * O) & M = (((N @ ) * O) * N) holds (((( Inv N) @ ) * O) * ( Inv N)) = ((1 / ra) * O)

    proof

      let ra be non zero Real;

      let N,O,M be Matrix of 3, 3, REAL ;

      assume that

       A1: N is invertible and

       A3: M = (ra * O) and

       A4: M = (((N @ ) * O) * N);

      reconsider NI = ( Inv N), NIT = (( Inv N) @ ) as Matrix of 3, 3, REAL ;

      

       A5: (( Inv N) @ ) = ( Inv (N @ )) & (N @ ) is invertible by A1, Th52;

      

       A6: ( len NI) = 3 & ( width NI) = 3 & ( width (O * N)) = 3 & ( len (O * N)) = 3 by MATRIX_0: 24;

      reconsider ira = (1 / ra) as Real;

      reconsider NTON = (((N @ ) * O) * N) as Matrix of REAL ;

      

       A7: ( len NTON) = 3 by MATRIX_0: 24;

      

       A8: ( width (NI @ )) = 3 by MATRIX_0: 24;

      O = (1 * O) by MATRIXR1: 32

      .= (((1 / ra) * ra) * O) by XCMPLX_1: 87

      .= (ira * (((N @ ) * O) * N)) by A3, A4, MATRIXR2: 11;

      

      then (((NI @ ) * O) * NI) = ((ira * ((NI @ ) * (((N @ ) * O) * N))) * NI) by A8, A7, MATRIXR1: 40

      .= ((ira * (NIT * ((N @ ) * (O * N)))) * NI) by MATRIXR2: 27

      .= ((ira * ((NIT * (N @ )) * (O * N))) * NI) by MATRIXR2: 27

      .= ((ira * (( 1_Rmatrix 3) * (O * N))) * NI) by A5, MATRIXR2:def 6

      .= ((ira * (O * N)) * NI) by MATRIXR2: 70

      .= (ira * ((O * N) * NI)) by A6, MATRIXR1: 41

      .= (ira * (O * (N * NI))) by MATRIXR2: 27

      .= (ira * (O * ( 1_Rmatrix 3))) by A1, MATRIXR2:def 6

      .= (ira * O) by MATRIXR2: 71;

      hence thesis;

    end;

    theorem :: BKMODEL1:62

    

     Th54: for ra be Real holds for M,N be Matrix of 3, F_Real holds for MR,NR be Matrix of 3, REAL st MR = M & NR = N & N is symmetric & MR = (ra * NR) holds M is symmetric

    proof

      let ra be Real;

      let M,N be Matrix of 3, F_Real ;

      let MR,NR be Matrix of 3, REAL ;

      assume that

       A1: MR = M & NR = N and

       A2: N is symmetric and

       A3: MR = (ra * NR);

      ( width NR) > 0 by MATRIX_0: 23;

      

      then (M @ ) = (ra * (NR @ )) by A1, A3, MATRIXR1: 30

      .= M by A1, A2, A3, MATRIX_6:def 5;

      hence thesis by MATRIX_6:def 5;

    end;

    theorem :: BKMODEL1:63

    

     Th55: for ra be Real holds for O,M be Matrix of 3, REAL st O = ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) & M = (ra * O) holds (O * M) = (ra * ( 1_Rmatrix 3)) & (M * O) = (ra * ( 1_Rmatrix 3))

    proof

      let ra be Real;

      let O,M be Matrix of 3, REAL ;

      assume that

       A1: O = ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) and

       A2: M = (ra * O);

      ( 1_Rmatrix 3) = ( MXF2MXR ( 1. ( F_Real ,3))) by MATRIXR2:def 2;

      then

       A3: ( MXR2MXF ( 1_Rmatrix 3)) = ( 1. ( F_Real ,3)) by ANPROJ_8: 16;

      

       A4: (O * O) = (( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) * ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 ))) by A1, ANPROJ_8: 17

      .= ( 1_Rmatrix 3) by Th43, A3, MATRIXR1:def 1;

      ( len O) = 3 & ( width O) = 3 by MATRIX_0: 23;

      hence thesis by A4, A2, MATRIXR1: 40, MATRIXR1: 41;

    end;

    theorem :: BKMODEL1:64

    for ra be Real holds for O,M be Matrix of 3, REAL st O = ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) & M = (ra * O) holds (((((M @ ) * O) @ ) * O) * ((M @ ) * O)) = ((ra ^2 ) * O)

    proof

      let ra be Real;

      let O,M be Matrix of 3, REAL ;

      assume that

       A1: O = ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) and

       A2: M = (ra * O);

      reconsider O1 = O as Matrix of 3, F_Real ;

      

       A3: (O @ ) = O by A1, PASCAL: 12, MATRIX_6:def 5;

      reconsider MR = M as Matrix of 3, F_Real ;

      

       A4: MR is symmetric by Th54, A2, A1, PASCAL: 12;

      

       A5: (((ra * ( 1_Rmatrix 3)) * O) * (ra * ( 1_Rmatrix 3))) = ((ra ^2 ) * O)

      proof

        reconsider z1 = 1, z2 = ( - 1), z3 = 0 as Element of F_Real by XREAL_0:def 1;

        

         A6: O = <* <*z1, z3, z3*>, <*z3, z1, z3*>, <*z3, z3, z2*>*> by A1, PASCAL:def 3;

        reconsider ea = ra as Element of F_Real by XREAL_0:def 1;

        

         A7: (ra * ( 1_Rmatrix 3)) = ( MXF2MXR (ea * ( MXR2MXF ( 1_Rmatrix 3)))) by MATRIXR1:def 7

        .= ( MXF2MXR (ea * ( MXR2MXF ( MXF2MXR ( 1. ( F_Real ,3)))))) by MATRIXR2:def 2

        .= ( MXF2MXR (ea * ( 1. ( F_Real ,3)))) by ANPROJ_8: 16

        .= (ea * ( 1. ( F_Real ,3))) by MATRIXR1:def 2

        .= <* <*(ea * z1), (ea * z3), (ea * z3)*>, <*(ea * z3), (ea * z1), (ea * z3)*>, <*(ea * z3), (ea * z3), (ea * z1)*>*> by ANPROJ_9: 1, Th39

        .= <* <*ea, z3, z3*>, <*z3, ea, z3*>, <*z3, z3, ea*>*>;

        then

        reconsider RA1R = (ra * ( 1_Rmatrix 3)) as Matrix of 3, F_Real by ANPROJ_8: 19;

        reconsider ea2 = (ra * ra) as Element of F_Real by XREAL_0:def 1;

        reconsider z4 = (ea * z2) as Element of F_Real ;

        

         A8: (RA1R * O1) = <* <*(((ea * z1) + (z3 * z3)) + (z3 * z3)), (((ea * z3) + (z3 * z1)) + (z3 * z3)), (((ea * z3) + (z3 * z3)) + (z3 * z2))*>, <*(((z3 * z1) + (ea * z3)) + (z3 * z3)), (((z3 * z3) + (ea * z1)) + (z3 * z3)), (((z3 * z3) + (ea * z3)) + (z3 * z2))*>, <*(((z3 * z1) + (z3 * z3)) + (ea * z3)), (((z3 * z3) + (z3 * z1)) + (ea * z3)), (((z3 * z3) + (z3 * z3)) + (ea * z2))*>*> by A7, A6, ANPROJ_9: 6

        .= <* <*ea, z3, z3*>, <*z3, ea, z3*>, <*z3, z3, z4*>*>;

        

         A9: ((RA1R * O1) * RA1R) = <* <*(((ea * ea) + (z3 * z3)) + (z3 * z3)), (((ea * z3) + (z3 * ea)) + (z3 * z3)), (((ea * z3) + (z3 * z3)) + (z3 * ea))*>, <*(((z3 * ea) + (ea * z3)) + (z3 * z3)), (((z3 * z3) + (ea * ea)) + (z3 * z3)), (((z3 * z3) + (ea * z3)) + (z3 * ea))*>, <*(((z3 * ea) + (z3 * z3)) + (z4 * z3)), (((z3 * z3) + (z3 * ea)) + (z4 * z3)), (((z3 * z3) + (z3 * z3)) + (z4 * ea))*>*> by A8, A7, ANPROJ_9: 6

        .= <* <*(ea * ea), z3, z3*>, <*z3, (ea * ea), z3*>, <*z3, z3, (z4 * ea)*>*>;

        

         A10: ((ra * ( 1_Rmatrix 3)) * O) = (RA1R * O1) by ANPROJ_8: 17;

        ((ra ^2 ) * O) = ( MXF2MXR (ea2 * ( MXR2MXF O))) by MATRIXR1:def 7

        .= (ea2 * ( MXR2MXF O)) by MATRIXR1:def 2

        .= <* <*(ea2 * z1), (ea2 * z3), (ea2 * z3)*>, <*(ea2 * z3), (ea2 * z1), (ea2 * z3)*>, <*(ea2 * z3), (ea2 * z3), (ea2 * z2)*>*> by A6, Th39, MATRIXR1:def 1;

        hence thesis by A10, A9, ANPROJ_8: 17;

      end;

      (((((M @ ) * O) @ ) * O) * ((M @ ) * O)) = ((((M * O) @ ) * O) * ((M @ ) * O)) by A4, MATRIX_6:def 5

      .= ((((M * O) @ ) * O) * (M * O)) by A4, MATRIX_6:def 5

      .= ((((O @ ) * (M @ )) * O) * (M * O)) by MATRIXR2: 30

      .= (((O * M) * O) * (M * O)) by A3, A4, MATRIX_6:def 5

      .= (((ra * ( 1_Rmatrix 3)) * O) * (M * O)) by A1, A2, Th55

      .= ((ra ^2 ) * O) by A1, A2, A5, Th55;

      hence thesis;

    end;

    theorem :: BKMODEL1:65

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

    proof

      let O,N be Matrix of 3, REAL ;

      (((((N @ ) * O) @ ) * O) * ((N @ ) * O)) = ((((O @ ) * ((N @ ) @ )) * O) * ((N @ ) * O)) by MATRIXR2: 30

      .= ((((O @ ) * N) * O) * ((N @ ) * O)) by MATRIXR2: 29

      .= (((O @ ) * (N * O)) * ((N @ ) * O)) by MATRIXR2: 27

      .= ((O @ ) * ((N * O) * ((N @ ) * O))) by MATRIXR2: 27

      .= ((O @ ) * (((N * O) * (N @ )) * O)) by MATRIXR2: 27;

      hence thesis by MATRIXR2: 27;

    end;

    theorem :: BKMODEL1:66

    for NR,MR be Matrix of 3, REAL holds for p1,p2,p3 be FinSequence of REAL st p1 = <*1, 0 , 0 *> & p2 = <* 0 , 1, 0 *> & p3 = <* 0 , 0 , 1*> & (NR * p1) = (MR * p1) & (NR * p2) = (MR * p2) & (NR * p3) = (MR * p3) holds NR = MR

    proof

      let NR,MR be Matrix of 3, REAL ;

      let p1,p2,p3 be FinSequence of REAL ;

      assume that

       A1: p1 = <*1, 0 , 0 *> & p2 = <* 0 , 1, 0 *> & p3 = <* 0 , 0 , 1*> and

       A2: (NR * p1) = (MR * p1) and

       A3: (NR * p2) = (MR * p2) and

       A4: (NR * p3) = (MR * p3);

      reconsider N = NR, M = MR as Matrix of 3, F_Real ;

      consider n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real such that

       A5: N = <* <*n11, n12, n13*>, <*n21, n22, n23*>, <*n31, n32, n33*>*> by PASCAL: 3;

      consider m11,m12,m13,m21,m22,m23,m31,m32,m33 be Element of F_Real such that

       A6: M = <* <*m11, m12, m13*>, <*m21, m22, m23*>, <*m31, m32, m33*>*> by PASCAL: 3;

      reconsider rn11 = n11, rn12 = n12, rn13 = n13, rn21 = n21, rn22 = n22, rn23 = n23, rn31 = n31, rn32 = n32, rn33 = n33 as Element of REAL ;

      reconsider rm11 = m11, rm12 = m12, rm13 = m13, rm21 = m21, rm22 = m22, rm23 = m23, rm31 = m31, rm32 = m32, rm33 = m33 as Element of REAL ;

      

       A7: |[1, 0 , 0 ]| in ( TOP-REAL 3);

      then

      reconsider q1 = <*1, 0 , 0 *> as FinSequence of REAL by EUCLID: 24;

      reconsider z1 = (q1 . 1), z2 = (q1 . 2), z3 = (q1 . 3) as Element of REAL by XREAL_0:def 1;

      

       A8: z1 = 1 & z2 = 0 & z3 = 0 by FINSEQ_1: 45;

      q1 in ( REAL 3) by A7, EUCLID: 22;

      then

       A9: ( len q1) = 3 by EUCLID_8: 50;

      then NR = <* <*rn11, rn12, rn13*>, <*rn21, rn22, rn23*>, <*rn31, rn32, rn33*>*> & q1 = <*z1, z2, z3*> by FINSEQ_1: 45, A5;

      

      then

       A10: (NR * q1) = <*(((rn11 * z1) + (rn12 * z2)) + (rn13 * z3)), (((rn21 * z1) + (rn22 * z2)) + (rn23 * z3)), (((rn31 * z1) + (rn32 * z2)) + (rn33 * z3))*> by PASCAL: 9

      .= <*rn11, rn21, rn31*> by A8;

      MR = <* <*rm11, rm12, rm13*>, <*rm21, rm22, rm23*>, <*rm31, rm32, rm33*>*> & q1 = <*z1, z2, z3*> by A9, FINSEQ_1: 45, A6;

      

      then (MR * q1) = <*(((rm11 * z1) + (rm12 * z2)) + (rm13 * z3)), (((rm21 * z1) + (rm22 * z2)) + (rm23 * z3)), (((rm31 * z1) + (rm32 * z2)) + (rm33 * z3))*> by PASCAL: 9

      .= <*rm11, rm21, rm31*> by A8;

      then

       A11: rn11 = rm11 & rn21 = rm21 & rn31 = rm31 by A10, A2, A1, FINSEQ_1: 78;

      

       A12: |[ 0 , 1, 0 ]| in ( TOP-REAL 3);

      then

      reconsider q1 = <* 0 , 1, 0 *> as FinSequence of REAL by EUCLID: 24;

      reconsider z1 = (q1 . 1), z2 = (q1 . 2), z3 = (q1 . 3) as Element of REAL by XREAL_0:def 1;

      

       A13: z1 = 0 & z2 = 1 & z3 = 0 by FINSEQ_1: 45;

      q1 in ( REAL 3) by A12, EUCLID: 22;

      then

       A14: ( len q1) = 3 by EUCLID_8: 50;

      then NR = <* <*rn11, rn12, rn13*>, <*rn21, rn22, rn23*>, <*rn31, rn32, rn33*>*> & q1 = <*z1, z2, z3*> by FINSEQ_1: 45, A5;

      

      then

       A15: (NR * q1) = <*(((rn11 * z1) + (rn12 * z2)) + (rn13 * z3)), (((rn21 * z1) + (rn22 * z2)) + (rn23 * z3)), (((rn31 * z1) + (rn32 * z2)) + (rn33 * z3))*> by PASCAL: 9

      .= <*rn12, rn22, rn32*> by A13;

      MR = <* <*rm11, rm12, rm13*>, <*rm21, rm22, rm23*>, <*rm31, rm32, rm33*>*> & q1 = <*z1, z2, z3*> by A14, FINSEQ_1: 45, A6;

      

      then (MR * q1) = <*(((rm11 * z1) + (rm12 * z2)) + (rm13 * z3)), (((rm21 * z1) + (rm22 * z2)) + (rm23 * z3)), (((rm31 * z1) + (rm32 * z2)) + (rm33 * z3))*> by PASCAL: 9

      .= <*rm12, rm22, rm32*> by A13;

      then

       A16: rn12 = rm12 & rn22 = rm22 & rn32 = rm32 by A15, A3, A1, FINSEQ_1: 78;

      

       A17: |[ 0 , 0 , 1]| in ( TOP-REAL 3);

      then

      reconsider q1 = <* 0 , 0 , 1*> as FinSequence of REAL by EUCLID: 24;

      reconsider z1 = (q1 . 1), z2 = (q1 . 2), z3 = (q1 . 3) as Element of REAL by XREAL_0:def 1;

      

       A18: z1 = 0 & z2 = 0 & z3 = 1 by FINSEQ_1: 45;

      q1 in ( REAL 3) by A17, EUCLID: 22;

      then

       A19: ( len q1) = 3 by EUCLID_8: 50;

      then NR = <* <*rn11, rn12, rn13*>, <*rn21, rn22, rn23*>, <*rn31, rn32, rn33*>*> & q1 = <*z1, z2, z3*> by FINSEQ_1: 45, A5;

      

      then

       A20: (NR * q1) = <*(((rn11 * z1) + (rn12 * z2)) + (rn13 * z3)), (((rn21 * z1) + (rn22 * z2)) + (rn23 * z3)), (((rn31 * z1) + (rn32 * z2)) + (rn33 * z3))*> by PASCAL: 9

      .= <*rn13, rn23, rn33*> by A18;

      MR = <* <*rm11, rm12, rm13*>, <*rm21, rm22, rm23*>, <*rm31, rm32, rm33*>*> & q1 = <*z1, z2, z3*> by A19, FINSEQ_1: 45, A6;

      

      then (MR * q1) = <*(((rm11 * z1) + (rm12 * z2)) + (rm13 * z3)), (((rm21 * z1) + (rm22 * z2)) + (rm23 * z3)), (((rm31 * z1) + (rm32 * z2)) + (rm33 * z3))*> by PASCAL: 9

      .= <*rm13, rm23, rm33*> by A18;

      then rn13 = rm13 & rn23 = rm23 & rn33 = rm33 by A20, A4, A1, FINSEQ_1: 78;

      hence thesis by A11, A16, A5, A6;

    end;

    theorem :: BKMODEL1:67

    

     Th56: for a be non zero Real holds for u be Element of ( TOP-REAL 3) st (a * u) = ( 0. ( TOP-REAL 3)) holds u is zero

    proof

      let a be non zero Real;

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

      assume (a * u) = ( 0. ( TOP-REAL 3));

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

      then (u `1 ) = 0 & (u `2 ) = 0 & (u `3 ) = 0 by FINSEQ_1: 78;

      hence thesis by EUCLID_5: 3, EUCLID_5: 4;

    end;

    theorem :: BKMODEL1:68

    

     Th57: for u,v be non zero Element of ( TOP-REAL 3) holds for a,b be Real st (a <> 0 or b <> 0 ) & ((a * u) + (b * v)) = ( 0. ( TOP-REAL 3)) holds are_Prop (u,v)

    proof

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

      let a,b be Real;

      assume that

       A1: a <> 0 or b <> 0 and

       A2: ((a * u) + (b * v)) = ( 0. ( TOP-REAL 3));

      reconsider n = 3 as Nat;

      reconsider au = (a * u), bv = (b * v) as Element of ( TOP-REAL 3);

      consider c be Real such that

       A3: c <> 0 and

       A4: au = (c * bv) by A2, ANPROJ_1: 1, ANPROJ_1: 13;

      

       A5: a <> 0 & b <> 0

      proof

        assume a = 0 or b = 0 ;

        per cases ;

          suppose

           A6: a = 0 ;

          u in ( TOP-REAL 3);

          then u in ( REAL 3) by EUCLID: 22;

          then

           A7: ( 0 * u) = ( 0* n) by EUCLID_4: 3;

          bv in ( TOP-REAL 3);

          then bv in ( REAL 3) by EUCLID: 22;

          then (( 0* n) + bv) = bv by EUCLID_4: 1;

          hence contradiction by A1, A6, A2, A7, Th56;

        end;

          suppose

           A8: b = 0 ;

          v in ( TOP-REAL 3);

          then v in ( REAL 3) by EUCLID: 22;

          then

           A9: ( 0 * v) = ( 0* n) by EUCLID_4: 3;

          au in ( TOP-REAL 3);

          then au in ( REAL 3) by EUCLID: 22;

          then (au + ( 0* n)) = au by EUCLID_4: 1;

          hence contradiction by A1, A8, A2, A9, Th56;

        end;

      end;

      u = (1 * u) by RVSUM_1: 52

      .= (((1 / a) * a) * u) by A5, XCMPLX_1: 106

      .= ((1 / a) * (c * (b * v))) by A4, RVSUM_1: 49

      .= (((1 / a) * c) * (b * v)) by RVSUM_1: 49

      .= ((((1 / a) * c) * b) * v) by RVSUM_1: 49;

      hence thesis by A3, A5, ANPROJ_1: 1;

    end;

    theorem :: BKMODEL1:69

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

    proof

      let N be invertible Matrix of 3, F_Real ;

      let P,Q,R be Point of ( ProjectiveSpace ( TOP-REAL 3));

      assume that

       A1: P <> Q and

       A2: (( homography N) . P) = Q and

       A3: (( homography N) . Q) = P and

       A4: (P,Q,R) are_collinear ;

      reconsider NR = ( MXF2MXR N) as Matrix of 3, REAL by MATRIXR1:def 2;

      consider u1,v1 be Element of ( TOP-REAL 3), u1f be FinSequence of F_Real , p1 be FinSequence of (1 -tuples_on REAL ) such that

       A5: P = ( Dir u1) & not u1 is zero & u1 = u1f & p1 = (N * u1f) & v1 = ( M2F p1) & not v1 is zero & (( homography N) . P) = ( Dir v1) by ANPROJ_8:def 4;

      consider u2,v2 be Element of ( TOP-REAL 3), u2f be FinSequence of F_Real , p2 be FinSequence of (1 -tuples_on REAL ) such that

       A6: Q = ( Dir u2) & not u2 is zero & u2 = u2f & p2 = (N * u2f) & v2 = ( M2F p2) & not v2 is zero & (( homography N) . Q) = ( Dir v2) by ANPROJ_8:def 4;

      reconsider u1fr = u1f, u2fr = u2f as FinSequence of REAL ;

      u1 in ( TOP-REAL 3) & u2 in ( TOP-REAL 3);

      then

       A7: u1 in ( REAL 3) & u2 in ( REAL 3) by EUCLID: 22;

      then

       A8: ( len u1) = 3 & ( len u2) = 3 by EUCLID_8: 50;

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

       A9: not u3 is zero and

       A10: R = ( Dir u3) by ANPROJ_1: 26;

      reconsider uf3r = u3 as FinSequence of REAL by EUCLID: 24;

      

       A11: are_Prop (v2,u1) & are_Prop (v1,u2) by A2, A3, A5, A6, ANPROJ_1: 22;

      then

      consider l1 be Real such that

       A12: l1 <> 0 and

       A13: v2 = (l1 * u1) by ANPROJ_1: 1;

      consider l2 be Real such that

       A14: l2 <> 0 and

       A15: v1 = (l2 * u2) by A11, ANPROJ_1: 1;

      

       A16: ( width NR) = 3 & ( len NR) = 3 & ( len u2fr) = 3 & ( len u1fr) = 3 by A7, EUCLID_8: 50, A5, A6, MATRIX_0: 24;

      

       A17: ( width NR) = ( len u2fr) & ( len u2fr) > 0 & ( width NR) = ( len u1fr) & ( len u1fr) > 0 by A8, A5, A6, MATRIX_0: 24;

      reconsider l = (l1 * l2) as non zero Real by A12, A14;

      

       A18: ((NR * NR) * u1fr) = (NR * (NR * u1fr)) by A16, MATRIXR2: 59

      .= (NR * (l2 * u2fr)) by A5, A6, A8, MATRIXR1:def 2, Th30, A15

      .= (l2 * (NR * u2fr)) by A17, MATRIXR2: 53

      .= (l2 * (l1 * u1fr)) by A5, A6, A8, MATRIXR1:def 2, Th30, A13

      .= (l * u1fr) by RVSUM_1: 49;

      

       A19: ((NR * NR) * u2fr) = (NR * (NR * u2fr)) by A16, MATRIXR2: 59

      .= (NR * (l1 * u1fr)) by A5, A6, A8, MATRIXR1:def 2, Th30, A13

      .= (l1 * (NR * u1fr)) by A17, MATRIXR2: 53

      .= (l1 * (l2 * u2fr)) by A5, A6, A8, MATRIXR1:def 2, Th30, A15

      .= (l * u2fr) by RVSUM_1: 49;

       |{u1, u2, u3}| = 0 by A4, A5, A6, A9, A10, Th01;

      then

      consider a,b,c be Real such that

       A20: (((a * u1) + (b * u2)) + (c * u3)) = ( 0. ( TOP-REAL 3)) & ((a <> 0 ) or (b <> 0 ) or (c <> 0 )) by ANPROJ_8: 42;

      

       A21: c <> 0

      proof

        assume

         A22: c = 0 ;

        reconsider bu2 = (b * u2) as Element of ( REAL 3) by EUCLID: 22;

        reconsider n = 3 as Nat;

        u3 in ( TOP-REAL 3);

        then u3 in ( REAL 3) by EUCLID: 22;

        

        then (bu2 + ( 0 * u3)) = (bu2 + ( 0* n)) by EUCLID_4: 3

        .= bu2 by EUCLID_4: 1;

        then ((a * u1) + (b * u2)) = ( 0. ( TOP-REAL 3)) by A20, A22, RVSUM_1: 15;

        then are_Prop (u1,u2) by A20, A22, A5, A6, Th57;

        hence contradiction by A1, A5, A6, ANPROJ_1: 22;

      end;

      

       A23: (((a * u1) + (b * u2)) + (c * u3)) = (((c * u3) + (a * u1)) + (b * u2)) by RVSUM_1: 15;

      reconsider d = (( - a) / c), e = (( - b) / c) as Real;

      

       A24: u3 = ((d * u1) + (e * u2)) by A23, A20, A21, ANPROJ_8: 12;

      reconsider u4fr = ((d * u1) + (e * u2)) as FinSequence of REAL ;

      reconsider NRNR = (NR * NR) as Matrix of 3, REAL ;

      u3 in ( TOP-REAL 3);

      then u3 in ( REAL 3) by EUCLID: 22;

      then

       A25: ( len u4fr) = ( width NR) & ( width NR) = ( len NR) & ( len u4fr) > 0 & ( len NR) > 0 by A16, A24, EUCLID_8: 50;

      

       A26: ( len u1fr) = 3 & ( len u2fr) = 3 & ( width NR) = 3 & ( len NR) = 3 by A5, A6, A7, EUCLID_8: 50, MATRIX_0: 24;

      ( len (d * u1fr)) = 3 & ( len (e * u2fr)) = 3 by RVSUM_1: 117, A5, A6, A8;

      then

       A27: ( len (d * u1fr)) = ( len (e * u2fr)) & ( width NR) = ( len (d * u1fr)) & ( len (d * u1fr)) > 0 & ( len NR) > 0 by MATRIX_0: 24;

      ( len (NR * u1fr)) = 3 & ( len (NR * u2fr)) = 3 by A26, MATRIXR1: 61;

      then

       A28: ( len (d * (NR * u1fr))) = 3 & ( len (e * (NR * u2fr))) = 3 & ( width NR) = 3 & ( len NR) = 3 by MATRIX_0: 24, RVSUM_1: 117;

      

       A29: ( width NR) = ( len (NR * u1fr)) & ( len (NR * u1fr)) > 0 by A26, MATRIXR1: 61;

      

       A30: ( width NR) = ( len (NR * u2fr)) & ( len (NR * u2fr)) > 0 by A26, MATRIXR1: 61;

      

       A31: ((NR * NR) * uf3r) = ((NR * NR) * u4fr) by A23, A20, A21, ANPROJ_8: 12

      .= (NR * (NR * ((d * u1fr) + (e * u2fr)))) by A5, A6, A25, MATRIXR2: 59

      .= (NR * ((NR * (d * u1fr)) + (NR * (e * u2fr)))) by MATRIXR1: 57, A27

      .= (NR * ((d * (NR * u1fr)) + (NR * (e * u2fr)))) by MATRIXR1: 59, A26

      .= (NR * ((d * (NR * u1fr)) + (e * (NR * u2fr)))) by MATRIXR1: 59, A26

      .= ((NR * (d * (NR * u1fr))) + (NR * (e * (NR * u2fr)))) by MATRIXR1: 57, A28

      .= ((d * (NR * (NR * u1fr))) + (NR * (e * (NR * u2fr)))) by MATRIXR1: 59, A29

      .= ((d * (NR * (NR * u1fr))) + (e * (NR * (NR * u2fr)))) by MATRIXR1: 59, A30

      .= ((d * ((NR * NR) * u1fr)) + (e * (NR * (NR * u2fr)))) by A16, MATRIXR2: 59

      .= ((d * (l * u1fr)) + (e * ((NR * NR) * u2fr))) by A18, A16, MATRIXR2: 59

      .= (((d * l) * u1fr) + (e * (l * u2fr))) by A19, RVSUM_1: 49

      .= (((d * l) * u1fr) + ((e * l) * u2fr)) by RVSUM_1: 49

      .= ((l * (d * u1fr)) + ((l * e) * u2fr)) by RVSUM_1: 49

      .= ((l * (d * u1fr)) + (l * (e * u2fr))) by RVSUM_1: 49

      .= (l * ((d * u1) + (e * u2))) by A5, A6, RVSUM_1: 51

      .= (l * uf3r) by A23, A20, A21, ANPROJ_8: 12;

      N = NR by MATRIXR1:def 2;

      then (( homography (N * N)) . R) = R by A31, A9, A10, Th33, ANPROJ_8: 17;

      hence thesis by ANPROJ_9: 13;

    end;

    theorem :: BKMODEL1:70

    for n be Nat holds for u,v be Element of ( TOP-REAL n) holds for a,b be Real st (((1 - a) * u) + (a * v)) = (((1 - b) * v) + (b * u)) holds ((1 - (a + b)) * u) = ((1 - (a + b)) * v)

    proof

      let n be Nat;

      let u,v be Element of ( TOP-REAL n);

      let a,b be Real;

      assume

       A1: (((1 - a) * u) + (a * v)) = (((1 - b) * v) + (b * u));

      reconsider ru = u, rv = v as Element of ( REAL n) by EUCLID: 22;

      

       A2: ((((1 - a) * ru) + (a * rv)) - (a * rv)) = ((1 - a) * ru)

      proof

        ((1 - a) * ru) in ( REAL n) & (a * rv) in ( REAL n);

        then

        reconsider t1 = ((1 - a) * u), t2 = (a * v) as Element of (n -tuples_on REAL ) by EUCLID:def 1;

        ((((1 - a) * ru) + (a * rv)) - (a * rv)) = ((t1 + t2) - t2)

        .= t1 by RVSUM_1: 42;

        hence thesis;

      end;

      

       A3: (((((1 - b) * rv) - (a * rv)) + (b * ru)) - (b * ru)) = (((1 - b) * rv) - (a * rv))

      proof

        reconsider t1 = (((1 - b) * rv) - (a * rv)), t2 = (b * ru) as Element of (n -tuples_on REAL ) by EUCLID:def 1;

        (((((1 - b) * rv) - (a * rv)) + (b * ru)) - (b * ru)) = ((t1 + t2) - t2)

        .= t1 by RVSUM_1: 42;

        hence thesis;

      end;

      ((1 - a) * ru) = ((((1 - b) * rv) + (b * ru)) + ( - (a * rv))) by A1, A2, RVSUM_1: 31

      .= ((((1 - b) * rv) + ( - (a * rv))) + (b * ru)) by RVSUM_1: 15;

      then (((1 - a) * ru) - (b * ru)) = (((1 - b) * rv) - (a * rv)) by A3, RVSUM_1: 31;

      

      then (((1 - a) * ru) + ( - (b * ru))) = (((1 - b) * rv) - (a * rv)) by RVSUM_1: 31

      .= (((1 - b) * rv) + ( - (a * rv))) by RVSUM_1: 31;

      then (((1 - a) * ru) + (( - 1) * (b * ru))) = (((1 - b) * rv) + ( - (a * rv))) by RVSUM_1: 54;

      then (((1 - a) * ru) + ((( - 1) * b) * ru)) = (((1 - b) * rv) + ( - (a * rv))) by RVSUM_1: 49;

      then (((1 - a) + (( - 1) * b)) * ru) = (((1 - b) * rv) + ( - (a * rv))) by RVSUM_1: 50;

      

      then (((1 - a) - b) * ru) = (((1 - b) * rv) + (( - 1) * (a * rv))) by RVSUM_1: 54

      .= (((1 - b) * rv) + ((( - 1) * a) * rv)) by RVSUM_1: 49

      .= (((1 - b) + (( - 1) * a)) * rv) by RVSUM_1: 50;

      hence thesis;

    end;

    theorem :: BKMODEL1:71

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

    definition

      :: BKMODEL1:def4

      func real_projective_plane -> non empty proper CollProjectivePlane equals ( ProjectiveSpace ( TOP-REAL 3));

      coherence by ANPROJ_8: 57;

    end

    reserve P,Q,R for POINT of ( IncProjSp_of real_projective_plane ),

L for LINE of ( IncProjSp_of real_projective_plane ),

p,q,r for Point of real_projective_plane ;

    theorem :: BKMODEL1:72

    for L be Element of ( ProjectiveLines real_projective_plane ) holds ex p, q st p <> q & L = ( Line (p,q))

    proof

      let L be Element of ( ProjectiveLines real_projective_plane );

      L in ( ProjectiveLines real_projective_plane );

      then L in { B where B be Subset of real_projective_plane : B is LINE of real_projective_plane } by INCPROJ:def 1;

      then ex B be Subset of real_projective_plane st L = B & B is LINE of real_projective_plane ;

      hence thesis by COLLSP:def 7;

    end;

    theorem :: BKMODEL1:73

    

     Th60: ex p, q st p <> q & L = ( Line (p,q))

    proof

      L in the Lines of ( IncProjSp_of real_projective_plane );

      then L in ( ProjectiveLines real_projective_plane ) by INCPROJ: 2;

      then L in { B where B be Subset of real_projective_plane : B is LINE of real_projective_plane } by INCPROJ:def 1;

      then ex B be Subset of real_projective_plane st L = B & B is LINE of real_projective_plane ;

      hence thesis by COLLSP:def 7;

    end;

    theorem :: BKMODEL1:74

    

     Th61: R = r & L = ( Line (p,q)) implies (R on L iff (p,q,r) are_collinear )

    proof

      assume

       A1: R = r & L = ( Line (p,q));

      hereby

        assume R on L;

        then [R, L] in the Inc of ( IncProjSp_of real_projective_plane ) by INCSP_1:def 1;

        then [R, L] in ( Proj_Inc real_projective_plane ) by INCPROJ: 2;

        then R in the carrier of real_projective_plane & L in ( ProjectiveLines real_projective_plane ) & ex Y be set st L = Y & R in Y by INCPROJ:def 2;

        hence (p,q,r) are_collinear by A1, COLLSP: 11;

      end;

      assume

       A2: (p,q,r) are_collinear ;

      now

        R is Point of real_projective_plane by INCPROJ: 3;

        hence R in the carrier of real_projective_plane ;

        L is Element of ( ProjectiveLines real_projective_plane ) by INCPROJ: 1, INCPROJ: 4;

        hence L in ( ProjectiveLines real_projective_plane );

        thus ex Y be set st L = Y & R in Y by A2, A1, COLLSP: 11;

      end;

      then [R, L] in ( Proj_Inc real_projective_plane ) by INCPROJ:def 2;

      then [R, L] in the Inc of ( IncProjSp_of real_projective_plane ) by INCPROJ: 2;

      hence R on L by INCSP_1:def 1;

    end;

    theorem :: BKMODEL1:75

    

     Th62: ( IncProjSp_of real_projective_plane ) is IncProjectivePlane

    proof

      ( IncProjSp_of real_projective_plane ) is 2-dimensional

      proof

        for M,N be LINE of ( IncProjSp_of real_projective_plane ) holds ex q be POINT of ( IncProjSp_of real_projective_plane ) st q on M & q on N

        proof

          let M,N be LINE of ( IncProjSp_of real_projective_plane );

          consider p1,q1 be Point of real_projective_plane such that p1 <> q1 and

           A1: M = ( Line (p1,q1)) by Th60;

          consider p2,q2 be Point of real_projective_plane such that p2 <> q2 and

           A2: N = ( Line (p2,q2)) by Th60;

          consider q be Element of real_projective_plane such that

           A3: (p1,q1,q) are_collinear and

           A4: (p2,q2,q) are_collinear by ANPROJ_2:def 14;

          reconsider Q = q as POINT of ( IncProjSp_of real_projective_plane ) by INCPROJ: 3;

          take Q;

          thus thesis by A1, A2, A3, A4, Th61;

        end;

        hence thesis by INCPROJ:def 9;

      end;

      hence thesis;

    end;

    theorem :: BKMODEL1:76

    for L1,L2 be LINE of real_projective_plane holds L1 meets L2

    proof

      let L1,L2 be LINE of real_projective_plane ;

      reconsider LI1 = L1, LI2 = L2 as LINE of ( IncProjSp_of real_projective_plane ) by INCPROJ: 4;

      consider R be POINT of ( IncProjSp_of real_projective_plane ) such that

       A1: R on LI1 and

       A2: R on LI2 by Th62, INCPROJ:def 9;

      reconsider S = R as Element of real_projective_plane by INCPROJ: 3;

      S in LI1 & S in LI2 by A1, A2, INCPROJ: 5;

      hence thesis by XBOOLE_0:def 4;

    end;

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

    theorem :: BKMODEL1:77

    p = ( Dir u) & q = ( Dir v) & R = ( Dir w) & L = ( Line (p,q)) implies (R on L iff |{u, v, w}| = 0 )

    proof

      assume that

       A1: p = ( Dir u) and

       A2: q = ( Dir v) and

       A3: R = ( Dir w) and

       A4: L = ( Line (p,q));

      reconsider r = ( Dir w) as Point of real_projective_plane by ANPROJ_1: 26;

      hereby

        assume R on L;

        then (p,q,r) are_collinear by A3, A4, Th61;

        then

        consider u1,v1,w1 be Element of ( TOP-REAL 3) such that

         A5: p = ( Dir u1) and

         A6: q = ( Dir v1) and

         A7: r = ( Dir w1) and

         A8: u1 is non zero & v1 is non zero & w1 is non zero and

         A9: u1 = v1 or u1 = w1 or v1 = w1 or {u1, v1, w1} is linearly-dependent by ANPROJ_8: 10;

        (u1,v1,w1) are_LinDep by A9, ANPROJ_8: 9;

        then |{u1, v1, w1}| = 0 by ANPROJ_8: 43;

        then |{u, v1, w1}| = 0 by A1, A5, A8, ANPROJ_8: 58;

        then |{u, v, w1}| = 0 by A2, A6, A8, ANPROJ_8: 59;

        hence |{u, v, w}| = 0 by A8, A7, ANPROJ_8: 60;

      end;

      assume |{u, v, w}| = 0 ;

      then u = v or u = w or v = w or {u, v, w} is linearly-dependent by ANPROJ_8: 9, ANPROJ_8: 43;

      then (p,q,r) are_collinear by A1, A2, ANPROJ_8: 10;

      hence R on L by A3, A4, Th61;

    end;

    theorem :: BKMODEL1:78

    

     Th64: for p,q be Element of ( ProjectiveSpace ( TOP-REAL 3)) st p <> q & p = ( Dir u) & q = ( Dir v) holds (u <X> v) is non zero

    proof

      let p,q be Element of ( ProjectiveSpace ( TOP-REAL 3));

      assume that

       A1: p <> q & p = ( Dir u) & q = ( Dir v);

      assume (u <X> v) is zero;

      then are_Prop (u,v) by ANPROJ_8: 51;

      hence contradiction by A1, ANPROJ_1: 22;

    end;

    definition

      let p,q be Point of real_projective_plane ;

      assume

       A1: p <> q;

      :: BKMODEL1:def5

      func L2P (p,q) -> Point of real_projective_plane means

      : Def01: ex u,v be non zero Element of ( TOP-REAL 3) st p = ( Dir u) & q = ( Dir v) & it = ( Dir (u <X> v));

      existence

      proof

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

         A2: not u is zero & p = ( Dir u) by ANPROJ_1: 26;

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

         A3: not v is zero & q = ( Dir v) by ANPROJ_1: 26;

        reconsider u, v as non zero Element of ( TOP-REAL 3) by A2, A3;

        (u <X> v) is non zero by A1, A2, A3, Th64;

        then ( Dir (u <X> v)) is Element of ( ProjectiveSpace ( TOP-REAL 3)) by ANPROJ_1: 26;

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        let P1,P2 be Point of real_projective_plane such that

         A4: ex u,v be non zero Element of ( TOP-REAL 3) st p = ( Dir u) & q = ( Dir v) & P1 = ( Dir (u <X> v)) and

         A5: ex u,v be non zero Element of ( TOP-REAL 3) st p = ( Dir u) & q = ( Dir v) & P2 = ( Dir (u <X> v));

        consider u1,v1 be non zero Element of ( TOP-REAL 3) such that

         A6: p = ( Dir u1) & q = ( Dir v1) & P1 = ( Dir (u1 <X> v1)) by A4;

        consider u2,v2 be non zero Element of ( TOP-REAL 3) such that

         A7: p = ( Dir u2) & q = ( Dir v2) & P2 = ( Dir (u2 <X> v2)) by A5;

        

         A8: (u1 <X> v1) is non zero & (u2 <X> v2) is non zero by A1, A6, A7, Th64;

        

         A9: are_Prop (u1,u2) & are_Prop (v1,v2) by A6, A7, ANPROJ_1: 22;

        then

        consider a be Real such that

         A10: a <> 0 & u1 = (a * u2) by ANPROJ_1: 1;

        consider b be Real such that

         A11: b <> 0 & v1 = (b * v2) by A9, ANPROJ_1: 1;

        (u1 <X> v1) = ((b * (a * u2)) <X> v2) by A10, A11, EUCLID_5: 16

        .= (((a * b) * u2) <X> v2) by RVSUM_1: 49

        .= ((a * b) * (u2 <X> v2)) by EUCLID_5: 16;

        then are_Prop ((u1 <X> v1),(u2 <X> v2)) by A10, A11, ANPROJ_1: 1;

        hence P1 = P2 by A6, A7, A8, ANPROJ_1: 22;

      end;

    end

    theorem :: BKMODEL1:79

    for p,q be Point of real_projective_plane st p <> q holds ( L2P (q,p)) = ( L2P (p,q)) & p <> ( L2P (p,q))

    proof

      let p,q be Point of real_projective_plane ;

      assume

       A1: p <> q;

      then

      consider u1,v1 be non zero Element of ( TOP-REAL 3) such that

       A2: p = ( Dir u1) and

       A3: q = ( Dir v1) and

       A4: ( L2P (p,q)) = ( Dir (u1 <X> v1)) by Def01;

      consider u2,v2 be non zero Element of ( TOP-REAL 3) such that

       A5: q = ( Dir u2) and

       A6: p = ( Dir v2) and

       A7: ( L2P (q,p)) = ( Dir (u2 <X> v2)) by A1, Def01;

       are_Prop (u1,v2) by A2, A6, ANPROJ_1: 22;

      then

      consider a be Real such that

       A8: a <> 0 and

       A9: u1 = (a * v2) by ANPROJ_1: 1;

       are_Prop (u2,v1) by A3, A5, ANPROJ_1: 22;

      then

      consider b be Real such that

       A10: b <> 0 and

       A11: v1 = (b * u2) by ANPROJ_1: 1;

      ((a * v2) <X> (b * u2)) = (( - (a * b)) * (u2 <X> v2))

      proof

        reconsider p1 = (a * v2), p2 = (b * u2) as Element of ( TOP-REAL 3);

        

         A12: (p1 `1 ) = ((a * v2) . 1) by EUCLID_5:def 1

        .= (a * (v2 . 1)) by RVSUM_1: 44;

        

         A13: (p1 `2 ) = ((a * v2) . 2) by EUCLID_5:def 2

        .= (a * (v2 . 2)) by RVSUM_1: 44;

        

         A14: (p1 `3 ) = ((a * v2) . 3) by EUCLID_5:def 3

        .= (a * (v2 . 3)) by RVSUM_1: 44;

        

         A15: (p2 `1 ) = ((b * u2) . 1) by EUCLID_5:def 1

        .= (b * (u2 . 1)) by RVSUM_1: 44;

        

         A16: (p2 `2 ) = ((b * u2) . 2) by EUCLID_5:def 2

        .= (b * (u2 . 2)) by RVSUM_1: 44;

        

         A17: (p2 `3 ) = ((b * u2) . 3) by EUCLID_5:def 3

        .= (b * (u2 . 3)) by RVSUM_1: 44;

        

         A18: ((a * v2) <X> (b * u2)) = |[(((a * (v2 . 2)) * (b * (u2 . 3))) - ((a * (v2 . 3)) * (b * (u2 . 2)))), (((a * (v2 . 3)) * (b * (u2 . 1))) - ((a * (v2 . 1)) * (b * (u2 . 3)))), (((a * (v2 . 1)) * (b * (u2 . 2))) - ((a * (v2 . 2)) * (b * (u2 . 1))))]| by A12, A13, A14, A15, A16, A17, EUCLID_5:def 4;

        (u2 `1 ) = (u2 . 1) & (u2 `2 ) = (u2 . 2) & (u2 `3 ) = (u2 . 3) & (v2 `1 ) = (v2 . 1) & (v2 `2 ) = (v2 . 2) & (v2 `3 ) = (v2 . 3) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

        

        then (( - (a * b)) * (u2 <X> v2)) = (( - (a * b)) * |[(((u2 . 2) * (v2 . 3)) - ((u2 . 3) * (v2 . 2))), (((u2 . 3) * (v2 . 1)) - ((u2 . 1) * (v2 . 3))), (((u2 . 1) * (v2 . 2)) - ((u2 . 2) * (v2 . 1)))]|) by EUCLID_5:def 4

        .= |[(( - (a * b)) * (((u2 . 2) * (v2 . 3)) - ((u2 . 3) * (v2 . 2)))), (( - (a * b)) * (((u2 . 3) * (v2 . 1)) - ((u2 . 1) * (v2 . 3)))), (( - (a * b)) * (((u2 . 1) * (v2 . 2)) - ((u2 . 2) * (v2 . 1))))]| by EUCLID_5: 8;

        hence thesis by A18;

      end;

      then

       A19: are_Prop ((u1 <X> v1),(u2 <X> v2)) by A8, A10, A9, A11, ANPROJ_1: 1;

      

       A20: (u1 <X> v1) is non zero

      proof

        assume (u1 <X> v1) is zero;

        then are_Prop (u1,v1) by ANPROJ_8: 51;

        hence contradiction by A1, A2, A3, ANPROJ_1: 22;

      end;

      (u2 <X> v2) is non zero

      proof

        assume (u2 <X> v2) is zero;

        then are_Prop (u2,v2) by ANPROJ_8: 51;

        hence contradiction by A1, A5, A6, ANPROJ_1: 22;

      end;

      hence ( L2P (q,p)) = ( L2P (p,q)) by A19, A20, A4, A7, ANPROJ_1: 22;

      thus p <> ( L2P (p,q))

      proof

        assume p = ( L2P (p,q));

        then are_Prop (u1,(u1 <X> v1)) by A2, A4, A20, ANPROJ_1: 22;

        then

        consider a be Real such that a <> 0 and

         A21: u1 = (a * (u1 <X> v1)) by ANPROJ_1: 1;

         |(u1, (a * (u1 <X> v1)))| = (a * |(u1, (u1 <X> v1))|) by Th19

        .= (a * 0 ) by ANPROJ_8: 44

        .= 0 ;

        then u1 = ( 0. ( TOP-REAL 3)) by A21, EUCLID_2: 43;

        hence contradiction;

      end;

    end;

    theorem :: BKMODEL1:80

    for N be invertible Matrix of 3, F_Real holds ( dom ( homography N)) = ( ProjectivePoints ( TOP-REAL 3))

    proof

      let N be invertible Matrix of 3, F_Real ;

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

      hence thesis by ANPROJ_1: 23;

    end;

    begin

    definition

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

      :: BKMODEL1:def6

      func negative_conic (a,b,c,d,e,f) -> Subset of ( ProjectiveSpace ( TOP-REAL 3)) equals { 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 (a,b,c,d,e,f,u)) is negative };

      coherence

      proof

        set C = { 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 (a,b,c,d,e,f,u)) is negative };

        C c= the carrier of ( ProjectiveSpace ( TOP-REAL 3))

        proof

          let x be object;

          assume x in C;

          then ex P be Point of ( ProjectiveSpace ( TOP-REAL 3)) st x = P & for u be Element of ( TOP-REAL 3) st u is non zero & P = ( Dir u) holds ( qfconic (a,b,c,d,e,f,u)) is negative;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: BKMODEL1:81

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

    proof

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

      let u1,u2 be non zero Element of ( TOP-REAL 3);

      assume that

       A1: ( Dir u1) = ( Dir u2) and

       A2: ( qfconic (a,b,c,d,e,f,u1)) is negative;

       are_Prop (u2,u1) by A1, ANPROJ_1: 22;

      then

      consider g be Real such that

       A3: g <> 0 and

       A4: u2 = (g * u1) by ANPROJ_1: 1;

      

       A5: (u2 . 1) = (g * (u1 . 1)) & (u2 . 2) = (g * (u1 . 2)) & (u2 . 3) = (g * (u1 . 3)) by A4, RVSUM_1: 44;

       0 < (g ^2 ) by A3, SQUARE_1: 12;

      then

      reconsider g2 = (g * g) as positive Real;

      ( qfconic (a,b,c,d,e,f,u2)) = (((((((a * (u2 . 1)) * (u2 . 1)) + ((b * (u2 . 2)) * (u2 . 2))) + ((c * (u2 . 3)) * (u2 . 3))) + ((d * (u2 . 1)) * (u2 . 2))) + ((e * (u2 . 1)) * (u2 . 3))) + ((f * (u2 . 2)) * (u2 . 3))) by PASCAL:def 1

      .= (g2 * (((((((a * (u1 . 1)) * (u1 . 1)) + ((b * (u1 . 2)) * (u1 . 2))) + ((c * (u1 . 3)) * (u1 . 3))) + ((d * (u1 . 1)) * (u1 . 2))) + ((e * (u1 . 1)) * (u1 . 3))) + ((f * (u1 . 2)) * (u1 . 3)))) by A5

      .= (g2 * ( qfconic (a,b,c,d,e,f,u1))) by PASCAL:def 1;

      hence thesis by A2;

    end;

    definition

      :: BKMODEL1:def7

      func absolute -> non empty Subset of ( ProjectiveSpace ( TOP-REAL 3)) equals ( conic (1,1,( - 1), 0 , 0 , 0 ));

      coherence

      proof

         Dir101 in ( conic (1,1,( - 1), 0 , 0 , 0 ))

        proof

           Dir101 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)) = 0 }

          proof

            now

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

              assume

               A1: u is non zero & Dir101 = ( Dir u);

               |[1, 0 , 1]| is non zero by EUCLID_5: 4, FINSEQ_1: 78;

              then are_Prop (u, |[1, 0 , 1]|) by A1, ANPROJ_1: 22;

              then

              consider a be Real such that a <> 0 and

               A2: u = (a * |[1, 0 , 1]|) by ANPROJ_1: 1;

              u = |[(a * 1), (a * 0 ), (a * 1)]| by A2, EUCLID_5: 8

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

              then (u `1 ) = a & (u `2 ) = 0 & (u `3 ) = a by EUCLID_5: 2;

              then

               A3: (u . 1) = a & (u . 2) = 0 & (u . 3) = a by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

              

              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

              .= 0 by A3;

            end;

            hence thesis;

          end;

          hence thesis by PASCAL:def 2;

        end;

        hence thesis;

      end;

    end

    theorem :: BKMODEL1:82

    

     Th66: for O be Matrix of 3, REAL holds for P be Element of ( ProjectiveSpace ( TOP-REAL 3)) holds for p be FinSequence of REAL st O = ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) & P = ( Dir u) & u = p holds P in absolute iff ( SumAll ( QuadraticForm (p,O,p))) = 0

    proof

      let O be Matrix of 3, REAL ;

      let P be Element of ( ProjectiveSpace ( TOP-REAL 3));

      let p be FinSequence of REAL ;

      assume

       A1: O = ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) & P = ( Dir u) & u = p;

      hereby

        assume P in absolute ;

        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)) = 0 } by PASCAL:def 2;

        then

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

         A2: P = Q and

         A3: for u be Element of ( TOP-REAL 3) st u is non zero & Q = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 ;

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

         A4: u1 is non zero and

         A5: Q = ( Dir u1) by ANPROJ_1: 26;

        reconsider p1 = u1 as FinSequence of REAL by EUCLID: 24;

        

         A6: ( SumAll ( QuadraticForm (p1,O,p1))) = ( qfconic (1,1,( - 1),(2 * 0 ),(2 * 0 ),(2 * 0 ),u1)) by A1, PASCAL: 13

        .= 0 by A3, A4, A5;

         are_Prop (u1,u) by A2, A5, A1, A4, ANPROJ_1: 22;

        then

        consider a be Real such that

         A7: a <> 0 and

         A8: u1 = (a * u) by ANPROJ_1: 1;

        reconsider fa = a as Element of F_Real by XREAL_0:def 1;

        u is Element of ( REAL 3) by EUCLID: 22;

        then ( len p) = 3 by A1, EUCLID_8: 50;

        then ( SumAll ( QuadraticForm (p1,O,p1))) = ((fa * fa) * ( SumAll ( QuadraticForm (p,O,p)))) by A1, A8, Th35;

        hence ( SumAll ( QuadraticForm (p,O,p))) = 0 by A7, A6;

      end;

      assume ( SumAll ( QuadraticForm (p,O,p))) = 0 ;

      

      then 0 = ( qfconic (1,1,( - 1),(2 * 0 ),(2 * 0 ),(2 * 0 ),u)) by A1, PASCAL: 13

      .= ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u));

      then 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)) = 0 by A1, PASCAL: 10;

      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)) = 0 };

      hence P in absolute by PASCAL:def 2;

    end;

    theorem :: BKMODEL1:83

    

     Th67: for P be Element of absolute st P = ( Dir u) holds (u . 3) <> 0

    proof

      let P be Element of absolute ;

      assume

       A1: P = ( Dir u);

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

      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)) = 0 } by PASCAL:def 2;

      then

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

       A2: P = Q and

       A3: for u be Element of ( TOP-REAL 3) st u is non zero & Q = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 ;

      

       A4: ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 by A1, A2, A3;

      thus (u . 3) <> 0

      proof

        assume

         A5: (u . 3) = 0 ;

        

         A6: (((((((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))) = 0 by A4, PASCAL:def 1;

        reconsider u1 = (u . 1), u2 = (u . 2) as Real;

        ((u1 ^2 ) + (u2 ^2 )) = 0 by A5, A6;

        then u1 = 0 & u2 = 0 by COMPLEX1: 1;

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

        hence contradiction by EUCLID_5: 3, EUCLID_5: 4;

      end;

    end;

    theorem :: BKMODEL1:84

    

     Th68: for P be Element of absolute st P = ( Dir u) & (u . 3) = 1 holds |[(u . 1), (u . 2)]| in ( circle ( 0 , 0 ,1))

    proof

      let P be Element of absolute ;

      assume that

       A1: P = ( Dir u) and

       A2: (u . 3) = 1;

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

      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)) = 0 } by PASCAL:def 2;

      then

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

       A3: P = Q and

       A4: for u be Element of ( TOP-REAL 3) st u is non zero & Q = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 ;

      ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 by A1, A3, A4;

      then

       A5: (((((((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))) = 0 by PASCAL:def 1;

      reconsider u1 = (u . 1), u2 = (u . 2) as Real;

      ((u1 ^2 ) + (u2 ^2 )) = 1 by A2, A5;

      hence thesis by Th11;

    end;

    theorem :: BKMODEL1:85

    

     Th69: for P be Point of ( ProjectiveSpace ( TOP-REAL 3)) st P = ( Dir u) & (u . 3) = 1 & |[(u . 1), (u . 2)]| in ( circle ( 0 , 0 ,1)) holds P is Element of absolute

    proof

      let P be Point of ( ProjectiveSpace ( TOP-REAL 3));

      assume that

       A1: P = ( Dir u) and

       A2: (u . 3) = 1 and

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

      reconsider u1 = (u . 1), u2 = (u . 2), u3 = (u . 3) as Real;

      

       A4: ((u1 ^2 ) + (u2 ^2 )) = ( |. |[(u1 - 0 ), (u2 - 0 )]|.| ^2 ) by TOPGEN_5: 9

      .= ( |.( |[u1, u2]| - |[ 0 , 0 ]|).| ^2 ) by EUCLID: 62

      .= (1 ^2 ) by A3, TOPREAL9: 43

      .= 1;

      now

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

        assume that

         A5: v is non zero and

         A6: P = ( Dir v);

         are_Prop (u,v) by A1, A5, A6, ANPROJ_1: 22;

        then

        consider a be Real such that

         A7: a <> 0 and

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

        reconsider v1 = (v . 1), v2 = (v . 2), v3 = (v . 3) as Real;

        u1 = (a * v1) & u2 = (a * v2) & u3 = (a * v3) by A8, RVSUM_1: 44;

        then

         A9: v1 = (u1 / a) & v2 = (u2 / a) & v3 = (u3 / a) by A7, XCMPLX_1: 89;

        ( qfconic (1,1,( - 1), 0 , 0 , 0 ,v)) = (((((((1 * v1) * v1) + ((1 * v2) * v2)) + ((( - 1) * v3) * v3)) + (( 0 * v1) * v2)) + (( 0 * v1) * v3)) + (( 0 * v2) * v3)) by PASCAL:def 1

        .= ((((u1 / a) * (u1 / a)) + ((u2 / a) * (u2 / a))) - ((u3 / a) * (u3 / a))) by A9

        .= (((((1 / a) * u1) * (u1 / a)) + ((u2 / a) * (u2 / a))) - ((u3 / a) * (u3 / a))) by XCMPLX_1: 99

        .= (((((1 / a) * u1) * ((1 / a) * u1)) + ((u2 / a) * (u2 / a))) - ((u3 / a) * (u3 / a))) by XCMPLX_1: 99

        .= ((((((1 / a) * (1 / a)) * u1) * u1) + (((1 / a) * u2) * (u2 / a))) - ((u3 / a) * (u3 / a))) by XCMPLX_1: 99

        .= ((((((1 / a) * (1 / a)) * u1) * u1) + (((1 / a) * u2) * ((1 / a) * u2))) - ((u3 / a) * (u3 / a))) by XCMPLX_1: 99

        .= ((((((1 / a) * (1 / a)) * u1) * u1) + ((((1 / a) * (1 / a)) * u2) * u2)) - (((1 / a) * u3) * (u3 / a))) by XCMPLX_1: 99

        .= ((((((1 / a) * (1 / a)) * u1) * u1) + ((((1 / a) * (1 / a)) * u2) * u2)) - (((1 / a) * u3) * ((1 / a) * u3))) by XCMPLX_1: 99

        .= (((1 / a) * (1 / a)) * (((u1 ^2 ) + (u2 * u2)) - (u3 * u3)))

        .= 0 by A2, A4;

        hence ( qfconic (1,1,( - 1), 0 , 0 , 0 ,v)) = 0 ;

      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)) = 0 };

      hence thesis by PASCAL:def 2;

    end;

    theorem :: BKMODEL1:86

    for P be Point of ( ProjectiveSpace ( TOP-REAL 3)) holds for u be non zero Element of ( TOP-REAL 3) st P = ( Dir u) & (u . 3) = 1 holds |[(u . 1), (u . 2)]| in ( circle ( 0 , 0 ,1)) iff P is Element of absolute by Th68, Th69;

    definition

      let P be Element of absolute ;

      :: BKMODEL1:def8

      func absolute_to_REAL2 (P) -> Element of ( circle ( 0 , 0 ,1)) means ex u be non zero Element of ( TOP-REAL 3) st P = ( Dir u) & (u . 3) = 1 & it = |[(u . 1), (u . 2)]|;

      existence

      proof

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

         A1: u is non zero and

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

        (u . 3) <> 0 by A1, A2, Th67;

        then

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

        then

        reconsider r = (1 / (u `3 )) as non zero Real;

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

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

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

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

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

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

        .= v by A3, XCMPLX_1: 60;

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

        then

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

        

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

        .= 1 by EUCLID_5: 2;

        then |[(v . 1), (v . 2)]| in ( circle ( 0 , 0 ,1)) by A4, Th68;

        hence thesis by A4, A5;

      end;

      uniqueness

      proof

        let u1,u2 be Element of ( circle ( 0 , 0 ,1)) such that

         A6: ex u be non zero Element of ( TOP-REAL 3) st P = ( Dir u) & (u . 3) = 1 & u1 = |[(u . 1), (u . 2)]| and

         A7: ex v be non zero Element of ( TOP-REAL 3) st P = ( Dir v) & (v . 3) = 1 & u2 = |[(v . 1), (v . 2)]|;

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

         A8: P = ( Dir u) & (u . 3) = 1 & u1 = |[(u . 1), (u . 2)]| by A6;

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

         A9: P = ( Dir v) & (v . 3) = 1 & u2 = |[(v . 1), (v . 2)]| by A7;

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

        .= v by A8, A9, Th37

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

        then (u `1 ) = (v `1 ) & (u `2 ) = (v `2 ) & (u `3 ) = (v `3 ) by FINSEQ_1: 78;

        then (u . 1) = (v `1 ) & (u . 2) = (v `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;

        then (u . 1) = (v . 1) & (u . 2) = (v . 2) by EUCLID_5:def 1, EUCLID_5:def 2;

        hence thesis by A8, A9;

      end;

    end

    theorem :: BKMODEL1:87

    the carrier of ( Tunit_circle 2) = ( circle ( 0 , 0 ,1))

    proof

      

       A1: the carrier of ( Tunit_circle 2) c= ( circle ( 0 , 0 ,1))

      proof

        let u be object;

        assume u in the carrier of ( Tunit_circle 2);

        then u in the carrier of ( Tcircle (( 0. ( TOP-REAL 2)),1)) by TOPREALB:def 7;

        then u in ( Sphere (( 0. ( TOP-REAL 2)),1)) by TOPREALB: 9;

        hence thesis by EUCLID: 54, TOPREAL9: 52;

      end;

      ( circle ( 0 , 0 ,1)) c= the carrier of ( Tunit_circle 2)

      proof

        let u be object;

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

        then u in ( Sphere (( 0. ( TOP-REAL 2)),1)) by TOPREAL9: 52, EUCLID: 54;

        then u in the carrier of ( Tcircle (( 0. ( TOP-REAL 2)),1)) by TOPREALB: 9;

        hence thesis by TOPREALB:def 7;

      end;

      hence thesis by A1;

    end;

    definition

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

      assume

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

      :: BKMODEL1:def9

      func REAL2_to_absolute (u) -> Element of absolute equals ( Dir |[(u . 1), (u . 2), 1]|);

      coherence

      proof

         |[(u `1 ), (u `2 )]| in ( circle ( 0 , 0 ,1)) by A1, EUCLID: 53;

        then

         A2: |[(u . 1), (u `2 )]| in ( circle ( 0 , 0 ,1)) by EUCLID:def 9;

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

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

        (v . 1) = (v `1 ) & (v . 2) = (v `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;

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

        then

         A3: |[(v . 1), (v . 2)]| in ( circle ( 0 , 0 ,1)) by A2, EUCLID:def 10;

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

        .= 1 by EUCLID_5: 2;

        then P is Element of absolute by A3, Th69;

        hence thesis;

      end;

    end

    theorem :: BKMODEL1:88

    

     Th70: for u be Element of ( TOP-REAL 3) st ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 & (u . 3) = 1 holds |[(u . 1), (u . 2)]| in ( Sphere (( 0. ( TOP-REAL 2)),1))

    proof

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

      assume that

       A1: ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 and

       A2: (u . 3) = 1;

       0 = (((((((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 A1, PASCAL:def 1

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

      then |[(u . 1), (u . 2)]| in ( circle ( 0 , 0 ,1)) by Th11;

      hence thesis by EUCLID: 54, TOPREAL9: 52;

    end;

    theorem :: BKMODEL1:89

    for P be Element of absolute holds ex u st (((u . 1) ^2 ) + ((u . 2) ^2 )) = 1 & (u . 3) = 1 & P = ( Dir u)

    proof

      let P be Element of absolute ;

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

       A1: u is non zero and

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

      reconsider v1 = ((u . 1) / (u . 3)), v2 = ((u . 2) / (u . 3)) as Real;

      reconsider v = |[v1, v2, 1]| as Element of ( TOP-REAL 3);

      

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

      .= 1 by EUCLID_5: 2;

      

       A4: v is non zero by EUCLID_5: 4, FINSEQ_1: 78;

      ((u . 3) * v) = |[((u . 3) * v1), ((u . 3) * v2), ((u . 3) * 1)]| by EUCLID_5: 8

      .= |[(u . 1), ((u . 3) * v2), (u . 3)]| by A1, A2, Th67, XCMPLX_1: 87

      .= |[(u . 1), (u . 2), (u . 3)]| by A1, A2, Th67, XCMPLX_1: 87

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

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

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

      .= u by EUCLID_5: 3;

      then are_Prop (u,v) by A1, A2, Th67, ANPROJ_1: 1;

      then

       A5: ( Dir v) = ( Dir u) by A1, A4, ANPROJ_1: 22;

       |[(v . 1), (v . 2)]| in ( circle ( 0 , 0 ,1)) by A2, A3, A4, A5, Th68;

      

      then (((v . 1) ^2 ) + ((v . 2) ^2 )) = (1 ^2 ) by Th12

      .= 1;

      hence thesis by A2, A3, A4, A5;

    end;

    theorem :: BKMODEL1:90

    for P be Element of absolute holds ex Q be Element of absolute st P <> Q

    proof

      let P be Element of absolute ;

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

      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)) = 0 } by PASCAL:def 2;

      then

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

       A1: P = Q and

       A2: for u be Element of ( TOP-REAL 3) st u is non zero & Q = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 ;

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

       A3: u is non zero and

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

      

       A5: ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 by A1, A2, A3, A4;

      

       A6: (u . 3) <> 0 by A3, A4, Th67;

       |[(u . 1), (u . 2), ( - (u . 3))]| is non zero

      proof

        assume |[(u . 1), (u . 2), ( - (u . 3))]| is zero;

        then (u . 3) = 0 by EUCLID_5: 4, FINSEQ_1: 78;

        hence contradiction by A3, A4, Th67;

      end;

      then

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

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

      take R;

      

       A7: R <> P

      proof

        assume R = P;

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

        then

        consider a be Real such that a <> 0 and

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

        

         A9: ( - (u . 3)) = (v `3 ) by EUCLID_5: 2

        .= ((a * u) . 3) by A8, EUCLID_5:def 3

        .= (a * (u . 3)) by RVSUM_1: 44;

        ((a + 1) * (u . 3)) = 0 by A9;

        then (a + 1) = 0 by A6;

        then

         A10: a = ( - 1);

        

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

        .= ((a * u) . 1) by A8, EUCLID_5:def 1

        .= (a * (u . 1)) by RVSUM_1: 44;

        

         A12: (u . 2) = (v `2 ) by EUCLID_5: 2

        .= ((a * u) . 2) by A8, EUCLID_5:def 2

        .= (a * (u . 2)) by RVSUM_1: 44;

         0 = (((((((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 A5, PASCAL:def 1

        .= (( - 1) * ((u . 3) ^2 )) by A11, A10, A12;

        hence contradiction by A6;

      end;

      for w be Element of ( TOP-REAL 3) st w is non zero & R = ( Dir w) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,w)) = 0

      proof

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

        assume that

         A13: w is non zero and

         A14: R = ( Dir w);

         are_Prop (v,w) by A13, A14, ANPROJ_1: 22;

        then

        consider b be Real such that b <> 0 and

         A15: w = (b * v) by ANPROJ_1: 1;

        

         A16: (w . 1) = (b * (v . 1)) by A15, RVSUM_1: 44

        .= (b * (v `1 )) by EUCLID_5:def 1

        .= (b * (u . 1)) by EUCLID_5: 2;

        

         A17: (w . 2) = (b * (v . 2)) by A15, RVSUM_1: 44

        .= (b * (v `2 )) by EUCLID_5:def 2

        .= (b * (u . 2)) by EUCLID_5: 2;

        

         A18: (w . 3) = (b * (v . 3)) by A15, RVSUM_1: 44

        .= (b * (v `3 )) by EUCLID_5:def 3

        .= (b * ( - (u . 3))) by EUCLID_5: 2;

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

        .= ((b * b) * (((((((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 A16, A17, A18

        .= ((b * b) * ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u))) by PASCAL:def 1

        .= 0 by A5;

        hence thesis;

      end;

      then R 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)) = 0 };

      hence thesis by A7, PASCAL:def 2;

    end;

    theorem :: BKMODEL1:91

    for a,b be Real st ((a ^2 ) + (b ^2 )) = 1 holds |[( - b), a, 0 ]| is non zero

    proof

      let a,b be Real;

      assume

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

      assume |[( - b), a, 0 ]| is zero;

      then ( - b) = 0 & a = 0 by EUCLID_5: 4, FINSEQ_1: 78;

      hence contradiction by A1;

    end;

    theorem :: BKMODEL1:92

    for P,Q,R be Element of absolute st (P,Q,R) are_mutually_distinct holds not (P,Q,R) are_collinear

    proof

      let P,Q,R be Element of absolute ;

      assume

       A1: (P,Q,R) are_mutually_distinct ;

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

       A2: up is non zero and

       A3: P = ( Dir up) by ANPROJ_1: 26;

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

       A4: uq is non zero and

       A5: Q = ( Dir uq) by ANPROJ_1: 26;

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

       A6: ur is non zero and

       A7: R = ( Dir ur) by ANPROJ_1: 26;

      reconsider up1 = (up `1 ), up2 = (up `2 ), up3 = (up `3 ), uq1 = (uq `1 ), uq2 = (uq `2 ), uq3 = (uq `3 ), ur1 = (ur `1 ), ur2 = (ur `2 ), ur3 = (ur `3 ) as Real;

      (up . 3) <> 0 & (uq . 3) <> 0 & (ur . 3) <> 0 by A2, A3, A4, A5, A6, A7, Th67;

      then

       A8: up3 <> 0 & uq3 <> 0 & ur3 <> 0 by EUCLID_5:def 3;

      reconsider vp1 = (up1 / up3), vp2 = (up2 / up3), vq1 = (uq1 / uq3), vq2 = (uq2 / uq3), vr1 = (ur1 / ur3), vr2 = (ur2 / ur3) as Real;

      reconsider vp = |[vp1, vp2, 1]|, vq = |[vq1, vq2, 1]|, vr = |[vr1, vr2, 1]| as non zero Element of ( TOP-REAL 3) by Th36;

      

       A9: (vp `3 ) = 1 & (vq `3 ) = 1 & (vr `3 ) = 1 by EUCLID_5: 2;

      then

       A10: (vp . 3) = 1 & (vq . 3) = 1 & (vr . 3) = 1 by EUCLID_5:def 3;

      

       A11: P = ( Dir vp) & Q = ( Dir vq) & R = ( Dir vr)

      proof

        thus P = ( Dir vp)

        proof

           are_Prop (up,vp)

          proof

            (up3 * vp) = |[(up3 * (up1 / up3)), (up3 * (up2 / up3)), (up3 * 1)]| by EUCLID_5: 8

            .= |[up1, (up3 * (up2 / up3)), (up3 * 1)]| by A8, XCMPLX_1: 87

            .= |[up1, up2, (up3 * 1)]| by A8, XCMPLX_1: 87

            .= up by EUCLID_5: 3;

            hence thesis by A8, ANPROJ_1: 1;

          end;

          hence thesis by A2, A3, ANPROJ_1: 22;

        end;

        thus Q = ( Dir vq)

        proof

           are_Prop (uq,vq)

          proof

            (uq3 * vq) = |[(uq3 * (uq1 / uq3)), (uq3 * (uq2 / uq3)), (uq3 * 1)]| by EUCLID_5: 8

            .= |[uq1, (uq3 * (uq2 / uq3)), (uq3 * 1)]| by A8, XCMPLX_1: 87

            .= |[uq1, uq2, (uq3 * 1)]| by A8, XCMPLX_1: 87

            .= uq by EUCLID_5: 3;

            hence thesis by A8, ANPROJ_1: 1;

          end;

          hence thesis by A4, A5, ANPROJ_1: 22;

        end;

        thus R = ( Dir vr)

        proof

           are_Prop (ur,vr)

          proof

            (ur3 * vr) = |[(ur3 * (ur1 / ur3)), (ur3 * (ur2 / ur3)), (ur3 * 1)]| by EUCLID_5: 8

            .= |[ur1, (ur3 * (ur2 / ur3)), (ur3 * 1)]| by A8, XCMPLX_1: 87

            .= |[ur1, ur2, (ur3 * 1)]| by A8, XCMPLX_1: 87

            .= ur by EUCLID_5: 3;

            hence thesis by A8, ANPROJ_1: 1;

          end;

          hence thesis by A6, A7, ANPROJ_1: 22;

        end;

      end;

      assume (P,Q,R) are_collinear ;

      then

      consider tp,tq,tr be Element of ( TOP-REAL 3) such that

       A12: P = ( Dir tp) & Q = ( Dir tq) & R = ( Dir tr) and

       A13: not tp is zero & not tq is zero & not tr is zero and

       A14: ex a1,b1,c1 be Real st (((a1 * tp) + (b1 * tq)) + (c1 * tr)) = ( 0. ( TOP-REAL 3)) & (a1 <> 0 or b1 <> 0 or c1 <> 0 ) by ANPROJ_8: 11;

      consider a1,b1,c1 be Real such that

       A15: (((a1 * tp) + (b1 * tq)) + (c1 * tr)) = ( 0. ( TOP-REAL 3)) and

       A16: (a1 <> 0 or b1 <> 0 or c1 <> 0 ) by A14;

      

       A17: are_Prop (tp,vp) & are_Prop (tq,vq) & are_Prop (tr,vr) by A12, A13, A11, ANPROJ_1: 22;

      consider lp be Real such that

       A18: lp <> 0 and

       A19: tp = (lp * vp) by A17, ANPROJ_1: 1;

      consider lq be Real such that

       A20: lq <> 0 and

       A21: tq = (lq * vq) by A17, ANPROJ_1: 1;

      consider lr be Real such that

       A22: lr <> 0 and

       A23: tr = (lr * vr) by A17, ANPROJ_1: 1;

      reconsider A = |[(vp `1 ), (vp `2 )]|, B = |[(vq `1 ), (vq `2 )]|, C = |[(vr `1 ), (vr `2 )]| as Element of ( TOP-REAL 2);

      

       A24: (B . 1) = (B `1 ) by EUCLID:def 9

      .= (vq `1 ) by EUCLID: 52

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

      

       A25: (B . 2) = (B `2 ) by EUCLID:def 10

      .= (vq `2 ) by EUCLID: 52

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

      

       A26: (C . 1) = (C `1 ) by EUCLID:def 9

      .= (vr `1 ) by EUCLID: 52

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

      

       A27: (C . 2) = (C `2 ) by EUCLID:def 10

      .= (vr `2 ) by EUCLID: 52

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

      

       A28: (A . 1) = (A `1 ) by EUCLID:def 9

      .= (vp `1 ) by EUCLID: 52

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

      

       A29: (A . 2) = (A `2 ) by EUCLID:def 10

      .= (vp `2 ) by EUCLID: 52

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

      

       A30: A <> B

      proof

        assume A = B;

        then

         A30BIS: (vp `1 ) = (vq `1 ) & (vp `2 ) = (vq `2 ) by FINSEQ_1: 77;

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

        .= vq by A9, A30BIS, EUCLID_5: 3;

        hence contradiction by A11, A1;

      end;

      

       A31: A <> C

      proof

        assume A = C;

        then

         A31BIS: (vp `1 ) = (vr `1 ) & (vp `2 ) = (vr `2 ) by FINSEQ_1: 77;

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

        .= vr by A9, A31BIS, EUCLID_5: 3;

        hence contradiction by A11, A1;

      end;

      

       A32: B <> C

      proof

        assume B = C;

        then

         A32BIS: (vq `1 ) = (vr `1 ) & (vq `2 ) = (vr `2 ) by FINSEQ_1: 77;

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

        .= vr by A9, A32BIS, EUCLID_5: 3;

        hence contradiction by A11, A1;

      end;

      

       A34: A in ( Sphere (( 0. ( TOP-REAL 2)),1))

      proof

        

         A35: ( qfconic (1,1,( - 1), 0 , 0 , 0 ,vp)) = 0

        proof

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

          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)) = 0 } by PASCAL:def 2;

          then ex PP be Point of ( ProjectiveSpace ( TOP-REAL 3)) st P = PP & for u be Element of ( TOP-REAL 3) st u is non zero & PP = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 ;

          hence thesis by A11;

        end;

        (vp . 1) = (vp `1 ) & (vp . 2) = (vp `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;

        hence A in ( Sphere (( 0. ( TOP-REAL 2)),1)) by A35, A10, Th70;

      end;

      

       A36: ( qfconic (1,1,( - 1), 0 , 0 , 0 ,vq)) = 0

      proof

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

        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)) = 0 } by PASCAL:def 2;

        then ex QP be Point of ( ProjectiveSpace ( TOP-REAL 3)) st Q = QP & for u be Element of ( TOP-REAL 3) st u is non zero & QP = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 ;

        hence thesis by A11;

      end;

      (vq . 1) = (vq `1 ) & (vq . 2) = (vq `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;

      then

       A37: B in ( Sphere (( 0. ( TOP-REAL 2)),1)) by A36, A10, Th70;

      

       A38: C in ( Sphere (( 0. ( TOP-REAL 2)),1))

      proof

        

         A39: ( qfconic (1,1,( - 1), 0 , 0 , 0 ,vr)) = 0

        proof

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

          then R 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)) = 0 } by PASCAL:def 2;

          then ex RP be Point of ( ProjectiveSpace ( TOP-REAL 3)) st R = RP & for u be Element of ( TOP-REAL 3) st u is non zero & RP = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 ;

          hence thesis by A11;

        end;

        (vr . 1) = (vr `1 ) & (vr . 2) = (vr `2 ) by EUCLID_5:def 1, EUCLID_5:def 2;

        hence C in ( Sphere (( 0. ( TOP-REAL 2)),1)) by A39, A10, Th70;

      end;

      

       A40: (( halfline (B,C)) /\ ( Sphere (( 0. ( TOP-REAL 2)),1))) = {B, C} & (( halfline (C,B)) /\ ( Sphere (( 0. ( TOP-REAL 2)),1))) = {C, B} & (( halfline (A,C)) /\ ( Sphere (( 0. ( TOP-REAL 2)),1))) = {A, C} & (( halfline (C,A)) /\ ( Sphere (( 0. ( TOP-REAL 2)),1))) = {C, A} & (( halfline (A,B)) /\ ( Sphere (( 0. ( TOP-REAL 2)),1))) = {A, B} & (( halfline (B,A)) /\ ( Sphere (( 0. ( TOP-REAL 2)),1))) = {B, A} by A37, A38, A34, TOPREAL9: 36;

      per cases by A16;

        suppose a1 <> 0 ;

        

        then

         A41: (lp * vp) = (((( - b1) / a1) * (lq * vq)) + ((( - c1) / a1) * (lr * vr))) by A19, A21, A23, A15, ANPROJ_8: 12

        .= ((((( - b1) / a1) * lq) * vq) + ((( - c1) / a1) * (lr * vr))) by RVSUM_1: 49

        .= ((((( - b1) / a1) * lq) * vq) + (((( - c1) / a1) * lr) * vr)) by RVSUM_1: 49;

        reconsider m1 = ((1 / lp) * ((( - b1) / a1) * lq)), m2 = ((1 / lp) * ((( - c1) / a1) * lr)) as Real;

        1 = (lp / lp) by A18, XCMPLX_1: 60

        .= ((1 / lp) * lp) by XCMPLX_1: 99;

        

        then

         A42: vp = (((1 / lp) * lp) * vp) by RVSUM_1: 52

        .= ((1 / lp) * ((((( - b1) / a1) * lq) * vq) + (((( - c1) / a1) * lr) * vr))) by A41, RVSUM_1: 49

        .= (((1 / lp) * (((( - b1) / a1) * lq) * vq)) + ((1 / lp) * (((( - c1) / a1) * lr) * vr))) by RVSUM_1: 51

        .= ((((1 / lp) * ((( - b1) / a1) * lq)) * vq) + ((1 / lp) * (((( - c1) / a1) * lr) * vr))) by RVSUM_1: 49

        .= ((m1 * vq) + (m2 * vr)) by RVSUM_1: 49;

        

         A43: m1 = (1 - m2)

        proof

          ((m1 * vq) + (m2 * vr)) = ( |[(m1 * (vq `1 )), (m1 * (vq `2 )), (m1 * (vq `3 ))]| + (m2 * vr)) by EUCLID_5: 7

          .= ( |[(m1 * (vq `1 )), (m1 * (vq `2 )), (m1 * (vq `3 ))]| + |[(m2 * (vr `1 )), (m2 * (vr `2 )), (m2 * (vr `3 ))]|) by EUCLID_5: 7

          .= |[((m1 * (vq `1 )) + (m2 * (vr `1 ))), ((m1 * (vq `2 )) + (m2 * (vr `2 ))), ((m1 * (vq `3 )) + (m2 * (vr `3 )))]| by EUCLID_5: 6;

          then (vp `3 ) = ((m1 * (vq `3 )) + (m2 * (vr `3 ))) by A42, EUCLID_5: 14;

          hence thesis by A9;

        end;

        per cases ;

          suppose

           A44: 0 <= m2;

          

           A45: A in ( halfline (B,C))

          proof

            reconsider tu = ((1 - m2) * vq), tv = (m2 * vr) as Element of ( TOP-REAL 3);

            

             A46: (((1 - m2) * vq) . 1) = ((1 - m2) * (vq . 1)) by RVSUM_1: 44;

            

             A47: (tu `1 ) = (tu . 1) & (tv `1 ) = (tv . 1) by EUCLID_5:def 1;

            

             A48: (A `1 ) = (vp `1 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `1 ) by A43, A42, EUCLID_5: 5

            .= ((tu . 1) + (tv . 1)) by A47, EUCLID_5: 2

            .= (((1 - m2) * (B . 1)) + (m2 * (C . 1))) by A46, RVSUM_1: 44, A24, A26;

            

             A49: (((1 - m2) * vq) . 2) = ((1 - m2) * (vq . 2)) by RVSUM_1: 44;

            

             A50: (tu `2 ) = (tu . 2) & (tv `2 ) = (tv . 2) by EUCLID_5:def 2;

            

             A51: (A `2 ) = (vp `2 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `2 ) by A43, A42, EUCLID_5: 5

            .= ((tu . 2) + (tv . 2)) by A50, EUCLID_5: 2

            .= (((1 - m2) * (B . 2)) + (m2 * (C . 2))) by A49, A25, A27, RVSUM_1: 44;

            

             A52: B = |[(B `1 ), (B `2 )]| by EUCLID: 53

            .= |[(B `1 ), (B . 2)]| by EUCLID:def 10

            .= |[(B . 1), (B . 2)]| by EUCLID:def 9;

            

             A53: C = |[(C `1 ), (C `2 )]| by EUCLID: 53

            .= |[(C `1 ), (C . 2)]| by EUCLID:def 10

            .= |[(C . 1), (C . 2)]| by EUCLID:def 9;

            A = |[(((1 - m2) * (B . 1)) + (m2 * (C . 1))), (((1 - m2) * (B . 2)) + (m2 * (C . 2)))]| by A48, A51, EUCLID: 53

            .= ( |[((1 - m2) * (B . 1)), ((1 - m2) * (B . 2))]| + |[(m2 * (C . 1)), (m2 * (C . 2))]|) by EUCLID: 56

            .= (((1 - m2) * |[(B . 1), (B . 2)]|) + |[(m2 * (C . 1)), (m2 * (C . 2))]|) by EUCLID: 58

            .= (((1 - m2) * B) + (m2 * C)) by A52, A53, EUCLID: 58;

            hence thesis by A44, TOPREAL9: 26;

          end;

          A in (( halfline (B,C)) /\ ( Sphere (( 0. ( TOP-REAL 2)),1))) by A45, A34, XBOOLE_0:def 4;

          hence contradiction by A30, A31, A40, TARSKI:def 2;

        end;

          suppose

           A54: m2 < 0 ;

          set m3 = (1 - m2);

          A in ( halfline (C,B))

          proof

            reconsider tu = ((1 - m3) * vr), tv = (m3 * vq) as Element of ( TOP-REAL 3);

            

             A55: (((1 - m3) * vr) . 1) = ((1 - m3) * (vr . 1)) by RVSUM_1: 44;

            

             A56: (tu `1 ) = (tu . 1) & (tv `1 ) = (tv . 1) by EUCLID_5:def 1;

            

             A56b: (A `1 ) = (vp `1 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `1 ) by A43, A42, EUCLID_5: 5

            .= ((tu . 1) + (tv . 1)) by EUCLID_5: 2, A56

            .= (((1 - m3) * (C . 1)) + (m3 * (B . 1))) by A24, A26, A55, RVSUM_1: 44;

            

             A57: (((1 - m3) * vr) . 2) = ((1 - m3) * (vr . 2)) by RVSUM_1: 44;

            

             A58: (tu `2 ) = (tu . 2) & (tv `2 ) = (tv . 2) by EUCLID_5:def 2;

            

             A59: (A `2 ) = (vp `2 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `2 ) by A43, A42, EUCLID_5: 5

            .= ((tu `2 ) + (tv `2 )) by EUCLID_5: 2

            .= (((1 - m3) * (C . 2)) + (m3 * (B . 2))) by A57, A58, RVSUM_1: 44, A25, A27;

            

             A60: B = |[(B `1 ), (B `2 )]| by EUCLID: 53

            .= |[(B `1 ), (B . 2)]| by EUCLID:def 10

            .= |[(B . 1), (B . 2)]| by EUCLID:def 9;

            

             A61: C = |[(C `1 ), (C `2 )]| by EUCLID: 53

            .= |[(C `1 ), (C . 2)]| by EUCLID:def 10

            .= |[(C . 1), (C . 2)]| by EUCLID:def 9;

            A = |[(((1 - m3) * (C . 1)) + (m3 * (B . 1))), (((1 - m3) * (C . 2)) + (m3 * (B . 2)))]| by A56b, A59, EUCLID: 53

            .= ( |[((1 - m3) * (C . 1)), ((1 - m3) * (C . 2))]| + |[(m3 * (B . 1)), (m3 * (B . 2))]|) by EUCLID: 56

            .= (((1 - m3) * |[(C . 1), (C . 2)]|) + |[(m3 * (B . 1)), (m3 * (B . 2))]|) by EUCLID: 58

            .= (((1 - m3) * C) + (m3 * B)) by A60, A61, EUCLID: 58;

            hence thesis by A54, TOPREAL9: 26;

          end;

          then A in {C, B} by A40, A34, XBOOLE_0:def 4;

          hence contradiction by A30, A31, TARSKI:def 2;

        end;

      end;

        suppose

         A62: b1 <> 0 ;

        (((b1 * tq) + (a1 * tp)) + (c1 * tr)) = ( 0. ( TOP-REAL 3)) by A15;

        

        then

         A63: (lq * vq) = (((( - a1) / b1) * (lp * vp)) + ((( - c1) / b1) * (lr * vr))) by A19, A21, A23, A62, ANPROJ_8: 12

        .= ((((( - a1) / b1) * lp) * vp) + ((( - c1) / b1) * (lr * vr))) by RVSUM_1: 49

        .= ((((( - a1) / b1) * lp) * vp) + (((( - c1) / b1) * lr) * vr)) by RVSUM_1: 49;

        reconsider m1 = ((1 / lq) * ((( - a1) / b1) * lp)), m2 = ((1 / lq) * ((( - c1) / b1) * lr)) as Real;

        1 = (lq / lq) by A20, XCMPLX_1: 60

        .= ((1 / lq) * lq) by XCMPLX_1: 99;

        

        then

         A65: vq = (((1 / lq) * lq) * vq) by RVSUM_1: 52

        .= ((1 / lq) * ((((( - a1) / b1) * lp) * vp) + (((( - c1) / b1) * lr) * vr))) by A63, RVSUM_1: 49

        .= (((1 / lq) * (((( - a1) / b1) * lp) * vp)) + ((1 / lq) * (((( - c1) / b1) * lr) * vr))) by RVSUM_1: 51

        .= ((((1 / lq) * ((( - a1) / b1) * lp)) * vp) + ((1 / lq) * (((( - c1) / b1) * lr) * vr))) by RVSUM_1: 49

        .= ((m1 * vp) + (m2 * vr)) by RVSUM_1: 49;

        

         A66: m1 = (1 - m2)

        proof

          ((m1 * vp) + (m2 * vr)) = ( |[(m1 * (vp `1 )), (m1 * (vp `2 )), (m1 * (vp `3 ))]| + (m2 * vr)) by EUCLID_5: 7

          .= ( |[(m1 * (vp `1 )), (m1 * (vp `2 )), (m1 * (vp `3 ))]| + |[(m2 * (vr `1 )), (m2 * (vr `2 )), (m2 * (vr `3 ))]|) by EUCLID_5: 7

          .= |[((m1 * (vp `1 )) + (m2 * (vr `1 ))), ((m1 * (vp `2 )) + (m2 * (vr `2 ))), ((m1 * (vp `3 )) + (m2 * (vr `3 )))]| by EUCLID_5: 6;

          then 1 = ((m1 * 1) + (m2 * 1)) by A9, A65, EUCLID_5: 14;

          hence thesis;

        end;

        per cases ;

          suppose

           A67: 0 <= m2;

          B in ( halfline (A,C))

          proof

            reconsider tu = ((1 - m2) * vp), tv = (m2 * vr) as Element of ( TOP-REAL 3);

            

             A68: (((1 - m2) * vp) . 1) = ((1 - m2) * (vp . 1)) by RVSUM_1: 44;

            

             A69: (tu `1 ) = (tu . 1) & (tv `1 ) = (tv . 1) by EUCLID_5:def 1;

            

             A70: (B `1 ) = (vq `1 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `1 ) by A66, A65, EUCLID_5: 5

            .= ((tu `1 ) + (tv `1 )) by EUCLID_5: 2

            .= (((1 - m2) * (A . 1)) + (m2 * (C . 1))) by A26, A28, A68, A69, RVSUM_1: 44;

            

             A71: (((1 - m2) * vp) . 2) = ((1 - m2) * (vp . 2)) by RVSUM_1: 44;

            

             A72: (tu `2 ) = (tu . 2) & (tv `2 ) = (tv . 2) by EUCLID_5:def 2;

            

             A73: (B `2 ) = (vq `2 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `2 ) by A66, A65, EUCLID_5: 5

            .= ((tu `2 ) + (tv `2 )) by EUCLID_5: 2

            .= (((1 - m2) * (A . 2)) + (m2 * (C . 2))) by A27, A29, A71, A72, RVSUM_1: 44;

            

             A74: A = |[(A `1 ), (A `2 )]| by EUCLID: 53

            .= |[(A `1 ), (A . 2)]| by EUCLID:def 10

            .= |[(A . 1), (A . 2)]| by EUCLID:def 9;

            

             A75: C = |[(C `1 ), (C `2 )]| by EUCLID: 53

            .= |[(C `1 ), (C . 2)]| by EUCLID:def 10

            .= |[(C . 1), (C . 2)]| by EUCLID:def 9;

            B = |[(((1 - m2) * (A . 1)) + (m2 * (C . 1))), (((1 - m2) * (A . 2)) + (m2 * (C . 2)))]| by A70, A73, EUCLID: 53

            .= ( |[((1 - m2) * (A . 1)), ((1 - m2) * (A . 2))]| + |[(m2 * (C . 1)), (m2 * (C . 2))]|) by EUCLID: 56

            .= (((1 - m2) * |[(A . 1), (A . 2)]|) + |[(m2 * (C . 1)), (m2 * (C . 2))]|) by EUCLID: 58

            .= (((1 - m2) * A) + (m2 * C)) by A74, A75, EUCLID: 58;

            hence thesis by A67, TOPREAL9: 26;

          end;

          then B in {A, C} by A40, A37, XBOOLE_0:def 4;

          hence contradiction by A30, A32, TARSKI:def 2;

        end;

          suppose

           A76: m2 < 0 ;

          set m3 = (1 - m2);

          B in ( halfline (C,A))

          proof

            reconsider tu = ((1 - m3) * vr), tv = (m3 * vp) as Element of ( TOP-REAL 3);

            

             A77: (((1 - m3) * vr) . 1) = ((1 - m3) * (vr . 1)) by RVSUM_1: 44;

            

             A78: (tu `1 ) = (tu . 1) & (tv `1 ) = (tv . 1) by EUCLID_5:def 1;

            

             A79: (B `1 ) = (vq `1 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `1 ) by EUCLID_5: 5, A66, A65

            .= ((tu `1 ) + (tv `1 )) by EUCLID_5: 2

            .= (((1 - m3) * (C . 1)) + (m3 * (A . 1))) by A26, A28, A77, A78, RVSUM_1: 44;

            

             A80: (((1 - m3) * vr) . 2) = ((1 - m3) * (vr . 2)) by RVSUM_1: 44;

            

             A81: (tu `2 ) = (tu . 2) & (tv `2 ) = (tv . 2) by EUCLID_5:def 2;

            

             A82: (B `2 ) = (vq `2 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `2 ) by A66, A65, EUCLID_5: 5

            .= ((tu `2 ) + (tv `2 )) by EUCLID_5: 2

            .= (((1 - m3) * (C . 2)) + (m3 * (A . 2))) by A27, A29, A80, A81, RVSUM_1: 44;

            

             A83: A = |[(A `1 ), (A `2 )]| by EUCLID: 53

            .= |[(A `1 ), (A . 2)]| by EUCLID:def 10

            .= |[(A . 1), (A . 2)]| by EUCLID:def 9;

            

             A84: C = |[(C `1 ), (C `2 )]| by EUCLID: 53

            .= |[(C `1 ), (C . 2)]| by EUCLID:def 10

            .= |[(C . 1), (C . 2)]| by EUCLID:def 9;

            B = |[(((1 - m3) * (C . 1)) + (m3 * (A . 1))), (((1 - m3) * (C . 2)) + (m3 * (A . 2)))]| by A79, A82, EUCLID: 53

            .= ( |[((1 - m3) * (C . 1)), ((1 - m3) * (C . 2))]| + |[(m3 * (A . 1)), (m3 * (A . 2))]|) by EUCLID: 56

            .= (((1 - m3) * |[(C . 1), (C . 2)]|) + |[(m3 * (A . 1)), (m3 * (A . 2))]|) by EUCLID: 58

            .= (((1 - m3) * C) + (m3 * A)) by A83, A84, EUCLID: 58;

            hence thesis by A76, TOPREAL9: 26;

          end;

          then B in {C, A} by A40, A37, XBOOLE_0:def 4;

          hence contradiction by A30, A32, TARSKI:def 2;

        end;

      end;

        suppose

         A85: c1 <> 0 ;

        (((c1 * tr) + (a1 * tp)) + (b1 * tq)) = ( 0. ( TOP-REAL 3)) by A15, RVSUM_1: 15;

        

        then

         A86: (lr * vr) = (((( - a1) / c1) * (lp * vp)) + ((( - b1) / c1) * (lq * vq))) by A19, A21, A23, A85, ANPROJ_8: 12

        .= ((((( - a1) / c1) * lp) * vp) + ((( - b1) / c1) * (lq * vq))) by RVSUM_1: 49

        .= ((((( - a1) / c1) * lp) * vp) + (((( - b1) / c1) * lq) * vq)) by RVSUM_1: 49;

        reconsider m1 = ((1 / lr) * ((( - a1) / c1) * lp)), m2 = ((1 / lr) * ((( - b1) / c1) * lq)) as Real;

        1 = (lr / lr) by A22, XCMPLX_1: 60

        .= ((1 / lr) * lr) by XCMPLX_1: 99;

        

        then

         A87: vr = (((1 / lr) * lr) * vr) by RVSUM_1: 52

        .= ((1 / lr) * ((((( - a1) / c1) * lp) * vp) + (((( - b1) / c1) * lq) * vq))) by A86, RVSUM_1: 49

        .= (((1 / lr) * (((( - a1) / c1) * lp) * vp)) + ((1 / lr) * (((( - b1) / c1) * lq) * vq))) by RVSUM_1: 51

        .= ((((1 / lr) * ((( - a1) / c1) * lp)) * vp) + ((1 / lr) * (((( - b1) / c1) * lq) * vq))) by RVSUM_1: 49

        .= ((m1 * vp) + (m2 * vq)) by RVSUM_1: 49;

        

         A88: m1 = (1 - m2)

        proof

          ((m1 * vp) + (m2 * vq)) = ( |[(m1 * (vp `1 )), (m1 * (vp `2 )), (m1 * (vp `3 ))]| + (m2 * vq)) by EUCLID_5: 7

          .= ( |[(m1 * (vp `1 )), (m1 * (vp `2 )), (m1 * (vp `3 ))]| + |[(m2 * (vq `1 )), (m2 * (vq `2 )), (m2 * (vq `3 ))]|) by EUCLID_5: 7

          .= |[((m1 * (vp `1 )) + (m2 * (vq `1 ))), ((m1 * (vp `2 )) + (m2 * (vq `2 ))), ((m1 * (vp `3 )) + (m2 * (vq `3 )))]| by EUCLID_5: 6;

          then 1 = ((m1 * 1) + (m2 * 1)) by A87, EUCLID_5: 14, A9;

          hence thesis;

        end;

        per cases ;

          suppose

           A89: 0 <= m2;

          C in ( halfline (A,B))

          proof

            reconsider tu = ((1 - m2) * vp), tv = (m2 * vq) as Element of ( TOP-REAL 3);

            

             A90: (((1 - m2) * vp) . 1) = ((1 - m2) * (vp . 1)) by RVSUM_1: 44;

            

             A91: (tu `1 ) = (tu . 1) & (tv `1 ) = (tv . 1) by EUCLID_5:def 1;

            

             A92: (C `1 ) = (vr `1 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `1 ) by A88, A87, EUCLID_5: 5

            .= ((tu . 1) + (tv . 1)) by A91, EUCLID_5: 2

            .= (((1 - m2) * (A . 1)) + (m2 * (B . 1))) by A24, A28, A90, RVSUM_1: 44;

            

             A93: (((1 - m2) * vp) . 2) = ((1 - m2) * (vp . 2)) by RVSUM_1: 44;

            

             A94: (tu `2 ) = (tu . 2) & (tv `2 ) = (tv . 2) by EUCLID_5:def 2;

            

             A95: (C `2 ) = (vr `2 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `2 ) by A88, A87, EUCLID_5: 5

            .= ((tu `2 ) + (tv `2 )) by EUCLID_5: 2

            .= (((1 - m2) * (A . 2)) + (m2 * (B . 2))) by A25, A29, A93, A94, RVSUM_1: 44;

            

             A96: A = |[(A `1 ), (A `2 )]| by EUCLID: 53

            .= |[(A `1 ), (A . 2)]| by EUCLID:def 10

            .= |[(A . 1), (A . 2)]| by EUCLID:def 9;

            

             A97: B = |[(B `1 ), (B `2 )]| by EUCLID: 53

            .= |[(B `1 ), (B . 2)]| by EUCLID:def 10

            .= |[(B . 1), (B . 2)]| by EUCLID:def 9;

            C = |[(C `1 ), (C `2 )]| by EUCLID: 53

            .= ( |[((1 - m2) * (A . 1)), ((1 - m2) * (A . 2))]| + |[(m2 * (B . 1)), (m2 * (B . 2))]|) by A92, A95, EUCLID: 56

            .= (((1 - m2) * |[(A . 1), (A . 2)]|) + |[(m2 * (B . 1)), (m2 * (B . 2))]|) by EUCLID: 58

            .= (((1 - m2) * A) + (m2 * B)) by EUCLID: 58, A96, A97;

            hence thesis by A89, TOPREAL9: 26;

          end;

          then C in {A, B} by A40, A38, XBOOLE_0:def 4;

          hence contradiction by A31, A32, TARSKI:def 2;

        end;

          suppose

           A98: m2 < 0 ;

          set m3 = (1 - m2);

          C in ( halfline (B,A))

          proof

            reconsider tu = ((1 - m3) * vq), tv = (m3 * vp) as Element of ( TOP-REAL 3);

            

             A99: (((1 - m3) * vq) . 1) = ((1 - m3) * (vq . 1)) by RVSUM_1: 44;

            

             A100: (tu `1 ) = (tu . 1) & (tv `1 ) = (tv . 1) by EUCLID_5:def 1;

            

             A101: (C `1 ) = (vr `1 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `1 ) by A88, A87, EUCLID_5: 5

            .= ((tu . 1) + (tv . 1)) by A100, EUCLID_5: 2

            .= (((1 - m3) * (B . 1)) + (m3 * (A . 1))) by A24, A28, A99, RVSUM_1: 44;

            

             A102: (((1 - m3) * vq) . 2) = ((1 - m3) * (vq . 2)) by RVSUM_1: 44;

            

             A103: (tu `2 ) = (tu . 2) & (tv `2 ) = (tv . 2) by EUCLID_5:def 2;

            

             A104: (C `2 ) = (vr `2 ) by EUCLID: 52

            .= ( |[((tu `1 ) + (tv `1 )), ((tu `2 ) + (tv `2 )), ((tu `3 ) + (tv `3 ))]| `2 ) by A88, A87, EUCLID_5: 5

            .= ((tu `2 ) + (tv `2 )) by EUCLID_5: 2

            .= (((1 - m3) * (B . 2)) + (m3 * (A . 2))) by A25, A29, A102, A103, RVSUM_1: 44;

            

             A105: A = |[(A `1 ), (A `2 )]| by EUCLID: 53

            .= |[(A `1 ), (A . 2)]| by EUCLID:def 10

            .= |[(A . 1), (A . 2)]| by EUCLID:def 9;

            

             A106: B = |[(B `1 ), (B `2 )]| by EUCLID: 53

            .= |[(B `1 ), (B . 2)]| by EUCLID:def 10

            .= |[(B . 1), (B . 2)]| by EUCLID:def 9;

            C = |[(((1 - m3) * (B . 1)) + (m3 * (A . 1))), (((1 - m3) * (B . 2)) + (m3 * (A . 2)))]| by A101, A104, EUCLID: 53

            .= ( |[((1 - m3) * (B . 1)), ((1 - m3) * (B . 2))]| + |[(m3 * (A . 1)), (m3 * (A . 2))]|) by EUCLID: 56

            .= (((1 - m3) * |[(B . 1), (B . 2)]|) + |[(m3 * (A . 1)), (m3 * (A . 2))]|) by EUCLID: 58

            .= (((1 - m3) * B) + (m3 * A)) by A105, A106, EUCLID: 58;

            hence thesis by A98, TOPREAL9: 26;

          end;

          then C in {B, A} by A40, A38, XBOOLE_0:def 4;

          hence contradiction by A31, A32, TARSKI:def 2;

        end;

      end;

    end;

    theorem :: BKMODEL1:93

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

    proof

      let ra be non zero Real;

      let O,N,M be invertible Matrix of 3, F_Real ;

      assume that

       A1: O = ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 )) and

       A2: M = ( symmetric_3 (ra,ra,( - ra), 0 , 0 , 0 )) and

       A4: M = (((N @ ) * O) * N) and

       A5: (( homography M) .: absolute ) = absolute ;

      reconsider O1 = O as Matrix of 3, REAL ;

      

       A6: ( len O1) = 3 & ( width O1) = 3 by MATRIX_0: 24;

      

       A7: (( homography N) .: absolute ) c= absolute

      proof

        let x be object;

        assume x in (( homography N) .: absolute );

        then

        consider y be object such that

         A8: y in ( dom ( homography N)) and

         A9: y in absolute and

         A10: (( homography N) . y) = x by FUNCT_1:def 6;

        

         A11: ( rng ( homography N)) c= the carrier of ( ProjectiveSpace ( TOP-REAL 3)) by RELAT_1:def 19;

        reconsider y9 = y as Element of ( ProjectiveSpace ( TOP-REAL 3)) by A8;

        consider z be object such that

         A12: z in ( dom ( homography M)) and

         A13: z in absolute and

         A14: (( homography M) . z) = y by A9, A5, FUNCT_1:def 6;

        reconsider z9 = z as Element of ( ProjectiveSpace ( TOP-REAL 3)) by A12;

        

         A15: x = (( homography N) . (( homography M) . z9)) by A14, A10

        .= (( homography (N * M)) . z) by ANPROJ_9: 13;

        reconsider NM = (N * M) as invertible Matrix of 3, F_Real ;

        reconsider NMR = NM as Matrix of 3, REAL ;

        consider u,v be Element of ( TOP-REAL 3), uf be FinSequence of F_Real , p be FinSequence of (1 -tuples_on REAL ) such that

         A16: z9 = ( Dir u) & not u is zero & u = uf & p = (NM * uf) & v = ( M2F p) & not v is zero & (( homography NM) . z9) = ( Dir v) by ANPROJ_8:def 4;

        reconsider u1 = u as FinSequence of REAL by EUCLID: 24;

        u is Element of ( REAL 3) by EUCLID: 22;

        then

         A17: ( len u1) = 3 by EUCLID_8: 50;

        reconsider x9 = x as Element of ( ProjectiveSpace ( TOP-REAL 3)) by A10, A11, A8, FUNCT_1: 3;

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

         A18: not u9 is zero and

         A19: x9 = ( Dir u9) by ANPROJ_1: 26;

        reconsider uf9 = u9 as FinSequence of REAL by EUCLID: 24;

        u9 is Element of ( REAL 3) by EUCLID: 22;

        then ( len uf9) = 3 by EUCLID_8: 50;

        then

         A20: ( len uf9) = ( len O1) & ( len uf9) = ( width O1) & ( len uf9) > 0 by MATRIX_0: 24;

         are_Prop (u9,v) by A19, A18, A16, ANPROJ_1: 22, A15;

        then

        consider b be Real such that b <> 0 and

         A21: u9 = (b * v) by ANPROJ_1: 1;

        reconsider vf = v as FinSequence of REAL by EUCLID: 24;

        

         A22: v is Element of ( REAL 3) by EUCLID: 22;

        then

         A23: ( len vf) = 3 by EUCLID_8: 50;

        

         A24: ( width O1) = ( len vf) & ( len vf) > 0 by A6, A22, EUCLID_8: 50;

         |(uf9, (O1 * uf9))| = 0

        proof

          ( width O1) = ( len vf) & ( len vf) > 0 by A23, MATRIX_0: 24;

          

          then

           A25: ( len (O1 * vf)) = ( len O1) by MATRIXR1: 61

          .= 3 by MATRIX_0: 24;

          then

           A26: ( len vf) = ( len (b * (O1 * vf))) by A23, RVSUM_1: 117;

          

           A27: ( len vf) = ( len (O1 * vf)) by A25, A22, EUCLID_8: 50;

          

           A28: |(uf9, (O1 * uf9))| = |((b * vf), (b * (O1 * vf)))| by A21, A24, MATRIXR1: 59

          .= (b * |(vf, (b * (O1 * vf)))|) by A26, RVSUM_1: 121

          .= (b * (b * |((O1 * vf), vf)|)) by A27, RVSUM_1: 121;

           |(vf, (O1 * vf))| = 0

          proof

            

             A29: ( len N) > 0 & ( width N) > 0 by MATRIX_0: 24;

            

             A30: ((((N @ ) * O) * N) @ ) = ((N @ ) * (((N @ ) * O) @ )) by MATRIX14: 30

            .= ((N @ ) * ((O @ ) * ((N @ ) @ ))) by MATRIX14: 30

            .= ((N @ ) * ((O @ ) * N)) by A29, MATRIX_0: 57;

            

             A31: ( len N) = 3 & ( width N) = 3 & ( len M) = 3 & ( width M) = 3 by MATRIX_0: 24;

            

             A32: ( len (O * (N * M))) = 3 by MATRIX_0: 24;

            

             A33: ( len O) = 3 & ( width O) = 3 & ( len N) = 3 by MATRIX_0: 24;

            then

             A34: ( width (N @ )) = ( len O) & ( width O) = ( len N) by MATRIX_0: 24;

            

             A35: ( width M) = ( len (N @ )) & ( width (N @ )) = ( len (O * (N * M))) by A31, A32, MATRIX_0: 29;

            

             A36: ( width (N @ )) = ( len O) & ( width O) = ( len (N * M)) by MATRIX_0: 24, A33;

            

             A37: ( width ((N @ ) * O)) = ( len N) & ( width N) = ( len M) by A31, MATRIX_0: 24;

            

             A38: ( width M) = 3 & ( len M) = 3 by MATRIX_0: 24;

            reconsider ra3 = ((ra * ra) * ra) as Element of F_Real by XREAL_0:def 1;

            reconsider ea = ra as Element of F_Real by XREAL_0:def 1;

            

             A39: M = ( symmetric_3 (ea,ea,( - ea), 0 , 0 , 0 )) by A2;

            (O1 * NMR) = (O * (N * M)) by ANPROJ_8: 17;

            

            then

             A40: ((NMR @ ) * (O1 * NMR)) = (((N * M) @ ) * (O * (N * M))) by ANPROJ_8: 17

            .= ((((N @ ) * ((O @ ) * N)) * (N @ )) * (O * (N * (((N @ ) * O) * N)))) by A30, A4, A31, MATRIX_3: 22

            .= ((((N @ ) * (O * N)) * (N @ )) * (O * (N * (((N @ ) * O) * N)))) by A1, PASCAL: 12, MATRIX_6:def 5

            .= ((M * (N @ )) * (O * (N * (((N @ ) * O) * N)))) by A4, A34, MATRIX_3: 33

            .= (M * ((N @ ) * (O * (N * M)))) by A4, A35, MATRIX_3: 33

            .= (M * (((N @ ) * O) * (N * M))) by A36, MATRIX_3: 33

            .= (M * ((((N @ ) * O) * N) * M)) by A37, MATRIX_3: 33

            .= ((M * M) * M) by A4, A38, MATRIX_3: 33

            .= (((ea * ea) * ea) * ( symmetric_3 (1,1,( - 1), 0 , 0 , 0 ))) by A39, Th49

            .= (ra3 * O1) by Th46, A1;

            reconsider ONMRUF9 = (O1 * (NMR * u1)) as FinSequence of REAL ;

            

             A41: u is Element of ( REAL 3) by EUCLID: 22;

            then

             A42: ( len u1) = 3 by EUCLID_8: 50;

            

             A43: ( width (NMR @ )) = 3 by MATRIX_0: 24;

            

             A44: ( width NMR) = 3 & ( len NMR) = 3 by MATRIX_0: 24;

            

             A45: ( len u1) = ( width (O1 * NMR)) & ( len (O1 * NMR)) = ( width (NMR @ )) & ( len (O1 * NMR)) > 0 & ( len u1) > 0 by A42, A43, MATRIX_0: 24;

            ( len u1) = ( width NMR) & ( width O1) = ( len NMR) & ( len u1) > 0 & ( len NMR) > 0 by A41, EUCLID_8: 50, A44, MATRIX_0: 24;

            

            then

             A46: ((NMR @ ) * (O1 * (NMR * u1))) = ((NMR @ ) * ((O1 * NMR) * u1)) by MATRIXR2: 59

            .= ((ra3 * O1) * u1) by A40, A45, MATRIXR2: 59;

            ( width O1) = ( len u1) & ( len u1) > 0 by A42, MATRIX_0: 24;

            

            then ( len (O1 * u1)) = ( len O1) by MATRIXR1: 61

            .= 3 by MATRIX_0: 24;

            then

             A47: ( len u1) = ( len (O1 * u1)) by A41, EUCLID_8: 50;

            

             A48: ( len O1) = 3 by MATRIX_0: 24;

            ( width NMR) = 3 by MATRIX_0: 24;

            

            then

             A49: ( len (NMR * u1)) = ( len NMR) by A42, MATRIXR1: 61

            .= 3 by MATRIX_0: 24;

            then

             A50: ( width O1) = ( len (NMR * u1)) by MATRIX_0: 24;

            

             A51: ( len ONMRUF9) = ( len NMR) & ( len u1) = ( width NMR) & ( len u1) > 0 & ( len ONMRUF9) > 0 by A44, A41, EUCLID_8: 50, A49, A48, A50, MATRIXR1: 61;

            consider s1,s2,s3,s4,s5,s6,s7,s8,s9 be Element of F_Real such that

             A52: NM = <* <*s1, s2, s3*>, <*s4, s5, s6*>, <*s7, s8, s9*>*> by PASCAL: 3;

            consider t1,t2,t3 be Real such that

             A53: u = <*t1, t2, t3*> by EUCLID_5: 1;

            reconsider et1 = t1, et2 = t2, et3 = t3 as Element of F_Real by XREAL_0:def 1;

            

             A54: vf = <*(((s1 * et1) + (s2 * et2)) + (s3 * et3)), (((s4 * et1) + (s5 * et2)) + (s6 * et3)), (((s7 * et1) + (s8 * et2)) + (s9 * et3))*> by A16, A52, A53, PASCAL: 8;

            reconsider rs1 = s1, rs2 = s2, rs3 = s3, rs4 = s4, rs5 = s5, rs6 = s6, rs7 = s7, rs8 = s8, rs9 = s9 as Element of REAL ;

            reconsider rt1 = t1, rt2 = t2, rt3 = t3 as Element of REAL by XREAL_0:def 1;

            (NMR * u1) = <*(((rs1 * rt1) + (rs2 * rt2)) + (rs3 * rt3)), (((rs4 * rt1) + (rs5 * rt2)) + (rs6 * rt3)), (((rs7 * rt1) + (rs8 * rt2)) + (rs9 * rt3))*> by A53, A52, PASCAL: 9;

            

            then

             A55: |(vf, (O1 * vf))| = |(u1, ((NMR @ ) * ONMRUF9))| by A54, A51, MATRPROB: 48

            .= |(u1, (ra3 * (O1 * u1)))| by A17, A46, Th51

            .= (ra3 * |(u1, (O1 * u1))|) by RVSUM_1: 121, A47;

            

             A56: ( len u1) = ( len O1) & ( len u1) = ( width O1) & ( len u1) > 0 by A42, MATRIX_0: 24;

             0 = ( SumAll ( QuadraticForm (u1,O1,u1))) by A16, A13, A1, Th66

            .= |(u1, (O1 * u1))| by A56, MATRPROB: 44;

            hence thesis by A55;

          end;

          hence thesis by A28;

        end;

        then ( SumAll ( QuadraticForm (uf9,O1,uf9))) = 0 by A20, MATRPROB: 44;

        hence thesis by A18, A19, A1, Th66;

      end;

       absolute c= (( homography N) .: absolute )

      proof

        let x be object;

        assume

         A57: x in absolute ;

        then x 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)) = 0 } by PASCAL:def 2;

        then

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

         A58: x = Q and for u be Element of ( TOP-REAL 3) st u is non zero & Q = ( Dir u) holds ( qfconic (1,1,( - 1), 0 , 0 , 0 ,u)) = 0 ;

        reconsider P = (( homography (N ~ )) . Q) as Element of ( ProjectiveSpace ( TOP-REAL 3));

        

         A59: (( homography N) . P) = x by A58, ANPROJ_9: 15;

        consider u2,v2 be Element of ( TOP-REAL 3), uf2 be FinSequence of F_Real , p2 be FinSequence of (1 -tuples_on REAL ) such that

         A60: Q = ( Dir u2) & not u2 is zero & u2 = uf2 & p2 = ((N ~ ) * uf2) & v2 = ( M2F p2) & not v2 is zero & (( homography (N ~ )) . Q) = ( Dir v2) by ANPROJ_8:def 4;

        reconsider vf2 = v2 as FinSequence of REAL by EUCLID: 24;

        v2 in ( TOP-REAL 3);

        then v2 in ( REAL 3) by EUCLID: 22;

        then ( len vf2) = 3 by EUCLID_8: 50;

        then

         A61: ( len vf2) = ( len O1) & ( len vf2) = ( width O1) & ( len vf2) > 0 by MATRIX_0: 24;

         |(vf2, (O1 * vf2))| = 0

        proof

          reconsider uf3 = uf2 as FinSequence of REAL ;

          

           A62: ( len O1) = 3 & ( width O1) = 3 by MATRIX_0: 24;

          u2 in ( TOP-REAL 3);

          then

           A63: u2 in ( REAL 3) by EUCLID: 22;

          then

           A64: ( len uf2) = 3 by A60, EUCLID_8: 50;

          

           A65: ( len uf3) = ( len O1) by A63, A62, A60, EUCLID_8: 50;

          

           A66: ( SumAll ( QuadraticForm (uf3,O1,uf3))) = 0 by A1, A58, A57, A60, Th66;

          

           A67: ( len (O1 * uf3)) = ( len uf3) by A62, A65, MATRIXR1: 61;

          reconsider NR = N as Matrix of 3, REAL ;

          reconsider NI = (N ~ ) as Matrix of 3, 3, REAL ;

          

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

          

           A69: (NI * NR) = ((N ~ ) * N) by ANPROJ_8: 17

          .= ( 1. ( F_Real ,3)) by A68, MATRIX_6:def 2

          .= ( MXF2MXR ( 1. ( F_Real ,3))) by MATRIXR1:def 2

          .= ( 1_Rmatrix 3) by MATRIXR2:def 2;

          

           A70: (NR * NI) = (N * (N ~ )) by ANPROJ_8: 17

          .= ( 1. ( F_Real ,3)) by A68, MATRIX_6:def 2

          .= ( MXF2MXR ( 1. ( F_Real ,3))) by MATRIXR1:def 2

          .= ( 1_Rmatrix 3) by MATRIXR2:def 2;

          then NR is invertible by A69, MATRIXR2:def 5;

          then

           A71: ( Inv NR) = NI by A69, A70, MATRIXR2:def 6;

          reconsider ea = ra as Element of F_Real by XREAL_0:def 1;

          M = ( symmetric_3 (ea,ea,( - ea), 0 , 0 , 0 )) by A2;

          

          then

           A72: M = (ea * O) by A1, Th48

          .= (ea * ( MXR2MXF O1)) by MATRIXR1:def 1

          .= ( MXF2MXR (ea * ( MXR2MXF O1))) by MATRIXR1:def 2

          .= (ra * O1) by MATRIXR1:def 7;

          ((N @ ) * O) = ((NR @ ) * O1) by ANPROJ_8: 17;

          then

           A73: M = (((NR @ ) * O1) * NR) by A4, ANPROJ_8: 17;

          ( width ((NI @ ) * O1)) = 3 by MATRIXR2: 4;

          then

           A75: ( len uf3) = ( width NI) & ( width ((NI @ ) * O1)) = ( len NI) & ( len uf3) > 0 & ( len NI) > 0 by A64, MATRIX_0: 24;

          ( width NI) = ( len uf3) & ( len uf3) > 0 & ( len NI) = 3 by A64, MATRIX_0: 24;

          then

           A76: ( len (NI * uf3)) = 3 & ( width O1) = 3 & ( len O1) = 3 & ( width (NI @ )) = 3 by MATRIX_0: 24, MATRIXR1: 61;

          ( width NI) = ( len uf3) & ( len uf3) > 0 by A64, MATRIX_0: 24;

          

          then ( len (NI * uf3)) = ( len NI) by MATRIXR1: 61

          .= 3 by MATRIX_0: 24;

          then ( width O1) = ( len (NI * uf3)) & ( len (NI * uf3)) > 0 by MATRIX_0: 24;

          

          then ( len (O1 * (NI * uf3))) = ( len O1) by MATRIXR1: 61

          .= 3 by MATRIX_0: 24;

          then

           A77: ( len (O1 * (NI * uf3))) = ( len NI) & ( len uf3) = ( width NI) & ( len uf3) > 0 & ( len (O1 * (NI * uf3))) > 0 by A64, MATRIX_0: 24;

          vf2 = (NI * uf3)

          proof

            consider s1,s2,s3,s4,s5,s6,s7,s8,s9 be Element of F_Real such that

             A78: (N ~ ) = <* <*s1, s2, s3*>, <*s4, s5, s6*>, <*s7, s8, s9*>*> by PASCAL: 3;

            consider t1,t2,t3 be Real such that

             A79: u2 = <*t1, t2, t3*> by EUCLID_5: 1;

            reconsider et1 = t1, et2 = t2, et3 = t3 as Element of F_Real by XREAL_0:def 1;

            vf2 = <*(((s1 * et1) + (s2 * et2)) + (s3 * et3)), (((s4 * et1) + (s5 * et2)) + (s6 * et3)), (((s7 * et1) + (s8 * et2)) + (s9 * et3))*> by A60, A78, A79, PASCAL: 8;

            hence thesis by A78, A79, A60, PASCAL: 9;

          end;

          

          then |(vf2, (O1 * vf2))| = |(uf3, ((NI @ ) * (O1 * (NI * uf3))))| by A77, MATRPROB: 48

          .= |(uf3, (((NI @ ) * O1) * (NI * uf3)))| by A76, MATRIXR2: 59

          .= |(uf3, ((((NI @ ) * O1) * NI) * uf3))| by A75, MATRIXR2: 59

          .= |(uf3, (((1 / ra) * O1) * uf3))| by A73, A69, A70, MATRIXR2:def 5, A72, Th53, A71

          .= |(((1 / ra) * (O1 * uf3)), uf3)| by A64, Th51

          .= ((1 / ra) * |((O1 * uf3), uf3)|) by A67, RVSUM_1: 121

          .= ((1 / ra) * 0 ) by A66, A62, A65, MATRPROB: 44

          .= 0 ;

          hence thesis;

        end;

        then ( SumAll ( QuadraticForm (vf2,O1,vf2))) = 0 by A61, MATRPROB: 44;

        then

         A80: P in absolute by A1, A60, Th66;

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

        hence thesis by A59, A80, FUNCT_1:def 6;

      end;

      hence thesis by A7;

    end;