let V be RealLinearSpace; :: thesis: 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) )
let P, Q, R, S be Element of V; :: thesis: 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) )
let x be Tuple of 4, the carrier of V; :: thesis: ( 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) ) )
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 ; :: thesis: ( 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) )
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; :: thesis: ( 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) )
now :: thesis: ( cross-ratio-tuple (pi_2341 x) = cross-ratio-tuple (pi_1432 x) & cross-ratio-tuple (pi_3214 x) = cross-ratio-tuple (pi_1432 x) & cross-ratio-tuple (pi_4123 x) = cross-ratio-tuple (pi_1432 x) )
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 ; :: thesis: ( cross-ratio-tuple (pi_3214 x) = cross-ratio-tuple (pi_1432 x) & cross-ratio-tuple (pi_4123 x) = cross-ratio-tuple (pi_1432 x) )
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 ; :: thesis: cross-ratio-tuple (pi_4123 x) = cross-ratio-tuple (pi_1432 x)
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 ; :: thesis: verum
end;
hence ( 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) ) by A6, XCMPLX_1:57; :: thesis: verum