let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a being Element of K

for v being Valuation of K st K is having_valuation & v . a = 0 holds

for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) )

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & v . a = 0 holds

for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) )

let v be Valuation of K; :: thesis: ( K is having_valuation & v . a = 0 implies for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) ) )

assume A1: K is having_valuation ; :: thesis: ( not v . a = 0 or for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) ) )

assume A2: v . a = 0 ; :: thesis: for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) )

let I be Ideal of (ValuatRing v); :: thesis: ( a in I iff I = the carrier of (ValuatRing v) )

thus ( a in I implies I = the carrier of (ValuatRing v) ) :: thesis: ( I = the carrier of (ValuatRing v) implies a in I )

hence ( I = the carrier of (ValuatRing v) implies a in I ) by A2; :: thesis: verum

for v being Valuation of K st K is having_valuation & v . a = 0 holds

for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) )

let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation & v . a = 0 holds

for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) )

let v be Valuation of K; :: thesis: ( K is having_valuation & v . a = 0 implies for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) ) )

assume A1: K is having_valuation ; :: thesis: ( not v . a = 0 or for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) ) )

assume A2: v . a = 0 ; :: thesis: for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) )

let I be Ideal of (ValuatRing v); :: thesis: ( a in I iff I = the carrier of (ValuatRing v) )

thus ( a in I implies I = the carrier of (ValuatRing v) ) :: thesis: ( I = the carrier of (ValuatRing v) implies a in I )

proof

the carrier of (ValuatRing v) = NonNegElements v
by A1, Def12;
assume A3:
a in I
; :: thesis: I = the carrier of (ValuatRing v)

thus I c= the carrier of (ValuatRing v) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (ValuatRing v) c= I

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ValuatRing v) or x in I )

assume x in the carrier of (ValuatRing v) ; :: thesis: x in I

then reconsider x = x as Element of (ValuatRing v) ;

reconsider b = x as Element of K by A1, Th51;

A4: a <> 0. K by A1, A2, Def8;

reconsider y = a, z = a " as Element of (ValuatRing v) by A1, A2, Th72;

A5: y * (z * x) in I by A3, IDEAL_1:def 2;

reconsider za = z * x as Element of K by A1, Th51;

z * x = (a ") * b by A1, Th55;

then y * (z * x) = a * ((a ") * b) by A1, Th55;

hence x in I by A5, A4, Lm8; :: thesis: verum

end;thus I c= the carrier of (ValuatRing v) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (ValuatRing v) c= I

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ValuatRing v) or x in I )

assume x in the carrier of (ValuatRing v) ; :: thesis: x in I

then reconsider x = x as Element of (ValuatRing v) ;

reconsider b = x as Element of K by A1, Th51;

A4: a <> 0. K by A1, A2, Def8;

reconsider y = a, z = a " as Element of (ValuatRing v) by A1, A2, Th72;

A5: y * (z * x) in I by A3, IDEAL_1:def 2;

reconsider za = z * x as Element of K by A1, Th51;

z * x = (a ") * b by A1, Th55;

then y * (z * x) = a * ((a ") * b) by A1, Th55;

hence x in I by A5, A4, Lm8; :: thesis: verum

hence ( I = the carrier of (ValuatRing v) implies a in I ) by A2; :: thesis: verum