let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

ex W being strict Subspace of V st V1 = the carrier of W

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

ex W being strict Subspace of V st V1 = the carrier of W

let V1 be Subset of V; :: thesis: ( V1 <> {} & V1 is linearly-closed implies ex W being strict Subspace of V st V1 = the carrier of W )

assume that

A1: V1 <> {} and

A2: V1 is linearly-closed ; :: thesis: ex W being strict Subspace of V st V1 = the carrier of W

reconsider D = V1 as non empty set by A1;

reconsider d = 0. V as Element of D by A2, Th1;

set VV = the carrier of V;

set C = (comp V) | D;

dom (comp V) = the carrier of V by FUNCT_2:def 1;

then A3: dom ((comp V) | D) = D by RELAT_1:62;

A4: rng ((comp V) | D) c= D

dom the lmult of V = [: the carrier of GF, the carrier of V:] by FUNCT_2:def 1;

then A7: dom ( the lmult of V | [: the carrier of GF,D:]) = [: the carrier of GF,D:] by RELAT_1:62, ZFMISC_1:96;

A8: rng ( the lmult of V | [: the carrier of GF,D:]) c= D

dom the addF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def 1;

then A13: dom ( the addF of V || D) = [:D,D:] by RELAT_1:62, ZFMISC_1:96;

A14: rng ( the addF of V || D) c= D

reconsider C = (comp V) | D as UnOp of D by A3, A4, FUNCT_2:def 1, RELSET_1:4;

reconsider A = the addF of V || D as BinOp of D by A13, A14, FUNCT_2:def 1, RELSET_1:4;

set W = ModuleStr(# D,A,d,M #);

A19: for a, b being Element of ModuleStr(# D,A,d,M #)

for x, y being Element of V st x = a & b = y holds

a + b = x + y

0. W = 0. V ;

then reconsider W = W as strict Subspace of V by Def2;

take W ; :: thesis: V1 = the carrier of W

thus V1 = the carrier of W ; :: thesis: verum

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

ex W being strict Subspace of V st V1 = the carrier of W

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

ex W being strict Subspace of V st V1 = the carrier of W

let V1 be Subset of V; :: thesis: ( V1 <> {} & V1 is linearly-closed implies ex W being strict Subspace of V st V1 = the carrier of W )

assume that

A1: V1 <> {} and

A2: V1 is linearly-closed ; :: thesis: ex W being strict Subspace of V st V1 = the carrier of W

reconsider D = V1 as non empty set by A1;

reconsider d = 0. V as Element of D by A2, Th1;

set VV = the carrier of V;

set C = (comp V) | D;

dom (comp V) = the carrier of V by FUNCT_2:def 1;

then A3: dom ((comp V) | D) = D by RELAT_1:62;

A4: rng ((comp V) | D) c= D

proof

set M = the lmult of V | [: the carrier of GF,D:];
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((comp V) | D) or x in D )

assume x in rng ((comp V) | D) ; :: thesis: x in D

then consider y being object such that

A5: y in dom ((comp V) | D) and

A6: ((comp V) | D) . y = x by FUNCT_1:def 3;

reconsider y = y as Element of V by A3, A5;

x = (comp V) . y by A5, A6, FUNCT_1:47

.= - y by VECTSP_1:def 13 ;

hence x in D by A2, A3, A5, Th2; :: thesis: verum

end;assume x in rng ((comp V) | D) ; :: thesis: x in D

then consider y being object such that

A5: y in dom ((comp V) | D) and

A6: ((comp V) | D) . y = x by FUNCT_1:def 3;

reconsider y = y as Element of V by A3, A5;

x = (comp V) . y by A5, A6, FUNCT_1:47

.= - y by VECTSP_1:def 13 ;

hence x in D by A2, A3, A5, Th2; :: thesis: verum

dom the lmult of V = [: the carrier of GF, the carrier of V:] by FUNCT_2:def 1;

then A7: dom ( the lmult of V | [: the carrier of GF,D:]) = [: the carrier of GF,D:] by RELAT_1:62, ZFMISC_1:96;

A8: rng ( the lmult of V | [: the carrier of GF,D:]) c= D

proof

set A = the addF of V || D;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ( the lmult of V | [: the carrier of GF,D:]) or x in D )

