let R be Ring; 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; 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; ( 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
; ( ( 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 )
( ( 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 (Carrier l) = $1 holds
Sum l in A;
assume that A2:
A <> {}
and A3:
A is
linearly-closed
;
for l being Linear_Combination of A holds Sum l in A
then A4:
S1[
0 ]
;
now for k being Nat st ( for l being Linear_Combination of A st card (Carrier l) = k holds
Sum l in A ) holds
for l being Linear_Combination of A st card (Carrier l) = k + 1 holds
Sum l in Alet k be
Nat;
( ( 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
;
for l being Linear_Combination of A st card (Carrier l) = k + 1 holds
Sum l in Alet l be
Linear_Combination of
A;
( card (Carrier l) = k + 1 implies Sum l in A )deffunc H1(
Element of
V)
-> Element of the
carrier of
R =
l . $1;
consider F being
FinSequence of
V such that A6:
F is
one-to-one
and A7:
rng F = Carrier l
and A8:
Sum l = Sum (l (#) F)
by Def7;
reconsider G =
F | (Seg k) as
FinSequence of
V by FINSEQ_1:18;
assume A9:
card (Carrier l) = k + 1
;
Sum l in Athen A10:
len F = k + 1
by A6, A7, FINSEQ_4:62;
then A11:
len (l (#) F) = k + 1
by Def6;
A12:
k + 1
in Seg (k + 1)
by FINSEQ_1:4;
then A13:
k + 1
in dom F
by A10, FINSEQ_1:def 3;
k + 1
in dom F
by A10, A12, FINSEQ_1:def 3;
then reconsider v =
F . (k + 1) as
Vector of
V by FINSEQ_2:11;
consider f being
Function of
V,
R such that A14:
f . v = 0. R
and A15:
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:8;
A16:
v in Carrier l
by A7, A13, FUNCT_1:def 3;
then reconsider f =
f as
Linear_Combination of
V by Def2;
A18:
A \ {v} c= A
by XBOOLE_1:36;
A19:
Carrier l c= A
by Def5;
then A20:
v * (l . v) in A
by A3, A16;
A21:
Carrier f = (Carrier l) \ {v}
then
Carrier f c= A \ {v}
by A19, XBOOLE_1:33;
then
Carrier f c= A
by A18;
then reconsider f =
f as
Linear_Combination of
A by Def5;
A28:
len G = k
by A10, FINSEQ_3:53;
then A29:
len (f (#) G) = k
by Def6;
A30:
rng G = Carrier f
(Seg (k + 1)) /\ (Seg k) =
Seg k
by FINSEQ_1:7, NAT_1:12
.=
dom (f (#) G)
by A29, FINSEQ_1:def 3
;
then A40:
dom (f (#) G) = (dom (l (#) F)) /\ (Seg k)
by A11, 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 )A41:
rng F c= the
carrier of
V
by FINSEQ_1:def 4;
assume A42:
x in dom (f (#) G)
;
(f (#) G) . x = (l (#) F) . xthen reconsider n =
x as
Nat by FINSEQ_3:23;
n in dom (l (#) F)
by A40, A42, XBOOLE_0:def 4;
then A43:
n in dom F
by A10, A11, FINSEQ_3:29;
then
F . n in rng F
by FUNCT_1:def 3;
then reconsider w =
F . n as
Vector of
V by A41;
A44:
n in dom G
by A28, A29, A42, FINSEQ_3:29;
then A45:
G . n in rng G
by FUNCT_1:def 3;
rng G c= the
carrier of
V
by FINSEQ_1:def 4;
then reconsider u =
G . n as
Vector of
V by A45;
not
u in {v}
by A21, A30, A45, XBOOLE_0:def 5;
then A46:
u <> v
by TARSKI:def 1;
A47:
(f (#) G) . n =
u * (f . u)
by A44, Th23
.=
u * (l . u)
by A15, A46
;
w = u
by A44, FUNCT_1:47;
hence
(f (#) G) . x = (l (#) F) . x
by A47, A43, Th23;
verum end; then
f (#) G = (l (#) F) | (Seg k)
by A40, FUNCT_1:46;
then A48:
f (#) G = (l (#) F) | (dom (f (#) G))
by A29, FINSEQ_1:def 3;
v in rng F
by A13, FUNCT_1:def 3;
then
{v} c= Carrier l
by A7, ZFMISC_1:31;
then card (Carrier f) =
(k + 1) - (card {v})
by A9, A21, CARD_2:44
.=
(k + 1) - 1
by CARD_1:30
.=
k
by XCMPLX_1:26
;
then A49:
Sum f in A
by A5;
G is
one-to-one
by A6, FUNCT_1:52;
then A50:
Sum (f (#) G) = Sum f
by A30, Def7;
(l (#) F) . (len F) = v * (l . v)
by A10, A13, Th23;
then
Sum (l (#) F) = (Sum (f (#) G)) + (v * (l . v))
by A10, A11, A29, A48, RLVECT_1:38;
hence
Sum l in A
by A3, A8, A20, A50, A49;
verum end;
then A51:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
;
let l be
Linear_Combination of
A;
Sum l in A
A52:
card (Carrier l) = card (Carrier l)
;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A4, A51);
hence
Sum l in A
by A52;
verum
end;
assume A53:
for l being Linear_Combination of A holds Sum l in A
; ( A <> {} & A is linearly-closed )
hence
A <> {}
; A is linearly-closed
( ZeroLC V is Linear_Combination of A & Sum (ZeroLC V) = 0. V )
by Lm3, Th20;
then A54:
0. V in A
by A53;
A55:
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
RMOD_2:def 1 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;
( v in A & u in A implies v + u in A )
assume that A65:
v in A
and A66:
u in A
;
v + u in A
now v + u in Aper cases
( u = v or v <> u )
;
suppose A67:
v <> u
;
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 A68:
(
f . v = 1_ R &
f . u = 1_ R )
and A69:
for
w being
Element of
V st
w <> v &
w <> u holds
f . w = H1(
w)
from FUNCT_2:sch 7(A67);
reconsider f =
f as
Element of
Funcs ( the
carrier of
V, the
carrier of
R)
by FUNCT_2:8;
then reconsider f =
f as
Linear_Combination of
V by Def2;
A70:
Carrier f = {v,u}
then A71:
Carrier f c= A
by A65, A66, ZFMISC_1:32;
A72:
(
u * (1_ R) = u &
v * (1_ R) = v )
by VECTSP_2:def 9;
reconsider f =
f as
Linear_Combination of
A by A71, Def5;
consider F being
FinSequence of
V such that A73:
(
F is
one-to-one &
rng F = Carrier f )
and A74:
Sum (f (#) F) = Sum f
by Def7;
(
F = <*v,u*> or
F = <*u,v*> )
by A67, A70, A73, FINSEQ_3:99;
then
(
f (#) F = <*(v * (1_ R)),(u * (1_ R))*> or
f (#) F = <*(u * (1_ R)),(v * (1_ R))*> )
by A68, Th26;
then
Sum f = v + u
by A74, A72, RLVECT_1:45;
hence
v + u in A
by A53;
verum end;
hence
v + u in A
;
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 A55; verum