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 S_{1}[ 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 & S_{1}[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 S_{2}[ 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 S_{2}[x,y] )
from RELSET_1:sch 2();

defpred S_{3}[ set , set ] means [$1,$2] in R;

_{3}[x,y] & S_{3}[y,z] holds

S_{3}[x,z]
;

_{3}[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_{3}[x,y] holds

S_{3}[y,x] ) holds

ex y being Element of X st

for x being Element of X st x in Y holds

S_{3}[x,y]
;

_{3}[x,y] & S_{3}[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 S_{3}[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 ; :: thesis: 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 :: according to RLSUB_2:def 4 :: thesis: L /\ W = (0). V

let W be Subspace of V; :: thesis: ex C being strict Subspace of V st V is_the_direct_sum_of C,W

defpred S

( $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 & S

( W /\ ((0). V) = (0). V & (0). V in Subspaces V ) by Def3, Th18;

then reconsider X = X as non empty set by A1;

defpred S

( $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 S

defpred S

now :: thesis: for x, y, z being Element of X st [x,y] in R & [y,z] in R holds

[x,z] in R

then A10:
for x, y, z being Element of X st S[x,z] in R

let x, y, z be Element of X; :: thesis: ( [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 ; :: thesis: [x,z] in R

consider 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; :: thesis: verum

end;assume that

A3: [x,y] in R and

A4: [y,z] in R ; :: thesis: [x,z] in R

consider 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; :: thesis: verum

S

A11: now :: thesis: for x being Element of X holds x is strict Subspace of V

let x be Element of X; :: thesis: x is strict Subspace of V

x in Subspaces V by A1;

hence x is strict Subspace of V by Def3; :: thesis: verum

end;x in Subspaces V by A1;

hence x is strict Subspace of V by Def3; :: thesis: verum

now :: thesis: for x being Element of X holds [x,x] in R

then A12:
for x being Element of X holds Slet x be Element of X; :: thesis: [x,x] in R

reconsider W = x as strict Subspace of V by A11;

W is Subspace of W by RLSUB_1:25;

hence [x,x] in R by A2; :: thesis: verum

end;reconsider W = x as strict Subspace of V by A11;

W is Subspace of W by RLSUB_1:25;

hence [x,x] in R by A2; :: thesis: verum

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

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 S
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

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 ; :: thesis: ex y being Element of X st

for x being Element of X st x in Y holds

[x,y] in R

for x being Element of X st x in Y holds

[x,y] in R ; :: thesis: verum

end;[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 ; :: thesis: ex y being Element of X st

for x being Element of X st x in Y holds

[x,y] in R

now :: thesis: ex y9 being Element of X st

for x being Element of X st x in Y holds

[x,y9] in Rend;

hence
ex y being Element of X st for x being Element of X st x in Y holds

[x,y9] in R

per cases
( Y = {} or Y <> {} )
;

end;

suppose A15:
Y = {}
; :: thesis: ex y9 being Element of X st

for x being Element of X st x in Y holds

[x,y9] in R

for x being Element of X st x in Y holds

[x,y9] in R

set y = the Element of X;

take y9 = the Element of X; :: thesis: for x being Element of X st x in Y holds

[x,y9] in R

let x be Element of X; :: thesis: ( x in Y implies [x,y9] in R )

assume x in Y ; :: thesis: [x,y9] in R

hence [x,y9] in R by A15; :: thesis: verum

end;take y9 = the Element of X; :: thesis: for x being Element of X st x in Y holds

[x,y9] in R

let x be Element of X; :: thesis: ( x in Y implies [x,y9] in R )

assume x in Y ; :: thesis: [x,y9] in R

hence [x,y9] in R by A15; :: thesis: verum

suppose A16:
Y <> {}
; :: thesis: ex y being Element of X st

for x being Element of X st x in Y holds

[x,y] in R

for x being Element of X st x in Y holds

[x,y] in R

defpred S_{4}[ 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 S_{4}[x,y]

A19: dom f = Y and

A20: for x being object st x in Y holds

S_{4}[x,f . x]
from CLASSES1:sch 1(A17);

set Z = union (rng f);

A26: Z is linearly-closed

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;

E in Subspaces V by Def3;

then reconsider y9 = E as Element of X by A1, A64;

take y = y9; :: thesis: for x being Element of X st x in Y holds

[x,y] in R

let x be Element of X; :: thesis: ( x in Y implies [x,y] in R )

assume A65: x in Y ; :: thesis: [x,y] in R

then consider W1 being strict Subspace of V such that

A66: x = W1 and

A67: f . x = the carrier of W1 by A20;

hence [x,y] in R by A2, A66; :: thesis: verum

end;( $1 = W1 & $2 = the carrier of W1 );

A17: for x being object st x in Y holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in Y implies ex y being object st S_{4}[x,y] )

assume x in Y ; :: thesis: ex y being object st S_{4}[x,y]

then consider W1 being strict Subspace of V such that

A18: x = W1 and

W /\ W1 = (0). V by A1, A13;

reconsider y = the carrier of W1 as set ;

take y ; :: thesis: S_{4}[x,y]

take W1 ; :: thesis: ( x = W1 & y = the carrier of W1 )

thus ( x = W1 & y = the carrier of W1 ) by A18; :: thesis: verum

end;assume x in Y ; :: thesis: ex y being object st S

then consider W1 being strict Subspace of V such that

A18: x = W1 and

W /\ W1 = (0). V by A1, A13;

reconsider y = the carrier of W1 as set ;

take y ; :: thesis: S

take W1 ; :: thesis: ( x = W1 & y = the carrier of W1 )

thus ( x = W1 & y = the carrier of W1 ) by A18; :: thesis: verum

A19: dom f = Y and

A20: for x being object st x in Y holds

S

set Z = union (rng f);

now :: thesis: for x being object st x in union (rng f) holds

x in the carrier of V

then reconsider Z = union (rng f) as Subset of V by TARSKI:def 3;x in the carrier of V

let x be object ; :: thesis: ( x in union (rng f) implies x in the carrier of V )

assume x in union (rng f) ; :: thesis: x in the carrier of V

then consider Y9 being set such that

A21: x in Y9 and

A22: Y9 in rng f by TARSKI:def 4;

consider y being object such that

A23: y in dom f and

A24: f . y = Y9 by A22, FUNCT_1:def 3;

consider W1 being strict Subspace of V such that

y = W1 and

A25: f . y = the carrier of W1 by A19, A20, A23;

the carrier of W1 c= the carrier of V by RLSUB_1:def 2;

hence x in the carrier of V by A21, A24, A25; :: thesis: verum

end;assume x in union (rng f) ; :: thesis: x in the carrier of V

then consider Y9 being set such that

A21: x in Y9 and

A22: Y9 in rng f by TARSKI:def 4;

consider y being object such that

A23: y in dom f and

A24: f . y = Y9 by A22, FUNCT_1:def 3;

consider W1 being strict Subspace of V such that

y = W1 and

A25: f . y = the carrier of W1 by A19, A20, A23;

the carrier of W1 c= the carrier of V by RLSUB_1:def 2;

hence x in the carrier of V by A21, A24, A25; :: thesis: verum

A26: Z is linearly-closed

proof

set z = the Element of rng f;
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 b_{1} being object

for b_{2} being Element of the carrier of V holds

( not b_{2} in Z or b_{1} * b_{2} in Z )_{1} being Element of the carrier of V holds

( not b_{1} in Z or a * b_{1} 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

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; :: thesis: verum

end;v1 + v2 in Z :: according to RLSUB_1:def 1 :: thesis: for b

for b

( not b

proof

let a be Real; :: thesis: for b
let v1, v2 be VECTOR of V; :: thesis: ( v1 in Z & v2 in Z implies v1 + v2 in Z )

assume that

A27: v1 in Z and

A28: v2 in Z ; :: thesis: 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;

end;assume that

A27: v1 in Z and

A28: v2 in Z ; :: thesis: 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 :: thesis: v1 + v2 in Zend;

hence
v1 + v2 in Z
; :: thesis: verumper cases
( [y1,y2] in R or [y2,y1] in R )
by A14, A19, A31, A35;

end;

suppose
[y1,y2] in R
; :: thesis: v1 + v2 in Z

then
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; :: thesis: verum

end;( 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; :: thesis: verum

suppose
[y2,y1] in R
; :: thesis: v1 + v2 in Z

then
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; :: thesis: verum

end;( 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; :: thesis: verum

( not b

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

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; :: thesis: verum

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 :: thesis: 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 ) )

then A64:
W /\ E = (0). V
by RLSUB_1:31;( ( u in W /\ E implies u in (0). V ) & ( u in (0). V implies u in W /\ E ) )

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 )

then 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; :: thesis: verum

end;thus ( u in W /\ E implies u in (0). V ) :: thesis: ( u in (0). V implies u in W /\ E )

proof

assume
u in (0). V
; :: thesis: u in W /\ E
assume A55:
u in W /\ E
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

then 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; :: thesis: verum

E in Subspaces V by Def3;

then reconsider y9 = E as Element of X by A1, A64;

take y = y9; :: thesis: for x being Element of X st x in Y holds

[x,y] in R

let x be Element of X; :: thesis: ( x in Y implies [x,y] in R )

assume A65: x in Y ; :: thesis: [x,y] in R

then consider W1 being strict Subspace of V such that

A66: x = W1 and

A67: f . x = the carrier of W1 by A20;

now :: thesis: for u being VECTOR of V st u in W1 holds

u in E

then
W1 is strict Subspace of E
by RLSUB_1:29;u in E

let u be VECTOR of V; :: thesis: ( u in W1 implies u in E )

assume u in W1 ; :: thesis: u in E

then A68: u in the carrier of W1 by STRUCT_0:def 5;

the carrier of W1 in rng f by A19, A65, A67, FUNCT_1:def 3;

then u in Z by A68, TARSKI:def 4;

hence u in E by A54, STRUCT_0:def 5; :: thesis: verum

end;assume u in W1 ; :: thesis: u in E

then A68: u in the carrier of W1 by STRUCT_0:def 5;

the carrier of W1 in rng f by A19, A65, A67, FUNCT_1:def 3;

then u in Z by A68, TARSKI:def 4;

hence u in E by A54, STRUCT_0:def 5; :: thesis: verum

hence [x,y] in R by A2, A66; :: thesis: verum

for x being Element of X st x in Y holds

[x,y] in R ; :: thesis: verum

S

ex y being Element of X st

for x being Element of X st x in Y holds

S

now :: thesis: for x, y being Element of X st [x,y] in R & [y,x] in R holds

x = y

then A70:
for x, y being Element of X st Sx = y

let x, y be Element of X; :: thesis: ( [x,y] in R & [y,x] in R implies x = y )

assume ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y

then ( ex W1, W2 being strict Subspace of V st

( x = W1 & y = W2 & W1 is Subspace of W2 ) & ex W3, W4 being strict Subspace of V st

( y = W3 & x = W4 & W3 is Subspace of W4 ) ) by A2;

hence x = y by RLSUB_1:26; :: thesis: verum

end;assume ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y

then ( ex W1, W2 being strict Subspace of V st

( x = W1 & y = W2 & W1 is Subspace of W2 ) & ex W3, W4 being strict Subspace of V st

( y = W3 & x = W4 & W3 is Subspace of W4 ) ) by A2;

hence x = y by RLSUB_1:26; :: thesis: verum

x = y ;

consider x being Element of X such that

A71: for y being Element of X st x <> y holds

not S

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 RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = L + W :: according to RLSUB_2:def 4 :: thesis: L /\ W = (0). V

proof

thus
L /\ W = (0). V
by A73, Th14; :: thesis: verum
assume
not RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult 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;

( 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 } ;

A is linearly-closed

A80: the carrier of Z = A by A76, RLSUB_1:35;

A81: not v in L + W by A74, Th1;

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; :: thesis: verum

end;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 } ;

now :: thesis: for x being object st x in { (a * v) where a is Real : verum } holds

x in the carrier of V

then reconsider A = { (a * v) where a is Real : verum } as Subset of V by TARSKI:def 3;x in the carrier of V

let x be object ; :: thesis: ( x in { (a * v) where a is Real : verum } implies x in the carrier of V )

assume x in { (a * v) where a is Real : verum } ; :: thesis: x in the carrier of V

then ex a being Real st x = a * v ;

hence x in the carrier of V ; :: thesis: verum

end;assume x in { (a * v) where a is Real : verum } ; :: thesis: x in the carrier of V

then ex a being Real st x = a * v ;

hence x in the carrier of V ; :: thesis: verum

A is linearly-closed

proof

then consider Z being strict Subspace of V such that
thus
for v1, v2 being VECTOR of V st v1 in A & v2 in A holds

v1 + v2 in A :: according to RLSUB_1:def 1 :: thesis: for b_{1} being object

for b_{2} being Element of the carrier of V holds

( not b_{2} in A or b_{1} * b_{2} in A )_{1} being Element of the carrier of V holds

( not b_{1} in A or a * b_{1} in A )

let v1 be VECTOR of V; :: thesis: ( not v1 in A or a * v1 in A )

assume v1 in A ; :: thesis: a * v1 in A

then consider a1 being Real such that

A79: v1 = a1 * v ;

a * v1 = (a * a1) * v by A79, RLVECT_1:def 7;

hence a * v1 in A ; :: thesis: verum

end;v1 + v2 in A :: according to RLSUB_1:def 1 :: thesis: for b

for b

( not b

proof

let a be Real; :: thesis: for b
let v1, v2 be VECTOR of V; :: thesis: ( v1 in A & v2 in A implies v1 + v2 in A )

assume v1 in A ; :: thesis: ( not v2 in A or v1 + v2 in A )

then consider a1 being Real such that

A77: v1 = a1 * v ;

assume v2 in A ; :: thesis: v1 + v2 in A

then consider a2 being Real such that

A78: v2 = a2 * v ;

v1 + v2 = (a1 + a2) * v by A77, A78, RLVECT_1:def 6;

hence v1 + v2 in A ; :: thesis: verum

end;assume v1 in A ; :: thesis: ( not v2 in A or v1 + v2 in A )

then consider a1 being Real such that

A77: v1 = a1 * v ;

assume v2 in A ; :: thesis: v1 + v2 in A

then consider a2 being Real such that

A78: v2 = a2 * v ;

v1 + v2 = (a1 + a2) * v by A77, A78, RLVECT_1:def 6;

hence v1 + v2 in A ; :: thesis: verum

( not b

let v1 be VECTOR of V; :: thesis: ( not v1 in A or a * v1 in A )

assume v1 in A ; :: thesis: a * v1 in A

then consider a1 being Real such that

A79: v1 = a1 * v ;

a * v1 = (a * a1) * v by A79, RLVECT_1:def 7;

hence a * v1 in A ; :: thesis: verum

A80: the carrier of Z = A by A76, RLSUB_1:35;

A81: not v in L + W by A74, Th1;

now :: thesis: for u being VECTOR of V holds

( ( u in Z /\ (W + L) implies u in (0). V ) & ( u in (0). V implies u in Z /\ (W + L) ) )

then A85:
Z /\ (W + L) = (0). V
by RLSUB_1:31;( ( u in Z /\ (W + L) implies u in (0). V ) & ( u in (0). V implies u in Z /\ (W + L) ) )

let u be VECTOR of V; :: thesis: ( ( u in Z /\ (W + L) implies u in (0). V ) & ( u in (0). V implies u in Z /\ (W + L) ) )

thus ( u in Z /\ (W + L) implies u in (0). V ) :: thesis: ( u in (0). V implies u in Z /\ (W + L) )

then 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 /\ (W + L) by RLSUB_1:17; :: thesis: verum

end;thus ( u in Z /\ (W + L) implies u in (0). V ) :: thesis: ( u in (0). V implies u in Z /\ (W + L) )

proof

assume
u in (0). V
; :: thesis: u in Z /\ (W + L)
assume A82:
u in Z /\ (W + L)
; :: thesis: u in (0). V

then u in Z by Th3;

then u in A by A80, STRUCT_0:def 5;

then consider a being Real such that

A83: u = a * v ;

hence u in (0). V by RLSUB_1:17; :: thesis: verum

end;then u in Z by Th3;

then u in A by A80, STRUCT_0:def 5;

then consider a being Real such that

A83: u = a * v ;

now :: thesis: not a <> 0

then
u = 0. V
by A83, RLVECT_1:10;
u in W + L
by A82, Th3;

then (a ") * (a * v) in W + L by A83, RLSUB_1:21;

then A84: ((a ") * a) * v in W + L by RLVECT_1:def 7;

assume a <> 0 ; :: thesis: contradiction

then 1 * v in W + L by A84, XCMPLX_0:def 7;

then 1 * v in L + W by Lm1;

hence contradiction by A81, RLVECT_1:def 8; :: thesis: verum

end;then (a ") * (a * v) in W + L by A83, RLSUB_1:21;

then A84: ((a ") * a) * v in W + L by RLVECT_1:def 7;

assume a <> 0 ; :: thesis: contradiction

then 1 * v in W + L by A84, XCMPLX_0:def 7;

then 1 * v in L + W by Lm1;

hence contradiction by A81, RLVECT_1:def 8; :: thesis: verum

hence u in (0). V by RLSUB_1:17; :: thesis: verum

then 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 /\ (W + L) by RLSUB_1:17; :: thesis: verum

now :: thesis: 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 ) )

then
(Z + L) /\ W = (0). V
by RLSUB_1:31;( ( 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; :: 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 )

then 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; :: thesis: verum

end;thus ( u in (Z + L) /\ W implies u in (0). V ) :: thesis: ( u in (0). V implies u in (Z + L) /\ W )

proof

assume
u in (0). V
; :: thesis: u in (Z + L) /\ W
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: 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; :: thesis: verum

end;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; :: thesis: verum

then 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; :: thesis: verum

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; :: thesis: verum