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