let OAS be OAffinSpace; :: thesis: for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is translation & a <> f . a & LIN a,f . a,b holds
a,f . a // b,f . b
let a, b be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is translation & a <> f . a & LIN a,f . a,b holds
a,f . a // b,f . b
let f be Permutation of the carrier of OAS; :: thesis: ( f is translation & a <> f . a & LIN a,f . a,b implies a,f . a // b,f . b )
assume that
A1:
f is translation
and
A2:
a <> f . a
and
A3:
LIN a,f . a,b
; :: thesis: a,f . a // b,f . b
A4:
f is dilatation
by A1, Def9;
consider p being Element of OAS such that
A5:
not LIN a,f . a,p
by A2, DIRAF:43;
f <> id the carrier of OAS
by A2, FUNCT_1:35;
then A6:
( p <> f . p & b <> f . b )
by A1, Def9;
A7:
not LIN p,f . p,a
proof
assume
LIN p,
f . p,
a
;
:: thesis: contradiction
then
(
LIN p,
f . p,
p &
LIN p,
f . p,
a &
LIN p,
f . p,
f . a )
by A4, Th60, DIRAF:37;
hence
contradiction
by A5, A6, DIRAF:38;
:: thesis: verum
end;
A8:
not LIN p,f . p,b
proof
assume A9:
LIN p,
f . p,
b
;
:: thesis: contradiction
(
LIN a,
f . a,
b &
LIN a,
f . a,
f . b &
LIN a,
f . a,
a )
by A3, A4, Th60, DIRAF:37;
then
LIN b,
f . b,
a
by A2, DIRAF:38;
then A10:
(
LIN b,
f . b,
f . a &
LIN b,
f . b,
a )
by A4, Th60;
A11:
LIN p,
f . p,
f . b
by A4, A9, Th60;
LIN p,
f . p,
p
by DIRAF:37;
then
LIN b,
f . b,
p
by A6, A9, A11, DIRAF:38;
hence
contradiction
by A5, A6, A10, DIRAF:38;
:: thesis: verum
end;
A12:
( p,a // f . p,f . a & p,f . p // a,f . a )
by A1, A7, Lm5;
( p,b // f . p,f . b & p,f . p // b,f . b )
by A1, A8, Lm5;
hence
a,f . a // b,f . b
by A6, A12, ANALOAF:def 5; :: thesis: verum