let V be RealLinearSpace; :: thesis: for A being Subset of V holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
let A be Subset of V; :: thesis: ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
thus
( A <> {} & A is linearly-closed implies for l being Linear_Combination of A holds Sum l in A )
:: thesis: ( ( for l being Linear_Combination of A holds Sum l in A ) implies ( A <> {} & A is linearly-closed ) )proof
assume that A1:
A <> {}
and A2:
A is
linearly-closed
;
:: thesis: for l being Linear_Combination of A holds Sum l in A
defpred S1[
Element of
NAT ]
means for
l being
Linear_Combination of
A st
card (Carrier l) = $1 holds
Sum l in A;
A3:
S1[
0 ]
A4:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
now let k be
Element of
NAT ;
:: thesis: ( ( for l being Linear_Combination of A st card (Carrier l) = k holds
Sum l in A ) implies for l being Linear_Combination of A st card (Carrier l) = k + 1 holds
Sum l in A )assume A5:
for
l being
Linear_Combination of
A st
card (Carrier l) = k holds
Sum l in A
;
:: thesis: for l being Linear_Combination of A st card (Carrier l) = k + 1 holds
Sum l in Alet l be
Linear_Combination of
A;
:: thesis: ( card (Carrier l) = k + 1 implies Sum l in A )assume A6:
card (Carrier l) = k + 1
;
:: thesis: Sum l in Aconsider F being
FinSequence of the
carrier of
V such that A7:
F is
one-to-one
and A8:
rng F = Carrier l
and A9:
Sum l = Sum (l (#) F)
by Def10;
A10:
len F = k + 1
by A6, A7, A8, FINSEQ_4:77;
reconsider G =
F | (Seg k) as
FinSequence of the
carrier of
V by FINSEQ_1:23;
A11:
len G = k
by A10, FINSEQ_3:59;
A12:
k + 1
in Seg (k + 1)
by FINSEQ_1:6;
then
k + 1
in dom F
by A10, FINSEQ_1:def 3;
then reconsider v =
F . (k + 1) as
VECTOR of
V by FUNCT_1:172;
A13:
k + 1
in dom F
by A10, A12, FINSEQ_1:def 3;
then A14:
(
v in Carrier l &
Carrier l c= A )
by A8, Def8, FUNCT_1:def 5;
then A15:
(l . v) * v in A
by A2, RLSUB_1:def 1;
deffunc H1(
Element of
V)
-> Element of
REAL =
l . $1;
consider f being
Function of the
carrier of
V,
REAL such that A16:
f . v = 0
and A17:
for
u being
Element of
V st
u <> v holds
f . u = H1(
u)
from FUNCT_2:sch 6();
reconsider f =
f as
Element of
Funcs the
carrier of
V,
REAL by FUNCT_2:11;
then reconsider f =
f as
Linear_Combination of
V by Def5;
A19:
Carrier f = (Carrier l) \ {v}
then
(
Carrier f c= A \ {v} &
A \ {v} c= A )
by A14, XBOOLE_1:33, XBOOLE_1:36;
then
Carrier f c= A
by XBOOLE_1:1;
then reconsider f =
f as
Linear_Combination of
A by Def8;
A23:
G is
one-to-one
by A7, FUNCT_1:84;
A24:
rng G = Carrier f
then A33:
Sum (f (#) G) = Sum f
by A23, Def10;
A34:
(
len (l (#) F) = k + 1 &
len (f (#) G) = k )
by A10, A11, Def9;
(Seg (k + 1)) /\ (Seg k) =
Seg k
by FINSEQ_1:9, NAT_1:12
.=
dom (f (#) G)
by A34, FINSEQ_1:def 3
;
then A35:
dom (f (#) G) = (dom (l (#) F)) /\ (Seg k)
by A34, FINSEQ_1:def 3;
now let x be
set ;
:: thesis: ( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x )assume A36:
x in dom (f (#) G)
;
:: thesis: (f (#) G) . x = (l (#) F) . xthen reconsider n =
x as
Element of
NAT ;
A37:
n in dom G
by A11, A34, A36, FINSEQ_3:31;
then A38:
(
G . n in rng G &
rng G c= the
carrier of
V )
by FUNCT_1:def 5;
then reconsider u =
G . n as
VECTOR of
V ;
not
u in {v}
by A19, A24, A38, XBOOLE_0:def 5;
then A39:
u <> v
by TARSKI:def 1;
A40:
(f (#) G) . n =
(f . u) * u
by A37, Th40
.=
(l . u) * u
by A17, A39
;
n in dom (l (#) F)
by A35, A36, XBOOLE_0:def 4;
then A41:
n in dom F
by A10, A34, FINSEQ_3:31;
then
(
F . n in rng F &
rng F c= the
carrier of
V )
by FUNCT_1:def 5;
then reconsider w =
F . n as
VECTOR of
V ;
w = u
by A37, FUNCT_1:70;
hence
(f (#) G) . x = (l (#) F) . x
by A40, A41, Th40;
:: thesis: verum end; then A42:
f (#) G = (l (#) F) | (Seg k)
by A35, FUNCT_1:68;
A43:
(
dom (l (#) F) = Seg (len (l (#) F)) &
dom (f (#) G) = Seg (len (f (#) G)) &
dom F = Seg (len F) )
by FINSEQ_1:def 3;
(l (#) F) . (len F) = (l . v) * v
by A10, A13, Th40;
then A44:
Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v)
by A10, A34, A42, A43, RLVECT_1:55;
v in rng F
by A13, FUNCT_1:def 5;
then
(
Carrier l is
finite &
{v} c= Carrier l )
by A8, ZFMISC_1:37;
then card (Carrier f) =
(k + 1) - (card {v})
by A6, A19, CARD_2:63
.=
(k + 1) - 1
by CARD_1:50
.=
k
;
then
Sum f in A
by A5;
hence
Sum l in A
by A2, A9, A15, A33, A44, RLSUB_1:def 1;
:: thesis: verum end;
hence
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
;
:: thesis: verum
end;
A45:
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A3, A4);
let l be
Linear_Combination of
A;
:: thesis: Sum l in A
card (Carrier l) = card (Carrier l)
;
hence
Sum l in A
by A45;
:: thesis: verum
end;
assume A46:
for l being Linear_Combination of A holds Sum l in A
; :: thesis: ( A <> {} & A is linearly-closed )
( ZeroLC V is Linear_Combination of A & Sum (ZeroLC V) = 0. V )
by Lm1, Th34;
then A47:
0. V in A
by A46;
thus
A <> {}
by A46; :: thesis: A is linearly-closed
A48:
for a being Real
for v being VECTOR of V st v in A holds
a * v in A
thus
for v, u being VECTOR of V st v in A & u in A holds
v + u in A
:: according to RLSUB_1:def 1 :: thesis: for b1 being Element of REAL
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A )proof
let v,
u be
VECTOR of
V;
:: thesis: ( v in A & u in A implies v + u in A )
assume that A58:
v in A
and A59:
u in A
;
:: thesis: v + u in A
now per cases
( u = v or v <> u )
;
suppose A60:
v <> u
;
:: thesis: v + u in Adeffunc H1(
Element of
V)
-> Element of
NAT =
0 ;
consider f being
Function of the
carrier of
V,
REAL such that A61:
f . v = 1
and A62:
f . u = 1
and A63:
for
w being
Element of
V st
w <> v &
w <> u holds
f . w = H1(
w)
from FUNCT_2:sch 7(A60);
reconsider f =
f as
Element of
Funcs the
carrier of
V,
REAL by FUNCT_2:11;
then reconsider f =
f as
Linear_Combination of
V by Def5;
A64:
Carrier f = {v,u}
then
Carrier f c= A
by A58, A59, ZFMISC_1:38;
then reconsider f =
f as
Linear_Combination of
A by Def8;
consider F being
FinSequence of the
carrier of
V such that A65:
F is
one-to-one
and A66:
rng F = Carrier f
and A67:
Sum (f (#) F) = Sum f
by Def10;
(
F = <*v,u*> or
F = <*u,v*> )
by A60, A64, A65, A66, FINSEQ_3:108;
then
( (
f (#) F = <*(1 * v),(1 * u)*> or
f (#) F = <*(1 * u),(1 * v)*> ) & 1
* u = u & 1
* v = v )
by A61, A62, Th43, RLVECT_1:def 9;
then
Sum f = v + u
by A67, RLVECT_1:62;
hence
v + u in A
by A46;
:: thesis: verum end;
hence
v + u in A
;
:: thesis: verum
end;
thus
for b1 being Element of REAL
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A )
by A48; :: thesis: verum