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

( A is affinely-independent iff for B being Subset of V st B c= A & Affin A = Affin B holds

A = B )

let A be Subset of V; :: thesis: ( A is affinely-independent iff for B being Subset of V st B c= A & Affin A = Affin B holds

A = B )

A = B ; :: thesis: A is affinely-independent

assume not A is affinely-independent ; :: thesis: contradiction

then consider p being Element of V such that

A21: p in A and

A22: not ((- p) + A) \ {(0. V)} is linearly-independent by Th41;

set L = Lin (((- p) + A) \ {(0. V)});

((- p) + A) \ {(0. V)} c= the carrier of (Lin (((- p) + A) \ {(0. V)}))

(- p) + p = 0. V by RLVECT_1:5;

then A23: 0. V in (- p) + A by A21;

then A24: pA0 \/ {(0. V)} = (- p) + A by ZFMISC_1:116;

Lin pA0 = Lin (((- p) + A) \ {(0. V)}) by RLVECT_5:20;

then consider b being Subset of (Lin (((- p) + A) \ {(0. V)})) such that

A25: b c= pA0 and

A26: b is linearly-independent and

A27: Lin b = Lin (((- p) + A) \ {(0. V)}) by RLVECT_3:25;

reconsider B = b as linearly-independent Subset of V by A26, RLVECT_5:14;

A28: B \/ {(0. V)} c= pA0 \/ {(0. V)} by A25, XBOOLE_1:9;

0. V in {(0. V)} by TARSKI:def 1;

then ( p + (0. V) = p & 0. V in B \/ {(0. V)} ) by XBOOLE_0:def 3;

then A29: p in p + (B \/ {(0. V)}) ;

A30: p + (B \/ {(0. V)}) c= Affin (p + (B \/ {(0. V)})) by Lm7;

A31: p + ((- p) + A) = (p + (- p)) + A by Th5

.= (0. V) + A by RLVECT_1:5

.= A by Th6 ;

A32: (- p) + (p + (B \/ {(0. V)})) = ((- p) + p) + (B \/ {(0. V)}) by Th5

.= (0. V) + (B \/ {(0. V)}) by RLVECT_1:5

.= B \/ {(0. V)} by Th6 ;

A c= Affin A by Lm7;

then Affin A = p + (Up (Lin ((- p) + A))) by A21, Th57

.= p + (Up (Lin ((((- p) + A) \ {(0. V)}) \/ {(0. V)}))) by A23, ZFMISC_1:116

.= p + (Up (Lin (((- p) + A) \ {(0. V)}))) by Lm9

.= p + (Up (Lin B)) by A27, RLVECT_5:20

.= p + (Up (Lin ((- p) + (p + (B \/ {(0. V)}))))) by A32, Lm9

.= Affin (p + (B \/ {(0. V)})) by A29, A30, Th57 ;

then pA0 = (B \/ {(0. V)}) \ {(0. V)} by A20, A24, A28, A31, A32, RLTOPSP1:8

.= B by RLVECT_3:6, ZFMISC_1:117 ;

hence contradiction by A22; :: thesis: verum

( A is affinely-independent iff for B being Subset of V st B c= A & Affin A = Affin B holds

A = B )

let A be Subset of V; :: thesis: ( A is affinely-independent iff for B being Subset of V st B c= A & Affin A = Affin B holds

A = B )

hereby :: thesis: ( ( for B being Subset of V st B c= A & Affin A = Affin B holds

A = B ) implies A is affinely-independent )

assume A20:
for B being Subset of V st B c= A & Affin A = Affin B holds A = B ) implies A is affinely-independent )

assume A1:
A is affinely-independent
; :: thesis: for B being Subset of V st B c= A & Affin A = Affin B holds

not A <> B

let B be Subset of V; :: thesis: ( B c= A & Affin A = Affin B implies not A <> B )

assume that

A2: B c= A and

A3: Affin A = Affin B ; :: thesis: not A <> B

assume A <> B ; :: thesis: contradiction

then B c< A by A2;

then consider p being object such that

A4: p in A and

A5: not p in B by XBOOLE_0:6;

reconsider p = p as Element of V by A4;

A6: A \ {p} c= Affin (A \ {p}) by Lm7;

not B is empty by A3, A4;

then consider q being object such that

A7: q in B ;

reconsider q = q as Element of V by A7;

- (- q) = q ;

then A8: (- q) + p <> 0. V by A5, A7, RLVECT_1:def 10;

set qA0 = ((- q) + A) \ {(0. V)};

(- q) + p in (- q) + A by A4;

