let V be RealLinearSpace; for v being VECTOR of V
for Af being finite Subset of V
for I being affinely-independent Subset of V st Af c= I & v in Af holds
(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V
let v be VECTOR of V; for Af being finite Subset of V
for I being affinely-independent Subset of V st Af c= I & v in Af holds
(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V
let Af be finite Subset of V; for I being affinely-independent Subset of V st Af c= I & v in Af holds
(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V
let I be affinely-independent Subset of V; ( Af c= I & v in Af implies (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V )
assume that
A1:
Af c= I
and
A2:
v in Af
; (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V
set Iv = I \ {v};
set Av = Af \ {v};
A3:
(I \ {v}) \/ {v} = I
by A1, A2, ZFMISC_1:116;
set BA = (center_of_mass V) /. Af;
A4:
(center_of_mass V) . Af = (1 / (card Af)) * (Sum Af)
by A2, Def2;
A5:
dom (center_of_mass V) = BOOL the carrier of V
by FUNCT_2:def 1;
then
Af in dom (center_of_mass V)
by A2, ZFMISC_1:56;
then A6:
(center_of_mass V) . Af = (center_of_mass V) /. Af
by PARTFUN1:def 6;
per cases
( Af = {v} or Af <> {v} )
;
suppose A7:
Af <> {v}
;
(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of VA8:
not
(center_of_mass V) /. Af in Affin (I \ {v})
proof
A9:
not
Af \ {v} is
empty
then
Af \ {v} in dom (center_of_mass V)
by A5, ZFMISC_1:56;
then A10:
(center_of_mass V) . (Af \ {v}) = (center_of_mass V) /. (Af \ {v})
by PARTFUN1:def 6;
Af \ {v} c= I \ {v}
by A1, XBOOLE_1:33;
then A11:
Affin (Af \ {v}) c= Affin (I \ {v})
by RLAFFIN1:52;
reconsider c =
card Af as
Real ;
A12:
c / c = c * (1 / c)
by XCMPLX_1:99;
(
conv (Af \ {v}) c= Affin (Af \ {v}) &
(center_of_mass V) . (Af \ {v}) in conv (Af \ {v}) )
by A9, Th16, RLAFFIN1:65;
then A13:
(center_of_mass V) . (Af \ {v}) in Affin (Af \ {v})
;
assume
(center_of_mass V) /. Af in Affin (I \ {v})
;
contradiction
then A14:
( not
v in I \ {v} &
((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af)) in Affin (I \ {v}) )
by A10, A11, A13, RUSUB_4:def 4, ZFMISC_1:56;
((center_of_mass V) /. Af) - ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))) = (((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / c) * v)) - ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v})))
by A2, A6, A9, Th22;
then A15:
(1 / c) * v =
((center_of_mass V) /. Af) - ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v})))
by RLVECT_4:1
.=
((center_of_mass V) /. Af) + (- ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))))
by RLVECT_1:def 11
.=
((- (1 - (1 / c))) * ((center_of_mass V) /. (Af \ {v}))) + ((center_of_mass V) /. Af)
by RLVECT_4:3
;
A16:
1
= c / c
by A2, XCMPLX_1:60;
((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af)) =
1
* (((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af)))
by RLVECT_1:def 8
.=
c * ((1 / c) * (((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af))))
by A12, A16, RLVECT_1:def 7
.=
c * (((1 / c) * ((1 - c) * ((center_of_mass V) /. (Af \ {v})))) + ((1 / c) * (c * ((center_of_mass V) /. Af))))
by RLVECT_1:def 5
.=
c * (((1 / c) * ((1 - c) * ((center_of_mass V) /. (Af \ {v})))) + (1 * ((center_of_mass V) /. Af)))
by A12, A16, RLVECT_1:def 7
.=
c * (((1 / c) * ((1 - c) * ((center_of_mass V) /. (Af \ {v})))) + ((center_of_mass V) /. Af))
by RLVECT_1:def 8
.=
c * ((((1 / c) * (1 - c)) * ((center_of_mass V) /. (Af \ {v}))) + ((center_of_mass V) /. Af))
by RLVECT_1:def 7
.=
1
* v
by A16, A15, A12, RLVECT_1:def 7
.=
v
by RLVECT_1:def 8
;
hence
contradiction
by A3, A14, Th27;
verum
end;
I \ {v} is
affinely-independent
by RLAFFIN1:43, XBOOLE_1:36;
hence
(I \ {v}) \/ {((center_of_mass V) . Af)} is
affinely-independent Subset of
V
by A6, A8, Th27;
verum end;