let r be Real; for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R st r <> 0 holds
sum LR = sum (r (*) LR)
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; for LR being Linear_Combination of R st r <> 0 holds
sum LR = sum (r (*) LR)
let LR be Linear_Combination of R; ( r <> 0 implies sum LR = sum (r (*) LR) )
set rL = r (*) LR;
deffunc H1( Element of R) -> Element of the carrier of R = r * $1;
consider f being Function of the carrier of R, the carrier of R such that
A1:
for v being Element of R holds f . v = H1(v)
from FUNCT_2:sch 4();
consider F being FinSequence of R such that
A2:
F is one-to-one
and
A3:
rng F = Carrier LR
and
A4:
sum LR = Sum (LR * F)
by Def3;
assume A5:
r <> 0
; sum LR = sum (r (*) LR)
now for x1, x2 being object st x1 in dom (f * F) & x2 in dom (f * F) & (f * F) . x1 = (f * F) . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in dom (f * F) & x2 in dom (f * F) & (f * F) . x1 = (f * F) . x2 implies x1 = x2 )assume that A6:
x1 in dom (f * F)
and A7:
x2 in dom (f * F)
and A8:
(f * F) . x1 = (f * F) . x2
;
x1 = x2A9:
f . (F /. x1) = r * (F /. x1)
by A1;
A10:
x1 in dom F
by A6, FUNCT_1:11;
then A11:
F . x1 = F /. x1
by PARTFUN1:def 6;
A12:
x2 in dom F
by A7, FUNCT_1:11;
then A13:
F . x2 = F /. x2
by PARTFUN1:def 6;
(
(f * F) . x1 = f . (F . x1) &
(f * F) . x2 = f . (F . x2) )
by A6, A7, FUNCT_1:12;
then A14:
r * (F /. x1) = r * (F /. x2)
by A1, A8, A9, A11, A13;
F /. x1 =
1
* (F /. x1)
by RLVECT_1:def 8
.=
((r ") * r) * (F /. x1)
by A5, XCMPLX_0:def 7
.=
(r ") * (r * (F /. x2))
by A14, RLVECT_1:def 7
.=
((r ") * r) * (F /. x2)
by RLVECT_1:def 7
.=
1
* (F /. x2)
by A5, XCMPLX_0:def 7
.=
F /. x2
by RLVECT_1:def 8
;
hence
x1 = x2
by A2, A10, A11, A12, A13, FUNCT_1:def 4;
verum end;
then A15:
f * F is one-to-one
by FUNCT_1:def 4;
A16:
len (LR * F) = len F
by FINSEQ_2:33;
A17:
len (f * F) = len F
by FINSEQ_2:33;
A18:
len ((r (*) LR) * (f * F)) = len (f * F)
by FINSEQ_2:33;
now for k being Nat st 1 <= k & k <= len F holds
((r (*) LR) * (f * F)) . k = (LR * F) . klet k be
Nat;
( 1 <= k & k <= len F implies ((r (*) LR) * (f * F)) . k = (LR * F) . k )assume A19:
( 1
<= k &
k <= len F )
;
((r (*) LR) * (f * F)) . k = (LR * F) . kthen
k in dom F
by FINSEQ_3:25;
then A20:
F /. k = F . k
by PARTFUN1:def 6;
k in dom (LR * F)
by A16, A19, FINSEQ_3:25;
then A21:
(LR * F) . k = LR . (F . k)
by FUNCT_1:12;
k in dom (f * F)
by A17, A19, FINSEQ_3:25;
then A22:
(f * F) . k = f . (F . k)
by FUNCT_1:12;
k in dom ((r (*) LR) * (f * F))
by A17, A18, A19, FINSEQ_3:25;
then
((r (*) LR) * (f * F)) . k = (r (*) LR) . ((f * F) . k)
by FUNCT_1:12;
hence ((r (*) LR) * (f * F)) . k =
(r (*) LR) . (r * (F /. k))
by A1, A20, A22
.=
LR . ((r ") * (r * (F /. k)))
by A5, Def2
.=
LR . (((r ") * r) * (F /. k))
by RLVECT_1:def 7
.=
LR . (1 * (F /. k))
by A5, XCMPLX_0:def 7
.=
(LR * F) . k
by A20, A21, RLVECT_1:def 8
;
verum end;
then A23:
LR * F = (r (*) LR) * (f * F)
by A16, A17, A18;
Carrier (r (*) LR) c= rng (f * F)
proof
let x be
object ;
TARSKI:def 3 ( not x in Carrier (r (*) LR) or x in rng (f * F) )
assume
x in Carrier (r (*) LR)
;
x in rng (f * F)
then
x in r * (Carrier LR)
by A5, Th23;
then consider v being
Element of
R such that A24:
x = r * v
and A25:
v in Carrier LR
;
consider y being
object such that A26:
y in dom F
and A27:
F . y = v
by A3, A25, FUNCT_1:def 3;
A28:
f . v = x
by A1, A24;
A29:
dom F = dom (f * F)
by A17, FINSEQ_3:29;
then
(f * F) . y = f . v
by A26, A27, FUNCT_1:12;
hence
x in rng (f * F)
by A26, A28, A29, FUNCT_1:def 3;
verum
end;
hence
sum LR = sum (r (*) LR)
by A4, A15, A23, Th30; verum