The Mizar article:

Dimension 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_4
[ MML identifier index ]


environ

 vocabulary RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2, FINSEQ_1, FUNCT_1, SEQ_1,
      RELAT_1, FINSEQ_4, BOOLE, FUNCT_2, ARYTM_1, TARSKI, CARD_1, RLVECT_3,
      BHSP_1, CONNSP_3, SUBSET_1, RLSUB_2, MATRLIN, VECTSP_9, RUSUB_4, ARYTM_3;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XREAL_0, REAL_1, NAT_1,
      FINSEQ_1, FUNCT_1, CARD_1, FUNCT_2, PRE_TOPC, STRUCT_0, RLVECT_1,
      FINSEQ_3, FINSEQ_4, FINSET_1, RLSUB_1, RLVECT_2, BHSP_1, RLVECT_3,
      RUSUB_1, RUSUB_2, RUSUB_3;
 constructors NAT_1, REAL_1, RLVECT_2, FINSEQ_4, DOMAIN_1, RLVECT_3, RUSUB_2,
      FINSEQ_3, RUSUB_3, PRE_TOPC, XREAL_0, MEMBERED;
 clusters SUBSET_1, FINSET_1, RELSET_1, STRUCT_0, FINSEQ_1, PRE_TOPC, RLVECT_1,
      RLSUB_1, NAT_1, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions XBOOLE_0, TARSKI;
 theorems FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSET_1, REAL_1,
      RLSUB_2, RLVECT_1, RLVECT_2, TARSKI, XBOOLE_0, XBOOLE_1, RUSUB_1,
      RUSUB_2, RLVECT_3, ENUMSET1, AXIOMS, RLVECT_5, NAT_1, SUBSET_1, RUSUB_3,
      RLSUB_1, CARD_1, CARD_2, MATRLIN, PRE_TOPC, VECTSP_9, XCMPLX_0, XCMPLX_1;
 schemes NAT_1, XBOOLE_0, FINSEQ_1, COMPLSP1;

begin  :: Finite-dimensional real unitary space

theorem Th1:
for V being RealUnitarySpace, A,B being finite Subset of V,
 v being VECTOR of V st v in Lin(A \/ B) & not v in Lin(B) holds
  ex w being VECTOR of V st w in A & w in Lin(A \/ B \ {w} \/ {v})
proof
   let V be RealUnitarySpace;
   let A, B be finite Subset of V;
   let v be VECTOR of V such that
A1:v in Lin(A \/ B) and
A2:not v in Lin(B);

   consider L being Linear_Combination of (A \/ B) such that
A3:v = Sum(L) by A1,RUSUB_3:1;

A4:Carrier(L) c= A \/ B by RLVECT_2:def 8;

     now
     assume
A5:  for w being VECTOR of V st w in A holds L.w = 0;
       now
       let x be set;
       assume
A6:    x in Carrier(L) & x in A;
       then consider u being VECTOR of V such that
A7:    x = u & L.u <> 0 by RLVECT_5:3;
       thus contradiction by A5,A6,A7;
     end;
     then Carrier(L) misses A by XBOOLE_0:3;
     then Carrier(L) c= B by A4,XBOOLE_1:73;
     then L is Linear_Combination of B by RLVECT_2:def 8;
     hence contradiction by A2,A3,RUSUB_3:1;
   end;
   then consider w being VECTOR of V such that
A8:w in A and
A9:L.w <> 0;
   take w;
   set a = L.w;

   consider F being FinSequence of the carrier of V such that
