:: {C}ross-ratio in Real Vector Space
::  by Roland Coghetto
:: 
:: Received February 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NAT_1, FINSEQ_2, REAL_1, XCMPLX_0, PENCIL_1, ALGSTR_0, ARYTM_1,
      ARYTM_3, CARD_1, EUCLID, FUNCT_1, INCSP_1, NUMBERS, PRE_TOPC, RELAT_1,
      STRUCT_0, SUBSET_1, SUPINF_2, VECTSP_1, XBOOLE_0, TARSKI, FINSEQ_1,
      RLTOPSP1, ANPROJ10, FUNCT_5, RLVECT_1, FUNCOP_1, FUNCT_2, FUNCSDOM,
      BINOP_2, PCOMPS_1, ZFMISC_1;
 notations ORDINAL1, XCMPLX_0, PRE_TOPC, TARSKI, XBOOLE_0, RLVECT_1, XREAL_0,
      SUBSET_1, NUMBERS, FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, ALGSTR_0,
      VECTSP_1, FINSEQ_2, BINOP_1, FUNCOP_1, FINSEQ_4, RVSUM_1, FUNCSDOM,
      BINOP_2, PCOMPS_1, EUCLID, SRINGS_5, RLTOPSP1, EUCLID_4, ZFMISC_1;
 constructors FINSEQ_4, MONOID_0, BINOP_2, FUNCSDOM, PCOMPS_1, SRINGS_5,
      EUCLID_4;
 registrations MEMBERED, ORDINAL1, STRUCT_0, XREAL_0, MONOID_0, EUCLID,
      VALUED_0, XCMPLX_0, NUMBERS, RLTOPSP1, RLVECT_1, RELAT_1, FINSEQ_4;
 requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;


begin :: Preliminaries

registration
  let a,b,c,d be object;
  reduce <*a,b,c,d*>.1 to a;
  reduce <*a,b,c,d*>.2 to b;
  reduce <*a,b,c,d*>.3 to c;
  reduce <*a,b,c,d*>.4 to d;
end;

theorem :: ANPROJ10:1
  for a,b,c,d,a9,b9,c9,d9 being object st
    <* a, b, c, d *> = <* a9, b9, c9, d9 *> holds
      a = a9 & b = b9 & c = c9 & d = d9;

definition
  let r be Real;
  attr r is unit means
:: ANPROJ10:def 1
  r = 1;
end;

registration
  cluster non unit for non zero Real;
end;

definition
  let r be non unit non zero Real;
  func op1(r) -> non unit non zero Real equals
:: ANPROJ10:def 2
  1 / r;
  involutiveness;
end;

definition
  let r being non unit non zero Real;
  func op2(r) -> non unit non zero Real equals
:: ANPROJ10:def 3
  1 - r;
  involutiveness;
end;

reserve a,b,r for non unit non zero Real;

theorem :: ANPROJ10:2
  op2(op1(r)) = (r - 1) / r &
  op1(op2(r)) = 1 / (1 - r) &
  op1(op2(op1(r))) = r / (r - 1) &
  op2(op1(op2(r))) = r / (r - 1);

theorem :: ANPROJ10:3
  op2(op1(op2(op1(r)))) = op1(op2(r)) &
  op1(op2(op1(op2(r)))) = op2(op1(r));

theorem :: ANPROJ10:4
  op1(a) / op1(b) = b / a;

reserve X for non empty set,
        x for Tuple of 4,X;

theorem :: ANPROJ10:5
  4-tuples_on X = the set of all <* d1, d2, d3, d4 *> where
    d1,d2,d3,d4 is Element of X;

theorem :: ANPROJ10:6
  for a,b,c,d being object st (a = x.1 or a = x.2 or a = x.3 or a = x.4) &
  (b = x.1 or b = x.2 or b = x.3 or b = x.4) &
  (c = x.1 or c = x.2 or c = x.3 or c = x.4) &
  (d = x.1 or d = x.2 or d = x.3 or d = x.4) holds
  <* a,b,c,d *> is Tuple of 4,X;

