:: VECTSP_5 semantic presentation

begin


definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let W1, W2 be Subspace of M;
funcW1 + W2 ->  strict Subspace of M means :Def1: :: VECTSP_5:def 1
 the carrier of it =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  ;
existence
 ex b1 being strict Subspace of M st the carrier of b1 =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }
proof
reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of M by VECTSP_4:def_2;
set VS =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  ;
  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  c= the carrier of M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  or x in the carrier of M )
assume  x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  ; ::_thesis: x in the carrier of M
then  ex v1, v2 being Element of M st
( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;
hence  x in the carrier of M ; ::_thesis: verum
end;
then reconsider VS =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  as Subset of M ;
A1: 0. M = (0. M) + (0. M) by RLVECT_1:4;
 ( 0. M in W1 & 0. M in W2 ) by VECTSP_4:17;
then A2: 0. M in VS by A1;
A3: VS =  {  (v + u) where v, u is Element of M : ( v in V1 & u in V2 )  }
proof
thus  VS c=  {  (v + u) where v, u is Element of M : ( v in V1 & u in V2 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (v + u) where v, u is Element of M : ( v in V1 & u in V2 )  }  c= VS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in VS or x in  {  (v + u) where v, u is Element of M : ( v in V1 & u in V2 )  }  )
assume  x in VS ; ::_thesis: x in  {  (v + u) where v, u is Element of M : ( v in V1 & u in V2 )  }
then consider v, u being Element of M such that
A4: x = v + u and
A5: ( v in W1 & u in W2 ) ;
 ( v in V1 & u in V2 ) by A5, STRUCT_0:def_5;
hence  x in  {  (v + u) where v, u is Element of M : ( v in V1 & u in V2 )  }  by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Element of M : ( v in V1 & u in V2 )  }  or x in VS )
assume  x in  {  (v + u) where v, u is Element of M : ( v in V1 & u in V2 )  }  ; ::_thesis: x in VS
then consider v, u being Element of M such that
A6: x = v + u and
A7: ( v in V1 & u in V2 ) ;
 ( v in W1 & u in W2 ) by A7, STRUCT_0:def_5;
hence  x in VS by A6; ::_thesis: verum
end;
 ( V1 is linearly-closed & V2 is linearly-closed ) by VECTSP_4:33;
hence  ex b1 being strict Subspace of M st the carrier of b1 =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  by A2, A3, VECTSP_4:6, VECTSP_4:34; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subspace of M st the carrier of b1 =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  & the carrier of b2 =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def1 defines + VECTSP_5:def_1_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for b5 being strict Subspace of M holds
( b5 = W1 + W2 iff the carrier of b5 =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  );

Lm1:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1
let W1, W2 be Subspace of M; ::_thesis: W1 + W2 = W2 + W1
set A =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  ;
set B =  {  (v + u) where v, u is Element of M : ( v in W2 & u in W1 )  }  ;
A1:  {  (v + u) where v, u is Element of M : ( v in W2 & u in W1 )  }  c=  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Element of M : ( v in W2 & u in W1 )  }  or x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  )
assume  x in  {  (v + u) where v, u is Element of M : ( v in W2 & u in W1 )  }  ; ::_thesis: x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }
then  ex v, u being Element of M st
( x = v + u & v in W2 & u in W1 ) ;
hence  x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  ; ::_thesis: verum
end;
A2: the carrier of (W1 + W2) =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  by Def1;
  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  c=  {  (v + u) where v, u is Element of M : ( v in W2 & u in W1 )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  or x in  {  (v + u) where v, u is Element of M : ( v in W2 & u in W1 )  }  )
assume  x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  ; ::_thesis: x in  {  (v + u) where v, u is Element of M : ( v in W2 & u in W1 )  }
then  ex v, u being Element of M st
( x = v + u & v in W1 & u in W2 ) ;
hence  x in  {  (v + u) where v, u is Element of M : ( v in W2 & u in W1 )  }  ; ::_thesis: verum
end;
then   {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  =  {  (v + u) where v, u is Element of M : ( v in W2 & u in W1 )  }  by A1, XBOOLE_0:def_10;
hence  W1 + W2 = W2 + W1 by A2, Def1; ::_thesis: verum
end;

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let W1, W2 be Subspace of M;
funcW1 /\ W2 ->  strict Subspace of M means :Def2: :: VECTSP_5:def 2
 the carrier of it = the carrier of W1 /\ the carrier of W2;
existence
 ex b1 being strict Subspace of M st the carrier of b1 = the carrier of W1 /\ the carrier of W2
proof
set VW2 = the carrier of W2;
set VW1 = the carrier of W1;
set VV = the carrier of M;
 0. M in W2 by VECTSP_4:17;
then A1: 0. M in the carrier of W2 by STRUCT_0:def_5;
 ( the carrier of W1 c= the carrier of M & the carrier of W2 c= the carrier of M ) by VECTSP_4:def_2;
then  the carrier of W1 /\ the carrier of W2 c= the carrier of M /\ the carrier of M by XBOOLE_1:27;
then reconsider V1 = the carrier of W1, V2 = the carrier of W2, V3 = the carrier of W1 /\ the carrier of W2 as Subset of M by VECTSP_4:def_2;
 ( V1 is linearly-closed & V2 is linearly-closed ) by VECTSP_4:33;
then A2: V3 is linearly-closed by VECTSP_4:7;
 0. M in W1 by VECTSP_4:17;
then  0. M in the carrier of W1 by STRUCT_0:def_5;
then  the carrier of W1 /\ the carrier of W2 <> {} by A1, XBOOLE_0:def_4;
hence  ex b1 being strict Subspace of M st the carrier of b1 = the carrier of W1 /\ the carrier of W2 by A2, VECTSP_4:34; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subspace of M st the carrier of b1 = the carrier of W1 /\ the carrier of W2 & the carrier of b2 = the carrier of W1 /\ the carrier of W2 holds
b1 = b2 by VECTSP_4:29;
commutativity
 for b1 being strict Subspace of M
for W1, W2 being Subspace of M st the carrier of b1 = the carrier of W1 /\ the carrier of W2 holds
the carrier of b1 = the carrier of W2 /\ the carrier of W1 ;
end;

:: deftheorem Def2 defines /\ VECTSP_5:def_2_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for b5 being strict Subspace of M holds
( b5 = W1 /\ W2 iff the carrier of b5 = the carrier of W1 /\ the carrier of W2 );

theorem Th1: :: VECTSP_5:1
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for x being set holds
( x in W1 + W2 iff ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for x being set holds
( x in W1 + W2 iff ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M
for x being set holds
( x in W1 + W2 iff ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
let W1, W2 be Subspace of M; ::_thesis: for x being set holds
( x in W1 + W2 iff ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
let x be set ; ::_thesis: ( x in W1 + W2 iff ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
thus  ( x in W1 + W2 implies ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) ) ::_thesis: ( ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) implies x in W1 + W2 )
proof
assume  x in W1 + W2 ; ::_thesis: ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 )
then  x in the carrier of (W1 + W2) by STRUCT_0:def_5;
then  x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  by Def1;
then consider v1, v2 being Element of M such that
A1: ( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;
take  v1 ; ::_thesis: ex v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 )
take  v2 ; ::_thesis: ( v1 in W1 & v2 in W2 & x = v1 + v2 )
thus  ( v1 in W1 & v2 in W2 & x = v1 + v2 ) by A1; ::_thesis: verum
end;
given v1, v2 being Element of M such that A2: ( v1 in W1 & v2 in W2 & x = v1 + v2 ) ; ::_thesis: x in W1 + W2
 x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  by A2;
then  x in the carrier of (W1 + W2) by Def1;
hence  x in W1 + W2 by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th2: :: VECTSP_5:2
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for v being Element of M st ( v in W1 or v in W2 ) holds
v in W1 + W2
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for v being Element of M st ( v in W1 or v in W2 ) holds
v in W1 + W2
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M
for v being Element of M st ( v in W1 or v in W2 ) holds
v in W1 + W2
let W1, W2 be Subspace of M; ::_thesis: for v being Element of M st ( v in W1 or v in W2 ) holds
v in W1 + W2
let v be Element of M; ::_thesis: ( ( v in W1 or v in W2 ) implies v in W1 + W2 )
assume A1: ( v in W1 or v in W2 ) ; ::_thesis: v in W1 + W2
now__::_thesis:_v_in_W1_+_W2
percases ( v in W1 or v in W2 ) by A1;
supposeA2: v in W1 ; ::_thesis: v in W1 + W2
 ( v = v + (0. M) & 0. M in W2 ) by RLVECT_1:4, VECTSP_4:17;
hence  v in W1 + W2 by A2, Th1; ::_thesis: verum
end;
supposeA3: v in W2 ; ::_thesis: v in W1 + W2
 ( v = (0. M) + v & 0. M in W1 ) by RLVECT_1:4, VECTSP_4:17;
hence  v in W1 + W2 by A3, Th1; ::_thesis: verum
end;
end;
end;
hence  v in W1 + W2 ; ::_thesis: verum
end;

theorem Th3: :: VECTSP_5:3
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M
for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
let W1, W2 be Subspace of M; ::_thesis: for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
let x be set ; ::_thesis: ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
 ( x in W1 /\ W2 iff x in the carrier of (W1 /\ W2) ) by STRUCT_0:def_5;
then  ( x in W1 /\ W2 iff x in the carrier of W1 /\ the carrier of W2 ) by Def2;
then  ( x in W1 /\ W2 iff ( x in the carrier of W1 & x in the carrier of W2 ) ) by XBOOLE_0:def_4;
hence  ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) ) by STRUCT_0:def_5; ::_thesis: verum
end;

Lm2:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of W1 c= the carrier of (W1 + W2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of W1 c= the carrier of (W1 + W2)
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds the carrier of W1 c= the carrier of (W1 + W2)
let W1, W2 be Subspace of M; ::_thesis: the carrier of W1 c= the carrier of (W1 + W2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of (W1 + W2) )
set A =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  ;
assume  x in the carrier of W1 ; ::_thesis: x in the carrier of (W1 + W2)
then reconsider v = x as Element of W1 ;
reconsider v = v as Element of M by VECTSP_4:10;
A1: v = v + (0. M) by RLVECT_1:4;
 ( v in W1 & 0. M in W2 ) by STRUCT_0:def_5, VECTSP_4:17;
then  x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  by A1;
hence  x in the carrier of (W1 + W2) by Def1; ::_thesis: verum
end;

Lm3:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1 being Subspace of M
for W2 being strict Subspace of M st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1 being Subspace of M
for W2 being strict Subspace of M st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1 being Subspace of M
for W2 being strict Subspace of M st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let W1 be Subspace of M; ::_thesis: for W2 being strict Subspace of M st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let W2 be strict Subspace of M; ::_thesis: ( the carrier of W1 c= the carrier of W2 implies W1 + W2 = W2 )
assume A1: the carrier of W1 c= the carrier of W2 ; ::_thesis: W1 + W2 = W2
A2: the carrier of (W1 + W2) c= the carrier of W2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W1 + W2) or x in the carrier of W2 )
assume  x in the carrier of (W1 + W2) ; ::_thesis: x in the carrier of W2
then  x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  by Def1;
then consider v, u being Element of M such that
A3: x = v + u and
A4: v in W1 and
A5: u in W2 ;
 W1 is Subspace of W2 by A1, VECTSP_4:27;
then  v in W2 by A4, VECTSP_4:8;
then  v + u in W2 by A5, VECTSP_4:20;
hence  x in the carrier of W2 by A3, STRUCT_0:def_5; ::_thesis: verum
end;
 W1 + W2 = W2 + W1 by Lm1;
then  the carrier of W2 c= the carrier of (W1 + W2) by Lm2;
then  the carrier of (W1 + W2) = the carrier of W2 by A2, XBOOLE_0:def_10;
hence  W1 + W2 = W2 by VECTSP_4:29; ::_thesis: verum
end;

theorem :: VECTSP_5:4
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds W + W = W by Lm3;

theorem :: VECTSP_5:5
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1 by Lm1;

theorem Th6: :: VECTSP_5:6
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds W1 + (W2 + W3) = (W1 + W2) + W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds W1 + (W2 + W3) = (W1 + W2) + W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M holds W1 + (W2 + W3) = (W1 + W2) + W3
let W1, W2, W3 be Subspace of M; ::_thesis: W1 + (W2 + W3) = (W1 + W2) + W3
set A =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  ;
set B =  {  (v + u) where v, u is Element of M : ( v in W2 & u in W3 )  }  ;
set C =  {  (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 )  }  ;
set D =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 )  }  ;
A1: the carrier of (W1 + (W2 + W3)) =  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 )  }  by Def1;
A2:  {  (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 )  }  c=  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 )  }  or x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 )  }  )
assume  x in  {  (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 )  }  ; ::_thesis: x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 )  }
then consider v, u being Element of M such that
A3: x = v + u and
A4: v in W1 + W2 and
A5: u in W3 ;
 v in the carrier of (W1 + W2) by A4, STRUCT_0:def_5;
then  v in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  by Def1;
then consider u1, u2 being Element of M such that
A6: v = u1 + u2 and
A7: u1 in W1 and
A8: u2 in W2 ;
 u2 + u in  {  (v + u) where v, u is Element of M : ( v in W2 & u in W3 )  }  by A5, A8;
