:: {C}ross-ratio in Real Vector Space
:: by Roland Coghetto
::
:: Copyright (c) 2019 Association of Mizar Users

registration
let a, b, c, d be object ;
reduce <*a,b,c,d*> . 1 to a;
reducibility
<*a,b,c,d*> . 1 = a
by FINSEQ_4:76;
reduce <*a,b,c,d*> . 2 to b;
reducibility
<*a,b,c,d*> . 2 = b
by FINSEQ_4:76;
reduce <*a,b,c,d*> . 3 to c;
reducibility
<*a,b,c,d*> . 3 = c
by FINSEQ_4:76;
reduce <*a,b,c,d*> . 4 to d;
reducibility
<*a,b,c,d*> . 4 = d
by FINSEQ_4:76;
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 )
proof end;

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

:: deftheorem Def01 defines unit ANPROJ10:def 1 :
for r being Real holds
( r is unit iff r = 1 );

registration
cluster non zero V109() V118() complex non unit for object ;
existence
not for b1 being non zero Real holds b1 is unit
proof end;
end;

definition
let r be non zero non unit Real;
func op1 r -> non zero non unit Real equals :: ANPROJ10:def 2
1 / r;
coherence
1 / r is non zero non unit Real
proof end;
involutiveness
for b1, b2 being non zero non unit Real st b1 = 1 / b2 holds
b2 = 1 / b1
;
end;

:: deftheorem defines op1 ANPROJ10:def 2 :
for r being non zero non unit Real holds op1 r = 1 / r;

definition
let r be non zero non unit Real;
func op2 r -> non zero non unit Real equals :: ANPROJ10:def 3
1 - r;
coherence
1 - r is non zero non unit Real
proof end;
involutiveness
for b1, b2 being non zero non unit Real st b1 = 1 - b2 holds
b2 = 1 - b1
;
end;

:: deftheorem defines op2 ANPROJ10:def 3 :
for r being non zero non unit Real holds op2 r = 1 - r;

theorem Th01: :: ANPROJ10:2
for r being non zero non unit Real holds
( 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) )
proof end;

theorem :: ANPROJ10:3
for r being non zero non unit Real holds
( op2 (op1 (op2 (op1 r))) = op1 (op2 r) & op1 (op2 (op1 (op2 r))) = op2 (op1 r) )
proof end;

theorem :: ANPROJ10:4
for a, b being non zero non unit Real holds (op1 a) / (op1 b) = b / a ;

theorem Th02: :: ANPROJ10:5
for X being non empty set holds 4 -tuples_on X = { <*d1,d2,d3,d4*> where d1, d2, d3, d4 is Element of X : verum }
proof end;