definition
  let X be non empty set;
  let x be Tuple of 4,X;
  func pi_1342(x) -> Tuple of 4,X equals
:: ANPROJ10:def 4
<* x.1,x.3,x.4,x.2 *>;
  func pi_1423(x) -> Tuple of 4,X equals
:: ANPROJ10:def 5
<* x.1,x.4,x.2,x.3 *>;
  func pi_2143(x) -> Tuple of 4,X equals
:: ANPROJ10:def 6
<* x.2,x.1,x.4,x.3 *>;
  func pi_2314(x) -> Tuple of 4,X equals
:: ANPROJ10:def 7
<* x.2,x.3,x.1,x.4 *>;
  func pi_2341(x) -> Tuple of 4,X equals
:: ANPROJ10:def 8
<* x.2,x.3,x.4,x.1 *>;
  func pi_2413(x) -> Tuple of 4,X equals
:: ANPROJ10:def 9
<* x.2,x.4,x.1,x.3 *>;
  func pi_2431(x) -> Tuple of 4,X equals
:: ANPROJ10:def 10
<* x.2,x.4,x.3,x.1 *>;
  func pi_3124(x) -> Tuple of 4,X equals
:: ANPROJ10:def 11
<* x.3,x.1,x.2,x.4 *>;
  func pi_3142(x) -> Tuple of 4,X equals
:: ANPROJ10:def 12
<* x.3,x.1,x.4,x.2 *>;
  func pi_3241(x) -> Tuple of 4,X equals
:: ANPROJ10:def 13
<* x.3,x.2,x.4,x.1 *>;
  func pi_3412(x) -> Tuple of 4,X equals
:: ANPROJ10:def 14
<* x.3,x.4,x.1,x.2 *>;
  func pi_3421(x) -> Tuple of 4,X equals
:: ANPROJ10:def 15
<* x.3,x.4,x.2,x.1 *>;
  func pi_4123(x) -> Tuple of 4,X equals
:: ANPROJ10:def 16
<* x.4,x.1,x.2,x.3 *>;
  func pi_4132(x) -> Tuple of 4,X equals
:: ANPROJ10:def 17
<* x.4,x.1,x.3,x.2 *>;
  func pi_4213(x) -> Tuple of 4,X equals
:: ANPROJ10:def 18
<* x.4,x.2,x.1,x.3 *>;
  func pi_4312(x) -> Tuple of 4,X equals
:: ANPROJ10:def 19
<* x.4,x.3,x.1,x.2 *>;
  func pi_4321(x) -> Tuple of 4,X equals
:: ANPROJ10:def 20
<* x.4,x.3,x.2,x.1 *>;
end;

definition
  let X be non empty set;
  let x be Tuple of 4,X;
  func pi_id(x) -> Tuple of 4,X equals
:: ANPROJ10:def 21
<* x.1,x.2,x.3,x.4 *>;
  func pi_12(x) -> Tuple of 4,X equals
:: ANPROJ10:def 22
<* x.2,x.1,x.3,x.4 *>;
  involutiveness;
  func pi_13(x) -> Tuple of 4,X equals
:: ANPROJ10:def 23
<* x.3,x.2,x.1,x.4 *>;
  involutiveness;
  func pi_14(x) -> Tuple of 4,X equals
:: ANPROJ10:def 24
<* x.4,x.2,x.3,x.1 *>;
  involutiveness;
  func pi_23(x) -> Tuple of 4,X equals
:: ANPROJ10:def 25
<* x.1,x.3,x.2,x.4 *>;
  involutiveness;
  func pi_24(x) -> Tuple of 4,X equals
:: ANPROJ10:def 26
<* x.1,x.4,x.3,x.2 *>;
  involutiveness;
  func pi_34(x) -> Tuple of 4,X equals
:: ANPROJ10:def 27
<* x.1,x.2,x.4,x.3 *>;
  involutiveness;
end;

registration
  let X be non empty set;
  let x be Tuple of 4,X;
  reduce pi_id(x) to x;
end;

