:: Operations on Subspaces in Real Linear Space
::  by Wojciech A. Trybulec
::
:: Received September 20, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RLVECT_1, RLSUB_1, REAL_1, ARYTM_3, STRUCT_0, SUBSET_1, TARSKI,
      SUPINF_2, XBOOLE_0, ARYTM_1, ZFMISC_1, FUNCT_1, RELAT_1, ALGSTR_0,
      CARD_1, FINSEQ_4, MCART_1, BINOP_1, LATTICES, EQREL_1, PBOOLE, RLSUB_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, FUNCT_1,
      NUMBERS, LATTICES, REAL_1, RELSET_1, STRUCT_0, ALGSTR_0, RLVECT_1,
      RLSUB_1, DOMAIN_1;
 constructors BINOP_1, REAL_1, MEMBERED, REALSET1, LATTICES, RLSUB_1;
 registrations SUBSET_1, RELSET_1, MEMBERED, STRUCT_0, LATTICES, RLVECT_1,
      RLSUB_1, RELAT_1;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions LATTICES, RLSUB_1, TARSKI, XBOOLE_0, RLVECT_1;
 theorems BINOP_1, FUNCT_1, LATTICES, MCART_1, RLSUB_1, RLVECT_1, TARSKI,
      ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, VECTSP_1, XCMPLX_0, ORDERS_1,
      STRUCT_0, XTUPLE_0;
 schemes BINOP_1, FUNCT_1, RELSET_1, XBOOLE_0, ORDERS_1, CLASSES1;

begin

reserve V for RealLinearSpace;
reserve W,W1,W2,W3 for Subspace of V;
reserve u,u1,u2,v,v1,v2 for VECTOR of V;
reserve a,a1,a2 for Real;
reserve X,Y,x,y,y1,y2 for set;

::
::  Definitions of sum and intersection of subspaces.
::

definition
  let V;
  let W1,W2;
  func W1 + W2 -> strict Subspace of V means
  :Def1:
  the carrier of it = {v + u : v in W1 & u in W2};
  existence
  proof
    reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of V
    by RLSUB_1:def 2;
    set VS = {v + u : v in W1 & u in W2};
    VS c= the carrier of V
    proof
      let x be set;
      assume x in VS;
      then ex v1,v2 st x = v1 + v2 & v1 in W1 & v2 in W2;
      hence thesis;
    end;
    then reconsider VS as Subset of V;
A1: 0.V = 0.V + 0.V by RLVECT_1:4;
    0.V in W1 & 0.V in W2 by RLSUB_1:17;
    then
A2: 0.V in VS by A1;
A3: VS = {v + u : v in V1 & u in V2}
    proof
      thus VS c= {v + u : v in V1 & u in V2}
      proof
        let x be set;
        assume x in VS;
        then consider v,u 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 thesis by A4;
      end;
      let x be set;
      assume x in {v + u : v in V1 & u in V2};
      then consider v,u 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 thesis by A6;
    end;
    V1 is linearly-closed & V2 is linearly-closed by RLSUB_1:34;
    hence thesis by A2,A3,RLSUB_1:6,35;
  end;
  uniqueness by RLSUB_1:30;
end;

definition
  let V;
  let W1,W2;
  func W1 /\ W2 -> strict Subspace of V means
  :Def2:
  the carrier of it = (the carrier of W1) /\ (the carrier of W2);
  existence
  proof
    set VW2 = the carrier of W2;
    set VW1 = the carrier of W1;
    set VV = the carrier of V;
    0.V in W2 by RLSUB_1:17;
    then
A1: 0.V in VW2 by STRUCT_0:def 5;
    VW1 c= VV & VW2 c= VV by RLSUB_1:def 2;
    then VW1 /\ VW2 c= VV /\ VV by XBOOLE_1:27;
    then reconsider
    V1 = VW1, V2 = VW2, V3 = VW1 /\ VW2 as Subset of the carrier of
    V by RLSUB_1:def 2;
    V1 is linearly-closed & V2 is linearly-closed by RLSUB_1:34;
    then
A2: V3 is linearly-closed by RLSUB_1:7;
    0.V in W1 by RLSUB_1:17;
    then 0.V in VW1 by STRUCT_0:def 5;
    then VW1 /\ VW2 <> {} by A1,XBOOLE_0:def 4;
    hence thesis by A2,RLSUB_1:35;
  end;
  uniqueness by RLSUB_1:30;
end;

::
::  Definitional theorems of sum and intersection of subspaces.
::

theorem Th1:
  x in W1 + W2 iff ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2
proof
  thus x in W1 + W2 implies ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2
  proof
    assume x in W1 + W2;
    then x in the carrier of W1 + W2 by STRUCT_0:def 5;
    then x in {v + u : v in W1 & u in W2} by Def1;
    then consider v1,v2 such that
A1: x = v1 + v2 & v1 in W1 & v2 in W2;
    take v1,v2;
    thus thesis by A1;
  end;
  given v1,v2 such that
A2: v1 in W1 & v2 in W2 & x = v1 + v2;
  x in {v + u : v in W1 & u in W2} by A2;
  then x in the carrier of W1 + W2 by Def1;
  hence thesis by STRUCT_0:def 5;
end;

theorem Th2:
  v in W1 or v in W2 implies v in W1 + W2
proof
  assume
A1: v in W1 or v in W2;
  now
    per cases by A1;
    suppose
A2:   v in W1;
      v = v + 0.V & 0.V in W2 by RLSUB_1:17,RLVECT_1:4;
      hence thesis by A2,Th1;
    end;
    suppose
A3:   v in W2;
      v = 0.V + v & 0.V in W1 by RLSUB_1:17,RLVECT_1:4;
      hence thesis by A3,Th1;
    end;
  end;
  hence thesis;
end;

theorem Th3:
  x in W1 /\ W2 iff x in W1 & x in W2
proof
  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 thesis by STRUCT_0:def 5;
end;

Lm1: W1 + W2 = W2 + W1
proof
  set A = {v + u : v in W1 & u in W2};
  set B = {v + u : v in W2 & u in W1};
A1: B c= A
  proof
    let x be set;
    assume x in B;
    then ex v,u st x = v + u & v in W2 & u in W1;
    hence thesis;
  end;
A2: the carrier of W1 + W2 = A by Def1;
  A c= B
  proof
    let x be set;
    assume x in A;
    then ex v,u st x = v + u & v in W1 & u in W2;
    hence thesis;
  end;
  then A = B by A1,XBOOLE_0:def 10;
  hence thesis by A2,Def1;
end;

Lm2: the carrier of W1 c= the carrier of W1 + W2
proof
  let x be set;
  set A = {v + u : v in W1 & u in W2};
  assume x in the carrier of W1;
  then reconsider v = x as Element of W1;
  reconsider v as VECTOR of V by RLSUB_1:10;
A1: v = v + 0.V by RLVECT_1:4;
  v in W1 & 0.V in W2 by RLSUB_1:17,STRUCT_0:def 5;
  then x in A by A1;
  hence thesis by Def1;
end;

Lm3: for W2 being strict Subspace of V holds the carrier of W1 c= the carrier
of W2 implies W1 + W2 = W2
proof
  let W2 be strict Subspace of V;
  assume
A1: the carrier of W1 c= the carrier of W2;
A2: the carrier of W1 + W2 c= the carrier of W2
  proof
    let x be set;
    assume x in the carrier of W1 + W2;
    then x in {v + u : v in W1 & u in W2} by Def1;
    then consider v,u such that
A3: x = v + u and
A4: v in W1 and
A5: u in W2;
    W1 is Subspace of W2 by A1,RLSUB_1:28;
    then v in W2 by A4,RLSUB_1:8;
    then v + u in W2 by A5,RLSUB_1:20;
    hence thesis by A3,STRUCT_0:def 5;
  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 thesis by RLSUB_1:30;
end;

theorem
  for W being strict Subspace of V holds W + W = W by Lm3;

theorem
  W1 + W2 = W2 + W1 by Lm1;

theorem Th6:
  W1 + (W2 + W3) = (W1 + W2) + W3
proof
  set A = {v + u : v in W1 & u in W2};
  set B = {v + u : v in W2 & u in W3};
  set C = {v + u : v in W1 + W2 & u in W3};
  set D = {v + u : v in W1 & u in W2 + W3};
A1: the carrier of W1 + (W2 + W3) = D by Def1;
A2: C c= D
  proof
    let x be set;
    assume x in C;
    then consider v,u 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 A by Def1;
    then consider u1,u2 such that
A6: v = u1 + u2 and
A7: u1 in W1 and
A8: u2 in W2;
    u2 + u in B 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 thesis by A3,A7,A9;
  end;
  D c= C
  proof
    let x be set;
    assume x in D;
    then consider v,u 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 B by Def1;
    then consider u1,u2 such that
A13: u = u1 + u2 and
A14: u1 in W2 and
A15: u2 in W3;
    v + u1 in A 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 thesis by A10,A15,A16;
  end;
  then D = C by A2,XBOOLE_0:def 10;
  hence thesis by A1,Def1;
end;

theorem Th7:
  W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2
proof
  the carrier of W1 c= the carrier of W1 + W2 by Lm2;
  hence W1 is Subspace of W1 + W2 by RLSUB_1:28;
  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 thesis by RLSUB_1:28;
end;

theorem Th8:
  for W2 being strict Subspace of V holds W1 is Subspace of W2 iff W1 + W2 = W2
