let r be Real; for V being RealLinearSpace
for v being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let V be RealLinearSpace; for v being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let v be VECTOR of V; for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let Affv be finite affinely-independent Subset of V; for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let EV be Enumeration of Affv; for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
set E = EV;
let rE be Enumeration of r * Affv; ( v in Affin Affv & rE = r (#) EV & r <> 0 implies v |-- EV = (r * v) |-- rE )
assume that
A1:
v in Affin Affv
and
A2:
rE = r (#) EV
and
A3:
r <> 0
; v |-- EV = (r * v) |-- rE
set vA = v |-- Affv;
A4:
Carrier (v |-- Affv) c= Affv
by RLVECT_2:def 6;
A5:
r * v in { (r * u) where u is VECTOR of V : u in Affin Affv }
by A1;
A6:
dom rE = dom EV
by A2, VFUNCT_1:def 4;
Carrier (r (*) (v |-- Affv)) = r * (Carrier (v |-- Affv))
by A3, RLAFFIN1:23;
then
Carrier (r (*) (v |-- Affv)) c= r * Affv
by A4, CONVEX1:39;
then reconsider rvA = r (*) (v |-- Affv) as Linear_Combination of r * Affv by RLVECT_2:def 6;
sum (v |-- Affv) = 1
by A1, RLAFFIN1:def 7;
then A7:
sum rvA = 1
by A3, RLAFFIN1:38;
Sum (v |-- Affv) = v
by A1, RLAFFIN1:def 7;
then A8:
Sum rvA = r * v
by RLAFFIN1:40;
A9:
len ((r * v) |-- rE) = card (r * Affv)
by Th16;
A10:
len (v |-- EV) = card Affv
by Th16;
rng EV = Affv
by Def1;
then
len EV = card Affv
by FINSEQ_4:62;
then A11:
dom (v |-- EV) = dom EV
by A10, FINSEQ_3:29;
card Affv = card (r * Affv)
by A3, Th12;
then A12:
dom (v |-- EV) = dom ((r * v) |-- rE)
by A10, A9, FINSEQ_3:29;
Affin (r * Affv) = r * (Affin Affv)
by A3, RLAFFIN1:55;
then
r * v in Affin (r * Affv)
by A5, CONVEX1:def 1;
then A13:
rvA = (r * v) |-- (r * Affv)
by A7, A8, RLAFFIN1:def 7;
now for k being Nat st k in dom (v |-- EV) holds
((r * v) |-- rE) . k = (v |-- EV) . klet k be
Nat;
( k in dom (v |-- EV) implies ((r * v) |-- rE) . k = (v |-- EV) . k )assume A14:
k in dom (v |-- EV)
;
((r * v) |-- rE) . k = (v |-- EV) . kthen A15:
(
(v |-- EV) . k = (v |-- Affv) . (EV . k) &
EV /. k = EV . k )
by A11, FUNCT_1:12, PARTFUN1:def 6;
A16:
rE /. k = r * (EV /. k)
by A2, A11, A6, A14, VFUNCT_1:def 4;
(
((r * v) |-- rE) . k = rvA . (rE . k) &
rE /. k = rE . k )
by A13, A12, A11, A6, A14, FUNCT_1:12, PARTFUN1:def 6;
hence ((r * v) |-- rE) . k =
(v |-- Affv) . ((r ") * (r * (EV /. k)))
by A3, A16, RLAFFIN1:def 2
.=
(v |-- Affv) . (((r ") * r) * (EV /. k))
by RLVECT_1:def 7
.=
(v |-- Affv) . (1 * (EV /. k))
by A3, XCMPLX_0:def 7
.=
(v |-- EV) . k
by A15, RLVECT_1:def 8
;
verum end;
hence
v |-- EV = (r * v) |-- rE
by A12, FINSEQ_1:13; verum