then A9: (- q) + p in ((- q) + A) \ {(0. V)} by A8, ZFMISC_1:56;

((- q) + A) \ {(0. V)} is linearly-independent by A1, A2, A7, Th41;

then A10: not (- q) + p in Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)}) by A9, RLVECT_5:17;

A11: q + ((- q) + p) = (q + (- q)) + p by RLVECT_1:def 3

.= (0. V) + p by RLVECT_1:5

.= p ;

(- q) + q = 0. V by RLVECT_1:5;

then 0. V in (- q) + A by A2, A7;

then A12: 0. V in ((- q) + A) \ {((- q) + p)} by A8, ZFMISC_1:56;

(((- q) + A) \ {(0. V)}) \ {((- q) + p)} = ((- q) + A) \ ({(0. V)} \/ {((- q) + p)}) by XBOOLE_1:41

.= (((- q) + A) \ {((- q) + p)}) \ {(0. V)} by XBOOLE_1:41 ;

then A13: Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)}) = Lin (((((- q) + A) \ {((- q) + p)}) \ {(0. V)}) \/ {(0. V)}) by Lm9

.= Lin (((- q) + A) \ {((- q) + p)}) by A12, ZFMISC_1:116

.= Lin (((- q) + A) \ ((- q) + {p})) by Lm3

.= Lin ((- q) + (A \ {p})) by Lm2 ;

q in A \ {p} by A2, A5, A7, ZFMISC_1:56;

then A14: Affin (A \ {p}) = q + (Up (Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)}))) by A6, A13, Th57;

A15: not p in Affin (A \ {p})

then A18: Affin B c= Affin (A \ {p}) by Th52;

Affin (A \ {p}) c= Affin A by Th52, XBOOLE_1:36;

then A19: Affin A = Affin (A \ {p}) by A3, A18;

A c= Affin A by Lm7;

hence contradiction by A4, A15, A19; :: thesis: verum

end;not A <> B

let B be Subset of V; :: thesis: ( B c= A & Affin A = Affin B implies not A <> B )

assume that

A2: B c= A and

A3: Affin A = Affin B ; :: thesis: not A <> B

assume A <> B ; :: thesis: contradiction

then B c< A by A2;

then consider p being object such that

A4: p in A and

A5: not p in B by XBOOLE_0:6;

reconsider p = p as Element of V by A4;

A6: A \ {p} c= Affin (A \ {p}) by Lm7;

not B is empty by A3, A4;

then consider q being object such that

A7: q in B ;

reconsider q = q as Element of V by A7;

- (- q) = q ;

then A8: (- q) + p <> 0. V by A5, A7, RLVECT_1:def 10;

set qA0 = ((- q) + A) \ {(0. V)};

(- q) + p in (- q) + A by A4;

then A9: (- q) + p in ((- q) + A) \ {(0. V)} by A8, ZFMISC_1:56;

((- q) + A) \ {(0. V)} is linearly-independent by A1, A2, A7, Th41;

then A10: not (- q) + p in Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)}) by A9, RLVECT_5:17;

A11: q + ((- q) + p) = (q + (- q)) + p by RLVECT_1:def 3

.= (0. V) + p by RLVECT_1:5

.= p ;

(- q) + q = 0. V by RLVECT_1:5;

then 0. V in (- q) + A by A2, A7;

then A12: 0. V in ((- q) + A) \ {((- q) + p)} by A8, ZFMISC_1:56;

(((- q) + A) \ {(0. V)}) \ {((- q) + p)} = ((- q) + A) \ ({(0. V)} \/ {((- q) + p)}) by XBOOLE_1:41

.= (((- q) + A) \ {((- q) + p)}) \ {(0. V)} by XBOOLE_1:41 ;

then A13: Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)}) = Lin (((((- q) + A) \ {((- q) + p)}) \ {(0. V)}) \/ {(0. V)}) by Lm9

.= Lin (((- q) + A) \ {((- q) + p)}) by A12, ZFMISC_1:116

.= Lin (((- q) + A) \ ((- q) + {p})) by Lm3

.= Lin ((- q) + (A \ {p})) by Lm2 ;

q in A \ {p} by A2, A5, A7, ZFMISC_1:56;

then A14: Affin (A \ {p}) = q + (Up (Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)}))) by A6, A13, Th57;

A15: not p in Affin (A \ {p})

proof

B c= A \ {p}
by A2, A5, ZFMISC_1:34;
assume
p in Affin (A \ {p})
; :: thesis: contradiction

then consider v being Element of V such that

A16: p = q + v and