proof
  let W2 be strict Subspace of V;
  thus W1 is Subspace of W2 implies W1 + W2 = W2
  proof
    assume W1 is Subspace of W2;
    then the carrier of W1 c= the carrier of W2 by RLSUB_1:def 2;
    hence thesis by Lm3;
  end;
  thus thesis by Th7;
end;

theorem Th9:
  for W being strict Subspace of V holds (0).V + W = W & W + (0).V = W
proof
  let W be strict Subspace of V;
  (0).V is Subspace of W by RLSUB_1:39;
  then the carrier of (0).V c= the carrier of W by RLSUB_1:def 2;
  hence (0).V + W = W by Lm3;
  hence thesis by Lm1;
end;

theorem
  (0).V + (Omega).V = the RLSStruct of V & (Omega). V + (0).V = the
  RLSStruct of V by Th9;

theorem Th11:
  (Omega).V + W = the RLSStruct of V & W + (Omega).V = the RLSStruct of V
proof
  the carrier of W c= the carrier of V by RLSUB_1:def 2;
  then W + (Omega).V = the RLSStruct of V by Lm3;
  hence thesis by Lm1;
end;

theorem
  for V being strict RealLinearSpace holds (Omega).V + (Omega).V = V by Th11;

theorem
  for W being strict Subspace of V holds W /\ W = W
proof
  let W be strict Subspace of V;
  the carrier of W = (the carrier of W) /\ (the carrier of W);
  hence thesis by Def2;
end;

theorem Th14:
  W1 /\ W2 = W2 /\ W1
proof
  the carrier of W1 /\ W2 = (the carrier of W2) /\ (the carrier of W1) by Def2;
  hence thesis by Def2;
end;

theorem Th15:
  W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
proof
  set V1 = the carrier of W1;
  set V2 = the carrier of W2;
  set V3 = the carrier of W3;
  the carrier of W1 /\ (W2 /\ W3) = V1 /\ (the carrier of W2 /\ W3) by Def2
    .= V1 /\ (V2 /\ V3) by Def2
    .= (V1 /\ V2) /\ V3 by XBOOLE_1:16
    .= (the carrier of W1 /\ W2) /\ V3 by Def2;
  hence thesis by Def2;
end;

Lm4: the carrier of W1 /\ W2 c= the carrier of W1
proof
  the carrier of W1 /\ W2 = (the carrier of W1) /\ (the carrier of W2) by Def2;
  hence thesis by XBOOLE_1:17;
end;

theorem Th16:
  W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2
proof
  the carrier of W1 /\ W2 c= the carrier of W1 by Lm4;
  hence W1 /\ W2 is Subspace of W1 by RLSUB_1:28;
  the carrier of W2 /\ W1 c= the carrier of W2 by Lm4;
  then the carrier of W1 /\ W2 c= the carrier of W2 by Th14;
  hence thesis by RLSUB_1:28;
end;

theorem Th17:
  for W1 being strict Subspace of V holds W1 is Subspace of W2 iff
  W1 /\ W2 = W1
proof
  let W1 be strict Subspace of V;
  thus W1 is Subspace of W2 implies W1 /\ W2 = W1
  proof
    assume W1 is Subspace of W2;
    then
A1: the carrier of W1 c= the carrier of W2 by RLSUB_1:def 2;
    the carrier of W1 /\ W2 = (the carrier of W1) /\ (the carrier of W2 )
    by Def2;
    hence thesis by A1,RLSUB_1:30,XBOOLE_1:28;
  end;
  thus thesis by Th16;
end;

theorem Th18:
  (0).V /\ W = (0).V & W /\ (0).V = (0).V
proof
  0.V in W by RLSUB_1:17;
  then 0.V in the carrier of W by STRUCT_0:def 5;
  then {0.V} c= the carrier of W by ZFMISC_1:31;
  then
A1: {0.V} /\ (the carrier of W) = {0.V} by XBOOLE_1:28;
  the carrier of (0).V /\ W = (the carrier of (0).V) /\ (the carrier of W)
  by Def2
    .= {0.V} /\ (the carrier of W) by RLSUB_1:def 3;
  hence (0).V /\ W = (0).V by A1,RLSUB_1:def 3;
  hence thesis by Th14;
end;

theorem
  (0).V /\ (Omega).V = (0).V & (Omega).V /\ (0).V = (0).V by Th18;

theorem Th20:
  for W being strict Subspace of V holds (Omega).V /\ W = W & W /\
  (Omega).V = W
proof
  let W be strict Subspace of V;
  the carrier of (Omega). V /\ W = (the carrier of V) /\ (the carrier of W
  ) & the carrier of W c= the carrier of V by Def2,RLSUB_1:def 2;
  hence (Omega).V /\ W = W by RLSUB_1:30,XBOOLE_1:28;
  hence thesis by Th14;
end;

theorem
  for V being strict RealLinearSpace holds (Omega).V /\ (Omega).V = V by Th20;

Lm5: the carrier of W1 /\ W2 c= the carrier of W1 + W2
proof
  the carrier of W1 /\ W2 c= the carrier of W1 & the carrier of W1 c= the
  carrier of W1 + W2 by Lm2,Lm4;
  hence thesis by XBOOLE_1:1;
end;

theorem
  W1 /\ W2 is Subspace of W1 + W2 by Lm5,RLSUB_1:28;

Lm6: the carrier of (W1 /\ W2) + W2 = the carrier of W2
proof
  thus the carrier of (W1 /\ W2) + W2 c= the carrier of W2
  proof
    let x be set;
    assume x in the carrier of (W1 /\ W2) + W2;
    then x in {u + v : u in W1 /\ W2 & v in W2} by Def1;
    then consider u,v 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,RLSUB_1:20;
    hence thesis by A1,STRUCT_0:def 5;
  end;
  let x be set;
  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;
  hence thesis by A4;
end;

theorem
  for W2 being strict Subspace of V holds (W1 /\ W2) + W2 = W2 by Lm6,
RLSUB_1:30;

Lm7: the carrier of W1 /\ (W1 + W2) = the carrier of W1
proof
  thus the carrier of W1 /\ (W1 + W2) c= the carrier of W1
  proof
    let x be set;
    assume
A1: x in the carrier of W1 /\ (W1 + W2);
    the carrier of W1 /\ (W1 + W2) = (the carrier of W1) /\ (the carrier
    of W1 + W2) by Def2;
    hence thesis by A1,XBOOLE_0:def 4;
  end;
  let x be set;
  assume
A2: x in the carrier of W1;
  the carrier of W1 c= the carrier of V by RLSUB_1:def 2;
  then reconsider x1 = x as Element of V by A2;
A3: x1 + 0.V = x1 & 0.V in W2 by RLSUB_1:17,RLVECT_1:4;
  x in W1 by A2,STRUCT_0:def 5;
  then x in {u + v : 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 thesis by Def2;
end;

theorem
  for W1 being strict Subspace of V holds W1 /\ (W1 + W2) = W1 by Lm7,
RLSUB_1:30;

Lm8: the carrier of (W1 /\ W2) + (W2 /\ W3) c= the carrier of W2 /\ (W1 + W3)
proof
  let x be set;
  assume x in the carrier of (W1 /\ W2) + (W2 /\ W3);
  then x in {u + v : u in W1 /\ W2 & v in W2 /\ W3} by Def1;
  then consider u,v 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,RLSUB_1: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 thesis by STRUCT_0:def 5;
end;

theorem
  (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3) by Lm8,RLSUB_1:28;

Lm9: W1 is Subspace of W2 implies the carrier of W2 /\ (W1 + W3) = the carrier
of (W1 /\ W2) + (W2 /\ W3)
proof
  assume
A1: W1 is Subspace of W2;
  thus the carrier of W2 /\ (W1 + W3) c= the carrier of (W1 /\ W2) + (W2 /\ W3
  )
  proof
    let x be set;
    assume x in the carrier of W2 /\ (W1 + 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 : u in W1 & v in W3} by Def1;
    then consider u1,v1 such that
A3: x = u1 + v1 and
A4: u1 in W1 and
A5: v1 in W3;
A6: u1 in W2 by A1,A4,RLSUB_1: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,RLSUB_1:23;
    then v1 + (u1 - u1) in W2 by RLVECT_1:def 3;
    then v1 + 0.V in W2 by RLVECT_1:15;
    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 thesis by STRUCT_0:def 5;
  end;
  thus thesis by Lm8;
end;

theorem
  W1 is Subspace of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3)
  by Lm9,RLSUB_1:30;

Lm10: the carrier of W2 + (W1 /\ W3) c= the carrier of (W1 + W2) /\ (W2 + W3)
proof
  let x be set;
  assume x in the carrier of W2 + (W1 /\ W3);
  then x in {u + v : u in W2 & v in W1 /\ W3} by Def1;
  then consider u,v 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 : 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 : 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 thesis by Def2;
end;

theorem
  W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3) by Lm10,RLSUB_1:28;

Lm11: W1 is Subspace of W2 implies the carrier of W2 + (W1 /\ W3) = the
carrier of (W1 + W2) /\ (W2 + W3)
proof
  reconsider V2 = the carrier of W2 as Subset of V by RLSUB_1:def 2;
A1: V2 is linearly-closed by RLSUB_1:34;
  assume W1 is Subspace of W2;
  then