then  u2 + u in the carrier of (W2 + W3) by Def1;
then A9: u2 + u in W2 + W3 by STRUCT_0:def_5;
 v + u = u1 + (u2 + u) by A6, RLVECT_1:def_3;
hence  x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 )  }  by A3, A7, A9; ::_thesis: verum
end;
  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 )  }  c=  {  (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 )  }  or x in  {  (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 )  }  )
assume  x in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 )  }  ; ::_thesis: x in  {  (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 )  }
then consider v, u being Element of M such that
A10: x = v + u and
A11: v in W1 and
A12: u in W2 + W3 ;
 u in the carrier of (W2 + W3) by A12, STRUCT_0:def_5;
then  u in  {  (v + u) where v, u is Element of M : ( v in W2 & u in W3 )  }  by Def1;
then consider u1, u2 being Element of M such that
A13: u = u1 + u2 and
A14: u1 in W2 and
A15: u2 in W3 ;
 v + u1 in  {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 )  }  by A11, A14;
then  v + u1 in the carrier of (W1 + W2) by Def1;
then A16: v + u1 in W1 + W2 by STRUCT_0:def_5;
 v + u = (v + u1) + u2 by A13, RLVECT_1:def_3;
hence  x in  {  (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 )  }  by A10, A15, A16; ::_thesis: verum
end;
then   {  (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 )  }  =  {  (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 )  }  by A2, XBOOLE_0:def_10;
hence  W1 + (W2 + W3) = (W1 + W2) + W3 by A1, Def1; ::_thesis: verum
end;

theorem Th7: :: VECTSP_5:7
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
let W1, W2 be Subspace of M; ::_thesis: ( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
 the carrier of W1 c= the carrier of (W1 + W2) by Lm2;
hence  W1 is Subspace of W1 + W2 by VECTSP_4:27; ::_thesis: W2 is Subspace of W1 + W2
 the carrier of W2 c= the carrier of (W2 + W1) by Lm2;
then  the carrier of W2 c= the carrier of (W1 + W2) by Lm1;
hence  W2 is Subspace of W1 + W2 by VECTSP_4:27; ::_thesis: verum
end;

theorem Th8: :: VECTSP_5:8
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1 being Subspace of M
for W2 being strict Subspace of M holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1 being Subspace of M
for W2 being strict Subspace of M holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1 being Subspace of M
for W2 being strict Subspace of M holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )
let W1 be Subspace of M; ::_thesis: for W2 being strict Subspace of M holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )
let W2 be strict Subspace of M; ::_thesis: ( W1 is Subspace of W2 iff W1 + W2 = W2 )
thus  ( W1 is Subspace of W2 implies W1 + W2 = W2 ) ::_thesis: ( W1 + W2 = W2 implies W1 is Subspace of W2 )
proof
assume  W1 is Subspace of W2 ; ::_thesis: W1 + W2 = W2
then  the carrier of W1 c= the carrier of W2 by VECTSP_4:def_2;
hence  W1 + W2 = W2 by Lm3; ::_thesis: verum
end;
thus  ( W1 + W2 = W2 implies W1 is Subspace of W2 ) by Th7; ::_thesis: verum
end;

theorem Th9: :: VECTSP_5:9
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds
( ((0). M) + W = W & W + ((0). M) = W )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds
( ((0). M) + W = W & W + ((0). M) = W )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being strict Subspace of M holds
( ((0). M) + W = W & W + ((0). M) = W )
let W be strict Subspace of M; ::_thesis: ( ((0). M) + W = W & W + ((0). M) = W )
 (0). M is Subspace of W by VECTSP_4:39;
then  the carrier of ((0). M) c= the carrier of W by VECTSP_4:def_2;
hence  ((0). M) + W = W by Lm3; ::_thesis: W + ((0). M) = W
hence  W + ((0). M) = W by Lm1; ::_thesis: verum
end;

Lm4:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of M ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
let W be Subspace of M; ::_thesis: ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
take W9 = W + W; ::_thesis: the carrier of W = the carrier of W9
thus  the carrier of W c= the carrier of W9 by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W9 c= the carrier of W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W9 or x in the carrier of W )
assume  x in the carrier of W9 ; ::_thesis: x in the carrier of W
then  x in  {  (v + u) where v, u is Element of M : ( v in W & u in W )  }  by Def1;
then  ex v1, v2 being Element of M st
( x = v1 + v2 & v1 in W & v2 in W ) ;
then  x in W by VECTSP_4:20;
hence  x in the carrier of W by STRUCT_0:def_5; ::_thesis: verum
end;

Lm5:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
let W, W9, W1 be Subspace of M; ::_thesis: ( the carrier of W = the carrier of W9 implies ( W1 + W = W1 + W9 & W + W1 = W9 + W1 ) )
assume A1: the carrier of W = the carrier of W9 ; ::_thesis: ( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
A2: now__::_thesis:_for_v_being_Element_of_M_holds_
(_(_v_in_W1_+_W_implies_v_in_W1_+_W9_)_&_(_v_in_W1_+_W9_implies_v_in_W1_+_W_)_)
let v be Element of M; ::_thesis: ( ( v in W1 + W implies v in W1 + W9 ) & ( v in W1 + W9 implies v in W1 + W ) )
set W1W9 =  {  (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W9 )  }  ;
set W1W =  {  (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W )  }  ;
thus  ( v in W1 + W implies v in W1 + W9 ) ::_thesis: ( v in W1 + W9 implies v in W1 + W )
proof
assume  v in W1 + W ; ::_thesis: v in W1 + W9
then  v in the carrier of (W1 + W) by STRUCT_0:def_5;
then  v in  {  (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W )  }  by Def1;
then consider v1, v2 being Element of M such that
A3: ( v = v1 + v2 & v1 in W1 ) and
A4: v2 in W ;
 v2 in the carrier of W9 by A1, A4, STRUCT_0:def_5;
then  v2 in W9 by STRUCT_0:def_5;
then  v in  {  (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W9 )  }  by A3;
then  v in the carrier of (W1 + W9) by Def1;
hence  v in W1 + W9 by STRUCT_0:def_5; ::_thesis: verum
end;
assume  v in W1 + W9 ; ::_thesis: v in W1 + W
then  v in the carrier of (W1 + W9) by STRUCT_0:def_5;
then  v in  {  (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W9 )  }  by Def1;
then consider v1, v2 being Element of M such that
A5: ( v = v1 + v2 & v1 in W1 ) and
A6: v2 in W9 ;
 v2 in the carrier of W by A1, A6, STRUCT_0:def_5;
then  v2 in W by STRUCT_0:def_5;
then  v in  {  (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W )  }  by A5;
then  v in the carrier of (W1 + W) by Def1;
hence  v in W1 + W by STRUCT_0:def_5; ::_thesis: verum
end;
hence  W1 + W = W1 + W9 by VECTSP_4:30; ::_thesis: W + W1 = W9 + W1
 ( W1 + W = W + W1 & W1 + W9 = W9 + W1 ) by Lm1;
hence  W + W1 = W9 + W1 by A2, VECTSP_4:30; ::_thesis: verum
end;

Lm6:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds W is Subspace of (Omega). M
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds W is Subspace of (Omega). M
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of M holds W is Subspace of (Omega). M
let W be Subspace of M; ::_thesis: W is Subspace of (Omega). M
thus  the carrier of W c= the carrier of ((Omega). M) by VECTSP_4:def_2; :: according to VECTSP_4:def_2 ::_thesis: ( 0. W = 0. ((Omega). M) & the addF of W = K114( the addF of ((Omega). M), the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [: the carrier of GF, the carrier of W:] )
thus  0. W = 0. M by VECTSP_4:def_2
.= 0. ((Omega). M) by VECTSP_4:def_2 ; ::_thesis: ( the addF of W = K114( the addF of ((Omega). M), the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [: the carrier of GF, the carrier of W:] )
thus  ( the addF of W = K114( the addF of ((Omega). M), the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [: the carrier of GF, the carrier of W:] ) by VECTSP_4:def_2; ::_thesis: verum
end;

theorem :: VECTSP_5:10
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds
( ((0). M) + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & ((Omega). M) + ((0). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) ) by Th9;

theorem Th11: :: VECTSP_5:11
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds
( ((Omega). M) + W = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds
( ((Omega). M) + W = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of M holds
( ((Omega). M) + W = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )
let W be Subspace of M; ::_thesis: ( ((Omega). M) + W = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )
consider W9 being strict Subspace of M such that
A1: the carrier of W9 = the carrier of ((Omega). M) ;
A2: the carrier of W c= the carrier of W9 by A1, VECTSP_4:def_2;
A3: W9 is Subspace of (Omega). M by Lm6;
W + ((Omega). M) = W + W9 by A1, Lm5
.= W9 by A2, Lm3
.= VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) by A1, A3, VECTSP_4:31 ;
hence  ( ((Omega). M) + W = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) ) by Lm1; ::_thesis: verum
end;

theorem :: VECTSP_5:12
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds ((Omega). M) + ((Omega). M) = M by Th11;

theorem :: VECTSP_5:13
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds W /\ W = W
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds W /\ W = W
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being strict Subspace of M holds W /\ W = W
let W be strict Subspace of M; ::_thesis: W /\ W = W
 the carrier of W = the carrier of W /\ the carrier of W ;
hence  W /\ W = W by Def2; ::_thesis: verum
end;

theorem Th14: :: VECTSP_5:14
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
let W1, W2, W3 be Subspace of M; ::_thesis: W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
set V1 = the carrier of W1;
set V2 = the carrier of W2;
set V3 = the carrier of W3;
the carrier of (W1 /\ (W2 /\ W3)) = the carrier of W1 /\ the carrier of (W2 /\ W3) by Def2
.= the carrier of W1 /\ ( the carrier of W2 /\ the carrier of W3) by Def2
.= ( the carrier of W1 /\ the carrier of W2) /\ the carrier of W3 by XBOOLE_1:16
.= the carrier of (W1 /\ W2) /\ the carrier of W3 by Def2 ;
hence  W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3 by Def2; ::_thesis: verum
end;

Lm7:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of W1
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of W1
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of W1
let W1, W2 be Subspace of M; ::_thesis: the carrier of (W1 /\ W2) c= the carrier of W1
 the carrier of (W1 /\ W2) = the carrier of W1 /\ the carrier of W2 by Def2;
hence  the carrier of (W1 /\ W2) c= the carrier of W1 by XBOOLE_1:17; ::_thesis: verum
end;

theorem Th15: :: VECTSP_5:15
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
let W1, W2 be Subspace of M; ::_thesis: ( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
 the carrier of (W1 /\ W2) c= the carrier of W1 by Lm7;
hence  W1 /\ W2 is Subspace of W1 by VECTSP_4:27; ::_thesis: W1 /\ W2 is Subspace of W2
 the carrier of (W2 /\ W1) c= the carrier of W2 by Lm7;
hence  W1 /\ W2 is Subspace of W2 by VECTSP_4:27; ::_thesis: verum
end;

Lm8:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds
( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 )
let W, W9, W1 be Subspace of M; ::_thesis: ( the carrier of W = the carrier of W9 implies ( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 ) )
assume  the carrier of W = the carrier of W9 ; ::_thesis: ( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 )
then A1: the carrier of (W1 /\ W) = the carrier of W1 /\ the carrier of W9 by Def2
.= the carrier of (W1 /\ W9) by Def2 ;
hence  W1 /\ W = W1 /\ W9 by VECTSP_4:29; ::_thesis: W /\ W1 = W9 /\ W1
thus  W /\ W1 = W9 /\ W1 by A1, VECTSP_4:29; ::_thesis: verum
end;

theorem Th16: :: VECTSP_5:16
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W2 being Subspace of M holds
( ( for W1 being strict Subspace of M st W1 is Subspace of W2 holds
W1 /\ W2 = W1 ) & ( for W1 being Subspace of M st W1 /\ W2 = W1 holds
W1 is Subspace of W2 ) )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W2 being Subspace of M holds
( ( for W1 being strict Subspace of M st W1 is Subspace of W2 holds
W1 /\ W2 = W1 ) & ( for W1 being Subspace of M st W1 /\ W2 = W1 holds
W1 is Subspace of W2 ) )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W2 being Subspace of M holds
( ( for W1 being strict Subspace of M st W1 is Subspace of W2 holds
W1 /\ W2 = W1 ) & ( for W1 being Subspace of M st W1 /\ W2 = W1 holds
W1 is Subspace of W2 ) )
let W2 be Subspace of M; ::_thesis: ( ( for W1 being strict Subspace of M st W1 is Subspace of W2 holds
W1 /\ W2 = W1 ) & ( for W1 being Subspace of M st W1 /\ W2 = W1 holds
W1 is Subspace of W2 ) )
thus  for W1 being strict Subspace of M st W1 is Subspace of W2 holds
W1 /\ W2 = W1 ::_thesis: for W1 being Subspace of M st W1 /\ W2 = W1 holds
W1 is Subspace of W2
proof
let W1 be strict Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies W1 /\ W2 = W1 )
assume  W1 is Subspace of W2 ; ::_thesis: W1 /\ W2 = W1
then A1: the carrier of W1 c= the carrier of W2 by VECTSP_4:def_2;
 the carrier of (W1 /\ W2) = the carrier of W1 /\ the carrier of W2 by Def2;
hence  W1 /\ W2 = W1 by A1, VECTSP_4:29, XBOOLE_1:28; ::_thesis: verum
end;
thus  for W1 being Subspace of M st W1 /\ W2 = W1 holds
W1 is Subspace of W2 by Th15; ::_thesis: verum
end;

theorem :: VECTSP_5:17
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 /\ W3 is Subspace of W2 /\ W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 /\ W3 is Subspace of W2 /\ W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 /\ W3 is Subspace of W2 /\ W3
let W1, W2, W3 be Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3 )
set A1 = the carrier of W1;
set A2 = the carrier of W2;
set A3 = the carrier of W3;
set A4 = the carrier of (W1 /\ W3);
assume  W1 is Subspace of W2 ; ::_thesis: W1 /\ W3 is Subspace of W2 /\ W3
then  the carrier of W1 c= the carrier of W2 by VECTSP_4:def_2;
then  the carrier of W1 /\ the carrier of W3 c= the carrier of W2 /\ the carrier of W3 by XBOOLE_1:26;
then  the carrier of (W1 /\ W3) c= the carrier of W2 /\ the carrier of W3 by Def2;
then  the carrier of (W1 /\ W3) c= the carrier of (W2 /\ W3) by Def2;
hence  W1 /\ W3 is Subspace of W2 /\ W3 by VECTSP_4:27; ::_thesis: verum
end;

theorem :: VECTSP_5:18
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
let W1, W3, W2 be Subspace of M; ::_thesis: ( W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3 )
assume A1: W1 is Subspace of W3 ; ::_thesis: W1 /\ W2 is Subspace of W3
 W1 /\ W2 is Subspace of W1 by Th15;
hence  W1 /\ W2 is Subspace of W3 by A1, VECTSP_4:26; ::_thesis: verum
end;

theorem :: VECTSP_5:19
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 & W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 & W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 & W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3
let W1, W2, W3 be Subspace of M; ::_thesis: ( W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of W2 /\ W3 )
assume A1: ( W1 is Subspace of W2 & W1 is Subspace of W3 ) ; ::_thesis: W1 is Subspace of W2 /\ W3
now__::_thesis:_for_v_being_Element_of_M_st_v_in_W1_holds_
v_in_W2_/\_W3
let v be Element of M; ::_thesis: ( v in W1 implies v in W2 /\ W3 )
assume  v in W1 ; ::_thesis: v in W2 /\ W3
then  ( v in W2 & v in W3 ) by A1, VECTSP_4:8;
hence  v in W2 /\ W3 by Th3; ::_thesis: verum
end;
hence  W1 is Subspace of W2 /\ W3 by VECTSP_4:28; ::_thesis: verum
end;

theorem Th20: :: VECTSP_5:20
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds
( ((0). M) /\ W = (0). M & W /\ ((0). M) = (0). M )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds
( ((0). M) /\ W = (0). M & W /\ ((0). M) = (0). M )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of M holds
( ((0). M) /\ W = (0). M & W /\ ((0). M) = (0). M )
let W be Subspace of M; ::_thesis: ( ((0). M) /\ W = (0). M & W /\ ((0). M) = (0). M )
 0. M in W by VECTSP_4:17;
then  0. M in the carrier of W by STRUCT_0:def_5;
then  {(0. M)} c= the carrier of W by ZFMISC_1:31;
then A1: {(0. M)} /\ the carrier of W = {(0. M)} by XBOOLE_1:28;
A2: the carrier of (((0). M) /\ W) = the carrier of ((0). M) /\ the carrier of W by Def2
.= {(0. M)} /\ the carrier of W by VECTSP_4:def_3 ;
hence  ((0). M) /\ W = (0). M by A1, VECTSP_4:def_3; ::_thesis: W /\ ((0). M) = (0). M
thus  W /\ ((0). M) = (0). M by A2, A1, VECTSP_4:def_3; ::_thesis: verum
end;

theorem Th21: :: VECTSP_5:21
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds
( ((Omega). M) /\ W = W & W /\ ((Omega). M) = W )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds
( ((Omega). M) /\ W = W & W /\ ((Omega). M) = W )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being strict Subspace of M holds
( ((Omega). M) /\ W = W & W /\ ((Omega). M) = W )
let W be strict Subspace of M; ::_thesis: ( ((Omega). M) /\ W = W & W /\ ((Omega). M) = W )
A1: ( the carrier of (((Omega). M) /\ W) = the carrier of VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) /\ the carrier of W & the carrier of W c= the carrier of M ) by Def2, VECTSP_4:def_2;
hence  ((Omega). M) /\ W = W by VECTSP_4:29, XBOOLE_1:28; ::_thesis: W /\ ((Omega). M) = W
thus  W /\ ((Omega). M) = W by A1, VECTSP_4:29, XBOOLE_1:28; ::_thesis: verum
end;

theorem :: VECTSP_5:22
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds ((Omega). M) /\ ((Omega). M) = M by Th21;

Lm9:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
let W1, W2 be Subspace of M; ::_thesis: the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
 ( the carrier of (W1 /\ W2) c= the carrier of W1 & the carrier of W1 c= the carrier of (W1 + W2) ) by Lm2, Lm7;
hence  the carrier of (W1 /\ W2) c= the carrier of (W1 + W2) by XBOOLE_1:1; ::_thesis: verum
end;

theorem :: VECTSP_5:23
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds W1 /\ W2 is Subspace of W1 + W2 by Lm9, VECTSP_4:27;

Lm10:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
let W1, W2 be Subspace of M; ::_thesis: the carrier of ((W1 /\ W2) + W2) = the carrier of W2
thus  the carrier of ((W1 /\ W2) + W2) c= the carrier of W2 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W2 c= the carrier of ((W1 /\ W2) + W2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 /\ W2) + W2) or x in the carrier of W2 )
assume  x in the carrier of ((W1 /\ W2) + W2) ; ::_thesis: x in the carrier of W2
then  x in  {  (u + v) where u, v is Element of M : ( u in W1 /\ W2 & v in W2 )  }  by Def1;
then consider u, v being Element of M such that
A1: x = u + v and
A2: u in W1 /\ W2 and
A3: v in W2 ;
 u in W2 by A2, Th3;
