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 )

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;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

per cases
( v in A or v in B \ A or not v in B )
by A2;

end;

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;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

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;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

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;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