A2: the carrier of W1 c= the carrier of W2 by RLSUB_1:def 2;
  thus the carrier of W2 + (W1 /\ W3) c= the carrier of (W1 + W2) /\ (W2 + W3)
  by Lm10;
  let x be set;
  assume x in the carrier of (W1 + W2) /\ (W2 + 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 : u1 in W1 & u2 in W2} by Def1;
  then consider u1,u2 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,RLSUB_1:def 1;
  then
A5: u1 + u2 in W2 by STRUCT_0:def 5;
  0.V in W1 /\ W3 & (u1 + u2) + 0.V = u1 + u2 by RLSUB_1:17,RLVECT_1:4;
  then x in {u + v : u in W2 & v in W1 /\ W3} by A3,A5;
  hence thesis by Def1;
end;

theorem
  W1 is Subspace of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3)
  by Lm11,RLSUB_1:30;

theorem Th29:
  W1 is strict Subspace of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3
proof
  assume
A1: W1 is strict Subspace of W3;
  thus (W1 + W2) /\ W3 = W3 /\ (W1 + W2) by Th14
    .= (W1 /\ W3) + (W3 /\ W2) by A1,Lm9,RLSUB_1:30
    .= W1 + (W3 /\ W2) by A1,Th17
    .= W1 + (W2 /\ W3) by Th14;
end;

theorem
  for W1,W2 being strict Subspace of V holds W1 + W2 = W2 iff W1 /\ W2 = W1
proof
  let W1,W2 be strict Subspace of V;
  W1 + W2 = W2 iff W1 is Subspace of W2 by Th8;
  hence thesis by Th17;
end;

theorem
  for W2,W3 being strict Subspace of V holds W1 is Subspace of W2
  implies W1 + W3 is Subspace of W2 + W3
proof
  let W2,W3 be strict Subspace of V;
  assume
