:: FVALUAT1 semantic presentation

begin


theorem Th1: :: FVALUAT1:1
for x being ext-real number st x = - x holds
x = 0
proof
let x be ext-real number ; ::_thesis: ( x = - x implies x = 0 )
percases ( x = +infty or x = -infty or x in REAL ) by XXREAL_0:14;
suppose ( x = +infty or x = -infty ) ; ::_thesis: ( x = - x implies x = 0 )
hence  ( x = - x implies x = 0 ) ; ::_thesis: verum
end;
suppose x in REAL ; ::_thesis: ( x = - x implies x = 0 )
then reconsider y = x as Element of REAL ;
 - x = - y by XXREAL_3:def_3;
hence  ( x = - x implies x = 0 ) ; ::_thesis: verum
end;
end;
end;

theorem Th2: :: FVALUAT1:2
for x being ext-real number st x + x = 0 holds
x = 0
proof
let x be ext-real number ; ::_thesis: ( x + x = 0 implies x = 0 )
assume  x + x = 0 ; ::_thesis: x = 0
then  x = - x by XXREAL_3:8;
hence  x = 0 by Th1; ::_thesis: verum
end;

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
proof
let x, y, s, z be ext-real number ; ::_thesis: ( 0 <= x & x <= y & 0 <= s & s <= z implies x * s <= y * z )
assume that
A1: 0 <= x and
A2: x <= y and
A3: 0 <= s and
A4: s <= z ; ::_thesis: x * s <= y * z
A5: x * s <= y * s by A2, A3, XXREAL_3:71;
 y * s <= y * z by A1, A2, A4, XXREAL_3:71;
hence  x * s <= y * z by A5, XXREAL_0:2; ::_thesis: verum
end;

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
proof
let y, x be ext-real number ; ::_thesis: ( y <> +infty & 0 < x & 0 < y implies 0 < x / y )
assume that
A1: y <> +infty and
A2: 0 < x and
A3: 0 < y ; ::_thesis: 0 < x / y
percases ( x in REAL or x = +infty or x = -infty ) by XXREAL_0:14;
suppose x in REAL ; ::_thesis: 0 < x / y
then reconsider x1 = x as Real ;
reconsider y1 = y as Real by A1, A3, XXREAL_0:14;
 x / y = x1 / y1 by Lm2;
hence  0 < x / y by A2, A3; ::_thesis: verum
end;
suppose x = +infty ; ::_thesis: 0 < x / y
hence  0 < x / y by A1, A3, XXREAL_3:83; ::_thesis: verum
end;
suppose x = -infty ; ::_thesis: 0 < x / y
hence  0 < x / y by A2; ::_thesis: verum
end;
end;
end;

theorem Th5: :: FVALUAT1:5
for y, x being ext-real number st y <> +infty & x < 0 & 0 < y holds
x / y < 0
proof
let y, x be ext-real number ; ::_thesis: ( y <> +infty & x < 0 & 0 < y implies x / y < 0 )
assume that
A1: y <> +infty and
A2: x < 0 and
A3: 0 < y ; ::_thesis: x / y < 0
reconsider y1 = y as Real by A3, A1, XXREAL_0:14;
percases ( x in REAL or x = +infty or x = -infty ) by XXREAL_0:14;
suppose x in REAL ; ::_thesis: x / y < 0
then reconsider x1 = x as Real ;
 x / y = x1 / y1 by Lm2;
hence  x / y < 0 by A2, A3; ::_thesis: verum
end;
suppose x = +infty ; ::_thesis: x / y < 0
hence  x / y < 0 by A2; ::_thesis: verum
end;
suppose x = -infty ; ::_thesis: x / y < 0
hence  x / y < 0 by A1, A3, XXREAL_3:86; ::_thesis: verum
end;
end;
end;

theorem :: FVALUAT1:6
for y, x being ext-real number st y <> -infty & 0 < x & y < 0 holds
x / y < 0
proof
let y, x be ext-real number ; ::_thesis: ( y <> -infty & 0 < x & y < 0 implies x / y < 0 )
assume that
A1: y <> -infty and
A2: 0 < x and
A3: y < 0 ; ::_thesis: x / y < 0
reconsider y1 = y as Real by A1, A3, XXREAL_0:14;
percases ( x in REAL or x = +infty or x = -infty ) by XXREAL_0:14;
suppose x in REAL ; ::_thesis: x / y < 0
then reconsider x1 = x as Real ;
 x / y = x1 / y1 by Lm2;
hence  x / y < 0 by A2, A3; ::_thesis: verum
end;
suppose x = +infty ; ::_thesis: x / y < 0
hence  x / y < 0 by A1, A3, XXREAL_3:85; ::_thesis: verum
end;
suppose x = -infty ; ::_thesis: x / y < 0
hence  x / y < 0 by A2; ::_thesis: verum
end;
end;
end;

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)
proof
let x, y, z be ext-real number ; ::_thesis: ( ( ( x in REAL & y in REAL ) or z in REAL ) implies (x + y) / z = (x / z) + (y / z) )
assume A1: ( ( x in REAL & y in REAL ) or z in REAL ) ; ::_thesis: (x + y) / z = (x / z) + (y / z)
percases ( ( x in REAL & y in REAL ) or z in REAL ) by A1;
suppose ( x in REAL & y in REAL ) ; ::_thesis: (x + y) / z = (x / z) + (y / z)
then reconsider x1 = x, y1 = y as Real ;
percases ( z in REAL or z = +infty or z = -infty ) by XXREAL_0:14;
suppose z in REAL ; ::_thesis: (x + y) / z = (x / z) + (y / z)
hence  (x + y) / z = (x / z) + (y / z) by XXREAL_3:95; ::_thesis: verum
end;
supposeA2: ( z = +infty or z = -infty ) ; ::_thesis: (x + y) / z = (x / z) + (y / z)
thus (x + y) / z = 0 + 0 by A2
.= (x / z) + (y / z) by A2 ; ::_thesis: verum
end;
end;
end;
suppose z in REAL ; ::_thesis: (x + y) / z = (x / z) + (y / z)
hence  (x + y) / z = (x / z) + (y / z) by XXREAL_3:95; ::_thesis: verum
end;
end;
end;

theorem Th8: :: FVALUAT1:8
for y, x being ext-real number st y <> +infty & y <> -infty & y <> 0 holds
(x / y) * y = x
proof
let y, x be ext-real number ; ::_thesis: ( y <> +infty & y <> -infty & y <> 0 implies (x / y) * y = x )
assume that
A1: ( y <> +infty & y <> -infty ) and
A2: y <> 0 ; ::_thesis: (x / y) * y = x
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 ; ::_thesis: verum
end;

theorem Th9: :: FVALUAT1:9
for y, x being ext-real number st y <> -infty & y <> +infty & x <> 0 & y <> 0 holds
x / y <> 0
proof
let y, x be ext-real number ; ::_thesis: ( y <> -infty & y <> +infty & x <> 0 & y <> 0 implies x / y <> 0 )
assume that
A1: ( y <> -infty & y <> +infty ) and
A2: x <> 0 and
A3: y <> 0 ; ::_thesis: x / y <> 0
assume  x / y = 0 ; ::_thesis: contradiction
then  y " = 0 by A2;
hence  contradiction by A1, A3, XXREAL_3:82; ::_thesis: verum
end;

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
proof
let x be number ; ::_thesis: ( x is ext-integer implies x is ext-real )
assume  ( x is integer or x = +infty ) ; :: according to FVALUAT1:def_1 ::_thesis: x is ext-real
hence  x is ext-real ; ::_thesis: verum
end;
end;

registration
cluster +infty  ->  ext-integer ;
coherence
 +infty is ext-integer by Def1;
cluster -infty  ->  non ext-integer ;
coherence
 not -infty is ext-integer
proof
thus  ( not -infty is integer & -infty <> +infty ) ; :: according to FVALUAT1:def_1 ::_thesis: verum
end;
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
proof
let x be number ; ::_thesis: ( x is real & x is ext-integer implies x is integer )
assume  ( x in REAL & ( x is integer or x = +infty ) ) ; :: according to XREAL_0:def_1,FVALUAT1:def_1 ::_thesis: x is integer
hence  x is integer ; ::_thesis: verum
end;
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 )
proof
take  1. ; ::_thesis: ( 1. is real & 1. is ext-integer & 1. is positive )
thus  ( 1. is real & 1. is ext-integer & 1. is positive ) ; ::_thesis: verum
end;
cluster ext-real positive ext-integer for set ;
existence
 ex b1 being ext-integer number st b1 is positive
proof
take  +infty ; ::_thesis: +infty is positive
thus  +infty is positive ; ::_thesis: verum
end;
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
proof
let x, y be ExtInt; ::_thesis: ( x < y implies x + 1 <= y )
assume A1: x < y ; ::_thesis: x + 1 <= y
percases ( ( x in REAL & y in REAL ) or not x in REAL or not y in REAL ) ;
suppose ( x in REAL & y in REAL ) ; ::_thesis: x + 1 <= y
then reconsider x1 = x, y1 = y as Real ;
 ex p, q being Real st
( p = x + 1. & q = y & p <= q )
proof
take  x1 + 1 ; ::_thesis: ex q being Real st
( x1 + 1 = x + 1. & q = y & x1 + 1 <= q )
take  y1 ; ::_thesis: ( x1 + 1 = x + 1. & y1 = y & x1 + 1 <= y1 )
thus  x1 + 1 = x + 1. by XXREAL_3:def_2; ::_thesis: ( y1 = y & x1 + 1 <= y1 )
thus  y1 = y ; ::_thesis: x1 + 1 <= y1
thus  x1 + 1 <= y1 by A1, INT_1:7; ::_thesis: verum
end;
hence  x + 1 <= y ; ::_thesis: verum
end;
suppose ( not x in REAL or not y in REAL ) ; ::_thesis: x + 1 <= y
then  ( x = +infty or x = -infty or y = +infty or y = -infty ) by XXREAL_0:14;
hence  x + 1 <= y by A1, XXREAL_0:3; ::_thesis: verum
end;
end;
end;

theorem :: FVALUAT1:11
for x being ExtInt holds -infty < x
proof
let x be ExtInt; ::_thesis: -infty < x
 ( x is Integer or x = +infty ) by Def1;
then  ( x in REAL or x = +infty ) by XREAL_0:def_1;
hence  -infty < x by XXREAL_0:12; ::_thesis: verum
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
defpred S1[ Integer] means ( $1 in X & $1 is positive );
percases ( ex i being positive Integer st i in X or for i being positive Integer holds not i in X ) ;
suppose ex i being positive Integer st i in X ; ::_thesis: ex b1 being positive ExtInt st
( b1 in X & ( for i being positive ExtInt st i in X holds
b1 <= i ) )
then A2: ex i being Integer st S1[i] ;
A3: for i being Integer st S1[i] holds
0 <= i ;
consider j0 being Integer such that
A4: S1[j0] and
A5: for i being Integer st S1[i] holds
j0 <= i from INT_1:sch_5(A3, A2);
reconsider j = j0 as positive ExtInt by A4;
take  j ; ::_thesis: ( j in X & ( for i being positive ExtInt st i in X holds
j <= i ) )
thus  j in X by A4; ::_thesis: for i being positive ExtInt st i in X holds
j <= i
let i be positive ExtInt; ::_thesis: ( i in X implies j <= i )
assume A6: i in X ; ::_thesis: j <= i
percases ( i is Integer or not i is Integer ) ;
suppose i is Integer ; ::_thesis: j <= i
then reconsider i1 = i as Integer ;
 j0 <= i1 by A6, A5;
hence  j <= i ; ::_thesis: verum
end;
suppose i is not Integer ; ::_thesis: j <= i
then  i = +infty by Def1;
hence  j <= i by XXREAL_0:3; ::_thesis: verum
end;
end;
end;
supposeA7: for i being positive Integer holds not i in X ; ::_thesis: ex b1 being positive ExtInt st
( b1 in X & ( for i being positive ExtInt st i in X holds
b1 <= i ) )
take  i0 ; ::_thesis: ( i0 in X & ( for i being positive ExtInt st i in X holds
i0 <= i ) )
thus  i0 in X by A1; ::_thesis: for i being positive ExtInt st i in X holds
i0 <= i
let i be positive ExtInt; ::_thesis: ( i in X implies i0 <= i )
assume  i in X ; ::_thesis: i0 <= i
then  ( i is not positive Integer & +infty <= +infty ) by A7;
then  i = +infty by Def1;
hence  i0 <= i by XXREAL_0:3; ::_thesis: verum
end;
end;
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
let a, b be positive ExtInt; ::_thesis: ( a in X & ( for i being positive ExtInt st i in X holds
a <= i ) & b in X & ( for i being positive ExtInt st i in X holds
b <= i ) implies a = b )
assume  ( a in X & ( for i being positive ExtInt st i in X holds
a <= i ) & b in X & ( for i being positive ExtInt st i in X holds
b <= i ) ) ; ::_thesis: a = b
then  ( a <= b & b <= a ) ;
hence  a = b by XXREAL_0:1; ::_thesis: verum
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;
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
proof
take f = 0 --> 0.; ::_thesis: f is e.i.-valued
let x be set ; :: according to FVALUAT1:def_3 ::_thesis: ( x in rng f implies x is ext-integer )
 rng f c= {0} by FUNCOP_1:13;
hence  ( x in rng f implies x is ext-integer ) ; ::_thesis: verum
end;
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
proof
take f = A --> 0.; ::_thesis: f is e.i.-valued
let x be set ; :: according to FVALUAT1:def_3 ::_thesis: ( x in rng f implies x is ext-integer )
 rng f c= {0} by FUNCOP_1:13;
hence  ( x in rng f implies x is ext-integer ) ; ::_thesis: verum
end;
end;

registration
let f be e.i.-valued Function;
let x be set ;
clusterf . x ->  ext-integer ;
coherence
 f . x is ext-integer
