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