set R = ValuatRing v;
set I = { x where x is Element of K : 0 < v . x } ;
A2: the carrier of () = NonNegElements v by ;
{ x where x is Element of K : 0 < v . x } c= the carrier of ()
proof
let a be object ; :: 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 () )
assume a in { x where x is Element of K : 0 < v . x } ; :: thesis: a in the carrier of ()
then ex x being Element of K st
( a = x & 0 < v . x ) ;
hence a in the carrier of () by A2; :: thesis: verum
end;
then reconsider I = { x where x is Element of K : 0 < v . x } as non empty Subset of () by ;
A3: the carrier of () c= the carrier of K by ;
( 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 (); :: 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 ;
0 < min ((v . x1),(v . y1)) by ;
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 (); :: 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 ;
reconsider p1 = p as Element of K by A3;
A12: p * x = p1 * x1 by ;
A13: v . (p1 * x1) = (v . p1) + (v . x1) by ;
0 <= v . p1 by ;
hence p * x in I by ; :: thesis: verum
end;
let p, x be Element of (); :: 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 ;
reconsider p1 = p as Element of K by A3;
A16: p * x = p1 * x1 by ;
A17: v . (p1 * x1) = (v . p1) + (v . x1) by ;
0 <= v . p1 by ;
hence x * p in I by ; :: thesis: verum
end;
hence { x where x is Element of K : 0 < v . x } is Ideal of () ; :: thesis: verum