:: Basis of Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 10, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

Lm1:  for V being RealLinearSpace
for F, G being FinSequence of the carrier of V
for f being Function of the carrier of V,REAL holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
proofend;

theorem Th1: :: RLVECT_3:1
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)
proofend;

theorem Th2: :: RLVECT_3:2
for a being Real
for V being RealLinearSpace
for L being Linear_Combination of V holds Sum (a * L) = a * (Sum L)
proofend;

theorem Th3: :: RLVECT_3:3
for V being RealLinearSpace
for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
proofend;

theorem Th4: :: RLVECT_3:4
for V being RealLinearSpace
for L1, L2 being Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
proofend;

definition
let V be RealLinearSpace;
let A be Subset of V;
attrA is linearly-independent  means :Def1: :: RLVECT_3:def 1
 for l being Linear_Combination of A st Sum l = 0. V holds
Carrier l = {} ;
end;

:: deftheorem Def1 defines linearly-independent RLVECT_3:def_1_:_
 for V being RealLinearSpace
for A being Subset of V holds
( A is linearly-independent iff for l being Linear_Combination of A st Sum l = 0. V holds
Carrier l = {} );

notation
let V be RealLinearSpace;
let A be Subset of V;
antonym  linearly-dependent A for  linearly-independent ;
end;

theorem :: RLVECT_3:5
for V being RealLinearSpace
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
proofend;

theorem Th6: :: RLVECT_3:6
for V being RealLinearSpace
for A being Subset of V st A is linearly-independent holds
not 0. V in A
proofend;

theorem Th7: :: RLVECT_3:7
for V being RealLinearSpace holds {} the carrier of V is linearly-independent
proofend;

registration
let V be RealLinearSpace;
cluster linearly-independent for Element of bool the carrier of V;
existence
 ex b1 being Subset of V st b1 is linearly-independent
proofend;
end;

theorem Th8: :: RLVECT_3:8
for V being RealLinearSpace
for v being VECTOR of V holds
( {v} is linearly-independent iff v <> 0. V )
proofend;

theorem :: RLVECT_3:9
for V being RealLinearSpace holds {(0. V)} is linearly-dependent by Th8;

theorem Th10: :: RLVECT_3:10
for V being RealLinearSpace
for v1, v2 being VECTOR of V st {v1,v2} is linearly-independent holds
( v1 <> 0. V &amp; v2 <> 0. V )
proofend;

theorem :: RLVECT_3:11
for V being RealLinearSpace
for v being VECTOR of V holds
( {v,(0. V)} is linearly-dependent &amp; {(0. V),v} is linearly-dependent ) by Th10;

theorem Th12: :: RLVECT_3:12
for V being RealLinearSpace
for v1, v2 being VECTOR of V holds
( v1 <> v2 &amp; {v1,v2} is linearly-independent iff ( v2 <> 0. V &amp; ( for a being Real holds v1 <> a * v2 ) ) )
proofend;

theorem :: RLVECT_3:13
for V being RealLinearSpace
for v1, v2 being VECTOR of V holds
( ( v1 <> v2 &amp; {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 &amp; b = 0 ) )
proofend;

definition
let V be RealLinearSpace;
let A be Subset of V;
func Lin A ->  strict Subspace of V means :Def2: :: RLVECT_3:def 2
 the carrier of it =  {  (Sum l) where l is Linear_Combination of A : verum  }  ;
existence
 ex b1 being strict Subspace of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }
proofend;
uniqueness
 for b1, b2 being strict Subspace of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  &amp; the carrier of b2 =  {  (Sum l) where l is Linear_Combination of A : verum  }  holds
b1 = b2 by RLSUB_1:30;
end;

:: deftheorem Def2 defines Lin RLVECT_3:def_2_:_
 for V being RealLinearSpace
for A being Subset of V
for b3 being strict Subspace of V holds
( b3 = Lin A iff the carrier of b3 =  {  (Sum l) where l is Linear_Combination of A : verum  }  );

theorem Th14: :: RLVECT_3:14
for x being set
for V being RealLinearSpace
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
proofend;

theorem Th15: :: RLVECT_3:15
for x being set
for V being RealLinearSpace
for A being Subset of V st x in A holds
x in Lin A
proofend;

Lm2:  for x being set
for V being RealLinearSpace holds
( x in (0). V iff x = 0. V )
proofend;

theorem :: RLVECT_3:16
for V being RealLinearSpace holds Lin ({} the carrier of V) = (0). V
proofend;

theorem :: RLVECT_3:17
for V being RealLinearSpace
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proofend;

theorem Th18: :: RLVECT_3:18
for V being RealLinearSpace
for A being Subset of V
for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
proofend;

theorem :: RLVECT_3:19
for V being strict RealLinearSpace
for A being Subset of V st A = the carrier of V holds
Lin A = V
proofend;

Lm3:  for V being RealLinearSpace
for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
proofend;

Lm4:  for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 &amp; W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3
proofend;

Lm5:  for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
proofend;

Lm6:  for V being RealLinearSpace
for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 &amp; W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
proofend;

theorem Th20: :: RLVECT_3:20
for V being RealLinearSpace
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
proofend;

theorem :: RLVECT_3:21
for V being strict RealLinearSpace
for A, B being Subset of V st Lin A = V &amp; A c= B holds
Lin B = V
proofend;

theorem :: RLVECT_3:22
for V being RealLinearSpace
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proofend;

theorem :: RLVECT_3:23
for V being RealLinearSpace
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
proofend;

Lm7:  for M being non empty set
for CF being Choice_Function of M st not {} in M holds
dom CF = M
proofend;

theorem Th24: :: RLVECT_3:24
for V being RealLinearSpace
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B &amp; B is linearly-independent &amp; Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )
proofend;

theorem Th25: :: RLVECT_3:25
for V being RealLinearSpace
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A &amp; B is linearly-independent &amp; Lin B = V )
proofend;

definition
let V be RealLinearSpace;
mode Basis of V ->  Subset of V means :Def3: :: RLVECT_3:def 3
( it is linearly-independent &amp; Lin it = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) );
existence
 ex b1 being Subset of V st
( b1 is linearly-independent &amp; Lin b1 = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )
proofend;
end;

:: deftheorem Def3 defines Basis RLVECT_3:def_3_:_
 for V being RealLinearSpace
for b2 being Subset of V holds
( b2 is Basis of V iff ( b2 is linearly-independent &amp; Lin b2 = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) );

theorem :: RLVECT_3:26
for V being strict RealLinearSpace
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
proofend;

theorem :: RLVECT_3:27
for V being RealLinearSpace
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
proofend;

::
:: Auxiliary theorems.
::
theorem :: RLVECT_3:28
for M being non empty set
for CF being Choice_Function of M st not {} in M holds
dom CF = M by Lm7;

theorem :: RLVECT_3:29
for x being set
for V being RealLinearSpace holds
( x in (0). V iff x = 0. V ) by Lm2;

theorem :: RLVECT_3:30
for V being RealLinearSpace
for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3 by Lm3;

theorem :: RLVECT_3:31
for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 &amp; W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3 by Lm4;

theorem :: RLVECT_3:32
for V being RealLinearSpace
for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 &amp; W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3 by Lm6;

theorem :: RLVECT_3:33
for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3 by Lm5;

theorem :: RLVECT_3:34
for V being RealLinearSpace
for F, G being FinSequence of the carrier of V
for f being Function of the carrier of V,REAL holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by Lm1;