let R be Ring; :: thesis: for V being LeftMod of R

for l, m being Linear_Combination of V st Carrier l misses Carrier m holds

Carrier (l + m) = (Carrier l) \/ (Carrier m)

let V be LeftMod of R; :: thesis: for l, m being Linear_Combination of V st Carrier l misses Carrier m holds

Carrier (l + m) = (Carrier l) \/ (Carrier m)

let l, m be Linear_Combination of V; :: thesis: ( Carrier l misses Carrier m implies Carrier (l + m) = (Carrier l) \/ (Carrier m) )

assume A1: Carrier l misses Carrier m ; :: thesis: Carrier (l + m) = (Carrier l) \/ (Carrier m)

thus Carrier (l + m) c= (Carrier l) \/ (Carrier m) by VECTSP_6:23; :: according to XBOOLE_0:def 10 :: thesis: (Carrier l) \/ (Carrier m) c= Carrier (l + m)

thus (Carrier l) \/ (Carrier m) c= Carrier (l + m) :: thesis: verum

for l, m being Linear_Combination of V st Carrier l misses Carrier m holds

Carrier (l + m) = (Carrier l) \/ (Carrier m)

let V be LeftMod of R; :: thesis: for l, m being Linear_Combination of V st Carrier l misses Carrier m holds

Carrier (l + m) = (Carrier l) \/ (Carrier m)

let l, m be Linear_Combination of V; :: thesis: ( Carrier l misses Carrier m implies Carrier (l + m) = (Carrier l) \/ (Carrier m) )

assume A1: Carrier l misses Carrier m ; :: thesis: Carrier (l + m) = (Carrier l) \/ (Carrier m)

thus Carrier (l + m) c= (Carrier l) \/ (Carrier m) by VECTSP_6:23; :: according to XBOOLE_0:def 10 :: thesis: (Carrier l) \/ (Carrier m) c= Carrier (l + m)

thus (Carrier l) \/ (Carrier m) c= Carrier (l + m) :: thesis: verum

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in (Carrier l) \/ (Carrier m) or v in Carrier (l + m) )

assume A2: v in (Carrier l) \/ (Carrier m) ; :: thesis: v in Carrier (l + m)

end;assume A2: v in (Carrier l) \/ (Carrier m) ; :: thesis: v in Carrier (l + m)

per cases
( v in Carrier l or v in Carrier m )
by A2, XBOOLE_0:def 3;

end;

suppose A3:
v in Carrier l
; :: thesis: v in Carrier (l + m)

then reconsider v = v as Element of V ;

not v in Carrier m by A1, A2, A3, XBOOLE_0:5;

then A4: ( (l + m) . v = (l . v) + (m . v) & m . v = 0. R ) by VECTSP_6:22;

l . v <> 0. R by A3, VECTSP_6:2;

hence v in Carrier (l + m) by A4; :: thesis: verum

end;not v in Carrier m by A1, A2, A3, XBOOLE_0:5;

then A4: ( (l + m) . v = (l . v) + (m . v) & m . v = 0. R ) by VECTSP_6:22;

l . v <> 0. R by A3, VECTSP_6:2;

hence v in Carrier (l + m) by A4; :: thesis: verum

suppose A5:
v in Carrier m
; :: thesis: v in Carrier (l + m)

then reconsider v = v as Element of V ;

not v in Carrier l by A1, A2, A5, XBOOLE_0:5;

then A6: ( (l + m) . v = (l . v) + (m . v) & l . v = 0. R ) by VECTSP_6:22;

m . v <> 0. R by A5, VECTSP_6:2;

hence v in Carrier (l + m) by A6; :: thesis: verum

end;not v in Carrier l by A1, A2, A5, XBOOLE_0:5;

then A6: ( (l + m) . v = (l . v) + (m . v) & l . v = 0. R ) by VECTSP_6:22;

m . v <> 0. R by A5, VECTSP_6:2;

hence v in Carrier (l + m) by A6; :: thesis: verum