let OAS be OAffinSpace; :: thesis: for p, q 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 holds
f is negative_dilatation
let p, q be Element of OAS; :: thesis: for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q holds
f is negative_dilatation
let f be Permutation of the carrier of OAS; :: thesis: ( f is dilatation & f . p = p & q <> p & Mid q,p,f . q implies f is negative_dilatation )
assume that
A1:
f is dilatation
and
A2:
f . p = p
and
A3:
q <> p
and
A4:
Mid q,p,f . q
; :: thesis: f is negative_dilatation
for x, y being Element of OAS holds x,y // f . y,f . x
proof
let x,
y be
Element of
OAS;
:: thesis: x,y // f . y,f . x
( not
LIN p,
x,
y implies
x,
y // f . y,
f . x )
by A1, A2, A3, A4, Th76;
hence
x,
y // f . y,
f . x
by A1, A2, A3, A4, Th77;
:: thesis: verum
end;
hence
f is negative_dilatation
by Def7; :: thesis: verum