let V be RealLinearSpace; 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; 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; ( 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
; (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;
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
;
L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . uthen
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;
verum end; suppose A16:
v = u
;
L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . uthen
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;
verum end; suppose A18:
(
u in Af &
u <> v )
;
L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . uthen
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;
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
;
verum