A17: v in Up (Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)})) by A14;

(- q) + p = v by A11, A16, RLVECT_1:8;

hence contradiction by A10, A17; :: thesis: verum

end;then consider v being Element of V such that

A16: p = q + v and

A17: v in Up (Lin ((((- q) + A) \ {(0. V)}) \ {((- q) + p)})) by A14;

(- q) + p = v by A11, A16, RLVECT_1:8;

hence contradiction by A10, A17; :: thesis: verum

then A18: Affin B c= Affin (A \ {p}) by Th52;

Affin (A \ {p}) c= Affin A by Th52, XBOOLE_1:36;

then A19: Affin A = Affin (A \ {p}) by A3, A18;

A c= Affin A by Lm7;

hence contradiction by A4, A15, A19; :: thesis: verum

A = B ; :: thesis: A is affinely-independent

assume not A is affinely-independent ; :: thesis: contradiction

then consider p being Element of V such that

A21: p in A and

A22: not ((- p) + A) \ {(0. V)} is linearly-independent by Th41;

set L = Lin (((- p) + A) \ {(0. V)});

((- p) + A) \ {(0. V)} c= the carrier of (Lin (((- p) + A) \ {(0. V)}))

proof

then reconsider pA0 = ((- p) + A) \ {(0. V)} as Subset of (Lin (((- p) + A) \ {(0. V)})) ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((- p) + A) \ {(0. V)} or x in the carrier of (Lin (((- p) + A) \ {(0. V)})) )

assume x in ((- p) + A) \ {(0. V)} ; :: thesis: x in the carrier of (Lin (((- p) + A) \ {(0. V)}))

then x in Lin (((- p) + A) \ {(0. V)}) by RLVECT_3:15;

hence x in the carrier of (Lin (((- p) + A) \ {(0. V)})) ; :: thesis: verum

end;assume x in ((- p) + A) \ {(0. V)} ; :: thesis: x in the carrier of (Lin (((- p) + A) \ {(0. V)}))

then x in Lin (((- p) + A) \ {(0. V)}) by RLVECT_3:15;

hence x in the carrier of (Lin (((- p) + A) \ {(0. V)})) ; :: thesis: verum

(- p) + p = 0. V by RLVECT_1:5;

then A23: 0. V in (- p) + A by A21;

then A24: pA0 \/ {(0. V)} = (- p) + A by ZFMISC_1:116;

Lin pA0 = Lin (((- p) + A) \ {(0. V)}) by RLVECT_5:20;

then consider b being Subset of (Lin (((- p) + A) \ {(0. V)})) such that

A25: b c= pA0 and

A26: b is linearly-independent and

A27: Lin b = Lin (((- p) + A) \ {(0. V)}) by RLVECT_3:25;

reconsider B = b as linearly-independent Subset of V by A26, RLVECT_5:14;

A28: B \/ {(0. V)} c= pA0 \/ {(0. V)} by A25, XBOOLE_1:9;

0. V in {(0. V)} by TARSKI:def 1;

then ( p + (0. V) = p & 0. V in B \/ {(0. V)} ) by XBOOLE_0:def 3;

then A29: p in p + (B \/ {(0. V)}) ;

A30: p + (B \/ {(0. V)}) c= Affin (p + (B \/ {(0. V)})) by Lm7;

A31: p + ((- p) + A) = (p + (- p)) + A by Th5

.= (0. V) + A by RLVECT_1:5

.= A by Th6 ;

A32: (- p) + (p + (B \/ {(0. V)})) = ((- p) + p) + (B \/ {(0. V)}) by Th5

.= (0. V) + (B \/ {(0. V)}) by RLVECT_1:5

.= B \/ {(0. V)} by Th6 ;

A c= Affin A by Lm7;

then Affin A = p + (Up (Lin ((- p) + A))) by A21, Th57

.= p + (Up (Lin ((((- p) + A) \ {(0. V)}) \/ {(0. V)}))) by A23, ZFMISC_1:116

.= p + (Up (Lin (((- p) + A) \ {(0. V)}))) by Lm9

.= p + (Up (Lin B)) by A27, RLVECT_5:20

.= p + (Up (Lin ((- p) + (p + (B \/ {(0. V)}))))) by A32, Lm9

.= Affin (p + (B \/ {(0. V)})) by A29, A30, Th57 ;

then pA0 = (B \/ {(0. V)}) \ {(0. V)} by A20, A24, A28, A31, A32, RLTOPSP1:8

.= B by RLVECT_3:6, ZFMISC_1:117 ;

hence contradiction by A22; :: thesis: verum