let V be RealLinearSpace; for v, w being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
let v, w be VECTOR of V; for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
let Affv be finite affinely-independent Subset of V; for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
let EV be Enumeration of Affv; for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E
set E = EV;
let Ev be Enumeration of v + Affv; ( w in Affin Affv & Ev = EV + ((card Affv) |-> v) implies w |-- EV = (v + w) |-- Ev )
assume that
A1:
w in Affin Affv
and
A2:
Ev = EV + ((card Affv) |-> v)
; w |-- EV = (v + w) |-- Ev
set wA = w |-- Affv;
A3:
sum (w |-- Affv) = 1
by A1, RLAFFIN1:def 7;
v + w in { (v + u) where u is VECTOR of V : u in Affin Affv }
by A1;
then A4:
v + w in v + (Affin Affv)
by RUSUB_4:def 8;
rng EV = Affv
by Def1;
then A5:
len EV = card Affv
by FINSEQ_4:62;
then reconsider e = EV, cAv = (card Affv) |-> v as Element of (card Affv) -tuples_on the carrier of V by FINSEQ_2:92;
A6:
( Affin (v + Affv) = v + (Affin Affv) & 1 * v = v )
by RLAFFIN1:53, RLVECT_1:def 8;
( Carrier (v + (w |-- Affv)) = v + (Carrier (w |-- Affv)) & Carrier (w |-- Affv) c= Affv )
by RLAFFIN1:16, RLVECT_2:def 6;
then
Carrier (v + (w |-- Affv)) c= v + Affv
by RLTOPSP1:8;
then reconsider vwA = v + (w |-- Affv) as Linear_Combination of v + Affv by RLVECT_2:def 6;
Sum (w |-- Affv) = w
by A1, RLAFFIN1:def 7;
then A7:
Sum vwA = (1 * v) + w
by A3, RLAFFIN1:39;
A8:
len (w |-- EV) = card Affv
by Th16;
A9:
card Affv = card (v + Affv)
by RLAFFIN1:7;
then
len ((v + w) |-- Ev) = card Affv
by Th16;
then A10:
dom (w |-- EV) = dom ((v + w) |-- Ev)
by A8, FINSEQ_3:29;
rng Ev = v + Affv
by Def1;
then A11:
len Ev = card Affv
by A9, FINSEQ_4:62;
sum vwA = 1
by A3, RLAFFIN1:37;
then A12:
vwA = (v + w) |-- (v + Affv)
by A4, A7, A6, RLAFFIN1:def 7;
now for i being Nat st i in dom (w |-- EV) holds
((v + w) |-- Ev) . i = (w |-- EV) . ilet i be
Nat;
( i in dom (w |-- EV) implies ((v + w) |-- Ev) . i = (w |-- EV) . i )assume A13:
i in dom (w |-- EV)
;
((v + w) |-- Ev) . i = (w |-- EV) . ithen A14:
(w |-- EV) . i = (w |-- Affv) . (EV . i)
by FUNCT_1:12;
dom EV = dom (w |-- EV)
by A8, A5, FINSEQ_3:29;
then A15:
EV . i = EV /. i
by A13, PARTFUN1:def 6;
i in Seg (card Affv)
by A8, A13, FINSEQ_1:def 3;
then A16:
cAv . i = v
by FINSEQ_2:57;
A17:
((v + w) |-- Ev) . i = ((v + w) |-- (v + Affv)) . (Ev . i)
by A10, A13, FUNCT_1:12;
dom Ev = dom (w |-- EV)
by A8, A11, FINSEQ_3:29;
then
Ev . i = (EV /. i) + v
by A2, A13, A16, A15, FVSUM_1:17;
hence ((v + w) |-- Ev) . i =
(w |-- Affv) . (((EV /. i) + v) - v)
by A12, A17, RLAFFIN1:def 1
.=
(w |-- Affv) . ((EV /. i) + (v - v))
by RLVECT_1:28
.=
(w |-- Affv) . ((EV /. i) + (0. V))
by RLVECT_1:15
.=
(w |-- EV) . i
by A14, A15, RLVECT_1:def 4
;
verum end;
hence
w |-- EV = (v + w) |-- Ev
by A10, FINSEQ_1:13; verum