:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama

::

:: Received October 9, 2002

:: Copyright (c) 2002-2012 Association of Mizar Users

begin

definition

let V be RealUnitarySpace;

let A be Subset of V;

ex b_{1} being strict Subspace of V st the carrier of b_{1} = { (Sum l) where l is Linear_Combination of A : verum }

for b_{1}, b_{2} being strict Subspace of V st the carrier of b_{1} = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b_{2} = { (Sum l) where l is Linear_Combination of A : verum } holds

b_{1} = b_{2}
by RUSUB_1:24;

end;
let A be Subset of V;

func Lin A -> strict Subspace of V means :Def1: :: RUSUB_3:def 1

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

existence the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines Lin RUSUB_3:def 1 :

for V being RealUnitarySpace

for A being Subset of V

for b_{3} being strict Subspace of V holds

( b_{3} = Lin A iff the carrier of b_{3} = { (Sum l) where l is Linear_Combination of A : verum } );

for V being RealUnitarySpace

for A being Subset of V

for b

( b

theorem Th1: :: RUSUB_3:1

for V being RealUnitarySpace

for A being Subset of V

for x being set holds

( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )

for A being Subset of V

for x being set holds

( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )

proof end;

Lm1: for V being RealUnitarySpace

for x being set holds

( x in (0). V iff x = 0. V )

proof end;

theorem :: RUSUB_3:4

for V being RealUnitarySpace

for A being Subset of V holds

( not Lin A = (0). V or A = {} or A = {(0. V)} )

for A being Subset of V holds

( not Lin A = (0). V or A = {} or A = {(0. V)} )

proof end;

theorem Th5: :: RUSUB_3:5

for V being RealUnitarySpace

for W being strict Subspace of V

for A being Subset of V st A = the carrier of W holds

Lin A = W

for W being strict Subspace of V

for A being Subset of V st A = the carrier of W holds

Lin A = W

proof end;

Lm2: for V being RealUnitarySpace

for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds

W1 /\ W2 is Subspace of W3

proof end;

Lm3: for V being RealUnitarySpace

for 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

proof end;

Lm4: for V being RealUnitarySpace

for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds

W1 is Subspace of W2 + W3

proof end;

Lm5: for V being RealUnitarySpace

for 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

proof end;

theorem :: RUSUB_3:8

for V being strict RealUnitarySpace

for A, B being Subset of V st Lin A = V & A c= B holds

Lin B = V

for A, B being Subset of V st Lin A = V & A c= B holds

Lin B = V

proof end;

theorem :: RUSUB_3:10

for V being RealUnitarySpace

for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)

for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)

proof end;

theorem Th11: :: RUSUB_3:11

for V being RealUnitarySpace

for 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 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )

for 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 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )

proof end;

theorem Th12: :: RUSUB_3:12

for V being RealUnitarySpace

for 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 )

for 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 )

proof end;

begin

definition

let V be RealUnitarySpace;

ex b_{1} being Subset of V st

( b_{1} is linearly-independent & Lin b_{1} = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) )

end;
mode Basis of V -> Subset of V means :Def2: :: RUSUB_3:def 2

( it is linearly-independent & Lin it = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) );

existence ( it is linearly-independent & Lin it = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) );

ex b

( b

proof end;

:: deftheorem Def2 defines Basis RUSUB_3:def 2 :

for V being RealUnitarySpace

for b_{2} being Subset of V holds

( b_{2} is Basis of V iff ( b_{2} is linearly-independent & Lin b_{2} = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) );

for V being RealUnitarySpace

for b

( b

theorem :: RUSUB_3:13

for V being strict RealUnitarySpace

for A being Subset of V st A is linearly-independent holds

ex I being Basis of V st A c= I

for A being Subset of V st A is linearly-independent holds

ex I being Basis of V st A c= I

proof end;

theorem :: RUSUB_3:14

for V being RealUnitarySpace

for A being Subset of V st Lin A = V holds

ex I being Basis of V st I c= A

for A being Subset of V st Lin A = V holds

ex I being Basis of V st I c= A

proof end;

theorem Th15: :: RUSUB_3:15

for V being RealUnitarySpace

for A being Subset of V st A is linearly-independent holds

ex I being Basis of V st A c= I

for A being Subset of V st A is linearly-independent holds

ex I being Basis of V st A c= I

proof end;

begin

theorem Th16: :: RUSUB_3:16

for V being RealUnitarySpace

for L being Linear_Combination of V

for A being Subset of V

for F being FinSequence 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

for L being Linear_Combination of V

for A being Subset of V

for F being FinSequence 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

proof end;

theorem :: RUSUB_3:17

for V being RealUnitarySpace

for L being Linear_Combination of V

for 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

for L being Linear_Combination of V

for 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

proof end;

theorem Th18: :: RUSUB_3:18

for V being RealUnitarySpace

for W being Subspace of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

for K being Linear_Combination of W st K = L | the carrier of W holds

( Carrier L = Carrier K & Sum L = Sum K )

for W being Subspace of V

for L being Linear_Combination of V st Carrier L c= the carrier of W holds

for K being Linear_Combination of W st K = L | the carrier of W holds

( Carrier L = Carrier K & Sum L = Sum K )

proof end;

theorem Th19: :: RUSUB_3:19

for V being RealUnitarySpace

for W being Subspace of V

for K being Linear_Combination of W ex L being Linear_Combination of V st

( Carrier K = Carrier L & Sum K = Sum L )

for W being Subspace of V

for K being Linear_Combination of W ex L being Linear_Combination of V st

( Carrier K = Carrier L & Sum K = Sum L )

proof end;

theorem Th20: :: RUSUB_3:20

for V being RealUnitarySpace

for W being Subspace of V

for 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 )

for W being Subspace of V

for 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 )