theorem Th03: :: ANPROJ10:6
for X being non empty set
for x being Tuple of 4,X
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
proof end;

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)*>;
coherence
<*(x . 1),(x . 3),(x . 4),(x . 2)*> is Tuple of 4,X
by Th03;
func pi_1423 x -> Tuple of 4,X equals :: ANPROJ10:def 5
<*(x . 1),(x . 4),(x . 2),(x . 3)*>;
coherence
<*(x . 1),(x . 4),(x . 2),(x . 3)*> is Tuple of 4,X
by Th03;
func pi_2143 x -> Tuple of 4,X equals :: ANPROJ10:def 6
<*(x . 2),(x . 1),(x . 4),(x . 3)*>;
coherence
<*(x . 2),(x . 1),(x . 4),(x . 3)*> is Tuple of 4,X
by Th03;
func pi_2314 x -> Tuple of 4,X equals :: ANPROJ10:def 7
<*(x . 2),(x . 3),(x . 1),(x . 4)*>;
coherence
<*(x . 2),(x . 3),(x . 1),(x . 4)*> is Tuple of 4,X
by Th03;
func pi_2341 x -> Tuple of 4,X equals :: ANPROJ10:def 8
<*(x . 2),(x . 3),(x . 4),(x . 1)*>;
coherence
<*(x . 2),(x . 3),(x . 4),(x . 1)*> is Tuple of 4,X
by Th03;
func pi_2413 x -> Tuple of 4,X equals :: ANPROJ10:def 9
<*(x . 2),(x . 4),(x . 1),(x . 3)*>;
coherence
<*(x . 2),(x . 4),(x . 1),(x . 3)*> is Tuple of 4,X
by Th03;
func pi_2431 x -> Tuple of 4,X equals :: ANPROJ10:def 10
<*(x . 2),(x . 4),(x . 3),(x . 1)*>;
coherence
<*(x . 2),(x . 4),(x . 3),(x . 1)*> is Tuple of 4,X
by Th03;
func pi_3124 x -> Tuple of 4,X equals :: ANPROJ10:def 11
<*(x . 3),(x . 1),(x . 2),(x . 4)*>;
coherence
<*(x . 3),(x . 1),(x . 2),(x . 4)*> is Tuple of 4,X
by Th03;
func pi_3142 x -> Tuple of 4,X equals :: ANPROJ10:def 12
<*(x . 3),(x . 1),(x . 4),(x . 2)*>;
coherence
<*(x . 3),(x . 1),(x . 4),(x . 2)*> is Tuple of 4,X
by Th03;
func pi_3241 x -> Tuple of 4,X equals :: ANPROJ10:def 13
<*(x . 3),(x . 2),(x . 4),(x . 1)*>;
coherence
<*(x . 3),(x . 2),(x . 4),(x . 1)*> is Tuple of 4,X
by Th03;
func pi_3412 x -> Tuple of 4,X equals :: ANPROJ10:def 14
<*(x . 3),(x . 4),(x . 1),(x . 2)*>;
coherence
<*(x . 3),(x . 4),(x . 1),(x . 2)*> is Tuple of 4,X
by Th03;
func pi_3421 x -> Tuple of 4,X equals :: ANPROJ10:def 15
<*(x . 3),(x . 4),(x . 2),(x . 1)*>;
coherence
<*(x . 3),(x . 4),(x . 2),(x . 1)*> is Tuple of 4,X
by Th03;
func pi_4123 x -> Tuple of 4,X equals :: ANPROJ10:def 16
<*(x . 4),(x . 1),(x . 2),(x . 3)*>;
coherence
<*(x . 4),(x . 1),(x . 2),(x . 3)*> is Tuple of 4,X
by Th03;
func pi_4132 x -> Tuple of 4,X equals :: ANPROJ10:def 17
<*(x . 4),(x . 1),(x . 3),(x . 2)*>;
coherence
<*(x . 4),(x . 1),(x . 3),(x . 2)*> is Tuple of 4,X
by Th03;
func pi_4213 x -> Tuple of 4,X equals :: ANPROJ10:def 18
<*(x . 4),(x . 2),(x . 1),(x . 3)*>;
coherence
<*(x . 4),(x . 2),(x . 1),(x . 3)*> is Tuple of 4,X
by Th03;
func pi_4312 x -> Tuple of 4,X equals :: ANPROJ10:def 19
<*(x . 4),(x . 3),(x . 1),(x . 2)*>;
coherence
<*(x . 4),(x . 3),(x . 1),(x . 2)*> is Tuple of 4,X
by Th03;
func pi_4321 x -> Tuple of 4,X equals :: ANPROJ10:def 20
<*(x . 4),(x . 3),(x . 2),(x . 1)*>;
coherence
<*(x . 4),(x . 3),(x . 2),(x . 1)*> is Tuple of 4,X
by Th03;
end;

:: deftheorem defines pi_1342 ANPROJ10:def 4 :
for X being non empty set
for x being Tuple of 4,X holds pi_1342 x = <*(x . 1),(x . 3),(x . 4),(x . 2)*>;

:: deftheorem defines pi_1423 ANPROJ10:def 5 :
for X being non empty set
for x being Tuple of 4,X holds pi_1423 x = <*(x . 1),(x . 4),(x . 2),(x . 3)*>;

