let V be RealLinearSpace; :: thesis: for F being c=-linear Subset-Family of V st union F is finite & union F is affinely-independent holds

(center_of_mass V) .: F is affinely-independent Subset of V

set B = center_of_mass V;

defpred S_{1}[ Nat] means for k being Nat st k <= $1 holds

for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V;

let S be c=-linear Subset-Family of V; :: thesis: ( union S is finite & union S is affinely-independent implies (center_of_mass V) .: S is affinely-independent Subset of V )

A1: dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def 1;

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A34, A2);

assume A41: ( union S is finite & union S is affinely-independent ) ; :: thesis: (center_of_mass V) .: S is affinely-independent Subset of V

then card (union S) is Nat ;

hence (center_of_mass V) .: S is affinely-independent Subset of V by A40, A41; :: thesis: verum

(center_of_mass V) .: F is affinely-independent Subset of V

set B = center_of_mass V;

defpred S

for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V;

let S be c=-linear Subset-Family of V; :: thesis: ( union S is finite & union S is affinely-independent implies (center_of_mass V) .: S is affinely-independent Subset of V )

A1: dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def 1;

A2: for n being Nat st S

S

proof

A34:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let k be Nat; :: thesis: ( k <= n + 1 implies for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V )

assume A4: k <= n + 1 ; :: thesis: for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V

end;assume A3: S

let k be Nat; :: thesis: ( k <= n + 1 implies for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V )

assume A4: k <= n + 1 ; :: thesis: for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V

per cases
( k <= n or k = n + 1 )
by A4, NAT_1:8;

end;

suppose
k <= n
; :: thesis: for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V

(center_of_mass V) .: S is affinely-independent Subset of V

hence
for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V by A3; :: thesis: verum

end;(center_of_mass V) .: S is affinely-independent Subset of V by A3; :: thesis: verum

suppose A5:
k = n + 1
; :: thesis: for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V

(center_of_mass V) .: S is affinely-independent Subset of V

let S be c=-linear Subset-Family of V; :: thesis: ( card (union S) = k & union S is finite & union S is affinely-independent implies (center_of_mass V) .: S is affinely-independent Subset of V )

assume that

A6: card (union S) = k and

A7: ( union S is finite & union S is affinely-independent ) ; :: thesis: (center_of_mass V) .: S is affinely-independent Subset of V

set U = union S;

A8: S c= bool (union S) by ZFMISC_1:82;

set SU = S \ {(union S)};

A9: union (S \ {(union S)}) c= union S by XBOOLE_1:36, ZFMISC_1:77;

then reconsider Usu = union (S \ {(union S)}) as finite set by A7;

A10: S \ {(union S)} c= S by XBOOLE_1:36;

A11: union (S \ {(union S)}) <> union S

then consider v being object such that

A13: v in union S and

A14: not v in union (S \ {(union S)}) by XBOOLE_0:6;

reconsider v = v as Element of V by A13;

A15: ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} is affinely-independent Subset of V by A7, A13, Th28;

not union S is empty by A5, A6;

then A16: union S in dom (center_of_mass V) by A1, ZFMISC_1:56;

(center_of_mass V) . (union S) in {((center_of_mass V) . (union S))} by TARSKI:def 1;

then (center_of_mass V) . (union S) in ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} by XBOOLE_0:def 3;

then reconsider BU = (center_of_mass V) . (union S) as Element of V by A15;

not S is empty by A5, A6, ZFMISC_1:2;

then (S \ {(union S)}) \/ {(union S)} = S by A7, A8, SIMPLEX0:9, ZFMISC_1:116;

then A17: (center_of_mass V) .: S = ((center_of_mass V) .: (S \ {(union S)})) \/ ((center_of_mass V) .: {(union S)}) by RELAT_1:120

.= ((center_of_mass V) .: (S \ {(union S)})) \/ (Im ((center_of_mass V),(union S))) by RELAT_1:def 16

.= ((center_of_mass V) .: (S \ {(union S)})) \/ {BU} by A16, FUNCT_1:59 ;

A18: {v} c= union S by A13, ZFMISC_1:31;