then  u + v in W2 by A3, VECTSP_4:20;
hence  x in the carrier of W2 by A1, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W2 or x in the carrier of ((W1 /\ W2) + W2) )
 the carrier of W2 c= the carrier of (W2 + (W1 /\ W2)) by Lm2;
then A4: the carrier of W2 c= the carrier of ((W1 /\ W2) + W2) by Lm1;
assume  x in the carrier of W2 ; ::_thesis: x in the carrier of ((W1 /\ W2) + W2)
hence  x in the carrier of ((W1 /\ W2) + W2) by A4; ::_thesis: verum
end;

theorem :: VECTSP_5:24
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1 being Subspace of M
for W2 being strict Subspace of M holds (W1 /\ W2) + W2 = W2 by Lm10, VECTSP_4:29;

Lm11:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let W1, W2 be Subspace of M; ::_thesis: the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
thus  the carrier of (W1 /\ (W1 + W2)) c= the carrier of W1 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W1 c= the carrier of (W1 /\ (W1 + W2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W1 /\ (W1 + W2)) or x in the carrier of W1 )
assume A1: x in the carrier of (W1 /\ (W1 + W2)) ; ::_thesis: x in the carrier of W1
 the carrier of (W1 /\ (W1 + W2)) = the carrier of W1 /\ the carrier of (W1 + W2) by Def2;
hence  x in the carrier of W1 by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of (W1 /\ (W1 + W2)) )
assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of (W1 /\ (W1 + W2))
 the carrier of W1 c= the carrier of M by VECTSP_4:def_2;
then reconsider x1 = x as Element of M by A2;
A3: ( x1 + (0. M) = x1 & 0. M in W2 ) by RLVECT_1:4, VECTSP_4:17;
 x in W1 by A2, STRUCT_0:def_5;
then  x in  {  (u + v) where u, v is Element of M : ( u in W1 & v in W2 )  }  by A3;
then  x in the carrier of (W1 + W2) by Def1;
then  x in the carrier of W1 /\ the carrier of (W1 + W2) by A2, XBOOLE_0:def_4;
hence  x in the carrier of (W1 /\ (W1 + W2)) by Def2; ::_thesis: verum
end;

theorem :: VECTSP_5:25
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W2 being Subspace of M
for W1 being strict Subspace of M holds W1 /\ (W1 + W2) = W1 by Lm11, VECTSP_4:29;

Lm12:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
let W1, W2, W3 be Subspace of M; ::_thesis: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) or x in the carrier of (W2 /\ (W1 + W3)) )
assume  x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) ; ::_thesis: x in the carrier of (W2 /\ (W1 + W3))
then  x in  {  (u + v) where u, v is Element of M : ( u in W1 /\ W2 & v in W2 /\ W3 )  }  by Def1;
then consider u, v being Element of M such that
A1: x = u + v and
A2: ( u in W1 /\ W2 & v in W2 /\ W3 ) ;
 ( u in W2 & v in W2 ) by A2, Th3;
then A3: x in W2 by A1, VECTSP_4:20;
 ( u in W1 & v in W3 ) by A2, Th3;
then  x in W1 + W3 by A1, Th1;
then  x in W2 /\ (W1 + W3) by A3, Th3;
hence  x in the carrier of (W2 /\ (W1 + W3)) by STRUCT_0:def_5; ::_thesis: verum
end;

theorem :: VECTSP_5:26
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3) by Lm12, VECTSP_4:27;

Lm13:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
let W1, W2, W3 be Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3)) )
assume A1: W1 is Subspace of W2 ; ::_thesis: the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
thus  the carrier of (W2 /\ (W1 + W3)) c= the carrier of ((W1 /\ W2) + (W2 /\ W3)) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W2 /\ (W1 + W3)) or x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) )
assume  x in the carrier of (W2 /\ (W1 + W3)) ; ::_thesis: x in the carrier of ((W1 /\ W2) + (W2 /\ W3))
then A2: x in the carrier of W2 /\ the carrier of (W1 + W3) by Def2;
then  x in the carrier of (W1 + W3) by XBOOLE_0:def_4;
then  x in  {  (u + v) where u, v is Element of M : ( u in W1 & v in W3 )  }  by Def1;
then consider u1, v1 being Element of M such that
A3: x = u1 + v1 and
A4: u1 in W1 and
A5: v1 in W3 ;
A6: u1 in W2 by A1, A4, VECTSP_4:8;
 x in the carrier of W2 by A2, XBOOLE_0:def_4;
then  u1 + v1 in W2 by A3, STRUCT_0:def_5;
then  (v1 + u1) - u1 in W2 by A6, VECTSP_4:23;
then  v1 + (u1 - u1) in W2 by RLVECT_1:def_3;
then  v1 + (0. M) in W2 by VECTSP_1:19;
then  v1 in W2 by RLVECT_1:4;
then A7: v1 in W2 /\ W3 by A5, Th3;
 u1 in W1 /\ W2 by A4, A6, Th3;
then  x in (W1 /\ W2) + (W2 /\ W3) by A3, A7, Th1;
hence  x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) by STRUCT_0:def_5; ::_thesis: verum
end;
thus  the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3)) by Lm12; ::_thesis: verum
end;

theorem :: VECTSP_5:27
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) by Lm13, VECTSP_4:29;

Lm14:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W2, W1, W3 being Subspace of M holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W2, W1, W3 being Subspace of M holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W2, W1, W3 being Subspace of M holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
let W2, W1, W3 be Subspace of M; ::_thesis: the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W2 + (W1 /\ W3)) or x in the carrier of ((W1 + W2) /\ (W2 + W3)) )
assume  x in the carrier of (W2 + (W1 /\ W3)) ; ::_thesis: x in the carrier of ((W1 + W2) /\ (W2 + W3))
then  x in  {  (u + v) where u, v is Element of M : ( u in W2 & v in W1 /\ W3 )  }  by Def1;
then consider u, v being Element of M such that
A1: ( x = u + v & u in W2 ) and
A2: v in W1 /\ W3 ;
 v in W3 by A2, Th3;
then  x in  {  (u1 + u2) where u1, u2 is Element of M : ( u1 in W2 & u2 in W3 )  }  by A1;
then A3: x in the carrier of (W2 + W3) by Def1;
 v in W1 by A2, Th3;
then  x in  {  (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W2 )  }  by A1;
then  x in the carrier of (W1 + W2) by Def1;
then  x in the carrier of (W1 + W2) /\ the carrier of (W2 + W3) by A3, XBOOLE_0:def_4;
hence  x in the carrier of ((W1 + W2) /\ (W2 + W3)) by Def2; ::_thesis: verum
end;

theorem :: VECTSP_5:28
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W2, W1, W3 being Subspace of M holds W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3) by Lm14, VECTSP_4:27;

