The Mizar article:

Subspaces and Cosets of Subspace of Real Unitary Space

by
Noboru Endou,
Takashi Mitsuishi, and
Yasunari Shidama

Received October 9, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: RUSUB_1
[ MML identifier index ]


environ

 vocabulary RLVECT_1, BINOP_1, FUNCT_1, PROB_2, ARYTM_1, RELAT_1, BHSP_1,
      BOOLE, RLSUB_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, NUMBERS, XCMPLX_0,
      XREAL_0, MCART_1, FUNCT_1, RELSET_1, REAL_1, FUNCT_2, DOMAIN_1, BINOP_1,
      RLVECT_1, RLSUB_1, BHSP_1;
 constructors REAL_1, DOMAIN_1, RLSUB_1, PARTFUN1, SEQ_1, BHSP_1, MEMBERED;
 clusters SUBSET_1, STRUCT_0, RELSET_1, BHSP_1, SEQ_1, FUNCT_1, MEMBERED;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions RLVECT_1, TARSKI, XBOOLE_0;
 theorems BHSP_1, RLVECT_1, FUNCT_1, TARSKI, FUNCT_2, ZFMISC_1, XBOOLE_0,
      RELAT_1, RELSET_1, RLSUB_1, XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes XBOOLE_0;

begin :: Definition and Axioms of the Subspace of Real Unitary Space

definition
let V be RealUnitarySpace;
mode Subspace of V -> RealUnitarySpace means
:Def1:
  the carrier of it c= the carrier of V &
  the Zero of it = the Zero of V &
  the add of it = (the add of V)|([:the carrier of it, the carrier of it:]) &
  the Mult of it = (the Mult of V)|([:REAL, the carrier of it:]) &
  the scalar of it
     = (the scalar of V)|([:the carrier of it, the carrier of it:]);
existence
proof
   take V;
A1:dom(the add of V)
     = [:the carrier of V, the carrier of V:] by FUNCT_2:def 1;
A2:dom(the Mult of V)
     = [:REAL, the carrier of V:] by FUNCT_2:def 1;
     dom(the scalar of V)
     = [:the carrier of V, the carrier of V:] by FUNCT_2:def 1;
   hence thesis by A1,A2,RELAT_1:98;
end;
end;

theorem
  for V being RealUnitarySpace, W1,W2 being Subspace of V, x being set st
 x in W1 & W1 is Subspace of W2 holds x in W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be Subspace of V;
   let x be set;
   assume x in W1 & W1 is Subspace of W2;
   then x in the carrier of W1 &
   the carrier of W1 c= the carrier of W2 by Def1,RLVECT_1:def 1;
   hence thesis by RLVECT_1:def 1;
end;

theorem Th2:
for V being RealUnitarySpace, W being Subspace of V, x being set st x in W
 holds x in V
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let x be set;
   assume x in W;
   then x in the carrier of W &
   the carrier of W c= the carrier of V by Def1,RLVECT_1:def 1;
   hence thesis by RLVECT_1:def 1;
end;

theorem Th3:
for V being RealUnitarySpace, W being Subspace of V, w being VECTOR of W holds
 w is VECTOR of V
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let w be VECTOR of W;
     w in W by RLVECT_1:3;
   then w in V by Th2;
   hence thesis by RLVECT_1:def 1;
end;

theorem Th4:
for V being RealUnitarySpace, W being Subspace of V holds 0.W = 0.V
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
     0.W = the Zero of W by RLVECT_1:def 2
      .= the Zero of V by Def1;
   hence thesis by RLVECT_1:def 2;
end;

theorem
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds 0.W1 = 0.W2
proof
   let V be RealUnitarySpace;
   let W1,W2 being Subspace of V;
     0.W1 = 0.V by Th4;
   hence thesis by Th4;
end;

theorem Th6:
for V being RealUnitarySpace, W being Subspace of V,
 u,v being VECTOR of V, w1,w2 being VECTOR of W st
  w1 = v & w2 = u holds w1 + w2 = v + u
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   let w1,w2 be VECTOR of W;
   assume
A1:v = w1 & u = w2;
   reconsider ww1 = w1, ww2 = w2 as VECTOR of V by Th3;
A2:v + u = (the add of V).[ww1,ww2] by A1,RLVECT_1:def 3;
     w1 + w2 = (the add of W).[w1,w2] by RLVECT_1:def 3
          .= ((the add of V) | [:the carrier of W, the carrier of W:]).[w1,w2]
          by Def1;
   hence thesis by A2,FUNCT_1:72;
end;

theorem Th7:
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V,
 w being VECTOR of W, a being Real st w = v holds a * w = a * v
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   let w be VECTOR of W;
   let a be Real;
   assume
A1:w = v;
   reconsider ww1 = w as VECTOR of V by Th3;
A2:a * v = (the Mult of V).[a,ww1] by A1,RLVECT_1:def 4;
     a * w = (the Mult of W).[a,w] by RLVECT_1:def 4
        .= ((the Mult of V) | [:REAL, the carrier of W:]).[a,w] by Def1;
   hence thesis by A2,FUNCT_1:72;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V, v1,v2 being VECTOR of V,
 w1,w2 being VECTOR of W st w1 = v1 & w2 = v2 holds w1 .|. w2 = v1 .|. v2
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v1,v2 be VECTOR of V;
   let w1,w2 be VECTOR of W;
   assume
A1:w1 = v1 & w2 = v2;
   reconsider ww1 = w1, ww2 = w2 as VECTOR of V by Th3;
A2:v1 .|. v2 = (the scalar of V).[ww1,ww2] by A1,BHSP_1:def 1;
     w1 .|. w2 = (the scalar of W).[w1,w2] by BHSP_1:def 1
    .= ((the scalar of V) | [:the carrier of W, the carrier of W:]).[w1,w2]
    by Def1;
   hence thesis by A2,FUNCT_1:72;
end;

theorem Th9:
for V being RealUnitarySpace, W being Subspace of V,
 v being VECTOR of V, w being VECTOR of W st w = v holds - v = - w
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   let w be VECTOR of W;
   assume
A1:w = v;
     - v = (- 1) * v & - w = (- 1) * w by RLVECT_1:29;
   hence thesis by A1,Th7;
end;

theorem Th10:
for V being RealUnitarySpace, W being Subspace of V,
 u,v being VECTOR of V, w1,w2 being VECTOR of W st w1 = v & w2 = u
 holds w1 - w2 = v - u
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   let w1,w2 be VECTOR of W;
   assume that
A1:w1 = v and
A2:w2 = u;
A3:- w2 = - u by A2,Th9;
     w1 - w2 = w1 + (- w2) & v - u = v + (- u) by RLVECT_1:def 11;
   hence thesis by A1,A3,Th6;
end;

theorem Th11:
for V being RealUnitarySpace, W being Subspace of V holds
 0.V in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
     0.W in W & 0.V = 0.W by Th4,RLVECT_1:3;
   hence thesis;
end;

theorem
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 0.W1 in W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be Subspace of V;
     0.W1 = 0.V by Th4;
   hence thesis by Th11;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V holds
 0.W in V
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
     0.W in W by RLVECT_1:3;
   hence thesis by Th2;
end;

Lm1:
for V being RealUnitarySpace, W being Subspace of V,
 V1,V2 being Subset of V st
  the carrier of W = V1 holds V1 is lineary-closed
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let V1,V2 be Subset of V;
   assume
A1:the carrier of W = V1;
   set VW = the carrier of W;
   reconsider WW = W as RealUnitarySpace;
A2:for v,u being VECTOR of V st v in V1 & u in V1 holds v + u in V1
   proof let v,u be VECTOR of V;
     assume v in V1 & u in V1;
      then reconsider vv = v, uu = u as VECTOR of WW by A1;
      reconsider vw = vv + uu as Element of VW;
         vw in V1 by A1;
    hence v + u in V1 by Th6;
   end;
     for a being Real, v being VECTOR of V st v in V1 holds a * v in V1
   proof
     let a be Real, v be VECTOR of V;
     assume v in V1;
     then reconsider vv = v as VECTOR of WW by A1;
     reconsider vw = a * vv as Element of VW;
       vw in V1 by A1;
     hence a * v in V1 by Th7;
   end;
   hence thesis by A2,RLSUB_1:def 1;
end;

theorem Th14:
for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V
 st u in W & v in W holds u + v in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   assume u in W & v in W;
then A1:u in the carrier of W & v in the carrier of W by RLVECT_1:def 1;
   reconsider VW = the carrier of W as Subset of V by Def1;
     VW is lineary-closed by Lm1;
   then u + v in the carrier of W by A1,RLSUB_1:def 1;
   hence thesis by RLVECT_1:def 1;
end;

theorem Th15:
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V,
 a being Real st v in W holds a * v in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   let a be Real;
   assume v in W;
then A1:v in the carrier of W by RLVECT_1:def 1;
   reconsider VW = the carrier of W as Subset of V by Def1;
     VW is lineary-closed by Lm1;
   then a * v in the carrier of W by A1,RLSUB_1:def 1;
   hence thesis by RLVECT_1:def 1;
end;

theorem Th16:
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V
 st v in W holds - v in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   assume v in W;
   then (- 1) * v in W by Th15;
   hence thesis by RLVECT_1:29;
end;

theorem Th17:
for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR of V
 st u in W & v in W holds u - v in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   assume that
A1:u in W and A2: v in W;
     - v in W by A2,Th16;
   then u + (- v) in W by A1,Th14;
   hence thesis by RLVECT_1:def 11;
end;

