:: {C}ross-ratio in Real Vector Space
:: by Roland Coghetto
::
:: Received February 27, 2019
:: Copyright (c) 2019-2021 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 b₁ being non zero Real holds b₁ 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 b₁, b₂ being non zero non unit Real st b₁ = 1 / b₂ holds
b₂ = 1 / b₁ ;

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 b₁, b₂ being non zero non unit Real st b₁ = 1 - b₂ holds
b₂ = 1 - b₁ ;

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 b₁, b₂ being Tuple of 4,X st b₁ = <*(b₂ . 2),(b₂ . 1),(b₂ . 3),(b₂ . 4)*> holds
b₂ = <*(b₁ . 2),(b₁ . 1),(b₁ . 3),(b₁ . 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 b₁, b₂ being Tuple of 4,X st b₁ = <*(b₂ . 3),(b₂ . 2),(b₂ . 1),(b₂ . 4)*> holds
b₂ = <*(b₁ . 3),(b₁ . 2),(b₁ . 1),(b₁ . 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 b₁, b₂ being Tuple of 4,X st b₁ = <*(b₂ . 4),(b₂ . 2),(b₂ . 3),(b₂ . 1)*> holds
b₂ = <*(b₁ . 4),(b₁ . 2),(b₁ . 3),(b₁ . 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 b₁, b₂ being Tuple of 4,X st b₁ = <*(b₂ . 1),(b₂ . 3),(b₂ . 2),(b₂ . 4)*> holds
b₂ = <*(b₁ . 1),(b₁ . 3),(b₁ . 2),(b₁ . 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 b₁, b₂ being Tuple of 4,X st b₁ = <*(b₂ . 1),(b₂ . 4),(b₂ . 3),(b₂ . 2)*> holds
b₂ = <*(b₁ . 1),(b₁ . 4),(b₁ . 3),(b₁ . 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 b₁, b₂ being Tuple of 4,X st b₁ = <*(b₂ . 1),(b₂ . 2),(b₂ . 4),(b₂ . 3)*> holds
b₂ = <*(b₁ . 1),(b₁ . 2),(b₁ . 4),(b₁ . 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 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

for X being non empty set
for x being Tuple of 4,X holds
( 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

for X being non empty set
for x being Tuple of 4,X holds
( 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

for X being non empty set
for x being Tuple of 4,X holds
( 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)) ) ;

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 b₁ being Real st B - A = b₁ * (C - A)

proof end;

uniqueness
for b₁, b₂ being Real st B - A = b₁ * (C - A) & B - A = b₂ * (C - A) holds
b₁ = b₂

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 b₅ being Real holds
( b₅ = affine-ratio (A,B,C) iff B - A = b₅ * (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 Th09, Th10, Th11, Th12, Th13;

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 (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 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 (TOP-REAL 1) 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 (TOP-REAL 1) 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 (TOP-REAL 1) 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 (TOP-REAL 1) 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 <> <*0*> 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 (TOP-REAL 1) 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 (TOP-REAL 1)
for a, r being Real st x = <*a*> holds
r * x = <*(r * a)*>

proof end;

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 )

proof end;

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)*> 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 Th06, Th07;

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

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 b₁ being Real ex P, Q, R, S being Element of V st
( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b₁ = cross-ratio (P,Q,R,S) )

proof end;

uniqueness
for b₁, b₂ 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 & b₁ = 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 & b₂ = cross-ratio (P,Q,R,S) ) holds
b₁ = b₂ ;

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 b₃ being Real holds
( b₃ = 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 & b₃ = 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 (pi_3412 x)

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 (pi_2143 x) & cross-ratio-tuple x = cross-ratio-tuple (pi_4321 x) )

proof end;

theorem Th39: :: ANPROJ10:70

for V being RealLinearSpace
for x being Tuple of 4, the carrier of V holds cross-ratio-tuple (pi_1243 x) = 1 / (cross-ratio-tuple x)

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 (pi_1243 x) = 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 (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) )

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

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

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

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

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

proof end;