proof
percases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; ::_thesis: f . x is ext-integer
then  f . x in rng f by FUNCT_1:def_3;
hence  f . x is ext-integer by Def3; ::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f . x is ext-integer
hence  f . x is ext-integer by FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
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
proof
let K be non empty right_complementable distributive left_unital add-associative right_zeroed doubleLoopStr ; ::_thesis: (- (1. K)) * (- (1. K)) = 1. K
thus (- (1. K)) * (- (1. K)) = (1. K) * (1. K) by VECTSP_1:10
.= 1. K by VECTSP_1:def_8 ; ::_thesis: verum
end;

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) ) ) ) )
proof
hereby  ::_thesis: ( 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) ) ) )
assume  n = 0 ; ::_thesis: ex A being Element of bool the carrier of K st A = the carrier of K
take A = [#] K; ::_thesis: A = the carrier of K
thus  A = the carrier of K ; ::_thesis: verum
end;
assume A1: n <> 0 ; ::_thesis: 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) ) )
set D = bool the carrier of K;
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
defpred S1[ set , set , set ] means  ex A being Subset of K st
( A = $2 & $3 = S *' A );
A2: for i being Element of NAT st 1 <= i & i < n1 holds
for x being Element of bool the carrier of K ex y being Element of bool the carrier of K st S1[i,x,y]
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < n1 implies for x being Element of bool the carrier of K ex y being Element of bool the carrier of K st S1[i,x,y] )
assume  ( 1 <= i & i < n1 ) ; ::_thesis: for x being Element of bool the carrier of K ex y being Element of bool the carrier of K st S1[i,x,y]
let x be Element of bool the carrier of K; ::_thesis: ex y being Element of bool the carrier of K st S1[i,x,y]
take  S *' x ; ::_thesis: S1[i,x,S *' x]
thus  S1[i,x,S *' x] ; ::_thesis: verum
end;
consider f being FinSequence of bool the carrier of K such that
A3: len f = n1 and
A4: ( f . 1 = S or n1 = 0 ) and
A5: for i being Element of NAT st 1 <= i & i < n1 holds
S1[i,f . i,f . (i + 1)] from RECDEF_1:sch_4(A2);
take  f /. (len f) ; ::_thesis: ex f being FinSequence of bool the carrier of K st
( f /. (len f) = 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) ) )
take  f ; ::_thesis: ( f /. (len f) = 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) ) )
 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; ::_thesis: ( 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) ) )