A19: card {v} = 1 by CARD_1:30;

end;assume that

A6: card (union S) = k and

A7: ( union S is finite & union S is affinely-independent ) ; :: thesis: (center_of_mass V) .: S is affinely-independent Subset of V

set U = union S;

A8: S c= bool (union S) by ZFMISC_1:82;

set SU = S \ {(union S)};

A9: union (S \ {(union S)}) c= union S by XBOOLE_1:36, ZFMISC_1:77;

then reconsider Usu = union (S \ {(union S)}) as finite set by A7;

A10: S \ {(union S)} c= S by XBOOLE_1:36;

A11: union (S \ {(union S)}) <> union S

proof

then
union (S \ {(union S)}) c< union S
by A9;
assume A12:
union (S \ {(union S)}) = union S
; :: thesis: contradiction

then not S \ {(union S)} is empty by A5, A6, ZFMISC_1:2;

then union (S \ {(union S)}) in S \ {(union S)} by A7, A10, A8, SIMPLEX0:9;

hence contradiction by A12, ZFMISC_1:56; :: thesis: verum

end;then not S \ {(union S)} is empty by A5, A6, ZFMISC_1:2;

then union (S \ {(union S)}) in S \ {(union S)} by A7, A10, A8, SIMPLEX0:9;

hence contradiction by A12, ZFMISC_1:56; :: thesis: verum

then consider v being object such that

A13: v in union S and

A14: not v in union (S \ {(union S)}) by XBOOLE_0:6;

reconsider v = v as Element of V by A13;

A15: ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} is affinely-independent Subset of V by A7, A13, Th28;

not union S is empty by A5, A6;

then A16: union S in dom (center_of_mass V) by A1, ZFMISC_1:56;

(center_of_mass V) . (union S) in {((center_of_mass V) . (union S))} by TARSKI:def 1;

then (center_of_mass V) . (union S) in ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} by XBOOLE_0:def 3;

then reconsider BU = (center_of_mass V) . (union S) as Element of V by A15;

not S is empty by A5, A6, ZFMISC_1:2;

then (S \ {(union S)}) \/ {(union S)} = S by A7, A8, SIMPLEX0:9, ZFMISC_1:116;

then A17: (center_of_mass V) .: S = ((center_of_mass V) .: (S \ {(union S)})) \/ ((center_of_mass V) .: {(union S)}) by RELAT_1:120

.= ((center_of_mass V) .: (S \ {(union S)})) \/ (Im ((center_of_mass V),(union S))) by RELAT_1:def 16

.= ((center_of_mass V) .: (S \ {(union S)})) \/ {BU} by A16, FUNCT_1:59 ;

A18: {v} c= union S by A13, ZFMISC_1:31;

A19: card {v} = 1 by CARD_1:30;

per cases
( n = 0 or n > 0 )
;

end;

suppose
n = 0
; :: thesis: (center_of_mass V) .: S is affinely-independent Subset of V

then A20:
union S = {v}
by A5, A6, A7, A18, A19, CARD_2:102;

(S \ {(union S)}) /\ (dom (center_of_mass V)) = {}

.= {} ;

hence (center_of_mass V) .: S is affinely-independent Subset of V by A17; :: thesis: verum

end;(S \ {(union S)}) /\ (dom (center_of_mass V)) = {}

proof

then (center_of_mass V) .: (S \ {(union S)}) =
(center_of_mass V) .: {}
by RELAT_1:112
assume
(S \ {(union S)}) /\ (dom (center_of_mass V)) <> {}
; :: thesis: contradiction

then consider x being object such that

A21: x in (S \ {(union S)}) /\ (dom (center_of_mass V)) by XBOOLE_0:def 1;

reconsider x = x as set by TARSKI:1;

x in S \ {(union S)} by A21, XBOOLE_0:def 4;

then A22: x c= union (S \ {(union S)}) by ZFMISC_1:74;

then x c= union S by A9;

then A23: ( x = union S or x = {} ) by A20, ZFMISC_1:33;

not v in x by A14, A22;

hence contradiction by A20, A21, A23, TARSKI:def 1, ZFMISC_1:56; :: thesis: verum