:: deftheorem defines pi_2143 ANPROJ10:def 6 :
for X being non empty set
for x being Tuple of 4,X holds pi_2143 x = <*(x . 2),(x . 1),(x . 4),(x . 3)*>;

:: deftheorem defines pi_2314 ANPROJ10:def 7 :
for X being non empty set
for x being Tuple of 4,X holds pi_2314 x = <*(x . 2),(x . 3),(x . 1),(x . 4)*>;

:: deftheorem defines pi_2341 ANPROJ10:def 8 :
for X being non empty set
for x being Tuple of 4,X holds pi_2341 x = <*(x . 2),(x . 3),(x . 4),(x . 1)*>;

:: deftheorem defines pi_2413 ANPROJ10:def 9 :
for X being non empty set
for x being Tuple of 4,X holds pi_2413 x = <*(x . 2),(x . 4),(x . 1),(x . 3)*>;

:: deftheorem defines pi_2431 ANPROJ10:def 10 :
for X being non empty set
for x being Tuple of 4,X holds pi_2431 x = <*(x . 2),(x . 4),(x . 3),(x . 1)*>;

:: deftheorem defines pi_3124 ANPROJ10:def 11 :
for X being non empty set
for x being Tuple of 4,X holds pi_3124 x = <*(x . 3),(x . 1),(x . 2),(x . 4)*>;

:: deftheorem defines pi_3142 ANPROJ10:def 12 :
for X being non empty set
for x being Tuple of 4,X holds pi_3142 x = <*(x . 3),(x . 1),(x . 4),(x . 2)*>;

:: deftheorem defines pi_3241 ANPROJ10:def 13 :
for X being non empty set
for x being Tuple of 4,X holds pi_3241 x = <*(x . 3),(x . 2),(x . 4),(x . 1)*>;

:: deftheorem defines pi_3412 ANPROJ10:def 14 :
for X being non empty set
for x being Tuple of 4,X holds pi_3412 x = <*(x . 3),(x . 4),(x . 1),(x . 2)*>;

:: deftheorem defines pi_3421 ANPROJ10:def 15 :
for X being non empty set
for x being Tuple of 4,X holds pi_3421 x = <*(x . 3),(x . 4),(x . 2),(x . 1)*>;

:: deftheorem defines pi_4123 ANPROJ10:def 16 :
for X being non empty set
for x being Tuple of 4,X holds pi_4123 x = <*(x . 4),(x . 1),(x . 2),(x . 3)*>;

:: deftheorem defines pi_4132 ANPROJ10:def 17 :
for X being non empty set
for x being Tuple of 4,X holds pi_4132 x = <*(x . 4),(x . 1),(x . 3),(x . 2)*>;

:: deftheorem defines pi_4213 ANPROJ10:def 18 :
for X being non empty set
for x being Tuple of 4,X holds pi_4213 x = <*(x . 4),(x . 2),(x . 1),(x . 3)*>;

:: deftheorem defines pi_4312 ANPROJ10:def 19 :
for X being non empty set
for x being Tuple of 4,X holds pi_4312 x = <*(x . 4),(x . 3),(x . 1),(x . 2)*>;

