anproj_1.miz



    begin

    reserve V for RealLinearSpace;

    reserve p,q,r,u,v,w,y,u1,v1,w1 for Element of V;

    reserve a,b,c,d,a1,b1,c1,a2,b2,c2,a3,b3,e,f for Real;

    definition

      let V, p, q;

      :: ANPROJ_1:def1

      pred are_Prop p,q means ex a, b st (a * p) = (b * q) & a <> 0 & b <> 0 ;

      reflexivity

      proof

        let p;

        (1 * p) = (1 * p);

        hence thesis;

      end;

      symmetry ;

    end

    theorem :: ANPROJ_1:1

    

     Th1: are_Prop (p,q) iff ex a st a <> 0 & p = (a * q)

    proof

       A1:

      now

        assume are_Prop (p,q);

        then

        consider a, b such that

         A2: (a * p) = (b * q) and

         A3: a <> 0 and

         A4: b <> 0 ;

        

         A5: (a " ) <> 0 by A3, XCMPLX_1: 202;

        p = (1 * p) by RLVECT_1:def 8

        .= (((a " ) * a) * p) by A3, XCMPLX_0:def 7

        .= ((a " ) * (b * q)) by A2, RLVECT_1:def 7

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

        hence ex a st a <> 0 & p = (a * q) by A4, A5, XCMPLX_1: 6;

      end;

      now

        given a such that

         A6: a <> 0 and

         A7: p = (a * q);

        (1 * p) = (a * q) by A7, RLVECT_1:def 8;

        hence are_Prop (p,q) by A6;

      end;

      hence thesis by A1;

    end;

    theorem :: ANPROJ_1:2

    

     Th2: are_Prop (p,u) & are_Prop (u,q) implies are_Prop (p,q)

    proof

      assume that

       A1: are_Prop (p,u) and

       A2: are_Prop (u,q);

      consider a, b such that

       A3: (a * p) = (b * u) and

       A4: a <> 0 and

       A5: b <> 0 by A1;

      consider c, d such that

       A6: (c * u) = (d * q) and

       A7: c <> 0 and

       A8: d <> 0 by A2;

      (b " ) <> 0 by A5, XCMPLX_1: 202;

      then ((b " ) * a) <> 0 by A4, XCMPLX_1: 6;

      then

       A9: (c * ((b " ) * a)) <> 0 by A7, XCMPLX_1: 6;

      (((b " ) * a) * p) = ((b " ) * (b * u)) by A3, RLVECT_1:def 7

      .= (((b " ) * b) * u) by RLVECT_1:def 7

      .= (1 * u) by A5, XCMPLX_0:def 7

      .= u by RLVECT_1:def 8;

      then (d * q) = ((c * ((b " ) * a)) * p) by A6, RLVECT_1:def 7;

      hence thesis by A8, A9;

    end;

    theorem :: ANPROJ_1:3

    

     Th3: are_Prop (p,( 0. V)) iff p = ( 0. V) by RLVECT_1: 11;

    definition

      let V, u, v, w;

      :: ANPROJ_1:def2

      pred u,v,w are_LinDep means ex a, b, c st (((a * u) + (b * v)) + (c * w)) = ( 0. V) & (a <> 0 or b <> 0 or c <> 0 );

    end

    theorem :: ANPROJ_1:4

    

     Th4: are_Prop (u,u1) & are_Prop (v,v1) & are_Prop (w,w1) & (u,v,w) are_LinDep implies (u1,v1,w1) are_LinDep

    proof

      assume that

       A1: are_Prop (u,u1) and

       A2: are_Prop (v,v1) and

       A3: are_Prop (w,w1) and

       A4: (u,v,w) are_LinDep ;

      consider b such that

       A5: b <> 0 and

       A6: v = (b * v1) by A2, Th1;

      consider a such that

       A7: a <> 0 and

       A8: u = (a * u1) by A1, Th1;

      consider d1,d2,d3 be Real such that

       A9: (((d1 * u) + (d2 * v)) + (d3 * w)) = ( 0. V) and

       A10: d1 <> 0 or d2 <> 0 or d3 <> 0 by A4;

      consider c such that

       A11: c <> 0 and

       A12: w = (c * w1) by A3, Th1;

      

       A13: (d1 * a) <> 0 or (d2 * b) <> 0 or (d3 * c) <> 0 by A7, A5, A11, A10, XCMPLX_1: 6;

      ( 0. V) = ((((d1 * a) * u1) + (d2 * (b * v1))) + (d3 * (c * w1))) by A8, A6, A12, A9, RLVECT_1:def 7

      .= ((((d1 * a) * u1) + ((d2 * b) * v1)) + (d3 * (c * w1))) by RLVECT_1:def 7

      .= ((((d1 * a) * u1) + ((d2 * b) * v1)) + ((d3 * c) * w1)) by RLVECT_1:def 7;

      hence thesis by A13;

    end;

    theorem :: ANPROJ_1:5

    

     Th5: (u,v,w) are_LinDep implies (u,w,v) are_LinDep & (v,u,w) are_LinDep & (w,v,u) are_LinDep & (w,u,v) are_LinDep & (v,w,u) are_LinDep

    proof

      assume (u,v,w) are_LinDep ;

      then

      consider a, b, c such that

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

       A2: a <> 0 or b <> 0 or c <> 0 ;

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

      hence thesis by A1, A2;

    end;

    

     Lm1: ((a * v) + (b * w)) = ( 0. V) implies (a * v) = (( - b) * w)

    proof

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

      

      then (a * v) = ( - (b * w)) by RLVECT_1: 6

      .= (b * ( - w)) by RLVECT_1: 25;

      hence thesis by RLVECT_1: 24;

    end;

    

     Lm2: (((a * u) + (b * v)) + (c * w)) = ( 0. V) & a <> 0 implies u = ((( - ((a " ) * b)) * v) + (( - ((a " ) * c)) * w))

    proof

      assume that

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

       A2: a <> 0 ;

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

      

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

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

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

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

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

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

      

      hence u = ((a " ) * ((( - b) * v) + (( - c) * w))) by A2, ANALOAF: 5

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

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

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

      .= ((( - ((a " ) * b)) * v) + (( - ((a " ) * c)) * w));

    end;

    theorem :: ANPROJ_1:6

    

     Th6: not v is zero & not w is zero & not are_Prop (v,w) implies ((v,w,u) are_LinDep iff ex a, b st u = ((a * v) + (b * w)))

    proof

      assume that

       A1: not v is zero and

       A2: not w is zero and

       A3: not are_Prop (v,w);

      

       A4: w <> ( 0. V) by A2;

      

       A5: v <> ( 0. V) by A1;

      

       A6: (v,w,u) are_LinDep implies ex a, b st u = ((a * v) + (b * w))

      proof

        assume (v,w,u) are_LinDep ;

        then (u,v,w) are_LinDep by Th5;

        then

        consider a, b, c such that

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

         A8: a <> 0 or b <> 0 or c <> 0 ;

        a <> 0

        proof

          assume

           A9: a = 0 ;

          

          then

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

          .= ((b * v) + (c * w));

          

           A11: b <> 0

          proof

            assume

             A12: b = 0 ;

            

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

            .= (c * w);

            hence thesis by A4, A8, A9, A12, RLVECT_1: 11;

          end;

          

           A13: c <> 0

          proof

            assume

             A14: c = 0 ;

            

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

            .= (b * v);

            hence thesis by A5, A8, A9, A14, RLVECT_1: 11;

          end;

          (b * v) = (( - c) * w) by A10, Lm1;

          then b = 0 or ( - c) = 0 by A3;

          hence contradiction by A11, A13;

        end;

        then u = ((( - ((a " ) * b)) * v) + (( - ((a " ) * c)) * w)) by A7, Lm2;

        hence thesis;

      end;

      (ex a, b st u = ((a * v) + (b * w))) implies (v,w,u) are_LinDep

      proof

        given a, b such that

         A15: u = ((a * v) + (b * w));

        ( 0. V) = (((a * v) + (b * w)) + ( - u)) by A15, RLVECT_1: 5

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

        hence thesis;

      end;

      hence thesis by A6;

    end;

    

     Lm3: (((a + b) + c) * p) = (((a * p) + (b * p)) + (c * p))

    proof

      

      thus (((a + b) + c) * p) = (((a + b) * p) + (c * p)) by RLVECT_1:def 6

      .= (((a * p) + (b * p)) + (c * p)) by RLVECT_1:def 6;

    end;

    

     Lm4: (((u + v) + w) + ((u1 + v1) + w1)) = (((u + u1) + (v + v1)) + (w + w1))

    proof

      

      thus (((u + u1) + (v + v1)) + (w + w1)) = ((u1 + (u + (v + v1))) + (w + w1)) by RLVECT_1:def 3

      .= ((u1 + (v1 + (u + v))) + (w + w1)) by RLVECT_1:def 3

      .= (((u1 + v1) + (u + v)) + (w + w1)) by RLVECT_1:def 3

      .= ((u1 + v1) + ((u + v) + (w + w1))) by RLVECT_1:def 3

      .= ((u1 + v1) + (w1 + ((u + v) + w))) by RLVECT_1:def 3

      .= (((u + v) + w) + ((u1 + v1) + w1)) by RLVECT_1:def 3;

    end;

    

     Lm5: (((a * a1) * p) + ((a * b1) * q)) = (a * ((a1 * p) + (b1 * q)))

    proof

      

      thus (((a * a1) * p) + ((a * b1) * q)) = ((a * (a1 * p)) + ((a * b1) * q)) by RLVECT_1:def 7

      .= ((a * (a1 * p)) + (a * (b1 * q))) by RLVECT_1:def 7

      .= (a * ((a1 * p) + (b1 * q))) by RLVECT_1:def 5;

    end;

    theorem :: ANPROJ_1:7

     not are_Prop (p,q) & ((a1 * p) + (b1 * q)) = ((a2 * p) + (b2 * q)) & not p is zero & not q is zero implies a1 = a2 & b1 = b2

    proof

      assume that

       A1: not are_Prop (p,q) and

       A2: ((a1 * p) + (b1 * q)) = ((a2 * p) + (b2 * q)) and

       A3: not p is zero and

       A4: not q is zero;

      (((a2 * p) + (b2 * q)) + ( - (b1 * q))) = ((a1 * p) + ((b1 * q) + ( - (b1 * q)))) by A2, RLVECT_1:def 3

      .= ((a1 * p) + ( 0. V)) by RLVECT_1: 5

      .= (a1 * p);

      

      then (a1 * p) = (((b2 * q) + ( - (b1 * q))) + (a2 * p)) by RLVECT_1:def 3

      .= (((b2 * q) - (b1 * q)) + (a2 * p)) by RLVECT_1:def 11

      .= (((b2 - b1) * q) + (a2 * p)) by RLVECT_1: 35;

      

      then ((a1 * p) + ( - (a2 * p))) = (((b2 - b1) * q) + ((a2 * p) + ( - (a2 * p)))) by RLVECT_1:def 3

      .= (((b2 - b1) * q) + ( 0. V)) by RLVECT_1: 5

      .= ((b2 - b1) * q);

      

      then

       A5: ((b2 - b1) * q) = ((a1 * p) - (a2 * p)) by RLVECT_1:def 11

      .= ((a1 - a2) * p) by RLVECT_1: 35;

      

       A6: q <> ( 0. V) by A4;

       A7:

      now

        assume

         A8: (a1 - a2) = 0 ;

        then ((b2 - b1) * q) = ( 0. V) by A5, RLVECT_1: 10;

        then (b2 - b1) = 0 by A6, RLVECT_1: 11;

        hence thesis by A8;

      end;

      

       A9: p <> ( 0. V) by A3;

      now

        assume

         A10: (b2 - b1) = 0 ;

        then ((a1 - a2) * p) = ( 0. V) by A5, RLVECT_1: 10;

        then (a1 - a2) = 0 by A9, RLVECT_1: 11;

        hence thesis by A10;

      end;

      hence thesis by A1, A5, A7;

    end;

    

     Lm6: (p + (a * v)) = (q + (b * v)) implies (((a - b) * v) + p) = q

    proof

      assume (p + (a * v)) = (q + (b * v));

      

      then ((p + (a * v)) + ( - (b * v))) = (q + ((b * v) + ( - (b * v)))) by RLVECT_1:def 3

      .= (q + ( 0. V)) by RLVECT_1: 5

      .= q;

      

      then q = (p + ((a * v) + ( - (b * v)))) by RLVECT_1:def 3

      .= (p + ((a * v) - (b * v))) by RLVECT_1:def 11

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

      hence thesis;

    end;

    theorem :: ANPROJ_1:8

     not (u,v,w) are_LinDep & (((a1 * u) + (b1 * v)) + (c1 * w)) = (((a2 * u) + (b2 * v)) + (c2 * w)) implies a1 = a2 & b1 = b2 & c1 = c2

    proof

      

       A1: (((a1 * u) + (b1 * v)) + (c1 * w)) = (((a2 * u) + (b2 * v)) + (c2 * w)) implies ((((a1 - a2) * u) + ((b1 - b2) * v)) + ((c1 - c2) * w)) = ( 0. V)

      proof

        assume (((a1 * u) + (b1 * v)) + (c1 * w)) = (((a2 * u) + (b2 * v)) + (c2 * w));

        then (((c1 - c2) * w) + ((a1 * u) + (b1 * v))) = ((a2 * u) + (b2 * v)) by Lm6;

        then ((((c1 - c2) * w) + (a1 * u)) + (b1 * v)) = ((a2 * u) + (b2 * v)) by RLVECT_1:def 3;

        then (((b1 - b2) * v) + (((c1 - c2) * w) + (a1 * u))) = (a2 * u) by Lm6;

        then ((((b1 - b2) * v) + ((c1 - c2) * w)) + (a1 * u)) = (a2 * u) by RLVECT_1:def 3;

        then ((((b1 - b2) * v) + ((c1 - c2) * w)) + (a1 * u)) = (( 0. V) + (a2 * u));

        then (((a1 - a2) * u) + (((b1 - b2) * v) + ((c1 - c2) * w))) = ( 0. V) by Lm6;

        hence thesis by RLVECT_1:def 3;

      end;

      assume

       A2: ( not (u,v,w) are_LinDep ) & (((a1 * u) + (b1 * v)) + (c1 * w)) = (((a2 * u) + (b2 * v)) + (c2 * w));

      then

       A3: (c1 - c2) = 0 by A1;

      (a1 - a2) = 0 & (b1 - b2) = 0 by A2, A1;

      hence thesis by A3;

    end;

    theorem :: ANPROJ_1:9

    

     Th9: not are_Prop (p,q) & u = ((a1 * p) + (b1 * q)) & v = ((a2 * p) + (b2 * q)) & ((a1 * b2) - (a2 * b1)) = 0 & not p is zero & not q is zero implies ( are_Prop (u,v) or u = ( 0. V) or v = ( 0. V))

    proof

      assume that

       A1: not are_Prop (p,q) and

       A2: u = ((a1 * p) + (b1 * q)) and

       A3: v = ((a2 * p) + (b2 * q)) and

       A4: ((a1 * b2) - (a2 * b1)) = 0 and

       A5: not p is zero & not q is zero;

      now

        assume that u <> ( 0. V) and v <> ( 0. V);

        

         A6: for p, q, u, v, a1, a2, b1, b2 st not are_Prop (p,q) & u = ((a1 * p) + (b1 * q)) & v = ((a2 * p) + (b2 * q)) & ((a1 * b2) - (a2 * b1)) = 0 & not p is zero & not q is zero & a1 = 0 & u <> ( 0. V) & v <> ( 0. V) holds are_Prop (u,v)

        proof

          let p, q, u, v, a1, a2, b1, b2;

          assume that not are_Prop (p,q) and

           A7: u = ((a1 * p) + (b1 * q)) and

           A8: v = ((a2 * p) + (b2 * q)) and

           A9: ((a1 * b2) - (a2 * b1)) = 0 and not p is zero and not q is zero and

           A10: a1 = 0 and

           A11: u <> ( 0. V) and

           A12: v <> ( 0. V);

           0 = (( - a2) * b1) by A9, A10;

          then

           A13: ( - a2) = 0 or b1 = 0 by XCMPLX_1: 6;

           A14:

          now

            assume b1 = 0 ;

            

            then u = (( 0. V) + ( 0 * q)) by A7, A10, RLVECT_1: 10

            .= (( 0. V) + ( 0. V)) by RLVECT_1: 10;

            hence contradiction by A11;

          end;

          then

           A15: (b1 " ) <> 0 by XCMPLX_1: 202;

           A16:

          now

            assume (b2 * (b1 " )) = 0 ;

            then b2 = 0 by A15, XCMPLX_1: 6;

            

            then v = (( 0. V) + ( 0 * q)) by A8, A13, A14, RLVECT_1: 10

            .= (( 0. V) + ( 0. V)) by RLVECT_1: 10;

            hence contradiction by A12;

          end;

          u = (( 0. V) + (b1 * q)) by A7, A10, RLVECT_1: 10;

          then

           A17: u = (b1 * q);

          v = (( 0. V) + (b2 * q)) by A8, A13, A14, RLVECT_1: 10;

          then v = (b2 * q);

          then v = (b2 * ((b1 " ) * u)) by A14, A17, ANALOAF: 5;

          then v = ((b2 * (b1 " )) * u) by RLVECT_1:def 7;

          then (1 * v) = ((b2 * (b1 " )) * u) by RLVECT_1:def 8;

          hence thesis by A16;

        end;

        now

          assume that

           A18: a1 <> 0 and

           A19: a2 <> 0 ;

           A20:

          now

            (a1 " ) <> 0 by A18, XCMPLX_1: 202;

            then

             A21: (a2 * (a1 " )) <> 0 by A19, XCMPLX_1: 6;

            assume

             A22: b1 = 0 ;

            then b2 = 0 by A4, A18, XCMPLX_1: 6;

            then v = ((a2 * p) + ( 0. V)) by A3, RLVECT_1: 10;

            then

             A23: v = (a2 * p);

            u = ((a1 * p) + ( 0. V)) by A2, A22, RLVECT_1: 10;

            then u = (a1 * p);

            

            then v = (a2 * ((a1 " ) * u)) by A18, A23, ANALOAF: 5

            .= ((a2 * (a1 " )) * u) by RLVECT_1:def 7;

            then (1 * v) = ((a2 * (a1 " )) * u) by RLVECT_1:def 8;

            hence are_Prop (u,v) by A21;

          end;

          now

            

             A24: (b2 * u) = (((a1 * b2) * p) + ((b2 * b1) * q)) & (b1 * v) = (((a2 * b1) * p) + ((b1 * b2) * q)) by A2, A3, Lm5;

            assume

             A25: b1 <> 0 ;

            then b2 <> 0 by A4, A19, XCMPLX_1: 6;

            hence are_Prop (u,v) by A4, A25, A24;

          end;

          hence thesis by A20;

        end;

        hence thesis by A1, A2, A3, A4, A5, A6;

      end;

      hence thesis;

    end;

    theorem :: ANPROJ_1:10

    

     Th10: (u = ( 0. V) or v = ( 0. V) or w = ( 0. V)) implies (u,v,w) are_LinDep

    proof

      

       A1: for u, v, w st u = ( 0. V) holds (u,v,w) are_LinDep

      proof

        let u, v, w such that

         A2: u = ( 0. V);

        ( 0. V) = (( 0. V) + ( 0. V))

        .= ((1 * u) + ( 0. V)) by A2

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

        .= (((1 * u) + ( 0 * v)) + ( 0. V))

        .= (((1 * u) + ( 0 * v)) + ( 0 * w)) by RLVECT_1: 10;

        hence thesis;

      end;

       A3:

      now

        assume v = ( 0. V);

        then (v,w,u) are_LinDep by A1;

        hence thesis by Th5;

      end;

       A4:

      now

        assume w = ( 0. V);

        then (w,u,v) are_LinDep by A1;

        hence thesis by Th5;

      end;

      assume u = ( 0. V) or v = ( 0. V) or w = ( 0. V);

      hence thesis by A1, A3, A4;

    end;

    theorem :: ANPROJ_1:11

    

     Th11: ( are_Prop (u,v) or are_Prop (w,u) or are_Prop (v,w)) implies (w,u,v) are_LinDep

    proof

      

       A1: for u, v, w st are_Prop (u,v) holds (w,u,v) are_LinDep

      proof

        let u, v, w;

        

         A2: ( 0 * w) = ( 0. V) by RLVECT_1: 10;

        assume are_Prop (u,v);

        then

        consider a, b such that

         A3: (a * u) = (b * v) and

         A4: a <> 0 and b <> 0 ;

        ( 0. V) = ((a * u) + ( - (b * v))) by A3, RLVECT_1: 5

        .= ((a * u) + (( - 1) * (b * v))) by RLVECT_1: 16

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

        then ( 0. V) = ((( 0 * w) + (a * u)) + ((( - 1) * b) * v)) by A2;

        hence thesis by A4;

      end;

       A5:

      now

        assume are_Prop (w,u);

        then (v,w,u) are_LinDep by A1;

        hence thesis by Th5;

      end;

       A6:

      now

        assume are_Prop (v,w);

        then (u,v,w) are_LinDep by A1;

        hence thesis by Th5;

      end;

      assume are_Prop (u,v) or are_Prop (w,u) or are_Prop (v,w);

      hence thesis by A1, A5, A6;

    end;

    theorem :: ANPROJ_1:12

    

     Th12: not (u,v,w) are_LinDep implies not u is zero & not v is zero & not w is zero & not are_Prop (u,v) & not are_Prop (v,w) & not are_Prop (w,u) by Th10, Th11;

    theorem :: ANPROJ_1:13

    

     Th13: (p + q) = ( 0. V) implies are_Prop (p,q)

    proof

      assume (p + q) = ( 0. V);

      then q = ( - p) by RLVECT_1:def 10;

      then q = (( - 1) * p) by RLVECT_1: 16;

      hence thesis by Th1;

    end;

    theorem :: ANPROJ_1:14

    

     Th14: not are_Prop (p,q) & (p,q,u) are_LinDep & (p,q,v) are_LinDep & (p,q,w) are_LinDep & not p is zero & not q is zero implies (u,v,w) are_LinDep

    proof

      assume that

       A1: not are_Prop (p,q) and

       A2: (p,q,u) are_LinDep and

       A3: (p,q,v) are_LinDep and

       A4: (p,q,w) are_LinDep and

       A5: not p is zero & not q is zero;

      consider a1, b1 such that

       A6: u = ((a1 * p) + (b1 * q)) by A1, A2, A5, Th6;

      consider a3, b3 such that

       A7: w = ((a3 * p) + (b3 * q)) by A1, A4, A5, Th6;

      consider a2, b2 such that

       A8: v = ((a2 * p) + (b2 * q)) by A1, A3, A5, Th6;

      set a = ((a2 * b3) - (a3 * b2)), b = (( - (a1 * b3)) + (a3 * b1)), c = ((a1 * b2) - (a2 * b1));

       A9:

      now

        

         A10: w = ( 0. V) & v = ( 0. V) & ( are_Prop (v,w) or v = ( 0. V) or w = ( 0. V)) implies thesis by Th10;

        

         A11: w = ( 0. V) & u = ( 0. V) & ( are_Prop (v,w) or v = ( 0. V) or w = ( 0. V)) implies thesis by Th10;

        

         A12: u = ( 0. V) & v = ( 0. V) & ( are_Prop (v,w) or v = ( 0. V) or w = ( 0. V)) implies thesis by Th10;

        

         A13: (w = ( 0. V) & are_Prop (u,v) & w = ( 0. V) or u = ( 0. V) & u = ( 0. V) & are_Prop (v,w) or are_Prop (w,u) & v = ( 0. V) & v = ( 0. V)) implies thesis by Th11;

        

         A14: are_Prop (w,u) & are_Prop (u,v) & are_Prop (v,w) implies thesis by Th11;

        assume that

         A15: a = 0 and

         A16: b = 0 and

         A17: c = 0 ;

         0 = ((a3 * b1) - (a1 * b3)) by A16;

        hence thesis by A1, A5, A6, A8, A7, A15, A17, A14, A13, A11, A10, A12, Th9;

      end;

      ( 0. V) = ((((a * a1) + (b * a2)) + (c * a3)) * p) & ( 0. V) = ((((a * b1) + (b * b2)) + (c * b3)) * q) by RLVECT_1: 10;

      then

       A18: ( 0. V) = (((((a * a1) + (b * a2)) + (c * a3)) * p) + ((((a * b1) + (b * b2)) + (c * b3)) * q));

      ((((a * a1) + (b * a2)) + (c * a3)) * p) = ((((a * a1) * p) + ((b * a2) * p)) + ((c * a3) * p)) by Lm3;

      then ( 0. V) = (((((a * a1) * p) + ((b * a2) * p)) + ((c * a3) * p)) + ((((a * b1) * q) + ((b * b2) * q)) + ((c * b3) * q))) by A18, Lm3;

      then

       A19: ( 0. V) = (((((a * a1) * p) + ((a * b1) * q)) + (((b * a2) * p) + ((b * b2) * q))) + (((c * a3) * p) + ((c * b3) * q))) by Lm4;

      

       A20: (((c * a3) * p) + ((c * b3) * q)) = (c * ((a3 * p) + (b3 * q))) by Lm5;

      (((a * a1) * p) + ((a * b1) * q)) = (a * ((a1 * p) + (b1 * q))) & (((b * a2) * p) + ((b * b2) * q)) = (b * ((a2 * p) + (b2 * q))) by Lm5;

      hence thesis by A6, A8, A7, A19, A20, A9;

    end;

    

     Lm7: (a * ((b * v) + (c * w))) = (((a * b) * v) + ((a * c) * w))

    proof

      

      thus (((a * b) * v) + ((a * c) * w)) = ((a * (b * v)) + ((a * c) * w)) by RLVECT_1:def 7

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

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

    end;

    theorem :: ANPROJ_1:15

     not (u,v,w) are_LinDep & (u,v,p) are_LinDep & (v,w,q) are_LinDep implies ex y st (u,w,y) are_LinDep & (p,q,y) are_LinDep & not y is zero

    proof

      assume that

       A1: not (u,v,w) are_LinDep and

       A2: (u,v,p) are_LinDep and

       A3: (v,w,q) are_LinDep ;

      

       A4: not v is zero by A1, Th12;

      

       A5: not w is zero by A1, Th12;

       A6:

      now

         A7:

        now

          assume not not q is zero;

          then q = ( 0. V);

          then

           A8: (p,q,w) are_LinDep by Th10;

          (u,w,w) are_LinDep by Th11;

          hence thesis by A5, A8;

        end;

         A9:

        now

          assume not not p is zero;

          then p = ( 0. V);

          then

           A10: (p,q,w) are_LinDep by Th10;

          (u,w,w) are_LinDep by Th11;

          hence thesis by A5, A10;

        end;

         A11:

        now

          assume are_Prop (p,q);

          then

           A12: (p,q,w) are_LinDep by Th11;

          (u,w,w) are_LinDep by Th11;

          hence thesis by A5, A12;

        end;

        assume are_Prop (p,q) or not not p is zero or not not q is zero;

        hence thesis by A11, A9, A7;

      end;

      

       A13: not u is zero by A1, Th12;

       not are_Prop (u,v) by A1, Th12;

      then

      consider a1, b1 such that

       A14: p = ((a1 * u) + (b1 * v)) by A2, A13, A4, Th6;

      

       A15: not are_Prop (w,u) by A1, Th12;

       not are_Prop (v,w) by A1, Th12;

      then

      consider a2, b2 such that

       A16: q = ((a2 * v) + (b2 * w)) by A3, A4, A5, Th6;

      

       A17: ((c * p) + (d * q)) = ((((c * a1) * u) + (((c * b1) + (d * a2)) * v)) + ((d * b2) * w))

      proof

        

        thus ((c * p) + (d * q)) = ((((c * a1) * u) + ((c * b1) * v)) + (d * ((a2 * v) + (b2 * w)))) by A14, A16, Lm7

        .= ((((c * a1) * u) + ((c * b1) * v)) + (((d * a2) * v) + ((d * b2) * w))) by Lm7

        .= (((((c * a1) * u) + ((c * b1) * v)) + ((d * a2) * v)) + ((d * b2) * w)) by RLVECT_1:def 3

        .= ((((c * a1) * u) + (((c * b1) * v) + ((d * a2) * v))) + ((d * b2) * w)) by RLVECT_1:def 3

        .= ((((c * a1) * u) + (((c * b1) + (d * a2)) * v)) + ((d * b2) * w)) by RLVECT_1:def 6;

      end;

       A18:

      now

        assume that

         A19: not are_Prop (p,q) and

         A20: not p is zero and

         A21: not q is zero and

         A22: b1 <> 0 ;

         A23:

        now

          set c = 1, d = ( - (b1 * (a2 " )));

          set y = ((c * p) + (d * q));

          assume

           A24: a2 <> 0 ;

          then (a2 " ) <> 0 by XCMPLX_1: 202;

          then

           A25: (b1 * (a2 " )) <> 0 by A22, XCMPLX_1: 6;

          

           A26: not y is zero

          proof

            assume not not y is zero;

            

            then ( 0. V) = ((1 * p) + (( - (b1 * (a2 " ))) * q))

            .= ((1 * p) + ((b1 * (a2 " )) * ( - q))) by RLVECT_1: 24

            .= ((1 * p) + ( - ((b1 * (a2 " )) * q))) by RLVECT_1: 25;

            then ( - (1 * p)) = ( - ((b1 * (a2 " )) * q)) by RLVECT_1:def 10;

            then (1 * p) = ((b1 * (a2 " )) * q) by RLVECT_1: 18;

            hence contradiction by A19, A25;

          end;

          ((c * b1) + (d * a2)) = (b1 + (( - b1) * ((a2 " ) * a2)))

          .= (b1 + (( - b1) * 1)) by A24, XCMPLX_0:def 7

          .= 0 ;

          

          then y = ((((c * a1) * u) + ( 0 * v)) + ((d * b2) * w)) by A17

          .= ((((c * a1) * u) + ( 0. V)) + ((d * b2) * w)) by RLVECT_1: 10

          .= (((c * a1) * u) + ((d * b2) * w));

          then

           A27: (u,w,y) are_LinDep by A15, A13, A5, Th6;

          (p,q,y) are_LinDep by A19, A20, A21, Th6;

          hence thesis by A26, A27;

        end;

        now

          set c = 0 , d = 1;

          set y = ((c * p) + (d * q));

          

           A28: y = (( 0. V) + (1 * q)) by RLVECT_1: 10

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

          .= q;

          assume a2 = 0 ;

          then ((c * b1) + (d * a2)) = 0 ;

          

          then y = ((((c * a1) * u) + ( 0 * v)) + ((d * b2) * w)) by A17

          .= ((((c * a1) * u) + ( 0. V)) + ((d * b2) * w)) by RLVECT_1: 10

          .= (((c * a1) * u) + ((d * b2) * w));

          then

           A29: (u,w,y) are_LinDep by A15, A13, A5, Th6;

          (p,q,y) are_LinDep by A19, A20, A21, Th6;

          hence thesis by A21, A28, A29;

        end;

        hence thesis by A23;

      end;

      now

        assume that

         A30: not are_Prop (p,q) and

         A31: not p is zero and

         A32: not q is zero and

         A33: b1 = 0 ;

        now

          set c = 1, d = 0 ;

          set y = ((c * p) + (d * q));

          

           A34: y = (p + ( 0 * q)) by RLVECT_1:def 8

          .= (p + ( 0. V)) by RLVECT_1: 10

          .= p;

          ((c * b1) + (d * a2)) = 0 by A33;

          

          then y = ((((c * a1) * u) + ( 0 * v)) + ((d * b2) * w)) by A17

          .= ((((c * a1) * u) + ( 0. V)) + ((d * b2) * w)) by RLVECT_1: 10

          .= (((c * a1) * u) + ((d * b2) * w));

          then

           A35: (u,w,y) are_LinDep by A15, A13, A5, Th6;

          (p,q,y) are_LinDep by A30, A31, A32, Th6;

          hence thesis by A31, A34, A35;

        end;

        hence thesis;

      end;

      hence thesis by A6, A18;

    end;

    theorem :: ANPROJ_1:16

     not are_Prop (p,q) & not p is zero & not q is zero implies for u, v holds ex y st not y is zero & (u,v,y) are_LinDep & not are_Prop (u,y) & not are_Prop (v,y)

    proof

      assume that

       A1: not are_Prop (p,q) and

       A2: not p is zero and

       A3: not q is zero;

      let u, v;

       A4:

      now

        assume that not are_Prop (u,v) and

         A5: not not u is zero;

        

         A6: u = ( 0. V) by A5;

        then

         A7: not are_Prop (v,q) implies not are_Prop (v,q) & not q is zero & (u,v,q) are_LinDep & not are_Prop (u,q) by A3, Th3, Th10;

         not are_Prop (v,p) implies not are_Prop (v,p) & not p is zero & (u,v,p) are_LinDep & not are_Prop (u,p) by A2, A6, Th3, Th10;

        hence thesis by A1, A7, Th2;

      end;

       A8:

      now

        set y = (u + v);

        assume that

         A9: not are_Prop (u,v) and

         A10: not u is zero and

         A11: not v is zero;

        (u + v) <> ( 0. V) by A9, Th13;

        hence not y is zero;

        (((1 * u) + (1 * v)) + (( - 1) * y)) = ((u + (1 * v)) + (( - 1) * (u + v))) by RLVECT_1:def 8

        .= ((u + v) + (( - 1) * (u + v))) by RLVECT_1:def 8

        .= ((u + v) + ( - (u + v))) by RLVECT_1: 16

        .= ((v + u) + (( - u) + ( - v))) by RLVECT_1: 31

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

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

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

        .= (v + ( - v))

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

        hence (u,v,y) are_LinDep ;

        

         A12: v <> ( 0. V) by A11;

        now

          let a, b;

          assume (a * u) = (b * y);

          

          then (( - (b * u)) + (a * u)) = (( - (b * u)) + ((b * u) + (b * v))) by RLVECT_1:def 5

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

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

          .= (b * v);

          

          then

           A13: (b * v) = ((a * u) + (b * ( - u))) by RLVECT_1: 25

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

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

          now

            assume (a + ( - b)) = 0 ;

            then (b * v) = ( 0. V) by A13, RLVECT_1: 10;

            hence b = 0 by A12, RLVECT_1: 11;

          end;

          hence a = 0 or b = 0 by A9, A13;

        end;

        hence not are_Prop (u,y);

        

         A14: u <> ( 0. V) by A10;

        now

          let a, b;

          assume (a * v) = (b * y);

          

          then ((a * v) + ( - (b * v))) = (((b * u) + (b * v)) + ( - (b * v))) by RLVECT_1:def 5

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

          .= ((b * u) + ( 0. V)) by RLVECT_1: 5

          .= (b * u);

          

          then

           A15: (b * u) = ((a * v) + (b * ( - v))) by RLVECT_1: 25

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

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

          now

            assume (a + ( - b)) = 0 ;

            then (b * u) = ( 0. V) by A15, RLVECT_1: 10;

            hence b = 0 by A14, RLVECT_1: 11;

          end;

          hence a = 0 or b = 0 by A9, A15;

        end;

        hence not are_Prop (v,y);

      end;

       A16:

      now

        assume that not are_Prop (u,v) and

         A17: not not v is zero;

        

         A18: v = ( 0. V) by A17;

        then

         A19: not are_Prop (u,q) implies not q is zero & (u,v,q) are_LinDep & not are_Prop (u,q) & not are_Prop (v,q) by A3, Th3, Th10;

         not are_Prop (u,p) implies not p is zero & (u,v,p) are_LinDep & not are_Prop (u,p) & not are_Prop (v,p) by A2, A18, Th3, Th10;

        hence thesis by A1, A19, Th2;

      end;

      now

        assume

         A20: are_Prop (u,v);

        then

         A21: not are_Prop (u,q) implies not q is zero & (u,v,q) are_LinDep & not are_Prop (u,q) & not are_Prop (v,q) by A3, Th2, Th11;

         not are_Prop (u,p) implies not p is zero & (u,v,p) are_LinDep & not are_Prop (u,p) & not are_Prop (v,p) by A2, A20, Th2, Th11;

        hence thesis by A1, A21, Th2;

      end;

      hence thesis by A8, A4, A16;

    end;

    

     Lm8: not (p,q,r) are_LinDep implies for u, v st not u is zero & not v is zero & not are_Prop (u,v) holds ex y st not (u,v,y) are_LinDep

    proof

      assume

       A1: not (p,q,r) are_LinDep ;

      let u, v;

      assume

       A2: not u is zero & not v is zero & not are_Prop (u,v);

      assume

       A3: not thesis;

      then

       A4: (u,v,r) are_LinDep ;

      (u,v,p) are_LinDep & (u,v,q) are_LinDep by A3;

      hence contradiction by A1, A2, A4, Th14;

    end;

    theorem :: ANPROJ_1:17

     not (p,q,r) are_LinDep implies for u, v st not u is zero & not v is zero & not are_Prop (u,v) holds ex y st not y is zero & not (u,v,y) are_LinDep

    proof

      assume

       A1: not (p,q,r) are_LinDep ;

      let u, v;

      assume not u is zero & not v is zero & not are_Prop (u,v);

      then

      consider y such that

       A2: not (u,v,y) are_LinDep by A1, Lm8;

      take y;

      thus not y is zero by A2, Th12;

      thus thesis by A2;

    end;

    

     Lm9: for A,B,C be Real holds (((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y)))) = (((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y))

    proof

      let A,B,C be Real;

      

       A1: (C * ((e * u) + (f * y))) = (((C * e) * u) + ((C * f) * y)) by Lm7;

      (A * ((a * u) + (b * w))) = (((A * a) * u) + ((A * b) * w)) & (B * ((c * w) + (d * y))) = (((B * c) * w) + ((B * d) * y)) by Lm7;

      

      hence (((A * ((a * u) + (b * w))) + (B * ((c * w) + (d * y)))) + (C * ((e * u) + (f * y)))) = ((((((A * a) * u) + ((A * b) * w)) + ((B * c) * w)) + ((B * d) * y)) + (((C * e) * u) + ((C * f) * y))) by A1, RLVECT_1:def 3

      .= (((((A * a) * u) + (((A * b) * w) + ((B * c) * w))) + ((B * d) * y)) + (((C * e) * u) + ((C * f) * y))) by RLVECT_1:def 3

      .= (((((A * a) * u) + (((A * b) + (B * c)) * w)) + ((B * d) * y)) + (((C * e) * u) + ((C * f) * y))) by RLVECT_1:def 6

      .= ((((A * a) * u) + (((A * b) + (B * c)) * w)) + (((B * d) * y) + (((C * f) * y) + ((C * e) * u)))) by RLVECT_1:def 3

      .= ((((A * a) * u) + (((A * b) + (B * c)) * w)) + ((((B * d) * y) + ((C * f) * y)) + ((C * e) * u))) by RLVECT_1:def 3

      .= ((((A * a) * u) + (((A * b) + (B * c)) * w)) + ((((B * d) + (C * f)) * y) + ((C * e) * u))) by RLVECT_1:def 6

      .= (((A * a) * u) + ((((A * b) + (B * c)) * w) + ((((B * d) + (C * f)) * y) + ((C * e) * u)))) by RLVECT_1:def 3

      .= (((A * a) * u) + (((C * e) * u) + ((((A * b) + (B * c)) * w) + (((B * d) + (C * f)) * y)))) by RLVECT_1:def 3

      .= ((((A * a) * u) + ((C * e) * u)) + ((((A * b) + (B * c)) * w) + (((B * d) + (C * f)) * y))) by RLVECT_1:def 3

      .= ((((A * a) + (C * e)) * u) + ((((A * b) + (B * c)) * w) + (((B * d) + (C * f)) * y))) by RLVECT_1:def 6

      .= (((((A * a) + (C * e)) * u) + (((A * b) + (B * c)) * w)) + (((B * d) + (C * f)) * y)) by RLVECT_1:def 3;

    end;

    theorem :: ANPROJ_1:18

    (u,v,q) are_LinDep & (w,y,q) are_LinDep & (u,w,p) are_LinDep & (v,y,p) are_LinDep & (u,y,r) are_LinDep & (v,w,r) are_LinDep & (p,q,r) are_LinDep & not p is zero & not q is zero & not r is zero implies ((u,v,y) are_LinDep or (u,v,w) are_LinDep or (u,w,y) are_LinDep or (v,w,y) are_LinDep )

    proof

      assume that

       A1: (u,v,q) are_LinDep and

       A2: (w,y,q) are_LinDep and

       A3: (u,w,p) are_LinDep and

       A4: (v,y,p) are_LinDep and

       A5: (u,y,r) are_LinDep and

       A6: (v,w,r) are_LinDep and

       A7: (p,q,r) are_LinDep and

       A8: not p is zero and

       A9: not q is zero and

       A10: not r is zero;

      assume

       A11: not thesis;

      then

       A12: not v is zero by Th12;

      

       A13: not w is zero by A11, Th12;

      

       A14: not y is zero by A11, Th12;

      

       A15: not u is zero by A11, Th12;

       not are_Prop (v,y) by A11, Th12;

      then

      consider a19,b19 be Real such that

       A16: p = ((a19 * v) + (b19 * y)) by A4, A12, A14, Th6;

       not are_Prop (u,v) by A11, Th12;

      then

      consider a2, b2 such that

       A17: q = ((a2 * u) + (b2 * v)) by A1, A15, A12, Th6;

       not are_Prop (v,w) by A11, Th12;

      then

      consider a39,b39 be Real such that

       A18: r = ((a39 * v) + (b39 * w)) by A6, A12, A13, Th6;

       not are_Prop (u,w) by A11, Th12;

      then

      consider a1, b1 such that

       A19: p = ((a1 * u) + (b1 * w)) by A3, A15, A13, Th6;

       not are_Prop (w,y) by A11, Th12;

      then

      consider a29,b29 be Real such that

       A20: q = ((a29 * w) + (b29 * y)) by A2, A13, A14, Th6;

       not are_Prop (y,u) by A11, Th12;

      then

      consider a3, b3 such that

       A21: r = ((a3 * u) + (b3 * y)) by A5, A15, A14, Th6;

      consider A,B,C be Real such that

       A22: (((A * p) + (B * q)) + (C * r)) = ( 0. V) and

       A23: A <> 0 or B <> 0 or C <> 0 by A7;

      

       A24: ( 0. V) = (((((A * a1) + (C * a3)) * u) + (((A * b1) + (B * a29)) * w)) + (((B * b29) + (C * b3)) * y)) by A19, A20, A21, A22, Lm9;

      then

       A25: ((A * a1) + (C * a3)) = 0 by A11;

      

       A26: ( 0. V) = (((C * ((a39 * v) + (b39 * w))) + (B * ((a29 * w) + (b29 * y)))) + (A * ((a19 * v) + (b19 * y)))) by A16, A20, A18, A22, RLVECT_1:def 3

      .= (((((C * a39) + (A * a19)) * v) + (((C * b39) + (B * a29)) * w)) + (((B * b29) + (A * b19)) * y)) by Lm9;

      then

       A27: ((C * a39) + (A * a19)) = 0 by A11;

      

       A28: ( 0. V) = (((((B * a2) + (C * a3)) * u) + (((B * b2) + (A * a19)) * v)) + (((A * b19) + (C * b3)) * y)) by A16, A17, A21, A22, Lm9;

      then

       A29: ((B * a2) + (C * a3)) = 0 by A11;

      

       A30: ( 0. V) = (((((B * a2) + (A * a1)) * u) + (((B * b2) + (C * a39)) * v)) + (((C * b39) + (A * b1)) * w)) by A19, A17, A18, A22, Lm9;

      then

       A31: ((B * a2) + (A * a1)) = 0 by A11;

      

       A32: ((C * b39) + (B * a29)) = 0 by A11, A26;

      

       A33: ((C * b39) + (A * b1)) = 0 by A11, A30;

      

       A34: ((B * b29) + (A * b19)) = 0 by A11, A26;

      

       A35: ((A * b19) + (C * b3)) = 0 by A11, A28;

      

       A36: ((B * b29) + (C * b3)) = 0 by A11, A24;

       A37:

      now

        assume

         A38: C <> 0 ;

        then a3 = 0 by A25, A29, A31, XCMPLX_1: 6;

        

        then r = (( 0 * u) + ( 0 * y)) by A21, A36, A35, A34, A38, XCMPLX_1: 6

        .= (( 0. V) + ( 0 * y)) by RLVECT_1: 10

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

        .= ( 0. V);

        hence contradiction by A10;

      end;

      

       A39: ((B * b2) + (C * a39)) = 0 by A11, A30;

      

       A40: ((B * b2) + (A * a19)) = 0 by A11, A28;

       A41:

      now

        assume

         A42: B <> 0 ;

        then a2 = 0 by A25, A29, A31, XCMPLX_1: 6;

        

        then q = (( 0 * u) + ( 0 * v)) by A17, A40, A39, A27, A42, XCMPLX_1: 6

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

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

        .= ( 0. V);

        hence contradiction by A9;

      end;

      

       A43: ((A * b1) + (B * a29)) = 0 by A11, A24;

      now

        assume

         A44: A <> 0 ;

        then a1 = 0 by A25, A29, A31, XCMPLX_1: 6;

        

        then p = (( 0 * u) + ( 0 * w)) by A19, A43, A33, A32, A44, XCMPLX_1: 6

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

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

        .= ( 0. V);

        hence contradiction by A8;

      end;

      hence thesis by A23, A41, A37;

    end;

    reserve x,y,z for object;

    definition

      let V;

      :: ANPROJ_1:def3

      func Proportionality_as_EqRel_of V -> Equivalence_Relation of ( NonZero V) means

      : Def3: for x, y holds [x, y] in it iff (x in ( NonZero V) & y in ( NonZero V) & ex u,v be Element of V st x = u & y = v & are_Prop (u,v));

      existence

      proof

        defpred P[ object, object] means ex u,v be Element of V st $1 = u & $2 = v & are_Prop (u,v);

        

         A1: for x be object st x in ( NonZero V) holds P[x, x];

        

         A2: for x,y be object st P[x, y] holds P[y, x];

        

         A3: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z] by Th2;

        consider R be Equivalence_Relation of ( NonZero V) such that

         A4: for x,y be object holds [x, y] in R iff x in ( NonZero V) & y in ( NonZero V) & P[x, y] from EQREL_1:sch 1( A1, A2, A3);

        take R;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let R1,R2 be Equivalence_Relation of ( NonZero V) such that

         A5: for x, y holds [x, y] in R1 iff (x in ( NonZero V) & y in ( NonZero V) & ex u,v be Element of V st x = u & y = v & are_Prop (u,v)) and

         A6: for x, y holds [x, y] in R2 iff (x in ( NonZero V) & y in ( NonZero V) & ex u,v be Element of V st x = u & y = v & are_Prop (u,v));

        for x,y be object holds ( [x, y] in R1 iff [x, y] in R2)

        proof

          let x,y be object;

           A7:

          now

            assume

             A8: [x, y] in R2;

            then

             A9: ex u,v be Element of V st x = u & y = v & are_Prop (u,v) by A6;

            x in ( NonZero V) & y in ( NonZero V) by A6, A8;

            hence [x, y] in R1 by A5, A9;

          end;

          now

            assume

             A10: [x, y] in R1;

            then

             A11: ex u,v be Element of V st x = u & y = v & are_Prop (u,v) by A5;

            x in ( NonZero V) & y in ( NonZero V) by A5, A10;

            hence [x, y] in R2 by A6, A11;

          end;

          hence thesis by A7;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    theorem :: ANPROJ_1:19

     [x, y] in ( Proportionality_as_EqRel_of V) implies x is Element of V & y is Element of V

    proof

      assume [x, y] in ( Proportionality_as_EqRel_of V);

      then ex u, v st x = u & y = v & are_Prop (u,v) by Def3;

      then

      reconsider x, y as Element of V;

      x is Element of V & y is Element of V;

      hence thesis;

    end;

    theorem :: ANPROJ_1:20

    

     Th20: [u, v] in ( Proportionality_as_EqRel_of V) iff not u is zero & not v is zero & are_Prop (u,v)

    proof

       A1:

      now

        assume

         A2: [u, v] in ( Proportionality_as_EqRel_of V);

        then u in ( NonZero V) & v in ( NonZero V) by Def3;

        hence not u is zero & not v is zero by STRUCT_0: 1;

        ex u1, v1 st u = u1 & v = v1 & are_Prop (u1,v1) by A2, Def3;

        hence are_Prop (u,v);

      end;

      now

        assume that

         A3: not u is zero & not v is zero and

         A4: are_Prop (u,v);

        u in ( NonZero V) & v in ( NonZero V) by A3, STRUCT_0: 1;

        hence [u, v] in ( Proportionality_as_EqRel_of V) by A4, Def3;

      end;

      hence thesis by A1;

    end;

    definition

      let V;

      let v;

      :: ANPROJ_1:def4

      func Dir (v) -> Subset of ( NonZero V) equals ( Class (( Proportionality_as_EqRel_of V),v));

      correctness ;

    end

    definition

      let V;

      :: ANPROJ_1:def5

      func ProjectivePoints (V) -> set means

      : Def5: ex Y be Subset-Family of ( NonZero V) st Y = ( Class ( Proportionality_as_EqRel_of V)) & it = Y;

      correctness ;

    end

    registration

      cluster strict non trivial for RealLinearSpace;

      existence

      proof

        consider V be strict RealLinearSpace such that

         A1: ex u,v be Element of V st (for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) & for w be Element of V holds ex a, b st w = ((a * u) + (b * v)) by FUNCSDOM: 23;

        consider u,v be Element of V such that

         A2: for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 and for w be Element of V holds ex a, b st w = ((a * u) + (b * v)) by A1;

        u <> ( 0. V)

        proof

          assume

           A3: u = ( 0. V);

          ( 0. V) = (( 0. V) + ( 0. V))

          .= ((1 * u) + ( 0. V)) by A3

          .= ((1 * u) + ( 0 * v)) by RLVECT_1: 10;

          hence contradiction by A2;

        end;

        then V is non trivial;

        hence thesis;

      end;

    end

    reserve V for non trivial RealLinearSpace;

    reserve p,q,r,u,v,w for Element of V;

    registration

      let V;

      cluster ( ProjectivePoints V) -> non empty;

      coherence

      proof

        consider u be Element of V such that

         A1: u <> ( 0. V) by STRUCT_0:def 18;

        set Y = ( Dir u);

        consider Z be Subset-Family of ( NonZero V) such that

         A2: Z = ( Class ( Proportionality_as_EqRel_of V)) and

         A3: ( ProjectivePoints V) = Z by Def5;

        u in ( NonZero V) by A1, ZFMISC_1: 56;

        then Y in Z by A2, EQREL_1:def 3;

        hence thesis by A3;

      end;

    end

    theorem :: ANPROJ_1:21

    

     Th21: not p is zero implies ( Dir p) is Element of ( ProjectivePoints V)

    proof

      assume not p is zero;

      then p in ( NonZero V) by STRUCT_0: 1;

      then ( Dir p) in ( Class ( Proportionality_as_EqRel_of V)) by EQREL_1:def 3;

      hence thesis by Def5;

    end;

    theorem :: ANPROJ_1:22

    

     Th22: not p is zero & not q is zero implies (( Dir p) = ( Dir q) iff are_Prop (p,q))

    proof

      assume that

       A1: not p is zero and

       A2: not q is zero;

      

       A3: p in ( NonZero V) by A1, STRUCT_0: 1;

       A4:

      now

        assume ( Dir p) = ( Dir q);

        then [p, q] in ( Proportionality_as_EqRel_of V) by A3, EQREL_1: 35;

        hence are_Prop (p,q) by Th20;

      end;

      now

        assume are_Prop (p,q);

        then [p, q] in ( Proportionality_as_EqRel_of V) by A1, A2, Th20;

        hence ( Dir p) = ( Dir q) by A3, EQREL_1: 35;

      end;

      hence thesis by A4;

    end;

    definition

      let V;

      :: ANPROJ_1:def6

      func ProjectiveCollinearity (V) -> Relation3 of ( ProjectivePoints V) means

      : Def6: for x,y,z be object holds ( [x, y, z] in it iff ex p, q, r st x = ( Dir p) & y = ( Dir q) & z = ( Dir r) & not p is zero & not q is zero & not r is zero & (p,q,r) are_LinDep );

      existence

      proof

        defpred P[ object] means ex p, q, r st $1 = [( Dir p), ( Dir q), ( Dir r)] & not p is zero & not q is zero & not r is zero & (p,q,r) are_LinDep ;

        set D = ( ProjectivePoints V), XXX = [:D, D, D:];

        consider R be set such that

         A1: for xyz be object holds (xyz in R iff xyz in XXX & P[xyz]) from XBOOLE_0:sch 1;

        for x be object holds x in R implies x in XXX by A1;

        then R c= XXX by TARSKI:def 3;

        then

        reconsider R9 = R as Relation3 of D by COLLSP:def 1;

        take R9;

        let x,y,z be object;

         A2:

        now

          set xyz = [x, y, z];

          given p, q, r such that

           A3: x = ( Dir p) & y = ( Dir q) & z = ( Dir r) and

           A4: not p is zero & not q is zero and

           A5: not r is zero and

           A6: (p,q,r) are_LinDep ;

          

           A7: ( Dir r) is Element of D by A5, Th21;

          ( Dir p) is Element of D & ( Dir q) is Element of D by A4, Th21;

          then xyz in XXX by A3, A7, MCART_1: 69;

          hence xyz in R9 by A1, A3, A4, A5, A6;

        end;

        now

          assume [x, y, z] in R9;

          then

          consider p, q, r such that

           A8: [x, y, z] = [( Dir p), ( Dir q), ( Dir r)] and

           A9: not p is zero & not q is zero & not r is zero & (p,q,r) are_LinDep by A1;

          

           A10: z = ( Dir r) by A8, XTUPLE_0: 3;

          x = ( Dir p) & y = ( Dir q) by A8, XTUPLE_0: 3;

          hence ex p, q, r st x = ( Dir p) & y = ( Dir q) & z = ( Dir r) & not p is zero & not q is zero & not r is zero & (p,q,r) are_LinDep by A9, A10;

        end;

        hence thesis by A2;

      end;

      uniqueness

      proof

        set X = ( ProjectivePoints V), XXX = [:( ProjectivePoints V), ( ProjectivePoints V), ( ProjectivePoints V):];

        let R1,R2 be Relation3 of ( ProjectivePoints V) such that

         A11: for x,y,z be object holds ( [x, y, z] in R1 iff ex p, q, r st x = ( Dir p) & y = ( Dir q) & z = ( Dir r) & not p is zero & not q is zero & not r is zero & (p,q,r) are_LinDep ) and

         A12: for x,y,z be object holds ( [x, y, z] in R2 iff ex p, q, r st x = ( Dir p) & y = ( Dir q) & z = ( Dir r) & not p is zero & not q is zero & not r is zero & (p,q,r) are_LinDep );

        

         A13: R2 c= XXX by COLLSP:def 1;

        

         A14: R1 c= XXX by COLLSP:def 1;

        now

          let u be object;

           A15:

          now

            assume

             A16: u in R2;

            then

            consider x,y,z be Element of X such that

             A17: u = [x, y, z] by A13, DOMAIN_1: 3;

            ex p, q, r st x = ( Dir p) & y = ( Dir q) & z = ( Dir r) & not p is zero & not q is zero & not r is zero & (p,q,r) are_LinDep by A12, A16, A17;

            hence u in R1 by A11, A17;

          end;

          now

            assume

             A18: u in R1;

            then

            consider x,y,z be Element of X such that

             A19: u = [x, y, z] by A14, DOMAIN_1: 3;

            ex p, q, r st x = ( Dir p) & y = ( Dir q) & z = ( Dir r) & not p is zero & not q is zero & not r is zero & (p,q,r) are_LinDep by A11, A18, A19;

            hence u in R2 by A12, A19;

          end;

          hence u in R1 iff u in R2 by A15;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let V;

      :: ANPROJ_1:def7

      func ProjectiveSpace (V) -> strict CollStr equals CollStr (# ( ProjectivePoints V), ( ProjectiveCollinearity V) #);

      correctness ;

    end

    registration

      let V;

      cluster ( ProjectiveSpace V) -> non empty;

      coherence ;

    end

    theorem :: ANPROJ_1:23

    for V holds the carrier of ( ProjectiveSpace V) = ( ProjectivePoints V) & the Collinearity of ( ProjectiveSpace V) = ( ProjectiveCollinearity V);

    theorem :: ANPROJ_1:24

     [x, y, z] in the Collinearity of ( ProjectiveSpace V) implies ex p, q, r st x = ( Dir p) & y = ( Dir q) & z = ( Dir r) & not p is zero & not q is zero & not r is zero & (p,q,r) are_LinDep by Def6;

    theorem :: ANPROJ_1:25

     not u is zero & not v is zero & not w is zero implies ( [( Dir u), ( Dir v), ( Dir w)] in the Collinearity of ( ProjectiveSpace V) iff (u,v,w) are_LinDep )

    proof

      assume that

       A1: not u is zero & not v is zero and

       A2: not w is zero;

      now

        reconsider du = ( Dir u), dv = ( Dir v), dw = ( Dir w) as set;

        assume [( Dir u), ( Dir v), ( Dir w)] in the Collinearity of ( ProjectiveSpace V);

        then

        consider p, q, r such that

         A3: du = ( Dir p) & dv = ( Dir q) and

         A4: dw = ( Dir r) and

         A5: not p is zero & not q is zero and

         A6: not r is zero and

         A7: (p,q,r) are_LinDep by Def6;

        

         A8: are_Prop (r,w) by A2, A4, A6, Th22;

         are_Prop (p,u) & are_Prop (q,v) by A1, A3, A5, Th22;

        hence (u,v,w) are_LinDep by A7, A8, Th4;

      end;

      hence thesis by A1, A2, Def6;

    end;

    theorem :: ANPROJ_1:26

    x is Element of ( ProjectiveSpace V) iff ex u st not u is zero & x = ( Dir u)

    proof

      now

        assume

         A1: x is Element of ( ProjectiveSpace V);

        

         A2: ex Y be Subset-Family of ( NonZero V) st Y = ( Class ( Proportionality_as_EqRel_of V)) & ( ProjectivePoints V) = Y by Def5;

        then

        reconsider x9 = x as Subset of ( NonZero V) by A1, TARSKI:def 3;

        consider y be object such that

         A3: y in ( NonZero V) and

         A4: x9 = ( Class (( Proportionality_as_EqRel_of V),y)) by A1, A2, EQREL_1:def 3;

        

         A5: y <> ( 0. V) by A3, ZFMISC_1: 56;

        reconsider y as Element of V by A3;

        take y;

        thus not y is zero by A5;

        thus x = ( Dir y) by A4;

      end;

      hence thesis by Th21;

    end;