:: Valuation Theory, Part {I} :: by Grzegorz Bancerek , Hidetsune Kobayashi and Artur Korni{\l}owicz :: :: Received April 7, 2011 :: Copyright (c) 2011-2012 Association of Mizar Users begin theorem Th1: :: FVALUAT1:1 for x being ext-real number st x = - x holds x = 0 proofend; theorem Th2: :: FVALUAT1:2 for x being ext-real number st x + x = 0 holds x = 0 proofend; theorem Th3: :: FVALUAT1:3 for x, y, s, z being ext-real number st 0 <= x & x <= y & 0 <= s & s <= z holds x * s <= y * z proofend; Lm1: now__::_thesis:_for_a,_b_being_real_number_ for_c,_d_being_ext-real_number_st_a_=_c_&_b_=_d_holds_ a_-_b_=_c_-_d let a, b be real number ; ::_thesis: for c, d being ext-real number st a = c & b = d holds a - b = c - d let c, d be ext-real number ; ::_thesis: ( a = c & b = d implies a - b = c - d ) assume A1: ( a = c & b = d ) ; ::_thesis: a - b = c - d then - b = - d by XXREAL_3:def_3; hence a - b = c - d by A1, XXREAL_3:def_2; ::_thesis: verum end; Lm2: now__::_thesis:_for_a,_b_being_real_number_ for_c,_d_being_ext-real_number_st_a_=_c_&_b_=_d_holds_ a_/_b_=_c_/_d let a, b be real number ; ::_thesis: for c, d being ext-real number st a = c & b = d holds a / b = c / d let c, d be ext-real number ; ::_thesis: ( a = c & b = d implies a / b = c / d ) assume A1: ( a = c & b = d ) ; ::_thesis: a / b = c / d then b " = d " by XXREAL_3:def_6; hence a / b = c / d by A1, XXREAL_3:def_5; ::_thesis: verum end; theorem :: FVALUAT1:4 for y, x being ext-real number st y <> +infty & 0 < x & 0 < y holds 0 < x / y proofend; theorem Th5: :: FVALUAT1:5 for y, x being ext-real number st y <> +infty & x < 0 & 0 < y holds x / y < 0 proofend; theorem :: FVALUAT1:6 for y, x being ext-real number st y <> -infty & 0 < x & y < 0 holds x / y < 0 proofend; theorem Th7: :: FVALUAT1:7 for x, y, z being ext-real number st ( ( x in REAL & y in REAL ) or z in REAL ) holds (x + y) / z = (x / z) + (y / z) proofend; theorem Th8: :: FVALUAT1:8 for y, x being ext-real number st y <> +infty & y <> -infty & y <> 0 holds (x / y) * y = x proofend; theorem Th9: :: FVALUAT1:9 for y, x being ext-real number st y <> -infty & y <> +infty & x <> 0 & y <> 0 holds x / y <> 0 proofend; definition let x be number ; attrx is ext-integer means :Def1: :: FVALUAT1:def 1 ( x is integer or x = +infty ); end; :: deftheorem Def1 defines ext-integer FVALUAT1:def_1_:_ for x being number holds ( x is ext-integer iff ( x is integer or x = +infty ) ); registration cluster ext-integer -> ext-real for set ; coherence for b1 being number st b1 is ext-integer holds b1 is ext-real proofend; end; registration cluster +infty -> ext-integer ; coherence +infty is ext-integer by Def1; cluster -infty -> non ext-integer ; coherence not -infty is ext-integer proofend; cluster 1. -> real positive ext-integer ; coherence ( 1. is ext-integer & 1. is positive & 1. is real ) by Def1; cluster integer -> ext-integer for set ; coherence for b1 being number st b1 is integer holds b1 is ext-integer by Def1; cluster real ext-integer -> integer for set ; coherence for b1 being number st b1 is real & b1 is ext-integer holds b1 is integer proofend; end; registration cluster real ext-real positive ext-integer for Element of ExtREAL ; existence ex b1 being Element of ExtREAL st ( b1 is real & b1 is ext-integer & b1 is positive ) proofend; cluster ext-real positive ext-integer for set ; existence ex b1 being ext-integer number st b1 is positive proofend; end; definition mode ExtInt is ext-integer number ; end; theorem Th10: :: FVALUAT1:10 for x, y being ExtInt st x < y holds x + 1 <= y proofend; theorem :: FVALUAT1:11 for x being ExtInt holds -infty < x proofend; definition let X be ext-real-membered set ; given i0 being positive ExtInt such that A1: i0 in X ; func least-positive X -> positive ExtInt means :Def2: :: FVALUAT1:def 2 ( it in X & ( for i being positive ExtInt st i in X holds it <= i ) ); existence ex b1 being positive ExtInt st ( b1 in X & ( for i being positive ExtInt st i in X holds b1 <= i ) ) proofend; uniqueness for b1, b2 being positive ExtInt st b1 in X & ( for i being positive ExtInt st i in X holds b1 <= i ) & b2 in X & ( for i being positive ExtInt st i in X holds b2 <= i ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines least-positive FVALUAT1:def_2_:_ for X being ext-real-membered set st ex i0 being positive ExtInt st i0 in X holds for b2 being positive ExtInt holds ( b2 = least-positive X iff ( b2 in X & ( for i being positive ExtInt st i in X holds b2 <= i ) ) ); definition let f be Relation; attrf is e.i.-valued means :Def3: :: FVALUAT1:def 3 for x being set st x in rng f holds x is ext-integer ; end; :: deftheorem Def3 defines e.i.-valued FVALUAT1:def_3_:_ for f being Relation holds ( f is e.i.-valued iff for x being set st x in rng f holds x is ext-integer ); registration cluster Relation-like Function-like e.i.-valued for set ; existence ex b1 being Function st b1 is e.i.-valued proofend; end; registration let A be set ; cluster Relation-like A -defined ExtREAL -valued Function-like V38(A, ExtREAL ) e.i.-valued for Element of bool [:A,ExtREAL:]; existence ex b1 being Function of A,ExtREAL st b1 is e.i.-valued proofend; end; registration let f be e.i.-valued Function; let x be set ; clusterf . x -> ext-integer ; coherence f . x is ext-integer proofend; end; begin theorem Th12: :: FVALUAT1:12 for K being non empty right_complementable distributive left_unital add-associative right_zeroed doubleLoopStr holds (- (1. K)) * (- (1. K)) = 1. K proofend; definition let K be non empty doubleLoopStr ; let S be Subset of K; let n be Nat; funcS |^ n -> Subset of K means :Def4: :: FVALUAT1:def 4 it = the carrier of K if n = 0 otherwise ex f being FinSequence of bool the carrier of K st ( it = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds f . (i + 1) = S *' (f /. i) ) ); consistency for b1 being Subset of K holds verum ; existence ( ( n = 0 implies ex b1 being Subset of K st b1 = the carrier of K ) & ( not n = 0 implies ex b1 being Subset of K ex f being FinSequence of bool the carrier of K st ( b1 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds f . (i + 1) = S *' (f /. i) ) ) ) ) proofend; uniqueness for b1, b2 being Subset of K holds ( ( n = 0 & b1 = the carrier of K & b2 = the carrier of K implies b1 = b2 ) & ( not n = 0 & ex f being FinSequence of bool the carrier of K st ( b1 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds f . (i + 1) = S *' (f /. i) ) ) & ex f being FinSequence of bool the carrier of K st ( b2 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds f . (i + 1) = S *' (f /. i) ) ) implies b1 = b2 ) ) proofend; end; :: deftheorem Def4 defines |^ FVALUAT1:def_4_:_ for K being non empty doubleLoopStr for S being Subset of K for n being Nat for b4 being Subset of K holds ( ( n = 0 implies ( b4 = S |^ n iff b4 = the carrier of K ) ) & ( not n = 0 implies ( b4 = S |^ n iff ex f being FinSequence of bool the carrier of K st ( b4 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds f . (i + 1) = S *' (f /. i) ) ) ) ) ); theorem :: FVALUAT1:13 for D being non empty doubleLoopStr for A being Subset of D holds A |^ 1 = A proofend; theorem :: FVALUAT1:14 for D being non empty doubleLoopStr for A being Subset of D holds A |^ 2 = A *' A proofend; registration let R be Ring; let S be Ideal of R; let n be Nat; clusterS |^ n -> non empty add-closed left-ideal right-ideal ; coherence ( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal ) proofend; end; definition let G be non empty doubleLoopStr ; let g be Element of G; let i be Integer; funcg |^ i -> Element of G equals :Def5: :: FVALUAT1:def 5 (power G) . (g,(abs i)) if 0 <= i otherwise ((power G) . (g,(abs i))) " ; correctness coherence ( ( 0 <= i implies (power G) . (g,(abs i)) is Element of G ) & ( not 0 <= i implies ((power G) . (g,(abs i))) " is Element of G ) ); consistency for b1 being Element of G holds verum; ; end; :: deftheorem Def5 defines |^ FVALUAT1:def_5_:_ for G being non empty doubleLoopStr for g being Element of G for i being Integer holds ( ( 0 <= i implies g |^ i = (power G) . (g,(abs i)) ) & ( not 0 <= i implies g |^ i = ((power G) . (g,(abs i))) " ) ); definition let G be non empty doubleLoopStr ; let g be Element of G; let n be Nat; redefine func g |^ n equals :: FVALUAT1:def 6 (power G) . (g,n); compatibility for b1 being Element of G holds ( b1 = g |^ n iff b1 = (power G) . (g,n) ) proofend; end; :: deftheorem defines |^ FVALUAT1:def_6_:_ for G being non empty doubleLoopStr for g being Element of G for n being Nat holds g |^ n = (power G) . (g,n); Lm3: for n being Nat for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K holds a |^ (n + 1) = (a |^ n) * a proofend; theorem :: FVALUAT1:15 for n, m being Nat for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K holds a |^ (n + m) = (a |^ n) * (a |^ m) proofend; Lm4: for n being Nat for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K st a <> 0. K holds a |^ n <> 0. K proofend; theorem Th16: :: FVALUAT1:16 for i being Integer for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K st a <> 0. K holds a |^ i <> 0. K proofend; begin definition let K be doubleLoopStr ; attrK is having_valuation means :Def7: :: FVALUAT1:def 7 ex f being e.i.-valued Function of K,ExtREAL st ( f . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds f . a in INT ) & ( for a, b being Element of K holds f . (a * b) = (f . a) + (f . b) ) & ( for a being Element of K st 0 <= f . a holds 0 <= f . ((1. K) + a) ) & ex a being Element of K st ( f . a <> 0 & f . a <> +infty ) ); end; :: deftheorem Def7 defines having_valuation FVALUAT1:def_7_:_ for K being doubleLoopStr holds ( K is having_valuation iff ex f being e.i.-valued Function of K,ExtREAL st ( f . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds f . a in INT ) & ( for a, b being Element of K holds f . (a * b) = (f . a) + (f . b) ) & ( for a being Element of K st 0 <= f . a holds 0 <= f . ((1. K) + a) ) & ex a being Element of K st ( f . a <> 0 & f . a <> +infty ) ) ); definition let K be doubleLoopStr ; assume A1: K is having_valuation ; mode Valuation of K -> e.i.-valued Function of K,ExtREAL means :Def8: :: FVALUAT1:def 8 ( it . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds it . a in INT ) & ( for a, b being Element of K holds it . (a * b) = (it . a) + (it . b) ) & ( for a being Element of K st 0 <= it . a holds 0 <= it . ((1. K) + a) ) & ex a being Element of K st ( it . a <> 0 & it . a <> +infty ) ); existence ex b1 being e.i.-valued Function of K,ExtREAL st ( b1 . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds b1 . a in INT ) & ( for a, b being Element of K holds b1 . (a * b) = (b1 . a) + (b1 . b) ) & ( for a being Element of K st 0 <= b1 . a holds 0 <= b1 . ((1. K) + a) ) & ex a being Element of K st ( b1 . a <> 0 & b1 . a <> +infty ) ) by A1, Def7; end; :: deftheorem Def8 defines Valuation FVALUAT1:def_8_:_ for K being doubleLoopStr st K is having_valuation holds for b2 being e.i.-valued Function of K,ExtREAL holds ( b2 is Valuation of K iff ( b2 . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds b2 . a in INT ) & ( for a, b being Element of K holds b2 . (a * b) = (b2 . a) + (b2 . b) ) & ( for a being Element of K st 0 <= b2 . a holds 0 <= b2 . ((1. K) + a) ) & ex a being Element of K st ( b2 . a <> 0 & b2 . a <> +infty ) ) ); theorem Th17: :: FVALUAT1:17 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds v . (1. K) = 0 proofend; theorem Th18: :: FVALUAT1:18 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & a <> 0. K holds v . a <> +infty proofend; theorem Th19: :: FVALUAT1:19 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds v . (- (1. K)) = 0 proofend; theorem Th20: :: FVALUAT1:20 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation holds v . (- a) = v . a proofend; theorem Th21: :: FVALUAT1:21 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & a <> 0. K holds v . (a ") = - (v . a) proofend; theorem Th22: :: FVALUAT1:22 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for b, a being Element of K for v being Valuation of K st K is having_valuation & b <> 0. K holds v . (a / b) = (v . a) - (v . b) proofend; theorem Th23: :: FVALUAT1:23 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a, b being Element of K for v being Valuation of K st K is having_valuation & a <> 0. K & b <> 0. K holds v . (a / b) = - (v . (b / a)) proofend; theorem Th24: :: FVALUAT1:24 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for b, a being Element of K for v being Valuation of K st K is having_valuation & b <> 0. K & 0 <= v . (a / b) holds v . b <= v . a proofend; theorem Th25: :: FVALUAT1:25 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a, b being Element of K for v being Valuation of K st K is having_valuation & a <> 0. K & b <> 0. K & v . (a / b) <= 0 holds 0 <= v . (b / a) proofend; theorem Th26: :: FVALUAT1:26 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for b, a being Element of K for v being Valuation of K st K is having_valuation & b <> 0. K & v . (a / b) <= 0 holds v . a <= v . b proofend; theorem Th27: :: FVALUAT1:27 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a, b being Element of K for v being Valuation of K st K is having_valuation holds min ((v . a),(v . b)) <= v . (a + b) proofend; theorem Th28: :: FVALUAT1:28 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a, b being Element of K for v being Valuation of K st K is having_valuation & v . a < v . b holds v . a = v . (a + b) proofend; theorem Th29: :: FVALUAT1:29 for i being Integer for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & a <> 0. K holds v . (a |^ i) = i * (v . a) proofend; theorem Th30: :: FVALUAT1:30 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & 0 <= v . ((1. K) + a) holds 0 <= v . a proofend; theorem :: FVALUAT1:31 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & 0 <= v . ((1. K) - a) holds 0 <= v . a proofend; Lm5: for a, b being ExtInt st a <= b holds 0 <= b - a proofend; theorem :: FVALUAT1:32 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a, b being Element of K for v being Valuation of K st K is having_valuation & a <> 0. K & v . a <= v . b holds 0 <= v . (b / a) proofend; theorem Th33: :: FVALUAT1:33 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds +infty in rng v proofend; Lm6: for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds least-positive (rng v) in rng v proofend; theorem Th34: :: FVALUAT1:34 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st v . a = 1 holds least-positive (rng v) = 1 proofend; theorem Th35: :: FVALUAT1:35 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds least-positive (rng v) is integer proofend; Lm7: for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds least-positive (rng v) in REAL proofend; theorem Th36: :: FVALUAT1:36 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for x being Element of K st x <> 0. K holds ex i being Integer st v . x = i * (least-positive (rng v)) proofend; definition let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; let v be Valuation of K; assume A1: K is having_valuation ; func Pgenerator v -> Element of K equals :Def9: :: FVALUAT1:def 9 the Element of v " {(least-positive (rng v))}; coherence the Element of v " {(least-positive (rng v))} is Element of K proofend; end; :: deftheorem Def9 defines Pgenerator FVALUAT1:def_9_:_ for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds Pgenerator v = the Element of v " {(least-positive (rng v))}; definition let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; let v be Valuation of K; assume A1: K is having_valuation ; func normal-valuation v -> Valuation of K means :Def10: :: FVALUAT1:def 10 for a being Element of K holds v . a = (it . a) * (least-positive (rng v)); existence ex b1 being Valuation of K st for a being Element of K holds v . a = (b1 . a) * (least-positive (rng v)) proofend; uniqueness for b1, b2 being Valuation of K st ( for a being Element of K holds v . a = (b1 . a) * (least-positive (rng v)) ) & ( for a being Element of K holds v . a = (b2 . a) * (least-positive (rng v)) ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines normal-valuation FVALUAT1:def_10_:_ for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for b3 being Valuation of K holds ( b3 = normal-valuation v iff for a being Element of K holds v . a = (b3 . a) * (least-positive (rng v)) ); theorem Th37: :: FVALUAT1:37 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation holds ( v . a = 0 iff (normal-valuation v) . a = 0 ) proofend; theorem Th38: :: FVALUAT1:38 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation holds ( v . a = +infty iff (normal-valuation v) . a = +infty ) proofend; theorem :: FVALUAT1:39 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a, b being Element of K for v being Valuation of K st K is having_valuation holds ( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b ) proofend; theorem Th40: :: FVALUAT1:40 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation holds ( v . a is positive iff (normal-valuation v) . a is positive ) proofend; theorem Th41: :: FVALUAT1:41 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation holds ( 0 <= v . a iff 0 <= (normal-valuation v) . a ) proofend; theorem :: FVALUAT1:42 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation holds ( not v . a is negative iff not (normal-valuation v) . a is negative ) proofend; theorem Th43: :: FVALUAT1:43 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds (normal-valuation v) . (Pgenerator v) = 1 proofend; theorem :: FVALUAT1:44 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & 0 <= v . a holds (normal-valuation v) . a <= v . a proofend; theorem :: FVALUAT1:45 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & v . a = 1 holds normal-valuation v = v proofend; theorem :: FVALUAT1:46 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds normal-valuation (normal-valuation v) = normal-valuation v proofend; begin definition let K be non empty doubleLoopStr ; let v be Valuation of K; func NonNegElements v -> set equals :: FVALUAT1:def 11 { x where x is Element of K : 0 <= v . x } ; coherence { x where x is Element of K : 0 <= v . x } is set ; end; :: deftheorem defines NonNegElements FVALUAT1:def_11_:_ for K being non empty doubleLoopStr for v being Valuation of K holds NonNegElements v = { x where x is Element of K : 0 <= v . x } ; theorem Th47: :: FVALUAT1:47 for K being non empty doubleLoopStr for v being Valuation of K for a being Element of K holds ( a in NonNegElements v iff 0 <= v . a ) proofend; theorem Th48: :: FVALUAT1:48 for K being non empty doubleLoopStr for v being Valuation of K holds NonNegElements v c= the carrier of K proofend; theorem Th49: :: FVALUAT1:49 for K being non empty doubleLoopStr for v being Valuation of K st K is having_valuation holds 0. K in NonNegElements v proofend; theorem Th50: :: FVALUAT1:50 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds 1. K in NonNegElements v proofend; definition let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; let v be Valuation of K; assume B1: K is having_valuation ; func ValuatRing v -> non degenerated strict commutative Ring means :Def12: :: FVALUAT1:def 12 ( 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 ex b1 being non degenerated strict commutative Ring st ( the carrier of b1 = NonNegElements v & the addF of b1 = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b1 = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b1 = 0. K & the OneF of b1 = 1. K ) proofend; uniqueness for b1, b2 being non degenerated strict commutative Ring st the carrier of b1 = NonNegElements v & the addF of b1 = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b1 = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b1 = 0. K & the OneF of b1 = 1. K & the carrier of b2 = NonNegElements v & the addF of b2 = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b2 = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b2 = 0. K & the OneF of b2 = 1. K holds b1 = b2 ; end; :: deftheorem Def12 defines ValuatRing FVALUAT1:def_12_:_ for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for b3 being non degenerated strict commutative Ring holds ( b3 = ValuatRing v iff ( the carrier of b3 = NonNegElements v & the addF of b3 = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b3 = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b3 = 0. K & the OneF of b3 = 1. K ) ); theorem Th51: :: FVALUAT1:51 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for x being Element of (ValuatRing v) holds x is Element of K proofend; theorem Th52: :: FVALUAT1:52 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation holds ( 0 <= v . a iff a is Element of (ValuatRing v) ) proofend; theorem Th53: :: FVALUAT1:53 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for S being Subset of (ValuatRing v) holds 0 is LowerBound of v .: S proofend; theorem Th54: :: FVALUAT1:54 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for x, y being Element of K for x1, y1 being Element of (ValuatRing v) st x = x1 & y = y1 holds x + y = x1 + y1 proofend; theorem Th55: :: FVALUAT1:55 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for x, y being Element of K for x1, y1 being Element of (ValuatRing v) st x = x1 & y = y1 holds x * y = x1 * y1 proofend; theorem :: FVALUAT1:56 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds 0. (ValuatRing v) = 0. K by Def12; theorem :: FVALUAT1:57 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds 1. (ValuatRing v) = 1. K by Def12; theorem :: FVALUAT1:58 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for x being Element of K for y being Element of (ValuatRing v) st x = y holds - x = - y proofend; Lm8: for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a, b being Element of K st a <> 0. K holds (a ") * (a * b) = b proofend; Lm9: for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for x, v being Element of K st x <> 0. K holds x * ((x ") * v) = v proofend; theorem :: FVALUAT1:59 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds ValuatRing v is domRing-like proofend; theorem Th60: :: FVALUAT1:60 for n being Nat for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n) proofend; Lm10: now__::_thesis:_for_K_being_non_empty_non_degenerated_right_complementable_associative_distributive_Abelian_add-associative_right_zeroed_Field-like_doubleLoopStr_ for_v_being_Valuation_of_K_st_K_is_having_valuation_holds_ 0._K_in__{__x_where_x_is_Element_of_K_:_0_<_v_._x__}_ let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: for v being Valuation of K st K is having_valuation holds 0. K in { x where x is Element of K : 0 < v . x } let v be Valuation of K; ::_thesis: ( K is having_valuation implies 0. K in { x where x is Element of K : 0 < v . x } ) assume K is having_valuation ; ::_thesis: 0. K in { x where x is Element of K : 0 < v . x } then v . (0. K) = +infty by Def8; hence 0. K in { x where x is Element of K : 0 < v . x } ; ::_thesis: verum end; definition let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; let v be Valuation of K; assume A1: K is having_valuation ; func PosElements v -> Ideal of (ValuatRing v) equals :Def13: :: FVALUAT1:def 13 { x where x is Element of K : 0 < v . x } ; coherence { x where x is Element of K : 0 < v . x } is Ideal of (ValuatRing v) proofend; end; :: deftheorem Def13 defines PosElements FVALUAT1:def_13_:_ for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds PosElements v = { x where x is Element of K : 0 < v . x } ; notation let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; let v be Valuation of K; synonym vp v for PosElements v; end; theorem Th61: :: FVALUAT1:61 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation holds ( a in vp v iff 0 < v . a ) proofend; theorem :: FVALUAT1:62 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds 0. K in vp v proofend; theorem Th63: :: FVALUAT1:63 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds not 1. K in vp v proofend; definition let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; let v be Valuation of K; let S be non empty Subset of K; assume that A1: K is having_valuation and A2: S is Subset of (ValuatRing v) ; func min (S,v) -> Subset of (ValuatRing v) equals :Def14: :: FVALUAT1:def 14 (v " {(inf (v .: S))}) /\ S; coherence (v " {(inf (v .: S))}) /\ S is Subset of (ValuatRing v) proofend; end; :: deftheorem Def14 defines min FVALUAT1:def_14_:_ for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K for S being non empty Subset of K st K is having_valuation & S is Subset of (ValuatRing v) holds min (S,v) = (v " {(inf (v .: S))}) /\ S; theorem Th64: :: FVALUAT1:64 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K for S being non empty Subset of K st K is having_valuation & S is Subset of (ValuatRing v) holds min (S,v) c= S proofend; theorem Th65: :: FVALUAT1:65 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K for S being non empty Subset of K st K is having_valuation & S is Subset of (ValuatRing v) holds for x being Element of K holds ( x in min (S,v) iff ( x in S & ( for y being Element of K st y in S holds v . x <= v . y ) ) ) proofend; theorem :: FVALUAT1:66 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for I being non empty Subset of K for x being Element of (ValuatRing v) st I is Ideal of (ValuatRing v) & x in min (I,v) holds I = {x} -Ideal proofend; theorem :: FVALUAT1:67 for R being non empty doubleLoopStr for I being non empty add-closed Subset of R holds I is Preserv of the addF of R proofend; Lm11: now__::_thesis:_for_R_being_Ring for_P_being_RightIdeal_of_R_ex_S_being_strict_Submodule_of_RightModule_R_st_the_carrier_of_S_=_P let R be Ring; ::_thesis: for P being RightIdeal of R ex S being strict Submodule of RightModule R st the carrier of S = P let P be RightIdeal of R; ::_thesis: ex S being strict Submodule of RightModule R st the carrier of S = P thus ex S being strict Submodule of RightModule R st the carrier of S = P ::_thesis: verum proof reconsider V1 = P as Subset of (RightModule R) ; V1 is linearly-closed proof hereby :: according toRMOD_2:def_1 ::_thesis: for b1 being Element of the carrier of R for b2 being Element of the carrier of (RightModule R) holds ( not b2 in V1 or b2 * b1 in V1 ) let v, u be Vector of (RightModule R); ::_thesis: ( v in V1 & u in V1 implies v + u in V1 ) assume A1: ( v in V1 & u in V1 ) ; ::_thesis: v + 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; ::_thesis: verum end; let a be Scalar of R; ::_thesis: for b1 being Element of the carrier of (RightModule R) holds ( not b1 in V1 or b1 * a in V1 ) let v be Vector of (RightModule R); ::_thesis: ( not v in V1 or v * a in V1 ) assume A2: v in V1 ; ::_thesis: v * a in V1 reconsider v1 = v as Element of R ; v1 * a = v * a ; hence v * a in V1 by A2, IDEAL_1:def_3; ::_thesis: verum end; hence ex S being strict Submodule of RightModule R st the carrier of S = P by RMOD_2:34; ::_thesis: verum end; end; definition let R be Ring; let P be RightIdeal of R; mode Submodule of P -> Submodule of RightModule R means :Def15: :: FVALUAT1:def 15 the carrier of it = P; existence ex b1 being Submodule of RightModule R st the carrier of b1 = P proofend; end; :: deftheorem Def15 defines Submodule FVALUAT1:def_15_:_ for R being Ring for P being RightIdeal of R for b3 being Submodule of RightModule R holds ( b3 is Submodule of P iff the carrier of b3 = P ); registration let R be Ring; let P be RightIdeal of R; cluster non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed strict RightMod-like V235() V236() V237() V238() for Submodule of P; existence ex b1 being Submodule of P st b1 is strict proofend; end; theorem :: FVALUAT1:68 for R being Ring for P being Ideal of R for M being Submodule of P for a being BinOp of P for z being Element of P for m being 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 RightModStr(# the carrier of M, the addF of M, the ZeroF of M, the rmult of M #) = RightModStr(# P,a,z,m #) proofend; definition let R be Ring; let M1, M2 be RightMod of R; let h be Function of M1,M2; attrh is scalar-linear means :: FVALUAT1:def 16 for x being Element of M1 for r being Element of R holds h . (x * r) = (h . x) * r; end; :: deftheorem defines scalar-linear FVALUAT1:def_16_:_ for R being Ring for M1, M2 being RightMod of R for h being Function of M1,M2 holds ( h is scalar-linear iff for x being Element of M1 for r being Element of R holds h . (x * r) = (h . x) * r ); registration let R be Ring; let M1 be RightMod of R; let M2 be Submodule of M1; cluster incl (M2,M1) -> additive scalar-linear ; coherence ( incl (M2,M1) is additive & incl (M2,M1) is scalar-linear ) proofend; end; theorem :: FVALUAT1:69 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for b, a being Element of K for v being Valuation of K st K is having_valuation & b is Element of (ValuatRing v) holds v . a <= (v . a) + (v . b) proofend; theorem :: FVALUAT1:70 for n being Nat for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & a is Element of (ValuatRing v) holds (power K) . (a,n) is Element of (ValuatRing v) proofend; theorem :: FVALUAT1:71 for n being Nat for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for x being Element of (ValuatRing v) st x <> 0. K holds (power K) . (x,n) <> 0. K proofend; theorem Th72: :: FVALUAT1:72 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & v . a = 0 holds ( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) ) proofend; theorem :: FVALUAT1:73 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & a <> 0. K & a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) holds v . a = 0 proofend; theorem Th74: :: FVALUAT1:74 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for a being Element of K for v being Valuation of K st K is having_valuation & v . a = 0 holds for I being Ideal of (ValuatRing v) holds ( a in I iff I = the carrier of (ValuatRing v) ) proofend; theorem :: FVALUAT1:75 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds Pgenerator v is Element of (ValuatRing v) proofend; theorem Th76: :: FVALUAT1:76 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds vp v is proper proofend; theorem Th77: :: FVALUAT1:77 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for x being Element of (ValuatRing v) st not x in vp v holds v . x = 0 proofend; theorem :: FVALUAT1:78 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds vp v is prime proofend; theorem Th79: :: FVALUAT1:79 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for I being proper Ideal of (ValuatRing v) holds I c= vp v proofend; theorem :: FVALUAT1:80 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds vp v is maximal proofend; theorem :: FVALUAT1:81 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds for I being maximal Ideal of (ValuatRing v) holds I = vp v proofend; theorem Th82: :: FVALUAT1:82 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds NonNegElements (normal-valuation v) = NonNegElements v proofend; theorem :: FVALUAT1:83 for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr for v being Valuation of K st K is having_valuation holds ValuatRing (normal-valuation v) = ValuatRing v proofend;