A1: W1 is Subspace of W2;
  (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 thesis by Th8;
end;

theorem
  (ex W st the carrier of W = (the carrier of W1) \/ (the carrier of W2)
  ) iff W1 is Subspace of W2 or W2 is Subspace of W1
proof
  set VW1 = the carrier of W1;
  set VW2 = the carrier of W2;
  thus (ex W st the carrier of W = (the carrier of W1) \/ (the carrier of W2))
  implies W1 is Subspace of W2 or W2 is Subspace of W1
  proof
    given W such that
A1: the carrier of W = (the carrier of W1) \/ (the carrier of W2);
    set VW = the carrier of W;
    assume that
A2: not W1 is Subspace of W2 and
A3: not W2 is Subspace of W1;
    not VW2 c= VW1 by A3,RLSUB_1:28;
    then consider y being set such that
A4: y in VW2 and
A5: not y in VW1 by TARSKI:def 3;
    reconsider y as Element of VW2 by A4;
    reconsider y as VECTOR of V by RLSUB_1:10;
    reconsider A1 = VW as Subset of V by RLSUB_1:def 2;
A6: A1 is linearly-closed by RLSUB_1:34;
    not VW1 c= VW2 by A2,RLSUB_1:28;
    then consider x being set such that
A7: x in VW1 and
A8: not x in VW2 by TARSKI:def 3;
    reconsider x as Element of VW1 by A7;
    reconsider x as VECTOR of V by RLSUB_1:10;
A9: now
      reconsider A2 = VW2 as Subset of V by RLSUB_1:def 2;
A10:  A2 is linearly-closed by RLSUB_1:34;
      assume x + y in VW2;
      then (x + y) - y in VW2 by A10,RLSUB_1:3;
      then x + (y - y) in VW2 by RLVECT_1:def 3;
      then x + 0.V in VW2 by RLVECT_1:15;
      hence contradiction by A8,RLVECT_1:4;
    end;
A11: now
      reconsider A2 = VW1 as Subset of V by RLSUB_1:def 2;
A12:  A2 is linearly-closed by RLSUB_1:34;
      assume x + y in VW1;
      then (y + x) - x in VW1 by A12,RLSUB_1:3;
      then y + (x - x) in VW1 by RLVECT_1:def 3;
      then y + 0.V in VW1 by RLVECT_1:15;
      hence contradiction by A5,RLVECT_1:4;
    end;
    x in VW & y in VW by A1,XBOOLE_0:def 3;
    then x + y in VW by A6,RLSUB_1:def 1;
    hence thesis by A1,A11,A9,XBOOLE_0:def 3;
  end;
A13: now
    assume W1 is Subspace of W2;
    then VW1 c= VW2 by RLSUB_1:def 2;
    then VW1 \/ VW2 = VW2 by XBOOLE_1:12;
    hence thesis;
  end;
A14: now
    assume W2 is Subspace of W1;
    then VW2 c= VW1 by RLSUB_1:def 2;
    then VW1 \/ VW2 = VW1 by XBOOLE_1:12;
    hence thesis;
  end;
  assume W1 is Subspace of W2 or W2 is Subspace of W1;
  hence thesis by A13,A14;
end;

::
::  Introduction of a set of subspaces of real linear space.
::

definition
  let V;
  func Subspaces(V) -> set means
  :Def3:
  for x holds x in it iff x is strict Subspace of V;
  existence
  proof
    defpred Q[set,set] means (ex W being strict Subspace of V st $2 = W & $1 =
    the carrier of W);
    defpred P[set] means (ex W being strict Subspace of V st $1 = the carrier
    of W);
    consider B being set such that
A1: for x holds x in B iff x in bool(the carrier of V) & P[x] from
    XBOOLE_0:sch 1;
A2: for x,y1,y2 st Q[x,y1] & Q[x,y2] holds y1 = y2 by RLSUB_1:30;
    consider f being Function such that
A3: for x,y holds [x,y] in f iff x in B & Q[x,y] from FUNCT_1:sch 1(A2
    );
    for x holds x in B iff ex y st [x,y] in f
    proof
      let x;
      thus x in B implies ex y st [x,y] in f
      proof
        assume
A4:     x in B;
        then consider W being strict Subspace of V such that
A5:     x = the carrier of W by A1;
        reconsider y = W as set;
        take y;
        thus thesis by A3,A4,A5;
      end;
      given y such that
A6:   [x,y] in f;
      thus thesis by A3,A6;
    end;
    then
A7: B = dom f by XTUPLE_0:def 12;
    for y holds y in rng f iff y is strict Subspace of V
    proof
      let y;
      thus y in rng f implies y is strict Subspace of V
      proof
        assume y in rng f;
        then consider x 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 V st y = W & x = the carrier of W
        by A3;
        hence thesis;
      end;
      assume y is strict Subspace of V;
      then reconsider W = y as strict Subspace of V;
      reconsider x = the carrier of W as set;
      the carrier of W c= the carrier of V by RLSUB_1:def 2;
      then
A9:   x in dom f by A1,A7;
      then [x,y] in f by A3,A7;
      then y = f.x by A9,FUNCT_1:def 2;
      hence thesis by A9,FUNCT_1:def 3;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let D1,D2 be set;
    assume
A10: for x holds x in D1 iff x is strict Subspace of V;
    assume
A11: for x holds x in D2 iff x is strict Subspace of V;
    now
      let x;
      thus x in D1 implies x in D2
      proof
        assume x in D1;
        then x is strict Subspace of V by A10;
        hence thesis by A11;
      end;
      assume x in D2;
      then x is strict Subspace of V by A11;
      hence x in D1 by A10;
    end;
    hence thesis by TARSKI:1;
  end;
end;

registration
  let V;
  cluster Subspaces(V) -> non empty;
  coherence
  proof
    set x = the strict Subspace of V;
    x in Subspaces(V) by Def3;
    hence thesis;
  end;
end;

theorem
  for V being strict RealLinearSpace holds V in Subspaces(V)
proof
  let V be strict RealLinearSpace;
  (Omega).V in Subspaces(V) by Def3;
  hence thesis;
end;

::
::  Introduction of the direct sum of subspaces and
::  linear complement of subspace.
::

definition
  let V;
  let W1,W2;
  pred V is_the_direct_sum_of W1,W2 means
  :Def4:
  the RLSStruct of V = W1 + W2 & W1 /\ W2 = (0).V;
end;

Lm12: for V being RealLinearSpace, W being strict Subspace of V holds (for v
being VECTOR of V holds v in W) implies W = the RLSStruct of V
proof
  let V be RealLinearSpace, W be strict Subspace of V;
  assume for v being VECTOR of V holds v in W;
  then for v be VECTOR of V holds (v in W iff v in (Omega).V) by RLVECT_1:1;
  hence thesis by RLSUB_1:31;
end;

Lm13: for V being RealLinearSpace, W1,W2 being Subspace of V holds W1 + W2 =
the RLSStruct of V iff for v being VECTOR of V ex v1,v2 being VECTOR of V st v1
in W1 & v2 in W2 & v = v1 + v2
proof
  let V be RealLinearSpace, W1,W2 be Subspace of V;
  thus W1 + W2 = the RLSStruct of V implies for v being VECTOR of V ex v1,v2
  being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2
  proof
    assume
A1: W1 + W2 = the RLSStruct of V;
    let v be VECTOR of V;
    v in the RLSStruct of V by RLVECT_1:1;
    hence thesis by A1,Th1;
  end;
  assume
A2: for v being VECTOR of V ex v1,v2 being VECTOR of V st v1 in W1 & v2
  in W2 & v = v1 + v2;
  now
    let u be VECTOR of V;
    ex v1,v2 being VECTOR of V st v1 in W1 & v2 in W2 & u = v1 + v2 by A2;
    hence u in W1 + W2 by Th1;
  end;
  hence thesis by Lm12;
end;

Lm14: for V being add-associative right_zeroed right_complementable non empty
addLoopStr, v,v1,v2 being Element of V holds v = v1 + v2 iff v1 = v - v2
proof
  let V be add-associative right_zeroed right_complementable non empty
  addLoopStr, v,v1,v2 be Element of V;
  thus v = v1 + v2 implies v1 = v - v2
  proof
    assume v = v1 + v2;
    hence v - v2 = v1 + (v2 - v2) by RLVECT_1:def 3
      .= v1 + 0.V by VECTSP_1:19
      .= v1 by RLVECT_1:4;
  end;
  thus v1 = v - v2 implies v = v1 + v2
  proof
    assume v1 = v - v2;
    hence v1 + v2 = v + (-v2 + v2) by RLVECT_1:def 3
      .= v + 0.V by RLVECT_1:5
      .= v by RLVECT_1:4;
  end;
end;

Lm15: for V being RealLinearSpace, W being Subspace of V ex C being strict
Subspace of V st V is_the_direct_sum_of C,W
proof
  let V be RealLinearSpace;
  let W be Subspace of V;
  defpred P[set] means ex W1 being strict Subspace of V st $1 = W1 & W /\ W1 =
  (0).V;
  consider X such that
A1: x in X iff x in Subspaces(V) & P[x] from XBOOLE_0:sch 1;
  W /\ (0).V = (0).V & (0).V in Subspaces(V) by Def3,Th18;
  then reconsider X as non empty set by A1;
  defpred P[set,set] means ex W1,W2 being strict Subspace of V st $1 = W1 & $2
  = W2 & W1 is Subspace of W2;
  consider R being Relation of X such that
A2: for x,y being Element of X holds [x,y] in R iff P[x,y] from RELSET_1
  :sch 2;
  defpred P[set,set] means [$1,$2] in R;
  now
    let x,y,z be Element of X;
    assume that
A3: [x,y] in R and
A4: [y,z] in R;
    consider W1,W2 being strict Subspace of V such that
A5: x = W1 and
A6: y = W2 & W1 is Subspace of W2 by A2,A3;
    consider W3,W4 being strict Subspace of V such that
A7: y = W3 and
A8: z = W4 and
A9: W3 is Subspace of W4 by A2,A4;
    W1 is strict Subspace of W4 by A6,A7,A9,RLSUB_1:27;
    hence [x,z] in R by A2,A5,A8;
  end;
  then
A10: for x,y,z being Element of X st P[x,y] & P[y,z] holds P[x,z];
A11: now
    let x be Element of X;
    x in Subspaces(V) by A1;
    hence x is strict Subspace of V by Def3;
  end;
  now
    let x be Element of X;
    reconsider W = x as strict Subspace of V by A11;
    W is Subspace of W by RLSUB_1:25;
    hence [x,x] in R by A2;
  end;
  then
A12: for x being Element of X holds P[x,x];
  for Y st Y c= X & (for x,y being Element of X st x in Y & y in Y holds
  [x,y] in R or [y,x] in R) ex y being Element of X st for x being Element of X
  st x in Y holds [x,y] in R
  proof
    let Y;
    assume that
A13: Y c= X and
A14: for x,y being Element of X st x in Y & y in Y holds [x,y] in R or
    [y,x] in R;
    now
      per cases;
      suppose
A15:    Y = {};
        set y = the Element of X;
        take y9 = y;
        let x be Element of X;
        assume x in Y;
        hence [x,y9] in R by A15;
      end;
      suppose
A16:    Y <> {};
        defpred P[set,set] means ex W1 being strict Subspace of V st $1 = W1 &
        $2 = the carrier of W1;
A17:    for x st x in Y ex y st P[x,y]
        proof
          let x;
          assume x in Y;
          then consider W1 being strict Subspace of V such that
A18:      x = W1 and
          W /\ W1 = (0).V by A1,A13;
          reconsider y = the carrier of W1 as set;
          take y;
          take W1;
          thus thesis by A18;
        end;
        consider f being Function such that
A19:    dom f = Y and
A20:    for x st x in Y holds P[x,f.x] from CLASSES1:sch 1(A17);
        set Z = union(rng f);
        now
          let x;
          assume x in Z;
          then consider Y9 being set such that
A21:      x in Y9 and
A22:      Y9 in rng f by TARSKI:def 4;
          consider y such that
A23:      y in dom f and
A24:      f.y = Y9 by A22,FUNCT_1:def 3;
          consider W1 being strict Subspace of V such that
          y = W1 and
A25:      f.y = the carrier of W1 by A19,A20,A23;
          the carrier of W1 c= the carrier of V by RLSUB_1:def 2;
          hence x in the carrier of V by A21,A24,A25;
        end;
        then reconsider Z as Subset of V by TARSKI:def 3;
A26:    Z is linearly-closed
        proof
          thus for v1,v2 being VECTOR of V st v1 in Z & v2 in Z holds v1 + v2
          in Z
          proof
            let v1,v2 be VECTOR of V;
            assume that
A27:        v1 in Z and
A28:        v2 in Z;
            consider Y1 being set such that
A29:        v1 in Y1 and
A30:        Y1 in rng f by A27,TARSKI:def 4;
            consider y1 such that
A31:        y1 in dom f and
A32:        f.y1 = Y1 by A30,FUNCT_1:def 3;
            consider Y2 being set such that
A33:        v2 in Y2 and
A34:        Y2 in rng f by A28,TARSKI:def 4;
            consider y2 such that
A35:        y2 in dom f and
A36:        f.y2 = Y2 by A34,FUNCT_1:def 3;
            consider W1 being strict Subspace of V such that
A37:        y1 = W1 and
A38:        f.y1 = the carrier of W1 by A19,A20,A31;
            consider W2 being strict Subspace of V such that
A39:        y2 = W2 and
A40:        f.y2 = the carrier of W2 by A19,A20,A35;
            reconsider y1,y2 as Element of X by A13,A19,A31,A35;
            now
              per cases by A14,A19,A31,A35;
              suppose
                [y1,y2] in R;
                then ex W3,W4 being strict Subspace of V st y1 = W3 & y2 = W4
                & W3 is Subspace of W4 by A2;
                then the carrier of W1 c= the carrier of W2 by A37,A39,
RLSUB_1:def 2;
                then
A41:            v1 in W2 by A29,A32,A38,STRUCT_0:def 5;
                v2 in W2 by A33,A36,A40,STRUCT_0:def 5;
                then v1 + v2 in W2 by A41,RLSUB_1:20;
                then
A42:            v1 + v2 in the carrier of W2 by STRUCT_0:def 5;
                f.y2 in rng f by A35,FUNCT_1:def 3;
                hence thesis by A40,A42,TARSKI:def 4;
              end;
              suppose
                [y2,y1] in R;
                then ex W3,W4 being strict Subspace of V st y2 = W3 & y1 = W4
                & W3 is Subspace of W4 by A2;
                then the carrier of W2 c= the carrier of W1 by A37,A39,
RLSUB_1:def 2;
                then
A43:            v2 in W1 by A33,A36,A40,STRUCT_0:def 5;
                v1 in W1 by A29,A32,A38,STRUCT_0:def 5;
                then v1 + v2 in W1 by A43,RLSUB_1:20;
                then
A44:            v1 + v2 in the carrier of W1 by STRUCT_0:def 5;
                f.y1 in rng f by A31,FUNCT_1:def 3;
                hence thesis by A38,A44,TARSKI:def 4;
              end;
            end;
            hence thesis;
          end;
          let a;
          let v1 be VECTOR of V;
          assume v1 in Z;
          then consider Y1 being set such that
A45:      v1 in Y1 and
A46:      Y1 in rng f by TARSKI:def 4;
          consider y1 such that
A47:      y1 in dom f and
A48:      f.y1 = Y1 by A46,FUNCT_1:def 3;
          consider W1 being strict Subspace of V such that
          y1 = W1 and
A49:      f.y1 = the carrier of W1 by A19,A20,A47;
          v1 in W1 by A45,A48,A49,STRUCT_0:def 5;
          then a * v1 in W1 by RLSUB_1:21;
          then
A50:      a * v1 in the carrier of W1 by STRUCT_0:def 5;
          f.y1 in rng f by A47,FUNCT_1:def 3;
          hence thesis by A49,A50,TARSKI:def 4;
        end;
        set z = the Element of rng f;
A51:    rng f <> {} by A16,A19,RELAT_1:42;
        then consider z1 being set such that
A52:    z1 in dom f and
A53:    f.z1 = z by FUNCT_1:def 3;
        ex W3 being strict Subspace of V st z1 = W3 & f.z1 = the carrier
        of W3 by A19,A20,A52;
        then Z <> {} by A51,A53,ORDERS_1:6;
        then consider E being strict Subspace of V such that
A54:    Z = the carrier of E by A26,RLSUB_1:35;
        now
          let u be VECTOR of V;
          thus u in W /\ E implies u in (0).V
          proof
            assume
A55:        u in W /\ E;
            then
A56:        u in W by Th3;
            u in E by A55,Th3;
            then u in Z by A54,STRUCT_0:def 5;
            then consider Y1 being set such that
A57:        u in Y1 and
A58:        Y1 in rng f by TARSKI:def 4;
            consider y1 such that
A59:        y1 in dom f and
A60:        f.y1 = Y1 by A58,FUNCT_1:def 3;
A61:        ex W2 being strict Subspace of V st y1 = W2 & W /\ W2 = (0).
            V by A1,A13,A19,A59;
            consider W1 being strict Subspace of V such that
A62:        y1 = W1 and
A63:        f.y1 = the carrier of W1 by A19,A20,A59;
            u in W1 by A57,A60,A63,STRUCT_0:def 5;
            hence thesis by A62,A56,A61,Th3;
          end;
          assume u in (0).V;
          then u in the carrier of (0).V by STRUCT_0:def 5;
          then u in {0.V} by RLSUB_1:def 3;
          then u = 0.V by TARSKI:def 1;
          hence u in W /\ E by RLSUB_1:17;
        end;
        then
A64:    W /\ E = (0).V by RLSUB_1:31;
        E in Subspaces(V) by Def3;
        then reconsider y9 = E as Element of X by A1,A64;
        take y = y9;
        let x be Element of X;
        assume
A65:    x in Y;
        then consider W1 being strict Subspace of V such that
A66:    x = W1 and
A67:    f.x = the carrier of W1 by A20;
        now
          let u be VECTOR of V;
          assume u in W1;
          then
A68:      u in the carrier of W1 by STRUCT_0:def 5;
          the carrier of W1 in rng f by A19,A65,A67,FUNCT_1:def 3;
          then u in Z by A68,TARSKI:def 4;
          hence u in E by A54,STRUCT_0:def 5;
        end;
        then W1 is strict Subspace of E by RLSUB_1:29;
        hence [x,y] in R by A2,A66;
      end;
    end;
    hence thesis;
  end;
  then
A69: for Y st Y c= X & (for x,y being Element of X st x in Y & y in Y
  holds P[x,y] or P[y,x]) holds ex y being Element of X st for x being Element
  of X st x in Y holds P[x,y];
  now
    let x,y be Element of X;
    assume [x,y] in R & [y,x] in R;
    then ( ex W1,W2 being strict Subspace of V st x = W1 & y = W2 & W1 is
Subspace of W2 )& ex W3,W4 being strict Subspace of V st y = W3 & x = W4 & W3
    is Subspace of W4 by A2;
    hence x = y by RLSUB_1:26;
  end;
  then
A70: for x,y being Element of X st P[x,y] & P[y,x] holds x=y;
  consider x being Element of X such that
A71: for y being Element of X st x <> y holds not P[x,y] from ORDERS_1:
  sch 1(A12,A70,A10,A69);
  consider L being strict Subspace of V such that
A72: x = L and
A73: W /\ L = (0).V by A1;
  take L;
  thus the RLSStruct of V = L + W
  proof
    assume not thesis;
    then consider v being VECTOR of V such that
A74: for v1,v2 being VECTOR of V holds not v1 in L or not v2 in W or
    v <> v1 + v2 by Lm13;
    v = 0.V + v & 0.V in W by RLSUB_1:17,RLVECT_1:4;
    then
A75: not v in L by A74;
    set A = {a * v : not contradiction};
A76: 1 * v in A;
    now
      let x;
      assume x in A;
      then ex a st x = a * v;
      hence x in the carrier of V;
    end;
    then reconsider A as Subset of V by TARSKI:def 3;
    A is linearly-closed
    proof
      thus for v1,v2 being VECTOR of V st v1 in A & v2 in A holds v1 + v2 in A
      proof
        let v1,v2 be VECTOR of V;
        assume v1 in A;
        then consider a1 such that
A77:    v1 = a1 * v;
        assume v2 in A;
        then consider a2 such that
A78:    v2 = a2 * v;
        v1 + v2 = (a1 + a2) * v by A77,A78,RLVECT_1:def 6;
        hence thesis;
      end;
      let a;
      let v1 be VECTOR of V;
      assume v1 in A;
      then consider a1 such that
A79:  v1 = a1 * v;
      a * v1 = (a * a1) * v by A79,RLVECT_1:def 7;
      hence thesis;
    end;
    then consider Z being strict Subspace of V such that
A80: the carrier of Z = A by A76,RLSUB_1:35;
A81: not v in L + W by A74,Th1;
    now
      let u be VECTOR of V;
      thus u in Z /\ (W + L) implies u in (0).V
      proof
        assume
A82:    u in Z /\ (W + L);
        then u in Z by Th3;
        then u in A by A80,STRUCT_0:def 5;
        then consider a such that
A83:    u = a * v;
        now
          u in W + L by A82,Th3;
          then a" * (a * v) in W + L by A83,RLSUB_1:21;
          then
A84:      (a" * a) * v in W + L by RLVECT_1:def 7;
          assume a <> 0;
          then 1 * v in W + L by A84,XCMPLX_0:def 7;
          then 1 * v in L + W by Lm1;
          hence contradiction by A81,RLVECT_1:def 8;
        end;
        then u = 0.V by A83,RLVECT_1:10;
        hence thesis by RLSUB_1:17;
      end;
      assume u in (0).V;
      then u in the carrier of (0).V by STRUCT_0:def 5;
      then u in {0.V} by RLSUB_1:def 3;
      then u = 0.V by TARSKI:def 1;
      hence u in Z /\ (W + L) by RLSUB_1:17;
    end;
    then
A85: Z /\ (W + L) = (0).V by RLSUB_1:31;
    now
      let u be VECTOR of V;
      thus u in (Z + L) /\ W implies u in (0).V
      proof
        assume
A86:    u in (Z + L) /\ W;
        then u in Z + L by Th3;
        then consider v1,v2 being VECTOR of V such that
A87:    v1 in Z and
A88:    v2 in L and
A89:    u = v1 + v2 by Th1;
A90:    u in W by A86,Th3;
        then
A91:    u in W + L by Th2;
        v1 = u - v2 & v2 in W + L by A88,A89,Lm14,Th2;
        then v1 in W + L by A91,RLSUB_1:23;
        then v1 in Z /\ (W + L) by A87,Th3;
        then v1 in the carrier of (0).V by A85,STRUCT_0:def 5;
        then v1 in {0.V} by RLSUB_1:def 3;
        then v1 = 0.V by TARSKI:def 1;
        then v2 = u by A89,RLVECT_1:4;
        hence thesis by A73,A88,A90,Th3;
      end;
      assume u in (0).V;
      then u in the carrier of (0).V by STRUCT_0:def 5;
      then u in {0.V} by RLSUB_1:def 3;
      then u = 0.V by TARSKI:def 1;
      hence u in (Z + L) /\ W by RLSUB_1:17;
    end;
    then (Z + L) /\ W = (0).V by RLSUB_1:31;
    then
A92: W /\ (Z + L) = (0).V by Th14;
    (Z + L) in Subspaces(V) by Def3;
    then reconsider x1 = Z + L as Element of X by A1,A92;
    L is Subspace of Z + L by Th7;
    then
A93: [x,x1] in R by A2,A72;
    v in A by A76,RLVECT_1:def 8;
    then v in Z by A80,STRUCT_0:def 5;
    then Z + L <> L by A75,Th2;
    hence contradiction by A71,A72,A93;
  end;
  thus thesis by A73,Th14;
end;

definition
  let V be RealLinearSpace;
  let W be Subspace of V;
  mode Linear_Compl of W -> Subspace of V means
    :Def5:
    V is_the_direct_sum_of it,W;
  existence
  proof
    ex C being strict Subspace of V st V is_the_direct_sum_of C,W by Lm15;
    hence thesis;
  end;
end;

registration
  let V be RealLinearSpace;
  let W be Subspace of V;
  cluster strict for Linear_Compl of W;
  existence
  proof
    consider C being strict Subspace of V such that
A1: V is_the_direct_sum_of C,W by Lm15;
    C is Linear_Compl of W by A1,Def5;
    hence thesis;
  end;
end;

Lm16: V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1
proof
  assume
A1: V is_the_direct_sum_of W1,W2;
  then W1 /\ W2 = (0).V by Def4;
  then
A2: W2 /\ W1 = (0).V by Th14;
  the RLSStruct of V = W1 + W2 by A1,Def4;
  then the RLSStruct of V = W2 + W1 by Lm1;
  hence thesis by A2,Def4;
end;

theorem
  for V being RealLinearSpace, W1,W2 being Subspace of V holds V
  is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1
proof
  let V be RealLinearSpace, W1,W2 be Subspace of V;
  assume V is_the_direct_sum_of W1,W2;
  then V is_the_direct_sum_of W2,W1 by Lm16;
  hence thesis by Def5;
end;

theorem Th35:
  for V being RealLinearSpace, W being Subspace of V, 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 V be RealLinearSpace, W be Subspace of V, L be Linear_Compl of W;
  thus V is_the_direct_sum_of L,W by Def5;
  hence thesis by Lm16;
end;

::
::  Theorems concerning the direct sum of a subspaces,
::  linear complement of a subspace and coset of a subspace.
::

theorem Th36:
  for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W holds W + L = the RLSStruct of V & L + W = the RLSStruct of V
proof
  let V be RealLinearSpace, W be Subspace of V, L be Linear_Compl of W;
  V is_the_direct_sum_of W,L by Th35;
  hence W + L = the RLSStruct of V by Def4;
  hence thesis by Lm1;
end;

theorem Th37:
  for V being RealLinearSpace, W being Subspace of V, L being
  Linear_Compl of W holds W /\ L = (0).V & L /\ W = (0).V
proof
  let V be RealLinearSpace, W be Subspace of V, L be Linear_Compl of W;
  V is_the_direct_sum_of W,L by Th35;
  hence W /\ L = (0).V by Def4;
  hence thesis by Th14;
end;

theorem
  V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1 by Lm16;

theorem Th39:
  for V being RealLinearSpace holds V is_the_direct_sum_of (0).V,
  (Omega).V & V is_the_direct_sum_of (Omega).V,(0).V
proof
  let V be RealLinearSpace;
  (0).V + (Omega).V = the RLSStruct of V & (0).V = (0).V /\ (Omega). V by Th9
,Th18;
  hence V is_the_direct_sum_of (0).V,(Omega).V by Def4;
  hence thesis by Lm16;
end;

theorem
  for V being RealLinearSpace, W being Subspace of V, L being
  Linear_Compl of W holds W is Linear_Compl of L
proof
  let V be RealLinearSpace, W be Subspace of V, L be Linear_Compl of W;
  V is_the_direct_sum_of L,W by Def5;
  then V is_the_direct_sum_of W,L by Lm16;
  hence thesis by Def5;
end;

theorem
  for V being RealLinearSpace holds (0).V is Linear_Compl of (Omega).V &
  (Omega).V is Linear_Compl of (0).V
proof
  let V be RealLinearSpace;
  V is_the_direct_sum_of (0).V,(Omega).V & V is_the_direct_sum_of (Omega).
  V, (0).V by Th39;
  hence thesis by Def5;
end;

reserve C for Coset of W;
reserve C1 for Coset of W1;
reserve C2 for Coset of W2;

theorem Th42:
  C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2
proof
  set v = the Element of C1 /\ C2;
  set C = C1 /\ C2;
  assume
A1: C1 /\ C2 <> {};
  then reconsider v as Element of V by TARSKI:def 3;
  v in C2 by A1,XBOOLE_0:def 4;
  then
A2: C2 = v + W2 by RLSUB_1:78;
  v in C1 by A1,XBOOLE_0:def 4;
  then
A3: C1 = v + W1 by RLSUB_1:78;
  C is Coset of W1 /\ W2
  proof
    take v;
    thus C c= v + W1 /\ W2
    proof
      let x;
      assume
A4:   x in C;
      then x in C1 by XBOOLE_0:def 4;
      then consider u1 such that
A5:   u1 in W1 and
A6:   x = v + u1 by A3,RLSUB_1:63;
      x in C2 by A4,XBOOLE_0:def 4;
      then consider u2 such that
A7:   u2 in W2 and
A8:   x = v + u2 by A2,RLSUB_1:63;
      u1 = u2 by A6,A8,RLVECT_1:8;
      then u1 in W1 /\ W2 by A5,A7,Th3;
      hence thesis by A6;
    end;
    let x;
    assume x in v + (W1 /\ W2);
    then consider u such that
A9: u in W1 /\ W2 and
A10: x = v + u by RLSUB_1:63;
    u in W2 by A9,Th3;
    then
A11: x in {v + u2 : u2 in W2} by A10;
    u in W1 by A9,Th3;
    then x in {v + u1 : u1 in W1} by A10;
    hence thesis by A3,A2,A11,XBOOLE_0:def 4;
  end;
  hence thesis;
end;

Lm17: ex C st v in C
proof
  reconsider C = v + W as Coset of W by RLSUB_1:def 6;
  take C;
  thus thesis by RLSUB_1:43;
end;

theorem Th43:
  for V being RealLinearSpace, W1,W2 being Subspace of V holds V
  is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1, C2 being Coset of W2
  ex v being VECTOR of V st C1 /\ C2 = {v}
proof
  let V be RealLinearSpace, W1,W2 be Subspace of V;
  set VW1 = the carrier of W1;
  set VW2 = the carrier of W2;
  0.V in W2 by RLSUB_1:17;
  then
A1: 0.V in VW2 by STRUCT_0:def 5;
  thus V is_the_direct_sum_of W1,W2 implies for C1 being Coset of W1, C2 being
  Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v}
  proof
    assume
A2: V is_the_direct_sum_of W1,W2;
    then
A3: the RLSStruct of V = W1 + W2 by Def4;
    let C1 be Coset of W1, C2 be Coset of W2;
    consider v1 being VECTOR of V such that
A4: C1 = v1 + W1 by RLSUB_1:def 6;
    v1 in the RLSStruct of V by RLVECT_1:1;
    then consider v11,v12 being VECTOR of V such that
A5: v11 in W1 and
A6: v12 in W2 and
A7: v1 = v11 + v12 by A3,Th1;
    consider v2 being VECTOR of V such that
A8: C2 = v2 + W2 by RLSUB_1:def 6;
    v2 in the RLSStruct of V by RLVECT_1:1;
    then consider v21,v22 being VECTOR of V such that
A9: v21 in W1 and
A10: v22 in W2 and
A11: v2 = v21 + v22 by A3,Th1;
    take v = v12 + v21;
    {v} = C1 /\ C2
    proof
      thus
A12:  {v} c= C1 /\ C2
      proof
        let x;
        assume x in {v};
        then
A13:    x = v by TARSKI:def 1;
        v21 = v2 - v22 by A11,Lm14;
        then v21 in C2 by A8,A10,RLSUB_1:64;
        then C2 = v21 + W2 by RLSUB_1:78;
        then
A14:    x in C2 by A6,A13;
        v12 = v1 - v11 by A7,Lm14;
        then v12 in C1 by A4,A5,RLSUB_1:64;
        then C1 = v12 + W1 by RLSUB_1:78;
        then x in C1 by A9,A13;
        hence thesis by A14,XBOOLE_0:def 4;
      end;
      let x;
      assume
A15:  x in C1 /\ C2;
      then C1 meets C2 by XBOOLE_0:4;
      then reconsider C = C1 /\ C2 as Coset of W1 /\ W2 by Th42;
A16:  v in {v} by TARSKI:def 1;
      W1 /\ W2 = (0).V by A2,Def4;
      then ex u being VECTOR of V st C = {u} by RLSUB_1:73;
      hence thesis by A12,A15,A16,TARSKI:def 1;
    end;
    hence thesis;
  end;
  assume
A17: for C1 being Coset of W1, C2 being Coset of W2 ex v being VECTOR of
  V st C1 /\ C2 = {v};
A18: VW2 is Coset of W2 by RLSUB_1:74;
  now
    let u be VECTOR of V;
    consider C1 being Coset of W1 such that
A19: u in C1 by Lm17;
    consider v being VECTOR of V such that
A20: C1 /\ VW2 = {v} by A18,A17;
A21: v in {v} by TARSKI:def 1;
    then v in C1 by A20,XBOOLE_0:def 4;
    then consider v1 being VECTOR of V such that
A22: v1 in W1 and
A23: u - v1 = v by A19,RLSUB_1:80;
    v in VW2 by A20,A21,XBOOLE_0:def 4;
    then
A24: v in W2 by STRUCT_0:def 5;
    u = v1 + v by A23,Lm14;
    hence u in W1 + W2 by A24,A22,Th1;
  end;
  hence the RLSStruct of V = W1 + W2 by Lm12;
  VW1 is Coset of W1 by RLSUB_1:74;
  then consider v being VECTOR of V such that
A25: VW1 /\ VW2 = {v} by A18,A17;
  0.V in W1 by RLSUB_1:17;
  then 0.V in VW1 by STRUCT_0:def 5;
  then
A26: 0.V in {v} by A25,A1,XBOOLE_0:def 4;
  the carrier of (0).V = {0.V} by RLSUB_1:def 3
    .= VW1 /\ VW2 by A25,A26,TARSKI:def 1
    .= the carrier of W1 /\ W2 by Def2;
  hence thesis by RLSUB_1:30;
end;

::
::  Decomposition of a vector.
::

theorem
  for V being RealLinearSpace, W1,W2 being Subspace of V holds W1 + W2 =
the RLSStruct of V iff for v being VECTOR of V ex v1,v2 being VECTOR of V st v1
  in W1 & v2 in W2 & v = v1 + v2 by Lm13;

theorem Th45:
  V 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
proof
  reconsider C2 = v1 + W2 as Coset of W2 by RLSUB_1:def 6;
  reconsider C1 = the carrier of W1 as Coset of W1 by RLSUB_1:74;
A1: v1 in C2 by RLSUB_1:43;
  assume V is_the_direct_sum_of W1,W2;
  then consider u being VECTOR of V such that
A2: C1 /\ C2 = {u} by Th43;
  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;
A7: v2 - u2 in W2 by A6,RLSUB_1: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;
  u1 = (v1 + v2) - u2 by A3,Lm14
    .= v1 + (v2 - u2) by RLVECT_1:def 3;
  then
A9: u1 in C2 by A7;
  u1 in C1 by A5,STRUCT_0:def 5;
  then
A10: u1 in C1 /\ C2 by A9,XBOOLE_0:def 4;
  hence v1 = u1 by A2,A8,TARSKI:def 1;
  u1 = u by A10,A2,TARSKI:def 1;
  hence thesis by A3,A8,RLVECT_1:8;
end;

theorem
  V = W1 + W2 & (ex v st for v1,v2,u1,u2 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 V
  is_the_direct_sum_of W1,W2
proof
  assume
A1: V = W1 + W2;
  the carrier of (0).V = {0.V} & (0).V is Subspace of W1 /\ W2 by RLSUB_1:39
,def 3;
  then
A2: {0.V} c= the carrier of W1 /\ W2 by RLSUB_1:def 2;
  given v such that
A3: for v1,v2,u1,u2 st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 &
  v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2;
  assume not thesis;
  then W1 /\ W2 <> (0).V by A1,Def4;
  then the carrier of W1 /\ W2 <> {0.V} by RLSUB_1:def 3;
  then {0.V} c< the carrier of W1 /\ W2 by A2,XBOOLE_0:def 8;
  then consider x such that
A4: x in the carrier of W1 /\ W2 and
A5: not x in {0.V} by XBOOLE_0:6;
A6: x <> 0.V by A5,TARSKI:def 1;
A7: x in W1 /\ W2 by A4,STRUCT_0:def 5;
  then x in V by RLSUB_1:9;
  then reconsider u = x as VECTOR of V by STRUCT_0:def 5;
  consider v1,v2 such that
A8: v1 in W1 and
A9: v2 in W2 and
A10: v = v1 + v2 by A1,Lm13;
A11: v = v1 + v2 + 0.V by A10,RLVECT_1:4
    .= (v1 + v2) + (u - u) by RLVECT_1:15
    .= ((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 A7,Th3;
  then
A12: v2 - u in W2 by A9,RLSUB_1:23;
  x in W1 by A7,Th3;
  then v1 + u in W1 by A8,RLSUB_1:20;
  then v2 - u = v2 by A3,A8,A9,A10,A11,A12
    .= v2 - 0.V by RLVECT_1:13;
  hence thesis by A6,RLVECT_1:23;
end;

reserve t1,t2 for Element of [:the carrier of V, the carrier of V:];

definition
  let V;
  let v;
  let W1,W2;
  assume
A1: V is_the_direct_sum_of W1,W2;
  func v |-- (W1,W2) -> Element of [:the carrier of V, the carrier of V:]
  means
  :Def6:
  v = it`1 + it`2 & it`1 in W1 & it`2 in W2;
  existence
  proof
    W1 + W2 = the RLSStruct of V by A1,Def4;
    then consider v1,v2 such that
A2: v1 in W1 & v2 in W2 & v = v1 + v2 by Lm13;
    take [v1,v2];
    [v1,v2]`1 = v1 by MCART_1:7;
    hence thesis by A2,MCART_1:7;
  end;
  uniqueness
  proof
    let 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;
    then
A3: t1`1 = t2`1 & t1`2 = t2`2 by A1,Th45;
    t1 = [t1`1,t1`2] by MCART_1:21;
    hence thesis by A3,MCART_1:21;
  end;
end;

theorem Th47:
  V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2
proof
  assume
A1: V is_the_direct_sum_of W1,W2;
  then
A2: (v |-- (W1,W2))`2 in W2 by Def6;
A3: V is_the_direct_sum_of W2,W1 by A1,Lm16;
  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 thesis by A1,A2,A4,A5,Th45;
end;

theorem Th48:
  V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1
proof
  assume
A1: V is_the_direct_sum_of W1,W2;
  then
A2: (v |-- (W1,W2))`2 in W2 by Def6;
A3: V is_the_direct_sum_of W2,W1 by A1,Lm16;
  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 thesis by A1,A2,A4,A5,Th45;
end;

theorem
  for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W, v being VECTOR of V, t being Element of [:the carrier of V,
the carrier of V:] holds t`1 + t`2 = v & t`1 in W & t`2 in L implies t = v |--
  (W,L)
proof
  let V be RealLinearSpace, W be Subspace of V, L be Linear_Compl of W;
  V is_the_direct_sum_of W,L by Th35;
  hence thesis by Def6;
end;

theorem
  for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W, v being VECTOR of V holds (v |-- (W,L))`1 + (v |-- (W,L))`2
  = v
proof
  let V be RealLinearSpace, W be Subspace of V, L be Linear_Compl of W;
  V is_the_direct_sum_of W,L by Th35;
  hence thesis by Def6;
end;

theorem
  for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W, v being VECTOR of V holds (v |-- (W,L))`1 in W & (v |-- (W,L
  ))`2 in L
proof
  let V be RealLinearSpace, W be Subspace of V, L be Linear_Compl of W;
  V is_the_direct_sum_of W,L by Th35;
  hence thesis by Def6;
end;

theorem
  for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W, v being VECTOR of V holds (v |-- (W,L))`1 = (v |-- (L,W))`2
proof
  let V be RealLinearSpace, W be Subspace of V, L be Linear_Compl of W;
  V is_the_direct_sum_of W,L by Th35;
  hence thesis by Th47;
end;

theorem
  for V being RealLinearSpace, W being Subspace of V, L being
Linear_Compl of W, v being VECTOR of V holds (v |-- (W,L))`2 = (v |-- (L,W))`1
proof
  let V be RealLinearSpace, W be Subspace of V, L be Linear_Compl of W;
  V is_the_direct_sum_of W,L by Th35;
  hence thesis by Th48;
end;

::
::  Introduction of operations on set of subspaces as binary operations.
::

reserve A1,A2,B for Element of Subspaces(V);

definition
  let V;
  func SubJoin(V) -> BinOp of Subspaces(V) means
  :Def7:
  for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 + W2;
  existence
  proof
    defpred P[Element of Subspaces(V),Element of Subspaces(V), Element of
    Subspaces(V)] means for W1,W2 st $1 = W1 & $2 = W2 holds $3 = W1 + W2;
A1: for A1,A2 ex B st P[A1,A2,B]
    proof
      let A1,A2;
      reconsider W1 = A1, W2 = A2 as Subspace of V by Def3;
      reconsider C = W1 + W2 as Element of Subspaces(V) by Def3;
      take C;
      thus thesis;
    end;
    ex o being BinOp of Subspaces(V) st for a,b being Element of Subspaces
    (V) holds P[a,b,o.(a,b)] from BINOP_1:sch 3(A1);
    hence thesis;
  end;
  uniqueness
  proof
    let o1,o2 be BinOp of Subspaces(V);
    assume
A2: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o1.(A1,A2) = W1 + W2;
    assume
A3: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o2.(A1,A2) = W1 + W2;
    now
      let x,y be set;
      assume
A4:   x in Subspaces(V) & y in Subspaces(V);
      then reconsider A = x, B = y as Element of Subspaces(V);
      reconsider W1 = x, W2 = y as Subspace of V by A4,Def3;
      o1.(A,B) = W1 + W2 by A2;
      hence o1.(x,y) = o2.(x,y) by A3;
    end;
    hence thesis by BINOP_1:1;
  end;
end;

definition
  let V;
  func SubMeet(V) -> BinOp of Subspaces(V) means
  :Def8:
  for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 /\ W2;
  existence
  proof
    defpred P[Element of Subspaces(V),Element of Subspaces(V), Element of
    Subspaces(V)] means for W1,W2 st $1 = W1 & $2 = W2 holds $3 = W1 /\ W2;
A1: for A1,A2 ex B st P[A1,A2,B]
    proof
      let A1,A2;
      reconsider W1 = A1, W2 = A2 as Subspace of V by Def3;
      reconsider C = W1 /\ W2 as Element of Subspaces(V) by Def3;
      take C;
      thus thesis;
    end;
    ex o being BinOp of Subspaces(V) st for a,b being Element of Subspaces
    (V) holds P[a,b,o.(a,b)] from BINOP_1:sch 3(A1);
    hence thesis;
  end;
  uniqueness
  proof
    let o1,o2 be BinOp of Subspaces(V);
    assume
A2: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o1.(A1,A2) = W1 /\ W2;
    assume
A3: for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds o2.(A1,A2) = W1 /\ W2;
    now
      let x,y be set;
      assume
A4:   x in Subspaces(V) & y in Subspaces(V);
      then reconsider A = x, B = y as Element of Subspaces(V);
      reconsider W1 = x, W2 = y as Subspace of V by A4,Def3;
      o1.(A,B) = W1 /\ W2 by A2;
      hence o1.(x,y) = o2.(x,y) by A3;
    end;
    hence thesis by BINOP_1:1;
  end;
end;

::
::  Definitional theorems of functions SubJoin, SubMeet.
::

theorem Th54:
  LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is Lattice
proof
  set S = LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #);
A1: for A,B being Element of S holds A "/\" B = B "/\" A
  proof
    let A,B be Element of S;
    reconsider W1 = A, W2 = B as Subspace of V by Def3;
    thus A "/\" B = W1 /\ W2 by Def8
      .= W2 /\ W1 by Th14
      .= B "/\" A by Def8;
  end;
A2: for A,B being Element of S holds (A "/\" B) "\/" B = B
  proof
    let A,B be Element of S;
    reconsider W1 = A, W2 = B as strict Subspace of V by Def3;
    reconsider AB = W1 /\ W2 as Element of S by Def3;
    thus (A "/\" B) "\/" B = SubJoin(V).(AB,B) by Def8
      .= (W1 /\ W2) + W2 by Def7
      .= B by Lm6,RLSUB_1:30;
  end;
A3: for A,B,C being Element of S holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
  proof
    let A,B,C be Element of S;
    reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3;
    reconsider AB = W1 + W2, BC = W2 + W3 as Element of S by Def3;
    thus A "\/" (B "\/" C) = SubJoin(V).(A,BC) by Def7
      .= W1 + (W2 + W3) by Def7
      .= (W1 + W2) + W3 by Th6
      .= SubJoin(V).(AB,C) by Def7
      .= (A "\/" B) "\/" C by Def7;
  end;
A4: for A,B being Element of S holds A "/\" (A "\/" B) = A
  proof
    let A,B be Element of S;
    reconsider W1 = A, W2 = B as strict Subspace of V by Def3;
    reconsider AB = W1 + W2 as Element of S by Def3;
    thus A "/\" (A "\/" B) = SubMeet(V).(A,AB) by Def7
      .= W1 /\ (W1 + W2) by Def8
      .= A by Lm7,RLSUB_1:30;
  end;
A5: for A,B,C being Element of S holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
  proof
    let A,B,C be Element of S;
    reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3;
    reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of S by Def3;
    thus A "/\" (B "/\" C) = SubMeet(V).(A,BC) by Def8
      .= W1 /\ (W2 /\ W3) by Def8
      .= (W1 /\ W2) /\ W3 by Th15
      .= SubMeet(V).(AB,C) by Def8
      .= (A "/\" B) "/\" C by Def8;
  end;
  for A,B being Element of S holds A "\/" B = B "\/" A
  proof
    let A,B be Element of S;
    reconsider W1 = A, W2 = B as Subspace of V by Def3;
    thus A "\/" B = W1 + W2 by Def7
      .= W2 + W1 by Lm1
      .= B "\/" A by Def7;
  end;
  then S is join-commutative join-associative meet-absorbing meet-commutative
  meet-associative join-absorbing by A3,A2,A1,A5,A4,LATTICES:def 4,def 5,def 6
,def 7,def 8,def 9;
  hence thesis;
end;

registration
  let V;
  cluster LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) -> Lattice-like;
  coherence by Th54;
end;

theorem Th55:
  for V being RealLinearSpace holds LattStr (# Subspaces(V),
    SubJoin(V), SubMeet(V) #) is lower-bounded
proof
  let V be RealLinearSpace;
  set S = LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #);
  ex C being Element of S st for A being Element of S holds C "/\" A = C &
  A "/\" C = C
  proof
    reconsider C = (0).V as Element of S by Def3;
    take C;
    let A be Element of S;
    reconsider W = A as Subspace of V by Def3;
    thus C "/\" A = (0).V /\ W by Def8
      .= C by Th18;
    hence thesis;
  end;
  hence thesis by LATTICES:def 13;
end;

theorem Th56:
  for V being RealLinearSpace holds LattStr (# Subspaces(V),
    SubJoin(V), SubMeet(V) #) is upper-bounded
proof
  let V be RealLinearSpace;
  set S = LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #);
  ex C being Element of S st for A being Element of S holds C "\/" A = C &
  A "\/" C = C
  proof
    reconsider C = (Omega).V as Element of S by Def3;
    take C;
    let A be Element of S;
    reconsider W = A as Subspace of V by Def3;
    thus C "\/" A = (Omega).V + W by Def7
      .= C by Th11;
    hence thesis;
  end;
  hence thesis by LATTICES:def 14;
end;

theorem Th57:
  for V being RealLinearSpace holds LattStr (# Subspaces(V),
    SubJoin(V), SubMeet(V) #) is 01_Lattice
proof
  let V be RealLinearSpace;
  LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is lower-bounded
  upper-bounded Lattice by Th55,Th56;
  hence thesis;
end;

theorem Th58:
  for V being RealLinearSpace holds LattStr (# Subspaces(V),
    SubJoin(V), SubMeet(V) #) is modular
proof
  let V be RealLinearSpace;
  set S = LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #);
  for A,B,C being Element of S st A [= C holds A "\/" (B "/\" C) = (A "\/"
  B) "/\" C
  proof
    let A,B,C be Element of S;
    reconsider W1 = A, W2 = B, W3 = C as strict Subspace of V by Def3;
    assume
A1: A [= C;
    reconsider AB = W1 + W2 as Element of S by Def3;
    reconsider BC = W2 /\ W3 as Element of S by Def3;
    W1 + W3 = A "\/" C by Def7
      .= W3 by A1,LATTICES:def 3;
    then
A2: W1 is Subspace of W3 by Th8;
    thus A "\/" (B "/\" C) = SubJoin(V).(A,BC) by Def8
      .= W1 + (W2 /\ W3) by Def7
      .= (W1 + W2) /\ W3 by A2,Th29
      .= SubMeet(V).(AB,C) by Def8
      .= (A "\/" B) "/\" C by Def7;
  end;
  hence thesis by LATTICES:def 12;
end;

reserve l for Lattice;
reserve a,b for Element of l;

Lm18: a is_a_complement_of b iff a "\/" b = Top l & a "/\" b = Bottom l
proof
  not (a "\/" b = Top l & a "/\" b = Bottom l) implies not a
  is_a_complement_of b
  proof
    assume not (a "\/" b = Top l & a "/\" b = Bottom l);
    hence not (a "\/" b = Top l & b "\/" a = Top l & a "/\" b = Bottom l & b
    "/\" a = Bottom l);
  end;
  hence a is_a_complement_of b implies a "\/" b = Top l & a "/\" b = Bottom l;
  assume a "\/" b = Top l & a "/\" b = Bottom l;
  hence a "\/" b = Top l & b "\/" a = Top l & a "/\" b = Bottom l & b "/\" a =
  Bottom l;
end;

Lm19: (for a holds a "/\" b = b) implies b = Bottom l
proof
  assume
A1: for a holds a "/\" b = b;
  then for a holds a "/\" b = b & b "/\" a = b;
  then l is lower-bounded by LATTICES:def 13;
  hence Bottom l = Bottom l "/\" b
    .= b by A1;
end;

Lm20: (for a holds a "\/" b = b) implies b = Top l
proof
  assume
A1: for a holds a "\/" b = b;
  then for a holds b "\/" a = b & a "\/" b = b;
  then l is upper-bounded by LATTICES:def 14;
  hence Top l = Top l "\/" b
    .= b by A1;
end;

theorem Th59:
  for V being RealLinearSpace holds LattStr (# Subspaces(V),
    SubJoin(V), SubMeet(V) #) is complemented
proof
  let V be RealLinearSpace;
  reconsider S = LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) as
  01_Lattice by Th57;
  reconsider S0 = S as 0_Lattice;
  reconsider S1 = S as 1_Lattice;
  reconsider Z = (0).V, I = (Omega).V as Element of S by Def3;
  reconsider Z0 = Z as Element of S0;
  reconsider I1 = I as Element of S1;
  now
    let A be Element of S0;
    reconsider W = A as Subspace of V by Def3;
    thus A "/\" Z0 = W /\ (0).V by Def8
      .= Z0 by Th18;
  end;
  then
A1: Bottom S = Z by Lm19;
  now
    let A be Element of S1;
    reconsider W = A as Subspace of V by Def3;
    thus A "\/" I1 = W + (Omega).V by Def7
      .= (Omega).V by Th11;
  end;
  then
A2: Top S = I by Lm20;
  now
    let A be Element of S;
    reconsider W = A as Subspace of V by Def3;
    set L = the strict Linear_Compl of W;
    reconsider B9 = L as Element of S by Def3;
    take B = B9;
A3: B "/\" A = L /\ W by Def8
      .= Bottom S by A1,Th37;
    B "\/" A = L + W by Def7
      .= Top S by A2,Th36;
    hence B is_a_complement_of A by A3,Lm18;
  end;
  hence thesis by LATTICES:def 19;
end;

registration
  let V;
  cluster LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) -> lower-bounded
    upper-bounded modular complemented;
  coherence by Th55,Th56,Th58,Th59;
end;

::
::  Theorems concerning operations on subspaces (continuation). Proven
::  on the basis that set of subspaces with operations is a lattice.
::

theorem
  for V being RealLinearSpace, W1,W2,W3 being strict Subspace of V holds
  W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3
proof
  let V be RealLinearSpace, W1,W2,W3 be strict Subspace of V;
  set S = LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #);
  reconsider A = W1, B = W2, C = W3, AC = W1 /\ W3, BC = W2 /\ W3 as Element
  of S by Def3;
  assume
A1: W1 is Subspace of W2;
  A "\/" B = W1 + W2 by Def7
    .= B by A1,Th8;
  then A [= B by LATTICES:def 3;
  then A "/\" C [= B "/\" C by LATTICES:9;
  then
A2: (A "/\" C) "\/" (B "/\" C) = (B "/\" C) by LATTICES:def 3;
A3: B "/\" C = W2 /\ W3 by Def8;
  (A "/\" C) "\/" (B "/\" C) = SubJoin(V).(SubMeet(V).(A,C),BC) by Def8
    .= SubJoin(V).(AC,BC) by Def8
    .= (W1 /\ W3) + (W2 /\ W3) by Def7;
  hence thesis by A2,A3,Th8;
end;

::
::  Auxiliary theorems.
::

theorem
  for V being add-associative right_zeroed right_complementable non
empty addLoopStr, v,v1,v2 being Element of V holds v = v1 + v2 iff v1 = v - v2
  by Lm14;

theorem
  for V being RealLinearSpace, W being strict Subspace of V holds (for v
  being VECTOR of V holds v in W) implies W = the RLSStruct of V by Lm12;

theorem
  ex C st v in C by Lm17;

theorem
  (for a holds a "/\" b = b) implies b = Bottom l by Lm19;

theorem
  (for a holds a "\/" b = b) implies b = Top l by Lm20;