let V be RealLinearSpace; :: thesis: for v being VECTOR of V

for A being Subset of V holds

( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )

let v be VECTOR of V; :: thesis: for A being Subset of V holds

( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )

let A be Subset of V; :: thesis: ( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )

set Av = A \/ {v};

v in {v} by TARSKI:def 1;

then A1: v in A \/ {v} by XBOOLE_0:def 3;

A2: A c= A \/ {v} by XBOOLE_1:7;

A4: A is affinely-independent and

A5: ( v in A or not v in Affin A ) ; :: thesis: A \/ {v} is affinely-independent

for A being Subset of V holds

( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )

let v be VECTOR of V; :: thesis: for A being Subset of V holds

( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )

let A be Subset of V; :: thesis: ( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )

set Av = A \/ {v};

v in {v} by TARSKI:def 1;

then A1: v in A \/ {v} by XBOOLE_0:def 3;

A2: A c= A \/ {v} by XBOOLE_1:7;

hereby :: thesis: ( A is affinely-independent & ( v in A or not v in Affin A ) implies A \/ {v} is affinely-independent )

assume that assume A3:
A \/ {v} is affinely-independent
; :: thesis: ( A is affinely-independent & ( v in A or not v in Affin A ) )

hence A is affinely-independent by Th43, XBOOLE_1:7; :: thesis: ( v in A or not v in Affin A )

( v in Affin A implies v in A )

end;hence A is affinely-independent by Th43, XBOOLE_1:7; :: thesis: ( v in A or not v in Affin A )

( v in Affin A implies v in A )

proof

hence
( v in A or not v in Affin A )
; :: thesis: verum
assume
v in Affin A
; :: thesis: v in A

then {v} c= Affin A by ZFMISC_1:31;

then Affin (A \/ {v}) = Affin A by Th69;

hence v in A by A2, A1, A3, Th58; :: thesis: verum

end;then {v} c= Affin A by ZFMISC_1:31;

then Affin (A \/ {v}) = Affin A by Th69;

hence v in A by A2, A1, A3, Th58; :: thesis: verum

A4: A is affinely-independent and

A5: ( v in A or not v in Affin A ) ; :: thesis: A \/ {v} is affinely-independent

per cases
( v in A or ( not v in Affin A & not v in A ) )
by A5;

end;

suppose A6:
( not v in Affin A & not v in A )
; :: thesis: A \/ {v} is affinely-independent

consider I being affinely-independent Subset of V such that

A7: A c= I and

A8: I c= A \/ {v} and

A9: Affin I = Affin (A \/ {v}) by A2, A4, Th60;

assume A10: not A \/ {v} is affinely-independent ; :: thesis: contradiction

not v in I

A12: A \/ {v} c= Affin (A \/ {v}) by Lm7;

(A \/ {v}) \ {v} = A by A6, ZFMISC_1:117;

then I = A by A7, A11;

hence contradiction by A1, A6, A9, A12; :: thesis: verum

end;A7: A c= I and

A8: I c= A \/ {v} and

A9: Affin I = Affin (A \/ {v}) by A2, A4, Th60;

assume A10: not A \/ {v} is affinely-independent ; :: thesis: contradiction

not v in I

proof

then A11:
I c= (A \/ {v}) \ {v}
by A8, ZFMISC_1:34;
assume
v in I
; :: thesis: contradiction

then {v} c= I by ZFMISC_1:31;

hence contradiction by A7, A10, Th43, XBOOLE_1:8; :: thesis: verum

end;then {v} c= I by ZFMISC_1:31;

hence contradiction by A7, A10, Th43, XBOOLE_1:8; :: thesis: verum

A12: A \/ {v} c= Affin (A \/ {v}) by Lm7;

(A \/ {v}) \ {v} = A by A6, ZFMISC_1:117;

then I = A by A7, A11;

hence contradiction by A1, A6, A9, A12; :: thesis: verum