Lm15:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
let W1, W2, W3 be Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3)) )
reconsider V2 = the carrier of W2 as Subset of M by VECTSP_4:def_2;
A1: V2 is linearly-closed by VECTSP_4:33;
assume  W1 is Subspace of W2 ; ::_thesis: the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
then A2: the carrier of W1 c= the carrier of W2 by VECTSP_4:def_2;
thus  the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3)) by Lm14; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of ((W1 + W2) /\ (W2 + W3)) c= the carrier of (W2 + (W1 /\ W3))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 + W2) /\ (W2 + W3)) or x in the carrier of (W2 + (W1 /\ W3)) )
assume  x in the carrier of ((W1 + W2) /\ (W2 + W3)) ; ::_thesis: x in the carrier of (W2 + (W1 /\ W3))
then  x in the carrier of (W1 + W2) /\ the carrier of (W2 + W3) by Def2;
then  x in the carrier of (W1 + W2) by XBOOLE_0:def_4;
then  x in  {  (u1 + u2) where u1, u2 is Element of M : ( u1 in W1 & u2 in W2 )  }  by Def1;
then consider u1, u2 being Element of M such that
A3: x = u1 + u2 and
A4: ( u1 in W1 & u2 in W2 ) ;
 ( u1 in the carrier of W1 & u2 in the carrier of W2 ) by A4, STRUCT_0:def_5;
then  u1 + u2 in V2 by A2, A1, VECTSP_4:def_1;
then A5: u1 + u2 in W2 by STRUCT_0:def_5;
 ( 0. M in W1 /\ W3 & (u1 + u2) + (0. M) = u1 + u2 ) by RLVECT_1:4, VECTSP_4:17;
then  x in  {  (u + v) where u, v is Element of M : ( u in W2 & v in W1 /\ W3 )  }  by A3, A5;
hence  x in the carrier of (W2 + (W1 /\ W3)) by Def1; ::_thesis: verum
end;

theorem :: VECTSP_5:29
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) by Lm15, VECTSP_4:29;

theorem Th30: :: VECTSP_5:30
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W3, W2 being Subspace of M
for W1 being strict Subspace of M st W1 is Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W3, W2 being Subspace of M
for W1 being strict Subspace of M st W1 is Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W3, W2 being Subspace of M
for W1 being strict Subspace of M st W1 is Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
let W3, W2 be Subspace of M; ::_thesis: for W1 being strict Subspace of M st W1 is Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
let W1 be strict Subspace of M; ::_thesis: ( W1 is Subspace of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3 )
assume A1: W1 is Subspace of W3 ; ::_thesis: W1 + (W2 /\ W3) = (W1 + W2) /\ W3
hence (W1 + W2) /\ W3 = (W1 /\ W3) + (W3 /\ W2) by Lm13, VECTSP_4:29
.= W1 + (W2 /\ W3) by A1, Th16 ;
::_thesis: verum
end;

theorem :: VECTSP_5:31
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being strict Subspace of M holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being strict Subspace of M holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being strict Subspace of M holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
let W1, W2 be strict Subspace of M; ::_thesis: ( W1 + W2 = W2 iff W1 /\ W2 = W1 )
 ( W1 + W2 = W2 iff W1 is Subspace of W2 ) by Th8;
hence  ( W1 + W2 = W2 iff W1 /\ W2 = W1 ) by Th16; ::_thesis: verum
end;

theorem :: VECTSP_5:32
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1 being Subspace of M
for W2, W3 being strict Subspace of M st W1 is Subspace of W2 holds
W1 + W3 is Subspace of W2 + W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1 being Subspace of M
for W2, W3 being strict Subspace of M st W1 is Subspace of W2 holds
W1 + W3 is Subspace of W2 + W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1 being Subspace of M
for W2, W3 being strict Subspace of M st W1 is Subspace of W2 holds
W1 + W3 is Subspace of W2 + W3
let W1 be Subspace of M; ::_thesis: for W2, W3 being strict Subspace of M st W1 is Subspace of W2 holds
W1 + W3 is Subspace of W2 + W3
let W2, W3 be strict Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies W1 + W3 is Subspace of W2 + W3 )
assume A1: W1 is Subspace of W2 ; ::_thesis: W1 + W3 is Subspace of W2 + W3
(W1 + W3) + (W2 + W3) = (W1 + W3) + (W3 + W2) by Lm1
.= ((W1 + W3) + W3) + W2 by Th6
.= (W1 + (W3 + W3)) + W2 by Th6
.= (W1 + W3) + W2 by Lm3
.= W1 + (W3 + W2) by Th6
.= W1 + (W2 + W3) by Lm1
.= (W1 + W2) + W3 by Th6
.= W2 + W3 by A1, Th8 ;
hence  W1 + W3 is Subspace of W2 + W3 by Th8; ::_thesis: verum
end;

theorem :: VECTSP_5:33
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
let W1, W2, W3 be Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies W1 is Subspace of W2 + W3 )
assume A1: W1 is Subspace of W2 ; ::_thesis: W1 is Subspace of W2 + W3
 W2 is Subspace of W2 + W3 by Th7;
hence  W1 is Subspace of W2 + W3 by A1, VECTSP_4:26; ::_thesis: verum
end;

theorem :: VECTSP_5:34
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
let W1, W3, W2 be Subspace of M; ::_thesis: ( W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace of W3 )
assume A1: ( W1 is Subspace of W3 & W2 is Subspace of W3 ) ; ::_thesis: W1 + W2 is Subspace of W3
now__::_thesis:_for_v_being_Element_of_M_st_v_in_W1_+_W2_holds_
v_in_W3
let v be Element of M; ::_thesis: ( v in W1 + W2 implies v in W3 )
assume  v in W1 + W2 ; ::_thesis: v in W3
then consider v1, v2 being Element of M such that
A2: ( v1 in W1 & v2 in W2 ) and
A3: v = v1 + v2 by Th1;
 ( v1 in W3 & v2 in W3 ) by A1, A2, VECTSP_4:8;
hence  v in W3 by A3, VECTSP_4:20; ::_thesis: verum
end;
hence  W1 + W2 is Subspace of W3 by VECTSP_4:28; ::_thesis: verum
end;

theorem :: VECTSP_5:35
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds
( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
let W1, W2 be Subspace of M; ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
thus  ( for W being Subspace of M holds not the carrier of W = the carrier of W1 \/ the carrier of W2 or W1 is Subspace of W2 or W2 is Subspace of W1 ) ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
proof
given W being Subspace of M such that A1: the carrier of W = the carrier of W1 \/ the carrier of W2 ; ::_thesis: ( W1 is Subspace of W2 or W2 is Subspace of W1 )
set VW = the carrier of W;
assume that
A2: W1 is not Subspace of W2 and
A3: W2 is not Subspace of W1 ; ::_thesis: contradiction
 not the carrier of W2 c= the carrier of W1 by A3, VECTSP_4:27;
then consider y being set  such that
A4: y in the carrier of W2 and
A5: not y in the carrier of W1 by TARSKI:def_3;
reconsider y = y as Element of the carrier of W2 by A4;
reconsider y = y as Element of M by VECTSP_4:10;
reconsider A1 = the carrier of W as Subset of M by VECTSP_4:def_2;
A6: A1 is linearly-closed by VECTSP_4:33;
 not the carrier of W1 c= the carrier of W2 by A2, VECTSP_4:27;
then consider x being set  such that
A7: x in the carrier of W1 and
A8: not x in the carrier of W2 by TARSKI:def_3;
reconsider x = x as Element of the carrier of W1 by A7;
reconsider x = x as Element of M by VECTSP_4:10;
A9: now__::_thesis:_not_x_+_y_in_the_carrier_of_W2
reconsider A2 = the carrier of W2 as Subset of M by VECTSP_4:def_2;
A10: A2 is linearly-closed by VECTSP_4:33;
assume  x + y in the carrier of W2 ; ::_thesis: contradiction
then  (x + y) - y in the carrier of W2 by A10, VECTSP_4:3;
then  x + (y - y) in the carrier of W2 by RLVECT_1:def_3;
then  x + (0. M) in the carrier of W2 by VECTSP_1:19;
hence  contradiction by A8, RLVECT_1:4; ::_thesis: verum
end;
A11: now__::_thesis:_not_x_+_y_in_the_carrier_of_W1
reconsider A2 = the carrier of W1 as Subset of M by VECTSP_4:def_2;
A12: A2 is linearly-closed by VECTSP_4:33;
assume  x + y in the carrier of W1 ; ::_thesis: contradiction
then  (y + x) - x in the carrier of W1 by A12, VECTSP_4:3;
then  y + (x - x) in the carrier of W1 by RLVECT_1:def_3;
then  y + (0. M) in the carrier of W1 by VECTSP_1:19;
hence  contradiction by A5, RLVECT_1:4; ::_thesis: verum
end;
 ( x in the carrier of W & y in the carrier of W ) by A1, XBOOLE_0:def_3;
then  x + y in the carrier of W by A6, VECTSP_4:def_1;
hence  contradiction by A1, A11, A9, XBOOLE_0:def_3; ::_thesis: verum
end;
A13: now__::_thesis:_(_W1_is_Subspace_of_W2_&_(_W1_is_Subspace_of_W2_or_W2_is_Subspace_of_W1_)_implies_ex_W_being_Subspace_of_M_st_the_carrier_of_W_=_the_carrier_of_W1_\/_the_carrier_of_W2_)
assume  W1 is Subspace of W2 ; ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
then  the carrier of W1 c= the carrier of W2 by VECTSP_4:def_2;
then  the carrier of W1 \/ the carrier of W2 = the carrier of W2 by XBOOLE_1:12;
hence  ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 ) ; ::_thesis: verum
end;
A14: now__::_thesis:_(_W2_is_Subspace_of_W1_&_(_W1_is_Subspace_of_W2_or_W2_is_Subspace_of_W1_)_implies_ex_W_being_Subspace_of_M_st_the_carrier_of_W_=_the_carrier_of_W1_\/_the_carrier_of_W2_)
assume  W2 is Subspace of W1 ; ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
then  the carrier of W2 c= the carrier of W1 by VECTSP_4:def_2;
then  the carrier of W1 \/ the carrier of W2 = the carrier of W1 by XBOOLE_1:12;
hence  ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 ) ; ::_thesis: verum
end;
assume  ( W1 is Subspace of W2 or W2 is Subspace of W1 ) ; ::_thesis: ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2
hence  ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 by A13, A14; ::_thesis: verum
end;

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
func Subspaces M ->  set  means :Def3: :: VECTSP_5:def 3
 for x being set holds
( x in it iff ex W being strict Subspace of M st W = x );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex W being strict Subspace of M st W = x )
proof
defpred S1[ set , set ] means  ex W being strict Subspace of M st
( $2 = W & $1 = the carrier of W );
defpred S2[ set ] means  ex W being strict Subspace of M st $1 = the carrier of W;
consider B being set  such that
A1: for x being set holds
( x in B iff ( x in bool the carrier of M & S2[x] ) ) from XBOOLE_0:sch_1();
A2: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2 by VECTSP_4:29;
consider f being Function such that
A3: for x, y being set holds
( [x,y] in f iff ( x in B & S1[x,y] ) ) from FUNCT_1:sch_1(A2);
 for x being set holds
( x in B iff ex y being set st [x,y] in f )
proof
let x be set ; ::_thesis: ( x in B iff ex y being set st [x,y] in f )
thus  ( x in B implies ex y being set st [x,y] in f ) ::_thesis: ( ex y being set st [x,y] in f implies x in B )
proof
assume A4: x in B ; ::_thesis: ex y being set st [x,y] in f
then consider W being strict Subspace of M such that
A5: x = the carrier of W by A1;
reconsider y = W as set ;
take  y ; ::_thesis: [x,y] in f
thus  [x,y] in f by A3, A4, A5; ::_thesis: verum
end;
given y being set  such that A6: [x,y] in f ; ::_thesis: x in B
thus  x in B by A3, A6; ::_thesis: verum
end;
then A7: B = dom f by XTUPLE_0:def_12;
 for y being set holds
( y in rng f iff ex W being strict Subspace of M st y = W )
proof
let y be set ; ::_thesis: ( y in rng f iff ex W being strict Subspace of M st y = W )
thus  ( y in rng f implies ex W being strict Subspace of M st y = W ) ::_thesis: ( ex W being strict Subspace of M st y = W implies y in rng f )
proof
assume  y in rng f ; ::_thesis: ex W being strict Subspace of M st y = W
then consider x being set  such that
A8: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
 [x,y] in f by A8, FUNCT_1:def_2;
then  ex W being strict Subspace of M st
( y = W & x = the carrier of W ) by A3;
hence  ex W being strict Subspace of M st y = W ; ::_thesis: verum
end;
given W being strict Subspace of M such that A9: y = W ; ::_thesis: y in rng f
reconsider W = y as Subspace of M by A9;
reconsider x = the carrier of W as set ;
 the carrier of W c= the carrier of M by VECTSP_4:def_2;
