let V be RealLinearSpace; :: thesis: for L1, L2 being Linear_Combination of V st Sum L1 <> Sum L2 & sum L1 = sum L2 holds

ex v being VECTOR of V st L1 . v > L2 . v

let L1, L2 be Linear_Combination of V; :: thesis: ( Sum L1 <> Sum L2 & sum L1 = sum L2 implies ex v being VECTOR of V st L1 . v > L2 . v )

assume that

A1: Sum L1 <> Sum L2 and

A2: sum L1 = sum L2 ; :: thesis: ex v being VECTOR of V st L1 . v > L2 . v

consider F being FinSequence such that

A3: rng F = (Carrier L1) \/ (Carrier L2) and

A4: F is one-to-one by FINSEQ_4:58;

reconsider F = F as FinSequence of V by A3, FINSEQ_1:def 4;

A5: len (L2 * F) = len F by FINSEQ_2:33;

A6: len (L1 * F) = len F by FINSEQ_2:33;

then reconsider L1F = L1 * F, L2F = L2 * F as Element of (len F) -tuples_on REAL by A5, FINSEQ_2:92;

A7: len (L2F - L1F) = len F by CARD_1:def 7;

assume A8: for v being Element of V holds L1 . v <= L2 . v ; :: thesis: contradiction

A9: for i being Nat st i in dom (L2F - L1F) holds

0 <= (L2F - L1F) . i

.= (sum L2) - (Sum L1F) by A3, A4, RLAFFIN1:30, XBOOLE_1:7

.= (sum L2) - (sum L1) by A3, A4, RLAFFIN1:30, XBOOLE_1:7

.= 0 by A2 ;

ex v being VECTOR of V st L1 . v > L2 . v

let L1, L2 be Linear_Combination of V; :: thesis: ( Sum L1 <> Sum L2 & sum L1 = sum L2 implies ex v being VECTOR of V st L1 . v > L2 . v )

assume that

A1: Sum L1 <> Sum L2 and

A2: sum L1 = sum L2 ; :: thesis: ex v being VECTOR of V st L1 . v > L2 . v

consider F being FinSequence such that

A3: rng F = (Carrier L1) \/ (Carrier L2) and

A4: F is one-to-one by FINSEQ_4:58;

reconsider F = F as FinSequence of V by A3, FINSEQ_1:def 4;

A5: len (L2 * F) = len F by FINSEQ_2:33;

A6: len (L1 * F) = len F by FINSEQ_2:33;

then reconsider L1F = L1 * F, L2F = L2 * F as Element of (len F) -tuples_on REAL by A5, FINSEQ_2:92;

A7: len (L2F - L1F) = len F by CARD_1:def 7;

assume A8: for v being Element of V holds L1 . v <= L2 . v ; :: thesis: contradiction

A9: for i being Nat st i in dom (L2F - L1F) holds

0 <= (L2F - L1F) . i

proof

A14: Sum (L2F - L1F) =
(Sum L2F) - (Sum L1F)
by RVSUM_1:90
let i be Nat; :: thesis: ( i in dom (L2F - L1F) implies 0 <= (L2F - L1F) . i )

L2 . (F /. i) >= L1 . (F /. i) by A8;

then A10: (L2 . (F /. i)) - (L1 . (F /. i)) >= (L1 . (F /. i)) - (L1 . (F /. i)) by XREAL_1:9;

assume A11: i in dom (L2F - L1F) ; :: thesis: 0 <= (L2F - L1F) . i

then i in dom F by A7, FINSEQ_3:29;

then A12: F /. i = F . i by PARTFUN1:def 6;

i in dom L2F by A5, A7, A11, FINSEQ_3:29;

then A13: L2F . i = L2 . (F . i) by FUNCT_1:12;

i in dom L1F by A6, A7, A11, FINSEQ_3:29;

then L1F . i = L1 . (F . i) by FUNCT_1:12;

hence 0 <= (L2F - L1F) . i by A10, A12, A13, RVSUM_1:27; :: thesis: verum

end;L2 . (F /. i) >= L1 . (F /. i) by A8;

then A10: (L2 . (F /. i)) - (L1 . (F /. i)) >= (L1 . (F /. i)) - (L1 . (F /. i)) by XREAL_1:9;

assume A11: i in dom (L2F - L1F) ; :: thesis: 0 <= (L2F - L1F) . i

then i in dom F by A7, FINSEQ_3:29;

then A12: F /. i = F . i by PARTFUN1:def 6;

i in dom L2F by A5, A7, A11, FINSEQ_3:29;

then A13: L2F . i = L2 . (F . i) by FUNCT_1:12;

i in dom L1F by A6, A7, A11, FINSEQ_3:29;

then L1F . i = L1 . (F . i) by FUNCT_1:12;

hence 0 <= (L2F - L1F) . i by A10, A12, A13, RVSUM_1:27; :: thesis: verum

.= (sum L2) - (Sum L1F) by A3, A4, RLAFFIN1:30, XBOOLE_1:7

.= (sum L2) - (sum L1) by A3, A4, RLAFFIN1:30, XBOOLE_1:7

.= 0 by A2 ;

now :: thesis: for v being Element of V holds L1 . v = L2 . v

hence
contradiction
by A1, RLVECT_2:def 9; :: thesis: verumlet v be Element of V; :: thesis: L1 . v = L2 . v

end;now :: thesis: L1 . v = L2 . vend;

hence
L1 . v = L2 . v
; :: thesis: verumper cases
( ( not v in Carrier L1 & not v in Carrier L2 ) or v in rng F )
by A3, XBOOLE_0:def 3;

end;

suppose
v in rng F
; :: thesis: L1 . v = L2 . v

then consider i being object such that

A16: i in dom F and

A17: F . i = v by FUNCT_1:def 3;

reconsider i = i as Nat by A16;

i in dom L2F by A5, A16, FINSEQ_3:29;

then A18: ( (L2F - L1F) . i = (L2F . i) - (L1F . i) & L2F . i = L2 . v ) by A17, FUNCT_1:12, RVSUM_1:27;

i in dom L1F by A6, A16, FINSEQ_3:29;

then A19: L1F . i = L1 . v by A17, FUNCT_1:12;

A20: i in dom (L2F - L1F) by A7, A16, FINSEQ_3:29;

then (L2 . v) - (L1 . v) <= 0 by A9, A14, A18, A19, RVSUM_1:85;

then (L2 . v) - (L1 . v) = 0 by A9, A18, A19, A20;

hence L1 . v = L2 . v ; :: thesis: verum

end;A16: i in dom F and

A17: F . i = v by FUNCT_1:def 3;

reconsider i = i as Nat by A16;

i in dom L2F by A5, A16, FINSEQ_3:29;

then A18: ( (L2F - L1F) . i = (L2F . i) - (L1F . i) & L2F . i = L2 . v ) by A17, FUNCT_1:12, RVSUM_1:27;

i in dom L1F by A6, A16, FINSEQ_3:29;

then A19: L1F . i = L1 . v by A17, FUNCT_1:12;

A20: i in dom (L2F - L1F) by A7, A16, FINSEQ_3:29;

then (L2 . v) - (L1 . v) <= 0 by A9, A14, A18, A19, RVSUM_1:85;

then (L2 . v) - (L1 . v) = 0 by A9, A18, A19, A20;

hence L1 . v = L2 . v ; :: thesis: verum