notation
  let X be non empty set;
  let x be Tuple of 4,X;
  synonym pi_1234(x) for pi_id(x);
  synonym pi_2134(x) for pi_12(x);
  synonym pi_3214(x) for pi_13(x);
  synonym pi_4231(x) for pi_14(x);
  synonym pi_1324(x) for pi_23(x);
  synonym pi_1432(x) for pi_24(x);
  synonym pi_1243(x) for pi_34(x);
end;

theorem :: ANPROJ10:7
  pi_12(pi_13(x)) = pi_13(pi_23(x)) &
  pi_12(pi_14(x)) = pi_14(pi_24(x)) &
  pi_12(pi_23(x)) = pi_13(pi_12(x)) &
  pi_12(pi_24(x)) = pi_14(pi_12(x)) &
  pi_12(pi_34(x)) = pi_34(pi_12(x)) &

  pi_13(pi_12(x)) = pi_23(pi_13(x)) &
  pi_13(pi_14(x)) = pi_34(pi_13(x)) &
  pi_13(pi_23(x)) = pi_12(pi_13(x)) &
  pi_13(pi_24(x)) = pi_13(pi_24(x)) &
  pi_13(pi_34(x)) = pi_14(pi_13(x)) &

  pi_23(pi_12(x)) = pi_13(pi_23(x)) &
  pi_23(pi_13(x)) = pi_12(pi_23(x)) &
  pi_23(pi_14(x)) = pi_14(pi_23(x)) &
  pi_23(pi_24(x)) = pi_34(pi_23(x)) &
  pi_23(pi_34(x)) = pi_24(pi_23(x)) &

  pi_24(pi_12(x)) = pi_14(pi_24(x)) &
  pi_24(pi_13(x)) = pi_13(pi_24(x)) &
  pi_24(pi_14(x)) = pi_12(pi_24(x)) &
  pi_24(pi_23(x)) = pi_34(pi_24(x)) &
  pi_24(pi_34(x)) = pi_23(pi_24(x)) &

  pi_34(pi_12(x)) = pi_12(pi_34(x)) &
  pi_34(pi_13(x)) = pi_14(pi_34(x)) &
  pi_34(pi_14(x)) = pi_13(pi_34(x)) &
  pi_34(pi_23(x)) = pi_24(pi_34(x)) &
  pi_34(pi_24(x)) = pi_23(pi_34(x));

theorem :: ANPROJ10:8
  pi_1342(x) = pi_34(pi_23(x)) &
  pi_1423(x) = pi_34(pi_24(x)) &
  pi_2143(x) = pi_12(pi_34(x)) &
  pi_2314(x) = pi_23(pi_12(x)) &
  pi_2341(x) = pi_34(pi_23(pi_12(x))) &
  pi_2413(x) = pi_34(pi_24(pi_12(x))) &
  pi_2431(x) = pi_24(pi_12(x)) &
  pi_3124(x) = pi_23(pi_13(x)) &
  pi_3142(x) = pi_24(pi_34(pi_13(x))) &
  pi_3241(x) = pi_34(pi_13(x)) &
  pi_3412(x) = pi_24(pi_13(x)) &
  pi_3421(x) = pi_24(pi_23(pi_13(x))) &
  pi_4123(x) = pi_23(pi_34(pi_14(x))) &
  pi_4132(x) = pi_24(pi_14(x)) &
  pi_4213(x) = pi_34(pi_14(x)) &
  pi_4312(x) = pi_23(pi_24(pi_14(x))) &
  pi_4321(x) = pi_23(pi_14(x));

theorem :: ANPROJ10:9
  pi_13(pi_23(pi_13(x))) = pi_12(x) &
  pi_12(pi_34(pi_23(pi_13(x)))) = pi_34(pi_23(x)) &
  pi_23(pi_24(pi_14(pi_23(pi_13(x))))) = pi_14(x);

theorem :: ANPROJ10:10
  pi_23(pi_14(pi_34(x))) = pi_24(pi_23(pi_13(x))) &
  pi_34(pi_24(pi_12(x))) = pi_24(pi_13(pi_23(x))) &
  pi_24(pi_34(pi_13(x))) = pi_12(pi_34(pi_23(x)));

