bhsp_1.miz



    begin

    definition

      struct ( RLSStruct) UNITSTR (# the carrier -> set,

the ZeroF -> Element of the carrier,

the addF -> BinOp of the carrier,

the Mult -> Function of [: REAL , the carrier:], the carrier,

the scalar -> Function of [: the carrier, the carrier:], REAL #)

       attr strict strict;

    end

    registration

      cluster non empty strict for UNITSTR;

      existence

      proof

        set D = the non empty set, Z = the Element of D, a = the BinOp of D, m = the Function of [: REAL , D:], D, s = the Function of [:D, D:], REAL ;

        take UNITSTR (# D, Z, a, m, s #);

        thus the carrier of UNITSTR (# D, Z, a, m, s #) is non empty;

        thus thesis;

      end;

    end

    registration

      let D be non empty set, Z be Element of D, a be BinOp of D, m be Function of [: REAL , D:], D, s be Function of [:D, D:], REAL ;

      cluster UNITSTR (# D, Z, a, m, s #) -> non empty;

      coherence ;

    end

    reserve X for non empty UNITSTR;

    reserve a,b for Real;

    reserve x,y for Point of X;

    deffunc 09( UNITSTR) = ( 0. $1);

    definition

      let X;

      let x, y;

      :: BHSP_1:def1

      func x .|. y -> Real equals (the scalar of X . [x, y]);

      correctness ;

    end

    set V0 = the RealLinearSpace;

    

     Lm1: the carrier of ( (0). V0) = {( 0. V0)} by RLSUB_1:def 3;

    reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> ( In ( 0 , REAL ))) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], REAL ;

    (for x,y be VECTOR of ( (0). V0) holds (nilfunc . [x, y]) = 0 ) & ( 0. V0) in the carrier of ( (0). V0) by Lm1, FUNCOP_1: 7, TARSKI:def 1;

    then

     Lm2: (nilfunc . [( 0. V0), ( 0. V0)]) = 0 ;

    

     Lm3: for u,v be VECTOR of ( (0). V0) holds (nilfunc . [u, v]) = (nilfunc . [v, u])

    proof

      let u,v be VECTOR of ( (0). V0);

      u = ( 0. V0) & v = ( 0. V0) by Lm1, TARSKI:def 1;

      hence thesis;

    end;

    

     Lm4: for u,v,w be VECTOR of ( (0). V0) holds (nilfunc . [(u + v), w]) = ((nilfunc . [u, w]) + (nilfunc . [v, w]))

    proof

      let u,v,w be VECTOR of ( (0). V0);

      

       A1: w = ( 0. V0) by Lm1, TARSKI:def 1;

      u = ( 0. V0) & v = ( 0. V0) by Lm1, TARSKI:def 1;

      hence thesis by A1, Lm1, Lm2, TARSKI:def 1;

    end;

    

     Lm5: for u,v be VECTOR of ( (0). V0), a holds (nilfunc . [(a * u), v]) = (a * (nilfunc . [u, v]))

    proof

      let u,v be VECTOR of ( (0). V0);

      let a;

      u = ( 0. V0) & v = ( 0. V0) by Lm1, TARSKI:def 1;

      hence thesis by Lm1, Lm2, TARSKI:def 1;

    end;

    set X0 = UNITSTR (# the carrier of ( (0). V0), ( 0. ( (0). V0)), the addF of ( (0). V0), the Mult of ( (0). V0), nilfunc #);

     Lm6:

    now

      let x,y,z be Point of X0;

      let a;

       09(X0) = ( 0. V0) by RLSUB_1: 11;

      hence (x .|. x) = ( In ( 0 , REAL )) iff x = 09(X0) by Lm1, FUNCOP_1: 7, TARSKI:def 1;

      thus 0 <= (x .|. x) by FUNCOP_1: 7;

      thus (x .|. y) = (y .|. x) by Lm3;

      thus ((x + y) .|. z) = ((x .|. z) + (y .|. z))

      proof

        reconsider u = x, v = y, w = z as VECTOR of ( (0). V0);

        ((x + y) .|. z) = (nilfunc . [(u + v), w]);

        hence thesis by Lm4;

      end;

      thus ((a * x) .|. y) = (a * (x .|. y))

      proof

        reconsider u = x, v = y as VECTOR of ( (0). V0);

        ((a * x) .|. y) = (nilfunc . [(a * u), v]);

        hence thesis by Lm5;

      end;

    end;

    definition

      let IT be non empty UNITSTR;

      :: BHSP_1:def2

      attr IT is RealUnitarySpace-like means

      : Def2: for x,y,z be Point of IT, a holds ((x .|. x) = 0 iff x = ( 0. IT)) & 0 <= (x .|. x) & (x .|. y) = (y .|. x) & ((x + y) .|. z) = ((x .|. z) + (y .|. z)) & ((a * x) .|. y) = (a * (x .|. y));

    end

    registration

      cluster RealUnitarySpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable strict for non empty UNITSTR;

      existence

      proof

        take X0;

        thus X0 is RealUnitarySpace-like by Lm6;

        thus X0 is vector-distributive scalar-distributive scalar-associative scalar-unital

        proof

          thus for a be Real holds for v,w be VECTOR of X0 holds (a * (v + w)) = ((a * v) + (a * w))

          proof

            let a be Real;

            let v,w be VECTOR of X0;

            reconsider v9 = v, w9 = w as VECTOR of ( (0). V0);

            

            thus (a * (v + w)) = (a * (v9 + w9))

            .= ((a * v9) + (a * w9)) by RLVECT_1:def 5

            .= ((a * v) + (a * w));

          end;

          thus for a,b be Real holds for v be VECTOR of X0 holds ((a + b) * v) = ((a * v) + (b * v))

          proof

            let a,b be Real;

            let v be VECTOR of X0;

            reconsider v9 = v as VECTOR of ( (0). V0);

            

            thus ((a + b) * v) = ((a + b) * v9)

            .= ((a * v9) + (b * v9)) by RLVECT_1:def 6

            .= ((a * v) + (b * v));

          end;

          thus for a,b be Real holds for v be VECTOR of X0 holds ((a * b) * v) = (a * (b * v))

          proof

            let a,b be Real;

            let v be VECTOR of X0;

            reconsider v9 = v as VECTOR of ( (0). V0);

            

            thus ((a * b) * v) = ((a * b) * v9)

            .= (a * (b * v9)) by RLVECT_1:def 7

            .= (a * (b * v));

          end;

          let v be VECTOR of X0;

          reconsider v9 = v as VECTOR of ( (0). V0);

          

          thus (1 * v) = (1 * v9)

          .= v by RLVECT_1:def 8;

        end;

        

         A1: for x,y be VECTOR of X0 holds for x9,y9 be VECTOR of ( (0). V0) st x = x9 & y = y9 holds (x + y) = (x9 + y9) & for a holds (a * x) = (a * x9);

        thus for v,w be VECTOR of X0 holds (v + w) = (w + v)

        proof

          let v,w be VECTOR of X0;

          reconsider v9 = v, w9 = w as VECTOR of ( (0). V0);

          

          thus (v + w) = (w9 + v9) by A1

          .= (w + v);

        end;

        thus for u,v,w be VECTOR of X0 holds ((u + v) + w) = (u + (v + w))

        proof

          let u,v,w be VECTOR of X0;

          reconsider u9 = u, v9 = v, w9 = w as VECTOR of ( (0). V0);

          

          thus ((u + v) + w) = ((u9 + v9) + w9)

          .= (u9 + (v9 + w9)) by RLVECT_1:def 3

          .= (u + (v + w));

        end;

        thus for v be VECTOR of X0 holds (v + ( 0. X0)) = v

        proof

          let v be VECTOR of X0;

          reconsider v9 = v as VECTOR of ( (0). V0);

          

          thus (v + ( 0. X0)) = (v9 + ( 0. ( (0). V0)))

          .= v by RLVECT_1: 4;

        end;

        thus X0 is right_complementable

        proof

          let v be VECTOR of X0;

          reconsider v9 = v as VECTOR of ( (0). V0);

          consider w9 be VECTOR of ( (0). V0) such that

           A2: (v9 + w9) = ( 0. ( (0). V0)) by ALGSTR_0:def 11;

          reconsider w = w9 as VECTOR of X0;

          take w;

          thus thesis by A2;

        end;

        thus thesis;

      end;

    end

    definition

      mode RealUnitarySpace is RealUnitarySpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty UNITSTR;

    end

    reserve X for RealUnitarySpace;

    reserve x,y,z,u,v for Point of X;

    definition

      let X, x, y;

      :: original: .|.

      redefine

      func x .|. y;

      commutativity by Def2;

    end

    theorem :: BHSP_1:1

    (( 0. X) .|. ( 0. X)) = 0 by Def2;

    theorem :: BHSP_1:2

    (x .|. (y + z)) = ((x .|. y) + (x .|. z)) by Def2;

    theorem :: BHSP_1:3

    (x .|. (a * y)) = (a * (x .|. y)) by Def2;

    theorem :: BHSP_1:4

    ((a * x) .|. y) = (x .|. (a * y))

    proof

      ((a * x) .|. y) = (a * (x .|. y)) by Def2;

      hence thesis by Def2;

    end;

    theorem :: BHSP_1:5

    

     Th5: (((a * x) + (b * y)) .|. z) = ((a * (x .|. z)) + (b * (y .|. z)))

    proof

      (((a * x) + (b * y)) .|. z) = (((a * x) .|. z) + ((b * y) .|. z)) by Def2

      .= ((a * (x .|. z)) + ((b * y) .|. z)) by Def2;

      hence thesis by Def2;

    end;

    theorem :: BHSP_1:6

    (x .|. ((a * y) + (b * z))) = ((a * (x .|. y)) + (b * (x .|. z))) by Th5;

    theorem :: BHSP_1:7

    (( - x) .|. y) = (x .|. ( - y))

    proof

      (( - x) .|. y) = ((( - 1) * x) .|. y) by RLVECT_1: 16

      .= (( - 1) * (x .|. y)) by Def2

      .= (x .|. (( - 1) * y)) by Def2;

      hence thesis by RLVECT_1: 16;

    end;

    theorem :: BHSP_1:8

    

     Th8: (( - x) .|. y) = ( - (x .|. y))

    proof

      (( - x) .|. y) = ((( - 1) * x) .|. y) by RLVECT_1: 16

      .= (( - 1) * (x .|. y)) by Def2;

      hence thesis;

    end;

    theorem :: BHSP_1:9

    (x .|. ( - y)) = ( - (x .|. y)) by Th8;

    theorem :: BHSP_1:10

    

     Th10: (( - x) .|. ( - y)) = (x .|. y)

    proof

      (( - x) .|. ( - y)) = ( - (x .|. ( - y))) by Th8

      .= ( - ( - (x .|. y))) by Th8;

      hence thesis;

    end;

    theorem :: BHSP_1:11

    

     Th11: ((x - y) .|. z) = ((x .|. z) - (y .|. z))

    proof

      ((x - y) .|. z) = ((x .|. z) + (( - y) .|. z)) by Def2

      .= ((x .|. z) + ( - (y .|. z))) by Th8;

      hence thesis;

    end;

    theorem :: BHSP_1:12

    

     Th12: (x .|. (y - z)) = ((x .|. y) - (x .|. z))

    proof

      (x .|. (y - z)) = ((x .|. y) + (x .|. ( - z))) by Def2

      .= ((x .|. y) + ( - (x .|. z))) by Th8;

      hence thesis;

    end;

    theorem :: BHSP_1:13

    ((x - y) .|. (u - v)) = ((((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v))

    proof

      ((x - y) .|. (u - v)) = ((x .|. (u - v)) - (y .|. (u - v))) by Th11

      .= (((x .|. u) - (x .|. v)) - (y .|. (u - v))) by Th12

      .= (((x .|. u) - (x .|. v)) - ((y .|. u) - (y .|. v))) by Th12;

      hence thesis;

    end;

    theorem :: BHSP_1:14

    

     Th14: (( 0. X) .|. x) = 0

    proof

      ( 09(X) .|. x) = ((x + ( - x)) .|. x) by RLVECT_1: 5

      .= ((x .|. x) + (( - x) .|. x)) by Def2

      .= ((x .|. x) + ( - (x .|. x))) by Th8;

      hence thesis;

    end;

    theorem :: BHSP_1:15

    (x .|. ( 0. X)) = 0 by Th14;

    theorem :: BHSP_1:16

    

     Th16: ((x + y) .|. (x + y)) = (((x .|. x) + (2 * (x .|. y))) + (y .|. y))

    proof

      ((x + y) .|. (x + y)) = ((x .|. (x + y)) + (y .|. (x + y))) by Def2

      .= (((x .|. x) + (x .|. y)) + (y .|. (x + y))) by Def2

      .= (((x .|. x) + (x .|. y)) + ((x .|. y) + (y .|. y))) by Def2

      .= (((x .|. x) + ((x .|. y) + (x .|. y))) + (y .|. y));

      hence thesis;

    end;

    theorem :: BHSP_1:17

    ((x + y) .|. (x - y)) = ((x .|. x) - (y .|. y))

    proof

      ((x + y) .|. (x - y)) = ((x .|. (x - y)) + (y .|. (x - y))) by Def2

      .= (((x .|. x) - (x .|. y)) + (y .|. (x - y))) by Th12

      .= (((x .|. x) - (x .|. y)) + ((x .|. y) - (y .|. y))) by Th12;

      hence thesis;

    end;

    theorem :: BHSP_1:18

    

     Th18: ((x - y) .|. (x - y)) = (((x .|. x) - (2 * (x .|. y))) + (y .|. y))

    proof

      ((x - y) .|. (x - y)) = ((x .|. (x - y)) - (y .|. (x - y))) by Th11

      .= (((x .|. x) - (x .|. y)) - (y .|. (x - y))) by Th12

      .= (((x .|. x) - (x .|. y)) - ((x .|. y) - (y .|. y))) by Th12

      .= (((x .|. x) - ((x .|. y) + (x .|. y))) + (y .|. y));

      hence thesis;

    end;

    theorem :: BHSP_1:19

    

     Th19: |.(x .|. y).| <= (( sqrt (x .|. x)) * ( sqrt (y .|. y)))

    proof

      

       A1: x <> 09(X) implies |.(x .|. y).| <= (( sqrt (x .|. x)) * ( sqrt (y .|. y)))

      proof

        

         A2: for t be Real holds ((((x .|. x) * (t ^2 )) + ((2 * (x .|. y)) * t)) + (y .|. y)) >= 0

        proof

          let t be Real;

          reconsider t as Real;

          (((t * x) + y) .|. ((t * x) + y)) >= 0 by Def2;

          then ((((t * x) .|. (t * x)) + (2 * ((t * x) .|. y))) + (y .|. y)) >= 0 by Th16;

          then (((t * (x .|. (t * x))) + (2 * ((t * x) .|. y))) + (y .|. y)) >= 0 by Def2;

          then (((t * (t * (x .|. x))) + (2 * ((t * x) .|. y))) + (y .|. y)) >= 0 by Def2;

          then ((((x .|. x) * (t ^2 )) + (2 * ((x .|. y) * t))) + (y .|. y)) >= 0 by Def2;

          hence thesis;

        end;

        

         A3: (x .|. x) >= 0 by Def2;

        assume x <> 09(X);

        then (x .|. x) <> 0 by Def2;

        then ( delta ((x .|. x),(2 * (x .|. y)),(y .|. y))) <= 0 by A3, A2, QUIN_1: 10;

        then (((2 * (x .|. y)) ^2 ) - ((4 * (x .|. x)) * (y .|. y))) <= 0 by QUIN_1:def 1;

        then (4 * (((x .|. y) ^2 ) - ((x .|. x) * (y .|. y)))) <= 0 ;

        then (((x .|. y) ^2 ) - ((x .|. x) * (y .|. y))) <= ( 0 / 4) by XREAL_1: 77;

        then ((x .|. y) ^2 ) <= ((x .|. x) * (y .|. y)) by XREAL_1: 50;

        then ( |.(x .|. y).| ^2 ) >= 0 & ( |.(x .|. y).| ^2 ) <= ((x .|. x) * (y .|. y)) by COMPLEX1: 75, XREAL_1: 63;

        then ( sqrt ( |.(x .|. y).| ^2 )) <= ( sqrt ((x .|. x) * (y .|. y))) by SQUARE_1: 26;

        then

         A4: |.(x .|. y).| <= ( sqrt ((x .|. x) * (y .|. y))) by COMPLEX1: 46, SQUARE_1: 22;

        (y .|. y) >= 0 by Def2;

        hence thesis by A3, A4, SQUARE_1: 29;

      end;

      x = 09(X) implies |.(x .|. y).| <= (( sqrt (x .|. x)) * ( sqrt (y .|. y)))

      proof

        assume x = 09(X);

        then (x .|. y) = 0 & ( sqrt (x .|. x)) = 0 by Th14, SQUARE_1: 17;

        hence thesis by ABSVALUE: 2;

      end;

      hence thesis by A1;

    end;

    definition

      let X, x, y;

      :: BHSP_1:def3

      pred x,y are_orthogonal means (x .|. y) = 0 ;

      symmetry ;

    end

    theorem :: BHSP_1:20

    (x,y) are_orthogonal implies (x,( - y)) are_orthogonal

    proof

      assume (x,y) are_orthogonal ;

      then ( - (x .|. y)) = ( - 0 );

      then (x .|. ( - y)) = 0 by Th8;

      hence thesis;

    end;

    theorem :: BHSP_1:21

    (x,y) are_orthogonal implies (( - x),y) are_orthogonal

    proof

      assume (x,y) are_orthogonal ;

      then ( - (x .|. y)) = ( - 0 );

      then (( - x) .|. y) = 0 by Th8;

      hence thesis;

    end;

    theorem :: BHSP_1:22

    (x,y) are_orthogonal implies (( - x),( - y)) are_orthogonal by Th10;

    theorem :: BHSP_1:23

    (x,( 0. X)) are_orthogonal by Th14;

    theorem :: BHSP_1:24

    (x,y) are_orthogonal implies ((x + y) .|. (x + y)) = ((x .|. x) + (y .|. y))

    proof

      assume (x,y) are_orthogonal ;

      then

       A1: (x .|. y) = 0 ;

      ((x + y) .|. (x + y)) = (((x .|. x) + (2 * (x .|. y))) + (y .|. y)) by Th16;

      hence thesis by A1;

    end;

    theorem :: BHSP_1:25

    (x,y) are_orthogonal implies ((x - y) .|. (x - y)) = ((x .|. x) + (y .|. y))

    proof

      assume (x,y) are_orthogonal ;

      then

       A1: (x .|. y) = 0 ;

      ((x - y) .|. (x - y)) = (((x .|. x) - (2 * (x .|. y))) + (y .|. y)) by Th18

      .= (((x .|. x) + (y .|. y)) - 0 ) by A1;

      hence thesis;

    end;

    definition

      let X, x;

      :: BHSP_1:def4

      func ||.x.|| -> Real equals ( sqrt (x .|. x));

      correctness ;

    end

    theorem :: BHSP_1:26

    

     Th26: ||.x.|| = 0 iff x = ( 0. X)

    proof

      thus ||.x.|| = 0 implies x = 09(X)

      proof

        assume

         A1: ||.x.|| = 0 ;

         0 <= (x .|. x) by Def2;

        then (x .|. x) = 0 by A1, SQUARE_1: 24;

        hence thesis by Def2;

      end;

      assume x = 09(X);

      hence thesis by Def2, SQUARE_1: 17;

    end;

    theorem :: BHSP_1:27

    

     Th27: ||.(a * x).|| = ( |.a.| * ||.x.||)

    proof

      

       A1: 0 <= (a ^2 ) & 0 <= (x .|. x) by Def2, XREAL_1: 63;

       ||.(a * x).|| = ( sqrt (a * (x .|. (a * x)))) by Def2

      .= ( sqrt (a * (a * (x .|. x)))) by Def2

      .= ( sqrt ((a ^2 ) * (x .|. x)))

      .= (( sqrt (a ^2 )) * ( sqrt (x .|. x))) by A1, SQUARE_1: 29

      .= ( |.a.| * ( sqrt (x .|. x))) by COMPLEX1: 72;

      hence thesis;

    end;

    theorem :: BHSP_1:28

    

     Th28: 0 <= ||.x.||

    proof

       0 <= (x .|. x) by Def2;

      hence thesis by SQUARE_1:def 2;

    end;

    theorem :: BHSP_1:29

     |.(x .|. y).| <= ( ||.x.|| * ||.y.||) by Th19;

    theorem :: BHSP_1:30

    

     Th30: ||.(x + y).|| <= ( ||.x.|| + ||.y.||)

    proof

      

       A1: ( sqrt ( ||.(x + y).|| ^2 )) = ( sqrt ((x + y) .|. (x + y))) by Th28, SQUARE_1: 22;

      ((x + y) .|. (x + y)) >= 0 & ( ||.(x + y).|| ^2 ) >= 0 by Def2, XREAL_1: 63;

      then ( ||.(x + y).|| ^2 ) = ((x + y) .|. (x + y)) by A1, SQUARE_1: 28;

      then

       A2: ( ||.(x + y).|| ^2 ) = (((x .|. x) + (2 * (x .|. y))) + (y .|. y)) by Th16;

      (x .|. x) >= 0 by Def2;

      then

       A3: ( ||.(x + y).|| ^2 ) = (((( sqrt (x .|. x)) ^2 ) + (2 * (x .|. y))) + (y .|. y)) by A2, SQUARE_1:def 2;

      

       A4: ||.x.|| >= 0 & ||.y.|| >= 0 by Th28;

       |.(x .|. y).| <= ( ||.x.|| * ||.y.||) & (x .|. y) <= |.(x .|. y).| by Th19, ABSVALUE: 4;

      then (x .|. y) <= ( ||.x.|| * ||.y.||) by XXREAL_0: 2;

      then (2 * (x .|. y)) <= (2 * ( ||.x.|| * ||.y.||)) by XREAL_1: 64;

      then (( ||.x.|| ^2 ) + (2 * (x .|. y))) <= (( ||.x.|| ^2 ) + ((2 * ||.x.||) * ||.y.||)) by XREAL_1: 7;

      then

       A5: ((( ||.x.|| ^2 ) + (2 * (x .|. y))) + ( ||.y.|| ^2 )) <= ((( ||.x.|| ^2 ) + ((2 * ||.x.||) * ||.y.||)) + ( ||.y.|| ^2 )) by XREAL_1: 6;

      (y .|. y) >= 0 by Def2;

      then ( ||.(x + y).|| ^2 ) <= (( ||.x.|| + ||.y.||) ^2 ) by A3, A5, SQUARE_1:def 2;

      hence thesis by A4, SQUARE_1: 16;

    end;

    theorem :: BHSP_1:31

    

     Th31: ||.( - x).|| = ||.x.||

    proof

      

       A1: |.( - 1).| = ( - ( - 1)) by ABSVALUE:def 1;

       ||.( - x).|| = ||.(( - 1) * x).|| by RLVECT_1: 16

      .= (1 * ||.x.||) by A1, Th27;

      hence thesis;

    end;

    theorem :: BHSP_1:32

    

     Th32: ( ||.x.|| - ||.y.||) <= ||.(x - y).||

    proof

      ((x - y) + y) = (x - (y - y)) by RLVECT_1: 29

      .= (x - 09(X)) by RLVECT_1: 15

      .= x by RLVECT_1: 13;

      then ||.x.|| <= ( ||.(x - y).|| + ||.y.||) by Th30;

      hence thesis by XREAL_1: 20;

    end;

    theorem :: BHSP_1:33

     |.( ||.x.|| - ||.y.||).| <= ||.(x - y).||

    proof

      ((y - x) + x) = (y - (x - x)) by RLVECT_1: 29

      .= (y - 09(X)) by RLVECT_1: 15

      .= y by RLVECT_1: 13;

      then ||.y.|| <= ( ||.(y - x).|| + ||.x.||) by Th30;

      then ( ||.y.|| - ||.x.||) <= ||.(y - x).|| by XREAL_1: 20;

      then ( ||.y.|| - ||.x.||) <= ||.( - (x - y)).|| by RLVECT_1: 33;

      then ( ||.y.|| - ||.x.||) <= ||.(x - y).|| by Th31;

      then

       A1: ( - ||.(x - y).||) <= ( - ( ||.y.|| - ||.x.||)) by XREAL_1: 24;

      ( ||.x.|| - ||.y.||) <= ||.(x - y).|| by Th32;

      hence thesis by A1, ABSVALUE: 5;

    end;

    definition

      let X, x, y;

      :: BHSP_1:def5

      func dist (x,y) -> Real equals ||.(x - y).||;

      correctness ;

      commutativity

      proof

        let IT be Real;

        let x, y;

         ||.(x - y).|| = ||.( - (y - x)).|| by RLVECT_1: 33

        .= ||.(y - x).|| by Th31;

        hence thesis;

      end;

    end

    theorem :: BHSP_1:34

    

     Th34: ( dist (x,x)) = 0

    proof

      

      thus ( dist (x,x)) = ||. 09(X).|| by RLVECT_1: 15

      .= 0 by Th26;

    end;

    theorem :: BHSP_1:35

    ( dist (x,z)) <= (( dist (x,y)) + ( dist (y,z)))

    proof

      ( dist (x,z)) = ||.((x - z) + 09(X)).|| by RLVECT_1: 4

      .= ||.((x - z) + (y - y)).|| by RLVECT_1: 15

      .= ||.(x - (z - (y - y))).|| by RLVECT_1: 29

      .= ||.(x - (y + (z - y))).|| by RLVECT_1: 29

      .= ||.((x - y) - (z - y)).|| by RLVECT_1: 27

      .= ||.((x - y) + (y - z)).|| by RLVECT_1: 33;

      hence thesis by Th30;

    end;

    theorem :: BHSP_1:36

    

     Th36: x <> y iff ( dist (x,y)) <> 0

    proof

      thus x <> y implies ( dist (x,y)) <> 0

      proof

        assume that

         A1: x <> y and

         A2: ( dist (x,y)) = 0 ;

        (x - y) = 09(X) by A2, Th26;

        hence contradiction by A1, RLVECT_1: 21;

      end;

      thus thesis by Th34;

    end;

    theorem :: BHSP_1:37

    ( dist (x,y)) >= 0 by Th28;

    theorem :: BHSP_1:38

    x <> y iff ( dist (x,y)) > 0

    proof

      thus x <> y implies ( dist (x,y)) > 0

      proof

        assume x <> y;

        then ( dist (x,y)) <> 0 by Th36;

        hence thesis by Th28;

      end;

      thus thesis by Th34;

    end;

    theorem :: BHSP_1:39

    ( dist (x,y)) = ( sqrt ((x - y) .|. (x - y)));

    theorem :: BHSP_1:40

    ( dist ((x + y),(u + v))) <= (( dist (x,u)) + ( dist (y,v)))

    proof

      ( dist ((x + y),(u + v))) = ||.((( - u) + ( - v)) + (x + y)).|| by RLVECT_1: 31

      .= ||.((x + (( - u) + ( - v))) + y).|| by RLVECT_1:def 3

      .= ||.(((x - u) + ( - v)) + y).|| by RLVECT_1:def 3

      .= ||.((x - u) + (y - v)).|| by RLVECT_1:def 3;

      hence thesis by Th30;

    end;

    theorem :: BHSP_1:41

    ( dist ((x - y),(u - v))) <= (( dist (x,u)) + ( dist (y,v)))

    proof

      ( dist ((x - y),(u - v))) = ||.(((x - y) - u) + v).|| by RLVECT_1: 29

      .= ||.((x - (u + y)) + v).|| by RLVECT_1: 27

      .= ||.(((x - u) - y) + v).|| by RLVECT_1: 27

      .= ||.((x - u) - (y - v)).|| by RLVECT_1: 29

      .= ||.((x - u) + ( - (y - v))).||;

      then ( dist ((x - y),(u - v))) <= ( ||.(x - u).|| + ||.( - (y - v)).||) by Th30;

      hence thesis by Th31;

    end;

    theorem :: BHSP_1:42

    ( dist ((x - z),(y - z))) = ( dist (x,y))

    proof

      

      thus ( dist ((x - z),(y - z))) = ||.(((x - z) - y) + z).|| by RLVECT_1: 29

      .= ||.((x - (y + z)) + z).|| by RLVECT_1: 27

      .= ||.(((x - y) - z) + z).|| by RLVECT_1: 27

      .= ||.((x - y) - (z - z)).|| by RLVECT_1: 29

      .= ||.((x - y) - 09(X)).|| by RLVECT_1: 15

      .= ( dist (x,y)) by RLVECT_1: 13;

    end;

    theorem :: BHSP_1:43

    ( dist ((x - z),(y - z))) <= (( dist (z,x)) + ( dist (z,y)))

    proof

      ( dist ((x - z),(y - z))) = ||.((x - z) + (z - y)).|| by RLVECT_1: 33

      .= ||.(( - (z - x)) + (z - y)).|| by RLVECT_1: 33;

      then ( dist ((x - z),(y - z))) <= ( ||.( - (z - x)).|| + ||.(z - y).||) by Th30;

      hence thesis by Th31;

    end;

    reserve seq,seq1,seq2,seq3 for sequence of X;

    reserve n for Nat;

    definition

      let X be non empty addLoopStr;

      let seq be sequence of X;

      let x be Point of X;

      :: BHSP_1:def6

      func seq + x -> sequence of X means

      : Def6: for n holds (it . n) = ((seq . n) + x);

      existence

      proof

        deffunc F( Nat) = ((seq . $1) + x);

        consider seq be sequence of X such that

         A1: for n be Element of NAT holds (seq . n) = F(n) from FUNCT_2:sch 4;

        take seq;

        let n;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let seq1,seq2 be sequence of X;

        assume that

         A2: for n holds (seq1 . n) = ((seq . n) + x) and

         A3: for n holds (seq2 . n) = ((seq . n) + x);

        let n be Element of NAT ;

        (seq1 . n) = ((seq . n) + x) by A2;

        hence thesis by A3;

      end;

    end

    theorem :: BHSP_1:44

    

     Th44: for X be non empty addLoopStr, seq be sequence of X holds (( - seq) . n) = ( - (seq . n))

    proof

      let X be non empty addLoopStr, seq be sequence of X;

      

       A1: ( dom ( - seq)) = NAT by FUNCT_2:def 1;

      

       A2: ( dom seq) = NAT by FUNCT_2:def 1;

      

       A3: n in NAT by ORDINAL1:def 12;

      

      hence (( - seq) . n) = (( - seq) /. n) by PARTFUN1:def 6, A1

      .= ( - (seq /. n)) by A1, VFUNCT_1:def 5, A3

      .= ( - (seq . n)) by A3, PARTFUN1:def 6, A2;

    end;

    definition

      let X, seq1, seq2;

      :: original: +

      redefine

      func seq1 + seq2;

      commutativity

      proof

        let seq1, seq2;

        let n be Element of NAT ;

        

        thus ((seq1 + seq2) . n) = ((seq2 . n) + (seq1 . n)) by NORMSP_1:def 2

        .= ((seq2 + seq1) . n) by NORMSP_1:def 2;

      end;

    end

    theorem :: BHSP_1:45

    (seq1 + (seq2 + seq3)) = ((seq1 + seq2) + seq3)

    proof

      let n be Element of NAT ;

      

      thus ((seq1 + (seq2 + seq3)) . n) = ((seq1 . n) + ((seq2 + seq3) . n)) by NORMSP_1:def 2

      .= ((seq1 . n) + ((seq2 . n) + (seq3 . n))) by NORMSP_1:def 2

      .= (((seq1 . n) + (seq2 . n)) + (seq3 . n)) by RLVECT_1:def 3

      .= (((seq1 + seq2) . n) + (seq3 . n)) by NORMSP_1:def 2

      .= (((seq1 + seq2) + seq3) . n) by NORMSP_1:def 2;

    end;

    theorem :: BHSP_1:46

    seq1 is constant & seq2 is constant implies (seq1 + seq2) is constant

    proof

      assume that

       A1: seq1 is constant and

       A2: seq2 is constant;

      set seq = (seq1 + seq2);

      consider x such that

       A3: for n be Nat holds (seq1 . n) = x by A1;

      consider y such that

       A4: for n be Nat holds (seq2 . n) = y by A2;

      take z = (x + y);

      let n be Nat;

      

      thus (seq . n) = ((seq1 . n) + (seq2 . n)) by NORMSP_1:def 2

      .= (x + (seq2 . n)) by A3

      .= z by A4;

    end;

    theorem :: BHSP_1:47

    seq1 is constant & seq2 is constant implies (seq1 - seq2) is constant

    proof

      assume that

       A1: seq1 is constant and

       A2: seq2 is constant;

      set seq = (seq1 - seq2);

      consider x such that

       A3: for n be Nat holds (seq1 . n) = x by A1;

      consider y such that

       A4: for n be Nat holds (seq2 . n) = y by A2;

      take z = (x - y);

      let n be Nat;

      

      thus (seq . n) = ((seq1 . n) - (seq2 . n)) by NORMSP_1:def 3

      .= (x - (seq2 . n)) by A3

      .= z by A4;

    end;

    theorem :: BHSP_1:48

    seq1 is constant implies (a * seq1) is constant

    proof

      assume

       A1: seq1 is constant;

      set seq = (a * seq1);

      consider x such that

       A2: for n be Nat holds (seq1 . n) = x by A1;

      take z = (a * x);

      let n be Nat;

      

      thus (seq . n) = (a * (seq1 . n)) by NORMSP_1:def 5

      .= z by A2;

    end;

    theorem :: BHSP_1:49

    (seq1 - seq2) = (seq1 + ( - seq2))

    proof

      let n be Element of NAT ;

      

      thus ((seq1 - seq2) . n) = ((seq1 . n) - (seq2 . n)) by NORMSP_1:def 3

      .= ((seq1 . n) + (( - seq2) . n)) by Th44

      .= ((seq1 + ( - seq2)) . n) by NORMSP_1:def 2;

    end;

    theorem :: BHSP_1:50

    seq = (seq + ( 0. X))

    proof

      let n be Element of NAT ;

      

      thus ((seq + 09(X)) . n) = ((seq . n) + 09(X)) by Def6

      .= (seq . n) by RLVECT_1: 4;

    end;

    theorem :: BHSP_1:51

    (a * (seq1 + seq2)) = ((a * seq1) + (a * seq2))

    proof

      let n be Element of NAT ;

      

      thus ((a * (seq1 + seq2)) . n) = (a * ((seq1 + seq2) . n)) by NORMSP_1:def 5

      .= (a * ((seq1 . n) + (seq2 . n))) by NORMSP_1:def 2

      .= ((a * (seq1 . n)) + (a * (seq2 . n))) by RLVECT_1:def 5

      .= (((a * seq1) . n) + (a * (seq2 . n))) by NORMSP_1:def 5

      .= (((a * seq1) . n) + ((a * seq2) . n)) by NORMSP_1:def 5

      .= (((a * seq1) + (a * seq2)) . n) by NORMSP_1:def 2;

    end;

    theorem :: BHSP_1:52

    ((a + b) * seq) = ((a * seq) + (b * seq))

    proof

      let n be Element of NAT ;

      

      thus (((a + b) * seq) . n) = ((a + b) * (seq . n)) by NORMSP_1:def 5

      .= ((a * (seq . n)) + (b * (seq . n))) by RLVECT_1:def 6

      .= (((a * seq) . n) + (b * (seq . n))) by NORMSP_1:def 5

      .= (((a * seq) . n) + ((b * seq) . n)) by NORMSP_1:def 5

      .= (((a * seq) + (b * seq)) . n) by NORMSP_1:def 2;

    end;

    theorem :: BHSP_1:53

    ((a * b) * seq) = (a * (b * seq))

    proof

      let n be Element of NAT ;

      

      thus (((a * b) * seq) . n) = ((a * b) * (seq . n)) by NORMSP_1:def 5

      .= (a * (b * (seq . n))) by RLVECT_1:def 7

      .= (a * ((b * seq) . n)) by NORMSP_1:def 5

      .= ((a * (b * seq)) . n) by NORMSP_1:def 5;

    end;

    theorem :: BHSP_1:54

    (1 qua Real * seq) = seq

    proof

      let n be Element of NAT ;

      

      thus ((1 * seq) . n) = (1 * (seq . n)) by NORMSP_1:def 5

      .= (seq . n) by RLVECT_1:def 8;

    end;

    theorem :: BHSP_1:55

    (( - 1) * seq) = ( - seq)

    proof

      let n be Element of NAT ;

      

      thus ((( - 1) * seq) . n) = (( - 1) * (seq . n)) by NORMSP_1:def 5

      .= ( - (seq . n)) by RLVECT_1: 16

      .= (( - seq) . n) by Th44;

    end;

    theorem :: BHSP_1:56

    (seq - x) = (seq + ( - x))

    proof

      let n be Element of NAT ;

      

      thus ((seq - x) . n) = ((seq . n) - x) by NORMSP_1:def 4

      .= ((seq + ( - x)) . n) by Def6;

    end;

    theorem :: BHSP_1:57

    (seq1 - seq2) = ( - (seq2 - seq1))

    proof

      let n be Element of NAT ;

      

      thus ((seq1 - seq2) . n) = ((seq1 . n) - (seq2 . n)) by NORMSP_1:def 3

      .= ( - ((seq2 . n) - (seq1 . n))) by RLVECT_1: 33

      .= ( - ((seq2 - seq1) . n)) by NORMSP_1:def 3

      .= (( - (seq2 - seq1)) . n) by Th44;

    end;

    theorem :: BHSP_1:58

    seq = (seq - ( 0. X))

    proof

      let n be Element of NAT ;

      

      thus ((seq - 09(X)) . n) = ((seq . n) - 09(X)) by NORMSP_1:def 4

      .= (seq . n) by RLVECT_1: 13;

    end;

    theorem :: BHSP_1:59

    seq = ( - ( - seq))

    proof

      let n be Element of NAT ;

      

      thus (( - ( - seq)) . n) = ( - (( - seq) . n)) by Th44

      .= ( - ( - (seq . n))) by Th44

      .= (seq . n) by RLVECT_1: 17;

    end;

    theorem :: BHSP_1:60

    (seq1 - (seq2 + seq3)) = ((seq1 - seq2) - seq3)

    proof

      let n be Element of NAT ;

      

      thus ((seq1 - (seq2 + seq3)) . n) = ((seq1 . n) - ((seq2 + seq3) . n)) by NORMSP_1:def 3

      .= ((seq1 . n) - ((seq2 . n) + (seq3 . n))) by NORMSP_1:def 2

      .= (((seq1 . n) - (seq2 . n)) - (seq3 . n)) by RLVECT_1: 27

      .= (((seq1 - seq2) . n) - (seq3 . n)) by NORMSP_1:def 3

      .= (((seq1 - seq2) - seq3) . n) by NORMSP_1:def 3;

    end;

    theorem :: BHSP_1:61

    ((seq1 + seq2) - seq3) = (seq1 + (seq2 - seq3))

    proof

      let n be Element of NAT ;

      

      thus (((seq1 + seq2) - seq3) . n) = (((seq1 + seq2) . n) - (seq3 . n)) by NORMSP_1:def 3

      .= (((seq1 . n) + (seq2 . n)) - (seq3 . n)) by NORMSP_1:def 2

      .= ((seq1 . n) + ((seq2 . n) - (seq3 . n))) by RLVECT_1:def 3

      .= ((seq1 . n) + ((seq2 - seq3) . n)) by NORMSP_1:def 3

      .= ((seq1 + (seq2 - seq3)) . n) by NORMSP_1:def 2;

    end;

    theorem :: BHSP_1:62

    (seq1 - (seq2 - seq3)) = ((seq1 - seq2) + seq3)

    proof

      let n be Element of NAT ;

      

      thus ((seq1 - (seq2 - seq3)) . n) = ((seq1 . n) - ((seq2 - seq3) . n)) by NORMSP_1:def 3

      .= ((seq1 . n) - ((seq2 . n) - (seq3 . n))) by NORMSP_1:def 3

      .= (((seq1 . n) - (seq2 . n)) + (seq3 . n)) by RLVECT_1: 29

      .= (((seq1 - seq2) . n) + (seq3 . n)) by NORMSP_1:def 3

      .= (((seq1 - seq2) + seq3) . n) by NORMSP_1:def 2;

    end;

    theorem :: BHSP_1:63

    (a * (seq1 - seq2)) = ((a * seq1) - (a * seq2))

    proof

      let n be Element of NAT ;

      

      thus ((a * (seq1 - seq2)) . n) = (a * ((seq1 - seq2) . n)) by NORMSP_1:def 5

      .= (a * ((seq1 . n) - (seq2 . n))) by NORMSP_1:def 3

      .= ((a * (seq1 . n)) - (a * (seq2 . n))) by RLVECT_1: 34

      .= (((a * seq1) . n) - (a * (seq2 . n))) by NORMSP_1:def 5

      .= (((a * seq1) . n) - ((a * seq2) . n)) by NORMSP_1:def 5

      .= (((a * seq1) - (a * seq2)) . n) by NORMSP_1:def 3;

    end;