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
ValuatRing v is domRing-like
let v be Valuation of K; :: thesis: ( K is having_valuation implies ValuatRing v is domRing-like )
set R = ValuatRing v;
assume A1: K is having_valuation ; :: thesis: ValuatRing v is domRing-like
let x, y be Element of (ValuatRing v); :: according to VECTSP_2:def 1 :: thesis: ( not x * y = 0. (ValuatRing v) or x = 0. (ValuatRing v) or y = 0. (ValuatRing v) )
assume that
A2: x * y = 0. (ValuatRing v) and
A3: x <> 0. (ValuatRing v) ; :: thesis: y = 0. (ValuatRing v)
reconsider x1 = x, y1 = y as Element of K by A1, Th51;
A4: 0. (ValuatRing v) = 0. K by A1, Def12;
A5: x1 * y1 = x * y by A1, Th55;
y1 = (x1 ") * (x1 * y1) by A3, A4, Lm7
.= 0. K by A2, A4, A5 ;
hence y = 0. (ValuatRing v) by A1, Def12; :: thesis: verum