:: deftheorem defines pi_4321 ANPROJ10:def 20 :
for X being non empty set
for x being Tuple of 4,X holds pi_4321 x = <*(x . 4),(x . 3),(x . 2),(x . 1)*>;

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)*>;
coherence
<*(x . 1),(x . 2),(x . 3),(x . 4)*> is Tuple of 4,X
by Th03;
func pi_12 x -> Tuple of 4,X equals :: ANPROJ10:def 22
<*(x . 2),(x . 1),(x . 3),(x . 4)*>;
coherence
<*(x . 2),(x . 1),(x . 3),(x . 4)*> is Tuple of 4,X
by Th03;
involutiveness
for b1, b2 being Tuple of 4,X st b1 = <*(b2 . 2),(b2 . 1),(b2 . 3),(b2 . 4)*> holds
b2 = <*(b1 . 2),(b1 . 1),(b1 . 3),(b1 . 4)*>
proof end;
func pi_13 x -> Tuple of 4,X equals :: ANPROJ10:def 23
<*(x . 3),(x . 2),(x . 1),(x . 4)*>;
coherence
<*(x . 3),(x . 2),(x . 1),(x . 4)*> is Tuple of 4,X
by Th03;
involutiveness
for b1, b2 being Tuple of 4,X st b1 = <*(b2 . 3),(b2 . 2),(b2 . 1),(b2 . 4)*> holds
b2 = <*(b1 . 3),(b1 . 2),(b1 . 1),(b1 . 4)*>
proof end;
func pi_14 x -> Tuple of 4,X equals :: ANPROJ10:def 24
<*(x . 4),(x . 2),(x . 3),(x . 1)*>;
coherence
<*(x . 4),(x . 2),(x . 3),(x . 1)*> is Tuple of 4,X
by Th03;
involutiveness
for b1, b2 being Tuple of 4,X st b1 = <*(b2 . 4),(b2 . 2),(b2 . 3),(b2 . 1)*> holds
b2 = <*(b1 . 4),(b1 . 2),(b1 . 3),(b1 . 1)*>
proof end;
func pi_23 x -> Tuple of 4,X equals :: ANPROJ10:def 25
<*(x . 1),(x . 3),(x . 2),(x . 4)*>;
coherence
<*(x . 1),(x . 3),(x . 2),(x . 4)*> is Tuple of 4,X
by Th03;
involutiveness
for b1, b2 being Tuple of 4,X st b1 = <*(b2 . 1),(b2 . 3),(b2 . 2),(b2 . 4)*> holds
b2 = <*(b1 . 1),(b1 . 3),(b1 . 2),(b1 . 4)*>
proof end;
func pi_24 x -> Tuple of 4,X equals :: ANPROJ10:def 26
<*(x . 1),(x . 4),(x . 3),(x . 2)*>;
coherence
<*(x . 1),(x . 4),(x . 3),(x . 2)*> is Tuple of 4,X
by Th03;
involutiveness
for b1, b2 being Tuple of 4,X st b1 = <*(b2 . 1),(b2 . 4),(b2 . 3),(b2 . 2)*> holds
b2 = <*(b1 . 1),(b1 . 4),(b1 . 3),(b1 . 2)*>
proof end;
func pi_34 x -> Tuple of 4,X equals :: ANPROJ10:def 27
<*(x . 1),(x . 2),(x . 4),(x . 3)*>;
coherence
<*(x . 1),(x . 2),(x . 4),(x . 3)*> is Tuple of 4,X
by Th03;
involutiveness
for b1, b2 being Tuple of 4,X st b1 = <*(b2 . 1),(b2 . 2),(b2 . 4),(b2 . 3)*> holds
b2 = <*(b1 . 1),(b1 . 2),(b1 . 4),(b1 . 3)*>
proof end;
end;

:: deftheorem defines pi_id ANPROJ10:def 21 :
for X being non empty set
for x being Tuple of 4,X holds pi_id x = <*(x . 1),(x . 2),(x . 3),(x . 4)*>;

:: deftheorem defines pi_12 ANPROJ10:def 22 :
for X being non empty set
for x being Tuple of 4,X holds pi_12 x = <*(x . 2),(x . 1),(x . 3),(x . 4)*>;

:: deftheorem defines pi_13 ANPROJ10:def 23 :
for X being non empty set
for x being Tuple of 4,X holds pi_13 x = <*(x . 3),(x . 2),(x . 1),(x . 4)*>;

:: deftheorem defines pi_14 ANPROJ10:def 24 :
for X being non empty set
for x being Tuple of 4,X holds pi_14 x = <*(x . 4),(x . 2),(x . 3),(x . 1)*>;

:: deftheorem defines pi_23 ANPROJ10:def 25 :
for X being non empty set
for x being Tuple of 4,X holds pi_23 x = <*(x . 1),(x . 3),(x . 2),(x . 4)*>;

