let OAS be OAffinSpace; for p, q, x, y being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & p,x,y are_collinear holds
x,y // f . y,f . x
let p, q, x, y be Element of OAS; for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & p,x,y are_collinear holds
x,y // f . y,f . x
let f be Permutation of the carrier of OAS; ( f is dilatation & f . p = p & q <> p & Mid q,p,f . q & p,x,y are_collinear implies x,y // f . y,f . x )
assume that
A1:
f is dilatation
and
A2:
f . p = p
and
A3:
( q <> p & Mid q,p,f . q )
and
A4:
p,x,y are_collinear
; x,y // f . y,f . x
A5:
Mid y,p,f . y
by A1, A2, A3, Th60;
A6:
now ( x = p implies x,y // f . y,f . x )end;
A8:
now ( x <> p & y <> p & x <> y implies x,y // f . y,f . x )assume that A9:
x <> p
and
y <> p
and A10:
x <> y
;
x,y // f . y,f . xconsider u being
Element of
OAS such that A11:
not
p,
x,
u are_collinear
by A9, DIRAF:37;
consider r being
Element of
OAS such that A12:
x,
y '||' u,
r
and A13:
x,
u '||' y,
r
by DIRAF:26;
A14:
not
x,
y,
u are_collinear
proof
assume A15:
x,
y,
u are_collinear
;
contradiction
(
x,
y,
p are_collinear &
x,
y,
x are_collinear )
by A4, DIRAF:30, DIRAF:31;
hence
contradiction
by A10, A11, A15, DIRAF:32;
verum
end; then A16:
x,
y // u,
r
by A12, A13, PASCH:14;
A17:
not
p,
u,
r are_collinear
proof
x,
y,
p are_collinear
by A4, DIRAF:30;
then
x,
y '||' x,
p
by DIRAF:def 5;
then
x,
y '||' p,
x
by DIRAF:22;
then A19:
u,
r '||' p,
x
by A10, A12, DIRAF:23;
A20:
u,
r,
u are_collinear
by DIRAF:31;
assume
p,
u,
r are_collinear
;
contradiction
then A21:
u,
r,
p are_collinear
by DIRAF:30;
p,
x '||' p,
y
by A4, DIRAF:def 5;
then
u,
r '||' p,
y
by A9, A19, DIRAF:23;
then A22:
u,
r,
y are_collinear
by A18, A21, DIRAF:33;
u,
r,
x are_collinear
by A18, A21, A19, DIRAF:33;
hence
contradiction
by A14, A18, A22, A20, DIRAF:32;
verum
end; then A23:
u <> r
by DIRAF:31;
set u9 =
f . u;
set r9 =
f . r;
set x9 =
f . x;
set y9 =
f . y;
A24:
not
f . x,
f . y,
f . u are_collinear
by A1, A14, Th46;
(
f . x,
f . y '||' f . u,
f . r &
f . x,
f . u '||' f . y,
f . r )
by A1, A12, A13, Th45;
then
f . x,
f . y // f . u,
f . r
by A24, PASCH:14;
then A25:
f . r,
f . u // f . y,
f . x
by DIRAF:2;
u,
r // f . r,
f . u
by A1, A2, A3, A17, Th61;
then
x,
y // f . r,
f . u
by A16, A23, DIRAF:3;
hence
x,
y // f . y,
f . x
by A25, A23, DIRAF:3, FUNCT_2:58;
verum end;
Mid x,p,f . x
by A1, A2, A3, Th60;
hence
x,y // f . y,f . x
by A2, A6, A8, DIRAF:4, DIRAF:def 3; verum