let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; for v being Valuation of K st K is having_valuation holds
for I being non empty Subset of K
for x being Element of (ValuatRing v) st I is Ideal of (ValuatRing v) & x in min (I,v) holds
I = {x} -Ideal
let v be Valuation of K; ( 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
; 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; 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); ( I is Ideal of (ValuatRing v) & x in min (I,v) implies I = {x} -Ideal )
assume A2:
I is Ideal of (ValuatRing v)
; ( not x in min (I,v) or I = {x} -Ideal )
assume A3:
x in min (I,v)
; I = {x} -Ideal
A4:
min (I,v) c= I
by A1, A2, Th64;
thus
I c= {x} -Ideal
XBOOLE_0:def 10 {x} -Ideal c= Iproof
let a be
object ;
TARSKI:def 3 ( not a in I or a in {x} -Ideal )
assume A5:
a in I
;
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;
per cases
( x <> 0. K or x = 0. (ValuatRing v) )
by A1, Def12;
suppose A8:
x = 0. (ValuatRing v)
;
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;
verum end;
end;
{x} c= I
by A4, A3, ZFMISC_1:31;
hence
{x} -Ideal c= I
by A2, IDEAL_1:def 14; verum