:: deftheorem defines pi_24 ANPROJ10:def 26 :
for X being non empty set
for x being Tuple of 4,X holds pi_24 x = <*(x . 1),(x . 4),(x . 3),(x . 2)*>;

:: deftheorem defines pi_34 ANPROJ10:def 27 :
for X being non empty set
for x being Tuple of 4,X holds pi_34 x = <*(x . 1),(x . 2),(x . 4),(x . 3)*>;

registration
let X be non empty set ;
let x be Tuple of 4,X;
reduce pi_id x to x;
reducibility
pi_id x = x
proof end;
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
for X being non empty set
for x being Tuple of 4,X holds
( pi_12 () = pi_13 () & pi_12 () = pi_14 () & pi_12 () = pi_13 () & pi_12 () = pi_14 () & pi_12 () = pi_34 () & pi_13 () = pi_23 () & pi_13 () = pi_34 () & pi_13 () = pi_12 () & pi_13 () = pi_13 () & pi_13 () = pi_14 () & pi_23 () = pi_13 () & pi_23 () = pi_12 () & pi_23 () = pi_14 () & pi_23 () = pi_34 () & pi_23 () = pi_24 () & pi_24 () = pi_14 () & pi_24 () = pi_13 () & pi_24 () = pi_12 () & pi_24 () = pi_34 () & pi_24 () = pi_23 () & pi_34 () = pi_12 () & pi_34 () = pi_14 () & pi_34 () = pi_13 () & pi_34 () = pi_24 () & pi_34 () = pi_23 () ) ;

theorem :: ANPROJ10:8
for X being non empty set
for x being Tuple of 4,X holds
( pi_1342 x = pi_34 () & pi_1423 x = pi_34 () & pi_2143 x = pi_12 () & pi_2314 x = pi_23 () & pi_2341 x = pi_34 (pi_23 ()) & pi_2413 x = pi_34 (pi_24 ()) & pi_2431 x = pi_24 () & pi_3124 x = pi_23 () & pi_3142 x = pi_24 (pi_34 ()) & pi_3241 x = pi_34 () & pi_3412 x = pi_24 () & pi_3421 x = pi_24 (pi_23 ()) & pi_4123 x = pi_23 (pi_34 ()) & pi_4132 x = pi_24 () & pi_4213 x = pi_34 () & pi_4312 x = pi_23 (pi_24 ()) & pi_4321 x = pi_23 () ) ;

theorem :: ANPROJ10:9
for X being non empty set
for x being Tuple of 4,X holds
( pi_13 (pi_23 ()) = pi_12 x & pi_12 (pi_34 (pi_23 ())) = pi_34 () & pi_23 (pi_24 (pi_14 (pi_23 ()))) = pi_14 x ) ;

theorem :: ANPROJ10:10
for X being non empty set
for x being Tuple of 4,X holds
( pi_23 (pi_14 ()) = pi_24 (pi_23 ()) & pi_34 (pi_24 ()) = pi_24 (pi_13 ()) & pi_24 (pi_34 ()) = pi_12 (pi_34 ()) ) ;

theorem Th05: :: ANPROJ10:11
for V being RealLinearSpace
for P, Q being Element of V holds P,Q,Q are_collinear
proof end;

Lm01: for V being RealLinearSpace
for A, B, P, Q being Element of V
for a, b being Real st A = ((1 - a) * P) + (a * Q) & B = ((1 - b) * P) + (b * Q) holds
A - B = (b - a) * (P - Q)

proof end;

definition
let V be RealLinearSpace;
let A, B, C be Element of V;
assume that
A1: A <> C and
A2: A,B,C are_collinear ;
func affine-ratio (A,B,C) -> Real means :Def02: :: ANPROJ10:def 28
B - A = it * (C - A);
existence
ex b1 being Real st B - A = b1 * (C - A)
proof end;
uniqueness
for b1, b2 being Real st B - A = b1 * (C - A) & B - A = b2 * (C - A) holds
b1 = b2
proof end;
end;

