let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for a, b being Element of K
for v being Valuation of K st K is having_valuation holds
min ((v . a),(v . b)) <= v . (a + b)
let a, b be Element of K; :: thesis: for v being Valuation of K st K is having_valuation holds
min ((v . a),(v . b)) <= v . (a + b)
let v be Valuation of K; :: thesis: ( K is having_valuation implies min ((v . a),(v . b)) <= v . (a + b) )
assume A1: K is having_valuation ; :: thesis: min ((v . a),(v . b)) <= v . (a + b)

per cases ( a = 0. K or b = 0. K or ( a <> 0. K & 0 <= v . (b / a) ) or ( a <> 0. K & b <> 0. K & v . (b / a) <= 0 ) ) ;

suppose A2: a = 0. K ; :: thesis: min ((v . a),(v . b)) <= v . (a + b)

then v . a = +infty by A1, Def8;
then min ((v . a),(v . b)) = v . b by XXREAL_0:42;
hence min ((v . a),(v . b)) <= v . (a + b) by A2, RLVECT_1:def 4; :: thesis: verum

end;

suppose A3: b = 0. K ; :: thesis: min ((v . a),(v . b)) <= v . (a + b)

then v . b = +infty by A1, Def8;
then min ((v . a),(v . b)) = v . a by XXREAL_0:42;
hence min ((v . a),(v . b)) <= v . (a + b) by A3, RLVECT_1:def 4; :: thesis: verum

end;

suppose that A4: a <> 0. K and
A5: 0 <= v . (b / a) ; :: thesis: min ((v . a),(v . b)) <= v . (a + b)

v . a <= v . b by A1, A4, A5, Th24;
then A6: min ((v . a),(v . b)) = v . a by XXREAL_0:def 9;
0 <= v . ((1. K) + (b / a)) by A5, A1, Def8;
then A7: 0 + (v . a) <= (v . ((1. K) + (b / a))) + (v . a) by XXREAL_3:36;
(v . ((1. K) + (b / a))) + (v . a) = v . (((1. K) + (b / a)) * a) by A1, Def8
.= v . (((1. K) * a) + ((b / a) * a)) by VECTSP_1:def 3
.= v . (a + ((b / a) * a))
.= v . (a + b) by A4, VECTSP_2:22 ;
hence min ((v . a),(v . b)) <= v . (a + b) by A6, A7, XXREAL_3:4; :: thesis: verum

end;

suppose that A8: a <> 0. K and
A9: b <> 0. K and
A10: v . (b / a) <= 0 ; :: thesis: min ((v . a),(v . b)) <= v . (a + b)

A11: 0 <= v . (a / b) by A1, A8, A9, A10, Th25;
v . b <= v . a by A1, A8, A10, Th26;
then A12: min ((v . a),(v . b)) = v . b by XXREAL_0:def 9;
0 <= v . ((1. K) + (a / b)) by A11, A1, Def8;
then A13: 0 + (v . b) <= (v . ((1. K) + (a / b))) + (v . b) by XXREAL_3:36;
(v . ((1. K) + (a / b))) + (v . b) = v . (((1. K) + (a / b)) * b) by A1, Def8
.= v . (((1. K) * b) + ((a / b) * b)) by VECTSP_1:def 3
.= v . (b + ((a / b) * b))
.= v . (b + a) by A9, VECTSP_2:22 ;
hence min ((v . a),(v . b)) <= v . (a + b) by A12, A13, XXREAL_3:4; :: thesis: verum

end;

end;