The abstract of the Mizar article:

Linear Combinations in Real Unitary Space

by

Noboru Endou,

Takashi Mitsuishi, and

Yasunari Shidama

Received October 9, 2002

MML identifier: RUSUB_3

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2, FINSEQ_1, FUNCT_1, ORDERS_1,
      SEQ_1, RELAT_1, FINSEQ_4, BOOLE, FUNCT_2, ARYTM_1, TARSKI, CARD_1,
      ZFMISC_1, RLVECT_3, HAHNBAN, BHSP_1, RFINSEQ;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1,
      NAT_1, FINSEQ_1, RELAT_1, ORDINAL1, FUNCT_1, FUNCT_2, STRUCT_0, RLVECT_1,
      FINSEQ_4, FRAENKEL, FINSET_1, RLSUB_1, ORDERS_1, RLVECT_2, BHSP_1,
      RLVECT_3, RUSUB_1, RUSUB_2, RFINSEQ;
 constructors NAT_1, REAL_1, ORDERS_1, RLVECT_2, FINSEQ_4, DOMAIN_1, PARTFUN1,
      RLVECT_3, RFINSEQ, RUSUB_2, XREAL_0, MEMBERED;
 clusters SUBSET_1, FINSET_1, RELSET_1, STRUCT_0, ARYTM_3, BHSP_1, RUSUB_1,
      FINSEQ_1, FUNCT_2, MEMBERED, NUMBERS, ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Definition and fundamental properties of linear combination

definition
let V be RealUnitarySpace;
let A be Subset of V;
 func Lin(A) -> strict Subspace of V means
:: RUSUB_3:def 1

  the carrier of it
     = {Sum(l) where l is Linear_Combination of A: not contradiction};
end;

theorem :: RUSUB_3:1
for V being RealUnitarySpace, A being Subset of V,
 x be set holds x in Lin(A)
  iff ex l being Linear_Combination of A st x = Sum(l);

theorem :: RUSUB_3:2
for V being RealUnitarySpace, A being Subset of V,
 x being set st x in A holds x in Lin(A);

theorem :: RUSUB_3:3
  for V being RealUnitarySpace holds Lin({}(the carrier of V)) = (0).V;

theorem :: RUSUB_3:4
  for V being RealUnitarySpace, A being Subset of V st
 Lin(A) = (0).V holds A = {} or A = {0.V};

theorem :: RUSUB_3:5
for V being RealUnitarySpace, W being strict Subspace of V,
 A being Subset of V st
  A = the carrier of W holds Lin(A) = W;

theorem :: RUSUB_3:6
  for V being strict RealUnitarySpace,A being Subset of V holds
 A = the carrier of V implies Lin(A) = V;

theorem :: RUSUB_3:7
for V being RealUnitarySpace, A,B being Subset of V st
 A c= B holds Lin(A) is Subspace of Lin(B);

theorem :: RUSUB_3:8
  for V being strict RealUnitarySpace, A,B being Subset of V st
 Lin(A) = V & A c= B holds Lin(B) = V;

theorem :: RUSUB_3:9
  for V being RealUnitarySpace, A,B being Subset of V holds
 Lin(A \/ B) = Lin(A) + Lin(B);

theorem :: RUSUB_3:10
  for V being RealUnitarySpace, A,B being Subset of V holds
 Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B);

theorem :: RUSUB_3:11
for V being RealUnitarySpace, A being Subset of V st
 A is linearly-independent holds
  ex B being Subset of V st
   A c= B & B is linearly-independent & Lin(B) = the UNITSTR of V;

theorem :: RUSUB_3:12
for V being RealUnitarySpace, A being Subset of V st
 Lin(A) = V holds
  ex B being Subset of V st
   B c= A & B is linearly-independent & Lin(B) = V;

begin :: Definition of the basis of real unitay space

definition
let V be RealUnitarySpace;
 mode Basis of V -> Subset of V means
:: RUSUB_3:def 2
 it is linearly-independent & Lin(it) = the UNITSTR of V;
end;

theorem :: RUSUB_3:13
  for V being strict RealUnitarySpace, A being Subset of V st
 A is linearly-independent holds ex I being Basis of V st A c= I;

theorem :: RUSUB_3:14
  for V being RealUnitarySpace, A being Subset of V st
 Lin(A) = V holds ex I being Basis of V st I c= A;

theorem :: RUSUB_3:15
for V being RealUnitarySpace, A being Subset of V st
 A is linearly-independent holds ex I being Basis of V st A c= I;

begin :: Some theorems of Lin, Sum, Carrier

