let V be ComplexLinearSpace; 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; ( A <> {} implies ( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A ) )
assume A1:
A <> {}
; ( 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 )
( ( for l being C_Linear_Combination of A holds Sum l in A ) implies A is linearly-closed )proof
defpred S1[
Nat]
means for
l being
C_Linear_Combination of
A st
card (Carrier l) = $1 holds
Sum l in A;
assume A2:
A is
linearly-closed
;
for l being C_Linear_Combination of A holds Sum l in A
A3:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
hereby verum
let l be
C_Linear_Combination of
A;
( card (Carrier l) = k + 1 implies Sum l in A )deffunc H1(
Element of
V)
-> Element of
COMPLEX =
l . $1;
consider F being
FinSequence of the
carrier of
V such that A5:
F is
one-to-one
and A6:
rng F = Carrier l
and A7:
Sum l = Sum (l (#) F)
by Def6;
reconsider G =
F | (Seg k) as
FinSequence of the
carrier of
V by FINSEQ_1:18;
assume A8:
card (Carrier l) = k + 1
;
Sum l in Athen A9:
len F = k + 1
by A5, A6, FINSEQ_4:62;
then A10:
len (l (#) F) = k + 1
by Def5;
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then A11:
k + 1
in dom F
by A9, FINSEQ_1:def 3;
then reconsider v =
F . (k + 1) as
VECTOR of
V by FUNCT_1:102;
consider f being
Function of the
carrier of
V,
COMPLEX such that A12:
(
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:8;
then reconsider f =
f as
C_Linear_Combination of
V by Def1;
A13:
Carrier f = (Carrier l) \ {v}
A18:
Carrier l c= A
by Def4;
then
Carrier f c= A \ {v}
by A13, XBOOLE_1:33;
then
Carrier f c= A
by XBOOLE_1:106;
then reconsider f =
f as
C_Linear_Combination of
A by Def4;
A19:
len G = k
by A9, FINSEQ_3:53;
then A20:
len (f (#) G) = k
by Def5;
A21:
rng G = Carrier f
proof
thus
rng G c= Carrier f
XBOOLE_0:def 10 Carrier f c= rng Gproof
let x be
object ;
TARSKI:def 3 ( not x in rng G or x in Carrier f )
assume
x in rng G
;
x in Carrier f
then consider y being
object such that A22:
y in dom G
and A23:
G . y = x
by FUNCT_1:def 3;
reconsider y =
y as
Element of
NAT by A22;
A24:
(
dom G c= dom F &
G . y = F . y )
by A22, FUNCT_1:47, RELAT_1:60;
then
(
x = v implies (
k + 1
= y &
y <= k &
k < k + 1 ) )
by A5, A19, A11, A22, A23, FINSEQ_3:25, FUNCT_1:def 4, XREAL_1:29;
then A25:
not
x in {v}
by TARSKI:def 1;
x in rng F
by A22, A23, A24, FUNCT_1:def 3;
hence
x in Carrier f
by A6, A13, A25, XBOOLE_0:def 5;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in Carrier f or x in rng G )
assume A26:
x in Carrier f
;
x in rng G
then
x in rng F
by A6, A13, XBOOLE_0:def 5;
then consider y being
object such that A27:
y in dom F
and A28:
F . y = x
by FUNCT_1:def 3;
then
y in (dom F) /\ (Seg k)
by A27, XBOOLE_0:def 4;
then A29:
y in dom G
by RELAT_1:61;
then
G . y = F . y
by FUNCT_1:47;
hence
x in rng G
by A28, A29, FUNCT_1:def 3;
verum
end; (Seg (k + 1)) /\ (Seg k) =
Seg k
by FINSEQ_1:7, NAT_1:12
.=
dom (f (#) G)
by A20, FINSEQ_1:def 3
;
then A30:
dom (f (#) G) = (dom (l (#) F)) /\ (Seg k)
by A10, FINSEQ_1:def 3;
now for x being object st x in dom (f (#) G) holds
(f (#) G) . x = (l (#) F) . xlet x be
object ;
( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x )assume A31:
x in dom (f (#) G)
;
(f (#) G) . x = (l (#) F) . xthen A32:
x in dom G
by A19, A20, FINSEQ_3:29;
then A33:
G . x in rng G
by FUNCT_1:def 3;
then reconsider u =
G . x as
VECTOR of
V ;
A34:
F . x = u
by A32, FUNCT_1:47;
not
u in {v}
by A13, A21, A33, XBOOLE_0:def 5;
then A35:
u <> v
by TARSKI:def 1;
x in dom (l (#) F)
by A30, A31, XBOOLE_0:def 4;
then A36:
x in dom F
by A9, A10, FINSEQ_3:29;
(f (#) G) . x =
(f . u) * u
by A32, Th6
.=
(l . u) * u
by A12, A35
;
hence
(f (#) G) . x = (l (#) F) . x
by A36, A34, Th6;
verum end; then A37:
f (#) G = (l (#) F) | (Seg k)
by A30, FUNCT_1:46;
v in rng F
by A11, FUNCT_1:def 3;
then
{v} c= Carrier l
by A6, ZFMISC_1:31;
then
card (Carrier f) = (k + 1) - (card {v})
by A8, A13, CARD_2:44;
then
card (Carrier f) = (k + 1) - 1
by CARD_1:30;
then A38:
Sum f in A
by A4;
v in Carrier l
by A6, A11, FUNCT_1:def 3;
then A39:
(l . v) * v in A
by A2, A18;
G is
one-to-one
by A5, FUNCT_1:52;
then A40:
Sum (f (#) G) = Sum f
by A21, Def6;
(
dom (f (#) G) = Seg (len (f (#) G)) &
(l (#) F) . (len F) = (l . v) * v )
by A9, A11, Th6, FINSEQ_1:def 3;
then
Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v)
by A9, A10, A20, A37, RLVECT_1:38;
hence
Sum l in A
by A2, A7, A39, A40, A38;
verum
end;
end;
let l be
C_Linear_Combination of
A;
Sum l in A
A41:
card (Carrier l) = card (Carrier l)
;
then A42:
S1[
0 ]
;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A42, A3);
hence
Sum l in A
by A41;
verum
end;
assume A43:
for l being C_Linear_Combination of A holds Sum l in A
; A is linearly-closed
( ZeroCLC V is C_Linear_Combination of A & Sum (ZeroCLC V) = 0. V )
by Th4, Th11;
then A44:
0. V in A
by A43;
A45:
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;
( v in A & u in A implies v + u in A )
assume that A52:
v in A
and A53:
u in A
;
v + u in A
A54:
1r * v = v
by CLVECT_1:def 5;
A55:
1r * u = u
by CLVECT_1:def 5;
A56:
now ( v <> u implies v + u in A )deffunc H1(
Element of
V)
-> Element of
COMPLEX =
0c ;
assume A57:
v <> u
;
v + u in Aconsider f being
Function of the
carrier of
V,
COMPLEX such that A58:
(
f . v = 1r &
f . u = 1r )
and A59:
for
w being
Element of
V st
w <> v &
w <> u holds
f . w = H1(
w)
from FUNCT_2:sch 7(A57);
reconsider f =
f as
Element of
Funcs ( the
carrier of
V,
COMPLEX)
by FUNCT_2:8;
then reconsider f =
f as
C_Linear_Combination of
V by Def1;
A60:
Carrier f = {v,u}
then
Carrier f c= A
by A52, A53, ZFMISC_1:32;
then reconsider f =
f as
C_Linear_Combination of
A by Def4;
consider F being
FinSequence of the
carrier of
V such that A61:
(
F is
one-to-one &
rng F = Carrier f )
and A62:
Sum (f (#) F) = Sum f
by Def6;
(
F = <*v,u*> or
F = <*u,v*> )
by A57, A60, A61, FINSEQ_3:99;
then
(
f (#) F = <*(1r * v),(1r * u)*> or
f (#) F = <*(1r * u),(1r * v)*> )
by A58, Th9;
then
Sum f = v + u
by A55, A54, A62, RLVECT_1:45;
hence
v + u in A
by A43;
verum end;
v + v = (1r + 1r) * v
by A54, CLVECT_1:def 3;
hence
v + u in A
by A45, A52, A56;
verum
end;
hence
A is linearly-closed
by A45; verum