let F be Field; :: thesis: for V being VectSp of F

for A being Subset of V st A is linearly-independent holds

for a being Element of V st a nin the carrier of (Lin A) holds

A \/ {a} is linearly-independent

let V be VectSp of F; :: thesis: for A being Subset of V st A is linearly-independent holds

for a being Element of V st a nin the carrier of (Lin A) holds

A \/ {a} is linearly-independent

let A be Subset of V; :: thesis: ( A is linearly-independent implies for a being Element of V st a nin the carrier of (Lin A) holds

A \/ {a} is linearly-independent )

assume A1: A is linearly-independent ; :: thesis: for a being Element of V st a nin the carrier of (Lin A) holds

A \/ {a} is linearly-independent

A2: { (Sum s) where s is Linear_Combination of A : verum } = the carrier of (Lin A) by VECTSP_7:def 2;

let a be Element of V; :: thesis: ( a nin the carrier of (Lin A) implies A \/ {a} is linearly-independent )

set B = A \/ {a};

assume that

A3: a nin the carrier of (Lin A) and

A4: A \/ {a} is linearly-dependent ; :: thesis: contradiction

consider l being Linear_Combination of A \/ {a} such that

A5: Sum l = 0. V and

A6: Carrier l <> {} by A4, VECTSP_7:def 1;

a in {a} by TARSKI:def 1;

then A7: (l ! {a}) . a = l . a by RANKNULL:25;

A c= the carrier of (Lin A)

then (A \/ {a}) \ A = {a} by XBOOLE_1:88, ZFMISC_1:50;

then l = (l ! A) + (l ! {a}) by RANKNULL:27, XBOOLE_1:7;

then 0. V = (Sum (l ! A)) + (Sum (l ! {a})) by A5, VECTSP_6:44

.= (Sum (l ! A)) + ((l . a) * a) by A7, VECTSP_6:17 ;

then A9: (l . a) * a = - (Sum (l ! A)) by ALGSTR_0:def 13;

A10: (- ((l . a) ")) * (l ! A) is Linear_Combination of A by VECTSP_6:31;

A12: Carrier l c= A \/ {a} by VECTSP_6:def 4;

Carrier l c= A by A11, A12, ZFMISC_1:136;

then l is Linear_Combination of A by VECTSP_6:def 4;

hence contradiction by A1, A5, A6, VECTSP_7:def 1; :: thesis: verum

for A being Subset of V st A is linearly-independent holds

for a being Element of V st a nin the carrier of (Lin A) holds

A \/ {a} is linearly-independent

let V be VectSp of F; :: thesis: for A being Subset of V st A is linearly-independent holds

for a being Element of V st a nin the carrier of (Lin A) holds

A \/ {a} is linearly-independent

let A be Subset of V; :: thesis: ( A is linearly-independent implies for a being Element of V st a nin the carrier of (Lin A) holds

A \/ {a} is linearly-independent )

assume A1: A is linearly-independent ; :: thesis: for a being Element of V st a nin the carrier of (Lin A) holds

A \/ {a} is linearly-independent

A2: { (Sum s) where s is Linear_Combination of A : verum } = the carrier of (Lin A) by VECTSP_7:def 2;

let a be Element of V; :: thesis: ( a nin the carrier of (Lin A) implies A \/ {a} is linearly-independent )

set B = A \/ {a};

assume that

A3: a nin the carrier of (Lin A) and

A4: A \/ {a} is linearly-dependent ; :: thesis: contradiction

consider l being Linear_Combination of A \/ {a} such that

A5: Sum l = 0. V and

A6: Carrier l <> {} by A4, VECTSP_7:def 1;

a in {a} by TARSKI:def 1;

then A7: (l ! {a}) . a = l . a by RANKNULL:25;

A c= the carrier of (Lin A)

proof

then
a nin A
by A3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in the carrier of (Lin A) )

assume A8: x in A ; :: thesis: x in the carrier of (Lin A)

then reconsider x = x as Element of V ;

x in Lin A by A8, VECTSP_7:8;

hence x in the carrier of (Lin A) ; :: thesis: verum

end;assume A8: x in A ; :: thesis: x in the carrier of (Lin A)

then reconsider x = x as Element of V ;

x in Lin A by A8, VECTSP_7:8;

hence x in the carrier of (Lin A) ; :: thesis: verum

then (A \/ {a}) \ A = {a} by XBOOLE_1:88, ZFMISC_1:50;

then l = (l ! A) + (l ! {a}) by RANKNULL:27, XBOOLE_1:7;

then 0. V = (Sum (l ! A)) + (Sum (l ! {a})) by A5, VECTSP_6:44

.= (Sum (l ! A)) + ((l . a) * a) by A7, VECTSP_6:17 ;

then A9: (l . a) * a = - (Sum (l ! A)) by ALGSTR_0:def 13;

A10: (- ((l . a) ")) * (l ! A) is Linear_Combination of A by VECTSP_6:31;

now :: thesis: not l . a <> 0. F

then A11:
a nin Carrier l
by VECTSP_6:2;assume
l . a <> 0. F
; :: thesis: contradiction

then a = ((l . a) ") * (- (Sum (l ! A))) by A9, VECTSP_1:20

.= - (((l . a) ") * (Sum (l ! A))) by VECTSP_1:22

.= (- ((l . a) ")) * (Sum (l ! A)) by VECTSP_1:21

.= Sum ((- ((l . a) ")) * (l ! A)) by VECTSP_6:45 ;

hence contradiction by A3, A2, A10; :: thesis: verum

end;then a = ((l . a) ") * (- (Sum (l ! A))) by A9, VECTSP_1:20

.= - (((l . a) ") * (Sum (l ! A))) by VECTSP_1:22

.= (- ((l . a) ")) * (Sum (l ! A)) by VECTSP_1:21

.= Sum ((- ((l . a) ")) * (l ! A)) by VECTSP_6:45 ;

hence contradiction by A3, A2, A10; :: thesis: verum

A12: Carrier l c= A \/ {a} by VECTSP_6:def 4;

Carrier l c= A by A11, A12, ZFMISC_1:136;

then l is Linear_Combination of A by VECTSP_6:def 4;

hence contradiction by A1, A5, A6, VECTSP_7:def 1; :: thesis: verum