thus  len f = n by A3; ::_thesis: ( f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ) )
thus  f . 1 = S by A1, A4; ::_thesis: for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i)
let i be Nat; ::_thesis: ( i in dom f & i + 1 in dom f implies f . (i + 1) = S *' (f /. i) )
assume A6: i in dom f ; ::_thesis: ( not i + 1 in dom f or f . (i + 1) = S *' (f /. i) )
assume  i + 1 in dom f ; ::_thesis: f . (i + 1) = S *' (f /. i)
then  i + 1 <= n1 by A3, FINSEQ_3:25;
then A7: i < n1 by NAT_1:13;
A8: i is Element of NAT by ORDINAL1:def_12;
 1 <= i by A6, FINSEQ_3:25;
then  S1[i,f . i,f . (i + 1)] by A5, A8, A7;
hence  f . (i + 1) = S *' (f /. i) by A6, PARTFUN1:def_6; ::_thesis: verum
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
let S1, S2 be Subset of K; ::_thesis: ( ( n = 0 & S1 = the carrier of K & S2 = the carrier of K implies S1 = S2 ) & ( not n = 0 & ex f being FinSequence of bool the carrier of K st
( S1 = 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
( S2 = 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 S1 = S2 ) )
thus  ( n = 0 & S1 = the carrier of K & S2 = the carrier of K implies S1 = S2 ) ; ::_thesis: ( not n = 0 & ex f being FinSequence of bool the carrier of K st
( S1 = 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
( S2 = 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 S1 = S2 )
assume  n <> 0 ; ::_thesis: ( for f being FinSequence of bool the carrier of K holds
( not S1 = f . (len f) or not len f = n or not f . 1 = S or ex i being Nat st
( i in dom f & i + 1 in dom f & not f . (i + 1) = S *' (f /. i) ) ) or for f being FinSequence of bool the carrier of K holds
( not S2 = f . (len f) or not len f = n or not f . 1 = S or ex i being Nat st
( i in dom f & i + 1 in dom f & not f . (i + 1) = S *' (f /. i) ) ) or S1 = S2 )
given f being FinSequence of bool the carrier of K such that A9: S1 = f . (len f) and
A10: len f = n and
A11: f . 1 = S and
A12: for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ; ::_thesis: ( for f being FinSequence of bool the carrier of K holds
( not S2 = f . (len f) or not len f = n or not f . 1 = S or ex i being Nat st
( i in dom f & i + 1 in dom f & not f . (i + 1) = S *' (f /. i) ) ) or S1 = S2 )
given g being FinSequence of bool the carrier of K such that A13: S2 = g . (len g) and
A14: len g = n and
A15: g . 1 = S and
A16: for i being Nat st i in dom g & i + 1 in dom g holds
g . (i + 1) = S *' (g /. i) ; ::_thesis: S1 = S2
A17: dom f = dom g by A10, A14, FINSEQ_3:29;
 for k being Nat st k in dom f holds
f . k = g . k
proof
let k be Nat; ::_thesis: ( k in dom f implies f . k = g . k )
defpred S1[ Nat] means ( $1 in dom f implies f . $1 = g . $1 );
A18: S1[ 0 ] by FINSEQ_3:24;
A19: for a being Nat st S1[a] holds
S1[a + 1]
proof
let a be Nat; ::_thesis: ( S1[a] implies S1[a + 1] )
assume that
A20: S1[a] and
A21: a + 1 in dom f ; ::_thesis: f . (a + 1) = g . (a + 1)
percases ( a in dom f or not a in dom f ) ;
supposeA22: a in dom f ; ::_thesis: f . (a + 1) = g . (a + 1)
then A23: f /. a = f . a by PARTFUN1:def_6
.= g /. a by A17, A20, A22, PARTFUN1:def_6 ;
thus f . (a + 1) = S *' (f /. a) by A12, A21, A22
.= g . (a + 1) by A16, A17, A21, A22, A23 ; ::_thesis: verum
end;
suppose not a in dom f ; ::_thesis: f . (a + 1) = g . (a + 1)
then  a = 0 by A21, TOPREALA:2;
hence  f . (a + 1) = g . (a + 1) by A11, A15; ::_thesis: verum
end;
end;
end;
 for a being Nat holds S1[a] from NAT_1:sch_2(A18, A19);
hence  ( k in dom f implies f . k = g . k ) ; ::_thesis: verum
end;
hence  S1 = S2 by A9, A13, A10, A14, A17, FINSEQ_1:13; ::_thesis: verum
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
let D be non empty doubleLoopStr ; ::_thesis: for A being Subset of D holds A |^ 1 = A
let A be Subset of D; ::_thesis: A |^ 1 = A
set f = <*A*>;
A1: ( len <*A*> = 1 & <*A*> . 1 = A ) by FINSEQ_1:40;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_<*A*>_&_i_+_1_in_dom_<*A*>_holds_
<*A*>_._(i_+_1)_=_A_*'_(<*A*>_/._i)
let i be Nat; ::_thesis: ( i in dom <*A*> & i + 1 in dom <*A*> implies <*A*> . (i + 1) = A *' (<*A*> /. i) )
assume A2: ( i in dom <*A*> & i + 1 in dom <*A*> ) ; ::_thesis: <*A*> . (i + 1) = A *' (<*A*> /. i)
 dom <*A*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then  ( i = 1 & i + 1 = 1 ) by A2, TARSKI:def_1;
hence  <*A*> . (i + 1) = A *' (<*A*> /. i) ; ::_thesis: verum
end;
hence  A |^ 1 = A by A1, Def4; ::_thesis: verum
end;

theorem :: FVALUAT1:14
for D being non empty doubleLoopStr
for A being Subset of D holds A |^ 2 = A *' A
proof
let D be non empty doubleLoopStr ; ::_thesis: for A being Subset of D holds A |^ 2 = A *' A
let A be Subset of D; ::_thesis: A |^ 2 = A *' A
set f = <*A,(A *' A)*>;
A1: len <*A,(A *' A)*> = 2 by FINSEQ_1:44;
A2: <*A,(A *' A)*> . 1 = A by FINSEQ_1:44;
A3: <*A,(A *' A)*> . 2 = A *' A by FINSEQ_1:44;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_<*A,(A_*'_A)*>_&_i_+_1_in_dom_<*A,(A_*'_A)*>_holds_
<*A,(A_*'_A)*>_._(i_+_1)_=_A_*'_(<*A,(A_*'_A)*>_/._i)
let i be Nat; ::_thesis: ( i in dom <*A,(A *' A)*> & i + 1 in dom <*A,(A *' A)*> implies <*A,(A *' A)*> . (i + 1) = A *' (<*A,(A *' A)*> /. i) )
assume that
A4: i in dom <*A,(A *' A)*> and
A5: i + 1 in dom <*A,(A *' A)*> ; ::_thesis: <*A,(A *' A)*> . (i + 1) = A *' (<*A,(A *' A)*> /. i)
 dom <*A,(A *' A)*> = {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  <*A,(A *' A)*> . (i + 1) = A *' (<*A,(A *' A)*> /. i) by A2, A3, A4, PARTFUN1:def_6; ::_thesis: verum
end;
hence  A |^ 2 = A *' A by A1, A2, A3, Def4; ::_thesis: verum
end;

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 )
proof
percases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;
supposeA1: n = 0 ; ::_thesis: ( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal )
A2: S |^ 0 = the carrier of R by Def4;
thus  not S |^ n is empty by A1, Def4; ::_thesis: ( S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal )
thus  S |^ n is add-closed ::_thesis: ( S |^ n is left-ideal & S |^ n is right-ideal )
proof
let x, y be Element of R; :: according to IDEAL_1:def_1 ::_thesis: ( not x in S |^ n or not y in S |^ n or x + y in S |^ n )
thus  ( not x in S |^ n or not y in S |^ n or x + y in S |^ n ) by A2, A1; ::_thesis: verum
end;
thus  S |^ n is left-ideal ::_thesis: S |^ n is right-ideal
proof
let p, x be Element of R; :: according to IDEAL_1:def_2 ::_thesis: ( not x in S |^ n or p * x in S |^ n )
thus  ( not x in S |^ n or p * x in S |^ n ) by A2, A1; ::_thesis: verum
end;
let p, x be Element of R; :: according to IDEAL_1:def_3 ::_thesis: ( not x in S |^ n or x * p in S |^ n )
thus  ( not x in S |^ n or x * p in S |^ n ) by A2, A1; ::_thesis: verum
end;
supposeA3: ex k being Nat st n = k + 1 ; ::_thesis: ( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal )
then consider f being 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 being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) by Def4;
defpred S1[ Nat] means ( R in dom f implies f . R is Ideal of R );
A6: S1[ 0 ] by FINSEQ_3:24;
A7: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume that
A8: S1[m] and
A9: m + 1 in dom f ; ::_thesis: f . (m + 1) is Ideal of R
percases ( m = 0 or m in dom f ) by A9, TOPREALA:2;
suppose m = 0 ; ::_thesis: f . (m + 1) is Ideal of R
hence  f . (m + 1) is Ideal of R by A4; ::_thesis: verum
end;
supposeA10: m in dom f ; ::_thesis: f . (m + 1) is Ideal of R
then A11: f /. m = f . m by PARTFUN1:def_6;
 f . (m + 1) = S *' (f /. m) by A5, A9, A10;
hence  f . (m + 1) is Ideal of R by A10, A8, A11; ::_thesis: verum
end;
end;
end;
A12: for m being Nat holds S1[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  ( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal ) by A4, A12; ::_thesis: verum
end;
end;
end;
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) )
proof
let g be Element of G; ::_thesis: ( g = g |^ n iff g = (power G) . (g,n) )
 abs n = n by ABSVALUE:def_1;
hence  ( g = g |^ n iff g = (power G) . (g,n) ) by Def5; ::_thesis: verum
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);

    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
proof
let n be Nat; ::_thesis: 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
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: for a being Element of K holds a |^ (n + 1) = (a |^ n) * a
let a be Element of K; ::_thesis: a |^ (n + 1) = (a |^ n) * a
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
thus a |^ (n + 1) = ((power K) . (a,n1)) * a by GROUP_1:def_7
.= (a |^ n) * a ; ::_thesis: verum
end;

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)
proof
let n, m be Nat; ::_thesis: 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)
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: for a being Element of K holds a |^ (n + m) = (a |^ n) * (a |^ m)
let a be Element of K; ::_thesis: a |^ (n + m) = (a |^ n) * (a |^ m)
defpred S1[ Nat] means  for n being Nat holds a |^ (n + $1) = (a |^ n) * (a |^ $1);
A1: S1[ 0 ]
proof
let n be Nat; ::_thesis: a |^ (n + 0) = (a |^ n) * (a |^ 0)
thus a |^ (n + 0) = (a |^ n) * (1_ K) by VECTSP_1:def_4
.= (a |^ n) * (a |^ 0) by GROUP_1:def_7 ; ::_thesis: verum
end;
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A3: for n being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m) ; ::_thesis: S1[m + 1]
let n be Nat; ::_thesis: a |^ (n + (m + 1)) = (a |^ n) * (a |^ (m + 1))
thus a |^ (n + (m + 1)) = a |^ ((n + m) + 1)
.= (a |^ (n + m)) * a by Lm3
.= ((a |^ n) * (a |^ m)) * a by A3
.= (a |^ n) * ((a |^ m) * a) by GROUP_1:def_3
.= (a |^ n) * (a |^ (m + 1)) by Lm3 ; ::_thesis: verum
end;
 for m being Nat holds S1[m] from NAT_1:sch_2(A1, A2);
hence  a |^ (n + m) = (a |^ n) * (a |^ m) ; ::_thesis: verum
end;

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
proof
let n be Nat; ::_thesis: 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
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: for a being Element of K st a <> 0. K holds
a |^ n <> 0. K
let a be Element of K; ::_thesis: ( a <> 0. K implies a |^ n <> 0. K )
assume A1: a <> 0. K ; ::_thesis: a |^ n <> 0. K
defpred S1[ Nat] means a |^ $1 <> 0. K;
 a |^ 0 = 1_ K by GROUP_1:def_7;
then A2: S1[ 0 ] ;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
 a |^ (n + 1) = (a |^ n) * a by Lm3;
hence  a |^ (n + 1) <> 0. K by A4, A1, VECTSP_1:12; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A2, A3);
hence  a |^ n <> 0. K ; ::_thesis: verum
end;

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
proof
let i be Integer; ::_thesis: 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
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: for a being Element of K st a <> 0. K holds
a |^ i <> 0. K
let a be Element of K; ::_thesis: ( a <> 0. K implies a |^ i <> 0. K )
assume A1: a <> 0. K ; ::_thesis: a |^ i <> 0. K
percases ( 0 <= i or i < 0 ) ;
suppose 0 <= i ; ::_thesis: a |^ i <> 0. K
then reconsider n1 = i as Element of NAT by INT_1:3;
 a |^ i = a |^ n1 ;
hence  a |^ i <> 0. K by A1, Lm4; ::_thesis: verum
end;
supposeA2: i < 0 ; ::_thesis: a |^ i <> 0. K
then reconsider n1 = - i as Element of NAT by INT_1:3;
A3: a |^ i = ((power K) . (a,(abs i))) " by A2, Def5
.= (a |^ n1) " by A2, ABSVALUE:def_1 ;
 a |^ n1 <> 0. K by A1, Lm4;
hence  a |^ i <> 0. K by A3, VECTSP_2:13; ::_thesis: verum
end;
end;
end;

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
proof
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
v . (1. K) = 0
let v be Valuation of K; ::_thesis: ( K is having_valuation implies v . (1. K) = 0 )
assume A1: K is having_valuation ; ::_thesis: v . (1. K) = 0
A2: v . (1. K) = v . ((1. K) * (1. K)) by VECTSP_1:def_8
.= (v . (1. K)) + (v . (1. K)) by A1, Def8 ;
 1. K <> 0. K ;
then  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  v . (1. K) = 0 ; ::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: for a being Element of K
for v being Valuation of K st K is having_valuation & a <> 0. K holds
v . a <> +infty
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & a <> 0. K holds
v . a <> +infty
let v be Valuation of K; ::_thesis: ( K is having_valuation & a <> 0. K implies v . a <> +infty )
assume  ( K is having_valuation & a <> 0. K ) ; ::_thesis: v . a <> +infty
then  v . a in INT by Def8;
hence  v . a <> +infty ; ::_thesis: verum
end;

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
proof
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
v . (- (1. K)) = 0
let v be Valuation of K; ::_thesis: ( K is having_valuation implies v . (- (1. K)) = 0 )
assume A1: K is having_valuation ; ::_thesis: v . (- (1. K)) = 0
 (- (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  v . (- (1. K)) = 0 by Th2; ::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: for a being Element of K
for v being Valuation of K st K is having_valuation holds
v . (- a) = v . a
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation holds
v . (- a) = v . a
let v be Valuation of K; ::_thesis: ( K is having_valuation implies v . (- a) = v . a )
assume A1: K is having_valuation ; ::_thesis: v . (- a) = v . a
 (- (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 ;
::_thesis: verum
end;

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)
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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)
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & a <> 0. K holds
v . (a ") = - (v . a)
let v be Valuation of K; ::_thesis: ( K is having_valuation & a <> 0. K implies v . (a ") = - (v . a) )
assume that
A1: K is having_valuation and
A2: a <> 0. K ; ::_thesis: v . (a ") = - (v . a)
 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__::_thesis:_not_a_"_=_0._K
assume  a " = 0. K ; ::_thesis: contradiction
then  1. K = a * (0. K) by A2, VECTSP_2:def_2
.= 0. K by VECTSP_1:6 ;
hence  contradiction ; ::_thesis: verum
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  v . (a ") = - (v . a) by XXREAL_3:def_3; ::_thesis: verum
end;

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)
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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)
let b, a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & b <> 0. K holds
v . (a / b) = (v . a) - (v . b)
let v be Valuation of K; ::_thesis: ( K is having_valuation & b <> 0. K implies v . (a / b) = (v . a) - (v . b) )
assume A1: K is having_valuation ; ::_thesis: ( not b <> 0. K or v . (a / b) = (v . a) - (v . b) )
assume A2: b <> 0. K ; ::_thesis: v . (a / b) = (v . a) - (v . b)
thus v . (a / b) = (v . a) + (v . (b ")) by A1, Def8
.= (v . a) - (v . b) by A1, A2, Th21 ; ::_thesis: verum
end;

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))
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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))
let a, b be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & a <> 0. K & b <> 0. K holds
v . (a / b) = - (v . (b / a))
let v be Valuation of K; ::_thesis: ( K is having_valuation & a <> 0. K & b <> 0. K implies v . (a / b) = - (v . (b / a)) )
assume A1: K is having_valuation ; ::_thesis: ( not a <> 0. K or not b <> 0. K or v . (a / b) = - (v . (b / a)) )
assume A2: a <> 0. K ; ::_thesis: ( not b <> 0. K or v . (a / b) = - (v . (b / a)) )
assume  b <> 0. K ; ::_thesis: v . (a / b) = - (v . (b / a))
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 ;
::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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
let b, a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & b <> 0. K & 0 <= v . (a / b) holds
v . b <= v . a
let v be Valuation of K; ::_thesis: ( K is having_valuation & b <> 0. K & 0 <= v . (a / b) implies v . b <= v . a )
assume that
A1: K is having_valuation and
A2: b <> 0. K and
A3: 0 <= v . (a / b) ; ::_thesis: v . b <= v . a
A4: v . (a / b) = (v . a) - (v . b) by A1, A2, Th22;
percases ( a = 0. K or a <> 0. K ) ;
suppose a = 0. K ; ::_thesis: v . b <= v . a
then  v . a = +infty by A1, Def8;
hence  v . b <= v . a by XXREAL_0:3; ::_thesis: verum
end;
suppose a <> 0. K ; ::_thesis: v . b <= v . a
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; ::_thesis: verum
end;
end;
end;

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)
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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)
let a, b be Element of K; ::_thesis: 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)
let v be Valuation of K; ::_thesis: ( K is having_valuation & a <> 0. K & b <> 0. K & v . (a / b) <= 0 implies 0 <= v . (b / a) )
assume  ( K is having_valuation & a <> 0. K & b <> 0. K ) ; ::_thesis: ( not v . (a / b) <= 0 or 0 <= v . (b / a) )
then  v . (a / b) = - (v . (b / a)) by Th23;
hence  ( not v . (a / b) <= 0 or 0 <= v . (b / a) ) ; ::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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
let b, a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & b <> 0. K & v . (a / b) <= 0 holds
v . a <= v . b
let v be Valuation of K; ::_thesis: ( K is having_valuation & b <> 0. K & v . (a / b) <= 0 implies v . a <= v . b )
assume that
A1: K is having_valuation and
A2: b <> 0. K and
A3: v . (a / b) <= 0 ; ::_thesis: v . a <= v . b
A4: now__::_thesis:_not_a_=_0._K
assume A5: a = 0. K ; ::_thesis: contradiction
a / b = a * (b ")
.= 0. K by A5, VECTSP_1:6 ;
hence  contradiction by A1, Def8, A3; ::_thesis: verum
end;
then  0 <= v . (b / a) by A1, A2, A3, Th25;
hence  v . a <= v . b by A1, A4, Th24; ::_thesis: verum
end;

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)
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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)
let a, b be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation holds
min ((v . a),(v . b)) <= v . (a + b)
let v be Valuation of K; ::_thesis: ( K is having_valuation implies min ((v . a),(v . b)) <= v . (a + b) )
assume A1: K is having_valuation ; ::_thesis: min ((v . a),(v . b)) <= v . (a + b)
percases ( a = 0. K or b = 0. K or ( a <> 0. K & 0 <= v . (b / a) ) or ( a <> 0. K & b <> 0. K & v . (b / a) <= 0 ) ) ;
supposeA2: a = 0. K ; ::_thesis: min ((v . a),(v . b)) <= v . (a + b)
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; ::_thesis: verum
end;
supposeA3: b = 0. K ; ::_thesis: min ((v . a),(v . b)) <= v . (a + b)
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; ::_thesis: verum
end;
supposethat A4: a <> 0. K and
A5: 0 <= v . (b / a) ; ::_thesis: min ((v . a),(v . b)) <= v . (a + b)
 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)) by VECTSP_1:def_8
.= v . (a + b) by A4, VECTSP_2:22 ;
hence  min ((v . a),(v . b)) <= v . (a + b) by A6, A7, XXREAL_3:4; ::_thesis: verum
end;
supposethat A8: a <> 0. K and
A9: b <> 0. K and
A10: v . (b / a) <= 0 ; ::_thesis: min ((v . a),(v . b)) <= v . (a + b)
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)) by VECTSP_1:def_8
.= v . (b + a) by A9, VECTSP_2:22 ;
hence  min ((v . a),(v . b)) <= v . (a + b) by A12, A13, XXREAL_3:4; ::_thesis: verum
end;
end;
end;

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)
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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)
let a, b be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & v . a < v . b holds
v . a = v . (a + b)
let v be Valuation of K; ::_thesis: ( K is having_valuation & v . a < v . b implies v . a = v . (a + b) )
assume A1: ( K is having_valuation & v . a < v . b ) ; ::_thesis: v . a = v . (a + 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  v . a = v . (a + b) by A3, A8, XXREAL_0:1; ::_thesis: verum
end;

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)
proof
let i be Integer; ::_thesis: 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)
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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)
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & a <> 0. K holds
v . (a |^ i) = i * (v . a)
let v be Valuation of K; ::_thesis: ( K is having_valuation & a <> 0. K implies v . (a |^ i) = i * (v . a) )
assume that
A1: K is having_valuation and
A2: a <> 0. K ; ::_thesis: v . (a |^ i) = i * (v . a)
defpred S1[ Nat] means v . (a |^ $1) = $1 * (v . a);
 a |^ 0 = 1_ K by GROUP_1:def_7;
then A3: S1[ 0 ] by A1, Th17;
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A5: S1[n] ; ::_thesis: S1[n + 1]
A6: v . a in REAL by A1, A2, Th18, XXREAL_0:14;
reconsider N = n as ext-real number ;
thus v . (a |^ (n + 1)) = v . ((a |^ n) * a) by Lm3
.= (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 ; ::_thesis: verum
end;
A7: for n being Nat holds S1[n] from NAT_1:sch_2(A3, A4);
percases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; ::_thesis: v . (a |^ i) = i * (v . a)
then reconsider j = i as Element of NAT by INT_1:3;
 S1[j] by A7;
hence  v . (a |^ i) = i * (v . a) ; ::_thesis: verum
end;
supposeA8: i < 0 ; ::_thesis: v . (a |^ i) = i * (v . a)
then reconsider n1 = - i as Element of NAT by INT_1:3;
reconsider I = i as ext-real number ;
A9: v . (a |^ i) = v . (((power K) . (a,(abs i))) ") by A8, Def5
.= v . ((a |^ n1) ") by A8, ABSVALUE:def_1 ;
v . ((a |^ n1) ") = - (v . (a |^ n1)) by A1, A2, Th21, Lm4
.= - (n1 * (v . a)) by A7
.= - ((- I) * (v . a)) by XXREAL_3:def_3
.= - (- (i * (v . a))) by XXREAL_3:92 ;
hence  v . (a |^ i) = i * (v . a) by A9; ::_thesis: verum
end;
end;
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & 0 <= v . ((1. K) + a) holds
0 <= v . a
let v be Valuation of K; ::_thesis: ( K is having_valuation & 0 <= v . ((1. K) + a) implies 0 <= v . a )
assume that
A1: ( K is having_valuation & 0 <= v . ((1. K) + a) ) and
A2: v . a < 0 ; ::_thesis: contradiction
 0 = v . (1. K) by A1, Th17;
hence  contradiction by A1, A2, Th28; ::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & 0 <= v . ((1. K) - a) holds
0 <= v . a
let v be Valuation of K; ::_thesis: ( K is having_valuation & 0 <= v . ((1. K) - a) implies 0 <= v . a )
assume that
A1: K is having_valuation and
A2: 0 <= v . ((1. K) - a) ; ::_thesis: 0 <= v . a
 ( (1. K) - a = (1. K) + (- a) & v . (- a) = v . a ) by A1, Th20;
hence  0 <= v . a by A1, A2, Th30; ::_thesis: verum
end;

Lm5:  for a, b being ExtInt st a <= b holds
0 <= b - a
proof
let a, b be ExtInt; ::_thesis: ( a <= b implies 0 <= b - a )
assume  a <= b ; ::_thesis: 0 <= b - a
then  a + (- a) <= b + (- a) by XXREAL_3:36;
hence  0 <= b - a by XXREAL_3:7; ::_thesis: verum
end;

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)
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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)
let a, b be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & a <> 0. K & v . a <= v . b holds
0 <= v . (b / a)
let v be Valuation of K; ::_thesis: ( K is having_valuation & a <> 0. K & v . a <= v . b implies 0 <= v . (b / a) )
assume that
A1: K is having_valuation and
A2: a <> 0. K ; ::_thesis: ( not v . a <= v . b or 0 <= v . (b / a) )
assume  v . a <= v . b ; ::_thesis: 0 <= v . (b / a)
then  0 <= (v . b) - (v . a) by Lm5;
hence  0 <= v . (b / a) by A1, A2, Th22; ::_thesis: verum
end;

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
proof
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
+infty in rng v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies +infty in rng v )
assume  K is having_valuation ; ::_thesis: +infty in rng v
then A1: v . (0. K) = +infty by Def8;
 dom v = the carrier of K by FUNCT_2:def_1;
hence  +infty in rng v by A1, FUNCT_1:def_3; ::_thesis: verum
end;

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
proof
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
least-positive (rng v) in rng v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies least-positive (rng v) in rng v )
assume  K is having_valuation ; ::_thesis: least-positive (rng v) in rng v
then  +infty in rng v by Th33;
hence  least-positive (rng v) in rng v by Def2; ::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: for a being Element of K
for v being Valuation of K st v . a = 1 holds
least-positive (rng v) = 1
let a be Element of K; ::_thesis: for v being Valuation of K st v . a = 1 holds
least-positive (rng v) = 1
let v be Valuation of K; ::_thesis: ( v . a = 1 implies least-positive (rng v) = 1 )
assume A1: v . a = 1 ; ::_thesis: least-positive (rng v) = 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__::_thesis:_for_i_being_positive_ExtInt_st_i_in_rng_v_holds_
1._<=_i
let i be positive ExtInt; ::_thesis: ( i in rng v implies 1. <= b1 )
assume  i in rng v ; ::_thesis: 1. <= b1
percases ( i is real positive number or i = +infty ) by XXREAL_3:1;
suppose i is real positive number ; ::_thesis: 1. <= b1
then reconsider i1 = i as real positive number ;
 ex p, q being Real st
( p = 1. & q = i & p <= q )
proof
reconsider i1 = i1 as Real by XREAL_0:def_1;
take  1 ; ::_thesis: ex q being Real st
( 1 = 1. & q = i & 1 <= q )
take  i1 ; ::_thesis: ( 1 = 1. & i1 = i & 1 <= i1 )
 0 + 1 <= i1 by INT_1:7;
hence  ( 1 = 1. & i1 = i & 1 <= i1 ) ; ::_thesis: verum
end;
hence  1. <= i ; ::_thesis: verum
end;
suppose i = +infty ; ::_thesis: 1. <= b1
hence  1. <= i by XXREAL_0:3; ::_thesis: verum
end;
end;
end;
hence  least-positive (rng v) = 1 by A1, A2, Def2; ::_thesis: verum
end;

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
proof
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
least-positive (rng v) is integer
let v be Valuation of K; ::_thesis: ( K is having_valuation implies least-positive (rng v) is integer )
set l = least-positive (rng v);
assume A1: K is having_valuation ; ::_thesis: least-positive (rng v) is integer
then consider a being Element of K 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 least-positive (rng v) is integer ; ::_thesis: contradiction
then A6: least-positive (rng v) = +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 by XREAL_0:def_1;
percases ( va is positive or not va is positive ) ;
suppose va is positive ; ::_thesis: contradiction
then  least-positive (rng v) <= v . a by A5, Def2;
hence  contradiction by A3, A6, XXREAL_0:4; ::_thesis: verum
end;
suppose not va is positive ; ::_thesis: contradiction
then reconsider va = va as real non positive number ;
reconsider va = va as real negative number by A2;
set b = a " ;
 a " <> 0. K by A7, VECTSP_2:13;
then A8: v . (a ") in INT by A1, Def8;
A9: v . (a ") in rng v by A4, FUNCT_1:def_3;
v . (a ") = - (v . a) by A1, A7, Th21
.= - va by XXREAL_3:def_3 ;
then  least-positive (rng v) <= v . (a ") by A9, Def2;
hence  contradiction by A8, A6, XXREAL_0:4; ::_thesis: verum
end;
end;
end;

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
proof
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
least-positive (rng v) in REAL
let v be Valuation of K; ::_thesis: ( K is having_valuation implies least-positive (rng v) in REAL )
assume  K is having_valuation ; ::_thesis: least-positive (rng v) in REAL
then  least-positive (rng v) is integer by Th35;
then  least-positive (rng v) in INT by INT_1:def_2;
hence  least-positive (rng v) in REAL by XREAL_0:def_1; ::_thesis: verum
end;

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))
proof
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
for x being Element of K st x <> 0. K holds
ex i being Integer st v . x = i * (least-positive (rng v))
let v be Valuation of K; ::_thesis: ( K is having_valuation implies for x being Element of K st x <> 0. K holds
ex i being Integer st v . x = i * (least-positive (rng v)) )
assume A1: K is having_valuation ; ::_thesis: for x being Element of K st x <> 0. K holds
ex i being Integer st v . x = i * (least-positive (rng v))
let x be Element of K; ::_thesis: ( x <> 0. K implies ex i being Integer st v . x = i * (least-positive (rng v)) )
assume A2: x <> 0. K ; ::_thesis: ex i being Integer st v . x = i * (least-positive (rng v))
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;
percases ( vx mod l = 0 or vx mod l <> 0 ) ;
supposeA4: vx mod l = 0 ; ::_thesis: ex i being Integer st v . x = i * (least-positive (rng v))
take  vx div l ; ::_thesis: v . x = (vx div l) * (least-positive (rng v))
thus  v . x = (vx div l) * (least-positive (rng v)) by A3, A4, XXREAL_3:def_5; ::_thesis: verum
end;
supposeA5: vx mod l <> 0 ; ::_thesis: ex i being Integer st v . x = i * (least-positive (rng v))
consider k being Element of K such that
A6: l = v . k by A1, Lm6, FUNCT_2:113;
set d = vx div l;
set kd = k |^ (vx div l);
set kD = (k |^ (vx div l)) " ;
A7: k <> 0. K by A1, A6, Def8;
then A8: (vx div l) * (v . k) = v . (k |^ (vx div l)) by A1, Th29;
A9: - (v . (k |^ (vx div l))) = v . ((k |^ (vx div l)) ") by A1, A7, Th16, Th21;
A10: (vx div l) * l = (vx div l) * (v . k) by A6, XXREAL_3:def_5;
A11: v . (x * ((k |^ (vx div l)) ")) = (v . x) - ((vx div l) * l) by A8, A9, A10, A1, Def8
.= vx - ((vx div l) * l) by Lm1
.= vx mod l by A3 ;
then A12: 0 <= v . (x * ((k |^ (vx div l)) ")) by INT_1:57;
A13: v . (x * ((k |^ (vx div l)) ")) < l by A11, INT_1:58;
 v . (x * ((k |^ (vx div l)) ")) in rng v by FUNCT_2:4;
hence  ex i being Integer st v . x = i * (least-positive (rng v)) by A12, A5, A11, A13, Def2; ::_thesis: verum
end;
end;
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 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
set l = least-positive (rng v);
 least-positive (rng v) in rng v by A1, Lm6;
then  {(least-positive (rng v))} c= rng v by ZFMISC_1:31;
then  not v " {(least-positive (rng v))} is empty by RELAT_1:139;
then  the Element of v " {(least-positive (rng v))} in v " {(least-positive (rng v))} ;
hence  the Element of v " {(least-positive (rng v))} is Element of K ; ::_thesis: verum
end;
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))
proof
set l = least-positive (rng v);
reconsider ll = least-positive (rng v) as Element of ExtREAL by XXREAL_0:def_1;
reconsider l1 = least-positive (rng v) as Integer by A1, Th35;
A2: l1 in REAL by XREAL_0:def_1;
deffunc H1( Element of K) ->  Element of ExtREAL = (v . $1) / ll;
consider f being Function of K,ExtREAL such that
A3: for x being Element of K holds f . x = H1(x) from FUNCT_2:sch_4();
 for y being set st y in rng f holds
y is ext-integer
proof
let y be set ; ::_thesis: ( y in rng f implies y is ext-integer )
assume  y in rng f ; ::_thesis: y is ext-integer
then consider x being set  such that
A4: x in dom f and
A5: f . x = y by FUNCT_1:def_3;
reconsider x = x as Element of K by A4;
A6: f . x = (v . x) / (least-positive (rng v)) by A3;
percases ( v . x is integer or v . x = +infty ) by Def1;
suppose v . x is integer ; ::_thesis: y is ext-integer
then  x <> 0. K by A1, Def8;
then consider r being Integer such that
A7: v . x = r * (least-positive (rng v)) by A1, Th36;
 (v . x) / (least-positive (rng v)) = r by A2, A7, XXREAL_3:88;
hence  y is ext-integer by A5, A3; ::_thesis: verum
end;
suppose v . x = +infty ; ::_thesis: y is ext-integer
hence  y is ext-integer by A5, A6, A2, XXREAL_3:83; ::_thesis: verum
end;
end;
end;
then reconsider f = f as e.i.-valued Function of K,ExtREAL by Def3;
 f is Valuation of K
proof
thus  K is having_valuation by A1; :: according to FVALUAT1:def_8 ::_thesis: ( 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 ) )
thus f . (0. K) = (v . (0. K)) / (least-positive (rng v)) by A3
.= +infty / (least-positive (rng v)) by A1, Def8
.= +infty by A2, XXREAL_3:83 ; ::_thesis: ( ( 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 ) )
thus  for a being Element of K st a <> 0. K holds
f . a in INT ::_thesis: ( ( 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 ) )
proof
let a be Element of K; ::_thesis: ( a <> 0. K implies f . a in INT )
assume  a <> 0. K ; ::_thesis: f . a in INT
then  v . a in INT by A1, Def8;
then reconsider va = v . a as Integer ;
f . a = (v . a) / (least-positive (rng v)) by A3
.= va / l1 by Lm2 ;
hence  f . a in INT by INT_1:def_2; ::_thesis: verum
end;
thus  for a, b being Element of K holds f . (a * b) = (f . a) + (f . b) ::_thesis: ( ( 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 ) )
proof
let a, b be Element of K; ::_thesis: f . (a * b) = (f . a) + (f . b)
thus f . (a * b) = (v . (a * b)) / (least-positive (rng v)) by A3
.= ((v . a) + (v . b)) / (least-positive (rng v)) by A1, Def8
.= ((v . a) / (least-positive (rng v))) + ((v . b) / (least-positive (rng v))) by A2, Th7
.= (f . a) + ((v . b) / (least-positive (rng v))) by A3
.= (f . a) + (f . b) by A3 ; ::_thesis: verum
end;
thus  for a being Element of K st 0 <= f . a holds
0 <= f . ((1. K) + a) ::_thesis: ex a being Element of K st
( f . a <> 0 & f . a <> +infty )
proof
let a be Element of K; ::_thesis: ( 0 <= f . a implies 0 <= f . ((1. K) + a) )
assume A8: 0 <= f . a ; ::_thesis: 0 <= f . ((1. K) + a)
A9: f . ((1. K) + a) = (v . ((1. K) + a)) / (least-positive (rng v)) by A3;
 f . a = (v . a) / (least-positive (rng v)) by A3;
then  0 <= v . a by A2, A8, Th5;
then  0 <= v . ((1. K) + a) by A1, Def8;
hence  0 <= f . ((1. K) + a) by A9; ::_thesis: verum
end;
consider a being Element of K such that
A10: v . a <> 0 and
A11: v . a <> +infty by A1, Def8;
take  a ; ::_thesis: ( f . a <> 0 & f . a <> +infty )
A12: f . a = (v . a) / (least-positive (rng v)) by A3;
hence  f . a <> 0 by A2, A10, Th9; ::_thesis: f . a <> +infty
reconsider va = v . a as Integer by A11, Def1;
A13: va in REAL by XREAL_0:def_1;
 least-positive (rng v) in REAL by A1, Lm7;
hence  f . a <> +infty by A12, A13; ::_thesis: verum
end;
then reconsider f = f as Valuation of K ;
take  f ; ::_thesis: for a being Element of K holds v . a = (f . a) * (least-positive (rng v))
let a be Element of K; ::_thesis: v . a = (f . a) * (least-positive (rng v))
thus v . a = ((v . a) / (least-positive (rng v))) * (least-positive (rng v)) by A2, Th8
.= (f . a) * (least-positive (rng v)) by A3 ; ::_thesis: verum
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
let f, g be Valuation of K; ::_thesis: ( ( for a being Element of K holds v . a = (f . a) * (least-positive (rng v)) ) & ( for a being Element of K holds v . a = (g . a) * (least-positive (rng v)) ) implies f = g )
assume that
A14: for a being Element of K holds v . a = (f . a) * (least-positive (rng v)) and
A15: for a being Element of K holds v . a = (g . a) * (least-positive (rng v)) ; ::_thesis: f = g
A16: least-positive (rng v) in REAL by A1, Lm7;
let x be Element of K; :: according to FUNCT_2:def_8 ::_thesis: f . x = g . x
(f . x) * (least-positive (rng v)) = v . x by A14
.= (g . x) * (least-positive (rng v)) by A15 ;
hence  f . x = g . x by A16, XXREAL_3:68; ::_thesis: verum
end;
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 )
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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 )
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation holds
( v . a = 0 iff (normal-valuation v) . a = 0 )
let v be Valuation of K; ::_thesis: ( K is having_valuation implies ( v . a = 0 iff (normal-valuation v) . a = 0 ) )
assume  K is having_valuation ; ::_thesis: ( v . a = 0 iff (normal-valuation v) . a = 0 )
then  v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by Def10;
hence  ( v . a = 0 iff (normal-valuation v) . a = 0 ) ; ::_thesis: verum
end;

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 )
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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 )
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation holds
( v . a = +infty iff (normal-valuation v) . a = +infty )
let v be Valuation of K; ::_thesis: ( K is having_valuation implies ( v . a = +infty iff (normal-valuation v) . a = +infty ) )
assume A1: K is having_valuation ; ::_thesis: ( v . a = +infty iff (normal-valuation v) . a = +infty )
set f = normal-valuation v;
set l = least-positive (rng v);
A2: v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by A1, Def10;
 least-positive (rng v) is integer by A1, Th35;
hence  ( v . a = +infty implies (normal-valuation v) . a = +infty ) by A2, XXREAL_3:69; ::_thesis: ( (normal-valuation v) . a = +infty implies v . a = +infty )
thus  ( (normal-valuation v) . a = +infty implies v . a = +infty ) by A2, XXREAL_3:def_5; ::_thesis: verum
end;

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 )
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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 )
let a, b be Element of K; ::_thesis: 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 )
let v be Valuation of K; ::_thesis: ( K is having_valuation implies ( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b ) )
set f = normal-valuation v;
set l = least-positive (rng v);
assume A1: K is having_valuation ; ::_thesis: ( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b )
then A2: least-positive (rng v) in REAL by Lm7;
 ( v . a = ((normal-valuation v) . a) * (least-positive (rng v)) & v . b = ((normal-valuation v) . b) * (least-positive (rng v)) ) by A1, Def10;
hence  ( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b ) by A2, XXREAL_3:68; ::_thesis: verum
end;

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 )
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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 )
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation holds
( v . a is positive iff (normal-valuation v) . a is positive )
let v be Valuation of K; ::_thesis: ( K is having_valuation implies ( v . a is positive iff (normal-valuation v) . a is positive ) )
set f = normal-valuation v;
set l = least-positive (rng v);
assume A1: K is having_valuation ; ::_thesis: ( v . a is positive iff (normal-valuation v) . a is positive )
then A2: v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by Def10;
reconsider l1 = least-positive (rng v) as Real by A1, Lm7;
hereby  ::_thesis: ( (normal-valuation v) . a is positive implies v . a is positive )
assume A3: v . a is positive ; ::_thesis: (normal-valuation v) . a is positive
percases ( v . a is real positive number or v . a = +infty ) by A3, XXREAL_3:1;
suppose v . a is real positive number ; ::_thesis: (normal-valuation v) . a is positive
then reconsider va = v . a as real positive number ;
A4: va in REAL by XREAL_0:def_1;
then  (normal-valuation v) . a in REAL by A2, XXREAL_3:73;
then consider c, b being complex number  such that
A5: ( (normal-valuation v) . a = c & l1 = b & ((normal-valuation v) . a) * l1 = c * b ) by XXREAL_3:def_5;
reconsider c = c as Real by A4, A5, A2, XXREAL_3:73;
 va = c * b by A1, Def10, A5;
hence  (normal-valuation v) . a is positive by A5; ::_thesis: verum
end;
suppose v . a = +infty ; ::_thesis: (normal-valuation v) . a is positive
hence  (normal-valuation v) . a is positive by A1, Th38; ::_thesis: verum
end;
end;
end;
assume A6: (normal-valuation v) . a is positive ; ::_thesis: v . a is positive
percases ( (normal-valuation v) . a is real positive number or (normal-valuation v) . a = +infty ) by A6, XXREAL_3:1;
suppose (normal-valuation v) . a is real positive number ; ::_thesis: v . a is positive
then reconsider fa = (normal-valuation v) . a as real positive number ;
 v . a = fa * l1 by A2, XXREAL_3:def_5;
hence  v . a is positive ; ::_thesis: verum
end;
suppose (normal-valuation v) . a = +infty ; ::_thesis: v . a is positive
hence  v . a is positive by A1, Th38; ::_thesis: verum
end;
end;
end;

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 )
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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 )
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation holds
( 0 <= v . a iff 0 <= (normal-valuation v) . a )
let v be Valuation of K; ::_thesis: ( K is having_valuation implies ( 0 <= v . a iff 0 <= (normal-valuation v) . a ) )
set f = normal-valuation v;
assume A1: K is having_valuation ; ::_thesis: ( 0 <= v . a iff 0 <= (normal-valuation v) . a )
hereby  ::_thesis: ( 0 <= (normal-valuation v) . a implies 0 <= v . a )
assume  0 <= v . a ; ::_thesis: 0 <= (normal-valuation v) . a
then  ( v . a is positive or 0 = v . a ) ;
hence  0 <= (normal-valuation v) . a by A1, Th40, Th37; ::_thesis: verum
end;
assume  0 <= (normal-valuation v) . a ; ::_thesis: 0 <= v . a
then  ( (normal-valuation v) . a is positive or 0 = (normal-valuation v) . a ) ;
hence  0 <= v . a by A1, Th40, Th37; ::_thesis: verum
end;

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 )
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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 )
let a be Element of K; ::_thesis: 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 )
let v be Valuation of K; ::_thesis: ( K is having_valuation implies ( not v . a is negative iff not (normal-valuation v) . a is negative ) )
set f = normal-valuation v;
set l = least-positive (rng v);
assume A1: K is having_valuation ; ::_thesis: ( not v . a is negative iff not (normal-valuation v) . a is negative )
then A2: v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by Def10;
percases ( v . a is empty or (normal-valuation v) . a is empty or ( not v . a is empty & not (normal-valuation v) . a is empty ) ) ;
suppose ( v . a is empty or (normal-valuation v) . a is empty ) ; ::_thesis: ( not v . a is negative iff not (normal-valuation v) . a is negative )
thus  ( not v . a is negative iff not (normal-valuation v) . a is negative ) by A2; ::_thesis: verum
end;
supposethat A3: not v . a is empty and
A4: not (normal-valuation v) . a is empty ; ::_thesis: ( not v . a is negative iff not (normal-valuation v) . a is negative )
thus  ( not v . a is negative implies not (normal-valuation v) . a is negative ) by A1, A3, Th40; ::_thesis: ( not (normal-valuation v) . a is negative implies not v . a is negative )
thus  ( not (normal-valuation v) . a is negative implies not v . a is negative ) by A4, A1, Th40; ::_thesis: verum
end;
end;
end;

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
proof
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
(normal-valuation v) . (Pgenerator v) = 1
let v be Valuation of K; ::_thesis: ( K is having_valuation implies (normal-valuation v) . (Pgenerator v) = 1 )
set f = normal-valuation v;
set a = Pgenerator v;
set l = least-positive (rng v);
assume A1: K is having_valuation ; ::_thesis: (normal-valuation v) . (Pgenerator v) = 1
then A2: v . (Pgenerator v) = ((normal-valuation v) . (Pgenerator v)) * (least-positive (rng v)) by Def10;
A3: least-positive (rng v) is Real by A1, Lm7;
 least-positive (rng v) in rng v by A1, Lm6;
