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 )
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 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})
proof
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;
B c= A \ {p} by A2, A5, ZFMISC_1:34;
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;
assume A20: for B being Subset of V st B c= A & Affin A = Affin B holds
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
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;
then reconsider pA0 = ((- p) + A) \ {(0. V)} as Subset 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