let OAS be OAffinSpace; :: thesis: for p, q, x being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds
Mid x,p,f . x
let p, q, x be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds
Mid x,p,f . x
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . p = p & Mid q,p,f . q & q <> p implies Mid x,p,f . x )
assume that
A1:
f is dilatation
and
A2:
f . p = p
and
A3:
Mid q,p,f . q
and
A4:
q <> p
; :: thesis: Mid x,p,f . x
now assume A5:
LIN p,
q,
x
;
:: thesis: Mid x,p,f . xconsider r being
Element of
OAS such that A6:
not
LIN p,
q,
r
by A4, DIRAF:43;
A7:
Mid r,
p,
f . r
by A1, A2, A3, A6, Th74;
(
x = p or not
LIN p,
r,
x )
proof
assume A8:
(
x <> p &
LIN p,
r,
x )
;
:: thesis: contradiction
then
(
LIN p,
x,
r &
LIN p,
x,
q &
LIN p,
x,
p )
by A5, DIRAF:36, DIRAF:37;
hence
contradiction
by A6, A8, DIRAF:38;
:: thesis: verum
end; hence
Mid x,
p,
f . x
by A1, A2, A7, Th74, DIRAF:14;
:: thesis: verum end;
hence
Mid x,p,f . x
by A1, A2, A3, Th74; :: thesis: verum