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 & b <> f . a & Mid a,b,f . a holds
a,b // f . a,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 & b <> f . a & Mid a,b,f . a holds
a,b // f . a,f . b
let f be Permutation of the carrier of OAS; :: thesis: ( f is translation & a <> f . a & b <> f . a & Mid a,b,f . a implies a,b // f . a,f . b )
assume A1:
( f is translation & a <> f . a & b <> f . a & Mid a,b,f . a )
; :: thesis: a,b // f . a,f . b
then A2:
f <> id the carrier of OAS
by FUNCT_1:35;
A3:
f is dilatation
by A1, Def9;
A4:
LIN a,b,f . a
by A1, DIRAF:34;
then A5:
LIN a,f . a,b
by DIRAF:36;
A6:
a,b // b,f . a
by A1, DIRAF:def 3;
now assume A7:
a <> b
;
:: thesis: a,b // f . a,f . bA8:
a,
b '||' f . a,
f . b
by A3, Th51;
now assume A9:
a,
b // f . b,
f . a
;
:: thesis: contradictionA10:
Mid f . a,
f . b,
b
proof
(
a,
b // a,
f . a &
a,
f . a // b,
f . b )
by A1, A5, A6, Lm6, ANALOAF:def 5;
then
a,
b // b,
f . b
by A1, DIRAF:6;
then
b,
f . b // f . b,
f . a
by A7, A9, ANALOAF:def 5;
then
Mid b,
f . b,
f . a
by DIRAF:def 3;
hence
Mid f . a,
f . b,
b
by DIRAF:13;
:: thesis: verum
end; consider q being
Element of
OAS such that A11:
not
LIN a,
f . a,
q
by A1, DIRAF:43;
consider x being
Element of
OAS such that A12:
(
q,
b // b,
x &
q,
a // f . a,
x )
by A6, A7, ANALOAF:def 5;
A13:
x <> f . a
proof
assume
x = f . a
;
:: thesis: contradiction
then
Mid q,
b,
f . a
by A12, DIRAF:def 3;
then
LIN q,
b,
f . a
by DIRAF:34;
then
(
LIN f . a,
b,
q &
LIN f . a,
b,
a &
LIN f . a,
b,
b )
by A4, DIRAF:36, DIRAF:37;
then
(
LIN a,
b,
q &
LIN a,
b,
f . a &
LIN a,
b,
a )
by A1, DIRAF:36, DIRAF:38;
hence
contradiction
by A7, A11, DIRAF:38;
:: thesis: verum
end; A14:
not
LIN x,
f . a,
b
proof
assume
LIN x,
f . a,
b
;
:: thesis: contradiction
then
LIN f . a,
x,
b
by DIRAF:36;
then
(
f . a,
x '||' f . a,
b &
q,
a '||' f . a,
x )
by A12, DIRAF:def 4, DIRAF:def 5;
then
(
f . a,
b '||' q,
a &
LIN f . a,
b,
a )
by A4, A13, DIRAF:28, DIRAF:36;
then
(
f . a,
b '||' q,
a &
f . a,
b '||' f . a,
a )
by DIRAF:def 5;
then
f . a,
a '||' q,
a
by A1, DIRAF:28;
then
a,
f . a '||' a,
q
by DIRAF:27;
hence
contradiction
by A11, DIRAF:def 5;
:: thesis: verum
end; A15:
(
a,
q // f . a,
f . q &
a,
f . a // q,
f . q &
a <> q )
by A1, A11, Lm5, DIRAF:37;
Mid q,
b,
x
by A12, DIRAF:def 3;
then A16:
Mid x,
b,
q
by DIRAF:13;
A17:
LIN x,
f . a,
f . q
proof
a,
q // x,
f . a
by A12, DIRAF:5;
then
f . a,
f . q // x,
f . a
by A15, ANALOAF:def 5;
then
f . a,
f . q '||' f . a,
x
by DIRAF:def 4;
then
LIN f . a,
f . q,
x
by DIRAF:def 5;
hence
LIN x,
f . a,
f . q
by DIRAF:36;
:: thesis: verum
end;
f . a,
b '||' q,
f . q
proof
LIN f . a,
a,
b
by A4, DIRAF:36;
then
f . a,
a '||' f . a,
b
by DIRAF:def 5;
then
(
a,
f . a '||' b,
f . a &
a,
f . a '||' q,
f . q )
by A15, DIRAF:27, DIRAF:def 4;
then
b,
f . a '||' q,
f . q
by A1, DIRAF:28;
hence
f . a,
b '||' q,
f . q
by DIRAF:27;
:: thesis: verum
end; then
Mid x,
f . a,
f . q
by A14, A16, A17, PASCH:15;
then consider y being
Element of
OAS such that A18:
(
Mid x,
y,
b &
Mid y,
f . b,
f . q )
by A10, A14, PASCH:35;
A19:
(
LIN x,
y,
b &
LIN y,
f . b,
f . q )
by A18, DIRAF:34;
A20:
(
LIN b,
f . b,
a &
LIN b,
f . b,
f . a )
proof
A21:
(
LIN a,
f . a,
f . b &
LIN a,
f . a,
a )
by A3, A5, Th60, DIRAF:37;
hence
LIN b,
f . b,
a
by A1, A5, DIRAF:38;
:: thesis: LIN b,f . b,f . a
LIN a,
f . a,
f . a
by DIRAF:37;
hence
LIN b,
f . b,
f . a
by A1, A5, A21, DIRAF:38;
:: thesis: verum
end; A22:
b <> f . b
by A1, A2, Def9;
then A23:
not
LIN b,
f . b,
q
by A11, A20, DIRAF:38;
A24:
not
LIN b,
f . b,
f . q
proof
assume
LIN b,
f . b,
f . q
;
:: thesis: contradiction
then
(
LIN b,
f . b,
f . q &
b,
f . b '||' q,
f . q )
by A1, A3, Th67;
then
(
LIN b,
f . b,
f . q &
b,
f . b '||' f . q,
q )
by DIRAF:27;
hence
contradiction
by A22, A23, DIRAF:39;
:: thesis: verum
end; A25:
x <> b
by A14, DIRAF:37;
A26:
(
LIN x,
b,
q &
LIN x,
b,
y &
LIN x,
b,
b )
by A16, A19, DIRAF:34, DIRAF:36, DIRAF:37;
then A27:
LIN y,
b,
q
by A25, DIRAF:38;
A28:
(
f . b <> f . q &
b <> q )
by A24, DIRAF:37;
A29:
b,
q '||' f . b,
f . q
by A3, Th51;
(
LIN f . b,
f . q,
y &
LIN b,
q,
y )
by A19, A25, A26, DIRAF:36, DIRAF:38;
then
(
f . b,
f . q '||' f . b,
y &
b,
q '||' b,
y )
by DIRAF:def 5;
then
(
b,
q '||' f . b,
y &
b,
q '||' b,
y )
by A28, A29, DIRAF:28;
then
f . b,
y '||' b,
y
by A28, DIRAF:28;
then
y,
b '||' y,
f . b
by DIRAF:27;
then
(
LIN y,
b,
f . b &
LIN y,
b,
b )
by DIRAF:37, DIRAF:def 5;
hence
contradiction
by A19, A23, A24, A27, DIRAF:38;
:: thesis: verum end; hence
a,
b // f . a,
f . b
by A8, DIRAF:def 4;
:: thesis: verum end;
hence
a,b // f . a,f . b
by DIRAF:7; :: thesis: verum