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 holds
( not v . a is negative iff not (normal-valuation v) . a is negative )
let a be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds
( not v . a is negative iff not (normal-valuation v) . a is negative )
let v be Valuation of K; :: thesis: ( K is having_valuation implies ( not v . a is negative iff not (normal-valuation v) . a is negative ) )
set f = normal-valuation v;
set l = least-positive (rng v);
assume A1: K is having_valuation ; :: thesis: ( not v . a is negative iff not (normal-valuation v) . a is negative )
then A2: v . a = ((normal-valuation v) . a) * (least-positive (rng v)) by Def10;
per cases ( v . a is zero or (normal-valuation v) . a is zero or ( not v . a is zero & not (normal-valuation v) . a is zero ) ) ;
suppose ( v . a is zero or (normal-valuation v) . a is zero ) ; :: thesis: ( not v . a is negative iff not (normal-valuation v) . a is negative )
thus ( not v . a is negative iff not (normal-valuation v) . a is negative ) by A2; :: thesis: verum
end;
suppose that A3: not v . a is zero and
A4: not (normal-valuation v) . a is zero ; :: thesis: ( not v . a is negative iff not (normal-valuation v) . a is negative )
thus ( not v . a is negative implies not (normal-valuation v) . a is negative ) by A1, A3, Th40; :: thesis: ( not (normal-valuation v) . a is negative implies not v . a is negative )
thus ( not (normal-valuation v) . a is negative implies not v . a is negative ) by A4, A1, Th40; :: thesis: verum
end;
end;