let V be RealLinearSpace; 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[ 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 XFAMILY: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
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;
now for x, y, z being Element of X st [x,y] in R & [y,z] in R holds
[x,z] in Rlet x,
y,
z be
Element of
X;
( [x,y] in R & [y,z] in R implies [x,z] in R )assume that A3:
[x,y] in R
and A4:
[y,z] in R
;
[x,z] in Rconsider W1,
W2 being
strict Subspace of
V such that A5:
x = W1
and A6:
(
y = W2 &
W1 is
Subspace of
W2 )
by A2, A3;
consider W3,
W4 being
strict Subspace of
V such that A7:
y = W3
and A8:
z = W4
and A9:
W3 is
Subspace of
W4
by A2, A4;
W1 is
strict Subspace of
W4
by A6, A7, A9, RLSUB_1:27;
hence
[x,z] in R
by A2, A5, A8;
verum end;
then A10:
for x, y, z being Element of X st S3[x,y] & S3[y,z] holds
S3[x,z]
;
then A12:
for x being Element of X holds S3[x,x]
;
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 ;
( 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 A13:
Y c= X
and A14:
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
[x,y] in R
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 A16:
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 );
A17:
for
x being
object st
x in Y holds
ex
y being
object st
S4[
x,
y]
consider f being
Function such that A19:
dom f = Y
and A20:
for
x being
object st
x in Y holds
S4[
x,
f . x]
from CLASSES1:sch 1(A17);
set Z =
union (rng f);
then reconsider Z =
union (rng f) as
Subset of
V by TARSKI:def 3;
A26:
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
RLSUB_1:def 1 for b1 being object
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;
( v1 in Z & v2 in Z implies v1 + v2 in Z )
assume that A27:
v1 in Z
and A28:
v2 in Z
;
v1 + v2 in Z
consider Y1 being
set such that A29:
v1 in Y1
and A30:
Y1 in rng f
by A27, TARSKI:def 4;
consider y1 being
object such that A31:
y1 in dom f
and A32:
f . y1 = Y1
by A30, FUNCT_1:def 3;
consider Y2 being
set such that A33:
v2 in Y2
and A34:
Y2 in rng f
by A28, TARSKI:def 4;
consider y2 being
object such that A35:
y2 in dom f
and A36:
f . y2 = Y2
by A34, FUNCT_1:def 3;
consider W1 being
strict Subspace of
V such that A37:
y1 = W1
and A38:
f . y1 = the
carrier of
W1
by A19, A20, A31;
consider W2 being
strict Subspace of
V such that A39:
y2 = W2
and A40:
f . y2 = the
carrier of
W2
by A19, A20, A35;
reconsider y1 =
y1,
y2 =
y2 as
Element of
X by A13, A19, A31, A35;
now v1 + v2 in Zper cases
( [y1,y2] in R or [y2,y1] in R )
by A14, A19, A31, A35;
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 A37, A39, RLSUB_1:def 2;
then A41:
v1 in W2
by A29, A32, A38, STRUCT_0:def 5;
v2 in W2
by A33, A36, A40, STRUCT_0:def 5;
then
v1 + v2 in W2
by A41, RLSUB_1:20;
then A42:
v1 + v2 in the
carrier of
W2
by STRUCT_0:def 5;
f . y2 in rng f
by A35, FUNCT_1:def 3;
hence
v1 + v2 in Z
by A40, A42, 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 A37, A39, RLSUB_1:def 2;
then A43:
v2 in W1
by A33, A36, A40, STRUCT_0:def 5;
v1 in W1
by A29, A32, A38, STRUCT_0:def 5;
then
v1 + v2 in W1
by A43, RLSUB_1:20;
then A44:
v1 + v2 in the
carrier of
W1
by STRUCT_0:def 5;
f . y1 in rng f
by A31, FUNCT_1:def 3;
hence
v1 + v2 in Z
by A38, A44, TARSKI:def 4;
verum end;
hence
v1 + v2 in Z
;
verum
end;
let a be
Real;
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;
( not v1 in Z or a * v1 in Z )
assume
v1 in Z
;
a * v1 in Z
then consider Y1 being
set such that A45:
v1 in Y1
and A46:
Y1 in rng f
by TARSKI:def 4;
consider y1 being
object such that A47:
y1 in dom f
and A48:
f . y1 = Y1
by A46, FUNCT_1:def 3;
consider W1 being
strict Subspace of
V such that
y1 = W1
and A49:
f . y1 = the
carrier of
W1
by A19, A20, A47;
v1 in W1
by A45, A48, A49, STRUCT_0:def 5;
then
a * v1 in W1
by RLSUB_1:21;
then A50:
a * v1 in the
carrier of
W1
by STRUCT_0:def 5;
f . y1 in rng f
by A47, FUNCT_1:def 3;
hence
a * v1 in Z
by A49, A50, TARSKI:def 4;
verum
end; set z = the
Element of
rng f;
A51:
rng f <> {}
by A16, A19, RELAT_1:42;
then consider z1 being
object such that A52:
z1 in dom f
and A53:
f . z1 = the
Element of
rng f
by FUNCT_1:def 3;
ex
W3 being
strict Subspace of
V st
(
z1 = W3 &
f . z1 = the
carrier of
W3 )
by A19, A20, A52;
then
Z <> {}
by A51, A53, ORDERS_1:6;
then consider E being
strict Subspace of
V such that A54:
Z = the
carrier of
E
by A26, RLSUB_1:35;
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 A55:
u in W /\ E
;
u in (0). V
then A56:
u in W
by Th3;
u in E
by A55, Th3;
then
u in Z
by A54, STRUCT_0:def 5;
then consider Y1 being
set such that A57:
u in Y1
and A58:
Y1 in rng f
by TARSKI:def 4;
consider y1 being
object such that A59:
y1 in dom f
and A60:
f . y1 = Y1
by A58, FUNCT_1:def 3;
A61:
ex
W2 being
strict Subspace of
V st
(
y1 = W2 &
W /\ W2 = (0). V )
by A1, A13, A19, A59;
consider W1 being
strict Subspace of
V such that A62:
y1 = W1
and A63:
f . y1 = the
carrier of
W1
by A19, A20, A59;
u in W1
by A57, A60, A63, STRUCT_0:def 5;
hence
u in (0). V
by A62, A56, A61, 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 RLSUB_1:def 3;
then
u = 0. V
by TARSKI:def 1;
hence
u in W /\ E
by RLSUB_1:17;
verum end; then A64:
W /\ E = (0). V
by RLSUB_1:31;
E in Subspaces V
by Def3;
then reconsider y9 =
E as
Element of
X by A1, A64;
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 A65:
x in Y
;
[x,y] in Rthen consider W1 being
strict Subspace of
V such that A66:
x = W1
and A67:
f . x = the
carrier of
W1
by A20;
then
W1 is
strict Subspace of
E
by RLSUB_1:29;
hence
[x,y] in R
by A2, A66;
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
;
verum
end;
then A69:
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]
;
then A70:
for x, y being Element of X st S3[x,y] & S3[y,x] holds
x = y
;
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(A12, A70, A10, A69);
consider L being strict Subspace of V such that
A72:
x = L
and
A73:
W /\ L = (0). V
by A1;
take
L
; V is_the_direct_sum_of L,W
thus
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = L + W
RLSUB_2:def 4 L /\ W = (0). Vproof
assume
not
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V #)
= L + W
;
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;
(
v = (0. V) + v &
0. V in W )
by RLSUB_1:17;
then A75:
not
v in L
by A74;
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 A80:
the
carrier of
Z = A
by A76, RLSUB_1:35;
A81:
not
v in L + W
by A74, Th1;
then A85:
Z /\ (W + L) = (0). V
by RLSUB_1:31;
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 A86:
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 A87:
v1 in Z
and A88:
v2 in L
and A89:
u = v1 + v2
by Th1;
A90:
u in W
by A86, Th3;
then A91:
u in W + L
by Th2;
(
v1 = u - v2 &
v2 in W + L )
by A88, A89, Lm14, Th2;
then
v1 in W + L
by A91, RLSUB_1:23;
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 RLSUB_1:def 3;
then
v1 = 0. V
by TARSKI:def 1;
then
v2 = u
by A89;
hence
u in (0). V
by A73, A88, A90, 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 RLSUB_1:def 3;
then
u = 0. V
by TARSKI:def 1;
hence
u in (Z + L) /\ W
by RLSUB_1:17;
verum end;
then
(Z + L) /\ W = (0). V
by RLSUB_1:31;
then A92:
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, A92;
L is
Subspace of
Z + L
by Th7;
then A93:
[x,x1] in R
by A2, A72;
v in A
by A76, RLVECT_1:def 8;
then
v in Z
by A80, STRUCT_0:def 5;
then
Z + L <> L
by A75, Th2;
hence
contradiction
by A71, A72, A93;
verum
end;
thus
L /\ W = (0). V
by A73, Th14; verum