then A10: x in dom f by A1, A7, A9;
then  [x,y] in f by A3, A7, A9;
then  y = f . x by A10, FUNCT_1:def_2;
hence  y in rng f by A10, FUNCT_1:def_3; ::_thesis: verum
end;
hence  ex b1 being set st
for x being set holds
( x in b1 iff ex W being strict Subspace of M st W = x ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex W being strict Subspace of M st W = x ) ) & ( for x being set holds
( x in b2 iff ex W being strict Subspace of M st W = x ) ) holds
b1 = b2
proof
let D1, D2 be set ; ::_thesis: ( ( for x being set holds
( x in D1 iff ex W being strict Subspace of M st W = x ) ) & ( for x being set holds
( x in D2 iff ex W being strict Subspace of M st W = x ) ) implies D1 = D2 )
assume A11: for x being set holds
( x in D1 iff ex W being strict Subspace of M st x = W ) ; ::_thesis: ( ex x being set st
( ( x in D2 implies ex W being strict Subspace of M st W = x ) implies ( ex W being strict Subspace of M st W = x & not x in D2 ) ) or D1 = D2 )
assume A12: for x being set holds
( x in D2 iff ex W being strict Subspace of M st x = W ) ; ::_thesis: D1 = D2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_D1_implies_x_in_D2_)_&_(_x_in_D2_implies_x_in_D1_)_)
let x be set ; ::_thesis: ( ( x in D1 implies x in D2 ) & ( x in D2 implies x in D1 ) )
thus  ( x in D1 implies x in D2 ) ::_thesis: ( x in D2 implies x in D1 )
proof
assume  x in D1 ; ::_thesis: x in D2
then  ex W being strict Subspace of M st x = W by A11;
hence  x in D2 by A12; ::_thesis: verum
end;
assume  x in D2 ; ::_thesis: x in D1
then  ex W being strict Subspace of M st x = W by A12;
hence  x in D1 by A11; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Subspaces VECTSP_5:def_3_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for b3 being set holds
( b3 = Subspaces M iff for x being set holds
( x in b3 iff ex W being strict Subspace of M st W = x ) );

registration
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
cluster Subspaces M ->  non empty ;
coherence
 not Subspaces M is empty
proof
set W = the strict Subspace of M;
 the strict Subspace of M in Subspaces M by Def3;
hence  not Subspaces M is empty ; ::_thesis: verum
end;
end;

theorem :: VECTSP_5:36
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds M in Subspaces M
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds M in Subspaces M
let M be non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: M in Subspaces M
 ex W9 being strict Subspace of M st the carrier of ((Omega). M) = the carrier of W9 ;
hence  M in Subspaces M by Def3; ::_thesis: verum
end;

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let W1, W2 be Subspace of M;
predM is_the_direct_sum_of W1,W2 means :Def4: :: VECTSP_5:def 4
( VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 & W1 /\ W2 = (0). M );
end;

:: deftheorem Def4 defines is_the_direct_sum_of VECTSP_5:def_4_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( M is_the_direct_sum_of W1,W2 iff ( VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 & W1 /\ W2 = (0). M ) );

Lm16:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) iff for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) iff for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds
( W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) iff for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
let W1, W2 be Subspace of M; ::_thesis: ( W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) iff for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
thus  ( W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) implies for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) ::_thesis: ( ( for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) implies W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )
proof
assume A1: W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) ; ::_thesis: for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 )
let v be Element of M; ::_thesis: ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 )
 v in (Omega). M by RLVECT_1:1;
hence  ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) by A1, Th1; ::_thesis: verum
end;
assume A2: for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ; ::_thesis: W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #)
now__::_thesis:_(_W1_+_W2_is_Subspace_of_(Omega)._M_&_(_for_u_being_Element_of_M_holds_u_in_W1_+_W2_)_)
thus  W1 + W2 is Subspace of (Omega). M by Lm6; ::_thesis: for u being Element of M holds u in W1 + W2
let u be Element of M; ::_thesis: u in W1 + W2
 ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & u = v1 + v2 ) by A2;
hence  u in W1 + W2 by Th1; ::_thesis: verum
end;
hence  W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) by VECTSP_4:32; ::_thesis: verum
end;


definition
let F be Field;
let V be VectSp of F;
let W be Subspace of V;
mode Linear_Compl of W ->  Subspace of V means :Def5: :: VECTSP_5:def 5
V is_the_direct_sum_of it,W;
existence
 ex b1 being Subspace of V st V is_the_direct_sum_of b1,W
proof
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 XBOOLE_0: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__::_thesis:_for_x,_y_being_Element_of_X_st_S3[x,y]_&_S3[y,x]_holds_
x_=_y
let x, y be Element of X; ::_thesis: ( S3[x,y] & S3[y,x] implies x = y )
assume  ( S3[x,y] & S3[y,x] ) ; ::_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 VECTSP_4:25; ::_thesis: verum
end;
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 ; ::_thesis: ( 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 ; ::_thesis: ex y being Element of X st
for x being Element of X st x in Y holds
S3[x,y]
now__::_thesis:_ex_y9_being_Element_of_X_st_
for_x_being_Element_of_X_st_x_in_Y_holds_
[x,y9]_in_R
percases ( Y = {} or Y <> {} ) ;
supposeA7: Y = {} ; ::_thesis: ex y9 being Element of X st
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 A7; ::_thesis: verum
end;
supposeA8: Y <> {} ; ::_thesis: ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in R
defpred S4[ set , set ] means  ex W1 being strict Subspace of V st
( $1 = W1 & $2 = the carrier of W1 );
A9: for x being set st x in Y holds
ex y being set st S4[x,y]
proof
let x be set ; ::_thesis: ( x in Y implies ex y being set st S4[x,y] )
assume  x in Y ; ::_thesis: ex y being set st S4[x,y]
then consider W1 being strict Subspace of V such that
A10: x = W1 and
 W /\ W1 = (0). V by A1, A5;
reconsider y = the carrier of W1 as set ;
take  y ; ::_thesis: S4[x,y]
take  W1 ; ::_thesis: ( x = W1 & y = the carrier of W1 )
thus  ( x = W1 & y = the carrier of W1 ) by A10; ::_thesis: verum
end;
consider f being Function such that
A11: dom f = Y and
A12: for x being set st x in Y holds
S4[x,f . x] from CLASSES1:sch_1(A9);
set Z = union (rng f);
now__::_thesis:_for_x_being_set_st_x_in_union_(rng_f)_holds_
x_in_the_carrier_of_V
let x be set ; ::_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
A13: x in Y9 and
A14: Y9 in rng f by TARSKI:def_4;
consider y being set  such that
A15: y in dom f and
A16: f . y = Y9 by A14, FUNCT_1:def_3;
consider W1 being strict Subspace of V such that
 y = W1 and
A17: f . y = the carrier of W1 by A11, A12, A15;
 the carrier of W1 c= the carrier of V by VECTSP_4:def_2;
hence  x in the carrier of V by A13, A16, A17; ::_thesis: verum
end;
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 :: according to VECTSP_4:def_1 ::_thesis: 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; ::_thesis: ( v1 in Z & v2 in Z implies v1 + v2 in Z )
assume that
A19: v1 in Z and
A20: v2 in Z ; ::_thesis: 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 set  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 set  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__::_thesis:_v1_+_v2_in_Z
percases ( [y1,y2] in R or [y2,y1] in R ) by A6, A11, A23, A27;
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 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; ::_thesis: verum
end;
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 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; ::_thesis: verum
end;
end;
end;
hence  v1 + v2 in Z ; ::_thesis: verum
end;
let a be Element of F; ::_thesis: 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; ::_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
A37: v1 in Y1 and
A38: Y1 in rng f by TARSKI:def_4;
consider y1 being set  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; ::_thesis: verum
end;
set z = the Element of rng f;
A43: rng f <> {} by A8, A11, RELAT_1:42;
then consider z1 being set  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__::_thesis:_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; ::_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 )
proof
assume A47: u in W /\ E ; ::_thesis: 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 set  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; ::_thesis: verum
end;
assume  u in (0). V ; ::_thesis: u in W /\ E
then  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; ::_thesis: 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; ::_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 A57: x in Y ; ::_thesis: [x,y] in R
then consider W1 being strict Subspace of V such that
A58: x = W1 and
A59: f . x = the carrier of W1 by A12;
now__::_thesis:_for_u_being_Element_of_V_st_u_in_W1_holds_
u_in_E
let u be Element of V; ::_thesis: ( u in W1 implies u in E )
assume  u in W1 ; ::_thesis: u in E
then A60: u in the carrier of W1 by STRUCT_0:def_5;
 the carrier of W1 in rng f by A11, A57, A59, FUNCT_1:def_3;
then  u in Z by A60, TARSKI:def_4;
hence  u in E by A46, STRUCT_0:def_5; ::_thesis: verum
end;
then  W1 is Subspace of E by VECTSP_4:28;
hence  [x,y] in R by A2, A58; ::_thesis: verum
end;
end;
end;
hence  ex y being Element of X st
for x being Element of X st x in Y holds
S3[x,y] ; ::_thesis: verum
end;
A61: now__::_thesis:_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; ::_thesis: ( S3[x,y] & S3[y,z] implies S3[x,z] )
assume that
A62: S3[x,y] and
A63: S3[y,z] ; ::_thesis: 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; ::_thesis: verum
end;
A69: now__::_thesis:_for_x_being_Element_of_X_holds_S3[x,x]
let x be Element of X; ::_thesis: S3[x,x]
consider W1 being strict Subspace of V such that
A70: x = W1 and
 W /\ W1 = (0). V by A1;
 W1 is Subspace of W1 by VECTSP_4:24;
hence  S3[x,x] by A2, A70; ::_thesis: verum
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 ; ::_thesis: V is_the_direct_sum_of L,W
thus  VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = L + W :: according to VECTSP_5:def_4 ::_thesis: L /\ W = (0). V
proof
assume  not VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = L + W ; ::_thesis: 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  }  ;
now__::_thesis:_for_x_being_set_st_x_in__{__(a_*_v)_where_a_is_Element_of_F_:_verum__}__holds_
x_in_the_carrier_of_V
let x be set ; ::_thesis: ( x in  {  (a * v) where a is Element of F : verum  }  implies x in the carrier of V )
assume  x in  {  (a * v) where a is Element of F : verum  }  ; ::_thesis: x in the carrier of V
then  ex a being Element of F st x = a * v ;
hence  x in the carrier of V ; ::_thesis: verum
end;
then reconsider A =  {  (a * v) where a is Element of F : verum  }  as Subset of V by TARSKI:def_3;
 A is linearly-closed
proof
thus  for v1, v2 being Element of V st v1 in A & v2 in A holds
v1 + v2 in A :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of F
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A )
proof
let v1, v2 be Element 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 Element of F such that
A77: v1 = a1 * v ;
assume  v2 in A ; ::_thesis: v1 + v2 in A
then consider a2 being Element of F such that
A78: v2 = a2 * v ;
 v1 + v2 = (a1 + a2) * v by A77, A78, VECTSP_1:def_15;
hence  v1 + v2 in A ; ::_thesis: verum
end;
let a be Element of F; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in A or a * b1 in A )
let v1 be Element 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 Element of F such that
A79: v1 = a1 * v ;
 a * v1 = (a * a1) * v by A79, VECTSP_1:def_16;
hence  a * v1 in A ; ::_thesis: verum
end;
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;
now__::_thesis:_for_u_being_Element_of_V_holds_
(_(_u_in_Z_/\_(W_+_L)_implies_u_in_(0)._V_)_&_(_u_in_(0)._V_implies_u_in_Z_/\_(W_+_L)_)_)
let u be Element 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) )
proof
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 Element of F such that
A83: u = a * v ;
now__::_thesis:_not_a_<>_0._F
 u in W + L by A82, Th3;
