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 <> S & Q <> R & Q <> S holds
cross-ratio-tuple x = cross-ratio-tuple (pi_3412 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 <> S & Q <> R & Q <> S holds
cross-ratio-tuple x = cross-ratio-tuple (pi_3412 x)
let x be Tuple of 4, the carrier of V; :: thesis: ( 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) )
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 ; :: thesis: cross-ratio-tuple x = cross-ratio-tuple (pi_3412 x)
consider P9, Q9, R9, S9 being 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 being 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 cross-ratio-tuple x = cross-ratio-tuple (pi_3412 x) by A1, A7, A2, A3, A4, A5, Th33; :: thesis: verum