:: deftheorem Def02 defines affine-ratio ANPROJ10:def 28 :
for V being RealLinearSpace
for A, B, C being Element of V st A <> C & A,B,C are_collinear holds
for b5 being Real holds
( b5 = affine-ratio (A,B,C) iff B - A = b5 * (C - A) );

theorem :: ANPROJ10:12
for V being RealLinearSpace
for A, B, C being Element of V st A <> C & A,B,C are_collinear holds
A - B = (affine-ratio (A,B,C)) * (A - C)
proof end;

theorem Th06: :: ANPROJ10:13
for V being RealLinearSpace
for A, B, C being Element of V st A <> C & A,B,C are_collinear holds
( affine-ratio (A,B,C) = 0 iff A = B )
proof end;

theorem Th07: :: ANPROJ10:14
for V being RealLinearSpace
for A, B, C being Element of V st A <> C & A,B,C are_collinear holds
( affine-ratio (A,B,C) = 1 iff B = C )
proof end;

theorem Th08: :: ANPROJ10:15
for V being RealLinearSpace
for P, Q being Element of V
for a, b being Real st P <> Q & a * (P - Q) = b * (P - Q) holds
a = b
proof end;

theorem Th09: :: ANPROJ10:16
for V being RealLinearSpace
for P, Q, R being Element of V st P,Q,R are_collinear & P <> R & P <> Q holds
affine-ratio (P,R,Q) = 1 / (affine-ratio (P,Q,R))
proof end;

theorem Th10: :: ANPROJ10:17
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 (Q,P,R) = (affine-ratio (P,Q,R)) / ((affine-ratio (P,Q,R)) - 1)
proof end;

theorem Th11: :: ANPROJ10:18
for V being RealLinearSpace
for P, Q, R being Element of V st P,Q,R are_collinear & P <> R holds
affine-ratio (R,Q,P) = 1 - (affine-ratio (P,Q,R))
proof end;

theorem Th12: :: ANPROJ10:19
for V being RealLinearSpace
for P, Q, R being Element of V st P,Q,R are_collinear & P <> R & P <> Q holds
affine-ratio (Q,R,P) = ((affine-ratio (P,Q,R)) - 1) / (affine-ratio (P,Q,R))
proof end;

theorem Th13: :: ANPROJ10:20
for V being RealLinearSpace
for P, Q, R being Element of V st P,Q,R are_collinear & P <> R & Q <> R holds
affine-ratio (R,P,Q) = 1 / (1 - (affine-ratio (P,Q,R)))
proof end;

theorem :: ANPROJ10:21
for V being RealLinearSpace
for P, Q, R being Element of V
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 ) by ;

theorem :: ANPROJ10:22
for V being RealLinearSpace
for P, Q, R being Element of V
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))
proof end;

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 ()
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 ()
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 ()
for p being Tuple of 1, REAL st p = x holds
- x = - p ;

theorem Th14: :: 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
proof end;

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

theorem Th16: :: 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
proof end;

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

theorem Th18: :: 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
proof end;

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

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

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

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

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

theorem Th23: :: 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
proof end;

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

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

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

theorem Th25: :: ANPROJ10:41
for x, y, z being Element of () holds x,y,z are_collinear
proof end;

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

theorem Th26: :: ANPROJ10:43
for T being RealLinearSpace st T = TOP-REAL 1 holds
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) )
proof end;

theorem Th27: :: ANPROJ10:44
for x being Element of ()
for a, r being Real st x = <*a*> holds
r * x = <*(r * a)*>
proof end;

theorem :: ANPROJ10:45
for x, y being Element of ()
for a, b, r being Real st x = <*a*> & y = <*b*> holds
( x = r * y iff a = r * b )
proof end;

theorem :: ANPROJ10:46
for x, y being Element of ()
for a, b being Real st x = <*a*> & y = <*b*> holds
x - y = <*(a - b)*> by RVSUM_1:29;

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