then  (a ") * (a * v) in W + L by A83, VECTSP_4:21;
then A84: ((a ") * a) * v in W + L by VECTSP_1:def_16;
assume  a <> 0. F ; ::_thesis: contradiction
then  (1_ F) * v in W + L by A84, VECTSP_1:def_10;
then  (1_ F) * v in L + W by Lm1;
hence  contradiction by A81, VECTSP_1:def_17; ::_thesis: verum
end;
then  u = 0. V by A83, VECTSP_1:14;
hence  u in (0). V by VECTSP_4:17; ::_thesis: verum
end;
assume  u in (0). V ; ::_thesis: u in Z /\ (W + L)
then  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 /\ (W + L) by VECTSP_4:17; ::_thesis: verum
end;
then A85: Z /\ (W + L) = (0). V by VECTSP_4:30;
now__::_thesis:_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; ::_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 )
proof
assume A86: u in (Z + L) /\ W ; ::_thesis: 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; ::_thesis: verum
end;
assume  u in (0). V ; ::_thesis: u in (Z + L) /\ W
then  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; ::_thesis: 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, VECTSP_1:def_17;
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;
thus  L /\ W = (0). V by A73; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Linear_Compl VECTSP_5:def_5_:_
 for F being Field
for V being VectSp of F
for W, b4 being Subspace of V holds
( b4 is Linear_Compl of W iff V is_the_direct_sum_of b4,W );

Lm17:  for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds
M is_the_direct_sum_of W2,W1
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds
M is_the_direct_sum_of W2,W1
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds
M is_the_direct_sum_of W2,W1
let W1, W2 be Subspace of M; ::_thesis: ( M is_the_direct_sum_of W1,W2 implies M is_the_direct_sum_of W2,W1 )
assume A1: M is_the_direct_sum_of W1,W2 ; ::_thesis: M is_the_direct_sum_of W2,W1
then  VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 by Def4;
then A2: VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W2 + W1 by Lm1;
 W2 /\ W1 = (0). M by A1, Def4;
hence  M is_the_direct_sum_of W2,W1 by A2, Def4; ::_thesis: verum
end;


theorem :: VECTSP_5:37
for F being Field
for V being VectSp of F
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
W2 is Linear_Compl of W1
proof
let F be Field; ::_thesis: for V being VectSp of F
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
W2 is Linear_Compl of W1
let V be VectSp of F; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
W2 is Linear_Compl of W1
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1 )
assume  V is_the_direct_sum_of W1,W2 ; ::_thesis: W2 is Linear_Compl of W1
then  V is_the_direct_sum_of W2,W1 by Lm17;
hence  W2 is Linear_Compl of W1 by Def5; ::_thesis: verum
end;

theorem Th38: :: VECTSP_5:38
for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds
( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds
( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W holds
( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds
( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )
let L be Linear_Compl of W; ::_thesis: ( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )
thus  V is_the_direct_sum_of L,W by Def5; ::_thesis: V is_the_direct_sum_of W,L
hence  V is_the_direct_sum_of W,L by Lm17; ::_thesis: verum
end;

theorem Th39: :: VECTSP_5:39
for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds
( W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds
( W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W holds
( W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds
( W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
let L be Linear_Compl of W; ::_thesis: ( W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
 V is_the_direct_sum_of W,L by Th38;
hence  W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by Def4; ::_thesis: L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
hence  L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by Lm1; ::_thesis: verum
end;

theorem Th40: :: VECTSP_5:40
for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds
( W /\ L = (0). V & L /\ W = (0). V )
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds
( W /\ L = (0). V & L /\ W = (0). V )
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W holds
( W /\ L = (0). V & L /\ W = (0). V )
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds
( W /\ L = (0). V & L /\ W = (0). V )
let L be Linear_Compl of W; ::_thesis: ( W /\ L = (0). V & L /\ W = (0). V )
A1: V is_the_direct_sum_of W,L by Th38;
hence  W /\ L = (0). V by Def4; ::_thesis: L /\ W = (0). V
thus  L /\ W = (0). V by A1, Def4; ::_thesis: verum
end;


theorem :: VECTSP_5:41
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds
M is_the_direct_sum_of W2,W1 by Lm17;

theorem Th42: :: VECTSP_5:42
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds
( M is_the_direct_sum_of (0). M, (Omega). M & M is_the_direct_sum_of (Omega). M, (0). M )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds
( M is_the_direct_sum_of (0). M, (Omega). M & M is_the_direct_sum_of (Omega). M, (0). M )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: ( M is_the_direct_sum_of (0). M, (Omega). M & M is_the_direct_sum_of (Omega). M, (0). M )
 ( ((0). M) + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & (0). M = ((0). M) /\ ((Omega). M) ) by Th9, Th20;
hence  M is_the_direct_sum_of (0). M, (Omega). M by Def4; ::_thesis: M is_the_direct_sum_of (Omega). M, (0). M
hence  M is_the_direct_sum_of (Omega). M, (0). M by Lm17; ::_thesis: verum
end;

theorem :: VECTSP_5:43
for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds W is Linear_Compl of L
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds W is Linear_Compl of L
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W holds W is Linear_Compl of L
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds W is Linear_Compl of L
let L be Linear_Compl of W; ::_thesis: W is Linear_Compl of L
 V is_the_direct_sum_of L,W by Def5;
then  V is_the_direct_sum_of W,L by Lm17;
hence  W is Linear_Compl of L by Def5; ::_thesis: verum
end;

theorem :: VECTSP_5:44
for F being Field
for V being VectSp of F holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
proof
let F be Field; ::_thesis: for V being VectSp of F holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
let V be VectSp of F; ::_thesis: ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
 ( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V ) by Th42;
hence  ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Def5; ::_thesis: verum
end;


theorem Th45: :: VECTSP_5:45
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M
for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let W1, W2 be Subspace of M; ::_thesis: for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let C2 be Coset of W2; ::_thesis: ( C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2 )
set v = the Element of C1 /\ C2;
set C = C1 /\ C2;
assume A1: C1 /\ C2 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: C1 /\ C2 is Coset of W1 /\ W2
then reconsider v = the Element of C1 /\ C2 as Element of M by TARSKI:def_3;
 v in C2 by A1, XBOOLE_0:def_4;
then A2: C2 = v + W2 by VECTSP_4:77;
 v in C1 by A1, XBOOLE_0:def_4;
then A3: C1 = v + W1 by VECTSP_4:77;
 C1 /\ C2 is Coset of W1 /\ W2
proof
take  v ; :: according to VECTSP_4:def_6 ::_thesis: C1 /\ C2 = v + (W1 /\ W2)
thus  C1 /\ C2 c= v + (W1 /\ W2) :: according to XBOOLE_0:def_10 ::_thesis: v + (W1 /\ W2) c= C1 /\ C2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C1 /\ C2 or x in v + (W1 /\ W2) )
assume A4: x in C1 /\ C2 ; ::_thesis: x in v + (W1 /\ W2)
then  x in C1 by XBOOLE_0:def_4;
then consider u1 being Element of M such that
A5: u1 in W1 and
A6: x = v + u1 by A3, VECTSP_4:42;
 x in C2 by A4, XBOOLE_0:def_4;
then consider u2 being Element of M such that
A7: u2 in W2 and
A8: x = v + u2 by A2, VECTSP_4:42;
 u1 = u2 by A6, A8, RLVECT_1:8;
then  u1 in W1 /\ W2 by A5, A7, Th3;
hence  x in v + (W1 /\ W2) by A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + (W1 /\ W2) or x in C1 /\ C2 )
assume  x in v + (W1 /\ W2) ; ::_thesis: x in C1 /\ C2
then consider u being Element of M such that
A9: u in W1 /\ W2 and
A10: x = v + u by VECTSP_4:42;
 u in W2 by A9, Th3;
then A11: x in  {  (v + u2) where u2 is Element of M : u2 in W2  }  by A10;
 u in W1 by A9, Th3;
then  x in  {  (v + u1) where u1 is Element of M : u1 in W1  }  by A10;
hence  x in C1 /\ C2 by A3, A2, A11, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  C1 /\ C2 is Coset of W1 /\ W2 ; ::_thesis: verum
end;

theorem Th46: :: VECTSP_5:46
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( M is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( M is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds
( M is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} )
let W1, W2 be Subspace of M; ::_thesis: ( M is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
A1: W1 + W2 is Subspace of (Omega). M by Lm6;
thus  ( M is_the_direct_sum_of W1,W2 implies for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} ) ::_thesis: ( ( for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} ) implies M is_the_direct_sum_of W1,W2 )
proof
assume A2: M is_the_direct_sum_of W1,W2 ; ::_thesis: for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v}
then A3: VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 by Def4;
let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v}
let C2 be Coset of W2; ::_thesis: ex v being Element of M st C1 /\ C2 = {v}
consider v1 being Element of M such that
A4: C1 = v1 + W1 by VECTSP_4:def_6;
 v1 in (Omega). M by RLVECT_1:1;
then consider v11, v12 being Element of M such that
A5: v11 in W1 and
A6: v12 in W2 and
A7: v1 = v11 + v12 by A3, Th1;
consider v2 being Element of M such that
A8: C2 = v2 + W2 by VECTSP_4:def_6;
 v2 in (Omega). M by RLVECT_1:1;
then consider v21, v22 being Element of M such that
A9: v21 in W1 and
A10: v22 in W2 and
A11: v2 = v21 + v22 by A3, Th1;
take v = v12 + v21; ::_thesis: C1 /\ C2 = {v}
 {v} = C1 /\ C2
proof
thus A12: {v} c= C1 /\ C2 :: according to XBOOLE_0:def_10 ::_thesis: C1 /\ C2 c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in C1 /\ C2 )
assume  x in {v} ; ::_thesis: x in C1 /\ C2
then A13: x = v by TARSKI:def_1;
 v21 = v2 - v22 by A11, VECTSP_2:2;
then  v21 in C2 by A8, A10, VECTSP_4:62;
then  C2 = v21 + W2 by VECTSP_4:77;
then A14: x in C2 by A6, A13;
 v12 = v1 - v11 by A7, VECTSP_2:2;
then  v12 in C1 by A4, A5, VECTSP_4:62;
then  C1 = v12 + W1 by VECTSP_4:77;
then  x in C1 by A9, A13;
hence  x in C1 /\ C2 by A14, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C1 /\ C2 or x in {v} )
assume A15: x in C1 /\ C2 ; ::_thesis: x in {v}
then  C1 meets C2 by XBOOLE_0:4;
then reconsider C = C1 /\ C2 as Coset of W1 /\ W2 by Th45;
A16: v in {v} by TARSKI:def_1;
 W1 /\ W2 = (0). M by A2, Def4;
then  ex u being Element of M st C = {u} by VECTSP_4:72;
hence  x in {v} by A12, A15, A16, TARSKI:def_1; ::_thesis: verum
end;
hence  C1 /\ C2 = {v} ; ::_thesis: verum
end;
assume A17: for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} ; ::_thesis: M is_the_direct_sum_of W1,W2
A18: the carrier of W2 is Coset of W2 by VECTSP_4:73;
A19: the carrier of M c= the carrier of (W1 + W2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of M or x in the carrier of (W1 + W2) )
assume  x in the carrier of M ; ::_thesis: x in the carrier of (W1 + W2)
then reconsider u = x as Element of M ;
consider C1 being Coset of W1 such that
A20: u in C1 by VECTSP_4:68;
consider v being Element of M such that
A21: C1 /\ the carrier of W2 = {v} by A18, A17;
A22: v in {v} by TARSKI:def_1;
then  v in C1 by A21, XBOOLE_0:def_4;
then consider v1 being Element of M such that
A23: v1 in W1 and
A24: u - v1 = v by A20, VECTSP_4:79;
 v in the carrier of W2 by A21, A22, XBOOLE_0:def_4;
then A25: v in W2 by STRUCT_0:def_5;
 u = v1 + v by A24, VECTSP_2:2;
then  x in W1 + W2 by A25, A23, Th1;
hence  x in the carrier of (W1 + W2) by STRUCT_0:def_5; ::_thesis: verum
end;
 the carrier of W1 is Coset of W1 by VECTSP_4:73;
then consider v being Element of M such that
A26: the carrier of W1 /\ the carrier of W2 = {v} by A18, A17;
 the carrier of (W1 + W2) c= the carrier of M by VECTSP_4:def_2;
then  the carrier of M = the carrier of (W1 + W2) by A19, XBOOLE_0:def_10;
hence  VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 by A1, VECTSP_4:31; :: according to VECTSP_5:def_4 ::_thesis: W1 /\ W2 = (0). M
 0. M in W2 by VECTSP_4:17;
then A27: 0. M in the carrier of W2 by STRUCT_0:def_5;
 0. M in W1 by VECTSP_4:17;
then  0. M in the carrier of W1 by STRUCT_0:def_5;
then A28: 0. M in {v} by A26, A27, XBOOLE_0:def_4;
the carrier of ((0). M) = {(0. M)} by VECTSP_4:def_3
.= the carrier of W1 /\ the carrier of W2 by A26, A28, TARSKI:def_1
.= the carrier of (W1 /\ W2) by Def2 ;
hence  W1 /\ W2 = (0). M by VECTSP_4:29; ::_thesis: verum
end;

theorem :: VECTSP_5:47
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 + W2 = M iff for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) by Lm16;

theorem Th48: :: VECTSP_5:48
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for v, v1, v2, u1, u2 being Element of M st M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for v, v1, v2, u1, u2 being Element of M st M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M
for v, v1, v2, u1, u2 being Element of M st M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )
let W1, W2 be Subspace of M; ::_thesis: for v, v1, v2, u1, u2 being Element of M st M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )
let v, v1, v2, u1, u2 be Element of M; ::_thesis: ( M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 implies ( v1 = u1 & v2 = u2 ) )
reconsider C2 = v1 + W2 as Coset of W2 by VECTSP_4:def_6;
reconsider C1 = the carrier of W1 as Coset of W1 by VECTSP_4:73;
A1: v1 in C2 by VECTSP_4:44;
assume  M is_the_direct_sum_of W1,W2 ; ::_thesis: ( not v = v1 + v2 or not v = u1 + u2 or not v1 in W1 or not u1 in W1 or not v2 in W2 or not u2 in W2 or ( v1 = u1 & v2 = u2 ) )
then consider u being Element of M such that
A2: C1 /\ C2 = {u} by Th46;
assume that
A3: ( v = v1 + v2 & v = u1 + u2 ) and
A4: v1 in W1 and
A5: u1 in W1 and
A6: ( v2 in W2 & u2 in W2 ) ; ::_thesis: ( v1 = u1 & v2 = u2 )
A7: v2 - u2 in W2 by A6, VECTSP_4:23;
 v1 in C1 by A4, STRUCT_0:def_5;
then  v1 in C1 /\ C2 by A1, XBOOLE_0:def_4;
then A8: v1 = u by A2, TARSKI:def_1;
A9: u1 in C1 by A5, STRUCT_0:def_5;
u1 = (v1 + v2) - u2 by A3, VECTSP_2:2
.= v1 + (v2 - u2) by RLVECT_1:def_3 ;
then  u1 in C2 by A7;
then A10: u1 in C1 /\ C2 by A9, XBOOLE_0:def_4;
hence  v1 = u1 by A2, A8, TARSKI:def_1; ::_thesis: v2 = u2
 u1 = u by A10, A2, TARSKI:def_1;
