rlvect_4.miz



    begin

    reserve x for set;

    reserve a,b,c,d,e,r1,r2,r3,r4,r5,r6 for Real;

    reserve V for RealLinearSpace;

    reserve u,v,v1,v2,v3,w,w1,w2,w3 for VECTOR of V;

    reserve W,W1,W2 for Subspace of V;

    scheme :: RLVECT_4:sch1

    LambdaSep3 { D,R() -> non empty set , A1,A2,A3() -> Element of D() , B1,B2,B3() -> Element of R() , F( set) -> Element of R() } :

ex f be Function of D(), R() st (f . A1()) = B1() & (f . A2()) = B2() & (f . A3()) = B3() & for C be Element of D() st C <> A1() & C <> A2() & C <> A3() holds (f . C) = F(C)

      provided

       A1: A1() <> A2()

       and

       A2: A1() <> A3()

       and

       A3: A2() <> A3();

      defpred P[ Element of D(), set] means ($1 = A1() implies $2 = B1()) & ($1 = A2() implies $2 = B2()) & ($1 = A3() implies $2 = B3()) & ($1 <> A1() & $1 <> A2() & $1 <> A3() implies $2 = F($1));

      

       A4: for x be Element of D() holds ex y be Element of R() st P[x, y]

      proof

        let x be Element of D();

        

         A5: x = A2() implies thesis by A1, A3;

        

         A6: x = A3() implies thesis by A2, A3;

        x = A1() implies thesis by A1, A2;

        hence thesis by A5, A6;

      end;

      consider f be Function of D(), R() such that

       A7: for x be Element of D() holds P[x, (f . x)] from FUNCT_2:sch 3( A4);

      take f;

      thus thesis by A7;

    end;

     Lm1:

    now

      let V be RealLinearSpace, v be VECTOR of V, a be Real;

      thus ex l be Linear_Combination of {v} st (l . v) = a

      proof

        reconsider zz = 0 , a as Element of REAL by XREAL_0:def 1;

        deffunc F( VECTOR of V) = zz;

        consider f be Function of the carrier of V, REAL such that

         A1: (f . v) = a and

         A2: for u be VECTOR of V st u <> v holds (f . u) = F(u) from FUNCT_2:sch 6;

        reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

        now

          let u be VECTOR of V;

          assume not u in {v};

          then u <> v by TARSKI:def 1;

          hence (f . u) = 0 by A2;

        end;

        then

        reconsider f as Linear_Combination of V by RLVECT_2:def 3;

        ( Carrier f) c= {v}

        proof

          let x be object;

          assume that

           A3: x in ( Carrier f) and

           A4: not x in {v};

          (f . x) <> 0 & x <> v by A3, A4, RLVECT_2: 19, TARSKI:def 1;

          hence thesis by A2, A3;

        end;

        then

        reconsider f as Linear_Combination of {v} by RLVECT_2:def 6;

        take f;

        thus thesis by A1;

      end;

    end;

     Lm2:

    now

      let V be RealLinearSpace, v1,v2 be VECTOR of V, a,b be Real;

      assume

       A1: v1 <> v2;

      thus ex l be Linear_Combination of {v1, v2} st (l . v1) = a & (l . v2) = b

      proof

        reconsider zz = 0 , a, b as Element of REAL by XREAL_0:def 1;

        deffunc F( VECTOR of V) = zz;

        consider f be Function of the carrier of V, REAL such that

         A2: (f . v1) = a & (f . v2) = b and

         A3: for u be VECTOR of V st u <> v1 & u <> v2 holds (f . u) = F(u) from FUNCT_2:sch 7( A1);

        reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

        now

          let u be VECTOR of V;

          assume not u in {v1, v2};

          then u <> v1 & u <> v2 by TARSKI:def 2;

          hence (f . u) = 0 by A3;

        end;

        then

        reconsider f as Linear_Combination of V by RLVECT_2:def 3;

        ( Carrier f) c= {v1, v2}

        proof

          let x be object;

          assume that

           A4: x in ( Carrier f) and

           A5: not x in {v1, v2};

          

           A6: x <> v2 by A5, TARSKI:def 2;

          (f . x) <> 0 & x <> v1 by A4, A5, RLVECT_2: 19, TARSKI:def 2;

          hence thesis by A3, A4, A6;

        end;

        then

        reconsider f as Linear_Combination of {v1, v2} by RLVECT_2:def 6;

        take f;

        thus thesis by A2;

      end;

    end;

     Lm3:

    now

      let V be RealLinearSpace, v1,v2,v3 be VECTOR of V, a,b,c be Real;

      assume that

       A1: v1 <> v2 and

       A2: v1 <> v3 and

       A3: v2 <> v3;

      thus ex l be Linear_Combination of {v1, v2, v3} st (l . v1) = a & (l . v2) = b & (l . v3) = c

      proof

        reconsider zz = 0 , a, b, c as Element of REAL by XREAL_0:def 1;

        deffunc F( VECTOR of V) = zz;

        consider f be Function of the carrier of V, REAL such that

         A4: (f . v1) = a & (f . v2) = b & (f . v3) = c and

         A5: for u be VECTOR of V st u <> v1 & u <> v2 & u <> v3 holds (f . u) = F(u) from LambdaSep3( A1, A2, A3);

        reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

        now

          let u be VECTOR of V;

          assume

           A6: not u in {v1, v2, v3};

          then

           A7: u <> v3 by ENUMSET1:def 1;

          u <> v1 & u <> v2 by A6, ENUMSET1:def 1;

          hence (f . u) = 0 by A5, A7;

        end;

        then

        reconsider f as Linear_Combination of V by RLVECT_2:def 3;

        ( Carrier f) c= {v1, v2, v3}

        proof

          let x be object;

          assume that

           A8: x in ( Carrier f) and

           A9: not x in {v1, v2, v3};

          

           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 thesis by A5, A8, A10;

        end;

        then

        reconsider f as Linear_Combination of {v1, v2, v3} by RLVECT_2:def 6;

        take f;

        thus thesis by A4;

      end;

    end;

    theorem :: RLVECT_4:1

    ((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

    proof

      thus ((v + w) - v) = w by RLSUB_2: 61;

      thus ((w + v) - v) = w by RLSUB_2: 61;

      

      thus

       A1: ((v - v) + w) = (( 0. V) + w) by RLVECT_1: 15

      .= w by RLVECT_1: 4;

      thus ((w - v) + v) = w by RLSUB_2: 61;

      thus thesis by A1, RLSUB_2: 61, RLVECT_1: 29;

    end;

    theorem :: RLVECT_4:2

    (v1 - w) = (v2 - w) implies v1 = v2

    proof

      assume (v1 - w) = (v2 - w);

      then ( - (v1 - w)) = (w - v2) by RLVECT_1: 33;

      then (w - v1) = (w - v2) by RLVECT_1: 33;

      hence thesis by RLVECT_1: 23;

    end;

    theorem :: RLVECT_4:3

    

     Th3: ( - (a * v)) = (( - a) * v)

    proof

      

      thus ( - (a * v)) = (a * ( - v)) by RLVECT_1: 25

      .= (( - a) * v) by RLVECT_1: 24;

    end;

    theorem :: RLVECT_4:4

    W1 is Subspace of W2 implies (v + W1) c= (v + W2)

    proof

      assume

       A1: W1 is Subspace of W2;

      let x be object;

      assume x in (v + W1);

      then

      consider u such that

       A2: u in W1 and

       A3: x = (v + u) by RLSUB_1: 63;

      u in W2 by A1, A2, RLSUB_1: 8;

      hence thesis by A3, RLSUB_1: 63;

    end;

    theorem :: RLVECT_4:5

    u in (v + W) implies (v + W) = (u + W)

    proof

      reconsider C = (v + W) as Coset of W by RLSUB_1:def 6;

      assume u in (v + W);

      then C = (u + W) by RLSUB_1: 78;

      hence thesis;

    end;

    theorem :: RLVECT_4:6

    

     Th6: for l be 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))

    proof

      let f be Linear_Combination of {u, v, w};

      assume that

       A1: u <> v and

       A2: u <> w and

       A3: v <> w;

      set c = (f . w);

      set b = (f . v);

      set a = (f . u);

      

       A4: ( Carrier f) c= {u, v, w} by RLVECT_2:def 6;

       A5:

      now

        let x be VECTOR of V;

        assume x <> v & x <> u & x <> w;

        then not x in ( Carrier f) by A4, ENUMSET1:def 1;

        hence (f . x) = 0 by RLVECT_2: 19;

      end;

      now

        per cases ;

          suppose

           A6: a = 0 ;

          now

            per cases ;

              suppose

               A7: b = 0 ;

              now

                per cases ;

                  suppose

                   A8: c = 0 ;

                  now

                    set x = the Element of ( Carrier f);

                    assume

                     A9: ( Carrier f) <> {} ;

                    then

                     A10: x is VECTOR of V by TARSKI:def 3;

                    then (f . x) <> 0 by A9, RLVECT_2: 19;

                    hence contradiction by A5, A6, A7, A8, A10;

                  end;

                  then f = ( ZeroLC V) by RLVECT_2:def 5;

                  

                  hence ( Sum f) = ( 0. V) by RLVECT_2: 30

                  .= ((f . u) * u) by A6, RLVECT_1: 10

                  .= (((f . u) * u) + ( 0. V)) by RLVECT_1: 4

                  .= (((f . u) * u) + ((f . v) * v)) by A7, RLVECT_1: 10

                  .= ((((f . u) * u) + ((f . v) * v)) + ( 0. V)) by RLVECT_1: 4

                  .= ((((f . u) * u) + ((f . v) * v)) + ((f . w) * w)) by A8, RLVECT_1: 10;

                end;

                  suppose

                   A11: c <> 0 ;

                  

                   A12: ( Carrier f) c= {w}

                  proof

                    let x be object;

                    assume that

                     A13: x in ( Carrier f) and

                     A14: not x in {w};

                    (f . x) <> 0 & x <> w by A13, A14, RLVECT_2: 19, TARSKI:def 1;

                    hence contradiction by A5, A6, A7, A13;

                  end;

                  w in ( Carrier f) by A11, RLVECT_2: 19;

                  then

                   A15: ( Carrier f) = {w} by A12, ZFMISC_1: 33;

                  set F = <*w*>;

                  

                   A16: (f (#) F) = <*(c * w)*> by RLVECT_2: 26;

                  ( rng F) = {w} & F is one-to-one by FINSEQ_1: 39, FINSEQ_3: 93;

                  

                  then ( Sum f) = ( Sum <*(c * w)*>) by A15, A16, RLVECT_2:def 8

                  .= (c * w) by RLVECT_1: 44

                  .= (( 0. V) + (c * w)) by RLVECT_1: 4

                  .= ((( 0. V) + ( 0. V)) + (c * w)) by RLVECT_1: 4

                  .= (((a * u) + ( 0. V)) + (c * w)) by A6, RLVECT_1: 10;

                  hence thesis by A7, RLVECT_1: 10;

                end;

              end;

              hence thesis;

            end;

              suppose

               A17: b <> 0 ;

              now

                per cases ;

                  suppose

                   A18: c = 0 ;

                  

                   A19: ( Carrier f) c= {v}

                  proof

                    let x be object;

                    assume that

                     A20: x in ( Carrier f) and

                     A21: not x in {v};

                    (f . x) <> 0 & x <> v by A20, A21, RLVECT_2: 19, TARSKI:def 1;

                    hence contradiction by A5, A6, A18, A20;

                  end;

                  v in ( Carrier f) by A17, RLVECT_2: 19;

                  then

                   A22: ( Carrier f) = {v} by A19, ZFMISC_1: 33;

                  set F = <*v*>;

                  

                   A23: (f (#) F) = <*(b * v)*> by RLVECT_2: 26;

                  ( rng F) = {v} & F is one-to-one by FINSEQ_1: 39, FINSEQ_3: 93;

                  

                  then ( Sum f) = ( Sum <*(b * v)*>) by A22, A23, RLVECT_2:def 8

                  .= (b * v) by RLVECT_1: 44

                  .= (( 0. V) + (b * v)) by RLVECT_1: 4

                  .= ((( 0. V) + (b * v)) + ( 0. V)) by RLVECT_1: 4

                  .= (((a * u) + (b * v)) + ( 0. V)) by A6, RLVECT_1: 10;

                  hence thesis by A18, RLVECT_1: 10;

                end;

                  suppose c <> 0 ;

                  then

                   A24: w in ( Carrier f) by RLVECT_2: 19;

                  

                   A25: ( Carrier f) c= {v, w}

                  proof

                    let x be object;

                    assume that

                     A26: x in ( Carrier f) and

                     A27: not x in {v, w};

                    

                     A28: x <> w by A27, TARSKI:def 2;

                    (f . x) <> 0 & x <> v by A26, A27, RLVECT_2: 19, TARSKI:def 2;

                    hence contradiction by A5, A6, A26, A28;

                  end;

                  v in ( Carrier f) by A17, RLVECT_2: 19;

                  then {v, w} c= ( Carrier f) by A24, ZFMISC_1: 32;

                  then

                   A29: ( Carrier f) = {v, w} by A25;

                  set F = <*v, w*>;

                  

                   A30: (f (#) F) = <*(b * v), (c * w)*> by RLVECT_2: 27;

                  ( rng F) = {v, w} & F is one-to-one by A3, FINSEQ_2: 127, FINSEQ_3: 94;

                  

                  then ( Sum f) = ( Sum <*(b * v), (c * w)*>) by A29, A30, RLVECT_2:def 8

                  .= ((b * v) + (c * w)) by RLVECT_1: 45

                  .= ((( 0. V) + (b * v)) + (c * w)) by RLVECT_1: 4;

                  hence thesis by A6, RLVECT_1: 10;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

          suppose

           A31: a <> 0 ;

          now

            per cases ;

              suppose

               A32: b = 0 ;

              now

                per cases ;

                  suppose

                   A33: c = 0 ;

                  

                   A34: ( Carrier f) c= {u}

                  proof

                    let x be object;

                    assume that

                     A35: x in ( Carrier f) and

                     A36: not x in {u};

                    (f . x) <> 0 & x <> u by A35, A36, RLVECT_2: 19, TARSKI:def 1;

                    hence contradiction by A5, A32, A33, A35;

                  end;

                  u in ( Carrier f) by A31, RLVECT_2: 19;

                  then

                   A37: ( Carrier f) = {u} by A34, ZFMISC_1: 33;

                  set F = <*u*>;

                  

                   A38: (f (#) F) = <*(a * u)*> by RLVECT_2: 26;

                  ( rng F) = {u} & F is one-to-one by FINSEQ_1: 39, FINSEQ_3: 93;

                  

                  then ( Sum f) = ( Sum <*(a * u)*>) by A37, A38, RLVECT_2:def 8

                  .= (a * u) by RLVECT_1: 44

                  .= ((a * u) + ( 0. V)) by RLVECT_1: 4

                  .= (((a * u) + ( 0. V)) + ( 0. V)) by RLVECT_1: 4

                  .= (((a * u) + (b * v)) + ( 0. V)) by A32, RLVECT_1: 10;

                  hence thesis by A33, RLVECT_1: 10;

                end;

                  suppose c <> 0 ;

                  then

                   A39: w in ( Carrier f) by RLVECT_2: 19;

                  

                   A40: ( Carrier f) c= {u, w}

                  proof

                    let x be object;

                    assume that

                     A41: x in ( Carrier f) and

                     A42: not x in {u, w};

                    

                     A43: x <> u by A42, TARSKI:def 2;

                    (f . x) <> 0 & x <> w by A41, A42, RLVECT_2: 19, TARSKI:def 2;

                    hence contradiction by A5, A32, A41, A43;

                  end;

                  u in ( Carrier f) by A31, RLVECT_2: 19;

                  then {u, w} c= ( Carrier f) by A39, ZFMISC_1: 32;

                  then

                   A44: ( Carrier f) = {u, w} by A40;

                  set F = <*u, w*>;

                  

                   A45: (f (#) F) = <*(a * u), (c * w)*> by RLVECT_2: 27;

                  ( rng F) = {u, w} & F is one-to-one by A2, FINSEQ_2: 127, FINSEQ_3: 94;

                  

                  then ( Sum f) = ( Sum <*(a * u), (c * w)*>) by A44, A45, RLVECT_2:def 8

                  .= ((a * u) + (c * w)) by RLVECT_1: 45

                  .= (((a * u) + ( 0. V)) + (c * w)) by RLVECT_1: 4;

                  hence thesis by A32, RLVECT_1: 10;

                end;

              end;

              hence thesis;

            end;

              suppose

               A46: b <> 0 ;

              now

                per cases ;

                  suppose

                   A47: c = 0 ;

                  

                   A48: ( Carrier f) c= {u, v}

                  proof

                    let x be object;

                    assume that

                     A49: x in ( Carrier f) and

                     A50: not x in {u, v};

                    

                     A51: x <> u by A50, TARSKI:def 2;

                    (f . x) <> 0 & x <> v by A49, A50, RLVECT_2: 19, TARSKI:def 2;

                    hence contradiction by A5, A47, A49, A51;

                  end;

                  v in ( Carrier f) & u in ( Carrier f) by A31, A46, RLVECT_2: 19;

                  then {u, v} c= ( Carrier f) by ZFMISC_1: 32;

                  then

                   A52: ( Carrier f) = {u, v} by A48;

                  set F = <*u, v*>;

                  

                   A53: (f (#) F) = <*(a * u), (b * v)*> by RLVECT_2: 27;

                  ( rng F) = {u, v} & F is one-to-one by A1, FINSEQ_2: 127, FINSEQ_3: 94;

                  

                  then ( Sum f) = ( Sum <*(a * u), (b * v)*>) by A52, A53, RLVECT_2:def 8

                  .= ((a * u) + (b * v)) by RLVECT_1: 45

                  .= (((a * u) + (b * v)) + ( 0. V)) by RLVECT_1: 4;

                  hence thesis by A47, RLVECT_1: 10;

                end;

                  suppose

                   A54: c <> 0 ;

                   {u, v, w} c= ( Carrier f)

                  proof

                    let x be object;

                    assume x in {u, v, w};

                    then x = u or x = v or x = w by ENUMSET1:def 1;

                    hence thesis by A31, A46, A54, RLVECT_2: 19;

                  end;

                  then

                   A55: ( Carrier f) = {u, v, w} by A4;

                  set F = <*u, v, w*>;

                  

                   A56: (f (#) F) = <*(a * u), (b * v), (c * w)*> by RLVECT_2: 28;

                  ( rng F) = {u, v, w} & F is one-to-one by A1, A2, A3, FINSEQ_2: 128, FINSEQ_3: 95;

                  

                  then ( Sum f) = ( Sum <*(a * u), (b * v), (c * w)*>) by A55, A56, RLVECT_2:def 8

                  .= (((a * u) + (b * v)) + (c * w)) by RLVECT_1: 46;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    reconsider zz = 0 as Element of REAL by XREAL_0:def 1;

    theorem :: RLVECT_4:7

    

     Th7: u <> v & u <> w & v <> w & {u, v, w} is linearly-independent iff for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0

    proof

      thus u <> v & u <> w & v <> w & {u, v, w} is linearly-independent implies for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0

      proof

        deffunc F( VECTOR of V) = zz;

        assume that

         A1: u <> v and

         A2: u <> w and

         A3: v <> w and

         A4: {u, v, w} is linearly-independent;

        let a, b, c;

        reconsider aa = a, bb = b, cc = c as Element of REAL by XREAL_0:def 1;

        consider f be Function of the carrier of V, REAL such that

         A5: (f . u) = aa & (f . v) = bb & (f . w) = cc and

         A6: for x be VECTOR of V st x <> u & x <> v & x <> w holds (f . x) = F(x) from LambdaSep3( A1, A2, A3);

        reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

        now

          let x be VECTOR of V;

          assume

           A7: not x in {u, v, w};

          then

           A8: x <> w by ENUMSET1:def 1;

          x <> u & x <> v by A7, ENUMSET1:def 1;

          hence (f . x) = 0 by A6, A8;

        end;

        then

        reconsider f as Linear_Combination of V by RLVECT_2:def 3;

        ( Carrier f) c= {u, v, w}

        proof

          let x be object;

          assume

           A9: x in ( Carrier f);

          then (f . x) <> 0 by RLVECT_2: 19;

          then x = u or x = v or x = w by A6, A9;

          hence thesis by ENUMSET1:def 1;

        end;

        then

        reconsider f as Linear_Combination of {u, v, w} by RLVECT_2:def 6;

        assume (((a * u) + (b * v)) + (c * w)) = ( 0. V);

        then

         A10: ( 0. V) = ( Sum f) by A1, A2, A3, A5, Th6;

        then

         A11: not u in ( Carrier f) by A4;

        ( not v in ( Carrier f)) & not w in ( Carrier f) by A4, A10;

        hence thesis by A5, A11, RLVECT_2: 19;

      end;

      assume

       A12: for a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) holds a = 0 & b = 0 & c = 0 ;

       A13:

      now

        assume

         A14: u = v or u = w or v = w;

        now

          per cases by A14;

            suppose u = v;

            

            then (((1 * u) + (( - 1) * v)) + ( 0 * w)) = ((u + (( - 1) * u)) + ( 0 * w)) by RLVECT_1:def 8

            .= ((u + ( - u)) + ( 0 * w)) by RLVECT_1: 16

            .= ((u + ( - u)) + ( 0. V)) by RLVECT_1: 10

            .= (u + ( - u)) by RLVECT_1: 4

            .= ( 0. V) by RLVECT_1: 5;

            hence contradiction by A12;

          end;

            suppose u = w;

            

            then (((1 * u) + ( 0 * v)) + (( - 1) * w)) = ((u + ( 0 * v)) + (( - 1) * u)) by RLVECT_1:def 8

            .= ((u + ( 0. V)) + (( - 1) * u)) by RLVECT_1: 10

            .= ((u + ( 0. V)) + ( - u)) by RLVECT_1: 16

            .= (u + ( - u)) by RLVECT_1: 4

            .= ( 0. V) by RLVECT_1: 5;

            hence contradiction by A12;

          end;

            suppose v = w;

            

            then ((( 0 * u) + (1 * v)) + (( - 1) * w)) = ((( 0 * u) + (1 * v)) + ( - v)) by RLVECT_1: 16

            .= ((( 0. V) + (1 * v)) + ( - v)) by RLVECT_1: 10

            .= ((( 0. V) + v) + ( - v)) by RLVECT_1:def 8

            .= (v + ( - v)) by RLVECT_1: 4

            .= ( 0. V) by RLVECT_1: 5;

            hence contradiction by A12;

          end;

        end;

        hence contradiction;

      end;

      hence u <> v & u <> w & v <> w;

      let l be Linear_Combination of {u, v, w};

      assume ( Sum l) = ( 0. V);

      then

       A15: ((((l . u) * u) + ((l . v) * v)) + ((l . w) * w)) = ( 0. V) by A13, Th6;

      then

       A16: (l . w) = 0 by A12;

      

       A17: (l . u) = 0 & (l . v) = 0 by A12, A15;

      thus ( Carrier l) c= {}

      proof

        let x be object;

        assume

         A18: x in ( Carrier l);

        ( Carrier l) c= {u, v, w} by RLVECT_2:def 6;

        then x = u or x = v or x = w by A18, ENUMSET1:def 1;

        hence thesis by A17, A16, A18, RLVECT_2: 19;

      end;

      thus thesis;

    end;

    theorem :: RLVECT_4:8

    

     Th8: x in ( Lin {v}) iff ex a st x = (a * v)

    proof

      thus x in ( Lin {v}) implies ex a st x = (a * v)

      proof

        assume x in ( Lin {v});

        then

        consider l be Linear_Combination of {v} such that

         A1: x = ( Sum l) by RLVECT_3: 14;

        ( Sum l) = ((l . v) * v) by RLVECT_2: 32;

        hence thesis by A1;

      end;

      given a such that

       A2: x = (a * v);

      deffunc F( VECTOR of V) = zz;

      reconsider aa = a as Element of REAL by XREAL_0:def 1;

      consider f be Function of the carrier of V, REAL such that

       A3: (f . v) = aa and

       A4: for z be VECTOR of V st z <> v holds (f . z) = F(z) from FUNCT_2:sch 6;

      reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

      now

        let z be VECTOR of V;

        assume not z in {v};

        then z <> v by TARSKI:def 1;

        hence (f . z) = 0 by A4;

      end;

      then

      reconsider f as Linear_Combination of V by RLVECT_2:def 3;

      ( Carrier f) c= {v}

      proof

        let x be object;

        assume

         A5: x in ( Carrier f);

        then (f . x) <> 0 by RLVECT_2: 19;

        then x = v by A4, A5;

        hence thesis by TARSKI:def 1;

      end;

      then

      reconsider f as Linear_Combination of {v} by RLVECT_2:def 6;

      ( Sum f) = x by A2, A3, RLVECT_2: 32;

      hence thesis by RLVECT_3: 14;

    end;

    theorem :: RLVECT_4:9

    v in ( Lin {v})

    proof

      v in {v} by TARSKI:def 1;

      hence thesis by RLVECT_3: 15;

    end;

    theorem :: RLVECT_4:10

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

    proof

      thus x in (v + ( Lin {w})) implies ex a st x = (v + (a * w))

      proof

        assume x in (v + ( Lin {w}));

        then

        consider u be VECTOR of V such that

         A1: u in ( Lin {w}) and

         A2: x = (v + u) by RLSUB_1: 63;

        ex a st u = (a * w) by A1, Th8;

        hence thesis by A2;

      end;

      given a such that

       A3: x = (v + (a * w));

      (a * w) in ( Lin {w}) by Th8;

      hence thesis by A3, RLSUB_1: 63;

    end;

    theorem :: RLVECT_4:11

    

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

    proof

      thus x in ( Lin {w1, w2}) implies ex a, b st x = ((a * w1) + (b * w2))

      proof

        assume

         A1: x in ( Lin {w1, w2});

        now

          per cases ;

            suppose w1 = w2;

            then {w1, w2} = {w1} by ENUMSET1: 29;

            then

            consider a such that

             A2: x = (a * w1) by A1, Th8;

            x = ((a * w1) + ( 0. V)) by A2, RLVECT_1: 4

            .= ((a * w1) + ( 0 * w2)) by RLVECT_1: 10;

            hence thesis;

          end;

            suppose

             A3: w1 <> w2;

            consider l be Linear_Combination of {w1, w2} such that

             A4: x = ( Sum l) by A1, RLVECT_3: 14;

            x = (((l . w1) * w1) + ((l . w2) * w2)) by A3, A4, RLVECT_2: 33;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      given a, b such that

       A5: x = ((a * w1) + (b * w2));

      now

        per cases ;

          suppose

           A6: w1 = w2;

          then x = ((a + b) * w1) by A5, RLVECT_1:def 6;

          then x in ( Lin {w1}) by Th8;

          hence thesis by A6, ENUMSET1: 29;

        end;

          suppose

           A7: w1 <> w2;

          deffunc F( VECTOR of V) = zz;

          reconsider aa = a, bb = b as Element of REAL by XREAL_0:def 1;

          consider f be Function of the carrier of V, REAL such that

           A8: (f . w1) = aa & (f . w2) = bb and

           A9: for u st u <> w1 & u <> w2 holds (f . u) = F(u) from FUNCT_2:sch 7( A7);

          reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

          now

            let u;

            assume not u in {w1, w2};

            then u <> w1 & u <> w2 by TARSKI:def 2;

            hence (f . u) = 0 by A9;

          end;

          then

          reconsider f as Linear_Combination of V by RLVECT_2:def 3;

          ( Carrier f) c= {w1, w2}

          proof

            let x be object;

            assume that

             A10: x in ( Carrier f) and

             A11: not x in {w1, w2};

            x <> w1 & x <> w2 by A11, TARSKI:def 2;

            then (f . x) = 0 by A9, A10;

            hence contradiction by A10, RLVECT_2: 19;

          end;

          then

          reconsider f as Linear_Combination of {w1, w2} by RLVECT_2:def 6;

          x = ( Sum f) by A5, A7, A8, RLVECT_2: 33;

          hence thesis by RLVECT_3: 14;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_4:12

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

    proof

      w1 in {w1, w2} & w2 in {w1, w2} by TARSKI:def 2;

      hence thesis by RLVECT_3: 15;

    end;

    theorem :: RLVECT_4:13

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

    proof

      thus x in (v + ( Lin {w1, w2})) implies ex a, b st x = ((v + (a * w1)) + (b * w2))

      proof

        assume x in (v + ( Lin {w1, w2}));

        then

        consider u such that

         A1: u in ( Lin {w1, w2}) and

         A2: x = (v + u) by RLSUB_1: 63;

        consider a, b such that

         A3: u = ((a * w1) + (b * w2)) by A1, Th11;

        take a, b;

        thus thesis by A2, A3, RLVECT_1:def 3;

      end;

      given a, b such that

       A4: x = ((v + (a * w1)) + (b * w2));

      ((a * w1) + (b * w2)) in ( Lin {w1, w2}) by Th11;

      then (v + ((a * w1) + (b * w2))) in (v + ( Lin {w1, w2})) by RLSUB_1: 63;

      hence thesis by A4, RLVECT_1:def 3;

    end;

    theorem :: RLVECT_4:14

    

     Th14: x in ( Lin {v1, v2, v3}) iff ex a, b, c st x = (((a * v1) + (b * v2)) + (c * v3))

    proof

      thus x in ( Lin {v1, v2, v3}) implies ex a, b, c st x = (((a * v1) + (b * v2)) + (c * v3))

      proof

        assume

         A1: x in ( Lin {v1, v2, v3});

        now

          per cases ;

            suppose

             A2: v1 <> v2 & v1 <> v3 & v2 <> v3;

            consider l be Linear_Combination of {v1, v2, v3} such that

             A3: x = ( Sum l) by A1, RLVECT_3: 14;

            x = ((((l . v1) * v1) + ((l . v2) * v2)) + ((l . v3) * v3)) by A2, A3, Th6;

            hence thesis;

          end;

            suppose v1 = v2 or v1 = v3 or v2 = 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

              per cases by A4, ENUMSET1: 30;

                suppose {v1, v2, v3} = {v1, v2};

                then

                consider a, b such that

                 A5: x = ((a * v1) + (b * v2)) by A1, Th11;

                x = (((a * v1) + (b * v2)) + ( 0. V)) by A5, RLVECT_1: 4

                .= (((a * v1) + (b * v2)) + ( 0 * v3)) by RLVECT_1: 10;

                hence thesis;

              end;

                suppose {v1, v2, v3} = {v1, v3};

                then

                consider a, b such that

                 A6: x = ((a * v1) + (b * v3)) by A1, Th11;

                x = (((a * v1) + ( 0. V)) + (b * v3)) by A6, RLVECT_1: 4

                .= (((a * v1) + ( 0 * v2)) + (b * v3)) by RLVECT_1: 10;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      given a, b, c such that

       A7: x = (((a * v1) + (b * v2)) + (c * v3));

      now

        per cases ;

          suppose

           A8: v1 = v2 or v1 = v3 or v2 = v3;

          now

            per cases by A8;

              suppose v1 = v2;

              then {v1, v2, v3} = {v1, v3} & x = (((a + b) * v1) + (c * v3)) by A7, ENUMSET1: 30, RLVECT_1:def 6;

              hence thesis by Th11;

            end;

              suppose

               A9: v1 = 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 thesis by A10, Th11;

            end;

              suppose

               A11: 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 thesis by A12, Th11;

            end;

          end;

          hence thesis;

        end;

          suppose

           A13: v1 <> v2 & v1 <> v3 & v2 <> v3;

          deffunc F( VECTOR of V) = zz;

          

           A14: v1 <> v3 by A13;

          

           A15: v2 <> v3 by A13;

          

           A16: v1 <> v2 by A13;

          reconsider aa = a, bb = b, cc = c as Element of REAL by XREAL_0:def 1;

          consider f be Function of the carrier of V, REAL such that

           A17: (f . v1) = aa & (f . v2) = bb & (f . v3) = cc and

           A18: for v st v <> v1 & v <> v2 & v <> v3 holds (f . v) = F(v) from LambdaSep3( A16, A14, A15);

          reconsider f as Element of ( Funcs (the carrier of V, REAL )) by FUNCT_2: 8;

          now

            let v;

            assume

             A19: not v in {v1, v2, v3};

            then

             A20: v <> v3 by ENUMSET1:def 1;

            v <> v1 & v <> v2 by A19, ENUMSET1:def 1;

            hence (f . v) = 0 by A18, A20;

          end;

          then

          reconsider f as Linear_Combination of V by RLVECT_2:def 3;

          ( Carrier f) c= {v1, v2, v3}

          proof

            let x be object;

            assume that

             A21: x in ( Carrier f) and

             A22: not x in {v1, v2, v3};

            

             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 thesis by A21, RLVECT_2: 19;

          end;

          then

          reconsider f as Linear_Combination of {v1, v2, v3} by RLVECT_2:def 6;

          x = ( Sum f) by A7, A13, A17, Th6;

          hence thesis by RLVECT_3: 14;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_4:15

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

    proof

      

       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 thesis by A1, RLVECT_3: 15;

    end;

    theorem :: RLVECT_4:16

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

    proof

      thus x in (v + ( Lin {w1, w2, w3})) implies ex a, b, c st x = (((v + (a * w1)) + (b * w2)) + (c * w3))

      proof

        assume x in (v + ( Lin {w1, w2, w3}));

        then

        consider u such that

         A1: u in ( Lin {w1, w2, w3}) and

         A2: x = (v + u) by RLSUB_1: 63;

        consider a, b, c such that

         A3: u = (((a * w1) + (b * w2)) + (c * w3)) by A1, Th14;

        take a, b, c;

        x = ((v + ((a * w1) + (b * w2))) + (c * w3)) by A2, A3, RLVECT_1:def 3;

        hence thesis by RLVECT_1:def 3;

      end;

      given a, b, c such that

       A4: x = (((v + (a * w1)) + (b * w2)) + (c * w3));

      (((a * w1) + (b * w2)) + (c * w3)) in ( Lin {w1, w2, w3}) by Th14;

      then (v + (((a * w1) + (b * w2)) + (c * w3))) in (v + ( Lin {w1, w2, w3})) by RLSUB_1: 63;

      then ((v + ((a * w1) + (b * w2))) + (c * w3)) in (v + ( Lin {w1, w2, w3})) by RLVECT_1:def 3;

      hence thesis by A4, RLVECT_1:def 3;

    end;

    theorem :: RLVECT_4:17

     {u, v} is linearly-independent & u <> v implies {u, (v - u)} is linearly-independent

    proof

      assume

       A1: {u, v} is linearly-independent & u <> v;

      now

        let a, b;

        assume ((a * u) + (b * (v - u))) = ( 0. V);

        

        then

         A2: ( 0. V) = ((a * u) + ((b * v) - (b * u))) by RLVECT_1: 34

        .= (((a * u) + (b * v)) - (b * u)) by RLVECT_1:def 3

        .= (((a * u) - (b * u)) + (b * v)) by RLVECT_1:def 3

        .= (((a - b) * u) + (b * v)) by RLVECT_1: 35;

        then (a - b) = 0 by A1, RLVECT_3: 13;

        hence a = 0 & b = 0 by A1, A2, RLVECT_3: 13;

      end;

      hence thesis by RLVECT_3: 13;

    end;

    theorem :: RLVECT_4:18

     {u, v} is linearly-independent & u <> v implies {u, (v + u)} is linearly-independent

    proof

      assume

       A1: {u, v} is linearly-independent & u <> v;

      now

        let a, b;

        assume ((a * u) + (b * (v + u))) = ( 0. V);

        

        then

         A2: ( 0. V) = ((a * u) + ((b * u) + (b * v))) by RLVECT_1:def 5

        .= (((a * u) + (b * u)) + (b * v)) by RLVECT_1:def 3

        .= (((a + b) * u) + (b * v)) by RLVECT_1:def 6;

        then b = 0 by A1, RLVECT_3: 13;

        hence a = 0 & b = 0 by A1, A2, RLVECT_3: 13;

      end;

      hence thesis by RLVECT_3: 13;

    end;

    theorem :: RLVECT_4:19

    

     Th19: {u, v} is linearly-independent & u <> v & a <> 0 implies {u, (a * v)} is linearly-independent

    proof

      assume that

       A1: {u, v} is linearly-independent & u <> v and

       A2: a <> 0 ;

      now

        let b, c;

        assume ((b * u) + (c * (a * v))) = ( 0. V);

        then

         A3: ( 0. V) = ((b * u) + ((c * a) * v)) by RLVECT_1:def 7;

        then (c * a) = 0 by A1, RLVECT_3: 13;

        hence b = 0 & c = 0 by A1, A2, A3, RLVECT_3: 13, XCMPLX_1: 6;

      end;

      hence thesis by RLVECT_3: 13;

    end;

    theorem :: RLVECT_4:20

     {u, v} is linearly-independent & u <> v implies {u, ( - v)} is linearly-independent

    proof

      

       A1: ( - v) = (( - 1) * v) by RLVECT_1: 16;

      assume {u, v} is linearly-independent & u <> v;

      hence thesis by A1, Th19;

    end;

    theorem :: RLVECT_4:21

    

     Th21: a <> b implies {(a * v), (b * v)} is linearly-dependent

    proof

      assume

       A1: a <> b;

      now

        per cases ;

          suppose v = ( 0. V);

          then (a * v) = ( 0. V) by RLVECT_1: 10;

          hence thesis by RLVECT_3: 11;

        end;

          suppose

           A2: v <> ( 0. V);

          

           A3: ((b * (a * v)) + (( - a) * (b * v))) = (((a * b) * v) + (( - a) * (b * v))) by RLVECT_1:def 7

          .= (((a * b) * v) - (a * (b * v))) by Th3

          .= (((a * b) * v) - ((a * b) * v)) by RLVECT_1:def 7

          .= ( 0. V) by RLVECT_1: 15;

          

           A4: not (b = 0 & ( - a) = 0 ) by A1;

          (a * v) <> (b * v) by A1, A2, RLVECT_1: 37;

          hence thesis by A3, A4, RLVECT_3: 13;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_4:22

    a <> 1 implies {v, (a * v)} is linearly-dependent

    proof

      v = (1 * v) by RLVECT_1:def 8;

      hence thesis by Th21;

    end;

    theorem :: RLVECT_4:23

     {u, w, v} is linearly-independent & u <> v & u <> w & v <> w implies {u, w, (v - u)} is linearly-independent

    proof

      assume

       A1: {u, w, v} is linearly-independent & u <> v & u <> w & v <> w;

      now

        let a, b, c;

        assume (((a * u) + (b * w)) + (c * (v - u))) = ( 0. V);

        

        then

         A2: ( 0. V) = (((a * u) + (b * w)) + ((c * v) - (c * u))) by RLVECT_1: 34

        .= ((a * u) + ((b * w) + ((c * v) - (c * u)))) by RLVECT_1:def 3

        .= ((a * u) + (((b * w) + (c * v)) - (c * u))) by RLVECT_1:def 3

        .= ((a * u) + (((b * w) - (c * u)) + (c * v))) by RLVECT_1:def 3

        .= (((a * u) + ((b * w) - (c * u))) + (c * v)) by RLVECT_1:def 3

        .= ((((a * u) + (b * w)) - (c * u)) + (c * v)) by RLVECT_1:def 3

        .= ((((a * u) - (c * u)) + (b * w)) + (c * v)) by RLVECT_1:def 3

        .= ((((a - c) * u) + (b * w)) + (c * v)) by RLVECT_1: 35;

        then (a - c) = 0 by A1, Th7;

        hence a = 0 & b = 0 & c = 0 by A1, A2, Th7;

      end;

      hence thesis by Th7;

    end;

    theorem :: RLVECT_4:24

     {u, w, v} is linearly-independent & u <> v & u <> w & v <> w implies {u, (w - u), (v - u)} is linearly-independent

    proof

      assume

       A1: {u, w, v} is linearly-independent & u <> v & u <> w & v <> w;

      now

        let a, b, c;

        assume (((a * u) + (b * (w - u))) + (c * (v - u))) = ( 0. V);

        

        then

         A2: ( 0. V) = (((a * u) + ((b * w) - (b * u))) + (c * (v - u))) by RLVECT_1: 34

        .= (((a * u) + ((b * w) + ( - (b * u)))) + ((c * v) - (c * u))) by RLVECT_1: 34

        .= ((((a * u) + ( - (b * u))) + (b * w)) + (( - (c * u)) + (c * v))) by RLVECT_1:def 3

        .= (((a * u) + ( - (b * u))) + ((b * w) + (( - (c * u)) + (c * v)))) by RLVECT_1:def 3

        .= (((a * u) + ( - (b * u))) + (( - (c * u)) + ((b * w) + (c * v)))) by RLVECT_1:def 3

        .= ((((a * u) + ( - (b * u))) + ( - (c * u))) + ((b * w) + (c * v))) by RLVECT_1:def 3

        .= ((((a * u) + (b * ( - u))) + ( - (c * u))) + ((b * w) + (c * v))) by RLVECT_1: 25

        .= ((((a * u) + (( - b) * u)) + ( - (c * u))) + ((b * w) + (c * v))) by RLVECT_1: 24

        .= ((((a * u) + (( - b) * u)) + (c * ( - u))) + ((b * w) + (c * v))) by RLVECT_1: 25

        .= ((((a * u) + (( - b) * u)) + (( - c) * u)) + ((b * w) + (c * v))) by RLVECT_1: 24

        .= ((((a + ( - b)) * u) + (( - c) * u)) + ((b * w) + (c * v))) by RLVECT_1:def 6

        .= ((((a + ( - b)) + ( - c)) * u) + ((b * w) + (c * v))) by RLVECT_1:def 6

        .= (((((a + ( - b)) + ( - c)) * u) + (b * w)) + (c * v)) by RLVECT_1:def 3;

        then ((a + ( - b)) + ( - c)) = 0 & b = 0 by A1, Th7;

        hence a = 0 & b = 0 & c = 0 by A1, A2, Th7;

      end;

      hence thesis by Th7;

    end;

    theorem :: RLVECT_4:25

     {u, w, v} is linearly-independent & u <> v & u <> w & v <> w implies {u, w, (v + u)} is linearly-independent

    proof

      assume

       A1: {u, w, v} is linearly-independent & u <> v & u <> w & v <> w;

      now

        let a, b, c;

        assume (((a * u) + (b * w)) + (c * (v + u))) = ( 0. V);

        

        then

         A2: ( 0. V) = (((a * u) + (b * w)) + ((c * u) + (c * v))) by RLVECT_1:def 5

        .= ((a * u) + ((b * w) + ((c * u) + (c * v)))) by RLVECT_1:def 3

        .= ((a * u) + ((c * u) + ((b * w) + (c * v)))) by RLVECT_1:def 3

        .= (((a * u) + (c * u)) + ((b * w) + (c * v))) by RLVECT_1:def 3

        .= (((a + c) * u) + ((b * w) + (c * v))) by RLVECT_1:def 6

        .= ((((a + c) * u) + (b * w)) + (c * v)) by RLVECT_1:def 3;

        then c = 0 by A1, Th7;

        hence a = 0 & b = 0 & c = 0 by A1, A2, Th7;

      end;

      hence thesis by Th7;

    end;

    theorem :: RLVECT_4:26

     {u, w, v} is linearly-independent & u <> v & u <> w & v <> w implies {u, (w + u), (v + u)} is linearly-independent

    proof

      assume

       A1: {u, w, v} is linearly-independent & u <> v & u <> w & v <> w;

      now

        let a, b, c;

        assume (((a * u) + (b * (w + u))) + (c * (v + u))) = ( 0. V);

        

        then

         A2: ( 0. V) = (((a * u) + ((b * u) + (b * w))) + (c * (v + u))) by RLVECT_1:def 5

        .= ((((a * u) + (b * u)) + (b * w)) + (c * (v + u))) by RLVECT_1:def 3

        .= ((((a + b) * u) + (b * w)) + (c * (v + u))) by RLVECT_1:def 6

        .= ((((a + b) * u) + (b * w)) + ((c * u) + (c * v))) by RLVECT_1:def 5

        .= (((a + b) * u) + ((b * w) + ((c * u) + (c * v)))) by RLVECT_1:def 3

        .= (((a + b) * u) + ((c * u) + ((b * w) + (c * v)))) by RLVECT_1:def 3

        .= ((((a + b) * u) + (c * u)) + ((b * w) + (c * v))) by RLVECT_1:def 3

        .= ((((a + b) + c) * u) + ((b * w) + (c * v))) by RLVECT_1:def 6

        .= (((((a + b) + c) * u) + (b * w)) + (c * v)) by RLVECT_1:def 3;

        then ((a + b) + c) = 0 & b = 0 by A1, Th7;

        hence a = 0 & b = 0 & c = 0 by A1, A2, Th7;

      end;

      hence thesis by Th7;

    end;

    theorem :: RLVECT_4:27

    

     Th27: {u, w, v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 implies {u, w, (a * v)} is linearly-independent

    proof

      assume that

       A1: {u, w, v} is linearly-independent & u <> v & u <> w & v <> w and

       A2: a <> 0 ;

      now

        let b, c, d;

        assume (((b * u) + (c * w)) + (d * (a * v))) = ( 0. V);

        then

         A3: ( 0. V) = (((b * u) + (c * w)) + ((d * a) * v)) by RLVECT_1:def 7;

        then (d * a) = 0 by A1, Th7;

        hence b = 0 & c = 0 & d = 0 by A1, A2, A3, Th7, XCMPLX_1: 6;

      end;

      hence thesis by Th7;

    end;

    theorem :: RLVECT_4:28

    

     Th28: {u, w, v} is linearly-independent & u <> v & u <> w & v <> w & a <> 0 & b <> 0 implies {u, (a * w), (b * v)} is linearly-independent

    proof

      assume that

       A1: {u, w, v} is linearly-independent & u <> v & u <> w & v <> w and

       A2: a <> 0 & b <> 0 ;

      now

        let c, d, e;

        assume (((c * u) + (d * (a * w))) + (e * (b * v))) = ( 0. V);

        

        then

         A3: ( 0. V) = (((c * u) + ((d * a) * w)) + (e * (b * v))) by RLVECT_1:def 7

        .= (((c * u) + ((d * a) * w)) + ((e * b) * v)) by RLVECT_1:def 7;

        then (d * a) = 0 & (e * b) = 0 by A1, Th7;

        hence c = 0 & d = 0 & e = 0 by A1, A2, A3, Th7, XCMPLX_1: 6;

      end;

      hence thesis by Th7;

    end;

    theorem :: RLVECT_4:29

     {u, w, v} is linearly-independent & u <> v & u <> w & v <> w implies {u, w, ( - v)} is linearly-independent

    proof

      ( - v) = (( - 1) * v) by RLVECT_1: 16;

      hence thesis by Th27;

    end;

    theorem :: RLVECT_4:30

     {u, w, v} is linearly-independent & u <> v & u <> w & v <> w implies {u, ( - w), ( - v)} is linearly-independent

    proof

      ( - v) = (( - 1) * v) & ( - w) = (( - 1) * w) by RLVECT_1: 16;

      hence thesis by Th28;

    end;

    theorem :: RLVECT_4:31

    

     Th31: a <> b implies {(a * v), (b * v), w} is linearly-dependent

    proof

      assume a <> b;

      then {(a * v), (b * v)} is linearly-dependent by Th21;

      hence thesis by RLVECT_3: 5, SETWISEO: 2;

    end;

    theorem :: RLVECT_4:32

    a <> 1 implies {v, (a * v), w} is linearly-dependent

    proof

      v = (1 * v) by RLVECT_1:def 8;

      hence thesis by Th31;

    end;

    theorem :: RLVECT_4:33

    v in ( Lin {w}) & v <> ( 0. V) implies ( Lin {v}) = ( Lin {w})

    proof

      assume that

       A1: v in ( Lin {w}) and

       A2: v <> ( 0. V);

      consider a such that

       A3: v = (a * w) by A1, Th8;

      now

        let u;

        

         A4: a <> 0 by A2, A3, RLVECT_1: 10;

        thus u in ( Lin {v}) implies u in ( Lin {w})

        proof

          assume u in ( Lin {v});

          then

          consider b such that

           A5: u = (b * v) by Th8;

          u = ((b * a) * w) by A3, A5, RLVECT_1:def 7;

          hence thesis by Th8;

        end;

        assume u in ( Lin {w});

        then

        consider b such that

         A6: u = (b * w) by Th8;

        ((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 Th8;

      end;

      hence thesis by RLSUB_1: 31;

    end;

    theorem :: RLVECT_4:34

    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

    proof

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

      consider r1, r2 such that

       A5: v1 = ((r1 * w1) + (r2 * w2)) by A3, Th11;

      consider r3, r4 such that

       A6: v2 = ((r3 * w1) + (r4 * w2)) by A4, Th11;

      set t = ((r1 * r4) - (r2 * r3));

       A7:

      now

        assume r1 = 0 & r2 = 0 ;

        

        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;

      end;

      now

        assume

         A8: (r1 * r4) = (r2 * r3);

        now

          per cases by A7;

            suppose

             A9: r1 <> 0 ;

            (((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;

          end;

            suppose

             A10: r2 <> 0 ;

            ((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;

          end;

        end;

        hence contradiction;

      end;

      then

       A11: ((r1 * r4) - (r2 * r3)) <> 0 ;

       A12:

      now

        assume

         A13: r2 <> 0 ;

        ((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) + (( - t) * w1))

        .= ((r4 * v1) + ( - (t * w1))) by Th3;

        then ( - (t * w1)) = ((r2 * v2) - (r4 * v1)) by RLSUB_2: 61;

        

        then (t * w1) = ( - ((r2 * v2) - (r4 * v1))) by RLVECT_1: 17

        .= ((r4 * v1) + ( - (r2 * v2))) by RLVECT_1: 33;

        then (((t " ) * t) * w1) = ((t " ) * ((r4 * v1) + ( - (r2 * v2)))) by RLVECT_1:def 7;

        then (1 * w1) = ((t " ) * ((r4 * v1) + ( - (r2 * v2)))) by A11, XCMPLX_0:def 7;

        

        then w1 = ((t " ) * ((r4 * v1) + ( - (r2 * v2)))) by RLVECT_1:def 8

        .= (((t " ) * (r4 * v1)) + ((t " ) * ( - (r2 * v2)))) by RLVECT_1:def 5

        .= ((((t " ) * r4) * v1) + ((t " ) * ( - (r2 * v2)))) by RLVECT_1:def 7

        .= ((((t " ) * r4) * v1) + ((t " ) * (( - r2) * v2))) by Th3

        .= ((((t " ) * r4) * v1) + (((t " ) * ( - r2)) * v2)) by RLVECT_1:def 7

        .= ((((t " ) * r4) * v1) + ((( - (t " )) * r2) * v2))

        .= ((((t " ) * r4) * v1) + (( - (t " )) * (r2 * v2))) by RLVECT_1:def 7

        .= ((((t " ) * r4) * v1) + ( - ((t " ) * (r2 * v2)))) by Th3;

        hence w1 = ((((t " ) * r4) * v1) + ( - (((t " ) * r2) * v2))) by RLVECT_1:def 7;

        

        then

         A15: w2 = (((r2 " ) * v1) - (((r2 " ) * r1) * (((t " ) * (r4 * v1)) - (((t " ) * r2) * v2)))) by A14, RLVECT_1:def 7

        .= (((r2 " ) * v1) - (((r2 " ) * r1) * (((t " ) * (r4 * v1)) - ((t " ) * (r2 * v2))))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - (((r2 " ) * r1) * ((t " ) * ((r4 * v1) - (r2 * v2))))) by RLVECT_1: 34

        .= (((r2 " ) * v1) - (((r1 * (r2 " )) * (t " )) * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - ((r1 * ((t " ) * (r2 " ))) * ((r4 * v1) - (r2 * v2))))

        .= (((r2 " ) * v1) - (r1 * (((t " ) * (r2 " )) * ((r4 * v1) - (r2 * v2))))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - (r1 * ((t " ) * ((r2 " ) * ((r4 * v1) - (r2 * v2)))))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - (r1 * ((t " ) * (((r2 " ) * (r4 * v1)) - ((r2 " ) * (r2 * v2)))))) by RLVECT_1: 34

        .= (((r2 " ) * v1) - (r1 * ((t " ) * (((r2 " ) * (r4 * v1)) - (((r2 " ) * r2) * v2))))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - (r1 * ((t " ) * ((((r2 " ) * r4) * v1) - (((r2 " ) * r2) * v2))))) by RLVECT_1:def 7

        .= (((r2 " ) * v1) - (r1 * ((t " ) * ((((r2 " ) * r4) * v1) - (1 * v2))))) by A13, XCMPLX_0:def 7

        .= (((r2 " ) * v1) - (r1 * ((t " ) * ((((r2 " ) * r4) * v1) - v2)))) by RLVECT_1:def 8

        .= (((r2 " ) * v1) - (r1 * (((t " ) * (((r2 " ) * r4) * v1)) - ((t " ) * v2)))) by RLVECT_1: 34

        .= (((r2 " ) * v1) - ((r1 * ((t " ) * (((r2 " ) * r4) * v1))) - (r1 * ((t " ) * v2)))) by RLVECT_1: 34

        .= ((((r2 " ) * v1) - (r1 * ((t " ) * (((r2 " ) * r4) * v1)))) + (r1 * ((t " ) * v2))) by RLVECT_1: 29

        .= ((((r2 " ) * v1) - (r1 * ((t " ) * (((r2 " ) * r4) * v1)))) + ((r1 * (t " )) * v2)) by RLVECT_1:def 7

        .= ((((r2 " ) * v1) - ((r1 * (t " )) * (((r2 " ) * r4) * v1))) + ((r1 * (t " )) * v2)) by RLVECT_1:def 7

        .= ((((r2 " ) * v1) - (((r1 * (t " )) * ((r2 " ) * r4)) * v1)) + ((r1 * (t " )) * v2)) by RLVECT_1:def 7

        .= ((((r2 " ) - ((r1 * (t " )) * ((r2 " ) * r4))) * v1) + (((t " ) * r1) * v2)) by RLVECT_1: 35;

        ((r2 " ) - ((r1 * (t " )) * ((r2 " ) * r4))) = ((r2 " ) * (1 - (r1 * ((t " ) * r4))))

        .= ((r2 " ) * (((t " ) * t) - ((t " ) * (r1 * r4)))) by A11, XCMPLX_0:def 7

        .= ((((r2 " ) * r2) * (t " )) * ( - r3))

        .= ((1 * (t " )) * ( - r3)) by A13, XCMPLX_0:def 7

        .= ( - ((t " ) * r3));

        hence w2 = (( - (((t " ) * r3) * v1)) + (((t " ) * r1) * v2)) by A15, Th3;

      end;

      set a4 = ((t " ) * r1);

      set a3 = ( - ((t " ) * r3));

      set a2 = ( - ((t " ) * r2));

      set a1 = ((t " ) * r4);

      now

        assume

         A16: r1 <> 0 ;

        

         A17: ((r1 " ) + ((((t " ) * r2) * (r1 " )) * r3)) = ((r1 " ) * (1 + ((t " ) * (r2 * r3))))

        .= ((r1 " ) * (((t " ) * t) + ((t " ) * (r2 * r3)))) by A11, XCMPLX_0:def 7

        .= ((t " ) * (((r1 " ) * r1) * r4))

        .= ((t " ) * (1 * r4)) by A16, XCMPLX_0:def 7

        .= ((t " ) * 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 Th3

        .= ((r3 * v1) + (t * w2));

        

        then ((t " ) * (r1 * v2)) = (((t " ) * (r3 * v1)) + ((t " ) * (t * w2))) by RLVECT_1:def 5

        .= (((t " ) * (r3 * v1)) + (((t " ) * t) * w2)) by RLVECT_1:def 7

        .= (((t " ) * (r3 * v1)) + (1 * w2)) by A11, XCMPLX_0:def 7

        .= (((t " ) * (r3 * v1)) + w2) by RLVECT_1:def 8;

        

        hence w2 = (((t " ) * (r1 * v2)) - ((t " ) * (r3 * v1))) by RLSUB_2: 61

        .= ((((t " ) * r1) * v2) - ((t " ) * (r3 * v1))) by RLVECT_1:def 7

        .= (( - (((t " ) * r3) * v1)) + (((t " ) * r1) * v2)) by RLVECT_1:def 7;

        

        hence w1 = (((r1 " ) * v1) - (((r2 * (r1 " )) * ( - (((t " ) * r3) * v1))) + ((r2 * (r1 " )) * (((t " ) * r1) * v2)))) by A18, RLVECT_1:def 5

        .= (((r1 " ) * v1) - (((r2 * (r1 " )) * ( - (((t " ) * r3) * v1))) + (((r2 * (r1 " )) * ((t " ) * r1)) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (((r2 * (r1 " )) * ( - (((t " ) * r3) * v1))) + ((r2 * (((r1 " ) * r1) * (t " ))) * v2)))

        .= (((r1 " ) * v1) - (((r2 * (r1 " )) * ( - (((t " ) * r3) * v1))) + ((r2 * (1 * (t " ))) * v2))) by A16, XCMPLX_0:def 7

        .= (((r1 " ) * v1) - (((r2 * (r1 " )) * ( - ((t " ) * (r3 * v1)))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (((r2 * (r1 " )) * (( - (t " )) * (r3 * v1))) + ((r2 * (t " )) * v2))) by Th3

        .= (((r1 " ) * v1) - ((((r2 * (r1 " )) * ( - (t " ))) * (r3 * v1)) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (((((( - 1) * (t " )) * r2) * (r1 " )) * (r3 * v1)) + ((r2 * (t " )) * v2)))

        .= (((r1 " ) * v1) - ((((( - 1) * (t " )) * r2) * ((r1 " ) * (r3 * v1))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (((( - 1) * (t " )) * (r2 * ((r1 " ) * (r3 * v1)))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - ((( - 1) * ((t " ) * (r2 * ((r1 " ) * (r3 * v1))))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (( - ((t " ) * (r2 * ((r1 " ) * (r3 * v1))))) + ((r2 * (t " )) * v2))) by RLVECT_1: 16

        .= (((r1 " ) * v1) - (( - (((t " ) * r2) * ((r1 " ) * (r3 * v1)))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (( - ((((t " ) * r2) * (r1 " )) * (r3 * v1))) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= (((r1 " ) * v1) - (( - (((((t " ) * r2) * (r1 " )) * r3) * v1)) + ((r2 * (t " )) * v2))) by RLVECT_1:def 7

        .= ((((r1 " ) * v1) - ( - (((((t " ) * r2) * (r1 " )) * r3) * v1))) - ((r2 * (t " )) * v2)) by RLVECT_1: 27

        .= ((((r1 " ) * v1) + (((((t " ) * r2) * (r1 " )) * r3) * v1)) - ((r2 * (t " )) * v2)) by RLVECT_1: 17

        .= ((((t " ) * r4) * v1) + ( - (((t " ) * r2) * v2))) by A17, RLVECT_1:def 6;

      end;

      then

       A19: w1 = ((((t " ) * r4) * v1) + (( - ((t " ) * r2)) * v2)) & w2 = ((( - ((t " ) * r3)) * v1) + (((t " ) * r1) * v2)) by A7, A12, Th3;

      now

        let u;

        thus u in ( Lin {w1, w2}) implies u in ( Lin {v1, v2})

        proof

          assume u in ( Lin {w1, w2});

          then

          consider r5, r6 such that

           A20: u = ((r5 * w1) + (r6 * w2)) by Th11;

          u = (((r5 * (a1 * v1)) + (r5 * (a2 * v2))) + (r6 * ((a3 * v1) + (a4 * v2)))) by A19, A20, RLVECT_1:def 5

          .= (((r5 * (a1 * v1)) + (r5 * (a2 * v2))) + ((r6 * (a3 * v1)) + (r6 * (a4 * v2)))) by RLVECT_1:def 5

          .= ((((r5 * a1) * v1) + (r5 * (a2 * v2))) + ((r6 * (a3 * v1)) + (r6 * (a4 * v2)))) by RLVECT_1:def 7

          .= ((((r5 * a1) * v1) + ((r5 * a2) * v2)) + ((r6 * (a3 * v1)) + (r6 * (a4 * v2)))) by RLVECT_1:def 7

          .= ((((r5 * a1) * v1) + ((r5 * a2) * v2)) + (((r6 * a3) * v1) + (r6 * (a4 * v2)))) by RLVECT_1:def 7

          .= ((((r5 * a1) * v1) + ((r5 * a2) * v2)) + (((r6 * a3) * v1) + ((r6 * a4) * v2))) by RLVECT_1:def 7

          .= (((r5 * a1) * v1) + (((r5 * a2) * v2) + (((r6 * a3) * v1) + ((r6 * a4) * v2)))) by RLVECT_1:def 3

          .= (((r5 * a1) * v1) + (((r6 * a3) * v1) + (((r5 * a2) * v2) + ((r6 * a4) * v2)))) by RLVECT_1:def 3

          .= ((((r5 * a1) * v1) + ((r6 * a3) * v1)) + (((r5 * a2) * v2) + ((r6 * a4) * v2))) by RLVECT_1:def 3

          .= ((((r5 * a1) + (r6 * a3)) * v1) + (((r5 * a2) * v2) + ((r6 * a4) * v2))) by RLVECT_1:def 6

          .= ((((r5 * a1) + (r6 * a3)) * v1) + (((r5 * a2) + (r6 * a4)) * v2)) by RLVECT_1:def 6;

          hence thesis by Th11;

        end;

        assume u in ( Lin {v1, v2});

        then

        consider r5, r6 such that

         A21: u = ((r5 * v1) + (r6 * v2)) by Th11;

        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 Th11;

      end;

      hence ( Lin {w1, w2}) = ( Lin {v1, v2}) by RLSUB_1: 31;

      now

        let a, b;

        

         A22: (t " ) <> 0 by A11, XCMPLX_1: 202;

        assume ((a * w1) + (b * w2)) = ( 0. V);

        

        then

         A23: ( 0. V) = (((a * (a1 * v1)) + (a * (a2 * v2))) + (b * ((a3 * v1) + (a4 * v2)))) by A19, RLVECT_1:def 5

        .= (((a * (a1 * v1)) + (a * (a2 * v2))) + ((b * (a3 * v1)) + (b * (a4 * v2)))) by RLVECT_1:def 5

        .= ((((a * a1) * v1) + (a * (a2 * v2))) + ((b * (a3 * v1)) + (b * (a4 * v2)))) by RLVECT_1:def 7

        .= ((((a * a1) * v1) + (a * (a2 * v2))) + ((b * (a3 * v1)) + ((b * a4) * v2))) by RLVECT_1:def 7

        .= ((((a * a1) * v1) + (a * (a2 * v2))) + (((b * a3) * v1) + ((b * a4) * v2))) by RLVECT_1:def 7

        .= ((((a * a1) * v1) + ((a * a2) * v2)) + (((b * a3) * v1) + ((b * a4) * v2))) by RLVECT_1:def 7

        .= (((a * a1) * v1) + (((a * a2) * v2) + (((b * a3) * v1) + ((b * a4) * v2)))) by RLVECT_1:def 3

        .= (((a * a1) * v1) + (((b * a3) * v1) + (((a * a2) * v2) + ((b * a4) * v2)))) by RLVECT_1:def 3

        .= ((((a * a1) * v1) + ((b * a3) * v1)) + (((a * a2) * v2) + ((b * a4) * v2))) by RLVECT_1:def 3

        .= ((((a * a1) + (b * a3)) * v1) + (((a * a2) * v2) + ((b * a4) * v2))) by RLVECT_1:def 6

        .= ((((a * a1) + (b * a3)) * v1) + (((a * a2) + (b * a4)) * v2)) by RLVECT_1:def 6;

        then 0 = ((t " ) * ((r4 * a) + (( - r3) * b))) by A1, A2, RLVECT_3: 13;

        then

         A24: ((r4 * a) - (r3 * b)) = 0 by A22, XCMPLX_1: 6;

         0 = ((t " ) * ((( - 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 ;

        now

          per cases by A26;

            suppose

             A27: a <> 0 ;

            ((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, Th21;

          end;

            suppose

             A29: b <> 0 ;

            (((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, Th21;

          end;

        end;

        hence contradiction;

      end;

      hence thesis by RLVECT_3: 13;

    end;

    theorem :: RLVECT_4:35

    w <> ( 0. V) & {v, w} is linearly-dependent implies ex a st v = (a * w)

    proof

      assume that

       A1: w <> ( 0. V) and

       A2: {v, w} is linearly-dependent;

      consider a, b such that

       A3: ((a * v) + (b * w)) = ( 0. V) and

       A4: a <> 0 or b <> 0 by A2, RLVECT_3: 13;

      

       A5: (a * v) = ( - (b * w)) by A3, RLVECT_1: 6;

      now

        per cases ;

          suppose

           A6: a <> 0 ;

          (((a " ) * a) * v) = ((a " ) * ( - (b * w))) by A5, RLVECT_1:def 7;

          then (1 * v) = ((a " ) * ( - (b * w))) by A6, XCMPLX_0:def 7;

          

          then v = ((a " ) * ( - (b * w))) by RLVECT_1:def 8

          .= ((a " ) * (( - b) * w)) by Th3

          .= (((a " ) * ( - b)) * w) by RLVECT_1:def 7;

          hence thesis;

        end;

          suppose

           A7: a = 0 ;

          then ( 0. V) = ( - (b * w)) by A5, RLVECT_1: 10;

          then

           A8: ( 0. V) = (( - b) * w) by Th3;

          ( - b) <> 0 by A4, A7;

          hence thesis by A1, A8, RLVECT_1: 11;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_4:36

    v <> w & {v, w} is linearly-independent & {u, v, w} is linearly-dependent implies ex a, b st u = ((a * v) + (b * w))

    proof

      assume that

       A1: v <> w & {v, w} is linearly-independent and

       A2: {u, v, w} is linearly-dependent;

      consider a, b, c such that

       A3: (((a * u) + (b * v)) + (c * w)) = ( 0. V) and

       A4: a <> 0 or b <> 0 or c <> 0 by A2, Th7;

      now

        per cases ;

          suppose

           A5: a <> 0 ;

          ((a * u) + ((b * v) + (c * w))) = ( 0. V) by A3, RLVECT_1:def 3;

          then (a * u) = ( - ((b * v) + (c * w))) by RLVECT_1: 6;

          then (((a " ) * a) * u) = ((a " ) * ( - ((b * v) + (c * w)))) by RLVECT_1:def 7;

          then (1 * u) = ((a " ) * ( - ((b * v) + (c * w)))) by A5, XCMPLX_0:def 7;

          

          then u = ((a " ) * ( - ((b * v) + (c * w)))) by RLVECT_1:def 8

          .= ((a " ) * (( - 1) * ((b * v) + (c * w)))) by RLVECT_1: 16

          .= (((a " ) * ( - 1)) * ((b * v) + (c * w))) by RLVECT_1:def 7

          .= ((((a " ) * ( - 1)) * (b * v)) + (((a " ) * ( - 1)) * (c * w))) by RLVECT_1:def 5

          .= (((((a " ) * ( - 1)) * b) * v) + (((a " ) * ( - 1)) * (c * w))) by RLVECT_1:def 7

          .= (((((a " ) * ( - 1)) * b) * v) + ((((a " ) * ( - 1)) * c) * w)) by RLVECT_1:def 7;

          hence thesis;

        end;

          suppose

           A6: a = 0 ;

          

          then ( 0. V) = ((( 0. V) + (b * v)) + (c * w)) by A3, RLVECT_1: 10

          .= ((b * v) + (c * w)) by RLVECT_1: 4;

          hence thesis by A1, A4, A6, RLVECT_3: 13;

        end;

      end;

      hence thesis;

    end;

    theorem :: RLVECT_4:37

    for V be RealLinearSpace, v be VECTOR of V, a be Real holds ex l be Linear_Combination of {v} st (l . v) = a by Lm1;

    theorem :: RLVECT_4:38

    for V be RealLinearSpace, v1,v2 be VECTOR of V, a,b be Real st v1 <> v2 holds ex l be Linear_Combination of {v1, v2} st (l . v1) = a & (l . v2) = b by Lm2;

    theorem :: RLVECT_4:39

    for V be RealLinearSpace, v1,v2,v3 be VECTOR of V, a,b,c be Real st v1 <> v2 & v1 <> v3 & v2 <> v3 holds ex l be Linear_Combination of {v1, v2, v3} st (l . v1) = a & (l . v2) = b & (l . v3) = c by Lm3;