then  {(least-positive (rng v))} c= rng v by ZFMISC_1:31;
then A4: not v " {(least-positive (rng v))} is empty by RELAT_1:139;
 Pgenerator v = the Element of v " {(least-positive (rng v))} by A1, Def9;
then  v . (Pgenerator v) in {(least-positive (rng v))} by A4, FUNCT_1:def_7;
then v . (Pgenerator v) = least-positive (rng v) by TARSKI:def_1
.= 1 * (least-positive (rng v)) by XXREAL_3:81 ;
hence  (normal-valuation v) . (Pgenerator v) = 1 by A2, A3, XXREAL_3:68; ::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & 0 <= v . a holds
(normal-valuation v) . a <= v . a
let v be Valuation of K; ::_thesis: ( K is having_valuation & 0 <= v . a implies (normal-valuation v) . a <= v . a )
set f = normal-valuation v;
set l = least-positive (rng v);
assume A1: K is having_valuation ; ::_thesis: ( not 0 <= v . a or (normal-valuation v) . a <= v . a )
then A2: v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by Def10;
assume  0 <= v . a ; ::_thesis: (normal-valuation v) . a <= v . a
then A3: 0 <= (normal-valuation v) . a by A1, Th41;
 0. + 1 <= least-positive (rng v) by Th10;