hence  v2 = u2 by A3, A8, RLVECT_1:8; ::_thesis: verum
end;

theorem :: VECTSP_5:49
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M st M = W1 + W2 & ex v being Element of M st
for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) holds
M is_the_direct_sum_of W1,W2
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M st M = W1 + W2 & ex v being Element of M st
for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) holds
M is_the_direct_sum_of W1,W2
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M st M = W1 + W2 & ex v being Element of M st
for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) holds
M is_the_direct_sum_of W1,W2
let W1, W2 be Subspace of M; ::_thesis: ( M = W1 + W2 & ex v being Element of M st
for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) implies M is_the_direct_sum_of W1,W2 )
assume A1: M = W1 + W2 ; ::_thesis: ( for v being Element of M ex v1, v2, u1, u2 being Element of M st
( v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 & not ( v1 = u1 & v2 = u2 ) ) or M is_the_direct_sum_of W1,W2 )
 ( the carrier of ((0). M) = {(0. M)} & (0). M is Subspace of W1 /\ W2 ) by VECTSP_4:39, VECTSP_4:def_3;
then A2: {(0. M)} c= the carrier of (W1 /\ W2) by VECTSP_4:def_2;
given v being Element of M such that A3: for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 ) ; ::_thesis: M is_the_direct_sum_of W1,W2
assume  not M is_the_direct_sum_of W1,W2 ; ::_thesis: contradiction
then  W1 /\ W2 <> (0). M by A1, Def4;
then  the carrier of (W1 /\ W2) <> {(0. M)} by VECTSP_4:def_3;
then  {(0. M)} c< the carrier of (W1 /\ W2) by A2, XBOOLE_0:def_8;
then consider x being set  such that
A4: x in the carrier of (W1 /\ W2) and
A5: not x in {(0. M)} by XBOOLE_0:6;
A6: x in W1 /\ W2 by A4, STRUCT_0:def_5;
then  x in M by VECTSP_4:9;
then reconsider u = x as Element of M by STRUCT_0:def_5;
consider v1, v2 being Element of M such that
A7: v1 in W1 and
A8: v2 in W2 and
A9: v = v1 + v2 by A1, Lm16;
A10: v = (v1 + v2) + (0. M) by A9, RLVECT_1:4
.= (v1 + v2) + (u - u) by VECTSP_1:19
.= ((v1 + v2) + u) - u by RLVECT_1:def_3
.= ((v1 + u) + v2) - u by RLVECT_1:def_3
.= (v1 + u) + (v2 - u) by RLVECT_1:def_3 ;
 x in W2 by A6, Th3;
then A11: v2 - u in W2 by A8, VECTSP_4:23;
 x in W1 by A6, Th3;
then  v1 + u in W1 by A7, VECTSP_4:20;
then  v2 - u = v2 by A3, A7, A8, A9, A10, A11;
then  v2 + (- u) = v2 + (0. M) by RLVECT_1:4;
then  - u = 0. M by RLVECT_1:8;
then A12: u = - (0. M) by RLVECT_1:17;
 x <> 0. M by A5, TARSKI:def_1;
hence  contradiction by A12, RLVECT_1:12; ::_thesis: verum
end;


definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let v be Element of M;
let W1, W2 be Subspace of M;
assume A1: M is_the_direct_sum_of W1,W2 ;
funcv |-- (W1,W2) ->  Element of [: the carrier of M, the carrier of M:] means :Def6: :: VECTSP_5:def 6
( v = (it `1) + (it `2) & it `1 in W1 & it `2 in W2 );
existence
 ex b1 being Element of [: the carrier of M, the carrier of M:] st
( v = (b1 `1) + (b1 `2) & b1 `1 in W1 & b1 `2 in W2 )
proof
 W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) by A1, Def4;