begin :: Affine-Ratio

reserve V             for RealLinearSpace,
        A,B,C,P,Q,R,S for Element of V;

theorem :: ANPROJ10:11
  P,Q,Q are_collinear;

definition
  let V be RealLinearSpace;
  let A,B,C be Element of V;
  assume that
 A <> C and
 A,B,C are_collinear;
  func affine-ratio(A,B,C) -> Real means
:: ANPROJ10:def 28
  (B - A) = it * (C - A);
end;

theorem :: ANPROJ10:12
  A <> C & A,B,C are_collinear implies
  A - B = affine-ratio(A,B,C) * (A - C);

theorem :: ANPROJ10:13
  A <> C & A,B,C are_collinear implies
  (affine-ratio(A,B,C) = 0 iff A = B);

theorem :: ANPROJ10:14
  A <> C & A,B,C are_collinear implies
  (affine-ratio(A,B,C) = 1 iff B = C);

theorem :: ANPROJ10:15
  for a,b being Real st P <> Q & a * (P - Q) = b * (P - Q) holds a = b;

theorem :: ANPROJ10:16
  P,Q,R are_collinear & P <> R & P <> Q implies
  affine-ratio(P,R,Q) = 1 / affine-ratio(P,Q,R);

theorem :: ANPROJ10:17
  P,Q,R are_collinear & P <> R & Q <> R & P <> Q implies
  affine-ratio(Q,P,R) =
    affine-ratio(P,Q,R) / (affine-ratio(P,Q,R) - 1);

theorem :: ANPROJ10:18
  P,Q,R are_collinear & P <> R implies
  affine-ratio(R,Q,P) = 1 - affine-ratio(P,Q,R);

theorem :: ANPROJ10:19
  P,Q,R are_collinear & P <> R & P <> Q implies
  affine-ratio(Q,R,P) =
  (affine-ratio(P,Q,R) - 1) / affine-ratio(P,Q,R);

theorem :: ANPROJ10:20
  P,Q,R are_collinear & P <> R & Q <> R implies
  affine-ratio(R,P,Q) = 1 / (1 - affine-ratio(P,Q,R));

theorem :: ANPROJ10:21
  for r being Real st P,Q,R are_collinear &
  P <> R & Q <> R & P <> Q &
  r = affine-ratio(P,Q,R) holds
  affine-ratio(P,R,Q) = 1 / r &
  affine-ratio(Q,P,R) = r / (r - 1) &
  affine-ratio(Q,R,P) = (r - 1) / r &
  affine-ratio(R,P,Q) = 1 / (1 - r) &
  affine-ratio(R,Q,P) = 1 - r;

theorem :: ANPROJ10:22
  for a being non zero Real st P,Q,R are_collinear & P <> R holds
  affine-ratio(P,Q,R) = affine-ratio(a * P,a * Q,a * R);

theorem :: ANPROJ10:23
  for x,y being Element of REAL 1
  for p,q being Tuple of 1,REAL st
  p = x & q = y holds x + y = p + q;

theorem :: ANPROJ10:24
  for x,y being Element of TOP-REAL 1
  for p,q being Tuple of 1,REAL st
  p = x & q = y holds x + y = p + q;

theorem :: ANPROJ10:25
  for x,y being Element of TOP-REAL 1
  for p,q being Tuple of 1,REAL st
  p = x & q = y holds x - y = p - q;

theorem :: ANPROJ10:26
  for x being Element of TOP-REAL 1
  for p being Tuple of 1,REAL st
  p = x holds - x = - p;

theorem :: ANPROJ10:27
  for T being RealLinearSpace
  for x,y being Element of T
  for p,q being Tuple of 1,REAL st
  T = TOP-REAL 1 & p = x & q = y
  holds x + y = p + q;

theorem :: ANPROJ10:28
  for p being Tuple of 1,REAL holds - p is Tuple of 1,REAL;

