fvaluat1.miz



    begin

    reserve x,y,z,s for ExtReal;

    reserve i,j for Integer;

    reserve n,m for Nat;

    theorem :: FVALUAT1:1

    

     Th1: x = ( - x) implies x = 0

    proof

      per cases by XXREAL_0: 14;

        suppose x = +infty or x = -infty ;

        hence thesis;

      end;

        suppose x in REAL ;

        then

        reconsider y = x as Element of REAL ;

        ( - x) = ( - y) by XXREAL_3:def 3;

        hence thesis;

      end;

    end;

    theorem :: FVALUAT1:2

    

     Th2: (x + x) = 0 implies x = 0

    proof

      assume (x + x) = 0 ;

      then x = ( - x) by XXREAL_3: 8;

      hence thesis by Th1;

    end;

    theorem :: FVALUAT1:3

    

     Th3: 0 <= x & x <= y & 0 <= s & s <= z implies (x * s) <= (y * z)

    proof

      assume that

       A1: 0 <= x and

       A2: x <= y and

       A3: 0 <= s and

       A4: s <= z;

      

       A5: (x * s) <= (y * s) by A2, A3, XXREAL_3: 71;

      (y * s) <= (y * z) by A1, A2, A4, XXREAL_3: 71;

      hence thesis by A5, XXREAL_0: 2;

    end;

     Lm1:

    now

      let a,b be Real, c,d be ExtReal;

      assume

       A1: a = c & b = d;

      then ( - b) = ( - d) by XXREAL_3:def 3;

      hence (a - b) = (c - d) by A1, XXREAL_3:def 2;

    end;

    theorem :: FVALUAT1:4

    y <> +infty & 0 < x & 0 < y implies 0 < (x / y)

    proof

      assume that

       A1: y <> +infty and

       A2: 0 < x and

       A3: 0 < y;

      per cases by XXREAL_0: 14;

        suppose x in REAL ;

        then

        reconsider x1 = x as Element of REAL ;

        reconsider y1 = y as Element of REAL by A1, A3, XXREAL_0: 14;

        (x / y) = (x1 / y1);

        hence thesis by A2, A3;

      end;

        suppose x = +infty ;

        hence thesis by A1, A3, XXREAL_3: 83;

      end;

        suppose x = -infty ;

        hence thesis by A2;

      end;

    end;

    theorem :: FVALUAT1:5

    

     Th5: y <> +infty & x < 0 & 0 < y implies (x / y) < 0

    proof

      assume that

       A1: y <> +infty and

       A2: x < 0 and

       A3: 0 < y;

      reconsider y1 = y as Element of REAL by A3, A1, XXREAL_0: 14;

      per cases by XXREAL_0: 14;

        suppose x in REAL ;

        then

        reconsider x1 = x as Real;

        (x / y) = (x1 / y1);

        hence thesis by A2, A3;

      end;

        suppose x = +infty ;

        hence thesis by A2;

      end;

        suppose x = -infty ;

        hence thesis by A1, A3, XXREAL_3: 86;

      end;

    end;

    theorem :: FVALUAT1:6

    y <> -infty & 0 < x & y < 0 implies (x / y) < 0

    proof

      assume that

       A1: y <> -infty and

       A2: 0 < x and

       A3: y < 0 ;

      reconsider y1 = y as Element of REAL by A1, A3, XXREAL_0: 14;

      per cases by XXREAL_0: 14;

        suppose x in REAL ;

        then

        reconsider x1 = x as Real;

        (x / y) = (x1 / y1);

        hence thesis by A2, A3;

      end;

        suppose x = +infty ;

        hence thesis by A1, A3, XXREAL_3: 85;

      end;

        suppose x = -infty ;

        hence thesis by A2;

      end;

    end;

    theorem :: FVALUAT1:7

    

     Th7: x in REAL & y in REAL or z in REAL implies ((x + y) / z) = ((x / z) + (y / z))

    proof

      assume

       A1: x in REAL & y in REAL or z in REAL ;

      per cases by A1;

        suppose x in REAL & y in REAL ;

        then

        reconsider x1 = x, y1 = y as Real;

        per cases by XXREAL_0: 14;

          suppose z in REAL ;

          hence thesis by XXREAL_3: 95;

        end;

          suppose

           A2: z = +infty or z = -infty ;

          

          thus ((x + y) / z) = ( 0 + 0 ) by A2

          .= ((x / z) + (y / z)) by A2;

        end;

      end;

        suppose z in REAL ;

        hence thesis by XXREAL_3: 95;

      end;

    end;

    theorem :: FVALUAT1:8

    

     Th8: y <> +infty & y <> -infty & y <> 0 implies ((x / y) * y) = x

    proof

      assume that

       A1: y <> +infty & y <> -infty and

       A2: y <> 0 ;

      

      thus ((x / y) * y) = ((x * (1 / y)) * y) by XXREAL_3: 81

      .= (x * ((1 / y) * y)) by XXREAL_3: 66

      .= (x * 1) by A1, A2, XXREAL_3: 87

      .= x by XXREAL_3: 81;

    end;

    theorem :: FVALUAT1:9

    

     Th9: y <> -infty & y <> +infty & x <> 0 & y <> 0 implies (x / y) <> 0

    proof

      assume that

       A1: y <> -infty & y <> +infty and

       A2: x <> 0 and

       A3: y <> 0 ;

      assume (x / y) = 0 ;

      then (y " ) = 0 by A2;

      hence thesis by A1, A3, XXREAL_3: 82;

    end;

    definition

      let x be object;

      :: FVALUAT1:def1

      attr x is ext-integer means

      : Def1: x is integer or x = +infty ;

    end

    registration

      cluster ext-integer -> ext-real for object;

      coherence ;

    end

    registration

      cluster +infty -> ext-integer;

      coherence ;

      cluster -infty -> non ext-integer;

      coherence ;

      cluster 1. -> ext-integer positive real;

      coherence ;

      cluster integer -> ext-integer for object;

      coherence ;

      cluster real ext-integer -> integer for object;

      coherence ;

    end

    registration

      cluster real ext-integer positive for Element of ExtREAL ;

      existence

      proof

        take 1. ;

        thus thesis;

      end;

      cluster positive for ext-integer object;

      existence

      proof

        take +infty ;

        thus thesis;

      end;

    end

    definition

      mode ExtInt is ext-integer object;

    end

    reserve x,y,v,u for ExtInt;

    theorem :: FVALUAT1:10

    

     Th10: x < y implies (x + 1) <= y

    proof

      assume

       A1: x < y;

      per cases ;

        suppose x in REAL & y in REAL ;

        then

        reconsider x1 = x, y1 = y as Real;

        ex p,q be Real st p = (x + 1. ) & q = y & p <= q

        proof

          take (x1 + 1), y1;

          thus (x1 + 1) = (x + 1. ) by XXREAL_3:def 2;

          thus y1 = y;

          thus (x1 + 1) <= y1 by A1, INT_1: 7;

        end;

        hence thesis;

      end;

        suppose not x in REAL or not y in REAL ;

        then x = +infty or x = -infty or y = +infty or y = -infty by XXREAL_0: 14;

        hence thesis by A1, XXREAL_0: 3;

      end;

    end;

    theorem :: FVALUAT1:11

     -infty < x

    proof

      x is Integer or x = +infty by Def1;

      then x in REAL or x = +infty by XREAL_0:def 1;

      hence thesis by XXREAL_0: 12;

    end;

    definition

      let X be ext-real-membered set;

      given i0 be positive ExtInt such that

       A1: i0 in X;

      :: FVALUAT1:def2

      func least-positive (X) -> positive ExtInt means

      : Def2: it in X & for i be positive ExtInt st i in X holds it <= i;

      existence

      proof

        defpred P[ Integer] means $1 in X & $1 is positive;

        per cases ;

          suppose ex i be positive Integer st i in X;

          then

           A2: ex i be Integer st P[i];

          

           A3: for i be Integer st P[i] holds 0 <= i;

          consider j0 be Integer such that

           A4: P[j0] and

           A5: for i be Integer st P[i] holds j0 <= i from INT_1:sch 5( A3, A2);

          reconsider j = j0 as positive ExtInt by A4;

          take j;

          thus j in X by A4;

          let i be positive ExtInt;

          assume

           A6: i in X;

          per cases ;

            suppose i is Integer;

            then

            reconsider i1 = i as Integer;

            j0 <= i1 by A6, A5;

            hence j <= i;

          end;

            suppose not i is Integer;

            then i = +infty by Def1;

            hence thesis by XXREAL_0: 3;

          end;

        end;

          suppose

           A7: not ex i be positive Integer st i in X;

          take i0;

          thus i0 in X by A1;

          let i be positive ExtInt;

          assume i in X;

          then not i is positive Integer & +infty <= +infty by A7;

          then i = +infty by Def1;

          hence i0 <= i by XXREAL_0: 3;

        end;

      end;

      uniqueness

      proof

        let a,b be positive ExtInt;

        assume a in X & (for i be positive ExtInt st i in X holds a <= i) & b in X & for i be positive ExtInt st i in X holds b <= i;

        then a <= b & b <= a;

        hence thesis by XXREAL_0: 1;

      end;

    end

    definition

      let f be Relation;

      :: FVALUAT1:def3

      attr f is e.i.-valued means

      : Def3: for x be set st x in ( rng f) holds x is ext-integer;

    end

    registration

      cluster e.i.-valued for Function;

      existence

      proof

        take f = ( 0 --> 0. );

        let x be set;

        ( rng f) c= { 0 } by FUNCOP_1: 13;

        hence thesis;

      end;

    end

    registration

      let A be set;

      cluster e.i.-valued for Function of A, ExtREAL ;

      existence

      proof

        take f = (A --> 0. );

        let x be set;

        ( rng f) c= { 0 } by FUNCOP_1: 13;

        hence thesis;

      end;

    end

    registration

      let f be e.i.-valued Function, x be set;

      cluster (f . x) -> ext-integer;

      coherence

      proof

        per cases ;

          suppose x in ( dom f);

          then (f . x) in ( rng f) by FUNCT_1:def 3;

          hence thesis by Def3;

        end;

          suppose not x in ( dom f);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    begin

    theorem :: FVALUAT1:12

    

     Th12: for K be distributive left_unital add-associative right_zeroed right_complementable non empty doubleLoopStr holds (( - ( 1. K)) * ( - ( 1. K))) = ( 1. K)

    proof

      let K be distributive left_unital add-associative right_zeroed right_complementable non empty doubleLoopStr;

      

      thus (( - ( 1. K)) * ( - ( 1. K))) = (( 1. K) * ( 1. K)) by VECTSP_1: 10

      .= ( 1. K);

    end;

    definition

      let K be non empty doubleLoopStr;

      let S be Subset of K;

      let n be Nat;

      :: FVALUAT1:def4

      func S |^ n -> Subset of K means

      : Def4: it = the carrier of K if n = 0

      otherwise ex f be FinSequence of ( bool the carrier of K) st it = (f . ( len f)) & ( len f) = n & (f . 1) = S & for i be Nat st i in ( dom f) & (i + 1) in ( dom f) holds (f . (i + 1)) = (S *' (f /. i));

      consistency ;

      existence

      proof

        hereby

          assume n = 0 ;

          take A = ( [#] K);

          thus A = the carrier of K;

        end;

        assume

         A1: n <> 0 ;

        set D = ( bool the carrier of K);

        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

        defpred P[ set, set, set] means ex A be Subset of K st A = $2 & $3 = (S *' A);

        

         A2: for i be Nat st 1 <= i & i < n1 holds for x be Element of D holds ex y be Element of D st P[i, x, y]

        proof

          let i be Nat such that 1 <= i & i < n1;

          let x be Element of D;

          take (S *' x);

          thus thesis;

        end;

        consider f be FinSequence of D such that

         A3: ( len f) = n1 and

         A4: (f . 1) = S or n1 = 0 and

         A5: for i be Nat st 1 <= i & i < n1 holds P[i, (f . i), (f . (i + 1))] from RECDEF_1:sch 4( A2);

        take (f /. ( len f)), f;

        ( len f) in ( dom f) by A1, A3, CARD_1: 27, FINSEQ_5: 6;

        hence (f /. ( len f)) = (f . ( len f)) by PARTFUN1:def 6;

        thus ( len f) = n by A3;

        thus (f . 1) = S by A1, A4;

        let i be Nat such that

         A6: i in ( dom f);

        assume (i + 1) in ( dom f);

        then (i + 1) <= n1 by A3, FINSEQ_3: 25;

        then

         A7: i < n1 by NAT_1: 13;

        1 <= i by A6, FINSEQ_3: 25;

        then P[i, (f . i), (f . (i + 1))] by A5, A7;

        hence thesis by A6, PARTFUN1:def 6;

      end;

      uniqueness

      proof

        let S1,S2 be Subset of K;

        thus n = 0 & S1 = the carrier of K & S2 = the carrier of K implies S1 = S2;

        assume n <> 0 ;

        given f be FinSequence of ( bool the carrier of K) such that

         A8: S1 = (f . ( len f)) and

         A9: ( len f) = n and

         A10: (f . 1) = S and

         A11: for i be Nat st i in ( dom f) & (i + 1) in ( dom f) holds (f . (i + 1)) = (S *' (f /. i));

        given g be FinSequence of ( bool the carrier of K) such that

         A12: S2 = (g . ( len g)) and

         A13: ( len g) = n and

         A14: (g . 1) = S and

         A15: for i be Nat st i in ( dom g) & (i + 1) in ( dom g) holds (g . (i + 1)) = (S *' (g /. i));

        

         A16: ( dom f) = ( dom g) by A9, A13, FINSEQ_3: 29;

        for k be Nat st k in ( dom f) holds (f . k) = (g . k)

        proof

          let k be Nat;

          defpred P[ Nat] means $1 in ( dom f) implies (f . $1) = (g . $1);

          

           A17: P[ 0 ] by FINSEQ_3: 24;

          

           A18: for a be Nat st P[a] holds P[(a + 1)]

          proof

            let a be Nat such that

             A19: P[a] and

             A20: (a + 1) in ( dom f);

            per cases ;

              suppose

               A21: a in ( dom f);

              

              then

               A22: (f /. a) = (f . a) by PARTFUN1:def 6

              .= (g /. a) by A16, A19, A21, PARTFUN1:def 6;

              

              thus (f . (a + 1)) = (S *' (f /. a)) by A11, A20, A21

              .= (g . (a + 1)) by A15, A16, A20, A21, A22;

            end;

              suppose not a in ( dom f);

              then a = 0 by A20, TOPREALA: 2;

              hence thesis by A10, A14;

            end;

          end;

          for a be Nat holds P[a] from NAT_1:sch 2( A17, A18);

          hence thesis;

        end;

        hence S1 = S2 by A8, A12, A9, A13, A16, FINSEQ_1: 13;

      end;

    end

    reserve D for non empty doubleLoopStr,

A for Subset of D;

    theorem :: FVALUAT1:13

    (A |^ 1) = A

    proof

      set f = <*A*>;

      

       A1: ( len f) = 1 & (f . 1) = A by FINSEQ_1: 40;

      now

        let i be Nat such that

         A2: i in ( dom f) & (i + 1) in ( dom f);

        ( dom f) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then i = 1 & (i + 1) = 1 by A2, TARSKI:def 1;

        hence (f . (i + 1)) = (A *' (f /. i));

      end;

      hence thesis by A1, Def4;

    end;

    theorem :: FVALUAT1:14

    (A |^ 2) = (A *' A)

    proof

      set f = <*A, (A *' A)*>;

      

       A1: ( len f) = 2 by FINSEQ_1: 44;

      

       A2: (f . 1) = A by FINSEQ_1: 44;

      

       A3: (f . 2) = (A *' A) by FINSEQ_1: 44;

      now

        let i be Nat such that

         A4: i in ( dom f) and

         A5: (i + 1) in ( dom f);

        ( dom f) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        then (i = 1 or i = 2) & ((i + 1) = 1 or (i + 1) = 2) by A4, A5, TARSKI:def 2;

        hence (f . (i + 1)) = (A *' (f /. i)) by A2, A3, A4, PARTFUN1:def 6;

      end;

      hence thesis by A1, A2, A3, Def4;

    end;

    registration

      let R be Ring;

      let S be Ideal of R;

      let n be Nat;

      cluster (S |^ n) -> non empty add-closed left-ideal right-ideal;

      coherence

      proof

        per cases by NAT_1: 6;

          suppose

           A1: n = 0 ;

          

           A2: (S |^ 0 ) = the carrier of R by Def4;

          thus (S |^ n) is non empty by A1, Def4;

          thus (S |^ n) is add-closed by A2, A1;

          thus (S |^ n) is left-ideal by A2, A1;

          let p,x be Element of R;

          thus thesis by A2, A1;

        end;

          suppose

           A3: ex k be Nat st n = (k + 1);

          then

          consider f be FinSequence of ( bool the carrier of R) such that

           A4: (S |^ n) = (f . ( len f)) & ( len f) = n & (f . 1) = S and

           A5: for i be Nat st i in ( dom f) & (i + 1) in ( dom f) holds (f . (i + 1)) = (S *' (f /. i)) by Def4;

          defpred P[ Nat] means $1 in ( dom f) implies (f . $1) is Ideal of R;

          

           A6: P[ 0 ] by FINSEQ_3: 24;

          

           A7: for m st P[m] holds P[(m + 1)]

          proof

            let m;

            assume that

             A8: P[m] and

             A9: (m + 1) in ( dom f);

            per cases by A9, TOPREALA: 2;

              suppose m = 0 ;

              hence thesis by A4;

            end;

              suppose

               A10: m in ( dom f);

              then

               A11: (f /. m) = (f . m) by PARTFUN1:def 6;

              (f . (m + 1)) = (S *' (f /. m)) by A5, A9, A10;

              hence thesis by A10, A8, A11;

            end;

          end;

          

           A12: for m holds P[m] from NAT_1:sch 2( A6, A7);

          ( 0 + 1) <= ( len f) by A3, A4, NAT_1: 13;

          then ( len f) in ( dom f) by FINSEQ_3: 25;

          hence thesis by A4, A12;

        end;

      end;

    end

    definition

      let G be non empty doubleLoopStr, g be Element of G, i be Integer;

      :: FVALUAT1:def5

      func g |^ i -> Element of G equals

      : Def5: (( power G) . (g, |.i.|)) if 0 <= i

      otherwise ( / (( power G) . (g, |.i.|)));

      correctness ;

    end

    definition

      let G be non empty doubleLoopStr, g be Element of G, n be Nat;

      :: original: |^

      redefine

      :: FVALUAT1:def6

      func g |^ n equals (( power G) . (g,n));

      compatibility

      proof

        let g be Element of G;

         |.n.| = n by ABSVALUE:def 1;

        hence thesis by Def5;

      end;

    end

    reserve K for Field-like non degenerated associative add-associative right_zeroed right_complementable distributive Abelian non empty doubleLoopStr,

a,b,c for Element of K;

    

     Lm2: (a |^ (n + 1)) = ((a |^ n) * a) by GROUP_1:def 7;

    theorem :: FVALUAT1:15

    (a |^ (n + m)) = ((a |^ n) * (a |^ m))

    proof

      defpred P[ Nat] means for n holds (a |^ (n + $1)) = ((a |^ n) * (a |^ $1));

      

       A1: P[ 0 ]

      proof

        let n;

        

        thus (a |^ (n + 0 )) = ((a |^ n) * ( 1_ K))

        .= ((a |^ n) * (a |^ 0 )) by GROUP_1:def 7;

      end;

      

       A2: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        assume

         A3: for n holds (a |^ (n + m)) = ((a |^ n) * (a |^ m));

        let n;

        

        thus (a |^ (n + (m + 1))) = (a |^ ((n + m) + 1))

        .= ((a |^ (n + m)) * a) by Lm2

        .= (((a |^ n) * (a |^ m)) * a) by A3

        .= ((a |^ n) * ((a |^ m) * a)) by GROUP_1:def 3

        .= ((a |^ n) * (a |^ (m + 1))) by Lm2;

      end;

      for m holds P[m] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    

     Lm3: a <> ( 0. K) implies (a |^ n) <> ( 0. K)

    proof

      assume

       A1: a <> ( 0. K);

      defpred P[ Nat] means (a |^ $1) <> ( 0. K);

      (a |^ 0 ) = ( 1_ K) by GROUP_1:def 7;

      then

       A2: P[ 0 ];

      

       A3: for n holds P[n] implies P[(n + 1)]

      proof

        let n;

        assume

         A4: P[n];

        (a |^ (n + 1)) = ((a |^ n) * a) by Lm2;

        hence (a |^ (n + 1)) <> ( 0. K) by A4, A1, VECTSP_1: 12;

      end;

      for n holds P[n] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

    theorem :: FVALUAT1:16

    

     Th16: a <> ( 0. K) implies (a |^ i) <> ( 0. K)

    proof

      assume

       A1: a <> ( 0. K);

      per cases ;

        suppose 0 <= i;

        then

        reconsider n1 = i as Element of NAT by INT_1: 3;

        (a |^ i) = (a |^ n1);

        hence (a |^ i) <> ( 0. K) by A1, Lm3;

      end;

        suppose

         A2: i < 0 ;

        then

        reconsider n1 = ( - i) as Element of NAT by INT_1: 3;

        

         A3: (a |^ i) = ((( power K) . (a, |.i.|)) " ) by A2, Def5

        .= ((a |^ n1) " ) by A2, ABSVALUE:def 1;

        (a |^ n1) <> ( 0. K) by A1, Lm3;

        hence (a |^ i) <> ( 0. K) by A3, VECTSP_2: 13;

      end;

    end;

    begin

    definition

      let K be doubleLoopStr;

      :: FVALUAT1:def7

      attr K is having_valuation means ex f be e.i.-valued Function of K, ExtREAL st (f . ( 0. K)) = +infty & (for a be Element of K st a <> ( 0. K) holds (f . a) in INT ) & (for a,b be Element of K holds (f . (a * b)) = ((f . a) + (f . b))) & (for a be Element of K st 0 <= (f . a) holds 0 <= (f . (( 1. K) + a))) & ex a be Element of K st (f . a) <> 0 & (f . a) <> +infty ;

    end

    definition

      let K be doubleLoopStr;

      :: FVALUAT1:def8

      mode Valuation of K -> e.i.-valued Function of K, ExtREAL means

      : Def8: (it . ( 0. K)) = +infty & (for a be Element of K st a <> ( 0. K) holds (it . a) in INT ) & (for a,b be Element of K holds (it . (a * b)) = ((it . a) + (it . b))) & (for a be Element of K st 0 <= (it . a) holds 0 <= (it . (( 1. K) + a))) & ex a be Element of K st (it . a) <> 0 & (it . a) <> +infty ;

      existence by A1;

    end

    reserve v for Valuation of K;

    theorem :: FVALUAT1:17

    

     Th17: K is having_valuation implies (v . ( 1. K)) = 0

    proof

      assume

       A1: K is having_valuation;

      

       A2: (v . ( 1. K)) = (v . (( 1. K) * ( 1. K)))

      .= ((v . ( 1. K)) + (v . ( 1. K))) by A1, Def8;

      (v . ( 1. K)) in INT by A1, Def8;

      then

      reconsider x = (v . ( 1. K)) as Element of REAL by XREAL_0:def 1;

      (x + 0 ) = (x + x) by A2, XXREAL_3:def 2;

      hence thesis;

    end;

    theorem :: FVALUAT1:18

    

     Th18: K is having_valuation & a <> ( 0. K) implies (v . a) <> +infty

    proof

      assume K is having_valuation & a <> ( 0. K);

      then (v . a) in INT by Def8;

      hence thesis;

    end;

    theorem :: FVALUAT1:19

    

     Th19: K is having_valuation implies (v . ( - ( 1. K))) = 0

    proof

      assume

       A1: K is having_valuation;

      (( - ( 1. K)) * ( - ( 1. K))) = ( 1. K) by Th12;

      

      then ((v . ( - ( 1. K))) + (v . ( - ( 1. K)))) = (v . ( 1. K)) by A1, Def8

      .= 0 by A1, Th17;

      hence thesis by Th2;

    end;

    theorem :: FVALUAT1:20

    

     Th20: K is having_valuation implies (v . ( - a)) = (v . a)

    proof

      assume

       A1: K is having_valuation;

      (( - ( 1. K)) * a) = ( - a) by VECTSP_2: 29;

      

      hence (v . ( - a)) = ((v . ( - ( 1. K))) + (v . a)) by A1, Def8

      .= ( 0 + (v . a)) by A1, Th19

      .= (v . a) by XXREAL_3: 4;

    end;

    theorem :: FVALUAT1:21

    

     Th21: K is having_valuation & a <> ( 0. K) implies (v . (a " )) = ( - (v . a))

    proof

      assume that

       A1: K is having_valuation and

       A2: a <> ( 0. K);

      (a * (a " )) = ( 1. K) by A2, VECTSP_2:def 2;

      

      then

       A3: ((v . a) + (v . (a " ))) = (v . ( 1. K)) by A1, Def8

      .= 0 by A1, Th17;

      now

        assume (a " ) = ( 0. K);

        

        then ( 1. K) = (a * ( 0. K)) by A2, VECTSP_2:def 2

        .= ( 0. K);

        hence contradiction;

      end;

      then (v . a) in INT & (v . (a " )) in INT by A1, A2, Def8;

      then

      reconsider w1 = (v . a), w2 = (v . (a " )) as Element of REAL by XREAL_0:def 1;

      (w1 + w2) = 0 by A3, XXREAL_3:def 2;

      then ( - w1) = w2;

      hence thesis by XXREAL_3:def 3;

    end;

    theorem :: FVALUAT1:22

    

     Th22: K is having_valuation & b <> ( 0. K) implies (v . (a / b)) = ((v . a) - (v . b))

    proof

      assume

       A1: K is having_valuation;

      assume

       A2: b <> ( 0. K);

      

      thus (v . (a / b)) = ((v . a) + (v . (b " ))) by A1, Def8

      .= ((v . a) - (v . b)) by A1, A2, Th21;

    end;

    theorem :: FVALUAT1:23

    

     Th23: K is having_valuation & a <> ( 0. K) & b <> ( 0. K) implies (v . (a / b)) = ( - (v . (b / a)))

    proof

      assume

       A1: K is having_valuation;

      assume

       A2: a <> ( 0. K);

      assume b <> ( 0. K);

      

      hence (v . (a / b)) = ((v . a) - (v . b)) by A1, Th22

      .= ( - ((v . b) - (v . a))) by XXREAL_3: 26

      .= ( - (v . (b / a))) by A1, A2, Th22;

    end;

    theorem :: FVALUAT1:24

    

     Th24: K is having_valuation & b <> ( 0. K) & 0 <= (v . (a / b)) implies (v . b) <= (v . a)

    proof

      assume that

       A1: K is having_valuation and

       A2: b <> ( 0. K) and

       A3: 0 <= (v . (a / b));

      

       A4: (v . (a / b)) = ((v . a) - (v . b)) by A1, A2, Th22;

      per cases ;

        suppose a = ( 0. K);

        then (v . a) = +infty by A1, Def8;

        hence (v . b) <= (v . a) by XXREAL_0: 3;

      end;

        suppose a <> ( 0. K);

        then (v . a) in INT & (v . b) in INT by A1, A2, Def8;

        then

        reconsider a1 = (v . a), b1 = (v . b) as Element of REAL by XREAL_0:def 1;

        

         A5: ((a1 - b1) + b1) = a1;

        (a1 - b1) = ((v . a) - (v . b)) by Lm1;

        then

         A6: ((v . (a / b)) + (v . b)) = (v . a) by A4, A5, XXREAL_3:def 2;

        ( 0 + (v . b)) <= ((v . (a / b)) + (v . b)) by A3, XXREAL_3: 35;

        hence (v . b) <= (v . a) by A6, XXREAL_3: 4;

      end;

    end;

    theorem :: FVALUAT1:25

    

     Th25: K is having_valuation & a <> ( 0. K) & b <> ( 0. K) & (v . (a / b)) <= 0 implies 0 <= (v . (b / a))

    proof

      assume K is having_valuation & a <> ( 0. K) & b <> ( 0. K);

      then (v . (a / b)) = ( - (v . (b / a))) by Th23;

      hence thesis;

    end;

    theorem :: FVALUAT1:26

    

     Th26: K is having_valuation & b <> ( 0. K) & (v . (a / b)) <= 0 implies (v . a) <= (v . b)

    proof

      assume that

       A1: K is having_valuation and

       A2: b <> ( 0. K) and

       A3: (v . (a / b)) <= 0 ;

      

       A4: a <> ( 0. K) by A1, Def8, A3;

      then 0 <= (v . (b / a)) by A1, A2, A3, Th25;

      hence (v . a) <= (v . b) by A1, A4, Th24;

    end;

    theorem :: FVALUAT1:27

    

     Th27: K is having_valuation implies ( min ((v . a),(v . b))) <= (v . (a + b))

    proof

      assume

       A1: K is having_valuation;

      per cases ;

        suppose

         A2: a = ( 0. K);

        then (v . a) = +infty by A1, Def8;

        then ( min ((v . a),(v . b))) = (v . b) by XXREAL_0: 42;

        hence ( min ((v . a),(v . b))) <= (v . (a + b)) by A2, RLVECT_1:def 4;

      end;

        suppose

         A3: b = ( 0. K);

        then (v . b) = +infty by A1, Def8;

        then ( min ((v . a),(v . b))) = (v . a) by XXREAL_0: 42;

        hence ( min ((v . a),(v . b))) <= (v . (a + b)) by A3, RLVECT_1:def 4;

      end;

        suppose that

         A4: a <> ( 0. K) and

         A5: 0 <= (v . (b / a));

        (v . a) <= (v . b) by A1, A4, A5, Th24;

        then

         A6: ( min ((v . a),(v . b))) = (v . a) by XXREAL_0:def 9;

         0 <= (v . (( 1. K) + (b / a))) by A5, A1, Def8;

        then

         A7: ( 0 + (v . a)) <= ((v . (( 1. K) + (b / a))) + (v . a)) by XXREAL_3: 36;

        ((v . (( 1. K) + (b / a))) + (v . a)) = (v . ((( 1. K) + (b / a)) * a)) by A1, Def8

        .= (v . ((( 1. K) * a) + ((b / a) * a))) by VECTSP_1:def 3

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

        .= (v . (a + b)) by A4, VECTSP_2: 22;

        hence ( min ((v . a),(v . b))) <= (v . (a + b)) by A6, A7, XXREAL_3: 4;

      end;

        suppose that

         A8: a <> ( 0. K) and

         A9: b <> ( 0. K) and

         A10: (v . (b / a)) <= 0 ;

        

         A11: 0 <= (v . (a / b)) by A1, A8, A9, A10, Th25;

        (v . b) <= (v . a) by A1, A8, A10, Th26;

        then

         A12: ( min ((v . a),(v . b))) = (v . b) by XXREAL_0:def 9;

         0 <= (v . (( 1. K) + (a / b))) by A11, A1, Def8;

        then

         A13: ( 0 + (v . b)) <= ((v . (( 1. K) + (a / b))) + (v . b)) by XXREAL_3: 36;

        ((v . (( 1. K) + (a / b))) + (v . b)) = (v . ((( 1. K) + (a / b)) * b)) by A1, Def8

        .= (v . ((( 1. K) * b) + ((a / b) * b))) by VECTSP_1:def 3

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

        .= (v . (b + a)) by A9, VECTSP_2: 22;

        hence ( min ((v . a),(v . b))) <= (v . (a + b)) by A12, A13, XXREAL_3: 4;

      end;

    end;

    theorem :: FVALUAT1:28

    

     Th28: K is having_valuation & (v . a) < (v . b) implies (v . a) = (v . (a + b))

    proof

      assume

       A1: K is having_valuation & (v . a) < (v . b);

      

       A2: ( min ((v . a),(v . b))) = (v . a) by A1, XXREAL_0:def 9;

      

       A3: (v . a) <= (v . (a + b)) by A2, A1, Th27;

      

       A4: a = (a + ( 0. K)) by RLVECT_1:def 4;

      

       A5: ( 0. K) = (b - b) by RLVECT_1: 15;

      

       A6: a = ((a + b) - b) by A4, A5, RLVECT_1: 28

      .= ((a + b) + ( - b));

      

       A7: (v . ( - b)) = (v . b) by A1, Th20;

      

       A8: ( min ((v . (a + b)),(v . b))) <= (v . a) by A6, A7, A1, Th27;

      then ( min ((v . (a + b)),(v . b))) = (v . (a + b)) by A1, XXREAL_0:def 9;

      hence thesis by A3, A8, XXREAL_0: 1;

    end;

    theorem :: FVALUAT1:29

    

     Th29: K is having_valuation & a <> ( 0. K) implies (v . (a |^ i)) = (i * (v . a))

    proof

      assume that

       A1: K is having_valuation and

       A2: a <> ( 0. K);

      defpred P[ Nat] means (v . (a |^ $1)) = ($1 * (v . a));

      (a |^ 0 ) = ( 1_ K) by GROUP_1:def 7;

      then

       A3: P[ 0 ] by A1, Th17;

      

       A4: P[n] implies P[(n + 1)]

      proof

        assume

         A5: P[n];

        

         A6: (v . a) in REAL by A1, A2, Th18, XXREAL_0: 14;

        reconsider N = n as ExtReal;

        

        thus (v . (a |^ (n + 1))) = (v . ((a |^ n) * a)) by Lm2

        .= ((n * (v . a)) + (v . a)) by A5, A1, Def8

        .= ((n * (v . a)) + ( 1. * (v . a))) by XXREAL_3: 81

        .= ((v . a) * (N + 1. )) by A6, XXREAL_3: 95

        .= ((n + 1) * (v . a)) by XXREAL_3:def 2;

      end;

      

       A7: P[n] from NAT_1:sch 2( A3, A4);

      per cases ;

        suppose i >= 0 ;

        then

        reconsider j = i as Element of NAT by INT_1: 3;

         P[j] by A7;

        hence thesis;

      end;

        suppose

         A8: i < 0 ;

        then

        reconsider n1 = ( - i) as Element of NAT by INT_1: 3;

        reconsider I = i as ExtReal;

        

         A9: (v . (a |^ i)) = (v . ((( power K) . (a, |.i.|)) " )) by A8, Def5

        .= (v . ((a |^ n1) " )) by A8, ABSVALUE:def 1;

        (v . ((a |^ n1) " )) = ( - (v . (a |^ n1))) by A1, A2, Th21, Lm3

        .= ( - (n1 * (v . a))) by A7

        .= ( - (( - I) * (v . a))) by XXREAL_3:def 3

        .= ( - ( - (i * (v . a)))) by XXREAL_3: 92;

        hence thesis by A9;

      end;

    end;

    theorem :: FVALUAT1:30

    

     Th30: K is having_valuation & 0 <= (v . (( 1. K) + a)) implies 0 <= (v . a)

    proof

      assume that

       A1: K is having_valuation & 0 <= (v . (( 1. K) + a)) and

       A2: (v . a) < 0 ;

       0 = (v . ( 1. K)) by A1, Th17;

      hence contradiction by A1, A2, Th28;

    end;

    theorem :: FVALUAT1:31

    K is having_valuation & 0 <= (v . (( 1. K) - a)) implies 0 <= (v . a)

    proof

      assume that

       A1: K is having_valuation and

       A2: 0 <= (v . (( 1. K) - a));

      (( 1. K) - a) = (( 1. K) + ( - a)) & (v . ( - a)) = (v . a) by A1, Th20;

      hence thesis by A1, A2, Th30;

    end;

    

     Lm4: for a,b be ExtInt st a <= b holds 0 <= (b - a)

    proof

      let a,b be ExtInt;

      assume a <= b;

      then (a + ( - a)) <= (b + ( - a)) by XXREAL_3: 36;

      hence thesis by XXREAL_3: 7;

    end;

    theorem :: FVALUAT1:32

    K is having_valuation & a <> ( 0. K) & (v . a) <= (v . b) implies 0 <= (v . (b / a))

    proof

      assume that

       A1: K is having_valuation and

       A2: a <> ( 0. K);

      assume (v . a) <= (v . b);

      then 0 <= ((v . b) - (v . a)) by Lm4;

      hence thesis by A1, A2, Th22;

    end;

    theorem :: FVALUAT1:33

    

     Th33: K is having_valuation implies +infty in ( rng v)

    proof

      assume K is having_valuation;

      then

       A1: (v . ( 0. K)) = +infty by Def8;

      ( dom v) = the carrier of K by FUNCT_2:def 1;

      hence thesis by A1, FUNCT_1:def 3;

    end;

    

     Lm5: K is having_valuation implies ( least-positive ( rng v)) in ( rng v)

    proof

      assume K is having_valuation;

      then +infty in ( rng v) by Th33;

      hence thesis by Def2;

    end;

    theorem :: FVALUAT1:34

    

     Th34: (v . a) = 1 implies ( least-positive ( rng v)) = 1

    proof

      assume

       A1: (v . a) = 1;

      ( dom v) = the carrier of K by FUNCT_2:def 1;

      then

       A2: (v . a) in ( rng v) by FUNCT_1:def 3;

      now

        let i be positive ExtInt;

        assume i in ( rng v);

        per cases by XXREAL_3: 1;

          suppose i is positive Real;

          then

          reconsider i1 = i as positive Real;

          ex p,q be Real st p = 1. & q = i & p <= q

          proof

            reconsider jj = 1, i1 as Real;

            take jj, i1;

            ( 0 + 1) <= i1 by INT_1: 7;

            hence thesis;

          end;

          hence 1. <= i;

        end;

          suppose i = +infty ;

          hence 1. <= i by XXREAL_0: 3;

        end;

      end;

      hence thesis by A1, A2, Def2;

    end;

    theorem :: FVALUAT1:35

    

     Th35: K is having_valuation implies ( least-positive ( rng v)) is integer

    proof

      set l = ( least-positive ( rng v));

      assume

       A1: K is having_valuation;

      then

      consider a such that

       A2: (v . a) <> 0 and

       A3: (v . a) <> +infty by Def8;

      

       A4: ( dom v) = the carrier of K by FUNCT_2:def 1;

      then

       A5: (v . a) in ( rng v) by FUNCT_1:def 3;

      assume not thesis;

      then

       A6: l = +infty by Def1;

      

       A7: a <> ( 0. K) by A1, A3, Def8;

      then (v . a) in INT by A1, Def8;

      then

      reconsider va = (v . a) as Real;

      per cases ;

        suppose va is positive;

        then l <= (v . a) by A5, Def2;

        hence contradiction by A3, A6, XXREAL_0: 4;

      end;

        suppose not va is positive;

        then

        reconsider va as non positive Real;

        reconsider va as negative Real by A2;

        set b = (a " );

        b <> ( 0. K) by A7, VECTSP_2: 13;

        then

         A8: (v . b) in INT by A1, Def8;

        

         A9: (v . b) in ( rng v) by A4, FUNCT_1:def 3;

        (v . b) = ( - (v . a)) by A1, A7, Th21

        .= ( - va) by XXREAL_3:def 3;

        then l <= (v . b) by A9, Def2;

        hence contradiction by A8, A6, XXREAL_0: 4;

      end;

    end;

    

     Lm6: K is having_valuation implies ( least-positive ( rng v)) in REAL

    proof

      assume K is having_valuation;

      then ( least-positive ( rng v)) is integer by Th35;

      then ( least-positive ( rng v)) in INT by INT_1:def 2;

      hence thesis by XREAL_0:def 1;

    end;

    theorem :: FVALUAT1:36

    

     Th36: K is having_valuation implies for x be Element of K st x <> ( 0. K) holds ex i be Integer st (v . x) = (i * ( least-positive ( rng v)))

    proof

      assume

       A1: K is having_valuation;

      let x be Element of K such that

       A2: x <> ( 0. K);

      reconsider vx = (v . x) as Element of INT by A1, A2, Def8;

      reconsider l = ( least-positive ( rng v)) as Integer by A1, Th35;

      

       A3: (v . x) = (((vx div l) * l) + (vx mod l)) by INT_1: 59;

      per cases ;

        suppose

         A4: (vx mod l) = 0 ;

        take (vx div l);

        thus thesis by A3, A4, XXREAL_3:def 5;

      end;

        suppose

         A5: (vx mod l) <> 0 ;

        consider k be Element of K such that

         A6: l = (v . k) by A1, Lm5, FUNCT_2: 113;

        set d = (vx div l);

        set kd = (k |^ d);

        set kD = (kd " );

        

         A7: k <> ( 0. K) by A1, A6, Def8;

        then

         A8: (d * (v . k)) = (v . kd) by A1, Th29;

        

         A9: ( - (v . kd)) = (v . kD) by A1, A7, Th16, Th21;

        

         A10: (d * l) = (d * (v . k)) by A6, XXREAL_3:def 5;

        

         A11: (v . (x * kD)) = ((v . x) - (d * l)) by A8, A9, A10, A1, Def8

        .= (vx - (d * l)) by Lm1

        .= (vx mod l) by A3;

        then

         A12: 0 <= (v . (x * kD)) by INT_1: 57;

        

         A13: (v . (x * kD)) < l by A11, INT_1: 58;

        (v . (x * kD)) in ( rng v) by FUNCT_2: 4;

        hence thesis by A12, A5, A11, A13, Def2;

      end;

    end;

    definition

      let K, v;

      assume

       A1: K is having_valuation;

      :: FVALUAT1:def9

      func Pgenerator (v) -> Element of K equals

      : Def9: the Element of (v " {( least-positive ( rng v))});

      coherence

      proof

        set l = ( least-positive ( rng v));

        l in ( rng v) by A1, Lm5;

        then {l} c= ( rng v) by ZFMISC_1: 31;

        then (v " {l}) is non empty by RELAT_1: 139;

        then the Element of (v " {l}) in (v " {l});

        hence thesis;

      end;

    end

    definition

      let K, v;

      assume

       A1: K is having_valuation;

      :: FVALUAT1:def10

      func normal-valuation (v) -> Valuation of K means

      : Def10: (v . a) = ((it . a) * ( least-positive ( rng v)));

      existence

      proof

        set l = ( least-positive ( rng v));

        reconsider ll = l as Element of ExtREAL by XXREAL_0:def 1;

        reconsider l1 = l as Integer by A1, Th35;

        

         A2: l1 in REAL by XREAL_0:def 1;

        deffunc F( Element of K) = ((v . $1) / ll);

        consider f be Function of K, ExtREAL such that

         A3: for x be Element of K holds (f . x) = F(x) from FUNCT_2:sch 4;

        for y be set st y in ( rng f) holds y is ext-integer

        proof

          let y be set;

          assume y in ( rng f);

          then

          consider x be object such that

           A4: x in ( dom f) and

           A5: (f . x) = y by FUNCT_1:def 3;

          reconsider x as Element of K by A4;

          

           A6: (f . x) = ((v . x) / l) by A3;

          per cases by Def1;

            suppose (v . x) is integer;

            then x <> ( 0. K) by A1, Def8;

            then

            consider r be Integer such that

             A7: (v . x) = (r * l) by A1, Th36;

            ((v . x) / l) = r by A2, A7, XXREAL_3: 88;

            hence thesis by A5, A3;

          end;

            suppose (v . x) = +infty ;

            hence thesis by A5, A6, A2, XXREAL_3: 83;

          end;

        end;

        then

        reconsider f as e.i.-valued Function of K, ExtREAL by Def3;

        f is Valuation of K

        proof

          thus K is having_valuation by A1;

          

          thus (f . ( 0. K)) = ((v . ( 0. K)) / l) by A3

          .= ( +infty / l) by A1, Def8

          .= +infty by A2, XXREAL_3: 83;

          thus for a st a <> ( 0. K) holds (f . a) in INT

          proof

            let a;

            assume a <> ( 0. K);

            then (v . a) in INT by A1, Def8;

            then

            reconsider va = (v . a) as Integer;

            (f . a) = ((v . a) / l) by A3

            .= (va / l1);

            hence thesis by INT_1:def 2;

          end;

          thus for a, b holds (f . (a * b)) = ((f . a) + (f . b))

          proof

            let a, b;

            

            thus (f . (a * b)) = ((v . (a * b)) / l) by A3

            .= (((v . a) + (v . b)) / l) by A1, Def8

            .= (((v . a) / l) + ((v . b) / l)) by A2, Th7

            .= ((f . a) + ((v . b) / l)) by A3

            .= ((f . a) + (f . b)) by A3;

          end;

          thus for a st 0 <= (f . a) holds 0 <= (f . (( 1. K) + a))

          proof

            let a such that

             A8: 0 <= (f . a);

            

             A9: (f . (( 1. K) + a)) = ((v . (( 1. K) + a)) / l) by A3;

            (f . a) = ((v . a) / l) by A3;

            then 0 <= (v . a) by A2, A8, Th5;

            then 0 <= (v . (( 1. K) + a)) by A1, Def8;

            hence thesis by A9;

          end;

          consider a such that

           A10: (v . a) <> 0 and

           A11: (v . a) <> +infty by A1, Def8;

          take a;

          

           A12: (f . a) = ((v . a) / l) by A3;

          hence (f . a) <> 0 by A2, A10, Th9;

          reconsider va = (v . a) as Integer by A11, Def1;

          

           A13: va in REAL by XREAL_0:def 1;

          l in REAL by A1, Lm6;

          hence (f . a) <> +infty by A12, A13;

        end;

        then

        reconsider f as Valuation of K;

        take f;

        let a;

        

        thus (v . a) = (((v . a) / l) * l) by A2, Th8

        .= ((f . a) * l) by A3;

      end;

      uniqueness

      proof

        let f,g be Valuation of K such that

         A14: for a holds (v . a) = ((f . a) * ( least-positive ( rng v))) and

         A15: for a holds (v . a) = ((g . a) * ( least-positive ( rng v)));

        

         A16: ( least-positive ( rng v)) in REAL by A1, Lm6;

        let x be Element of K;

        ((f . x) * ( least-positive ( rng v))) = (v . x) by A14

        .= ((g . x) * ( least-positive ( rng v))) by A15;

        hence thesis by A16, XXREAL_3: 68;

      end;

    end

    theorem :: FVALUAT1:37

    

     Th37: K is having_valuation implies ((v . a) = 0 iff (( normal-valuation v) . a) = 0 )

    proof

      assume K is having_valuation;

      then (v . a) = ((( normal-valuation v) . a) * ( least-positive ( rng v))) by Def10;

      hence thesis;

    end;

    theorem :: FVALUAT1:38

    

     Th38: K is having_valuation implies ((v . a) = +infty iff (( normal-valuation v) . a) = +infty )

    proof

      assume

       A1: K is having_valuation;

      set f = ( normal-valuation v);

      set l = ( least-positive ( rng v));

      

       A2: (v . a) = ((f . a) * l) by A1, Def10;

      l is integer by A1, Th35;

      hence (v . a) = +infty implies (f . a) = +infty by A2, XXREAL_3: 69;

      thus thesis by A2, XXREAL_3:def 5;

    end;

    theorem :: FVALUAT1:39

    K is having_valuation implies ((v . a) = (v . b) iff (( normal-valuation v) . a) = (( normal-valuation v) . b))

    proof

      set f = ( normal-valuation v);

      set l = ( least-positive ( rng v));

      assume

       A1: K is having_valuation;

      then

       A2: l in REAL by Lm6;

      (v . a) = ((f . a) * l) & (v . b) = ((f . b) * l) by A1, Def10;

      hence thesis by A2, XXREAL_3: 68;

    end;

    theorem :: FVALUAT1:40

    

     Th40: K is having_valuation implies ((v . a) is positive iff (( normal-valuation v) . a) is positive)

    proof

      set f = ( normal-valuation v);

      set l = ( least-positive ( rng v));

      assume

       A1: K is having_valuation;

      then

       A2: (v . a) = ((f . a) * l) by Def10;

      reconsider l1 = l as Element of REAL by A1, Lm6;

      hereby

        assume

         A3: (v . a) is positive;

        per cases by A3, XXREAL_3: 1;

          suppose (v . a) is positive Real;

          then

          reconsider va = (v . a) as positive Real;

          

           A4: va in REAL by XREAL_0:def 1;

          then (f . a) in REAL by A2, XXREAL_3: 73;

          then

          consider c,b be Complex such that

           A5: (f . a) = c & l1 = b & ((f . a) * l1) = (c * b) by XXREAL_3:def 5;

          reconsider c as Element of REAL by A4, A5, A2, XXREAL_3: 73;

          va = (c * b) by A1, Def10, A5;

          hence (f . a) is positive by A5;

        end;

          suppose (v . a) = +infty ;

          hence (f . a) is positive by A1, Th38;

        end;

      end;

      assume

       A6: (f . a) is positive;

      per cases by A6, XXREAL_3: 1;

        suppose (f . a) is positive Real;

        then

        reconsider fa = (f . a) as positive Real;

        (v . a) = (fa * l1) by A2, XXREAL_3:def 5;

        hence (v . a) is positive;

      end;

        suppose (f . a) = +infty ;

        hence (v . a) is positive by A1, Th38;

      end;

    end;

    theorem :: FVALUAT1:41

    

     Th41: K is having_valuation implies ( 0 <= (v . a) iff 0 <= (( normal-valuation v) . a))

    proof

      set f = ( normal-valuation v);

      assume

       A1: K is having_valuation;

      hereby

        assume 0 <= (v . a);

        then (v . a) is positive or 0 = (v . a);

        hence 0 <= (f . a) by A1, Th40, Th37;

      end;

      assume 0 <= (f . a);

      then (f . a) is positive or 0 = (f . a);

      hence thesis by A1, Th40, Th37;

    end;

    theorem :: FVALUAT1:42

    K is having_valuation implies ((v . a) is non negative iff (( normal-valuation v) . a) is non negative)

    proof

      set f = ( normal-valuation v);

      set l = ( least-positive ( rng v));

      assume

       A1: K is having_valuation;

      then

       A2: (v . a) = ((f . a) * l) by Def10;

      per cases ;

        suppose (v . a) is zero or (f . a) is zero;

        thus thesis by A2;

      end;

        suppose that

         A3: (v . a) is non zero and

         A4: (f . a) is non zero;

        thus (v . a) is non negative implies (f . a) is non negative by A1, A3, Th40;

        thus thesis by A4, A1, Th40;

      end;

    end;

    theorem :: FVALUAT1:43

    

     Th43: K is having_valuation implies (( normal-valuation v) . ( Pgenerator v)) = 1

    proof

      set f = ( normal-valuation v);

      set a = ( Pgenerator v);

      set l = ( least-positive ( rng v));

      assume

       A1: K is having_valuation;

      then

       A2: (v . a) = ((f . a) * l) by Def10;

      

       A3: l in REAL by A1, Lm6;

      l in ( rng v) by A1, Lm5;

      then {l} c= ( rng v) by ZFMISC_1: 31;

      then

       A4: (v " {l}) is non empty by RELAT_1: 139;

      a = the Element of (v " {l}) by A1, Def9;

      then (v . a) in {l} by A4, FUNCT_1:def 7;

      

      then (v . a) = l by TARSKI:def 1

      .= (1 * l) by XXREAL_3: 81;

      hence (f . a) = 1 by A2, A3, XXREAL_3: 68;

    end;

    theorem :: FVALUAT1:44

    K is having_valuation & 0 <= (v . a) implies (( normal-valuation v) . a) <= (v . a)

    proof

      set f = ( normal-valuation v);

      set l = ( least-positive ( rng v));

      assume

       A1: K is having_valuation;

      then

       A2: (v . a) = ((f . a) * l) by Def10;

      assume 0 <= (v . a);

      then

       A3: 0 <= (f . a) by A1, Th41;

      ( 0. qua ExtInt + 1) <= l by Th10;

      then ((f . a) * 1) <= ((f . a) * l) by A3, Th3;

      hence thesis by A2, XXREAL_3: 81;

    end;

    theorem :: FVALUAT1:45

    K is having_valuation & (v . a) = 1 implies ( normal-valuation v) = v

    proof

      set f = ( normal-valuation v);

      assume that

       A1: K is having_valuation and

       A2: (v . a) = 1;

      let a be Element of K;

      

      thus (v . a) = ((f . a) * ( least-positive ( rng v))) by A1, Def10

      .= ((f . a) * 1) by A2, Th34

      .= (f . a) by XXREAL_3: 81;

    end;

    theorem :: FVALUAT1:46

    K is having_valuation implies ( normal-valuation ( normal-valuation v)) = ( normal-valuation v)

    proof

      assume

       A1: K is having_valuation;

      set f = ( normal-valuation v);

      set g = ( normal-valuation f);

      let a be Element of K;

      set k = ( least-positive ( rng f));

      

       A2: (f . a) = ((g . a) * k) by A1, Def10;

      (f . ( Pgenerator v)) = 1 by A1, Th43;

      then k = 1 by Th34;

      hence thesis by A2, XXREAL_3: 81;

    end;

    begin

    definition

      let K be non empty doubleLoopStr;

      let v be Valuation of K;

      :: FVALUAT1:def11

      func NonNegElements v -> set equals { x where x be Element of K : 0 <= (v . x) };

      coherence ;

    end

    theorem :: FVALUAT1:47

    

     Th47: for K be non empty doubleLoopStr, v be Valuation of K, a be Element of K holds a in ( NonNegElements v) iff 0 <= (v . a)

    proof

      let K be non empty doubleLoopStr, v be Valuation of K, a be Element of K;

      hereby

        assume a in ( NonNegElements v);

        then ex x be Element of K st a = x & 0 <= (v . x);

        hence 0 <= (v . a);

      end;

      thus thesis;

    end;

    theorem :: FVALUAT1:48

    

     Th48: for K be non empty doubleLoopStr, v be Valuation of K holds ( NonNegElements v) c= the carrier of K

    proof

      let K be non empty doubleLoopStr, v be Valuation of K;

      let a be object;

      assume a in ( NonNegElements v);

      then ex x be Element of K st a = x & 0 <= (v . x);

      hence thesis;

    end;

    theorem :: FVALUAT1:49

    

     Th49: for K be non empty doubleLoopStr, v be Valuation of K holds K is having_valuation implies ( 0. K) in ( NonNegElements v)

    proof

      let K be non empty doubleLoopStr, v be Valuation of K;

      assume K is having_valuation;

      then (v . ( 0. K)) = +infty by Def8;

      hence thesis;

    end;

    theorem :: FVALUAT1:50

    

     Th50: K is having_valuation implies ( 1. K) in ( NonNegElements v)

    proof

      assume K is having_valuation;

      then (v . ( 1. K)) = 0 by Th17;

      hence thesis;

    end;

    definition

      let K, v;

      :: FVALUAT1:def12

      func ValuatRing v -> strict commutative non degenerated Ring means

      : Def12: the carrier of it = ( NonNegElements v) & the addF of it = (the addF of K | [:( NonNegElements v), ( NonNegElements v):]) & the multF of it = (the multF of K | [:( NonNegElements v), ( NonNegElements v):]) & the ZeroF of it = ( 0. K) & the OneF of it = ( 1. K);

      existence

      proof

        set c = ( NonNegElements v);

        set a = (the addF of K | [:c, c:]);

        set m = (the multF of K | [:c, c:]);

        set j = ( 1. K);

        set z = ( 0. K);

        

         A2: c c= the carrier of K by Th48;

        now

          let x be set such that

           A3: x in [:c, c:];

          set q = (the addF of K . x);

          consider x1,x2 be object such that

           A4: x1 in c and

           A5: x2 in c and

           A6: x = [x1, x2] by A3, ZFMISC_1:def 2;

          consider y1 be Element of K such that

           A7: y1 = x1 and

           A8: 0 <= (v . y1) by A4;

          consider y2 be Element of K such that

           A9: y2 = x2 and

           A10: 0 <= (v . y2) by A5;

          

           A11: ( min ((v . y1),(v . y2))) <= (v . (y1 + y2)) by A1, Th27;

           0 <= ( min ((v . y1),(v . y2))) by A8, A10, XXREAL_0: 20;

          hence q in c by A6, A7, A11, A9;

        end;

        then

        reconsider ca = c as Preserv of the addF of K by A2, REALSET1:def 1;

        (the addF of K || ca) is BinOp of c;

        then

        reconsider a as BinOp of c;

        now

          let x be set such that

           A12: x in [:c, c:];

          set q = (the multF of K . x);

          consider x1,x2 be object such that

           A13: x1 in c and

           A14: x2 in c and

           A15: x = [x1, x2] by A12, ZFMISC_1:def 2;

          consider y1 be Element of K such that

           A16: y1 = x1 and

           A17: 0 <= (v . y1) by A13;

          consider y2 be Element of K such that

           A18: y2 = x2 and

           A19: 0 <= (v . y2) by A14;

          ( 0 + 0 ) <= ((v . y1) + (v . y2)) by A17, A19;

          then 0 <= (v . (y1 * y2)) by A1, Def8;

          hence q in c by A15, A16, A18;

        end;

        then

        reconsider cm = c as Preserv of the multF of K by A2, REALSET1:def 1;

        (the multF of K || cm) is BinOp of c;

        then

        reconsider m as BinOp of c;

        

         A20: (v . z) = +infty by A1, Def8;

        reconsider j, z as Element of c by A1, Th49, Th50;

        set R = doubleLoopStr (# c, a, m, j, z #);

        z in c by A20;

        then

        reconsider R as non empty doubleLoopStr;

         A21:

        now

          let x,y be Element of R, x1,y1 be Element of K such that

           A22: x = x1 & y = y1;

           [x, y] in [:c, c:];

          hence (x + y) = (x1 + y1) by A22, FUNCT_1: 49;

        end;

         A23:

        now

          let x,y be Element of R, x1,y1 be Element of K such that

           A24: x = x1 & y = y1;

           [x, y] in [:c, c:];

          hence (x * y) = (x1 * y1) by A24, FUNCT_1: 49;

        end;

         A25:

        now

          let x,e be Element of R;

          assume

           A26: e = j;

          reconsider x1 = x, e1 = e as Element of K by A2;

          

          thus (x * e) = (x1 * e1) by A23

          .= x by A26;

          

          thus (e * x) = (e1 * x1) by A23

          .= x by A26;

        end;

        R is well-unital by A25;

        then

        reconsider R as well-unital non empty doubleLoopStr;

        R is Abelian add-associative right_zeroed right_complementable commutative associative distributive non degenerated

        proof

          hereby

            let x,y be Element of R;

            reconsider x1 = x, y1 = y as Element of K by A2;

            

            thus (x + y) = (x1 + y1) by A21

            .= (y + x) by A21;

          end;

          hereby

            let x,y,z be Element of R;

            reconsider x1 = x, y1 = y, z1 = z as Element of K by A2;

            

             A27: (y + z) = (y1 + z1) by A21;

            (x + y) = (x1 + y1) by A21;

            

            hence ((x + y) + z) = ((x1 + y1) + z1) by A21

            .= (x1 + (y1 + z1)) by RLVECT_1:def 3

            .= (x + (y + z)) by A27, A21;

          end;

          hereby

            let x be Element of R;

            reconsider x1 = x as Element of K by A2;

            

            thus (x + ( 0. R)) = (x1 + ( 0. K)) by A21

            .= x by RLVECT_1:def 4;

          end;

          thus R is right_complementable

          proof

            let x be Element of R;

            reconsider x1 = x as Element of K by A2;

            consider w1 be Element of K such that

             A28: (x1 + w1) = ( 0. K) by ALGSTR_0:def 11;

            

             A29: (v . (x1 + w1)) = +infty by A1, A28, Def8;

            per cases ;

              suppose (v . w1) < (v . x1);

              then (v . w1) = (v . (w1 + x1)) by A1, Th28;

              then

              reconsider w = w1 as Element of R by A29, Th47;

              take w;

              thus (x + w) = ( 0. R) by A28, A21;

            end;

              suppose

               A30: (v . x1) <= (v . w1);

               0 <= (v . x1) by Th47;

              then

              reconsider w = w1 as Element of R by A30, Th47;

              take w;

              thus (x + w) = ( 0. R) by A28, A21;

            end;

          end;

          hereby

            let x,y be Element of R;

            reconsider x1 = x, y1 = y as Element of K by A2;

            

            thus (x * y) = (x1 * y1) by A23

            .= (y * x) by A23;

          end;

          hereby

            let x,y,z be Element of R;

            reconsider x1 = x, y1 = y, z1 = z as Element of K by A2;

            

             A31: (y * z) = (y1 * z1) by A23;

            (x * y) = (x1 * y1) by A23;

            

            hence ((x * y) * z) = ((x1 * y1) * z1) by A23

            .= (x1 * (y1 * z1)) by GROUP_1:def 3

            .= (x * (y * z)) by A31, A23;

          end;

          hereby

            let x,y,z be Element of R;

            reconsider x1 = x, y1 = y, z1 = z as Element of K by A2;

            

             A32: (y + z) = (y1 + z1) by A21;

            

             A33: (x * y) = (x1 * y1) by A23;

            

             A34: (x * z) = (x1 * z1) by A23;

            

             A35: (y * x) = (y1 * x1) by A23;

            

             A36: (z * x) = (z1 * x1) by A23;

            

            thus (x * (y + z)) = (x1 * (y1 + z1)) by A32, A23

            .= ((x1 * y1) + (x1 * z1)) by VECTSP_1:def 2

            .= ((x * y) + (x * z)) by A21, A33, A34;

            

            thus ((y + z) * x) = ((y1 + z1) * x1) by A32, A23

            .= ((y1 * x1) + (z1 * x1)) by VECTSP_1:def 2

            .= ((y * x) + (z * x)) by A21, A35, A36;

          end;

          thus ( 0. R) <> ( 1. R);

        end;

        hence thesis;

      end;

      uniqueness ;

    end

    theorem :: FVALUAT1:51

    

     Th51: K is having_valuation implies for x be Element of ( ValuatRing v) holds x is Element of K

    proof

      assume

       A1: K is having_valuation;

      let x be Element of ( ValuatRing v);

      the carrier of ( ValuatRing v) = ( NonNegElements v) by A1, Def12;

      then x in ( NonNegElements v) & ( NonNegElements v) c= the carrier of K by Th48;

      hence thesis;

    end;

    theorem :: FVALUAT1:52

    

     Th52: K is having_valuation implies ( 0 <= (v . a) iff a is Element of ( ValuatRing v))

    proof

      assume K is having_valuation;

      then the carrier of ( ValuatRing v) = ( NonNegElements v) by Def12;

      hence thesis by Th47;

    end;

    theorem :: FVALUAT1:53

    

     Th53: K is having_valuation implies for S be Subset of ( ValuatRing v) holds 0 is LowerBound of (v .: S)

    proof

      assume

       A1: K is having_valuation;

      let S be Subset of ( ValuatRing v);

      let x be ExtReal;

      assume x in (v .: S);

      then

       A2: ex c be Element of K st c in S & x = (v . c) by FUNCT_2: 65;

      the carrier of ( ValuatRing v) = ( NonNegElements v) by A1, Def12;

      hence thesis by A2, Th47;

    end;

    theorem :: FVALUAT1:54

    

     Th54: K is having_valuation implies for x,y be Element of K, x1,y1 be Element of ( ValuatRing v) st x = x1 & y = y1 holds (x + y) = (x1 + y1)

    proof

      set R = ( ValuatRing v);

      set c = ( NonNegElements v);

      assume

       A1: K is having_valuation;

      let x,y be Element of K, x1,y1 be Element of R such that

       A2: x = x1 & y = y1;

      

       A3: c = the carrier of R by A1, Def12;

      

       A4: the addF of R = (the addF of K | [:c, c:]) by A1, Def12;

      

      thus (x1 + y1) = (the addF of R . [x1, y1])

      .= (x + y) by A3, A4, A2, FUNCT_1: 49;

    end;

    theorem :: FVALUAT1:55

    

     Th55: K is having_valuation implies for x,y be Element of K, x1,y1 be Element of ( ValuatRing v) st x = x1 & y = y1 holds (x * y) = (x1 * y1)

    proof

      set R = ( ValuatRing v);

      set c = ( NonNegElements v);

      assume

       A1: K is having_valuation;

      let x,y be Element of K, x1,y1 be Element of R such that

       A2: x = x1 & y = y1;

      

       A3: c = the carrier of R by A1, Def12;

      

       A4: the multF of R = (the multF of K | [:c, c:]) by A1, Def12;

      

      thus (x1 * y1) = (the multF of R . [x1, y1])

      .= (x * y) by A3, A4, A2, FUNCT_1: 49;

    end;

    theorem :: FVALUAT1:56

    K is having_valuation implies ( 0. ( ValuatRing v)) = ( 0. K) by Def12;

    theorem :: FVALUAT1:57

    K is having_valuation implies ( 1. ( ValuatRing v)) = ( 1. K) by Def12;

    theorem :: FVALUAT1:58

    K is having_valuation implies for x be Element of K, y be Element of ( ValuatRing v) st x = y holds ( - x) = ( - y)

    proof

      set R = ( ValuatRing v);

      set c = ( NonNegElements v);

      assume

       A1: K is having_valuation;

      let x be Element of K, y be Element of R such that

       A2: x = y;

      

       A3: 0 <= (v . y) by A1, A2, Th52;

      (v . ( - x)) = (v . x) by A1, Th20;

      then

      reconsider x1 = ( - x) as Element of R by A1, A2, A3, Th52;

      (x + ( - x)) = ( 0. K) by RLVECT_1:def 10;

      

      then (y + x1) = ( 0. K) by A2, A1, Th54

      .= ( 0. ( ValuatRing v)) by A1, Def12;

      hence thesis by RLVECT_1:def 10;

    end;

    

     Lm7: a <> ( 0. K) implies ((a " ) * (a * b)) = b

    proof

      assume

       A1: a <> ( 0. K);

      

      thus ((a " ) * (a * b)) = (((a " ) * a) * b) by GROUP_1:def 3

      .= (( 1. K) * b) by A1, VECTSP_2:def 2

      .= b;

    end;

    

     Lm8: for x,v be Element of K st x <> ( 0. K) holds (x * ((x " ) * v)) = v

    proof

      let x,v be Element of K such that

       A1: x <> ( 0. K);

      

      thus (x * ((x " ) * v)) = ((x * (x " )) * v) by GROUP_1:def 3

      .= (( 1. K) * v) by A1, VECTSP_2:def 2

      .= v;

    end;

    theorem :: FVALUAT1:59

    K is having_valuation implies ( ValuatRing v) is domRing-like

    proof

      set R = ( ValuatRing v);

      assume

       A1: K is having_valuation;

      let x,y be Element of R;

      assume that

       A2: (x * y) = ( 0. R) and

       A3: x <> ( 0. R);

      reconsider x1 = x, y1 = y as Element of K by A1, Th51;

      

       A4: ( 0. R) = ( 0. K) by A1, Def12;

      

       A5: (x1 * y1) = (x * y) by A1, Th55;

      y1 = ((x1 " ) * (x1 * y1)) by A3, A4, Lm7

      .= ( 0. K) by A2, A4, A5;

      hence thesis by A1, Def12;

    end;

    theorem :: FVALUAT1:60

    

     Th60: K is having_valuation implies for y be Element of ( ValuatRing v) holds (( power K) . (y,n)) = (( power ( ValuatRing v)) . (y,n))

    proof

      set R = ( ValuatRing v);

      assume

       A1: K is having_valuation;

      let y be Element of R;

      defpred P[ Nat] means (( power K) . (y,$1)) = (( power ( ValuatRing v)) . (y,$1));

      reconsider x = y as Element of K by A1, Th51;

      (( power K) . (x, 0 )) = ( 1_ K) & (( power R) . (y, 0 )) = ( 1_ R) by GROUP_1:def 7;

      then

       A2: P[ 0 ] by A1, Def12;

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A4: P[n];

        reconsider m = n as Element of NAT by ORDINAL1:def 12;

        (( power K) . (y,(n + 1))) = ((( power K) . (x,m)) * x) & (( power ( ValuatRing v)) . (y,(n + 1))) = ((( power ( ValuatRing v)) . (y,m)) * y) by GROUP_1:def 7;

        hence P[(n + 1)] by A1, A4, Th55;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

     Lm9:

    now

      let K, v;

      assume K is having_valuation;

      then (v . ( 0. K)) = +infty by Def8;

      hence ( 0. K) in { x where x be Element of K : 0 < (v . x) };

    end;

    definition

      let K, v;

      assume

       A1: K is having_valuation;

      :: FVALUAT1:def13

      func PosElements v -> Ideal of ( ValuatRing v) equals

      : Def13: { x where x be Element of K : 0 < (v . x) };

      coherence

      proof

        set R = ( ValuatRing v);

        set I = { x where x be Element of K : 0 < (v . x) };

        

         A2: the carrier of R = ( NonNegElements v) by A1, Def12;

        I c= the carrier of R

        proof

          let a be object;

          assume a in I;

          then ex x be Element of K st a = x & 0 < (v . x);

          hence thesis by A2;

        end;

        then

        reconsider I as non empty Subset of R by A1, Lm9;

        

         A3: the carrier of R c= the carrier of K by A2, Th48;

        I is add-closed left-ideal right-ideal

        proof

          hereby

            let x,y be Element of R;

            assume x in I;

            then

            consider x1 be Element of K such that

             A4: x1 = x and

             A5: 0 < (v . x1);

            assume y in I;

            then

            consider y1 be Element of K such that

             A6: y1 = y and

             A7: 0 < (v . y1);

            

             A8: (x + y) = (x1 + y1) by A1, A4, A6, Th54;

            

             A9: ( min ((v . x1),(v . y1))) <= (v . (x1 + y1)) by A1, Th27;

             0 < ( min ((v . x1),(v . y1))) by A5, A7, XXREAL_0: 21;

            hence (x + y) in I by A8, A9;

          end;

          hereby

            let p,x be Element of R;

            assume x in I;

            then

            consider x1 be Element of K such that

             A10: x1 = x and

             A11: 0 < (v . x1);

            reconsider p1 = p as Element of K by A3;

            

             A12: (p * x) = (p1 * x1) by A1, A10, Th55;

            

             A13: (v . (p1 * x1)) = ((v . p1) + (v . x1)) by A1, Def8;

             0 <= (v . p1) by A2, Th47;

            hence (p * x) in I by A11, A12, A13;

          end;

          let p,x be Element of R;

          assume x in I;

          then

          consider x1 be Element of K such that

           A14: x1 = x and

           A15: 0 < (v . x1);

          reconsider p1 = p as Element of K by A3;

          

           A16: (p * x) = (p1 * x1) by A1, A14, Th55;

          

           A17: (v . (p1 * x1)) = ((v . p1) + (v . x1)) by A1, Def8;

           0 <= (v . p1) by A2, Th47;

          hence (x * p) in I by A15, A16, A17;

        end;

        hence thesis;

      end;

    end

    notation

      let K, v;

      synonym vp v for PosElements v;

    end

    theorem :: FVALUAT1:61

    

     Th61: K is having_valuation implies (a in ( vp v) iff 0 < (v . a))

    proof

      assume K is having_valuation;

      then

       A1: ( vp v) = { x where x be Element of K : 0 < (v . x) } by Def13;

      hereby

        assume a in ( vp v);

        then ex b be Element of K st b = a & 0 < (v . b) by A1;

        hence 0 < (v . a);

      end;

      thus thesis by A1;

    end;

    theorem :: FVALUAT1:62

    K is having_valuation implies ( 0. K) in ( vp v)

    proof

      assume

       A1: K is having_valuation;

      then ( vp v) = { x where x be Element of K : 0 < (v . x) } by Def13;

      hence thesis by A1, Lm9;

    end;

    theorem :: FVALUAT1:63

    

     Th63: K is having_valuation implies not ( 1. K) in ( vp v)

    proof

      assume

       A1: K is having_valuation;

      then

       A2: ( vp v) = { x where x be Element of K : 0 < (v . x) } by Def13;

      assume ( 1. K) in ( vp v);

      then ex x be Element of K st x = ( 1. K) & 0 < (v . x) by A2;

      hence thesis by A1, Th17;

    end;

    definition

      let K, v;

      let S be non empty Subset of K;

      assume that

       A1: K is having_valuation and

       A2: S is Subset of ( ValuatRing v);

      :: FVALUAT1:def14

      func min (S,v) -> Subset of ( ValuatRing v) equals

      : Def14: ((v " {( inf (v .: S))}) /\ S);

      coherence

      proof

        ((v " {( inf (v .: S))}) /\ S) c= ( NonNegElements v)

        proof

          let a be object;

          assume

           A3: a in ((v " {( inf (v .: S))}) /\ S);

          then

           A4: a in (v " {( inf (v .: S))}) by XBOOLE_0:def 4;

          reconsider a as Element of K by A3;

          reconsider vS = (v .: S) as non empty Subset of ExtREAL ;

          (v . a) in {( inf (v .: S))} by A4, FUNCT_2: 38;

          then

           A5: (v . a) = ( inf vS) by TARSKI:def 1;

           0 is LowerBound of vS by A1, A2, Th53;

          then 0 <= ( inf vS) by XXREAL_2:def 4;

          hence thesis by A5;

        end;

        hence thesis by A1, Def12;

      end;

    end

    theorem :: FVALUAT1:64

    

     Th64: for S be non empty Subset of K st K is having_valuation & S is Subset of ( ValuatRing v) holds ( min (S,v)) c= S

    proof

      let S be non empty Subset of K;

      assume K is having_valuation & S is Subset of ( ValuatRing v);

      then ( min (S,v)) = ((v " {( inf (v .: S))}) /\ S) by Def14;

      hence ( min (S,v)) c= S by XBOOLE_1: 17;

    end;

    theorem :: FVALUAT1:65

    

     Th65: for S be non empty Subset of K st K is having_valuation & S is Subset of ( ValuatRing v) holds for x be Element of K holds x in ( min (S,v)) iff x in S & for y be Element of K st y in S holds (v . x) <= (v . y)

    proof

      let S be non empty Subset of K;

      assume

       A1: K is having_valuation;

      assume

       A2: S is Subset of ( ValuatRing v);

      

       A3: ( min (S,v)) = ((v " {( inf (v .: S))}) /\ S) by A1, A2, Def14;

      

       A4: ( inf (v .: S)) is LowerBound of (v .: S) by XXREAL_2:def 4;

      let x be Element of K;

      hereby

        assume

         A5: x in ( min (S,v));

        then x in (v " {( inf (v .: S))}) by A3, XBOOLE_0:def 4;

        then (v . x) in {( inf (v .: S))} by FUNCT_2: 38;

        then

         A6: (v . x) = ( inf (v .: S)) by TARSKI:def 1;

        ( min (S,v)) c= S by A1, A2, Th64;

        hence x in S by A5;

        let y be Element of K;

        assume y in S;

        hence (v . x) <= (v . y) by A6, A4, FUNCT_2: 35, XXREAL_2:def 2;

      end;

      assume that

       A7: x in S and

       A8: for y be Element of K st y in S holds (v . x) <= (v . y);

      

       A9: (v . x) is LowerBound of (v .: S)

      proof

        let a be ExtReal;

        assume a in (v .: S);

        then ex y be Element of K st y in S & a = (v . y) by FUNCT_2: 65;

        hence (v . x) <= a by A8;

      end;

      for y be LowerBound of (v .: S) holds y <= (v . x) by A7, FUNCT_2: 35, XXREAL_2:def 2;

      then (v . x) = ( inf (v .: S)) by A9, XXREAL_2:def 4;

      then (v . x) in {( inf (v .: S))} by TARSKI:def 1;

      then x in (v " {( inf (v .: S))}) by FUNCT_2: 38;

      hence x in ( min (S,v)) by A7, A3;

    end;

    theorem :: FVALUAT1:66

    K is having_valuation implies for I be non empty Subset of K, x be Element of ( ValuatRing v) st I is Ideal of ( ValuatRing v) & x in ( min (I,v)) holds I = ( {x} -Ideal )

    proof

      assume

       A1: K is having_valuation;

      let I be non empty Subset of K;

      let x be Element of ( ValuatRing v);

      assume

       A2: I is Ideal of ( ValuatRing v);

      assume

       A3: x in ( min (I,v));

      

       A4: ( min (I,v)) c= I by A1, A2, Th64;

      thus I c= ( {x} -Ideal )

      proof

        let a be object;

        assume

         A5: a in I;

        then

        reconsider y = a as Element of ( ValuatRing v) by A2;

        reconsider x1 = x, y1 = y as Element of K by A1, Th51;

        per cases by A1, Def12;

          suppose

           A6: x <> ( 0. K);

          set r1 = (y1 / x1);

          (v . x1) <= (v . y1) by A1, A2, A3, A5, Th65;

          then 0 <= ((v . y1) - (v . x1)) by Lm4;

          then 0 <= (v . r1) by A6, A1, Th22;

          then

          reconsider r0 = r1 as Element of ( ValuatRing v) by A1, Th52;

          (x1 * r1) = (y1 * ((x1 " ) * x1)) by GROUP_1:def 3

          .= (y1 * ( 1_ K)) by A6, VECTSP_2: 9

          .= y1;

          then

           A7: y = (x * r0) by A1, Th55;

          ( {x} -Ideal ) = the set of all (x * r) where r be Element of ( ValuatRing v) by IDEAL_1: 64;

          hence a in ( {x} -Ideal ) by A7;

        end;

          suppose

           A8: x = ( 0. ( ValuatRing v));

          then

           A9: ( {x} -Ideal ) = {( 0. ( ValuatRing v))} by IDEAL_1: 47;

          

           A10: ( 0. ( ValuatRing v)) = ( 0. K) by A1, Def12;

          then

           A11: (v . x1) = +infty by A1, A8, Def8;

          (v . x1) <= (v . y1) by A1, A5, A2, A3, Th65;

          then y = ( 0. ( ValuatRing v)) by A1, A10, Th18, A11, XXREAL_0: 4;

          hence a in ( {x} -Ideal ) by A9, TARSKI:def 1;

        end;

      end;

       {x} c= I by A4, A3, ZFMISC_1: 31;

      hence ( {x} -Ideal ) c= I by A2, IDEAL_1:def 14;

    end;

    theorem :: FVALUAT1:67

    for R be non empty doubleLoopStr, I be add-closed non empty Subset of R holds I is Preserv of the addF of R

    proof

      let R be non empty doubleLoopStr, I be add-closed non empty Subset of R;

      I is the addF of R -binopclosed

      proof

        let x be set;

        assume x in [:I, I:];

        then

        consider y,z be object such that

         A1: y in I & z in I and

         A2: x = [y, z] by ZFMISC_1:def 2;

        reconsider y, z as Element of I by A1;

        (the addF of R . x) = (y + z) by A2;

        hence (the addF of R . x) in I by IDEAL_1:def 1;

      end;

      hence thesis;

    end;

     Lm10:

    now

      let R be Ring;

      let P be RightIdeal of R;

      thus ex S be strict Submodule of ( RightModule R) st the carrier of S = P

      proof

        reconsider V1 = P as Subset of ( RightModule R);

        V1 is linearly-closed

        proof

          hereby

            let v,u be Vector of ( RightModule R) such that

             A1: v in V1 & u in V1;

            reconsider v1 = v, u1 = u as Element of R;

            (v1 + u1) = (v + u);

            hence (v + u) in V1 by A1, IDEAL_1:def 1;

          end;

          let a be Scalar of R, v be Vector of ( RightModule R) such that

           A2: v in V1;

          reconsider v1 = v as Element of R;

          (v1 * a) = (v * a);

          hence (v * a) in V1 by A2, IDEAL_1:def 3;

        end;

        hence thesis by RMOD_2: 34;

      end;

    end;

    definition

      let R be Ring;

      let P be RightIdeal of R;

      :: FVALUAT1:def15

      mode Submodule of P -> Submodule of ( RightModule R) means

      : Def15: the carrier of it = P;

      existence

      proof

        ex S be strict Submodule of ( RightModule R) st the carrier of S = P by Lm10;

        hence thesis;

      end;

    end

    registration

      let R be Ring;

      let P be RightIdeal of R;

      cluster strict for Submodule of P;

      existence

      proof

        consider S be strict Submodule of ( RightModule R) such that

         A1: the carrier of S = P by Lm10;

        reconsider T = the RightModStr of S as Submodule of P by A1, Def15;

        take T;

        thus thesis;

      end;

    end

    theorem :: FVALUAT1:68

    for R be Ring, P be Ideal of R, M be Submodule of P holds for a be BinOp of P, z be Element of P holds for m be Function of [:P, the carrier of R:], P st a = (the addF of R | [:P, P:]) & m = (the multF of R | [:P, the carrier of R:]) & z = the ZeroF of R holds the RightModStr of M = RightModStr (# P, a, z, m #)

    proof

      let R be Ring;

      let P be Ideal of R;

      let M be Submodule of P;

      

       A1: the carrier of M = P by Def15;

      set V = ( RightModule R);

      ( 0. M) = ( 0. V) & the addF of M = (the addF of V | [:P, P:]) & the rmult of M = (the rmult of V | [:P, the carrier of R:]) by A1, RMOD_2:def 2;

      hence thesis by Def15;

    end;

    definition

      let R be Ring;

      let M1,M2 be RightMod of R;

      let h be Function of M1, M2;

      :: FVALUAT1:def16

      attr h is scalar-linear means for x be Element of M1, r be Element of R holds (h . (x * r)) = ((h . x) * r);

    end

    registration

      let R be Ring, M1 be RightMod of R, M2 be Submodule of M1;

      cluster ( incl (M2,M1)) -> additive scalar-linear;

      coherence

      proof

        set h = ( incl (M2,M1));

        the carrier of M2 c= the carrier of M1 by RMOD_2:def 2;

        then

         A1: h = ( id the carrier of M2) by YELLOW_9:def 1;

        thus ( incl (M2,M1)) is additive

        proof

          let x,y be Element of M2;

          (h . x) = x & (h . y) = y & (h . (x + y)) = (x + y) by A1, FUNCT_1: 17;

          hence thesis by RMOD_2: 13;

        end;

        let x be Element of M2, r be Element of R;

        (h . x) = x & (h . (x * r)) = (x * r) by A1, FUNCT_1: 17;

        hence thesis by RMOD_2: 14;

      end;

    end

    theorem :: FVALUAT1:69

    K is having_valuation & b is Element of ( ValuatRing v) implies (v . a) <= ((v . a) + (v . b))

    proof

      assume

       A1: K is having_valuation;

      assume b is Element of ( ValuatRing v);

      then 0 <= (v . b) by A1, Th52;

      then ((v . a) + 0 ) <= ((v . a) + (v . b)) by XXREAL_3: 35;

      hence thesis by XXREAL_3: 4;

    end;

    theorem :: FVALUAT1:70

    K is having_valuation & a is Element of ( ValuatRing v) implies (( power K) . (a,n)) is Element of ( ValuatRing v)

    proof

      assume

       A1: K is having_valuation;

      assume a is Element of ( ValuatRing v);

      then

      reconsider y = a as Element of ( ValuatRing v);

      reconsider n as Element of NAT by ORDINAL1:def 12;

      (( power ( ValuatRing v)) . (y,n)) is Element of ( ValuatRing v);

      hence thesis by A1, Th60;

    end;

    theorem :: FVALUAT1:71

    K is having_valuation implies for x be Element of ( ValuatRing v) st x <> ( 0. K) holds (( power K) . (x,n)) <> ( 0. K)

    proof

      assume

       A1: K is having_valuation;

      let x be Element of ( ValuatRing v);

      reconsider y = x as Element of K by A1, Th51;

      (( power K) . (y,n)) = (y |^ n);

      hence thesis by Th16;

    end;

    theorem :: FVALUAT1:72

    

     Th72: K is having_valuation & (v . a) = 0 implies a is Element of ( ValuatRing v) & (a " ) is Element of ( ValuatRing v)

    proof

      assume

       A1: K is having_valuation;

      assume

       A2: (v . a) = 0 ;

      thus a is Element of ( ValuatRing v) by A1, A2, Th52;

      a <> ( 0. K) by A1, A2, Def8;

      then (v . (a " )) = ( - (v . a)) by A1, Th21;

      hence thesis by A1, A2, Th52;

    end;

    theorem :: FVALUAT1:73

    K is having_valuation & a <> ( 0. K) & a is Element of ( ValuatRing v) & (a " ) is Element of ( ValuatRing v) implies (v . a) = 0

    proof

      assume

       A1: K is having_valuation;

      assume that

       A2: a <> ( 0. K) and

       A3: a is Element of ( ValuatRing v);

      assume (a " ) is Element of ( ValuatRing v);

      then 0 <= (v . (a " )) by A1, Th52;

      then ( - ( - (v . a))) <= ( - 0 ) by A1, A2, Th21;

      hence thesis by A3, A1, Th52;

    end;

    theorem :: FVALUAT1:74

    

     Th74: K is having_valuation & (v . a) = 0 implies for I be Ideal of ( ValuatRing v) holds a in I iff I = the carrier of ( ValuatRing v)

    proof

      assume

       A1: K is having_valuation;

      assume

       A2: (v . a) = 0 ;

      let I be Ideal of ( ValuatRing v);

      thus a in I implies I = the carrier of ( ValuatRing v)

      proof

        assume

         A3: a in I;

        thus I c= the carrier of ( ValuatRing v);

        let x be object;

        assume x in the carrier of ( ValuatRing v);

        then

        reconsider x as Element of ( ValuatRing v);

        reconsider b = x as Element of K by A1, Th51;

        

         A4: a <> ( 0. K) by A1, A2, Def8;

        reconsider y = a, z = (a " ) as Element of ( ValuatRing v) by A1, A2, Th72;

        

         A5: (y * (z * x)) in I by A3, IDEAL_1:def 2;

        reconsider za = (z * x) as Element of K by A1, Th51;

        (z * x) = ((a " ) * b) by A1, Th55;

        then (y * (z * x)) = (a * ((a " ) * b)) by A1, Th55;

        hence thesis by A5, A4, Lm8;

      end;

      the carrier of ( ValuatRing v) = ( NonNegElements v) by A1, Def12;

      hence thesis by A2;

    end;

    theorem :: FVALUAT1:75

    K is having_valuation implies ( Pgenerator v) is Element of ( ValuatRing v)

    proof

      set a = ( Pgenerator v);

      set l = ( least-positive ( rng v));

      assume

       A1: K is having_valuation;

      then

       A2: a = the Element of (v " {l}) by Def9;

      l in ( rng v) by A1, Lm5;

      then {l} c= ( rng v) by ZFMISC_1: 31;

      then (v " {l}) is non empty by RELAT_1: 139;

      then (v . a) in {l} by A2, FUNCT_1:def 7;

      then (v . a) = l by TARSKI:def 1;

      hence thesis by A1, Th52;

    end;

    theorem :: FVALUAT1:76

    

     Th76: K is having_valuation implies ( vp v) is proper

    proof

      assume

       A1: K is having_valuation;

      then ( 1. K) is Element of ( ValuatRing v) by Def12;

      hence ( vp v) <> the carrier of ( ValuatRing v) by A1, Th63;

    end;

    theorem :: FVALUAT1:77

    

     Th77: K is having_valuation implies for x be Element of ( ValuatRing v) st not x in ( vp v) holds (v . x) = 0

    proof

      assume

       A1: K is having_valuation;

      let x be Element of ( ValuatRing v);

      reconsider y = x as Element of K by A1, Th51;

      assume not x in ( vp v);

      then (v . y) <= 0 by A1, Th61;

      hence thesis by A1, Th52;

    end;

    theorem :: FVALUAT1:78

    K is having_valuation implies ( vp v) is prime

    proof

      assume

       A1: K is having_valuation;

      hence ( vp v) is proper by Th76;

      let a,b be Element of ( ValuatRing v) such that

       A2: (a * b) in ( vp v);

      assume not a in ( vp v);

      then

       A3: (v . a) = 0 by A1, Th77;

      assume

       A4: not b in ( vp v);

      reconsider x = a, y = b as Element of K by A1, Th51;

      

       A5: (a * b) = (x * y) by A1, Th55;

      

       A6: (v . y) = 0 by A1, A4, Th77;

      (v . (x * y)) = ((v . x) + (v . y)) by A1, Def8

      .= 0 by A3, A6;

      hence thesis by A1, A2, A5, Th61;

    end;

    theorem :: FVALUAT1:79

    

     Th79: K is having_valuation implies for I be proper Ideal of ( ValuatRing v) holds I c= ( vp v)

    proof

      assume

       A1: K is having_valuation;

      let I be proper Ideal of ( ValuatRing v);

      

       A2: I <> the carrier of ( ValuatRing v) by SUBSET_1:def 6;

      assume not I c= ( vp v);

      then

      consider x be object such that

       A3: x in I and

       A4: not x in ( vp v);

      

       A5: x is Element of K by A1, A3, Th51;

      (v . x) = 0 by A1, A4, A3, Th77;

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

    end;

    theorem :: FVALUAT1:80

    K is having_valuation implies ( vp v) is maximal

    proof

      assume

       A1: K is having_valuation;

      thus ( vp v) is proper

      proof

        ( 1. ( ValuatRing v)) = ( 1. K) by A1, Def12;

        hence ( vp v) <> the carrier of ( ValuatRing v) by A1, Th63;

      end;

      let J be Ideal of ( ValuatRing v);

      assume

       A2: ( vp v) c= J;

      J is non proper or J = ( vp v) by A1, Th79, A2;

      hence thesis;

    end;

    theorem :: FVALUAT1:81

    K is having_valuation implies for I be maximal Ideal of ( ValuatRing v) holds I = ( vp v)

    proof

      assume

       A1: K is having_valuation;

      let I be maximal Ideal of ( ValuatRing v);

      assume

       A2: not thesis;

      per cases ;

        suppose not I c= ( vp v);

        hence contradiction by A1, Th79;

      end;

        suppose I c= ( vp v);

        then ( vp v) is non proper or I = ( vp v) by RING_1:def 3;

        then

         A3: ( vp v) = the carrier of ( ValuatRing v) or I = ( vp v);

        ( 1. ( ValuatRing v)) = ( 1. K) by A1, Def12;

        hence contradiction by A3, A1, A2, Th63;

      end;

    end;

    theorem :: FVALUAT1:82

    

     Th82: K is having_valuation implies ( NonNegElements ( normal-valuation v)) = ( NonNegElements v)

    proof

      assume

       A1: K is having_valuation;

      set f = ( normal-valuation v);

      thus ( NonNegElements f) c= ( NonNegElements v)

      proof

        let a be object;

        assume a in ( NonNegElements f);

        then

        consider x be Element of K such that

         A2: a = x and

         A3: 0 <= (f . x);

         0 <= (v . x) by A1, A3, Th41;

        hence thesis by A2;

      end;

      let a be object;

      assume a in ( NonNegElements v);

      then

      consider x be Element of K such that

       A4: a = x and

       A5: 0 <= (v . x);

       0 <= (f . x) by A1, A5, Th41;

      hence thesis by A4;

    end;

    theorem :: FVALUAT1:83

    K is having_valuation implies ( ValuatRing ( normal-valuation v)) = ( ValuatRing v)

    proof

      assume

       A1: K is having_valuation;

      set f = ( normal-valuation v);

      set R = ( ValuatRing v);

      set S = ( ValuatRing f);

      

       A2: the carrier of S = ( NonNegElements f) by A1, Def12;

      

       A3: ( NonNegElements f) = ( NonNegElements v) by A1, Th82;

      

       A4: the addF of R = (the addF of K | [:( NonNegElements v), ( NonNegElements v):]) by A1, Def12

      .= the addF of S by A1, A3, Def12;

      

       A5: the multF of R = (the multF of K | [:( NonNegElements v), ( NonNegElements v):]) by A1, Def12

      .= the multF of S by A1, A3, Def12;

      

       A6: the ZeroF of R = ( 0. K) by A1, Def12

      .= the ZeroF of S by A1, Def12;

      the OneF of R = ( 1. K) by A1, Def12

      .= the OneF of S by A1, Def12;

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

    end;