A10:F is one-to-one and
A11:rng F = Carrier(L) and
A12:Sum(L) = Sum(L (#) F) by RLVECT_2:def 10;

A13:w in rng F by A9,A11,RLVECT_5:3;
then A14:F = (F -| w) ^ <* w *> ^ (F |-- w) by FINSEQ_4:66;
   reconsider Fw1 = (F -| w) as FinSequence of the carrier of V
                                                   by A13,FINSEQ_4:53;
   reconsider Fw2 = (F |-- w) as FinSequence of the carrier of V
                                                   by A13,FINSEQ_4:65;
     F = Fw1 ^ (<* w *> ^ Fw2) by A14,FINSEQ_1:45;
   then L (#) F = (L (#) Fw1) ^ (L (#) (<* w *> ^ Fw2)) by RLVECT_3:41
          .= (L (#) Fw1) ^ ((L (#) <* w *>) ^ (L (#) Fw2)) by RLVECT_3:41
          .= (L (#) Fw1) ^ (L (#) <* w *>) ^ (L (#) Fw2) by FINSEQ_1:45
          .= (L (#) Fw1) ^ <* a*w *> ^ (L (#) Fw2) by RLVECT_2:42;
then A15:Sum(L (#) F) = Sum((L (#) Fw1) ^ (<* a*w *> ^ (L (#) Fw2))) by
FINSEQ_1:45
                .= Sum(L (#) Fw1) + Sum(<* a*w *> ^ (L (#) Fw2)) by RLVECT_1:58
                .= Sum(L (#) Fw1) + (Sum(<* a*w *>) + Sum(L (#) Fw2))
                    by RLVECT_1:58
                .= Sum(L (#) Fw1) + (Sum(L (#) Fw2) + a*w) by RLVECT_1:61
                .= (Sum(L (#) Fw1) + Sum(L (#) Fw2)) + a*w by RLVECT_1:def 6
                .= Sum((L (#) Fw1) ^ (L (#) Fw2)) + a*w by RLVECT_1:58
                .= Sum(L (#) (Fw1 ^ Fw2)) + a*w by RLVECT_3:41;
   set Fw = Fw1 ^ Fw2;
   consider K being Linear_Combination of V such that
A16:Carrier(K) = rng Fw /\ Carrier(L) & L (#) Fw = K (#) Fw by RLVECT_5:8;

     F just_once_values w by A10,A13,FINSEQ_4:10;
   then Fw = F - {w} by FINSEQ_4:69;
then A17:rng Fw = Carrier(L) \ {w} by A11,FINSEQ_3:72;
   then rng Fw c= Carrier(L) by XBOOLE_1:36;
then A18:Carrier(K) = rng Fw by A16,XBOOLE_1:28;

then A19:Carrier(K) c= A \/ B \ {w} by A4,A17,XBOOLE_1:33;
   then reconsider K as Linear_Combination of (A \/ B \ {w}) by RLVECT_2:def 8;

     Fw1 is one-to-one & Fw2 is one-to-one & rng Fw1 misses rng Fw2
       by A10,A13,FINSEQ_4:67,68,72;
   then Fw is one-to-one by FINSEQ_3:98;
   then Sum(K (#) Fw) = Sum(K) by A18,RLVECT_2:def 10;
   then a"*v = a"*Sum(K) + a"*(a*w) by A3,A12,A15,A16,RLVECT_1:def 9
       .= a"*Sum(K) + (a"*a)*w by RLVECT_1:def 9
       .= a"*Sum(K) +1*w by A9,XCMPLX_0:def 7
       .= a"*Sum(K) + w by RLVECT_1:def 9;
then A20:w = a"*v - a"*Sum(K) by RLSUB_2:78
     .= a"*(v - Sum(K)) by RLVECT_1:48
     .= a"*(-Sum(K) + v) by RLVECT_1:def 11;

     v in {v} by TARSKI:def 1;
   then v in Lin({v}) by RUSUB_3:2;
   then consider Lv being Linear_Combination of {v} such that
A21:v = Sum(Lv) by RUSUB_3:1;

A22:w = a"*(Sum(-K) + Sum(Lv)) by A20,A21,RLVECT_3:3
     .= a"*Sum(-K + Lv) by RLVECT_3:1
     .= Sum(a"*(-K + Lv)) by RLVECT_3:2;

A23:a" <> 0 by A9,XCMPLX_1:203;
   set LC = a"*(-K + Lv);
A24:Carrier(Lv) c= {v} by RLVECT_2:def 8;
     Carrier (-K + Lv) c= Carrier(-K) \/ Carrier(Lv) by RLVECT_2:58;
then A25:Carrier (-K + Lv) c= Carrier(K) \/ Carrier(Lv) by RLVECT_2:75;
     Carrier(K) \/ Carrier(Lv) c= A \/ B \ {w} \/ {v} by A19,A24,XBOOLE_1:13;
   then Carrier (-K + Lv) c= A \/ B \ {w} \/ {v} by A25,XBOOLE_1:1;
   then Carrier (LC) c= A \/ B \ {w} \/ {v} by A23,RLVECT_2:65;
   then LC is Linear_Combination of (A \/ B \ {w} \/ {v}) by RLVECT_2:def 8;
   hence thesis by A8,A22,RUSUB_3:1;
end;

Lm1:
  for X being set, x be set st x in X holds X \ {x} \/ {x} = X
proof
  let X be set;
  let x be set;
  assume x in X;
then A1: {x} is Subset of X by SUBSET_1:63;
    {x} \/ (X \ {x}) = {x} \/ X by XBOOLE_1:39
                 .= X by A1,XBOOLE_1:12;
  hence thesis;
end;

Lm2:
  for X being set, x being set st not x in X holds X \ {x} = X
proof
  let X be set,
      x be set such that
A1: not x in X;
    now
    assume X meets {x};
    then consider y being set such that
  A2: y in X /\ {x} by XBOOLE_0:4;
      y in X & y in {x} by A2,XBOOLE_0:def 3;
    hence contradiction by A1,TARSKI:def 1;
  end;
  hence X \ {x} = X by XBOOLE_1:83;
end;

theorem Th2:
for V being RealUnitarySpace, A,B being finite Subset of V st
 the UNITSTR of V = Lin(A) & B is linearly-independent holds
  Card B <= Card A &
   ex C being finite Subset of V st
    C c= A & Card C = Card A - Card B & the UNITSTR of V = Lin(B \/ C)
proof
   let V be RealUnitarySpace;
   let A, B be finite Subset of V such that
A1:the UNITSTR of V = Lin(A) and
A2:B is linearly-independent;
   defpred P[Nat] means
    for n being Nat
     for A, B being finite Subset of V st card(A) = n & card(B) = $1 &
      the UNITSTR of V = Lin(A) & B is linearly-independent
    holds
     $1 <= n &
      ex C being finite Subset of V st C c= A
       & card(C) = n - $1 & the UNITSTR of V = Lin(B \/ C);
A3:P[0]
   proof
     let n be Nat;
     let A, B be finite Subset of V such that
A4:  card(A) = n & card(B) = 0 &
     the UNITSTR of V = Lin(A) & B is linearly-independent;
       B = {} by A4,CARD_2:59;
     then A = B \/ A;
     hence thesis by A4,NAT_1:18;
   end;
A5:for m being Nat st P[m] holds P[m + 1]
   proof
     let m be Nat such that
A6:  P[m];
     let n be Nat;
     let A, B be finite Subset of V such that
A7:  card(A) = n and
A8: card(B) = m + 1 and
A9: the UNITSTR of V = Lin(A) and
A10: B is linearly-independent;
     consider v being set such that
A11: v in B by A8,CARD_1:47,XBOOLE_0:def 1;
     reconsider v as VECTOR of V by A11;
       {v} is Subset of B by A11,SUBSET_1:63;
then A12: card(B \ {v}) = card(B) - card({v}) by CARD_2:63
                    .= m + 1 - 1 by A8,CARD_1:79
                    .= m by XCMPLX_1:26;
     set Bv = B \ {v};
A13: Bv c= B by XBOOLE_1:36;
then A14: Bv is linearly-independent by A10,RLVECT_3:6;
A15: not v in Lin(Bv) by A10,A11,RUSUB_3:25;
       now
       assume m = n;
       then consider C being finite Subset of V such that
A16:   C c= A & card(C) = m - m & the UNITSTR of V = Lin(Bv \/ C)
         by A6,A7,A9,A12,A14;
         card(C) = 0 by A16,XCMPLX_1:14;
       then C = {} by CARD_2:59;
       then Bv is Basis of V by A14,A16,RUSUB_3:def 2;
       hence contradiction by A15,RUSUB_3:21;
     end;
     then m <> n & m <= n by A6,A7,A9,A12,A14;
then A17: m < n by REAL_1:def 5;
     consider C being finite Subset of V such that
A18: C c= A and
A19: card(C) = n - m and
A20: the UNITSTR of V = Lin(Bv \/ C) by A6,A7,A9,A12,A14;
       v in Lin(Bv \/ C) by A20,RLVECT_1:def 1;
     then consider w being VECTOR of V such that
A21: w in C and
A22: w in Lin(C \/ Bv \ {w} \/ {v}) by A15,Th1;
     set Cw = C \ {w};
       Cw c= C by XBOOLE_1:36;
then A23: Cw c= A by A18,XBOOLE_1:1;
       {w} is Subset of C by A21,SUBSET_1:63;
then A24: card(Cw) = card(C) - card({w}) by CARD_2:63
              .= n - m - 1 by A19,CARD_1:79
              .= n - (m + 1) by XCMPLX_1:36;
A25: C = Cw \/ {w} by A21,Lm1;
A26: C \/ Bv \ {w} \/ {v} = (Cw \/ (Bv \ {w})) \/ {v} by XBOOLE_1:42
                       .= Cw \/ ((Bv \ {w}) \/ {v}) by XBOOLE_1:4;
       Bv \ {w} c= Bv by XBOOLE_1:36;
     then (Bv \ {w}) \/ {v} c= Bv \/ {v} by XBOOLE_1:9;
     then Cw \/ ((Bv \ {w}) \/ {v}) c= Cw \/ (Bv \/ {v}) by XBOOLE_1:9;
     then Cw \/ ((Bv \ {w}) \/ {v}) c= B \/ Cw by A11,Lm1;
     then Lin(C \/ Bv \ {w} \/ {v}) is Subspace of Lin(B \/ Cw)
          by A26,RUSUB_3:7;
then A27: w in Lin(B \/ Cw) by A22,RUSUB_1:1;
       now
       let x be set;
       assume x in Bv \/ C;
       then x in Bv or x in C by XBOOLE_0:def 2;
       then x in B or x in Cw or x in {w} by A13,A25,XBOOLE_0:def 2;
       then x in B \/ Cw or x in {w} by XBOOLE_0:def 2;
       then x in Lin(B \/ Cw) or x = w by RUSUB_3:2,TARSKI:def 1;
       hence x in the carrier of Lin(B \/ Cw) by A27,RLVECT_1:def 1;
     end;
     then Bv \/ C c= the carrier of Lin(B \/ Cw) by TARSKI:def 3;
     then Lin(Bv \/ C) is Subspace of Lin(B \/ Cw) by RUSUB_3:27;
     then the carrier of Lin(Bv \/ C) c= the carrier of Lin(B \/ Cw) &
     the carrier of Lin(B \/ Cw) c= the carrier of V by RUSUB_1:def 1;
     then the carrier of Lin(B \/ Cw) = the carrier of V
            by A20,XBOOLE_0:def 10;
     then the UNITSTR of V = Lin(B \/ Cw) by A20,RUSUB_1:24;
     hence thesis by A17,A23,A24,NAT_1:38;
   end;
   for m being Nat holds P[m] from Ind(A3, A5);
   hence thesis by A1,A2;
end;

definition
  let V be RealUnitarySpace;
  attr V is finite-dimensional means
:Def1:
    ex A being finite Subset of V st A is Basis of V;
end;

definition
  cluster strict finite-dimensional RealUnitarySpace;
existence
proof
   consider V being RealUnitarySpace;
   take (0).V;
   thus (0).V is strict;
   take A = {}( the carrier of (0).V );
A1:A is linearly-independent by RLVECT_3:8;
     Lin(A) = (0).(0).V by RUSUB_3:3;
   then Lin(A) = the UNITSTR of (0).V by RUSUB_1:30;
   hence A is Basis of (0).V by A1,RUSUB_3:def 2;
end;
end;

definition
  let V be RealUnitarySpace;
  redefine attr V is finite-dimensional means
:Def2:
  ex I being finite Subset of V st I is Basis of V;
compatibility by Def1;
end;

theorem Th3:
for V being RealUnitarySpace st V is finite-dimensional holds
 for I being Basis of V holds I is finite
proof
   let V be RealUnitarySpace;
   assume V is finite-dimensional;
   then consider A being finite Subset of V such that
A1:A is Basis of V by Def2;
   let B be Basis of V;
   consider p being FinSequence such that
A2:rng p = A by FINSEQ_1:73;
   reconsider p as FinSequence of the carrier of V by A2,FINSEQ_1:def 4;

   set Car = {Carrier(L) where L is Linear_Combination of B:
              ex i being Nat st i in dom p & Sum(L) = p.i};
   set C = union Car;

A3:C c= B
   proof
     let x be set;
     assume x in C;
     then consider R being set such that
A4:  x in R and
A5:  R in Car by TARSKI:def 4;
     consider L being Linear_Combination of B such that
A6:  R = Carrier(L) and
       ex i being Nat st i in dom p & Sum(L) = p.i by A5;
       R c= B by A6,RLVECT_2:def 8;
     hence x in B by A4;
   end;
   then C c= the carrier of V by XBOOLE_1:1;
   then reconsider C as Subset of V;
A7:B is linearly-independent by RUSUB_3:def 2;
then A8:C is linearly-independent by A3,RLVECT_3:6;
     for v being VECTOR of V holds v in (Omega).V iff v in Lin(C)
   proof
     let v be VECTOR of V;
     hereby
       assume v in (Omega).V;
       then v in the UNITSTR of V by RUSUB_1:def 3;
       then v in Lin(A) by A1,RUSUB_3:def 2;
       then consider LA being Linear_Combination of A such that
A9:    v = Sum(LA) by RUSUB_3:1;
         Carrier(LA) c= the carrier of Lin(C)
       proof
         let w be set;
         assume
A10:     w in Carrier(LA);
then A11:     w in Carrier(LA) & Carrier(LA) c= A by RLVECT_2:def 8;
         reconsider w'= w as VECTOR of V by A10;
           w' in Lin(B) by RUSUB_3:21;
         then consider LB being Linear_Combination of B such that
A12:     w = Sum(LB) by RUSUB_3:1;
          ex i being set st i in dom p & w = p.i by A2,A11,FUNCT_1:def 5;
         then A13:     Carrier(LB) in Car by A12;
           Carrier(LB) c= C
         proof
           let x be set;
           assume x in Carrier(LB);
           hence x in C by A13,TARSKI:def 4;
         end;
         then LB is Linear_Combination of C by RLVECT_2:def 8;
         then w in Lin(C) by A12,RUSUB_3:1;
         hence w in the carrier of Lin(C) by RLVECT_1:def 1;
       end;
       then consider LC being Linear_Combination of C such that
A14:   Sum(LA) = Sum(LC) by RUSUB_3:17;
       thus v in Lin(C) by A9,A14,RUSUB_3:1;
     end;
     assume v in Lin(C);
       v in the carrier of the UNITSTR of V;
     then v in the carrier of (Omega).V by RUSUB_1:def 3;
     hence thesis by RLVECT_1:def 1;
   end;
   then (Omega).V = Lin(C) by RUSUB_1:25;
   then the UNITSTR of V = Lin(C) by RUSUB_1:def 3;
then A15:C is Basis of V by A8,RUSUB_3:def 2;
     B c= C
   proof
     assume not B c= C;
     then consider v being set such that
A16: v in B and
A17: not v in C by TARSKI:def 3;

     set D = B \ C;

A18: D misses C by XBOOLE_1:79;
     reconsider B as Subset of V;
     reconsider D as non empty Subset of V by A16,A17,XBOOLE_0:def 4;
       C \/ (B \ C) = C \/ B by XBOOLE_1:39
                 .= B by A3,XBOOLE_1:12;
     then B = C \/ D;
     hence contradiction by A7,A15,A18,RUSUB_3:26;
   end;

then A19:B = C by A3,XBOOLE_0:def 10;

   defpred P[set, set] means
    ex L being Linear_Combination of B st $2 = Carrier(L) & Sum(L) = p.$1;

A20:for i being Nat, y1,y2 being set st
     i in Seg len p & P[i, y1] & P[i, y2] holds y1 = y2
   proof
     let i be Nat;
     let y1,y2 be set;
     assume that
       i in Seg len p and
A21: P[i, y1] and
A22: P[i, y2];
     consider L1 being Linear_Combination of B such that
A23: y1 = Carrier(L1) and
A24: Sum(L1) = p.i by A21;
     consider L2 being Linear_Combination of B such that
A25: y2 = Carrier(L2) and
A26: Sum(L2) = p.i by A22;
       Carrier(L1) c= B & Carrier(L2) c= B by RLVECT_2:def 8;
     hence y1 = y2 by A7,A23,A24,A25,A26,RLVECT_5:1;
   end;
A27:for i being Nat st i in Seg len p ex x being set st P[i, x]
   proof
     let i be Nat;
     assume i in Seg len p;
     then i in dom p by FINSEQ_1:def 3;
     then p.i in the carrier of V by FINSEQ_2:13;
     then p.i in Lin(B) by RUSUB_3:21;
     then consider L being Linear_Combination of B such that
A28: p.i = Sum(L) by RUSUB_3:1;
       P[i, Carrier(L)] by A28;
     hence thesis;
   end;
   ex q being FinSequence st dom q = Seg len p &
    for i being Nat st i in Seg len p holds P[i, q.i]
     from SeqEx(A20, A27);
   then consider q being FinSequence such that
A29:dom q = Seg len p & for i being Nat st i in Seg len p holds P[i, q.i];
A30:dom p = dom q by A29,FINSEQ_1:def 3;

     now
     let x be set;
     assume x in rng q;
     then consider i being set such that
A31: i in dom q and
A32: x = q.i by FUNCT_1:def 5;
     reconsider i as Nat by A31;
     consider L being Linear_Combination of B such that
A33: x = Carrier(L) and
A34: Sum(L) = p.i by A29,A31,A32;
     thus x in Car by A30,A31,A33,A34;
   end;
then A35:rng q c= Car by TARSKI:def 3;

     now
     let x be set;
     assume x in Car;
     then consider L being Linear_Combination of B such that
A36: x = Carrier(L) and
A37: ex i being Nat st i in dom p & Sum(L) = p.i;
     consider i being Nat such that
A38: i in dom p & Sum(L) = p.i by A37;
       P[i, x] & P[i, q.i] by A29,A30,A36,A38;
     then x = q.i by A20,A29,A30,A38;
     hence x in rng q by A30,A38,FUNCT_1:def 5;
   end;
   then Car c= rng q by TARSKI:def 3;
then A39:Car is finite by A35,XBOOLE_0:def 10;

     for R being set st R in Car holds R is finite
   proof
     let R be set;
     assume R in Car;
     then consider L being Linear_Combination of B such that
A40: R = Carrier(L) and
       ex i being Nat st i in dom p & Sum(L) = p.i;
     thus R is finite by A40;
   end;
   hence B is finite by A19,A39,FINSET_1:25;
end;

theorem
  for V being RealUnitarySpace, A being Subset of V st
 V is finite-dimensional & A is linearly-independent holds A is finite
proof
   let V be RealUnitarySpace;
   let A be Subset of V;
   assume
A1:V is finite-dimensional &
   A is linearly-independent;
   then consider B being Basis of V such that
A2:A c= B by RUSUB_3:15;
     B is finite by A1,Th3;
   hence A is finite by A2,FINSET_1:13;
end;

theorem Th5:
for V being RealUnitarySpace, A,B being Basis of V st
 V is finite-dimensional holds Card A = Card B
proof
   let V be RealUnitarySpace;
   let A, B be Basis of V;
   assume V is finite-dimensional;
   then reconsider A'= A, B'= B as finite Subset of V by Th3;
A1:the UNITSTR of V = Lin(A) by RUSUB_3:def 2;
     B' is linearly-independent by RUSUB_3:def 2;
then A2:Card B' <= Card A' by A1,Th2;
A3:the UNITSTR of V = Lin(B) by RUSUB_3:def 2;
     A' is linearly-independent by RUSUB_3:def 2;
   then Card A' <= Card B' by A3,Th2;
   hence Card A = Card B by A2,AXIOMS:21;
end;

theorem Th6:
for V being RealUnitarySpace holds (0).V is finite-dimensional
proof
   let V be RealUnitarySpace;
   reconsider V'= (0).V as strict RealUnitarySpace;
     the carrier of V' = {0.V} by RUSUB_1:def 2
                    .= {0.V'} by RUSUB_1:4
                    .= the carrier of (0).V' by RUSUB_1:def 2;
then A1:V' = (0).V' by RUSUB_1:26;
   reconsider I = {}(the carrier of V') as finite Subset of V'
  ;
A2:I is linearly-independent by RLVECT_3:8;
     Lin(I) = (0).V' by RUSUB_3:3;
   then I is Basis of V' by A1,A2,RUSUB_3:def 2;
   hence thesis by Def2;
end;

theorem Th7:
for V being RealUnitarySpace, W being Subspace of V st
 V is finite-dimensional holds W is finite-dimensional
proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
   assume
A1:V is finite-dimensional;
   consider A being Basis of W;
   consider I being Basis of V such that
A2:A c= I by RUSUB_3:24;
     I is finite by A1,Th3;
   then A is finite by A2,FINSET_1:13;
   hence thesis by Def1;
end;

definition
  let V be RealUnitarySpace;
  cluster finite-dimensional strict Subspace of V;
existence
proof
   take (0).V;
   thus thesis by Th6;
end;
end;

definition
  let V be finite-dimensional RealUnitarySpace;
  cluster -> finite-dimensional Subspace of V;
correctness by Th7;
end;

definition
  let V be finite-dimensional RealUnitarySpace;
  cluster strict Subspace of V;
existence
   proof
     (0).V is strict finite-dimensional Subspace of V;
   hence thesis;
end;
end;

begin  :: Dimension of real unitary space

definition
  let V be RealUnitarySpace;
  assume A1: V is finite-dimensional;
  func dim V -> Nat means
:Def3:
  for I being Basis of V holds it = Card I;
existence
proof
   consider A being finite Subset of V such that
A2:A is Basis of V by A1,Def2;
   consider n being Nat such that
A3:n = Card A;
     for I being Basis of V holds Card I = n by A1,A2,A3,Th5;
   hence thesis;
end;
uniqueness
proof
    let n, m be Nat;
    assume that
  A4: for I being Basis of V holds Card I = n and
  A5: for I being Basis of V holds Card I = m;

    consider A being finite Subset of V such that
  A6: A is Basis of V by A1,Def2;

      Card A = n & Card A = m by A4,A5,A6;
    hence n = m;
  end;
end;

theorem Th8:
for V being finite-dimensional RealUnitarySpace, W being Subspace of V holds
 dim W <= dim V
proof
   let V be finite-dimensional RealUnitarySpace;
   let W be Subspace of V;
   reconsider V'= V as RealUnitarySpace;
   consider I being Basis of V';
A1:Lin(I) = the UNITSTR of V' by RUSUB_3:def 2;
   reconsider I as finite Subset of V by Th3;
A2:dim V = Card I by Def3;
   consider A being Basis of W;
   reconsider A as Subset of W;
     A is linearly-independent by RUSUB_3:def 2;
   then consider B being Subset of V such that
A3:B is linearly-independent & B = A by RUSUB_3:22;
   reconsider A'= A as finite Subset of V by A3,Th3;
     Card A' <= Card I by A1,A3,Th2;
   hence dim W <= dim V by A2,Def3;
end;

theorem Th9:
for V being finite-dimensional RealUnitarySpace, A being Subset of V st
 A is linearly-independent holds Card A = dim Lin(A)
proof
   let V be finite-dimensional RealUnitarySpace;
   let A be Subset of V such that
A1:A is linearly-independent;
   set W = Lin(A);
     now
     let x be set;
     assume x in A;
     then x in W by RUSUB_3:2;
     hence x in the carrier of W by RLVECT_1:def 1;
   end;
   then A c= the carrier of W by TARSKI:def 3;
   then consider B being Subset of W such that
A2:B is linearly-independent & B = A by A1,RUSUB_3:23;
     W = Lin(B) by A2,RUSUB_3:28;
   then reconsider B as Basis of W by A2,RUSUB_3:def 2;
     Card B = dim W by Def3;
   hence Card A = dim Lin(A) by A2;
end;

theorem Th10:
for V being finite-dimensional RealUnitarySpace holds
 dim V = dim (Omega).V
proof
   let V be finite-dimensional RealUnitarySpace;
   consider I being finite Subset of V such that
A1:I is Basis of V by Def2;
A2:Card I = dim V by A1,Def3;
A3:I is linearly-independent by A1,RUSUB_3:def 2;
     (Omega).V = the UNITSTR of V by RUSUB_1:def 3
            .= Lin(I) by A1,RUSUB_3:def 2;
   hence thesis by A2,A3,Th9;
end;

theorem
  for V being finite-dimensional RealUnitarySpace, W being Subspace of V holds
 dim V = dim W iff (Omega).V = (Omega).W
proof
   let V be finite-dimensional RealUnitarySpace;
   let W be Subspace of V;
   hereby
     assume
A1:  dim V = dim W;
     consider A being Basis of W;
     consider B being Basis of V such that
A2:  A c= B by RUSUB_3:24;
A3:  Card A = dim V by A1,Def3
           .= Card B by Def3;
       A c= the carrier of W & the carrier of W c= the carrier of V
       by RUSUB_1:def 1;
     then A c= the carrier of V & A is finite by Th3,XBOOLE_1:1;
     then reconsider A'= A as finite Subset of V;
     reconsider B'= B as finite Subset of V by Th3;
A4:  now
       assume A <> B;
       then A c< B by A2,XBOOLE_0:def 8;
       then Card A' < Card B' by CARD_2:67;
       hence contradiction by A3;
     end;
     reconsider A as Subset of W;
     reconsider B as Subset of V;
       (Omega).V = the UNITSTR of V by RUSUB_1:def 3
              .= Lin(B) by RUSUB_3:def 2
              .= Lin(A) by A4,RUSUB_3:28
              .= the UNITSTR of W by RUSUB_3:def 2
              .= (Omega).W by RUSUB_1:def 3;
     hence (Omega).V = (Omega).W;
   end;
   assume (Omega).V = (Omega).W;
then A5:the UNITSTR of V = (Omega).W by RUSUB_1:def 3
                   .= the UNITSTR of W by RUSUB_1:def 3;
   consider A being finite Subset of V such that
A6:A is Basis of V by Def2;
   consider B being finite Subset of W such that
A7:B is Basis of W by Def2;
A8:A is linearly-independent by A6,RUSUB_3:def 2;
A9:B is linearly-independent by A7,RUSUB_3:def 2;
A10:Lin(A) = the UNITSTR of W by A5,A6,RUSUB_3:def 2
         .= Lin(B) by A7,RUSUB_3:def 2;

   reconsider A as Subset of V;
   reconsider B as Subset of W;

     dim V = Card A by A6,Def3
        .= dim Lin(B) by A8,A10,Th9
        .= Card B by A9,Th9
        .= dim W by A7,Def3;
   hence dim V = dim W;
end;

theorem Th12:
for V being finite-dimensional RealUnitarySpace holds
 dim V = 0 iff (Omega).V = (0).V
proof
   let V be finite-dimensional RealUnitarySpace;
   hereby assume
A1:  dim V = 0;
     consider I being finite Subset of V such that
A2:  I is Basis of V by Def2;
       Card I = 0 by A1,A2,Def3;
then A3:  I = {}(the carrier of V) by CARD_2:59;
       (Omega).V = the UNITSTR of V by RUSUB_1:def 3
              .= Lin(I) by A2,RUSUB_3:def 2
              .= (0).V by A3,RUSUB_3:3;
     hence (Omega).V = (0).V;
   end;
   assume (Omega).V = (0).V;
then A4:the UNITSTR of V = (0).V by RUSUB_1:def 3;
   consider I being finite Subset of V such that
A5:I is Basis of V by Def2;
     Lin(I) = (0).V by A4,A5,RUSUB_3:def 2;
then A6:I = {} or I = {0.V} by RUSUB_3:4;
     now
     assume I = {0.V};
     then I is linearly-dependent by RLVECT_3:9;
     hence contradiction by A5,RUSUB_3:def 2;
   end;
   hence dim V = 0 by A5,A6,Def3,CARD_1:47;
end;

theorem
  for V being finite-dimensional RealUnitarySpace holds
 dim V = 1 iff ex v being VECTOR of V st v <> 0.V & (Omega).V = Lin{v}
proof
   let V be finite-dimensional RealUnitarySpace;
   hereby
     consider I being finite Subset of V such that
A1:  I is Basis of V by Def2;
     assume dim V = 1;
     then Card I = 1 by A1,Def3;
     then consider v being set such that
A2:  I = {v} by CARD_2:60;
       v in I by A2,TARSKI:def 1;
     then reconsider v as VECTOR of V;
       {v} is linearly-independent & Lin{v} = the UNITSTR of V
       by A1,A2,RUSUB_3:def 2;
     then v <> 0.V & (Omega).V = Lin{v} by RLVECT_3:9,RUSUB_1:def 3;
     hence ex v being VECTOR of V st v <> 0.V & (Omega).V = Lin{v};
   end;
   given v being VECTOR of V such that
A3:v <> 0.V and
A4:(Omega).V = Lin{v};
     {v} is linearly-independent & Lin{v} = the UNITSTR of V
     by A3,A4,RLVECT_3:9,RUSUB_1:def 3;
   then {v} is Basis of V & Card {v} = 1 by CARD_1:79,RUSUB_3:def 2;
   hence dim V = 1 by Def3;
end;

theorem
  for V being finite-dimensional RealUnitarySpace holds
 dim V = 2 iff
  ex u,v being VECTOR of V st u <> v & {u, v} is linearly-independent &
   (Omega).V = Lin{u, v}
proof
   let V be finite-dimensional RealUnitarySpace;
   hereby
     consider I being finite Subset of V such that
A1:  I is Basis of V by Def2;
     assume dim V = 2;
then A2:  Card I = 2 by A1,Def3;
     then consider u being set such that
A3:  u in I by CARD_1:47,XBOOLE_0:def 1;
     reconsider u as VECTOR of V by A3;
       now
       assume I c= {u};
       then card I <= card {u} by CARD_1:80;
       then 2 <= 1 by A2,CARD_1:79;
       hence contradiction;
     end;
     then consider v being set such that
A4:  v in I & not v in {u} by TARSKI:def 3;
     reconsider v as VECTOR of V by A4;
A5:  v <> u by A4,TARSKI:def 1;

       for x being set st x in {u,v} holds x in I by A3,A4,TARSKI:def 2;
then A6:  {u, v} c= I by TARSKI:def 3;
       now
       assume not I c= {u, v};
       then consider w being set such that
A7:    w in I & not w in {u, v} by TARSKI:def 3;
A8:    w <> u & w <> v by A7,TARSKI:def 2;
         for x being set st x in {u,v,w} holds x in I
         by A3,A4,A7,ENUMSET1:13;
       then {u, v, w} c= I by TARSKI:def 3;
       then card {u, v, w} <= card I by CARD_1:80;
       then 3 <= 2 by A2,A5,A8,CARD_2:77;
       hence contradiction;
     end;
then A9:  I = {u, v} by A6,XBOOLE_0:def 10;
then A10: Lin{u, v} = the UNITSTR of V by A1,RUSUB_3:def 2
              .= (Omega).V by RUSUB_1:def 3;
       {u, v} is linearly-independent by A1,A9,RUSUB_3:def 2;
     hence ex u,v being VECTOR of V st u <> v & {u,v} is linearly-independent
&
     (Omega).V = Lin{u, v} by A5,A10;
   end;
   given u,v being VECTOR of V such that
A11:u <> v and
A12:{u, v} is linearly-independent and
A13:(Omega).V = Lin{u, v};
     Lin{u, v} = the UNITSTR of V by A13,RUSUB_1:def 3;
   then {u, v} is Basis of V & Card {u, v} = 2 by A11,A12,CARD_2:76,RUSUB_3:def
2;
   hence dim V = 2 by Def3;
end;

theorem Th15:
for V being finite-dimensional RealUnitarySpace, W1,W2 being Subspace of V
 holds
  dim(W1 + W2) + dim(W1 /\ W2) = dim W1 + dim W2
proof
   let V be finite-dimensional RealUnitarySpace;
   let W1,W2 be Subspace of V;
   reconsider V as RealUnitarySpace;
   reconsider W1, W2 as Subspace of V;

A1:W1 /\ W2 is finite-dimensional by Th7;
   then consider I being finite Subset of W1 /\ W2 such that
A2:I is Basis of W1 /\ W2 by Def2;
A3:Card I = dim(W1 /\ W2) by A1,A2,Def3;

     W1 /\ W2 is Subspace of W1 by RUSUB_2:16;
   then consider I1 being Basis of W1 such that
A4:I c= I1 by A2,RUSUB_3:24;
   reconsider I1 as finite Subset of W1 by Th3;

     W1 /\ W2 is Subspace of W2 by RUSUB_2:16;
   then consider I2 being Basis of W2 such that
A5:I c= I2 by A2,RUSUB_3:24;
   reconsider I2 as finite Subset of W2 by Th3;
A6:Card I2 = dim W2 by Def3;

A7:W1 + W2 is finite-dimensional by Th7;

   set A = I1 \/ I2;

     now
     let v be set;
     assume v in A;
then A8:  v in I1 or v in I2 by XBOOLE_0:def 2;
then A9:  v in the carrier of W1 or v in the carrier of W2;
       the carrier of W1 c= the carrier of V &
     the carrier of W2 c= the carrier of V by RUSUB_1:def 1;
     then reconsider v'= v as VECTOR of V by A9;
       v' in W1 or v' in W2 by A8,RLVECT_1:def 1;
     then v' in W1 + W2 by RUSUB_2:2;
     hence v in the carrier of W1 + W2 by RLVECT_1:def 1;
   end;
   then A c= the carrier of W1 + W2 & A is finite by TARSKI:def 3;
   then reconsider A as finite Subset of W1 + W2;

A10:I c= I1 /\ I2 by A4,A5,XBOOLE_1:19;
     now
     assume not I1 /\ I2 c= I;
     then consider x being set such that
A11: x in I1 /\ I2 and
A12: not x in I by TARSKI:def 3;
       x in I1 & x in I2 by A11,XBOOLE_0:def 3;
     then x in Lin(I1) & x in Lin(I2) by RUSUB_3:2;
     then x in the UNITSTR of W1 & x in the UNITSTR of W2
       by RUSUB_3:def 2;
then A13: x in the carrier of W1 & x in the carrier of W2 by RLVECT_1:def 1;
     then x in (the carrier of W1) /\ (the carrier of W2) by XBOOLE_0:def 3;
     then x in the carrier of W1 /\ W2 by RUSUB_2:def 2;
     then x in the UNITSTR of W1 /\ W2 by RLVECT_1:def 1;
then A14: x in Lin(I) by A2,RUSUB_3:def 2;

A15: the carrier of W1 c= the carrier of V by RUSUB_1:def 1;
     then reconsider x'= x as VECTOR of V by A13;

       I c= the carrier of W1 /\ W2 & the carrier of W1 /\ W2 c= the carrier of
V
       by RUSUB_1:def 1;
     then I c= the carrier of V by XBOOLE_1:1;
     then reconsider I'= I as Subset of V;
       now
       let y be set;
       assume y in I \/ {x};
then A16:   y in I or y in {x} by XBOOLE_0:def 2;
         I c= the carrier of W1 /\ W2 &
       the carrier of W1 /\ W2 c= the carrier of V by RUSUB_1:def 1;
       then I c= the carrier of V by XBOOLE_1:1;
       then y in the carrier of V or y = x by A16,TARSKI:def 1;
       hence y in the carrier of V by A13,A15;
     end;
     then I \/ {x} c= the carrier of V by TARSKI:def 3;
     then reconsider Ix = I \/ {x} as Subset of V;

       I1 is linearly-independent & I1 is Subset of W1
       by RUSUB_3:def 2;
     then consider I1' being Subset of V such that
A17: I1' is linearly-independent & I1'= I1 by RUSUB_3:22;
       now
       let y be set;
       assume y in I \/ {x};
       then y in I or y in {x} by XBOOLE_0:def 2;
       then y in I1 or y = x by A4,TARSKI:def 1;
       hence y in I1' by A11,A17,XBOOLE_0:def 3;
     end;
     then Ix c= I1' by TARSKI:def 3;
then A18: Ix is linearly-independent by A17,RLVECT_3:6;

       x in {x} by TARSKI:def 1;
then A19: x' in Ix by XBOOLE_0:def 2;

       Ix \ {x} = I \ {x} by XBOOLE_1:40
             .= I by A12,Lm2;
     then not x' in Lin(I') by A18,A19,RUSUB_3:25;
     hence contradiction by A14,RUSUB_3:28;
   end;
   then I = I1 /\ I2 by A10,XBOOLE_0:def 10;
then A20:Card A = Card I1 + Card I2 - Card I by CARD_2:64;

     A c= the carrier of W1 + W2 & the carrier of W1 + W2 c= the carrier of V
     by RUSUB_1:def 1;
   then A c= the carrier of V by XBOOLE_1:1;
   then reconsider A'= A as Subset of V;
A21: Lin(A') = Lin(A) by RUSUB_3:28;

     now
     let x be set;
     assume x in the carrier of W1 + W2;
     then x in W1 + W2 by RLVECT_1:def 1;
     then consider w1, w2 being VECTOR of V such that
A22: w1 in W1 and
A23: w2 in W2 and
A24: x = w1 + w2 by RUSUB_2:1;
     reconsider w1 as VECTOR of W1 by A22,RLVECT_1:def 1;
     reconsider w2 as VECTOR of W2 by A23,RLVECT_1:def 1;
       w1 in Lin(I1) by RUSUB_3:21;
     then consider K1 being Linear_Combination of I1 such that
A25: w1 = Sum(K1) by RUSUB_3:1;
     consider L1 being Linear_Combination of V such that
A26: Carrier(L1) = Carrier(K1) & Sum(L1) = Sum(K1) by RUSUB_3:19;

       w2 in Lin(I2) by RUSUB_3:21;
     then consider K2 being Linear_Combination of I2 such that
A27: w2 = Sum(K2) by RUSUB_3:1;
     consider L2 being Linear_Combination of V such that
A28: Carrier(L2) = Carrier(K2) & Sum(L2) = Sum(K2) by RUSUB_3:19;

     set L = L1 + L2;

       Carrier(L1) c= I1 & Carrier(L2) c= I2 by A26,A28,RLVECT_2:def 8;
     then Carrier(L) c= Carrier(L1) \/ Carrier(L2) &
     Carrier(L1) \/ Carrier(L2) c= I1 \/ I2 by RLVECT_2:58,XBOOLE_1:13;
     then Carrier(L) c= I1 \/ I2 by XBOOLE_1:1;
     then reconsider L as Linear_Combination of A' by RLVECT_2:def 8;

       x = Sum(L) by A24,A25,A26,A27,A28,RLVECT_3:1;
     then x in Lin(A') by RUSUB_3:1;
     hence x in the carrier of Lin(A') by RLVECT_1:def 1;
   end;
   then the carrier of W1 + W2 c= the carrier of Lin(A') by TARSKI:def 3;
   then W1 + W2 is Subspace of Lin(A') by RUSUB_1:22;
then A29: Lin(A) = W1 + W2 by A21,RUSUB_1:20;

     for L being Linear_Combination of A st Sum(L) = 0.(W1 + W2)
    holds Carrier(L) = {}
   proof
     let L be Linear_Combination of A;
     assume
A30: Sum(L) = 0.(W1 + W2);

A31: W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 by RUSUB_2:7;
     reconsider W1'= W1 as Subspace of W1 + W2 by RUSUB_2:7;
     reconsider W2'= W2 as Subspace of W1 + W2 by RUSUB_2:7;
A32: Carrier(L) c= I1 \/ I2 by RLVECT_2:def 8;

     consider F being FinSequence of the carrier of W1 + W2 such that
A33: F is one-to-one and
A34: rng F = Carrier(L) and
A35: Sum(L) = Sum(L (#) F) by RLVECT_2:def 10;

     set B = Carrier(L) /\ I1;
     reconsider B as Subset of rng F by A34,XBOOLE_1:17;

     consider P being Permutation of dom F such that
A36: (F - B`) ^ (F - B) = F*P by A33,MATRLIN:8;

     reconsider F1 = F - B`, F2 = F - B
      as FinSequence of the carrier of W1 + W2 by FINSEQ_3:93;
A37: F1 is one-to-one & F2 is one-to-one by A33,FINSEQ_3:94;

     consider L1 being Linear_Combination of W1 + W2 such that
A38: Carrier(L1) = rng F1 /\ Carrier(L) and
A39: L1 (#) F1 = L (#) F1 by RLVECT_5:8;
       Carrier(L1) c= rng F1 by A38,XBOOLE_1:17;
then A40: Sum(L (#) F1) = Sum(L1) by A37,A39,RLVECT_5:7;

       rng F c= rng F;
     then reconsider X = rng F as Subset of rng F;
       X \ B` = X /\ B`` by SUBSET_1:32
           .= B by XBOOLE_1:28;
     then rng F1 = B by FINSEQ_3:72;
then A41: Carrier(L1) = I1 /\ (Carrier(L) /\ Carrier(L)) by A38,XBOOLE_1:16
                .= Carrier(L) /\ I1;
then A42: Carrier(L1) c= I1 & I1 c= the carrier of W1 by XBOOLE_1:17;
     then Carrier(L1) c= the carrier of W1' by XBOOLE_1:1;
     then consider K1 being Linear_Combination of W1' such that
       Carrier(K1) = Carrier(L1) and
A43: Sum(K1) = Sum(L1) by RUSUB_3:20;

     consider L2 being Linear_Combination of W1 + W2 such that
A44: Carrier(L2) = rng F2 /\ Carrier(L) and
A45: L2 (#) F2 = L (#) F2 by RLVECT_5:8;
       Carrier(L2) c= rng F2 by A44,XBOOLE_1:17;
then A46: Sum(L (#) F2) = Sum(L2) by A37,A45,RLVECT_5:7;

A47: Carrier(L) \ I1 c= Carrier(L) by XBOOLE_1:36;
       rng F2 = Carrier(L) \ (Carrier(L) /\ I1) by A34,FINSEQ_3:72
           .= Carrier(L) \ I1 by XBOOLE_1:47;
then A48: Carrier(L2) = Carrier(L) \ I1 by A44,A47,XBOOLE_1:28;
     then Carrier(L2) c= I2 & I2 c= the carrier of W2 by A32,XBOOLE_1:43;
     then Carrier(L2) c= the carrier of W2' by XBOOLE_1:1;
     then consider K2 being Linear_Combination of W2' such that
       Carrier(K2) = Carrier(L2) and
A49: Sum(K2) = Sum(L2) by RUSUB_3:20;

A50: 0.(W1 + W2) = Sum(L (#) (F1^F2)) by A30,A35,A36,RLVECT_5:5
                .= Sum((L (#) F1) ^ (L (#) F2)) by RLVECT_3:41
                .= Sum(L1) + Sum(L2) by A40,A46,RLVECT_1:58;
     then Sum(L1) = - Sum(L2) by RLVECT_1:def 10
            .= - Sum(K2) by A49,RUSUB_1:9;
     then Sum(K1) in W2 & Sum(K1) in W1 by A43,RLVECT_1:def 1;
     then Sum(K1) in W1 /\ W2 by RUSUB_2:3;
     then Sum(K1) in Lin(I) by A2,RUSUB_3:def 2;
     then consider KI being Linear_Combination of I such that
A51: Sum(K1) = Sum(KI) by RUSUB_3:1;
       W1 /\ W2 is Subspace of W1 + W2 by RUSUB_2:22;
     then consider LI being Linear_Combination of W1 + W2 such that
A52: Carrier(LI) = Carrier(KI) and
A53: Sum(LI) = Sum(KI) by RUSUB_3:19;

A54: Carrier(LI + L2) c= Carrier(LI) \/ Carrier(L2) by RLVECT_2:58;
A55: I \/ I2 = I2 by A5,XBOOLE_1:12;
       Carrier(LI) c= I & Carrier(L2) c= I2
       by A32,A48,A52,RLVECT_2:def 8,XBOOLE_1:43;
     then Carrier(LI) \/ Carrier(L2) c= I2 by A55,XBOOLE_1:13;
then A56: Carrier(LI + L2) c= I2 & I2 c= the carrier of W2 by A54,XBOOLE_1:1;
     then Carrier(LI + L2) c= the carrier of W2 by XBOOLE_1:1;
     then consider K being Linear_Combination of W2 such that
A57: Carrier(K) = Carrier(LI + L2) and
A58: Sum(K) = Sum(LI + L2) by A31,RUSUB_3:20;
     reconsider K as Linear_Combination of I2 by A56,A57,RLVECT_2:def 8;

       I1 is Subset of W1 & I1 is linearly-independent
       by RUSUB_3:def 2;
     then consider I1' being Subset of W1 + W2 such that
A59: I1' is linearly-independent & I1'= I1 by A31,RUSUB_3:22;
       Carrier(LI) c= I by A52,RLVECT_2:def 8;
     then Carrier(LI) c= I1' by A4,A59,XBOOLE_1:1;
then A60: LI = L1 by A42,A43,A51,A53,A59,RLVECT_5:1;

A61: I2 is linearly-independent by RUSUB_3:def 2;

       0.W2 = Sum(LI) + Sum(L2) by A43,A50,A51,A53,RUSUB_1:5
         .= Sum(K) by A58,RLVECT_3:1;
then A62: {} = Carrier(L1 + L2) by A57,A60,A61,RLVECT_3:def 1;
A63: Carrier(L) = Carrier(L1) \/ Carrier(L2) by A41,A48,XBOOLE_1:51;

A64: I1 misses (Carrier(L) \ I1) by XBOOLE_1:79;
       Carrier(L1) /\ Carrier(L2)
              = Carrier(L) /\ (I1 /\ (Carrier(L) \ I1)) by A41,A48,XBOOLE_1:16
             .= Carrier(L) /\ {} by A64,XBOOLE_0:def 7
             .= {};
then A65: Carrier(L1) misses Carrier(L2) by XBOOLE_0:def 7;
       now assume not Carrier(L) c= Carrier(L1 + L2);
     then consider x being set such that
A66: x in Carrier(L) and
A67: not x in Carrier(L1 + L2) by TARSKI:def 3;
     reconsider x as VECTOR of W1 + W2 by A66;
A68: 0 = (L1 + L2).x by A67,RLVECT_2:28
           .= L1.x + L2.x by RLVECT_2:def 12;
     per cases by A63,A66,XBOOLE_0:def 2;

       suppose
A69:   x in Carrier(L1);
       then consider v being VECTOR of W1 + W2 such that
A70:   x = v & L1.v <> 0 by RLVECT_5:3;
         not x in Carrier(L2) by A65,A69,XBOOLE_0:3;
       then L2.x = 0 by RLVECT_2:28;
       hence contradiction by A68,A70;

       suppose
A71:   x in Carrier(L2);
       then consider v being VECTOR of W1 + W2 such that
A72:   x = v & L2.v <> 0 by RLVECT_5:3;
         not x in Carrier(L1) by A65,A71,XBOOLE_0:3;
       then L1.x = 0 by RLVECT_2:28;
       hence contradiction by A68,A72;
     end;
     hence Carrier(L) = {} by A62,XBOOLE_1:3;
   end;
   then A is linearly-independent by RLVECT_3:def 1;
   then A is Basis of W1 + W2 by A29,RUSUB_3:def 2;
   then Card A = dim(W1 + W2) by A7,Def3;
   then dim(W1 + W2) + dim(W1 /\ W2)
           = Card I1 + Card I2 + - Card I + Card I by A3,A20,XCMPLX_0:def 8
          .= Card I1 + Card I2 + (- Card I + Card I) by XCMPLX_1:1
          .= Card I1 + Card I2 + 0 by XCMPLX_0:def 6
          .= dim W1 + dim W2 by A6,Def3;
   hence thesis;
end;

theorem
  for V being finite-dimensional RealUnitarySpace,
 W1,W2 being Subspace of V holds
  dim(W1 /\ W2) >= dim W1 + dim W2 - dim V
proof
   let V be finite-dimensional RealUnitarySpace;
   let W1,W2 be Subspace of V;
A1:dim W1 + dim W2 - dim V = dim(W1 + W2) + dim(W1 /\ W2) - dim V by Th15
                       .= dim(W1 + W2) + (dim(W1 /\ W2) - dim V) by XCMPLX_1:29
;
A2:dim(W1 + W2) <= dim V by Th8;
     dim V + (dim(W1 /\ W2) - dim V)
            = dim V + (dim(W1 /\ W2) + -dim V) by XCMPLX_0:def 8
           .= dim(W1 /\ W2) + (dim V + -dim V) by XCMPLX_1:1
           .= dim(W1 /\ W2) + 0 by XCMPLX_0:def 6
           .= dim(W1 /\ W2);
  hence thesis by A1,A2,AXIOMS:24;
end;

theorem
  for V being finite-dimensional RealUnitarySpace,
 W1,W2 being Subspace of V st
  V is_the_direct_sum_of W1, W2 holds dim V = dim W1 + dim W2
proof
   let V be finite-dimensional RealUnitarySpace;
   let W1,W2 be Subspace of V;
   assume V is_the_direct_sum_of W1, W2;
then A1:the UNITSTR of V = W1 + W2 & W1 /\ W2 = (0).V by RUSUB_2:def 4;
   then (Omega).(W1 /\ W2) = (0).V by RUSUB_1:def 3
                .= (0).(W1 /\ W2) by RUSUB_1:30;
   then dim(W1 /\ W2) = 0 by Th12;
   then dim W1 + dim W2 = dim(W1 + W2) + 0 by Th15
                  .= dim (Omega).V by A1,RUSUB_1:def 3
                  .= dim V by Th10;
   hence dim V = dim W1 + dim W2;
end;

begin   :: Fixed-dimensional subspace family

Lm3:
for V being finite-dimensional RealUnitarySpace, n being Nat st
  n <= dim V holds ex W being strict Subspace of V st dim W = n
proof
   let V be finite-dimensional RealUnitarySpace;
   let n be Nat;
   assume
A1:n <= dim V;
   consider I being finite Subset of V such that
A2:I is Basis of V by Def2;
     n <= Card I by A1,A2,Def3;
   then consider A being finite Subset of I such that
A3:Card A = n by VECTSP_9:1;
     A c= the carrier of V by XBOOLE_1:1;
   then reconsider A as Subset of V;
   reconsider W = Lin(A) as strict finite-dimensional Subspace of V;
     I is linearly-independent by A2,RUSUB_3:def 2;
   then A is linearly-independent by RLVECT_3:6;
   then dim W = n by A3,Th9;
   hence thesis;
end;

theorem
  for V being finite-dimensional RealUnitarySpace, W being Subspace of V,
 n being Nat holds
  n <= dim V iff ex W being strict Subspace of V st dim W = n
by Lm3,Th8;

definition
let V be finite-dimensional RealUnitarySpace, n be Nat;
  func n Subspaces_of V -> set means
:Def4:
  for x being set holds x in it
   iff ex W being strict Subspace of V st W = x & dim W = n;
existence
proof
   set S = {Lin(A) where A is Subset of V:
             A is linearly-independent & Card A = n};
A1:  for x being set holds x in S
       iff ex W being strict Subspace of V st W = x & dim W = n
     proof
       let x be set;
       hereby assume x in S;
         then consider A being Subset of V such that
A2:      x = Lin(A) and
A3:      A is linearly-independent and
A4:      Card A = n;
         reconsider W = x as strict Subspace of V by A2;
           dim W = n by A2,A3,A4,Th9;
         hence ex W being strict Subspace of V st W = x & dim W = n;
       end;
       given W being strict Subspace of V such that
A5:    W = x and
A6:    dim W = n;
       consider A being finite Subset of W such that
A7:    A is Basis of W by Def2;
       reconsider A as Subset of W;
         A is linearly-independent by A7,RUSUB_3:def 2;
       then consider B being Subset of V such that
A8:    B is linearly-independent and
A9:    B = A by RUSUB_3:22;
A10:   x = Lin(A) by A5,A7,RUSUB_3:def 2
        .= Lin(B) by A9,RUSUB_3:28;
       then Card B = n by A5,A6,A8,Th9;
       hence x in S by A8,A10;
     end;
     take S;
     thus thesis by A1;
end;
uniqueness
  proof
    defpred P[set] means
     ex W being strict Subspace of V st W = $1 & dim W = n;
  for X1,X2 being set st
   (for x being set holds x in X1 iff P[x]) &
   (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
   hence thesis;
  end;
end;

theorem
  for V being finite-dimensional RealUnitarySpace, n being Nat st
  n <= dim V holds n Subspaces_of V is non empty
proof
   let V be finite-dimensional RealUnitarySpace;
   let n be Nat;
   assume n <= dim V;
   then consider W being strict Subspace of V such that
A1:dim W = n by Lm3;
   thus n Subspaces_of V is non empty by A1,Def4;
end;

theorem
  for V being finite-dimensional RealUnitarySpace, n being Nat st
 dim V < n holds n Subspaces_of V = {}
proof
   let V be finite-dimensional RealUnitarySpace;
   let n be Nat;
   assume that
A1:dim V < n and
A2:n Subspaces_of V <> {};
   consider x being set such that
A3:x in n Subspaces_of V by A2,XBOOLE_0:def 1;
   consider W being strict Subspace of V such that
     W = x and
A4:dim W = n by A3,Def4;
   thus contradiction by A1,A4,Th8;
end;

theorem
  for V being finite-dimensional RealUnitarySpace, W being Subspace of V,
 n being Nat holds
  n Subspaces_of W c= n Subspaces_of V
proof
   let V be finite-dimensional RealUnitarySpace;
   let W be Subspace of V;
   let n be Nat;
   let x be set;
   assume x in n Subspaces_of W;
   then consider W1 being strict Subspace of W such that
A1:W1 = x and
A2:dim W1 = n by Def4;
   reconsider W1 as strict Subspace of V by RUSUB_1:21;
     W1 in n Subspaces_of V by A2,Def4;
   hence x in n Subspaces_of V by A1;
end;

begin  :: Affine set

definition
let V be non empty RLSStruct, S be Subset of V;
  attr S is Affine means
:Def5:
  for x,y being VECTOR of V, a being Real st
   x in S & y in S holds (1 - a) * x + a * y in S;
end;

theorem Th22:
for V being non empty RLSStruct holds [#]V is Affine & {}V is Affine
proof
   let V be non empty RLSStruct;
     for x,y being VECTOR of V, a being Real st x in [#]V & y in [#]V
   holds (1-a) * x + a * y in [#]V by PRE_TOPC:13;
   hence [#]V is Affine by Def5;
     for x,y being VECTOR of V, a being Real st x in {}V & y in {}V
   holds (1-a) * x + a * y in {}V;
   hence thesis by Def5;
end;

theorem
  for V being RealLinearSpace-like (non empty RLSStruct),
 v being VECTOR of V holds {v} is Affine
proof
   let V be RealLinearSpace-like (non empty RLSStruct);
   let v be VECTOR of V;
     for x,y being VECTOR of V, a being Real st
    x in {v} & y in {v} holds (1-a)*x + a*y in {v}
   proof
     let x,y being VECTOR of V;
     let a be Real;
     assume x in {v} & y in {v};
     then x = v & y = v by TARSKI:def 1;
     then (1-a)*x + a*y = ((1-a)+a)*v by RLVECT_1:def 9
                  .= (1-(a-a))*v by XCMPLX_1:37
                  .= (1-0)*v by XCMPLX_1:14
                  .= v by RLVECT_1:def 9;
    hence thesis by TARSKI:def 1;
   end;
   hence thesis by Def5;
end;

definition
let V be non empty RLSStruct;
cluster non empty Affine Subset of V;
existence
proof
   take [#]V;
   thus thesis by Th22;
end;

cluster empty Affine Subset of V;
existence
proof
   take {}V;
   thus thesis by Th22;
end;
end;

definition
let V be RealLinearSpace, W be Subspace of V;
  func Up(W) -> non empty Subset of V equals
:Def6:
   the carrier of W;
coherence by RLSUB_1:def 2;
end;

definition
let V be RealUnitarySpace, W be Subspace of V;
  func Up(W) -> non empty Subset of V equals
:Def7:
  the carrier of W;
coherence by RUSUB_1:def 1;
end;

theorem
  for V being RealLinearSpace, W being Subspace of V holds
Up(W) is Affine & 0.V in the carrier of W
proof
   let V be RealLinearSpace;
   let W be Subspace of V;

     for x,y being VECTOR of V, a being Real st x in Up(W) & y in Up(W)
   holds (1 - a) * x + a * y in Up(W)
   proof
     let x,y be VECTOR of V;
     let a be Real;
     assume x in Up(W) & y in Up(W);
     then x in the carrier of W & y in the carrier of W by Def6;
     then x in W & y in W by RLVECT_1:def 1;
then (1 - a) * x in W & a * y in W by RLSUB_1:29;
then A1:  (1 - a) * x + a * y in W by RLSUB_1:28;
     reconsider z = (1 - a) * x + a * y as VECTOR of V;
       z in the carrier of W by A1,RLVECT_1:def 1;
     hence thesis by Def6;
   end;
   hence Up(W) is Affine by Def5;
     0.V in W by RLSUB_1:25;
   hence thesis by RLVECT_1:def 1;
end;

theorem Th25:
for V being RealLinearSpace, A being Affine Subset of V st
0.V in A holds for x being VECTOR of V, a being Real st x in A holds a * x in A
proof
   let V be RealLinearSpace;
   let A be Affine Subset of V;
   assume
A1:0.V in A;
     for x being VECTOR of V, a being Real st x in A holds a * x in A
   proof
     let x be VECTOR of V;
     let a be Real;
     assume x in A;
     then (1-a) * 0.V + a * x in A by A1,Def5;
     then 0.V + a * x in A by RLVECT_1:23;
     hence thesis by RLVECT_1:10;
   end;
   hence thesis;
end;

definition
let V be non empty RLSStruct, S be non empty Subset of V;
  attr S is Subspace-like means
:Def8:
  the Zero of V in S &
  for x,y being Element of V, a being Real st x in S & y in S
  holds x + y in S & a * x in S;
end;

theorem Th26:
for V being RealLinearSpace, A being non empty Affine Subset of V st
0.V in A holds
A is Subspace-like & A = the carrier of Lin(A)
proof
   let V be RealLinearSpace;
   let A be non empty Affine Subset of V;
   assume
A1:0.V in A;
then A2:the Zero of V in A by RLVECT_1:def 2;
A3:for x,y being Element of V, a being Real st x in A & y in A
   holds x + y in A & a * x in A
   proof
     let x,y be Element of V;
     let a be Real;
     assume
A4:  x in A & y in A;
     reconsider x,y as VECTOR of V;
A5:  (1 - 1/2) * x + (1/2) * y in A by A4,Def5;
       2 * ( (1-1/2) * x + (1/2) * y )
         = 2*( (1-1/2) * x) + 2*((1/2) * y) by RLVECT_1:def 9
        .= ( 2*(1-1/2) ) * x + 2*((1/2) * y) by RLVECT_1:def 9
        .= ( 2 - 1 ) * x + ( 2*(1/2) ) * y by RLVECT_1:def 9
        .= x + 1 * y by RLVECT_1:def 9
        .= x + y by RLVECT_1:def 9;
     hence thesis by A1,A4,A5,Th25;
   end;
   hence
     A is Subspace-like by A2,Def8;

     for x being set st x in A holds x in the carrier of Lin(A)
   proof
     let x be set;
     assume x in A;
     then x in Lin(A) by RLVECT_3:18;
     hence thesis by RLVECT_1:def 1;
   end;
then A6:A c= the carrier of Lin(A) by TARSKI:def 3;
     for x being set st x in the carrier of Lin(A) holds x in A
   proof
     let x be set;
     assume x in the carrier of Lin(A);
     then x in Lin(A) by RLVECT_1:def 1;
     then consider l being Linear_Combination of A such that
A7:  x = Sum(l) by RLVECT_3:17;

A8:  for v,u being VECTOR of V st v in A & u in A holds v + u in A by A3;
       for a being Real, v being VECTOR of V st v in A holds a * v in A
       by A3;
     then A is lineary-closed by A8,RLSUB_1:def 1;

     hence x in A by A7,RLVECT_2:47;
   end;
   then the carrier of Lin(A) c= A by TARSKI:def 3;
   hence thesis by A6,XBOOLE_0:def 10;
end;

theorem
  for V being RealLinearSpace, W being Subspace of V holds
Up(W) is Subspace-like
proof
   let V be RealLinearSpace;
   let W be Subspace of V;
     0.V in W by RLSUB_1:25;
   then 0.V in the carrier of W by RLVECT_1:def 1;
   then 0.V in Up(W) by Def6;
   hence the Zero of V in Up(W) by RLVECT_1:def 2;
   thus for x,y being Element of V, a being Real st
        x in Up(W) & y in Up(W) holds x + y in Up(W) & a * x in Up(W)
   proof
     let x,y be Element of V;
     let a be Real;
     assume
       x in Up(W) & y in Up(W);
then A1:  x in the carrier of W &
     y in the carrier of W by Def6;
     reconsider x,y as Element of V;
       x in W & y in W by A1,RLVECT_1:def 1;
     then x + y in W & a * x in W by RLSUB_1:28,29;
     then x + y in the carrier of W & a * x in the carrier of W by RLVECT_1:def
1;
     hence thesis by Def6;
   end;
end;

theorem
  for V being RealLinearSpace, W being strict Subspace of V holds
W = Lin(Up(W))
proof
   let V be RealLinearSpace;
   let W be strict Subspace of V;
     Up(W) = the carrier of W by Def6;
   hence thesis by RLVECT_3:21;
end;

theorem
  for V being RealUnitarySpace, A being non empty Affine Subset of V st
0.V in A holds
A = the carrier of Lin(A)
proof
   let V be RealUnitarySpace;
   let A be non empty Affine Subset of V;
   assume
     0.V in A;
then A1:A is Subspace-like by Th26;

     for x being set st x in A holds x in the carrier of Lin(A)
   proof
     let x be set;
     assume x in A;
     then x in Lin(A) by RUSUB_3:2;
     hence thesis by RLVECT_1:def 1;
   end;
then A2:A c= the carrier of Lin(A) by TARSKI:def 3;
     for x being set st x in the carrier of Lin(A) holds x in A
   proof
     let x be set;
     assume x in the carrier of Lin(A);
     then x in Lin(A) by RLVECT_1:def 1;
     then consider l being Linear_Combination of A such that
A3:  x = Sum(l) by RUSUB_3:1;

A4:  for v,u being VECTOR of V st v in A & u in A holds v + u in A by A1,Def8;
       for a being Real, v being VECTOR of V st v in A holds a * v in A
       by A1,Def8;
     then A is lineary-closed by A4,RLSUB_1:def 1;

     hence x in A by A3,RLVECT_2:47;
   end;
   then the carrier of Lin(A) c= A by TARSKI:def 3;
   hence thesis by A2,XBOOLE_0:def 10;
end;

theorem
  for V being RealUnitarySpace, W being Subspace of V holds
Up(W) is Subspace-like proof
   let V be RealUnitarySpace;
   let W be Subspace of V;
     0.V in W by RUSUB_1:11;
   then 0.V in the carrier of W by RLVECT_1:def 1;
   then 0.V in Up(W) by Def7;
   hence the Zero of V in Up(W) by RLVECT_1:def 2;
   thus for x,y being Element of V, a being Real st
        x in Up(W) & y in Up(W) holds x + y in Up(W) & a * x in Up(W)
   proof
     let x,y be Element of V;
     let a be Real;
     assume
       x in Up(W) & y in Up(W);
then A1:  x in the carrier of W &
     y in the carrier of W by Def7;
     reconsider x,y as Element of V;
       x in W & y in W by A1,RLVECT_1:def 1;
     then x + y in W & a * x in W by RUSUB_1:14,15;
     then x + y in the carrier of W & a * x in the carrier of W by RLVECT_1:def
1;
     hence thesis by Def7;
   end;
end;

theorem
  for V being RealUnitarySpace, W being strict Subspace of V holds
W = Lin(Up(W))
proof
   let V be RealUnitarySpace;
   let W be strict Subspace of V;
     Up(W) = the carrier of W by Def7;
   hence thesis by RUSUB_3:5;
end;

definition
let V be non empty LoopStr, M be Subset of V,
 v be Element of V;
  func v + M -> Subset of V equals
:Def9:
  {v + u where u is Element of V: u in M};
coherence
proof
  defpred P[set] means
    ex u being Element of V st $1 = v + u & u in M;
   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;
   reconsider X as Subset of V;
   set Y = {v + u where u is Element of V: u in M};
     X = Y
   proof
     thus X c= Y
     proof
       let x be set;
       assume x in X;
       then ex u being Element of V st x = v + u & u in M by A1
;
       hence thesis;
     end;
     thus Y c= X
     proof
       let x be set;
       assume x in Y;
       then ex u being Element of V st x = v + u & u in M;
       hence thesis by A1;
     end;
   end;
   hence thesis;
end;
end;

theorem
  for V being RealLinearSpace, W being strict Subspace of V,
 M being Subset of V, v being VECTOR of V st
  Up(W) = M holds v + W = v + M
proof
   let V be RealLinearSpace;
   let W be strict Subspace of V;
   let M be Subset of V;
   let v be VECTOR of V;
   assume Up(W) = M;
then A1:the carrier of W = M by Def6;
     for x being set st x in v + W holds x in v + M
   proof
     let x be set;
     assume x in v + W;
     then x in {v + u where u is VECTOR of V : u in W} by RLSUB_1:def 5;
     then consider u being VECTOR of V such that
A2:  x = v + u & u in W;
       u in M by A1,A2,RLVECT_1:def 1;
     then x in {v + u' where u' is Element of V : u' in M}
       by A2;
     hence thesis by Def9;
   end;
then A3:v + W c= v + M by TARSKI:def 3;
     for x being set st x in v + M holds x in v + W
   proof
     let x be set;
     assume x in v + M;
     then x in {v + u where u is Element of V : u in M} by Def9
;
     then consider u being Element of V such that
A4:  x = v + u & u in M;
       u in W by A1,A4,RLVECT_1:def 1;
     then x in {v + u' where u' is VECTOR of V : u' in W} by A4;
     hence thesis by RLSUB_1:def 5;
   end;
   then v + M c= v + W by TARSKI:def 3;
   hence thesis by A3,XBOOLE_0:def 10;
end;

theorem Th33:
for V being Abelian add-associative
 RealLinearSpace-like (non empty RLSStruct),
  M being Affine Subset of V, v being VECTOR of V
   holds v + M is Affine
proof
   let V be Abelian add-associative RealLinearSpace-like (non empty RLSStruct);
   let M be Affine Subset of V;
   let v be VECTOR of V;
     for x,y being VECTOR of V, a being Real st x in v + M & y in v + M holds
    (1-a)*x + a*y in v + M
   proof
     let x,y be VECTOR of V;
     let a be Real;
     assume x in v + M & y in v + M;
then A1:  x in {v + u where u is Element of V : u in M} &
     y in {v + u where u is Element of V : u in M} by Def9;
     then consider x' being Element of V such that
A2:  x = v + x' & x' in M;
     consider y' being Element of V such that
A3:  y = v + y' & y' in M by A1;
A4:  (1 - a) * x' + a * y' in M by A2,A3,Def5;
       (1 - a) * x + a * y = (1-a)*v + (1-a)*x' + a * (v + y') by A2,A3,
RLVECT_1:def 9
       .= (1-a)*v + (1-a)*x' + (a*v + a*y') by RLVECT_1:def 9
       .= (1-a)*v + (1-a)*x' + a*v + a*y' by RLVECT_1:def 6
       .= (1-a)*x' + ((1-a)*v + a*v) + a*y' by RLVECT_1:def 6
       .= (1-a)*x' + (1-a+a)*v + a*y' by RLVECT_1:def 9
       .= (1-a)*x' + (1-(a-a))*v + a*y' by XCMPLX_1:37
       .= (1-a)*x' + 1*v + a*y' by XCMPLX_1:17
       .= (1-a)*x' + v + a*y' by RLVECT_1:def 9
       .= v + ((1-a)*x' + a*y') by RLVECT_1:def 6;
     then (1 - a) * x + a * y in {v + u where u is Element of V
                              : u in M} by A4;
     hence thesis by Def9;
   end;
   hence thesis by Def5;
end;

theorem
  for V being RealUnitarySpace, W being strict Subspace of V,
 M being Subset of V, v being VECTOR of V st
  Up(W) = M holds v + W = v + M
proof
   let V be RealUnitarySpace;
   let W be strict Subspace of V;
   let M be Subset of V;
   let v be VECTOR of V;
   assume Up(W) = M;
then A1:the carrier of W = M by Def7;
     for x being set st x in v + W holds x in v + M
   proof
     let x be set;
     assume x in v + W;
     then x in {v + u where u is VECTOR of V : u in W} by RUSUB_1:def 4;
     then consider u being VECTOR of V such that
A2:  x = v + u & u in W;
       u in M by A1,A2,RLVECT_1:def 1;
     then x in {v + u' where u' is Element of V : u' in M}
       by A2;
     hence thesis by Def9;
   end;
then A3:v + W c= v + M by TARSKI:def 3;
     for x being set st x in v + M holds x in v + W
   proof
     let x be set;
     assume x in v + M;
     then x in {v + u where u is Element of V : u in M} by Def9
;
     then consider u being Element of V such that
A4:  x = v + u & u in M;
       u in W by A1,A4,RLVECT_1:def 1;
     then x in {v + u' where u' is VECTOR of V : u' in W} by A4;
     hence thesis by RUSUB_1:def 4;
   end;
   then v + M c= v + W by TARSKI:def 3;
   hence thesis by A3,XBOOLE_0:def 10;
end;

definition
let V be non empty LoopStr,
M,N be Subset of V;
func M + N -> Subset of V equals
:Def10:
  {u + v where u,v is Element of V: u in M & v in N};
coherence
proof
  deffunc F(Element of V,Element of V) = $1+$2;
  defpred P[set,set] means $1 in M & $2 in N;
  {F(u,v) where u,v is Element of V : P[u,v]}
    is Subset of V from SubsetFD2;
   hence thesis;
end;
end;

theorem Th35:
for V be Abelian (non empty LoopStr), M,N be Subset of V holds
N + M = M + N
proof
   let V be Abelian (non empty LoopStr);
   let M,N be Subset of V;
     for x being set st x in N + M holds x in M + N
   proof
     let x be set;
     assume x in N + M;
     then x in {u + v where u,v is Element of V: u in N & v in
M}
       by Def10;
     then consider u1,v1 being Element of V such that
A1:  x = u1 + v1 & u1 in N & v1 in M;
       x in {u + v where u,v is Element of V: u in M & v in N}
       by A1;
     hence thesis by Def10;
   end;
then A2:N + M c= M + N by TARSKI:def 3;
     for x being set st x in M + N holds x in N + M
   proof
     let x be set;
     assume x in M + N;
     then x in {u + v where u,v is Element of V: u in M & v in
N}
       by Def10;
     then consider u1,v1 being Element of V such that
A3:  x = u1 + v1 & u1 in M & v1 in N;
       x in {u + v where u,v is Element of V: u in N & v in M}
       by A3;
     hence thesis by Def10;
   end;
   then M + N c= N + M by TARSKI:def 3;
   hence thesis by A2,XBOOLE_0:def 10;
end;

definition
let V be Abelian (non empty LoopStr), M,N be Subset of V;
redefine func M + N;
commutativity by Th35;
end;

theorem Th36:
for V being non empty LoopStr, M being Subset of V,
 v being Element of V holds {v} + M = v + M
proof
   let V be non empty LoopStr;
   let M be Subset of V;
   let v be Element of V;
     for x being set st x in {v} + M holds x in v + M
   proof
     let x be set;
     assume x in {v} + M;
     then x in {v1 + u1 where v1,u1 is Element of V
           : v1 in {v} & u1 in M} by Def10;
     then consider v1,u1 being Element of V such that
A1:  x = v1 + u1 & v1 in {v} & u1 in M;
       v1 = v by A1,TARSKI:def 1;
     then x in {v + u' where u' is Element of V: u' in M} by A1
;
     hence thesis by Def9;
   end;
then A2:{v} + M c= v + M by TARSKI:def 3;
     for x being set st x in v + M holds x in {v} + M
   proof
     let x be set;
     assume x in v + M;
     then x in {v + u where u is Element of V: u in M} by Def9;
     then consider u being Element of V such that
A3:  x = v + u & u in M;
       v in {v} by TARSKI:def 1;
     then x in {v1 + u1 where v1,u1 is Element of V
           : v1 in {v} & u1 in M} by A3;
     hence thesis by Def10;
   end;
   then v + M c= {v} + M by TARSKI:def 3;
   hence thesis by A2,XBOOLE_0:def 10;
end;

theorem
  for V being Abelian add-associative
 RealLinearSpace-like (non empty RLSStruct),
  M being Affine Subset of V, v being VECTOR of V
   holds {v} + M is Affine
proof
   let V be Abelian add-associative
            RealLinearSpace-like (non empty RLSStruct);
   let M be Affine Subset of V;
   let v be VECTOR of V;
     {v} + M = v + M by Th36;
   hence thesis by Th33;
end;

theorem
  for V being non empty RLSStruct, M,N being Affine Subset of V holds
 M /\ N is Affine
proof
   let V be non empty RLSStruct;
   let M,N be Affine Subset of V;
     for x,y being VECTOR of V, a being Real st x in M /\ N & y in M /\ N
   holds
    (1 - a) * x + a * y in M /\ N
   proof
     let x,y be VECTOR of V;
     let a be Real;
     assume x in M /\ N & y in M /\ N;
     then x in M & x in N & y in M & y in N by XBOOLE_0:def 3;
     then (1 - a) * x + a * y in M & (1 - a) * x + a * y in N by Def5;
     hence thesis by XBOOLE_0:def 3;
   end;
   hence thesis by Def5;
end;

theorem
  for V being Abelian add-associative
 RealLinearSpace-like (non empty RLSStruct),
  M,N being Affine Subset of V holds
   M + N is Affine
proof
   let V be Abelian add-associative
            RealLinearSpace-like (non empty RLSStruct);
   let M,N be Affine Subset of V;
     for x,y being VECTOR of V, a being Real st x in M + N & y in M + N
   holds
    (1 - a) * x + a * y in M + N
   proof
     let x,y be VECTOR of V;
     let a be Real;
     assume x in M + N & y in M + N;
then A1:  x in {u + v where u,v is Element of V: u in M & v in N
} &
     y in {u + v where u,v is Element of V: u in M & v in N}
       by Def10;
     then consider u1,v1 being Element of V such that
A2:  x = u1 + v1 & u1 in M & v1 in N;
     consider u2,v2 being Element of V such that
A3:  y = u2 + v2 & u2 in M & v2 in N by A1;
A4:  (1 - a) * u1 + a * u2 in M by A2,A3,Def5;
A5:  (1 - a) * v1 + a * v2 in N by A2,A3,Def5;
       (1 - a) * x + a * y
       = (1 - a) * u1 + (1 - a) * v1 + a * (u2 + v2) by A2,A3,RLVECT_1:def 9
      .= (1 - a) * u1 + (1 - a) * v1 + ( a * u2 + a * v2 ) by RLVECT_1:def 9
      .= (1 - a) * u1 + (1 - a) * v1 + a * u2 + a * v2 by RLVECT_1:def 6
      .= (1 - a) * v1 + ((1 - a) * u1 + a * u2) + a * v2 by RLVECT_1:def 6
      .= ((1 - a) * u1 + a * u2) + ((1 - a) * v1 + a * v2)
        by RLVECT_1:def 6;
     then (1 - a) * x + a * y
       in {u + v where u,v is Element of V: u in M & v in N}
       by A4,A5;
     hence thesis by Def10;
   end;
   hence thesis by Def5;
end;

Back to top