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_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) )
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_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) )
let x be Tuple of 4, the carrier of V; :: thesis: ( 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) ) )
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 ; :: thesis: ( 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) )
A7: ( pi_1243 x = <*P,Q,S,R*> & P,Q,S,R are_collinear ) by A2, A1;
consider P9, Q9, R9, S9 being 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 being 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 :: thesis: ( cross-ratio-tuple (pi_2134 x) = cross-ratio-tuple (pi_1243 x) & cross-ratio-tuple (pi_3421 x) = cross-ratio-tuple (pi_1243 x) & cross-ratio-tuple (pi_4312 x) = cross-ratio-tuple (pi_1243 x) )
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 ; :: thesis: ( cross-ratio-tuple (pi_3421 x) = cross-ratio-tuple (pi_1243 x) & cross-ratio-tuple (pi_4312 x) = cross-ratio-tuple (pi_1243 x) )
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 ; :: thesis: cross-ratio-tuple (pi_4312 x) = cross-ratio-tuple (pi_1243 x)
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 ; :: thesis: verum
end;
hence ( 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) ) by A8, A9, XCMPLX_1:57; :: thesis: verum