let V be RealUnitarySpace; :: 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, Th18;
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;
A5:
now let x,
y be
Element of
X;
:: thesis: ( S3[x,y] & S3[y,x] implies x = y )assume that A6:
S3[
x,
y]
and A7:
S3[
y,
x]
;
:: 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, RUSUB_1:20;
:: thesis: verum end;
A9:
now let x,
y,
z be
Element of
X;
:: thesis: ( S3[x,y] & S3[y,z] implies S3[x,z] )assume that A10:
S3[
x,
y]
and A11:
S3[
y,
z]
;
:: thesis: S3[x,z]consider 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, RUSUB_1:21;
hence
S3[
x,
z]
by A3, A12, A13;
:: 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
let Y be
set ;
:: thesis: ( 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] ) implies ex y being Element of X st
for x being Element of X st x in Y holds
S3[x,y] )
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
S3[x,y]
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
A34:
for
v1,
v2 being
VECTOR of
V st
v1 in Z &
v2 in Z holds
v1 + v2 in Z
proof
let v1,
v2 be
VECTOR of
V;
:: thesis: ( v1 in Z & v2 in Z implies v1 + v2 in Z )
assume that A35:
v1 in Z
and A36:
v2 in Z
;
:: thesis: v1 + v2 in Z
consider Y1 being
set such that A37:
v1 in Y1
and A38:
Y1 in rng f
by A35, TARSKI:def 4;
consider Y2 being
set such that A39:
v2 in Y2
and A40:
Y2 in rng f
by A36, TARSKI:def 4;
consider y1 being
set such that A41:
y1 in dom f
and A42:
f . y1 = Y1
by A38, FUNCT_1:def 5;
consider y2 being
set such that A43:
y2 in dom f
and A44:
f . y2 = Y2
by A40, FUNCT_1:def 5;
consider W1 being
strict Subspace of
V such that A45:
y1 = W1
and A46:
f . y1 = the
carrier of
W1
by A22, A23, A41;
consider W2 being
strict Subspace of
V such that A47:
y2 = W2
and A48:
f . y2 = the
carrier of
W2
by A22, A23, A43;
reconsider y1 =
y1,
y2 =
y2 as
Element of
X by A15, A22, A41, A43;
now per cases
( [y1,y2] in R or [y2,y1] in R )
by A16, A22, A41, A43;
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 A45, A47, RUSUB_1:def 1;
then
(
v1 in W2 &
v2 in W2 )
by A37, A39, A42, A44, A46, A48, STRUCT_0:def 5;
then
v1 + v2 in W2
by RUSUB_1:14;
then A49:
v1 + v2 in the
carrier of
W2
by STRUCT_0:def 5;
f . y2 in rng f
by A43, FUNCT_1:def 5;
hence
v1 + v2 in Z
by A48, A49, 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 A45, A47, RUSUB_1:def 1;
then
(
v1 in W1 &
v2 in W1 )
by A37, A39, A42, A44, A46, A48, STRUCT_0:def 5;
then
v1 + v2 in W1
by RUSUB_1:14;
then A50:
v1 + v2 in the
carrier of
W1
by STRUCT_0:def 5;
f . y1 in rng f
by A41, FUNCT_1:def 5;
hence
v1 + v2 in Z
by A46, A50, TARSKI:def 4;
:: thesis: verum end;
hence
v1 + v2 in Z
;
:: thesis: verum
end;
for
a being
Real for
v1 being
VECTOR of
V st
v1 in Z holds
a * v1 in Z
hence
Z is
linearly-closed
by A34, RLSUB_1:def 1;
:: thesis: verum
end; then consider E being
strict Subspace of
V such that A57:
Z = the
carrier of
E
by A33, RUSUB_1:29;
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 A58:
u in W /\ E
;
:: thesis: u in (0). V
then
u in E
by Th3;
then
u in Z
by A57, STRUCT_0:def 5;
then consider Y1 being
set such that A59:
u in Y1
and A60:
Y1 in rng f
by TARSKI:def 4;
consider y1 being
set such that A61:
y1 in dom f
and A62:
f . y1 = Y1
by A60, FUNCT_1:def 5;
consider W1 being
strict Subspace of
V such that A63:
y1 = W1
and A64:
f . y1 = the
carrier of
W1
by A22, A23, A61;
A65:
(
u in W1 &
u in W )
by A58, A59, A62, A64, Th3, STRUCT_0:def 5;
ex
W2 being
strict Subspace of
V st
(
y1 = W2 &
W /\ W2 = (0). V )
by A1, A15, A22, A61;
hence
u in (0). V
by A63, A65, Th3;
:: 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 RUSUB_1:def 2;
then
u = 0. V
by TARSKI:def 1;
hence
u in W /\ E
by RUSUB_1:11;
:: thesis: verum end; then A66:
W /\ E = (0). V
by RUSUB_1:25;
E in Subspaces V
by Def3;
then reconsider y' =
E as
Element of
X by A1, A66;
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 A67:
x in Y
;
:: thesis: [x,y] in Rthen consider W1 being
strict Subspace of
V such that A68:
x = W1
and A69:
f . x = the
carrier of
W1
by A23;
then
W1 is
strict Subspace of
E
by RUSUB_1:23;
hence
[x,y] in R
by A3, A68;
:: thesis: verum end;
hence
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
A71:
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
A72:
x = L
and
A73:
W /\ L = (0). V
by A1;
take
L
; :: thesis: V is_the_direct_sum_of L,W
thus
UNITSTR(# the carrier of V,the U2 of V,the U7 of V,the Mult of V,the scalar of V #) = L + W
:: according to RUSUB_2:def 4 :: thesis: L /\ W = (0). Vproof
assume
not
UNITSTR(# the
carrier of
V,the
U2 of
V,the
U7 of
V,the
Mult of
V,the
scalar of
V #)
= L + W
;
:: thesis: contradiction
then consider v being
VECTOR of
V such that A74:
for
v1,
v2 being
VECTOR of
V holds
( not
v1 in L or not
v2 in W or
v <> v1 + v2 )
by Lm13;
A75:
not
v in L + W
by A74, Th1;
set A =
{ (a * v) where a is Real : verum } ;
A76:
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 A81:
the
carrier of
Z = A
by A76, RUSUB_1:29;
then A85:
Z /\ (W + L) = (0). V
by RUSUB_1:25;
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 A86:
u in (Z + L) /\ W
;
:: thesis: u in (0). V
then
u in Z + L
by Th3;
then consider v1,
v2 being
VECTOR of
V such that A87:
v1 in Z
and A88:
v2 in L
and A89:
u = v1 + v2
by Th1;
A90:
v1 = u - v2
by A89, RLSUB_2:78;
A91:
u in W
by A86, Th3;
then
(
u in W + L &
v2 in W + L )
by A88, Th2;
then
v1 in W + L
by A90, RUSUB_1:17;
then
v1 in Z /\ (W + L)
by A87, Th3;
then
v1 in the
carrier of
((0). V)
by A85, STRUCT_0:def 5;
then
v1 in {(0. V)}
by RUSUB_1:def 2;
then
v1 = 0. V
by TARSKI:def 1;
then
v2 = u
by A89, RLVECT_1:10;
hence
u in (0). V
by A73, A88, A91, Th3;
:: 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 RUSUB_1:def 2;
then
u = 0. V
by TARSKI:def 1;
hence
u in (Z + L) /\ W
by RUSUB_1:11;
:: thesis: verum end;
then
(Z + L) /\ W = (0). V
by RUSUB_1:25;
then
(
W /\ (Z + L) = (0). V &
Z + L in Subspaces V )
by Def3, Th14;
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 RLVECT_1:10, RUSUB_1:11;
then A92:
not
v in L
by A74;
v in A
by A76, RLVECT_1:def 9;
then
v in Z
by A81, STRUCT_0:def 5;
then A93:
Z + L <> L
by A92, Th2;
L is
Subspace of
Z + L
by Th7;
then
[x,x1] in R
by A3, A72;
hence
contradiction
by A71, A72, A93;
:: thesis: verum
end;
thus
L /\ W = (0). V
by A73, Th14; :: thesis: verum