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 A3, XBOOLE_0:def 4;
A7: x in the carrier of (Lin A2) by A3, A5, XBOOLE_0:def 4;
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 A8, MOD_3:4;
consider l2 being Linear_Combination of A2 such that
A11: x = Sum l2 by A9, MOD_3:4;
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 A12, XBOOLE_1:13;
Carrier (l1 - l2) c= (Carrier l1) \/ (Carrier l2) by VECTSP_6:41;
then Carrier (l1 - l2) c= A1 \/ A2 by A13, XBOOLE_1:1;
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 A10, A11, VECTSP_1:19 ;
then A14: Carrier l = {} by A1, VECTSP_7:def 1;
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 A15, VECTSP_6:1;
b in A1 by A12, A15, A16, TARSKI:def 3;
then A18: not b in A2 by A2, XBOOLE_0:def 4;
0. K = l . b by A14, VECTSP_6:2
.= (l1 . b) - (l2 . b) by VECTSP_6:40 ;
then l1 . b = l2 . b by RLVECT_1:21
.= 0. K by A18, Th2 ;
hence contradiction by A17; :: thesis: verum

end;

hence x = 0. V by A10, VECTSP_6:19; :: 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