let V be RealUnitarySpace; 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; ex C being strict Subspace of V st V is_the_direct_sum_of C,W
defpred S1[ object ] 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 object 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[ object , object ] 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
A2:
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;
A3:
now for x, y, z being Element of X st S3[x,y] & S3[y,z] holds
S3[x,z]let x,
y,
z be
Element of
X;
( S3[x,y] & S3[y,z] implies S3[x,z] )assume that A4:
S3[
x,
y]
and A5:
S3[
y,
z]
;
S3[x,z]consider W1,
W2 being
strict Subspace of
V such that A6:
x = W1
and A7:
(
y = W2 &
W1 is
Subspace of
W2 )
by A2, A4;
consider W3,
W4 being
strict Subspace of
V such that A8:
y = W3
and A9:
z = W4
and A10:
W3 is
Subspace of
W4
by A2, A5;
W1 is
strict Subspace of
W4
by A7, A8, A10, RUSUB_1:21;
hence
S3[
x,
z]
by A2, A6, A9;
verum end;
A11:
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 ;
( 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 A12:
Y c= X
and A13:
for
x,
y being
Element of
X st
x in Y &
y in Y & not
[x,y] in R holds
[y,x] in R
;
ex y being Element of X st
for x being Element of X st x in Y holds
S3[x,y]
now ex y9 being Element of X st
for x being Element of X st x in Y holds
[x,y9] in Rper cases
( Y = {} or Y <> {} )
;
suppose A15:
Y <> {}
;
ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in Rdefpred S4[
object ,
object ]
means ex
W1 being
strict Subspace of
V st
( $1
= W1 & $2
= the
carrier of
W1 );
A16:
for
x being
object st
x in Y holds
ex
y being
object st
S4[
x,
y]
consider f being
Function such that A18:
dom f = Y
and A19:
for
x being
object st
x in Y holds
S4[
x,
f . x]
from CLASSES1:sch 1(A16);
set Z =
union (rng f);
set z = the
Element of
rng f;
A26:
rng f <> {}
by A15, A18, RELAT_1:42;
then consider z1 being
object such that A27:
z1 in dom f
and A28:
f . z1 = the
Element of
rng f
by FUNCT_1:def 3;
reconsider Z =
union (rng f) as
Subset of
V by A20, TARSKI:def 3;
ex
W3 being
strict Subspace of
V st
(
z1 = W3 &
f . z1 = the
carrier of
W3 )
by A18, A19, A27;
then A29:
Z <> {}
by A26, A28, ORDERS_1:6;
A30:
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;
( v1 in Z & v2 in Z implies v1 + v2 in Z )
assume that A31:
v1 in Z
and A32:
v2 in Z
;
v1 + v2 in Z
consider Y1 being
set such that A33:
v1 in Y1
and A34:
Y1 in rng f
by A31, TARSKI:def 4;
consider y1 being
object such that A35:
y1 in dom f
and A36:
f . y1 = Y1
by A34, FUNCT_1:def 3;
consider Y2 being
set such that A37:
v2 in Y2
and A38:
Y2 in rng f
by A32, TARSKI:def 4;
consider y2 being
object such that A39:
y2 in dom f
and A40:
f . y2 = Y2
by A38, FUNCT_1:def 3;
consider W1 being
strict Subspace of
V such that A41:
y1 = W1
and A42:
f . y1 = the
carrier of
W1
by A18, A19, A35;
consider W2 being
strict Subspace of
V such that A43:
y2 = W2
and A44:
f . y2 = the
carrier of
W2
by A18, A19, A39;
reconsider y1 =
y1,
y2 =
y2 as
Element of
X by A12, A18, A35, A39;
now v1 + v2 in Zper cases
( [y1,y2] in R or [y2,y1] in R )
by A13, A18, A35, A39;
suppose
[y1,y2] in R
;
v1 + v2 in Zthen
ex
W3,
W4 being
strict Subspace of
V st
(
y1 = W3 &
y2 = W4 &
W3 is
Subspace of
W4 )
by A2;
then
the
carrier of
W1 c= the
carrier of
W2
by A41, A43, RUSUB_1:def 1;
then A45:
v1 in W2
by A33, A36, A42, STRUCT_0:def 5;
v2 in W2
by A37, A40, A44, STRUCT_0:def 5;
then
v1 + v2 in W2
by A45, RUSUB_1:14;
then A46:
v1 + v2 in the
carrier of
W2
by STRUCT_0:def 5;
f . y2 in rng f
by A39, FUNCT_1:def 3;
hence
v1 + v2 in Z
by A44, A46, TARSKI:def 4;
verum end; suppose
[y2,y1] in R
;
v1 + v2 in Zthen
ex
W3,
W4 being
strict Subspace of
V st
(
y2 = W3 &
y1 = W4 &
W3 is
Subspace of
W4 )
by A2;
then
the
carrier of
W2 c= the
carrier of
W1
by A41, A43, RUSUB_1:def 1;
then A47:
v2 in W1
by A37, A40, A44, STRUCT_0:def 5;
v1 in W1
by A33, A36, A42, STRUCT_0:def 5;
then
v1 + v2 in W1
by A47, RUSUB_1:14;
then A48:
v1 + v2 in the
carrier of
W1
by STRUCT_0:def 5;
f . y1 in rng f
by A35, FUNCT_1:def 3;
hence
v1 + v2 in Z
by A42, A48, TARSKI:def 4;
verum end;
hence
v1 + v2 in Z
;
verum
end;
for
a being
Real for
v1 being
VECTOR of
V st
v1 in Z holds
a * v1 in Z
then
Z is
linearly-closed
by A30, RLSUB_1:def 1;
then consider E being
strict Subspace of
V such that A55:
Z = the
carrier of
E
by A29, RUSUB_1:29;
now for u being VECTOR of V holds
( ( u in W /\ E implies u in (0). V ) & ( u in (0). V implies u in W /\ E ) )let u be
VECTOR of
V;
( ( 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 )
( u in (0). V implies u in W /\ E )proof
assume A56:
u in W /\ E
;
u in (0). V
then A57:
u in W
by Th3;
u in E
by A56, Th3;
then
u in Z
by A55, 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
object such that A60:
y1 in dom f
and A61:
f . y1 = Y1
by A59, FUNCT_1:def 3;
A62:
ex
W2 being
strict Subspace of
V st
(
y1 = W2 &
W /\ W2 = (0). V )
by A1, A12, A18, A60;
consider W1 being
strict Subspace of
V such that A63:
y1 = W1
and A64:
f . y1 = the
carrier of
W1
by A18, A19, A60;
u in W1
by A58, A61, A64, STRUCT_0:def 5;
hence
u in (0). V
by A63, A57, A62, Th3;
verum
end; assume
u in (0). V
;
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;
verum end; then A65:
W /\ E = (0). V
by RUSUB_1:25;
E in Subspaces V
by Def3;
then reconsider y9 =
E as
Element of
X by A1, A65;
take y =
y9;
for x being Element of X st x in Y holds
[x,y] in Rlet x be
Element of
X;
( x in Y implies [x,y] in R )assume A66:
x in Y
;
[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 A19;
then
W1 is
strict Subspace of
E
by RUSUB_1:23;
hence
[x,y] in R
by A2, A67;
verum end;
hence
ex
y being
Element of
X st
for
x being
Element of
X st
x in Y holds
S3[
x,
y]
;
verum
end;
A71:
now for x being Element of X holds S3[x,x]end;
A72:
now for x, y being Element of X st S3[x,y] & S3[y,x] holds
x = yend;
consider x being Element of X such that
A73:
for y being Element of X st x <> y holds
not S3[x,y]
from ORDERS_1:sch 1(A71, A72, A3, A11);
consider L being strict Subspace of V such that
A74:
x = L
and
A75:
W /\ L = (0). V
by A1;
take
L
; V is_the_direct_sum_of L,W
thus
UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) = L + W
RUSUB_2:def 4 L /\ W = (0). Vproof
assume
not
UNITSTR(# the
carrier of
V, the
ZeroF of
V, the
U7 of
V, the
Mult of
V, the
scalar of
V #)
= L + W
;
contradiction
then consider v being
VECTOR of
V such that A76:
for
v1,
v2 being
VECTOR of
V holds
( not
v1 in L or not
v2 in W or
v <> v1 + v2 )
by Lm13;
(
v = (0. V) + v &
0. V in W )
by RLVECT_1:4, RUSUB_1:11;
then A77:
not
v in L
by A76;
set A =
{ (a * v) where a is Real : verum } ;
A78:
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;
A79:
for
v1,
v2 being
VECTOR of
V st
v1 in A &
v2 in A holds
v1 + v2 in A
proof
let v1,
v2 be
VECTOR of
V;
( v1 in A & v2 in A implies v1 + v2 in A )
assume
v1 in A
;
( not v2 in A or v1 + v2 in A )
then consider a1 being
Real such that A80:
v1 = a1 * v
;
assume
v2 in A
;
v1 + v2 in A
then consider a2 being
Real such that A81:
v2 = a2 * v
;
v1 + v2 = (a1 + a2) * v
by A80, A81, RLVECT_1:def 6;
hence
v1 + v2 in A
;
verum
end;
for
a being
Real for
v1 being
VECTOR of
V st
v1 in A holds
a * v1 in A
then
A is
linearly-closed
by A79, RLSUB_1:def 1;
then consider Z being
strict Subspace of
V such that A83:
the
carrier of
Z = A
by A78, RUSUB_1:29;
A84:
not
v in L + W
by A76, Th1;
then A88:
Z /\ (W + L) = (0). V
by RUSUB_1:25;
now for u being VECTOR of V holds
( ( u in (Z + L) /\ W implies u in (0). V ) & ( u in (0). V implies u in (Z + L) /\ W ) )let u be
VECTOR of
V;
( ( 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 )
( u in (0). V implies u in (Z + L) /\ W )proof
assume A89:
u in (Z + L) /\ W
;
u in (0). V
then
u in Z + L
by Th3;
then consider v1,
v2 being
VECTOR of
V such that A90:
v1 in Z
and A91:
v2 in L
and A92:
u = v1 + v2
by Th1;
A93:
u in W
by A89, Th3;
then A94:
u in W + L
by Th2;
(
v1 = u - v2 &
v2 in W + L )
by A91, A92, Th2, RLSUB_2:61;
then
v1 in W + L
by A94, RUSUB_1:17;
then
v1 in Z /\ (W + L)
by A90, Th3;
then
v1 in the
carrier of
((0). V)
by A88, 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 A92, RLVECT_1:4;
hence
u in (0). V
by A75, A91, A93, Th3;
verum
end; assume
u in (0). V
;
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;
verum end;
then
(Z + L) /\ W = (0). V
by RUSUB_1:25;
then A95:
W /\ (Z + L) = (0). V
by Th14;
Z + L in Subspaces V
by Def3;
then reconsider x1 =
Z + L as
Element of
X by A1, A95;
L is
Subspace of
Z + L
by Th7;
then A96:
[x,x1] in R
by A2, A74;
v in A
by A78, RLVECT_1:def 8;
then
v in Z
by A83, STRUCT_0:def 5;
then
Z + L <> L
by A77, Th2;
hence
contradiction
by A73, A74, A96;
verum
end;
thus
L /\ W = (0). V
by A75, Th14; verum