theorem Th28: :: 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 zero non unit 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 )
proof end;

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_1423 x & pi_2143 () = pi_2134 x & pi_3412 () = pi_4312 x & pi_4321 () = pi_3421 x & pi_3412 () = pi_2413 x & pi_2143 () = pi_3142 x & pi_4321 () = pi_4231 x & pi_3412 () = pi_2314 x & pi_2143 () = pi_4132 x & pi_4321 () = pi_3241 x & pi_1243 () = pi_1432 x & pi_4321 () = pi_2341 x & pi_3412 () = pi_3214 x & pi_2143 () = pi_4123 x & pi_4321 () = pi_4213 x & pi_3412 () = pi_2431 x & pi_2143 () = pi_1342 x & pi_4312 () = pi_4231 x & pi_4321 () = pi_4213 x ) ;

definition
let V be RealLinearSpace;
let P, Q, R, S be 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));
coherence
(affine-ratio (R,P,Q)) / (affine-ratio (S,P,Q)) is Real
;
end;

:: deftheorem defines cross-ratio ANPROJ10:def 29 :
for V being RealLinearSpace
for P, Q, R, S being Element of V holds cross-ratio (P,Q,R,S) = (affine-ratio (R,P,Q)) / (affine-ratio (S,P,Q));

theorem Th31: :: ANPROJ10:52
for V being RealLinearSpace
for P, Q, R, S being Element of V st P,Q,R,S are_collinear & R <> Q & S <> Q & S <> P holds
( R = P iff cross-ratio (P,Q,R,S) = 0 )
proof end;

theorem :: ANPROJ10:53
for V being RealLinearSpace
for P, R, S being Element of V st P <> R & P <> S holds
cross-ratio (P,P,R,S) = 1
proof end;

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

theorem :: ANPROJ10:55
for V being RealLinearSpace
for P, Q, R, S, P9, Q9, R9, S9 being Element of V st P,Q,R,S are_collinear & P9,Q9,R9,S9 are_collinear & S <> P & S <> Q & S9 <> P9 & S9 <> Q9 holds
( 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)) )
proof end;

Lm02: for V being RealLinearSpace
for P, Q, R, S being Element of V
for r being Real st P - Q = r * (R - S) holds
Q - P = r * (S - R)

proof end;

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

theorem Th34: :: 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)
proof end;

theorem Th34bis: :: ANPROJ10:58
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 (S,R,Q,P)
proof end;

theorem :: ANPROJ10:59
for V being RealLinearSpace
for P, Q, R, S being Element of V holds cross-ratio (P,Q,S,R) = 1 / (cross-ratio (P,Q,R,S)) by XCMPLX_1:57;

theorem :: ANPROJ10:60
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 (Q,P,R,S) = 1 / (cross-ratio (P,Q,R,S))
proof end;

theorem :: ANPROJ10:61
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 (R,S,Q,P) = 1 / (cross-ratio (P,Q,R,S))
proof end;

theorem :: ANPROJ10:62
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 (S,R,P,Q) = 1 / (cross-ratio (P,Q,R,S))
proof end;

theorem Th35: :: ANPROJ10:63
for V being RealLinearSpace
for P, Q, R, S being Element of V st P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct holds
cross-ratio (P,R,Q,S) = 1 - (cross-ratio (P,Q,R,S))
proof end;

theorem :: ANPROJ10:64
for V being RealLinearSpace
for P, Q, R, S being Element of V st P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct holds
cross-ratio (Q,S,P,R) = 1 - (cross-ratio (P,Q,R,S))
proof end;

theorem :: ANPROJ10:65
for V being RealLinearSpace
for P, Q, R, S being Element of V st P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct holds
cross-ratio (R,P,S,Q) = 1 - (cross-ratio (P,Q,R,S))
proof end;

theorem :: ANPROJ10:66
for V being RealLinearSpace
for P, Q, R, S being Element of V st P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct holds
cross-ratio (S,Q,R,P) = 1 - (cross-ratio (P,Q,R,S))
proof end;