theorem :: ANPROJ10:29
  for T being RealLinearSpace
  for x being Element of T
  for p being Tuple of 1,REAL st
  T = TOP-REAL 1 & p = x
  holds - p = - x;

theorem :: ANPROJ10:30
  for T being RealLinearSpace
  for x being Element of T
  for p being Element of TOP-REAL 1 st
  T = TOP-REAL 1 & p = x
  holds - p = - x;

theorem :: ANPROJ10:31
  for T being RealLinearSpace
  for x,y being Element of T
  for p,q being Tuple of 1,REAL st
  T = TOP-REAL 1 & p = x & q = y
  holds x - y = p - q;

theorem :: ANPROJ10:32
  for T being RealLinearSpace
  for x,y being Element of T
  for p,q being Element of TOP-REAL 1 st
  T = TOP-REAL 1 & p = x & q = y
  holds x + y = p + q;

theorem :: ANPROJ10:33
  for D being set
  for d being Element of D holds Seg 1 --> d = <* d *>;

theorem :: ANPROJ10:34
  for a,r being Real holds
  multreal.:( Seg 1 --> a, <* r *> ) = <* a * r *>;

theorem :: ANPROJ10:35
  for a being Real for p being Tuple of 1,REAL holds
  multreal.:(dom p --> a,p) = a * p;

theorem :: ANPROJ10:36
  for a being Real for p being Tuple of 1,REAL holds
  multreal.:(dom p --> a,p) = a * p;

theorem :: ANPROJ10:37
  for T being RealLinearSpace for x,y being Element of T
  for a being Real for p,q being Tuple of 1,REAL st
  T = TOP-REAL 1 & p = x & q = y & x = a * y holds p = a * q;

theorem :: ANPROJ10:38
  for T being RealLinearSpace for x,y being Element of T
  for a being Real for p,q being Element of TOP-REAL 1 st
  T = TOP-REAL 1 & p = x & q = y holds x = a * y implies p = a * q;

theorem :: ANPROJ10:39
  for T being RealLinearSpace for x,y being Element of T
  for p,q being Element of TOP-REAL 1 st T = TOP-REAL 1 & p = x & q = y
  holds x - y = p - q;

theorem :: ANPROJ10:40
  for p,q being Tuple of 1,REAL for r being Real st
  p = r * q & p <> <* 0 *> holds ex a,b being Real st
  p = <* a *> & q =<* b *> & r = a / b;

theorem :: ANPROJ10:41
  for x,y,z being Element of TOP-REAL 1 holds x,y,z are_collinear;

theorem :: ANPROJ10:42
  for T being RealLinearSpace st T = TOP-REAL 1
  for x,y,z being Element of T holds x,y,z are_collinear;

theorem :: ANPROJ10:43
  for T being RealLinearSpace st T = TOP-REAL 1
  for x,y,z being Element of T st z <> x & y <> x holds
  ex a,b,c being Real st x = <* a *> & y = <* b *> & z = <* c *> &
  affine-ratio(x,y,z) = (b - a) / (c - a);

theorem :: ANPROJ10:44
  for x being Element of TOP-REAL 1 for a,r being Real st
  x = <* a *> holds r * x = <* (r * a) *>;

theorem :: ANPROJ10:45
  for x,y being Element of TOP-REAL 1 for a,b,r being Real st
  x = <* a *> & y = <* b *> holds x = r * y iff a = r * b;

theorem :: ANPROJ10:46
  for x,y being Element of TOP-REAL 1 for a,b being Real st
  x = <* a *> & y = <* b *> holds x - y = <* a - b *>;

theorem :: ANPROJ10:47
  for V being RealLinearSpace for x,y being Element of F_Real
  for x9,y9 being Element of V st V = F_Real & x = x9 & y = y9 holds
  x + y = x9 + y9;

theorem :: ANPROJ10:48
  for V being RealLinearSpace for P,Q,R being Element of V st
  P,Q,R are_collinear & P <> R & Q <> R & P <> Q holds
  affine-ratio(P,Q,R) <> 0 & affine-ratio(P,Q,R) <> 1;

