:: Subspaces of Real Linear Space Generated by One, Two, or Three Vectors and Their Cosets :: by Wojciech A. Trybulec :: :: Received February 24, 1993 :: Copyright (c) 1993-2012 Association of Mizar Users begin scheme :: RLVECT_4:sch 1 LambdaSep3{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of F1(), F4() -> Element of F1(), F5() -> Element of F1(), F6() -> Element of F2(), F7() -> Element of F2(), F8() -> Element of F2(), F9( set ) -> Element of F2() } : ex f being Function of F1(),F2() st ( f . F3() = F6() & f . F4() = F7() & f . F5() = F8() & ( for C being Element of F1() st C <> F3() & C <> F4() & C <> F5() holds f . C = F9(C) ) ) provided A1: F3() <> F4() and A2: F3() <> F5() and A3: F4() <> F5() proofend; Lm1: now__::_thesis:_for_V_being_RealLinearSpace for_v_being_VECTOR_of_V for_a_being_Real_ex_l_being_Linear_Combination_of_{v}_st_l_._v_=_a let V be RealLinearSpace; ::_thesis: for v being VECTOR of V for a being Real ex l being Linear_Combination of {v} st l . v = a let v be VECTOR of V; ::_thesis: for a being Real ex l being Linear_Combination of {v} st l . v = a let a be Real; ::_thesis: ex l being Linear_Combination of {v} st l . v = a thus ex l being Linear_Combination of {v} st l . v = a ::_thesis: verum proof deffunc H1( VECTOR of V) -> Element of NAT = 0 ; consider f being Function of the carrier of V,REAL such that A1: f . v = a and A2: 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; now__::_thesis:_for_u_being_VECTOR_of_V_st_not_u_in_{v}_holds_ f_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in {v} implies f . u = 0 ) assume not u in {v} ; ::_thesis: f . u = 0 then u <> v by TARSKI:def_1; hence f . u = 0 by A2; ::_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 toTARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} ) assume that A3: x in Carrier f and A4: not x in {v} ; ::_thesis: contradiction ( f . x <> 0 & x <> v ) by A3, A4, RLVECT_2:19, TARSKI:def_1; hence contradiction by A2, A3; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {v} by RLVECT_2:def_6; take f ; ::_thesis: f . v = a thus f . v = a by A1; ::_thesis: verum end; end; Lm2: now__::_thesis:_for_V_being_RealLinearSpace for_v1,_v2_being_VECTOR_of_V for_a,_b_being_Real_st_v1_<>_v2_holds_ ex_l_being_Linear_Combination_of_{v1,v2}_st_ (_l_._v1_=_a_&_l_._v2_=_b_) let V be RealLinearSpace; ::_thesis: for v1, v2 being VECTOR of V for a, b being Real st v1 <> v2 holds ex l being Linear_Combination of {v1,v2} st ( l . v1 = a & l . v2 = b ) let v1, v2 be VECTOR of V; ::_thesis: for a, b being Real st v1 <> v2 holds ex l being Linear_Combination of {v1,v2} st ( l . v1 = a & l . v2 = b ) let a, b be Real; ::_thesis: ( v1 <> v2 implies ex l being Linear_Combination of {v1,v2} st ( l . v1 = a & l . v2 = b ) ) assume A1: v1 <> v2 ; ::_thesis: ex l being Linear_Combination of {v1,v2} st ( l . v1 = a & l . v2 = b ) thus ex l being Linear_Combination of {v1,v2} st ( l . v1 = a & l . v2 = b ) ::_thesis: verum proof deffunc H1( VECTOR of V) -> Element of NAT = 0 ; consider f being Function of the carrier of V,REAL such that A2: ( f . v1 = a & f . v2 = b ) and A3: for u being VECTOR of V st u <> v1 & u <> v2 holds f . u = H1(u) from FUNCT_2:sch_7(A1); 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_{v1,v2}_holds_ f_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in {v1,v2} implies f . u = 0 ) assume not u in {v1,v2} ; ::_thesis: f . u = 0 then ( u <> v1 & u <> v2 ) by TARSKI:def_2; hence f . u = 0 by A3; ::_thesis: verum end; then reconsider f = f as Linear_Combination of V by RLVECT_2:def_3; Carrier f c= {v1,v2} proof let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2} ) assume that A4: x in Carrier f and A5: not x in {v1,v2} ; ::_thesis: contradiction A6: x <> v2 by A5, TARSKI:def_2; ( f . x <> 0 & x <> v1 ) by A4, A5, RLVECT_2:19, TARSKI:def_2; hence contradiction by A3, A4, A6; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {v1,v2} by RLVECT_2:def_6; take f ; ::_thesis: ( f . v1 = a & f . v2 = b ) thus ( f . v1 = a & f . v2 = b ) by A2; ::_thesis: verum end; end; Lm3: now__::_thesis:_for_V_being_RealLinearSpace for_v1,_v2,_v3_being_VECTOR_of_V for_a,_b,_c_being_Real_st_v1_<>_v2_&_v1_<>_v3_&_v2_<>_v3_holds_ ex_l_being_Linear_Combination_of_{v1,v2,v3}_st_ (_l_._v1_=_a_&_l_._v2_=_b_&_l_._v3_=_c_) let V be RealLinearSpace; ::_thesis: for v1, v2, v3 being VECTOR of V for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds ex l being Linear_Combination of {v1,v2,v3} st ( l . v1 = a & l . v2 = b & l . v3 = c ) let v1, v2, v3 be VECTOR of V; ::_thesis: for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds ex l being Linear_Combination of {v1,v2,v3} st ( l . v1 = a & l . v2 = b & l . v3 = c ) let a, b, c be Real; ::_thesis: ( v1 <> v2 & v1 <> v3 & v2 <> v3 implies ex l being Linear_Combination of {v1,v2,v3} st ( l . v1 = a & l . v2 = b & l . v3 = c ) ) assume that A1: v1 <> v2 and A2: v1 <> v3 and A3: v2 <> v3 ; ::_thesis: ex l being Linear_Combination of {v1,v2,v3} st ( l . v1 = a & l . v2 = b & l . v3 = c ) thus ex l being Linear_Combination of {v1,v2,v3} st ( l . v1 = a & l . v2 = b & l . v3 = c ) ::_thesis: verum proof deffunc H1( VECTOR of V) -> Element of NAT = 0 ; consider f being Function of the carrier of V,REAL such that A4: ( f . v1 = a & f . v2 = b & f . v3 = c ) and A5: for u being VECTOR of V st u <> v1 & u <> v2 & u <> v3 holds f . u = H1(u) from RLVECT_4:sch_1(A1, A2, A3); 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_{v1,v2,v3}_holds_ f_._u_=_0 let u be VECTOR of V; ::_thesis: ( not u in {v1,v2,v3} implies f . u = 0 ) assume A6: not u in {v1,v2,v3} ; ::_thesis: f . u = 0 then A7: u <> v3 by ENUMSET1:def_1; ( u <> v1 & u <> v2 ) by A6, ENUMSET1:def_1; hence f . u = 0 by A5, A7; ::_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 toTARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2,v3} ) assume that A8: x in Carrier f and A9: not x in {v1,v2,v3} ; ::_thesis: contradiction A10: ( x <> v2 & x <> v3 ) by A9, ENUMSET1:def_1; ( f . x <> 0 & x <> v1 ) by A8, A9, ENUMSET1:def_1, RLVECT_2:19; hence contradiction by A5, A8, A10; ::_thesis: verum end; then reconsider f = f as Linear_Combination of {v1,v2,v3} by RLVECT_2:def_6; take f ; ::_thesis: ( f . v1 = a & f . v2 = b & f . v3 = c ) thus ( f . v1 = a & f . v2 = b & f . v3 = c ) by A4; ::_thesis: verum end; end; theorem :: RLVECT_4:1 for V being RealLinearSpace for v, w being VECTOR of V holds ( (v + w) - v = w & (w + v) - v = w & (v - v) + w = w & (w - v) + v = w & v + (w - v) = w & w + (v - v) = w & v - (v - w) = w ) proofend; :: RLVECT_1:37 extended theorem :: RLVECT_4:2 for V being RealLinearSpace for v1, w, v2 being VECTOR of V st v1 - w = v2 - w holds v1 = v2 proofend; :: Composition of RLVECT_1:38 and RLVECT_1:39 theorem Th3: :: RLVECT_4:3 for a being Real for V being RealLinearSpace for v being VECTOR of V holds - (a * v) = (- a) * v proofend; theorem :: RLVECT_4:4 for V being RealLinearSpace for v being VECTOR of V for W1, W2 being Subspace of V st W1 is Subspace of W2 holds v + W1 c= v + W2 proofend; theorem :: RLVECT_4:5 for V being RealLinearSpace for u, v being VECTOR of V for W being Subspace of V st u in v + W holds v + W = u + W proofend; theorem Th6: :: RLVECT_4:6 for V being RealLinearSpace for u, v, w being VECTOR of V for l being Linear_Combination of {u,v,w} st u <> v & u <> w & v <> w holds Sum l = (((l . u) * u) + ((l . v) * v)) + ((l . w) * w) proofend; theorem Th7: :: RLVECT_4:7 for V being RealLinearSpace for u, v, w being VECTOR of V holds ( ( u <> v & u <> w & v <> w & {u,v,w} is linearly-independent ) iff for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds ( a = 0 & b = 0 & c = 0 ) ) proofend; theorem Th8: :: RLVECT_4:8 for x being set for V being RealLinearSpace for v being VECTOR of V holds ( x in Lin {v} iff ex a being Real st x = a * v ) proofend; theorem :: RLVECT_4:9 for V being RealLinearSpace for v being VECTOR of V holds v in Lin {v} proofend; theorem :: RLVECT_4:10 for x being set for V being RealLinearSpace for v, w being VECTOR of V holds ( x in v + (Lin {w}) iff ex a being Real st x = v + (a * w) ) proofend; theorem Th11: :: RLVECT_4:11 for x being set for V being RealLinearSpace for w1, w2 being VECTOR of V holds ( x in Lin {w1,w2} iff ex a, b being Real st x = (a * w1) + (b * w2) ) proofend; theorem :: RLVECT_4:12 for V being RealLinearSpace for w1, w2 being VECTOR of V holds ( w1 in Lin {w1,w2} & w2 in Lin {w1,w2} ) proofend; theorem :: RLVECT_4:13 for x being set for V being RealLinearSpace for v, w1, w2 being VECTOR of V holds ( x in v + (Lin {w1,w2}) iff ex a, b being Real st x = (v + (a * w1)) + (b * w2) ) proofend; theorem Th14: :: RLVECT_4:14 for x being set for V being RealLinearSpace for v1, v2, v3 being VECTOR of V holds ( x in Lin {v1,v2,v3} iff ex a, b, c being Real st x = ((a * v1) + (b * v2)) + (c * v3) ) proofend; theorem :: RLVECT_4:15 for V being RealLinearSpace 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} ) proofend; theorem :: RLVECT_4:16 for x being set for V being RealLinearSpace for v, w1, w2, w3 being VECTOR of V holds ( x in v + (Lin {w1,w2,w3}) iff ex a, b, c being Real st x = ((v + (a * w1)) + (b * w2)) + (c * w3) ) proofend; theorem :: RLVECT_4:17 for V being RealLinearSpace for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds {u,(v - u)} is linearly-independent proofend; theorem :: RLVECT_4:18 for V being RealLinearSpace for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds {u,(v + u)} is linearly-independent proofend; theorem Th19: :: RLVECT_4:19 for a being Real for V being RealLinearSpace for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v & a <> 0 holds {u,(a * v)} is linearly-independent proofend; theorem :: RLVECT_4:20 for V being RealLinearSpace for u, v being VECTOR of V st {u,v} is linearly-independent & u <> v holds {u,(- v)} is linearly-independent proofend; theorem Th21: :: RLVECT_4:21 for a, b being Real for V being RealLinearSpace for v being VECTOR of V st a <> b holds {(a * v),(b * v)} is linearly-dependent proofend; theorem :: RLVECT_4:22 for a being Real for V being RealLinearSpace for v being VECTOR of V st a <> 1 holds {v,(a * v)} is linearly-dependent proofend; theorem :: RLVECT_4:23 for V being RealLinearSpace for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds {u,w,(v - u)} is linearly-independent proofend; theorem :: RLVECT_4:24 for V being RealLinearSpace for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds {u,(w - u),(v - u)} is linearly-independent proofend; theorem :: RLVECT_4:25 for V being RealLinearSpace for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds {u,w,(v + u)} is linearly-independent proofend; theorem :: RLVECT_4:26 for V being RealLinearSpace for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds {u,(w + u),(v + u)} is linearly-independent proofend; theorem Th27: :: RLVECT_4:27 for a being Real for V being RealLinearSpace for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 holds {u,w,(a * v)} is linearly-independent proofend; theorem Th28: :: RLVECT_4:28 for a, b being Real for V being RealLinearSpace for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 holds {u,(a * w),(b * v)} is linearly-independent proofend; theorem :: RLVECT_4:29 for V being RealLinearSpace for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds {u,w,(- v)} is linearly-independent proofend; theorem :: RLVECT_4:30 for V being RealLinearSpace for u, w, v being VECTOR of V st {u,w,v} is linearly-independent & u <> v & u <> w & v <> w holds {u,(- w),(- v)} is linearly-independent proofend; theorem Th31: :: RLVECT_4:31 for a, b being Real for V being RealLinearSpace for v, w being VECTOR of V st a <> b holds {(a * v),(b * v),w} is linearly-dependent proofend; theorem :: RLVECT_4:32 for a being Real for V being RealLinearSpace for v, w being VECTOR of V st a <> 1 holds {v,(a * v),w} is linearly-dependent proofend; theorem :: RLVECT_4:33 for V being RealLinearSpace for v, w being VECTOR of V st v in Lin {w} & v <> 0. V holds Lin {v} = Lin {w} proofend; theorem :: RLVECT_4:34 for V being RealLinearSpace 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 ) proofend; theorem :: RLVECT_4:35 for V being RealLinearSpace for w, v being VECTOR of V st w <> 0. V & {v,w} is linearly-dependent holds ex a being Real st v = a * w proofend; theorem :: RLVECT_4:36 for V being RealLinearSpace for v, w, u being VECTOR of V st v <> w & {v,w} is linearly-independent & {u,v,w} is linearly-dependent holds ex a, b being Real st u = (a * v) + (b * w) proofend; theorem :: RLVECT_4:37 for V being RealLinearSpace for v being VECTOR of V for a being Real ex l being Linear_Combination of {v} st l . v = a by Lm1; theorem :: RLVECT_4:38 for V being RealLinearSpace for v1, v2 being VECTOR of V for a, b being Real st v1 <> v2 holds ex l being Linear_Combination of {v1,v2} st ( l . v1 = a & l . v2 = b ) by Lm2; theorem :: RLVECT_4:39 for V being RealLinearSpace for v1, v2, v3 being VECTOR of V for a, b, c being Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds ex l being Linear_Combination of {v1,v2,v3} st ( l . v1 = a & l . v2 = b & l . v3 = c ) by Lm3;