let AFP be AffinPlane; for f, g being Permutation of the carrier of AFP st AFP is translational & f is translation & g is translation holds
f * g = g * f
let f, g be Permutation of the carrier of AFP; ( AFP is translational & f is translation & g is translation implies f * g = g * f )
assume that
A1:
AFP is translational
and
A2:
f is translation
and
A3:
g is translation
; f * g = g * f
A4:
g is dilatation
by A3, TRANSGEO:def 11;
now consider a being
Element of
AFP;
assume that A5:
f <> id the
carrier of
AFP
and A6:
g <> id the
carrier of
AFP
;
f * g = g * fA7:
a <> f . a
by A2, A5, TRANSGEO:def 11;
A8:
a <> g . a
by A3, A6, TRANSGEO:def 11;
now consider b being
Element of
AFP such that A9:
not
LIN a,
f . a,
b
by A7, AFF_1:22;
consider h being
Permutation of the
carrier of
AFP such that A10:
h is
translation
and A11:
h . a = b
by A1, Th9;
A12:
h * g is
translation
by A3, A10, TRANSGEO:105;
assume A13:
LIN a,
f . a,
g . a
;
f * g = g * f
not
LIN a,
f . a,
h . (g . a)
proof
A14:
not
LIN a,
g . a,
b
proof
assume A15:
LIN a,
g . a,
b
;
contradiction
(
LIN a,
g . a,
f . a &
LIN a,
g . a,
a )
by A13, AFF_1:15, AFF_1:16;
hence
contradiction
by A8, A9, A15, AFF_1:17;
verum
end;
then
(g * h) . a = (h * g) . a
by A3, A10, A11, Th11;
then
(g * h) . a = h . (g . a)
by FUNCT_2:21;
then A16:
g . b = h . (g . a)
by A11, FUNCT_2:21;
assume A17:
LIN a,
f . a,
h . (g . a)
;
contradiction
(
a,
g . a // b,
g . b &
a,
b // g . a,
g . b )
by A3, A4, TRANSGEO:85, TRANSGEO:100;
then
(
LIN a,
f . a,
a & not
LIN g . a,
a,
h . (g . a) )
by A14, A16, Lm5, AFF_1:16;
hence
contradiction
by A7, A13, A17, AFF_1:17;
verum
end; then A18:
not
LIN a,
f . a,
(h * g) . a
by FUNCT_2:21;
h * (f * g) =
(h * f) * g
by RELAT_1:55
.=
(f * h) * g
by A2, A9, A10, A11, Th11
.=
f * (h * g)
by RELAT_1:55
.=
(h * g) * f
by A2, A12, A18, Th11
.=
h * (g * f)
by RELAT_1:55
;
hence
f * g = g * f
by TRANSGEO:13;
verum end; hence
f * g = g * f
by A2, A3, Th11;
verum end;
hence
f * g = g * f
by TRANSGEO:11; verum