theorem :: ANPROJ10:49
  for V being RealLinearSpace for P,Q,R being Element of V st
  P,Q,R are_collinear & P <> R & Q <> R & P <> Q holds
  ex r being non unit non zero Real st
  r = affine-ratio(P,Q,R) &
  affine-ratio(P,R,Q) = op1(r) &
  affine-ratio(Q,P,R) = op1(op2(op1(r))) &
  affine-ratio(Q,R,P) = op2(op1(r)) &
  affine-ratio(R,P,Q) = op1(op2(r)) &
  affine-ratio(R,Q,P) = op2(r);

begin :: Cross-Ratio

theorem :: ANPROJ10:50
  for X being non empty set
  for x being Tuple of 4,X
  for P,Q,R,S being Element of X st x = <* P,Q,R,S *> holds
  pi_1234(x) = <* P, Q, R, S *> &
  pi_1243(x) = <* P, Q, S, R *> &
  pi_1324(x) = <* P, R, Q, S *> &
  pi_1342(x) = <* P, R, S, Q *> &
  pi_1423(x) = <* P, S, Q, R *> &
  pi_1432(x) = <* P, S, R, Q *> &
  pi_2134(x) = <* Q, P, R, S *> &
  pi_2143(x) = <* Q, P, S, R *> &
  pi_2314(x) = <* Q, R, P, S *> &
  pi_2341(x) = <* Q, R, S, P *> &
  pi_2413(x) = <* Q, S, P, R *> &
  pi_2431(x) = <* Q, S, R, P *> &
  pi_3124(x) = <* R, P, Q, S *> &
  pi_3142(x) = <* R, P, S, Q *> &
  pi_3214(x) = <* R, Q, P, S *> &
  pi_3241(x) = <* R, Q, S, P *> &
  pi_3412(x) = <* R, S, P, Q *> &
  pi_3421(x) = <* R, S, Q ,P *> &
  pi_4123(x) = <* S, P, Q, R *> &
  pi_4132(x) = <* S, P, R, Q *> &
  pi_4213(x) = <* S, Q, P, R *> &
  pi_4231(x) = <* S, Q, R, P *> &
  pi_4312(x) = <* S, R, P, Q *> &
  pi_4321(x) = <* S, R, Q, P *>;

theorem :: ANPROJ10:51
  for X being non empty set
  for x being Tuple of 4,X holds
  pi_1324(pi_1243(x)) = pi_1423(x) & pi_2143(pi_1243(x)) = pi_2134(x) &
  pi_3412(pi_1243(x)) = pi_4312(x) & pi_4321(pi_1243(x)) = pi_3421(x) &
  pi_3412(pi_1324(x)) = pi_2413(x) & pi_2143(pi_1324(x)) = pi_3142(x) &
  pi_4321(pi_1324(x)) = pi_4231(x) & pi_3412(pi_1423(x)) = pi_2314(x) &
  pi_2143(pi_1423(x)) = pi_4132(x) & pi_4321(pi_1423(x)) = pi_3241(x) &
  pi_1243(pi_1423(x)) = pi_1432(x) & pi_4321(pi_1432(x)) = pi_2341(x) &
  pi_3412(pi_1432(x)) = pi_3214(x) & pi_2143(pi_1432(x)) = pi_4123(x) &
  pi_4321(pi_3124(x)) = pi_4213(x) & pi_3412(pi_3124(x)) = pi_2431(x) &
  pi_2143(pi_3124(x)) = pi_1342(x) & pi_4312(pi_3124(x)) = pi_4231(x) &
  pi_4321(pi_3124(x)) = pi_4213(x);

reserve x           for Tuple of 4,the carrier of V,
        P9,Q9,R9,S9 for Element of V;

definition
  let V being RealLinearSpace;
  let P,Q,R,S being Element of V;
  func cross-ratio(P,Q,R,S) -> Real equals
:: ANPROJ10:def 29
  affine-ratio(R,P,Q) / affine-ratio(S,P,Q);
end;

