let V be ComplexLinearSpace; :: thesis: for v1, v2 being VECTOR of V st v1 <> v2 holds
for l being C_Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
let v1, v2 be VECTOR of V; :: thesis: ( v1 <> v2 implies for l being C_Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2) )
assume A1: v1 <> v2 ; :: thesis: for l being C_Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)
let l be C_Linear_Combination of {v1,v2}; :: thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
A2: 0. V = 0c * v1 by CLVECT_1:1;
A3: Carrier l c= {v1,v2} by Def4;
A4: 0. V = 0c * v2 by CLVECT_1:1;
per cases ( Carrier l = {} or Carrier l = {v1} or Carrier l = {v2} or Carrier l = {v1,v2} ) by A3, ZFMISC_1:36;
suppose Carrier l = {} ; :: thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
then A5: l = ZeroCLC V by Def3;
hence Sum l = 0. V by Th11
.= (0. V) + (0. V)
.= ((l . v1) * v1) + (0c * v2) by A4, A5, Th2, CLVECT_1:1
.= ((l . v1) * v1) + ((l . v2) * v2) by A5, Th2 ;
:: thesis: verum
end;
suppose A6: Carrier l = {v1} ; :: thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
then reconsider L = l as C_Linear_Combination of {v1} by Def4;
Sum L = (l . v1) * v1 by Th14;
then A7: Sum l = ((l . v1) * v1) + (0. V) ;
not v2 in Carrier l by A1, A6, TARSKI:def 1;
hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) by A4, A7; :: thesis: verum
end;
suppose A8: Carrier l = {v2} ; :: thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
then reconsider L = l as C_Linear_Combination of {v2} by Def4;
Sum L = (l . v2) * v2 by Th14;
then A9: Sum l = (0. V) + ((l . v2) * v2) ;
not v1 in Carrier l by A1, A8, TARSKI:def 1;
hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) by A2, A9; :: thesis: verum
end;
suppose Carrier l = {v1,v2} ; :: thesis: Sum l = ((l . v1) * v1) + ((l . v2) * v2)
then consider F being FinSequence of the carrier of V such that
A10: ( F is one-to-one & rng F = {v1,v2} ) and
A11: Sum l = Sum (l (#) F) by Def6;
( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A10, FINSEQ_3:99;
then ( l (#) F = <*((l . v1) * v1),((l . v2) * v2)*> or l (#) F = <*((l . v2) * v2),((l . v1) * v1)*> ) by Th9;
hence Sum l = ((l . v1) * v1) + ((l . v2) * v2) by A11, RLVECT_1:45; :: thesis: verum
end;
end;