then consider v1, v2 being Element of M such that
A2: ( v1 in W1 & v2 in W2 & v = v1 + v2 ) by Lm16;
take  [v1,v2] ; ::_thesis: ( v = ([v1,v2] `1) + ([v1,v2] `2) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 )
 [v1,v2] `1 = v1 by MCART_1:7;
hence  ( v = ([v1,v2] `1) + ([v1,v2] `2) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 ) by A2, MCART_1:7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of [: the carrier of M, the carrier of M:] st v = (b1 `1) + (b1 `2) & b1 `1 in W1 & b1 `2 in W2 & v = (b2 `1) + (b2 `2) & b2 `1 in W1 & b2 `2 in W2 holds
b1 = b2
proof
let t1, t2 be Element of [: the carrier of M, the carrier of M:]; ::_thesis: ( v = (t1 `1) + (t1 `2) & t1 `1 in W1 & t1 `2 in W2 & v = (t2 `1) + (t2 `2) & t2 `1 in W1 & t2 `2 in W2 implies t1 = t2 )
assume  ( v = (t1 `1) + (t1 `2) & t1 `1 in W1 & t1 `2 in W2 & v = (t2 `1) + (t2 `2) & t2 `1 in W1 & t2 `2 in W2 ) ; ::_thesis: t1 = t2
then A3: ( t1 `1 = t2 `1 & t1 `2 = t2 `2 ) by A1, Th48;
 t1 = [(t1 `1),(t1 `2)] by MCART_1:21;
hence  t1 = t2 by A3, MCART_1:21; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines |-- VECTSP_5:def_6_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for v being Element of M
for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds
for b6 being Element of [: the carrier of M, the carrier of M:] holds
( b6 = v |-- (W1,W2) iff ( v = (b6 `1) + (b6 `2) & b6 `1 in W1 & b6 `2 in W2 ) );

theorem Th50: :: VECTSP_5:50
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for v being Element of M st M is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for v being Element of M st M is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M
for v being Element of M st M is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
let W1, W2 be Subspace of M; ::_thesis: for v being Element of M st M is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
let v be Element of M; ::_thesis: ( M is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 )
assume A1: M is_the_direct_sum_of W1,W2 ; ::_thesis: (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
then A2: (v |-- (W1,W2)) `2 in W2 by Def6;
A3: M is_the_direct_sum_of W2,W1 by A1, Lm17;
then A4: ( v = ((v |-- (W2,W1)) `2) + ((v |-- (W2,W1)) `1) & (v |-- (W2,W1)) `1 in W2 ) by Def6;
A5: (v |-- (W2,W1)) `2 in W1 by A3, Def6;
 ( v = ((v |-- (W1,W2)) `1) + ((v |-- (W1,W2)) `2) & (v |-- (W1,W2)) `1 in W1 ) by A1, Def6;
hence  (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 by A1, A2, A4, A5, Th48; ::_thesis: verum
end;

theorem Th51: :: VECTSP_5:51
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for v being Element of M st M is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for v being Element of M st M is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M
for v being Element of M st M is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
let W1, W2 be Subspace of M; ::_thesis: for v being Element of M st M is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
let v be Element of M; ::_thesis: ( M is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 )
assume A1: M is_the_direct_sum_of W1,W2 ; ::_thesis: (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
then A2: (v |-- (W1,W2)) `2 in W2 by Def6;
A3: M is_the_direct_sum_of W2,W1 by A1, Lm17;
then A4: ( v = ((v |-- (W2,W1)) `2) + ((v |-- (W2,W1)) `1) & (v |-- (W2,W1)) `1 in W2 ) by Def6;
A5: (v |-- (W2,W1)) `2 in W1 by A3, Def6;
 ( v = ((v |-- (W1,W2)) `1) + ((v |-- (W1,W2)) `2) & (v |-- (W1,W2)) `1 in W1 ) by A1, Def6;
hence  (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 by A1, A2, A4, A5, Th48; ::_thesis: verum
end;

theorem :: VECTSP_5:52
for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V
for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds
t = v |-- (W,L)
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V
for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds
t = v |-- (W,L)
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V
for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds
t = v |-- (W,L)
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W
for v being Element of V
for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds
t = v |-- (W,L)
let L be Linear_Compl of W; ::_thesis: for v being Element of V
for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds
t = v |-- (W,L)
let v be Element of V; ::_thesis: for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds
t = v |-- (W,L)
let t be Element of [: the carrier of V, the carrier of V:]; ::_thesis: ( (t `1) + (t `2) = v & t `1 in W & t `2 in L implies t = v |-- (W,L) )
 V is_the_direct_sum_of W,L by Th38;
hence  ( (t `1) + (t `2) = v & t `1 in W & t `2 in L implies t = v |-- (W,L) ) by Def6; ::_thesis: verum
end;

theorem :: VECTSP_5:53
for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W
for v being Element of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
let L be Linear_Compl of W; ::_thesis: for v being Element of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
let v be Element of V; ::_thesis: ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
 V is_the_direct_sum_of W,L by Th38;
hence  ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v by Def6; ::_thesis: verum
end;

theorem :: VECTSP_5:54
for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W
for v being Element of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
let L be Linear_Compl of W; ::_thesis: for v being Element of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
let v be Element of V; ::_thesis: ( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
 V is_the_direct_sum_of W,L by Th38;
hence  ( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L ) by Def6; ::_thesis: verum
end;

theorem :: VECTSP_5:55
for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2
let L be Linear_Compl of W; ::_thesis: for v being Element of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2
let v be Element of V; ::_thesis: (v |-- (W,L)) `1 = (v |-- (L,W)) `2
 V is_the_direct_sum_of W,L by Th38;
hence  (v |-- (W,L)) `1 = (v |-- (L,W)) `2 by Th50; ::_thesis: verum
end;

theorem :: VECTSP_5:56
for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
let L be Linear_Compl of W; ::_thesis: for v being Element of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
let v be Element of V; ::_thesis: (v |-- (W,L)) `2 = (v |-- (L,W)) `1
 V is_the_direct_sum_of W,L by Th38;
hence  (v |-- (W,L)) `2 = (v |-- (L,W)) `1 by Th51; ::_thesis: verum
end;


definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
func SubJoin M ->  BinOp of (Subspaces M) means :Def7: :: VECTSP_5:def 7
 for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
it . (A1,A2) = W1 + W2;
existence
 ex b1 being BinOp of (Subspaces M) st
for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2
proof
defpred S1[ set , set , set ] means  for W1, W2 being Subspace of M st $1 = W1 & $2 = W2 holds
$3 = W1 + W2;
A1: for A1, A2 being Element of Subspaces M ex B being Element of Subspaces M st S1[A1,A2,B]
proof
let A1, A2 be Element of Subspaces M; ::_thesis: ex B being Element of Subspaces M st S1[A1,A2,B]
consider W1 being strict Subspace of M such that
A2: W1 = A1 by Def3;
consider W2 being strict Subspace of M such that
A3: W2 = A2 by Def3;
reconsider C = W1 + W2 as Element of Subspaces M by Def3;
take  C ; ::_thesis: S1[A1,A2,C]
thus  S1[A1,A2,C] by A2, A3; ::_thesis: verum
end;
thus  ex o being BinOp of (Subspaces M) st
for A1, A2 being Element of Subspaces M holds S1[A1,A2,o . (A1,A2)] from BINOP_1:sch_3(A1); ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Subspaces M) st ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 + W2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (Subspaces M); ::_thesis: ( ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 + W2 ) implies o1 = o2 )
assume A4: for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 + W2 ; ::_thesis: ( ex A1, A2 being Element of Subspaces M ex W1, W2 being Subspace of M st
( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 + W2 ) or o1 = o2 )
assume A5: for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 + W2 ; ::_thesis: o1 = o2
now__::_thesis:_for_x,_y_being_set_st_x_in_Subspaces_M_&_y_in_Subspaces_M_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Subspaces M & y in Subspaces M implies o1 . (x,y) = o2 . (x,y) )
assume that
A6: x in Subspaces M and
A7: y in Subspaces M ; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider A = x, B = y as Element of Subspaces M by A6, A7;
consider W1 being strict Subspace of M such that
A8: W1 = x by A6, Def3;
consider W2 being strict Subspace of M such that
A9: W2 = y by A7, Def3;
 o1 . (A,B) = W1 + W2 by A4, A8, A9;
hence  o1 . (x,y) = o2 . (x,y) by A5, A8, A9; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines SubJoin VECTSP_5:def_7_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for b3 being BinOp of (Subspaces M) holds
( b3 = SubJoin M iff for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b3 . (A1,A2) = W1 + W2 );

definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
func SubMeet M ->  BinOp of (Subspaces M) means :Def8: :: VECTSP_5:def 8
 for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
it . (A1,A2) = W1 /\ W2;
existence
 ex b1 being BinOp of (Subspaces M) st
for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2
proof
defpred S1[ set , set , set ] means  for W1, W2 being Subspace of M st $1 = W1 & $2 = W2 holds
$3 = W1 /\ W2;
A1: for A1, A2 being Element of Subspaces M ex B being Element of Subspaces M st S1[A1,A2,B]
proof
let A1, A2 be Element of Subspaces M; ::_thesis: ex B being Element of Subspaces M st S1[A1,A2,B]
consider W1 being strict Subspace of M such that
A2: W1 = A1 by Def3;
consider W2 being strict Subspace of M such that
A3: W2 = A2 by Def3;
reconsider C = W1 /\ W2 as Element of Subspaces M by Def3;
take  C ; ::_thesis: S1[A1,A2,C]
thus  S1[A1,A2,C] by A2, A3; ::_thesis: verum
end;
thus  ex o being BinOp of (Subspaces M) st
for A1, A2 being Element of Subspaces M holds S1[A1,A2,o . (A1,A2)] from BINOP_1:sch_3(A1); ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Subspaces M) st ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 /\ W2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (Subspaces M); ::_thesis: ( ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 /\ W2 ) implies o1 = o2 )
assume A4: for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 /\ W2 ; ::_thesis: ( ex A1, A2 being Element of Subspaces M ex W1, W2 being Subspace of M st
( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 /\ W2 ) or o1 = o2 )
assume A5: for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 /\ W2 ; ::_thesis: o1 = o2
now__::_thesis:_for_x,_y_being_set_st_x_in_Subspaces_M_&_y_in_Subspaces_M_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Subspaces M & y in Subspaces M implies o1 . (x,y) = o2 . (x,y) )
assume that
A6: x in Subspaces M and
A7: y in Subspaces M ; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider A = x, B = y as Element of Subspaces M by A6, A7;
consider W1 being strict Subspace of M such that
A8: W1 = x by A6, Def3;
consider W2 being strict Subspace of M such that
A9: W2 = y by A7, Def3;
 o1 . (A,B) = W1 /\ W2 by A4, A8, A9;
hence  o1 . (x,y) = o2 . (x,y) by A5, A8, A9; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines SubMeet VECTSP_5:def_8_:_
 for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for b3 being BinOp of (Subspaces M) holds
( b3 = SubMeet M iff for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b3 . (A1,A2) = W1 /\ W2 );

theorem Th57: :: VECTSP_5:57
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
A1: for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" B = B "/\" A
proof
let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: A "/\" B = B "/\" A
consider W1 being strict Subspace of M such that
A2: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A3: W2 = B by Def3;
thus A "/\" B = (SubMeet M) . (A,B) by LATTICES:def_2
.= W1 /\ W2 by A2, A3, Def8
.= (SubMeet M) . (B,A) by A2, A3, Def8
.= B "/\" A by LATTICES:def_2 ; ::_thesis: verum
end;
A4: for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds (A "/\" B) "\/" B = B
proof
let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: (A "/\" B) "\/" B = B
consider W1 being strict Subspace of M such that
A5: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A6: W2 = B by Def3;
reconsider AB = W1 /\ W2 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus (A "/\" B) "\/" B = (SubJoin M) . ((A "/\" B),B) by LATTICES:def_1
.= (SubJoin M) . (((SubMeet M) . (A,B)),B) by LATTICES:def_2
.= (SubJoin M) . (AB,B) by A5, A6, Def8
.= (W1 /\ W2) + W2 by A6, Def7
.= B by A6, Lm10, VECTSP_4:29 ; ::_thesis: verum
end;
A7: for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
proof
let A, B, C be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: A "/\" (B "/\" C) = (A "/\" B) "/\" C
consider W1 being strict Subspace of M such that
A8: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A9: W2 = B by Def3;
consider W3 being strict Subspace of M such that
A10: W3 = C by Def3;
reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "/\" (B "/\" C) = (SubMeet M) . (A,(B "/\" C)) by LATTICES:def_2
.= (SubMeet M) . (A,((SubMeet M) . (B,C))) by LATTICES:def_2
.= (SubMeet M) . (A,BC) by A9, A10, Def8
.= W1 /\ (W2 /\ W3) by A8, Def8
.= (W1 /\ W2) /\ W3 by Th14
.= (SubMeet M) . (AB,C) by A10, Def8
.= (SubMeet M) . (((SubMeet M) . (A,B)),C) by A8, A9, Def8
.= (SubMeet M) . ((A "/\" B),C) by LATTICES:def_2
.= (A "/\" B) "/\" C by LATTICES:def_2 ; ::_thesis: verum
end;
A11: for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
proof
let A, B, C be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: A "\/" (B "\/" C) = (A "\/" B) "\/" C
consider W1 being strict Subspace of M such that
A12: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A13: W2 = B by Def3;
consider W3 being strict Subspace of M such that
A14: W3 = C by Def3;
reconsider AB = W1 + W2, BC = W2 + W3 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "\/" (B "\/" C) = (SubJoin M) . (A,(B "\/" C)) by LATTICES:def_1
.= (SubJoin M) . (A,((SubJoin M) . (B,C))) by LATTICES:def_1
.= (SubJoin M) . (A,BC) by A13, A14, Def7
.= W1 + (W2 + W3) by A12, Def7
.= (W1 + W2) + W3 by Th6
.= (SubJoin M) . (AB,C) by A14, Def7
.= (SubJoin M) . (((SubJoin M) . (A,B)),C) by A12, A13, Def7
.= (SubJoin M) . ((A "\/" B),C) by LATTICES:def_1
.= (A "\/" B) "\/" C by LATTICES:def_1 ; ::_thesis: verum
end;
A15: for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" (A "\/" B) = A
proof
let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: A "/\" (A "\/" B) = A
consider W1 being strict Subspace of M such that
A16: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A17: W2 = B by Def3;
reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "/\" (A "\/" B) = (SubMeet M) . (A,(A "\/" B)) by LATTICES:def_2
.= (SubMeet M) . (A,((SubJoin M) . (A,B))) by LATTICES:def_1
.= (SubMeet M) . (A,AB) by A16, A17, Def7
.= W1 /\ (W1 + W2) by A16, Def8
.= A by A16, Lm11, VECTSP_4:29 ; ::_thesis: verum
end;
 for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "\/" B = B "\/" A
proof
let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: A "\/" B = B "\/" A
consider W1 being strict Subspace of M such that
A18: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A19: W2 = B by Def3;
thus A "\/" B = (SubJoin M) . (A,B) by LATTICES:def_1
.= W1 + W2 by A18, A19, Def7
.= W2 + W1 by Lm1
.= (SubJoin M) . (B,A) by A18, A19, Def7
.= B "\/" A by LATTICES:def_1 ; ::_thesis: verum
end;
then  ( LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-commutative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-associative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-absorbing & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-commutative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-associative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-absorbing ) by A11, A4, A1, A7, A15, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence  LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice ; ::_thesis: verum
end;

theorem Th58: :: VECTSP_5:58
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
 ex C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st
for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "/\" A = C & A "/\" C = C )
proof
reconsider C = (0). M as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
take  C ; ::_thesis: for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "/\" A = C & A "/\" C = C )
let A be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: ( C "/\" A = C & A "/\" C = C )
consider W being strict Subspace of M such that
A1: W = A by Def3;
thus C "/\" A = (SubMeet M) . (C,A) by LATTICES:def_2
.= ((0). M) /\ W by A1, Def8
.= C by Th20 ; ::_thesis: A "/\" C = C
thus A "/\" C = (SubMeet M) . (A,C) by LATTICES:def_2
.= W /\ ((0). M) by A1, Def8
.= C by Th20 ; ::_thesis: verum
end;
hence  LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice by Th57, LATTICES:def_13; ::_thesis: verum
end;

theorem Th59: :: VECTSP_5:59
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
 ex C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st
for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "\/" A = C & A "\/" C = C )
proof
consider W9 being strict Subspace of M such that
A1: the carrier of W9 = the carrier of ((Omega). M) ;
reconsider C = W9 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
take  C ; ::_thesis: for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "\/" A = C & A "\/" C = C )
let A be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: ( C "\/" A = C & A "\/" C = C )
consider W being strict Subspace of M such that
A2: W = A by Def3;
A3: C is Subspace of (Omega). M by Lm6;
thus C "\/" A = (SubJoin M) . (C,A) by LATTICES:def_1
.= W9 + W by A2, Def7
.= ((Omega). M) + W by A1, Lm5
.= VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) by Th11
.= C by A1, A3, VECTSP_4:31 ; ::_thesis: A "\/" C = C
thus A "\/" C = (SubJoin M) . (A,C) by LATTICES:def_1
.= W + W9 by A2, Def7
.= W + ((Omega). M) by A1, Lm5
.= VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) by Th11
.= C by A1, A3, VECTSP_4:31 ; ::_thesis: verum
end;
hence  LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice by Th57, LATTICES:def_14; ::_thesis: verum
end;

theorem Th60: :: VECTSP_5:60
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 01_Lattice
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 01_Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 01_Lattice
 LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is lower-bounded upper-bounded Lattice by Th58, Th59;
hence  LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 01_Lattice ; ::_thesis: verum
end;

theorem :: VECTSP_5:61
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
 for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st A [= C holds
A "\/" (B "/\" C) = (A "\/" B) "/\" C
proof
let A, B, C be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: ( A [= C implies A "\/" (B "/\" C) = (A "\/" B) "/\" C )
assume A1: A [= C ; ::_thesis: A "\/" (B "/\" C) = (A "\/" B) "/\" C
consider W1 being strict Subspace of M such that
A2: W1 = A by Def3;
consider W3 being strict Subspace of M such that
A3: W3 = C by Def3;
W1 + W3 = (SubJoin M) . (A,C) by A2, A3, Def7
.= A "\/" C by LATTICES:def_1
.= W3 by A1, A3, LATTICES:def_3 ;
then A4: W1 is Subspace of W3 by Th8;
consider W2 being strict Subspace of M such that
A5: W2 = B by Def3;
reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
reconsider BC = W2 /\ W3 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "\/" (B "/\" C) = (SubJoin M) . (A,(B "/\" C)) by LATTICES:def_1
.= (SubJoin M) . (A,((SubMeet M) . (B,C))) by LATTICES:def_2
.= (SubJoin M) . (A,BC) by A5, A3, Def8
.= W1 + (W2 /\ W3) by A2, Def7
.= (W1 + W2) /\ W3 by A4, Th30
.= (SubMeet M) . (AB,C) by A3, Def8
.= (SubMeet M) . (((SubJoin M) . (A,B)),C) by A2, A5, Def7
.= (SubMeet M) . ((A "\/" B),C) by LATTICES:def_1
.= (A "\/" B) "/\" C by LATTICES:def_2 ; ::_thesis: verum
end;
hence  LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice by Th57, LATTICES:def_12; ::_thesis: verum
end;

theorem :: VECTSP_5:62
for F being Field
for V being VectSp of F holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice
proof
let F be Field; ::_thesis: for V being VectSp of F holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice
let V be VectSp of F; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice
reconsider S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) as 01_Lattice by Th60;
reconsider S0 = S as 0_Lattice ;
reconsider S1 = S as 1_Lattice ;
consider W9 being strict Subspace of V such that
A1: the carrier of W9 = the carrier of ((Omega). V) ;
reconsider I = W9 as Element of S by Def3;
reconsider I1 = I as Element of S1 ;
reconsider Z = (0). V as Element of S by Def3;
reconsider Z0 = Z as Element of S0 ;
now__::_thesis:_for_A_being_Element_of_S0_holds_A_"/\"_Z0_=_Z0
let A be Element of S0; ::_thesis: A "/\" Z0 = Z0
consider W being strict Subspace of V such that
A2: W = A by Def3;
thus A "/\" Z0 = (SubMeet V) . (A,Z0) by LATTICES:def_2
.= W /\ ((0). V) by A2, Def8
.= Z0 by Th20 ; ::_thesis: verum
end;
then A3: Bottom S = Z by RLSUB_2:64;
now__::_thesis:_for_A_being_Element_of_S1_holds_A_"\/"_I1_=_W9
let A be Element of S1; ::_thesis: A "\/" I1 = W9
consider W being strict Subspace of V such that
A4: W = A by Def3;
A5: W9 is Subspace of (Omega). V by Lm6;
thus A "\/" I1 = (SubJoin V) . (A,I1) by LATTICES:def_1
.= W + W9 by A4, Def7
.= W + ((Omega). V) by A1, Lm5
.= VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by Th11
.= W9 by A1, A5, VECTSP_4:31 ; ::_thesis: verum
end;
then A6: Top S = I by RLSUB_2:65;
now__::_thesis:_for_A_being_Element_of_S_ex_B_being_Element_of_S_st_B_is_a_complement_of_A
A7: I is Subspace of (Omega). V by Lm6;
let A be Element of S; ::_thesis: ex B being Element of S st B is_a_complement_of A
consider W being strict Subspace of V such that
A8: W = A by Def3;
set L = the Linear_Compl of W;
consider W99 being strict Subspace of V such that
A9: the carrier of W99 = the carrier of the Linear_Compl of W by Lm4;
reconsider B9 = W99 as Element of S by Def3;
take B = B9; ::_thesis: B is_a_complement_of A
A10: B "/\" A = (SubMeet V) . (B,A) by LATTICES:def_2
.= W99 /\ W by A8, Def8
.= the Linear_Compl of W /\ W by A9, Lm8
.= Bottom S by A3, Th40 ;
B "\/" A = (SubJoin V) . (B,A) by LATTICES:def_1
.= W99 + W by A8, Def7
.= the Linear_Compl of W + W by A9, Lm5
.= VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by Th39
.= Top S by A1, A6, A7, VECTSP_4:31 ;
hence  B is_a_complement_of A by A10, LATTICES:def_18; ::_thesis: verum
end;
hence  LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice by LATTICES:def_19; ::_thesis: verum
end;