:: Valuation Theory, Part {I}
:: by Grzegorz Bancerek , Hidetsune Kobayashi and Artur Korni{\l}owicz
::
:: Received April 7, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users


theorem Th1: :: FVALUAT1:1
for x being ExtReal st x = - x holds
x = 0
proof end;

theorem Th2: :: FVALUAT1:2
for x being ExtReal st x + x = 0 holds
x = 0
proof end;

theorem Th3: :: FVALUAT1:3
for x, y, z, s being ExtReal st 0 <= x & x <= y & 0 <= s & s <= z holds
x * s <= y * z
proof end;

Lm1: now :: thesis: for a, b being Real
for c, d being ExtReal st a = c & b = d holds
a - b = c - d
let a, b be Real; :: thesis: for c, d being ExtReal st a = c & b = d holds
a - b = c - d

let c, d be ExtReal; :: 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;

theorem :: FVALUAT1:4
for x, y being ExtReal st y <> +infty & 0 < x & 0 < y holds
0 < x / y
proof end;

theorem Th5: :: FVALUAT1:5
for x, y being ExtReal st y <> +infty & x < 0 & 0 < y holds
x / y < 0
proof end;

theorem :: FVALUAT1:6
for x, y being ExtReal st y <> -infty & 0 < x & y < 0 holds
x / y < 0
proof end;

theorem Th7: :: FVALUAT1:7
for x, y, z being ExtReal st ( ( x in REAL & y in REAL ) or z in REAL ) holds
(x + y) / z = (x / z) + (y / z)
proof end;

theorem Th8: :: FVALUAT1:8
for x, y being ExtReal st y <> +infty & y <> -infty & y <> 0 holds
(x / y) * y = x
proof end;

theorem Th9: :: FVALUAT1:9
for x, y being ExtReal st y <> -infty & y <> +infty & x <> 0 & y <> 0 holds
x / y <> 0
proof end;

definition
let x be object ;
attr x 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 object holds
( x is ext-integer iff ( x is integer or x = +infty ) );

registration
cluster ext-integer -> ext-real for object ;
coherence
for b1 being object st b1 is ext-integer holds
b1 is ext-real
;
end;

registration
cluster +infty -> ext-integer ;
coherence
+infty is ext-integer
;
cluster -infty -> non ext-integer ;
coherence
not -infty is ext-integer
;
cluster 1. -> positive real ext-integer ;
coherence
( 1. is ext-integer & 1. is positive & 1. is real )
;
cluster integer -> ext-integer for object ;
coherence
for b1 being object st b1 is integer holds
b1 is ext-integer
;
cluster real ext-integer -> integer for object ;
coherence
for b1 being object st b1 is real & b1 is ext-integer holds
b1 is integer
;
end;

registration
cluster ext-real positive real ext-integer for Element of ExtREAL ;
existence
ex b1 being Element of ExtREAL st
( b1 is real & b1 is ext-integer & b1 is positive )
proof end;
cluster ext-real positive ext-integer for object ;
existence
ex b1 being ext-integer object st b1 is positive
proof end;
end;

definition
mode ExtInt is ext-integer object ;
end;

theorem Th10: :: FVALUAT1:10
for x, y being ExtInt st x < y holds
x + 1 <= y
proof end;

theorem :: FVALUAT1:11
for x being ExtInt holds -infty < x
proof end;

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 ) )
proof end;
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
proof end;
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;
attr f 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
proof end;
end;

registration
let A be set ;
cluster Relation-like A -defined ExtREAL -valued Function-like V40(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
proof end;
end;

registration
let f be e.i.-valued Function;
let x be set ;
cluster f . x -> ext-integer ;
coherence
f . x is ext-integer
proof end;
end;

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
proof end;

definition
let K be non empty doubleLoopStr ;
let S be Subset of K;
let n be Nat;
func S |^ 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) ) ) ) )
proof end;
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 ) )
proof end;
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
proof end;

theorem :: FVALUAT1:14
for D being non empty doubleLoopStr
for A being Subset of D holds A |^ 2 = A *' A
proof 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
( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal )
proof end;
end;

definition
let G be non empty doubleLoopStr ;
let g be Element of G;
let i be Integer;
func g |^ i -> Element of G equals :Def5: :: FVALUAT1:def 5
(power G) . (g,|.i.|) if 0 <= i
otherwise / ((power G) . (g,|.i.|));
correctness
coherence
( ( 0 <= i implies (power G) . (g,|.i.|) is Element of G ) & ( not 0 <= i implies / ((power G) . (g,|.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,|.i.|) ) & ( not 0 <= i implies g |^ i = / ((power G) . (g,|.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) )
proof end;
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);

Lm2: for n being Nat
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a being Element of K holds a |^ (n + 1) = (a |^ n) * a

by GROUP_1:def 7;

theorem :: FVALUAT1:15
for n, m being Nat
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a being Element of K holds a |^ (n + m) = (a |^ n) * (a |^ m)
proof end;

Lm3: for n being Nat
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a being Element of K st a <> 0. K holds
a |^ n <> 0. K

proof end;

theorem Th16: :: FVALUAT1:16
for i being Integer
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a being Element of K st a <> 0. K holds
a |^ i <> 0. K
proof end;

definition
let K be doubleLoopStr ;
attr K is having_valuation means :: 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 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;
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 distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
v . (1. K) = 0
proof end;

theorem Th18: :: FVALUAT1:18
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem Th19: :: FVALUAT1:19
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
v . (- (1. K)) = 0
proof end;

theorem Th20: :: FVALUAT1:20
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem Th21: :: FVALUAT1:21
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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)
proof end;

theorem Th22: :: FVALUAT1:22
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a, b 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)
proof end;

