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)
then reconsider I = { x where x is Element of K : 0 < v . x } as non empty Subset of (ValuatRing v) by A1, Lm9;
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 IDEAL_1:def 1 ( I is left-ideal & I is right-ideal )
let x,
y be
Element of
(ValuatRing v);
( x in I & y in I implies x + y in I )assume
x in I
;
( 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
;
x + y in Ithen 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;
verum
end;
let p,
x be
Element of
(ValuatRing v);
IDEAL_1:def 3 ( not x in I or x * p in I )
assume
x in I
;
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;
verum
end;
hence
{ x where x is Element of K : 0 < v . x } is Ideal of (ValuatRing v)
; verum