:: RUSUB_3 semantic presentation begin definition let V be RealUnitarySpace; let A be Subset of V; func Lin A -> strict Subspace of V means :Def1: :: RUSUB_3:def 1 the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ; existence ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } proof set A1 = { (Sum l) where l is Linear_Combination of A : verum } ; { (Sum l) where l is Linear_Combination of A : verum } c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Sum l) where l is Linear_Combination of A : verum } or x in the carrier of V ) assume x in { (Sum l) where l is Linear_Combination of A : verum } ; ::_thesis: x in the carrier of V then ex l being Linear_Combination of A st x = Sum l ; hence x in the carrier of V ; ::_thesis: verum end; then reconsider A1 = { (Sum l) where l is Linear_Combination of A : verum } as Subset of V ; reconsider l = ZeroLC V as Linear_Combination of A by RLVECT_2:22; A1: A1 is linearly-closed proof thus for v, u being VECTOR of V st v in A1 & u in A1 holds v + u in A1 :: according to RLSUB_1:def_1 ::_thesis: for b1 being Element of REAL for b2 being Element of the carrier of V holds ( not b2 in A1 or b1 * b2 in A1 ) proof let v, u be VECTOR of V; ::_thesis: ( v in A1 & u in A1 implies v + u in A1 ) assume that A2: v in A1 and A3: u in A1 ; ::_thesis: v + u in A1 consider l1 being Linear_Combination of A such that A4: v = Sum l1 by A2; consider l2 being Linear_Combination of A such that A5: u = Sum l2 by A3; reconsider f = l1 + l2 as Linear_Combination of A by RLVECT_2:38; v + u = Sum f by A4, A5, RLVECT_3:1; hence v + u in A1 ; ::_thesis: verum end; let a be Real; ::_thesis: for b1 being Element of the carrier of V holds ( not b1 in A1 or a * b1 in A1 ) let v be VECTOR of V; ::_thesis: ( not v in A1 or a * v in A1 ) assume v in A1 ; ::_thesis: a * v in A1 then consider l being Linear_Combination of A such that A6: v = Sum l ; reconsider f = a * l as Linear_Combination of A by RLVECT_2:44; a * v = Sum f by A6, RLVECT_3:2; hence a * v in A1 ; ::_thesis: verum end; Sum l = 0. V by RLVECT_2:30; then 0. V in A1 ; hence ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } by A1, RUSUB_1:29; ::_thesis: verum end; uniqueness for b1, b2 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b2 = { (Sum l) where l is Linear_Combination of A : verum } holds b1 = b2 by RUSUB_1:24; end; :: deftheorem Def1 defines Lin RUSUB_3:def_1_:_ for V being RealUnitarySpace for A being Subset of V for b3 being strict Subspace of V holds ( b3 = Lin A iff the carrier of b3 = { (Sum l) where l is Linear_Combination of A : verum } ); theorem Th1: :: RUSUB_3:1 for V being RealUnitarySpace for A being Subset of V for x being set holds ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) proof let V be RealUnitarySpace; ::_thesis: for A being Subset of V for x being set holds ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) let A be Subset of V; ::_thesis: for x being set holds ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) let x be set ; ::_thesis: ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l ) thus ( x in Lin A implies ex l being Linear_Combination of A st x = Sum l ) ::_thesis: ( ex l being Linear_Combination of A st x = Sum l implies x in Lin A ) proof assume x in Lin A ; ::_thesis: ex l being Linear_Combination of A st x = Sum l then x in the carrier of (Lin A) by STRUCT_0:def_5; then x in { (Sum l) where l is Linear_Combination of A : verum } by Def1; hence ex l being Linear_Combination of A st x = Sum l ; ::_thesis: verum end; given k being Linear_Combination of A such that A1: x = Sum k ; ::_thesis: x in Lin A x in { (Sum l) where l is Linear_Combination of A : verum } by A1; then x in the carrier of (Lin A) by Def1; hence x in Lin A by STRUCT_0:def_5; ::_thesis: verum end; theorem Th2: :: RUSUB_3:2 for V being RealUnitarySpace for A being Subset of V for x being set st x in A holds x in Lin A proof deffunc H1( set ) -> Element of NAT = 0 ; let V be RealUnitarySpace; ::_thesis: for A being Subset of V for x being set st x in A holds x in Lin A let A be Subset of V; ::_thesis: for x being set st x in A holds x in Lin A let x be set ; ::_thesis: ( x in A implies x in Lin A ) assume A1: x in A ; ::_thesis: x in Lin A then reconsider v = x as VECTOR of V ; consider f being Function of the carrier of V,REAL such that A2: f . v = 1 and A3: for u being VECTOR of V st u <> v holds f . u = H1(u) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; ex T being finite Subset of V st for u being VECTOR of V st not u in T holds f . u = 0 proof take T = {v}; ::_thesis: for u being VECTOR of V st not u in T holds f . u = 0 let u be VECTOR of V; ::_thesis: ( not u in T implies f . u = 0 ) assume not u in T ; ::_thesis: f . u = 0 then u <> v by TARSKI:def_1; hence f . u = 0 by A3; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; A4: Carrier f c= {v} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} ) assume x in Carrier f ; ::_thesis: x in {v} then consider u being VECTOR of V such that A5: x = u and A6: f . u <> 0 ; u = v by A3, A6; hence x in {v} by A5, TARSKI:def_1; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def_6; A7: Sum f = 1 * v by A2, RLVECT_2:32 .= v by RLVECT_1:def_8 ; {v} c= A by A1, ZFMISC_1:31; then Carrier f c= A by A4, XBOOLE_1:1; then reconsider f = f as Linear_Combination of A by RLVECT_2:def_6; Sum f = v by A7; hence x in Lin A by Th1; ::_thesis: verum end; Lm1: for V being RealUnitarySpace for x being set holds ( x in (0). V iff x = 0. V ) proof let V be RealUnitarySpace; ::_thesis: for x being set holds ( x in (0). V iff x = 0. V ) let x be set ; ::_thesis: ( x in (0). V iff x = 0. V ) thus ( x in (0). V implies x = 0. V ) ::_thesis: ( x = 0. V implies x in (0). V ) proof assume x in (0). V ; ::_thesis: x = 0. V then x in the carrier of ((0). V) by STRUCT_0:def_5; then x in {(0. V)} by RUSUB_1:def_2; hence x = 0. V by TARSKI:def_1; ::_thesis: verum end; thus ( x = 0. V implies x in (0). V ) by RUSUB_1:11; ::_thesis: verum end; theorem :: RUSUB_3:3 for V being RealUnitarySpace holds Lin ({} the carrier of V) = (0). V proof let V be RealUnitarySpace; ::_thesis: Lin ({} the carrier of V) = (0). V set A = Lin ({} the carrier of V); now__::_thesis:_for_v_being_VECTOR_of_V_holds_ (_(_v_in_Lin_({}_the_carrier_of_V)_implies_v_in_(0)._V_)_&_(_v_in_(0)._V_implies_v_in_Lin_({}_the_carrier_of_V)_)_) let v be VECTOR of V; ::_thesis: ( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) ) thus ( v in Lin ({} the carrier of V) implies v in (0). V ) ::_thesis: ( v in (0). V implies v in Lin ({} the carrier of V) ) proof assume v in Lin ({} the carrier of V) ; ::_thesis: v in (0). V then A1: v in the carrier of (Lin ({} the carrier of V)) by STRUCT_0:def_5; the carrier of (Lin ({} the carrier of V)) = { (Sum l0) where l0 is Linear_Combination of {} the carrier of V : verum } by Def1; then ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1; then v = 0. V by RLVECT_2:31; hence v in (0). V by Lm1; ::_thesis: verum end; assume v in (0). V ; ::_thesis: v in Lin ({} the carrier of V) then v = 0. V by Lm1; hence v in Lin ({} the carrier of V) by RUSUB_1:11; ::_thesis: verum end; hence Lin ({} the carrier of V) = (0). V by RUSUB_1:25; ::_thesis: verum end; theorem :: RUSUB_3:4 for V being RealUnitarySpace for A being Subset of V holds ( not Lin A = (0). V or A = {} or A = {(0. V)} ) proof let V be RealUnitarySpace; ::_thesis: for A being Subset of V holds ( not Lin A = (0). V or A = {} or A = {(0. V)} ) let A be Subset of V; ::_thesis: ( not Lin A = (0). V or A = {} or A = {(0. V)} ) assume that A1: Lin A = (0). V and A2: A <> {} ; ::_thesis: A = {(0. V)} thus A c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in {(0. V)} ) assume x in A ; ::_thesis: x in {(0. V)} then x in Lin A by Th2; then x = 0. V by A1, Lm1; hence x in {(0. V)} by TARSKI:def_1; ::_thesis: verum end; set y = the Element of A; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in A ) assume x in {(0. V)} ; ::_thesis: x in A then A3: x = 0. V by TARSKI:def_1; ( the Element of A in A & the Element of A in Lin A ) by A2, Th2; hence x in A by A1, A3, Lm1; ::_thesis: verum end; theorem Th5: :: RUSUB_3:5 for V being RealUnitarySpace for W being strict Subspace of V for A being Subset of V st A = the carrier of W holds Lin A = W proof let V be RealUnitarySpace; ::_thesis: for W being strict Subspace of V for A being Subset of V st A = the carrier of W holds Lin A = W let W be strict Subspace of V; ::_thesis: for A being Subset of V st A = the carrier of W holds Lin A = W let A be Subset of V; ::_thesis: ( A = the carrier of W implies Lin A = W ) assume A1: A = the carrier of W ; ::_thesis: Lin A = W now__::_thesis:_for_v_being_VECTOR_of_V_holds_ (_(_v_in_Lin_A_implies_v_in_W_)_&_(_v_in_W_implies_v_in_Lin_A_)_) let v be VECTOR of V; ::_thesis: ( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) ) thus ( v in Lin A implies v in W ) ::_thesis: ( v in W implies v in Lin A ) proof assume v in Lin A ; ::_thesis: v in W then A2: ex l being Linear_Combination of A st v = Sum l by Th1; A is linearly-closed by A1, RUSUB_1:28; then v in the carrier of W by A1, A2, RLVECT_2:29; hence v in W by STRUCT_0:def_5; ::_thesis: verum end; ( v in W iff v in the carrier of W ) by STRUCT_0:def_5; hence ( v in W implies v in Lin A ) by A1, Th2; ::_thesis: verum end; hence Lin A = W by RUSUB_1:25; ::_thesis: verum end; theorem :: RUSUB_3:6 for V being strict RealUnitarySpace for A being Subset of V st A = the carrier of V holds Lin A = V proof let V be strict RealUnitarySpace; ::_thesis: for A being Subset of V st A = the carrier of V holds Lin A = V let A be Subset of V; ::_thesis: ( A = the carrier of V implies Lin A = V ) assume A = the carrier of V ; ::_thesis: Lin A = V then A = the carrier of ((Omega). V) by RUSUB_1:def_3; hence Lin A = (Omega). V by Th5 .= V by RUSUB_1:def_3 ; ::_thesis: verum end; Lm2: for V being RealUnitarySpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds W1 /\ W2 is Subspace of W3 proof let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds W1 /\ W2 is Subspace of W3 let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3 ) A1: W1 /\ W2 is Subspace of W1 by RUSUB_2:16; assume W1 is Subspace of W3 ; ::_thesis: W1 /\ W2 is Subspace of W3 hence W1 /\ W2 is Subspace of W3 by A1, RUSUB_1:21; ::_thesis: verum end; Lm3: for V being RealUnitarySpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds W1 is Subspace of W2 /\ W3 proof let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds W1 is Subspace of W2 /\ W3 let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of W2 /\ W3 ) assume A1: ( W1 is Subspace of W2 & W1 is Subspace of W3 ) ; ::_thesis: W1 is Subspace of W2 /\ W3 now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_W1_holds_ v_in_W2_/\_W3 let v be VECTOR of V; ::_thesis: ( v in W1 implies v in W2 /\ W3 ) assume v in W1 ; ::_thesis: v in W2 /\ W3 then ( v in W2 & v in W3 ) by A1, RUSUB_1:1; hence v in W2 /\ W3 by RUSUB_2:3; ::_thesis: verum end; hence W1 is Subspace of W2 /\ W3 by RUSUB_1:23; ::_thesis: verum end; Lm4: for V being RealUnitarySpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds W1 is Subspace of W2 + W3 proof let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds W1 is Subspace of W2 + W3 let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies W1 is Subspace of W2 + W3 ) A1: W2 is Subspace of W2 + W3 by RUSUB_2:7; assume W1 is Subspace of W2 ; ::_thesis: W1 is Subspace of W2 + W3 hence W1 is Subspace of W2 + W3 by A1, RUSUB_1:21; ::_thesis: verum end; Lm5: for V being RealUnitarySpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds W1 + W2 is Subspace of W3 proof let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds W1 + W2 is Subspace of W3 let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace of W3 ) assume A1: ( W1 is Subspace of W3 & W2 is Subspace of W3 ) ; ::_thesis: W1 + W2 is Subspace of W3 now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_W1_+_W2_holds_ v_in_W3 let v be VECTOR of V; ::_thesis: ( v in W1 + W2 implies v in W3 ) assume v in W1 + W2 ; ::_thesis: v in W3 then consider v1, v2 being VECTOR of V such that A2: ( v1 in W1 & v2 in W2 ) and A3: v = v1 + v2 by RUSUB_2:1; ( v1 in W3 & v2 in W3 ) by A1, A2, RUSUB_1:1; hence v in W3 by A3, RUSUB_1:14; ::_thesis: verum end; hence W1 + W2 is Subspace of W3 by RUSUB_1:23; ::_thesis: verum end; theorem Th7: :: RUSUB_3:7 for V being RealUnitarySpace for A, B being Subset of V st A c= B holds Lin A is Subspace of Lin B proof let V be RealUnitarySpace; ::_thesis: for A, B being Subset of V st A c= B holds Lin A is Subspace of Lin B let A, B be Subset of V; ::_thesis: ( A c= B implies Lin A is Subspace of Lin B ) assume A1: A c= B ; ::_thesis: Lin A is Subspace of Lin B now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_Lin_A_holds_ v_in_Lin_B let v be VECTOR of V; ::_thesis: ( v in Lin A implies v in Lin B ) assume v in Lin A ; ::_thesis: v in Lin B then consider l being Linear_Combination of A such that A2: v = Sum l by Th1; reconsider l = l as Linear_Combination of B by A1, RLVECT_2:21; Sum l = v by A2; hence v in Lin B by Th1; ::_thesis: verum end; hence Lin A is Subspace of Lin B by RUSUB_1:23; ::_thesis: verum end; theorem :: RUSUB_3:8 for V being strict RealUnitarySpace for A, B being Subset of V st Lin A = V & A c= B holds Lin B = V proof let V be strict RealUnitarySpace; ::_thesis: for A, B being Subset of V st Lin A = V & A c= B holds Lin B = V let A, B be Subset of V; ::_thesis: ( Lin A = V & A c= B implies Lin B = V ) assume ( Lin A = V & A c= B ) ; ::_thesis: Lin B = V then V is Subspace of Lin B by Th7; hence Lin B = V by RUSUB_1:20; ::_thesis: verum end; theorem :: RUSUB_3:9 for V being RealUnitarySpace for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B) proof let V be RealUnitarySpace; ::_thesis: for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B) let A, B be Subset of V; ::_thesis: Lin (A \/ B) = (Lin A) + (Lin B) now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_Lin_(A_\/_B)_holds_ v_in_(Lin_A)_+_(Lin_B) deffunc H1( set ) -> Element of NAT = 0 ; let v be VECTOR of V; ::_thesis: ( v in Lin (A \/ B) implies v in (Lin A) + (Lin B) ) assume v in Lin (A \/ B) ; ::_thesis: v in (Lin A) + (Lin B) then consider l being Linear_Combination of A \/ B such that A1: v = Sum l by Th1; deffunc H2( set ) -> set = l . $1; set D = (Carrier l) \ A; set C = (Carrier l) /\ A; defpred S1[ set ] means $1 in (Carrier l) /\ A; defpred S2[ set ] means $1 in (Carrier l) \ A; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_ (_(_x_in_(Carrier_l)_/\_A_implies_l_._x_in_REAL_)_&_(_not_x_in_(Carrier_l)_/\_A_implies_0_in_REAL_)_) let x be set ; ::_thesis: ( x in the carrier of V implies ( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ A implies 0 in REAL ) ) ) assume x in the carrier of V ; ::_thesis: ( ( x in (Carrier l) /\ A implies l . x in REAL ) & ( not x in (Carrier l) /\ A implies 0 in REAL ) ) then reconsider v = x as VECTOR of V ; for f being Function of the carrier of V,REAL holds f . v in REAL ; hence ( x in (Carrier l) /\ A implies l . x in REAL ) ; ::_thesis: ( not x in (Carrier l) /\ A implies 0 in REAL ) assume not x in (Carrier l) /\ A ; ::_thesis: 0 in REAL thus 0 in REAL ; ::_thesis: verum end; then A2: for x being set st x in the carrier of V holds ( ( S1[x] implies H2(x) in REAL ) & ( not S1[x] implies H1(x) in REAL ) ) ; consider f being Function of the carrier of V,REAL such that A3: for x being set st x in the carrier of V holds ( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A2); reconsider C = (Carrier l) /\ A as finite Subset of V ; reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; for u being VECTOR of V st not u in C holds f . u = 0 by A3; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; A4: Carrier f c= C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in C ) assume x in Carrier f ; ::_thesis: x in C then A5: ex u being VECTOR of V st ( x = u & f . u <> 0 ) ; assume not x in C ; ::_thesis: contradiction hence contradiction by A3, A5; ::_thesis: verum end; C c= A by XBOOLE_1:17; then Carrier f c= A by A4, XBOOLE_1:1; then reconsider f = f as Linear_Combination of A by RLVECT_2:def_6; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_ (_(_x_in_(Carrier_l)_\_A_implies_l_._x_in_REAL_)_&_(_not_x_in_(Carrier_l)_\_A_implies_0_in_REAL_)_) let x be set ; ::_thesis: ( x in the carrier of V implies ( ( x in (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ A implies 0 in REAL ) ) ) assume x in the carrier of V ; ::_thesis: ( ( x in (Carrier l) \ A implies l . x in REAL ) & ( not x in (Carrier l) \ A implies 0 in REAL ) ) then reconsider v = x as VECTOR of V ; for g being Function of the carrier of V,REAL holds g . v in REAL ; hence ( x in (Carrier l) \ A implies l . x in REAL ) ; ::_thesis: ( not x in (Carrier l) \ A implies 0 in REAL ) assume not x in (Carrier l) \ A ; ::_thesis: 0 in REAL thus 0 in REAL ; ::_thesis: verum end; then A6: for x being set st x in the carrier of V holds ( ( S2[x] implies H2(x) in REAL ) & ( not S2[x] implies H1(x) in REAL ) ) ; consider g being Function of the carrier of V,REAL such that A7: for x being set st x in the carrier of V holds ( ( S2[x] implies g . x = H2(x) ) & ( not S2[x] implies g . x = H1(x) ) ) from FUNCT_2:sch_5(A6); reconsider D = (Carrier l) \ A as finite Subset of V ; reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; for u being VECTOR of V st not u in D holds g . u = 0 by A7; then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3; A8: D c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in B ) assume x in D ; ::_thesis: x in B then A9: ( x in Carrier l & not x in A ) by XBOOLE_0:def_5; Carrier l c= A \/ B by RLVECT_2:def_6; hence x in B by A9, XBOOLE_0:def_3; ::_thesis: verum end; Carrier g c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in D ) assume x in Carrier g ; ::_thesis: x in D then A10: ex u being VECTOR of V st ( x = u & g . u <> 0 ) ; assume not x in D ; ::_thesis: contradiction hence contradiction by A7, A10; ::_thesis: verum end; then Carrier g c= B by A8, XBOOLE_1:1; then reconsider g = g as Linear_Combination of B by RLVECT_2:def_6; l = f + g proof let v be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: l . v = (f + g) . v now__::_thesis:_(f_+_g)_._v_=_l_._v percases ( v in C or not v in C ) ; supposeA11: v in C ; ::_thesis: (f + g) . v = l . v A12: now__::_thesis:_not_v_in_D assume v in D ; ::_thesis: contradiction then not v in A by XBOOLE_0:def_5; hence contradiction by A11, XBOOLE_0:def_4; ::_thesis: verum end; thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10 .= (l . v) + (g . v) by A3, A11 .= (l . v) + 0 by A7, A12 .= l . v ; ::_thesis: verum end; supposeA13: not v in C ; ::_thesis: l . v = (f + g) . v now__::_thesis:_(f_+_g)_._v_=_l_._v percases ( v in Carrier l or not v in Carrier l ) ; supposeA14: v in Carrier l ; ::_thesis: (f + g) . v = l . v A15: now__::_thesis:_v_in_D assume not v in D ; ::_thesis: contradiction then ( not v in Carrier l or v in A ) by XBOOLE_0:def_5; hence contradiction by A13, A14, XBOOLE_0:def_4; ::_thesis: verum end; thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10 .= 0 + (g . v) by A3, A13 .= l . v by A7, A15 ; ::_thesis: verum end; supposeA16: not v in Carrier l ; ::_thesis: (f + g) . v = l . v then A17: not v in D by XBOOLE_0:def_5; A18: not v in C by A16, XBOOLE_0:def_4; thus (f + g) . v = (f . v) + (g . v) by RLVECT_2:def_10 .= 0 + (g . v) by A3, A18 .= 0 + 0 by A7, A17 .= l . v by A16 ; ::_thesis: verum end; end; end; hence l . v = (f + g) . v ; ::_thesis: verum end; end; end; hence l . v = (f + g) . v ; ::_thesis: verum end; then A19: v = (Sum f) + (Sum g) by A1, RLVECT_3:1; ( Sum f in Lin A & Sum g in Lin B ) by Th1; hence v in (Lin A) + (Lin B) by A19, RUSUB_2:1; ::_thesis: verum end; then A20: Lin (A \/ B) is Subspace of (Lin A) + (Lin B) by RUSUB_1:23; ( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by Th7, XBOOLE_1:7; then (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by Lm5; hence Lin (A \/ B) = (Lin A) + (Lin B) by A20, RUSUB_1:20; ::_thesis: verum end; theorem :: RUSUB_3:10 for V being RealUnitarySpace for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) proof let V be RealUnitarySpace; ::_thesis: for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) let A, B be Subset of V; ::_thesis: Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) ( Lin (A /\ B) is Subspace of Lin A & Lin (A /\ B) is Subspace of Lin B ) by Th7, XBOOLE_1:17; hence Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) by Lm3; ::_thesis: verum end; theorem Th11: :: RUSUB_3:11 for V being RealUnitarySpace for A being Subset of V st A is linearly-independent holds ex B being Subset of V st ( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) proof let V be RealUnitarySpace; ::_thesis: for A being Subset of V st A is linearly-independent holds ex B being Subset of V st ( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) let A be Subset of V; ::_thesis: ( A is linearly-independent implies ex B being Subset of V st ( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) ) defpred S1[ set ] means ex B being Subset of V st ( B = $1 & A c= B & B is linearly-independent ); consider Q being set such that A1: for Z being set holds ( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) ) from XBOOLE_0:sch_1(); A2: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_Q_&_Z_is_c=-linear_holds_ union_Z_in_Q let Z be set ; ::_thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q ) assume that A3: Z <> {} and A4: Z c= Q and A5: Z is c=-linear ; ::_thesis: union Z in Q set x = the Element of Z; the Element of Z in Q by A3, A4, TARSKI:def_3; then A6: ex B being Subset of V st ( B = the Element of Z & A c= B & B is linearly-independent ) by A1; set W = union Z; union Z c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in the carrier of V ) assume x in union Z ; ::_thesis: x in the carrier of V then consider X being set such that A7: x in X and A8: X in Z by TARSKI:def_4; X in bool the carrier of V by A1, A4, A8; hence x in the carrier of V by A7; ::_thesis: verum end; then reconsider W = union Z as Subset of V ; A9: W is linearly-independent proof deffunc H1( set ) -> set = { C where C is Subset of V : ( $1 in C & C in Z ) } ; let l be Linear_Combination of W; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} ) assume that A10: Sum l = 0. V and A11: Carrier l <> {} ; ::_thesis: contradiction consider f being Function such that A12: dom f = Carrier l and A13: for x being set st x in Carrier l holds f . x = H1(x) from FUNCT_1:sch_3(); reconsider M = rng f as non empty set by A11, A12, RELAT_1:42; set F = the Choice_Function of M; set S = rng the Choice_Function of M; A14: now__::_thesis:_not_{}_in_M assume {} in M ; ::_thesis: contradiction then consider x being set such that A15: x in dom f and A16: f . x = {} by FUNCT_1:def_3; Carrier l c= W by RLVECT_2:def_6; then consider X being set such that A17: x in X and A18: X in Z by A12, A15, TARSKI:def_4; reconsider X = X as Subset of V by A1, A4, A18; X in { C where C is Subset of V : ( x in C & C in Z ) } by A17, A18; hence contradiction by A12, A13, A15, A16; ::_thesis: verum end; then A19: dom the Choice_Function of M = M by RLVECT_3:28; then dom the Choice_Function of M is finite by A12, FINSET_1:8; then A20: rng the Choice_Function of M is finite by FINSET_1:8; A21: now__::_thesis:_for_X_being_set_st_X_in_rng_the_Choice_Function_of_M_holds_ X_in_Z let X be set ; ::_thesis: ( X in rng the Choice_Function of M implies X in Z ) assume X in rng the Choice_Function of M ; ::_thesis: X in Z then consider x being set such that A22: x in dom the Choice_Function of M and A23: the Choice_Function of M . x = X by FUNCT_1:def_3; consider y being set such that A24: ( y in dom f & f . y = x ) by A19, A22, FUNCT_1:def_3; A25: x = { C where C is Subset of V : ( y in C & C in Z ) } by A12, A13, A24; X in x by A14, A19, A22, A23, ORDERS_1:def_1; then ex C being Subset of V st ( C = X & y in C & C in Z ) by A25; hence X in Z ; ::_thesis: verum end; A26: now__::_thesis:_for_X,_Y_being_set_st_X_in_rng_the_Choice_Function_of_M_&_Y_in_rng_the_Choice_Function_of_M_&_not_X_c=_Y_holds_ Y_c=_X let X, Y be set ; ::_thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X ) assume ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; ::_thesis: ( X c= Y or Y c= X ) then ( X in Z & Y in Z ) by A21; then X,Y are_c=-comparable by A5, ORDINAL1:def_8; hence ( X c= Y or Y c= X ) by XBOOLE_0:def_9; ::_thesis: verum end; rng the Choice_Function of M <> {} by A19, RELAT_1:42; then union (rng the Choice_Function of M) in rng the Choice_Function of M by A26, A20, CARD_2:62; then union (rng the Choice_Function of M) in Z by A21; then consider B being Subset of V such that A27: B = union (rng the Choice_Function of M) and A c= B and A28: B is linearly-independent by A1, A4; Carrier l c= union (rng the Choice_Function of M) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) ) set X = f . x; assume A29: x in Carrier l ; ::_thesis: x in union (rng the Choice_Function of M) then A30: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A13; A31: f . x in M by A12, A29, FUNCT_1:def_3; then the Choice_Function of M . (f . x) in f . x by A14, ORDERS_1:def_1; then A32: ex C being Subset of V st ( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A30; the Choice_Function of M . (f . x) in rng the Choice_Function of M by A19, A31, FUNCT_1:def_3; hence x in union (rng the Choice_Function of M) by A32, TARSKI:def_4; ::_thesis: verum end; then l is Linear_Combination of B by A27, RLVECT_2:def_6; hence contradiction by A10, A11, A28, RLVECT_3:def_1; ::_thesis: verum end; the Element of Z c= W by A3, ZFMISC_1:74; then A c= W by A6, XBOOLE_1:1; hence union Z in Q by A1, A9; ::_thesis: verum end; A33: (Omega). V = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3; assume A is linearly-independent ; ::_thesis: ex B being Subset of V st ( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) then Q <> {} by A1; then consider X being set such that A34: X in Q and A35: for Z being set st Z in Q & Z <> X holds not X c= Z by A2, ORDERS_1:67; consider B being Subset of V such that A36: B = X and A37: A c= B and A38: B is linearly-independent by A1, A34; take B ; ::_thesis: ( A c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) thus ( A c= B & B is linearly-independent ) by A37, A38; ::_thesis: Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) assume Lin B <> UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ; ::_thesis: contradiction then consider v being VECTOR of V such that A39: ( ( v in Lin B & not v in UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) or ( v in UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) & not v in Lin B ) ) by A33, RUSUB_1:25; A40: B \/ {v} is linearly-independent proof let l be Linear_Combination of B \/ {v}; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} ) assume A41: Sum l = 0. V ; ::_thesis: Carrier l = {} now__::_thesis:_Carrier_l_=_{} percases ( v in Carrier l or not v in Carrier l ) ; suppose v in Carrier l ; ::_thesis: Carrier l = {} then A42: - (l . v) <> 0 by RLVECT_2:19; deffunc H1( set ) -> Element of NAT = 0 ; deffunc H2( VECTOR of V) -> Element of REAL = l . $1; consider f being Function of the carrier of V,REAL such that A43: f . v = 0 and A44: for u being VECTOR of V st u <> v holds f . u = H2(u) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_ f_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0 ) assume not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0 then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5; then ( ( l . u = 0 & u <> v ) or u = v ) by TARSKI:def_1; hence f . u = 0 by A43, A44; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; Carrier f c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in B ) A45: Carrier l c= B \/ {v} by RLVECT_2:def_6; assume x in Carrier f ; ::_thesis: x in B then consider u being VECTOR of V such that A46: u = x and A47: f . u <> 0 ; f . u = l . u by A43, A44, A47; then u in Carrier l by A47; then ( u in B or u in {v} ) by A45, XBOOLE_0:def_3; hence x in B by A43, A46, A47, TARSKI:def_1; ::_thesis: verum end; then reconsider f = f as Linear_Combination of B by RLVECT_2:def_6; consider g being Function of the carrier of V,REAL such that A48: g . v = - (l . v) and A49: for u being VECTOR of V st u <> v holds g . u = H1(u) from FUNCT_2:sch_6(); reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_ g_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in {v} implies g . u = 0 ) assume not u in {v} ; ::_thesis: g . u = 0 then u <> v by TARSKI:def_1; hence g . u = 0 by A49; ::_thesis: verum end; then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3; Carrier g c= {v} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in {v} ) assume x in Carrier g ; ::_thesis: x in {v} then ex u being VECTOR of V st ( x = u & g . u <> 0 ) ; then x = v by A49; hence x in {v} by TARSKI:def_1; ::_thesis: verum end; then reconsider g = g as Linear_Combination of {v} by RLVECT_2:def_6; A50: Sum g = (- (l . v)) * v by A48, RLVECT_2:32; f - g = l proof let u be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (f - g) . u = l . u now__::_thesis:_(f_-_g)_._u_=_l_._u percases ( v = u or v <> u ) ; supposeA51: v = u ; ::_thesis: (f - g) . u = l . u thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54 .= l . u by A43, A48, A51 ; ::_thesis: verum end; supposeA52: v <> u ; ::_thesis: (f - g) . u = l . u thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54 .= (l . u) - (g . u) by A44, A52 .= (l . u) - 0 by A49, A52 .= l . u ; ::_thesis: verum end; end; end; hence (f - g) . u = l . u ; ::_thesis: verum end; then 0. V = (Sum f) - (Sum g) by A41, RLVECT_3:4; then Sum f = (0. V) + (Sum g) by RLSUB_2:61 .= (- (l . v)) * v by A50, RLVECT_1:4 ; then A53: (- (l . v)) * v in Lin B by Th1; ((- (l . v)) ") * ((- (l . v)) * v) = (((- (l . v)) ") * (- (l . v))) * v by RLVECT_1:def_7 .= 1 * v by A42, XCMPLX_0:def_7 .= v by RLVECT_1:def_8 ; hence Carrier l = {} by A39, A53, RLVECT_1:1, RUSUB_1:15; ::_thesis: verum end; supposeA54: not v in Carrier l ; ::_thesis: Carrier l = {} Carrier l c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in B ) assume A55: x in Carrier l ; ::_thesis: x in B Carrier l c= B \/ {v} by RLVECT_2:def_6; then ( x in B or x in {v} ) by A55, XBOOLE_0:def_3; hence x in B by A54, A55, TARSKI:def_1; ::_thesis: verum end; then l is Linear_Combination of B by RLVECT_2:def_6; hence Carrier l = {} by A38, A41, RLVECT_3:def_1; ::_thesis: verum end; end; end; hence Carrier l = {} ; ::_thesis: verum end; v in {v} by TARSKI:def_1; then A56: v in B \/ {v} by XBOOLE_0:def_3; A57: not v in B by A39, Th2, RLVECT_1:1; B c= B \/ {v} by XBOOLE_1:7; then A c= B \/ {v} by A37, XBOOLE_1:1; then B \/ {v} in Q by A1, A40; hence contradiction by A35, A36, A56, A57, XBOOLE_1:7; ::_thesis: verum end; theorem Th12: :: RUSUB_3:12 for V being RealUnitarySpace for A being Subset of V st Lin A = V holds ex B being Subset of V st ( B c= A & B is linearly-independent & Lin B = V ) proof let V be RealUnitarySpace; ::_thesis: for A being Subset of V st Lin A = V holds ex B being Subset of V st ( B c= A & B is linearly-independent & Lin B = V ) let A be Subset of V; ::_thesis: ( Lin A = V implies ex B being Subset of V st ( B c= A & B is linearly-independent & Lin B = V ) ) assume A1: Lin A = V ; ::_thesis: ex B being Subset of V st ( B c= A & B is linearly-independent & Lin B = V ) defpred S1[ set ] means ex B being Subset of V st ( B = $1 & B c= A & B is linearly-independent ); consider Q being set such that A2: for Z being set holds ( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) ) from XBOOLE_0:sch_1(); A3: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_Q_&_Z_is_c=-linear_holds_ union_Z_in_Q let Z be set ; ::_thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q ) assume that Z <> {} and A4: Z c= Q and A5: Z is c=-linear ; ::_thesis: union Z in Q set W = union Z; union Z c= the carrier of V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in the carrier of V ) assume x in union Z ; ::_thesis: x in the carrier of V then consider X being set such that A6: x in X and A7: X in Z by TARSKI:def_4; X in bool the carrier of V by A2, A4, A7; hence x in the carrier of V by A6; ::_thesis: verum end; then reconsider W = union Z as Subset of V ; A8: W is linearly-independent proof deffunc H1( set ) -> set = { C where C is Subset of V : ( $1 in C & C in Z ) } ; let l be Linear_Combination of W; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} ) assume that A9: Sum l = 0. V and A10: Carrier l <> {} ; ::_thesis: contradiction consider f being Function such that A11: dom f = Carrier l and A12: for x being set st x in Carrier l holds f . x = H1(x) from FUNCT_1:sch_3(); reconsider M = rng f as non empty set by A10, A11, RELAT_1:42; set F = the Choice_Function of M; set S = rng the Choice_Function of M; A13: now__::_thesis:_not_{}_in_M assume {} in M ; ::_thesis: contradiction then consider x being set such that A14: x in dom f and A15: f . x = {} by FUNCT_1:def_3; Carrier l c= W by RLVECT_2:def_6; then consider X being set such that A16: x in X and A17: X in Z by A11, A14, TARSKI:def_4; reconsider X = X as Subset of V by A2, A4, A17; X in { C where C is Subset of V : ( x in C & C in Z ) } by A16, A17; hence contradiction by A11, A12, A14, A15; ::_thesis: verum end; then A18: dom the Choice_Function of M = M by RLVECT_3:28; then dom the Choice_Function of M is finite by A11, FINSET_1:8; then A19: rng the Choice_Function of M is finite by FINSET_1:8; A20: now__::_thesis:_for_X_being_set_st_X_in_rng_the_Choice_Function_of_M_holds_ X_in_Z let X be set ; ::_thesis: ( X in rng the Choice_Function of M implies X in Z ) assume X in rng the Choice_Function of M ; ::_thesis: X in Z then consider x being set such that A21: x in dom the Choice_Function of M and A22: the Choice_Function of M . x = X by FUNCT_1:def_3; consider y being set such that A23: ( y in dom f & f . y = x ) by A18, A21, FUNCT_1:def_3; A24: x = { C where C is Subset of V : ( y in C & C in Z ) } by A11, A12, A23; X in x by A13, A18, A21, A22, ORDERS_1:def_1; then ex C being Subset of V st ( C = X & y in C & C in Z ) by A24; hence X in Z ; ::_thesis: verum end; A25: now__::_thesis:_for_X,_Y_being_set_st_X_in_rng_the_Choice_Function_of_M_&_Y_in_rng_the_Choice_Function_of_M_&_not_X_c=_Y_holds_ Y_c=_X let X, Y be set ; ::_thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X ) assume ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; ::_thesis: ( X c= Y or Y c= X ) then ( X in Z & Y in Z ) by A20; then X,Y are_c=-comparable by A5, ORDINAL1:def_8; hence ( X c= Y or Y c= X ) by XBOOLE_0:def_9; ::_thesis: verum end; rng the Choice_Function of M <> {} by A18, RELAT_1:42; then union (rng the Choice_Function of M) in rng the Choice_Function of M by A25, A19, CARD_2:62; then union (rng the Choice_Function of M) in Z by A20; then consider B being Subset of V such that A26: B = union (rng the Choice_Function of M) and B c= A and A27: B is linearly-independent by A2, A4; Carrier l c= union (rng the Choice_Function of M) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) ) set X = f . x; assume A28: x in Carrier l ; ::_thesis: x in union (rng the Choice_Function of M) then A29: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A12; A30: f . x in M by A11, A28, FUNCT_1:def_3; then the Choice_Function of M . (f . x) in f . x by A13, ORDERS_1:def_1; then A31: ex C being Subset of V st ( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A29; the Choice_Function of M . (f . x) in rng the Choice_Function of M by A18, A30, FUNCT_1:def_3; hence x in union (rng the Choice_Function of M) by A31, TARSKI:def_4; ::_thesis: verum end; then l is Linear_Combination of B by A26, RLVECT_2:def_6; hence contradiction by A9, A10, A27, RLVECT_3:def_1; ::_thesis: verum end; W c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W or x in A ) assume x in W ; ::_thesis: x in A then consider X being set such that A32: x in X and A33: X in Z by TARSKI:def_4; ex B being Subset of V st ( B = X & B c= A & B is linearly-independent ) by A2, A4, A33; hence x in A by A32; ::_thesis: verum end; hence union Z in Q by A2, A8; ::_thesis: verum end; ( {} the carrier of V c= A & {} the carrier of V is linearly-independent ) by RLVECT_3:7, XBOOLE_1:2; then Q <> {} by A2; then consider X being set such that A34: X in Q and A35: for Z being set st Z in Q & Z <> X holds not X c= Z by A3, ORDERS_1:67; consider B being Subset of V such that A36: B = X and A37: B c= A and A38: B is linearly-independent by A2, A34; take B ; ::_thesis: ( B c= A & B is linearly-independent & Lin B = V ) thus ( B c= A & B is linearly-independent ) by A37, A38; ::_thesis: Lin B = V assume A39: Lin B <> V ; ::_thesis: contradiction now__::_thesis:_ex_v_being_VECTOR_of_V_st_ (_v_in_A_&_not_v_in_Lin_B_) assume A40: for v being VECTOR of V st v in A holds v in Lin B ; ::_thesis: contradiction now__::_thesis:_for_v_being_VECTOR_of_V_st_v_in_Lin_A_holds_ v_in_Lin_B reconsider F = the carrier of (Lin B) as Subset of V by RUSUB_1:def_1; let v be VECTOR of V; ::_thesis: ( v in Lin A implies v in Lin B ) assume v in Lin A ; ::_thesis: v in Lin B then consider l being Linear_Combination of A such that A41: v = Sum l by Th1; Carrier l c= the carrier of (Lin B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in the carrier of (Lin B) ) assume A42: x in Carrier l ; ::_thesis: x in the carrier of (Lin B) then reconsider a = x as VECTOR of V ; Carrier l c= A by RLVECT_2:def_6; then a in Lin B by A40, A42; hence x in the carrier of (Lin B) by STRUCT_0:def_5; ::_thesis: verum end; then reconsider l = l as Linear_Combination of F by RLVECT_2:def_6; Sum l = v by A41; then v in Lin F by Th1; hence v in Lin B by Th5; ::_thesis: verum end; then Lin A is Subspace of Lin B by RUSUB_1:23; hence contradiction by A1, A39, RUSUB_1:20; ::_thesis: verum end; then consider v being VECTOR of V such that A43: v in A and A44: not v in Lin B ; A45: B \/ {v} is linearly-independent proof let l be Linear_Combination of B \/ {v}; :: according to RLVECT_3:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} ) assume A46: Sum l = 0. V ; ::_thesis: Carrier l = {} now__::_thesis:_Carrier_l_=_{} percases ( v in Carrier l or not v in Carrier l ) ; suppose v in Carrier l ; ::_thesis: Carrier l = {} then A47: - (l . v) <> 0 by RLVECT_2:19; deffunc H1( set ) -> Element of NAT = 0 ; deffunc H2( VECTOR of V) -> Element of REAL = l . $1; consider f being Function of the carrier of V,REAL such that A48: f . v = 0 and A49: for u being VECTOR of V st u <> v holds f . u = H2(u) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_ f_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0 ) assume not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0 then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5; then ( ( l . u = 0 & u <> v ) or u = v ) by TARSKI:def_1; hence f . u = 0 by A48, A49; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; Carrier f c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in B ) A50: Carrier l c= B \/ {v} by RLVECT_2:def_6; assume x in Carrier f ; ::_thesis: x in B then consider u being VECTOR of V such that A51: u = x and A52: f . u <> 0 ; f . u = l . u by A48, A49, A52; then u in Carrier l by A52; then ( u in B or u in {v} ) by A50, XBOOLE_0:def_3; hence x in B by A48, A51, A52, TARSKI:def_1; ::_thesis: verum end; then reconsider f = f as Linear_Combination of B by RLVECT_2:def_6; consider g being Function of the carrier of V,REAL such that A53: g . v = - (l . v) and A54: for u being VECTOR of V st u <> v holds g . u = H1(u) from FUNCT_2:sch_6(); reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_ g_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in {v} implies g . u = 0 ) assume not u in {v} ; ::_thesis: g . u = 0 then u <> v by TARSKI:def_1; hence g . u = 0 by A54; ::_thesis: verum end; then reconsider g = g as Linear_Combination of V by RLVECT_2:def_3; Carrier g c= {v} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in {v} ) assume x in Carrier g ; ::_thesis: x in {v} then ex u being VECTOR of V st ( x = u & g . u <> 0 ) ; then x = v by A54; hence x in {v} by TARSKI:def_1; ::_thesis: verum end; then reconsider g = g as Linear_Combination of {v} by RLVECT_2:def_6; A55: Sum g = (- (l . v)) * v by A53, RLVECT_2:32; f - g = l proof let u be VECTOR of V; :: according to RLVECT_2:def_9 ::_thesis: (f - g) . u = l . u now__::_thesis:_(f_-_g)_._u_=_l_._u percases ( v = u or v <> u ) ; supposeA56: v = u ; ::_thesis: (f - g) . u = l . u thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54 .= l . u by A48, A53, A56 ; ::_thesis: verum end; supposeA57: v <> u ; ::_thesis: (f - g) . u = l . u thus (f - g) . u = (f . u) - (g . u) by RLVECT_2:54 .= (l . u) - (g . u) by A49, A57 .= (l . u) - 0 by A54, A57 .= l . u ; ::_thesis: verum end; end; end; hence (f - g) . u = l . u ; ::_thesis: verum end; then 0. V = (Sum f) - (Sum g) by A46, RLVECT_3:4; then Sum f = (0. V) + (Sum g) by RLSUB_2:61 .= (- (l . v)) * v by A55, RLVECT_1:4 ; then A58: (- (l . v)) * v in Lin B by Th1; ((- (l . v)) ") * ((- (l . v)) * v) = (((- (l . v)) ") * (- (l . v))) * v by RLVECT_1:def_7 .= 1 * v by A47, XCMPLX_0:def_7 .= v by RLVECT_1:def_8 ; hence Carrier l = {} by A44, A58, RUSUB_1:15; ::_thesis: verum end; supposeA59: not v in Carrier l ; ::_thesis: Carrier l = {} Carrier l c= B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in B ) assume A60: x in Carrier l ; ::_thesis: x in B Carrier l c= B \/ {v} by RLVECT_2:def_6; then ( x in B or x in {v} ) by A60, XBOOLE_0:def_3; hence x in B by A59, A60, TARSKI:def_1; ::_thesis: verum end; then l is Linear_Combination of B by RLVECT_2:def_6; hence Carrier l = {} by A38, A46, RLVECT_3:def_1; ::_thesis: verum end; end; end; hence Carrier l = {} ; ::_thesis: verum end; {v} c= A by A43, ZFMISC_1:31; then B \/ {v} c= A by A37, XBOOLE_1:8; then A61: B \/ {v} in Q by A2, A45; v in {v} by TARSKI:def_1; then A62: v in B \/ {v} by XBOOLE_0:def_3; not v in B by A44, Th2; hence contradiction by A35, A36, A62, A61, XBOOLE_1:7; ::_thesis: verum end; begin definition let V be RealUnitarySpace; mode Basis of V -> Subset of V means :Def2: :: RUSUB_3:def 2 ( it is linearly-independent & Lin it = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ); existence ex b1 being Subset of V st ( b1 is linearly-independent & Lin b1 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) proof {} the carrier of V is linearly-independent by RLVECT_3:7; then ex B being Subset of V st ( {} the carrier of V c= B & B is linearly-independent & Lin B = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) by Th11; hence ex b1 being Subset of V st ( b1 is linearly-independent & Lin b1 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) ; ::_thesis: verum end; end; :: deftheorem Def2 defines Basis RUSUB_3:def_2_:_ for V being RealUnitarySpace for b2 being Subset of V holds ( b2 is Basis of V iff ( b2 is linearly-independent & Lin b2 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) ); theorem :: RUSUB_3:13 for V being strict RealUnitarySpace for A being Subset of V st A is linearly-independent holds ex I being Basis of V st A c= I proof let V be strict RealUnitarySpace; ::_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 = V ) by Th11; reconsider B = B as Basis of V by A2, Def2; take B ; ::_thesis: A c= B thus A c= B by A1; ::_thesis: verum end; theorem :: RUSUB_3:14 for V being RealUnitarySpace for A being Subset of V st Lin A = V holds ex I being Basis of V st I c= A proof let V be RealUnitarySpace; ::_thesis: for A being Subset of V st Lin A = V holds ex I being Basis of V st I c= A let A be Subset of V; ::_thesis: ( Lin A = V implies ex I being Basis of V st I c= A ) assume Lin A = V ; ::_thesis: ex I being Basis of V st I c= A then consider B being Subset of V such that A1: B c= A and A2: ( B is linearly-independent & Lin B = V ) by Th12; reconsider B = B as Basis of V by A2, Def2; take B ; ::_thesis: B c= A thus B c= A by A1; ::_thesis: verum end; theorem Th15: :: RUSUB_3:15 for V being RealUnitarySpace for A being Subset of V st A is linearly-independent holds ex I being Basis of V st A c= I proof let V be RealUnitarySpace; ::_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 = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) by Th11; reconsider B = B as Basis of V by A2, Def2; take B ; ::_thesis: A c= B thus A c= B by A1; ::_thesis: verum end; begin theorem Th16: :: RUSUB_3:16 for V being RealUnitarySpace for L being Linear_Combination of V for A being Subset of V for F being FinSequence of V st rng F c= the carrier of (Lin A) holds ex K being Linear_Combination of A st Sum (L (#) F) = Sum K proof let V be RealUnitarySpace; ::_thesis: for L being Linear_Combination of V for A being Subset of V for F being FinSequence of V st rng F c= the carrier of (Lin A) holds ex K being Linear_Combination of A st Sum (L (#) F) = Sum K let L be Linear_Combination of V; ::_thesis: for A being Subset of V for F being FinSequence of V st rng F c= the carrier of (Lin A) holds ex K being Linear_Combination of A st Sum (L (#) F) = Sum K let A be Subset of V; ::_thesis: for F being FinSequence of V st rng F c= the carrier of (Lin A) holds ex K being Linear_Combination of A st Sum (L (#) F) = Sum K defpred S1[ Element of NAT ] means for F being FinSequence 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; let F be FinSequence 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 A1: rng F c= the carrier of (Lin A) ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K A2: len F is Nat ; A3: 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 A4: S1[n] ; ::_thesis: S1[n + 1] let F be FinSequence 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 A5: rng F c= the carrier of (Lin A) and A6: 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 A7: F = G ^ <*x*> by A6, FINSEQ_2:18; reconsider G = G, x9 = <*x*> as FinSequence of V by A7, FINSEQ_1:36; A8: rng (G ^ <*x*>) = (rng G) \/ (rng <*x*>) by FINSEQ_1:31 .= (rng G) \/ {x} by FINSEQ_1:38 ; then A9: rng G c= rng F by A7, XBOOLE_1:7; {x} c= rng F by A7, A8, XBOOLE_1:7; then {x} c= the carrier of (Lin A) by A5, XBOOLE_1:1; then ( x in {x} implies x in the carrier of (Lin A) ) ; then A10: x in Lin A by STRUCT_0:def_5, TARSKI:def_1; then A11: x in V by RUSUB_1:2; consider LA1 being Linear_Combination of A such that A12: x = Sum LA1 by A10, Th1; reconsider x = x as VECTOR of V by A11, 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 A13: Sum (L (#) G) = Sum LA2 by A4, A5, A6, A7, A9, XBOOLE_1:1; (L . x) * LA1 is Linear_Combination of A by RLVECT_2:44; then A14: LA2 + ((L . x) * LA1) is Linear_Combination of A by RLVECT_2:38; Sum (L (#) F) = Sum ((L (#) G) ^ (L (#) x9)) by A7, RLVECT_3:34 .= (Sum LA2) + (Sum (L (#) x9)) by A13, RLVECT_1:41 .= (Sum LA2) + (Sum <*((L . x) * x)*>) by RLVECT_2:26 .= (Sum LA2) + ((L . x) * (Sum LA1)) by A12, 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 A14; ::_thesis: verum end; A15: S1[ 0 ] proof let F be FinSequence 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 A16: len F = 0 ; ::_thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K F = <*> the carrier of V by A16; then L (#) F = <*> the carrier of V by RLVECT_2:25; then A17: 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 A17; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A15, A3); hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A1, A2; ::_thesis: verum end; theorem :: RUSUB_3:17 for V being RealUnitarySpace for L being Linear_Combination of V for A being Subset of V st Carrier L c= the carrier of (Lin A) holds ex K being Linear_Combination of A st Sum L = Sum K proof let V be RealUnitarySpace; ::_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 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, Th16; take K ; ::_thesis: Sum L = Sum K thus Sum L = Sum K by A2, A3; ::_thesis: verum end; theorem Th18: :: RUSUB_3:18 for V being RealUnitarySpace for W being Subspace of V for L being Linear_Combination of V st Carrier L c= the carrier of W holds for K being Linear_Combination of W st K = L | the carrier of W holds ( Carrier L = Carrier K & Sum L = Sum K ) proof let V be RealUnitarySpace; ::_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 ; A6: w is VECTOR of V by RUSUB_1:3; L . w <> 0 by A2, A3, A5, FUNCT_1:47; hence x in Carrier L by A4, A6; ::_thesis: verum end; then A7: Carrier K c= Carrier L by TARSKI:def_3; consider G being FinSequence 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 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 ; K . v <> 0 by A1, A2, A3, A13, A14, A15, FUNCT_1:47; hence x in Carrier K by A1, A13, A14; ::_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 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 RUSUB_1:def_1; 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 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 RUSUB_1:6; ::_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; A33: i in NAT by ORDINAL1:def_12; assume A34: i in dom (L (#) F) ; ::_thesis: (L (#) F) . i = q . i then A35: F /. i = F . i by A31, A30, PARTFUN1:def_6; then F /. i in rng F by A31, A30, A34, 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 A36: P . i in dom G by A31, A34, FUNCT_1:def_3; then P . i in Seg (card G) by FINSEQ_1:def_3; then reconsider j = P . i as Element of NAT ; A37: G /. j = G . (P . i) by A36, PARTFUN1:def_6 .= F /. i by A18, A31, A30, A34, A35, FUNCT_1:12 ; q . i = (K (#) G) . j by A31, A21, A34, FUNCT_1:12 .= (K . w) * w by A32, A21, A36, A37, RLVECT_2:def_7 .= (L . (F /. i)) * w by A2, A3, FUNCT_1:47 .= (L . (F /. i)) * (F /. i) by RUSUB_1:7 ; hence (L (#) F) . i = q . i by A34, A33, RLVECT_2:def_7; ::_thesis: verum end; then A38: 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 A39: Sum (K (#) G) = Sum q by RLVECT_2:7; A40: f9 . (len q9) is Element of V ; f9 . 0 = 0. V by A24, RUSUB_1:4; hence ( Carrier L = Carrier K & Sum L = Sum K ) by A7, A16, A12, A9, A38, A39, A23, A26, A40, RLVECT_1:def_12, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th19: :: RUSUB_3:19 for V being RealUnitarySpace for W being Subspace of V for K being Linear_Combination of W ex L being Linear_Combination of V st ( Carrier K = Carrier L & Sum K = Sum L ) proof let V be RealUnitarySpace; ::_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 RUSUB_1:def_1; 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 ] ) ; 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 ( x in Carrier L & not x in the carrier of W ) ; ::_thesis: contradiction then ( ex v being VECTOR of V st ( x = v & L . v <> 0 ) & not x in W ) by STRUCT_0:def_5; hence contradiction by A4; ::_thesis: verum end; then A6: 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 A7: 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 A7, 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 A6, Th18; ::_thesis: verum end; theorem Th20: :: RUSUB_3:20 for V being RealUnitarySpace for W being Subspace of V for L being Linear_Combination of V st Carrier L c= the carrier of W holds ex K being Linear_Combination of W st ( Carrier K = Carrier L & Sum K = Sum L ) proof let V be RealUnitarySpace; ::_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 RUSUB_1:def_1; 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 RUSUB_1:3; assume not w in C ; ::_thesis: K . w = 0 then L . w = 0 by A4; 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, Th18; ::_thesis: verum end; theorem Th21: :: RUSUB_3:21 for V being RealUnitarySpace for I being Basis of V for v being VECTOR of V holds v in Lin I proof let V be RealUnitarySpace; ::_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 UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) by STRUCT_0:def_5; hence v in Lin I by Def2; ::_thesis: verum end; theorem Th22: :: RUSUB_3:22 for V being RealUnitarySpace for W being Subspace of V for A being Subset of W st A is linearly-independent holds A is linearly-independent Subset of V proof let V be RealUnitarySpace; ::_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 RUSUB_1:def_1; 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 Th20, XBOOLE_1:1; reconsider LW = LW as Linear_Combination of A by A4, RLVECT_2:def_6; Sum LW = 0. W by A2, A5, RUSUB_1:4; 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 :: RUSUB_3:23 for V being RealUnitarySpace for W being Subspace of V for A being Subset of V st A is linearly-independent & A c= the carrier of W holds A is linearly-independent Subset of W proof let V be RealUnitarySpace; ::_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 Th19; reconsider L = L as Linear_Combination of A by A5, RLVECT_2:def_6; Sum L = 0. V by A3, A6, RUSUB_1:4; 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 :: RUSUB_3:24 for V being RealUnitarySpace for W being Subspace of V for A being Basis of W ex B being Basis of V st A c= B proof let V be RealUnitarySpace; ::_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 Def2; then reconsider B = A as linearly-independent Subset of V by Th22; consider I being Basis of V such that A1: B c= I by Th15; take I ; ::_thesis: A c= I thus A c= I by A1; ::_thesis: verum end; theorem Th25: :: RUSUB_3:25 for V being RealUnitarySpace for A being Subset of V st A is linearly-independent holds for v being VECTOR of V st v in A holds for B being Subset of V st B = A \ {v} holds not v in Lin B proof let V be RealUnitarySpace; ::_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; let B be Subset of V; ::_thesis: ( B = A \ {v} implies not v in Lin B ) assume A3: B = A \ {v} ; ::_thesis: not v in Lin B B c= A by A3, XBOOLE_1:36; then A4: 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 A5: v = Sum L by Th1; {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 A5, RLVECT_2:34; then A6: ex w being set st w in Carrier L by XBOOLE_0:def_1; v in {v} by TARSKI:def_1; then v in Lin {v} by Th2; then consider K being Linear_Combination of {v} such that A7: v = Sum K by Th1; A8: ( 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 A4, RLVECT_2:55, XBOOLE_1:1; then Carrier (L - K) c= A by XBOOLE_1:1; then A9: L - K is Linear_Combination of A by RLVECT_2:def_6; A10: 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 A3, A8, XBOOLE_0:def_5; hence K . x = 0 ; ::_thesis: verum end; 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 A10, A11 .= L . x ; hence contradiction by A12, A13; ::_thesis: verum end; then A14: Carrier L c= Carrier (L - K) by TARSKI:def_3; 0. V = (Sum L) + (- (Sum K)) by A5, A7, RLVECT_1:5 .= (Sum L) + (Sum (- K)) by RLVECT_3:3 .= Sum (L - K) by RLVECT_3:1 ; hence contradiction by A1, A6, A9, A14, RLVECT_3:def_1; ::_thesis: verum end; Lm6: for X, x being set st not x in X holds X \ {x} = X proof let X, x be set ; ::_thesis: ( not x in X implies X \ {x} = X ) assume A1: not x in X ; ::_thesis: X \ {x} = X now__::_thesis:_not_X_meets_{x} assume X meets {x} ; ::_thesis: contradiction then consider y being set such that A2: y in X /\ {x} by XBOOLE_0:4; ( y in X & y in {x} ) by A2, XBOOLE_0:def_4; hence contradiction by A1, TARSKI:def_1; ::_thesis: verum end; hence X \ {x} = X by XBOOLE_1:83; ::_thesis: verum end; theorem :: RUSUB_3:26 for V being RealUnitarySpace for I being Basis of V for A being non empty Subset of V st A misses I holds for B being Subset of V st B = I \/ A holds B is linearly-dependent proof let V be RealUnitarySpace; ::_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, Lm6; then A6: Lin I is Subspace of Lin Bv by Th7; assume A7: B is linearly-independent ; ::_thesis: contradiction v in Lin I by Th21; hence contradiction by A7, A2, A4, A6, Th25, RUSUB_1:1; ::_thesis: verum end; theorem :: RUSUB_3:27 for V being RealUnitarySpace for W being Subspace of V for A being Subset of V st A c= the carrier of W holds Lin A is Subspace of W proof let V be RealUnitarySpace; ::_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 Th1; 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, Th20, 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 RUSUB_1:22; ::_thesis: verum end; theorem :: RUSUB_3:28 for V being RealUnitarySpace for W being Subspace of V for A being Subset of V for B being Subset of W st A = B holds Lin A = Lin B proof let V be RealUnitarySpace; ::_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 RealUnitarySpace ; A1: B9 is Subspace of V9 by RUSUB_1:21; 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 Th1; 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, Th20, 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 Th1; 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 Th1; consider L being Linear_Combination of V such that A8: Carrier L = Carrier K and A9: Sum L = Sum K by Th19; 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 Th1; 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, RUSUB_1:24; ::_thesis: verum end; begin theorem Th29: :: RUSUB_3:29 for V being RealUnitarySpace for v being VECTOR of V for x being set holds ( x in Lin {v} iff ex a being Real st x = a * v ) proof deffunc H1( set ) -> Element of NAT = 0 ; let V be RealUnitarySpace; ::_thesis: for v being VECTOR of V for x being set holds ( x in Lin {v} iff ex a being Real st x = a * v ) let v be VECTOR of V; ::_thesis: for x being set holds ( x in Lin {v} iff ex a being Real st x = a * v ) let x be set ; ::_thesis: ( x in Lin {v} iff ex a being Real st x = a * v ) thus ( x in Lin {v} implies ex a being Real st x = a * v ) ::_thesis: ( ex a being Real st x = a * v implies x in Lin {v} ) proof assume x in Lin {v} ; ::_thesis: ex a being Real st x = a * v then consider l being Linear_Combination of {v} such that A1: x = Sum l by Th1; Sum l = (l . v) * v by RLVECT_2:32; hence ex a being Real st x = a * v by A1; ::_thesis: verum end; given a being Real such that A2: x = a * v ; ::_thesis: x in Lin {v} consider f being Function of the carrier of V,REAL such that A3: f . v = a and A4: for z being VECTOR of V st z <> v holds f . z = H1(z) from FUNCT_2:sch_6(); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_z_being_VECTOR_of_V_st_not_z_in_{v}_holds_ f_._z_=_0 let z be VECTOR of V; ::_thesis: ( not z in {v} implies f . z = 0 ) assume not z in {v} ; ::_thesis: f . z = 0 then z <> v by TARSKI:def_1; hence f . z = 0 by A4; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; Carrier f c= {v} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} ) assume A5: x in Carrier f ; ::_thesis: x in {v} then f . x <> 0 by RLVECT_2:19; then x = v by A4, A5; hence x in {v} by TARSKI:def_1; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def_6; Sum f = x by A2, A3, RLVECT_2:32; hence x in Lin {v} by Th1; ::_thesis: verum end; theorem :: RUSUB_3:30 for V being RealUnitarySpace for v being VECTOR of V holds v in Lin {v} proof let V be RealUnitarySpace; ::_thesis: for v being VECTOR of V holds v in Lin {v} let v be VECTOR of V; ::_thesis: v in Lin {v} v in {v} by TARSKI:def_1; hence v in Lin {v} by Th2; ::_thesis: verum end; theorem :: RUSUB_3:31 for V being RealUnitarySpace for v, w being VECTOR of V for x being set holds ( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) ) proof let V be RealUnitarySpace; ::_thesis: for v, w being VECTOR of V for x being set holds ( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) ) let v, w be VECTOR of V; ::_thesis: for x being set holds ( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) ) let x be set ; ::_thesis: ( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) ) thus ( x in v + (Lin {w}) implies ex a being Real st x = v + (a * w) ) ::_thesis: ( ex a being Real st x = v + (a * w) implies x in v + (Lin {w}) ) proof assume x in v + (Lin {w}) ; ::_thesis: ex a being Real st x = v + (a * w) then consider u being VECTOR of V such that A1: u in Lin {w} and A2: x = v + u by RUSUB_2:63; ex a being Real st u = a * w by A1, Th29; hence ex a being Real st x = v + (a * w) by A2; ::_thesis: verum end; given a being Real such that A3: x = v + (a * w) ; ::_thesis: x in v + (Lin {w}) a * w in Lin {w} by Th29; hence x in v + (Lin {w}) by A3, RUSUB_2:63; ::_thesis: verum end; theorem Th32: :: RUSUB_3:32 for V being RealUnitarySpace for w1, w2 being VECTOR of V for x being set holds ( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) ) proof let V be RealUnitarySpace; ::_thesis: for w1, w2 being VECTOR of V for x being set holds ( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) ) let w1, w2 be VECTOR of V; ::_thesis: for x being set holds ( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) ) let x be set ; ::_thesis: ( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) ) thus ( x in Lin {w1,w2} implies ex a, b being Real st x = (a * w1) + (b * w2) ) ::_thesis: ( ex a, b being Real st x = (a * w1) + (b * w2) implies x in Lin {w1,w2} ) proof assume A1: x in Lin {w1,w2} ; ::_thesis: ex a, b being Real st x = (a * w1) + (b * w2) now__::_thesis:_ex_a,_b_being_Real_st_x_=_(a_*_w1)_+_(b_*_w2) percases ( w1 = w2 or w1 <> w2 ) ; suppose w1 = w2 ; ::_thesis: ex a, b being Real st x = (a * w1) + (b * w2) then {w1,w2} = {w1} by ENUMSET1:29; then consider a being Real such that A2: x = a * w1 by A1, Th29; x = (a * w1) + (0. V) by A2, RLVECT_1:4 .= (a * w1) + (0 * w2) by RLVECT_1:10 ; hence ex a, b being Real st x = (a * w1) + (b * w2) ; ::_thesis: verum end; supposeA3: w1 <> w2 ; ::_thesis: ex a, b being Real st x = (a * w1) + (b * w2) consider l being Linear_Combination of {w1,w2} such that A4: x = Sum l by A1, Th1; x = ((l . w1) * w1) + ((l . w2) * w2) by A3, A4, RLVECT_2:33; hence ex a, b being Real st x = (a * w1) + (b * w2) ; ::_thesis: verum end; end; end; hence ex a, b being Real st x = (a * w1) + (b * w2) ; ::_thesis: verum end; given a, b being Real such that A5: x = (a * w1) + (b * w2) ; ::_thesis: x in Lin {w1,w2} now__::_thesis:_x_in_Lin_{w1,w2} percases ( w1 = w2 or w1 <> w2 ) ; supposeA6: w1 = w2 ; ::_thesis: x in Lin {w1,w2} then x = (a + b) * w1 by A5, RLVECT_1:def_6; then x in Lin {w1} by Th29; hence x in Lin {w1,w2} by A6, ENUMSET1:29; ::_thesis: verum end; supposeA7: w1 <> w2 ; ::_thesis: x in Lin {w1,w2} deffunc H1( set ) -> Element of NAT = 0 ; consider f being Function of the carrier of V,REAL such that A8: ( f . w1 = a & f . w2 = b ) and A9: for u being VECTOR of V st u <> w1 & u <> w2 holds f . u = H1(u) from FUNCT_2:sch_7(A7); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{w1,w2}_holds_ f_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in {w1,w2} implies f . u = 0 ) assume not u in {w1,w2} ; ::_thesis: f . u = 0 then ( u <> w1 & u <> w2 ) by TARSKI:def_2; hence f . u = 0 by A9; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; Carrier f c= {w1,w2} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {w1,w2} ) assume that A10: x in Carrier f and A11: not x in {w1,w2} ; ::_thesis: contradiction ( x <> w1 & x <> w2 ) by A11, TARSKI:def_2; then f . x = 0 by A9, A10; hence contradiction by A10, RLVECT_2:19; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {w1,w2} by RLVECT_2:def_6; x = Sum f by A5, A7, A8, RLVECT_2:33; hence x in Lin {w1,w2} by Th1; ::_thesis: verum end; end; end; hence x in Lin {w1,w2} ; ::_thesis: verum end; theorem :: RUSUB_3:33 for V being RealUnitarySpace for w1, w2 being VECTOR of V holds ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} ) proof let V be RealUnitarySpace; ::_thesis: for w1, w2 being VECTOR of V holds ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} ) let w1, w2 be VECTOR of V; ::_thesis: ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} ) ( w1 in {w1,w2} & w2 in {w1,w2} ) by TARSKI:def_2; hence ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} ) by Th2; ::_thesis: verum end; theorem :: RUSUB_3:34 for V being RealUnitarySpace for v, w1, w2 being VECTOR of V for x being set holds ( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) ) proof let V be RealUnitarySpace; ::_thesis: for v, w1, w2 being VECTOR of V for x being set holds ( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) ) let v, w1, w2 be VECTOR of V; ::_thesis: for x being set holds ( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) ) let x be set ; ::_thesis: ( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) ) thus ( x in v + (Lin {w1,w2}) implies ex a, b being Real st x = (v + (a * w1)) + (b * w2) ) ::_thesis: ( ex a, b being Real st x = (v + (a * w1)) + (b * w2) implies x in v + (Lin {w1,w2}) ) proof assume x in v + (Lin {w1,w2}) ; ::_thesis: ex a, b being Real st x = (v + (a * w1)) + (b * w2) then consider u being VECTOR of V such that A1: u in Lin {w1,w2} and A2: x = v + u by RUSUB_2:63; consider a, b being Real such that A3: u = (a * w1) + (b * w2) by A1, Th32; take a ; ::_thesis: ex b being Real st x = (v + (a * w1)) + (b * w2) take b ; ::_thesis: x = (v + (a * w1)) + (b * w2) thus x = (v + (a * w1)) + (b * w2) by A2, A3, RLVECT_1:def_3; ::_thesis: verum end; given a, b being Real such that A4: x = (v + (a * w1)) + (b * w2) ; ::_thesis: x in v + (Lin {w1,w2}) (a * w1) + (b * w2) in Lin {w1,w2} by Th32; then v + ((a * w1) + (b * w2)) in v + (Lin {w1,w2}) by RUSUB_2:63; hence x in v + (Lin {w1,w2}) by A4, RLVECT_1:def_3; ::_thesis: verum end; theorem Th35: :: RUSUB_3:35 for V being RealUnitarySpace for v1, v2, v3 being VECTOR of V for x being set holds ( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ) proof let V be RealUnitarySpace; ::_thesis: for v1, v2, v3 being VECTOR of V for x being set holds ( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ) let v1, v2, v3 be VECTOR of V; ::_thesis: for x being set holds ( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ) let x be set ; ::_thesis: ( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ) thus ( x in Lin {v1,v2,v3} implies ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ) ::_thesis: ( ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) implies x in Lin {v1,v2,v3} ) proof assume A1: x in Lin {v1,v2,v3} ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) now__::_thesis:_ex_a,_b,_c_being_Real_st_x_=_((a_*_v1)_+_(b_*_v2))_+_(c_*_v3) percases ( ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) or v1 = v2 or v1 = v3 or v2 = v3 ) ; supposeA2: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) consider l being Linear_Combination of {v1,v2,v3} such that A3: x = Sum l by A1, Th1; x = (((l . v1) * v1) + ((l . v2) * v2)) + ((l . v3) * v3) by A2, A3, RLVECT_4:6; hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum end; suppose ( v1 = v2 or v1 = v3 or v2 = v3 ) ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) then A4: ( {v1,v2,v3} = {v1,v3} or {v1,v2,v3} = {v1,v1,v2} or {v1,v2,v3} = {v3,v3,v1} ) by ENUMSET1:30, ENUMSET1:59; now__::_thesis:_ex_a,_b,_c_being_Real_st_x_=_((a_*_v1)_+_(b_*_v2))_+_(c_*_v3) percases ( {v1,v2,v3} = {v1,v2} or {v1,v2,v3} = {v1,v3} ) by A4, ENUMSET1:30; suppose {v1,v2,v3} = {v1,v2} ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) then consider a, b being Real such that A5: x = (a * v1) + (b * v2) by A1, Th32; x = ((a * v1) + (b * v2)) + (0. V) by A5, RLVECT_1:4 .= ((a * v1) + (b * v2)) + (0 * v3) by RLVECT_1:10 ; hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum end; suppose {v1,v2,v3} = {v1,v3} ; ::_thesis: ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) then consider a, b being Real such that A6: x = (a * v1) + (b * v3) by A1, Th32; x = ((a * v1) + (0. V)) + (b * v3) by A6, RLVECT_1:4 .= ((a * v1) + (0 * v2)) + (b * v3) by RLVECT_1:10 ; hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum end; end; end; hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum end; end; end; hence ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: verum end; given a, b, c being Real such that A7: x = ((a * v1) + (b * v2)) + (c * v3) ; ::_thesis: x in Lin {v1,v2,v3} now__::_thesis:_x_in_Lin_{v1,v2,v3} percases ( v1 = v2 or v1 = v3 or v2 = v3 or ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ) ; supposeA8: ( v1 = v2 or v1 = v3 or v2 = v3 ) ; ::_thesis: x in Lin {v1,v2,v3} now__::_thesis:_x_in_Lin_{v1,v2,v3} percases ( v1 = v2 or v1 = v3 or v2 = v3 ) by A8; suppose v1 = v2 ; ::_thesis: x in Lin {v1,v2,v3} then ( {v1,v2,v3} = {v1,v3} & x = ((a + b) * v1) + (c * v3) ) by A7, ENUMSET1:30, RLVECT_1:def_6; hence x in Lin {v1,v2,v3} by Th32; ::_thesis: verum end; supposeA9: v1 = v3 ; ::_thesis: x in Lin {v1,v2,v3} then A10: {v1,v2,v3} = {v1,v1,v2} by ENUMSET1:57 .= {v2,v1} by ENUMSET1:30 ; x = (b * v2) + ((a * v1) + (c * v1)) by A7, A9, RLVECT_1:def_3 .= (b * v2) + ((a + c) * v1) by RLVECT_1:def_6 ; hence x in Lin {v1,v2,v3} by A10, Th32; ::_thesis: verum end; supposeA11: v2 = v3 ; ::_thesis: x in Lin {v1,v2,v3} then A12: {v1,v2,v3} = {v2,v2,v1} by ENUMSET1:59 .= {v1,v2} by ENUMSET1:30 ; x = (a * v1) + ((b * v2) + (c * v2)) by A7, A11, RLVECT_1:def_3 .= (a * v1) + ((b + c) * v2) by RLVECT_1:def_6 ; hence x in Lin {v1,v2,v3} by A12, Th32; ::_thesis: verum end; end; end; hence x in Lin {v1,v2,v3} ; ::_thesis: verum end; supposeA13: ( v1 <> v2 & v1 <> v3 & v2 <> v3 ) ; ::_thesis: x in Lin {v1,v2,v3} deffunc H1( set ) -> Element of NAT = 0 ; A14: v1 <> v3 by A13; A15: v2 <> v3 by A13; A16: v1 <> v2 by A13; consider f being Function of the carrier of V,REAL such that A17: ( f . v1 = a & f . v2 = b & f . v3 = c ) and A18: for v being VECTOR of V st v <> v1 & v <> v2 & v <> v3 holds f . v = H1(v) from RLVECT_4:sch_1(A16, A14, A15); reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8; now__::_thesis:_for_v_being_VECTOR_of_V_st_not_v_in_{v1,v2,v3}_holds_ f_._v_=_0 let v be VECTOR of V; ::_thesis: ( not v in {v1,v2,v3} implies f . v = 0 ) assume A19: not v in {v1,v2,v3} ; ::_thesis: f . v = 0 then A20: v <> v3 by ENUMSET1:def_1; ( v <> v1 & v <> v2 ) by A19, ENUMSET1:def_1; hence f . v = 0 by A18, A20; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; Carrier f c= {v1,v2,v3} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2,v3} ) assume that A21: x in Carrier f and A22: not x in {v1,v2,v3} ; ::_thesis: contradiction A23: x <> v3 by A22, ENUMSET1:def_1; ( x <> v1 & x <> v2 ) by A22, ENUMSET1:def_1; then f . x = 0 by A18, A21, A23; hence contradiction by A21, RLVECT_2:19; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def_6; x = Sum f by A7, A13, A17, RLVECT_4:6; hence x in Lin {v1,v2,v3} by Th1; ::_thesis: verum end; end; end; hence x in Lin {v1,v2,v3} ; ::_thesis: verum end; theorem :: RUSUB_3:36 for V being RealUnitarySpace for w1, w2, w3 being VECTOR of V holds ( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} ) proof let V be RealUnitarySpace; ::_thesis: for w1, w2, w3 being VECTOR of V holds ( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} ) let w1, w2, w3 be VECTOR of V; ::_thesis: ( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} ) A1: w3 in {w1,w2,w3} by ENUMSET1:def_1; ( w1 in {w1,w2,w3} & w2 in {w1,w2,w3} ) by ENUMSET1:def_1; hence ( w1 in Lin {w1,w2,w3} & w2 in Lin {w1,w2,w3} & w3 in Lin {w1,w2,w3} ) by A1, Th2; ::_thesis: verum end; theorem :: RUSUB_3:37 for V being RealUnitarySpace for v, w1, w2, w3 being VECTOR of V for x being set holds ( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) proof let V be RealUnitarySpace; ::_thesis: for v, w1, w2, w3 being VECTOR of V for x being set holds ( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) let v, w1, w2, w3 be VECTOR of V; ::_thesis: for x being set holds ( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) let x be set ; ::_thesis: ( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) thus ( x in v + (Lin {w1,w2,w3}) implies ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) ::_thesis: ( ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) implies x in v + (Lin {w1,w2,w3}) ) proof assume x in v + (Lin {w1,w2,w3}) ; ::_thesis: ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) then consider u being VECTOR of V such that A1: u in Lin {w1,w2,w3} and A2: x = v + u by RUSUB_2:63; consider a, b, c being Real such that A3: u = ((a * w1) + (b * w2)) + (c * w3) by A1, Th35; take a ; ::_thesis: ex b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) take b ; ::_thesis: ex c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) take c ; ::_thesis: x = ((v + (a * w1)) + (b * w2)) + (c * w3) x = (v + ((a * w1) + (b * w2))) + (c * w3) by A2, A3, RLVECT_1:def_3; hence x = ((v + (a * w1)) + (b * w2)) + (c * w3) by RLVECT_1:def_3; ::_thesis: verum end; given a, b, c being Real such that A4: x = ((v + (a * w1)) + (b * w2)) + (c * w3) ; ::_thesis: x in v + (Lin {w1,w2,w3}) ((a * w1) + (b * w2)) + (c * w3) in Lin {w1,w2,w3} by Th35; then v + (((a * w1) + (b * w2)) + (c * w3)) in v + (Lin {w1,w2,w3}) by RUSUB_2:63; then (v + ((a * w1) + (b * w2))) + (c * w3) in v + (Lin {w1,w2,w3}) by RLVECT_1:def_3; hence x in v + (Lin {w1,w2,w3}) by A4, RLVECT_1:def_3; ::_thesis: verum end; theorem :: RUSUB_3:38 for V being RealUnitarySpace for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds Lin {v} = Lin {w} proof let V be RealUnitarySpace; ::_thesis: for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds Lin {v} = Lin {w} let v, w be VECTOR of V; ::_thesis: ( v in Lin {w} & v <> 0. V implies Lin {v} = Lin {w} ) assume that A1: v in Lin {w} and A2: v <> 0. V ; ::_thesis: Lin {v} = Lin {w} consider a being Real such that A3: v = a * w by A1, Th29; now__::_thesis:_for_u_being_VECTOR_of_V_holds_ (_(_u_in_Lin_{v}_implies_u_in_Lin_{w}_)_&_(_u_in_Lin_{w}_implies_u_in_Lin_{v}_)_) let u be VECTOR of V; ::_thesis: ( ( u in Lin {v} implies u in Lin {w} ) & ( u in Lin {w} implies u in Lin {v} ) ) A4: a <> 0 by A2, A3, RLVECT_1:10; thus ( u in Lin {v} implies u in Lin {w} ) ::_thesis: ( u in Lin {w} implies u in Lin {v} ) proof assume u in Lin {v} ; ::_thesis: u in Lin {w} then consider b being Real such that A5: u = b * v by Th29; u = (b * a) * w by A3, A5, RLVECT_1:def_7; hence u in Lin {w} by Th29; ::_thesis: verum end; assume u in Lin {w} ; ::_thesis: u in Lin {v} then consider b being Real such that A6: u = b * w by Th29; (a ") * v = ((a ") * a) * w by A3, RLVECT_1:def_7 .= 1 * w by A4, XCMPLX_0:def_7 .= w by RLVECT_1:def_8 ; then u = (b * (a ")) * v by A6, RLVECT_1:def_7; hence u in Lin {v} by Th29; ::_thesis: verum end; hence Lin {v} = Lin {w} by RUSUB_1:25; ::_thesis: verum end; theorem :: RUSUB_3:39 for V being RealUnitarySpace for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 ) proof let V be RealUnitarySpace; ::_thesis: for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 ) let v1, v2, w1, w2 be VECTOR of V; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} implies ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 ) ) assume that A1: v1 <> v2 and A2: {v1,v2} is linearly-independent and A3: v1 in Lin {w1,w2} and A4: v2 in Lin {w1,w2} ; ::_thesis: ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 ) consider r1, r2 being Real such that A5: v1 = (r1 * w1) + (r2 * w2) by A3, Th32; consider r3, r4 being Real such that A6: v2 = (r3 * w1) + (r4 * w2) by A4, Th32; set t = (r1 * r4) - (r2 * r3); A7: now__::_thesis:_(_r1_=_0_implies_not_r2_=_0_) assume ( r1 = 0 & r2 = 0 ) ; ::_thesis: contradiction then v1 = (0. V) + (0 * w2) by A5, RLVECT_1:10 .= (0. V) + (0. V) by RLVECT_1:10 .= 0. V by RLVECT_1:4 ; hence contradiction by A2, RLVECT_3:11; ::_thesis: verum end; now__::_thesis:_not_r1_*_r4_=_r2_*_r3 assume A8: r1 * r4 = r2 * r3 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( r1 <> 0 or r2 <> 0 ) by A7; supposeA9: r1 <> 0 ; ::_thesis: contradiction ((r1 ") * r1) * r4 = (r1 ") * (r2 * r3) by A8, XCMPLX_1:4; then 1 * r4 = (r1 ") * (r2 * r3) by A9, XCMPLX_0:def_7; then v2 = (r3 * w1) + ((r3 * ((r1 ") * r2)) * w2) by A6 .= (r3 * w1) + (r3 * (((r1 ") * r2) * w2)) by RLVECT_1:def_7 .= (r3 * 1) * (w1 + (((r1 ") * r2) * w2)) by RLVECT_1:def_5 .= (r3 * ((r1 ") * r1)) * (w1 + (((r1 ") * r2) * w2)) by A9, XCMPLX_0:def_7 .= ((r3 * (r1 ")) * r1) * (w1 + (((r1 ") * r2) * w2)) .= (r3 * (r1 ")) * (r1 * (w1 + (((r1 ") * r2) * w2))) by RLVECT_1:def_7 .= (r3 * (r1 ")) * ((r1 * w1) + (r1 * (((r1 ") * r2) * w2))) by RLVECT_1:def_5 .= (r3 * (r1 ")) * ((r1 * w1) + ((r1 * ((r1 ") * r2)) * w2)) by RLVECT_1:def_7 .= (r3 * (r1 ")) * ((r1 * w1) + (((r1 * (r1 ")) * r2) * w2)) .= (r3 * (r1 ")) * ((r1 * w1) + ((1 * r2) * w2)) by A9, XCMPLX_0:def_7 .= (r3 * (r1 ")) * ((r1 * w1) + (r2 * w2)) ; hence contradiction by A1, A2, A5, RLVECT_3:12; ::_thesis: verum end; supposeA10: r2 <> 0 ; ::_thesis: contradiction (r2 ") * (r1 * r4) = (r2 ") * (r2 * r3) by A8 .= ((r2 ") * r2) * r3 .= 1 * r3 by A10, XCMPLX_0:def_7 .= r3 ; then v2 = ((r4 * ((r2 ") * r1)) * w1) + (r4 * w2) by A6 .= (r4 * (((r2 ") * r1) * w1)) + (r4 * w2) by RLVECT_1:def_7 .= (r4 * 1) * ((((r2 ") * r1) * w1) + w2) by RLVECT_1:def_5 .= (r4 * ((r2 ") * r2)) * ((((r2 ") * r1) * w1) + w2) by A10, XCMPLX_0:def_7 .= ((r4 * (r2 ")) * r2) * ((((r2 ") * r1) * w1) + w2) .= (r4 * (r2 ")) * (r2 * ((((r2 ") * r1) * w1) + w2)) by RLVECT_1:def_7 .= (r4 * (r2 ")) * ((r2 * (((r2 ") * r1) * w1)) + (r2 * w2)) by RLVECT_1:def_5 .= (r4 * (r2 ")) * (((r2 * ((r2 ") * r1)) * w1) + (r2 * w2)) by RLVECT_1:def_7 .= (r4 * (r2 ")) * ((((r2 * (r2 ")) * r1) * w1) + (r2 * w2)) .= (r4 * (r2 ")) * (((1 * r1) * w1) + (r2 * w2)) by A10, XCMPLX_0:def_7 .= (r4 * (r2 ")) * ((r1 * w1) + (r2 * w2)) ; hence contradiction by A1, A2, A5, RLVECT_3:12; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; then A11: (r1 * r4) - (r2 * r3) <> 0 ; A12: now__::_thesis:_(_r2_<>_0_implies_(_w1_=_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r4)_*_v1)_+_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r2)_*_v2))_&_w2_=_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r3)_*_v1))_+_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r1)_*_v2)_)_) assume A13: r2 <> 0 ; ::_thesis: ( w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) & w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) ) (r2 ") * v1 = ((r2 ") * (r1 * w1)) + ((r2 ") * (r2 * w2)) by A5, RLVECT_1:def_5 .= (((r2 ") * r1) * w1) + ((r2 ") * (r2 * w2)) by RLVECT_1:def_7 .= (((r2 ") * r1) * w1) + (((r2 ") * r2) * w2) by RLVECT_1:def_7 .= (((r2 ") * r1) * w1) + (1 * w2) by A13, XCMPLX_0:def_7 .= (((r2 ") * r1) * w1) + w2 by RLVECT_1:def_8 ; then A14: w2 = ((r2 ") * v1) - (((r2 ") * r1) * w1) by RLSUB_2:61; then w2 = ((r2 ") * v1) - ((r2 ") * (r1 * w1)) by RLVECT_1:def_7; then v2 = (r3 * w1) + (r4 * ((r2 ") * (v1 - (r1 * w1)))) by A6, RLVECT_1:34 .= (r3 * w1) + ((r4 * (r2 ")) * (v1 - (r1 * w1))) by RLVECT_1:def_7 .= (r3 * w1) + (((r4 * (r2 ")) * v1) - ((r4 * (r2 ")) * (r1 * w1))) by RLVECT_1:34 .= ((r3 * w1) + ((r4 * (r2 ")) * v1)) - ((r4 * (r2 ")) * (r1 * w1)) by RLVECT_1:def_3 .= (((r4 * (r2 ")) * v1) + (r3 * w1)) - (((r4 * (r2 ")) * r1) * w1) by RLVECT_1:def_7 .= ((r4 * (r2 ")) * v1) + ((r3 * w1) - (((r4 * (r2 ")) * r1) * w1)) by RLVECT_1:def_3 .= ((r4 * (r2 ")) * v1) + ((r3 - ((r4 * (r2 ")) * r1)) * w1) by RLVECT_1:35 ; then r2 * v2 = (r2 * ((r4 * (r2 ")) * v1)) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by RLVECT_1:def_5 .= ((r2 * (r4 * (r2 "))) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by RLVECT_1:def_7 .= ((r4 * (r2 * (r2 "))) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) .= ((r4 * 1) * v1) + (r2 * ((r3 - ((r4 * (r2 ")) * r1)) * w1)) by A13, XCMPLX_0:def_7 .= (r4 * v1) + ((r2 * (r3 - ((r4 * (r2 ")) * r1))) * w1) by RLVECT_1:def_7 .= (r4 * v1) + (((r2 * r3) - ((r2 * (r2 ")) * (r4 * r1))) * w1) .= (r4 * v1) + (((r2 * r3) - (1 * (r4 * r1))) * w1) by A13, XCMPLX_0:def_7 .= (r4 * v1) + ((- ((r1 * r4) - (r2 * r3))) * w1) .= (r4 * v1) + (- (((r1 * r4) - (r2 * r3)) * w1)) by RLVECT_4:3 ; then - (((r1 * r4) - (r2 * r3)) * w1) = (r2 * v2) - (r4 * v1) by RLSUB_2:61; then ((r1 * r4) - (r2 * r3)) * w1 = - ((r2 * v2) - (r4 * v1)) by RLVECT_1:17 .= (r4 * v1) + (- (r2 * v2)) by RLVECT_1:33 ; then ((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) * w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by RLVECT_1:def_7; then 1 * w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by A11, XCMPLX_0:def_7; then w1 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) + (- (r2 * v2))) by RLVECT_1:def_8 .= ((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) + ((((r1 * r4) - (r2 * r3)) ") * (- (r2 * v2))) by RLVECT_1:def_5 .= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((((r1 * r4) - (r2 * r3)) ") * (- (r2 * v2))) by RLVECT_1:def_7 .= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((((r1 * r4) - (r2 * r3)) ") * ((- r2) * v2)) by RLVECT_4:3 .= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (((((r1 * r4) - (r2 * r3)) ") * (- r2)) * v2) by RLVECT_1:def_7 .= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (((- (((r1 * r4) - (r2 * r3)) ")) * r2) * v2) .= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((- (((r1 * r4) - (r2 * r3)) ")) * (r2 * v2)) by RLVECT_1:def_7 .= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- ((((r1 * r4) - (r2 * r3)) ") * (r2 * v2))) by RLVECT_4:3 ; hence w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) by RLVECT_1:def_7; ::_thesis: w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) then A15: w2 = ((r2 ") * v1) - (((r2 ") * r1) * (((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) - (((((r1 * r4) - (r2 * r3)) ") * r2) * v2))) by A14, RLVECT_1:def_7 .= ((r2 ") * v1) - (((r2 ") * r1) * (((((r1 * r4) - (r2 * r3)) ") * (r4 * v1)) - ((((r1 * r4) - (r2 * r3)) ") * (r2 * v2)))) by RLVECT_1:def_7 .= ((r2 ") * v1) - (((r2 ") * r1) * ((((r1 * r4) - (r2 * r3)) ") * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:34 .= ((r2 ") * v1) - (((r1 * (r2 ")) * (((r1 * r4) - (r2 * r3)) ")) * ((r4 * v1) - (r2 * v2))) by RLVECT_1:def_7 .= ((r2 ") * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) ") * (r2 "))) * ((r4 * v1) - (r2 * v2))) .= ((r2 ") * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) ") * (r2 ")) * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:def_7 .= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((r2 ") * ((r4 * v1) - (r2 * v2))))) by RLVECT_1:def_7 .= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * v1)) - ((r2 ") * (r2 * v2))))) by RLVECT_1:34 .= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * v1)) - (((r2 ") * r2) * v2)))) by RLVECT_1:def_7 .= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - (((r2 ") * r2) * v2)))) by RLVECT_1:def_7 .= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - (1 * v2)))) by A13, XCMPLX_0:def_7 .= ((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * v1) - v2))) by RLVECT_1:def_8 .= ((r2 ") * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)) - ((((r1 * r4) - (r2 * r3)) ") * v2))) by RLVECT_1:34 .= ((r2 ") * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1))) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * v2))) by RLVECT_1:34 .= (((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)))) + (r1 * ((((r1 * r4) - (r2 * r3)) ") * v2)) by RLVECT_1:29 .= (((r2 ") * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) ") * (((r2 ") * r4) * v1)))) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def_7 .= (((r2 ") * v1) - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * (((r2 ") * r4) * v1))) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def_7 .= (((r2 ") * v1) - (((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) * v1)) + ((r1 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:def_7 .= (((r2 ") - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4))) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by RLVECT_1:35 ; (r2 ") - ((r1 * (((r1 * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) = (r2 ") * (1 - (r1 * ((((r1 * r4) - (r2 * r3)) ") * r4))) .= (r2 ") * (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) - ((((r1 * r4) - (r2 * r3)) ") * (r1 * r4))) by A11, XCMPLX_0:def_7 .= (((r2 ") * r2) * (((r1 * r4) - (r2 * r3)) ")) * (- r3) .= (1 * (((r1 * r4) - (r2 * r3)) ")) * (- r3) by A13, XCMPLX_0:def_7 .= - ((((r1 * r4) - (r2 * r3)) ") * r3) ; hence w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by A15, RLVECT_4:3; ::_thesis: verum end; set a4 = (((r1 * r4) - (r2 * r3)) ") * r1; set a3 = - ((((r1 * r4) - (r2 * r3)) ") * r3); set a2 = - ((((r1 * r4) - (r2 * r3)) ") * r2); set a1 = (((r1 * r4) - (r2 * r3)) ") * r4; now__::_thesis:_(_r1_<>_0_implies_(_w2_=_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r3)_*_v1))_+_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r1)_*_v2)_&_w1_=_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r4)_*_v1)_+_(-_(((((r1_*_r4)_-_(r2_*_r3))_")_*_r2)_*_v2))_)_) assume A16: r1 <> 0 ; ::_thesis: ( w2 = (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) & w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) ) A17: (r1 ") + ((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) = (r1 ") * (1 + ((((r1 * r4) - (r2 * r3)) ") * (r2 * r3))) .= (r1 ") * (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) + ((((r1 * r4) - (r2 * r3)) ") * (r2 * r3))) by A11, XCMPLX_0:def_7 .= (((r1 * r4) - (r2 * r3)) ") * (((r1 ") * r1) * r4) .= (((r1 * r4) - (r2 * r3)) ") * (1 * r4) by A16, XCMPLX_0:def_7 .= (((r1 * r4) - (r2 * r3)) ") * r4 ; (r1 ") * v1 = ((r1 ") * (r1 * w1)) + ((r1 ") * (r2 * w2)) by A5, RLVECT_1:def_5 .= (((r1 ") * r1) * w1) + ((r1 ") * (r2 * w2)) by RLVECT_1:def_7 .= (1 * w1) + ((r1 ") * (r2 * w2)) by A16, XCMPLX_0:def_7 .= w1 + ((r1 ") * (r2 * w2)) by RLVECT_1:def_8 .= w1 + ((r2 * (r1 ")) * w2) by RLVECT_1:def_7 ; then A18: w1 = ((r1 ") * v1) - ((r2 * (r1 ")) * w2) by RLSUB_2:61; then v2 = ((r3 * ((r1 ") * v1)) - (r3 * ((r2 * (r1 ")) * w2))) + (r4 * w2) by A6, RLVECT_1:34 .= (((r3 * (r1 ")) * v1) - (r3 * (((r1 ") * r2) * w2))) + (r4 * w2) by RLVECT_1:def_7 .= (((r3 * (r1 ")) * v1) - ((r3 * ((r1 ") * r2)) * w2)) + (r4 * w2) by RLVECT_1:def_7 .= (((r3 * (r1 ")) * v1) - (((r1 ") * (r3 * r2)) * w2)) + (r4 * w2) .= ((((r1 ") * r3) * v1) - ((r1 ") * ((r3 * r2) * w2))) + (r4 * w2) by RLVECT_1:def_7 .= (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2))) + (r4 * w2) by RLVECT_1:def_7 ; then r1 * v2 = (r1 * (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2)))) + (r1 * (r4 * w2)) by RLVECT_1:def_5 .= (r1 * (((r1 ") * (r3 * v1)) - ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:def_7 .= ((r1 * ((r1 ") * (r3 * v1))) - (r1 * ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:34 .= (((r1 * (r1 ")) * (r3 * v1)) - (r1 * ((r1 ") * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:def_7 .= (((r1 * (r1 ")) * (r3 * v1)) - ((r1 * (r1 ")) * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by RLVECT_1:def_7 .= ((1 * (r3 * v1)) - ((r1 * (r1 ")) * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by A16, XCMPLX_0:def_7 .= ((1 * (r3 * v1)) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by A16, XCMPLX_0:def_7 .= ((r3 * v1) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by RLVECT_1:def_8 .= ((r3 * v1) - ((r3 * r2) * w2)) + ((r1 * r4) * w2) by RLVECT_1:def_8 .= (r3 * v1) - (((r3 * r2) * w2) - ((r1 * r4) * w2)) by RLVECT_1:29 .= (r3 * v1) + (- (((r3 * r2) - (r1 * r4)) * w2)) by RLVECT_1:35 .= (r3 * v1) + ((- ((r3 * r2) - (r1 * r4))) * w2) by RLVECT_4:3 .= (r3 * v1) + (((r1 * r4) - (r2 * r3)) * w2) ; then (((r1 * r4) - (r2 * r3)) ") * (r1 * v2) = ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + ((((r1 * r4) - (r2 * r3)) ") * (((r1 * r4) - (r2 * r3)) * w2)) by RLVECT_1:def_5 .= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + (((((r1 * r4) - (r2 * r3)) ") * ((r1 * r4) - (r2 * r3))) * w2) by RLVECT_1:def_7 .= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + (1 * w2) by A11, XCMPLX_0:def_7 .= ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) + w2 by RLVECT_1:def_8 ; hence w2 = ((((r1 * r4) - (r2 * r3)) ") * (r1 * v2)) - ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) by RLSUB_2:61 .= (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) - ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)) by RLVECT_1:def_7 .= (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) by RLVECT_1:def_7 ; ::_thesis: w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) hence w1 = ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (r1 ")) * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A18, RLVECT_1:def_5 .= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + (((r2 * (r1 ")) * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7 .= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (((r1 ") * r1) * (((r1 * r4) - (r2 * r3)) "))) * v2)) .= ((r1 ") * v1) - (((r2 * (r1 ")) * (- (((((r1 * r4) - (r2 * r3)) ") * r3) * v1))) + ((r2 * (1 * (((r1 * r4) - (r2 * r3)) "))) * v2)) by A16, XCMPLX_0:def_7 .= ((r1 ") * v1) - (((r2 * (r1 ")) * (- ((((r1 * r4) - (r2 * r3)) ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7 .= ((r1 ") * v1) - (((r2 * (r1 ")) * ((- (((r1 * r4) - (r2 * r3)) ")) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_4:3 .= ((r1 ") * v1) - ((((r2 * (r1 ")) * (- (((r1 * r4) - (r2 * r3)) "))) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7 .= ((r1 ") * v1) - ((((((- 1) * (((r1 * r4) - (r2 * r3)) ")) * r2) * (r1 ")) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) .= ((r1 ") * v1) - (((((- 1) * (((r1 * r4) - (r2 * r3)) ")) * r2) * ((r1 ") * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7 .= ((r1 ") * v1) - ((((- 1) * (((r1 * r4) - (r2 * r3)) ")) * (r2 * ((r1 ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7 .= ((r1 ") * v1) - (((- 1) * ((((r1 * r4) - (r2 * r3)) ") * (r2 * ((r1 ") * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7 .= ((r1 ") * v1) - ((- ((((r1 * r4) - (r2 * r3)) ") * (r2 * ((r1 ") * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:16 .= ((r1 ") * v1) - ((- (((((r1 * r4) - (r2 * r3)) ") * r2) * ((r1 ") * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7 .= ((r1 ") * v1) - ((- ((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7 .= ((r1 ") * v1) - ((- (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2)) by RLVECT_1:def_7 .= (((r1 ") * v1) - (- (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1))) - ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:27 .= (((r1 ") * v1) + (((((((r1 * r4) - (r2 * r3)) ") * r2) * (r1 ")) * r3) * v1)) - ((r2 * (((r1 * r4) - (r2 * r3)) ")) * v2) by RLVECT_1:17 .= (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) ") * r2) * v2)) by A17, RLVECT_1:def_6 ; ::_thesis: verum end; then A19: ( w1 = (((((r1 * r4) - (r2 * r3)) ") * r4) * v1) + ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2) & w2 = ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2) ) by A7, A12, RLVECT_4:3; now__::_thesis:_for_u_being_VECTOR_of_V_holds_ (_(_u_in_Lin_{w1,w2}_implies_u_in_Lin_{v1,v2}_)_&_(_u_in_Lin_{v1,v2}_implies_u_in_Lin_{w1,w2}_)_) let u be VECTOR of V; ::_thesis: ( ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) & ( u in Lin {v1,v2} implies u in Lin {w1,w2} ) ) thus ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) ::_thesis: ( u in Lin {v1,v2} implies u in Lin {w1,w2} ) proof assume u in Lin {w1,w2} ; ::_thesis: u in Lin {v1,v2} then consider r5, r6 being Real such that A20: u = (r5 * w1) + (r6 * w2) by Th32; u = ((r5 * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (r6 * (((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A19, A20, RLVECT_1:def_5 .= ((r5 * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_5 .= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7 .= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7 .= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (r6 * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7 .= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7 .= ((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3 .= ((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3 .= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1)) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_3 .= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_6 .= (((r5 * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) + (r6 * ((((r1 * r4) - (r2 * r3)) ") * r1))) * v2) by RLVECT_1:def_6 ; hence u in Lin {v1,v2} by Th32; ::_thesis: verum end; assume u in Lin {v1,v2} ; ::_thesis: u in Lin {w1,w2} then consider r5, r6 being Real such that A21: u = (r5 * v1) + (r6 * v2) by Th32; u = (r5 * ((r1 * w1) + (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2))) by A5, A6, A21, RLVECT_1:def_5 .= ((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2))) by RLVECT_1:def_5 .= (((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + (r6 * (r3 * w1))) + (r6 * (r4 * w2)) by RLVECT_1:def_3 .= (((r5 * (r1 * w1)) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def_3 .= ((((r5 * r1) * w1) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def_7 .= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def_7 .= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + (r6 * (r4 * w2)) by RLVECT_1:def_7 .= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + ((r6 * r4) * w2) by RLVECT_1:def_7 .= ((((r5 * r1) + (r6 * r3)) * w1) + ((r5 * r2) * w2)) + ((r6 * r4) * w2) by RLVECT_1:def_6 .= (((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) * w2) + ((r6 * r4) * w2)) by RLVECT_1:def_3 .= (((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) + (r6 * r4)) * w2) by RLVECT_1:def_6 ; hence u in Lin {w1,w2} by Th32; ::_thesis: verum end; hence Lin {w1,w2} = Lin {v1,v2} by RUSUB_1:25; ::_thesis: ( {w1,w2} is linearly-independent & w1 <> w2 ) now__::_thesis:_for_a,_b_being_Real_st_(a_*_w1)_+_(b_*_w2)_=_0._V_holds_ (_not_a_<>_0_&_not_b_<>_0_) let a, b be Real; ::_thesis: ( (a * w1) + (b * w2) = 0. V implies ( not a <> 0 & not b <> 0 ) ) A22: ((r1 * r4) - (r2 * r3)) " <> 0 by A11, XCMPLX_1:202; assume (a * w1) + (b * w2) = 0. V ; ::_thesis: ( not a <> 0 & not b <> 0 ) then A23: 0. V = ((a * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (b * (((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by A19, RLVECT_1:def_5 .= ((a * (((((r1 * r4) - (r2 * r3)) ") * r4) * v1)) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (b * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_5 .= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + (b * (((((r1 * r4) - (r2 * r3)) ") * r1) * v2))) by RLVECT_1:def_7 .= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) ") * r3)) * v1)) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7 .= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) ") * r2)) * v2))) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7 .= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2)) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_7 .= ((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3 .= ((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + (((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2))) by RLVECT_1:def_3 .= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) * v1) + ((b * (- ((((r1 * r4) - (r2 * r3)) ") * r3))) * v1)) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_3 .= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) ") * r1)) * v2)) by RLVECT_1:def_6 .= (((a * ((((r1 * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((r1 * r4) - (r2 * r3)) ") * r3)))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) ") * r2))) + (b * ((((r1 * r4) - (r2 * r3)) ") * r1))) * v2) by RLVECT_1:def_6 ; then 0 = (((r1 * r4) - (r2 * r3)) ") * ((r4 * a) + ((- r3) * b)) by A1, A2, RLVECT_3:13; then A24: (r4 * a) - (r3 * b) = 0 by A22, XCMPLX_1:6; 0 = (((r1 * r4) - (r2 * r3)) ") * (((- r2) * a) + (r1 * b)) by A1, A2, A23, RLVECT_3:13; then A25: (r1 * b) + (- (r2 * a)) = 0 by A22, XCMPLX_1:6; assume A26: ( a <> 0 or b <> 0 ) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( a <> 0 or b <> 0 ) by A26; supposeA27: a <> 0 ; ::_thesis: contradiction (a ") * (r1 * b) = ((a ") * a) * r2 by A25, XCMPLX_1:4; then (a ") * (r1 * b) = 1 * r2 by A27, XCMPLX_0:def_7; then r2 = r1 * ((a ") * b) ; then v1 = (r1 * w1) + (r1 * (((a ") * b) * w2)) by A5, RLVECT_1:def_7; then A28: v1 = r1 * (w1 + (((a ") * b) * w2)) by RLVECT_1:def_5; ((a ") * a) * r4 = (a ") * (r3 * b) by A24, XCMPLX_1:4; then 1 * r4 = (a ") * (r3 * b) by A27, XCMPLX_0:def_7; then r4 = r3 * ((a ") * b) ; then v2 = (r3 * w1) + (r3 * (((a ") * b) * w2)) by A6, RLVECT_1:def_7; then v2 = r3 * (w1 + (((a ") * b) * w2)) by RLVECT_1:def_5; hence contradiction by A1, A2, A28, RLVECT_4:21; ::_thesis: verum end; supposeA29: b <> 0 ; ::_thesis: contradiction ((b ") * b) * r1 = (b ") * (r2 * a) by A25, XCMPLX_1:4; then 1 * r1 = (b ") * (r2 * a) by A29, XCMPLX_0:def_7; then r1 = r2 * ((b ") * a) ; then v1 = (r2 * (((b ") * a) * w1)) + (r2 * w2) by A5, RLVECT_1:def_7; then A30: v1 = r2 * ((((b ") * a) * w1) + w2) by RLVECT_1:def_5; ((b ") * b) * r3 = (b ") * (r4 * a) by A24, XCMPLX_1:4; then 1 * r3 = (b ") * (r4 * a) by A29, XCMPLX_0:def_7; then r3 = r4 * ((b ") * a) ; then v2 = (r4 * (((b ") * a) * w1)) + (r4 * w2) by A6, RLVECT_1:def_7; then v2 = r4 * ((((b ") * a) * w1) + w2) by RLVECT_1:def_5; hence contradiction by A1, A2, A30, RLVECT_4:21; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence ( {w1,w2} is linearly-independent & w1 <> w2 ) by RLVECT_3:13; ::_thesis: verum end; begin theorem :: RUSUB_3:40 for V being RealUnitarySpace for x being set holds ( x in (0). V iff x = 0. V ) by Lm1; theorem :: RUSUB_3:41 for V being RealUnitarySpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds W1 /\ W2 is Subspace of W3 by Lm2; theorem :: RUSUB_3:42 for V being RealUnitarySpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds W1 is Subspace of W2 /\ W3 by Lm3; theorem :: RUSUB_3:43 for V being RealUnitarySpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds W1 + W2 is Subspace of W3 by Lm5; theorem :: RUSUB_3:44 for V being RealUnitarySpace for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds W1 is Subspace of W2 + W3 by Lm4; theorem :: RUSUB_3:45 for V being RealUnitarySpace for W1, W2 being Subspace of V for v being VECTOR of V st W1 is Subspace of W2 holds v + W1 c= v + W2 proof let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V for v being VECTOR of V st W1 is Subspace of W2 holds v + W1 c= v + W2 let W1, W2 be Subspace of V; ::_thesis: for v being VECTOR of V st W1 is Subspace of W2 holds v + W1 c= v + W2 let v be VECTOR of V; ::_thesis: ( W1 is Subspace of W2 implies v + W1 c= v + W2 ) assume A1: W1 is Subspace of W2 ; ::_thesis: v + W1 c= v + W2 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + W1 or x in v + W2 ) assume x in v + W1 ; ::_thesis: x in v + W2 then consider u being VECTOR of V such that A2: u in W1 and A3: x = v + u by RUSUB_2:63; u in W2 by A1, A2, RUSUB_1:1; hence x in v + W2 by A3, RUSUB_2:63; ::_thesis: verum end;