let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds
(center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)
let v be VECTOR of V; :: thesis: for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds
(center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)
let Af be finite Subset of V; :: thesis: ( v in Af & not Af \ {v} is empty implies (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) )
set Av = Af \ {v};
assume that
A1: v in Af and
A2: not Af \ {v} is empty ; :: thesis: (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)
consider L3 being Linear_Combination of {v} such that
A3: L3 . v = jj / (card Af) by RLVECT_4:37;
consider L1 being Linear_Combination of Af \ {v} such that
A4: Sum L1 = (1 / (card (Af \ {v}))) * (Sum (Af \ {v})) and
sum L1 = (1 / (card (Af \ {v}))) * (card (Af \ {v})) and
A5: L1 = (ZeroLC V) +* ((Af \ {v}) --> (1 / (card (Af \ {v})))) by Th15;
consider L2 being Linear_Combination of Af such that
A6: Sum L2 = (1 / (card Af)) * (Sum Af) and
sum L2 = (1 / (card Af)) * (card Af) and
A7: L2 = (ZeroLC V) +* (Af --> (1 / (card Af))) by Th15;
A8: Sum L1 = (center_of_mass V) . (Af \ {v}) by A2, A4, Def2;
for u being Element of V holds L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u
proof
let u be Element of V; :: thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u
A9: ( (((1 - (1 / (card Af))) * L1) + L3) . u = (((1 - (1 / (card Af))) * L1) . u) + (L3 . u) & ((1 - (1 / (card Af))) * L1) . u = (1 - (1 / (card Af))) * (L1 . u) ) by RLVECT_2:def 10, RLVECT_2:def 11;
A10: (ZeroLC V) . u = 0 by RLVECT_2:20;
A11: Carrier L3 c= {v} by RLVECT_2:def 6;
A12: dom (Af --> (1 / (card Af))) = Af ;
A13: dom ((Af \ {v}) --> (1 / (card (Af \ {v})))) = Af \ {v} ;
per cases ( not u in Af or v = u or ( u in Af & u <> v ) ) ;
suppose A14: not u in Af ; :: thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u
then not u in Carrier L3 by A1, A11, TARSKI:def 1;
then A15: L3 . u = 0 ;
not u in Af \ {v} by A14, ZFMISC_1:56;
then L1 . u = 0 by A5, A10, A13, FUNCT_4:11;
hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A7, A9, A10, A12, A14, A15, FUNCT_4:11; :: thesis: verum
end;
suppose A16: v = u ; :: thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u
then not u in Af \ {v} by ZFMISC_1:56;
then A17: L1 . u = 0 by A5, A10, A13, FUNCT_4:11;
L2 . u = (Af --> (1 / (card Af))) . v by A1, A7, A12, A16, FUNCT_4:13;
hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A1, A3, A9, A16, A17, FUNCOP_1:7; :: thesis: verum
end;
suppose A18: ( u in Af & u <> v ) ; :: thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u
then L2 . u = (Af --> (1 / (card Af))) . u by A7, A12, FUNCT_4:13;
then A19: L2 . u = 1 / (card Af) by A18, FUNCOP_1:7;
not u in Carrier L3 by A11, A18, TARSKI:def 1;
then A20: L3 . u = 0 ;
( not v in Af \ {v} & (Af \ {v}) \/ {v} = Af ) by A1, ZFMISC_1:56, ZFMISC_1:116;
then A21: card Af = (card (Af \ {v})) + 1 by CARD_2:41;
1 - (1 / (card Af)) = ((card Af) / (card Af)) - (1 / (card Af)) by A1, XCMPLX_1:60
.= ((card Af) - 1) / (card Af) by XCMPLX_1:120
.= (card (Af \ {v})) / (card Af) by A21 ;
then A22: (1 - (1 / (card Af))) * (1 / (card (Af \ {v}))) = ((card (Af \ {v})) / (card Af)) / (card (Af \ {v})) by XCMPLX_1:99
.= ((card (Af \ {v})) / (card (Af \ {v}))) / (card Af) by XCMPLX_1:48
.= 1 / (card Af) by A2, XCMPLX_1:60 ;
A23: u in Af \ {v} by A18, ZFMISC_1:56;
then L1 . u = ((Af \ {v}) --> (1 / (card (Af \ {v})))) . u by A5, A13, FUNCT_4:13;
hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A9, A19, A20, A22, A23, FUNCOP_1:7; :: thesis: verum
end;
end;
end;
then A24: L2 = ((1 - (1 / (card Af))) * L1) + L3 ;
dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def 1;
then A25: Af \ {v} in dom (center_of_mass V) by A2, ZFMISC_1:56;
Sum L2 = (center_of_mass V) . Af by A1, A6, Def2;
hence (center_of_mass V) . Af = (Sum ((1 - (1 / (card Af))) * L1)) + (Sum L3) by A24, RLVECT_3:1
.= ((1 - (1 / (card Af))) * (Sum L1)) + (Sum L3) by RLVECT_3:2
.= ((1 - (1 / (card Af))) * (Sum L1)) + ((1 / (card Af)) * v) by A3, RLVECT_2:32
.= ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) by A8, A25, PARTFUN1:def 6 ;
:: thesis: verum