euclid_5.miz



    begin

    reserve x,y,z for Real,

x3,y3 for Real,

p for Point of ( TOP-REAL 3);

    theorem :: EUCLID_5:1

    

     Th1: ex x, y, z st p = <*x, y, z*>

    proof

      the carrier of ( TOP-REAL 3) = ( REAL 3) by EUCLID: 22;

      then p is Element of (3 -tuples_on REAL ) by EUCLID:def 1;

      then p in (3 -tuples_on REAL );

      then

      reconsider p as Tuple of 3, REAL by FINSEQ_2: 131;

      ex x,y,z be Element of REAL st p = <*x, y, z*> by FINSEQ_2: 103;

      hence thesis;

    end;

    definition

      let p;

      :: EUCLID_5:def1

      func p `1 -> Real equals (p . 1);

      coherence ;

      :: EUCLID_5:def2

      func p `2 -> Real equals (p . 2);

      coherence ;

      :: EUCLID_5:def3

      func p `3 -> Real equals (p . 3);

      coherence ;

    end

    notation

      let x,y,z be Real;

      synonym |[x,y,z]| for <*x,y,z*>;

    end

    definition

      let x,y,z be Real;

      :: original: |[

      redefine

      func |[x,y,z]| -> Point of ( TOP-REAL 3) ;

      coherence

      proof

        reconsider x, y, z as Element of REAL by XREAL_0:def 1;

         <*x, y, z*> is Element of (3 -tuples_on REAL ) by FINSEQ_2: 104;

        then <*x, y, z*> is Element of ( REAL 3) by EUCLID:def 1;

        hence thesis by EUCLID: 22;

      end;

    end

    theorem :: EUCLID_5:2

    

     Th2: ( |[x, y, z]| `1 ) = x & ( |[x, y, z]| `2 ) = y & ( |[x, y, z]| `3 ) = z by FINSEQ_1: 45;

    theorem :: EUCLID_5:3

    

     Th3: p = |[(p `1 ), (p `2 ), (p `3 )]|

    proof

      consider x, y, z such that

       A1: p = <*x, y, z*> by Th1;

      (p `1 ) = x & (p `2 ) = y by A1, FINSEQ_1: 45;

      hence thesis by A1, FINSEQ_1: 45;

    end;

    theorem :: EUCLID_5:4

    

     Th4: ( 0. ( TOP-REAL 3)) = |[ 0 , 0 , 0 ]|

    proof

      ( 0. ( TOP-REAL 3)) = ( 0* 3) by EUCLID: 70

      .= (3 |-> 0 ) by EUCLID:def 4

      .= <* 0 , 0 , 0 *> by FINSEQ_2: 62;

      hence thesis;

    end;

    reserve p1,p2,p3,p4 for Point of ( TOP-REAL 3),

x1,x2,y1,y2,z1,z2 for Real;

    theorem :: EUCLID_5:5

    

     Th5: (p1 + p2) = |[((p1 `1 ) + (p2 `1 )), ((p1 `2 ) + (p2 `2 )), ((p1 `3 ) + (p2 `3 ))]|

    proof

      reconsider p19 = p1, p29 = p2 as Element of ( REAL 3) by EUCLID: 22;

      ( len (p19 + p29)) = 3 by CARD_1:def 7;

      then

       A1: ( dom (p19 + p29)) = ( Seg 3) by FINSEQ_1:def 3;

      then 2 in ( dom (p19 + p29)) by FINSEQ_1: 1;

      then ((p19 + p29) . 2) = ((p19 . 2) + (p29 . 2)) by VALUED_1:def 1;

      then

       A2: ((p1 + p2) `2 ) = ((p1 `2 ) + (p2 `2 ));

      3 in ( dom (p19 + p29)) by A1, FINSEQ_1: 1;

      then ((p19 + p29) . 3) = ((p19 . 3) + (p29 . 3)) by VALUED_1:def 1;

      then

       A3: ((p1 + p2) `3 ) = ((p1 `3 ) + (p2 `3 ));

      1 in ( dom (p19 + p29)) by A1, FINSEQ_1: 1;

      then ((p19 + p29) . 1) = ((p19 . 1) + (p29 . 1)) by VALUED_1:def 1;

      then ((p1 + p2) `1 ) = ((p1 `1 ) + (p2 `1 ));

      hence thesis by A2, A3, Th3;

    end;

    theorem :: EUCLID_5:6

    

     Th6: ( |[x1, y1, z1]| + |[x2, y2, z2]|) = |[(x1 + x2), (y1 + y2), (z1 + z2)]|

    proof

      

       A1: ( |[x1, y1, z1]| `3 ) = z1 & ( |[x2, y2, z2]| `1 ) = x2 by FINSEQ_1: 45;

      

       A2: ( |[x2, y2, z2]| `2 ) = y2 & ( |[x2, y2, z2]| `3 ) = z2 by FINSEQ_1: 45;

      ( |[x1, y1, z1]| `1 ) = x1 & ( |[x1, y1, z1]| `2 ) = y1 by FINSEQ_1: 45;

      hence thesis by A1, A2, Th5;

    end;

    theorem :: EUCLID_5:7

    

     Th7: (x * p) = |[(x * (p `1 )), (x * (p `2 )), (x * (p `3 ))]|

    proof

      reconsider q = p as Element of ( REAL 3) by EUCLID: 22;

      ((x * q) . 2) = (x * (q . 2)) by RVSUM_1: 44;

      then

       A1: ((x * p) `2 ) = (x * (p `2 ));

      ((x * q) . 3) = (x * (q . 3)) by RVSUM_1: 44;

      then

       A2: ((x * p) `3 ) = (x * (p `3 ));

      ((x * q) . 1) = (x * (q . 1)) by RVSUM_1: 44;

      then ((x * p) `1 ) = (x * (p `1 ));

      hence thesis by A1, A2, Th3;

    end;

    theorem :: EUCLID_5:8

    

     Th8: (x * |[x1, y1, z1]|) = |[(x * x1), (x * y1), (x * z1)]|

    proof

      

       A1: ( |[x1, y1, z1]| `3 ) = z1 by FINSEQ_1: 45;

      ( |[x1, y1, z1]| `1 ) = x1 & ( |[x1, y1, z1]| `2 ) = y1 by FINSEQ_1: 45;

      hence thesis by A1, Th7;

    end;

    theorem :: EUCLID_5:9

    ((x * p) `1 ) = (x * (p `1 )) & ((x * p) `2 ) = (x * (p `2 )) & ((x * p) `3 ) = (x * (p `3 ))

    proof

      

       A1: ((x * p) `3 ) = ( |[(x * (p `1 )), (x * (p `2 )), (x * (p `3 ))]| `3 ) by Th7;

      ((x * p) `1 ) = ( |[(x * (p `1 )), (x * (p `2 )), (x * (p `3 ))]| `1 ) & ((x * p) `2 ) = ( |[(x * (p `1 )), (x * (p `2 )), (x * (p `3 ))]| `2 ) by Th7;

      hence thesis by A1, FINSEQ_1: 45;

    end;

    theorem :: EUCLID_5:10

    

     Th10: ( - p) = |[( - (p `1 )), ( - (p `2 )), ( - (p `3 ))]|

    proof

      

      thus ( - p) = (( - 1) * p) by RLVECT_1: 16

      .= |[(( - 1) * (p `1 )), (( - 1) * (p `2 )), (( - 1) * (p `3 ))]| by Th7

      .= |[( - (p `1 )), ( - (p `2 )), ( - (p `3 ))]|;

    end;

    theorem :: EUCLID_5:11

    ( - |[x1, y1, z1]|) = |[( - x1), ( - y1), ( - z1)]|

    proof

      

       A1: ( |[x1, y1, z1]| `3 ) = z1 by FINSEQ_1: 45;

      ( |[x1, y1, z1]| `1 ) = x1 & ( |[x1, y1, z1]| `2 ) = y1 by FINSEQ_1: 45;

      hence thesis by A1, Th10;

    end;

    theorem :: EUCLID_5:12

    

     Th12: (p1 - p2) = |[((p1 `1 ) - (p2 `1 )), ((p1 `2 ) - (p2 `2 )), ((p1 `3 ) - (p2 `3 ))]|

    proof

      

       A1: ( - p2) = |[( - (p2 `1 )), ( - (p2 `2 )), ( - (p2 `3 ))]| by Th10;

      then

       A2: (( - p2) `3 ) = ( - (p2 `3 )) by FINSEQ_1: 45;

      (( - p2) `1 ) = ( - (p2 `1 )) & (( - p2) `2 ) = ( - (p2 `2 )) by A1, FINSEQ_1: 45;

      

      hence (p1 - p2) = |[((p1 `1 ) + ( - (p2 `1 ))), ((p1 `2 ) + ( - (p2 `2 ))), ((p1 `3 ) + ( - (p2 `3 )))]| by A2, Th5

      .= |[((p1 `1 ) - (p2 `1 )), ((p1 `2 ) - (p2 `2 )), ((p1 `3 ) - (p2 `3 ))]|;

    end;

    theorem :: EUCLID_5:13

    

     Th13: ( |[x1, y1, z1]| - |[x2, y2, z2]|) = |[(x1 - x2), (y1 - y2), (z1 - z2)]|

    proof

      

       A1: ( |[x1, y1, z1]| `3 ) = z1 & ( |[x2, y2, z2]| `1 ) = x2 by FINSEQ_1: 45;

      

       A2: ( |[x2, y2, z2]| `2 ) = y2 & ( |[x2, y2, z2]| `3 ) = z2 by FINSEQ_1: 45;

      ( |[x1, y1, z1]| `1 ) = x1 & ( |[x1, y1, z1]| `2 ) = y1 by FINSEQ_1: 45;

      hence thesis by A1, A2, Th12;

    end;

    definition

      let p1, p2;

      :: EUCLID_5:def4

      func p1 <X> p2 -> Point of ( TOP-REAL 3) equals |[(((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 ))), (((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))), (((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 )))]|;

      correctness ;

    end

    theorem :: EUCLID_5:14

    p = |[x, y, z]| implies (p `1 ) = x & (p `2 ) = y & (p `3 ) = z by FINSEQ_1: 45;

    theorem :: EUCLID_5:15

    

     Th15: ( |[x1, y1, z1]| <X> |[x2, y2, z2]|) = |[((y1 * z2) - (z1 * y2)), ((z1 * x2) - (x1 * z2)), ((x1 * y2) - (y1 * x2))]|

    proof

      consider p1 such that

       A1: p1 = |[x1, y1, z1]|;

      

       A2: (p1 `3 ) = z1 by A1, FINSEQ_1: 45;

      consider p2 such that

       A3: p2 = |[x2, y2, z2]|;

      

       A4: (p2 `3 ) = z2 by A3, FINSEQ_1: 45;

      

       A5: (p2 `1 ) = x2 & (p2 `2 ) = y2 by A3, FINSEQ_1: 45;

      (p1 `1 ) = x1 & (p1 `2 ) = y1 by A1, FINSEQ_1: 45;

      hence thesis by A1, A2, A3, A5, A4;

    end;

    theorem :: EUCLID_5:16

    ((x * p1) <X> p2) = (x * (p1 <X> p2)) & ((x * p1) <X> p2) = (p1 <X> (x * p2))

    proof

      

       A1: ((x * p1) <X> p2) = ( |[(x * (p1 `1 )), (x * (p1 `2 )), (x * (p1 `3 ))]| <X> p2) by Th7

      .= ( |[(x * (p1 `1 )), (x * (p1 `2 )), (x * (p1 `3 ))]| <X> |[(p2 `1 ), (p2 `2 ), (p2 `3 )]|) by Th3

      .= |[(((x * (p1 `2 )) * (p2 `3 )) - ((x * (p1 `3 )) * (p2 `2 ))), (((x * (p1 `3 )) * (p2 `1 )) - ((x * (p1 `1 )) * (p2 `3 ))), (((x * (p1 `1 )) * (p2 `2 )) - ((x * (p1 `2 )) * (p2 `1 )))]| by Th15;

      

      then

       A2: ((x * p1) <X> p2) = |[(x * (((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 )))), (x * (((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 )))), (x * (((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 ))))]|

      .= (x * (p1 <X> p2)) by Th8;

      ((x * p1) <X> p2) = |[(((p1 `2 ) * (x * (p2 `3 ))) - ((p1 `3 ) * (x * (p2 `2 )))), (((p1 `3 ) * (x * (p2 `1 ))) - ((p1 `1 ) * (x * (p2 `3 )))), (((p1 `1 ) * (x * (p2 `2 ))) - ((p1 `2 ) * (x * (p2 `1 ))))]| by A1

      .= ( |[(p1 `1 ), (p1 `2 ), (p1 `3 )]| <X> |[(x * (p2 `1 )), (x * (p2 `2 )), (x * (p2 `3 ))]|) by Th15

      .= (p1 <X> |[(x * (p2 `1 )), (x * (p2 `2 )), (x * (p2 `3 ))]|) by Th3

      .= (p1 <X> (x * p2)) by Th7;

      hence thesis by A2;

    end;

    theorem :: EUCLID_5:17

    

     Th17: (p1 <X> p2) = ( - (p2 <X> p1))

    proof

      ( - (p2 <X> p1)) = (( - 1) * (p2 <X> p1)) by RLVECT_1: 16

      .= |[(( - 1) * (((p2 `2 ) * (p1 `3 )) - ((p2 `3 ) * (p1 `2 )))), (( - 1) * (((p2 `3 ) * (p1 `1 )) - ((p2 `1 ) * (p1 `3 )))), (( - 1) * (((p2 `1 ) * (p1 `2 )) - ((p2 `2 ) * (p1 `1 ))))]| by Th8

      .= (p1 <X> p2);

      hence thesis;

    end;

    theorem :: EUCLID_5:18

    (( - p1) <X> p2) = (p1 <X> ( - p2))

    proof

      (( - p1) <X> p2) = ( |[( - (p1 `1 )), ( - (p1 `2 )), ( - (p1 `3 ))]| <X> p2) by Th10

      .= ( |[( - (p1 `1 )), ( - (p1 `2 )), ( - (p1 `3 ))]| <X> |[(p2 `1 ), (p2 `2 ), (p2 `3 )]|) by Th3

      .= |[((( - (p1 `2 )) * (p2 `3 )) - (( - (p1 `3 )) * (p2 `2 ))), ((( - (p1 `3 )) * (p2 `1 )) - (( - (p1 `1 )) * (p2 `3 ))), ((( - (p1 `1 )) * (p2 `2 )) - (( - (p1 `2 )) * (p2 `1 )))]| by Th15

      .= |[(((p1 `2 ) * ( - (p2 `3 ))) - ((p1 `3 ) * ( - (p2 `2 )))), (((p1 `3 ) * ( - (p2 `1 ))) - ((p1 `1 ) * ( - (p2 `3 )))), (((p1 `1 ) * ( - (p2 `2 ))) - ((p1 `2 ) * ( - (p2 `1 ))))]|

      .= ( |[(p1 `1 ), (p1 `2 ), (p1 `3 )]| <X> |[( - (p2 `1 )), ( - (p2 `2 )), ( - (p2 `3 ))]|) by Th15

      .= ( |[(p1 `1 ), (p1 `2 ), (p1 `3 )]| <X> ( - p2)) by Th10;

      hence thesis by Th3;

    end;

    theorem :: EUCLID_5:19

    ( |[ 0 , 0 , 0 ]| <X> |[x, y, z]|) = ( 0. ( TOP-REAL 3))

    proof

      ( |[ 0 , 0 , 0 ]| <X> |[x, y, z]|) = |[(( 0 * z) - ( 0 * y)), (( 0 * x) - ( 0 * z)), (( 0 * y) - ( 0 * x))]| by Th15

      .= |[( 0 * (z - y)), ( 0 * (x - z)), ( 0 * (y - x))]|

      .= ( 0 * |[(z - y), (x - z), (y - x)]|) by Th8;

      hence thesis by RLVECT_1: 10;

    end;

    theorem :: EUCLID_5:20

    ( |[x1, 0 , 0 ]| <X> |[x2, 0 , 0 ]|) = ( 0. ( TOP-REAL 3))

    proof

      ( |[x1, 0 , 0 ]| <X> |[x2, 0 , 0 ]|) = |[(( 0 * 0 ) - ( 0 * 0 )), (( 0 * x2) - (x1 * 0 )), ((x1 * 0 ) - ( 0 * x2))]| by Th15

      .= |[( 0 * ( 0 - 0 )), ( 0 * (x2 - x1)), ( 0 * (x1 - x2))]|

      .= ( 0 * |[( 0 - 0 ), (x2 - x1), (x1 - x2)]|) by Th8

      .= ( 0. ( TOP-REAL 3)) by RLVECT_1: 10;

      hence thesis;

    end;

    theorem :: EUCLID_5:21

    ( |[ 0 , y1, 0 ]| <X> |[ 0 , y2, 0 ]|) = ( 0. ( TOP-REAL 3))

    proof

      ( |[ 0 , y1, 0 ]| <X> |[ 0 , y2, 0 ]|) = |[((y1 * 0 ) - ( 0 * y2)), (( 0 * 0 ) - ( 0 * 0 )), (( 0 * y2) - (y1 * 0 ))]| by Th15

      .= |[( 0 * (y1 - y2)), ( 0 * ( 0 - 0 )), ( 0 * (y2 - y1))]|

      .= ( 0 * |[(y1 - y2), ( 0 - 0 ), (y2 - y1)]|) by Th8

      .= ( 0. ( TOP-REAL 3)) by RLVECT_1: 10;

      hence thesis;

    end;

    theorem :: EUCLID_5:22

    ( |[ 0 , 0 , z1]| <X> |[ 0 , 0 , z2]|) = ( 0. ( TOP-REAL 3))

    proof

      ( |[ 0 , 0 , z1]| <X> |[ 0 , 0 , z2]|) = |[(( 0 * z2) - (z1 * 0 )), ((z1 * 0 ) - ( 0 * z2)), (( 0 * 0 ) - ( 0 * 0 ))]| by Th15

      .= |[( 0 * (z2 - z1)), ( 0 * (z1 - z2)), ( 0 * ( 0 * 0 ))]|

      .= ( 0 * |[(z2 - z1), (z1 - z2), ( 0 - 0 )]|) by Th8

      .= ( 0. ( TOP-REAL 3)) by RLVECT_1: 10;

      hence thesis;

    end;

    theorem :: EUCLID_5:23

    

     Th23: (p1 <X> (p2 + p3)) = ((p1 <X> p2) + (p1 <X> p3))

    proof

      

       A1: ((p1 <X> p2) + (p1 <X> p3)) = |[((((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 ))) + (((p1 `2 ) * (p3 `3 )) - ((p1 `3 ) * (p3 `2 )))), ((((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))) + (((p1 `3 ) * (p3 `1 )) - ((p1 `1 ) * (p3 `3 )))), ((((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 ))) + (((p1 `1 ) * (p3 `2 )) - ((p1 `2 ) * (p3 `1 ))))]| by Th6

      .= |[(((((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 ))) + ((p1 `2 ) * (p3 `3 ))) - ((p1 `3 ) * (p3 `2 ))), (((((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))) + ((p1 `3 ) * (p3 `1 ))) - ((p1 `1 ) * (p3 `3 ))), (((((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 ))) + ((p1 `1 ) * (p3 `2 ))) - ((p1 `2 ) * (p3 `1 )))]|;

      

       A2: (p2 + p3) = |[((p2 `1 ) + (p3 `1 )), ((p2 `2 ) + (p3 `2 )), ((p2 `3 ) + (p3 `3 ))]| by Th5;

      then

       A3: ((p2 + p3) `3 ) = ((p2 `3 ) + (p3 `3 )) by FINSEQ_1: 45;

      ((p2 + p3) `1 ) = ((p2 `1 ) + (p3 `1 )) & ((p2 + p3) `2 ) = ((p2 `2 ) + (p3 `2 )) by A2, FINSEQ_1: 45;

      hence thesis by A3, A1;

    end;

    theorem :: EUCLID_5:24

    

     Th24: ((p1 + p2) <X> p3) = ((p1 <X> p3) + (p2 <X> p3))

    proof

      ((p1 + p2) <X> p3) = ( - (p3 <X> (p1 + p2))) by Th17

      .= ( - ((p3 <X> p1) + (p3 <X> p2))) by Th23

      .= ( - ((p3 <X> p1) - (p2 <X> p3))) by Th17

      .= (( - (p3 <X> p1)) + (p2 <X> p3)) by RLVECT_1: 33;

      hence thesis by Th17;

    end;

    theorem :: EUCLID_5:25

    (p1 <X> p1) = ( 0. ( TOP-REAL 3)) by Th4;

    theorem :: EUCLID_5:26

    ((p1 + p2) <X> (p3 + p4)) = ((((p1 <X> p3) + (p1 <X> p4)) + (p2 <X> p3)) + (p2 <X> p4))

    proof

      ((p1 + p2) <X> (p3 + p4)) = ((p1 <X> (p3 + p4)) + (p2 <X> (p3 + p4))) by Th24

      .= (((p1 <X> p3) + (p1 <X> p4)) + (p2 <X> (p3 + p4))) by Th23

      .= (((p1 <X> p3) + (p1 <X> p4)) + ((p2 <X> p3) + (p2 <X> p4))) by Th23;

      hence thesis by RLVECT_1:def 3;

    end;

    theorem :: EUCLID_5:27

    

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

    proof

      reconsider f = p as FinSequence;

      consider x,y,z be Real such that

       A1: p = <*x, y, z*> by Th1;

       <*x, y, z*> = <*(f . 1), y, z*> by A1, FINSEQ_1: 45

      .= <*(f . 1), (f . 2), z*> by A1, FINSEQ_1: 45

      .= <*(p `1 ), (p `2 ), (p `3 )*> by A1, FINSEQ_1: 45;

      hence thesis by A1;

    end;

    theorem :: EUCLID_5:28

    

     Th28: for f1,f2 be FinSequence of REAL st ( len f1) = 3 & ( len f2) = 3 holds ( mlt (f1,f2)) = <*((f1 . 1) * (f2 . 1)), ((f1 . 2) * (f2 . 2)), ((f1 . 3) * (f2 . 3))*>

    proof

      let f1,f2 be FinSequence of REAL such that

       A1: ( len f1) = 3 and

       A2: ( len f2) = 3;

      

       A3: f2 = <*(f2 . 1), (f2 . 2), (f2 . 3)*> by A2, FINSEQ_1: 45;

      reconsider f11 = (f1 . 1), f12 = (f1 . 2), f13 = (f1 . 3), f21 = (f2 . 1), f22 = (f2 . 2), f23 = (f2 . 3) as Element of REAL by XREAL_0:def 1;

      ( mlt (f1,f2)) = ( multreal .: (f1,f2)) by RVSUM_1:def 9

      .= ( multreal .: ( <*f11, f12, f13*>, <*f21, f22, f23*>)) by A1, A3, FINSEQ_1: 45

      .= <*( multreal . ((f1 . 1),(f2 . 1))), ( multreal . ((f1 . 2),(f2 . 2))), ( multreal . ((f1 . 3),(f2 . 3)))*> by FINSEQ_2: 76

      .= <*((f1 . 1) * (f2 . 1)), ( multreal . ((f1 . 2),(f2 . 2))), ( multreal . ((f1 . 3),(f2 . 3)))*> by BINOP_2:def 11

      .= <*((f1 . 1) * (f2 . 1)), ((f1 . 2) * (f2 . 2)), ( multreal . ((f1 . 3),(f2 . 3)))*> by BINOP_2:def 11;

      hence thesis by BINOP_2:def 11;

    end;

    theorem :: EUCLID_5:29

    

     Th29: |(p1, p2)| = ((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 )))

    proof

      reconsider f1 = p1, f2 = p2 as FinSequence of REAL by EUCLID: 24;

      

       A1: ( len f1) = ( len <*(p1 `1 ), (p1 `2 ), (p1 `3 )*>) by Th27

      .= 3 by FINSEQ_1: 45;

      

       A2: ( len f2) = ( len <*(p2 `1 ), (p2 `2 ), (p2 `3 )*>) by Th27

      .= 3 by FINSEQ_1: 45;

       |(p1, p2)| = ( Sum ( mlt (f1,f2))) by RVSUM_1:def 16

      .= ( Sum <*((f1 . 1) * (f2 . 1)), ((f1 . 2) * (f2 . 2)), ((f1 . 3) * (f2 . 3))*>) by A1, A2, Th28

      .= ((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (f2 . 3))) by RVSUM_1: 78;

      hence thesis;

    end;

    theorem :: EUCLID_5:30

    

     Th30: |( |[x1, x2, x3]|, |[y1, y2, y3]|)| = (((x1 * y1) + (x2 * y2)) + (x3 * y3))

    proof

      consider p1 such that

       A1: p1 = |[x1, x2, x3]|;

      

       A2: (p1 `3 ) = x3 by A1, FINSEQ_1: 45;

      consider p2 such that

       A3: p2 = |[y1, y2, y3]|;

      

       A4: (p2 `3 ) = y3 by A3, FINSEQ_1: 45;

      

       A5: (p2 `1 ) = y1 & (p2 `2 ) = y2 by A3, FINSEQ_1: 45;

      (p1 `1 ) = x1 & (p1 `2 ) = x2 by A1, FINSEQ_1: 45;

      hence thesis by A1, A2, A3, A5, A4, Th29;

    end;

    definition

      let p1, p2, p3;

      :: EUCLID_5:def5

      func |{p1,p2,p3}| -> Real equals |(p1, (p2 <X> p3))|;

      coherence ;

    end

    theorem :: EUCLID_5:31

     |{p1, p1, p2}| = 0 & |{p2, p1, p2}| = 0

    proof

      

       A1: |{p2, p1, p2}| = ((((p2 `1 ) * ((p1 <X> p2) `1 )) + ((p2 `2 ) * ((p1 <X> p2) `2 ))) + ((p2 `3 ) * ((p1 <X> p2) `3 ))) by Th29

      .= ((((p2 `1 ) * (((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 )))) + ((p2 `2 ) * ((p1 <X> p2) `2 ))) + ((p2 `3 ) * ((p1 <X> p2) `3 ))) by FINSEQ_1: 45

      .= ((((p2 `1 ) * (((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 )))) + ((p2 `2 ) * (((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))))) + ((p2 `3 ) * ((p1 <X> p2) `3 ))) by FINSEQ_1: 45

      .= (((((p2 `1 ) * ((p1 `2 ) * (p2 `3 ))) - ((p2 `1 ) * ((p1 `3 ) * (p2 `2 )))) + ((p2 `2 ) * (((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))))) + ((p2 `3 ) * (((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 ))))) by FINSEQ_1: 45

      .= (( 0 - ((p2 `2 ) * ((p1 `1 ) * (p2 `3 )))) + ((p2 `2 ) * ((p1 `1 ) * (p2 `3 ))));

       |{p1, p1, p2}| = ((((p1 `1 ) * ((p1 <X> p2) `1 )) + ((p1 `2 ) * ((p1 <X> p2) `2 ))) + ((p1 `3 ) * ((p1 <X> p2) `3 ))) by Th29

      .= ((((p1 `1 ) * (((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 )))) + ((p1 `2 ) * ((p1 <X> p2) `2 ))) + ((p1 `3 ) * ((p1 <X> p2) `3 ))) by FINSEQ_1: 45

      .= ((((p1 `1 ) * (((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 )))) + ((p1 `2 ) * (((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))))) + ((p1 `3 ) * ((p1 <X> p2) `3 ))) by FINSEQ_1: 45

      .= (((((p1 `1 ) * ((p1 `2 ) * (p2 `3 ))) - ((p1 `1 ) * ((p1 `3 ) * (p2 `2 )))) + ((p1 `2 ) * (((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))))) + ((p1 `3 ) * (((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 ))))) by FINSEQ_1: 45

      .= 0 ;

      hence thesis by A1;

    end;

    theorem :: EUCLID_5:32

    (p1 <X> (p2 <X> p3)) = (( |(p1, p3)| * p2) - ( |(p1, p2)| * p3))

    proof

      

       A1: (((p1 `2 ) * (((p2 `1 ) * (p3 `2 )) - ((p2 `2 ) * (p3 `1 )))) - ((p1 `3 ) * (((p2 `3 ) * (p3 `1 )) - ((p2 `1 ) * (p3 `3 ))))) = ((((((p1 `2 ) * (p3 `2 )) + ((p1 `3 ) * (p3 `3 ))) + ((p1 `1 ) * (p3 `1 ))) * (p2 `1 )) - (((((p1 `2 ) * (p2 `2 )) + ((p1 `3 ) * (p2 `3 ))) + ((p1 `1 ) * (p2 `1 ))) * (p3 `1 ))) & (((p1 `3 ) * (((p2 `2 ) * (p3 `3 )) - ((p2 `3 ) * (p3 `2 )))) - ((p1 `1 ) * (((p2 `1 ) * (p3 `2 )) - ((p2 `2 ) * (p3 `1 ))))) = ((((((p1 `3 ) * (p3 `3 )) + ((p1 `1 ) * (p3 `1 ))) + ((p1 `2 ) * (p3 `2 ))) * (p2 `2 )) - (((((p1 `3 ) * (p2 `3 )) + ((p1 `1 ) * (p2 `1 ))) + ((p1 `2 ) * (p2 `2 ))) * (p3 `2 )));

      

       A2: (((p1 `1 ) * (((p2 `3 ) * (p3 `1 )) - ((p2 `1 ) * (p3 `3 )))) - ((p1 `2 ) * (((p2 `2 ) * (p3 `3 )) - ((p2 `3 ) * (p3 `2 ))))) = ((((((p1 `1 ) * (p3 `1 )) + ((p1 `2 ) * (p3 `2 ))) + ((p1 `3 ) * (p3 `3 ))) * (p2 `3 )) - (((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))) * (p3 `3 )));

      (p1 <X> (p2 <X> p3)) = ( |[(p1 `1 ), (p1 `2 ), (p1 `3 )]| <X> |[(((p2 `2 ) * (p3 `3 )) - ((p2 `3 ) * (p3 `2 ))), (((p2 `3 ) * (p3 `1 )) - ((p2 `1 ) * (p3 `3 ))), (((p2 `1 ) * (p3 `2 )) - ((p2 `2 ) * (p3 `1 )))]|) by Th3

      .= |[(((p1 `2 ) * (((p2 `1 ) * (p3 `2 )) - ((p2 `2 ) * (p3 `1 )))) - ((p1 `3 ) * (((p2 `3 ) * (p3 `1 )) - ((p2 `1 ) * (p3 `3 ))))), (((p1 `3 ) * (((p2 `2 ) * (p3 `3 )) - ((p2 `3 ) * (p3 `2 )))) - ((p1 `1 ) * (((p2 `1 ) * (p3 `2 )) - ((p2 `2 ) * (p3 `1 ))))), (((p1 `1 ) * (((p2 `3 ) * (p3 `1 )) - ((p2 `1 ) * (p3 `3 )))) - ((p1 `2 ) * (((p2 `2 ) * (p3 `3 )) - ((p2 `3 ) * (p3 `2 )))))]| by Th15;

      

      then (p1 <X> (p2 <X> p3)) = ( |[(((((p1 `1 ) * (p3 `1 )) + ((p1 `2 ) * (p3 `2 ))) + ((p1 `3 ) * (p3 `3 ))) * (p2 `1 )), (((((p1 `1 ) * (p3 `1 )) + ((p1 `2 ) * (p3 `2 ))) + ((p1 `3 ) * (p3 `3 ))) * (p2 `2 )), (((((p1 `1 ) * (p3 `1 )) + ((p1 `2 ) * (p3 `2 ))) + ((p1 `3 ) * (p3 `3 ))) * (p2 `3 ))]| - |[(((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))) * (p3 `1 )), (((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))) * (p3 `2 )), (((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))) * (p3 `3 ))]|) by A1, A2, Th13

      .= ((((((p1 `1 ) * (p3 `1 )) + ((p1 `2 ) * (p3 `2 ))) + ((p1 `3 ) * (p3 `3 ))) * |[(p2 `1 ), (p2 `2 ), (p2 `3 )]|) - |[(((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))) * (p3 `1 )), (((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))) * (p3 `2 )), (((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))) * (p3 `3 ))]|) by Th8

      .= ((((((p1 `1 ) * (p3 `1 )) + ((p1 `2 ) * (p3 `2 ))) + ((p1 `3 ) * (p3 `3 ))) * |[(p2 `1 ), (p2 `2 ), (p2 `3 )]|) - (((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))) * |[(p3 `1 ), (p3 `2 ), (p3 `3 )]|)) by Th8

      .= (( |(p1, p3)| * |[(p2 `1 ), (p2 `2 ), (p2 `3 )]|) - (((((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))) * |[(p3 `1 ), (p3 `2 ), (p3 `3 )]|)) by Th29

      .= (( |(p1, p3)| * |[(p2 `1 ), (p2 `2 ), (p2 `3 )]|) - ( |(p1, p2)| * |[(p3 `1 ), (p3 `2 ), (p3 `3 )]|)) by Th29

      .= (( |(p1, p3)| * p2) - ( |(p1, p2)| * |[(p3 `1 ), (p3 `2 ), (p3 `3 )]|)) by Th3;

      hence thesis by Th3;

    end;

    theorem :: EUCLID_5:33

    

     Th33: |{p1, p2, p3}| = |{p2, p3, p1}|

    proof

       |{p1, p2, p3}| = |( |[(p1 `1 ), (p1 `2 ), (p1 `3 )]|, |[(((p2 `2 ) * (p3 `3 )) - ((p2 `3 ) * (p3 `2 ))), (((p2 `3 ) * (p3 `1 )) - ((p2 `1 ) * (p3 `3 ))), (((p2 `1 ) * (p3 `2 )) - ((p2 `2 ) * (p3 `1 )))]|)| by Th3

      .= ((((p1 `1 ) * (((p2 `2 ) * (p3 `3 )) - ((p2 `3 ) * (p3 `2 )))) + ((p1 `2 ) * (((p2 `3 ) * (p3 `1 )) - ((p2 `1 ) * (p3 `3 ))))) + ((p1 `3 ) * (((p2 `1 ) * (p3 `2 )) - ((p2 `2 ) * (p3 `1 ))))) by Th30

      .= ((((p2 `1 ) * (((p3 `2 ) * (p1 `3 )) - ((p3 `3 ) * (p1 `2 )))) + ((p2 `2 ) * (((p3 `3 ) * (p1 `1 )) - ((p3 `1 ) * (p1 `3 ))))) + ((p2 `3 ) * (((p3 `1 ) * (p1 `2 )) - ((p3 `2 ) * (p1 `1 )))))

      .= |( |[(p2 `1 ), (p2 `2 ), (p2 `3 )]|, |[(((p3 `2 ) * (p1 `3 )) - ((p3 `3 ) * (p1 `2 ))), (((p3 `3 ) * (p1 `1 )) - ((p3 `1 ) * (p1 `3 ))), (((p3 `1 ) * (p1 `2 )) - ((p3 `2 ) * (p1 `1 )))]|)| by Th30

      .= |(p2, (p3 <X> p1))| by Th3;

      hence thesis;

    end;

    theorem :: EUCLID_5:34

     |{p1, p2, p3}| = |{p3, p1, p2}| by Th33;

    theorem :: EUCLID_5:35

     |{p1, p2, p3}| = |((p1 <X> p2), p3)|

    proof

       |{p1, p2, p3}| = |( |[(p1 `1 ), (p1 `2 ), (p1 `3 )]|, |[(((p2 `2 ) * (p3 `3 )) - ((p2 `3 ) * (p3 `2 ))), (((p2 `3 ) * (p3 `1 )) - ((p2 `1 ) * (p3 `3 ))), (((p2 `1 ) * (p3 `2 )) - ((p2 `2 ) * (p3 `1 )))]|)| by Th3

      .= ((((p1 `1 ) * (((p2 `2 ) * (p3 `3 )) - ((p2 `3 ) * (p3 `2 )))) + ((p1 `2 ) * (((p2 `3 ) * (p3 `1 )) - ((p2 `1 ) * (p3 `3 ))))) + ((p1 `3 ) * (((p2 `1 ) * (p3 `2 )) - ((p2 `2 ) * (p3 `1 ))))) by Th30

      .= (((((p2 `2 ) * ((p1 `1 ) * (p3 `3 ))) - ((p2 `3 ) * ((p1 `1 ) * (p3 `2 )))) + (((p2 `3 ) * ((p1 `2 ) * (p3 `1 ))) - ((p2 `1 ) * ((p1 `2 ) * (p3 `3 ))))) + (((p2 `1 ) * ((p1 `3 ) * (p3 `2 ))) - ((p2 `2 ) * ((p1 `3 ) * (p3 `1 )))));

      

      then |{p1, p2, p3}| = ((((((p2 `3 ) * (p1 `2 )) - ((p2 `2 ) * (p1 `3 ))) * (p3 `1 )) + ((((p2 `1 ) * (p1 `3 )) - ((p2 `3 ) * (p1 `1 ))) * (p3 `2 ))) + ((((p2 `2 ) * (p1 `1 )) - ((p2 `1 ) * (p1 `2 ))) * (p3 `3 )))

      .= |((p1 <X> p2), |[(p3 `1 ), (p3 `2 ), (p3 `3 )]|)| by Th30

      .= |((p1 <X> p2), p3)| by Th3;

      hence thesis;

    end;

    registration

      cluster ( TOP-REAL 3) -> up-3-dimensional;

      coherence

      proof

        take u = |[1, 0 , 0 ]|, v = |[ 0 , 1, 0 ]|, w = |[ 0 , 0 , 1]|;

        let a,b,c be Real such that

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

        

         A2: ( |[a, b, c]| `1 ) = a & ( |[a, b, c]| `2 ) = b & ( |[a, b, c]| `3 ) = c by Th2;

        

         A3: (c * w) = |[(c * 0 ), (c * 0 ), (c * 1)]| by Th8;

        (a * u) = |[(a * 1), (a * 0 ), (a * 0 )]| & (b * v) = |[(b * 0 ), (b * 1), (b * 0 )]| by Th8;

        

        then (((a * u) + (b * v)) + (c * w)) = ( |[(a + 0 ), ( 0 + b), ( 0 + 0 )]| + (c * w)) by Th6

        .= |[(a + 0 ), (b + 0 ), ( 0 + c)]| by A3, Th6;

        hence thesis by A1, A2, Th2, Th4;

      end;

    end