let OAS be OAffinSpace; :: thesis: for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is negative_dilatation holds
( f * g is negative_dilatation & g * f is negative_dilatation )
let f, g be Permutation of the carrier of OAS; :: thesis: ( f is positive_dilatation & g is negative_dilatation implies ( f * g is negative_dilatation & g * f is negative_dilatation ) )
assume A1: ( f is positive_dilatation & g is negative_dilatation ) ; :: thesis: ( f * g is negative_dilatation & g * f is negative_dilatation )
thus for x, y being Element of OAS holds x,y // (f * g) . y,(f * g) . x :: according to TRANSGEO:def 7 :: thesis: g * f is negative_dilatation
proof
let x, y be Element of OAS; :: thesis: x,y // (f * g) . y,(f * g) . x
set x9 = g . x;
set y9 = g . y;
A2: ( (f * g) . x = f . (g . x) & (f * g) . y = f . (g . y) ) by FUNCT_2:15;
A3: now :: thesis: ( g . x = g . y implies x,y // (f * g) . y,(f * g) . x )
assume g . x = g . y ; :: thesis: x,y // (f * g) . y,(f * g) . x
then x = y by FUNCT_2:58;
hence x,y // (f * g) . y,(f * g) . x by DIRAF:4; :: thesis: verum
end;
( x,y // g . y,g . x & g . y,g . x // f . (g . y),f . (g . x) ) by A1, Th27;
hence x,y // (f * g) . y,(f * g) . x by A2, A3, DIRAF:3; :: thesis: verum
end;
thus for x, y being Element of OAS holds x,y // (g * f) . y,(g * f) . x :: according to TRANSGEO:def 7 :: thesis: verum
proof
let x, y be Element of OAS; :: thesis: x,y // (g * f) . y,(g * f) . x
set x9 = f . x;
set y9 = f . y;
A4: ( (g * f) . x = g . (f . x) & (g * f) . y = g . (f . y) ) by FUNCT_2:15;
A5: now :: thesis: ( f . x = f . y implies x,y // (g * f) . y,(g * f) . x )
assume f . x = f . y ; :: thesis: x,y // (g * f) . y,(g * f) . x
then x = y by FUNCT_2:58;
hence x,y // (g * f) . y,(g * f) . x by DIRAF:4; :: thesis: verum
end;
( x,y // f . x,f . y & f . x,f . y // g . (f . y),g . (f . x) ) by A1, Th27;
hence x,y // (g * f) . y,(g * f) . x by A4, A5, DIRAF:3; :: thesis: verum
end;