let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; 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; 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; ( 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
; ( 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
; 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); ( a in I iff I = the carrier of (ValuatRing v) )
thus
( a in I implies I = the carrier of (ValuatRing v) )
( I = the carrier of (ValuatRing v) implies a in I )proof
assume A3:
a in I
;
I = the carrier of (ValuatRing v)
thus
I c= the
carrier of
(ValuatRing v)
;
XBOOLE_0:def 10 the carrier of (ValuatRing v) c= I
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (ValuatRing v) or x in I )
assume
x in the
carrier of
(ValuatRing v)
;
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;
verum
end;
the carrier of (ValuatRing v) = NonNegElements v
by A1, Def12;
hence
( I = the carrier of (ValuatRing v) implies a in I )
by A2; verum