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)

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 )

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

then reconsider I = { x where x is Element of K : 0 < v . x } as non empty Subset of (ValuatRing v) by A1, Lm9;
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 (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;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

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

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 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: verumhereby :: 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;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

hereby :: according to IDEAL_1:def 2 :: thesis: I is right-ideal

let p, x be Element of (ValuatRing v); :: according to IDEAL_1:def 3 :: thesis: ( not x in I or x * p in I )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 ;

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

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 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