then  ((normal-valuation v) . a) * 1 <= ((normal-valuation v) . a) * (least-positive (rng v)) by A3, Th3;
hence  (normal-valuation v) . a <= v . a by A2, XXREAL_3:81; ::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & v . a = 1 holds
normal-valuation v = v
let v be Valuation of K; ::_thesis: ( K is having_valuation & v . a = 1 implies normal-valuation v = v )
set f = normal-valuation v;
assume that
A1: K is having_valuation and
A2: v . a = 1 ; ::_thesis: normal-valuation v = v
let a be Element of K; :: according to FUNCT_2:def_8 ::_thesis: (normal-valuation v) . a = v . a
thus v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by A1, Def10
.= ((normal-valuation v) . a) * 1 by A2, Th34
.= (normal-valuation v) . a by XXREAL_3:81 ; ::_thesis: verum
end;

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
proof
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
normal-valuation (normal-valuation v) = normal-valuation v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies normal-valuation (normal-valuation v) = normal-valuation v )
assume A1: K is having_valuation ; ::_thesis: normal-valuation (normal-valuation v) = normal-valuation v
set f = normal-valuation v;
set g = normal-valuation (normal-valuation v);
let a be Element of K; :: according to FUNCT_2:def_8 ::_thesis: (normal-valuation (normal-valuation v)) . a = (normal-valuation v) . a
set k = least-positive (rng (normal-valuation v));
A2: (normal-valuation v) . a = ((normal-valuation (normal-valuation v)) . a) * (least-positive (rng (normal-valuation v))) by A1, Def10;
 (normal-valuation v) . (Pgenerator v) = 1 by A1, Th43;
then  least-positive (rng (normal-valuation v)) = 1 by Th34;
hence  (normal-valuation (normal-valuation v)) . a = (normal-valuation v) . a by A2, XXREAL_3:81; ::_thesis: verum
end;

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 )
proof
let K be non empty doubleLoopStr ; ::_thesis: for v being Valuation of K
for a being Element of K holds
( a in NonNegElements v iff 0 <= v . a )
let v be Valuation of K; ::_thesis: for a being Element of K holds
( a in NonNegElements v iff 0 <= v . a )
let a be Element of K; ::_thesis: ( a in NonNegElements v iff 0 <= v . a )
hereby  ::_thesis: ( 0 <= v . a implies a in NonNegElements v )
assume  a in NonNegElements v ; ::_thesis: 0 <= v . a
then  ex x being Element of K st
( a = x & 0 <= v . x ) ;
hence  0 <= v . a ; ::_thesis: verum
end;
thus  ( 0 <= v . a implies a in NonNegElements v ) ; ::_thesis: verum
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
let K be non empty doubleLoopStr ; ::_thesis: for v being Valuation of K holds NonNegElements v c= the carrier of K
let v be Valuation of K; ::_thesis: NonNegElements v c= the carrier of K
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in NonNegElements v or a in the carrier of K )
assume  a in NonNegElements v ; ::_thesis: a in the carrier of K
then  ex x being Element of K st
( a = x & 0 <= v . x ) ;
hence  a in the carrier of K ; ::_thesis: verum
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
let K be non empty doubleLoopStr ; ::_thesis: for v being Valuation of K st K is having_valuation holds
0. K in NonNegElements v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies 0. K in NonNegElements v )
assume  K is having_valuation ; ::_thesis: 0. K in NonNegElements v
then  v . (0. K) = +infty by Def8;
hence  0. K in NonNegElements v ; ::_thesis: verum
end;

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
proof
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
1. K in NonNegElements v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies 1. K in NonNegElements v )
assume  K is having_valuation ; ::_thesis: 1. K in NonNegElements v
then  v . (1. K) = 0 by Th17;
hence  1. K in NonNegElements v ; ::_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 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 )
proof
set c = NonNegElements v;
set a = the addF of K | [:(NonNegElements v),(NonNegElements v):];
set m = the multF of K | [:(NonNegElements v),(NonNegElements v):];
set j = 1. K;
set z = 0. K;
A1: NonNegElements v c= the carrier of K by Th48;
now__::_thesis:_for_x_being_set_st_x_in_[:(NonNegElements_v),(NonNegElements_v):]_holds_
the_addF_of_K_._x_in_NonNegElements_v
let x be set ; ::_thesis: ( x in [:(NonNegElements v),(NonNegElements v):] implies the addF of K . x in NonNegElements v )
assume A2: x in [:(NonNegElements v),(NonNegElements v):] ; ::_thesis: the addF of K . x in NonNegElements v
set q = the addF of K . x;
consider x1, x2 being set  such that
A3: x1 in NonNegElements v and
A4: x2 in NonNegElements v and
A5: x = [x1,x2] by A2, ZFMISC_1:def_2;
consider y1 being Element of K such that
A6: y1 = x1 and
A7: 0 <= v . y1 by A3;
consider y2 being Element of K such that
A8: y2 = x2 and
A9: 0 <= v . y2 by A4;
A10: min ((v . y1),(v . y2)) <= v . (y1 + y2) by B1, Th27;
 0 <= min ((v . y1),(v . y2)) by A7, A9, XXREAL_0:20;
hence  the addF of K . x in NonNegElements v by A5, A6, A10, A8; ::_thesis: verum
end;
then reconsider ca = NonNegElements v as Preserv of the addF of K by A1, REALSET1:def_1;
 the addF of K || ca is BinOp of (NonNegElements v) ;
then reconsider a = the addF of K | [:(NonNegElements v),(NonNegElements v):] as BinOp of (NonNegElements v) ;
now__::_thesis:_for_x_being_set_st_x_in_[:(NonNegElements_v),(NonNegElements_v):]_holds_
the_multF_of_K_._x_in_NonNegElements_v
let x be set ; ::_thesis: ( x in [:(NonNegElements v),(NonNegElements v):] implies the multF of K . x in NonNegElements v )
assume A11: x in [:(NonNegElements v),(NonNegElements v):] ; ::_thesis: the multF of K . x in NonNegElements v
set q = the multF of K . x;
consider x1, x2 being set  such that
A12: x1 in NonNegElements v and
A13: x2 in NonNegElements v and
A14: x = [x1,x2] by A11, ZFMISC_1:def_2;
consider y1 being Element of K such that
A15: y1 = x1 and
A16: 0 <= v . y1 by A12;
consider y2 being Element of K such that
A17: y2 = x2 and
A18: 0 <= v . y2 by A13;
 0 + 0 <= (v . y1) + (v . y2) by A16, A18;