end;then consider x being object such that

A21: x in (S \ {(union S)}) /\ (dom (center_of_mass V)) by XBOOLE_0:def 1;

reconsider x = x as set by TARSKI:1;

x in S \ {(union S)} by A21, XBOOLE_0:def 4;

then A22: x c= union (S \ {(union S)}) by ZFMISC_1:74;

then x c= union S by A9;

then A23: ( x = union S or x = {} ) by A20, ZFMISC_1:33;

not v in x by A14, A22;

hence contradiction by A20, A21, A23, TARSKI:def 1, ZFMISC_1:56; :: thesis: verum

.= {} ;

hence (center_of_mass V) .: S is affinely-independent Subset of V by A17; :: thesis: verum

suppose A24:
n > 0
; :: thesis: (center_of_mass V) .: S is affinely-independent Subset of V

reconsider u = union S as finite set by A7;

A25: Usu c= u by XBOOLE_1:36, ZFMISC_1:77;

then card Usu <= n + 1 by A5, A6, NAT_1:43;

then card Usu < n + 1 by A5, A6, A11, A25, CARD_2:102, XXREAL_0:1;

then A26: card Usu <= n by NAT_1:13;

( union (S \ {(union S)}) c= (union S) \ {v} & (union S) \ {v} c= ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} ) by A9, A14, XBOOLE_1:7, ZFMISC_1:34;

then union (S \ {(union S)}) is affinely-independent by A15, RLAFFIN1:43, XBOOLE_1:1;

then reconsider BSU = (center_of_mass V) .: (S \ {(union S)}) as affinely-independent Subset of V by A3, A10, A26;

BSU c= Affin ((union S) \ {v})

card (union S) <> 1 by A5, A6, A24;

then not BU in union S by A7, Th19;

then not BU in (union S) \ {v} by XBOOLE_0:def 5;

then not BU in Affin BSU by A15, A33, Th27;

hence (center_of_mass V) .: S is affinely-independent Subset of V by A17, Th27; :: thesis: verum

end;A25: Usu c= u by XBOOLE_1:36, ZFMISC_1:77;

then card Usu <= n + 1 by A5, A6, NAT_1:43;

then card Usu < n + 1 by A5, A6, A11, A25, CARD_2:102, XXREAL_0:1;

then A26: card Usu <= n by NAT_1:13;

( union (S \ {(union S)}) c= (union S) \ {v} & (union S) \ {v} c= ((union S) \ {v}) \/ {((center_of_mass V) . (union S))} ) by A9, A14, XBOOLE_1:7, ZFMISC_1:34;

then union (S \ {(union S)}) is affinely-independent by A15, RLAFFIN1:43, XBOOLE_1:1;

then reconsider BSU = (center_of_mass V) .: (S \ {(union S)}) as affinely-independent Subset of V by A3, A10, A26;

BSU c= Affin ((union S) \ {v})

proof

then A33:
Affin BSU c= Affin ((union S) \ {v})
by RLAFFIN1:51;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in BSU or y in Affin ((union S) \ {v}) )

assume y in BSU ; :: thesis: y in Affin ((union S) \ {v})

then consider x being object such that

A27: x in dom (center_of_mass V) and

A28: x in S \ {(union S)} and

A29: (center_of_mass V) . x = y by FUNCT_1:def 6;

reconsider x = x as non empty Subset of V by A27, ZFMISC_1:56;

x in S by A28, XBOOLE_0:def 5;

then A30: x c= union S by ZFMISC_1:74;

x c= union (S \ {(union S)}) by A28, ZFMISC_1:74;

then not v in x by A14;

then x c= (union S) \ {v} by A30, ZFMISC_1:34;

then A31: conv x c= conv ((union S) \ {v}) by RLTOPSP1:20;

y in conv x by A7, A29, A30, Th16;

then A32: y in conv ((union S) \ {v}) by A31;

conv ((union S) \ {v}) c= Affin ((union S) \ {v}) by RLAFFIN1:65;

hence y in Affin ((union S) \ {v}) by A32; :: thesis: verum

end;assume y in BSU ; :: thesis: y in Affin ((union S) \ {v})

