:: by Roland Coghetto

::

:: Received February 27, 2019

:: Copyright (c) 2019 Association of Mizar Users

registration

let a, b, c, d be object ;

reducibility

<*a,b,c,d*> . 1 = a by FINSEQ_4:76;

reducibility

<*a,b,c,d*> . 2 = b by FINSEQ_4:76;

reducibility

<*a,b,c,d*> . 3 = c by FINSEQ_4:76;

reducibility

<*a,b,c,d*> . 4 = d by FINSEQ_4:76;

end;
reducibility

<*a,b,c,d*> . 1 = a by FINSEQ_4:76;

reducibility

<*a,b,c,d*> . 2 = b by FINSEQ_4:76;

reducibility

<*a,b,c,d*> . 3 = c by FINSEQ_4:76;

reducibility

<*a,b,c,d*> . 4 = d by FINSEQ_4:76;

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 )

( a = a9 & b = b9 & c = c9 & d = d9 )

proof end;

definition

let r be non zero non unit Real;

coherence

1 / r is non zero non unit Real

for b_{1}, b_{2} being non zero non unit Real st b_{1} = 1 / b_{2} holds

b_{2} = 1 / b_{1}
;

end;
coherence

1 / r is non zero non unit Real

proof end;

involutiveness for b

b

definition

let r be non zero non unit Real;

coherence

1 - r is non zero non unit Real

for b_{1}, b_{2} being non zero non unit Real st b_{1} = 1 - b_{2} holds

b_{2} = 1 - b_{1}
;

end;
coherence

1 - r is non zero non unit Real

proof end;

involutiveness for b

b

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

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

( op2 (op1 (op2 (op1 r))) = op1 (op2 r) & op1 (op2 (op1 (op2 r))) = op2 (op1 r) )

proof end;

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

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;

coherence

<*(x . 1),(x . 3),(x . 4),(x . 2)*> is Tuple of 4,X by Th03;

coherence

<*(x . 1),(x . 4),(x . 2),(x . 3)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 1),(x . 4),(x . 3)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 3),(x . 1),(x . 4)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 3),(x . 4),(x . 1)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 4),(x . 1),(x . 3)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 4),(x . 3),(x . 1)*> is Tuple of 4,X by Th03;

coherence

<*(x . 3),(x . 1),(x . 2),(x . 4)*> is Tuple of 4,X by Th03;

coherence

<*(x . 3),(x . 1),(x . 4),(x . 2)*> is Tuple of 4,X by Th03;

coherence

<*(x . 3),(x . 2),(x . 4),(x . 1)*> is Tuple of 4,X by Th03;

coherence

<*(x . 3),(x . 4),(x . 1),(x . 2)*> is Tuple of 4,X by Th03;

coherence

<*(x . 3),(x . 4),(x . 2),(x . 1)*> is Tuple of 4,X by Th03;

coherence

<*(x . 4),(x . 1),(x . 2),(x . 3)*> is Tuple of 4,X by Th03;

coherence

<*(x . 4),(x . 1),(x . 3),(x . 2)*> is Tuple of 4,X by Th03;

coherence

<*(x . 4),(x . 2),(x . 1),(x . 3)*> is Tuple of 4,X by Th03;

coherence

<*(x . 4),(x . 3),(x . 1),(x . 2)*> is Tuple of 4,X by Th03;

coherence

<*(x . 4),(x . 3),(x . 2),(x . 1)*> is Tuple of 4,X by Th03;

end;
let x be Tuple of 4,X;

coherence

<*(x . 1),(x . 3),(x . 4),(x . 2)*> is Tuple of 4,X by Th03;

coherence

<*(x . 1),(x . 4),(x . 2),(x . 3)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 1),(x . 4),(x . 3)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 3),(x . 1),(x . 4)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 3),(x . 4),(x . 1)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 4),(x . 1),(x . 3)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 4),(x . 3),(x . 1)*> is Tuple of 4,X by Th03;

coherence

<*(x . 3),(x . 1),(x . 2),(x . 4)*> is Tuple of 4,X by Th03;

coherence

<*(x . 3),(x . 1),(x . 4),(x . 2)*> is Tuple of 4,X by Th03;

coherence

<*(x . 3),(x . 2),(x . 4),(x . 1)*> is Tuple of 4,X by Th03;

coherence

<*(x . 3),(x . 4),(x . 1),(x . 2)*> is Tuple of 4,X by Th03;

coherence

<*(x . 3),(x . 4),(x . 2),(x . 1)*> is Tuple of 4,X by Th03;

coherence

<*(x . 4),(x . 1),(x . 2),(x . 3)*> is Tuple of 4,X by Th03;

coherence

<*(x . 4),(x . 1),(x . 3),(x . 2)*> is Tuple of 4,X by Th03;

coherence

<*(x . 4),(x . 2),(x . 1),(x . 3)*> is Tuple of 4,X by Th03;

coherence

<*(x . 4),(x . 3),(x . 1),(x . 2)*> is Tuple of 4,X by Th03;

coherence

<*(x . 4),(x . 3),(x . 2),(x . 1)*> is Tuple of 4,X by Th03;

:: 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)*>;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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;

coherence

<*(x . 1),(x . 2),(x . 3),(x . 4)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 1),(x . 3),(x . 4)*> is Tuple of 4,X by Th03;

involutiveness

for b_{1}, b_{2} being Tuple of 4,X st b_{1} = <*(b_{2} . 2),(b_{2} . 1),(b_{2} . 3),(b_{2} . 4)*> holds

b_{2} = <*(b_{1} . 2),(b_{1} . 1),(b_{1} . 3),(b_{1} . 4)*>

