let V be RealLinearSpace; :: thesis: for W being Subspace of V ex C being strict Subspace of V st V is_the_direct_sum_of C,W
let W be Subspace of V; :: thesis: ex C being strict Subspace of V st V is_the_direct_sum_of C,W
defpred S1[ set ] means ex W1 being strict Subspace of V st
( $1 = W1 & W /\ W1 = (0). V );
consider X being set such that
A1:
for x being set holds
( x in X iff ( x in Subspaces V & S1[x] ) )
from XBOOLE_0:sch 1();
( W /\ ((0). V) = (0). V & (0). V in Subspaces V )
by Def3, Th22;
then reconsider X = X as non empty set by A1;
defpred S2[ set , set ] means ex W1, W2 being strict Subspace of V st
( $1 = W1 & $2 = W2 & W1 is Subspace of W2 );
consider R being Relation of X such that
A3:
for x, y being Element of X holds
( [x,y] in R iff S2[x,y] )
from RELSET_1:sch 2();
defpred S3[ set , set ] means [$1,$2] in R;
A4:
for x being Element of X holds S3[x,x]
A5:
for x, y being Element of X st S3[x,y] & S3[y,x] holds
x = y
proof
now let x,
y be
Element of
X;
:: thesis: ( [x,y] in R & [y,x] in R implies x = y )assume that A6:
[x,y] in R
and A7:
[y,x] in R
;
:: thesis: x = yA8:
ex
W1,
W2 being
strict Subspace of
V st
(
x = W1 &
y = W2 &
W1 is
Subspace of
W2 )
by A3, A6;
ex
W3,
W4 being
strict Subspace of
V st
(
y = W3 &
x = W4 &
W3 is
Subspace of
W4 )
by A3, A7;
hence
x = y
by A8, RLSUB_1:34;
:: thesis: verum end;
hence
for
x,
y being
Element of
X st
S3[
x,
y] &
S3[
y,
x] holds
x = y
;
:: thesis: verum
end;
A9:
for x, y, z being Element of X st S3[x,y] & S3[y,z] holds
S3[x,z]
proof
now let x,
y,
z be
Element of
X;
:: thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )assume that A10:
[x,y] in R
and A11:
[y,z] in R
;
:: thesis: [x,z] in Rconsider W1,
W2 being
strict Subspace of
V such that A12:
(
x = W1 &
y = W2 &
W1 is
Subspace of
W2 )
by A3, A10;
consider W3,
W4 being
strict Subspace of
V such that A13:
(
y = W3 &
z = W4 &
W3 is
Subspace of
W4 )
by A3, A11;
W1 is
strict Subspace of
W4
by A12, A13, RLSUB_1:35;
hence
[x,z] in R
by A3, A12, A13;
:: thesis: verum end;
hence
for
x,
y,
z being
Element of
X st
S3[
x,
y] &
S3[
y,
z] holds
S3[
x,
z]
;
:: thesis: verum
end;
A14:
for Y being set st Y c= X & ( for x, y being Element of X st x in Y & y in Y & not S3[x,y] holds
S3[y,x] ) holds
ex y being Element of X st
for x being Element of X st x in Y holds
S3[x,y]
proof
for
Y being
set st
Y c= X & ( for
x,
y being
Element of
X st
x in Y &
y in Y & not
[x,y] in R holds
[y,x] in R ) holds
ex
y being
Element of
X st
for
x being
Element of
X st
x in Y holds
[x,y] in R
proof
let Y be
set ;
:: thesis: ( Y c= X & ( for x, y being Element of X st x in Y & y in Y & not [x,y] in R holds
[y,x] in R ) implies ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in R )
assume that A15:
Y c= X
and A16:
for
x,
y being
Element of
X st
x in Y &
y in Y & not
[x,y] in R holds
[y,x] in R
;
:: thesis: ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in R
now per cases
( Y = {} or Y <> {} )
;
suppose A18:
Y <> {}
;
:: thesis: ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in Rdefpred S4[
set ,
set ]
means ex
W1 being
strict Subspace of
V st
( $1
= W1 & $2
= the
carrier of
W1 );
A20:
for
x being
set st
x in Y holds
ex
y being
set st
S4[
x,
y]
consider f being
Function such that A22:
dom f = Y
and A23:
for
x being
set st
x in Y holds
S4[
x,
f . x]
from CLASSES1:sch 1(A20);
set Z =
union (rng f);
then reconsider Z =
union (rng f) as
Subset of
V by TARSKI:def 3;
A29:
rng f <> {}
by A18, A22, RELAT_1:65;
consider z being
Element of
rng f;
consider z1 being
set such that A30:
z1 in dom f
and A31:
f . z1 = z
by A29, FUNCT_1:def 5;
consider W3 being
strict Subspace of
V such that A32:
(
z1 = W3 &
f . z1 = the
carrier of
W3 )
by A22, A23, A30;
A33:
Z <> {}
by A29, A31, A32, ORDERS_1:91;
Z is
linearly-closed
proof
thus
for
v1,
v2 being
VECTOR of
V st
v1 in Z &
v2 in Z holds
v1 + v2 in Z
:: according to RLSUB_1:def 1 :: thesis: for b1 being Element of REAL
for b2 being Element of the carrier of V holds
( not b2 in Z or b1 * b2 in Z )proof
let v1,
v2 be
VECTOR of
V;
:: thesis: ( v1 in Z & v2 in Z implies v1 + v2 in Z )
assume that A34:
v1 in Z
and A35:
v2 in Z
;
:: thesis: v1 + v2 in Z
consider Y1 being
set such that A36:
v1 in Y1
and A37:
Y1 in rng f
by A34, TARSKI:def 4;
consider Y2 being
set such that A38:
v2 in Y2
and A39:
Y2 in rng f
by A35, TARSKI:def 4;
consider y1 being
set such that A40:
y1 in dom f
and A41:
f . y1 = Y1
by A37, FUNCT_1:def 5;
consider y2 being
set such that A42:
y2 in dom f
and A43:
f . y2 = Y2
by A39, FUNCT_1:def 5;
consider W1 being
strict Subspace of
V such that A44:
y1 = W1
and A45:
f . y1 = the
carrier of
W1
by A22, A23, A40;
consider W2 being
strict Subspace of
V such that A46:
y2 = W2
and A47:
f . y2 = the
carrier of
W2
by A22, A23, A42;
reconsider y1 =
y1,
y2 =
y2 as
Element of
X by A15, A22, A40, A42;
now per cases
( [y1,y2] in R or [y2,y1] in R )
by A16, A22, A40, A42;
suppose
[y1,y2] in R
;
:: thesis: v1 + v2 in Zthen
ex
W3,
W4 being
strict Subspace of
V st
(
y1 = W3 &
y2 = W4 &
W3 is
Subspace of
W4 )
by A3;
then
the
carrier of
W1 c= the
carrier of
W2
by A44, A46, RLSUB_1:def 2;
then
(
v1 in W2 &
v2 in W2 )
by A36, A38, A41, A43, A45, A47, STRUCT_0:def 5;
then
v1 + v2 in W2
by RLSUB_1:28;
then A48:
v1 + v2 in the
carrier of
W2
by STRUCT_0:def 5;
f . y2 in rng f
by A42, FUNCT_1:def 5;
hence
v1 + v2 in Z
by A47, A48, TARSKI:def 4;
:: thesis: verum end; suppose
[y2,y1] in R
;
:: thesis: v1 + v2 in Zthen
ex
W3,
W4 being
strict Subspace of
V st
(
y2 = W3 &
y1 = W4 &
W3 is
Subspace of
W4 )
by A3;
then
the
carrier of
W2 c= the
carrier of
W1
by A44, A46, RLSUB_1:def 2;
then
(
v1 in W1 &
v2 in W1 )
by A36, A38, A41, A43, A45, A47, STRUCT_0:def 5;
then
v1 + v2 in W1
by RLSUB_1:28;
then A49:
v1 + v2 in the
carrier of
W1
by STRUCT_0:def 5;
f . y1 in rng f
by A40, FUNCT_1:def 5;
hence
v1 + v2 in Z
by A45, A49, TARSKI:def 4;
:: thesis: verum end;
hence
v1 + v2 in Z
;
:: thesis: verum
end;
let a be
Real;
:: thesis: for b1 being Element of the carrier of V holds
( not b1 in Z or a * b1 in Z )let v1 be
VECTOR of
V;
:: thesis: ( not v1 in Z or a * v1 in Z )
assume
v1 in Z
;
:: thesis: a * v1 in Z
then consider Y1 being
set such that A50:
v1 in Y1
and A51:
Y1 in rng f
by TARSKI:def 4;
consider y1 being
set such that A52:
y1 in dom f
and A53:
f . y1 = Y1
by A51, FUNCT_1:def 5;
consider W1 being
strict Subspace of
V such that
y1 = W1
and A54:
f . y1 = the
carrier of
W1
by A22, A23, A52;
v1 in W1
by A50, A53, A54, STRUCT_0:def 5;
then
a * v1 in W1
by RLSUB_1:29;
then A55:
a * v1 in the
carrier of
W1
by STRUCT_0:def 5;
f . y1 in rng f
by A52, FUNCT_1:def 5;
hence
a * v1 in Z
by A54, A55, TARSKI:def 4;
:: thesis: verum
end; then consider E being
strict Subspace of
V such that A56:
Z = the
carrier of
E
by A33, RLSUB_1:43;
now let u be
VECTOR of
V;
:: thesis: ( ( u in W /\ E implies u in (0). V ) & ( u in (0). V implies u in W /\ E ) )thus
(
u in W /\ E implies
u in (0). V )
:: thesis: ( u in (0). V implies u in W /\ E )proof
assume A57:
u in W /\ E
;
:: thesis: u in (0). V
then
u in E
by Th7;
then
u in Z
by A56, STRUCT_0:def 5;
then consider Y1 being
set such that A58:
u in Y1
and A59:
Y1 in rng f
by TARSKI:def 4;
consider y1 being
set such that A60:
y1 in dom f
and A61:
f . y1 = Y1
by A59, FUNCT_1:def 5;
consider W1 being
strict Subspace of
V such that A62:
y1 = W1
and A63:
f . y1 = the
carrier of
W1
by A22, A23, A60;
A64:
(
u in W1 &
u in W )
by A57, A58, A61, A63, Th7, STRUCT_0:def 5;
ex
W2 being
strict Subspace of
V st
(
y1 = W2 &
W /\ W2 = (0). V )
by A1, A15, A22, A60;
hence
u in (0). V
by A62, A64, Th7;
:: thesis: verum
end; assume
u in (0). V
;
:: thesis: u in W /\ Ethen
u in the
carrier of
((0). V)
by STRUCT_0:def 5;
then
u in {(0. V)}
by RLSUB_1:def 3;
then
u = 0. V
by TARSKI:def 1;
hence
u in W /\ E
by RLSUB_1:25;
:: thesis: verum end; then A65:
W /\ E = (0). V
by RLSUB_1:39;
E in Subspaces V
by Def3;
then reconsider y' =
E as
Element of
X by A1, A65;
take y =
y';
:: thesis: for x being Element of X st x in Y holds
[x,y] in Rlet x be
Element of
X;
:: thesis: ( x in Y implies [x,y] in R )assume A66:
x in Y
;
:: thesis: [x,y] in Rthen consider W1 being
strict Subspace of
V such that A67:
x = W1
and A68:
f . x = the
carrier of
W1
by A23;
then
W1 is
strict Subspace of
E
by RLSUB_1:37;
hence
[x,y] in R
by A3, A67;
:: thesis: verum end;
hence
ex
y being
Element of
X st
for
x being
Element of
X st
x in Y holds
[x,y] in R
;
:: thesis: verum
end;
hence
for
Y being
set st
Y c= X & ( for
x,
y being
Element of
X st
x in Y &
y in Y & not
S3[
x,
y] holds
S3[
y,
x] ) holds
ex
y being
Element of
X st
for
x being
Element of
X st
x in Y holds
S3[
x,
y]
;
:: thesis: verum
end;
consider x being Element of X such that
A70:
for y being Element of X st x <> y holds
not S3[x,y]
from ORDERS_1:sch 1(A4, A5, A9, A14);
consider L being strict Subspace of V such that
A71:
x = L
and
A72:
W /\ L = (0). V
by A1;
take
L
; :: thesis: V is_the_direct_sum_of L,W
thus
RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) = L + W
:: according to RLSUB_2:def 4 :: thesis: L /\ W = (0). Vproof
assume
not
RLSStruct(# the
carrier of
V,the
U2 of
V,the
addF of
V,the
Mult of
V #)
= L + W
;
:: thesis: contradiction
then consider v being
VECTOR of
V such that A73:
for
v1,
v2 being
VECTOR of
V holds
( not
v1 in L or not
v2 in W or
v <> v1 + v2 )
by Lm13;
A74:
not
v in L + W
by A73, Th5;
set A =
{ (a * v) where a is Real : verum } ;
A75:
1
* v in { (a * v) where a is Real : verum }
;
then reconsider A =
{ (a * v) where a is Real : verum } as
Subset of
V by TARSKI:def 3;
A is
linearly-closed
then consider Z being
strict Subspace of
V such that A79:
the
carrier of
Z = A
by A75, RLSUB_1:43;
then A83:
Z /\ (W + L) = (0). V
by RLSUB_1:39;
now let u be
VECTOR of
V;
:: thesis: ( ( u in (Z + L) /\ W implies u in (0). V ) & ( u in (0). V implies u in (Z + L) /\ W ) )thus
(
u in (Z + L) /\ W implies
u in (0). V )
:: thesis: ( u in (0). V implies u in (Z + L) /\ W )proof
assume A84:
u in (Z + L) /\ W
;
:: thesis: u in (0). V
then
u in Z + L
by Th7;
then consider v1,
v2 being
VECTOR of
V such that A85:
v1 in Z
and A86:
v2 in L
and A87:
u = v1 + v2
by Th5;
A88:
v1 = u - v2
by A87, Lm14;
A89:
u in W
by A84, Th7;
then
(
u in W + L &
v2 in W + L )
by A86, Th6;
then
v1 in W + L
by A88, RLSUB_1:31;
then
v1 in Z /\ (W + L)
by A85, Th7;
then
v1 in the
carrier of
((0). V)
by A83, STRUCT_0:def 5;
then
v1 in {(0. V)}
by RLSUB_1:def 3;
then
v1 = 0. V
by TARSKI:def 1;
then
v2 = u
by A87, RLVECT_1:10;
hence
u in (0). V
by A72, A86, A89, Th7;
:: thesis: verum
end; assume
u in (0). V
;
:: thesis: u in (Z + L) /\ Wthen
u in the
carrier of
((0). V)
by STRUCT_0:def 5;
then
u in {(0. V)}
by RLSUB_1:def 3;
then
u = 0. V
by TARSKI:def 1;
hence
u in (Z + L) /\ W
by RLSUB_1:25;
:: thesis: verum end;
then
(Z + L) /\ W = (0). V
by RLSUB_1:39;
then
(
W /\ (Z + L) = (0). V &
Z + L in Subspaces V )
by Def3, Th18;
then reconsider x1 =
Z + L as
Element of
X by A1;
(
v = (0. V) + v &
v = v + (0. V) &
0. V in W &
0. V in L )
by RLSUB_1:25, RLVECT_1:10;
then A90:
not
v in L
by A73;
v in A
by A75, RLVECT_1:def 9;
then
v in Z
by A79, STRUCT_0:def 5;
then A91:
Z + L <> L
by A90, Th6;
L is
Subspace of
Z + L
by Th11;
then
[x,x1] in R
by A3, A71;
hence
contradiction
by A70, A71, A91;
:: thesis: verum
end;
thus
L /\ W = (0). V
by A72, Th18; :: thesis: verum