proof end;

theorem Th22: :: RUSUB_3:22

for V being RealUnitarySpace

for W being Subspace of V

for A being Subset of W st A is linearly-independent holds

A is linearly-independent Subset of V

for W being Subspace of V

for A being Subset of W st A is linearly-independent holds

A is linearly-independent Subset of V

proof end;

theorem :: RUSUB_3:23

for V being RealUnitarySpace

for W being Subspace of V

for A being Subset of V st A is linearly-independent & A c= the carrier of W holds

A is linearly-independent Subset of W

for W being Subspace of V

for A being Subset of V st A is linearly-independent & A c= the carrier of W holds

A is linearly-independent Subset of W

proof end;

theorem :: RUSUB_3:24

for V being RealUnitarySpace

for W being Subspace of V

for A being Basis of W ex B being Basis of V st A c= B

for W being Subspace of V

for A being Basis of W ex B being Basis of V st A c= B

proof end;

theorem Th25: :: RUSUB_3:25

for V being RealUnitarySpace

for A being Subset of V st A is linearly-independent holds

for v being VECTOR of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B

for A being Subset of V st A is linearly-independent holds

for v being VECTOR of V st v in A holds

for B being Subset of V st B = A \ {v} holds

not v in Lin B

proof end;

Lm6: for X, x being set st not x in X holds

X \ {x} = X

proof end;

theorem :: RUSUB_3:26

for V being RealUnitarySpace

for I being Basis of V

for A being non empty Subset of V st A misses I holds

for B being Subset of V st B = I \/ A holds

B is linearly-dependent

for I being Basis of V

for A being non empty Subset of V st A misses I holds

for B being Subset of V st B = I \/ A holds

B is linearly-dependent

proof end;

theorem :: RUSUB_3:27

for V being RealUnitarySpace

for W being Subspace of V

for A being Subset of V st A c= the carrier of W holds

Lin A is Subspace of W

for W being Subspace of V

for A being Subset of V st A c= the carrier of W holds

Lin A is Subspace of W

proof end;

theorem :: RUSUB_3:28

for V being RealUnitarySpace

for W being Subspace of V

for A being Subset of V

for B being Subset of W st A = B holds

Lin A = Lin B

for W being Subspace of V

for A being Subset of V

for B being Subset of W st A = B holds

Lin A = Lin B

proof end;

begin

theorem Th29: :: RUSUB_3:29

for V being RealUnitarySpace

for v being VECTOR of V

for x being set holds

( x in Lin {v} iff ex a being Real st x = a * v )

for v being VECTOR of V

for x being set holds

( x in Lin {v} iff ex a being Real st x = a * v )

proof end;

theorem :: RUSUB_3:31

for V being RealUnitarySpace

for v, w being VECTOR of V

for x being set holds

( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )

for v, w being VECTOR of V

for x being set holds

( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) )

proof end;

theorem Th32: :: RUSUB_3:32

for V being RealUnitarySpace

for w1, w2 being VECTOR of V

for x being set holds

( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )

for w1, w2 being VECTOR of V

for x being set holds

( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) )

proof end;

theorem :: RUSUB_3:33

for V being RealUnitarySpace

for w1, w2 being VECTOR of V holds

( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )

for w1, w2 being VECTOR of V holds

( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} )

proof end;

theorem :: RUSUB_3:34

for V being RealUnitarySpace

for v, w1, w2 being VECTOR of V

for x being set holds

( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )

for v, w1, w2 being VECTOR of V

for x being set holds

( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) )

proof end;

theorem Th35: :: RUSUB_3:35

for V being RealUnitarySpace

for v1, v2, v3 being VECTOR of V

for 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) )

for v1, v2, v3 being VECTOR of V

for 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) )

proof end;

theorem :: RUSUB_3:36

for V being RealUnitarySpace

for 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} )

for 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} )

proof end;

theorem :: RUSUB_3:37

for V being RealUnitarySpace

for v, w1, w2, w3 being VECTOR of V

for 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) )

for v, w1, w2, w3 being VECTOR of V

for 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) )

proof end;

theorem :: RUSUB_3:38

for V being RealUnitarySpace

for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds

Lin {v} = Lin {w}

for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds

Lin {v} = Lin {w}

proof end;

theorem :: RUSUB_3:39

for V being RealUnitarySpace

for 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 )

for 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 )

proof end;

begin

theorem :: RUSUB_3:40

theorem :: RUSUB_3:41

theorem :: RUSUB_3:42

theorem :: RUSUB_3:43

theorem :: RUSUB_3:44

theorem :: RUSUB_3:45

for V being RealUnitarySpace

for W1, W2 being Subspace of V

for v being VECTOR of V st W1 is Subspace of W2 holds

v + W1 c= v + W2

for W1, W2 being Subspace of V

for v being VECTOR of V st W1 is Subspace of W2 holds

v + W1 c= v + W2

proof end;