then  0 <= v . (y1 * y2) by B1, Def8;
hence  the multF of K . x in NonNegElements v by A14, A15, A17; ::_thesis: verum
end;
then reconsider cm = NonNegElements v as Preserv of the multF of K by A1, REALSET1:def_1;
 the multF of K || cm is BinOp of (NonNegElements v) ;
then reconsider m = the multF of K | [:(NonNegElements v),(NonNegElements v):] as BinOp of (NonNegElements v) ;
A19: v . (0. K) = +infty by B1, Def8;
reconsider j = 1. K, z = 0. K as Element of NonNegElements v by B1, Th49, Th50;
set R = doubleLoopStr(# (NonNegElements v),a,m,j,z #);
 z in NonNegElements v by A19;
then reconsider R = doubleLoopStr(# (NonNegElements v),a,m,j,z #) as non empty doubleLoopStr ;
A20: now__::_thesis:_for_x,_y_being_Element_of_R
for_x1,_y1_being_Element_of_K_st_x_=_x1_&_y_=_y1_holds_
x_+_y_=_x1_+_y1
let x, y be Element of R; ::_thesis: for x1, y1 being Element of K st x = x1 & y = y1 holds
x + y = x1 + y1
let x1, y1 be Element of K; ::_thesis: ( x = x1 & y = y1 implies x + y = x1 + y1 )
assume A21: ( x = x1 & y = y1 ) ; ::_thesis: x + y = x1 + y1
 [x,y] in [:(NonNegElements v),(NonNegElements v):] ;
hence  x + y = x1 + y1 by A21, FUNCT_1:49; ::_thesis: verum
end;
A22: now__::_thesis:_for_x,_y_being_Element_of_R
for_x1,_y1_being_Element_of_K_st_x_=_x1_&_y_=_y1_holds_
x_*_y_=_x1_*_y1
let x, y be Element of R; ::_thesis: for x1, y1 being Element of K st x = x1 & y = y1 holds
x * y = x1 * y1
let x1, y1 be Element of K; ::_thesis: ( x = x1 & y = y1 implies x * y = x1 * y1 )
assume A23: ( x = x1 & y = y1 ) ; ::_thesis: x * y = x1 * y1
 [x,y] in [:(NonNegElements v),(NonNegElements v):] ;
hence  x * y = x1 * y1 by A23, FUNCT_1:49; ::_thesis: verum
end;
A24: now__::_thesis:_for_x,_e_being_Element_of_R_st_e_=_j_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let x, e be Element of R; ::_thesis: ( e = j implies ( x * e = x & e * x = x ) )
assume A25: e = j ; ::_thesis: ( x * e = x & e * x = x )
 ( x in NonNegElements v & e in NonNegElements v ) ;
then reconsider x1 = x, e1 = e as Element of K by A1;
thus x * e = x1 * e1 by A22
.= x by A25, VECTSP_1:def_4 ; ::_thesis: e * x = x
thus e * x = e1 * x1 by A22
.= x by A25, VECTSP_1:def_4 ; ::_thesis: verum
end;
 R is well-unital
proof
let x be Element of R; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. R) = x & (1. R) * x = x )
thus  ( x * (1. R) = x & (1. R) * x = x ) by A24; ::_thesis: verum
end;
then reconsider R = R as non empty well-unital doubleLoopStr ;
 ( R is Abelian & R is add-associative & R is right_zeroed & R is right_complementable & R is commutative & R is associative & R is distributive & not R is degenerated )
proof
hereby  :: according to RLVECT_1:def_2 ::_thesis: ( R is add-associative & R is right_zeroed & R is right_complementable & R is commutative & R is associative & R is distributive & not R is degenerated )
let x, y be Element of R; ::_thesis: x + y = y + x
 ( x in NonNegElements v & y in NonNegElements v ) ;
then reconsider x1 = x, y1 = y as Element of K by A1;
thus x + y = x1 + y1 by A20
.= y + x by A20 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( R is right_zeroed & R is right_complementable & R is commutative & R is associative & R is distributive & not R is degenerated )
let x, y, z be Element of R; ::_thesis: (x + y) + z = x + (y + z)
 ( x in NonNegElements v & y in NonNegElements v & z in NonNegElements v ) ;
then reconsider x1 = x, y1 = y, z1 = z as Element of K by A1;
A26: y + z = y1 + z1 by A20;
 x + y = x1 + y1 by A20;
hence (x + y) + z = (x1 + y1) + z1 by A20
.= x1 + (y1 + z1) by RLVECT_1:def_3
.= x + (y + z) by A26, A20 ;
::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: ( R is right_complementable & R is commutative & R is associative & R is distributive & not R is degenerated )
let x be Element of R; ::_thesis: x + (0. R) = x
 x in NonNegElements v ;
then reconsider x1 = x as Element of K by A1;
thus x + (0. R) = x1 + (0. K) by A20
.= x by RLVECT_1:def_4 ; ::_thesis: verum
end;
thus  R is right_complementable ::_thesis: ( R is commutative & R is associative & R is distributive & not R is degenerated )
proof
let x be Element of R; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
 x in NonNegElements v ;
then reconsider x1 = x as Element of K by A1;
consider w1 being Element of K such that
A27: x1 + w1 = 0. K by ALGSTR_0:def_11;
A28: v . (x1 + w1) = +infty by B1, A27, Def8;
percases ( v . w1 < v . x1 or v . x1 <= v . w1 ) ;
suppose v . w1 < v . x1 ; ::_thesis: x is right_complementable
then  v . w1 = v . (w1 + x1) by B1, Th28;
then reconsider w = w1 as Element of R by A28, Th47;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: x + w = 0. R
thus  x + w = 0. R by A27, A20; ::_thesis: verum
end;
supposeA29: v . x1 <= v . w1 ; ::_thesis: x is right_complementable
 0 <= v . x1 by Th47;
then reconsider w = w1 as Element of R by A29, Th47;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: x + w = 0. R
thus  x + w = 0. R by A27, A20; ::_thesis: verum
end;
end;
end;
hereby  :: according to GROUP_1:def_12 ::_thesis: ( R is associative & R is distributive & not R is degenerated )
let x, y be Element of R; ::_thesis: x * y = y * x
 ( x in NonNegElements v & y in NonNegElements v ) ;
then reconsider x1 = x, y1 = y as Element of K by A1;
thus x * y = x1 * y1 by A22
.= y * x by A22 ; ::_thesis: verum
end;
hereby  :: according to GROUP_1:def_3 ::_thesis: ( R is distributive & not R is degenerated )
let x, y, z be Element of R; ::_thesis: (x * y) * z = x * (y * z)
 ( x in NonNegElements v & y in NonNegElements v & z in NonNegElements v ) ;
then reconsider x1 = x, y1 = y, z1 = z as Element of K by A1;
A30: y * z = y1 * z1 by A22;
 x * y = x1 * y1 by A22;
hence (x * y) * z = (x1 * y1) * z1 by A22
.= x1 * (y1 * z1) by GROUP_1:def_3
.= x * (y * z) by A30, A22 ;
::_thesis: verum
end;
hereby  :: according to VECTSP_1:def_7 ::_thesis: not R is degenerated
let x, y, z be Element of R; ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
 ( x in NonNegElements v & y in NonNegElements v & z in NonNegElements v ) ;
then reconsider x1 = x, y1 = y, z1 = z as Element of K by A1;
A31: y + z = y1 + z1 by A20;
A32: x * y = x1 * y1 by A22;
A33: x * z = x1 * z1 by A22;
A34: y * x = y1 * x1 by A22;
A35: z * x = z1 * x1 by A22;
thus x * (y + z) = x1 * (y1 + z1) by A31, A22
.= (x1 * y1) + (x1 * z1) by VECTSP_1:def_2
.= (x * y) + (x * z) by A20, A32, A33 ; ::_thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (y1 + z1) * x1 by A31, A22
.= (y1 * x1) + (z1 * x1) by VECTSP_1:def_2
.= (y * x) + (z * x) by A20, A34, A35 ; ::_thesis: verum
end;
thus  0. R <> 1. R ; :: according to STRUCT_0:def_8 ::_thesis: verum
end;
hence  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 ) ; ::_thesis: verum
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 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
proof
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
for x being Element of (ValuatRing v) holds x is Element of K
let v be Valuation of K; ::_thesis: ( K is having_valuation implies for x being Element of (ValuatRing v) holds x is Element of K )
assume A1: K is having_valuation ; ::_thesis: for x being Element of (ValuatRing v) holds x is Element of K
let x be Element of (ValuatRing v); ::_thesis: x is Element of K
 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  x is Element of K ; ::_thesis: verum
end;

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) )
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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) )
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation holds
( 0 <= v . a iff a is Element of (ValuatRing v) )
let v be Valuation of K; ::_thesis: ( K is having_valuation implies ( 0 <= v . a iff a is Element of (ValuatRing v) ) )
assume  K is having_valuation ; ::_thesis: ( 0 <= v . a iff a is Element of (ValuatRing v) )
then  the carrier of (ValuatRing v) = NonNegElements v by Def12;
hence  ( 0 <= v . a iff a is Element of (ValuatRing v) ) by Th47; ::_thesis: verum
end;

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
proof
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
for S being Subset of (ValuatRing v) holds 0 is LowerBound of v .: S
let v be Valuation of K; ::_thesis: ( K is having_valuation implies for S being Subset of (ValuatRing v) holds 0 is LowerBound of v .: S )
assume A1: K is having_valuation ; ::_thesis: for S being Subset of (ValuatRing v) holds 0 is LowerBound of v .: S
let S be Subset of (ValuatRing v); ::_thesis: 0 is LowerBound of v .: S
let x be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not x in v .: S or 0 <= x )
assume  x in v .: S ; ::_thesis: 0 <= x
then A2: ex c being 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  0 <= x by A2, Th47; ::_thesis: verum
end;

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
proof
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
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
let v be Valuation of K; ::_thesis: ( K is having_valuation implies 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 )
set R = ValuatRing v;
set c = NonNegElements v;
assume A1: K is having_valuation ; ::_thesis: 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
let x, y be Element of K; ::_thesis: for x1, y1 being Element of (ValuatRing v) st x = x1 & y = y1 holds
x + y = x1 + y1
let x1, y1 be Element of (ValuatRing v); ::_thesis: ( x = x1 & y = y1 implies x + y = x1 + y1 )
assume A2: ( x = x1 & y = y1 ) ; ::_thesis: x + y = x1 + y1
A3: NonNegElements v = the carrier of (ValuatRing v) by A1, Def12;
A4: the addF of (ValuatRing v) = the addF of K | [:(NonNegElements v),(NonNegElements v):] by A1, Def12;
thus x1 + y1 = the addF of (ValuatRing v) . [x1,y1]
.= x + y by A3, A4, A2, FUNCT_1:49 ; ::_thesis: verum
end;

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
proof
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
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
let v be Valuation of K; ::_thesis: ( K is having_valuation implies 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 )
set R = ValuatRing v;
set c = NonNegElements v;
assume A1: K is having_valuation ; ::_thesis: 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
let x, y be Element of K; ::_thesis: for x1, y1 being Element of (ValuatRing v) st x = x1 & y = y1 holds
x * y = x1 * y1
let x1, y1 be Element of (ValuatRing v); ::_thesis: ( x = x1 & y = y1 implies x * y = x1 * y1 )
assume A2: ( x = x1 & y = y1 ) ; ::_thesis: x * y = x1 * y1
A3: NonNegElements v = the carrier of (ValuatRing v) by A1, Def12;
A4: the multF of (ValuatRing v) = the multF of K | [:(NonNegElements v),(NonNegElements v):] by A1, Def12;
thus x1 * y1 = the multF of (ValuatRing v) . [x1,y1]
.= x * y by A3, A4, A2, FUNCT_1:49 ; ::_thesis: verum
end;

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
proof
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
for x being Element of K
for y being Element of (ValuatRing v) st x = y holds
- x = - y
let v be Valuation of K; ::_thesis: ( K is having_valuation implies for x being Element of K
for y being Element of (ValuatRing v) st x = y holds
- x = - y )
set R = ValuatRing v;
set c = NonNegElements v;
assume A1: K is having_valuation ; ::_thesis: for x being Element of K
for y being Element of (ValuatRing v) st x = y holds
- x = - y
let x be Element of K; ::_thesis: for y being Element of (ValuatRing v) st x = y holds
- x = - y
let y be Element of (ValuatRing v); ::_thesis: ( x = y implies - x = - y )
assume A2: x = y ; ::_thesis: - x = - y
A3: 0 <= v . y by A1, A2, Th52;
 v . (- x) = v . x by A1, Th20;
