algstr_3.miz



    begin

    definition

      struct ( ZeroOneStr) TernaryFieldStr (# the carrier -> set,

the ZeroF, OneF -> Element of the carrier,

the TernOp -> TriOp of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty for TernaryFieldStr;

      existence

      proof

        set A = the non empty set, Z = the Element of A, t = the TriOp of A;

        take TernaryFieldStr (# A, Z, Z, t #);

        thus the carrier of TernaryFieldStr (# A, Z, Z, t #) is non empty;

      end;

    end

    reserve F for non empty TernaryFieldStr;

    definition

      let F;

      mode Scalar of F is Element of F;

    end

    reserve a,b,c for Scalar of F;

    definition

      let F, a, b, c;

      :: ALGSTR_3:def1

      func Tern (a,b,c) -> Scalar of F equals (the TernOp of F . (a,b,c));

      correctness ;

    end

    definition

      :: ALGSTR_3:def2

      func ternaryreal -> TriOp of REAL means

      : Def2: for a,b,c be Real holds (it . (a,b,c)) = ((a * b) + c);

      existence

      proof

        deffunc F( Real, Real, Real) = ( In ((($1 * $2) + $3), REAL ));

        consider X be TriOp of REAL such that

         A1: for a,b,c be Element of REAL holds (X . (a,b,c)) = F(a,b,c) from MULTOP_1:sch 4;

        take X;

        let a,b,c be Real;

        reconsider a, b, c as Element of REAL by XREAL_0:def 1;

        (X . (a,b,c)) = F(a,b,c) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let o1,o2 be TriOp of REAL ;

        assume that

         A2: for a,b,c be Real holds (o1 . (a,b,c)) = ((a * b) + c) and

         A3: for a,b,c be Real holds (o2 . (a,b,c)) = ((a * b) + c);

        for a,b,c be Element of REAL holds (o1 . (a,b,c)) = (o2 . (a,b,c))

        proof

          let a,b,c be Element of REAL ;

          

          thus (o1 . (a,b,c)) = ((a * b) + c) by A2

          .= (o2 . (a,b,c)) by A3;

        end;

        hence thesis by MULTOP_1: 3;

      end;

    end

    definition

      :: ALGSTR_3:def3

      func TernaryFieldEx -> strict TernaryFieldStr equals TernaryFieldStr (# REAL , ( In ( 0 , REAL )), ( In (1, REAL )), ternaryreal #);

      correctness ;

    end

    registration

      cluster TernaryFieldEx -> non empty;

      coherence ;

    end

    definition

      let a,b,c be Scalar of TernaryFieldEx ;

      :: ALGSTR_3:def4

      func tern (a,b,c) -> Scalar of TernaryFieldEx equals (the TernOp of TernaryFieldEx . (a,b,c));

      correctness ;

    end

    theorem :: ALGSTR_3:1

    

     Th1: for u,u9,v,v9 be Real holds u <> u9 implies ex x be Real st ((u * x) + v) = ((u9 * x) + v9)

    proof

      let u,u9,v,v9 be Real;

      set x = ((v9 - v) / (u - u9));

      assume u <> u9;

      then (u - u9) <> 0 ;

      then

       A1: ((u - u9) * x) = (v9 - v) by XCMPLX_1: 87;

      reconsider x as Real;

      take x;

      thus thesis by A1;

    end;

    theorem :: ALGSTR_3:2

    for u,a,v be Scalar of TernaryFieldEx holds for z,x,y be Real holds u = z & a = x & v = y implies ( Tern (u,a,v)) = ((z * x) + y) by Def2;

    reconsider jj = 1, zz = 0 as Real;

    theorem :: ALGSTR_3:3

    1 = ( 1. TernaryFieldEx );

    

     Lm1: for a be Scalar of TernaryFieldEx holds ( Tern (a,( 1. TernaryFieldEx ),( 0. TernaryFieldEx ))) = a

    proof

      let a be Scalar of TernaryFieldEx ;

      reconsider x = a as Real;

      

      thus ( Tern (a,( 1. TernaryFieldEx ),( 0. TernaryFieldEx ))) = ((x * jj) + zz) by Def2

      .= a;

    end;

    

     Lm2: for a be Scalar of TernaryFieldEx holds ( Tern (( 1. TernaryFieldEx ),a,( 0. TernaryFieldEx ))) = a

    proof

      let a be Scalar of TernaryFieldEx ;

      reconsider x = a as Real;

      

      thus ( Tern (( 1. TernaryFieldEx ),a,( 0. TernaryFieldEx ))) = ( ternaryreal . (jj,x,zz))

      .= ((x * 1) + 0 ) by Def2

      .= a;

    end;

    

     Lm3: for a,b be Scalar of TernaryFieldEx holds ( Tern (a,( 0. TernaryFieldEx ),b)) = b

    proof

      let a,b be Scalar of TernaryFieldEx ;

      reconsider x = a, y = b as Real;

      

      thus ( Tern (a,( 0. TernaryFieldEx ),b)) = ((x * 0 ) + y) by Def2

      .= b;

    end;

    

     Lm4: for a,b be Scalar of TernaryFieldEx holds ( Tern (( 0. TernaryFieldEx ),a,b)) = b

    proof

      let a,b be Scalar of TernaryFieldEx ;

      reconsider x = a, y = b as Real;

      

      thus ( Tern (( 0. TernaryFieldEx ),a,b)) = (( 0 * x) + y) by Def2

      .= b;

    end;

    

     Lm5: for u,a,b be Scalar of TernaryFieldEx holds ex v be Scalar of TernaryFieldEx st ( Tern (u,a,v)) = b

    proof

      let u,a,b be Scalar of TernaryFieldEx ;

      reconsider z = u, x = a, y = b as Real;

      reconsider t = (y - (z * x)) as Element of REAL by XREAL_0:def 1;

      reconsider v = t as Scalar of TernaryFieldEx ;

      take v;

      y = ((z * x) + t);

      hence thesis by Def2;

    end;

    

     Lm6: for u,a,v,v9 be Scalar of TernaryFieldEx holds ( Tern (u,a,v)) = ( Tern (u,a,v9)) implies v = v9

    proof

      let u,a,v,v9 be Scalar of TernaryFieldEx ;

      reconsider z = u, x = a, y = v, y9 = v9 as Real;

      ( Tern (u,a,v)) = ((z * x) + y) & ( Tern (u,a,v9)) = ((z * x) + y9) by Def2;

      hence thesis;

    end;

    

     Lm7: for a,a9 be Scalar of TernaryFieldEx holds a <> a9 implies for b,b9 be Scalar of TernaryFieldEx holds ex u,v be Scalar of TernaryFieldEx st ( Tern (u,a,v)) = b & ( Tern (u,a9,v)) = b9

    proof

      let a,a9 be Scalar of TernaryFieldEx ;

      assume

       A1: a <> a9;

      let b,b9 be Scalar of TernaryFieldEx ;

      reconsider x = a, x9 = a9, y = b, y9 = b9 as Real;

      

       A2: (x9 - x) <> 0 by A1;

      set s = ((y9 - y) / (x9 - x));

      set t = (y - (x * s));

      reconsider u = s, v = t as Scalar of TernaryFieldEx by XREAL_0:def 1;

      take u, v;

      

      thus ( Tern (u,a,v)) = ((s * x) + (( - (s * x)) + y)) by Def2

      .= b;

      

      thus ( Tern (u,a9,v)) = ((((y9 - y) / (x9 - x)) * x9) + (( - (x * ((y9 - y) / (x9 - x)))) + y)) by Def2

      .= ((((y9 - y) / (x9 - x)) * (x9 - x)) + y)

      .= ((y9 - y) + y) by A2, XCMPLX_1: 87

      .= b9;

    end;

    

     Lm8: for u,u9 be Scalar of TernaryFieldEx holds u <> u9 implies for v,v9 be Scalar of TernaryFieldEx holds ex a be Scalar of TernaryFieldEx st ( Tern (u,a,v)) = ( Tern (u9,a,v9))

    proof

      let u,u9 be Scalar of TernaryFieldEx ;

      assume

       A1: u <> u9;

      let v,v9 be Scalar of TernaryFieldEx ;

      reconsider uu = u, uu9 = u9, vv = v, vv9 = v9 as Real;

      consider aa be Real such that

       A2: ((uu * aa) + vv) = ((uu9 * aa) + vv9) by A1, Th1;

      reconsider a = aa as Scalar of TernaryFieldEx by XREAL_0:def 1;

      ( Tern (u,a,v)) = ((uu * aa) + vv) & ( Tern (u9,a,v9)) = ((uu9 * aa) + vv9) by Def2;

      hence thesis by A2;

    end;

    

     Lm9: for a,a9,u,u9,v,v9 be Scalar of TernaryFieldEx holds ( Tern (u,a,v)) = ( Tern (u9,a,v9)) & ( Tern (u,a9,v)) = ( Tern (u9,a9,v9)) implies a = a9 or u = u9

    proof

      let a,a9,u,u9,v,v9 be Scalar of TernaryFieldEx ;

      assume

       A1: ( Tern (u,a,v)) = ( Tern (u9,a,v9)) & ( Tern (u,a9,v)) = ( Tern (u9,a9,v9));

      reconsider aa = a, aa9 = a9, uu = u, uu9 = u9, vv = v, vv9 = v9 as Real;

      

       A2: ( Tern (u,a9,v)) = ((uu * aa9) + vv) & ( Tern (u9,a9,v9)) = ((uu9 * aa9) + vv9) by Def2;

      ( Tern (u,a,v)) = ((uu * aa) + vv) & ( Tern (u9,a,v9)) = ((uu9 * aa) + vv9) by Def2;

      then (uu * (aa - aa9)) = (uu9 * (aa - aa9)) by A1, A2;

      then uu = uu9 or (aa - aa9) = 0 by XCMPLX_1: 5;

      hence thesis;

    end;

    definition

      let IT be non empty TernaryFieldStr;

      :: ALGSTR_3:def5

      attr IT is Ternary-Field-like means

      : Def5: ( 0. IT) <> ( 1. IT) & (for a be Scalar of IT holds ( Tern (a,( 1. IT),( 0. IT))) = a) & (for a be Scalar of IT holds ( Tern (( 1. IT),a,( 0. IT))) = a) & (for a,b be Scalar of IT holds ( Tern (a,( 0. IT),b)) = b) & (for a,b be Scalar of IT holds ( Tern (( 0. IT),a,b)) = b) & (for u,a,b be Scalar of IT holds ex v be Scalar of IT st ( Tern (u,a,v)) = b) & (for u,a,v,v9 be Scalar of IT holds ( Tern (u,a,v)) = ( Tern (u,a,v9)) implies v = v9) & (for a,a9 be Scalar of IT holds a <> a9 implies for b,b9 be Scalar of IT holds ex u,v be Scalar of IT st ( Tern (u,a,v)) = b & ( Tern (u,a9,v)) = b9) & (for u,u9 be Scalar of IT holds u <> u9 implies for v,v9 be Scalar of IT holds ex a be Scalar of IT st ( Tern (u,a,v)) = ( Tern (u9,a,v9))) & for a,a9,u,u9,v,v9 be Scalar of IT holds ( Tern (u,a,v)) = ( Tern (u9,a,v9)) & ( Tern (u,a9,v)) = ( Tern (u9,a9,v9)) implies a = a9 or u = u9;

    end

    registration

      cluster strict Ternary-Field-like for non empty TernaryFieldStr;

      existence by Def5, Lm1, Lm2, Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, Lm9;

    end

    definition

      mode Ternary-Field is Ternary-Field-like non empty TernaryFieldStr;

    end

    reserve F for Ternary-Field;

    reserve a,a9,b,c,x,x9,u,u9,v,v9,z for Scalar of F;

    theorem :: ALGSTR_3:4

    a <> a9 & ( Tern (u,a,v)) = ( Tern (u9,a,v9)) & ( Tern (u,a9,v)) = ( Tern (u9,a9,v9)) implies u = u9 & v = v9

    proof

      assume that

       A1: a <> a9 and

       A2: ( Tern (u,a,v)) = ( Tern (u9,a,v9)) and

       A3: ( Tern (u,a9,v)) = ( Tern (u9,a9,v9));

      u = u9 by A1, A2, A3, Def5;

      hence thesis by A2, Def5;

    end;

    theorem :: ALGSTR_3:5

    a <> ( 0. F) implies for b, c holds ex x st ( Tern (a,x,b)) = c

    proof

      assume

       A1: a <> ( 0. F);

      let b, c;

      consider x such that

       A2: ( Tern (a,x,b)) = ( Tern (( 0. F),x,c)) by A1, Def5;

      take x;

      thus thesis by A2, Def5;

    end;

    theorem :: ALGSTR_3:6

    a <> ( 0. F) & ( Tern (a,x,b)) = ( Tern (a,x9,b)) implies x = x9

    proof

      assume that

       A1: a <> ( 0. F) and

       A2: ( Tern (a,x,b)) = ( Tern (a,x9,b));

      set c = ( Tern (a,x,b));

      

       A3: ( Tern (a,x,b)) = ( Tern (( 0. F),x,c)) by Def5;

      ( Tern (a,x9,b)) = ( Tern (( 0. F),x9,c)) by A2, Def5;

      hence thesis by A1, A3, Def5;

    end;

    theorem :: ALGSTR_3:7

    a <> ( 0. F) implies for b, c holds ex x st ( Tern (x,a,b)) = c

    proof

      assume

       A1: a <> ( 0. F);

      let b, c;

      consider x, z such that

       A2: ( Tern (x,a,z)) = c & ( Tern (x,( 0. F),z)) = b by A1, Def5;

      take x;

      thus thesis by A2, Def5;

    end;

    theorem :: ALGSTR_3:8

    a <> ( 0. F) & ( Tern (x,a,b)) = ( Tern (x9,a,b)) implies x = x9

    proof

      assume

       A1: a <> ( 0. F) & ( Tern (x,a,b)) = ( Tern (x9,a,b));

      ( Tern (x,( 0. F),b)) = b & ( Tern (x9,( 0. F),b)) = b by Def5;

      hence thesis by A1, Def5;

    end;