theorem Th23: :: FVALUAT1:23
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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))
proof end;

theorem Th24: :: FVALUAT1:24
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a, b 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
proof end;

theorem Th25: :: FVALUAT1:25
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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)
proof end;

theorem Th26: :: FVALUAT1:26
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a, b 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
proof end;

theorem Th27: :: FVALUAT1:27
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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)
proof end;

theorem Th28: :: FVALUAT1:28
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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)
proof end;

theorem Th29: :: FVALUAT1:29
for i being Integer
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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)
proof end;

theorem Th30: :: FVALUAT1:30
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem :: FVALUAT1:31
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

Lm4: for a, b being ExtInt st a <= b holds
0 <= b - a

proof end;

theorem :: FVALUAT1:32
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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)
proof end;

theorem Th33: :: FVALUAT1:33
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
+infty in rng v
proof end;

Lm5: for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
least-positive (rng v) in rng v

proof end;

theorem Th34: :: FVALUAT1:34
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem Th35: :: FVALUAT1:35
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
least-positive (rng v) is integer
proof end;

Lm6: for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
least-positive (rng v) in REAL

proof end;

theorem Th36: :: FVALUAT1:36
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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))
proof end;

definition
let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;
end;

:: deftheorem Def9 defines Pgenerator FVALUAT1:def 9 :
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 distributive Abelian add-associative right_zeroed associative 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))
proof end;
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
proof end;
end;

:: deftheorem Def10 defines normal-valuation FVALUAT1:def 10 :
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 distributive Abelian add-associative right_zeroed associative 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 )
proof end;

theorem Th38: :: FVALUAT1:38
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 )
proof end;

theorem :: FVALUAT1:39
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 )
proof end;

theorem Th40: :: FVALUAT1:40
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 )
proof end;

theorem Th41: :: FVALUAT1:41
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 )
proof end;

theorem :: FVALUAT1:42
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 )
proof end;

theorem Th43: :: FVALUAT1:43
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
(normal-valuation v) . (Pgenerator v) = 1
proof end;

theorem :: FVALUAT1:44
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem :: FVALUAT1:45
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem :: FVALUAT1:46
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
normal-valuation (normal-valuation v) = normal-valuation v
proof end;

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 )
proof end;

theorem Th48: :: FVALUAT1:48
for K being non empty doubleLoopStr
for v being Valuation of K holds NonNegElements v c= the carrier of K
proof end;

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
proof end;

theorem Th50: :: FVALUAT1:50
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
1. K in NonNegElements v
proof end;

definition
let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ;
let v be Valuation of K;
assume A1: 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 )
proof end;
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 distributive Abelian add-associative right_zeroed associative 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 distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem Th52: :: FVALUAT1:52
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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) )
proof end;

theorem Th53: :: FVALUAT1:53
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem Th54: :: FVALUAT1:54
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem Th55: :: FVALUAT1:55
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem :: FVALUAT1:56
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 distributive Abelian add-associative right_zeroed associative 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 distributive Abelian add-associative right_zeroed associative 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
proof end;

Lm7: for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a, b being Element of K st a <> 0. K holds
(a ") * (a * b) = b

proof end;

Lm8: for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for x, v being Element of K st x <> 0. K holds
x * ((x ") * v) = v

proof end;

theorem :: FVALUAT1:59
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
ValuatRing v is domRing-like
proof end;

theorem Th60: :: FVALUAT1:60
for n being Nat
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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)
proof end;

Lm9: now :: thesis: for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 distributive Abelian add-associative right_zeroed associative 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 distributive Abelian add-associative right_zeroed associative 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)
proof end;
end;

:: deftheorem Def13 defines PosElements FVALUAT1:def 13 :
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 distributive Abelian add-associative right_zeroed associative 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 distributive Abelian add-associative right_zeroed associative 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 )
proof end;

theorem :: FVALUAT1:62
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
0. K in vp v
proof end;

theorem Th63: :: FVALUAT1:63
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
not 1. K in vp v
proof end;

definition
let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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)
proof end;
end;

:: deftheorem Def14 defines min FVALUAT1:def 14 :
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem Th65: :: FVALUAT1:65
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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 ) ) )
proof end;

theorem :: FVALUAT1:66
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

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
proof end;

Lm10: 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 to RMOD_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
proof end;
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 V251() V252() V253() V254() for Submodule of P;
existence
ex b1 being Submodule of P st b1 is strict
proof end;
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 #)
proof end;

definition
let R be Ring;
let M1, M2 be RightMod of R;
let h be Function of M1,M2;
attr h 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 )
proof end;
end;

theorem :: FVALUAT1:69
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a, b 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)
proof end;

theorem :: FVALUAT1:70
for n being Nat
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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)
proof end;

theorem :: FVALUAT1:71
for n being Nat
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem Th72: :: FVALUAT1:72
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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) )
proof end;

theorem :: FVALUAT1:73
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem Th74: :: FVALUAT1:74
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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) )
proof end;

theorem :: FVALUAT1:75
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
Pgenerator v is Element of (ValuatRing v)
proof end;

theorem Th76: :: FVALUAT1:76
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
vp v is proper
proof end;

theorem Th77: :: FVALUAT1:77
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem :: FVALUAT1:78
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
vp v is prime
proof end;

theorem Th79: :: FVALUAT1:79
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem :: FVALUAT1:80
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
vp v is maximal
proof end;

theorem :: FVALUAT1:81
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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
proof end;

theorem Th82: :: FVALUAT1:82
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
NonNegElements (normal-valuation v) = NonNegElements v
proof end;

theorem :: FVALUAT1:83
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
ValuatRing (normal-valuation v) = ValuatRing v
proof end;