then reconsider x1 = - x as Element of (ValuatRing v) 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  - x = - y by RLVECT_1:def_10; ::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: for a, b being Element of K st a <> 0. K holds
(a ") * (a * b) = b
let a, b be Element of K; ::_thesis: ( a <> 0. K implies (a ") * (a * b) = b )
assume A1: a <> 0. K ; ::_thesis: (a ") * (a * b) = b
thus (a ") * (a * b) = ((a ") * a) * b by GROUP_1:def_3
.= (1. K) * b by A1, VECTSP_2:def_2
.= b by VECTSP_1:def_8 ; ::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: for x, v being Element of K st x <> 0. K holds
x * ((x ") * v) = v
let x, v be Element of K; ::_thesis: ( x <> 0. K implies x * ((x ") * v) = v )
assume A1: x <> 0. K ; ::_thesis: x * ((x ") * v) = v
thus x * ((x ") * v) = (x * (x ")) * v by GROUP_1:def_3
.= (1. K) * v by A1, VECTSP_2:def_2
.= v by VECTSP_1:def_8 ; ::_thesis: verum
end;

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
proof
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
ValuatRing v is domRing-like
let v be Valuation of K; ::_thesis: ( K is having_valuation implies ValuatRing v is domRing-like )
set R = ValuatRing v;
assume A1: K is having_valuation ; ::_thesis: ValuatRing v is domRing-like
let x, y be Element of (ValuatRing v); :: according to VECTSP_2:def_1 ::_thesis: ( not x * y = 0. (ValuatRing v) or x = 0. (ValuatRing v) or y = 0. (ValuatRing v) )
assume that
A2: x * y = 0. (ValuatRing v) and
A3: x <> 0. (ValuatRing v) ; ::_thesis: y = 0. (ValuatRing v)
reconsider x1 = x, y1 = y as Element of K by A1, Th51;
A4: 0. (ValuatRing v) = 0. K by A1, Def12;
A5: x1 * y1 = x * y by A1, Th55;
y1 = (x1 ") * (x1 * y1) by A3, A4, Lm8
.= 0. K by A2, A4, A5, VECTSP_1:6 ;
hence  y = 0. (ValuatRing v) by A1, Def12; ::_thesis: verum
end;

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)
proof
let n be Nat; ::_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
for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n)
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
for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n)
let v be Valuation of K; ::_thesis: ( K is having_valuation implies for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n) )
set R = ValuatRing v;
assume A1: K is having_valuation ; ::_thesis: for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n)
let y be Element of (ValuatRing v); ::_thesis: (power K) . (y,n) = (power (ValuatRing v)) . (y,n)
defpred S1[ 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 (ValuatRing v)) . (y,0) = 1_ (ValuatRing v) ) by GROUP_1:def_7;
then A2: S1[ 0 ] by A1, Def12;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
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  S1[n + 1] by A1, A4, Th55; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A2, A3);
hence  (power K) . (y,n) = (power (ValuatRing v)) . (y,n) ; ::_thesis: verum
end;

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)
proof
set R = ValuatRing v;
set I =  {  x where x is Element of K : 0 < v . x  }  ;
A2: the carrier of (ValuatRing v) = NonNegElements v by A1, Def12;
  {  x where x is Element of K : 0 < v . x  }  c= the carrier of (ValuatRing v)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  x where x is Element of K : 0 < v . x  }  or a in the carrier of (ValuatRing v) )
assume  a in  {  x where x is Element of K : 0 < v . x  }  ; ::_thesis: a in the carrier of (ValuatRing v)
then  ex x being Element of K st
( a = x & 0 < v . x ) ;
hence  a in the carrier of (ValuatRing v) by A2; ::_thesis: verum
end;
then reconsider I =  {  x where x is Element of K : 0 < v . x  }  as non empty Subset of (ValuatRing v) by A1, Lm10;
A3: the carrier of (ValuatRing v) c= the carrier of K by A2, Th48;
 ( I is add-closed & I is left-ideal & I is right-ideal )
proof
hereby  :: according to IDEAL_1:def_1 ::_thesis: ( I is left-ideal & I is right-ideal )
let x, y be Element of (ValuatRing v); ::_thesis: ( x in I & y in I implies x + y in I )
assume  x in I ; ::_thesis: ( y in I implies x + y in I )
then consider x1 being Element of K such that
A4: x1 = x and
A5: 0 < v . x1 ;
assume  y in I ; ::_thesis: x + y in I
then consider y1 being 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; ::_thesis: verum
end;
hereby  :: according to IDEAL_1:def_2 ::_thesis: I is right-ideal
let p, x be Element of (ValuatRing v); ::_thesis: ( x in I implies p * x in I )
assume  x in I ; ::_thesis: p * x in I
then consider x1 being Element of K such that
A10: x1 = x and
A11: 0 < v . x1 ;
 p in the carrier of (ValuatRing v) ;
then 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; ::_thesis: verum
end;
let p, x be Element of (ValuatRing v); :: according to IDEAL_1:def_3 ::_thesis: ( not x in I or x * p in I )
assume  x in I ; ::_thesis: x * p in I
then consider x1 being Element of K such that
A14: x1 = x and
A15: 0 < v . x1 ;
 p in the carrier of (ValuatRing v) ;
then 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; ::_thesis: verum
end;
hence   {  x where x is Element of K : 0 < v . x  }  is Ideal of (ValuatRing v) ; ::_thesis: verum
end;
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 )
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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 )
let a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation holds
( a in vp v iff 0 < v . a )
let v be Valuation of K; ::_thesis: ( K is having_valuation implies ( a in vp v iff 0 < v . a ) )
assume  K is having_valuation ; ::_thesis: ( a in vp v iff 0 < v . a )
then A1: vp v =  {  x where x is Element of K : 0 < v . x  }  by Def13;
hereby  ::_thesis: ( 0 < v . a implies a in vp v )
assume  a in vp v ; ::_thesis: 0 < v . a
then  ex b being Element of K st
( b = a & 0 < v . b ) by A1;
hence  0 < v . a ; ::_thesis: verum
end;
thus  ( 0 < v . a implies a in vp v ) by A1; ::_thesis: verum
end;

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
proof
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 vp v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies 0. K in vp v )
assume A1: K is having_valuation ; ::_thesis: 0. K in vp v
then  vp v =  {  x where x is Element of K : 0 < v . x  }  by Def13;
hence  0. K in vp v by A1, Lm10; ::_thesis: verum
end;

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
proof
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
not 1. K in vp v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies not 1. K in vp v )
assume A1: K is having_valuation ; ::_thesis: not 1. K in vp v
then A2: vp v =  {  x where x is Element of K : 0 < v . x  }  by Def13;
assume  1. K in vp v ; ::_thesis: contradiction
then  ex x being Element of K st
( x = 1. K & 0 < v . x ) by A2;
hence  contradiction by A1, Th17; ::_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;
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
 (v " {(inf (v .: S))}) /\ S c= NonNegElements v
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (v " {(inf (v .: S))}) /\ S or a in NonNegElements v )
assume A3: a in (v " {(inf (v .: S))}) /\ S ; ::_thesis: a in NonNegElements v
then A4: a in v " {(inf (v .: S))} by XBOOLE_0:def_4;
reconsider a = 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  a in NonNegElements v by A5; ::_thesis: verum
end;
hence  (v " {(inf (v .: S))}) /\ S is Subset of (ValuatRing v) by A1, Def12; ::_thesis: verum
end;
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
proof
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
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
let v be Valuation of K; ::_thesis: 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
let S be non empty Subset of K; ::_thesis: ( K is having_valuation & S is Subset of (ValuatRing v) implies min (S,v) c= S )
assume  ( K is having_valuation & S is Subset of (ValuatRing v) ) ; ::_thesis: min (S,v) c= S
then  min (S,v) = (v " {(inf (v .: S))}) /\ S by Def14;
hence  min (S,v) c= S by XBOOLE_1:17; ::_thesis: verum
end;

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 ) ) )
proof
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
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 ) ) )
let v be Valuation of K; ::_thesis: 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 ) ) )
let S be non empty Subset of K; ::_thesis: ( K is having_valuation & S is Subset of (ValuatRing v) implies 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 ) ) ) )
assume A1: K is having_valuation ; ::_thesis: ( not S is Subset of (ValuatRing v) or 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 ) ) ) )
assume A2: S is Subset of (ValuatRing v) ; ::_thesis: 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 ) ) )
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; ::_thesis: ( x in min (S,v) iff ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) ) )
hereby  ::_thesis: ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) implies x in min (S,v) )
assume A5: x in min (S,v) ; ::_thesis: ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) )
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; ::_thesis: for y being Element of K st y in S holds
v . x <= v . y
let y be Element of K; ::_thesis: ( y in S implies v . x <= v . y )
assume  y in S ; ::_thesis: v . x <= v . y
hence  v . x <= v . y by A6, A4, FUNCT_2:35, XXREAL_2:def_2; ::_thesis: verum
end;
assume that
A7: x in S and
A8: for y being Element of K st y in S holds
v . x <= v . y ; ::_thesis: x in min (S,v)
A9: v . x is LowerBound of v .: S
proof
let a be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not a in v .: S or v . x <= a )
assume  a in v .: S ; ::_thesis: v . x <= a
then  ex y being Element of K st
( y in S & a = v . y ) by FUNCT_2:65;
hence  v . x <= a by A8; ::_thesis: verum
end;
 for y being 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; ::_thesis: verum
end;

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
proof
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
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
let v be Valuation of K; ::_thesis: ( K is having_valuation implies 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 )
assume A1: K is having_valuation ; ::_thesis: 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
let I be non empty Subset of K; ::_thesis: for x being Element of (ValuatRing v) st I is Ideal of (ValuatRing v) & x in min (I,v) holds
I = {x} -Ideal
let x be Element of (ValuatRing v); ::_thesis: ( I is Ideal of (ValuatRing v) & x in min (I,v) implies I = {x} -Ideal )
assume A2: I is Ideal of (ValuatRing v) ; ::_thesis: ( not x in min (I,v) or I = {x} -Ideal )
assume A3: x in min (I,v) ; ::_thesis: I = {x} -Ideal
A4: min (I,v) c= I by A1, A2, Th64;
thus  I c= {x} -Ideal :: according to XBOOLE_0:def_10 ::_thesis: {x} -Ideal c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in I or a in {x} -Ideal )
assume A5: a in I ; ::_thesis: a in {x} -Ideal
then reconsider y = a as Element of (ValuatRing v) by A2;
reconsider x1 = x, y1 = y as Element of K by A1, Th51;
percases ( x <> 0. K or x = 0. (ValuatRing v) ) by A1, Def12;
supposeA6: x <> 0. K ; ::_thesis: a in {x} -Ideal
set r1 = y1 / x1;
 v . x1 <= v . y1 by A1, A2, A3, A5, Th65;
then  0 <= (v . y1) - (v . x1) by Lm5;
then  0 <= v . (y1 / x1) by A6, A1, Th22;
then reconsider r0 = y1 / x1 as Element of (ValuatRing v) by A1, Th52;
x1 * (y1 / x1) = y1 * ((x1 ") * x1) by GROUP_1:def_3
.= y1 * (1_ K) by A6, VECTSP_2:9
.= y1 by GROUP_1:def_4 ;
then A7: y = x * r0 by A1, Th55;
 {x} -Ideal =  {  (x * r) where r is Element of (ValuatRing v) : verum  }  by IDEAL_1:64;
hence  a in {x} -Ideal by A7; ::_thesis: verum
end;
supposeA8: x = 0. (ValuatRing v) ; ::_thesis: a in {x} -Ideal
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; ::_thesis: verum
end;
end;
end;
 {x} c= I by A4, A3, ZFMISC_1:31;
hence  {x} -Ideal c= I by A2, IDEAL_1:def_14; ::_thesis: verum
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
let R be non empty doubleLoopStr ; ::_thesis: for I being non empty add-closed Subset of R holds I is Preserv of the addF of R
let I be non empty add-closed Subset of R; ::_thesis: I is Preserv of the addF of R
let x be set ; :: according to REALSET1:def_1 ::_thesis: ( not x in [:I,I:] or the addF of R . x in I )
assume  x in [:I,I:] ; ::_thesis: the addF of R . x in I
then consider y, z being set  such that
A1: ( y in I & z in I ) and
A2: x = [y,z] by ZFMISC_1:def_2;
reconsider y = y, z = 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; ::_thesis: verum
end;

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 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
 ex S being strict Submodule of RightModule R st the carrier of S = P by Lm11;
hence  ex b1 being Submodule of RightModule R st the carrier of b1 = P ; ::_thesis: verum
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 V235() V236() V237() V238() for Submodule of P;
existence
 ex b1 being Submodule of P st b1 is strict
proof
consider S being strict Submodule of RightModule R such that
A1: the carrier of S = P by Lm11;
reconsider T = RightModStr(# the carrier of S, the addF of S, the ZeroF of S, the rmult of S #) as Submodule of P by A1, Def15;
take  T ; ::_thesis: T is strict
thus  T is strict ; ::_thesis: verum
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
let R be Ring; ::_thesis: 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 #)
let P be Ideal of R; ::_thesis: 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 #)
let M be Submodule of P; ::_thesis: 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 #)
A1: the carrier of M = P by Def15;
set V = RightModule R;
 ( 0. M = 0. (RightModule R) & the addF of M = the addF of (RightModule R) | [:P,P:] & the rmult of M = the rmult of (RightModule R) | [:P, the carrier of R:] ) by A1, RMOD_2:def_2;
hence  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 #) by Def15; ::_thesis: verum
end;

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 )
proof
set h = incl (M2,M1);
 the carrier of M2 c= the carrier of M1 by RMOD_2:def_2;
then A1: incl (M2,M1) = id the carrier of M2 by YELLOW_9:def_1;
thus  incl (M2,M1) is additive ::_thesis: incl (M2,M1) is scalar-linear
proof
let x, y be Element of M2; :: according to VECTSP_1:def_20 ::_thesis: (incl (M2,M1)) . (x + y) = ((incl (M2,M1)) . x) + ((incl (M2,M1)) . y)
 ( (incl (M2,M1)) . x = x & (incl (M2,M1)) . y = y & (incl (M2,M1)) . (x + y) = x + y ) by A1, FUNCT_1:17;
hence  (incl (M2,M1)) . (x + y) = ((incl (M2,M1)) . x) + ((incl (M2,M1)) . y) by RMOD_2:13; ::_thesis: verum
end;
let x be Element of M2; :: according to FVALUAT1:def_16 ::_thesis: for r being Element of R holds (incl (M2,M1)) . (x * r) = ((incl (M2,M1)) . x) * r
let r be Element of R; ::_thesis: (incl (M2,M1)) . (x * r) = ((incl (M2,M1)) . x) * r
 ( (incl (M2,M1)) . x = x & (incl (M2,M1)) . (x * r) = x * r ) by A1, FUNCT_1:17;
hence  (incl (M2,M1)) . (x * r) = ((incl (M2,M1)) . x) * r by RMOD_2:14; ::_thesis: verum
end;
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)
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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)
let b, a be Element of K; ::_thesis: for v being Valuation of K st K is having_valuation & b is Element of (ValuatRing v) holds
v . a <= (v . a) + (v . b)
let v be Valuation of K; ::_thesis: ( K is having_valuation & b is Element of (ValuatRing v) implies v . a <= (v . a) + (v . b) )
assume A1: K is having_valuation ; ::_thesis: ( not b is Element of (ValuatRing v) or v . a <= (v . a) + (v . b) )
assume  b is Element of (ValuatRing v) ; ::_thesis: v . a <= (v . a) + (v . b)
then  0 <= v . b by A1, Th52;
then  (v . a) + 0 <= (v . a) + (v . b) by XXREAL_3:35;
hence  v . a <= (v . a) + (v . b) by XXREAL_3:4; ::_thesis: verum
end;

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)
proof
let n be Nat; ::_thesis: 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)
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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)
let a be Element of K; ::_thesis: 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)
let v be Valuation of K; ::_thesis: ( K is having_valuation & a is Element of (ValuatRing v) implies (power K) . (a,n) is Element of (ValuatRing v) )
assume A1: K is having_valuation ; ::_thesis: ( not a is Element of (ValuatRing v) or (power K) . (a,n) is Element of (ValuatRing v) )
assume  a is Element of (ValuatRing v) ; ::_thesis: (power K) . (a,n) is Element of (ValuatRing v)
then reconsider y = a as Element of (ValuatRing v) ;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 (power (ValuatRing v)) . (y,n) is Element of (ValuatRing v) ;
hence  (power K) . (a,n) is Element of (ValuatRing v) by A1, Th60; ::_thesis: verum
end;

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
proof
let n be Nat; ::_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
for x being Element of (ValuatRing v) st x <> 0. K holds
(power K) . (x,n) <> 0. K
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
for x being Element of (ValuatRing v) st x <> 0. K holds
(power K) . (x,n) <> 0. K
let v be Valuation of K; ::_thesis: ( K is having_valuation implies for x being Element of (ValuatRing v) st x <> 0. K holds
(power K) . (x,n) <> 0. K )
assume A1: K is having_valuation ; ::_thesis: for x being Element of (ValuatRing v) st x <> 0. K holds
(power K) . (x,n) <> 0. K
let x be Element of (ValuatRing v); ::_thesis: ( x <> 0. K implies (power K) . (x,n) <> 0. K )
reconsider y = x as Element of K by A1, Th51;
 (power K) . (y,n) = y |^ n ;
