let K be Ring; :: thesis: for V being LeftMod of K
for A1, A2 being Subset of V st A1 \/ A2 is linearly-independent & A1 misses A2 holds
(Lin A1) /\ (Lin A2) = (0). V

let V be LeftMod of K; :: thesis: for A1, A2 being Subset of V st A1 \/ A2 is linearly-independent & A1 misses A2 holds
(Lin A1) /\ (Lin A2) = (0). V

let A1, A2 be Subset of V; :: thesis: ( A1 \/ A2 is linearly-independent & A1 misses A2 implies (Lin A1) /\ (Lin A2) = (0). V )
assume that
A1: A1 \/ A2 is linearly-independent and
A2: A1 /\ A2 = {} ; :: according to XBOOLE_0:def 7 :: thesis: (Lin A1) /\ (Lin A2) = (0). V
reconsider P = (Lin A1) /\ (Lin A2) as strict Subspace of V ;
set Z = the carrier of P;
A3: the carrier of P = the carrier of (Lin A1) /\ the carrier of (Lin A2) by VECTSP_5:def 2;
A4: now :: thesis: for x being set st x in the carrier of P holds
x = 0. V
let x be set ; :: thesis: ( x in the carrier of P implies x = 0. V )
assume A5: x in the carrier of P ; :: thesis: x = 0. V
then A6: x in the carrier of (Lin A1) by ;
A7: x in the carrier of (Lin A2) by ;
A8: x in Lin A1 by A6;
A9: x in Lin A2 by A7;
consider l1 being Linear_Combination of A1 such that
A10: x = Sum l1 by ;
consider l2 being Linear_Combination of A2 such that
A11: x = Sum l2 by ;
A12: Carrier l1 c= A1 by VECTSP_6:def 4;
Carrier l2 c= A2 by VECTSP_6:def 4;
then A13: (Carrier l1) \/ (Carrier l2) c= A1 \/ A2 by ;
Carrier (l1 - l2) c= (Carrier l1) \/ (Carrier l2) by VECTSP_6:41;
then Carrier (l1 - l2) c= A1 \/ A2 by ;
then reconsider l = l1 - l2 as Linear_Combination of A1 \/ A2 by VECTSP_6:def 4;
Sum l = (Sum l1) - (Sum l2) by VECTSP_6:47
.= 0. V by ;
then A14: Carrier l = {} by ;
Carrier l1 = {}
proof
assume A15: Carrier l1 <> {} ; :: thesis: contradiction
set x = the Element of Carrier l1;
consider b being Vector of V such that
A16: the Element of Carrier l1 = b and
A17: l1 . b <> 0. K by ;
b in A1 by ;
then A18: not b in A2 by ;
0. K = l . b by
.= (l1 . b) - (l2 . b) by VECTSP_6:40 ;
then l1 . b = l2 . b by RLVECT_1:21
.= 0. K by ;
hence contradiction by A17; :: thesis: verum
end;
hence x = 0. V by ; :: thesis: verum
end;
0. V in (Lin A1) /\ (Lin A2) by VECTSP_4:17;
then for x being object holds
( x in the carrier of P iff x = 0. V ) by A4;
then the carrier of P = {(0. V)} by TARSKI:def 1;
hence (Lin A1) /\ (Lin A2) = (0). V by VECTSP_4:def 3; :: thesis: verum