theorem Th18:
for V being RealUnitarySpace, V1 being Subset of V,
D being non empty set, d1 being Element of D, A being BinOp of D,
M being Function of [:REAL, D:], D, S being Function of [:D,D:],REAL st
 V1 = D &
 d1 = 0.V &
 A = (the add of V) | [:V1,V1:] &
 M = (the Mult of V) | [:REAL,V1:] &
 S = (the scalar of V) | [:V1,V1:] holds
           UNITSTR (# D,d1,A,M,S #) is Subspace of V
proof
   let V be RealUnitarySpace;
   let V1 be Subset of V;
   let D be non empty set;
   let d1 be Element of D;
   let A be BinOp of D;
   let M be Function of [:REAL, D:], D;
   let S be Function of [:D, D:], REAL;
   assume that
A1:V1 = D and
A2:d1 = 0.V and
A3:A = (the add of V) | [:V1,V1:] and
A4:M = (the Mult of V) | [:REAL,V1:] and
A5:S = (the scalar of V) | [:V1,V1:];
     UNITSTR (# D,d1,A,M,S #) is Subspace of V
   proof
     set W = UNITSTR (# D,d1,A,M,S #);
A6:  the Zero of W = the Zero of V by A2,RLVECT_1:def 2;
A7:  for x,y being VECTOR of W holds x + y = (the add of V).[x,y]
     proof
       let x,y be VECTOR of W;
         x + y = ((the add of V) | [:the carrier of W, the carrier of W:]
       ).[x,y] by A1,A3,RLVECT_1:def 3;
       hence thesis by FUNCT_1:72;
     end;
A8:  for a being Real, x being VECTOR of W holds a * x = (the Mult of V).[a,x]
     proof
       let a be Real;
       let x be VECTOR of W;
         a * x = ((the Mult of V) | [:REAL, the carrier of W:]).[a,x]
       by A1,A4,RLVECT_1:def 4;
       hence thesis by FUNCT_1:72;
     end;
A9:  d1 = 0.W by RLVECT_1:def 2;
A10: for x,y being VECTOR of W holds x .|. y = (the scalar of V).[x,y]
     proof
       let x,y be VECTOR of W;
         x .|. y
        = ((the scalar of V) | [:the carrier of W, the carrier of W:]).[x,y]
        by A1,A5,BHSP_1:def 1;
        hence thesis by FUNCT_1:72;
     end;
       W is RealUnitarySpace-like RealLinearSpace-like
     Abelian add-associative right_zeroed right_complementable
     proof
       set AV = the add of V;
       set MV = the Mult of V;
       set SV = the scalar of V;
       A11: for x,y being Element of W holds x + y = y + x
       proof
         let x,y be Element of W;
         reconsider x1 = x, y1 = y as VECTOR of V by A1,TARSKI:def 3;
         thus x + y = AV.[x1,y1] by A7
                .= y1 + x1 by RLVECT_1:def 3
                .= AV.[y1,x1] by RLVECT_1:def 3
                .= y + x by A7;
       end;
       A12: for x,y,z being VECTOR of W holds (x + y) + z = x + (y + z)
       proof
         let x,y,z be VECTOR of W;
         reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1,TARSKI:def 3;
         thus (x + y) + z = AV.[x + y,z1] by A7
                          .= AV.[AV.[x1,y1],z1] by A7
                          .= AV.[x1 + y1,z1] by RLVECT_1:def 3
                          .= (x1 + y1) + z1 by RLVECT_1:def 3
                          .= x1 + (y1 + z1) by RLVECT_1:def 6
                          .= AV.[x1,y1 + z1] by RLVECT_1:def 3
                          .= AV.[x1,AV.[y1,z1]] by RLVECT_1:def 3
                          .= AV.[x1,y + z] by A7
                          .= x + (y + z) by A7;
       end;
       A13: for x being VECTOR of W holds x + 0.W = x
       proof
         let x be VECTOR of W;
         reconsider y = x, z = 0.W as VECTOR of V by A1,TARSKI:def 3;
         thus x + 0.W = AV.[y,z] by A7
                      .= y + 0.V by A2,A9,RLVECT_1:def 3
                      .= x by RLVECT_1:10;
       end;
       A14: for x being VECTOR of W
        ex y being VECTOR of W st x + y = 0.W
       proof let x be VECTOR of W;
         reconsider x1 = x as VECTOR of V by A1,TARSKI:def 3;
         consider v being VECTOR of V such that
A15:     x1 + v = 0.V by RLVECT_1:def 8;
         v = - x1 by A15,RLVECT_1:def 10
          .= (- 1) * x1 by RLVECT_1:29
          .= MV.[- 1,x1] by RLVECT_1:def 4
          .= (- 1) * x by A8;
         then reconsider y = v as VECTOR of W;
         take y;
         thus x + y = AV.[x1,v] by A7
                   .= 0.W by A2,A9,A15,RLVECT_1:def 3;
       end;
A16:    for a being Real, x,y being VECTOR of W holds
       a * (x + y) = a * x + a * y
       proof
         let a be Real;
         let x,y be VECTOR of W;
         reconsider x1 = x, y1 = y as VECTOR of V by A1,TARSKI:def 3;
         thus a * (x + y) = MV.[a,x + y] by A8
                         .= MV.[a,AV.[x1,y1]] by A7
                         .= MV.[a,x1 + y1] by RLVECT_1:def 3
                         .= a * (x1 + y1) by RLVECT_1:def 4
                         .= a * x1 + a * y1 by RLVECT_1:def 9
                         .= AV.[a * x1,a * y1] by RLVECT_1:def 3
                         .= AV.[MV.[a,x1],a * y1] by RLVECT_1:def 4
                         .= AV.[MV.[a,x1],MV.[a,y1]] by RLVECT_1:def 4
                         .= AV.[MV.[a,x1],a * y] by A8
                         .= AV.[a * x, a * y] by A8
                         .= a * x + a * y by A7;
       end;

A17:    for a,b being Real, x being VECTOR of W holds
       (a + b) * x = a * x + b * x
       proof
         let a,b be Real;
         let x be VECTOR of W;
         reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
         thus (a + b) * x = MV.[a + b,y] by A8
                         .= (a + b) * y by RLVECT_1:def 4
                         .= a * y + b * y by RLVECT_1:def 9
                         .= AV.[a * y,b * y] by RLVECT_1:def 3
                         .= AV.[MV.[a,y],b * y] by RLVECT_1:def 4
                         .= AV.[MV.[a,y],MV.[b,y]] by RLVECT_1:def 4
                         .= AV.[MV.[a,y],b * x] by A8
                         .= AV.[a * x,b * x] by A8
                         .= a * x + b * x by A7;
       end;
A18:    for a,b being Real, x being VECTOR of W holds
       (a * b) * x = a * (b * x)
       proof
         let a,b be Real;
         let x be VECTOR of W;
         reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
         thus (a * b) * x = MV.[(a * b),y] by A8
                         .= (a * b) * y by RLVECT_1:def 4
                         .= a * (b * y) by RLVECT_1:def 9
                         .= MV.[a,b * y] by RLVECT_1:def 4
                         .= MV.[a,MV.[b,y]] by RLVECT_1:def 4
                         .= MV.[a,b * x] by A8
                         .= a * (b * x) by A8;
       end;
       A19: for x being VECTOR of W holds 1 * x = x
       proof
         let x be VECTOR of W;
         reconsider y = x as VECTOR of V by A1,TARSKI:def 3;
         thus 1 * x = MV.[1,y] by A8
                   .= 1 * y by RLVECT_1:def 4
                   .= x by RLVECT_1:def 9;
       end;
         for x,y,z being VECTOR of W, a being Real holds
         (x .|. x = 0 iff x = 0.W) &
         0 <= x .|. x &
         x .|. y = y .|. x &
         (x+y) .|. z = x .|. z + y .|. z &
         (a*x) .|. y = a * ( x .|. y )
       proof
         let x,y,z be VECTOR of W;
         let a be Real;
         reconsider x1 = x as VECTOR of V by A1,TARSKI:def 3;
         reconsider y1 = y as VECTOR of V by A1,TARSKI:def 3;
         reconsider z1 = z as VECTOR of V by A1,TARSKI:def 3;
A20:      x .|. x = 0 implies x = 0.W
         proof
           assume x .|. x = 0;
           then SV.[x1,x1] = 0 by A10;
           then x1 .|. x1 = 0 by BHSP_1:def 1;
           then x1 = 0.V by BHSP_1:def 2;
           hence thesis by A2,RLVECT_1:def 2;
         end;
           x = 0.W implies x .|. x = 0
         proof
           assume x = 0.W;
           then x1 = 0.V by A2,RLVECT_1:def 2;
           then x1 .|. x1 = 0 by BHSP_1:def 2;
           then SV.[x1,x1] = 0 by BHSP_1:def 1;
           hence thesis by A10;
         end;
         hence x .|. x = 0 iff x = 0.W by A20;
         thus 0 <= x .|. x
         proof
             0 <= x1 .|. x1 by BHSP_1:def 2;
           then 0 <= SV.[x1,x1] by BHSP_1:def 1;
           hence thesis by A10;
         end;
         thus x .|. y = y .|. x
         proof
             SV.[x1,y1] = y1 .|. x1 by BHSP_1:def 1;
           then SV.[x1,y1] = SV.[y1,x1] by BHSP_1:def 1;
           then x .|. y = SV.[y1,x1] by A10;
           hence thesis by A10;
         end;
         thus (x+y) .|. z = x .|. z + y .|. z
         proof
A21:        SV.[y1,z1] = y1 .|. z1 by BHSP_1:def 1;
A22:        (x + y) .|. z = SV.[x+y, z] by A10
                        .= SV.[AV.[x1,y1], z] by A7
                        .= SV.[x1+y1, z] by RLVECT_1:def 3
                        .= (x1 + y1) .|. z1 by BHSP_1:def 1
                        .= x1 .|. z1 + y1 .|. z1 by BHSP_1:def 2;
             x .|. z + y .|. z = (SV.[x, z]) + (y .|. z) by A10
                            .= (SV.[x, z]) + (SV.[y, z]) by A10
                            .= x1 .|. z1 + y1 .|. z1 by A21,BHSP_1:def 1;
           hence thesis by A22;
         end;
         thus thesis
         proof
A23:        (a*x) .|. y = SV.[(a*x), y] by A10
                      .= SV.[MV.[a,x1], y] by A8
                      .= SV.[(a*x1), y] by RLVECT_1:def 4
                      .= (a*x1) .|. y1 by BHSP_1:def 1
                      .= a * ( x1 .|. y1 ) by BHSP_1:def 2;
              a * ( x .|. y ) = a * SV.[x,y] by A10
                           .= a * (x1 .|. y1) by BHSP_1:def 1;
            hence thesis by A23;
         end;
       end;
       hence thesis by A11,A12,A13,A14,A16,A17,A18,A19,BHSP_1:def 2,RLVECT_1:
def 5,def 6,def 7,def 8,def 9;
     end;
     hence thesis by A1,A3,A4,A5,A6,Def1;
   end;
   hence thesis;
end;

theorem Th19:
for V being RealUnitarySpace holds V is Subspace of V
proof
   let V be RealUnitarySpace;
   thus the carrier of V c= the carrier of V &
        the Zero of V = the Zero of V;
   thus thesis by FUNCT_2:40;
end;

theorem Th20:
for V,X being strict RealUnitarySpace holds
 V is Subspace of X & X is Subspace of V implies V = X
proof
   let V,X be strict RealUnitarySpace;
   assume
A1:V is Subspace of X & X is Subspace of V;
   set VV = the carrier of V; set VX = the carrier of X;
   set AV = the add of V; set AX = the add of X;
   set MV = the Mult of V; set MX = the Mult of X;
   set SV = the scalar of V; set SX = the scalar of X;
     VV c= VX & VX c= VV by A1,Def1;
then A2:VV = VX by XBOOLE_0:def 10;
A3:the Zero of V = the Zero of X by A1,Def1;
     AV = AX | [:VV,VV:] & AX = AV | [:VX,VX:] by A1,Def1;
then A4:AV = AX by A2,RELAT_1:101;
     MV = MX | [:REAL,VV:] & MX = MV | [:REAL,VX:] by A1,Def1;
then A5:MV = MX by A2,RELAT_1:101;
     SV = SX | [:VV,VV:] & SX = SV | [:VX,VX:] by A1,Def1;
   hence thesis by A2,A3,A4,A5,RELAT_1:101;
end;

theorem Th21:
for V,X,Y being RealUnitarySpace st
 V is Subspace of X & X is Subspace of Y holds V is Subspace of Y
proof
   let V,X,Y be RealUnitarySpace;
   assume
A1:V is Subspace of X & X is Subspace of Y;
   thus the carrier of V c= the carrier of Y
   proof
       the carrier of V c= the carrier of X &
     the carrier of X c= the carrier of Y by A1,Def1;
     hence thesis by XBOOLE_1:1;
   end;
   thus the Zero of V = the Zero of Y
   proof
       the Zero of V = the Zero of X & the Zero of X = the Zero of Y by A1,Def1
;
     hence thesis;
   end;
   thus the add of V = (the add of Y) | [:the carrier of V, the carrier of V:]
   proof
     set AV = the add of V; set VV = the carrier of V;
     set AX = the add of X; set VX = the carrier of X;
     set AY = the add of Y;
       AV = AX | [:VV,VV:] & AX = AY | [:VX,VX:] & VV c= VX by A1,Def1;
     then AV = (AY | [:VX,VX:]) | [:VV,VV:] & [:VV,VV:] c= [:VX,VX:]
                                                           by ZFMISC_1:119;
     hence thesis by FUNCT_1:82;
   end;
   thus the Mult of V = (the Mult of Y) | [:REAL, the carrier of V:]
   proof
     set MV = the Mult of V; set VV = the carrier of V;
     set MX = the Mult of X; set VX = the carrier of X;
     set MY = the Mult of Y;
       MV = MX | [:REAL,VV:] & MX = MY | [:REAL,VX:] & VV c= VX by A1,Def1;
     then MV = (MY | [:REAL,VX:]) | [:REAL,VV:] & [:REAL,VV:] c= [:REAL,VX:]
                                                              by ZFMISC_1:118;
     hence thesis by FUNCT_1:82;
   end;
     set SV = the scalar of V; set VV = the carrier of V;
     set SX = the scalar of X; set VX = the carrier of X;
     set SY = the scalar of Y;
       SV = SX | [:VV,VV:] & SX = SY | [:VX,VX:] & VV c= VX by A1,Def1;
     then SV = (SY | [:VX,VX:]) | [:VV,VV:] & [:VV,VV:] c= [:VX,VX:]
                                                              by ZFMISC_1:119;
   hence thesis by FUNCT_1:82;
end;

theorem Th22:
for V being RealUnitarySpace, W1,W2 being Subspace of V st
 the carrier of W1 c= the carrier of W2 holds W1 is Subspace of W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be Subspace of V;
   assume
A1:the carrier of W1 c= the carrier of W2;
   set VW1 = the carrier of W1; set VW2 = the carrier of W2;
   set AV = the add of V; set MV = the Mult of V;
   set SV = the scalar of V;
     the Zero of W1 = the Zero of V & the Zero of W2 = the Zero of V by Def1;
   hence the carrier of W1 c= the carrier of W2 &
         the Zero of W1 = the Zero of W2 by A1;
   thus the add of W1 =
        (the add of W2) | [:the carrier of W1,the carrier of W1:]
   proof
       the add of W1 = AV | [:VW1,VW1:] & the add of W2 = AV | [:VW2,VW2:] &
     [:VW1,VW1:] c= [:VW2,VW2:] by A1,Def1,ZFMISC_1:119;
     hence thesis by FUNCT_1:82;
   end;
   thus the Mult of W1 =
        (the Mult of W2) | [:REAL, the carrier of W1:]
   proof
       the Mult of W1 = MV | [:REAL,VW1:] & the Mult of W2 = MV | [:REAL,VW2:]
&
     [:REAL,VW1:] c= [:REAL,VW2:] by A1,Def1,ZFMISC_1:118;
     hence thesis by FUNCT_1:82;
   end;
     the scalar of W1 = SV | [:VW1,VW1:] & the scalar of W2 = SV | [:VW2,VW2:]
&
   [:VW1,VW1:] c= [:VW2,VW2:] by A1,Def1,ZFMISC_1:119;
   hence thesis by FUNCT_1:82;
end;

theorem
  for V being RealUnitarySpace, W1,W2 being Subspace of V st
 (for v being VECTOR of V st v in W1 holds v in W2) holds
  W1 is Subspace of W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be Subspace of V;
   assume
A1:for v being VECTOR of V st v in W1 holds v in W2;
     the carrier of W1 c= the carrier of W2
   proof
     let x be set;
     assume
A2:  x in the carrier of W1;
       the carrier of W1 c= the carrier of V by Def1;
     then reconsider v = x as VECTOR of V by A2;
       v in W1 by A2,RLVECT_1:def 1;
     then v in W2 by A1;
     hence thesis by RLVECT_1:def 1;
   end;
   hence thesis by Th22;
end;

definition let V be RealUnitarySpace;
 cluster strict Subspace of V;
existence
proof
     the carrier of V is Subset of V iff
     the carrier of V c= the carrier of V;
   then reconsider V1 = the carrier of V as Subset of V;
     the Zero of V = 0.V &
   the add of V = (the add of V) | [:V1,V1:] &
   the Mult of V = (the Mult of V) | [:REAL,V1:] &
   the scalar of V = (the scalar of V) | [:V1, V1:]
   by FUNCT_2:40,RLVECT_1:def 2;
   then UNITSTR(#the carrier of V,the Zero of V,the add of V,the Mult of V,
   the scalar of V #) is Subspace of V by Th18;
   hence thesis;
end;
end;

theorem Th24:
for V being RealUnitarySpace, W1,W2 being strict Subspace of V st
 the carrier of W1 = the carrier of W2 holds W1 = W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be strict Subspace of V;
   assume
     the carrier of W1 = the carrier of W2;
   then W1 is Subspace of W2 & W2 is Subspace of W1 by Th22;
   hence thesis by Th20;
end;

theorem Th25:
for V being RealUnitarySpace, W1,W2 being strict Subspace of V st
 (for v being VECTOR of V holds v in W1 iff v in W2) holds W1 = W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be strict Subspace of V;
   assume
A1:for v being VECTOR of V holds v in W1 iff v in W2;
     for x being set holds x in the carrier of W1 iff x in the carrier of W2
   proof
     let x be set;
     thus x in the carrier of W1 implies x in the carrier of W2
     proof
       assume
A2:    x in the carrier of W1;
         the carrier of W1 c= the carrier of V by Def1;
       then reconsider v = x as VECTOR of V by A2;
         v in W1 by A2,RLVECT_1:def 1;
       then v in W2 by A1;
       hence thesis by RLVECT_1:def 1;
     end;
     assume
A3:  x in the carrier of W2;
       the carrier of W2 c= the carrier of V by Def1;
     then reconsider v = x as VECTOR of V by A3;
       v in W2 by A3,RLVECT_1:def 1;
     then v in W1 by A1;
     hence thesis by RLVECT_1:def 1;
   end;
   then the carrier of W1 = the carrier of W2 by TARSKI:2;
   hence thesis by Th24;
end;


theorem
  for V being strict RealUnitarySpace, W being strict Subspace of V st
 the carrier of W = the carrier of V holds W = V
proof
   let V be strict RealUnitarySpace;
   let W be strict Subspace of V;
   assume
A1:the carrier of W = the carrier of V;
     V is Subspace of V by Th19;
   hence thesis by A1,Th24;
end;


theorem
  for V being strict RealUnitarySpace, W being strict Subspace of V st
 (for v being VECTOR of V holds v in W iff v in V) holds W = V
proof
   let V be strict RealUnitarySpace;
   let W be strict Subspace of V;
   assume
A1:for v being VECTOR of V holds v in W iff v in V;
     V is Subspace of V by Th19;
   hence thesis by A1,Th25;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
 V1 being Subset of V st
 the carrier of W = V1 holds V1 is lineary-closed by Lm1;


theorem Th29:
for V being RealUnitarySpace, W being Subspace of V,
 V1 being Subset of V st
  V1 <> {} & V1 is lineary-closed holds
   (ex W being strict Subspace of V st V1 = the carrier of W)
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let V1 be Subset of V;
   assume that
A1:V1 <> {} and
A2:V1 is lineary-closed;
   reconsider D = V1 as non empty set by A1;
   reconsider d1 = 0.V as Element of D by A2,RLSUB_1:4;
   set A = (the add of V) | [:V1,V1:];
   set M = (the Mult of V) | [:REAL,V1:];
   set S = (the scalar of V) | [:V1,V1:];
   set VV = the carrier of V;
     dom(the add of V) = [:VV,VV:] by FUNCT_2:def 1;
   then dom A = [:VV,VV:] /\ [:V1,V1:] & [:V1,V1:] c= [:VV,VV:] by RELAT_1:90;
then A3:dom A = [:D,D:] by XBOOLE_1:28;
     dom(the Mult of V) = [:REAL,VV:] by FUNCT_2:def 1;
   then dom M = [:REAL,VV:] /\ [:REAL,V1:] & [:REAL,V1:] c= [:REAL,VV:]
                                               by RELAT_1:90,ZFMISC_1:118;
then A4:dom M = [:REAL,D:] by XBOOLE_1:28;
A5:D = rng A
   proof
       now let y be set;
     thus y in D implies ex x being set st x in dom A & y = A.x
     proof
       assume
A6:    y in D;
       then reconsider v1 = y, v0 = d1 as Element of VV;

A7:    [d1,y] in [:D,D:] & [d1,y] in [:VV,VV:] by A6,ZFMISC_1:106;
       then A.[d1,y] = (the add of V).[d1,y] by FUNCT_1:72
               .= v0 + v1 by RLVECT_1:def 3
               .= y by RLVECT_1:10;
       hence thesis by A3,A7;
     end;
     given x being set such that
A8:  x in dom A and
A9:  y = A.x;
       consider x1,x2 being set such that
A10:   x1 in D & x2 in D and
A11:   x = [x1,x2] by A3,A8,ZFMISC_1:def 2;
A12:   [x1,x2] in [:VV,VV:] & [x1,x2] in [:V1,V1:] by A10,ZFMISC_1:106;
       reconsider v1 = x1, v2 = x2 as Element of VV by A10;

         y = (the add of V).[x1,x2] by A9,A11,A12,FUNCT_1:72
        .= v1 + v2 by RLVECT_1:def 3;
       hence y in D by A2,A10,RLSUB_1:def 1;
     end;
     hence thesis by FUNCT_1:def 5;
   end;

A13:D = rng M
   proof
       now let y be set;
     thus y in D implies ex x being set st x in dom M & y = M.x
     proof
       assume
A14:   y in D;
       then reconsider v1 = y as Element of VV;
A15:   [1,y] in [:REAL,D:] & [1,y] in [:REAL,VV:] by A14,ZFMISC_1:106;
       then M.[1,y] = (the Mult of V).[1,y] by FUNCT_1:72
              .= 1 * v1 by RLVECT_1:def 4
              .= y by RLVECT_1:def 9;
       hence thesis by A4,A15;
     end;
     given x being set such that
A16: x in dom M and
A17: y = M.x;
       consider x1,x2 being set such that
A18:   x1 in REAL and
A19:   x2 in D and
A20:   x = [x1,x2] by A4,A16,ZFMISC_1:def 2;
A21:   [x1,x2] in [:REAL,VV:] & [x1,x2] in [:REAL,V1:] by A18,A19,ZFMISC_1:106;
       reconsider v2 = x2 as Element of VV by A19;

       reconsider xx1 = x1 as Real by A18;
         y = (the Mult of V).[x1,x2] by A17,A20,A21,FUNCT_1:72
        .= xx1 * v2 by RLVECT_1:def 4;
       hence y in D by A2,A19,RLSUB_1:def 1;
     end;
     hence thesis by FUNCT_1:def 5;
   end;
   reconsider A as Function of [:D,D:],D by A3,A5,FUNCT_2:def 1,RELSET_1:11;
   reconsider M as Function of [:REAL,D:],D
                                           by A4,A13,FUNCT_2:def 1,RELSET_1:11;
   reconsider S as Function of [:D,D:],REAL by FUNCT_2:38;
   set W = UNITSTR (# D,d1,A,M,S #);
         W is Subspace of V & the carrier of W = D by Th18;
   hence thesis;
end;

begin
:: Definition of Zero Subspace and Improper Subspace of Real Unitary Space

definition
let V being RealUnitarySpace;
 func (0).V -> strict Subspace of V means
:Def2:
 the carrier of it = {0.V};
correctness
proof
     {0.V} is lineary-closed & {0.V} <> {} by RLSUB_1:7;
   hence thesis by Th24,Th29;
   end;
end;

definition
let V being RealUnitarySpace;
 func (Omega).V -> strict Subspace of V equals
:Def3:
 the UNITSTR of V;
coherence
proof
   set W = the UNITSTR of V;
     W is Abelian add-associative right_zeroed right_complementable
           RealLinearSpace-like RealUnitarySpace-like
   proof
A1:  0.W = the Zero of W by RLVECT_1:def 2 .= 0.V by RLVECT_1:def 2;
A2:  now
       let a be Real;
       let v,w be VECTOR of W, v',w' be VECTOR of V such that
A3:    v=v' & w=w';
       thus v+w = (the add of W).[v,w] by RLVECT_1:def 3
               .= v'+w' by A3,RLVECT_1:def 3;
       thus a*v = (the Mult of W).[a,v] by RLVECT_1:def 4
               .= a*v' by A3,RLVECT_1:def 4;
       thus v .|. w = (the scalar of W).[v,w] by BHSP_1:def 1
                   .= v' .|. w' by A3,BHSP_1:def 1;
     end;
     thus for v,w being VECTOR of W holds v + w = w + v
     proof
       let v,w be VECTOR of W;
       reconsider v'=v,w'=w as VECTOR of V;
       thus v + w = w' + v' by A2 .= w + v by A2;
     end;
     thus for u,v,w being VECTOR of W holds (u + v) + w = u + (v + w)
     proof
       let u,v,w be VECTOR of W;
        reconsider u'=u,v'=v,w'=w as VECTOR of V;
A4:     v + w = v' + w' & u + v = u' + v' by A2;
        hence (u + v) + w = (u' + v') + w' by A2
                         .= u' + (v' + w') by RLVECT_1:def 6
                         .= u + (v + w) by A2,A4;
     end;
     thus for v being VECTOR of W holds v + 0.W = v
     proof
       let v be VECTOR of W;
       reconsider v'=v as VECTOR of V;
       thus v + 0.W = v' + 0.V by A1,A2 .= v by RLVECT_1:10;
     end;
     thus for v being VECTOR of W ex w being VECTOR of W st v + w = 0.W
     proof
       let v be VECTOR of W;
       reconsider v'=v as VECTOR of V;
       consider w' being VECTOR of V such that
A5:    v' + w' = 0.V by RLVECT_1:def 8;
       reconsider w=w' as VECTOR of W;
       take w;
       thus v + w = 0.W by A1,A2,A5;
     end;
     thus for a be Real ,v,w being VECTOR of W holds
           a * (v + w) = a * v + a * w
     proof
       let a be Real; let v,w be VECTOR of W;
       reconsider v'=v,w'=w as VECTOR of V;
A6:    v + w = v' + w' & a * v = a * v' & a * w = a * w' by A2;
       hence a * (v + w) = a * (v' + w') by A2
                        .= a * v' + a * w' by RLVECT_1:def 9
                        .= a * v + a * w by A2,A6;
     end;
     thus for a,b be Real, v being VECTOR of W holds
           (a + b) * v = a * v + b * v
     proof
       let a,b be Real;
       let v be VECTOR of W;
       reconsider v'=v as VECTOR of V;
A7:    a * v = a * v' & b * v = b * v' by A2;
       thus (a + b) * v = (a + b) * v' by A2
                       .= a * v' + b * v' by RLVECT_1:def 9
                       .= a * v + b * v by A2,A7;
     end;
     thus for a,b be Real, v being VECTOR of W holds
           (a * b) * v = a * (b * v)
     proof
       let a,b be Real;
       let v be VECTOR of W;
       reconsider v'=v as VECTOR of V;
A8:    b * v = b * v' by A2;
       thus (a * b) * v = (a * b) * v' by A2
                       .= a * (b * v') by RLVECT_1:def 9
                       .= a * (b * v) by A2,A8;
     end;
     thus for v being VECTOR of W holds 1 * v = v
     proof
       let v be VECTOR of W;
       reconsider v'=v as VECTOR of V;
       thus 1 * v = 1 * v' by A2 .= v by RLVECT_1:def 9;
     end;
     thus W is RealUnitarySpace-like
     proof
         for x , y , z being VECTOR of W , a being Real holds
           ( x .|. x = 0 iff x = 0.W ) &
           0 <= x .|. x &
           x .|. y = y .|. x &
           (x+y) .|. z = x .|. z + y .|. z &
           (a*x) .|. y = a * ( x .|. y )
       proof
          let x,y,z be VECTOR of W;
          let a be Real;
          reconsider x' = x as VECTOR of V;
          reconsider y' = y as VECTOR of V;
          reconsider z' = z as VECTOR of V;
          thus x .|. x = 0 iff x = 0.W
          proof
              x' .|. x' = x .|. x by A2;
            hence thesis by A1,BHSP_1:def 2;
          end;
          thus 0 <= x .|. x
          proof
              x' .|. x' = x .|. x by A2;
            hence thesis by BHSP_1:def 2;
          end;
          thus x .|. y = y .|. x
          proof
              x' .|. y' = x .|. y & y' .|. x' = y .|. x by A2;
            hence thesis;
          end;
          thus (x+y) .|. z = x .|. z + y .|. z
          proof
A9:        x'+y' = x+y & x' .|. z' = x .|. z & y' .|. z' = y .|. z by A2;
            then (x+y) .|. z = (x'+y') .|. z' by A2
                       .= x' .|. z' + y' .|. z' by BHSP_1:def 2;
            hence thesis by A9;
          end;
          thus (a*x) .|. y = a * ( x .|. y )
          proof
              a*x' = a*x & x' .|. y' = x .|. y by A2;
            then (a*x) .|. y = (a*x') .|. y' by A2
                       .= a * (x' .|. y') by BHSP_1:def 2;
            hence thesis by A2;
          end;
       end;
       hence thesis by BHSP_1:def 2;
     end;

   end;
   then reconsider W as RealUnitarySpace;
     W is Subspace of V
   proof
     thus the carrier of W c= the carrier of V &
          the Zero of W = the Zero of V;
     thus thesis by FUNCT_2:40;
   end;
   hence thesis;
end;
end;

begin :: Theorems of Zero Subspace and Improper Subspace

theorem Th30:
for V being RealUnitarySpace, W being Subspace of V holds
 (0).W = (0).V
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
     the carrier of (0).W = {0.W} & the carrier of (0).V = {0.V} by Def2;
   then the carrier of (0).W = the carrier of (0).V & (0).W is Subspace of V
     by Th4,Th21;
   hence thesis by Th24;
end;

theorem Th31:
for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 (0).W1 = (0).W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be Subspace of V;
     (0).W1 = (0).V & (0).W2 = (0).V by Th30;
   hence thesis;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V holds
 (0).W is Subspace of V by Th21;


theorem
  for V being RealUnitarySpace, W being Subspace of V holds
 (0).V is Subspace of W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
     the carrier of (0).V = {0.V} by Def2
                       .= {0.W} by Th4
                       .= {the Zero of W} by RLVECT_1:def 2;
   hence thesis by Th22;
end;

theorem
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 (0).W1 is Subspace of W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be Subspace of V;
     (0).W1 = (0).W2 & (0).W2 is Subspace of W2 by Th31;
   hence thesis;
end;

theorem
  for V being strict RealUnitarySpace holds V is Subspace of (Omega).V
proof
   let V be strict RealUnitarySpace;
     V is Subspace of V by Th19;
   hence thesis by Def3;
end;

begin :: The Cosets of Subspace of Real Unitary Space

definition
let V be RealUnitarySpace, v be VECTOR of V, W be Subspace of V;
func v + W -> Subset of V equals
:Def4:
  {v + u where u is VECTOR of V : u in W};
coherence
proof
  defpred P[set] means ex u being VECTOR of V st $1 = v + u & u in W;
   consider X being set such that
A1:for x being set holds x in X iff x in the carrier of V & P[x]
       from Separation;
     X c= the carrier of V
   proof
     let x be set;
     assume x in X;
     hence x in the carrier of V by A1;
   end;
   then reconsider X as Subset of V;
   set Y = {v + u where u is VECTOR of V : u in W};
     X = Y
   proof
     thus X c= Y
     proof
       let x be set;
       assume x in X;
       then ex u being VECTOR of V st x = v + u & u in W by A1;
       hence thesis;
     end;
     thus Y c= X
     proof
       let x be set;
       assume x in Y;
       then ex u being VECTOR of V st x = v + u & u in W;
       hence thesis by A1;
     end;
   end;
   hence thesis;
end;
end;

Lm2:
for V being RealUnitarySpace, W being Subspace of V holds
0.V + W = the carrier of W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   set A = {0.V + u where u is VECTOR of V : u in W};
A1:0.V + W = A by Def4;
A2:A c= the carrier of W
   proof
     let x be set;
     assume x in A;
     then consider u being VECTOR of V such that
A3:  x = 0.V + u and
A4:  u in W;
       x = u by A3,RLVECT_1:10;
     hence thesis by A4,RLVECT_1:def 1;
   end;
     the carrier of W c= A
   proof
     let x be set;
     assume x in the carrier of W;
then A5:  x in W by RLVECT_1:def 1;
     then x in V by Th2;
     then reconsider y = x as Element of V by RLVECT_1:def 1;

       0.V + y = x by RLVECT_1:10;
     hence thesis by A5;
   end;
   hence thesis by A1,A2,XBOOLE_0:def 10;
end;

definition
let V be RealUnitarySpace; let W be Subspace of V;
mode Coset of W -> Subset of V means
:Def5:
   ex v be VECTOR of V st it = v + W;
existence
proof
   reconsider VW = the carrier of W as Subset of V by Def1;
   take VW; take 0.V;
   thus thesis by Lm2;
end;
end;

begin :: Theorems of the Cosets

theorem Th36:
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds
 0.V in v + W iff v in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   set A = {v + u where u is VECTOR of V : u in W};
   thus 0.V in v + W implies v in W
   proof
     assume 0.V in v + W;
     then 0.V in A by Def4;
     then consider u being VECTOR of V such that
A1:  0.V = v + u and
A2:  u in W;
     v = - u by A1,RLVECT_1:def 10;
   hence thesis by A2,Th16;
   end;
   assume v in W;
then A3:- v in W by Th16;
     0.V = v - v by RLVECT_1:28
      .= v + (- v) by RLVECT_1:def 11;
   then 0.V in A by A3;
   hence thesis by Def4;
end;

theorem Th37:
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds
 v in v + W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
     v + 0.V = v & 0.V in W by Th11,RLVECT_1:10;
  then v in {v + u where u is VECTOR of V : u in W};
   hence thesis by Def4;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V holds
 0.V + W = the carrier of W by Lm2;

theorem Th39:
for V being RealUnitarySpace, v being VECTOR of V holds
 v + (0).V = {v}
proof
   let V be RealUnitarySpace;
   let v be VECTOR of V;
   set A = {v + u where u is VECTOR of V : u in (0).V};
   thus v + (0).V c= {v}
   proof let x be set;
     assume x in v + (0).V;
     then x in A by Def4;
     then consider u being VECTOR of V such that
A1:  x = v + u and
A2:  u in (0).V;
       the carrier of (0).V = {0.V} & u in the carrier of (0).V
                                           by A2,Def2,RLVECT_1:def 1;
     then u = 0.V by TARSKI:def 1;
     then x = v by A1,RLVECT_1:10;
     hence thesis by TARSKI:def 1;
   end;
   let x be set;
   assume x in {v};
then A3:x = v by TARSKI:def 1;
     0.V in (0).V & v = v + 0.V by Th11,RLVECT_1:10;
   then x in A by A3;
   hence thesis by Def4;
end;

Lm3:
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds
v in W iff v + W = the carrier of W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   set A = {v + u where u is VECTOR of V: u in W};
   thus v in W implies v + W = the carrier of W
   proof
     assume
A1:  v in W;
     thus v + W c= the carrier of W
     proof
       let x be set;
       assume x in v + W;
       then x in A by Def4;
       then consider u being VECTOR of V such that
A2:    x = v + u and
A3:    u in W;
         v + u in W by A1,A3,Th14;
       hence thesis by A2,RLVECT_1:def 1;
     end;
     let x be set;
     assume x in the carrier of W;
     then reconsider y = x, z = v as Element of W
                                              by A1,RLVECT_1:def 1;

     reconsider y1 = y, z1 = z as VECTOR of V by Th3;
A4:  y - z in W by RLVECT_1:def 1;
A5:  z + (y - z) = (y + z) - z by RLVECT_1:42
                .= y + (z - z) by RLVECT_1:42
                .= y + 0.W by RLVECT_1:28
                .= x by RLVECT_1:10;
A6:  y - z = y1 - z1 by Th10;
A7:  y1 - z1 in W by A4,Th10;
       z1 + (y1 - z1) = x by A5,A6,Th6;
     then x in A by A7;
     hence thesis by Def4;
   end;
   assume
A8:v + W = the carrier of W;
   assume
A9:not v in W;
     0.V in W & v + 0.V = v by Th11,RLVECT_1:10;
   then v in {v + u where u is VECTOR of V : u in W};
   then v in the carrier of W by A8,Def4;
   hence thesis by A9,RLVECT_1:def 1;
 end;

theorem Th40:
for V being RealUnitarySpace, v being VECTOR of V holds
 v + (Omega).V = the carrier of V
proof
   let V be RealUnitarySpace;
   let v be VECTOR of V;
A1:the carrier of (Omega).V = the carrier of the UNITSTR of V by Def3
     .= the carrier of V;
   then v in (Omega).V by RLVECT_1:def 1;
   hence thesis by A1,Lm3;
end;

theorem Th41:
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds
 0.V in v + W iff v + W = the carrier of W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
     (0.V in v + W iff v in W) & (v in W iff v + W = the carrier of W)
     by Lm3,Th36;
   hence thesis;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V
holds
 v in W iff v + W = the carrier of W by Lm3;

theorem Th43:
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V,
 a being Real st v in W holds (a * v) + W = the carrier of W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   let a be Real;
   set A = {a * v + u where u is VECTOR of V : u in W};
   assume
A1:v in W;
   thus (a * v) + W c= the carrier of W
   proof
     let x be set;
     assume x in (a * v) + W;
     then x in A by Def4;
     then consider u being VECTOR of V such that
A2:  x = a * v + u and
A3:  u in W;
       a * v in W by A1,Th15;
     then a * v + u in W by A3,Th14;
     hence thesis by A2,RLVECT_1:def 1;
   end;
   let x be set;
   assume
A4:x in the carrier of W;
     the carrier of W c= the carrier of V & v in V by Def1,RLVECT_1:3;
   then reconsider y = x as Element of V by A4;

     a * v in W & x in W by A1,A4,Th15,RLVECT_1:def 1;
then A5:y - a * v in W by Th17;
     a * v + (y - a * v) = (y + a * v) - a * v by RLVECT_1:42
                      .= y + (a * v - a * v) by RLVECT_1:42
                      .= y + 0.V by RLVECT_1:28
                      .= x by RLVECT_1:10;
   then x in A by A5;
   hence thesis by Def4;
end;

theorem Th44:
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V,
 a being Real st a <> 0 & (a * v) + W = the carrier of W holds v in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   let a be Real;
   assume that
A1:a <> 0 and
A2:(a * v) + W = the carrier of W;
   assume not v in W;
   then not 1 * v in W by RLVECT_1:def 9;
   then not (a" * a) * v in W by A1,XCMPLX_0:def 7;
   then not a" * (a * v) in W by RLVECT_1:def 9;
then A3:not a * v in W by Th15;
     0.V in W & a * v + 0.V = a * v by Th11,RLVECT_1:10;
   then a * v in {a * v + u where u is VECTOR of V : u in W};
   then a * v in the carrier of W by A2,Def4;
   hence contradiction by A3,RLVECT_1:def 1;
end;

theorem Th45:
for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V holds
 v in W iff - v + W = the carrier of W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
     (v in W iff ((- 1) * v) + W = the carrier of W) & (- 1) * v = - v
                                                 by Th43,Th44,RLVECT_1:29;
   hence thesis;
end;

theorem Th46:
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V holds u in W iff v + W = (v + u) + W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   set A = {v + v1 where v1 is VECTOR of V : v1 in W};
   set B = {(v + u) + v2 where v2 is VECTOR of V : v2 in W};
   thus u in W implies v + W = (v + u) + W
   proof
     assume
A1:  u in W;
     thus v + W c= (v + u) + W
     proof
       let x be set;
       assume x in v + W;
       then x in A by Def4;
       then consider v1 being VECTOR of V such that
A2:    x = v + v1 and
A3:    v1 in W;
A4:    v1 - u in W by A1,A3,Th17;
         (v + u) + (v1 - u) = v + (u + (v1 - u)) by RLVECT_1:def 6
                         .= v + ((v1 + u) - u) by RLVECT_1:42
                         .= v + (v1 + (u - u)) by RLVECT_1:42
                         .= v + (v1 + 0.V) by RLVECT_1:28
                         .= x by A2,RLVECT_1:10;
       then x in B by A4;
       hence thesis by Def4;
     end;
     let x be set;
     assume x in (v + u) + W;
     then x in B by Def4;
     then consider v2 being VECTOR of V such that
A5:  x = (v + u) + v2 and
A6:  v2 in W;
A7:  u + v2 in W by A1,A6,Th14;
       x = v + (u + v2) by A5,RLVECT_1:def 6;
     then x in A by A7;
     hence thesis by Def4;
   end;
   assume
A8:v + W = (v + u) + W;
     0.V in W & v + 0.V = v by Th11,RLVECT_1:10;
   then v in A;
   then v in (v + u) + W by A8,Def4;
   then v in B by Def4;
   then consider u1 being VECTOR of V such that
A9:v = (v + u) + u1 and
A10:u1 in W;
     v = v + 0.V & v = v + (u + u1) by A9,RLVECT_1:10,def 6;
then A11:u + u1 = 0.V by RLVECT_1:21;
   u = - u1 by A11,RLVECT_1:def 10;
   hence thesis by A10,Th16;
  end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V holds u in W iff v + W = (v - u) + W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
A1:(- u in W iff v + W = (v + (- u)) + W) & v + (- u) = v - u
                                             by Th46,RLVECT_1:def 11;
     - u in W implies u in W
   proof
     assume - u in W;
     then - (- u) in W by Th16;
     hence thesis by RLVECT_1:30;
   end;
   hence thesis by A1,Th16;
end;

theorem Th48:
for V being RealUnitarySpace, W being Subspace of V,
u,v being VECTOR of V holds v in u + W iff u + W = v + W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   set A = {u + v1 where v1 is VECTOR of V: v1 in W};
   set B = {v + v2 where v2 is VECTOR of V: v2 in W};
   thus v in u + W implies u + W = v + W
   proof
     assume v in u + W;
     then v in A by Def4;
     then consider z being VECTOR of V such that
A1:  v = u + z and
A2:  z in W;
     thus u + W c= v + W
     proof
       let x be set;
       assume x in u + W;
       then x in A by Def4;
       then consider v1 being VECTOR of V such that
A3:    x = u + v1 and
A4:    v1 in W;
A5:    v1 - z in W by A2,A4,Th17;
         v - z = u + (z - z) by A1,RLVECT_1:42
            .= u + 0.V by RLVECT_1:28
            .= u by RLVECT_1:10;
       then x = (v + (- z)) + v1 by A3,RLVECT_1:def 11
        .= v + (v1 + (- z)) by RLVECT_1:def 6
        .= v + (v1 - z) by RLVECT_1:def 11;
       then x in B by A5;
       hence thesis by Def4;
     end;
     let x be set;
     assume x in v + W;
     then x in B by Def4;
     then consider v2 being VECTOR of V such that
A6:  x = v + v2 and
A7:  v2 in W;
A8:  z + v2 in W by A2,A7,Th14;
       x = u + (z + v2) by A1,A6,RLVECT_1:def 6;
     then x in A by A8;
     hence thesis by Def4;
   end;
   thus thesis by Th37;
end;

theorem Th49:
for V being RealUnitarySpace, W being Subspace of V,
 v being VECTOR of V holds v + W = (- v) + W iff v in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   thus v + W = (- v) + W implies v in W
   proof
     assume v + W = (- v) + W;
     then v in (- v) + W by Th37;
     then v in {- v + u where u is VECTOR of V : u in W} by Def4;
     then consider u being VECTOR of V such that
A1:  v = - v + u and
A2:  u in W;
       0.V = v - (- v + u) by A1,RLVECT_1:28
        .= (v - (- v)) - u by RLVECT_1:41
        .= (v + (- (- v))) - u by RLVECT_1:def 11
        .= (v + v) - u by RLVECT_1:30
        .= (1 * v + v) - u by RLVECT_1:def 9
        .= (1 * v + 1 * v) - u by RLVECT_1:def 9
        .= ((1 + 1) * v) - u by RLVECT_1:def 9
        .= 2 * v - u;
     then 2" * (2 * v) = 2" * u by RLVECT_1:35;
     then (2" * 2) * v = 2" * u & 0 <> 2 by RLVECT_1:def 9;
     then v = 2" * u by RLVECT_1:def 9;
     hence thesis by A2,Th15;
   end;
   assume v in W;
   then v + W = the carrier of W & (- v) + W = the carrier of W by Lm3,Th45;
   hence thesis;
end;

theorem Th50:
for V being RealUnitarySpace, W being Subspace of V,
 u,v1,v2 being VECTOR of V st
  u in v1 + W & u in v2 + W holds v1 + W = v2 + W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v1,v2 be VECTOR of V;
   assume that
A1:u in v1 + W and
A2:u in v2 + W;
   set A = {v1 + u1 where u1 is VECTOR of V : u1 in W};
   set B = {v2 + u2 where u2 is VECTOR of V : u2 in W};
     u in A by A1,Def4;
   then consider x1 being VECTOR of V such that
A3:u = v1 + x1 and
A4:x1 in W;
     u in B by A2,Def4;
   then consider x2 being VECTOR of V such that
A5:u = v2 + x2 and
A6:x2 in W;
   thus v1 + W c= v2 + W
   proof
     let x be set;
     assume x in v1 + W;
     then x in A by Def4;
     then consider u1 being VECTOR of V such that
A7:  x = v1 + u1 and
A8:  u1 in W;
       u - x1 = v1 + (x1 - x1) by A3,RLVECT_1:42
           .= v1 + 0.V by RLVECT_1:28
           .= v1 by RLVECT_1:10;
then A9:  x = (v2 + (x2 - x1)) + u1 by A5,A7,RLVECT_1:42
      .= v2 + ((x2 - x1) + u1) by RLVECT_1:def 6;
       x2 - x1 in W by A4,A6,Th17;
     then (x2 - x1) + u1 in W by A8,Th14;
     then x in B by A9;
     hence thesis by Def4;
   end;
   let x be set;
   assume x in v2 + W;
   then x in B by Def4;
   then consider u1 being VECTOR of V such that
A10:x = v2 + u1 and
A11:u1 in W;
     u - x2 = v2 + (x2 - x2) by A5,RLVECT_1:42
         .= v2 + 0.V by RLVECT_1:28
         .= v2 by RLVECT_1:10;
then A12:x = (v1 + (x1 - x2)) + u1 by A3,A10,RLVECT_1:42
     .= v1 + ((x1 - x2) + u1) by RLVECT_1:def 6;
     x1 - x2 in W by A4,A6,Th17;
   then (x1 - x2) + u1 in W by A11,Th14;
   then x in A by A12;
   hence thesis by Def4;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
 u,v being VECTOR of V st u in v + W & u in (- v) + W holds v in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   assume u in v + W & u in (- v) + W;
   then v + W = (- v) + W by Th50;
   hence thesis by Th49;
end;

theorem Th52:
for V being RealUnitarySpace, W being Subspace of V,
 v being VECTOR of V, a being Real st a <> 1 & a * v in v + W holds v in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   let a be Real;
   assume that
A1:a <> 1 and
A2:a * v in v + W;
A3:now assume a - 1 = 0;
     then (- 1) + a = 0 by XCMPLX_0:def 8;
     then a = - (- 1) by XCMPLX_0:def 6;
     hence contradiction by A1;
   end;
     a * v in {v + u where u is VECTOR of V : u in W} by A2,Def4;
   then consider u being VECTOR of V such that
A4:a * v = v + u and
A5:u in W;
     u = u + 0.V by RLVECT_1:10
    .= u + (v - v) by RLVECT_1:28
    .= a * v - v by A4,RLVECT_1:42
    .= a * v - 1 * v by RLVECT_1:def 9
    .= (a - 1) * v by RLVECT_1:49;
   then (a - 1)" * u = ((a - 1)" * (a - 1)) * v & a - 1 <> 0
                                                 by A3,RLVECT_1:def 9;
   then 1 * v = (a - 1)" * u by XCMPLX_0:def 7;
   then v = (a - 1)" * u by RLVECT_1:def 9;
   hence thesis by A5,Th15;
end;

theorem Th53:
for V being RealUnitarySpace, W being Subspace of V,
 v being VECTOR of V, a being Real st v in W holds a * v in v + W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
   let a be Real;
   assume
A1:v in W;
A2:a * v = (a - (1 - 1)) * v
        .= ((a - 1) + 1) * v by XCMPLX_1:37
        .= (a - 1) * v + 1 * v by RLVECT_1:def 9
        .= v + (a - 1) * v by RLVECT_1:def 9;
     (a - 1) * v in W by A1,Th15;
   then a * v in {v + u where u is VECTOR of V : u in W} by A2;
   hence thesis by Def4;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
 v being VECTOR of V holds - v in v + W iff v in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v be VECTOR of V;
     (v in W implies (- 1) * v in v + W) & (- 1) * v = - v &
   (-1 <> 1 & (- 1) * v in v + W implies v in W) by Th52,Th53,RLVECT_1:29;
   hence thesis;
end;

theorem Th55:
for V being RealUnitarySpace, W being Subspace of V,
 u,v being VECTOR of V holds u + v in v + W iff u in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   set A = {v + v1 where v1 is VECTOR of V : v1 in W};
   thus u + v in v + W implies u in W
   proof
     assume u + v in v + W;
     then u + v in A by Def4;
     then consider v1 being VECTOR of V such that
A1:  u + v = v + v1 and
A2:  v1 in W;
     thus thesis by A1,A2,RLVECT_1:21;
   end;
   assume u in W;
   then u + v in A;
   hence thesis by Def4;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
 u,v being VECTOR of V holds v - u in v + W iff u in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
A1:v - u = (- u) + v by RLVECT_1:def 11;
A2:u in W implies - u in W by Th16;
     - u in W implies - (- u) in W by Th16;
   hence thesis by A1,A2,Th55,RLVECT_1:30;
end;

theorem Th57:
for V being RealUnitarySpace, W being Subspace of V,
 u,v being VECTOR of V holds u in v + W iff
  (ex v1 being VECTOR of V st v1 in W & u = v + v1)
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   set A = {v + v2 where v2 is VECTOR of V : v2 in W};
   thus u in v + W implies (ex v1 being VECTOR of V st v1 in W & u = v + v1)
   proof
     assume u in v + W;
     then u in A by Def4;
     then ex v1 being VECTOR of V st u = v + v1 & v1 in W;
     hence thesis;
   end;
   given v1 being VECTOR of V such that
A1:v1 in W & u = v + v1;
     u in A by A1;
   hence thesis by Def4;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
 u,v being VECTOR of V holds u in v + W iff
  (ex v1 being VECTOR of V st v1 in W & u = v - v1)
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   set A = {v + v2 where v2 is VECTOR of V : v2 in W};
   thus u in v + W implies (ex v1 being VECTOR of V st v1 in W & u = v - v1)
   proof
     assume u in v + W;
     then u in A by Def4;
     then consider v1 being VECTOR of V such that
A1:  u = v + v1 and
A2:  v1 in W;
     take x = - v1;
     thus x in W by A2,Th16;
       u = v + (- (- v1)) by A1,RLVECT_1:30
      .= v - (- v1) by RLVECT_1:def 11;
     hence thesis;
   end;
   given v1 being VECTOR of V such that
A3:v1 in W & u = v - v1;
     u = v + (- v1) & - v1 in W by A3,Th16,RLVECT_1:def 11;
   then u in A;
   hence thesis by Def4;
end;

theorem Th59:
for V being RealUnitarySpace, W being Subspace of V,
 v1,v2 being VECTOR of V holds
  (ex v being VECTOR of V st v1 in v + W & v2 in v + W) iff v1 - v2 in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v1,v2 be VECTOR of V;
   thus (ex v being VECTOR of V st v1 in v + W & v2 in v + W)
        implies v1 - v2 in W
   proof
     given v be VECTOR of V such that
A1:  v1 in v + W and
A2:  v2 in v + W;
     consider u1 being VECTOR of V such that
A3:  u1 in W and
A4:  v1 = v + u1 by A1,Th57;
     consider u2 being VECTOR of V such that
A5:  u2 in W and
A6:  v2 = v + u2 by A2,Th57;
       v1 - v2 = (u1 + v) + (- (v + u2)) by A4,A6,RLVECT_1:def 11
            .= (u1 + v) + ((- v) - u2) by RLVECT_1:44
            .= ((u1 + v) + (- v)) - u2 by RLVECT_1:42
            .= (u1 + (v + (- v))) - u2 by RLVECT_1:def 6
            .= (u1 + 0.V) - u2 by RLVECT_1:16
            .= u1 - u2 by RLVECT_1:10;
     hence thesis by A3,A5,Th17;
   end;
   assume v1 - v2 in W;
   then A7: - (v1 - v2) in W by Th16;
   take v1;
   thus v1 in v1 + W by Th37;
     v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by RLVECT_1:47
                     .= (v1 + (- v1)) + v2 by RLVECT_1:def 6
                     .= 0.V + v2 by RLVECT_1:16
                     .= v2 by RLVECT_1:10;
   hence thesis by A7,Th57;
end;

theorem Th60:
for V being RealUnitarySpace, W being Subspace of V,
 u,v being VECTOR of V st v + W = u + W holds
  (ex v1 being VECTOR of V st v1 in W & v + v1 = u)
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   assume
A1:v + W = u + W;
   take v1 = u - v;
     v in u + W by A1,Th37;
   then v in {u + u2 where u2 is VECTOR of V : u2 in W} by Def4;
   then consider u1 being VECTOR of V such that
A2:v = u + u1 and
A3:u1 in W;
     0.V = (u + u1) - v by A2,RLVECT_1:28
      .= u + (u1 - v) by RLVECT_1:42
      .= u + ((- v) + u1) by RLVECT_1:def 11
      .= (u + (- v)) + u1 by RLVECT_1:def 6
      .= u1 + (u - v) by RLVECT_1:def 11;
   then v1 = - u1 by RLVECT_1:def 10;
   hence v1 in W by A3,Th16;
   thus v + v1 = (u + v) - v by RLVECT_1:42
              .= u + (v - v) by RLVECT_1:42
              .= u + 0.V by RLVECT_1:28
              .= u by RLVECT_1:10;
end;

theorem Th61:
for V being RealUnitarySpace, W being Subspace of V,
 u,v being VECTOR of V st v + W = u + W holds
  (ex v1 being VECTOR of V st v1 in W & v - v1 = u)
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u,v be VECTOR of V;
   assume
A1:v + W = u + W;
   take v1 = v - u;
     u in v + W by A1,Th37;
   then u in {v + u2 where u2 is VECTOR of V : u2 in W} by Def4;
   then consider u1 being VECTOR of V such that
A2:u = v + u1 and A3: u1 in W;
     0.V = (v + u1) - u by A2,RLVECT_1:28
      .= v + (u1 - u) by RLVECT_1:42
      .= v + ((- u) + u1) by RLVECT_1:def 11
      .= (v + (- u)) + u1 by RLVECT_1:def 6
      .= u1 + (v - u) by RLVECT_1:def 11;
   then v1 = - u1 by RLVECT_1:def 10;
   hence v1 in W by A3,Th16;
   thus v - v1 = (v - v) + u by RLVECT_1:43
              .= 0.V + u by RLVECT_1:28
              .= u by RLVECT_1:10;
end;

theorem Th62:
for V being RealUnitarySpace, W1,W2 being strict Subspace of V,
 v being VECTOR of V holds v + W1 = v + W2 iff W1 = W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be strict Subspace of V;
   let v be VECTOR of V;
   thus v + W1 = v + W2 implies W1 = W2
   proof
     assume
A1:  v + W1 = v + W2;
       the carrier of W1 = the carrier of W2
     proof
A2:    the carrier of W1 c= the carrier of V by Def1;
A3:    the carrier of W2 c= the carrier of V by Def1;
       thus the carrier of W1 c= the carrier of W2
       proof
         let x be set;
         assume
A4:      x in the carrier of W1;
         then reconsider y = x as Element of V by A2;
         set z = v + y;
           x in W1 by A4,RLVECT_1:def 1;
         then z in {v + u where u is VECTOR of V : u in W1};
         then z in v + W2 by A1,Def4;
         then z in {v + u where u is VECTOR of V : u in W2} by Def4;
         then consider u being VECTOR of V such that
A5:      z = v + u and
A6:      u in W2;
           y = u by A5,RLVECT_1:21;
         hence thesis by A6,RLVECT_1:def 1;
       end;
       let x be set;
       assume
A7:    x in the carrier of W2;
       then reconsider y = x as Element of V by A3;

       set z = v + y;
         x in W2 by A7,RLVECT_1:def 1;
       then z in {v + u where u is VECTOR of V : u in W2};
       then z in v + W1 by A1,Def4;
       then z in {v + u where u is VECTOR of V : u in W1} by Def4;
       then consider u being VECTOR of V such that
A8:    z = v + u and A9: u in W1;
         y = u by A8,RLVECT_1:21;
       hence thesis by A9,RLVECT_1:def 1;
     end;
     hence thesis by Th24;
   end;
   thus thesis;
end;

theorem Th63:
for V being RealUnitarySpace, W1,W2 being strict Subspace of V,
 u,v being VECTOR of V st v + W1 = u + W2 holds W1 = W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be strict Subspace of V;
   let u,v be VECTOR of V;
   assume
A1:v + W1 = u + W2;
   set V1 = the carrier of W1; set V2 = the carrier of W2;
   assume
A2:W1 <> W2;
   then V1 <> V2 by Th24;
then A3:not V1 c= V2 or not V2 c= V1 by XBOOLE_0:def 10;

A4:now
     assume
A5:  V1 \ V2 <> {};
     consider x being Element of V1 \ V2;
       x in V1 & not x in V2 by A5,XBOOLE_0:def 4;
then A6:  x in W1 & not x in W2 by RLVECT_1:def 1;
     then x in V by Th2;
     then reconsider x as Element of V by RLVECT_1:def 1;

     set z = v + x;
       z in {v + u2 where u2 is VECTOR of V : u2 in W1} by A6;
     then z in u + W2 by A1,Def4;
     then z in {u + u2 where u2 is VECTOR of V : u2 in W2} by Def4;
     then consider u1 being VECTOR of V such that
A7:  z = u + u1 and
A8:  u1 in W2;
       x = 0.V + x by RLVECT_1:10
      .= v - v + x by RLVECT_1:28
      .= (- v + v) + x by RLVECT_1:def 11
      .= - v + (u + u1) by A7,RLVECT_1:def 6;
then A9:  (v + (- v + (u + u1))) + W1 = v + W1 by A6,Th46;
       v + (- v + (u + u1)) = (v + (- v)) + (u + u1) by RLVECT_1:def 6
                         .= (v - v) + (u + u1) by RLVECT_1:def 11
                         .= 0.V + (u + u1) by RLVECT_1:28
                         .= u + u1 by RLVECT_1:10;
     then (u + u1) + W2 = (u + u1) + W1 by A1,A8,A9,Th46;
     hence thesis by A2,Th62;
   end;
     now
     assume
A10: V2 \ V1 <> {};
     consider x being Element of V2 \ V1;
       x in V2 & not x in V1 by A10,XBOOLE_0:def 4;
then A11: x in W2 & not x in W1 by RLVECT_1:def 1;
     then x in V by Th2;
     then reconsider x as Element of V by RLVECT_1:def 1;

     set z = u + x;
       z in {u + u2 where u2 is VECTOR of V : u2 in W2} by A11;
     then z in v + W1 by A1,Def4;
     then z in {v + u2 where u2 is VECTOR of V : u2 in W1} by Def4;
     then consider u1 being VECTOR of V such that
A12: z = v + u1 and
A13: u1 in W1;
       x = 0.V + x by RLVECT_1:10
      .= u - u + x by RLVECT_1:28
      .= (- u + u) + x by RLVECT_1:def 11
      .= - u + (v + u1) by A12,RLVECT_1:def 6;
then A14: (u + (- u + (v + u1))) + W2 = u + W2 by A11,Th46;
       u + (- u + (v + u1)) = (u + (- u)) + (v + u1) by RLVECT_1:def 6
                         .= (u - u) + (v + u1) by RLVECT_1:def 11
                         .= 0.V + (v + u1) by RLVECT_1:28
                         .= v + u1 by RLVECT_1:10;
     then (v + u1) + W1 = (v + u1) + W2 by A1,A13,A14,Th46;
     hence thesis by A2,Th62;
   end;
   hence thesis by A3,A4,XBOOLE_1:37;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V, C being Coset of W holds
 C is lineary-closed iff C = the carrier of W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let C be Coset of W;
   thus C is lineary-closed implies C = the carrier of W
   proof
     assume
A1:  C is lineary-closed;
     consider v being VECTOR of V such that
A2:  C = v + W by Def5;
       C <> {} by A2,Th37;
     then 0.V in v + W by A1,A2,RLSUB_1:4;
     hence thesis by A2,Th41;
   end;
   thus thesis by Lm1;
end;

theorem
  for V being RealUnitarySpace, W1,W2 being strict Subspace of V,
  C1 being Coset of W1, C2 being Coset of W2 holds
 C1 = C2 implies W1 = W2
proof
   let V be RealUnitarySpace;
   let W1,W2 be strict Subspace of V;
   let C1 be Coset of W1;
   let C2 be Coset of W2;
A1:ex v1 being VECTOR of V st C1 = v1 + W1 by Def5;
     ex v2 being VECTOR of V st C2 = v2 + W2 by Def5;
   hence thesis by A1,Th63;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
 C being Coset of W, v being VECTOR of V holds
  {v} is Coset of (0).V
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let C be Coset of W;
   let v be VECTOR of V;
     v + (0).V = {v} by Th39;
   hence thesis by Def5;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
 V1 being Subset of V, v being VECTOR of V holds
 V1 is Coset of (0).V implies (ex v being VECTOR of V st V1 = {v})
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let V1 be Subset of V;
   let v be VECTOR of V;
   assume V1 is Coset of (0).V;
   then consider v being VECTOR of V such that
A1:V1 = v + (0).V by Def5;
   take v;
   thus thesis by A1,Th39;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V holds
 the carrier of W is Coset of W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
     the carrier of W = 0.V + W by Lm2;
   hence thesis by Def5;
end;

theorem
  for V being RealUnitarySpace holds the carrier of V is Coset of (Omega).V
proof
   let V be RealUnitarySpace;
     the carrier of V is Subset of V iff
    the carrier of V c= the carrier of V;
   then reconsider A = the carrier of V as Subset of V;
   consider v being VECTOR of V;
     A = v + (Omega).V by Th40;
   hence thesis by Def5;
  end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
 V1 being Subset of V st V1 is Coset of (Omega).V holds
  V1 = the carrier of V
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let V1 be Subset of V;
   assume V1 is Coset of (Omega).V;
   then ex v being VECTOR of V st V1 = v + (Omega).V by Def5;
   hence thesis by Th40;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V, C being Coset of W holds
 0.V in C iff C = the carrier of W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let C be Coset of W;
     ex v being VECTOR of V st C = v + W by Def5;
   hence thesis by Th41;
end;

theorem Th72:
for V being RealUnitarySpace, W being Subspace of V, C being Coset of W,
 u being VECTOR of V holds u in C iff C = u + W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let C be Coset of W;
   let u be VECTOR of V;
   thus u in C implies C = u + W
   proof
     assume
A1:  u in C;
       ex v being VECTOR of V st C = v + W by Def5;
     hence thesis by A1,Th48;
     end;
   thus thesis by Th37;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V, C being Coset of W,
 u,v being VECTOR of V st u in C & v in C holds
  (ex v1 being VECTOR of V st v1 in W & u + v1 = v)
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let C be Coset of W;
   let u,v be VECTOR of V;
   assume u in C & v in C;
   then C = u + W & C = v + W by Th72;
   hence thesis by Th60;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V, C being Coset of W,
 u,v being VECTOR of V st u in C & v in C holds
  (ex v1 being VECTOR of V st v1 in W & u - v1 = v)
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let C be Coset of W;
   let u,v be VECTOR of V;
   assume u in C & v in C;
   then C = u + W & C = v + W by Th72;
   hence thesis by Th61;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
 v1,v2 being VECTOR of V holds
  (ex C being Coset of W st v1 in C & v2 in C) iff v1 - v2 in W
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let v1,v2 be VECTOR of V;
   thus (ex C being Coset of W st v1 in C & v2 in C) implies v1 - v2 in W
   proof
     given C be Coset of W such that
A1:  v1 in C & v2 in C;
       ex v being VECTOR of V st C = v + W by Def5;
     hence thesis by A1,Th59;
   end;
   assume v1 - v2 in W;
   then consider v being VECTOR of V such that
A2:v1 in v + W & v2 in v + W by Th59;
   reconsider C = v + W as Coset of W by Def5;
   take C;
   thus thesis by A2;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V,
 u being VECTOR of V, B,C being Coset of W st u in B & u in C holds B = C
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   let u be VECTOR of V;
   let B,C be Coset of W;
   assume
A1:u in B & u in C;
A2:ex v1 being VECTOR of V st B = v1 + W by Def5;
     ex v2 being VECTOR of V st C = v2 + W by Def5;
   hence thesis by A1,A2,Th50;
end;



Back to top