let V be ComplexLinearSpace; :: thesis: for A being Subset of V st A <> {} holds
( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A )
let A be Subset of V; :: thesis: ( A <> {} implies ( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A ) )
assume A1:
A <> {}
; :: thesis: ( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A )
thus
( A is linearly-closed implies for l being C_Linear_Combination of A holds Sum l in A )
:: thesis: ( ( for l being C_Linear_Combination of A holds Sum l in A ) implies A is linearly-closed )proof
assume A2:
A is
linearly-closed
;
:: thesis: for l being C_Linear_Combination of A holds Sum l in A
defpred S1[
Nat]
means for
l being
C_Linear_Combination of
A st
card (Carrier l) = $1 holds
Sum l in A;
then A3:
S1[
0 ]
;
A4:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
:: thesis: S1[k + 1]
hereby :: thesis: verum
let l be
C_Linear_Combination of
A;
:: thesis: ( card (Carrier l) = k + 1 implies Sum l in A )consider F being
FinSequence of the
carrier of
V such that A7:
(
F is
one-to-one &
rng F = Carrier l &
Sum l = Sum (l (#) F) )
by Def5;
assume A6:
card (Carrier l) = k + 1
;
:: thesis: Sum l in Athen A10:
len F = k + 1
by A7, 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;
k + 1
in Seg (k + 1)
by FINSEQ_1:6;
then A13:
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;
A14:
(
v in Carrier l &
Carrier l c= A )
by A7, Def3, A13, FUNCT_1:def 5;
then A15:
(l . v) * v in A
by A2, CLVECT_1:def 4;
deffunc H1(
Element of
V)
-> Element of
COMPLEX =
l . $1;
consider f being
Function of the
carrier of
V,
COMPLEX such that A16:
(
f . v = 0c & ( 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,
COMPLEX by FUNCT_2:11;
then reconsider f =
f as
C_Linear_Combination of
V by Def1;
A19:
Carrier f = (Carrier l) \ {v}
then
Carrier f c= A \ {v}
by A14, XBOOLE_1:33;
then
Carrier f c= A
by XBOOLE_1:106;
then reconsider f =
f as
C_Linear_Combination of
A by Def3;
A23:
G is
one-to-one
by A7, FUNCT_1:84;
A24:
rng G = Carrier f
proof
thus
rng G c= Carrier f
:: according to XBOOLE_0:def 10 :: thesis: Carrier f c= rng Gproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng G or x in Carrier f )
assume
x in rng G
;
:: thesis: x in Carrier f
then consider y being
set such that A25:
(
y in dom G &
G . y = x )
by FUNCT_1:def 5;
reconsider y =
y as
Element of
NAT by A25;
dom G c= dom F
by RELAT_1:89;
then A27:
(
y in dom F &
G . y = F . y )
by A25, FUNCT_1:70;
then A28:
x in rng F
by A25, FUNCT_1:def 5;
(
x = v implies (
k + 1
= y &
y <= k &
k < k + 1 ) )
by A7, A11, A13, A25, A27, FINSEQ_3:27, FUNCT_1:def 8, XREAL_1:31;
then
not
x in {v}
by TARSKI:def 1;
hence
x in Carrier f
by A7, A19, A28, XBOOLE_0:def 5;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in rng G )
assume A29:
x in Carrier f
;
:: thesis: x in rng G
then
x in rng F
by A7, A19, XBOOLE_0:def 5;
then consider y being
set such that A30:
(
y in dom F &
F . y = x )
by FUNCT_1:def 5;
then
y in (dom F) /\ (Seg k)
by A30, XBOOLE_0:def 4;
then A32:
y in dom G
by RELAT_1:90;
then
G . y = F . y
by FUNCT_1:70;
hence
x in rng G
by A30, A32, FUNCT_1:def 5;
:: thesis: verum
end; then A33:
Sum (f (#) G) = Sum f
by A23, Def5;
A34:
(
len (l (#) F) = k + 1 &
len (f (#) G) = k )
by A10, A11, Def4;
(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 A37:
x in dom G
by A11, A34, FINSEQ_3:31;
then A38:
G . x in rng G
by FUNCT_1:def 5;
reconsider u =
G . x as
VECTOR of
V by A38;
not
u in {v}
by A19, A24, A38, XBOOLE_0:def 5;
then A39:
u <> v
by TARSKI:def 1;
A40:
(f (#) G) . x =
(f . u) * u
by A37, Th40
.=
(l . u) * u
by A16, A39
;
x in dom (l (#) F)
by A35, A36, XBOOLE_0:def 4;
then A41:
x in dom F
by A10, A34, FINSEQ_3:31;
F . x = 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 (f (#) G) = Seg (len (f (#) G))
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
{v} c= Carrier l
by A7, ZFMISC_1:37;
then
card (Carrier f) = (k + 1) - (card {v})
by A6, A19, CARD_2:63;
then
card (Carrier f) = (k + 1) - 1
by CARD_1:50;
then
Sum f in A
by A5;
hence
Sum l in A
by A2, A7, A15, A33, A44, CLVECT_1:def 4;
:: thesis: verum
end;
end;
A45:
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A3, A4);
let l be
C_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 C_Linear_Combination of A holds Sum l in A
; :: thesis: A is linearly-closed
( ZeroCLC V is C_Linear_Combination of A & Sum (ZeroCLC V) = 0. V )
by Lm2, Th34;
then A47:
0. V in A
by A46;
A48:
for a being Complex
for v being VECTOR of V st v in A holds
a * v in A
for v, u being VECTOR of V st v in A & u in A holds
v + u in A
proof
let v,
u be
VECTOR of
V;
:: thesis: ( v in A & u in A implies v + u in A )
assume A58:
(
v in A &
u in A )
;
:: thesis: v + u in A
C:
(
1r * u = u &
1r * v = v )
by CLVECT_1:def 2;
then B:
v + v = (1r + 1r ) * v
by CLVECT_1:def 2;
now assume A60:
v <> u
;
:: thesis: v + u in Adeffunc H1(
Element of
V)
-> Element of
COMPLEX =
0c ;
consider f being
Function of the
carrier of
V,
COMPLEX such that A61:
(
f . v = 1r &
f . u = 1r )
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,
COMPLEX by FUNCT_2:11;
then reconsider f =
f as
C_Linear_Combination of
V by Def1;
A64:
Carrier f = {v,u}
then
Carrier f c= A
by A58, ZFMISC_1:38;
then reconsider f =
f as
C_Linear_Combination of
A by Def3;
consider F being
FinSequence of the
carrier of
V such that A65:
(
F is
one-to-one &
rng F = Carrier f &
Sum (f (#) F) = Sum f )
by Def5;
(
F = <*v,u*> or
F = <*u,v*> )
by A60, A64, A65, FINSEQ_3:108;
then
(
f (#) F = <*(1r * v),(1r * u)*> or
f (#) F = <*(1r * u),(1r * v)*> )
by A61, Th43;
then
Sum f = v + u
by A65, C, RLVECT_1:62;
hence
v + u in A
by A46;
:: thesis: verum end;
hence
v + u in A
by B, A48, A58;
:: thesis: verum
end;
hence
A is linearly-closed
by A48, CLVECT_1:def 4; :: thesis: verum