let R be Ring; :: thesis: for V being RightMod of R
for A being Subset of V st 0. R <> 1_ R holds
( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A )
let V be RightMod of R; :: thesis: for A being Subset of V st 0. R <> 1_ R 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: ( 0. R <> 1_ R implies ( ( A <> {} & A is linearly-closed ) iff for l being Linear_Combination of A holds Sum l in A ) )
assume A1:
0. R <> 1_ R
; :: 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 A2:
A <> {}
and A3:
A is
linearly-closed
;
:: thesis: for l being Linear_Combination of A holds Sum l in A
defpred S1[
Nat]
means for
l being
Linear_Combination of
A st
card (Carrier l) = $1 holds
Sum l in A;
A4:
S1[
0 ]
A5:
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 A6:
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 A7:
card (Carrier l) = k + 1
;
:: thesis: Sum l in Aconsider F being
FinSequence of
V such that A8:
F is
one-to-one
and A9:
rng F = Carrier l
and A10:
Sum l = Sum (l (#) F)
by Def9;
A11:
len F = k + 1
by A7, A8, A9, FINSEQ_4:77;
reconsider G =
F | (Seg k) as
FinSequence of
V by FINSEQ_1:23;
A12:
len G = k
by A11, FINSEQ_3:59;
A13:
k + 1
in Seg (k + 1)
by FINSEQ_1:6;
then
k + 1
in dom F
by A11, FINSEQ_1:def 3;
then reconsider v =
F . (k + 1) as
Vector of
V by FINSEQ_2:13;
A14:
k + 1
in dom F
by A11, A13, FINSEQ_1:def 3;
then A15:
(
v in Carrier l &
Carrier l c= A )
by A9, Def7, FUNCT_1:def 5;
then A16:
v * (l . v) in A
by A3, RMOD_2:def 1;
deffunc H1(
Element of
V)
-> Element of the
carrier of
R =
l . $1;
consider f being
Function of
V,
R such that A17:
f . v = 0. R
and A18:
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,the
carrier of
R by FUNCT_2:11;
then reconsider f =
f as
Linear_Combination of
V by Def4;
A20:
Carrier f = (Carrier l) \ {v}
then
(
Carrier f c= A \ {v} &
A \ {v} c= A )
by A15, 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 Def7;
A24:
G is
one-to-one
by A8, FUNCT_1:84;
A25:
rng G = Carrier f
then A34:
Sum (f (#) G) = Sum f
by A24, Def9;
A35:
(
len (l (#) F) = k + 1 &
len (f (#) G) = k )
by A11, A12, Def8;
(Seg (k + 1)) /\ (Seg k) =
Seg k
by FINSEQ_1:9, NAT_1:12
.=
dom (f (#) G)
by A35, FINSEQ_1:def 3
;
then A36:
dom (f (#) G) = (dom (l (#) F)) /\ (Seg k)
by A35, FINSEQ_1:def 3;
now let x be
set ;
:: thesis: ( x in dom (f (#) G) implies (f (#) G) . x = (l (#) F) . x )assume A37:
x in dom (f (#) G)
;
:: thesis: (f (#) G) . x = (l (#) F) . xthen reconsider n =
x as
Nat by FINSEQ_3:25;
A38:
n in dom G
by A12, A35, A37, FINSEQ_3:31;
then A39:
(
G . n in rng G &
rng G c= the
carrier of
V )
by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider u =
G . n as
Vector of
V ;
not
u in {v}
by A20, A25, A39, XBOOLE_0:def 5;
then A40:
u <> v
by TARSKI:def 1;
A41:
(f (#) G) . n =
u * (f . u)
by A38, Th32
.=
u * (l . u)
by A18, A40
;
n in dom (l (#) F)
by A36, A37, XBOOLE_0:def 4;
then A42:
n in dom F
by A11, A35, FINSEQ_3:31;
then
(
F . n in rng F &
rng F c= the
carrier of
V )
by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider w =
F . n as
Vector of
V ;
w = u
by A38, FUNCT_1:70;
hence
(f (#) G) . x = (l (#) F) . x
by A41, A42, Th32;
:: thesis: verum end; then
f (#) G = (l (#) F) | (Seg k)
by A36, FUNCT_1:68;
then A43:
f (#) G = (l (#) F) | (dom (f (#) G))
by A35, FINSEQ_1:def 3;
(l (#) F) . (len F) = v * (l . v)
by A11, A14, Th32;
then A44:
Sum (l (#) F) = (Sum (f (#) G)) + (v * (l . v))
by A11, A35, A43, RLVECT_1:55;
v in rng F
by A14, FUNCT_1:def 5;
then
(
Carrier l is
finite &
{v} c= Carrier l )
by A9, ZFMISC_1:37;
then card (Carrier f) =
(k + 1) - (card {v})
by A7, A20, CARD_2:63
.=
(k + 1) - 1
by CARD_1:50
.=
k
by XCMPLX_1:26
;
then
Sum f in A
by A6;
hence
Sum l in A
by A3, A10, A16, A34, A44, RMOD_2: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(A4, A5);
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 Lm3, Th26;
then A47:
0. V in A
by A46;
thus
A <> {}
by A46; :: thesis: A is linearly-closed
A48:
for a being Scalar of R
for v being Vector of V st v in A holds
v * a in A
thus
for v, u being Vector of V st v in A & u in A holds
v + u in A
:: according to RMOD_2:def 1 :: thesis: for b1 being Element of the carrier of R
for b2 being Element of the carrier of V holds
( not b2 in A or b2 * b1 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 the
carrier of
R =
0. R;
consider f being
Function of
V,
R such that A61:
f . v = 1_ R
and A62:
f . u = 1_ R
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,the
carrier of
R by FUNCT_2:11;
then reconsider f =
f as
Linear_Combination of
V by Def4;
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 Def7;
consider F being
FinSequence of
V such that A65:
F is
one-to-one
and A66:
rng F = Carrier f
and A67:
Sum (f (#) F) = Sum f
by Def9;
(
F = <*v,u*> or
F = <*u,v*> )
by A60, A64, A65, A66, FINSEQ_3:108;
then
( (
f (#) F = <*(v * (1_ R)),(u * (1_ R))*> or
f (#) F = <*(u * (1_ R)),(v * (1_ R))*> ) &
u * (1_ R) = u &
v * (1_ R) = v )
by A61, A62, Th35, VECTSP_2:def 23;
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 the carrier of R
for b2 being Element of the carrier of V holds
( not b2 in A or b2 * b1 in A )
by A48; :: thesis: verum