defpred S1[ set , set ] means ex W1, W2 being strict Subspace of V st
( $1 = W1 & $2 = W2 & W1 is Subspace of W2 );
defpred S2[ 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 & S2[x] ) )
from XFAMILY:sch 1();
( W /\ ((0). V) = (0). V & (0). V in Subspaces V )
by Def3, Th20;
then reconsider X = X as non empty set by A1;
consider R being Relation of X such that
A2:
for x, y being Element of X holds
( [x,y] in R iff S1[x,y] )
from RELSET_1:sch 2();
defpred S3[ set , set ] means [$1,$2] in R;
A3:
now for x, y being Element of X st S3[x,y] & S3[y,x] holds
x = yend;
A4:
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 A5:
Y c= X
and A6:
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 A8:
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 );
A9:
for
x being
object st
x in Y holds
ex
y being
object st
S4[
x,
y]
consider f being
Function such that A11:
dom f = Y
and A12:
for
x being
object st
x in Y holds
S4[
x,
f . x]
from CLASSES1:sch 1(A9);
set Z =
union (rng f);
then reconsider Z =
union (rng f) as
Subset of
V by TARSKI:def 3;
A18:
Z is
linearly-closed
proof
thus
for
v1,
v2 being
Element of
V st
v1 in Z &
v2 in Z holds
v1 + v2 in Z
VECTSP_4:def 1 for b1 being Element of the carrier of F
for b2 being Element of the carrier of V holds
( not b2 in Z or b1 * b2 in Z )proof
let v1,
v2 be
Element of
V;
( v1 in Z & v2 in Z implies v1 + v2 in Z )
assume that A19:
v1 in Z
and A20:
v2 in Z
;
v1 + v2 in Z
consider Y1 being
set such that A21:
v1 in Y1
and A22:
Y1 in rng f
by A19, TARSKI:def 4;
consider y1 being
object such that A23:
y1 in dom f
and A24:
f . y1 = Y1
by A22, FUNCT_1:def 3;
consider Y2 being
set such that A25:
v2 in Y2
and A26:
Y2 in rng f
by A20, TARSKI:def 4;
consider y2 being
object such that A27:
y2 in dom f
and A28:
f . y2 = Y2
by A26, FUNCT_1:def 3;
consider W1 being
strict Subspace of
V such that A29:
y1 = W1
and A30:
f . y1 = the
carrier of
W1
by A11, A12, A23;
consider W2 being
strict Subspace of
V such that A31:
y2 = W2
and A32:
f . y2 = the
carrier of
W2
by A11, A12, A27;
reconsider y1 =
y1,
y2 =
y2 as
Element of
X by A5, A11, A23, A27;
now v1 + v2 in Zper cases
( [y1,y2] in R or [y2,y1] in R )
by A6, A11, A23, A27;
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 A29, A31, VECTSP_4:def 2;
then A33:
v1 in W2
by A21, A24, A30, STRUCT_0:def 5;
v2 in W2
by A25, A28, A32, STRUCT_0:def 5;
then
v1 + v2 in W2
by A33, VECTSP_4:20;
then A34:
v1 + v2 in the
carrier of
W2
by STRUCT_0:def 5;
f . y2 in rng f
by A27, FUNCT_1:def 3;
hence
v1 + v2 in Z
by A32, A34, 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 A29, A31, VECTSP_4:def 2;
then A35:
v2 in W1
by A25, A28, A32, STRUCT_0:def 5;
v1 in W1
by A21, A24, A30, STRUCT_0:def 5;
then
v1 + v2 in W1
by A35, VECTSP_4:20;
then A36:
v1 + v2 in the
carrier of
W1
by STRUCT_0:def 5;
f . y1 in rng f
by A23, FUNCT_1:def 3;
hence
v1 + v2 in Z
by A30, A36, TARSKI:def 4;
verum end;
hence
v1 + v2 in Z
;
verum
end;
let a be
Element of
F;
for b1 being Element of the carrier of V holds
( not b1 in Z or a * b1 in Z )let v1 be
Element 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 A37:
v1 in Y1
and A38:
Y1 in rng f
by TARSKI:def 4;
consider y1 being
object such that A39:
y1 in dom f
and A40:
f . y1 = Y1
by A38, FUNCT_1:def 3;
consider W1 being
strict Subspace of
V such that
y1 = W1
and A41:
f . y1 = the
carrier of
W1
by A11, A12, A39;
v1 in W1
by A37, A40, A41, STRUCT_0:def 5;
then
a * v1 in W1
by VECTSP_4:21;
then A42:
a * v1 in the
carrier of
W1
by STRUCT_0:def 5;
f . y1 in rng f
by A39, FUNCT_1:def 3;
hence
a * v1 in Z
by A41, A42, TARSKI:def 4;
verum
end; set z = the
Element of
rng f;
A43:
rng f <> {}
by A8, A11, RELAT_1:42;
then consider z1 being
object such that A44:
z1 in dom f
and A45:
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 A11, A12, A44;
then
Z <> {}
by A43, A45, ORDERS_1:6;
then consider E being
strict Subspace of
V such that A46:
Z = the
carrier of
E
by A18, VECTSP_4:34;
now for u being Element of V holds
( ( u in W /\ E implies u in (0). V ) & ( u in (0). V implies u in W /\ E ) )let u be
Element 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 A47:
u in W /\ E
;
u in (0). V
then A48:
u in W
by Th3;
u in E
by A47, Th3;
then
u in Z
by A46, STRUCT_0:def 5;
then consider Y1 being
set such that A49:
u in Y1
and A50:
Y1 in rng f
by TARSKI:def 4;
consider y1 being
object such that A51:
y1 in dom f
and A52:
f . y1 = Y1
by A50, FUNCT_1:def 3;
A53:
ex
W2 being
strict Subspace of
V st
(
y1 = W2 &
W /\ W2 = (0). V )
by A1, A5, A11, A51;
consider W1 being
strict Subspace of
V such that A54:
y1 = W1
and A55:
f . y1 = the
carrier of
W1
by A11, A12, A51;
u in W1
by A49, A52, A55, STRUCT_0:def 5;
hence
u in (0). V
by A54, A48, A53, 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 VECTSP_4:def 3;
then
u = 0. V
by TARSKI:def 1;
hence
u in W /\ E
by VECTSP_4:17;
verum end; then A56:
W /\ E = (0). V
by VECTSP_4:30;
E in Subspaces V
by Def3;
then reconsider y9 =
E as
Element of
X by A1, A56;
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 A57:
x in Y
;
[x,y] in Rthen consider W1 being
strict Subspace of
V such that A58:
x = W1
and A59:
f . x = the
carrier of
W1
by A12;
then
W1 is
Subspace of
E
by VECTSP_4:28;
hence
[x,y] in R
by A2, A58;
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;
A61:
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 A62:
S3[
x,
y]
and A63:
S3[
y,
z]
;
S3[x,z]consider W1,
W2 being
strict Subspace of
V such that A64:
x = W1
and A65:
(
y = W2 &
W1 is
Subspace of
W2 )
by A2, A62;
consider W3,
W4 being
strict Subspace of
V such that A66:
y = W3
and A67:
z = W4
and A68:
W3 is
Subspace of
W4
by A2, A63;
W1 is
Subspace of
W4
by A65, A66, A68, VECTSP_4:26;
hence
S3[
x,
z]
by A2, A64, A67;
verum end;
A69:
now for x being Element of X holds S3[x,x]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(A69, A3, A61, A4);
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
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = L + W
VECTSP_5:def 4 L /\ W = (0). Vproof
assume
not
ModuleStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
lmult of
V #)
= L + W
;
contradiction
then consider v being
Element of
V such that A74:
for
v1,
v2 being
Element of
V holds
( not
v1 in L or not
v2 in W or
v <> v1 + v2 )
by Lm16;
(
v = (0. V) + v &
0. V in W )
by RLVECT_1:4, VECTSP_4:17;
then A75:
not
v in L
by A74;
set A =
{ (a * v) where a is Element of F : verum } ;
A76:
(1_ F) * v in { (a * v) where a is Element of F : verum }
;
then reconsider A =
{ (a * v) where a is Element of F : 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, VECTSP_4:34;
A81:
not
v in L + W
by A74, Th1;
then A85:
Z /\ (W + L) = (0). V
by VECTSP_4:30;
now for u being Element 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
Element 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
Element 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, Th2, VECTSP_2:2;
then
v1 in W + L
by A91, VECTSP_4: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 VECTSP_4:def 3;
then
v1 = 0. V
by TARSKI:def 1;
then
v2 = u
by A89, RLVECT_1:4;
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 VECTSP_4:def 3;
then
u = 0. V
by TARSKI:def 1;
hence
u in (Z + L) /\ W
by VECTSP_4:17;
verum end;
then A92:
W /\ (Z + L) = (0). V
by VECTSP_4:30;
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;
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; verum