definition
let V be RealLinearSpace;
let x be Tuple of 4, the carrier of V;
func cross-ratio-tuple x -> Real means :Def03: :: 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) );
existence
ex b1 being Real ex P, Q, R, S being Element of V st
( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b1 = cross-ratio (P,Q,R,S) )
proof end;
uniqueness
for b1, b2 being Real st ex P, Q, R, S being Element of V st
( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b1 = cross-ratio (P,Q,R,S) ) & ex P, Q, R, S being Element of V st
( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b2 = cross-ratio (P,Q,R,S) ) holds
b1 = b2
;
end;

:: deftheorem Def03 defines cross-ratio-tuple ANPROJ10:def 30 :
for V being RealLinearSpace
for x being Tuple of 4, the carrier of V
for b3 being Real holds
( b3 = cross-ratio-tuple x iff ex P, Q, R, S being Element of V st
( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b3 = cross-ratio (P,Q,R,S) ) );

theorem Th36: :: ANPROJ10:67
for V being RealLinearSpace
for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> holds
cross-ratio (P,Q,R,S) = cross-ratio-tuple x
proof end;

theorem Th37: :: ANPROJ10:68
for V being RealLinearSpace
for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_collinear & P <> S & Q <> R & Q <> S holds
cross-ratio-tuple x = cross-ratio-tuple ()
proof end;

theorem Th38: :: ANPROJ10:69
for V being RealLinearSpace
for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_collinear & P <> R & P <> S & Q <> R & Q <> S holds
( cross-ratio-tuple x = cross-ratio-tuple () & cross-ratio-tuple x = cross-ratio-tuple () )
proof end;

theorem Th39: :: ANPROJ10:70
for V being RealLinearSpace
for x being Tuple of 4, the carrier of V holds cross-ratio-tuple () = 1 /
proof end;

theorem :: ANPROJ10:71
for V being RealLinearSpace
for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear holds
ex r being non zero non unit Real st
( r = cross-ratio-tuple x & cross-ratio-tuple () = op1 r )
proof end;

theorem Th40: :: ANPROJ10:72
for V being RealLinearSpace
for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_collinear & P <> R & P <> S & Q <> R & Q <> S holds
( cross-ratio-tuple () = 1 / & cross-ratio-tuple () = 1 / & cross-ratio-tuple () = 1 / & cross-ratio-tuple () = 1 / )
proof end;

theorem Th41: :: ANPROJ10:73
for V being RealLinearSpace
for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear holds
( cross-ratio-tuple () = 1 - & cross-ratio-tuple () = 1 - & cross-ratio-tuple () = 1 - & cross-ratio-tuple () = 1 - )
proof end;

theorem :: ANPROJ10:74
for V being RealLinearSpace
for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear holds
( cross-ratio-tuple () = 1 / (1 - ) & cross-ratio-tuple () = 1 / (1 - ) & cross-ratio-tuple () = 1 / (1 - ) & cross-ratio-tuple () = 1 / (1 - ) )
proof end;

theorem Th42: :: ANPROJ10:75
for V being RealLinearSpace
for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear holds
( cross-ratio-tuple () = ( - 1) / & cross-ratio-tuple () = ( - 1) / & cross-ratio-tuple () = ( - 1) / & cross-ratio-tuple () = ( - 1) / )
proof end;

theorem :: ANPROJ10:76
for V being RealLinearSpace
for P, Q, R, S being Element of V
for x being Tuple of 4, the carrier of V st x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct & P,Q,R,S are_collinear holds
( cross-ratio-tuple () = / ( - 1) & cross-ratio-tuple () = / ( - 1) & cross-ratio-tuple () = / ( - 1) & cross-ratio-tuple () = / ( - 1) )
proof end;

Lm03: for a, b, c, d being Complex holds ((a - c) / (b - c)) / ((a - d) / (b - d)) = ((c - a) / (c - b)) * ((d - b) / (d - a))
proof end;

theorem :: ANPROJ10:77
for x1, x2, x3, x4 being Element of () 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)) )
proof end;