<*(x . 3),(x . 2),(x . 1),(x . 4)*> is Tuple of 4,X by Th03;

involutiveness

for b_{1}, b_{2} being Tuple of 4,X st b_{1} = <*(b_{2} . 3),(b_{2} . 2),(b_{2} . 1),(b_{2} . 4)*> holds

b_{2} = <*(b_{1} . 3),(b_{1} . 2),(b_{1} . 1),(b_{1} . 4)*>

<*(x . 4),(x . 2),(x . 3),(x . 1)*> is Tuple of 4,X by Th03;

involutiveness

for b_{1}, b_{2} being Tuple of 4,X st b_{1} = <*(b_{2} . 4),(b_{2} . 2),(b_{2} . 3),(b_{2} . 1)*> holds

b_{2} = <*(b_{1} . 4),(b_{1} . 2),(b_{1} . 3),(b_{1} . 1)*>

<*(x . 1),(x . 3),(x . 2),(x . 4)*> is Tuple of 4,X by Th03;

involutiveness

for b_{1}, b_{2} being Tuple of 4,X st b_{1} = <*(b_{2} . 1),(b_{2} . 3),(b_{2} . 2),(b_{2} . 4)*> holds

b_{2} = <*(b_{1} . 1),(b_{1} . 3),(b_{1} . 2),(b_{1} . 4)*>

<*(x . 1),(x . 4),(x . 3),(x . 2)*> is Tuple of 4,X by Th03;

involutiveness

for b_{1}, b_{2} being Tuple of 4,X st b_{1} = <*(b_{2} . 1),(b_{2} . 4),(b_{2} . 3),(b_{2} . 2)*> holds

b_{2} = <*(b_{1} . 1),(b_{1} . 4),(b_{1} . 3),(b_{1} . 2)*>

<*(x . 1),(x . 2),(x . 4),(x . 3)*> is Tuple of 4,X by Th03;

involutiveness

for b_{1}, b_{2} being Tuple of 4,X st b_{1} = <*(b_{2} . 1),(b_{2} . 2),(b_{2} . 4),(b_{2} . 3)*> holds

b_{2} = <*(b_{1} . 1),(b_{1} . 2),(b_{1} . 4),(b_{1} . 3)*>

end;
let x be Tuple of 4,X;

coherence

<*(x . 1),(x . 2),(x . 3),(x . 4)*> is Tuple of 4,X by Th03;

coherence

<*(x . 2),(x . 1),(x . 3),(x . 4)*> is Tuple of 4,X by Th03;

involutiveness

for b

b

proof end;

coherence <*(x . 3),(x . 2),(x . 1),(x . 4)*> is Tuple of 4,X by Th03;

involutiveness

for b

b

proof end;

coherence <*(x . 4),(x . 2),(x . 3),(x . 1)*> is Tuple of 4,X by Th03;

involutiveness

for b

b

proof end;

coherence <*(x . 1),(x . 3),(x . 2),(x . 4)*> is Tuple of 4,X by Th03;

involutiveness

for b

b

proof end;

coherence <*(x . 1),(x . 4),(x . 3),(x . 2)*> is Tuple of 4,X by Th03;

involutiveness

for b

b

proof end;

coherence <*(x . 1),(x . 2),(x . 4),(x . 3)*> is Tuple of 4,X by Th03;

involutiveness

for b

b

proof 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)*>;

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

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

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

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

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

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

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

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

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

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

theorem :: ANPROJ10:10

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 ;

existence

ex b_{1} being Real st B - A = b_{1} * (C - A)

for b_{1}, b_{2} being Real st B - A = b_{1} * (C - A) & B - A = b_{2} * (C - A) holds

b_{1} = b_{2}

end;
let A, B, C be Element of V;

assume that

A1: A <> C and

A2: A,B,C are_collinear ;

existence

ex b

proof end;

uniqueness for b

b

proof 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_{5} being Real holds

( b_{5} = affine-ratio (A,B,C) iff B - A = b_{5} * (C - A) );

for V being RealLinearSpace

for A, B, C being Element of V st A <> C & A,B,C are_collinear holds

for b

( b

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)

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 )

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 )

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

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

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)

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

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

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

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;

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

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

theorem :: ANPROJ10:24

theorem :: ANPROJ10:25

theorem :: ANPROJ10:26

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

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

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

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

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

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 :: ANPROJ10:36

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

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

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

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 )

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 :: 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;

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

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

for a, b, r being Real st x = <*a*> & y = <*b*> holds

( x = r * y iff a = r * b )

proof end;

theorem :: ANPROJ10:46

theorem :: ANPROJ10:47

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;

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 )

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

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

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;

(affine-ratio (R,P,Q)) / (affine-ratio (S,P,Q)) is Real ;

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

(affine-ratio (R,P,Q)) / (affine-ratio (S,P,Q)) is Real ;

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

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 )

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

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

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

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)

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)

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)

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;

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

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

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

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

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

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

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

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;

ex b_{1} 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_{1} = cross-ratio (P,Q,R,S) )

for b_{1}, b_{2} 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_{1} = 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_{2} = cross-ratio (P,Q,R,S) ) holds

b_{1} = b_{2}
;

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

ex b

( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b

proof end;

uniqueness for b

( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b

( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b

b

:: 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_{3} being Real holds

( b_{3} = 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_{3} = cross-ratio (P,Q,R,S) ) );

for V being RealLinearSpace

for x being Tuple of 4, the carrier of V

for b

( b

( P = x . 1 & Q = x . 2 & R = x . 3 & S = x . 4 & b

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

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)

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

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)

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 )

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

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

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

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

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

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

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;