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
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)
per cases ( v in Carrier l or v in Carrier m ) by A2, XBOOLE_0:def 3;
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;
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;
end;
end;