let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative 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

hence {x} -Ideal c= I by A2, IDEAL_1:def 14; :: thesis: verum

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

{x} c= I
by A4, A3, ZFMISC_1:31;
let a be object ; :: 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;

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

per cases
( x <> 0. K or x = 0. (ValuatRing v) )
by A1, Def12;

end;

suppose A6:
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 Lm4;

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 ;

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;v . x1 <= v . y1 by A1, A2, A3, A5, Th65;

then 0 <= (v . y1) - (v . x1) by Lm4;

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 ;

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

suppose A8:
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;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

hence {x} -Ideal c= I by A2, IDEAL_1:def 14; :: thesis: verum