theorem :: RUSUB_3:16
for V being RealUnitarySpace, L being Linear_Combination of V,
 A being Subset of V, F being FinSequence of the carrier of V st
  rng F c= the carrier of Lin(A) holds
   ex K being Linear_Combination of A st Sum(L (#) F) = Sum(K);

theorem :: RUSUB_3:17
  for V being RealUnitarySpace, L being Linear_Combination of V,
 A being Subset of V st Carrier(L) c= the carrier of Lin(A) holds
  ex K being Linear_Combination of A st Sum(L) = Sum(K);

theorem :: RUSUB_3:18
for V being RealUnitarySpace, W being Subspace of V,
 L being Linear_Combination of V st Carrier(L) c= the carrier of W
  for K being Linear_Combination of W st K = L|the carrier of W holds
   Carrier(L) = Carrier(K) & Sum(L) = Sum(K);

theorem :: RUSUB_3:19
for V being RealUnitarySpace, W being Subspace of V,
 K being Linear_Combination of W holds
  ex L being Linear_Combination of V st Carrier(K) = Carrier(L) &
   Sum(K) = Sum(L);

theorem :: RUSUB_3:20
for V being RealUnitarySpace, W being Subspace of V,
 L being Linear_Combination of V st Carrier(L) c= the carrier of W holds
  ex K being Linear_Combination of W st Carrier(K) = Carrier(L) & Sum(K) = Sum
(L);

theorem :: RUSUB_3:21
for V being RealUnitarySpace, I being Basis of V, v being VECTOR of V holds
 v in Lin(I);

theorem :: RUSUB_3:22
for V being RealUnitarySpace, W being Subspace of V, A being Subset of W st
 A is linearly-independent holds
  ex B being Subset of V st B is linearly-independent & B = A;

theorem :: RUSUB_3:23
  for V being RealUnitarySpace, W being Subspace of V, A being Subset of V st
 A is linearly-independent & A c= the carrier of W
   holds
    ex B being Subset of W st B is linearly-independent & B = A;

theorem :: RUSUB_3:24
  for V being RealUnitarySpace, W being Subspace of V,
 A being Basis of W ex B being Basis of V st A c= B;

theorem :: RUSUB_3:25
for V being RealUnitarySpace, A being Subset of V st
 A is linearly-independent
  for v being VECTOR of V st v in A
  for B being Subset of V st B = A \ {v}
    holds
   not v in Lin(B);

theorem :: RUSUB_3:26
  for V being RealUnitarySpace, I being Basis of V,
 A being non empty Subset of V st A misses I
  for B being Subset of V st B = I \/ A holds B is linearly-dependent;

theorem :: RUSUB_3:27
  for V being RealUnitarySpace, W being Subspace of V, A being Subset of V st
 A c= the carrier of W holds Lin(A) is Subspace of W;

theorem :: RUSUB_3:28
  for V being RealUnitarySpace, W being Subspace of V,
 A being Subset of V, B being Subset of W st A = B
    holds
   Lin(A) = Lin(B);

begin ::Subspaces of real unitary space generated by one, two, or three vectors

theorem :: RUSUB_3:29
for V being RealUnitarySpace, v being VECTOR of V, x being set holds
 x in Lin{v} iff ex a being Real st x = a * v;

theorem :: RUSUB_3:30
  for V being RealUnitarySpace, v being VECTOR of V holds
 v in Lin{v};

theorem :: RUSUB_3:31
  for V being RealUnitarySpace, v,w being VECTOR of V, x being set holds
 x in v + Lin{w} iff ex a being Real st x = v + a * w;

theorem :: RUSUB_3:32
for V being RealUnitarySpace, w1,w2 being VECTOR of V, x being set holds
 x in Lin{w1,w2} iff ex a,b being Real st x = a * w1 + b * w2;

theorem :: RUSUB_3:33
  for V being RealUnitarySpace, w1,w2 being VECTOR of V holds
 w1 in Lin{w1,w2} & w2 in Lin{w1,w2};

theorem :: RUSUB_3:34
  for V being RealUnitarySpace, v,w1,w2 being VECTOR of V,
 x being set holds
  x in v + Lin{w1,w2} iff ex a,b being Real st x = v + a * w1 + b * w2;

theorem :: RUSUB_3:35
for V being RealUnitarySpace, v1,v2,v3 being VECTOR of V,
 x being set holds
  x in Lin{v1,v2,v3} iff ex a,b,c being Real st x = a * v1 + b * v2 + c * v3;

theorem :: RUSUB_3:36
  for V being RealUnitarySpace, w1,w2,w3 being VECTOR of V holds
 w1 in Lin{w1,w2,w3} & w2 in Lin{w1,w2,w3} & w3 in Lin{w1,w2,w3};

theorem :: RUSUB_3:37
  for V being RealUnitarySpace, v,w1,w2,w3 being VECTOR of V, x being set holds
 x in v + Lin{w1,w2,w3} iff
  ex a,b,c being Real st x = v + a * w1 + b * w2 + c * w3;

theorem :: RUSUB_3:38
  for V being RealUnitarySpace, v,w being VECTOR of V st
 v in Lin{w} & v <> 0.V holds Lin{v} = Lin{w};

theorem :: RUSUB_3:39
  for V being RealUnitarySpace, v1,v2,w1,w2 being VECTOR of V st
 v1 <> v2 & {v1,v2} is linearly-independent &
  v1 in Lin{w1,w2} & v2 in Lin{w1,w2} holds
   Lin{w1,w2} = Lin{v1,v2} & {w1,w2} is linearly-independent & w1 <> w2;

begin :: Auxiliary theorems

theorem :: RUSUB_3:40
  for V being RealUnitarySpace, x being set holds
 x in (0).V iff x = 0.V;

theorem :: RUSUB_3:41
  for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st
 W1 is Subspace of W3 holds W1 /\ W2 is Subspace of W3;

theorem :: RUSUB_3:42
  for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st
 W1 is Subspace of W2 & W1 is Subspace of W3 holds
  W1 is Subspace of W2 /\ W3;

theorem :: RUSUB_3:43
  for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st
 W1 is Subspace of W3 & W2 is Subspace of W3 holds
  W1 + W2 is Subspace of W3;

theorem :: RUSUB_3:44
  for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st
 W1 is Subspace of W2 holds W1 is Subspace of W2 + W3;

theorem :: RUSUB_3:45
  for V being RealUnitarySpace, W1,W2 being Subspace of V,
 v being VECTOR of V st W1 is Subspace of W2 holds v + W1 c= v + W2;