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 & a <> 0. K holds

v . (a ") = - (v . a)

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

v . (a ") = - (v . a)

let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K implies v . (a ") = - (v . a) )

assume that

A1: K is having_valuation and

A2: a <> 0. K ; :: thesis: v . (a ") = - (v . a)

a * (a ") = 1. K by A2, VECTSP_2:def 2;

then A3: (v . a) + (v . (a ")) = v . (1. K) by A1, Def8

.= 0 by A1, Th17 ;

then reconsider w1 = v . a, w2 = v . (a ") as Element of REAL by XREAL_0:def 1;

w1 + w2 = 0 by A3, XXREAL_3:def 2;

then - w1 = w2 ;

hence v . (a ") = - (v . a) by XXREAL_3:def 3; :: thesis: verum

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

v . (a ") = - (v . a)

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

v . (a ") = - (v . a)

let v be Valuation of K; :: thesis: ( K is having_valuation & a <> 0. K implies v . (a ") = - (v . a) )

assume that

A1: K is having_valuation and

A2: a <> 0. K ; :: thesis: v . (a ") = - (v . a)

a * (a ") = 1. K by A2, VECTSP_2:def 2;

then A3: (v . a) + (v . (a ")) = v . (1. K) by A1, Def8

.= 0 by A1, Th17 ;

now :: thesis: not a " = 0. K

then
( v . a in INT & v . (a ") in INT )
by A1, A2, Def8;assume
a " = 0. K
; :: thesis: contradiction

then 1. K = a * (0. K) by A2, VECTSP_2:def 2

.= 0. K ;

hence contradiction ; :: thesis: verum

end;then 1. K = a * (0. K) by A2, VECTSP_2:def 2

.= 0. K ;

hence contradiction ; :: thesis: verum

then reconsider w1 = v . a, w2 = v . (a ") as Element of REAL by XREAL_0:def 1;

w1 + w2 = 0 by A3, XXREAL_3:def 2;

then - w1 = w2 ;

hence v . (a ") = - (v . a) by XXREAL_3:def 3; :: thesis: verum