assume x in rng ( the lmult of V | [: the carrier of GF,D:]) ; :: thesis: x in D

then consider y being object such that

A9: y in dom ( the lmult of V | [: the carrier of GF,D:]) and

A10: ( the lmult of V | [: the carrier of GF,D:]) . y = x by FUNCT_1:def 3;

consider y1, y2 being object such that

A11: [y1,y2] = y by A7, A9, RELAT_1:def 1;

reconsider y1 = y1 as Element of GF by A7, A9, A11, ZFMISC_1:87;

A12: y2 in V1 by A7, A9, A11, ZFMISC_1:87;

then reconsider y2 = y2 as Element of V ;

x = y1 * y2 by A9, A10, A11, FUNCT_1:47;

hence x in D by A2, A12; :: thesis: verum

end;assume x in rng ( the lmult of V | [: the carrier of GF,D:]) ; :: thesis: x in D

then consider y being object such that

A9: y in dom ( the lmult of V | [: the carrier of GF,D:]) and

A10: ( the lmult of V | [: the carrier of GF,D:]) . y = x by FUNCT_1:def 3;

consider y1, y2 being object such that

A11: [y1,y2] = y by A7, A9, RELAT_1:def 1;

reconsider y1 = y1 as Element of GF by A7, A9, A11, ZFMISC_1:87;

A12: y2 in V1 by A7, A9, A11, ZFMISC_1:87;

then reconsider y2 = y2 as Element of V ;

x = y1 * y2 by A9, A10, A11, FUNCT_1:47;

hence x in D by A2, A12; :: thesis: verum

dom the addF of V = [: the carrier of V, the carrier of V:] by FUNCT_2:def 1;

then A13: dom ( the addF of V || D) = [:D,D:] by RELAT_1:62, ZFMISC_1:96;

A14: rng ( the addF of V || D) c= D

proof

reconsider M = the lmult of V | [: the carrier of GF,D:] as Function of [: the carrier of GF,D:],D by A7, A8, FUNCT_2:def 1, RELSET_1:4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ( the addF of V || D) or x in D )

assume x in rng ( the addF of V || D) ; :: thesis: x in D

then consider y being object such that

A15: y in dom ( the addF of V || D) and

A16: ( the addF of V || D) . y = x by FUNCT_1:def 3;

consider y1, y2 being object such that

A17: [y1,y2] = y by A13, A15, RELAT_1:def 1;

A18: ( y1 in D & y2 in D ) by A13, A15, A17, ZFMISC_1:87;

then reconsider y1 = y1, y2 = y2 as Element of V ;

x = y1 + y2 by A15, A16, A17, FUNCT_1:47;

hence x in D by A2, A18; :: thesis: verum

end;assume x in rng ( the addF of V || D) ; :: thesis: x in D

then consider y being object such that

A15: y in dom ( the addF of V || D) and

A16: ( the addF of V || D) . y = x by FUNCT_1:def 3;

consider y1, y2 being object such that

A17: [y1,y2] = y by A13, A15, RELAT_1:def 1;

A18: ( y1 in D & y2 in D ) by A13, A15, A17, ZFMISC_1:87;

then reconsider y1 = y1, y2 = y2 as Element of V ;

x = y1 + y2 by A15, A16, A17, FUNCT_1:47;

hence x in D by A2, A18; :: thesis: verum

reconsider C = (comp V) | D as UnOp of D by A3, A4, FUNCT_2:def 1, RELSET_1:4;

reconsider A = the addF of V || D as BinOp of D by A13, A14, FUNCT_2:def 1, RELSET_1:4;

