ortsp_1.miz

    begin

    reserve F for Field;

    reconsider X = { 0 } as non empty set;

    reconsider o = 0 as Element of X by TARSKI:def 1;

    deffunc F( Element of X, Element of X) = o;

    consider md be BinOp of X such that

     Lm1: for x,y be Element of X holds (md . (x,y)) = F(x,y) from BINOP_1:sch 4;

     Lm2:

    now

      defpred P[ object] means ex a,b be Element of X st $1 = [a, b] & b = o;

      set CV = [:X, X:];

      let F;

      consider mo be set such that

       A1: for x be object holds x in mo iff x in CV & P[x] from XBOOLE_0:sch 1;

      mo c= CV by A1;

      then

      reconsider mo as Relation of X;

      take mo;

      thus for x be set holds x in mo iff x in CV & ex a,b be Element of X st x = [a, b] & b = o by A1;

    end;



     Lm3: for mF be Function of [:the carrier of F, X:], X, mo be Relation of X holds SymStr (# X, md, o, mF, mo #) is Abelian add-associative right_zeroed right_complementable

    proof

      let mF be Function of [:the carrier of F, X:], X;

      let mo be Relation of X;

      set H = SymStr (# X, md, o, mF, mo #);



       A1: for x be Element of H holds (x + ( 0. H)) = x

      proof

        let x be Element of H;

        (md . (x,( 0. H))) = o by Lm1;

        hence thesis by TARSKI:def 1;

      end;



       A2: H is right_complementable

      proof

        let x be Element of H;

        take ( - x);

        ( 0. H) = o by STRUCT_0:def 6;

        hence thesis by Lm1;

      end;



       A3: for x,y,z be Element of H holds ((x + y) + z) = (x + (y + z))

      proof

        let x,y,z be Element of H;

        reconsider x, y, z as Element of X;

        (md . (x,(md . (y,z)))) = o by Lm1;

        hence thesis by Lm1;

      end;

      for x,y be Element of H holds (x + y) = (y + x)

      proof

        let x,y be Element of H;

        (md . (x,y)) = o by Lm1;

        hence thesis by Lm1;

      end;

      hence thesis by A3, A1, A2, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

    end;

     Lm4:

    now

      let F;

      let mF be Function of [:the carrier of F, X:], X such that

       A1: for a be Element of F holds for x be Element of X holds (mF . [a, x qua set]) = o;

      let mo be Relation of X;

      let MPS be Abelian add-associative right_zeroed right_complementable non empty SymStr over F such that

       A2: MPS = SymStr (# X, md, o, mF, mo #);

      for x,y be Element of F holds for v,w be Element of MPS holds (x * (v + w)) = ((x * v) + (x * w)) & ((x + y) * v) = ((x * v) + (y * v)) & ((x * y) * v) = (x * (y * v)) & (( 1_ F) * v) = v

      proof

        let x,y be Element of F;

        let v,w be Element of MPS;



         A3: ((x * y) * v) = (x * (y * v))

        proof

          set z = (x * y);



           A4: (z * v) = (mF . (z,v)) by A2, VECTSP_1:def 12;

          reconsider v as Element of MPS;

          reconsider v as Element of MPS;



           A5: ((x * y) * v) = o by A1, A2, A4;

          reconsider v as Element of MPS;



           A6: (mF . (y,v qua set)) = o by A1, A2;

          reconsider v as Element of MPS;

          (y * v) = o by A2, A6, VECTSP_1:def 12;

          then (x * (y * v)) = (mF . (x,o)) by A2, VECTSP_1:def 12;

          hence thesis by A1, A5;

        end;



         A7: (x * (v + w)) = ((x * v) + (x * w))

        proof

          reconsider v, w as Element of MPS;



           A8: o = ( 0. MPS) by A2, STRUCT_0:def 6;

          reconsider v, w as Element of X by A2;



           A9: (md . (v,w)) = o by Lm1;

          reconsider v, w as Element of MPS;

          (x * (v + w)) = (mF . (x,o)) by A2, A9, VECTSP_1:def 12;

          then

           A10: (x * (v + w)) = o by A1;

          reconsider w as Element of MPS;

          reconsider v as Element of MPS;



           A11: (mF . (x,v qua set)) = o by A1;

          reconsider v as Element of MPS;



           A12: (mF . (x,w qua set)) = o by A1;

          reconsider w as Element of MPS;



           A13: (x * w) = o by A2, A12, VECTSP_1:def 12;

          (x * v) = o by A2, A11, VECTSP_1:def 12;

          hence thesis by A10, A13, A8, RLVECT_1: 4;

        end;



         A14: ((x + y) * v) = ((x * v) + (y * v))

        proof

          set z = (x + y);



           A15: (z * v) = (mF . (z,v)) by A2, VECTSP_1:def 12;

          reconsider v as Element of MPS;

          reconsider v as Element of MPS;



           A16: ((x + y) * v) = o by A1, A2, A15;

          reconsider v as Element of MPS;



           A17: (mF . (x,v qua set)) = o by A1, A2;

          reconsider v as Element of MPS;



           A18: (x * v) = o by A2, A17, VECTSP_1:def 12;

          reconsider v as Element of MPS;



           A19: (mF . (y,v qua set)) = o by A1, A2;



           A20: o = ( 0. MPS) by A2, STRUCT_0:def 6;

          reconsider v as Element of MPS;

          (y * v) = o by A2, A19, VECTSP_1:def 12;

          hence thesis by A16, A18, A20, RLVECT_1: 4;

        end;

        (( 1_ F) * v) = v

        proof

          set one1 = ( 1_ F);



           A21: (one1 * v) = (mF . (one1,v)) by A2, VECTSP_1:def 12;

          reconsider v as Element of MPS;

          (mF . (one1,v qua set)) = o by A1, A2;

          hence thesis by A2, A21, TARSKI:def 1;

        end;

        hence thesis by A7, A14, A3;

      end;

      hence MPS is vector-distributive scalar-distributive scalar-associative scalar-unital by VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;

    end;

     Lm5:

    now

      set CV = [:X, X:];

      let F;

      let mF be Function of [:the carrier of F, X:], X;

      let mo be Relation of X such that

       A1: for x be set holds x in mo iff x in CV & ex a,b be Element of X st x = [a, b] & b = o;

      let MPS be Abelian add-associative right_zeroed right_complementable non empty SymStr over F such that

       A2: MPS = SymStr (# X, md, o, mF, mo #);

      ( 0. MPS) = o by A2, TARSKI:def 1;

      hence for a,b,c,d be Element of MPS holds (a <> ( 0. MPS) & b <> ( 0. MPS) & c <> ( 0. MPS) & d <> ( 0. MPS) implies ex p be Element of MPS st not p _|_ a & not p _|_ b & not p _|_ c & not p _|_ d) by A2, TARSKI:def 1;



       A3: for a,b be Element of MPS holds a _|_ b iff [a, b] in CV & ex c,d be Element of X st [a, b] = [c, d] & d = o

      proof

        let a,b be Element of MPS;

        a _|_ b iff [a, b] in mo by A2, ORDERS_2:def 5;

        hence thesis by A1;

      end;



       A4: for a,b be Element of MPS holds a _|_ b iff b = o

      proof

        let a,b be Element of MPS;



         A5: b = o implies a _|_ b

        proof

          consider c,d be Element of MPS such that

           A6: c = a & d = b;

          assume

           A7: b = o;

           [a, b] = [c, d] by A6;

          hence thesis by A2, A3, A7;

        end;

        a _|_ b implies b = o

        proof

          assume a _|_ b;

          then ex c,d be Element of X st [a, b] = [c, d] & d = o by A3;

          hence thesis by XTUPLE_0: 1;

        end;

        hence thesis by A5;

      end;

      thus for a,b be Element of MPS holds for l be Element of F holds (a _|_ b implies (l * a) _|_ b)

      proof

        let a,b be Element of MPS;

        let l be Element of F;

        assume a _|_ b;

        then b = o by A4;

        hence thesis by A4;

      end;

      thus for a,b,c be Element of MPS holds (b _|_ a & c _|_ a implies (b + c) _|_ a)

      proof

        let a,b,c be Element of MPS;

        assume that

         A8: b _|_ a and c _|_ a;

        a = o by A4, A8;

        hence thesis by A4;

      end;

      thus for a,b,x be Element of MPS holds ( not b _|_ a implies ex k be Element of F st (x - (k * b)) _|_ a)

      proof

        let a,b,x be Element of MPS;

        assume

         A9: not b _|_ a;

        assume not thesis;

        a <> o by A4, A9;

        hence contradiction by A2, TARSKI:def 1;

      end;

      thus for a,b,c be Element of MPS holds (a _|_ (b - c) & b _|_ (c - a) implies c _|_ (a - b))

      proof

        let a,b,c be Element of MPS;

        assume that a _|_ (b - c) and b _|_ (c - a);

        assume not thesis;

        then (a - b) <> o by A4;

        hence contradiction by A2, TARSKI:def 1;

      end;

    end;

    definition

      let F;

      let IT be Abelian add-associative right_zeroed right_complementable non empty SymStr over F;

      :: ORTSP_1:def1

      attr IT is OrtSp-like means

      : Def1: for a,b,c,d,x be Element of IT holds for l be Element of F holds (a <> ( 0. IT) & b <> ( 0. IT) & c <> ( 0. IT) & d <> ( 0. IT) implies ex p be Element of IT st not p _|_ a & not p _|_ b & not p _|_ c & not p _|_ d) & (a _|_ b implies (l * a) _|_ b) & (b _|_ a & c _|_ a implies (b + c) _|_ a) & ( not b _|_ a implies ex k be Element of F st (x - (k * b)) _|_ a) & (a _|_ (b - c) & b _|_ (c - a) implies c _|_ (a - b));

    end

    registration

      let F;

      cluster OrtSp-like vector-distributive scalar-distributive scalar-associative scalar-unital strict for Abelian add-associative right_zeroed right_complementable non empty SymStr over F;

      existence

      proof

        reconsider mF = ( [:the carrier of F, X:] --> o) as Function of [:the carrier of F, X:], X;

        consider mo be Relation of X such that

         A1: for x be set holds x in mo iff x in [:X, X:] & ex a,b be Element of X st x = [a, b] & b = o by Lm2;

        reconsider MPS = SymStr (# X, md, o, mF, mo #) as Abelian add-associative right_zeroed right_complementable non empty SymStr over F by Lm3;

        take MPS;

        thus for a,b,c,d,x be Element of MPS holds for l be Element of F holds (a <> ( 0. MPS) & b <> ( 0. MPS) & c <> ( 0. MPS) & d <> ( 0. MPS) implies ex p be Element of MPS st not p _|_ a & not p _|_ b & not p _|_ c & not p _|_ d) & (a _|_ b implies (l * a) _|_ b) & (b _|_ a & c _|_ a implies (b + c) _|_ a) & ( not b _|_ a implies ex k be Element of F st (x - (k * b)) _|_ a) & (a _|_ (b - c) & b _|_ (c - a) implies c _|_ (a - b)) by A1, Lm5;

        for a be Element of F holds for x be Element of X holds (mF . [a, x]) = o by FUNCOP_1: 7;

        hence MPS is vector-distributive scalar-distributive scalar-associative scalar-unital by Lm4;

        thus thesis;

      end;

    end

    definition

      let F;

      mode OrtSp of F is OrtSp-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty SymStr over F;

    end

    reserve S for OrtSp of F;

    reserve a,b,c,d,p,q,r,x,y,z for Element of S;

    reserve k,l for Element of F;

    theorem :: ORTSP_1:1



     Th1: ( 0. S) _|_ a

    proof

      set 0F = ( 0. F), 0V = ( 0. S);

       A1:

      now

        assume not a _|_ a;

        then

        consider m be Element of F such that

         A2: (0V - (m * a)) _|_ a by Def1;

        (0F * (0V - (m * a))) _|_ a by A2, Def1;

        hence thesis by VECTSP_1: 14;

      end;

      now

        assume a _|_ a;

        then (0F * a) _|_ a by Def1;

        hence thesis by VECTSP_1: 14;

      end;

      hence thesis by A1;

    end;

    theorem :: ORTSP_1:2



     Th2: a _|_ b implies b _|_ a

    proof

      set 0V = ( 0. S);

      assume a _|_ b;

      then a _|_ ( - ( - b)) by RLVECT_1: 17;

      then

       A1: a _|_ (0V - ( - b)) by RLVECT_1: 4;

      0V _|_ (( - b) - a) by Th1;

      then ( - b) _|_ (a - 0V) by A1, Def1;

      then ( - b) _|_ a by VECTSP_1: 18;

      then (( - ( 1_ F)) * ( - b)) _|_ a by Def1;

      then ( - ( - b)) _|_ a by VECTSP_1: 14;

      hence thesis by RLVECT_1: 17;

    end;

    theorem :: ORTSP_1:3



     Th3: not a _|_ b & (c + a) _|_ b implies not c _|_ b

    proof

      assume that

       A1: not a _|_ b and

       A2: (c + a) _|_ b;

      assume not thesis;

      then (( - ( 1_ F)) * c) _|_ b by Def1;

      then ( - c) _|_ b by VECTSP_1: 14;

      then (( - c) + (c + a)) _|_ b by A2, Def1;

      then ((c + ( - c)) + a) _|_ b by RLVECT_1:def 3;

      then (( 0. S) + a) _|_ b by RLVECT_1: 5;

      hence contradiction by A1, RLVECT_1: 4;

    end;

    theorem :: ORTSP_1:4



     Th4: not b _|_ a & c _|_ a implies not (b + c) _|_ a

    proof

      assume that

       A1: not b _|_ a and

       A2: c _|_ a;

      (( - ( 1_ F)) * c) _|_ a by A2, Def1;

      then

       A3: ( - c) _|_ a by VECTSP_1: 14;

      assume not thesis;

      then ((b + c) + ( - c)) _|_ a by A3, Def1;

      then (b + (c + ( - c))) _|_ a by RLVECT_1:def 3;

      then (b + ( 0. S)) _|_ a by RLVECT_1: 5;

      hence contradiction by A1, RLVECT_1: 4;

    end;

    theorem :: ORTSP_1:5



     Th5: not b _|_ a & not l = ( 0. F) implies not (l * b) _|_ a & not b _|_ (l * a)

    proof

      set 1F = ( 1_ F);

      assume that

       A1: not b _|_ a and

       A2: not l = ( 0. F);

       A3:

      now

        consider k such that

         A4: (k * l) = 1F by A2, VECTSP_1:def 9;

        assume b _|_ (l * a);

        then (l * a) _|_ b by Th2;

        then (k * (l * a)) _|_ b by Def1;

        then (1F * a) _|_ b by A4, VECTSP_1:def 16;

        then a _|_ b by VECTSP_1:def 17;

        hence contradiction by A1, Th2;

      end;

      now

        consider k such that

         A5: (k * l) = 1F by A2, VECTSP_1:def 9;

        assume (l * b) _|_ a;

        then (k * (l * b)) _|_ a by Def1;

        then (1F * b) _|_ a by A5, VECTSP_1:def 16;

        hence contradiction by A1, VECTSP_1:def 17;

      end;

      hence thesis by A3;

    end;

    theorem :: ORTSP_1:6



     Th6: a _|_ b implies ( - a) _|_ b

    proof

      assume a _|_ b;

      then (( - ( 1_ F)) * a) _|_ b by Def1;

      hence thesis by VECTSP_1: 14;

    end;

    theorem :: ORTSP_1:7



     Th7: (a - b) _|_ d & (a - c) _|_ d implies (b - c) _|_ d

    proof

      assume that

       A1: (a - b) _|_ d and

       A2: (a - c) _|_ d;

      ( - (a - b)) _|_ d by A1, Th6;

      then (( - a) + b) _|_ d by VECTSP_1: 17;

      then ((b + ( - a)) + (a - c)) _|_ d by A2, Def1;

      then (b + (( - a) + (a + ( - c)))) _|_ d by RLVECT_1:def 3;

      then (b + ((( - a) + a) + ( - c))) _|_ d by RLVECT_1:def 3;

      then (b + (( 0. S) + ( - c))) _|_ d by RLVECT_1: 5;

      hence thesis by RLVECT_1: 4;

    end;

    theorem :: ORTSP_1:8



     Th8: not b _|_ a & (x - (k * b)) _|_ a & (x - (l * b)) _|_ a implies k = l

    proof

      set 1F = ( 1_ F);

      assume that

       A1: not b _|_ a and

       A2: (x - (k * b)) _|_ a & (x - (l * b)) _|_ a;

      ((k * b) - (l * b)) _|_ a by A2, Th7;

      then ((k * b) + (( - 1F) * (l * b))) _|_ a by VECTSP_1: 14;

      then ((k * b) + ((( - 1F) * l) * b)) _|_ a by VECTSP_1:def 16;

      then ((k * b) + (( - (l * 1F)) * b)) _|_ a by VECTSP_1: 9;

      then ((k * b) + (( - l) * b)) _|_ a;

      then ((k + ( - l)) * b) _|_ a by VECTSP_1:def 15;

      then (((k + ( - l)) " ) * ((k + ( - l)) * b)) _|_ a by Def1;

      then

       A3: ((((k + ( - l)) " ) * (k + ( - l))) * b) _|_ a by VECTSP_1:def 16;

      assume not thesis;

      then (k - l) <> ( 0. F) by RLVECT_1: 21;

      then (1F * b) _|_ a by A3, VECTSP_1:def 10;

      hence contradiction by A1, VECTSP_1:def 17;

    end;

    theorem :: ORTSP_1:9



     Th9: a _|_ a & b _|_ b implies (a + b) _|_ (a - b)

    proof

      set 0V = ( 0. S);

      assume that

       A1: a _|_ a and

       A2: b _|_ b;

      (( - ( 1_ F)) * a) _|_ a by A1, Def1;

      then ( - a) _|_ a by VECTSP_1: 14;

      then a _|_ ( - a) by Th2;

      then a _|_ (0V + ( - a)) by RLVECT_1: 4;

      then a _|_ ((b + ( - b)) + ( - a)) by RLVECT_1: 5;

      then a _|_ (b + (( - b) - a)) by RLVECT_1:def 3;

      then

       A3: a _|_ (b - (a + b)) by VECTSP_1: 17;

      b _|_ (b + 0V) by A2, RLVECT_1: 4;

      then b _|_ (b + (a + ( - a))) by RLVECT_1: 5;

      then b _|_ ((a + b) - a) by RLVECT_1:def 3;

      hence thesis by A3, Def1;

    end;

    theorem :: ORTSP_1:10

    (( 1_ F) + ( 1_ F)) <> ( 0. F) & (ex a st a <> ( 0. S)) implies ex b st not b _|_ b

    proof

      set 1F = ( 1_ F), 0V = ( 0. S);

      assume that

       A1: (( 1_ F) + ( 1_ F)) <> ( 0. F) and

       A2: ex a st a <> ( 0. S);

      consider a such that

       A3: a <> ( 0. S) by A2;

      assume

       A4: not thesis;



       A5: for c, d holds c _|_ d

      proof

        let c, d;

        d _|_ d & c _|_ c by A4;

        then (d + c) _|_ (d - c) by Th9;

        then

         A6: (d - c) _|_ (d + c) by Th2;

        (d + c) _|_ (d + c) by A4;

        then ((d + c) + (( - c) + d)) _|_ (d + c) by A6, Def1;

        then (((d + c) + ( - c)) + d) _|_ (d + c) by RLVECT_1:def 3;

        then ((d + (c + ( - c))) + d) _|_ (d + c) by RLVECT_1:def 3;

        then ((d + 0V) + d) _|_ (d + c) by RLVECT_1: 5;

        then (d + d) _|_ (d + c) by RLVECT_1: 4;

        then ((1F * d) + d) _|_ (d + c) by VECTSP_1:def 17;

        then ((1F * d) + (1F * d)) _|_ (d + c) by VECTSP_1:def 17;

        then ((1F + 1F) * d) _|_ (d + c) by VECTSP_1:def 15;

        then (((1F + 1F) " ) * ((1F + 1F) * d)) _|_ (d + c) by Def1;

        then ((((1F + 1F) " ) * (1F + 1F)) * d) _|_ (d + c) by VECTSP_1:def 16;

        then (1F * d) _|_ (d + c) by A1, VECTSP_1:def 10;

        then d _|_ (d + c) by VECTSP_1:def 17;

        then

         A7: (d + c) _|_ d by Th2;

        ( - d) _|_ d by A4, Th6;

        then (( - d) + (d + c)) _|_ d by A7, Def1;

        then ((( - d) + d) + c) _|_ d by RLVECT_1:def 3;

        then (0V + c) _|_ d by RLVECT_1: 5;

        hence thesis by RLVECT_1: 4;

      end;

      ex c st not c _|_ a & not c _|_ a & not c _|_ a & not c _|_ a by A3, Def1;

      hence contradiction by A5;

    end;

    definition

      let F, S, a, b, x;

      assume

       A1: not b _|_ a;

      :: ORTSP_1:def2

      func ProJ (a,b,x) -> Element of F means

      : Def2: for l be Element of F st (x - (l * b)) _|_ a holds it = l;

      existence

      proof

        consider k be Element of F such that

         A2: (x - (k * b)) _|_ a by A1, Def1;

        take k;

        let l be Element of F;

        assume (x - (l * b)) _|_ a;

        hence thesis by A1, A2, Th8;

      end;

      uniqueness

      proof

        let l1,l2 be Element of F such that

         A3: for l be Element of F st (x - (l * b)) _|_ a holds l1 = l and

         A4: for l be Element of F st (x - (l * b)) _|_ a holds l2 = l;

        consider k be Element of F such that

         A5: (x - (k * b)) _|_ a by A1, Def1;

        l1 = k by A3, A5;

        hence thesis by A4, A5;

      end;

    end

    theorem :: ORTSP_1:11



     Th11: not b _|_ a implies (x - (( ProJ (a,b,x)) * b)) _|_ a

    proof

      assume

       A1: not b _|_ a;

      then ex l be Element of F st (x - (l * b)) _|_ a by Def1;

      hence thesis by A1, Def2;

    end;

    theorem :: ORTSP_1:12



     Th12: not b _|_ a implies ( ProJ (a,b,(l * x))) = (l * ( ProJ (a,b,x)))

    proof

      set L = (x - (( ProJ (a,b,x)) * b));



       A1: (l * L) = ((l * x) - (l * (( ProJ (a,b,x)) * b))) by VECTSP_1: 23

      .= ((l * x) - ((l * ( ProJ (a,b,x))) * b)) by VECTSP_1:def 16;

      assume

       A2: not b _|_ a;

      then

       A3: ((l * x) - (( ProJ (a,b,(l * x))) * b)) _|_ a by Th11;

      L _|_ a by A2, Th11;

      then ((l * x) - ((l * ( ProJ (a,b,x))) * b)) _|_ a by A1, Def1;

      hence thesis by A2, A3, Th8;

    end;

    theorem :: ORTSP_1:13



     Th13: not b _|_ a implies ( ProJ (a,b,(x + y))) = (( ProJ (a,b,x)) + ( ProJ (a,b,y)))

    proof

      set 1F = ( 1_ F);

      set L = ((x - (( ProJ (a,b,x)) * b)) + (y - (( ProJ (a,b,y)) * b)));



       A1: L = ((x + ( - (( ProJ (a,b,x)) * b))) + (y - (( ProJ (a,b,y)) * b)))

      .= ((x + ( - (( ProJ (a,b,x)) * b))) + (y + ( - (( ProJ (a,b,y)) * b))))

      .= (((( - (( ProJ (a,b,x)) * b)) + x) + y) + ( - (( ProJ (a,b,y)) * b))) by RLVECT_1:def 3

      .= (((x + y) + ( - (( ProJ (a,b,x)) * b))) + ( - (( ProJ (a,b,y)) * b))) by RLVECT_1:def 3

      .= ((x + y) + (( - (( ProJ (a,b,x)) * b)) + ( - (( ProJ (a,b,y)) * b)))) by RLVECT_1:def 3

      .= ((x + y) + ((1F * ( - (( ProJ (a,b,x)) * b))) + ( - (( ProJ (a,b,y)) * b)))) by VECTSP_1:def 17

      .= ((x + y) + ((1F * ( - (( ProJ (a,b,x)) * b))) + (1F * ( - (( ProJ (a,b,y)) * b))))) by VECTSP_1:def 17

      .= ((x + y) + ((1F * (( - ( ProJ (a,b,x))) * b)) + (1F * ( - (( ProJ (a,b,y)) * b))))) by VECTSP_1: 21

      .= ((x + y) + ((1F * (( - ( ProJ (a,b,x))) * b)) + (1F * (( - ( ProJ (a,b,y))) * b)))) by VECTSP_1: 21

      .= ((x + y) + (((1F * ( - ( ProJ (a,b,x)))) * b) + (1F * (( - ( ProJ (a,b,y))) * b)))) by VECTSP_1:def 16

      .= ((x + y) + (((( - ( ProJ (a,b,x))) * 1F) * b) + ((1F * ( - ( ProJ (a,b,y)))) * b))) by VECTSP_1:def 16

      .= ((x + y) + ((( - ( ProJ (a,b,x))) * b) + ((( - ( ProJ (a,b,y))) * 1F) * b)))

      .= ((x + y) + ((( - ( ProJ (a,b,x))) * b) + (( - ( ProJ (a,b,y))) * b)))

      .= ((x + y) + ((( - ( ProJ (a,b,x))) + ( - ( ProJ (a,b,y)))) * b)) by VECTSP_1:def 15

      .= ((x + y) + (( - (( ProJ (a,b,x)) + ( ProJ (a,b,y)))) * b)) by RLVECT_1: 31

      .= ((x + y) - ((( ProJ (a,b,x)) + ( ProJ (a,b,y))) * b)) by VECTSP_1: 21;

      assume

       A2: not b _|_ a;

      then (x - (( ProJ (a,b,x)) * b)) _|_ a & (y - (( ProJ (a,b,y)) * b)) _|_ a by Th11;

      then

       A3: L _|_ a by Def1;

      ((x + y) - (( ProJ (a,b,(x + y))) * b)) _|_ a by A2, Th11;

      hence thesis by A2, A1, A3, Th8;

    end;

    theorem :: ORTSP_1:14

     not b _|_ a & l <> ( 0. F) implies ( ProJ (a,(l * b),x)) = ((l " ) * ( ProJ (a,b,x)))

    proof

      assume that

       A1: not b _|_ a and

       A2: l <> ( 0. F);

      set L = (x - (( ProJ (a,(l * b),x)) * (l * b)));

       not (l * b) _|_ a by A1, A2, Th5;

      then

       A3: L _|_ a by Th11;



       A4: L = (x - ((( ProJ (a,(l * b),x)) * l) * b)) by VECTSP_1:def 16;

      (x - (( ProJ (a,b,x)) * b)) _|_ a by A1, Th11;

      then (( ProJ (a,b,x)) * (l " )) = ((( ProJ (a,(l * b),x)) * l) * (l " )) by A1, A3, A4, Th8;

      then (( ProJ (a,b,x)) * (l " )) = (( ProJ (a,(l * b),x)) * (l * (l " ))) by GROUP_1:def 3;

      then ((l " ) * ( ProJ (a,b,x))) = (( ProJ (a,(l * b),x)) * ( 1_ F)) by A2, VECTSP_1:def 10;

      hence thesis;

    end;

    theorem :: ORTSP_1:15



     Th15: not b _|_ a & l <> ( 0. F) implies ( ProJ ((l * a),b,x)) = ( ProJ (a,b,x))

    proof

      assume that

       A1: not b _|_ a and

       A2: l <> ( 0. F);

       not b _|_ (l * a) by A1, A2, Th5;

      then (x - (( ProJ ((l * a),b,x)) * b)) _|_ (l * a) by Th11;

      then (l * a) _|_ (x - (( ProJ ((l * a),b,x)) * b)) by Th2;

      then ((l " ) * (l * a)) _|_ (x - (( ProJ ((l * a),b,x)) * b)) by Def1;

      then (((l " ) * l) * a) _|_ (x - (( ProJ ((l * a),b,x)) * b)) by VECTSP_1:def 16;

      then (( 1_ F) * a) _|_ (x - (( ProJ ((l * a),b,x)) * b)) by A2, VECTSP_1:def 10;

      then a _|_ (x - (( ProJ ((l * a),b,x)) * b)) by VECTSP_1:def 17;

      then

       A3: (x - (( ProJ ((l * a),b,x)) * b)) _|_ a by Th2;

      (x - (( ProJ (a,b,x)) * b)) _|_ a by A1, Th11;

      hence thesis by A1, A3, Th8;

    end;

    theorem :: ORTSP_1:16

     not b _|_ a & p _|_ a implies ( ProJ (a,(b + p),c)) = ( ProJ (a,b,c)) & ( ProJ (a,b,(c + p))) = ( ProJ (a,b,c))

    proof

      set 0V = ( 0. S);

      assume that

       A1: not b _|_ a and

       A2: p _|_ a;

       not (b + p) _|_ a by A1, A2, Th4;

      then (c - (( ProJ (a,(b + p),c)) * (b + p))) _|_ a by Th11;

      then (c - ((( ProJ (a,(b + p),c)) * b) + (( ProJ (a,(b + p),c)) * p))) _|_ a by VECTSP_1:def 14;

      then

       A3: ((c - (( ProJ (a,(b + p),c)) * b)) - (( ProJ (a,(b + p),c)) * p)) _|_ a by VECTSP_1: 17;

      ((c + p) - (( ProJ (a,b,(c + p))) * b)) _|_ a & ( - p) _|_ a by A1, A2, Th6, Th11;

      then (( - p) + ((p + c) + ( - (( ProJ (a,b,(c + p))) * b)))) _|_ a by Def1;

      then (( - p) + (p + (c + ( - (( ProJ (a,b,(c + p))) * b))))) _|_ a by RLVECT_1:def 3;

      then ((( - p) + p) + (c + ( - (( ProJ (a,b,(c + p))) * b)))) _|_ a by RLVECT_1:def 3;

      then (0V + (c + ( - (( ProJ (a,b,(c + p))) * b)))) _|_ a by RLVECT_1: 5;

      then

       A4: (c - (( ProJ (a,b,(c + p))) * b)) _|_ a by RLVECT_1: 4;

      (( ProJ (a,(b + p),c)) * p) _|_ a by A2, Def1;

      then (((c + ( - (( ProJ (a,(b + p),c)) * b))) - (( ProJ (a,(b + p),c)) * p)) + (( ProJ (a,(b + p),c)) * p)) _|_ a by A3, Def1;

      then ((c + ( - (( ProJ (a,(b + p),c)) * b))) + (( - (( ProJ (a,(b + p),c)) * p)) + (( ProJ (a,(b + p),c)) * p))) _|_ a by RLVECT_1:def 3;

      then ((c + ( - (( ProJ (a,(b + p),c)) * b))) + 0V) _|_ a by RLVECT_1: 5;

      then

       A5: (c - (( ProJ (a,(b + p),c)) * b)) _|_ a by RLVECT_1: 4;

      (c - (( ProJ (a,b,c)) * b)) _|_ a by A1, Th11;

      hence thesis by A1, A5, A4, Th8;

    end;

    theorem :: ORTSP_1:17

     not b _|_ a & p _|_ b & p _|_ c implies ( ProJ ((a + p),b,c)) = ( ProJ (a,b,c))

    proof

      assume that

       A1: not b _|_ a and

       A2: p _|_ b and

       A3: p _|_ c;

      b _|_ p by A2, Th2;

      then (( ProJ (a,b,c)) * b) _|_ p by Def1;

      then

       A4: ( - (( ProJ (a,b,c)) * b)) _|_ p by Th6;

      c _|_ p by A3, Th2;

      then (c + ( - (( ProJ (a,b,c)) * b))) _|_ p by A4, Def1;

      then

       A5: p _|_ (c - (( ProJ (a,b,c)) * b)) by Th2;

      (c - (( ProJ (a,b,c)) * b)) _|_ a by A1, Th11;

      then a _|_ (c - (( ProJ (a,b,c)) * b)) by Th2;

      then (a + p) _|_ (c - (( ProJ (a,b,c)) * b)) by A5, Def1;

      then

       A6: (c - (( ProJ (a,b,c)) * b)) _|_ (a + p) by Th2;

       not a _|_ b by A1, Th2;

      then not (a + p) _|_ b by A2, Th4;

      then

       A7: not b _|_ (a + p) by Th2;

      then (c - (( ProJ ((a + p),b,c)) * b)) _|_ (a + p) by Th11;

      hence thesis by A7, A6, Th8;

    end;

    theorem :: ORTSP_1:18



     Th18: not b _|_ a & (c - b) _|_ a implies ( ProJ (a,b,c)) = ( 1_ F)

    proof

      assume that

       A1: not b _|_ a and

       A2: (c - b) _|_ a;

      (c - (( 1_ F) * b)) _|_ a & (c - (( ProJ (a,b,c)) * b)) _|_ a by A1, A2, Th11, VECTSP_1:def 17;

      hence thesis by A1, Th8;

    end;

    theorem :: ORTSP_1:19



     Th19: not b _|_ a implies ( ProJ (a,b,b)) = ( 1_ F)

    proof



       A1: (b - b) = ( 0. S) by RLVECT_1: 5;

      assume not b _|_ a;

      hence thesis by A1, Th1, Th18;

    end;

    theorem :: ORTSP_1:20



     Th20: not b _|_ a implies (x _|_ a iff ( ProJ (a,b,x)) = ( 0. F))

    proof

      set 0F = ( 0. F);

      set 0V = ( 0. S);

       A1:

      now

        assume that

         A2: not b _|_ a and

         A3: x _|_ a;

        (x + 0V) _|_ a by A3, RLVECT_1: 4;

        then (x + ( - 0V)) _|_ a by RLVECT_1: 12;

        then

         A4: (x - (0F * b)) _|_ a by VECTSP_1: 14;

        (x - (( ProJ (a,b,x)) * b)) _|_ a by A2, Th11;

        hence ( ProJ (a,b,x)) = ( 0. F) by A2, A4, Th8;

      end;

      now

        assume ( not b _|_ a) & ( ProJ (a,b,x)) = ( 0. F);

        then (x - (0F * b)) _|_ a by Th11;

        then (x + ( - 0V)) _|_ a by VECTSP_1: 14;

        then (x + 0V) _|_ a by RLVECT_1: 12;

        hence x _|_ a by RLVECT_1: 4;

      end;

      hence thesis by A1;

    end;

    theorem :: ORTSP_1:21



     Th21: not b _|_ a & not q _|_ a implies (( ProJ (a,b,p)) * (( ProJ (a,b,q)) " )) = ( ProJ (a,q,p))

    proof

      assume that

       A1: not b _|_ a and

       A2: not q _|_ a;

      ((( ProJ (a,q,p)) * q) - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b)) _|_ a & (p - (( ProJ (a,q,p)) * q)) _|_ a by A1, A2, Th11;

      then ((p + ( - (( ProJ (a,q,p)) * q))) + ((( ProJ (a,q,p)) * q) - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b))) _|_ a by Def1;

      then (((p + ( - (( ProJ (a,q,p)) * q))) + (( ProJ (a,q,p)) * q)) + ( - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b))) _|_ a by RLVECT_1:def 3;

      then ((p + (( - (( ProJ (a,q,p)) * q)) + (( ProJ (a,q,p)) * q))) + ( - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b))) _|_ a by RLVECT_1:def 3;

      then ((p + ( 0. S)) + ( - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b))) _|_ a by RLVECT_1: 5;

      then (p - (( ProJ (a,b,(( ProJ (a,q,p)) * q))) * b)) _|_ a by RLVECT_1: 4;

      then

       A3: (p - ((( ProJ (a,q,p)) * ( ProJ (a,b,q))) * b)) _|_ a by A1, Th12;

      (p - (( ProJ (a,b,p)) * b)) _|_ a by A1, Th11;

      then (( ProJ (a,q,p)) * ( ProJ (a,b,q))) = ( ProJ (a,b,p)) by A1, A3, Th8;

      then

       A4: (( ProJ (a,q,p)) * (( ProJ (a,b,q)) * (( ProJ (a,b,q)) " ))) = (( ProJ (a,b,p)) * (( ProJ (a,b,q)) " )) by GROUP_1:def 3;

      ( ProJ (a,b,q)) <> ( 0. F) by A1, A2, Th20;

      then (( ProJ (a,q,p)) * ( 1_ F)) = (( ProJ (a,b,p)) * (( ProJ (a,b,q)) " )) by A4, VECTSP_1:def 10;

      hence thesis;

    end;

    theorem :: ORTSP_1:22



     Th22: not b _|_ a & not c _|_ a implies ( ProJ (a,b,c)) = (( ProJ (a,c,b)) " )

    proof

      set 1F = ( 1_ F);

      set 0F = ( 0. F);

      assume that

       A1: not b _|_ a and

       A2: not c _|_ a;



       A3: ( ProJ (a,c,b)) <> 0F by A1, A2, Th20;

      (( ProJ (a,b,b)) * (( ProJ (a,b,c)) " )) = ( ProJ (a,c,b)) by A1, A2, Th21;

      then ((( ProJ (a,b,c)) " ) * 1F) = ( ProJ (a,c,b)) by A1, Th19;

      then

       A4: (( ProJ (a,b,c)) " ) = ( ProJ (a,c,b));

      ( ProJ (a,b,c)) <> 0F by A1, A2, Th20;

      then 1F = (( ProJ (a,c,b)) * ( ProJ (a,b,c))) by A4, VECTSP_1:def 10;



      then (( ProJ (a,c,b)) " ) = ((( ProJ (a,c,b)) " ) * (( ProJ (a,c,b)) * ( ProJ (a,b,c))))

      .= (((( ProJ (a,c,b)) " ) * ( ProJ (a,c,b))) * ( ProJ (a,b,c))) by GROUP_1:def 3

      .= (( ProJ (a,b,c)) * 1F) by A3, VECTSP_1:def 10;

      hence thesis;

    end;

    theorem :: ORTSP_1:23



     Th23: not b _|_ a & b _|_ (c + a) implies ( ProJ (a,b,c)) = ( - ( ProJ (c,b,a)))

    proof

      set 1F = ( 1_ F);

      assume that

       A1: not b _|_ a and

       A2: b _|_ (c + a);

      (c - (( ProJ (a,b,c)) * b)) _|_ a by A1, Th11;

      then ((( - ( ProJ (a,b,c))) * b) + c) _|_ a by VECTSP_1: 21;

      then (( - 1F) * ((( - ( ProJ (a,b,c))) * b) + c)) _|_ a by Def1;

      then ((( - 1F) * (( - ( ProJ (a,b,c))) * b)) + (( - 1F) * c)) _|_ a by VECTSP_1:def 14;

      then (((( - 1F) * ( - ( ProJ (a,b,c)))) * b) + (( - 1F) * c)) _|_ a by VECTSP_1:def 16;

      then (((( ProJ (a,b,c)) * 1F) * b) + (( - 1F) * c)) _|_ a by VECTSP_1: 10;

      then ((( ProJ (a,b,c)) * b) + (( - 1F) * c)) _|_ a;

      then ((( ProJ (a,b,c)) * b) - c) _|_ a by VECTSP_1: 14;

      then a _|_ ((( ProJ (a,b,c)) * b) - c) by Th2;

      then

       A3: ( - a) _|_ ((( ProJ (a,b,c)) * b) - c) by Th6;

      (( ProJ (a,b,c)) * b) _|_ (c + a) by A2, Def1;

      then (( ProJ (a,b,c)) * b) _|_ (c - ( - a)) by RLVECT_1: 17;

      then c _|_ (( - a) - (( ProJ (a,b,c)) * b)) by A3, Def1;

      then

       A4: (( - a) - (( ProJ (a,b,c)) * b)) _|_ c by Th2;

      ( not a _|_ b) & (c + a) _|_ b by A1, A2, Th2;

      then

       A5: not c _|_ b by Th3;

      then

       A6: not b _|_ c by Th2;

      then (( - a) - (( ProJ (c,b,( - a))) * b)) _|_ c by Th11;



      then ( ProJ (a,b,c)) = ( ProJ (c,b,( - a))) by A6, A4, Th8

      .= ( ProJ (c,b,(( - 1F) * a))) by VECTSP_1: 14

      .= (( - 1F) * ( ProJ (c,b,a))) by A5, Th2, Th12

      .= ( - (( ProJ (c,b,a)) * 1F)) by VECTSP_1: 9;

      hence thesis;

    end;

    theorem :: ORTSP_1:24



     Th24: not a _|_ b & not c _|_ b implies ( ProJ (c,b,a)) = ((( ProJ (b,a,c)) " ) * ( ProJ (a,b,c)))

    proof

      set 1F = ( 1_ F);

      assume that

       A1: not a _|_ b and

       A2: not c _|_ b;

      ( ProJ (b,a,c)) <> ( 0. F) by A1, A2, Th20;

      then

       A3: ( - (( ProJ (b,a,c)) " )) <> ( 0. F) by VECTSP_1: 25;

      ( ProJ (b,a,c)) <> ( 0. F) by A1, A2, Th20;

      then (( - 1F) * ((( ProJ (b,a,c)) " ) * ( ProJ (b,a,c)))) = (( - 1F) * 1F) by VECTSP_1:def 10;

      then ((( - 1F) * (( ProJ (b,a,c)) " )) * ( ProJ (b,a,c))) = (( - 1F) * 1F) by GROUP_1:def 3;

      then ((( - 1F) * (( ProJ (b,a,c)) " )) * ( ProJ (b,a,c))) = ( - 1F);

      then (( - ((( ProJ (b,a,c)) " ) * 1F)) * ( ProJ (b,a,c))) = ( - 1F) by VECTSP_1: 9;

      then (( - (( ProJ (b,a,c)) " )) * ( ProJ (b,a,c))) = ( - 1F);

      then ( ProJ (b,a,(( - (( ProJ (b,a,c)) " )) * c))) = ( - 1F) by A1, Th12;

      then ((( - (( ProJ (b,a,c)) " )) * c) - (( - 1F) * a)) _|_ b by A1, Th11;

      then ((( - (( ProJ (b,a,c)) " )) * c) + ( - ( - a))) _|_ b by VECTSP_1: 14;

      then ((( - (( ProJ (b,a,c)) " )) * c) + a) _|_ b by RLVECT_1: 17;

      then

       A4: b _|_ ((( - (( ProJ (b,a,c)) " )) * c) + a) by Th2;

       not b _|_ a by A1, Th2;

      then ( ProJ (a,b,(( - (( ProJ (b,a,c)) " )) * c))) = ( - ( ProJ ((( - (( ProJ (b,a,c)) " )) * c),b,a))) by A4, Th23;

      then ( ProJ (a,b,(( - (( ProJ (b,a,c)) " )) * c))) = ( - ( ProJ (c,b,a))) by A2, A3, Th2, Th15;

      then (( - (( ProJ (b,a,c)) " )) * ( ProJ (a,b,c))) = ( - ( ProJ (c,b,a))) by A1, Th2, Th12;

      then (( - ((( ProJ (b,a,c)) " ) * ( ProJ (a,b,c)))) * ( - 1F)) = (( - ( ProJ (c,b,a))) * ( - 1F)) by VECTSP_1: 9;

      then (((( ProJ (b,a,c)) " ) * ( ProJ (a,b,c))) * 1F) = (( - ( ProJ (c,b,a))) * ( - 1F)) by VECTSP_1: 10;

      then (((( ProJ (b,a,c)) " ) * ( ProJ (a,b,c))) * 1F) = (( ProJ (c,b,a)) * 1F) by VECTSP_1: 10;

      then ((( ProJ (b,a,c)) " ) * ( ProJ (a,b,c))) = (( ProJ (c,b,a)) * 1F);

      hence thesis;

    end;

    theorem :: ORTSP_1:25



     Th25: not p _|_ a & not p _|_ x & not q _|_ a & not q _|_ x implies (( ProJ (a,q,p)) * ( ProJ (p,a,x))) = (( ProJ (q,a,x)) * ( ProJ (x,q,p)))

    proof

      set 0F = ( 0. F);

      set 1F = ( 1_ F);

      assume that

       A1: not p _|_ a and

       A2: not p _|_ x and

       A3: not q _|_ a and

       A4: not q _|_ x;



       A5: p <> ( 0. S) & q <> ( 0. S) by A1, A3, Th1;



       A6: not a _|_ p by A1, Th2;

      a <> ( 0. S) & x <> ( 0. S) by A1, A2, Th1, Th2;

      then

      consider r such that

       A7: not r _|_ p and

       A8: not r _|_ q and

       A9: not r _|_ a and

       A10: not r _|_ x by A5, Def1;



       A11: not q _|_ r by A8, Th2;



       A12: not x _|_ r by A10, Th2;



       A13: not p _|_ r by A7, Th2;

      then

       A14: ( ProJ (r,q,p)) <> 0F by A11, Th20;



       A15: not a _|_ r by A9, Th2;



       A16: not x _|_ q by A4, Th2;



       A17: not x _|_ p by A2, Th2;



       A18: not a _|_ q by A3, Th2;

      ((( ProJ (a,q,p)) * ( ProJ (p,a,x))) * (( ProJ (q,a,x)) " )) = (((( ProJ (a,r,p)) * (( ProJ (a,r,q)) " )) * ( ProJ (p,a,x))) * (( ProJ (q,a,x)) " )) by A3, A9, Th21

      .= (((( ProJ (a,r,p)) * (( ProJ (a,r,q)) " )) * (( ProJ (p,r,x)) * (( ProJ (p,r,a)) " ))) * (( ProJ (q,a,x)) " )) by A6, A7, Th21

      .= (((( ProJ (a,r,p)) * (( ProJ (a,r,q)) " )) * (( ProJ (p,r,x)) * (( ProJ (p,r,a)) " ))) * ( ProJ (q,x,a))) by A18, A16, Th22

      .= (((( ProJ (a,r,p)) * (( ProJ (a,r,q)) " )) * (( ProJ (p,r,x)) * (( ProJ (p,r,a)) " ))) * (( ProJ (q,r,a)) * (( ProJ (q,r,x)) " ))) by A16, A8, Th21

      .= ((((( ProJ (a,p,r)) " ) * (( ProJ (a,r,q)) " )) * (( ProJ (p,r,x)) * (( ProJ (p,r,a)) " ))) * (( ProJ (q,r,a)) * (( ProJ (q,r,x)) " ))) by A1, A9, Th22

      .= ((((( ProJ (a,p,r)) " ) * (( ProJ (a,r,q)) " )) * (( ProJ (p,r,x)) * ( ProJ (p,a,r)))) * (( ProJ (q,r,a)) * (( ProJ (q,r,x)) " ))) by A6, A7, Th22

      .= ((((( ProJ (a,p,r)) " ) * ( ProJ (a,q,r))) * (( ProJ (p,r,x)) * ( ProJ (p,a,r)))) * (( ProJ (q,r,a)) * (( ProJ (q,r,x)) " ))) by A3, A9, Th22

      .= ((((( ProJ (a,p,r)) " ) * ( ProJ (a,q,r))) * (( ProJ (p,r,x)) * ( ProJ (p,a,r)))) * ((( ProJ (q,a,r)) " ) * (( ProJ (q,r,x)) " ))) by A18, A8, Th22

      .= ((((( ProJ (a,p,r)) " ) * ( ProJ (a,q,r))) * ((( ProJ (p,x,r)) " ) * ( ProJ (p,a,r)))) * ((( ProJ (q,a,r)) " ) * (( ProJ (q,r,x)) " ))) by A17, A7, Th22

      .= ((((( ProJ (p,x,r)) " ) * ( ProJ (p,a,r))) * ((( ProJ (a,p,r)) " ) * ( ProJ (a,q,r)))) * ((( ProJ (q,a,r)) " ) * ( ProJ (q,x,r)))) by A16, A8, Th22

      .= (((( ProJ (p,x,r)) " ) * (((( ProJ (a,p,r)) " ) * ( ProJ (a,q,r))) * ( ProJ (p,a,r)))) * ((( ProJ (q,a,r)) " ) * ( ProJ (q,x,r)))) by GROUP_1:def 3

      .= (((( ProJ (p,x,r)) " ) * (((( ProJ (a,p,r)) " ) * ( ProJ (p,a,r))) * ( ProJ (a,q,r)))) * ((( ProJ (q,a,r)) " ) * ( ProJ (q,x,r)))) by GROUP_1:def 3

      .= (((( ProJ (p,x,r)) " ) * (( ProJ (r,a,p)) * ( ProJ (a,q,r)))) * ((( ProJ (q,a,r)) " ) * ( ProJ (q,x,r)))) by A1, A9, Th24

      .= ((((( ProJ (p,x,r)) " ) * ( ProJ (r,a,p))) * ( ProJ (a,q,r))) * ((( ProJ (q,a,r)) " ) * ( ProJ (q,x,r)))) by GROUP_1:def 3

      .= (((( ProJ (p,x,r)) " ) * ( ProJ (r,a,p))) * (( ProJ (a,q,r)) * ((( ProJ (q,a,r)) " ) * ( ProJ (q,x,r))))) by GROUP_1:def 3

      .= (((( ProJ (p,x,r)) " ) * ( ProJ (r,a,p))) * (((( ProJ (q,a,r)) " ) * ( ProJ (a,q,r))) * ( ProJ (q,x,r)))) by GROUP_1:def 3

      .= (((( ProJ (p,x,r)) " ) * ( ProJ (r,a,p))) * (( ProJ (r,q,a)) * ( ProJ (q,x,r)))) by A18, A8, Th24

      .= ((( ProJ (p,x,r)) " ) * (( ProJ (r,a,p)) * (( ProJ (r,q,a)) * ( ProJ (q,x,r))))) by GROUP_1:def 3

      .= ((( ProJ (p,x,r)) " ) * ((( ProJ (r,a,p)) * ( ProJ (r,q,a))) * ( ProJ (q,x,r)))) by GROUP_1:def 3

      .= ((( ProJ (p,x,r)) " ) * ((( ProJ (r,a,p)) * (( ProJ (r,a,q)) " )) * ( ProJ (q,x,r)))) by A11, A15, Th22

      .= ((( ProJ (p,x,r)) " ) * (( ProJ (r,q,p)) * ( ProJ (q,x,r)))) by A11, A15, Th21

      .= (( ProJ (p,r,x)) * (( ProJ (r,q,p)) * ( ProJ (q,x,r)))) by A17, A7, Th22

      .= (((( ProJ (r,x,p)) " ) * ( ProJ (x,r,p))) * (( ProJ (r,q,p)) * ( ProJ (q,x,r)))) by A13, A12, Th24

      .= (((( ProJ (r,x,p)) " ) * ( ProJ (x,r,p))) * (( ProJ (r,q,p)) * ((( ProJ (x,r,q)) " ) * ( ProJ (r,x,q))))) by A4, A10, Th24

      .= (((( ProJ (r,x,p)) " ) * ( ProJ (x,r,p))) * (( ProJ (r,x,q)) * (( ProJ (r,q,p)) * (( ProJ (x,r,q)) " )))) by GROUP_1:def 3

      .= (((( ProJ (x,r,p)) * (( ProJ (r,x,p)) " )) * ( ProJ (r,x,q))) * (( ProJ (r,q,p)) * (( ProJ (x,r,q)) " ))) by GROUP_1:def 3

      .= ((( ProJ (x,r,p)) * (( ProJ (r,x,q)) * (( ProJ (r,x,p)) " ))) * (( ProJ (r,q,p)) * (( ProJ (x,r,q)) " ))) by GROUP_1:def 3

      .= ((( ProJ (x,r,p)) * ( ProJ (r,p,q))) * (( ProJ (r,q,p)) * (( ProJ (x,r,q)) " ))) by A13, A12, Th21

      .= (( ProJ (x,r,p)) * (( ProJ (r,p,q)) * (( ProJ (r,q,p)) * (( ProJ (x,r,q)) " )))) by GROUP_1:def 3

      .= (( ProJ (x,r,p)) * ((( ProJ (r,p,q)) * ( ProJ (r,q,p))) * (( ProJ (x,r,q)) " ))) by GROUP_1:def 3

      .= (( ProJ (x,r,p)) * (((( ProJ (r,q,p)) " ) * ( ProJ (r,q,p))) * (( ProJ (x,r,q)) " ))) by A13, A11, Th22

      .= (( ProJ (x,r,p)) * ((( ProJ (x,r,q)) " ) * 1F)) by A14, VECTSP_1:def 10

      .= (( ProJ (x,r,p)) * (( ProJ (x,r,q)) " ))

      .= ( ProJ (x,q,p)) by A4, A10, Th21;

      then

       A19: ((( ProJ (q,a,x)) * (( ProJ (q,a,x)) " )) * (( ProJ (a,q,p)) * ( ProJ (p,a,x)))) = (( ProJ (q,a,x)) * ( ProJ (x,q,p))) by GROUP_1:def 3;

      ( ProJ (q,a,x)) <> 0F by A18, A16, Th20;

      then ((( ProJ (a,q,p)) * ( ProJ (p,a,x))) * 1F) = (( ProJ (q,a,x)) * ( ProJ (x,q,p))) by A19, VECTSP_1:def 10;

      hence thesis;

    end;

    theorem :: ORTSP_1:26



     Th26: not p _|_ a & not p _|_ x & not q _|_ a & not q _|_ x & not b _|_ a implies ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y)))

    proof

      set 0F = ( 0. F);

      set 1F = ( 1_ F);

      assume that

       A1: not p _|_ a and

       A2: not p _|_ x and

       A3: not q _|_ a and

       A4: not q _|_ x and

       A5: not b _|_ a;

       A6:

      now



         A7: ( ProJ (a,b,q)) <> 0F by A3, A5, Th20;

        assume

         A8: not y _|_ x;

        (( ProJ (a,q,p)) * ( ProJ (p,a,x))) = (( ProJ (x,q,p)) * ( ProJ (q,a,x))) by A1, A2, A3, A4, Th25;

        then ((( ProJ (a,b,p)) * (( ProJ (a,b,q)) " )) * ( ProJ (p,a,x))) = (( ProJ (x,q,p)) * ( ProJ (q,a,x))) by A3, A5, Th21;

        then (((( ProJ (a,b,q)) " ) * ( ProJ (a,b,p))) * ( ProJ (p,a,x))) = ((( ProJ (x,y,p)) * (( ProJ (x,y,q)) " )) * ( ProJ (q,a,x))) by A4, A8, Th21;

        then (( ProJ (a,b,q)) * ((( ProJ (a,b,q)) " ) * (( ProJ (a,b,p)) * ( ProJ (p,a,x))))) = (( ProJ (a,b,q)) * ((( ProJ (x,y,p)) * (( ProJ (x,y,q)) " )) * ( ProJ (q,a,x)))) by GROUP_1:def 3;

        then ((( ProJ (a,b,q)) * (( ProJ (a,b,q)) " )) * (( ProJ (a,b,p)) * ( ProJ (p,a,x)))) = (( ProJ (a,b,q)) * ((( ProJ (x,y,p)) * (( ProJ (x,y,q)) " )) * ( ProJ (q,a,x)))) by GROUP_1:def 3;

        then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * 1F) = (( ProJ (a,b,q)) * ((( ProJ (x,y,p)) * (( ProJ (x,y,q)) " )) * ( ProJ (q,a,x)))) by A7, VECTSP_1:def 10;

        then (( ProJ (a,b,p)) * ( ProJ (p,a,x))) = (( ProJ (a,b,q)) * ((( ProJ (x,y,p)) * (( ProJ (x,y,q)) " )) * ( ProJ (q,a,x))));

        then (( ProJ (a,b,p)) * ( ProJ (p,a,x))) = (( ProJ (a,b,q)) * (((( ProJ (x,y,q)) " ) * (( ProJ (x,p,y)) " )) * ( ProJ (q,a,x)))) by A2, A8, Th22;

        then (( ProJ (a,b,p)) * ( ProJ (p,a,x))) = ((( ProJ (a,b,q)) * ((( ProJ (x,y,q)) " ) * (( ProJ (x,p,y)) " ))) * ( ProJ (q,a,x))) by GROUP_1:def 3;

        then (( ProJ (a,b,p)) * ( ProJ (p,a,x))) = (( ProJ (q,a,x)) * ((( ProJ (a,b,q)) * (( ProJ (x,y,q)) " )) * (( ProJ (x,p,y)) " ))) by GROUP_1:def 3;

        then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = (((( ProJ (q,a,x)) * (( ProJ (a,b,q)) * (( ProJ (x,y,q)) " ))) * (( ProJ (x,p,y)) " )) * ( ProJ (x,p,y))) by GROUP_1:def 3;

        then

         A9: ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = ((( ProJ (q,a,x)) * (( ProJ (a,b,q)) * (( ProJ (x,y,q)) " ))) * ((( ProJ (x,p,y)) " ) * ( ProJ (x,p,y)))) by GROUP_1:def 3;

        ( ProJ (x,p,y)) <> 0F by A2, A8, Th20;

        then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = ((( ProJ (q,a,x)) * (( ProJ (a,b,q)) * (( ProJ (x,y,q)) " ))) * 1F) by A9, VECTSP_1:def 10;

        then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = (( ProJ (q,a,x)) * (( ProJ (a,b,q)) * (( ProJ (x,y,q)) " )));

        then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = (( ProJ (q,a,x)) * (( ProJ (a,b,q)) * ( ProJ (x,q,y)))) by A4, A8, Th22;

        hence thesis by GROUP_1:def 3;

      end;

      now

        assume

         A10: y _|_ x;

        then ( ProJ (x,p,y)) = 0F by A2, Th20;

        then

         A11: ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = 0F;

        ( ProJ (x,q,y)) = 0F by A4, A10, Th20;

        hence thesis by A11;

      end;

      hence thesis by A6;

    end;

    theorem :: ORTSP_1:27



     Th27: not a _|_ p & not x _|_ p & not y _|_ p implies (( ProJ (p,a,x)) * ( ProJ (x,p,y))) = (( ProJ (p,a,y)) * ( ProJ (y,p,x)))

    proof

      set 0F = ( 0. F);

      set 1F = ( 1_ F);

      assume that

       A1: not a _|_ p and

       A2: not x _|_ p and

       A3: not y _|_ p;



       A4: not p _|_ y by A3, Th2;



       A5: not p _|_ x by A2, Th2;

       A6:

      now



         A7: ( ProJ (p,a,x)) <> 0F by A1, A2, Th20;

        assume

         A8: not y _|_ x;

        then

         A9: not x _|_ y by Th2;

        (( ProJ (p,a,y)) * (( ProJ (p,a,x)) " )) = ( ProJ (p,x,y)) by A1, A2, Th21;

        then ((( ProJ (p,a,y)) * (( ProJ (p,a,x)) " )) * ( ProJ (p,a,x))) = (((( ProJ (x,y,p)) " ) * ( ProJ (y,x,p))) * ( ProJ (p,a,x))) by A5, A8, Th24;

        then (( ProJ (p,a,y)) * ((( ProJ (p,a,x)) " ) * ( ProJ (p,a,x)))) = (((( ProJ (x,y,p)) " ) * ( ProJ (y,x,p))) * ( ProJ (p,a,x))) by GROUP_1:def 3;

        then (( ProJ (p,a,y)) * 1F) = (((( ProJ (x,y,p)) " ) * ( ProJ (y,x,p))) * ( ProJ (p,a,x))) by A7, VECTSP_1:def 10;

        then ( ProJ (p,a,y)) = ((( ProJ (y,x,p)) * (( ProJ (x,y,p)) " )) * ( ProJ (p,a,x)));

        then ( ProJ (p,a,y)) = (( ProJ (y,x,p)) * ((( ProJ (x,y,p)) " ) * ( ProJ (p,a,x)))) by GROUP_1:def 3;

        then (( ProJ (y,p,x)) * ( ProJ (p,a,y))) = (( ProJ (y,p,x)) * ((( ProJ (y,p,x)) " ) * ((( ProJ (x,y,p)) " ) * ( ProJ (p,a,x))))) by A4, A9, Th22;

        then

         A10: (( ProJ (y,p,x)) * ( ProJ (p,a,y))) = ((( ProJ (y,p,x)) * (( ProJ (y,p,x)) " )) * ((( ProJ (x,y,p)) " ) * ( ProJ (p,a,x)))) by GROUP_1:def 3;

        ( ProJ (y,p,x)) <> 0F by A4, A9, Th20;



        then (( ProJ (y,p,x)) * ( ProJ (p,a,y))) = (((( ProJ (x,y,p)) " ) * ( ProJ (p,a,x))) * 1F) by A10, VECTSP_1:def 10

        .= ((( ProJ (x,y,p)) " ) * ( ProJ (p,a,x)));

        hence thesis by A5, A8, Th22;

      end;

      now

        assume

         A11: y _|_ x;

        then ( ProJ (x,p,y)) = 0F by A5, Th20;

        then

         A12: (( ProJ (p,a,x)) * ( ProJ (x,p,y))) = 0F;

        x _|_ y by A11, Th2;

        then ( ProJ (y,p,x)) = 0F by A4, Th20;

        hence thesis by A12;

      end;

      hence thesis by A6;

    end;

    definition

      let F, S, x, y, a, b;

      assume

       A1: not b _|_ a;

      :: ORTSP_1:def3

      func PProJ (a,b,x,y) -> Element of F means

      : Def3: for q st not q _|_ a & not q _|_ x holds it = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y))) if ex p st not p _|_ a & not p _|_ x

      otherwise it = ( 0. F);

      existence

      proof

        thus (ex p st not p _|_ a & not p _|_ x) implies ex IT be Element of F st for q st not q _|_ a & not q _|_ x holds IT = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y)))

        proof

          given p such that

           A2: ( not p _|_ a) & not p _|_ x;

          take ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y)));

          let q;

          assume ( not q _|_ a) & not q _|_ x;

          hence thesis by A1, A2, Th26;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of F;

        thus (ex p st not p _|_ a & not p _|_ x) & (for q st not q _|_ a & not q _|_ x holds IT1 = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y)))) & (for q st not q _|_ a & not q _|_ x holds IT2 = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y)))) implies IT1 = IT2

        proof

          given p such that

           A3: ( not p _|_ a) & not p _|_ x;

          consider r such that

           A4: ( not r _|_ a) & not r _|_ x by A3;

          assume that

           A5: for q st not q _|_ a & not q _|_ x holds IT1 = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y))) and

           A6: for q st not q _|_ a & not q _|_ x holds IT2 = ((( ProJ (a,b,q)) * ( ProJ (q,a,x))) * ( ProJ (x,q,y)));

          IT1 = ((( ProJ (a,b,r)) * ( ProJ (r,a,x))) * ( ProJ (x,r,y))) by A5, A4;

          hence thesis by A6, A4;

        end;

        thus thesis;

      end;

      consistency ;

    end

    theorem :: ORTSP_1:28



     Th28: not b _|_ a & x = ( 0. S) implies ( PProJ (a,b,x,y)) = ( 0. F)

    proof

      assume that

       A1: not b _|_ a and

       A2: x = ( 0. S);

      for p holds p _|_ a or p _|_ x by A2, Th1, Th2;

      hence thesis by A1, Def3;

    end;

    theorem :: ORTSP_1:29



     Th29: not b _|_ a implies (( PProJ (a,b,x,y)) = ( 0. F) iff y _|_ x)

    proof

      set 0F = ( 0. F);

      assume

       A1: not b _|_ a;

      then

       A2: a <> ( 0. S) by Th1, Th2;



       A3: ( PProJ (a,b,x,y)) = ( 0. F) implies y _|_ x

      proof

        assume

         A4: ( PProJ (a,b,x,y)) = ( 0. F);

         A5:

        now

          given p such that

           A6: not p _|_ a and

           A7: not p _|_ x;

           A8:

          now

            assume

             A9: ( ProJ (p,a,x)) = ( 0. F);

             not a _|_ p by A6, Th2;

            then x _|_ p by A9, Th20;

            hence contradiction by A7, Th2;

          end;

          ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = 0F by A1, A4, A6, A7, Def3;

          then (( ProJ (a,b,p)) * ( ProJ (p,a,x))) = 0F or ( ProJ (x,p,y)) = 0F by VECTSP_1: 12;

          then ( ProJ (a,b,p)) = ( 0. F) or ( ProJ (p,a,x)) = ( 0. F) or ( ProJ (x,p,y)) = ( 0. F) by VECTSP_1: 12;

          hence thesis by A1, A6, A7, A8, Th20;

        end;

        now

          assume

           A10: for p holds p _|_ a or p _|_ x;

          x = ( 0. S)

          proof

            assume not thesis;

            then ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by A2, Def1;

            hence contradiction by A10;

          end;

          hence thesis by Th1, Th2;

        end;

        hence thesis by A5;

      end;

      y _|_ x implies ( PProJ (a,b,x,y)) = ( 0. F)

      proof

        assume

         A11: y _|_ x;

         A12:

        now

          assume x <> ( 0. S);

          then ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by A2, Def1;

          then

          consider p such that

           A13: not p _|_ a and

           A14: not p _|_ x;

          ( ProJ (x,p,y)) = 0F by A11, A14, Th20;

          then ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) = ( 0. F);

          hence thesis by A1, A13, A14, Def3;

        end;

        now

          assume x = ( 0. S);

          then for p holds p _|_ a or p _|_ x by Th1, Th2;

          hence thesis by A1, Def3;

        end;

        hence thesis by A12;

      end;

      hence thesis by A3;

    end;

    theorem :: ORTSP_1:30

     not b _|_ a implies ( PProJ (a,b,x,y)) = ( PProJ (a,b,y,x))

    proof

      assume

       A1: not b _|_ a;

       A2:

      now

        assume not x _|_ y;

        then

         A3: x <> ( 0. S) & y <> ( 0. S) by Th1, Th2;

        a <> ( 0. S) by A1, Th1, Th2;

        then ex r st not r _|_ a & not r _|_ x & not r _|_ y & not r _|_ a by A3, Def1;

        then

        consider r such that

         A4: not r _|_ a and

         A5: not r _|_ x and

         A6: not r _|_ y;



         A7: not y _|_ r by A6, Th2;

        ( PProJ (a,b,y,x)) = ((( ProJ (a,b,r)) * ( ProJ (r,a,y))) * ( ProJ (y,r,x))) by A1, A4, A6, Def3;

        then

         A8: ( PProJ (a,b,y,x)) = (( ProJ (a,b,r)) * (( ProJ (r,a,y)) * ( ProJ (y,r,x)))) by GROUP_1:def 3;

        ( not a _|_ r) & not x _|_ r by A4, A5, Th2;

        then

         A9: ( PProJ (a,b,y,x)) = (( ProJ (a,b,r)) * (( ProJ (r,a,x)) * ( ProJ (x,r,y)))) by A7, A8, Th27;

        ( PProJ (a,b,x,y)) = ((( ProJ (a,b,r)) * ( ProJ (r,a,x))) * ( ProJ (x,r,y))) by A1, A4, A5, Def3;

        hence thesis by A9, GROUP_1:def 3;

      end;

      now

        assume x _|_ y;

        then y _|_ x & ( PProJ (a,b,y,x)) = ( 0. F) by A1, Th2, Th29;

        hence thesis by A1, Th29;

      end;

      hence thesis by A2;

    end;

    theorem :: ORTSP_1:31

     not b _|_ a implies ( PProJ (a,b,x,(l * y))) = (l * ( PProJ (a,b,x,y)))

    proof

      set 0F = ( 0. F);

      assume

       A1: not b _|_ a;

       A2:

      now

        assume not x _|_ y;

        then

         A3: x <> ( 0. S) by Th1;

        a <> ( 0. S) by A1, Th1, Th2;

        then ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by A3, Def1;

        then

        consider p such that

         A4: not p _|_ a and

         A5: not p _|_ x;

        ( PProJ (a,b,x,(l * y))) = ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,(l * y)))) by A1, A4, A5, Def3;

        then

         A6: ( PProJ (a,b,x,(l * y))) = ((l * ( ProJ (x,p,y))) * (( ProJ (a,b,p)) * ( ProJ (p,a,x)))) by A5, Th12;

        ( PProJ (a,b,x,y)) = ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) by A1, A4, A5, Def3;

        hence thesis by A6, GROUP_1:def 3;

      end;

      now

        assume

         A7: x _|_ y;

        then y _|_ x by Th2;

        then (l * y) _|_ x by Def1;

        then

         A8: ( PProJ (a,b,x,(l * y))) = 0F by A1, Th29;

        y _|_ x by A7, Th2;

        then (l * ( PProJ (a,b,x,y))) = (l * 0F) by A1, Th29;

        hence thesis by A8;

      end;

      hence thesis by A2;

    end;

    theorem :: ORTSP_1:32

     not b _|_ a implies ( PProJ (a,b,x,(y + z))) = (( PProJ (a,b,x,y)) + ( PProJ (a,b,x,z)))

    proof

      set 0F = ( 0. F);

      assume

       A1: not b _|_ a;

       A2:

      now

        assume

         A3: x <> ( 0. S);

        a <> ( 0. S) by A1, Th1, Th2;

        then ex p st not p _|_ a & not p _|_ x & not p _|_ a & not p _|_ x by A3, Def1;

        then

        consider p such that

         A4: ( not p _|_ a) & not p _|_ x;



         A5: ( PProJ (a,b,x,(y + z))) = ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,(y + z)))) & ( PProJ (a,b,x,y)) = ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,y))) by A1, A4, Def3;

        ( PProJ (a,b,x,z)) = ((( ProJ (a,b,p)) * ( ProJ (p,a,x))) * ( ProJ (x,p,z))) & ( ProJ (x,p,(y + z))) = (( ProJ (x,p,y)) + ( ProJ (x,p,z))) by A1, A4, Def3, Th13;

        hence thesis by A5, VECTSP_1:def 7;

      end;

      now

        assume

         A6: x = ( 0. S);

        then

         A7: ( PProJ (a,b,x,z)) = 0F by A1, Th28;

        ( PProJ (a,b,x,(y + z))) = 0F & ( PProJ (a,b,x,y)) = 0F by A1, A6, Th28;

        hence thesis by A7, RLVECT_1: 4;

      end;

      hence thesis by A2;

    end;