theorem :: ANPROJ10:52
  P,Q,R,S are_collinear & R <> Q & S <> Q & S <> P implies
  (R = P iff cross-ratio(P,Q,R,S) = 0);

theorem :: ANPROJ10:53
  P <> R & P <> S implies cross-ratio(P,P,R,S) = 1;

theorem :: ANPROJ10:54
  P,Q,R,S are_collinear & R <> Q & S <> Q & R <> S &
  cross-ratio(P,Q,R,S) = 1 implies P = Q;

theorem :: ANPROJ10:55
  P,Q,R,S are_collinear & P9,Q9,R9,S9 are_collinear & S <> P & S <> Q &
  S9 <> P9 & S9 <> Q9 implies
  (cross-ratio(P,Q,R,S) = cross-ratio(P9,Q9,R9,S9) iff
  affine-ratio(R,P,Q) * affine-ratio(S9,P9,Q9) =
  affine-ratio(R9,P9,Q9) * affine-ratio(S,P,Q));

theorem :: ANPROJ10:56
  P,Q,R,S are_collinear & P <> S & R <> Q & S <> Q implies
  cross-ratio(P,Q,R,S) = cross-ratio(R,S,P,Q);

theorem :: ANPROJ10:57
  for V being RealLinearSpace for P,Q,R,S being Element of V st
  P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q holds
  cross-ratio(P,Q,R,S) = cross-ratio(Q,P,S,R);

theorem :: ANPROJ10:58
  P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies
  cross-ratio(P,Q,R,S) = cross-ratio(S,R,Q,P);

theorem :: ANPROJ10:59
  cross-ratio(P,Q,S,R) = 1 / cross-ratio(P,Q,R,S);

theorem :: ANPROJ10:60
  P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies
  cross-ratio(Q,P,R,S) = 1 / cross-ratio(P,Q,R,S);

theorem :: ANPROJ10:61
  P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies
  cross-ratio(R,S,Q,P) = 1 / cross-ratio(P,Q,R,S);

theorem :: ANPROJ10:62
  P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies
  cross-ratio(S,R,P,Q) = 1 / cross-ratio(P,Q,R,S);

theorem :: ANPROJ10:63
  P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct implies
  cross-ratio(P,R,Q,S) = 1 - cross-ratio(P,Q,R,S);

theorem :: ANPROJ10:64
  P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct implies
  cross-ratio(Q,S,P,R) = 1 - cross-ratio(P,Q,R,S);

theorem :: ANPROJ10:65
  P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct implies
  cross-ratio(R,P,S,Q) = 1 - cross-ratio(P,Q,R,S);

theorem :: ANPROJ10:66
  P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct implies
  cross-ratio(S,Q,R,P) = 1 - cross-ratio(P,Q,R,S);

definition
  let V being RealLinearSpace;
  let x being Tuple of 4,the carrier of V;
  func cross-ratio-tuple(x) -> Real means
:: ANPROJ10:def 30
  ex P,Q,R,S being Element of V st P = x.1 & Q = x.2 & R = x.3 &
  S = x.4 & it = cross-ratio(P,Q,R,S);
end;

theorem :: ANPROJ10:67
  x = <* P, Q, R, S *> implies
  cross-ratio(P,Q,R,S) = cross-ratio-tuple(x);

theorem :: ANPROJ10:68
  x = <* P, Q, R, S *> & P,Q,R,S are_collinear &
  P <> S & Q <> R & Q <> S implies
  cross-ratio-tuple(x) = cross-ratio-tuple(pi_3412(x));

theorem :: ANPROJ10:69
  x = <* P, Q, R, S *> & P,Q,R,S are_collinear & P <> R & P <> S &
  Q <> R & Q <> S implies
  cross-ratio-tuple(x) = cross-ratio-tuple(pi_2143(x)) &
  cross-ratio-tuple(x) = cross-ratio-tuple(pi_4321(x));

theorem :: ANPROJ10:70
  cross-ratio-tuple(pi_1243(x)) = 1 / cross-ratio-tuple(x);

