:: {C}ross-ratio in Real Vector Space
:: by Roland Coghetto
::
:: Received February 27, 2019
:: Copyright (c) 2019-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NAT_1, FINSEQ_2, REAL_1, XCMPLX_0, PENCIL_1, ALGSTR_0, ARYTM_1,
ARYTM_3, CARD_1, EUCLID, FUNCT_1, INCSP_1, NUMBERS, PRE_TOPC, RELAT_1,
STRUCT_0, SUBSET_1, SUPINF_2, VECTSP_1, XBOOLE_0, TARSKI, FINSEQ_1,
RLTOPSP1, ANPROJ10, FUNCT_5, RLVECT_1, FUNCOP_1, FUNCT_2, FUNCSDOM,
BINOP_2, PCOMPS_1, ZFMISC_1;
notations ORDINAL1, XCMPLX_0, PRE_TOPC, TARSKI, XBOOLE_0, RLVECT_1, XREAL_0,
SUBSET_1, NUMBERS, FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, ALGSTR_0,
VECTSP_1, FINSEQ_2, BINOP_1, FUNCOP_1, FINSEQ_4, RVSUM_1, FUNCSDOM,
BINOP_2, PCOMPS_1, EUCLID, SRINGS_5, RLTOPSP1, EUCLID_4, ZFMISC_1;
constructors FINSEQ_4, MONOID_0, BINOP_2, FUNCSDOM, PCOMPS_1, SRINGS_5,
EUCLID_4;
registrations MEMBERED, ORDINAL1, STRUCT_0, XREAL_0, MONOID_0, EUCLID,
VALUED_0, XCMPLX_0, NUMBERS, RLTOPSP1, RLVECT_1, RELAT_1, FINSEQ_4,
FINSEQ_1;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities STRUCT_0, EUCLID, XCMPLX_0, RLVECT_1, FINSEQ_1, FUNCSDOM, PCOMPS_1,
FINSEQ_2, RVSUM_1, VALUED_1;
expansions RLTOPSP1;
theorems XREAL_0, EUCLID, XCMPLX_1, RVSUM_1, FINSEQ_1, FINSEQ_2, RLTOPSP1,
EUCLID12, RLVECT_1, FINSEQ_4, JORDAN2B, FUNCSDOM, ALGSTR_0, BINOP_2,
SRINGS_5, FUNCOP_1, EUCLID_4, ZFMISC_1, CARD_1;
begin :: Preliminaries
theorem
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
let a,b,c,d,a9,b9,c9,d9 be object;
assume
A1: <* a, b, c, d *> = <* a9, b9, c9, d9 *>;
set x = <* a,b,c,d *>, y = <*a9,b9,c9,d9 *>;
x.1 = a & x.2 = b & x.3 = c & x.4 = d & y.1 = a9 & y.2 = b9 &
y.3 = c9 & y.4 = d9;
hence thesis by A1;
end;
definition
let r be Real;
attr r is unit means :Def01:
r = 1;
end;
registration
cluster non unit for non zero Real;
existence
proof
take 2;
thus thesis;
end;
end;
definition
let r be non unit non zero Real;
func op1(r) -> non unit non zero Real equals
1 / r;
coherence
proof
1 / r <> 1
proof
assume 1 / r = 1;
then r * (1 / r) = r;
hence contradiction by Def01,XCMPLX_1:106;
end;
hence thesis by Def01;
end;
involutiveness;
end;
definition
let r being non unit non zero Real;
func op2(r) -> non unit non zero Real equals
1 - r;
coherence
proof
r <> 0; then
1 - r <> 0 & 1 - r <> 1 by Def01;
hence thesis by Def01;
end;
involutiveness;
end;
reserve a,b,r for non unit non zero Real;
theorem Th01:
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
A1: 1 - 1 / r = r / r - 1 / r by XCMPLX_1:60
.= (r - 1) / r;
1 - r <> 0 by Def01;
then 1 - (1 / (1 - r)) = ((1 - r) / (1 - r)) - 1 / (1 - r) by XCMPLX_1:60
.= -r / (1 - r)
.= r / -(1 - r) by XCMPLX_1:188;
hence thesis by A1,XCMPLX_1:57;
end;
theorem
op2(op1(op2(op1(r)))) = op1(op2(r)) &
op1(op2(op1(op2(r)))) = op2(op1(r))
proof
op2(op1(op2(op1(r)))) = 1 - (r / (r - 1)) &
op1(op2(op1(op2(r)))) = 1 / (r / (r - 1)) by Th01;
hence thesis;
end;
theorem
op1(a) / op1(b) = b / a;
reserve X for non empty set,
x for Tuple of 4,X;
theorem Th02:
4-tuples_on X = the set of all <* d1, d2, d3, d4 *> where
d1,d2,d3,d4 is Element of X
proof
hereby
let x be object;
assume x in 4-tuples_on X;
then consider s be Element of X* such that
A1: x = s and
A2: len s = 4;
1 in Seg 4 & 2 in Seg 4 & 3 in Seg 4 & 4 in Seg 4;
then 1 in dom s & 2 in dom s & 3 in dom s & 4 in dom s
by A2,FINSEQ_1:def 3;
then reconsider d19 = s.1, d29 = s.2, d39 = s.3,
d49 = s.4 as Element of X by FINSEQ_2:11;
s = <* d19, d29, d39, d49 *> by A2,FINSEQ_4:76;
hence x in the set of all <* d1, d2, d3, d4 *>
where d1,d2,d3,d4 is Element of X by A1;
end;
let x be object;
assume x in the set of all <* d1, d2, d3, d4 *>
where d1,d2,d3,d4 is Element of X;
then consider d1, d2, d3, d4 be Element of X such that
A3: x = <* d1, d2, d3,d4 *>;
len <* d1, d2, d3, d4 *> = 4 & <* d1, d2, d3, d4 *> is Element of X*
by FINSEQ_1:def 11,FINSEQ_4:76;
hence x in 4-tuples_on X by A3;
end;
theorem Th03:
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
let a,b,c,d be object;
assume
A1: (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);
set y = <* a,b,c,d *>;
dom x = Seg 4 by FINSEQ_2:124; then
A2: 1 in dom x & 2 in dom x & 3 in dom x & 4 in dom x;
reconsider d19 = y.1, d29 = y.2, d39 = y.3,
d49 = y.4 as Element of X by A1,A2,FINSEQ_2:11;
a is Element of X & b is Element of X & c is Element of X &
d is Element of X by A1,A2,FINSEQ_2:11; then
y in the set of all <* d1, d2, d3, d4 *> where
d1,d2,d3,d4 is Element of X;
then y in 4-tuples_on X by Th02;
hence thesis by FINSEQ_2:131;
end;
definition
let X be non empty set;
let x be Tuple of 4,X;
func pi_1342(x) -> Tuple of 4,X equals <* x.1,x.3,x.4,x.2 *>;
coherence by Th03;
func pi_1423(x) -> Tuple of 4,X equals <* x.1,x.4,x.2,x.3 *>;
coherence by Th03;
func pi_2143(x) -> Tuple of 4,X equals <* x.2,x.1,x.4,x.3 *>;
coherence by Th03;
func pi_2314(x) -> Tuple of 4,X equals <* x.2,x.3,x.1,x.4 *>;
coherence by Th03;
func pi_2341(x) -> Tuple of 4,X equals <* x.2,x.3,x.4,x.1 *>;
coherence by Th03;
func pi_2413(x) -> Tuple of 4,X equals <* x.2,x.4,x.1,x.3 *>;
coherence by Th03;
func pi_2431(x) -> Tuple of 4,X equals <* x.2,x.4,x.3,x.1 *>;
coherence by Th03;
func pi_3124(x) -> Tuple of 4,X equals <* x.3,x.1,x.2,x.4 *>;
coherence by Th03;
func pi_3142(x) -> Tuple of 4,X equals <* x.3,x.1,x.4,x.2 *>;
coherence by Th03;
func pi_3241(x) -> Tuple of 4,X equals <* x.3,x.2,x.4,x.1 *>;
coherence by Th03;
func pi_3412(x) -> Tuple of 4,X equals <* x.3,x.4,x.1,x.2 *>;
coherence by Th03;
func pi_3421(x) -> Tuple of 4,X equals <* x.3,x.4,x.2,x.1 *>;
coherence by Th03;
func pi_4123(x) -> Tuple of 4,X equals <* x.4,x.1,x.2,x.3 *>;
coherence by Th03;
func pi_4132(x) -> Tuple of 4,X equals <* x.4,x.1,x.3,x.2 *>;
coherence by Th03;
func pi_4213(x) -> Tuple of 4,X equals <* x.4,x.2,x.1,x.3 *>;
coherence by Th03;
func pi_4312(x) -> Tuple of 4,X equals <* x.4,x.3,x.1,x.2 *>;
coherence by Th03;
func pi_4321(x) -> Tuple of 4,X equals <* x.4,x.3,x.2,x.1 *>;
coherence by Th03;
end;
definition
let X be non empty set;
let x be Tuple of 4,X;
func pi_id(x) -> Tuple of 4,X equals <* x.1,x.2,x.3,x.4 *>;
coherence by Th03;
func pi_12(x) -> Tuple of 4,X equals <* x.2,x.1,x.3,x.4 *>;
coherence by Th03;
involutiveness
proof
let x,PI be Tuple of 4,X;
assume x = <* PI.2,PI.1,PI.3,PI.4 *>;
then x.1 = PI.2 & x.2 = PI.1 & x.3 = PI.3 & x.4 = PI.4 & len PI=4
by CARD_1:def 7;
hence thesis by FINSEQ_4:76;
end;
func pi_13(x) -> Tuple of 4,X equals <* x.3,x.2,x.1,x.4 *>;
coherence by Th03;
involutiveness
proof
let x,PI be Tuple of 4,X;
assume x = <* PI.3,PI.2,PI.1,PI.4 *>;
then x.1 = PI.3 & x.2 = PI.2 & x.3 = PI.1 & x.4 = PI.4 & len PI=4
by CARD_1:def 7;
hence thesis by FINSEQ_4:76;
end;
func pi_14(x) -> Tuple of 4,X equals <* x.4,x.2,x.3,x.1 *>;
coherence by Th03;
involutiveness
proof
let x,PI be Tuple of 4,X;
assume x = <* PI.4,PI.2,PI.3,PI.1 *>;
then x.1 = PI.4 & x.2 = PI.2 & x.3 = PI.3 & x.4 = PI.1 & len PI=4
by CARD_1:def 7;
hence thesis by FINSEQ_4:76;
end;
func pi_23(x) -> Tuple of 4,X equals <* x.1,x.3,x.2,x.4 *>;
coherence by Th03;
involutiveness
proof
let x,PI be Tuple of 4,X;
assume x = <* PI.1,PI.3,PI.2,PI.4 *>;
then x.1 = PI.1 & x.2 = PI.3 & x.3 = PI.2 & x.4 = PI.4 & len PI=4
by CARD_1:def 7;
hence thesis by FINSEQ_4:76;
end;
func pi_24(x) -> Tuple of 4,X equals <* x.1,x.4,x.3,x.2 *>;
coherence by Th03;
involutiveness
proof
let x,PI be Tuple of 4,X;
assume x = <* PI.1,PI.4,PI.3,PI.2 *>;
then x.1 = PI.1 & x.2 = PI.4 & x.3 = PI.3 & x.4 = PI.2 & len PI=4
by CARD_1:def 7;
hence thesis by FINSEQ_4:76;
end;
func pi_34(x) -> Tuple of 4,X equals <* x.1,x.2,x.4,x.3 *>;
coherence by Th03;
involutiveness
proof
let x,PI be Tuple of 4,X;
assume x = <* PI.1,PI.2,PI.4,PI.3 *>;
then x.1 = PI.1 & x.2 = PI.2 & x.3 = PI.4 & x.4 = PI.3 & len PI=4
by CARD_1:def 7;
hence thesis by FINSEQ_4:76;
end;
end;
registration
let X be non empty set;
let x be Tuple of 4,X;
reduce pi_id(x) to x;
reducibility
proof
dom x = Seg 4 by FINSEQ_2:124;
then len x = 4 by FINSEQ_1:def 3;
hence thesis by FINSEQ_4:76;
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
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
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
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
pi_23(pi_14(pi_34(x))) = pi_24(pi_23(pi_13(x))) &
pi_34(pi_24(pi_12(x))) = pi_24(pi_13(pi_23(x))) &
pi_24(pi_34(pi_13(x))) = pi_12(pi_34(pi_23(x)));
begin :: Affine-Ratio
reserve V for RealLinearSpace,
A,B,C,P,Q,R,S for Element of V;
theorem Th05:
P,Q,Q are_collinear
proof
P in Line(P,Q) & Q in Line(P,Q) by RLTOPSP1:72;
hence thesis;
end;
Lm01:
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
let a,b be Real;
assume that
A1: A = (1 - a) * P + a * Q and
A2: B = (1 - b) * P + b * Q;
A - B = (1 - a) * P + (a * Q - ((1 - b) * P + b * Q))
by A1,A2,RLVECT_1:def 3
.= (1 - a) * P + ((a * Q - b * Q ) - (1 - b) * P)
by RLVECT_1:27
.= (1 - a) * P + ((a - b) * Q - ((1 - b) * P)) by RLVECT_1:35
.= ((1 - a) * P + ((a - b) * Q)) + -((1 - b) * P) by RLVECT_1:def 3
.= ((1 - a) * P + ((a - b) * Q)) + ((-1) * ((1 - b) * P))
by RLVECT_1:16
.= ((1 - a) * P + ((a - b) * Q)) + ((-1) * (1 - b)) * P
by RLVECT_1:def 7
.= (1 - a) * P + ((a - b) * Q + (b - 1) * P) by RLVECT_1:def 3
.= (1 - a) * P + (((b - 1) * P) + ((a - b) * Q)) by RLVECT_1:def 2
.= (((1 - a) * P + (b - 1) * P)) + ((a - b) * Q) by RLVECT_1:def 3
.= (1 - a + (b - 1)) * P + (a - b) * Q by RLVECT_1:def 6
.= (b - a) * P + (-1) * (b - a) * Q
.= (b - a) * P + (-1) * ((b - a) * Q) by RLVECT_1:def 7
.= (b - a) * P - ((-1) * (a - b) * Q) by RLVECT_1:16;
hence thesis by RLVECT_1:34;
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:
(B - A) = it * (C - A);
existence
proof
consider L be line of V such that
A3: A in L and
A4: B in L and
A5: C in L by A2;
consider P,Q be Element of V such that
A6: L = Line(P,Q) by RLTOPSP1:def 15;
A7: Line(P,Q) = the set of all (((1 - r) * P) + (r * Q)) where r is Real
by RLTOPSP1:def 14;
consider a be Real such that
A8: A = (1 - a) * P + a * Q by A3,A6,A7;
consider b be Real such that
A9: B = (1 - b) * P + b * Q by A4,A6,A7;
consider c be Real such that
A10: C = (1 - c) * P + c * Q by A5,A6,A7;
A11: a - c <> 0 by A8,A10,A1;
set k = (a - b) / (a - c);
B - A = (a - b) * (P - Q) by A8,A9,Lm01
.= ((a - b) / (a - c) * (a - c)) * (P - Q) by A11,XCMPLX_1:87
.= ((a - b) / (a - c)) * ((a - c) * (P - Q)) by RLVECT_1:def 7
.= k * (C - A) by A8,A10,Lm01;
hence thesis;
end;
uniqueness
proof
let r1,r2 be Real such that
A12: (B - A) = r1 * (C - A) and
A13: (B - A) = r2 * (C - A);
C - A <> 0.V & r1 * (C - A) = r2 * (C - A)
by A12,A13,A1,RLVECT_1:21;
hence thesis by RLVECT_1:37;
end;
end;
theorem
A <> C & A,B,C are_collinear implies
A - B = affine-ratio(A,B,C) * (A - C)
proof
assume that
A1: A <> C and
A2: A,B,C are_collinear;
A - B = - (B - A) by RLVECT_1:33
.= - affine-ratio(A,B,C) * (C - A) by Def02,A1,A2
.= (- 1) * (affine-ratio(A,B,C) * (C - A)) by RLVECT_1:16
.= ((- 1) * affine-ratio(A,B,C)) * (C - A) by RLVECT_1:def 7
.= affine-ratio(A,B,C) * ((- 1) * (C - A)) by RLVECT_1:def 7
.= affine-ratio(A,B,C) * (-(C - A)) by RLVECT_1:16
.= affine-ratio(A,B,C) * (A - C) by RLVECT_1:33;
hence thesis;
end;
theorem Th06:
A <> C & A,B,C are_collinear implies
(affine-ratio(A,B,C) = 0 iff A = B)
proof
assume that
A1: A <> C and
A2: A,B,C are_collinear;
hereby
assume affine-ratio(A,B,C) = 0;
then (B - A) = 0 * (C - A) by A1,A2,Def02
.= 0.V by RLVECT_1:10;
hence A = B by RLVECT_1:21;
end;
assume A = B;
then B - A = 0.V by RLVECT_1:5
.= 0 * (C - A) by RLVECT_1:10;
hence affine-ratio(A,B,C) = 0 by A1,A2,Def02;
end;
theorem Th07:
A <> C & A,B,C are_collinear implies
(affine-ratio(A,B,C) = 1 iff B = C)
proof
assume that
A1: A <> C and
A2: A,B,C are_collinear;
hereby
assume affine-ratio(A,B,C) = 1;
then (B - A) = 1 * (C - A) by A1,A2,Def02
.= C - A by RLVECT_1:def 8;
hence B = C by RLVECT_1:8;
end;
assume B = C;
then B - A = 1 * (C - A) by RLVECT_1:def 8;
hence affine-ratio(A,B,C) = 1 by A1,A2,Def02;
end;
theorem Th08:
for a,b being Real st P <> Q & a * (P - Q) = b * (P - Q) holds a = b
proof
let a,b be Real;
assume that
A1: P <> Q and
A2: a * (P - Q) = b * (P - Q);
P - Q <> 0.V by A1, RLVECT_1:21;
hence thesis by A2,RLVECT_1:37;
end;
theorem Th09:
P,Q,R are_collinear & P <> R & P <> Q implies
affine-ratio(P,R,Q) = 1 / affine-ratio(P,Q,R)
proof
assume that
A1: P,Q,R are_collinear and
A2: P <> R and
A3: P <> Q;
set r = affine-ratio(P,Q,R),
s = affine-ratio(P,R,Q);
P,R,Q are_collinear by A1;
then R - P = s * (Q - P) by A3,Def02
.= s * (r * (R - P)) by A1,A2,Def02
.= (s * r) * (R - P) by RLVECT_1:def 7;
then 1 * (R - P) = (s * r) * (R - P) by RLVECT_1:def 8;
hence thesis by A2,Th08,XCMPLX_1:73;
end;
theorem Th10:
P,Q,R are_collinear & P <> R & Q <> R & P <> Q implies
affine-ratio(Q,P,R) =
affine-ratio(P,Q,R) / (affine-ratio(P,Q,R) - 1)
proof
assume that
A1: P,Q,R are_collinear and
A2: P <> R and
A3: Q <> R and
A4: P <> Q;
set r = affine-ratio(P,Q,R),
s = affine-ratio(Q,P,R);
A5: Q - P = r * (R - P) by A1,A2,Def02;
Q,P,R are_collinear by A1;
then P - Q = s * (R - Q) by A3,Def02;
then r * (R - P) = -s * (R + 0.V - Q) by A5,RLVECT_1:33
.= -s * (R + (-P + P) - Q) by RLVECT_1:5
.= -s * (R - P + P - Q) by RLVECT_1:def 3
.= -(s * ((R - P) + (P - Q))) by RLVECT_1:def 3
.= (-1) * (s * ((R - P) + (P - Q))) by RLVECT_1:16
.= ((-1) * s) * ((R - P) + (P - Q)) by RLVECT_1:def 7
.= (-s) * (R - P) + (-s) * (P - Q) by RLVECT_1:def 5;
then
A6: r * (R - P) + s * (R - P)
= (-s) * (R - P) + ((-s) * (P - Q) + s * (R - P)) by RLVECT_1:def 3
.= (-s) * (R - P) + (s * (R - P) + (-s) * (P - Q)) by RLVECT_1:def 2
.= ((-s) * (R - P) + s * (R - P)) + (-s) * (P - Q) by RLVECT_1:def 3
.= (-s + s) * (R - P) + (-s) * (P - Q) by RLVECT_1:def 6
.= 0.V + (-s) * (P - Q) by RLVECT_1:10
.= (-s) * (P - Q);
Q,P,R are_collinear by A1; then
A7: s <> 0 by A3,A4,Th06;
then reconsider s9 = 1 / s as non zero Real;
A8: s9 * s = 1 by A7,XCMPLX_1:106;
A9: r - 1 <> 0 by A1,A2,A3,Th07;
(r + s) * (R - P) = (-s) * (P - Q) by A6,RLVECT_1:def 6
.= s * (-(P - Q)) by RLVECT_1:24
.= s * (Q - P) by RLVECT_1:33;
then (s9 * (r + s)) * (R - P) = s9 * (s * (Q - P)) by RLVECT_1:def 7
.= (s9 * s) * (Q - P) by RLVECT_1:def 7
.= 1 * (Q - P) by A7,XCMPLX_1:106
.= Q - P by RLVECT_1:def 8;
then s * r = s * ((1/s) * (r + s)) by A1,Def02,A2;
then r * s = (s * (1/s)) * (r + s);
then r * s = r + s by A8;
then s * (r - 1) / (r - 1) = r / (r - 1);
then s * ((r - 1) / (r - 1)) = r / (r - 1);
then s * 1 = r / (r - 1) by A9,XCMPLX_1:60;
hence thesis;
end;
theorem Th11:
P,Q,R are_collinear & P <> R implies
affine-ratio(R,Q,P) = 1 - affine-ratio(P,Q,R)
proof
assume that
A1: P,Q,R are_collinear and
A2: P <> R;
set r = affine-ratio(P,Q,R),
s = affine-ratio(R,Q,P);
A3: Q - P = r * (R - P) by A1,A2,Def02;
A4: Q - P = Q + 0.V - P
.= Q + (-R + R) - P by RLVECT_1:5
.= Q + (-R) + R - P by RLVECT_1:def 3
.= (Q - R) + (R - P) by RLVECT_1:def 3
.= (Q - R) - (P - R) by RLVECT_1:33;
R,Q,P are_collinear by A1;
then r * (R - P) - s * (P - R) = s * (P - R) - (P - R) - s * (P - R)
by A3,A4,A2,Def02
.= s * (P - R) + (R - P) - s * (P - R)
by RLVECT_1:33
.= s * (P - R) + ((R - P) - s * (P - R))
by RLVECT_1:def 3
.= s * (P - R) + (- s * (P - R) + (R - P))
by RLVECT_1:def 2
.= s * (P - R) - s * (P - R) + (R - P)
by RLVECT_1:def 3
.= 0.V + (R - P) by RLVECT_1:5
.= R - P;
then R - P = r * (R - P) - s * (-(R - P)) by RLVECT_1:33
.= r * (R - P) - (s * ((-1) * (R - P))) by RLVECT_1:16
.= r * (R - P) - (s * (-1)) * (R - P) by RLVECT_1:def 7
.= r * (R - P) - (-s) * (R - P);
then (R - P) + (-s) * (R - P)
= r * (R - P) + (- (-s) * (R - P) + (-s) * (R - P)) by RLVECT_1:def 3
.= r * (R - P) + 0.V by RLVECT_1:5
.= r * (R - P);
then 1 * (R - P) + (-s) * (R - P) = r * (R - P) by RLVECT_1:def 8;
then (1 - s) * (R - P) = r * (R - P) by RLVECT_1:def 6;
then 1 - s = r by A2,Th08;
hence thesis;
end;
theorem Th12:
P,Q,R are_collinear & P <> R & P <> Q implies
affine-ratio(Q,R,P) =
(affine-ratio(P,Q,R) - 1) / affine-ratio(P,Q,R)
proof
assume that
A1: P,Q,R are_collinear and
A2: P <> R and
A3: P <> Q;
set r = affine-ratio(P,Q,R),
s = affine-ratio(Q,R,P);
A4: r <> 0 by A1,A2,A3,Th06;
A5: Q - P = r * (R + 0.V - P) by A1,A2,Def02
.= r * (R + (-Q + Q) - P) by RLVECT_1:5
.= r * ((R + -Q) + Q - P) by RLVECT_1:def 3
.= r * (R - Q + (Q - P)) by RLVECT_1:def 3
.= r * (R - Q) + r * (Q - P) by RLVECT_1:def 5;
Q,R,P are_collinear by A1;
then Q - P = r * (s * (P - Q)) + r * (Q - P) by A5,A3,Def02
.= (r * s) * (P - Q) + r * (Q - P) by RLVECT_1:def 7
.= (r * s) * (-(Q - P)) + r * (Q - P) by RLVECT_1:33
.= (r * s) * ((-1) * (Q - P)) + r * (Q - P) by RLVECT_1:16
.= (r * s * (-1)) * (Q - P) + r * (Q - P) by RLVECT_1:def 7
.= (-r * s + r) * (Q - P) by RLVECT_1:def 6;
then 1 * (Q - P) = (r - r * s) * (Q - P) by RLVECT_1:def 8;
then 1 = r - r * s by A3,Th08;
hence thesis by A4,XCMPLX_1:89;
end;
theorem Th13:
P,Q,R are_collinear & P <> R & Q <> R implies
affine-ratio(R,P,Q) = 1 / (1 - affine-ratio(P,Q,R))
proof
assume that
A1: P,Q,R are_collinear and
A2: P <> R and
A3: Q <> R;
set r = affine-ratio(P,Q,R),
s = affine-ratio(R,P,Q);
A4: 1 - r <> 0 by A1,A2,A3,Th07;
A5: r * (R - P) = Q + 0.V - P by A1,A2,Def02
.= Q + (-R + R) - P by RLVECT_1:5
.= Q - R + R - P by RLVECT_1:def 3
.= Q - R + --(R - P) by RLVECT_1:def 3
.= Q - R - (P - R) by RLVECT_1:33;
A6: R,P,Q are_collinear by A1;
then - (s * (Q - R)) = - (P - R) by A3,Def02
.= R - P by RLVECT_1:33;
then
A7: R - P = (-1) * (s * (Q - R)) by RLVECT_1:16
.= ((-1) * s) * (Q - R) by RLVECT_1:def 7
.= (-s) * (Q - R);
r * (R - P) = (Q - R) + -(s * (Q - R)) by A5,A6,A3,Def02
.= (Q - R) + (-1) * (s * (Q - R)) by RLVECT_1:16
.= (Q - R) + ((-1) * s) * (Q - R) by RLVECT_1:def 7
.= 1 * (Q - R) + (-s) * (Q - R) by RLVECT_1:def 8
.= (1 - s) * (Q - R) by RLVECT_1:def 6;
then (r * (-s)) * (Q - R) = (1 - s) * (Q - R) by A7,RLVECT_1:def 7;
then - r * s = (1 - s) by Th08,A3;
then s * (1 - r) = 1;
hence thesis by A4,XCMPLX_1:89;
end;
theorem
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
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
let a be non zero Real;
assume
A1: P,Q,R are_collinear & P <> R;
reconsider aP = a * P, aQ = a * Q, aR = a * R as Element of V;
now
thus aP <> aR by A1,RLVECT_1:36;
Q in Line(P,R) by A1,RLTOPSP1:80;
then Q in the set of all (1 - l) * P + l * R where l is Real
by RLTOPSP1:def 14;
then consider l be Real such that
A2: Q = (1 - l) * P + l * R;
reconsider aL = Line(aP,aR) as line of V;
H1: aP in aL & aR in aL by RLTOPSP1:72;
aQ = a * ((1 - l) * P) + a * (l * R) by A2,RLVECT_1:def 5
.= (a * (1 - l)) * P + a * (l * R) by RLVECT_1:def 7
.= (a * (1 - l)) * P + (a * l) * R by RLVECT_1:def 7
.= (1 - l) * (a * P) + (a * l) * R by RLVECT_1:def 7
.= (1 - l) * aP + l * aR by RLVECT_1:def 7;
then aQ in the set of all (1 - l) * aP + l * aR where l is Real;
then aQ in aL by RLTOPSP1:def 14;
hence aP,aQ,aR are_collinear by H1;
end;
then aQ - aP = affine-ratio(aP,aQ,aR) * (aR - aP) by Def02;
then a * (Q - P) = affine-ratio(aP,aQ,aR) * (aR - aP) by RLVECT_1:34;
then a * (Q - P) = affine-ratio(aP,aQ,aR) * (a * (R - P))
by RLVECT_1:34;
then a * (Q - P) = (affine-ratio(aP,aQ,aR) * a) * (R - P)
by RLVECT_1:def 7;
then a * (Q - P) = a * (affine-ratio(aP,aQ,aR) * (R - P))
by RLVECT_1:def 7;
then Q - P = affine-ratio(aP,aQ,aR) * (R - P) by RLVECT_1:36;
hence thesis by A1,Def02;
end;
theorem
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
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
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
for x being Element of TOP-REAL 1
for p being Tuple of 1,REAL st
p = x holds - x = - p;
theorem Th14:
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
let T be RealLinearSpace;
let x,y be Element of T;
let p,q be Tuple of 1,REAL;
assume that
A1: T = TOP-REAL 1 and
A2: p = x and
A3: q = y;
A4: p in Funcs(Seg 1,REAL) & q is Element of Funcs(Seg 1,REAL) by SRINGS_5:11;
(the addF of the RLSStruct of TOP-REAL 1).(p,q)
= (the addF of RealVectSpace Seg 1).(p,q) by EUCLID:def 8
.= p + q by A4,FUNCSDOM:def 1;
hence thesis by A1,A2,A3,ALGSTR_0:def 1;
end;
theorem Th15:
for p being Tuple of 1,REAL holds - p is Tuple of 1,REAL
proof
let p be Tuple of 1,REAL;
consider d be Element of REAL such that
A1: p = <* d *> by FINSEQ_2:97;
-p = <* -d *> by A1,RVSUM_1:20;
hence thesis;
end;
theorem Th16:
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
let T be RealLinearSpace;
let x be Element of T;
let p be Tuple of 1,REAL;
assume that
A1: T = TOP-REAL 1 and
A2: p = x;
consider d be Element of REAL such that
A3: p = <* d *> by FINSEQ_2:97;
reconsider x9 = <* -d *> as Tuple of 1,REAL;
reconsider n = 1 as Nat;
REAL is non empty & REAL c= REAL;
then reconsider p9 = p as Element of 1-tuples_on REAL
by FINSEQ_2:109;
A4: the RLSStruct of TOP-REAL 1 = RealVectSpace Seg 1 & 0.REAL 1 = <* 0 *>
by EUCLID:def 8,FINSEQ_2:59;
A5: p + (-p) = p9 + (-p9)
.= 0.TOP-REAL 1 by A4,RVSUM_1:22;
the TopStruct of TOP-REAL 1 = TopSpaceMetr Euclid 1 by EUCLID:def 8;
then reconsider x99 = x9 as Element of T by A1;
A6: -p = <* -d *> by A3,RVSUM_1:20;
x + x99 = 0.T by A1,A2,A6,Th14,A5;
then - x = x99 by RLVECT_1:def 10;
hence thesis by A3,RVSUM_1:20;
end;
theorem Th17:
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
let T be RealLinearSpace;
let x be Element of T;
let p be Element of TOP-REAL 1;
assume that
A1: T = TOP-REAL 1 and
A2: p = x;
p is Element of REAL 1 by EUCLID:22;
then reconsider p9 = p as Tuple of 1,REAL;
- p9 = - x by A1,A2,Th16;
hence thesis;
end;
theorem Th18:
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
let T be RealLinearSpace;
let x,y be Element of T;
let p,q be Tuple of 1,REAL;
assume that
A1: T = TOP-REAL 1 and
A2: p = x and
A3: q = y;
set p9 = p, q9 = q;
reconsider y9 = -y as Element of T;
reconsider qm9 = -q as Tuple of 1,REAL by Th15;
A4: p9 in Funcs(Seg 1,REAL) &
qm9 is Element of Funcs(Seg 1,REAL) by SRINGS_5:11;
A5: (the addF of the RLSStruct of TOP-REAL 1).(p9,qm9)
= (the addF of RealVectSpace Seg 1).(p9,qm9) by EUCLID:def 8
.= p9 + qm9 by A4,FUNCSDOM:def 1;
x - y = (the addF of (TOP-REAL 1)).(x,-y) by A1,ALGSTR_0:def 1
.= p - q by A5,A1,A2,A3,Th16;
hence thesis;
end;
theorem Th19:
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
let T be RealLinearSpace;
let x,y be Element of T;
let p,q be Element of TOP-REAL 1;
assume that
A1: T = TOP-REAL 1 and
A2: p = x and
A3: q = y;
reconsider p9 = p,q9 = q as Element of REAL 1 by EUCLID:22;
x + y = p9 + q9 by A1,A2,A3,Th14;
hence thesis;
end;
theorem Th20:
for D being set
for d being Element of D holds Seg 1 --> d = <* d *>
proof
let D be set;
let d be Element of D;
Seg 1 --> d = 1 |-> d
.= <* d *> by FINSEQ_2:59;
hence thesis;
end;
theorem Th21:
for a,r being Real holds
multreal.:( Seg 1 --> a, <* r *> ) = <* a * r *>
proof
let a,r be Real;
reconsider r1 = a, r2 = r as Element of REAL by XREAL_0:def 1;
a is Element of REAL by XREAL_0:def 1;
then multreal.:( Seg 1 --> a, <* r *> ) = multreal.:(<* a *>, <* r *>)
by Th20
.= <* multreal.(r1,r2) *>
by FINSEQ_2:74
.= <* r1 * r2 *> by BINOP_2:def 11;
hence thesis;
end;
theorem Th22:
for a being Real for p being Tuple of 1,REAL holds
multreal.:(dom p --> a,p) = a * p
proof
let a be Real;
let p be Tuple of 1,REAL;
consider d be Element of REAL such that
A1: p = <* d *> by FINSEQ_2:97;
A2: a * p = <* a * d *> by A1,RVSUM_1:47;
dom p = Seg 1 by A1,FINSEQ_1:def 8;
hence thesis by A1,A2,Th21;
end;
theorem
for a being Real for p being Tuple of 1,REAL holds
multreal.:(dom p --> a,p) = a * p by Th22;
theorem Th23:
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
let T be RealLinearSpace;
let x,y be Element of T;
let a be Real;
let p,q be Tuple of 1,REAL;
assume that
A1: T = TOP-REAL 1 and
A2: p = x and
A3: q = y and
A4: x = a * y;
set p9 = q;
A5: p9 in Funcs(Seg 1,REAL) by SRINGS_5:11;
(the Mult of the RLSStruct of TOP-REAL 1).(a,p9)
= (the Mult of RealVectSpace Seg 1).(a,p9) by EUCLID:def 8
.= multreal[;](a,p9) by A5,FUNCSDOM:def 3
.= multreal.:(dom p9 --> a,p9) by FUNCOP_1:31
.= a * p9 by Th22;
hence thesis by A1,A2,A3,A4;
end;
theorem
for T being RealLinearSpace for x,y being Element of T
for a being Real for p,q being Element of TOP-REAL 1 st
T = TOP-REAL 1 & p = x & q = y holds x = a * y implies p = a * q
proof
let T be RealLinearSpace;
let x,y be Element of T;
let a be Real;
let p,q be Element of TOP-REAL 1;
assume that
A1: T = TOP-REAL 1 and
A2: p = x and
A3: q = y and
A4: x = a * y;
p is Element of REAL 1 & q is Element of REAL 1 by EUCLID:22;
then reconsider p9 = p,q9 = q as Tuple of 1,REAL;
p9 = a * q9 by A1,A2,A3,A4,Th23;
hence thesis;
end;
theorem
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
let T be RealLinearSpace;
let x,y be Element of T;
let p,q be Element of TOP-REAL 1;
assume that
A1: T = TOP-REAL 1 and
A2: p = x and
A3: q = y;
reconsider y9 = -y as Element of T;
reconsider q as Element of REAL 1 by EUCLID:22;
reconsider q9 = -q as Element of TOP-REAL 1 by EUCLID:22;
- q = - y by A1,A3,Th17;
hence thesis by A1,A2,Th19;
end;
theorem Th24:
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
let p,q be Tuple of 1,REAL;
let r be Real;
assume that
A1: p = r * q and
A2: p <> <* 0 *>;
consider r1 be Element of REAL such that
A3: p = <* r1 *> by FINSEQ_2:97;
consider r2 be Element of REAL such that
A4: q = <* r2 *> by FINSEQ_2:97;
reconsider r1,r2 as Real;
take r1,r2;
A5: <* r1 *> = <* r * r2 *> by A1,A3,A4,RVSUM_1:47;
then
A6: r1 = r * r2 by FINSEQ_1:76;
per cases;
suppose
r2 = 0;
hence thesis by A5,A2,A3;
end;
suppose
A7: r2 <> 0;
r = r * 1
.= r * (r2 / r2) by A7,XCMPLX_1:60
.= r1 / r2 by A6;
hence thesis by A3,A4;
end;
end;
theorem Th25:
for x,y,z being Element of TOP-REAL 1 holds x,y,z are_collinear
proof
let x,y,z be Element of TOP-REAL 1;
per cases;
suppose
A1: z <> y;
reconsider L = Line(y,z) as line of TOP-REAL 1;
H1: y in L & z in L by RLTOPSP1:72;
reconsider x1 = x,y1 = y,z1 = z as Element of REAL 1 by EUCLID:22;
A2: x1 in REAL 1 & y1 in REAL 1 & z1 in REAL 1;
consider xr be Element of REAL such that
A3: x = <* xr *> by A2,FINSEQ_2:97;
consider yr be Element of REAL such that
A4: y = <* yr *> by A2,FINSEQ_2:97;
consider zr be Element of REAL such that
A5: z = <* zr *> by A2,FINSEQ_2:97;
A6: zr - yr <> 0 by A4,A5,A1;
reconsider r = (xr - yr) / (zr - yr) as Real;
A7: (1 - r) * yr + r * zr = yr + (xr -yr) / (zr - yr) * (zr - yr)
.= yr + (xr - yr) by A6,XCMPLX_1:87
.= xr;
(1 - r) * y1 + r * z1 = <* (1 - r) * yr *> + r * <* zr *>
by A4,A5,RVSUM_1:47
.= <* (1 - r) * yr *> + <* r * zr *> by RVSUM_1:47
.= x by RVSUM_1:13,A3,A7;
then x in the set of all (1 - r) * y1 + r * z1 where r is Real;
then x in Line(y1,z1) by EUCLID_4:def 1;
then x in L by EUCLID12:4;
hence thesis by H1;
end;
suppose z = y;
then x in Line(x,y) & y in Line(x,y) & z in Line(x,y) by RLTOPSP1:72;
hence thesis;
end;
end;
theorem
for T being RealLinearSpace st T = TOP-REAL 1
for x,y,z being Element of T holds x,y,z are_collinear by Th25;
theorem Th26:
for T being RealLinearSpace st T = TOP-REAL 1
for x,y,z being Element of T st z <> x & y <> x holds
ex a,b,c being Real st x = <* a *> & y = <* b *> & z = <* c *> &
affine-ratio(x,y,z) = (b - a) / (c - a)
proof
let T be RealLinearSpace;
assume
A1: T = TOP-REAL 1;
let x,y,z be Element of T;
assume that
A2: z <> x and
A3: y <> x;
reconsider p9 = x,q9 = y,r9 = z as Element of REAL 1 by A1,EUCLID:22;
reconsider p = p9, q = q9,r = r9 as Tuple of 1,REAL;
set ma = affine-ratio(x,y,z);
reconsider yx = y - x, zx = z - x as Element of T;
q9 - p9 is Element of 1-tuples_on REAL &
r9 - p9 is Element of 1-tuples_on REAL;
then reconsider qp = q - p, rp = r - p as Tuple of 1,REAL;
A4: qp = yx & rp = zx by A1,Th18;
consider r1 be Element of REAL such that
A5: q = <* r1 *> by FINSEQ_2:97;
consider r2 be Element of REAL such that
A6: p = <* r2 *> by FINSEQ_2:97;
consider r3 be Element of REAL such that
A7: r = <* r3 *> by FINSEQ_2:97;
A8: qp =<* r1 - r2 *> & rp = <* r3 - r2 *> by A5,A6,A7,RVSUM_1:29;
now
x,y,z are_collinear by A1,Th25;
then (y - x) = ma * (z - x) by A2,Def02;
hence qp = ma * rp by A4,A1,Th23;
thus qp <> <* 0 *>
proof
assume qp = <* 0 *>;
then r1 - r2 = 0 by A8,FINSEQ_1:76;
hence contradiction by A5,A6,A3;
end;
end;
then consider a,b be Real such that
A9: qp = <* a *> and
A10: rp =<* b *> and
A11: ma = a / b by Th24;
reconsider s1 = r1 - r2, s2 = r3 - r2 as Real;
A12: a = s1 & b = s2 by A9,A10,A8,FINSEQ_1:76;
reconsider r2,r1,r3 as Real;
take r2,r1,r3;
thus thesis by A11,A12,A5,A6,A7;
end;
theorem Th27:
for x being Element of TOP-REAL 1 for a,r being Real st
x = <* a *> holds r * x = <* (r * a) *>
proof
let x be Element of TOP-REAL 1;
let a,r be Real;
assume x = <* a *>; then
A1: x.1 = a;
reconsider x9 = x as Element of REAL 1 by EUCLID:22;
A2: (r * x9).1 = r * x.1 by RVSUM_1:44;
r * x9 in REAL 1;
then r * x is Element of TOP-REAL 1 by EUCLID:22;
then consider b be Real such that
A3: r * x = <* b *> by JORDAN2B:20;
thus thesis by A1,A3,A2;
end;
theorem
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
let x,y be Element of TOP-REAL 1;
let a,b,r be Real;
assume that
A1: x = <* a *> and
A2: y = <* b *>;
reconsider rb = r * b as Real;
hereby
assume x = r * y;
then x = <* rb *> by A2,Th27;
hence a = r * b by A1,FINSEQ_1:76;
end;
assume a = r * b;
hence x = r * y by A2,A1,Th27;
end;
theorem
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
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
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:
for V being RealLinearSpace for P,Q,R being Element of V st
P,Q,R are_collinear & P <> R & Q <> R & P <> Q holds
ex r being non unit non zero Real st
r = affine-ratio(P,Q,R) &
affine-ratio(P,R,Q) = op1(r) &
affine-ratio(Q,P,R) = op1(op2(op1(r))) &
affine-ratio(Q,R,P) = op2(op1(r)) &
affine-ratio(R,P,Q) = op1(op2(r)) &
affine-ratio(R,Q,P) = op2(r)
proof
let V be RealLinearSpace;
let P,Q,R be Element of V;
assume that
A1: P,Q,R are_collinear and
A2: P <> R and
A3: Q <> R and
A4: P <> Q;
A5: affine-ratio(P,Q,R) <> 0 & affine-ratio(P,Q,R) <> 1
by A1,A2,A3,A4,Th06,Th07;
reconsider r = affine-ratio(P,Q,R) as Element of REAL
by XREAL_0:def 1;
reconsider r9 = r as non unit non zero Real by A5,Def01;
take r9;
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 A1,A2,A3,A4,Th09,Th10,Th11,Th12,Th13;
hence thesis by Th01;
end;
begin :: Cross-Ratio
theorem
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
for X being non empty set
for x being Tuple of 4,X holds
pi_1324(pi_1243(x)) = pi_1423(x) & pi_2143(pi_1243(x)) = pi_2134(x) &
pi_3412(pi_1243(x)) = pi_4312(x) & pi_4321(pi_1243(x)) = pi_3421(x) &
pi_3412(pi_1324(x)) = pi_2413(x) & pi_2143(pi_1324(x)) = pi_3142(x) &
pi_4321(pi_1324(x)) = pi_4231(x) & pi_3412(pi_1423(x)) = pi_2314(x) &
pi_2143(pi_1423(x)) = pi_4132(x) & pi_4321(pi_1423(x)) = pi_3241(x) &
pi_1243(pi_1423(x)) = pi_1432(x) & pi_4321(pi_1432(x)) = pi_2341(x) &
pi_3412(pi_1432(x)) = pi_3214(x) & pi_2143(pi_1432(x)) = pi_4123(x) &
pi_4321(pi_3124(x)) = pi_4213(x) & pi_3412(pi_3124(x)) = pi_2431(x) &
pi_2143(pi_3124(x)) = pi_1342(x) & pi_4312(pi_3124(x)) = pi_4231(x) &
pi_4321(pi_3124(x)) = pi_4213(x);
reserve x for Tuple of 4,the carrier of V,
P9,Q9,R9,S9 for Element of V;
definition
let V being RealLinearSpace;
let P,Q,R,S being Element of V;
func cross-ratio(P,Q,R,S) -> Real equals
affine-ratio(R,P,Q) / affine-ratio(S,P,Q);
coherence;
end;
theorem Th31:
P,Q,R,S are_collinear & R <> Q & S <> Q & S <> P implies
(R = P iff cross-ratio(P,Q,R,S) = 0)
proof
assume that
A1: P,Q,R,S are_collinear and
A2: R <> Q and
A3: S <> Q and
A4: S <> P;
consider L be line of V such that
A5: P in L & Q in L & R in L & S in L by A1;
A6: R,P,Q are_collinear & S,P,Q are_collinear by A5;
hereby
assume R = P;
then affine-ratio(R,P,Q) = 0 by A6,A2,Th06;
hence cross-ratio(P,Q,R,S) = 0;
end;
assume
A7: cross-ratio(P,Q,R,S) = 0;
per cases;
suppose affine-ratio(S,P,Q) = 0;
hence R = P by A3,A4,A6,Th06;
end;
suppose affine-ratio(S,P,Q) <> 0;
then affine-ratio(R,P,Q) = 0 by A7;
hence R = P by A2,A6,Th06;
end;
end;
theorem
P <> R & P <> S implies cross-ratio(P,P,R,S) = 1
proof
assume that
A1: P <> R and
A2: P <> S;
R,P,P are_collinear & S,P,P are_collinear by Th05;
then affine-ratio(R,P,P) = 1 & affine-ratio(S,P,P) = 1
by A1,A2,Th07;
hence thesis;
end;
theorem Th32:
P,Q,R,S are_collinear & R <> Q & S <> Q & R <> S &
cross-ratio(P,Q,R,S) = 1 implies P = Q
proof
assume that
A1: P,Q,R,S are_collinear and
A2: R <> Q and
A3: S <> Q and
A4: R <> S and
A5: cross-ratio(P,Q,R,S) = 1;
A6: affine-ratio(R,P,Q) = affine-ratio(S,P,Q) by A5,XCMPLX_1:58;
set r = affine-ratio(R,P,Q);
A7: R,P,Q are_collinear & S,P,Q are_collinear by A1;
then P + 0.V - R = r * (Q + 0.V - R) by A2,Def02;
then P + (-S + S) - R = r * (Q + 0.V - R) by RLVECT_1:5
.= r * (Q + (-S + S) - R) by RLVECT_1:5
.= r * (Q - S + S - R) by RLVECT_1:def 3;
then P - S + S - R = r * (Q - S + S - R) by RLVECT_1:def 3
.= r * ((Q - S) + (S - R)) by RLVECT_1:def 3
.= r * (Q - S) + r * (S - R) by RLVECT_1:def 5
.= (P - S) + r * (S - R) by A7,A6,A3,Def02;
then -(P - S) + ((P - S) + (S - R)) = -(P - S) + ((P - S) + r * (S - R))
by RLVECT_1:def 3;
then (-(P - S) + (P - S)) + (S - R) = -(P - S) + ((P - S) + r * (S - R))
by RLVECT_1:def 3
.= (-(P - S) + (P - S)) + r * (S - R)
by RLVECT_1:def 3;
then r * (S - R) = S - R by RLVECT_1:8
.= 1 * (S - R) by RLVECT_1:def 8;
then r = 1 by A4,Th08;
hence P = Q by A2,Th07,A7;
end;
theorem
P,Q,R,S are_collinear & P9,Q9,R9,S9 are_collinear & S <> P & S <> Q &
S9 <> P9 & S9 <> Q9 implies
(cross-ratio(P,Q,R,S) = cross-ratio(P9,Q9,R9,S9) iff
affine-ratio(R,P,Q) * affine-ratio(S9,P9,Q9) =
affine-ratio(R9,P9,Q9) * affine-ratio(S,P,Q))
proof
assume that
A1: P,Q,R,S are_collinear and
A2: P9,Q9,R9,S9 are_collinear and
A3: S <> P and
A4: S <> Q and
A5: S9 <> P9 and
A6: S9 <> Q9;
set r = affine-ratio(R,P,Q), s = affine-ratio(S,P,Q),
r9 = affine-ratio(R9,P9,Q9), s9 = affine-ratio(S9,P9,Q9);
S,P,Q are_collinear & S9,P9,Q9 are_collinear by A1,A2;
then s <> 0 & s9 <> 0 by A3,A4,A5,A6,Th06;
hence thesis by XCMPLX_1:94,95;
end;
Lm02:
for r being Real st
P - Q = r * (R - S) holds Q - P = r * (S - R)
proof
let r be Real;
assume
A1: P - Q = r * (R - S);
Q - P = - r * (R - S) by A1,RLVECT_1:33
.= r * (-(R-S)) by RLVECT_1:25
.= r * (S - R) by RLVECT_1:33;
hence thesis;
end;
theorem Th33:
P,Q,R,S are_collinear & P <> S & R <> Q & S <> Q implies
cross-ratio(P,Q,R,S) = cross-ratio(R,S,P,Q)
proof
assume that
A1: P,Q,R,S are_collinear and
A2: P <> S and
A3: R <> Q and
A4: S <> Q;
A5: R,P,Q are_collinear & P,R,S are_collinear & S,P,Q are_collinear &
Q,R,S are_collinear by A1;
set r1 = affine-ratio(R,P,Q), r2 = affine-ratio(S,P,Q),
s1 = affine-ratio(P,R,S), s2 = affine-ratio(Q,R,S);
A6: r2 <> 0 & s2 <> 0 by A2,A3,A4,A5,Th06;
A7: Q - S <> 0.V by A4,RLVECT_1:21;
A8: P - R = r1 * (Q - R) by A5,A3,Def02;
A9: P - S = r2 * (Q - S) by A5,A4,Def02;
R - Q = s2 * (S - Q) by A5,A4,Def02; then
A10: Q - R = s2 * (Q - S) by Lm02;
R - P = s1 * (S - P) by A5,A2,Def02;
then P - R = s1 * (P - S) by Lm02
.= s1 * r2 * (Q - S) by A9,RLVECT_1:def 7;
then r1 * s2 * (Q - S) = s1 * r2 * (Q - S) by A8,A10,RLVECT_1:def 7;
hence thesis by A7,RLVECT_1:37,A6,XCMPLX_1:94;
end;
theorem Th34:
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
let V be RealLinearSpace;
let P,Q,R,S be Element of V;
assume that
A1: P,Q,R,S are_collinear and
A2: P <> R and
A3: P <> S and
A4: R <> Q and
A5: S <> Q;
set r1 = affine-ratio(R,P,Q), r2 = affine-ratio(S,P,Q),
s1 = affine-ratio(S,Q,P), s2 = affine-ratio(R,Q,P);
per cases;
suppose
A6: P = Q;
R,P,P are_collinear & S,P,P are_collinear by Th05;
then r1 = 1 & r2 = 1 & s1 = 1 & s2 = 1 by A2,A3,A6,Th07;
hence thesis;
end;
suppose
A7: P <> Q;
P,Q,R are_collinear by A1;
then consider r9 be non unit non zero Real such that
A8: r9 = affine-ratio(P,Q,R) &
affine-ratio(P,R,Q) = op1(r9) &
affine-ratio(Q,P,R) = op1(op2(op1(r9))) &
affine-ratio(Q,R,P) = op2(op1(r9)) &
affine-ratio(R,P,Q) = op1(op2(r9)) &
affine-ratio(R,Q,P) = op2(r9) by A2,A4,A7,Th28;
P,Q,S are_collinear & P <> S & Q <> S by A1,A3,A5;
then ex s9 be non unit non zero Real st
s9 = affine-ratio(P,Q,S) &
affine-ratio(P,S,Q) = op1(s9) &
affine-ratio(Q,P,S) = op1(op2(op1(s9))) &
affine-ratio(Q,S,P) = op2(op1(s9)) &
affine-ratio(S,P,Q) = op1(op2(s9)) &
affine-ratio(S,Q,P) = op2(s9) by A7,Th28;
hence thesis by A8;
end;
end;
theorem Th34bis:
P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies
cross-ratio(P,Q,R,S) = cross-ratio(S,R,Q,P)
proof
assume that
A1: P,Q,R,S are_collinear and
A2: P <> R and
A3: P <> S and
A4: R <> Q and
A5: S <> Q;
R,S,P,Q are_collinear by A1;
then cross-ratio(R,S,P,Q) = cross-ratio(S,R,Q,P) by A2,A3,A4,A5,Th34;
hence thesis by A1,A3,A4,A5,Th33;
end;
theorem
cross-ratio(P,Q,S,R) = 1 / cross-ratio(P,Q,R,S) by XCMPLX_1:57;
theorem
P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies
cross-ratio(Q,P,R,S) = 1 / cross-ratio(P,Q,R,S)
proof
assume that
A1: P,Q,R,S are_collinear and
A2: P <> R and
A3: P <> S and
A4: R <> Q and
A5: S <> Q;
A6: cross-ratio(P,Q,S,R) = 1 / cross-ratio(P,Q,R,S) by XCMPLX_1:57;
Q,P,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q
by A2,A3,A4,A5,A1;
hence thesis by A6,Th34;
end;
theorem
P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies
cross-ratio(R,S,Q,P) = 1 / cross-ratio(P,Q,R,S)
proof
assume that
A1: P,Q,R,S are_collinear and
A2: P <> R and
A3: P <> S and
A4: R <> Q and
A5: S <> Q;
A6: cross-ratio(P,Q,S,R) = 1 / cross-ratio(P,Q,R,S) by XCMPLX_1:57;
P,Q,S,R are_collinear & P <> R & P <> S & R <> Q & S <> Q
by A1,A2,A3,A4,A5;
hence thesis by A6,Th34bis;
end;
theorem
P,Q,R,S are_collinear & P <> R & P <> S & R <> Q & S <> Q implies
cross-ratio(S,R,P,Q) = 1 / cross-ratio(P,Q,R,S)
proof
assume that
A1: P,Q,R,S are_collinear and
A2: P <> R and
A3: P <> S and
A4: R <> Q and
A5: S <> Q;
A6: cross-ratio(P,Q,S,R) = 1 / cross-ratio(P,Q,R,S) by XCMPLX_1:57;
S,R,P,Q are_collinear & P <> R & P <> S & R <> Q & S <> Q
by A1,A2,A3,A4,A5;
hence thesis by A6,Th33;
end;
theorem Th35:
P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct implies
cross-ratio(P,R,Q,S) = 1 - cross-ratio(P,Q,R,S)
proof
assume that
A1: P,Q,R,S are_collinear and
A2: P,Q,R,S are_mutually_distinct;
A3: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2,ZFMISC_1:def 6;
set r1 = affine-ratio(R,P,Q), r2 = affine-ratio(S,P,Q),
s1 = affine-ratio(Q,P,R), s2 = affine-ratio(S,P,R),
r = affine-ratio(P,Q,R);
A4: P,Q,R are_collinear by A1;
then
A5: r1 = 1 / (1 -r) & s1 = r / (r - 1) by A3,Th10,Th13;
P,Q,R are_collinear by A1;
then
A6: r - 1 <> 0 by A3,Th07;
A7: 1 - s1 = r1
proof
1 - s1 = 1 - r / (r - 1) by A4,A3,Th10
.= (r - 1) / (r - 1) - r / (r - 1) by A6,XCMPLX_1:60
.= (-1) / (r - 1)
.= 1 / (-(r - 1)) by XCMPLX_1:192;
hence thesis by A5;
end;
R <> Q & R,P,Q are_collinear by A1,A2,ZFMISC_1:def 6;
then
A8: r2 * (P - R) = r2 * (r1 * (Q - R)) by Def02;
A9: S <> Q & S,P,Q are_collinear by A1,A2,ZFMISC_1:def 6;
A10: S <> R & S,P,R are_collinear by A1,A2,ZFMISC_1:def 6; then
A11: P - S = s2 * (R - S) by Def02;
S,P,Q are_collinear by A1; then
A12: r2 <> 0 by A3,Th06;
S,P,R are_collinear by A1; then
A13: s2 <> 0 by A3,Th06;
P - R = P + 0.V - R
.= P + (-S + S) - R by RLVECT_1:5
.= ((P - S) + S) - R by RLVECT_1:def 3
.= (P - S) + (S - R) by RLVECT_1:def 3
.= s2 * (R - S) + (S - R) by A10,Def02
.= s2 * (R - S) + -(R - S) by RLVECT_1:33
.= s2 * (R - S) + (-1) * (R - S) by RLVECT_1:16
.= (s2 - 1) * (R - S) by RLVECT_1:def 6;
then
A14: r2 * (P - R) = (r2 * (s2 - 1)) * (R - S) by RLVECT_1:def 7;
r1 * (Q - R) = r1 * (Q + 0.V - R)
.= r1 * (Q + (-S + S) - R) by RLVECT_1:5
.= r1 * (Q - S + S - R) by RLVECT_1:def 3
.= r1 * ((Q - S) + (S - R)) by RLVECT_1:def 3
.= r1 * (Q - S) + r1 * (S - R) by RLVECT_1:def 5
.= r1 * (Q - S) + r1 * ( - (R - S)) by RLVECT_1:33
.= r1 * (Q - S) + r1 * ((-1) * (R - S)) by RLVECT_1:16
.= r1 * (Q - S) + (r1 * (-1)) * (R - S) by RLVECT_1:def 7
.= r1 * (Q - S) + (-r1) * (R - S);
then r2 * (r1 * (Q - R)) = r2 * (r1 * ((Q - S))) + r2 * ((-r1) * (R - S))
by RLVECT_1:def 5
.= (r2 * r1) * (Q - S) + r2 * ((-r1) * (R - S))
by RLVECT_1:def 7
.= r1 * (r2 * (Q - S)) + r2 * ((-r1) * (R - S))
by RLVECT_1:def 7
.= r1 * (s2 * (R - S)) + r2 * ((-r1) * (R - S))
by A9,Def02,A11
.= (r1 * s2) * (R - S) + r2 * ((-r1) * (R - S))
by RLVECT_1:def 7
.= (r1 * s2) * (R - S) + (r2 * (-r1)) * (R - S)
by RLVECT_1:def 7
.= (r1 * s2 + (r2 * (-r1))) * (R - S)
by RLVECT_1:def 6;
then r2 * (s2 - 1) = r1 * s2 + (r2 * (-r1)) by A14,A8,A3,Th08;
then r1 * r2 - r2 = r1 * s2 - r2 * s2;
then (-s1) * r2 = (r1 - r2) * s2 by A7;
then s1 * r2 = (r2 - r1) * s2;
then s1 / s2 = (r2 - r1) / r2 by A12,A13,XCMPLX_1:94
.= r2 / r2 - r1 / r2
.= 1 - r1 / r2 by A12,XCMPLX_1:60;
hence thesis;
end;
theorem
P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct implies
cross-ratio(Q,S,P,R) = 1 - cross-ratio(P,Q,R,S)
proof
assume that
A1: P,Q,R,S are_collinear and
A2: P,Q,R,S are_mutually_distinct;
A3: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2,ZFMISC_1:def 6;
P,R,Q,S are_collinear by A1;
then cross-ratio(P,R,Q,S) = cross-ratio(Q,S,P,R) by A3,Th33;
hence thesis by A1,A2,Th35;
end;
theorem
P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct implies
cross-ratio(R,P,S,Q) = 1 - cross-ratio(P,Q,R,S)
proof
assume that
A1: P,Q,R,S are_collinear and
A2: P,Q,R,S are_mutually_distinct;
A3: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2,ZFMISC_1:def 6;
P,R,Q,S are_collinear by A1;
then cross-ratio(P,R,Q,S) = cross-ratio(R,P,S,Q) by A3,Th34;
hence thesis by A1,A2,Th35;
end;
theorem
P,Q,R,S are_collinear & P,Q,R,S are_mutually_distinct implies
cross-ratio(S,Q,R,P) = 1 - cross-ratio(P,Q,R,S)
proof
assume that
A1: P,Q,R,S are_collinear and
A2: P,Q,R,S are_mutually_distinct;
A3: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q by A2,ZFMISC_1:def 6;
P,R,Q,S are_collinear by A1;
then cross-ratio(S,Q,R,P) = cross-ratio(P,R,Q,S)
by A3,Th34bis;
hence thesis by A1,A2,Th35;
end;
definition
let V being RealLinearSpace;
let x being Tuple of 4,the carrier of V;
func cross-ratio-tuple(x) -> Real means :Def03:
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
proof
dom x = Seg 4 by FINSEQ_2:124;
then 1 in dom x & 2 in dom x & 3 in dom x & 4 in dom x;
then reconsider P = x.1, Q = x.2, R = x.3, S = x.4 as Element of V
by FINSEQ_2:11;
cross-ratio(P,Q,R,S) is Real;
hence thesis;
end;
uniqueness;
end;
theorem Th36:
x = <* P, Q, R, S *> implies
cross-ratio(P,Q,R,S) = cross-ratio-tuple(x)
proof
assume x = <* P, Q, R, S *>;
then x.1 = P & x.2 = Q & x.3 = R & x.4 = S;
hence thesis by Def03;
end;
theorem Th37:
x = <* P, Q, R, S *> & P,Q,R,S are_collinear &
P <> S & Q <> R & Q <> S implies
cross-ratio-tuple(x) = cross-ratio-tuple(pi_3412(x))
proof
assume that
A1: x = <* P, Q, R, S *> and
A2: P,Q,R,S are_collinear and
A3: P <> S and
A4: Q <> R and
A5: Q <> S;
consider P9,Q9,R9,S9 be Element of V such that
A7: P9 = x.1 & Q9 = x.2 & R9 = x.3 & S9 = x.4 &
cross-ratio-tuple(x) = cross-ratio(P9,Q9,R9,S9) by Def03;
ex P99,Q99,R99,S99 be Element of V st
P99 = (pi_3412(x)).1 & Q99 = (pi_3412(x)).2 &
R99 = (pi_3412(x)).3 & S99 = (pi_3412(x)).4 &
cross-ratio-tuple(pi_3412(x)) = cross-ratio(P99,Q99,R99,S99) by Def03;
hence thesis by A1,A7,A2,A3,A4,A5,Th33;
end;
theorem Th38:
x = <* P, Q, R, S *> & P,Q,R,S are_collinear & P <> R & P <> S &
Q <> R & Q <> S implies
cross-ratio-tuple(x) = cross-ratio-tuple(pi_2143(x)) &
cross-ratio-tuple(x) = cross-ratio-tuple(pi_4321(x))
proof
assume that
A1: x = <* P, Q, R, S *> and
A2: P,Q,R,S are_collinear and
A3: P <> R and
A4: P <> S and
A5: Q <> R and
A6: Q <> S;
A8: ex P9,Q9,R9,S9 be Element of V st P9 = x.1 & Q9 = x.2 & R9 = x.3 &
S9 = x.4 & cross-ratio-tuple(x) = cross-ratio(P9,Q9,R9,S9) by Def03;
H1: ex P99,Q99,R99,S99 be Element of V st P99 = (pi_2143(x)).1 &
Q99 = (pi_2143(x)).2 & R99 = (pi_2143(x)).3 & S99 = (pi_2143(x)).4 &
cross-ratio-tuple(pi_2143(x)) = cross-ratio(P99,Q99,R99,S99) by Def03;
ex P99,Q99,R99,S99 be Element of V st P99 = (pi_4321(x)).1 &
Q99 = (pi_4321(x)).2 & R99 = (pi_4321(x)).3 & S99 = (pi_4321(x)).4 &
cross-ratio-tuple(pi_4321(x)) = cross-ratio(P99,Q99,R99,S99) by Def03;
hence thesis by H1,A6,A1,A8,A2,A3,A4,A5,Th34,Th34bis;
end;
theorem Th39:
cross-ratio-tuple(pi_1243(x)) = 1 / cross-ratio-tuple(x)
proof
consider P9,Q9,R9,S9 be Element of V such that
A1: P9 = x.1 & Q9 = x.2 & R9 = x.3 & S9 = x.4 &
cross-ratio-tuple(x) = cross-ratio(P9,Q9,R9,S9) by Def03;
ex P99,Q99,R99,S99 be Element of V st
P99 = (pi_1243(x)).1 & Q99 = (pi_1243(x)).2 &
R99 = (pi_1243(x)).3 & S99 = (pi_1243(x)).4 &
cross-ratio-tuple(pi_1243(x)) = cross-ratio(P99,Q99,R99,S99) by Def03;
hence thesis by A1,XCMPLX_1:57;
end;
theorem
x = <*P,Q,R,S*> & P,Q,R,S are_mutually_distinct &
P,Q,R,S are_collinear implies
(ex r being non unit non zero Real st r = cross-ratio-tuple(x) &
cross-ratio-tuple(pi_1243(x)) = op1(r))
proof
assume that
A1: x = <*P,Q,R,S*> and
A2: P,Q,R,S are_mutually_distinct and
A3: P,Q,R,S are_collinear;
A4: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q
by A2,ZFMISC_1:def 6;
consider P9,Q9,R9,S9 be Element of V such that
A5: P9 = x.1 & Q9 = x.2 & R9 = x.3 & S9 = x.4 &
cross-ratio-tuple(x) = cross-ratio(P9,Q9,R9,S9) by Def03;
reconsider r=cross-ratio-tuple(x) as non unit non zero Real
by Def01,A1,A3,A5,A4,Th32,Th31;
take r;
thus thesis by Th39;
end;
theorem Th40:
x = <*P,Q,R,S*> & P,Q,R,S are_collinear & P <> R & P <> S &
Q <> R & Q <> S implies
cross-ratio-tuple(pi_1243(x)) = 1 / cross-ratio-tuple(x) &
cross-ratio-tuple(pi_2134(x)) = 1 / cross-ratio-tuple(x) &
cross-ratio-tuple(pi_3421(x)) = 1 / cross-ratio-tuple(x) &
cross-ratio-tuple(pi_4312(x)) = 1 / cross-ratio-tuple(x)
proof
assume that
A1: x = <*P,Q,R,S*> and
A2: P,Q,R,S are_collinear and
A3: P <> R and
A4: P <> S and
A5: Q <> R and
A6: Q <> S;
A7: pi_1243(x) = <*P,Q,S,R*> & P,Q,S,R are_collinear by A2,A1;
consider P9,Q9,R9,S9 be Element of V such that
A8: P9 = x.1 & Q9 = x.2 & R9 = x.3 & S9 = x.4 &
cross-ratio-tuple(x) = cross-ratio(P9,Q9,R9,S9) by Def03;
consider P99,Q99,R99,S99 be Element of V such that
A9: P99 = (pi_1243(x)).1 & Q99 = (pi_1243(x)).2 &
R99 = (pi_1243(x)).3 & S99 = (pi_1243(x)).4 &
cross-ratio-tuple(pi_1243(x)) = cross-ratio(P99,Q99,R99,S99) by Def03;
now
thus cross-ratio-tuple(pi_2134(x))
= cross-ratio-tuple(pi_2143(pi_1243(x)))
.= cross-ratio-tuple(pi_1243(x)) by A7,A3,A4,A5,A6,Th38;
thus cross-ratio-tuple(pi_3421(x))
= cross-ratio-tuple(pi_4321(pi_1243(x)))
.= cross-ratio-tuple(pi_1243(x)) by A7,A3,A4,A5,A6,Th38;
thus cross-ratio-tuple(pi_4312(x))
= cross-ratio-tuple(pi_3412(pi_1243(x)))
.= cross-ratio-tuple(pi_1243(x)) by A7,A3,A5,A6,Th37;
end;
hence thesis by A8,A9,XCMPLX_1:57;
end;
theorem Th41:
x = <* P,Q,R,S *> & P,Q,R,S are_mutually_distinct &
P,Q,R,S are_collinear implies
cross-ratio-tuple(pi_1324(x)) = 1 - cross-ratio-tuple(x) &
cross-ratio-tuple(pi_2413(x)) = 1 - cross-ratio-tuple(x) &
cross-ratio-tuple(pi_3142(x)) = 1 - cross-ratio-tuple(x) &
cross-ratio-tuple(pi_4231(x)) = 1 - cross-ratio-tuple(x)
proof
assume that
A1: x = <* P,Q,R,S *> and
A2: P,Q,R,S are_mutually_distinct and
A3: P,Q,R,S are_collinear;
A4: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q
by A2,ZFMISC_1:def 6;
A6: pi_1324(x) = <*P,R,Q,S*> & P,R,Q,S are_collinear by A3,A1;
now
x.1 = P & x.2 = Q & x.3 = R & x.4 = S & (pi_1324(x)).1 = P &
(pi_1324(x)).2 = R & (pi_1324(x)).3 = Q & (pi_1324(x)).4 = S by A1;
hence cross-ratio-tuple(pi_1324(x)) = cross-ratio(P,R,Q,S) &
cross-ratio-tuple(x) = cross-ratio(P,Q,R,S) by Def03;
thus cross-ratio-tuple(pi_2413(x))
= cross-ratio-tuple(pi_3412(pi_1324(x)))
.= cross-ratio-tuple(pi_1324(x)) by A6,A4,Th37;
thus cross-ratio-tuple(pi_3142(x))
= cross-ratio-tuple(pi_2143(pi_1324(x)))
.= cross-ratio-tuple(pi_1324(x)) by A4,Th38,A6;
thus cross-ratio-tuple(pi_4231(x))
= cross-ratio-tuple(pi_4321(pi_1324(x)))
.= cross-ratio-tuple(pi_1324(x)) by A4,Th38,A6;
end;
hence thesis by A2,A3,Th35;
end;
theorem
x = <* P,Q,R,S *> & P,Q,R,S are_mutually_distinct &
P,Q,R,S are_collinear implies
cross-ratio-tuple(pi_3124(x)) = 1 / (1 - cross-ratio-tuple(x)) &
cross-ratio-tuple(pi_2431(x)) = 1 / (1 - cross-ratio-tuple(x)) &
cross-ratio-tuple(pi_1342(x)) = 1 / (1 - cross-ratio-tuple(x)) &
cross-ratio-tuple(pi_4213(x)) = 1 / (1 - cross-ratio-tuple(x))
proof
assume that
A1: x = <* P,Q,R,S *> and
A2: P,Q,R,S are_mutually_distinct and
A3: P,Q,R,S are_collinear;
A4: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q
by A2,ZFMISC_1:def 6;
A7: cross-ratio-tuple(pi_1243(pi_3142(x))) = 1 / cross-ratio-tuple(pi_3142(x))
by Th39;
hence cross-ratio-tuple(pi_3124(x)) = 1 / (1 - cross-ratio-tuple(x))
by A2,A3,A1,Th41;
A8: pi_3124(x) = <* R,P,Q,S *> & R,P,Q,S are_collinear by A3,A1;
now
thus cross-ratio-tuple(pi_3412(pi_3124(x)))
= cross-ratio-tuple(pi_3124(x)) by A8,Th37,A4
.= 1 / (1 - cross-ratio-tuple(x)) by A3,A7,A1,A2,Th41;
thus cross-ratio-tuple(pi_2143(pi_3124(x)))
= cross-ratio-tuple(pi_3124(x)) by A8,A4,Th38
.= 1 / (1 - cross-ratio-tuple(x))
by A3,A7,A1,A2,Th41;
thus cross-ratio-tuple(pi_4321(pi_3124(x)))
= cross-ratio-tuple(pi_3124(x)) by A4,A8,Th38
.= 1 / (1 - cross-ratio-tuple(x)) by A3,A7,A1,A2,Th41;
end;
hence thesis;
end;
theorem Th42:
x = <* P,Q,R,S *> & P,Q,R,S are_mutually_distinct &
P,Q,R,S are_collinear implies
cross-ratio-tuple(pi_1423(x))
= (cross-ratio-tuple(x) - 1) / cross-ratio-tuple(x) &
cross-ratio-tuple(pi_2314(x))
= (cross-ratio-tuple(x) - 1) / cross-ratio-tuple(x) &
cross-ratio-tuple(pi_4132(x))
= (cross-ratio-tuple(x) - 1) / cross-ratio-tuple(x) &
cross-ratio-tuple(pi_3241(x))
= (cross-ratio-tuple(x) - 1) / cross-ratio-tuple(x)
proof
assume that
A1: x = <* P,Q,R,S *> and
A2: P,Q,R,S are_mutually_distinct and
A3: P,Q,R,S are_collinear;
A4: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q
by A2,ZFMISC_1:def 6;
cross-ratio(P,Q,R,S) <> 0 by A3,A4,Th31;
then reconsider cr = cross-ratio-tuple(x) as non zero Complex by A1,Th36;
pi_1243(x) = <* P,Q,S,R *> & P,Q,S,R are_collinear &
P,Q,S,R are_mutually_distinct by A4,A1,A3,ZFMISC_1:def 6;
then A5: cross-ratio-tuple(pi_1324(pi_1243(x)))
= 1 - cross-ratio-tuple(pi_1243(x)) by Th41
.= 1 - (1 / cr) by A1,A3,A4,Th40
.= cr / cr - 1 / cr by XCMPLX_1:60
.= (cr - 1) / cr;
hence cross-ratio-tuple(pi_1423(x))
= (cross-ratio-tuple(x) - 1) / cross-ratio-tuple(x);
pi_1423(x) = <* P,S,Q,R *> & P,S,Q,R are_collinear by A1,A3;
then cross-ratio-tuple(pi_3412(pi_1423(x)))=cross-ratio-tuple(pi_1423(x)) &
cross-ratio-tuple(pi_2143(pi_1423(x)))=cross-ratio-tuple(pi_1423(x)) &
cross-ratio-tuple(pi_4321(pi_1423(x)))=cross-ratio-tuple(pi_1423(x))
by A4,Th37,Th38;
hence thesis by A5;
end;
theorem
x = <* P,Q,R,S *> & P,Q,R,S are_mutually_distinct &
P,Q,R,S are_collinear implies
cross-ratio-tuple(pi_1432(x))
= cross-ratio-tuple(x) / (cross-ratio-tuple(x) - 1) &
cross-ratio-tuple(pi_2341(x))
= cross-ratio-tuple(x) / (cross-ratio-tuple(x) - 1) &
cross-ratio-tuple(pi_3214(x))
= cross-ratio-tuple(x) / (cross-ratio-tuple(x) - 1) &
cross-ratio-tuple(pi_4123(x))
= cross-ratio-tuple(x) / (cross-ratio-tuple(x) - 1)
proof
assume that
A1: x = <* P,Q,R,S *> and
A2: P,Q,R,S are_mutually_distinct and
A3: P,Q,R,S are_collinear;
A4: P <> R & P <> S & R <> Q & S <> Q & S <> R & P <> Q
by A2,ZFMISC_1:def 6;
A5: P,S,R,Q are_collinear & pi_1432(x) = <*P,S,R,Q*> by A1,A3;
A6: cross-ratio-tuple(pi_1432(x))
= cross-ratio-tuple(pi_1243(pi_1423(x)))
.= 1 / (cross-ratio-tuple(pi_1423(x))) by Th39
.= 1 / ((cross-ratio-tuple(x) - 1) / cross-ratio-tuple(x))
by A1,A3,A2,Th42;
hence cross-ratio-tuple(pi_1432(x))
= cross-ratio-tuple(x) / (cross-ratio-tuple(x) - 1) by XCMPLX_1:57;
now
thus cross-ratio-tuple(pi_2341(x))
= cross-ratio-tuple(pi_4321(pi_1432(x)))
.= cross-ratio-tuple(pi_1432(x)) by A5,A4,Th38;
thus cross-ratio-tuple(pi_3214(x))
= cross-ratio-tuple(pi_3412(pi_1432(x)))
.= cross-ratio-tuple(pi_1432(x)) by A4,A5,Th37;
thus cross-ratio-tuple(pi_4123(x))
= cross-ratio-tuple(pi_2143(pi_1432(x)))
.= cross-ratio-tuple(pi_1432(x)) by A4,A5,Th38;
end;
hence thesis by A6,XCMPLX_1:57;
end;
begin :: Cross-Ratio and real numbers line
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
let a,b,c,d be Complex;
((a - c) / (b - c)) / ((a - d)/(b - d))
= (((-1) * (c - a)) /
(((-1) * (c - b)))) / (((-1) * (d - a))/((-1)*(d - b)))
.= ((c - a) / (c - b)) / (((-1) * (d - a))/((-1)*(d - b))) by XCMPLX_1:91
.= ((c - a) / (c - b)) / ((d - a) / (d - b)) by XCMPLX_1:91
.= ((c - a) / (c - b)) * ((d - b) / (d - a)) by XCMPLX_1:79;
hence thesis;
end;
theorem
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
let x1,x2,x3,x4 be Element of TOP-REAL 1;
assume that
A1: x2 <> x3 and
A2: x3 <> x1 and
A3: x2 <> x4 and
A4: x1 <> x4;
reconsider x = <*x1,x2,x3,x4*> as Tuple of 4,the carrier of TOP-REAL 1;
consider P,Q,R,S be Element of TOP-REAL 1 such that
A5: P = x.1 & Q = x.2 & R = x.3 & S = x.4 &
cross-ratio-tuple(x) = cross-ratio(P,Q,R,S) by Def03;
consider a1,b1,c1 be Real such that
A7: x3 = <* a1 *> & x1 = <* b1 *> & x2 = <* c1 *> &
affine-ratio(x3,x1,x2) = (b1 - a1) / (c1 - a1) by A1,A2,Th26;
consider a2,b2,c2 be Real such that
A8: x4 = <* a2 *> & x1 = <* b2 *> & x2 = <* c2 *> &
affine-ratio(x4,x1,x2) = (b2 - a2) / (c2 - a2) by A3,A4,Th26;
take b1,c1,a1,a2;
b1 = b2 & c1 = c2 by A7,A8,FINSEQ_1:76;
hence thesis by A7,A8,Lm03,A5;
end;