:: RLVECT_5 semantic presentation begin theorem Th1: :: RLVECT_5:1 for V being RealLinearSpace for KL1, KL2 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds KL1 = KL2 proof let V be RealLinearSpace; ::_thesis: for KL1, KL2 being Linear_Combination of V for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds KL1 = KL2 let KL1, KL2 be Linear_Combination of V; ::_thesis: for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds KL1 = KL2 let X be Subset of V; ::_thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 implies KL1 = KL2 ) assume A1: X is linearly-independent ; ::_thesis: ( not Carrier KL1 c= X or not Carrier KL2 c= X or not Sum KL1 = Sum KL2 or KL1 = KL2 ) assume A2: Carrier KL1 c= X ; ::_thesis: ( not Carrier KL2 c= X or not Sum KL1 = Sum KL2 or KL1 = KL2 ) assume Carrier KL2 c= X ; ::_thesis: ( not Sum KL1 = Sum KL2 or KL1 = KL2 ) then A3: (Carrier KL1) \/ (Carrier KL2) c= X by A2, XBOOLE_1:8; assume Sum KL1 = Sum KL2 ; ::_thesis: KL1 = KL2 then (Sum KL1) - (Sum KL2) = (Sum KL1) + (- (Sum KL1)) by RLVECT_1:def_11 .= 0. V by RLVECT_1:5 ; then A4: ( KL1 - KL2 is Linear_Combination of Carrier (KL1 - KL2) & Sum (KL1 - KL2) = 0. V ) by RLVECT_2:def_6, RLVECT_3:4; Carrier (KL1 - KL2) c= (Carrier KL1) \/ (Carrier KL2) by RLVECT_2:55; then A5: Carrier (KL1 - KL2) is linearly-independent by A1, A3, RLVECT_3:5, XBOOLE_1:1; now__::_thesis:_for_v_being_VECTOR_of_V_holds_KL1_._v_=_KL2_._v let v be VECTOR of V; ::_thesis: KL1 . v = KL2 . v not v in Carrier (KL1 - KL2) by A5, A4, RLVECT_3:def_1; then (KL1 - KL2) . v = 0 by RLVECT_2:19; then (KL1 . v) - (KL2 . v) = 0 by RLVECT_2:54; hence KL1 . v = KL2 . v ; ::_thesis: verum end; hence KL1 = KL2 by RLVECT_2:def_9; ::_thesis: verum end; theorem Th2: :: RLVECT_5:2 for V being RealLinearSpace for A being Subset of V st A is linearly-independent holds ex I being Basis of V st A c= I proof let V be RealLinearSpace; ::_thesis: for A being Subset of V st A is linearly-independent holds ex I being Basis of V st A c= I let A be Subset of V; ::_thesis: ( A is linearly-independent implies ex I being Basis of V st A c= I ) assume A is linearly-independent ; ::_thesis: ex I being Basis of V st A c= I then consider B being Subset of V such that A1: A c= B and A2: ( B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) by RLVECT_3:24; reconsider B = B as Basis of V by A2, RLVECT_3:def_3; take B ; ::_thesis: A c= B thus A c= B by A1; ::_thesis: verum end; theorem Th3: :: RLVECT_5:3 for V being RealLinearSpace for L being Linear_Combination of V for x being VECTOR of V holds ( x in Carrier L iff ex v being VECTOR of V st ( x = v & L . v <> 0 ) ) proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V for x being VECTOR of V holds ( x in Carrier L iff ex v being VECTOR of V st ( x = v & L . v <> 0 ) ) let L be Linear_Combination of V; ::_thesis: for x being VECTOR of V holds ( x in Carrier L iff ex v being VECTOR of V st ( x = v & L . v <> 0 ) ) let x be VECTOR of V; ::_thesis: ( x in Carrier L iff ex v being VECTOR of V st ( x = v & L . v <> 0 ) ) hereby ::_thesis: ( ex v being VECTOR of V st ( x = v & L . v <> 0 ) implies x in Carrier L ) assume x in Carrier L ; ::_thesis: ex v being VECTOR of V st ( x = v & L . v <> 0 ) then x in { w where w is VECTOR of V : L . w <> 0 } by RLVECT_2:def_4; hence ex v being VECTOR of V st ( x = v & L . v <> 0 ) ; ::_thesis: verum end; given v being VECTOR of V such that A1: ( x = v & L . v <> 0 ) ; ::_thesis: x in Carrier L x in { w where w is VECTOR of V : L . w <> 0 } by A1; hence x in Carrier L by RLVECT_2:def_4; ::_thesis: verum end; Lm1: for X, x being set st x in X holds (X \ {x}) \/ {x} = X proof let X, x be set ; ::_thesis: ( x in X implies (X \ {x}) \/ {x} = X ) assume x in X ; ::_thesis: (X \ {x}) \/ {x} = X then A1: {x} is Subset of X by SUBSET_1:41; {x} \/ (X \ {x}) = {x} \/ X by XBOOLE_1:39 .= X by A1, XBOOLE_1:12 ; hence (X \ {x}) \/ {x} = X ; ::_thesis: verum end; theorem Th4: :: RLVECT_5:4 for V being RealLinearSpace for L being Linear_Combination of V for F, G being FinSequence of the carrier of V for P being Permutation of (dom F) st G = F * P holds Sum (L (#) F) = Sum (L (#) G) proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V for F, G being FinSequence of the carrier of V for P being Permutation of (dom F) st G = F * P holds Sum (L (#) F) = Sum (L (#) G) let L be Linear_Combination of V; ::_thesis: for F, G being FinSequence of the carrier of V for P being Permutation of (dom F) st G = F * P holds Sum (L (#) F) = Sum (L (#) G) let F, G be FinSequence of the carrier of V; ::_thesis: for P being Permutation of (dom F) st G = F * P holds Sum (L (#) F) = Sum (L (#) G) set p = L (#) F; set q = L (#) G; let P be Permutation of (dom F); ::_thesis: ( G = F * P implies Sum (L (#) F) = Sum (L (#) G) ) assume A1: G = F * P ; ::_thesis: Sum (L (#) F) = Sum (L (#) G) A2: len G = len F by A1, FINSEQ_2:44; len F = len (L (#) F) by RLVECT_2:def_7; then A3: dom F = dom (L (#) F) by FINSEQ_3:29; then reconsider r = (L (#) F) * P as FinSequence of the carrier of V by FINSEQ_2:47; len r = len (L (#) F) by A3, FINSEQ_2:44; then A4: dom r = dom (L (#) F) by FINSEQ_3:29; A5: len (L (#) F) = len F by RLVECT_2:def_7; then A6: dom F = dom (L (#) F) by FINSEQ_3:29; len (L (#) G) = len G by RLVECT_2:def_7; then A7: dom (L (#) F) = dom (L (#) G) by A5, A2, FINSEQ_3:29; A8: dom F = dom G by A2, FINSEQ_3:29; A9: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(L_(#)_G)_holds_ (L_(#)_G)_._k_=_r_._k let k be Nat; ::_thesis: ( k in dom (L (#) G) implies (L (#) G) . k = r . k ) assume A10: k in dom (L (#) G) ; ::_thesis: (L (#) G) . k = r . k set l = P . k; ( dom P = dom F & rng P = dom F ) by FUNCT_2:52, FUNCT_2:def_3; then A11: P . k in dom F by A7, A6, A10, FUNCT_1:def_3; then reconsider l = P . k as Element of NAT ; G /. k = G . k by A7, A8, A6, A10, PARTFUN1:def_6 .= F . (P . k) by A1, A7, A8, A6, A10, FUNCT_1:12 .= F /. l by A11, PARTFUN1:def_6 ; then (L (#) G) . k = (L . (F /. l)) * (F /. l) by A10, RLVECT_2:def_7 .= (L (#) F) . (P . k) by A6, A11, RLVECT_2:def_7 .= r . k by A7, A4, A10, FUNCT_1:12 ; hence (L (#) G) . k = r . k ; ::_thesis: verum end; thus Sum (L (#) F) = Sum r by A3, RLVECT_2:7 .= Sum (L (#) G) by A7, A4, A9, FINSEQ_1:13 ; ::_thesis: verum end; theorem Th5: :: RLVECT_5:5 for V being RealLinearSpace for L being Linear_Combination of V for F being FinSequence of the carrier of V st Carrier L misses rng F holds Sum (L (#) F) = 0. V proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V for F being FinSequence of the carrier of V st Carrier L misses rng F holds Sum (L (#) F) = 0. V let L be Linear_Combination of V; ::_thesis: for F being FinSequence of the carrier of V st Carrier L misses rng F holds Sum (L (#) F) = 0. V defpred S1[ FinSequence] means for G being FinSequence of the carrier of V st G = $1 & Carrier L misses rng G holds Sum (L (#) G) = 0. V; A1: for p being FinSequence for x being set st S1[p] holds S1[p ^ <*x*>] proof let p be FinSequence; ::_thesis: for x being set st S1[p] holds S1[p ^ <*x*>] let x be set ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] ) assume A2: S1[p] ; ::_thesis: S1[p ^ <*x*>] let G be FinSequence of the carrier of V; ::_thesis: ( G = p ^ <*x*> & Carrier L misses rng G implies Sum (L (#) G) = 0. V ) assume A3: G = p ^ <*x*> ; ::_thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V ) then reconsider p = p, x9 = <*x*> as FinSequence of the carrier of V by FINSEQ_1:36; x in {x} by TARSKI:def_1; then A4: x in rng x9 by FINSEQ_1:38; rng x9 c= the carrier of V by FINSEQ_1:def_4; then reconsider x = x as VECTOR of V by A4; assume Carrier L misses rng G ; ::_thesis: Sum (L (#) G) = 0. V then A5: {} = (Carrier L) /\ (rng G) by XBOOLE_0:def_7 .= (Carrier L) /\ ((rng p) \/ (rng <*x*>)) by A3, FINSEQ_1:31 .= (Carrier L) /\ ((rng p) \/ {x}) by FINSEQ_1:38 .= ((Carrier L) /\ (rng p)) \/ ((Carrier L) /\ {x}) by XBOOLE_1:23 ; then (Carrier L) /\ (rng p) = {} ; then Carrier L misses rng p by XBOOLE_0:def_7; then A6: Sum (L (#) p) = 0. V by A2; A7: (Carrier L) /\ {x} = {} by A5; now__::_thesis:_not_x_in_Carrier_L A8: x in {x} by TARSKI:def_1; assume x in Carrier L ; ::_thesis: contradiction hence contradiction by A7, A8, XBOOLE_0:def_4; ::_thesis: verum end; then A9: L . x = 0 by RLVECT_2:19; Sum (L (#) G) = Sum ((L (#) p) ^ (L (#) x9)) by A3, RLVECT_3:34 .= (Sum (L (#) p)) + (Sum (L (#) x9)) by RLVECT_1:41 .= (0. V) + (Sum <*((L . x) * x)*>) by A6, RLVECT_2:26 .= Sum <*((L . x) * x)*> by RLVECT_1:4 .= 0 * x by A9, RLVECT_1:44 .= 0. V by RLVECT_1:10 ; hence Sum (L (#) G) = 0. V ; ::_thesis: verum end; A10: S1[ {} ] proof let G be FinSequence of the carrier of V; ::_thesis: ( G = {} & Carrier L misses rng G implies Sum (L (#) G) = 0. V ) assume G = {} ; ::_thesis: ( not Carrier L misses rng G or Sum (L (#) G) = 0. V ) then A11: L (#) G = <*> the carrier of V by RLVECT_2:25; assume Carrier L misses rng G ; ::_thesis: Sum (L (#) G) = 0. V thus Sum (L (#) G) = 0. V by A11, RLVECT_1:43; ::_thesis: verum end; A12: for p being FinSequence holds S1[p] from FINSEQ_1:sch_3(A10, A1); let F be FinSequence of the carrier of V; ::_thesis: ( Carrier L misses rng F implies Sum (L (#) F) = 0. V ) assume Carrier L misses rng F ; ::_thesis: Sum (L (#) F) = 0. V hence Sum (L (#) F) = 0. V by A12; ::_thesis: verum end; theorem Th6: :: RLVECT_5:6 for V being RealLinearSpace for F being FinSequence of the carrier of V st F is one-to-one holds for L being Linear_Combination of V st Carrier L c= rng F holds Sum (L (#) F) = Sum L proof let V be RealLinearSpace; ::_thesis: for F being FinSequence of the carrier of V st F is one-to-one holds for L being Linear_Combination of V st Carrier L c= rng F holds Sum (L (#) F) = Sum L let F be FinSequence of the carrier of V; ::_thesis: ( F is one-to-one implies for L being Linear_Combination of V st Carrier L c= rng F holds Sum (L (#) F) = Sum L ) assume A1: F is one-to-one ; ::_thesis: for L being Linear_Combination of V st Carrier L c= rng F holds Sum (L (#) F) = Sum L rng F c= rng F ; then reconsider X = rng F as Subset of (rng F) ; let L be Linear_Combination of V; ::_thesis: ( Carrier L c= rng F implies Sum (L (#) F) = Sum L ) assume A2: Carrier L c= rng F ; ::_thesis: Sum (L (#) F) = Sum L consider G being FinSequence of the carrier of V such that A3: G is one-to-one and A4: rng G = Carrier L and A5: Sum L = Sum (L (#) G) by RLVECT_2:def_8; reconsider A = rng G as Subset of (rng F) by A2, A4; set F1 = F - (A `); X \ (A `) = X /\ ((A `) `) by SUBSET_1:13 .= A by XBOOLE_1:28 ; then A6: rng (F - (A `)) = rng G by FINSEQ_3:65; F - (A `) is one-to-one by A1, FINSEQ_3:87; then F - (A `),G are_fiberwise_equipotent by A3, A6, RFINSEQ:26; then A7: ex Q being Permutation of (dom G) st F - (A `) = G * Q by RFINSEQ:4; reconsider F1 = F - (A `), F2 = F - A as FinSequence of the carrier of V by FINSEQ_3:86; A8: (rng F) \ (rng G) misses rng G by XBOOLE_1:79; (rng F2) /\ (rng G) = ((rng F) \ (rng G)) /\ (rng G) by FINSEQ_3:65 .= {} by A8, XBOOLE_0:def_7 ; then A9: Carrier L misses rng F2 by A4, XBOOLE_0:def_7; ex P being Permutation of (dom F) st (F - (A `)) ^ (F - A) = F * P by FINSEQ_3:115; then Sum (L (#) F) = Sum (L (#) (F1 ^ F2)) by Th4 .= Sum ((L (#) F1) ^ (L (#) F2)) by RLVECT_3:34 .= (Sum (L (#) F1)) + (Sum (L (#) F2)) by RLVECT_1:41 .= (Sum (L (#) F1)) + (0. V) by A9, Th5 .= (Sum (L (#) G)) + (0. V) by A7, Th4 .= Sum L by A5, RLVECT_1:4 ; hence Sum (L (#) F) = Sum L ; ::_thesis: verum end; theorem Th7: :: RLVECT_5:7 for V being RealLinearSpace for L being Linear_Combination of V for F being FinSequence of the carrier of V ex K being Linear_Combination of V st ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V for F being FinSequence of the carrier of V ex K being Linear_Combination of V st ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) let L be Linear_Combination of V; ::_thesis: for F being FinSequence of the carrier of V ex K being Linear_Combination of V st ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) let F be FinSequence of the carrier of V; ::_thesis: ex K being Linear_Combination of V st ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) defpred S1[ set , set ] means ( not $1 is VECTOR of V or ( $1 in rng F & $2 = L . $1 ) or ( not $1 in rng F & $2 = 0 ) ); reconsider R = rng F as finite Subset of V by FINSEQ_1:def_4; A1: for x being set st x in the carrier of V holds ex y being set st ( y in REAL & S1[x,y] ) proof let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st ( y in REAL & S1[x,y] ) ) assume x in the carrier of V ; ::_thesis: ex y being set st ( y in REAL & S1[x,y] ) then reconsider x9 = x as VECTOR of V ; percases ( x in rng F or not x in rng F ) ; suppose x in rng F ; ::_thesis: ex y being set st ( y in REAL & S1[x,y] ) then S1[x,L . x9] ; hence ex y being set st ( y in REAL & S1[x,y] ) ; ::_thesis: verum end; suppose not x in rng F ; ::_thesis: ex y being set st ( y in REAL & S1[x,y] ) hence ex y being set st ( y in REAL & S1[x,y] ) ; ::_thesis: verum end; end; end; ex K being Function of the carrier of V,REAL st for x being set st x in the carrier of V holds S1[x,K . x] from FUNCT_2:sch_1(A1); then consider K being Function of the carrier of V,REAL such that A2: for x being set st x in the carrier of V holds S1[x,K . x] ; A3: now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_R_/\_(Carrier_L)_holds_ K_._v_=_0 let v be VECTOR of V; ::_thesis: ( not v in R /\ (Carrier L) implies K . b1 = 0 ) assume A4: not v in R /\ (Carrier L) ; ::_thesis: K . b1 = 0 percases ( not v in R or not v in Carrier L ) by A4, XBOOLE_0:def_4; suppose not v in R ; ::_thesis: K . b1 = 0 hence K . v = 0 by A2; ::_thesis: verum end; suppose not v in Carrier L ; ::_thesis: K . b1 = 0 then L . v = 0 by RLVECT_2:19; hence K . v = 0 by A2; ::_thesis: verum end; end; end; reconsider K = K as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; reconsider K = K as Linear_Combination of V by A3, RLVECT_2:def_3; now__::_thesis:_for_v_being_set_st_v_in_(rng_F)_/\_(Carrier_L)_holds_ v_in_Carrier_K let v be set ; ::_thesis: ( v in (rng F) /\ (Carrier L) implies v in Carrier K ) assume A5: v in (rng F) /\ (Carrier L) ; ::_thesis: v in Carrier K then reconsider v9 = v as VECTOR of V ; v in Carrier L by A5, XBOOLE_0:def_4; then A6: L . v9 <> 0 by RLVECT_2:19; v in R by A5, XBOOLE_0:def_4; then K . v9 = L . v9 by A2; then v in { w where w is VECTOR of V : K . w <> 0 } by A6; hence v in Carrier K by RLVECT_2:def_4; ::_thesis: verum end; then A7: (rng F) /\ (Carrier L) c= Carrier K by TARSKI:def_3; take K ; ::_thesis: ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) A8: L (#) F = K (#) F proof set p = L (#) F; set q = K (#) F; A9: len (L (#) F) = len F by RLVECT_2:def_7; len (K (#) F) = len F by RLVECT_2:def_7; then A10: dom (L (#) F) = dom (K (#) F) by A9, FINSEQ_3:29; A11: dom (L (#) F) = dom F by A9, FINSEQ_3:29; now__::_thesis:_for_k_being_Nat_st_k_in_dom_(L_(#)_F)_holds_ (L_(#)_F)_._k_=_(K_(#)_F)_._k let k be Nat; ::_thesis: ( k in dom (L (#) F) implies (L (#) F) . k = (K (#) F) . k ) set u = F /. k; A12: S1[F /. k,K . (F /. k)] by A2; assume A13: k in dom (L (#) F) ; ::_thesis: (L (#) F) . k = (K (#) F) . k then ( F /. k = F . k & (L (#) F) . k = (L . (F /. k)) * (F /. k) ) by A11, PARTFUN1:def_6, RLVECT_2:def_7; hence (L (#) F) . k = (K (#) F) . k by A10, A11, A13, A12, FUNCT_1:def_3, RLVECT_2:def_7; ::_thesis: verum end; hence L (#) F = K (#) F by A10, FINSEQ_1:13; ::_thesis: verum end; now__::_thesis:_for_v_being_set_st_v_in_Carrier_K_holds_ v_in_(rng_F)_/\_(Carrier_L) let v be set ; ::_thesis: ( v in Carrier K implies v in (rng F) /\ (Carrier L) ) assume v in Carrier K ; ::_thesis: v in (rng F) /\ (Carrier L) then v in { v9 where v9 is VECTOR of V : K . v9 <> 0 } by RLVECT_2:def_4; then ex v9 being VECTOR of V st ( v9 = v & K . v9 <> 0 ) ; hence v in (rng F) /\ (Carrier L) by A3; ::_thesis: verum end; then Carrier K c= (rng F) /\ (Carrier L) by TARSKI:def_3; hence ( Carrier K = (rng F) /\ (Carrier L) & L (#) F = K (#) F ) by A7, A8, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th8: :: RLVECT_5:8 for V being RealLinearSpace for L being Linear_Combination of V for A being Subset of V for 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 proof let V be RealLinearSpace; ::_thesis: for L being Linear_Combination of V for A being Subset of V for 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 let L be Linear_Combination of V; ::_thesis: for A being Subset of V for 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 let A be Subset of V; ::_thesis: for 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 defpred S1[ Element of NAT ] means for F being FinSequence of the carrier of V st rng F c= the carrier of (Lin A) & len F = $1 holds ex K being Linear_Combination of A st Sum (L (#) F) = Sum K; A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] let F be FinSequence of the carrier of V; ::_thesis: ( rng F c= the carrier of (Lin A) & len F = n + 1 implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K ) assume that A3: rng F c= the carrier of (Lin A) and A4: len F = n + 1 ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K consider G being FinSequence, x being set such that A5: F = G ^ <*x*> by A4, FINSEQ_2:18; reconsider G = G, x9 = <*x*> as FinSequence of the carrier of V by A5, FINSEQ_1:36; A6: rng (G ^ <*x*>) = (rng G) \/ (rng <*x*>) by FINSEQ_1:31 .= (rng G) \/ {x} by FINSEQ_1:38 ; then A7: rng G c= rng F by A5, XBOOLE_1:7; {x} c= rng F by A5, A6, XBOOLE_1:7; then {x} c= the carrier of (Lin A) by A3, XBOOLE_1:1; then ( x in {x} implies x in the carrier of (Lin A) ) ; then A8: x in Lin A by STRUCT_0:def_5, TARSKI:def_1; then consider LA1 being Linear_Combination of A such that A9: x = Sum LA1 by RLVECT_3:14; x in V by A8, RLSUB_1:9; then reconsider x = x as VECTOR of V by STRUCT_0:def_5; len (G ^ <*x*>) = (len G) + (len <*x*>) by FINSEQ_1:22 .= (len G) + 1 by FINSEQ_1:39 ; then consider LA2 being Linear_Combination of A such that A10: Sum (L (#) G) = Sum LA2 by A2, A3, A4, A5, A7, XBOOLE_1:1; (L . x) * LA1 is Linear_Combination of A by RLVECT_2:44; then A11: LA2 + ((L . x) * LA1) is Linear_Combination of A by RLVECT_2:38; Sum (L (#) F) = Sum ((L (#) G) ^ (L (#) x9)) by A5, RLVECT_3:34 .= (Sum LA2) + (Sum (L (#) x9)) by A10, RLVECT_1:41 .= (Sum LA2) + (Sum <*((L . x) * x)*>) by RLVECT_2:26 .= (Sum LA2) + ((L . x) * (Sum LA1)) by A9, RLVECT_1:44 .= (Sum LA2) + (Sum ((L . x) * LA1)) by RLVECT_3:2 .= Sum (LA2 + ((L . x) * LA1)) by RLVECT_3:1 ; hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A11; ::_thesis: verum end; let F be FinSequence of the carrier of V; ::_thesis: ( rng F c= the carrier of (Lin A) implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K ) assume A12: rng F c= the carrier of (Lin A) ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K A13: len F is Element of NAT ; A14: S1[ 0 ] proof let F be FinSequence of the carrier of V; ::_thesis: ( rng F c= the carrier of (Lin A) & len F = 0 implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K ) assume that rng F c= the carrier of (Lin A) and A15: len F = 0 ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K F = <*> the carrier of V by A15; then L (#) F = <*> the carrier of V by RLVECT_2:25; then A16: Sum (L (#) F) = 0. V by RLVECT_1:43 .= Sum (ZeroLC V) by RLVECT_2:30 ; ZeroLC V is Linear_Combination of A by RLVECT_2:22; hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A16; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A14, A1); hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A12, A13; ::_thesis: verum end; theorem Th9: :: RLVECT_5:9 for V being RealLinearSpace 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 let V be RealLinearSpace; ::_thesis: 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 let L be Linear_Combination of V; ::_thesis: 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 let A be Subset of V; ::_thesis: ( Carrier L c= the carrier of (Lin A) implies ex K being Linear_Combination of A st Sum L = Sum K ) consider F being FinSequence of the carrier of V such that F is one-to-one and A1: rng F = Carrier L and A2: Sum L = Sum (L (#) F) by RLVECT_2:def_8; assume Carrier L c= the carrier of (Lin A) ; ::_thesis: ex K being Linear_Combination of A st Sum L = Sum K then consider K being Linear_Combination of A such that A3: Sum (L (#) F) = Sum K by A1, Th8; take K ; ::_thesis: Sum L = Sum K thus Sum L = Sum K by A2, A3; ::_thesis: verum end; theorem Th10: :: RLVECT_5:10 for V being RealLinearSpace 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 let V be RealLinearSpace; ::_thesis: 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 ) let W be Subspace of V; ::_thesis: 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 ) let L be Linear_Combination of V; ::_thesis: ( Carrier L c= the carrier of W implies for K being Linear_Combination of W st K = L | the carrier of W holds ( Carrier L = Carrier K & Sum L = Sum K ) ) assume A1: Carrier L c= the carrier of W ; ::_thesis: for K being Linear_Combination of W st K = L | the carrier of W holds ( Carrier L = Carrier K & Sum L = Sum K ) let K be Linear_Combination of W; ::_thesis: ( K = L | the carrier of W implies ( Carrier L = Carrier K & Sum L = Sum K ) ) assume A2: K = L | the carrier of W ; ::_thesis: ( Carrier L = Carrier K & Sum L = Sum K ) A3: dom K = the carrier of W by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_Carrier_K_holds_ x_in_Carrier_L let x be set ; ::_thesis: ( x in Carrier K implies x in Carrier L ) assume x in Carrier K ; ::_thesis: x in Carrier L then consider w being VECTOR of W such that A4: x = w and A5: K . w <> 0 by Th3; A6: w is VECTOR of V by RLSUB_1:10; L . w <> 0 by A2, A3, A5, FUNCT_1:47; hence x in Carrier L by A4, A6, Th3; ::_thesis: verum end; then A7: Carrier K c= Carrier L by TARSKI:def_3; consider G being FinSequence of the carrier of W such that A8: ( G is one-to-one & rng G = Carrier K ) and A9: Sum K = Sum (K (#) G) by RLVECT_2:def_8; 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_8; now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_ x_in_Carrier_K let x be set ; ::_thesis: ( x in Carrier L implies x in Carrier K ) assume A13: x in Carrier L ; ::_thesis: x in Carrier K then consider v being VECTOR of V such that A14: x = v and A15: L . v <> 0 by Th3; K . v <> 0 by A1, A2, A3, A13, A14, A15, FUNCT_1:47; hence x in Carrier K by A1, A13, A14, Th3; ::_thesis: verum end; then A16: Carrier L c= Carrier K by TARSKI:def_3; then A17: Carrier K = Carrier L by A7, XBOOLE_0:def_10; then F,G are_fiberwise_equipotent by A10, A11, A8, RFINSEQ:26; then consider P being Permutation of (dom G) such that A18: F = G * P by RFINSEQ:4; len (K (#) G) = len G by RLVECT_2:def_7; then A19: dom (K (#) G) = dom G by FINSEQ_3:29; then reconsider q = (K (#) G) * P as FinSequence of the carrier of W by FINSEQ_2:47; A20: len q = len (K (#) G) by A19, FINSEQ_2:44; then len q = len G by RLVECT_2:def_7; then A21: dom q = dom G by FINSEQ_3:29; set p = L (#) F; A22: the carrier of W c= the carrier of V by RLSUB_1:def_2; rng q c= the carrier of W by FINSEQ_1:def_4; then rng q c= the carrier of V by A22, XBOOLE_1:1; then reconsider q9 = q as FinSequence of the carrier of V by FINSEQ_1:def_4; consider f being Function of NAT, the carrier of W such that A23: Sum q = f . (len q) and A24: f . 0 = 0. W and A25: for i being Element of NAT for w being VECTOR of W st i < len q & w = q . (i + 1) holds f . (i + 1) = (f . i) + w by RLVECT_1:def_12; ( dom f = NAT & rng f c= the carrier of W ) by FUNCT_2:def_1, RELAT_1:def_19; then reconsider f9 = f as Function of NAT, the carrier of V by A22, FUNCT_2:2, XBOOLE_1:1; A26: for i being Element of NAT for v being VECTOR of V st i < len q9 & v = q9 . (i + 1) holds f9 . (i + 1) = (f9 . i) + v proof let i be Element of NAT ; ::_thesis: for v being VECTOR of V st i < len q9 & v = q9 . (i + 1) holds f9 . (i + 1) = (f9 . i) + v let v be VECTOR of V; ::_thesis: ( i < len q9 & v = q9 . (i + 1) implies f9 . (i + 1) = (f9 . i) + v ) assume that A27: i < len q9 and A28: v = q9 . (i + 1) ; ::_thesis: f9 . (i + 1) = (f9 . i) + v ( 1 <= i + 1 & i + 1 <= len q ) by A27, NAT_1:11, NAT_1:13; then i + 1 in dom q by FINSEQ_3:25; then reconsider v9 = v as VECTOR of W by A28, FINSEQ_2:11; f . (i + 1) = (f . i) + v9 by A25, A27, A28; hence f9 . (i + 1) = (f9 . i) + v by RLSUB_1:13; ::_thesis: verum end; A29: len G = len F by A18, FINSEQ_2:44; then A30: dom G = dom F by FINSEQ_3:29; len G = len (L (#) F) by A29, RLVECT_2:def_7; then A31: dom (L (#) F) = dom G by FINSEQ_3:29; A32: dom q = dom (K (#) G) by A20, FINSEQ_3:29; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(L_(#)_F)_holds_ (L_(#)_F)_._i_=_q_._i let i be Nat; ::_thesis: ( i in dom (L (#) F) implies (L (#) F) . i = q . i ) set v = F /. i; set j = P . i; assume A33: i in dom (L (#) F) ; ::_thesis: (L (#) F) . i = q . i then A34: F /. i = F . i by A31, A30, PARTFUN1:def_6; then F /. i in rng F by A31, A30, A33, FUNCT_1:def_3; then reconsider w = F /. i as VECTOR of W by A17, A11; ( dom P = dom G & rng P = dom G ) by FUNCT_2:52, FUNCT_2:def_3; then A35: P . i in dom G by A31, A33, FUNCT_1:def_3; then reconsider j = P . i as Element of NAT ; A36: G /. j = G . (P . i) by A35, PARTFUN1:def_6 .= F /. i by A18, A31, A30, A33, A34, FUNCT_1:12 ; q . i = (K (#) G) . j by A31, A21, A33, FUNCT_1:12 .= (K . w) * w by A32, A21, A35, A36, RLVECT_2:def_7 .= (L . (F /. i)) * w by A2, A3, FUNCT_1:47 .= (L . (F /. i)) * (F /. i) by RLSUB_1:14 ; hence (L (#) F) . i = q . i by A33, RLVECT_2:def_7; ::_thesis: verum end; then A37: L (#) F = (K (#) G) * P by A31, A21, FINSEQ_1:13; len G = len (K (#) G) by RLVECT_2:def_7; then dom G = dom (K (#) G) by FINSEQ_3:29; then reconsider P = P as Permutation of (dom (K (#) G)) ; q = (K (#) G) * P ; then A38: Sum (K (#) G) = Sum q by RLVECT_2:7; A39: f9 . (len q9) is Element of V ; f9 . 0 = 0. V by A24, RLSUB_1:11; hence ( Carrier L = Carrier K & Sum L = Sum K ) by A7, A16, A12, A9, A37, A38, A23, A26, A39, RLVECT_1:def_12, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th11: :: RLVECT_5:11 for V being RealLinearSpace 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 let V be RealLinearSpace; ::_thesis: 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 ) let W be Subspace of V; ::_thesis: for K being Linear_Combination of W ex L being Linear_Combination of V st ( Carrier K = Carrier L & Sum K = Sum L ) let K be Linear_Combination of W; ::_thesis: ex L being Linear_Combination of V st ( Carrier K = Carrier L & Sum K = Sum L ) defpred S1[ set , set ] means ( ( $1 in W & $2 = K . $1 ) or ( not $1 in W & $2 = 0 ) ); reconsider K9 = K as Function of the carrier of W,REAL ; A1: the carrier of W c= the carrier of V by RLSUB_1:def_2; then reconsider C = Carrier K as finite Subset of V by XBOOLE_1:1; A2: for x being set st x in the carrier of V holds ex y being set st ( y in REAL & S1[x,y] ) proof let x be set ; ::_thesis: ( x in the carrier of V implies ex y being set st ( y in REAL & S1[x,y] ) ) assume x in the carrier of V ; ::_thesis: ex y being set st ( y in REAL & S1[x,y] ) then reconsider x = x as VECTOR of V ; percases ( x in W or not x in W ) ; supposeA3: x in W ; ::_thesis: ex y being set st ( y in REAL & S1[x,y] ) then reconsider x = x as VECTOR of W by STRUCT_0:def_5; S1[x,K . x] by A3; hence ex y being set st ( y in REAL & S1[x,y] ) ; ::_thesis: verum end; suppose not x in W ; ::_thesis: ex y being set st ( y in REAL & S1[x,y] ) hence ex y being set st ( y in REAL & S1[x,y] ) ; ::_thesis: verum end; end; end; ex L being Function of the carrier of V,REAL st for x being set st x in the carrier of V holds S1[x,L . x] from FUNCT_2:sch_1(A2); then consider L being Function of the carrier of V,REAL such that A4: for x being set st x in the carrier of V holds S1[x,L . x] ; A5: now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_C_holds_ L_._v_=_0 let v be VECTOR of V; ::_thesis: ( not v in C implies L . v = 0 ) assume not v in C ; ::_thesis: L . v = 0 then ( ( S1[v,K . v] & not v in C & v in the carrier of W ) or S1[v, 0 ] ) by STRUCT_0:def_5; then ( ( S1[v,K . v] & K . v = 0 ) or S1[v, 0 ] ) by RLVECT_2:19; hence L . v = 0 by A4; ::_thesis: verum end; L is Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; then reconsider L = L as Linear_Combination of V by A5, RLVECT_2:def_3; reconsider L9 = L | the carrier of W as Function of the carrier of W,REAL by A1, FUNCT_2:32; take L ; ::_thesis: ( Carrier K = Carrier L & Sum K = Sum L ) now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_ x_in_the_carrier_of_W let x be set ; ::_thesis: ( x in Carrier L implies x in the carrier of W ) assume that A6: x in Carrier L and A7: not x in the carrier of W ; ::_thesis: contradiction consider v being VECTOR of V such that A8: x = v and A9: L . v <> 0 by A6, Th3; S1[v, 0 ] by A7, A8, STRUCT_0:def_5; hence contradiction by A4, A9; ::_thesis: verum end; then A10: Carrier L c= the carrier of W by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_W_holds_ K9_._x_=_L9_._x let x be set ; ::_thesis: ( x in the carrier of W implies K9 . x = L9 . x ) assume A11: x in the carrier of W ; ::_thesis: K9 . x = L9 . x then S1[x,L . x] by A4, A1; hence K9 . x = L9 . x by A11, FUNCT_1:49, STRUCT_0:def_5; ::_thesis: verum end; then K9 = L9 by FUNCT_2:12; hence ( Carrier K = Carrier L & Sum K = Sum L ) by A10, Th10; ::_thesis: verum end; theorem Th12: :: RLVECT_5:12 for V being RealLinearSpace 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 let V be RealLinearSpace; ::_thesis: 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 ) let W be Subspace of V; ::_thesis: 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 ) let L be Linear_Combination of V; ::_thesis: ( Carrier L c= the carrier of W implies ex K being Linear_Combination of W st ( Carrier K = Carrier L & Sum K = Sum L ) ) assume A1: Carrier L c= the carrier of W ; ::_thesis: ex K being Linear_Combination of W st ( Carrier K = Carrier L & Sum K = Sum L ) then reconsider C = Carrier L as finite Subset of W ; the carrier of W c= the carrier of V by RLSUB_1:def_2; then reconsider K = L | the carrier of W as Function of the carrier of W,REAL by FUNCT_2:32; A2: K is Element of Funcs ( the carrier of W,REAL) by FUNCT_2:8; A3: dom K = the carrier of W by FUNCT_2:def_1; now__::_thesis:_for_w_being_VECTOR_of_W_st_not_w_in_C_holds_ K_._w_=_0 let w be VECTOR of W; ::_thesis: ( not w in C implies K . w = 0 ) A4: w is VECTOR of V by RLSUB_1:10; assume not w in C ; ::_thesis: K . w = 0 then L . w = 0 by A4, RLVECT_2:19; hence K . w = 0 by A3, FUNCT_1:47; ::_thesis: verum end; then reconsider K = K as Linear_Combination of W by A2, RLVECT_2:def_3; take K ; ::_thesis: ( Carrier K = Carrier L & Sum K = Sum L ) thus ( Carrier K = Carrier L & Sum K = Sum L ) by A1, Th10; ::_thesis: verum end; theorem Th13: :: RLVECT_5:13 for V being RealLinearSpace for I being Basis of V for v being VECTOR of V holds v in Lin I proof let V be RealLinearSpace; ::_thesis: for I being Basis of V for v being VECTOR of V holds v in Lin I let I be Basis of V; ::_thesis: for v being VECTOR of V holds v in Lin I let v be VECTOR of V; ::_thesis: v in Lin I v in RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by STRUCT_0:def_5; hence v in Lin I by RLVECT_3:def_3; ::_thesis: verum end; theorem Th14: :: RLVECT_5:14 for V being RealLinearSpace 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 let V be RealLinearSpace; ::_thesis: 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 let W be Subspace of V; ::_thesis: for A being Subset of W st A is linearly-independent holds A is linearly-independent Subset of V let A be Subset of W; ::_thesis: ( A is linearly-independent implies A is linearly-independent Subset of V ) the carrier of W c= the carrier of V by RLSUB_1:def_2; then reconsider A9 = A as Subset of V by XBOOLE_1:1; assume A1: A is linearly-independent ; ::_thesis: A is linearly-independent Subset of V now__::_thesis:_not_A9_is_linearly-dependent assume A9 is linearly-dependent ; ::_thesis: contradiction then consider L being Linear_Combination of A9 such that A2: Sum L = 0. V and A3: Carrier L <> {} by RLVECT_3:def_1; Carrier L c= A by RLVECT_2:def_6; then consider LW being Linear_Combination of W such that A4: Carrier LW = Carrier L and A5: Sum LW = Sum L by Th12, XBOOLE_1:1; reconsider LW = LW as Linear_Combination of A by A4, RLVECT_2:def_6; Sum LW = 0. W by A2, A5, RLSUB_1:11; hence contradiction by A1, A3, A4, RLVECT_3:def_1; ::_thesis: verum end; hence A is linearly-independent Subset of V ; ::_thesis: verum end; theorem Th15: :: RLVECT_5:15 for V being RealLinearSpace 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 let V be RealLinearSpace; ::_thesis: 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 let W be Subspace of V; ::_thesis: 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 let A be Subset of V; ::_thesis: ( A is linearly-independent & A c= the carrier of W implies A is linearly-independent Subset of W ) assume that A1: A is linearly-independent and A2: A c= the carrier of W ; ::_thesis: A is linearly-independent Subset of W reconsider A9 = A as Subset of W by A2; now__::_thesis:_not_A9_is_linearly-dependent assume A9 is linearly-dependent ; ::_thesis: contradiction then consider K being Linear_Combination of A9 such that A3: Sum K = 0. W and A4: Carrier K <> {} by RLVECT_3:def_1; consider L being Linear_Combination of V such that A5: Carrier L = Carrier K and A6: Sum L = Sum K by Th11; reconsider L = L as Linear_Combination of A by A5, RLVECT_2:def_6; Sum L = 0. V by A3, A6, RLSUB_1:11; hence contradiction by A1, A4, A5, RLVECT_3:def_1; ::_thesis: verum end; hence A is linearly-independent Subset of W ; ::_thesis: verum end; theorem Th16: :: RLVECT_5:16 for V being RealLinearSpace for W being Subspace of V for A being Basis of W ex B being Basis of V st A c= B proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V for A being Basis of W ex B being Basis of V st A c= B let W be Subspace of V; ::_thesis: for A being Basis of W ex B being Basis of V st A c= B let A be Basis of W; ::_thesis: ex B being Basis of V st A c= B A is linearly-independent by RLVECT_3:def_3; then A is linearly-independent Subset of V by Th14; then consider I being Basis of V such that A1: A c= I by Th2; take I ; ::_thesis: A c= I thus A c= I by A1; ::_thesis: verum end; theorem Th17: :: RLVECT_5:17 for V being RealLinearSpace 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 let V be RealLinearSpace; ::_thesis: 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 let A be Subset of V; ::_thesis: ( A is linearly-independent implies 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 ) assume A1: A is linearly-independent ; ::_thesis: 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 let v be VECTOR of V; ::_thesis: ( v in A implies for B being Subset of V st B = A \ {v} holds not v in Lin B ) assume v in A ; ::_thesis: for B being Subset of V st B = A \ {v} holds not v in Lin B then A2: {v} is Subset of A by SUBSET_1:41; v in {v} by TARSKI:def_1; then v in Lin {v} by RLVECT_3:15; then consider K being Linear_Combination of {v} such that A3: v = Sum K by RLVECT_3:14; let B be Subset of V; ::_thesis: ( B = A \ {v} implies not v in Lin B ) assume A4: B = A \ {v} ; ::_thesis: not v in Lin B B c= A by A4, XBOOLE_1:36; then A5: B \/ {v} c= A \/ A by A2, XBOOLE_1:13; assume v in Lin B ; ::_thesis: contradiction then consider L being Linear_Combination of B such that A6: v = Sum L by RLVECT_3:14; A7: ( Carrier L c= B & Carrier K c= {v} ) by RLVECT_2:def_6; then (Carrier L) \/ (Carrier K) c= B \/ {v} by XBOOLE_1:13; then ( Carrier (L - K) c= (Carrier L) \/ (Carrier K) & (Carrier L) \/ (Carrier K) c= A ) by A5, RLVECT_2:55, XBOOLE_1:1; then Carrier (L - K) c= A by XBOOLE_1:1; then A8: L - K is Linear_Combination of A by RLVECT_2:def_6; A9: for x being VECTOR of V st x in Carrier L holds K . x = 0 proof let x be VECTOR of V; ::_thesis: ( x in Carrier L implies K . x = 0 ) assume x in Carrier L ; ::_thesis: K . x = 0 then not x in Carrier K by A4, A7, XBOOLE_0:def_5; hence K . x = 0 by RLVECT_2:19; ::_thesis: verum end; A10: now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_ x_in_Carrier_(L_-_K) let x be set ; ::_thesis: ( x in Carrier L implies x in Carrier (L - K) ) assume that A11: x in Carrier L and A12: not x in Carrier (L - K) ; ::_thesis: contradiction reconsider x = x as VECTOR of V by A11; A13: L . x <> 0 by A11, RLVECT_2:19; (L - K) . x = (L . x) - (K . x) by RLVECT_2:54 .= (L . x) - 0 by A9, A11 .= L . x ; hence contradiction by A12, A13, RLVECT_2:19; ::_thesis: verum end; {v} is linearly-independent by A1, A2, RLVECT_3:5; then v <> 0. V by RLVECT_3:8; then not Carrier L is empty by A6, RLVECT_2:34; then ex w being set st w in Carrier L by XBOOLE_0:def_1; then A14: not Carrier (L - K) is empty by A10; 0. V = (Sum L) + (- (Sum K)) by A6, A3, RLVECT_1:5 .= (Sum L) + (Sum (- K)) by RLVECT_3:3 .= Sum (L + (- K)) by RLVECT_3:1 .= Sum (L - K) by RLVECT_2:def_13 ; hence contradiction by A1, A8, A14, RLVECT_3:def_1; ::_thesis: verum end; theorem Th18: :: RLVECT_5:18 for V being RealLinearSpace 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 let V be RealLinearSpace; ::_thesis: 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 let I be Basis of V; ::_thesis: 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 let A be non empty Subset of V; ::_thesis: ( A misses I implies for B being Subset of V st B = I \/ A holds B is linearly-dependent ) assume A1: A misses I ; ::_thesis: for B being Subset of V st B = I \/ A holds B is linearly-dependent consider v being set such that A2: v in A by XBOOLE_0:def_1; let B be Subset of V; ::_thesis: ( B = I \/ A implies B is linearly-dependent ) assume A3: B = I \/ A ; ::_thesis: B is linearly-dependent A4: A c= B by A3, XBOOLE_1:7; reconsider v = v as VECTOR of V by A2; reconsider Bv = B \ {v} as Subset of V ; A5: I \ {v} c= B \ {v} by A3, XBOOLE_1:7, XBOOLE_1:33; not v in I by A1, A2, XBOOLE_0:3; then I c= Bv by A5, ZFMISC_1:57; then A6: Lin I is Subspace of Lin Bv by RLVECT_3:20; assume A7: B is linearly-independent ; ::_thesis: contradiction v in Lin I by Th13; hence contradiction by A7, A2, A4, A6, Th17, RLSUB_1:8; ::_thesis: verum end; theorem Th19: :: RLVECT_5:19 for V being RealLinearSpace 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 let V be RealLinearSpace; ::_thesis: 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 let W be Subspace of V; ::_thesis: for A being Subset of V st A c= the carrier of W holds Lin A is Subspace of W let A be Subset of V; ::_thesis: ( A c= the carrier of W implies Lin A is Subspace of W ) assume A1: A c= the carrier of W ; ::_thesis: Lin A is Subspace of W now__::_thesis:_for_w_being_set_st_w_in_the_carrier_of_(Lin_A)_holds_ w_in_the_carrier_of_W let w be set ; ::_thesis: ( w in the carrier of (Lin A) implies w in the carrier of W ) assume w in the carrier of (Lin A) ; ::_thesis: w in the carrier of W then w in Lin A by STRUCT_0:def_5; then consider L being Linear_Combination of A such that A2: w = Sum L by RLVECT_3:14; Carrier L c= A by RLVECT_2:def_6; then ex K being Linear_Combination of W st ( Carrier K = Carrier L & Sum L = Sum K ) by A1, Th12, XBOOLE_1:1; hence w in the carrier of W by A2; ::_thesis: verum end; then the carrier of (Lin A) c= the carrier of W by TARSKI:def_3; hence Lin A is Subspace of W by RLSUB_1:28; ::_thesis: verum end; theorem Th20: :: RLVECT_5:20 for V being RealLinearSpace 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 let V be RealLinearSpace; ::_thesis: 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 let W be Subspace of V; ::_thesis: for A being Subset of V for B being Subset of W st A = B holds Lin A = Lin B let A be Subset of V; ::_thesis: for B being Subset of W st A = B holds Lin A = Lin B let B be Subset of W; ::_thesis: ( A = B implies Lin A = Lin B ) reconsider B9 = Lin B, V9 = V as RealLinearSpace ; A1: B9 is Subspace of V9 by RLSUB_1:27; assume A2: A = B ; ::_thesis: Lin A = Lin B now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Lin_A)_holds_ x_in_the_carrier_of_(Lin_B) let x be set ; ::_thesis: ( x in the carrier of (Lin A) implies x in the carrier of (Lin B) ) assume x in the carrier of (Lin A) ; ::_thesis: x in the carrier of (Lin B) then x in Lin A by STRUCT_0:def_5; then consider L being Linear_Combination of A such that A3: x = Sum L by RLVECT_3:14; Carrier L c= A by RLVECT_2:def_6; then consider K being Linear_Combination of W such that A4: Carrier K = Carrier L and A5: Sum K = Sum L by A2, Th12, XBOOLE_1:1; reconsider K = K as Linear_Combination of B by A2, A4, RLVECT_2:def_6; x = Sum K by A3, A5; then x in Lin B by RLVECT_3:14; hence x in the carrier of (Lin B) by STRUCT_0:def_5; ::_thesis: verum end; then A6: the carrier of (Lin A) c= the carrier of (Lin B) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(Lin_B)_holds_ x_in_the_carrier_of_(Lin_A) let x be set ; ::_thesis: ( x in the carrier of (Lin B) implies x in the carrier of (Lin A) ) assume x in the carrier of (Lin B) ; ::_thesis: x in the carrier of (Lin A) then x in Lin B by STRUCT_0:def_5; then consider K being Linear_Combination of B such that A7: x = Sum K by RLVECT_3:14; consider L being Linear_Combination of V such that A8: Carrier L = Carrier K and A9: Sum L = Sum K by Th11; reconsider L = L as Linear_Combination of A by A2, A8, RLVECT_2:def_6; x = Sum L by A7, A9; then x in Lin A by RLVECT_3:14; hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum end; then the carrier of (Lin B) c= the carrier of (Lin A) by TARSKI:def_3; then the carrier of (Lin A) = the carrier of (Lin B) by A6, XBOOLE_0:def_10; hence Lin A = Lin B by A1, RLSUB_1:30; ::_thesis: verum end; begin theorem Th21: :: RLVECT_5:21 for V being RealLinearSpace for A, B being finite Subset of V for 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 RealLinearSpace; ::_thesis: for A, B being finite Subset of V for 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}) ) let A, B be finite Subset of V; ::_thesis: for 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}) ) let v be VECTOR of V; ::_thesis: ( v in Lin (A \/ B) & not v in Lin B implies ex w being VECTOR of V st ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) ) assume that A1: v in Lin (A \/ B) and A2: not v in Lin B ; ::_thesis: ex w being VECTOR of V st ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) consider L being Linear_Combination of A \/ B such that A3: v = Sum L by A1, RLVECT_3:14; A4: Carrier L c= A \/ B by RLVECT_2:def_6; now__::_thesis:_ex_w_being_VECTOR_of_V_st_ (_w_in_A_&_not_L_._w_=_0_) assume A5: for w being VECTOR of V st w in A holds L . w = 0 ; ::_thesis: contradiction now__::_thesis:_for_x_being_set_st_x_in_Carrier_L_holds_ not_x_in_A let x be set ; ::_thesis: ( x in Carrier L implies not x in A ) assume that A6: x in Carrier L and A7: x in A ; ::_thesis: contradiction ex u being VECTOR of V st ( x = u & L . u <> 0 ) by A6, Th3; hence contradiction by A5, A7; ::_thesis: verum 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_6; hence contradiction by A2, A3, RLVECT_3:14; ::_thesis: verum end; then consider w being VECTOR of V such that A8: w in A and A9: L . w <> 0 ; set a = L . w; take w ; ::_thesis: ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) 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_8; A13: w in Carrier L by A9, Th3; then reconsider Fw1 = F -| w as FinSequence of the carrier of V by A11, FINSEQ_4:41; reconsider Fw2 = F |-- w as FinSequence of the carrier of V by A11, A13, FINSEQ_4:50; A14: rng Fw1 misses rng Fw2 by A10, A11, A13, FINSEQ_4:57; set Fw = Fw1 ^ Fw2; F just_once_values w by A10, A11, A13, FINSEQ_4:8; then A15: Fw1 ^ Fw2 = F - {w} by FINSEQ_4:54; then A16: rng (Fw1 ^ Fw2) = (Carrier L) \ {w} by A11, FINSEQ_3:65; F = ((F -| w) ^ <*w*>) ^ (F |-- w) by A11, A13, FINSEQ_4:51; then F = Fw1 ^ (<*w*> ^ Fw2) by FINSEQ_1:32; then L (#) F = (L (#) Fw1) ^ (L (#) (<*w*> ^ Fw2)) by RLVECT_3:34 .= (L (#) Fw1) ^ ((L (#) <*w*>) ^ (L (#) Fw2)) by RLVECT_3:34 .= ((L (#) Fw1) ^ (L (#) <*w*>)) ^ (L (#) Fw2) by FINSEQ_1:32 .= ((L (#) Fw1) ^ <*((L . w) * w)*>) ^ (L (#) Fw2) by RLVECT_2:26 ; then A17: Sum (L (#) F) = Sum ((L (#) Fw1) ^ (<*((L . w) * w)*> ^ (L (#) Fw2))) by FINSEQ_1:32 .= (Sum (L (#) Fw1)) + (Sum (<*((L . w) * w)*> ^ (L (#) Fw2))) by RLVECT_1:41 .= (Sum (L (#) Fw1)) + ((Sum <*((L . w) * w)*>) + (Sum (L (#) Fw2))) by RLVECT_1:41 .= (Sum (L (#) Fw1)) + ((Sum (L (#) Fw2)) + ((L . w) * w)) by RLVECT_1:44 .= ((Sum (L (#) Fw1)) + (Sum (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:def_3 .= (Sum ((L (#) Fw1) ^ (L (#) Fw2))) + ((L . w) * w) by RLVECT_1:41 .= (Sum (L (#) (Fw1 ^ Fw2))) + ((L . w) * w) by RLVECT_3:34 ; v in {v} by TARSKI:def_1; then v in Lin {v} by RLVECT_3:15; then consider Lv being Linear_Combination of {v} such that A18: v = Sum Lv by RLVECT_3:14; consider K being Linear_Combination of V such that A19: Carrier K = (rng (Fw1 ^ Fw2)) /\ (Carrier L) and A20: L (#) (Fw1 ^ Fw2) = K (#) (Fw1 ^ Fw2) by Th7; rng (Fw1 ^ Fw2) = (rng F) \ {w} by A15, FINSEQ_3:65; then A21: Carrier K = rng (Fw1 ^ Fw2) by A11, A19, XBOOLE_1:28; A22: (Carrier L) \ {w} c= (A \/ B) \ {w} by A4, XBOOLE_1:33; then reconsider K = K as Linear_Combination of (A \/ B) \ {w} by A16, A21, RLVECT_2:def_6; (L . w) " <> 0 by A9, XCMPLX_1:202; then A23: Carrier (((L . w) ") * ((- K) + Lv)) = Carrier ((- K) + Lv) by RLVECT_2:42; set LC = ((L . w) ") * ((- K) + Lv); Carrier ((- K) + Lv) c= (Carrier (- K)) \/ (Carrier Lv) by RLVECT_2:37; then A24: Carrier ((- K) + Lv) c= (Carrier K) \/ (Carrier Lv) by RLVECT_2:51; Carrier Lv c= {v} by RLVECT_2:def_6; then (Carrier K) \/ (Carrier Lv) c= ((A \/ B) \ {w}) \/ {v} by A16, A21, A22, XBOOLE_1:13; then Carrier ((- K) + Lv) c= ((A \/ B) \ {w}) \/ {v} by A24, XBOOLE_1:1; then A25: ((L . w) ") * ((- K) + Lv) is Linear_Combination of ((A \/ B) \ {w}) \/ {v} by A23, RLVECT_2:def_6; ( Fw1 is one-to-one & Fw2 is one-to-one ) by A10, A11, A13, FINSEQ_4:52, FINSEQ_4:53; then Fw1 ^ Fw2 is one-to-one by A14, FINSEQ_3:91; then Sum (K (#) (Fw1 ^ Fw2)) = Sum K by A21, RLVECT_2:def_8; then ((L . w) ") * v = (((L . w) ") * (Sum K)) + (((L . w) ") * ((L . w) * w)) by A3, A12, A17, A20, RLVECT_1:def_5 .= (((L . w) ") * (Sum K)) + ((((L . w) ") * (L . w)) * w) by RLVECT_1:def_7 .= (((L . w) ") * (Sum K)) + (1 * w) by A9, XCMPLX_0:def_7 .= (((L . w) ") * (Sum K)) + w by RLVECT_1:def_8 ; then w = (((L . w) ") * v) - (((L . w) ") * (Sum K)) by RLSUB_2:61 .= ((L . w) ") * (v - (Sum K)) by RLVECT_1:34 .= ((L . w) ") * ((- (Sum K)) + v) by RLVECT_1:def_11 ; then w = ((L . w) ") * ((Sum (- K)) + (Sum Lv)) by A18, RLVECT_3:3 .= ((L . w) ") * (Sum ((- K) + Lv)) by RLVECT_3:1 .= Sum (((L . w) ") * ((- K) + Lv)) by RLVECT_3:2 ; hence ( w in A & w in Lin (((A \/ B) \ {w}) \/ {v}) ) by A8, A25, RLVECT_3:14; ::_thesis: verum end; theorem Th22: :: RLVECT_5:22 for V being RealLinearSpace for A, B being finite Subset of V st RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult 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) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) proof let V be RealLinearSpace; ::_thesis: for A, B being finite Subset of V st RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult 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) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) defpred S1[ Element of NAT ] means for n being Element of NAT for A, B being finite Subset of V st card A = n & card B = $1 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult 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 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ); A1: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A2: S1[m] ; ::_thesis: S1[m + 1] let n be Element of NAT ; ::_thesis: for A, B being finite Subset of V st card A = n & card B = m + 1 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent holds ( m + 1 <= n & ex C being finite Subset of V st ( C c= A & card C = n - (m + 1) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) let A, B be finite Subset of V; ::_thesis: ( card A = n & card B = m + 1 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent implies ( m + 1 <= n & ex C being finite Subset of V st ( C c= A & card C = n - (m + 1) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) ) assume that A3: card A = n and A4: card B = m + 1 and A5: RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A and A6: B is linearly-independent ; ::_thesis: ( m + 1 <= n & ex C being finite Subset of V st ( C c= A & card C = n - (m + 1) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) consider v being set such that A7: v in B by A4, CARD_1:27, XBOOLE_0:def_1; reconsider v = v as VECTOR of V by A7; set Bv = B \ {v}; A8: B \ {v} is linearly-independent by A6, RLVECT_3:5, XBOOLE_1:36; {v} is Subset of B by A7, SUBSET_1:41; then A9: card (B \ {v}) = (card B) - (card {v}) by CARD_2:44 .= (m + 1) - 1 by A4, CARD_1:30 .= m ; then consider C being finite Subset of V such that A10: C c= A and A11: card C = n - m and A12: RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin ((B \ {v}) \/ C) by A2, A3, A5, A8; A13: not v in Lin (B \ {v}) by A6, A7, Th17; A14: now__::_thesis:_not_m_=_n assume m = n ; ::_thesis: contradiction then consider C being finite Subset of V such that C c= A and A15: card C = m - m and A16: RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin ((B \ {v}) \/ C) by A2, A3, A5, A9, A8; C = {} by A15; then B \ {v} is Basis of V by A8, A16, RLVECT_3:def_3; hence contradiction by A13, Th13; ::_thesis: verum end; v in Lin ((B \ {v}) \/ C) by A12, STRUCT_0:def_5; then consider w being VECTOR of V such that A17: w in C and A18: w in Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) by A13, Th21; set Cw = C \ {w}; ((B \ {v}) \ {w}) \/ {v} c= (B \ {v}) \/ {v} by XBOOLE_1:9, XBOOLE_1:36; then (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= (C \ {w}) \/ ((B \ {v}) \/ {v}) by XBOOLE_1:9; then A19: (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) c= B \/ (C \ {w}) by A7, Lm1; {w} is Subset of C by A17, SUBSET_1:41; then A20: card (C \ {w}) = (card C) - (card {w}) by CARD_2:44 .= (n - m) - 1 by A11, CARD_1:30 .= n - (m + 1) ; C \ {w} c= C by XBOOLE_1:36; then A21: C \ {w} c= A by A10, XBOOLE_1:1; ((C \/ (B \ {v})) \ {w}) \/ {v} = ((C \ {w}) \/ ((B \ {v}) \ {w})) \/ {v} by XBOOLE_1:42 .= (C \ {w}) \/ (((B \ {v}) \ {w}) \/ {v}) by XBOOLE_1:4 ; then Lin (((C \/ (B \ {v})) \ {w}) \/ {v}) is Subspace of Lin (B \/ (C \ {w})) by A19, RLVECT_3:20; then A22: w in Lin (B \/ (C \ {w})) by A18, RLSUB_1:8; A23: ( B \ {v} c= B & C = (C \ {w}) \/ {w} ) by A17, Lm1, XBOOLE_1:36; now__::_thesis:_for_x_being_set_st_x_in_(B_\_{v})_\/_C_holds_ x_in_the_carrier_of_(Lin_(B_\/_(C_\_{w}))) let x be set ; ::_thesis: ( x in (B \ {v}) \/ C implies x in the carrier of (Lin (B \/ (C \ {w}))) ) assume x in (B \ {v}) \/ C ; ::_thesis: x in the carrier of (Lin (B \/ (C \ {w}))) then ( x in B \ {v} or x in C ) by XBOOLE_0:def_3; then ( x in B or x in C \ {w} or x in {w} ) by A23, XBOOLE_0:def_3; then ( x in B \/ (C \ {w}) or x in {w} ) by XBOOLE_0:def_3; then ( x in Lin (B \/ (C \ {w})) or x = w ) by RLVECT_3:15, TARSKI:def_1; hence x in the carrier of (Lin (B \/ (C \ {w}))) by A22, STRUCT_0:def_5; ::_thesis: verum end; then (B \ {v}) \/ C c= the carrier of (Lin (B \/ (C \ {w}))) by TARSKI:def_3; then Lin ((B \ {v}) \/ C) is Subspace of Lin (B \/ (C \ {w})) by Th19; then A24: the carrier of (Lin ((B \ {v}) \/ C)) c= the carrier of (Lin (B \/ (C \ {w}))) by RLSUB_1:def_2; the carrier of (Lin (B \/ (C \ {w}))) c= the carrier of V by RLSUB_1:def_2; then the carrier of (Lin (B \/ (C \ {w}))) = the carrier of V by A12, A24, XBOOLE_0:def_10; then A25: RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ (C \ {w})) by A12, RLSUB_1:30; m <= n by A2, A3, A5, A9, A8; then m < n by A14, XXREAL_0:1; hence ( m + 1 <= n & ex C being finite Subset of V st ( C c= A & card C = n - (m + 1) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) by A21, A20, A25, NAT_1:13; ::_thesis: verum end; A26: S1[ 0 ] proof let n be Element of NAT ; ::_thesis: for A, B being finite Subset of V st card A = n & card B = 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent holds ( 0 <= n & ex C being finite Subset of V st ( C c= A & card C = n - 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) let A, B be finite Subset of V; ::_thesis: ( card A = n & card B = 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent implies ( 0 <= n & ex C being finite Subset of V st ( C c= A & card C = n - 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) ) assume that A27: card A = n and A28: card B = 0 and A29: RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A and B is linearly-independent ; ::_thesis: ( 0 <= n & ex C being finite Subset of V st ( C c= A & card C = n - 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) B = {} by A28; then A = B \/ A ; hence ( 0 <= n & ex C being finite Subset of V st ( C c= A & card C = n - 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) by A27, A29, NAT_1:2; ::_thesis: verum end; A30: for m being Element of NAT holds S1[m] from NAT_1:sch_1(A26, A1); let A, B be finite Subset of V; ::_thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent implies ( card B <= card A & ex C being finite Subset of V st ( C c= A & card C = (card A) - (card B) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) ) assume ( RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B is linearly-independent ) ; ::_thesis: ( card B <= card A & ex C being finite Subset of V st ( C c= A & card C = (card A) - (card B) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) hence ( card B <= card A & ex C being finite Subset of V st ( C c= A & card C = (card A) - (card B) & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin (B \/ C) ) ) by A30; ::_thesis: verum end; begin definition let V be RealLinearSpace; attrV is finite-dimensional means :Def1: :: RLVECT_5:def 1 ex A being finite Subset of V st A is Basis of V; end; :: deftheorem Def1 defines finite-dimensional RLVECT_5:def_1_:_ for V being RealLinearSpace holds ( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V ); registration cluster non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional for RLSStruct ; existence ex b1 being RealLinearSpace st ( b1 is strict & b1 is finite-dimensional ) proof set V = the RealLinearSpace; take (0). the RealLinearSpace ; ::_thesis: ( (0). the RealLinearSpace is strict & (0). the RealLinearSpace is finite-dimensional ) thus (0). the RealLinearSpace is strict ; ::_thesis: (0). the RealLinearSpace is finite-dimensional take A = {} the carrier of ((0). the RealLinearSpace); :: according to RLVECT_5:def_1 ::_thesis: A is Basis of (0). the RealLinearSpace Lin A = (0). ((0). the RealLinearSpace) by RLVECT_3:16; then ( A is linearly-independent & Lin A = RLSStruct(# the carrier of ((0). the RealLinearSpace), the ZeroF of ((0). the RealLinearSpace), the U5 of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace) #) ) by RLSUB_1:36, RLVECT_3:7; hence A is Basis of (0). the RealLinearSpace by RLVECT_3:def_3; ::_thesis: verum end; end; theorem Th23: :: RLVECT_5:23 for V being RealLinearSpace st V is finite-dimensional holds for I being Basis of V holds I is finite proof let V be RealLinearSpace; ::_thesis: ( V is finite-dimensional implies for I being Basis of V holds I is finite ) assume V is finite-dimensional ; ::_thesis: for I being Basis of V holds I is finite then consider A being finite Subset of V such that A1: A is Basis of V by Def1; let B be Basis of V; ::_thesis: B is finite consider p being FinSequence such that A2: rng p = A by FINSEQ_1:52; reconsider p = 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 Element of NAT st ( i in dom p & Sum L = p . i ) } ; set C = union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } ; A3: union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } or x in B ) assume x in union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } ; ::_thesis: x in B then consider R being set such that A4: x in R and A5: R in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } by TARSKI:def_4; ex L being Linear_Combination of B st ( R = Carrier L & ex i being Element of NAT st ( i in dom p & Sum L = p . i ) ) by A5; then R c= B by RLVECT_2:def_6; hence x in B by A4; ::_thesis: verum end; then reconsider C = union { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } as Subset of V by XBOOLE_1:1; for v being VECTOR of V holds ( v in (Omega). V iff v in Lin C ) proof let v be VECTOR of V; ::_thesis: ( v in (Omega). V iff v in Lin C ) hereby ::_thesis: ( v in Lin C implies v in (Omega). V ) assume v in (Omega). V ; ::_thesis: v in Lin C then v in RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by RLSUB_1:def_4; then v in Lin A by A1, RLVECT_3:def_3; then consider LA being Linear_Combination of A such that A6: v = Sum LA by RLVECT_3:14; Carrier LA c= the carrier of (Lin C) proof let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in Carrier LA or w in the carrier of (Lin C) ) assume A7: w in Carrier LA ; ::_thesis: w in the carrier of (Lin C) then reconsider w9 = w as VECTOR of V ; w9 in Lin B by Th13; then consider LB being Linear_Combination of B such that A8: w = Sum LB by RLVECT_3:14; Carrier LA c= A by RLVECT_2:def_6; then ex i being set st ( i in dom p & w = p . i ) by A2, A7, FUNCT_1:def_3; then A9: Carrier LB in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } by A8; Carrier LB c= C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier LB or x in C ) assume x in Carrier LB ; ::_thesis: x in C hence x in C by A9, TARSKI:def_4; ::_thesis: verum end; then LB is Linear_Combination of C by RLVECT_2:def_6; then w in Lin C by A8, RLVECT_3:14; hence w in the carrier of (Lin C) by STRUCT_0:def_5; ::_thesis: verum end; then ex LC being Linear_Combination of C st Sum LA = Sum LC by Th9; hence v in Lin C by A6, RLVECT_3:14; ::_thesis: verum end; assume v in Lin C ; ::_thesis: v in (Omega). V v in the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ; then v in the carrier of ((Omega). V) by RLSUB_1:def_4; hence v in (Omega). V by STRUCT_0:def_5; ::_thesis: verum end; then (Omega). V = Lin C by RLSUB_1:31; then A10: RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin C by RLSUB_1:def_4; A11: B is linearly-independent by RLVECT_3:def_3; then C is linearly-independent by A3, RLVECT_3:5; then A12: C is Basis of V by A10, RLVECT_3:def_3; B c= C proof set D = B \ C; assume not B c= C ; ::_thesis: contradiction then ex v being set st ( v in B & not v in C ) by TARSKI:def_3; then reconsider D = B \ C as non empty Subset of V by XBOOLE_0:def_5; reconsider B = B as Subset of V ; C \/ (B \ C) = C \/ B by XBOOLE_1:39 .= B by A3, XBOOLE_1:12 ; then B = C \/ D ; hence contradiction by A11, A12, Th18, XBOOLE_1:79; ::_thesis: verum end; then A13: B = C by A3, XBOOLE_0:def_10; defpred S1[ set , set ] means ex L being Linear_Combination of B st ( $2 = Carrier L & Sum L = p . $1 ); A14: for i being Nat st i in Seg (len p) holds ex x being set st S1[i,x] proof let i be Nat; ::_thesis: ( i in Seg (len p) implies ex x being set st S1[i,x] ) assume i in Seg (len p) ; ::_thesis: ex x being set st S1[i,x] then i in dom p by FINSEQ_1:def_3; then p . i in the carrier of V by FINSEQ_2:11; then p . i in Lin B by Th13; then consider L being Linear_Combination of B such that A15: p . i = Sum L by RLVECT_3:14; S1[i, Carrier L] by A15; hence ex x being set st S1[i,x] ; ::_thesis: verum end; ex q being FinSequence st ( dom q = Seg (len p) & ( for i being Nat st i in Seg (len p) holds S1[i,q . i] ) ) from FINSEQ_1:sch_1(A14); then consider q being FinSequence such that A16: dom q = Seg (len p) and A17: for i being Nat st i in Seg (len p) holds S1[i,q . i] ; A18: dom p = dom q by A16, FINSEQ_1:def_3; A19: for i being Nat for y1, y2 being set st i in Seg (len p) & S1[i,y1] & S1[i,y2] holds y1 = y2 proof let i be Nat; ::_thesis: for y1, y2 being set st i in Seg (len p) & S1[i,y1] & S1[i,y2] holds y1 = y2 let y1, y2 be set ; ::_thesis: ( i in Seg (len p) & S1[i,y1] & S1[i,y2] implies y1 = y2 ) assume that i in Seg (len p) and A20: S1[i,y1] and A21: S1[i,y2] ; ::_thesis: y1 = y2 consider L1 being Linear_Combination of B such that A22: ( y1 = Carrier L1 & Sum L1 = p . i ) by A20; consider L2 being Linear_Combination of B such that A23: ( y2 = Carrier L2 & Sum L2 = p . i ) by A21; ( Carrier L1 c= B & Carrier L2 c= B ) by RLVECT_2:def_6; hence y1 = y2 by A11, A22, A23, Th1; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in__{__(Carrier_L)_where_L_is_Linear_Combination_of_B_:_ex_i_being_Element_of_NAT_st_ (_i_in_dom_p_&_Sum_L_=_p_._i_)__}__holds_ x_in_rng_q let x be set ; ::_thesis: ( x in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } implies x in rng q ) assume x in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } ; ::_thesis: x in rng q then consider L being Linear_Combination of B such that A24: x = Carrier L and A25: ex i being Element of NAT st ( i in dom p & Sum L = p . i ) ; consider i being Element of NAT such that A26: i in dom p and A27: Sum L = p . i by A25; S1[i,q . i] by A16, A17, A18, A26; then x = q . i by A19, A16, A18, A24, A26, A27; hence x in rng q by A18, A26, FUNCT_1:def_3; ::_thesis: verum end; then A28: { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } c= rng q by TARSKI:def_3; for R being set st R in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } holds R is finite proof let R be set ; ::_thesis: ( R in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } implies R is finite ) assume R in { (Carrier L) where L is Linear_Combination of B : ex i being Element of NAT st ( i in dom p & Sum L = p . i ) } ; ::_thesis: R is finite then ex L being Linear_Combination of B st ( R = Carrier L & ex i being Element of NAT st ( i in dom p & Sum L = p . i ) ) ; hence R is finite ; ::_thesis: verum end; hence B is finite by A13, A28, FINSET_1:7; ::_thesis: verum end; theorem :: RLVECT_5:24 for V being RealLinearSpace st V is finite-dimensional holds for A being Subset of V st A is linearly-independent holds A is finite proof let V be RealLinearSpace; ::_thesis: ( V is finite-dimensional implies for A being Subset of V st A is linearly-independent holds A is finite ) assume A1: V is finite-dimensional ; ::_thesis: for A being Subset of V st A is linearly-independent holds A is finite let A be Subset of V; ::_thesis: ( A is linearly-independent implies A is finite ) assume A is linearly-independent ; ::_thesis: A is finite then consider B being Basis of V such that A2: A c= B by Th2; B is finite by A1, Th23; hence A is finite by A2; ::_thesis: verum end; theorem Th25: :: RLVECT_5:25 for V being RealLinearSpace st V is finite-dimensional holds for A, B being Basis of V holds card A = card B proof let V be RealLinearSpace; ::_thesis: ( V is finite-dimensional implies for A, B being Basis of V holds card A = card B ) assume A1: V is finite-dimensional ; ::_thesis: for A, B being Basis of V holds card A = card B let A, B be Basis of V; ::_thesis: card A = card B reconsider A9 = A, B9 = B as finite Subset of V by A1, Th23; ( RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin B & A9 is linearly-independent ) by RLVECT_3:def_3; then A2: card A9 <= card B9 by Th22; ( RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = Lin A & B9 is linearly-independent ) by RLVECT_3:def_3; then card B9 <= card A9 by Th22; hence card A = card B by A2, XXREAL_0:1; ::_thesis: verum end; theorem Th26: :: RLVECT_5:26 for V being RealLinearSpace holds (0). V is finite-dimensional proof let V be RealLinearSpace; ::_thesis: (0). V is finite-dimensional reconsider V9 = (0). V as strict RealLinearSpace ; reconsider I = {} the carrier of V9 as finite Subset of V9 ; the carrier of V9 = {(0. V)} by RLSUB_1:def_3 .= {(0. V9)} by RLSUB_1:11 .= the carrier of ((0). V9) by RLSUB_1:def_3 ; then A1: V9 = (0). V9 by RLSUB_1:32; ( I is linearly-independent & Lin I = (0). V9 ) by RLVECT_3:7, RLVECT_3:16; then I is Basis of V9 by A1, RLVECT_3:def_3; hence (0). V is finite-dimensional by Def1; ::_thesis: verum end; theorem Th27: :: RLVECT_5:27 for V being RealLinearSpace for W being Subspace of V st V is finite-dimensional holds W is finite-dimensional proof let V be RealLinearSpace; ::_thesis: for W being Subspace of V st V is finite-dimensional holds W is finite-dimensional let W be Subspace of V; ::_thesis: ( V is finite-dimensional implies W is finite-dimensional ) set A = the Basis of W; consider I being Basis of V such that A1: the Basis of W c= I by Th16; assume V is finite-dimensional ; ::_thesis: W is finite-dimensional then I is finite by Th23; hence W is finite-dimensional by A1, Def1; ::_thesis: verum end; registration let V be RealLinearSpace; cluster non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional for Subspace of V; existence ex b1 being Subspace of V st ( b1 is finite-dimensional & b1 is strict ) proof take (0). V ; ::_thesis: ( (0). V is finite-dimensional & (0). V is strict ) thus ( (0). V is finite-dimensional & (0). V is strict ) by Th26; ::_thesis: verum end; end; registration let V be finite-dimensional RealLinearSpace; cluster -> finite-dimensional for Subspace of V; correctness coherence for b1 being Subspace of V holds b1 is finite-dimensional ; by Th27; end; registration let V be finite-dimensional RealLinearSpace; cluster non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional for Subspace of V; existence ex b1 being Subspace of V st b1 is strict proof (0). V is strict finite-dimensional Subspace of V ; hence ex b1 being Subspace of V st b1 is strict ; ::_thesis: verum end; end; begin definition let V be RealLinearSpace; assume A1: V is finite-dimensional ; func dim V -> Element of NAT means :Def2: :: RLVECT_5:def 2 for I being Basis of V holds it = card I; existence ex b1 being Element of NAT st for I being Basis of V holds b1 = card I proof consider A being finite Subset of V such that A2: A is Basis of V by A1, Def1; consider n being Element of NAT such that A3: n = card A ; for I being Basis of V holds card I = n by A1, A2, A3, Th25; hence ex b1 being Element of NAT st for I being Basis of V holds b1 = card I ; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st ( for I being Basis of V holds b1 = card I ) & ( for I being Basis of V holds b2 = card I ) holds b1 = b2 proof let n, m be Element of NAT ; ::_thesis: ( ( for I being Basis of V holds n = card I ) & ( for I being Basis of V holds m = card I ) implies n = m ) 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 ; ::_thesis: n = m consider A being finite Subset of V such that A6: A is Basis of V by A1, Def1; card A = n by A4, A6; hence n = m by A5, A6; ::_thesis: verum end; end; :: deftheorem Def2 defines dim RLVECT_5:def_2_:_ for V being RealLinearSpace st V is finite-dimensional holds for b2 being Element of NAT holds ( b2 = dim V iff for I being Basis of V holds b2 = card I ); theorem Th28: :: RLVECT_5:28 for V being finite-dimensional RealLinearSpace for W being Subspace of V holds dim W <= dim V proof let V be finite-dimensional RealLinearSpace; ::_thesis: for W being Subspace of V holds dim W <= dim V let W be Subspace of V; ::_thesis: dim W <= dim V reconsider V9 = V as RealLinearSpace ; set I = the Basis of V9; reconsider I = the Basis of V9 as finite Subset of V by Th23; set A = the Basis of W; reconsider A = the Basis of W as Subset of W ; A is linearly-independent by RLVECT_3:def_3; then reconsider A9 = A as finite Subset of V by Th14, Th23; ( Lin I = RLSStruct(# the carrier of V9, the ZeroF of V9, the U5 of V9, the Mult of V9 #) & A is linearly-independent Subset of V ) by Th14, RLVECT_3:def_3; then A1: card A9 <= card I by Th22; dim W = card A by Def2; hence dim W <= dim V by A1, Def2; ::_thesis: verum end; theorem Th29: :: RLVECT_5:29 for V being finite-dimensional RealLinearSpace for A being Subset of V st A is linearly-independent holds card A = dim (Lin A) proof let V be finite-dimensional RealLinearSpace; ::_thesis: for A being Subset of V st A is linearly-independent holds card A = dim (Lin A) let A be Subset of V; ::_thesis: ( A is linearly-independent implies card A = dim (Lin A) ) assume A1: A is linearly-independent ; ::_thesis: card A = dim (Lin A) set W = Lin A; now__::_thesis:_for_x_being_set_st_x_in_A_holds_ x_in_the_carrier_of_(Lin_A) let x be set ; ::_thesis: ( x in A implies x in the carrier of (Lin A) ) assume x in A ; ::_thesis: x in the carrier of (Lin A) then x in Lin A by RLVECT_3:15; hence x in the carrier of (Lin A) by STRUCT_0:def_5; ::_thesis: verum end; then reconsider B = A as linearly-independent Subset of (Lin A) by A1, Th15, TARSKI:def_3; Lin A = Lin B by Th20; then reconsider B = B as Basis of Lin A by RLVECT_3:def_3; card B = dim (Lin A) by Def2; hence card A = dim (Lin A) ; ::_thesis: verum end; theorem Th30: :: RLVECT_5:30 for V being finite-dimensional RealLinearSpace holds dim V = dim ((Omega). V) proof let V be finite-dimensional RealLinearSpace; ::_thesis: dim V = dim ((Omega). V) consider I being finite Subset of V such that A1: I is Basis of V by Def1; A2: (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by RLSUB_1:def_4 .= Lin I by A1, RLVECT_3:def_3 ; ( card I = dim V & I is linearly-independent ) by A1, Def2, RLVECT_3:def_3; hence dim V = dim ((Omega). V) by A2, Th29; ::_thesis: verum end; theorem :: RLVECT_5:31 for V being finite-dimensional RealLinearSpace for W being Subspace of V holds ( dim V = dim W iff (Omega). V = (Omega). W ) proof let V be finite-dimensional RealLinearSpace; ::_thesis: for W being Subspace of V holds ( dim V = dim W iff (Omega). V = (Omega). W ) let W be Subspace of V; ::_thesis: ( dim V = dim W iff (Omega). V = (Omega). W ) consider A being finite Subset of V such that A1: A is Basis of V by Def1; hereby ::_thesis: ( (Omega). V = (Omega). W implies dim V = dim W ) set A = the Basis of W; consider B being Basis of V such that A2: the Basis of W c= B by Th16; the carrier of W c= the carrier of V by RLSUB_1:def_2; then reconsider A9 = the Basis of W as finite Subset of V by Th23, XBOOLE_1:1; reconsider B9 = B as finite Subset of V by Th23; assume dim V = dim W ; ::_thesis: (Omega). V = (Omega). W then A3: card the Basis of W = dim V by Def2 .= card B by Def2 ; A4: now__::_thesis:_not_the_Basis_of_W_<>_B assume the Basis of W <> B ; ::_thesis: contradiction then the Basis of W c< B by A2, XBOOLE_0:def_8; then card A9 < card B9 by CARD_2:48; hence contradiction by A3; ::_thesis: verum end; reconsider B = B as Subset of V ; reconsider A = the Basis of W as Subset of W ; (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by RLSUB_1:def_4 .= Lin B by RLVECT_3:def_3 .= Lin A by A4, Th20 .= RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) by RLVECT_3:def_3 .= (Omega). W by RLSUB_1:def_4 ; hence (Omega). V = (Omega). W ; ::_thesis: verum end; consider B being finite Subset of W such that A5: B is Basis of W by Def1; A6: A is linearly-independent by A1, RLVECT_3:def_3; assume (Omega). V = (Omega). W ; ::_thesis: dim V = dim W then RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = (Omega). W by RLSUB_1:def_4 .= RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) by RLSUB_1:def_4 ; then A7: Lin A = RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) by A1, RLVECT_3:def_3 .= Lin B by A5, RLVECT_3:def_3 ; A8: B is linearly-independent by A5, RLVECT_3:def_3; reconsider B = B as Subset of W ; reconsider A = A as Subset of V ; dim V = card A by A1, Def2 .= dim (Lin B) by A6, A7, Th29 .= card B by A8, Th29 .= dim W by A5, Def2 ; hence dim V = dim W ; ::_thesis: verum end; theorem Th32: :: RLVECT_5:32 for V being finite-dimensional RealLinearSpace holds ( dim V = 0 iff (Omega). V = (0). V ) proof let V be finite-dimensional RealLinearSpace; ::_thesis: ( dim V = 0 iff (Omega). V = (0). V ) consider I being finite Subset of V such that A1: I is Basis of V by Def1; hereby ::_thesis: ( (Omega). V = (0). V implies dim V = 0 ) consider I being finite Subset of V such that A2: I is Basis of V by Def1; assume dim V = 0 ; ::_thesis: (Omega). V = (0). V then card I = 0 by A2, Def2; then A3: I = {} the carrier of V ; (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by RLSUB_1:def_4 .= Lin I by A2, RLVECT_3:def_3 .= (0). V by A3, RLVECT_3:16 ; hence (Omega). V = (0). V ; ::_thesis: verum end; A4: now__::_thesis:_not_I_=_{(0._V)} assume I = {(0. V)} ; ::_thesis: contradiction then I is linearly-dependent by RLVECT_3:8; hence contradiction by A1, RLVECT_3:def_3; ::_thesis: verum end; assume (Omega). V = (0). V ; ::_thesis: dim V = 0 then RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = (0). V by RLSUB_1:def_4; then Lin I = (0). V by A1, RLVECT_3:def_3; then ( I = {} or I = {(0. V)} ) by RLVECT_3:17; hence dim V = 0 by A1, A4, Def2, CARD_1:27; ::_thesis: verum end; theorem :: RLVECT_5:33 for V being finite-dimensional RealLinearSpace 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 RealLinearSpace; ::_thesis: ( dim V = 1 iff ex v being VECTOR of V st ( v <> 0. V & (Omega). V = Lin {v} ) ) hereby ::_thesis: ( ex v being VECTOR of V st ( v <> 0. V & (Omega). V = Lin {v} ) implies dim V = 1 ) consider I being finite Subset of V such that A1: I is Basis of V by Def1; assume dim V = 1 ; ::_thesis: ex v being VECTOR of V st ( v <> 0. V & (Omega). V = Lin {v} ) then card I = 1 by A1, Def2; then consider v being set such that A2: I = {v} by CARD_2:42; v in I by A2, TARSKI:def_1; then reconsider v = v as VECTOR of V ; {v} is linearly-independent by A1, A2, RLVECT_3:def_3; then A3: v <> 0. V by RLVECT_3:8; Lin {v} = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by A1, A2, RLVECT_3:def_3; hence ex v being VECTOR of V st ( v <> 0. V & (Omega). V = Lin {v} ) by A3, RLSUB_1:def_4; ::_thesis: verum end; given v being VECTOR of V such that A4: ( v <> 0. V & (Omega). V = Lin {v} ) ; ::_thesis: dim V = 1 ( {v} is linearly-independent & Lin {v} = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) by A4, RLSUB_1:def_4, RLVECT_3:8; then A5: {v} is Basis of V by RLVECT_3:def_3; card {v} = 1 by CARD_1:30; hence dim V = 1 by A5, Def2; ::_thesis: verum end; theorem :: RLVECT_5:34 for V being finite-dimensional RealLinearSpace 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 RealLinearSpace; ::_thesis: ( dim V = 2 iff ex u, v being VECTOR of V st ( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) ) hereby ::_thesis: ( ex u, v being VECTOR of V st ( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) implies dim V = 2 ) consider I being finite Subset of V such that A1: I is Basis of V by Def1; assume dim V = 2 ; ::_thesis: ex u, v being VECTOR of V st ( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) then A2: card I = 2 by A1, Def2; then consider u being set such that A3: u in I by CARD_1:27, XBOOLE_0:def_1; reconsider u = u as VECTOR of V by A3; now__::_thesis:_not_I_c=_{u} assume I c= {u} ; ::_thesis: contradiction then card I <= card {u} by NAT_1:43; then 2 <= 1 by A2, CARD_1:30; hence contradiction ; ::_thesis: verum end; then consider v being set such that A4: v in I and A5: not v in {u} by TARSKI:def_3; reconsider v = v as VECTOR of V by A4; A6: v <> u by A5, TARSKI:def_1; A7: now__::_thesis:_I_c=_{u,v} assume not I c= {u,v} ; ::_thesis: contradiction then consider w being set such that A8: w in I and A9: not w in {u,v} by TARSKI:def_3; for x being set st x in {u,v,w} holds x in I by A3, A4, A8, ENUMSET1:def_1; then {u,v,w} c= I by TARSKI:def_3; then A10: card {u,v,w} <= card I by NAT_1:43; ( w <> u & w <> v ) by A9, TARSKI:def_2; then 3 <= 2 by A2, A6, A10, CARD_2:58; hence contradiction ; ::_thesis: verum end; for x being set st x in {u,v} holds x in I by A3, A4, TARSKI:def_2; then {u,v} c= I by TARSKI:def_3; then A11: I = {u,v} by A7, XBOOLE_0:def_10; then A12: {u,v} is linearly-independent by A1, RLVECT_3:def_3; Lin {u,v} = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by A1, A11, RLVECT_3:def_3 .= (Omega). V by RLSUB_1:def_4 ; hence ex u, v being VECTOR of V st ( u <> v & {u,v} is linearly-independent & (Omega). V = Lin {u,v} ) by A6, A12; ::_thesis: verum end; given u, v being VECTOR of V such that A13: u <> v and A14: {u,v} is linearly-independent and A15: (Omega). V = Lin {u,v} ; ::_thesis: dim V = 2 Lin {u,v} = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by A15, RLSUB_1:def_4; then A16: {u,v} is Basis of V by A14, RLVECT_3:def_3; card {u,v} = 2 by A13, CARD_2:57; hence dim V = 2 by A16, Def2; ::_thesis: verum end; theorem Th35: :: RLVECT_5:35 for V being finite-dimensional RealLinearSpace for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2) proof let V be finite-dimensional RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2) let W1, W2 be Subspace of V; ::_thesis: (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2) reconsider V = V as RealLinearSpace ; reconsider W1 = W1, W2 = W2 as Subspace of V ; consider I being finite Subset of (W1 /\ W2) such that A1: I is Basis of W1 /\ W2 by Def1; W1 /\ W2 is Subspace of W2 by RLSUB_2:16; then consider I2 being Basis of W2 such that A2: I c= I2 by A1, Th16; W1 /\ W2 is Subspace of W1 by RLSUB_2:16; then consider I1 being Basis of W1 such that A3: I c= I1 by A1, Th16; reconsider I2 = I2 as finite Subset of W2 by Th23; reconsider I1 = I1 as finite Subset of W1 by Th23; A4: now__::_thesis:_I1_/\_I2_c=_I I1 is linearly-independent by RLVECT_3:def_3; then reconsider I19 = I1 as linearly-independent Subset of V by Th14; assume not I1 /\ I2 c= I ; ::_thesis: contradiction then consider x being set such that A5: x in I1 /\ I2 and A6: not x in I by TARSKI:def_3; x in I1 by A5, XBOOLE_0:def_4; then x in Lin I1 by RLVECT_3:15; then x in RLSStruct(# the carrier of W1, the ZeroF of W1, the U5 of W1, the Mult of W1 #) by RLVECT_3:def_3; then A7: x in the carrier of W1 by STRUCT_0:def_5; A8: the carrier of W1 c= the carrier of V by RLSUB_1:def_2; then reconsider x9 = x as VECTOR of V by A7; now__::_thesis:_for_y_being_set_st_y_in_I_\/_{x}_holds_ y_in_the_carrier_of_V let y be set ; ::_thesis: ( y in I \/ {x} implies y in the carrier of V ) the carrier of (W1 /\ W2) c= the carrier of V by RLSUB_1:def_2; then A9: I c= the carrier of V by XBOOLE_1:1; assume y in I \/ {x} ; ::_thesis: y in the carrier of V then ( y in I or y in {x} ) by XBOOLE_0:def_3; then ( y in the carrier of V or y = x ) by A9, TARSKI:def_1; hence y in the carrier of V by A7, A8; ::_thesis: verum end; then reconsider Ix = I \/ {x} as Subset of V by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_I_\/_{x}_holds_ y_in_I19 let y be set ; ::_thesis: ( y in I \/ {x} implies y in I19 ) assume y in I \/ {x} ; ::_thesis: y in I19 then ( y in I or y in {x} ) by XBOOLE_0:def_3; then ( y in I1 or y = x ) by A3, TARSKI:def_1; hence y in I19 by A5, XBOOLE_0:def_4; ::_thesis: verum end; then A10: Ix c= I19 by TARSKI:def_3; x in {x} by TARSKI:def_1; then A11: x9 in Ix by XBOOLE_0:def_3; x in I2 by A5, XBOOLE_0:def_4; then x in Lin I2 by RLVECT_3:15; then x in RLSStruct(# the carrier of W2, the ZeroF of W2, the U5 of W2, the Mult of W2 #) by RLVECT_3:def_3; then x in the carrier of W2 by STRUCT_0:def_5; then x in the carrier of W1 /\ the carrier of W2 by A7, XBOOLE_0:def_4; then x in the carrier of (W1 /\ W2) by RLSUB_2:def_2; then A12: x in RLSStruct(# the carrier of (W1 /\ W2), the ZeroF of (W1 /\ W2), the U5 of (W1 /\ W2), the Mult of (W1 /\ W2) #) by STRUCT_0:def_5; the carrier of (W1 /\ W2) c= the carrier of V by RLSUB_1:def_2; then reconsider I9 = I as Subset of V by XBOOLE_1:1; A13: Lin I = Lin I9 by Th20; Ix \ {x} = I \ {x} by XBOOLE_1:40 .= I by A6, ZFMISC_1:57 ; then not x9 in Lin I9 by A10, A11, Th17, RLVECT_3:5; hence contradiction by A1, A12, A13, RLVECT_3:def_3; ::_thesis: verum end; set A = I1 \/ I2; now__::_thesis:_for_v_being_set_st_v_in_I1_\/_I2_holds_ v_in_the_carrier_of_(W1_+_W2) let v be set ; ::_thesis: ( v in I1 \/ I2 implies v in the carrier of (W1 + W2) ) A14: ( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by RLSUB_1:def_2; assume v in I1 \/ I2 ; ::_thesis: v in the carrier of (W1 + W2) then A15: ( v in I1 or v in I2 ) by XBOOLE_0:def_3; then ( v in the carrier of W1 or v in the carrier of W2 ) ; then reconsider v9 = v as VECTOR of V by A14; ( v9 in W1 or v9 in W2 ) by A15, STRUCT_0:def_5; then v9 in W1 + W2 by RLSUB_2:2; hence v in the carrier of (W1 + W2) by STRUCT_0:def_5; ::_thesis: verum end; then reconsider A = I1 \/ I2 as finite Subset of (W1 + W2) by TARSKI:def_3; I c= I1 /\ I2 by A3, A2, XBOOLE_1:19; then I = I1 /\ I2 by A4, XBOOLE_0:def_10; then A16: card A = ((card I1) + (card I2)) - (card I) by CARD_2:45; for L being Linear_Combination of A st Sum L = 0. (W1 + W2) holds Carrier L = {} proof ( W1 is Subspace of W1 + W2 & I1 is linearly-independent ) by RLSUB_2:7, RLVECT_3:def_3; then reconsider I19 = I1 as linearly-independent Subset of (W1 + W2) by Th14; reconsider W29 = W2 as Subspace of W1 + W2 by RLSUB_2:7; reconsider W19 = W1 as Subspace of W1 + W2 by RLSUB_2:7; let L be Linear_Combination of A; ::_thesis: ( Sum L = 0. (W1 + W2) implies Carrier L = {} ) assume A17: Sum L = 0. (W1 + W2) ; ::_thesis: Carrier L = {} A18: I1 misses (Carrier L) \ I1 by XBOOLE_1:79; set B = (Carrier L) /\ I1; consider F being FinSequence of the carrier of (W1 + W2) such that A19: F is one-to-one and A20: rng F = Carrier L and A21: Sum L = Sum (L (#) F) by RLVECT_2:def_8; reconsider B = (Carrier L) /\ I1 as Subset of (rng F) by A20, XBOOLE_1:17; reconsider F1 = F - (B `), F2 = F - B as FinSequence of the carrier of (W1 + W2) by FINSEQ_3:86; consider L1 being Linear_Combination of W1 + W2 such that A22: Carrier L1 = (rng F1) /\ (Carrier L) and A23: L1 (#) F1 = L (#) F1 by Th7; F1 is one-to-one by A19, FINSEQ_3:87; then A24: Sum (L (#) F1) = Sum L1 by A22, A23, Th6, XBOOLE_1:17; rng F c= rng F ; then reconsider X = rng F as Subset of (rng F) ; consider L2 being Linear_Combination of W1 + W2 such that A25: Carrier L2 = (rng F2) /\ (Carrier L) and A26: L2 (#) F2 = L (#) F2 by Th7; F2 is one-to-one by A19, FINSEQ_3:87; then A27: Sum (L (#) F2) = Sum L2 by A25, A26, Th6, XBOOLE_1:17; X \ (B `) = X /\ ((B `) `) by SUBSET_1:13 .= B by XBOOLE_1:28 ; then rng F1 = B by FINSEQ_3:65; then A28: Carrier L1 = I1 /\ ((Carrier L) /\ (Carrier L)) by A22, XBOOLE_1:16 .= (Carrier L) /\ I1 ; then consider K1 being Linear_Combination of W19 such that Carrier K1 = Carrier L1 and A29: Sum K1 = Sum L1 by Th12; rng F2 = (Carrier L) \ ((Carrier L) /\ I1) by A20, FINSEQ_3:65 .= (Carrier L) \ I1 by XBOOLE_1:47 ; then A30: Carrier L2 = (Carrier L) \ I1 by A25, XBOOLE_1:28, XBOOLE_1:36; then (Carrier L1) /\ (Carrier L2) = (Carrier L) /\ (I1 /\ ((Carrier L) \ I1)) by A28, XBOOLE_1:16 .= (Carrier L) /\ {} by A18, XBOOLE_0:def_7 .= {} ; then A31: Carrier L1 misses Carrier L2 by XBOOLE_0:def_7; A32: Carrier L c= I1 \/ I2 by RLVECT_2:def_6; then A33: Carrier L2 c= I2 by A30, XBOOLE_1:43; Carrier L2 c= I2 by A32, A30, XBOOLE_1:43; then consider K2 being Linear_Combination of W29 such that Carrier K2 = Carrier L2 and A34: Sum K2 = Sum L2 by Th12, XBOOLE_1:1; A35: Sum K1 in W1 by STRUCT_0:def_5; ex P being Permutation of (dom F) st (F - (B `)) ^ (F - B) = F * P by FINSEQ_3:115; then A36: 0. (W1 + W2) = Sum (L (#) (F1 ^ F2)) by A17, A21, Th4 .= Sum ((L (#) F1) ^ (L (#) F2)) by RLVECT_3:34 .= (Sum L1) + (Sum L2) by A24, A27, RLVECT_1:41 ; then Sum L1 = - (Sum L2) by RLVECT_1:def_10 .= - (Sum K2) by A34, RLSUB_1:15 ; then Sum K1 in W2 by A29, STRUCT_0:def_5; then Sum K1 in W1 /\ W2 by A35, RLSUB_2:3; then Sum K1 in Lin I by A1, RLVECT_3:def_3; then consider KI being Linear_Combination of I such that A37: Sum K1 = Sum KI by RLVECT_3:14; A38: Carrier L = (Carrier L1) \/ (Carrier L2) by A28, A30, XBOOLE_1:51; A39: now__::_thesis:_Carrier_L_c=_Carrier_(L1_+_L2) assume not Carrier L c= Carrier (L1 + L2) ; ::_thesis: contradiction then consider x being set such that A40: x in Carrier L and A41: not x in Carrier (L1 + L2) by TARSKI:def_3; reconsider x = x as VECTOR of (W1 + W2) by A40; A42: 0 = (L1 + L2) . x by A41, RLVECT_2:19 .= (L1 . x) + (L2 . x) by RLVECT_2:def_10 ; percases ( x in Carrier L1 or x in Carrier L2 ) by A38, A40, XBOOLE_0:def_3; supposeA43: x in Carrier L1 ; ::_thesis: contradiction then not x in Carrier L2 by A31, XBOOLE_0:3; then A44: L2 . x = 0 by RLVECT_2:19; ex v being VECTOR of (W1 + W2) st ( x = v & L1 . v <> 0 ) by A43, Th3; hence contradiction by A42, A44; ::_thesis: verum end; supposeA45: x in Carrier L2 ; ::_thesis: contradiction then not x in Carrier L1 by A31, XBOOLE_0:3; then A46: L1 . x = 0 by RLVECT_2:19; ex v being VECTOR of (W1 + W2) st ( x = v & L2 . v <> 0 ) by A45, Th3; hence contradiction by A42, A46; ::_thesis: verum end; end; end; A47: I \/ I2 = I2 by A2, XBOOLE_1:12; A48: I2 is linearly-independent by RLVECT_3:def_3; A49: Carrier L1 c= I1 by A28, XBOOLE_1:17; W1 /\ W2 is Subspace of W1 + W2 by RLSUB_2:22; then consider LI being Linear_Combination of W1 + W2 such that A50: Carrier LI = Carrier KI and A51: Sum LI = Sum KI by Th11; Carrier LI c= I by A50, RLVECT_2:def_6; then Carrier LI c= I19 by A3, XBOOLE_1:1; then A52: LI = L1 by A49, A29, A37, A51, Th1; Carrier LI c= I by A50, RLVECT_2:def_6; then ( Carrier (LI + L2) c= (Carrier LI) \/ (Carrier L2) & (Carrier LI) \/ (Carrier L2) c= I2 ) by A47, A33, RLVECT_2:37, XBOOLE_1:13; then A53: Carrier (LI + L2) c= I2 by XBOOLE_1:1; W2 is Subspace of W1 + W2 by RLSUB_2:7; then consider K being Linear_Combination of W2 such that A54: Carrier K = Carrier (LI + L2) and A55: Sum K = Sum (LI + L2) by A53, Th12, XBOOLE_1:1; reconsider K = K as Linear_Combination of I2 by A53, A54, RLVECT_2:def_6; 0. W2 = (Sum LI) + (Sum L2) by A29, A36, A37, A51, RLSUB_1:12 .= Sum K by A55, RLVECT_3:1 ; then {} = Carrier (L1 + L2) by A54, A52, A48, RLVECT_3:def_1; hence Carrier L = {} by A39; ::_thesis: verum end; then A56: A is linearly-independent by RLVECT_3:def_1; the carrier of (W1 + W2) c= the carrier of V by RLSUB_1:def_2; then reconsider A9 = A as Subset of V by XBOOLE_1:1; A57: card I2 = dim W2 by Def2; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(W1_+_W2)_holds_ x_in_the_carrier_of_(Lin_A9) let x be set ; ::_thesis: ( x in the carrier of (W1 + W2) implies x in the carrier of (Lin A9) ) assume x in the carrier of (W1 + W2) ; ::_thesis: x in the carrier of (Lin A9) then x in W1 + W2 by STRUCT_0:def_5; then consider w1, w2 being VECTOR of V such that A58: w1 in W1 and A59: w2 in W2 and A60: x = w1 + w2 by RLSUB_2:1; reconsider w1 = w1 as VECTOR of W1 by A58, STRUCT_0:def_5; w1 in Lin I1 by Th13; then consider K1 being Linear_Combination of I1 such that A61: w1 = Sum K1 by RLVECT_3:14; reconsider w2 = w2 as VECTOR of W2 by A59, STRUCT_0:def_5; w2 in Lin I2 by Th13; then consider K2 being Linear_Combination of I2 such that A62: w2 = Sum K2 by RLVECT_3:14; consider L2 being Linear_Combination of V such that A63: Carrier L2 = Carrier K2 and A64: Sum L2 = Sum K2 by Th11; A65: Carrier L2 c= I2 by A63, RLVECT_2:def_6; consider L1 being Linear_Combination of V such that A66: Carrier L1 = Carrier K1 and A67: Sum L1 = Sum K1 by Th11; set L = L1 + L2; Carrier L1 c= I1 by A66, RLVECT_2:def_6; then ( Carrier (L1 + L2) c= (Carrier L1) \/ (Carrier L2) & (Carrier L1) \/ (Carrier L2) c= I1 \/ I2 ) by A65, RLVECT_2:37, XBOOLE_1:13; then Carrier (L1 + L2) c= I1 \/ I2 by XBOOLE_1:1; then reconsider L = L1 + L2 as Linear_Combination of A9 by RLVECT_2:def_6; x = Sum L by A60, A61, A67, A62, A64, RLVECT_3:1; then x in Lin A9 by RLVECT_3:14; hence x in the carrier of (Lin A9) by STRUCT_0:def_5; ::_thesis: verum end; then the carrier of (W1 + W2) c= the carrier of (Lin A9) by TARSKI:def_3; then A68: W1 + W2 is Subspace of Lin A9 by RLSUB_1:28; Lin A9 = Lin A by Th20; then Lin A = W1 + W2 by A68, RLSUB_1:26; then A is Basis of W1 + W2 by A56, RLVECT_3:def_3; then A69: card A = dim (W1 + W2) by Def2; card I = dim (W1 /\ W2) by A1, Def2; hence (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2) by A57, A16, A69, Def2; ::_thesis: verum end; theorem :: RLVECT_5:36 for V being finite-dimensional RealLinearSpace for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V) proof let V be finite-dimensional RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V holds dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V) let W1, W2 be Subspace of V; ::_thesis: dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V) A1: ( dim (W1 + W2) <= dim V & (dim V) + ((dim (W1 /\ W2)) - (dim V)) = dim (W1 /\ W2) ) by Th28; ((dim W1) + (dim W2)) - (dim V) = ((dim (W1 + W2)) + (dim (W1 /\ W2))) - (dim V) by Th35 .= (dim (W1 + W2)) + ((dim (W1 /\ W2)) - (dim V)) ; hence dim (W1 /\ W2) >= ((dim W1) + (dim W2)) - (dim V) by A1, XREAL_1:6; ::_thesis: verum end; theorem :: RLVECT_5:37 for V being finite-dimensional RealLinearSpace for 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 RealLinearSpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds dim V = (dim W1) + (dim W2) let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies dim V = (dim W1) + (dim W2) ) assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: dim V = (dim W1) + (dim W2) then A2: RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = W1 + W2 by RLSUB_2:def_4; W1 /\ W2 = (0). V by A1, RLSUB_2:def_4; then (Omega). (W1 /\ W2) = (0). V by RLSUB_1:def_4 .= (0). (W1 /\ W2) by RLSUB_1:36 ; then dim (W1 /\ W2) = 0 by Th32; then (dim W1) + (dim W2) = (dim (W1 + W2)) + 0 by Th35 .= dim ((Omega). V) by A2, RLSUB_1:def_4 .= dim V by Th30 ; hence dim V = (dim W1) + (dim W2) ; ::_thesis: verum end; Lm2: for n being Element of NAT for V being finite-dimensional RealLinearSpace st n <= dim V holds ex W being strict Subspace of V st dim W = n proof let n be Element of NAT ; ::_thesis: for V being finite-dimensional RealLinearSpace st n <= dim V holds ex W being strict Subspace of V st dim W = n let V be finite-dimensional RealLinearSpace; ::_thesis: ( n <= dim V implies ex W being strict Subspace of V st dim W = n ) consider I being finite Subset of V such that A1: I is Basis of V by Def1; assume n <= dim V ; ::_thesis: ex W being strict Subspace of V st dim W = n then n <= card I by A1, Def2; then consider A being finite Subset of I such that A2: card A = n by FINSEQ_4:72; reconsider A = A as Subset of V by XBOOLE_1:1; reconsider W = Lin A as strict finite-dimensional Subspace of V ; I is linearly-independent by A1, RLVECT_3:def_3; then dim W = n by A2, Th29, RLVECT_3:5; hence ex W being strict Subspace of V st dim W = n ; ::_thesis: verum end; theorem :: RLVECT_5:38 for n being Element of NAT for V being finite-dimensional RealLinearSpace holds ( n <= dim V iff ex W being strict Subspace of V st dim W = n ) by Lm2, Th28; definition let V be finite-dimensional RealLinearSpace; let n be Element of NAT ; funcn Subspaces_of V -> set means :Def3: :: RLVECT_5:def 3 for x being set holds ( x in it iff ex W being strict Subspace of V st ( W = x & dim W = n ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) proof set S = { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; take { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; ::_thesis: for x being set holds ( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) for x being set holds ( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) proof let x be set ; ::_thesis: ( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) hereby ::_thesis: ( ex W being strict Subspace of V st ( W = x & dim W = n ) implies x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ) assume x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } ; ::_thesis: ex W being strict Subspace of V st ( W = x & dim W = n ) then A1: ex A being Subset of V st ( x = Lin A & A is linearly-independent & card A = n ) ; then reconsider W = x as strict Subspace of V ; dim W = n by A1, Th29; hence ex W being strict Subspace of V st ( W = x & dim W = n ) ; ::_thesis: verum end; given W being strict Subspace of V such that A2: W = x and A3: dim W = n ; ::_thesis: x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } consider A being finite Subset of W such that A4: A is Basis of W by Def1; reconsider A = A as Subset of W ; A is linearly-independent by A4, RLVECT_3:def_3; then reconsider B = A as linearly-independent Subset of V by Th14; A5: x = Lin A by A2, A4, RLVECT_3:def_3 .= Lin B by Th20 ; then card B = n by A2, A3, Th29; hence x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } by A5; ::_thesis: verum end; hence for x being set holds ( x in { (Lin A) where A is Subset of V : ( A is linearly-independent & card A = n ) } iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) ) & ( for x being set holds ( x in b2 iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) ) holds b1 = b2 proof let S1, S2 be set ; ::_thesis: ( ( for x being set holds ( x in S1 iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) ) & ( for x being set holds ( x in S2 iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) ) implies S1 = S2 ) assume that A6: for x being set holds ( x in S1 iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) and A7: for x being set holds ( x in S2 iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) ; ::_thesis: S1 = S2 for x being set holds ( x in S1 iff x in S2 ) proof let x be set ; ::_thesis: ( x in S1 iff x in S2 ) hereby ::_thesis: ( x in S2 implies x in S1 ) assume x in S1 ; ::_thesis: x in S2 then ex W being strict Subspace of V st ( W = x & dim W = n ) by A6; hence x in S2 by A7; ::_thesis: verum end; assume x in S2 ; ::_thesis: x in S1 then ex W being strict Subspace of V st ( W = x & dim W = n ) by A7; hence x in S1 by A6; ::_thesis: verum end; hence S1 = S2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def3 defines Subspaces_of RLVECT_5:def_3_:_ for V being finite-dimensional RealLinearSpace for n being Element of NAT for b3 being set holds ( b3 = n Subspaces_of V iff for x being set holds ( x in b3 iff ex W being strict Subspace of V st ( W = x & dim W = n ) ) ); theorem :: RLVECT_5:39 for n being Element of NAT for V being finite-dimensional RealLinearSpace st n <= dim V holds not n Subspaces_of V is empty proof let n be Element of NAT ; ::_thesis: for V being finite-dimensional RealLinearSpace st n <= dim V holds not n Subspaces_of V is empty let V be finite-dimensional RealLinearSpace; ::_thesis: ( n <= dim V implies not n Subspaces_of V is empty ) assume n <= dim V ; ::_thesis: not n Subspaces_of V is empty then ex W being strict Subspace of V st dim W = n by Lm2; hence not n Subspaces_of V is empty by Def3; ::_thesis: verum end; theorem :: RLVECT_5:40 for n being Element of NAT for V being finite-dimensional RealLinearSpace st dim V < n holds n Subspaces_of V = {} proof let n be Element of NAT ; ::_thesis: for V being finite-dimensional RealLinearSpace st dim V < n holds n Subspaces_of V = {} let V be finite-dimensional RealLinearSpace; ::_thesis: ( dim V < n implies n Subspaces_of V = {} ) assume that A1: dim V < n and A2: n Subspaces_of V <> {} ; ::_thesis: contradiction consider x being set such that A3: x in n Subspaces_of V by A2, XBOOLE_0:def_1; ex W being strict Subspace of V st ( W = x & dim W = n ) by A3, Def3; hence contradiction by A1, Th28; ::_thesis: verum end; theorem :: RLVECT_5:41 for n being Element of NAT for V being finite-dimensional RealLinearSpace for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V proof let n be Element of NAT ; ::_thesis: for V being finite-dimensional RealLinearSpace for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V let V be finite-dimensional RealLinearSpace; ::_thesis: for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V let W be Subspace of V; ::_thesis: n Subspaces_of W c= n Subspaces_of V let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in n Subspaces_of W or x in n Subspaces_of V ) assume x in n Subspaces_of W ; ::_thesis: x in n Subspaces_of V then consider W1 being strict Subspace of W such that A1: W1 = x and A2: dim W1 = n by Def3; reconsider W1 = W1 as strict Subspace of V by RLSUB_1:27; W1 in n Subspaces_of V by A2, Def3; hence x in n Subspaces_of V by A1; ::_thesis: verum end;