hence  ( x <> 0. K implies (power K) . (x,n) <> 0. K ) by Th16; ::_thesis: verum
end;

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) )
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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) )
let a be Element of K; ::_thesis: 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) )
let v be Valuation of K; ::_thesis: ( K is having_valuation & v . a = 0 implies ( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) ) )
assume A1: K is having_valuation ; ::_thesis: ( not v . a = 0 or ( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) ) )
assume A2: v . a = 0 ; ::_thesis: ( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) )
thus  a is Element of (ValuatRing v) by A1, A2, Th52; ::_thesis: a " is Element of (ValuatRing v)
 a <> 0. K by A1, A2, Def8;
then  v . (a ") = - (v . a) by A1, Th21;
hence  a " is Element of (ValuatRing v) by A1, A2, Th52; ::_thesis: verum
end;

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
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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
let a be Element of K; ::_thesis: 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
let v be Valuation of K; ::_thesis: ( K is having_valuation & a <> 0. K & a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) implies v . a = 0 )
assume A1: K is having_valuation ; ::_thesis: ( not a <> 0. K or not a is Element of (ValuatRing v) or not a " is Element of (ValuatRing v) or v . a = 0 )
assume that
A2: a <> 0. K and
A3: a is Element of (ValuatRing v) ; ::_thesis: ( not a " is Element of (ValuatRing v) or v . a = 0 )
assume  a " is Element of (ValuatRing v) ; ::_thesis: v . a = 0
then  0 <= v . (a ") by A1, Th52;
then  - (- (v . a)) <= - 0 by A1, A2, Th21;
hence  v . a = 0 by A3, A1, Th52; ::_thesis: verum
end;

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) )
proof
let K be non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr ; ::_thesis: 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) )
let a be Element of K; ::_thesis: 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) )
let v be Valuation of K; ::_thesis: ( K is having_valuation & v . a = 0 implies for I being Ideal of (ValuatRing v) holds
( a in I iff I = the carrier of (ValuatRing v) ) )
assume A1: K is having_valuation ; ::_thesis: ( not v . a = 0 or for I being Ideal of (ValuatRing v) holds
( a in I iff I = the carrier of (ValuatRing v) ) )
assume A2: v . a = 0 ; ::_thesis: for I being Ideal of (ValuatRing v) holds
( a in I iff I = the carrier of (ValuatRing v) )
let I be Ideal of (ValuatRing v); ::_thesis: ( a in I iff I = the carrier of (ValuatRing v) )
thus  ( a in I implies I = the carrier of (ValuatRing v) ) ::_thesis: ( I = the carrier of (ValuatRing v) implies a in I )
proof
assume A3: a in I ; ::_thesis: I = the carrier of (ValuatRing v)
thus  I c= the carrier of (ValuatRing v) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (ValuatRing v) c= I
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (ValuatRing v) or x in I )
assume  x in the carrier of (ValuatRing v) ; ::_thesis: x in I
then reconsider x = 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  x in I by A5, A4, Lm9; ::_thesis: verum
end;
 the carrier of (ValuatRing v) = NonNegElements v by A1, Def12;
hence  ( I = the carrier of (ValuatRing v) implies a in I ) by A2; ::_thesis: verum
end;

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)
proof
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
Pgenerator v is Element of (ValuatRing v)
let v be Valuation of K; ::_thesis: ( K is having_valuation implies Pgenerator v is Element of (ValuatRing v) )
set a = Pgenerator v;
set l = least-positive (rng v);
assume A1: K is having_valuation ; ::_thesis: Pgenerator v is Element of (ValuatRing v)
then A2: Pgenerator v = the Element of v " {(least-positive (rng v))} by Def9;
 least-positive (rng v) in rng v by A1, Lm6;
then  {(least-positive (rng v))} c= rng v by ZFMISC_1:31;
then  not v " {(least-positive (rng v))} is empty by RELAT_1:139;
then  v . (Pgenerator v) in {(least-positive (rng v))} by A2, FUNCT_1:def_7;
then  v . (Pgenerator v) = least-positive (rng v) by TARSKI:def_1;
hence  Pgenerator v is Element of (ValuatRing v) by A1, Th52; ::_thesis: verum
end;

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
proof
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
vp v is proper
let v be Valuation of K; ::_thesis: ( K is having_valuation implies vp v is proper )
assume A1: K is having_valuation ; ::_thesis: vp v is proper
then  1. K is Element of (ValuatRing v) by Def12;
hence  vp v <> the carrier of (ValuatRing v) by A1, Th63; :: according to SUBSET_1:def_6 ::_thesis: verum
end;

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
proof
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
for x being Element of (ValuatRing v) st not x in vp v holds
v . x = 0
let v be Valuation of K; ::_thesis: ( K is having_valuation implies for x being Element of (ValuatRing v) st not x in vp v holds
v . x = 0 )
assume A1: K is having_valuation ; ::_thesis: for x being Element of (ValuatRing v) st not x in vp v holds
v . x = 0
let x be Element of (ValuatRing v); ::_thesis: ( not x in vp v implies v . x = 0 )
reconsider y = x as Element of K by A1, Th51;
assume  not x in vp v ; ::_thesis: v . x = 0
then  v . y <= 0 by A1, Th61;
hence  v . x = 0 by A1, Th52; ::_thesis: verum
end;

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
proof
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
vp v is prime
let v be Valuation of K; ::_thesis: ( K is having_valuation implies vp v is prime )
assume A1: K is having_valuation ; ::_thesis: vp v is prime
hence  vp v is proper by Th76; :: according to RING_1:def_2 ::_thesis: vp v is V250( ValuatRing v)
let a, b be Element of (ValuatRing v); :: according to RING_1:def_1 ::_thesis: ( not a * b in vp v or a in vp v or b in vp v )
assume A2: a * b in vp v ; ::_thesis: ( a in vp v or b in vp v )
assume  not a in vp v ; ::_thesis: b in vp v
then A3: v . a = 0 by A1, Th77;
assume A4: not b in vp v ; ::_thesis: contradiction
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  contradiction by A1, A2, A5, Th61; ::_thesis: verum
end;

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
proof
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
for I being proper Ideal of (ValuatRing v) holds I c= vp v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies for I being proper Ideal of (ValuatRing v) holds I c= vp v )
assume A1: K is having_valuation ; ::_thesis: for I being proper Ideal of (ValuatRing v) holds I c= vp v
let I be proper Ideal of (ValuatRing v); ::_thesis: I c= vp v
A2: I <> the carrier of (ValuatRing v) by SUBSET_1:def_6;
assume  not I c= vp v ; ::_thesis: contradiction
then consider x being set  such that
A3: x in I and
A4: not x in vp v by TARSKI:def_3;
A5: x is Element of K by A1, A3, Th51;
 v . x = 0 by A1, A4, A3, Th77;
hence  contradiction by A1, A2, A3, A5, Th74; ::_thesis: verum
end;

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
proof
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
vp v is maximal
let v be Valuation of K; ::_thesis: ( K is having_valuation implies vp v is maximal )
assume A1: K is having_valuation ; ::_thesis: vp v is maximal
thus  vp v is proper :: according to RING_1:def_4 ::_thesis: vp v is V252( ValuatRing v)
proof
 1. (ValuatRing v) = 1. K by A1, Def12;
hence  vp v <> the carrier of (ValuatRing v) by A1, Th63; :: according to SUBSET_1:def_6 ::_thesis: verum
end;
let J be Ideal of (ValuatRing v); :: according to RING_1:def_3 ::_thesis: ( not vp v c= J or J = vp v or not J is proper )
assume A2: vp v c= J ; ::_thesis: ( J = vp v or not J is proper )
 ( not J is proper or J = vp v )
proof
assume  J is proper ; ::_thesis: J = vp v
then  J c= vp v by A1, Th79;
hence  J = vp v by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  ( J = vp v or not J is proper ) ; ::_thesis: verum
end;

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
proof
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
for I being maximal Ideal of (ValuatRing v) holds I = vp v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies for I being maximal Ideal of (ValuatRing v) holds I = vp v )
assume A1: K is having_valuation ; ::_thesis: for I being maximal Ideal of (ValuatRing v) holds I = vp v
let I be maximal Ideal of (ValuatRing v); ::_thesis: I = vp v
assume A2: not I = vp v ; ::_thesis: contradiction
percases ( not I c= vp v or I c= vp v ) ;
suppose not I c= vp v ; ::_thesis: contradiction
hence  contradiction by A1, Th79; ::_thesis: verum
end;
suppose I c= vp v ; ::_thesis: contradiction
then  ( not vp v is proper or I = vp v ) by RING_1:def_3;
then A3: ( vp v = the carrier of (ValuatRing v) or I = vp v ) by SUBSET_1:def_6;
 1. (ValuatRing v) = 1. K by A1, Def12;
hence  contradiction by A3, A1, A2, Th63; ::_thesis: verum
end;
end;
end;

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
proof
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
NonNegElements (normal-valuation v) = NonNegElements v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies NonNegElements (normal-valuation v) = NonNegElements v )
assume A1: K is having_valuation ; ::_thesis: NonNegElements (normal-valuation v) = NonNegElements v
set f = normal-valuation v;
thus  NonNegElements (normal-valuation v) c= NonNegElements v :: according to XBOOLE_0:def_10 ::_thesis: NonNegElements v c= NonNegElements (normal-valuation v)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in NonNegElements (normal-valuation v) or a in NonNegElements v )
assume  a in NonNegElements (normal-valuation v) ; ::_thesis: a in NonNegElements v
then consider x being Element of K such that
A2: a = x and
A3: 0 <= (normal-valuation v) . x ;
 0 <= v . x by A1, A3, Th41;
hence  a in NonNegElements v by A2; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in NonNegElements v or a in NonNegElements (normal-valuation v) )
assume  a in NonNegElements v ; ::_thesis: a in NonNegElements (normal-valuation v)
then consider x being Element of K such that
A4: a = x and
A5: 0 <= v . x ;
 0 <= (normal-valuation v) . x by A1, A5, Th41;
hence  a in NonNegElements (normal-valuation v) by A4; ::_thesis: verum
end;

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
proof
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
ValuatRing (normal-valuation v) = ValuatRing v
let v be Valuation of K; ::_thesis: ( K is having_valuation implies ValuatRing (normal-valuation v) = ValuatRing v )
assume A1: K is having_valuation ; ::_thesis: ValuatRing (normal-valuation v) = ValuatRing v
set f = normal-valuation v;
set R = ValuatRing v;
set S = ValuatRing (normal-valuation v);
A2: the carrier of (ValuatRing (normal-valuation v)) = NonNegElements (normal-valuation v) by A1, Def12;
A3: NonNegElements (normal-valuation v) = NonNegElements v by A1, Th82;
A4: the addF of (ValuatRing v) = the addF of K | [:(NonNegElements v),(NonNegElements v):] by A1, Def12
.= the addF of (ValuatRing (normal-valuation v)) by A1, A3, Def12 ;
A5: the multF of (ValuatRing v) = the multF of K | [:(NonNegElements v),(NonNegElements v):] by A1, Def12
.= the multF of (ValuatRing (normal-valuation v)) by A1, A3, Def12 ;
A6: the ZeroF of (ValuatRing v) = 0. K by A1, Def12
.= the ZeroF of (ValuatRing (normal-valuation v)) by A1, Def12 ;
the OneF of (ValuatRing v) = 1. K by A1, Def12
.= the OneF of (ValuatRing (normal-valuation v)) by A1, Def12 ;
hence  ValuatRing (normal-valuation v) = ValuatRing v by A3, A2, A4, A5, A6, A1, Def12; ::_thesis: verum
end;