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
defpred S1[ Nat] means for l being Linear_Combination of A st card () = \$1 holds
Sum l in A;
assume that
A1: A <> {} and
A2: A is linearly-closed ; :: thesis: for l being Linear_Combination of A holds Sum l in A
now :: thesis: for l being Linear_Combination of A st card () = 0 holds
Sum l in A
let l be Linear_Combination of A; :: thesis: ( card () = 0 implies Sum l in A )
assume card () = 0 ; :: thesis: Sum l in A
then Carrier l = {} ;
then l = ZeroLC V by Def5;
then Sum l = 0. V by Lm2;
hence Sum l in A by ; :: thesis: verum
end;
then A3: S1[ 0 ] ;
now :: thesis: for k being Nat st ( for l being Linear_Combination of A st card () = k holds
Sum l in A ) holds
for l being Linear_Combination of A st card () = k + 1 holds
Sum l in A
let k be Nat; :: thesis: ( ( for l being Linear_Combination of A st card () = k holds
Sum l in A ) implies for l being Linear_Combination of A st card () = k + 1 holds
Sum l in A )

assume A4: for l being Linear_Combination of A st card () = k holds
Sum l in A ; :: thesis: for l being Linear_Combination of A st card () = k + 1 holds
Sum l in A

let l be Linear_Combination of A; :: thesis: ( card () = k + 1 implies Sum l in A )
deffunc H1( Element of V) -> Element of REAL = l . \$1;
consider F being FinSequence of V such that
A5: F is one-to-one and
A6: rng F = Carrier l and
A7: Sum l = Sum (l (#) F) by Def8;
reconsider G = F | (Seg k) as FinSequence of the carrier of V by FINSEQ_1:18;
assume A8: card () = k + 1 ; :: thesis: Sum l in A
then A9: len F = k + 1 by ;
then A10: len (l (#) F) = k + 1 by Def7;
A11: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A12: k + 1 in dom F by ;
k + 1 in dom F by ;
then reconsider v = F . (k + 1) as VECTOR of V by FUNCT_1:102;
consider f being Function of the carrier of V,REAL such that
A13: f . v = In (0,REAL) and
A14: for u being Element of V st u <> v holds
f . u = H1(u) from reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
A15: v in Carrier l by ;
now :: thesis: for u being VECTOR of V st not u in Carrier l holds
f . u = 0
let u be VECTOR of V; :: thesis: ( not u in Carrier l implies f . u = 0 )
assume A16: not u in Carrier l ; :: thesis: f . u = 0
hence f . u = l . u by
.= 0 by A16 ;
:: thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def3;
A17: A \ {v} c= A by XBOOLE_1:36;
A18: Carrier l c= A by Def6;
then A19: (l . v) * v in A by ;
A20: Carrier f = () \ {v}
proof
thus Carrier f c= () \ {v} :: according to XBOOLE_0:def 10 :: thesis: () \ {v} c= Carrier f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in () \ {v} )
assume x in Carrier f ; :: thesis: x in () \ {v}
then consider u being VECTOR of V such that
A21: u = x and
A22: f . u <> 0 ;
f . u = l . u by ;
then A23: x in Carrier l by ;
not x in {v} by ;
hence x in () \ {v} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in () \ {v} or x in Carrier f )
assume A24: x in () \ {v} ; :: thesis:
then x in Carrier l by XBOOLE_0:def 5;
then consider u being VECTOR of V such that
A25: x = u and
A26: l . u <> 0 ;
not x in {v} by ;
then x <> v by TARSKI:def 1;
then l . u = f . u by ;
hence x in Carrier f by ; :: thesis: verum
end;
then Carrier f c= A \ {v} by ;
then Carrier f c= A by A17;
then reconsider f = f as Linear_Combination of A by Def6;
A27: len G = k by ;
then A28: len (f (#) G) = k by Def7;
A29: rng G = Carrier f
proof
thus rng G c= Carrier f :: according to XBOOLE_0:def 10 :: thesis:
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng G or x in Carrier f )
assume x in rng G ; :: thesis:
then consider y being object such that
A30: y in dom G and
A31: G . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A30;
A32: ( dom G c= dom F & G . y = F . y ) by ;
now :: thesis: not x = v
assume x = v ; :: thesis: contradiction
then A33: k + 1 = y by A5, A12, A30, A31, A32;
y <= k by ;
hence contradiction by A33, XREAL_1:29; :: thesis: verum
end;
then A34: not x in {v} by TARSKI:def 1;
x in rng F by ;
hence x in Carrier f by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in rng G )
assume A35: x in Carrier f ; :: thesis: x in rng G
then x in rng F by ;
then consider y being object such that
A36: y in dom F and
A37: F . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A36;
then y in (dom F) /\ (Seg k) by ;
then A38: y in dom G by RELAT_1:61;
then G . y = F . y by FUNCT_1:47;
hence x in rng G by ; :: thesis: verum
end;
(Seg (k + 1)) /\ (Seg k) = Seg k by
.= dom (f (#) G) by ;
then A39: dom (f (#) G) = (dom (l (#) F)) /\ (Seg k) by ;
now :: thesis: for x being object st x in dom (f (#) G) holds
(f (#) G) . x = (l (#) F) . x
let x be object ; :: thesis: ( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x )
assume A40: x in dom (f (#) G) ; :: thesis: (f (#) G) . x = (l (#) F) . x
then reconsider n = x as Element of NAT ;
n in dom (l (#) F) by ;
then A41: n in dom F by ;
then F . n in rng F by FUNCT_1:def 3;
then reconsider w = F . n as VECTOR of V ;
A42: n in dom G by ;
then A43: G . n in rng G by FUNCT_1:def 3;
then reconsider u = G . n as VECTOR of V ;
not u in {v} by ;
then A44: u <> v by TARSKI:def 1;
A45: (f (#) G) . n = (f . u) * u by
.= (l . u) * u by ;
w = u by ;
hence (f (#) G) . x = (l (#) F) . x by ; :: thesis: verum
end;
then A46: f (#) G = (l (#) F) | (Seg k) by ;
v in rng F by ;
then {v} c= Carrier l by ;
then card () = (k + 1) - () by
.= (k + 1) - 1 by CARD_1:30
.= k ;
then A47: Sum f in A by A4;
G is one-to-one by ;
then A48: Sum (f (#) G) = Sum f by ;
( dom (f (#) G) = Seg (len (f (#) G)) & (l (#) F) . (len F) = (l . v) * v ) by ;
then Sum (l (#) F) = (Sum (f (#) G)) + ((l . v) * v) by ;
hence Sum l in A by A2, A7, A19, A48, A47; :: thesis: verum
end;
then A49: for k being Nat st S1[k] holds
S1[k + 1] ;
let l be Linear_Combination of A; :: thesis: Sum l in A
A50: card () = card () ;
for k being Nat holds S1[k] from NAT_1:sch 2(A3, A49);
hence Sum l in A by A50; :: thesis: verum
end;
assume A51: for l being Linear_Combination of A holds Sum l in A ; :: thesis: ( A <> {} & A is linearly-closed )
hence A <> {} ; :: thesis:
( ZeroLC V is Linear_Combination of A & Sum () = 0. V ) by ;
then A52: 0. V in A by A51;
A53: for a being Real
for v being VECTOR of V st v in A holds
a * v in A
proof
let a be Real; :: thesis: for v being VECTOR of V st v in A holds
a * v in A

let v be VECTOR of V; :: thesis: ( v in A implies a * v in A )
assume A54: v in A ; :: thesis: a * v in A
now :: thesis: a * v in A
per cases ( a = 0 or a <> 0 ) ;
suppose a = 0 ; :: thesis: a * v in A
hence a * v in A by ; :: thesis: verum
end;
suppose A55: a <> 0 ; :: thesis: a * v in A
deffunc H1( Element of V) -> Element of REAL = zz;
reconsider aa = a as Element of REAL by XREAL_0:def 1;
consider f being Function of the carrier of V,REAL such that
A56: f . v = aa and
A57: for u being Element of V st u <> v holds
f . u = H1(u) from reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now :: thesis: for u being VECTOR of V st not u in {v} holds
f . u = 0
let u be VECTOR of V; :: thesis: ( not u in {v} implies f . u = 0 )
assume not u in {v} ; :: thesis: f . u = 0
then u <> v by TARSKI:def 1;
hence f . u = 0 by A57; :: thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def3;
A58: Carrier f = {v}
proof
thus Carrier f c= {v} :: according to XBOOLE_0:def 10 :: thesis:
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v} )
assume x in Carrier f ; :: thesis: x in {v}
then consider u being VECTOR of V such that
A59: x = u and
A60: f . u <> 0 ;
u = v by ;
hence x in {v} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v} or x in Carrier f )
assume x in {v} ; :: thesis:
then x = v by TARSKI:def 1;
hence x in Carrier f by ; :: thesis: verum
end;
{v} c= A by ;
then reconsider f = f as Linear_Combination of A by ;
consider F being FinSequence of V such that
A61: ( F is one-to-one & rng F = Carrier f ) and
A62: Sum (f (#) F) = Sum f by Def8;
F = <*v*> by ;
then f (#) F = <*((f . v) * v)*> by Th26;
then Sum f = a * v by ;
hence a * v in A by A51; :: thesis: verum
end;
end;
end;
hence a * v in A ; :: thesis: verum
end;
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 object
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
A63: v in A and
A64: u in A ; :: thesis: v + u in A
now :: thesis: v + u in A
per cases ( u = v or v <> u ) ;
suppose u = v ; :: thesis: v + u in A
then v + u = (1 * v) + v by RLVECT_1:def 8
.= (1 * v) + (1 * v) by RLVECT_1:def 8
.= (1 + 1) * v by RLVECT_1:def 6
.= 2 * v ;
hence v + u in A by ; :: thesis: verum
end;
suppose A65: v <> u ; :: thesis: v + u in A
deffunc H1( Element of V) -> Element of REAL = zz;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
consider f being Function of the carrier of V,REAL such that
A66: ( f . v = jj & f . u = jj ) and
A67: for w being Element of V st w <> v & w <> u holds
f . w = H1(w) from reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;
now :: thesis: for w being VECTOR of V st not w in {v,u} holds
f . w = 0
let w be VECTOR of V; :: thesis: ( not w in {v,u} implies f . w = 0 )
assume not w in {v,u} ; :: thesis: f . w = 0
then ( w <> v & w <> u ) by TARSKI:def 2;
hence f . w = 0 by A67; :: thesis: verum
end;
then reconsider f = f as Linear_Combination of V by Def3;
A68: Carrier f = {v,u}
proof
thus Carrier f c= {v,u} :: according to XBOOLE_0:def 10 :: thesis: {v,u} c= Carrier f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {v,u} )
assume x in Carrier f ; :: thesis: x in {v,u}
then ex w being VECTOR of V st
( x = w & f . w <> 0 ) ;
then ( x = v or x = u ) by A67;
hence x in {v,u} by TARSKI:def 2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {v,u} or x in Carrier f )
assume x in {v,u} ; :: thesis:
then ( x = v or x = u ) by TARSKI:def 2;
hence x in Carrier f by A66; :: thesis: verum
end;
then A69: Carrier f c= A by ;
A70: ( 1 * u = u & 1 * v = v ) by RLVECT_1:def 8;
reconsider f = f as Linear_Combination of A by ;
consider F being FinSequence of V such that
A71: ( F is one-to-one & rng F = Carrier f ) and
A72: Sum (f (#) F) = Sum f by Def8;
( F = <*v,u*> or F = <*u,v*> ) by ;
then ( f (#) F = <*(1 * v),(1 * u)*> or f (#) F = <*(1 * u),(1 * v)*> ) by ;
then Sum f = v + u by ;
hence v + u in A by A51; :: thesis: verum
end;
end;
end;
hence v + u in A ; :: thesis: verum
end;
thus for b1 being object
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A ) by A53; :: thesis: verum