then consider x being object such that

A27: x in dom (center_of_mass V) and

A28: x in S \ {(union S)} and

A29: (center_of_mass V) . x = y by FUNCT_1:def 6;

reconsider x = x as non empty Subset of V by A27, ZFMISC_1:56;

x in S by A28, XBOOLE_0:def 5;

then A30: x c= union S by ZFMISC_1:74;

x c= union (S \ {(union S)}) by A28, ZFMISC_1:74;

then not v in x by A14;

then x c= (union S) \ {v} by A30, ZFMISC_1:34;

then A31: conv x c= conv ((union S) \ {v}) by RLTOPSP1:20;

y in conv x by A7, A29, A30, Th16;

then A32: y in conv ((union S) \ {v}) by A31;

conv ((union S) \ {v}) c= Affin ((union S) \ {v}) by RLAFFIN1:65;

hence y in Affin ((union S) \ {v}) by A32; :: thesis: verum

card (union S) <> 1 by A5, A6, A24;

then not BU in union S by A7, Th19;

then not BU in (union S) \ {v} by XBOOLE_0:def 5;

then not BU in Affin BSU by A15, A33, Th27;

hence (center_of_mass V) .: S is affinely-independent Subset of V by A17, Th27; :: thesis: verum

proof

A40:
for n being Nat holds S
let k be Nat; :: thesis: ( k <= 0 implies for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V )

assume A35: k <= 0 ; :: thesis: for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V

let S be c=-linear Subset-Family of V; :: thesis: ( card (union S) = k & union S is finite & union S is affinely-independent implies (center_of_mass V) .: S is affinely-independent Subset of V )

assume that

A36: card (union S) = k and

( union S is finite & union S is affinely-independent ) ; :: thesis: (center_of_mass V) .: S is affinely-independent Subset of V

A37: union S = {} by A35, A36;

S /\ (dom (center_of_mass V)) = {}

.= {} ;

hence (center_of_mass V) .: S is affinely-independent Subset of V ; :: thesis: verum

end;(center_of_mass V) .: S is affinely-independent Subset of V )

assume A35: k <= 0 ; :: thesis: for S being c=-linear Subset-Family of V st card (union S) = k & union S is finite & union S is affinely-independent holds

(center_of_mass V) .: S is affinely-independent Subset of V

let S be c=-linear Subset-Family of V; :: thesis: ( card (union S) = k & union S is finite & union S is affinely-independent implies (center_of_mass V) .: S is affinely-independent Subset of V )

assume that

A36: card (union S) = k and

( union S is finite & union S is affinely-independent ) ; :: thesis: (center_of_mass V) .: S is affinely-independent Subset of V

A37: union S = {} by A35, A36;

S /\ (dom (center_of_mass V)) = {}

proof

then (center_of_mass V) .: S =
(center_of_mass V) .: {}
by RELAT_1:112
assume
S /\ (dom (center_of_mass V)) <> {}
; :: thesis: contradiction

then consider x being object such that

A38: x in S /\ (dom (center_of_mass V)) by XBOOLE_0:def 1;

reconsider x = x as set by TARSKI:1;

x in S by A38, XBOOLE_0:def 4;

then A39: x c= {} by A37, ZFMISC_1:74;

x <> {} by A38, ZFMISC_1:56;

hence contradiction by A39; :: thesis: verum

end;then consider x being object such that

A38: x in S /\ (dom (center_of_mass V)) by XBOOLE_0:def 1;

reconsider x = x as set by TARSKI:1;

x in S by A38, XBOOLE_0:def 4;

then A39: x c= {} by A37, ZFMISC_1:74;

x <> {} by A38, ZFMISC_1:56;

hence contradiction by A39; :: thesis: verum

.= {} ;

hence (center_of_mass V) .: S is affinely-independent Subset of V ; :: thesis: verum

assume A41: ( union S is finite & union S is affinely-independent ) ; :: thesis: (center_of_mass V) .: S is affinely-independent Subset of V

then card (union S) is Nat ;

hence (center_of_mass V) .: S is affinely-independent Subset of V by A40, A41; :: thesis: verum