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;

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

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

0. V in (Lin A1) /\ (Lin A2)
by VECTSP_4:17;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 = {}

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

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

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