let V be 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) )
let P, Q, R, S be 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 x be Tuple of 4, the carrier of V; ( 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
; ( 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 ( 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
;
( 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
;
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
;
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; verum