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 x being Element of K
for y being Element of (ValuatRing v) st x = y holds
- x = - y
let v be Valuation of K; :: thesis: ( K is having_valuation implies for x being Element of K
for y being Element of (ValuatRing v) st x = y holds
- x = - y )
set R = ValuatRing v;
set c = NonNegElements v;
assume A1: K is having_valuation ; :: thesis: for x being Element of K
for y being Element of (ValuatRing v) st x = y holds
- x = - y
let x be Element of K; :: thesis: for y being Element of (ValuatRing v) st x = y holds
- x = - y
let y be Element of (ValuatRing v); :: thesis: ( x = y implies - x = - y )
assume A2: x = y ; :: thesis: - x = - y
A3: 0 <= v . y by A1, A2, Th52;
v . (- x) = v . x by A1, Th20;
then reconsider x1 = - x as Element of (ValuatRing v) by A1, A2, A3, Th52;
x + (- x) = 0. K by RLVECT_1:def 10;
then y + x1 = 0. K by A2, A1, Th54
.= 0. (ValuatRing v) by A1, Def12 ;
hence - x = - y by RLVECT_1:def 10; :: thesis: verum