theorem :: ANPROJ10:71
  x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct &
  P,Q,R,S are_collinear implies
  (ex r being non unit non zero Real st r = cross-ratio-tuple(x) &
  cross-ratio-tuple(pi_1243(x)) = op1(r));

theorem :: ANPROJ10:72
  x = <*P,Q,R,S*> & P,Q,R,S are_collinear & P <> R & P <> S &
  Q <> R & Q <> S implies
  cross-ratio-tuple(pi_1243(x)) = 1 / cross-ratio-tuple(x) &
  cross-ratio-tuple(pi_2134(x)) = 1 / cross-ratio-tuple(x) &
  cross-ratio-tuple(pi_3421(x)) = 1 / cross-ratio-tuple(x) &
  cross-ratio-tuple(pi_4312(x)) = 1 / cross-ratio-tuple(x);

theorem :: ANPROJ10:73
  x = <* P,Q,R,S *> & P,Q,R,S are_mutually_distinct &
  P,Q,R,S are_collinear implies
  cross-ratio-tuple(pi_1324(x)) = 1 - cross-ratio-tuple(x) &
  cross-ratio-tuple(pi_2413(x)) = 1 - cross-ratio-tuple(x) &
  cross-ratio-tuple(pi_3142(x)) = 1 - cross-ratio-tuple(x) &
  cross-ratio-tuple(pi_4231(x)) = 1 - cross-ratio-tuple(x);

theorem :: ANPROJ10:74
  x = <* P,Q,R,S *> & P,Q,R,S are_mutually_distinct &
  P,Q,R,S are_collinear implies
  cross-ratio-tuple(pi_3124(x)) = 1 / (1 - cross-ratio-tuple(x)) &
  cross-ratio-tuple(pi_2431(x)) = 1 / (1 - cross-ratio-tuple(x)) &
  cross-ratio-tuple(pi_1342(x)) = 1 / (1 - cross-ratio-tuple(x)) &
  cross-ratio-tuple(pi_4213(x)) = 1 / (1 - cross-ratio-tuple(x));

theorem :: ANPROJ10:75
  x = <* P,Q,R,S *> & P,Q,R,S are_mutually_distinct &
  P,Q,R,S are_collinear implies
  cross-ratio-tuple(pi_1423(x))
    = (cross-ratio-tuple(x) - 1) / cross-ratio-tuple(x) &
  cross-ratio-tuple(pi_2314(x))
    = (cross-ratio-tuple(x) - 1) / cross-ratio-tuple(x) &
  cross-ratio-tuple(pi_4132(x))
    = (cross-ratio-tuple(x) - 1) / cross-ratio-tuple(x) &
  cross-ratio-tuple(pi_3241(x))
    = (cross-ratio-tuple(x) - 1) / cross-ratio-tuple(x);

theorem :: ANPROJ10:76
  x = <* P,Q,R,S *> & P,Q,R,S are_mutually_distinct &
  P,Q,R,S are_collinear implies
  cross-ratio-tuple(pi_1432(x))
    = cross-ratio-tuple(x) / (cross-ratio-tuple(x) - 1) &
  cross-ratio-tuple(pi_2341(x))
    = cross-ratio-tuple(x) / (cross-ratio-tuple(x) - 1) &
  cross-ratio-tuple(pi_3214(x))
    = cross-ratio-tuple(x) / (cross-ratio-tuple(x) - 1) &
  cross-ratio-tuple(pi_4123(x))
    = cross-ratio-tuple(x) / (cross-ratio-tuple(x) - 1);

begin

theorem :: ANPROJ10:77
  for x1,x2,x3,x4 being Element of TOP-REAL 1 st
  x2 <> x3 & x3 <> x1 & x2 <> x4 & x1 <> x4 holds
  ex a,b,c,d being Real st x1 = <* a *> & x2 =  <* b *> & x3 = <* c *> &
  x4 = <* d *> & cross-ratio-tuple(<*x1,x2,x3,x4*>)
    = ((c - a) / (c - b)) * ((d - b) / (d - a));