set W = ModuleStr(# D,A,d,M #);

A19: for a, b being Element of ModuleStr(# D,A,d,M #)

for x, y being Element of V st x = a & b = y holds

a + b = x + y

proof

A21:
( ModuleStr(# D,A,d,M #) is Abelian & ModuleStr(# D,A,d,M #) is add-associative & ModuleStr(# D,A,d,M #) is right_zeroed & ModuleStr(# D,A,d,M #) is right_complementable )
let a, b be Element of ModuleStr(# D,A,d,M #); :: thesis: for x, y being Element of V st x = a & b = y holds

a + b = x + y

let x, y be Element of V; :: thesis: ( x = a & b = y implies a + b = x + y )

assume A20: ( x = a & b = y ) ; :: thesis: a + b = x + y

thus a + b = A . [a,b]

.= x + y by A13, A20, FUNCT_1:47 ; :: thesis: verum

end;a + b = x + y

let x, y be Element of V; :: thesis: ( x = a & b = y implies a + b = x + y )

assume A20: ( x = a & b = y ) ; :: thesis: a + b = x + y

thus a + b = A . [a,b]

.= x + y by A13, A20, FUNCT_1:47 ; :: thesis: verum

proof

A23:
ModuleStr(# D,A,d,M #) is vector-distributive
thus
ModuleStr(# D,A,d,M #) is Abelian
:: thesis: ( ModuleStr(# D,A,d,M #) is add-associative & ModuleStr(# D,A,d,M #) is right_zeroed & ModuleStr(# D,A,d,M #) is right_complementable )

reconsider x = a as Element of V by TARSKI:def 3;

reconsider a9 = a as Element of D ;

reconsider b = C . a9 as Element of D ;

reconsider b = b as Element of ModuleStr(# D,A,d,M #) ;

take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. ModuleStr(# D,A,d,M #)

thus a + b = x + ((comp V) . x) by A3, A19, FUNCT_1:47

.= x + (- x) by VECTSP_1:def 13

.= 0. ModuleStr(# D,A,d,M #) by RLVECT_1:5 ; :: thesis: verum

end;proof

let a, b be Element of ModuleStr(# D,A,d,M #); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a

reconsider x = a, y = b as Element of V by TARSKI:def 3;

thus a + b = y + x by A19

.= b + a by A19 ; :: thesis: verum

end;reconsider x = a, y = b as Element of V by TARSKI:def 3;

thus a + b = y + x by A19

.= b + a by A19 ; :: thesis: verum

hereby :: according to RLVECT_1:def 3 :: thesis: ( ModuleStr(# D,A,d,M #) is right_zeroed & ModuleStr(# D,A,d,M #) is right_complementable )

let a, b, c be Element of ModuleStr(# D,A,d,M #); :: thesis: (a + b) + c = a + (b + c)

reconsider x = a, y = b, z = c as Element of V by TARSKI:def 3;

A22: b + c = y + z by A19;

a + b = x + y by A19;

hence (a + b) + c = (x + y) + z by A19

.= x + (y + z) by RLVECT_1:def 3

.= a + (b + c) by A19, A22 ;

:: thesis: verum

end;reconsider x = a, y = b, z = c as Element of V by TARSKI:def 3;

A22: b + c = y + z by A19;

a + b = x + y by A19;

hence (a + b) + c = (x + y) + z by A19

.= x + (y + z) by RLVECT_1:def 3

.= a + (b + c) by A19, A22 ;

:: thesis: verum

hereby :: according to RLVECT_1:def 4 :: thesis: ModuleStr(# D,A,d,M #) is right_complementable

let a be Element of ModuleStr(# D,A,d,M #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable let a be Element of ModuleStr(# D,A,d,M #); :: thesis: a + (0. ModuleStr(# D,A,d,M #)) = a

reconsider x = a as Element of V by TARSKI:def 3;

thus a + (0. ModuleStr(# D,A,d,M #)) = x + (0. V) by A19

.= a by RLVECT_1:4 ; :: thesis: verum

end;reconsider x = a as Element of V by TARSKI:def 3;

thus a + (0. ModuleStr(# D,A,d,M #)) = x + (0. V) by A19

.= a by RLVECT_1:4 ; :: thesis: verum

reconsider x = a as Element of V by TARSKI:def 3;

reconsider a9 = a as Element of D ;

reconsider b = C . a9 as Element of D ;

reconsider b = b as Element of ModuleStr(# D,A,d,M #) ;

take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. ModuleStr(# D,A,d,M #)

thus a + b = x + ((comp V) . x) by A3, A19, FUNCT_1:47

.= x + (- x) by VECTSP_1:def 13

.= 0. ModuleStr(# D,A,d,M #) by RLVECT_1:5 ; :: thesis: verum

proof

A28:
ModuleStr(# D,A,d,M #) is scalar-distributive
let a be Element of GF; :: according to VECTSP_1:def 13 :: thesis: for b_{1}, b_{2} being Element of the carrier of ModuleStr(# D,A,d,M #) holds a * (b_{1} + b_{2}) = (a * b_{1}) + (a * b_{2})

let v, w be Element of ModuleStr(# D,A,d,M #); :: thesis: a * (v + w) = (a * v) + (a * w)

reconsider x = v, y = w as Element of V by TARSKI:def 3;

A27: a * w = a * y by A24;

v + w = x + y by A19;

hence a * (v + w) = a * (x + y) by A24

.= (a * x) + (a * y) by VECTSP_1:def 14

.= (a * v) + (a * w) by A19, A26, A27 ;

:: thesis: verum

end;let v, w be Element of ModuleStr(# D,A,d,M #); :: thesis: a * (v + w) = (a * v) + (a * w)

reconsider x = v, y = w as Element of V by TARSKI:def 3;

A24: now :: thesis: for a being Element of GF

for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

then A26:
a * v = a * x
;for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

let a be Element of GF; :: thesis: for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

let x be Element of ModuleStr(# D,A,d,M #); :: thesis: for y being Element of V st y = x holds

a * x = a * y

let y be Element of V; :: thesis: ( y = x implies a * x = a * y )

assume A25: y = x ; :: thesis: a * x = a * y

[a,x] in dom M by A7;

hence a * x = a * y by A25, FUNCT_1:47; :: thesis: verum

end;for y being Element of V st y = x holds

a * x = a * y

let x be Element of ModuleStr(# D,A,d,M #); :: thesis: for y being Element of V st y = x holds

a * x = a * y

let y be Element of V; :: thesis: ( y = x implies a * x = a * y )

assume A25: y = x ; :: thesis: a * x = a * y

[a,x] in dom M by A7;

hence a * x = a * y by A25, FUNCT_1:47; :: thesis: verum

A27: a * w = a * y by A24;

v + w = x + y by A19;

hence a * (v + w) = a * (x + y) by A24

.= (a * x) + (a * y) by VECTSP_1:def 14

.= (a * v) + (a * w) by A19, A26, A27 ;

:: thesis: verum

proof

A33:
ModuleStr(# D,A,d,M #) is scalar-associative
let a, b be Element of GF; :: according to VECTSP_1:def 14 :: thesis: for b_{1} being Element of the carrier of ModuleStr(# D,A,d,M #) holds (a + b) * b_{1} = (a * b_{1}) + (b * b_{1})

let v be Element of ModuleStr(# D,A,d,M #); :: thesis: (a + b) * v = (a * v) + (b * v)

reconsider x = v as Element of V by TARSKI:def 3;

A32: b * v = b * x by A29;

thus (a + b) * v = (a + b) * x by A29

.= (a * x) + (b * x) by VECTSP_1:def 15

.= (a * v) + (b * v) by A19, A32, A31 ; :: thesis: verum

end;let v be Element of ModuleStr(# D,A,d,M #); :: thesis: (a + b) * v = (a * v) + (b * v)

reconsider x = v as Element of V by TARSKI:def 3;

A29: now :: thesis: for a being Element of GF

for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

then A31:
a * v = a * x
;for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

let a be Element of GF; :: thesis: for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

let x be Element of ModuleStr(# D,A,d,M #); :: thesis: for y being Element of V st y = x holds

a * x = a * y

let y be Element of V; :: thesis: ( y = x implies a * x = a * y )

assume A30: y = x ; :: thesis: a * x = a * y

[a,x] in dom M by A7;

hence a * x = a * y by A30, FUNCT_1:47; :: thesis: verum

end;for y being Element of V st y = x holds

a * x = a * y

let x be Element of ModuleStr(# D,A,d,M #); :: thesis: for y being Element of V st y = x holds

a * x = a * y

let y be Element of V; :: thesis: ( y = x implies a * x = a * y )

assume A30: y = x ; :: thesis: a * x = a * y

[a,x] in dom M by A7;

hence a * x = a * y by A30, FUNCT_1:47; :: thesis: verum

A32: b * v = b * x by A29;

thus (a + b) * v = (a + b) * x by A29

.= (a * x) + (b * x) by VECTSP_1:def 15

.= (a * v) + (b * v) by A19, A32, A31 ; :: thesis: verum

proof

ModuleStr(# D,A,d,M #) is scalar-unital
let a, b be Element of GF; :: according to VECTSP_1:def 15 :: thesis: for b_{1} being Element of the carrier of ModuleStr(# D,A,d,M #) holds (a * b) * b_{1} = a * (b * b_{1})

let v be Element of ModuleStr(# D,A,d,M #); :: thesis: (a * b) * v = a * (b * v)

reconsider x = v as Element of V by TARSKI:def 3;

thus (a * b) * v = (a * b) * x by A34

.= a * (b * x) by VECTSP_1:def 16

.= a * (b * v) by A34, A36 ; :: thesis: verum

end;let v be Element of ModuleStr(# D,A,d,M #); :: thesis: (a * b) * v = a * (b * v)

reconsider x = v as Element of V by TARSKI:def 3;

A34: now :: thesis: for a being Element of GF

for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

then A36:
b * v = b * x
;for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

let a be Element of GF; :: thesis: for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

let x be Element of ModuleStr(# D,A,d,M #); :: thesis: for y being Element of V st y = x holds

a * x = a * y

let y be Element of V; :: thesis: ( y = x implies a * x = a * y )

assume A35: y = x ; :: thesis: a * x = a * y

[a,x] in dom M by A7;

hence a * x = a * y by A35, FUNCT_1:47; :: thesis: verum

end;for y being Element of V st y = x holds

a * x = a * y

let x be Element of ModuleStr(# D,A,d,M #); :: thesis: for y being Element of V st y = x holds

a * x = a * y

let y be Element of V; :: thesis: ( y = x implies a * x = a * y )

assume A35: y = x ; :: thesis: a * x = a * y

[a,x] in dom M by A7;

hence a * x = a * y by A35, FUNCT_1:47; :: thesis: verum

thus (a * b) * v = (a * b) * x by A34

.= a * (b * x) by VECTSP_1:def 16

.= a * (b * v) by A34, A36 ; :: thesis: verum

proof

then reconsider W = ModuleStr(# D,A,d,M #) as non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF by A21, A23, A28, A33;
let v be Element of ModuleStr(# D,A,d,M #); :: according to VECTSP_1:def 16 :: thesis: (1. GF) * v = v

reconsider x = v as Element of V by TARSKI:def 3;

.= v by VECTSP_1:def 17 ;

:: thesis: verum

end;reconsider x = v as Element of V by TARSKI:def 3;

now :: thesis: for a being Element of GF

for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

hence (1. GF) * v =
(1_ GF) * x
for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

let a be Element of GF; :: thesis: for x being Element of ModuleStr(# D,A,d,M #)

for y being Element of V st y = x holds

a * x = a * y

let x be Element of ModuleStr(# D,A,d,M #); :: thesis: for y being Element of V st y = x holds

a * x = a * y

let y be Element of V; :: thesis: ( y = x implies a * x = a * y )

assume A37: y = x ; :: thesis: a * x = a * y

[a,x] in dom M by A7;

hence a * x = a * y by A37, FUNCT_1:47; :: thesis: verum

end;for y being Element of V st y = x holds

a * x = a * y

let x be Element of ModuleStr(# D,A,d,M #); :: thesis: for y being Element of V st y = x holds

a * x = a * y

let y be Element of V; :: thesis: ( y = x implies a * x = a * y )

assume A37: y = x ; :: thesis: a * x = a * y

[a,x] in dom M by A7;

hence a * x = a * y by A37, FUNCT_1:47; :: thesis: verum

.= v by VECTSP_1:def 17 ;

:: thesis: verum

0. W = 0. V ;

then reconsider W = W as strict Subspace of V by Def2;

take W ; :: thesis: V1 = the carrier of W

thus V1 = the carrier of W ; :: thesis: verum