let R be Ring; :: thesis: for V being LeftMod of R
for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let V be LeftMod of R; :: thesis: for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let A, B be Subset of V; :: thesis: for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let l be Linear_Combination of B; :: thesis: ( A c= B implies l = (l ! A) + (l ! (B \ A)) )
assume A1: A c= B ; :: thesis: l = (l ! A) + (l ! (B \ A))
set r = (l ! A) + (l ! (B \ A));
let v be Element of V; :: according to FUNCT_2:def 8 :: thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
A2: ( not v in B or v in A or v in B \ A )
proof
assume A3: v in B ; :: thesis: ( v in A or v in B \ A )
B = A \/ (B \ A) by A1, XBOOLE_1:45;
hence ( v in A or v in B \ A ) by A3, XBOOLE_0:def 3; :: thesis: verum
end;
per cases ( v in A or v in B \ A or not v in B ) by A2;
suppose A4: v in A ; :: thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
then not v in B \ A by XBOOLE_0:def 5;
then A5: (l ! (B \ A)) . v = 0. R by Th26;
(l ! A) . v = l . v by A4, Th25;
then ((l ! A) + (l ! (B \ A))) . v = (l . v) + (0. R) by A5, VECTSP_6:22
.= l . v ;
hence l . v = ((l ! A) + (l ! (B \ A))) . v ; :: thesis: verum
end;
suppose A6: v in B \ A ; :: thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
then not v in A by XBOOLE_0:def 5;
then A7: (l ! A) . v = 0. R by Th26;
(l ! (B \ A)) . v = l . v by A6, Th25;
then ((l ! A) + (l ! (B \ A))) . v = (0. R) + (l . v) by A7, VECTSP_6:22
.= l . v ;
hence l . v = ((l ! A) + (l ! (B \ A))) . v ; :: thesis: verum
end;
suppose A8: not v in B ; :: thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
Carrier l c= B by VECTSP_6:def 4;
then A9: not v in Carrier l by A8;
not v in B \ A by A8, XBOOLE_0:def 5;
then A10: (l ! (B \ A)) . v = 0. R by Th26;
(l ! A) . v = 0. R by A1, A8, Th26;
then ((l ! A) + (l ! (B \ A))) . v = (0. R) + (0. R) by A10, VECTSP_6:22
.= 0. R ;
hence l . v = ((l ! A) + (l ! (B \ A))) . v by A9; :: thesis: verum
end;
end;