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 ( f <> id the carrier of AFP & g <> id the carrier of AFP implies f * g = g * f )set a = the
Element of
AFP;
assume that A5:
f <> id the
carrier of
AFP
and A6:
g <> id the
carrier of
AFP
;
f * g = g * fA7:
the
Element of
AFP <> f . the
Element of
AFP
by A2, A5, TRANSGEO:def 11;
A8:
the
Element of
AFP <> g . the
Element of
AFP
by A3, A6, TRANSGEO:def 11;
now ( LIN the Element of AFP,f . the Element of AFP,g . the Element of AFP implies f * g = g * f )consider b being
Element of
AFP such that A9:
not
LIN the
Element of
AFP,
f . the
Element of
AFP,
b
by A7, AFF_1:13;
consider h being
Permutation of the
carrier of
AFP such that A10:
h is
translation
and A11:
h . the
Element of
AFP = b
by A1, Th7;
A12:
h * g is
translation
by A3, A10, TRANSGEO:86;
assume A13:
LIN the
Element of
AFP,
f . the
Element of
AFP,
g . the
Element of
AFP
;
f * g = g * f
not
LIN the
Element of
AFP,
f . the
Element of
AFP,
h . (g . the Element of AFP)
proof
A14:
not
LIN the
Element of
AFP,
g . the
Element of
AFP,
b
proof
assume A15:
LIN the
Element of
AFP,
g . the
Element of
AFP,
b
;
contradiction
(
LIN the
Element of
AFP,
g . the
Element of
AFP,
f . the
Element of
AFP &
LIN the
Element of
AFP,
g . the
Element of
AFP, the
Element of
AFP )
by A13, AFF_1:6, AFF_1:7;
hence
contradiction
by A8, A9, A15, AFF_1:8;
verum
end;
then
(g * h) . the
Element of
AFP = (h * g) . the
Element of
AFP
by A3, A10, A11, Th9;
then
(g * h) . the
Element of
AFP = h . (g . the Element of AFP)
by FUNCT_2:15;
then A16:
g . b = h . (g . the Element of AFP)
by A11, FUNCT_2:15;
assume A17:
LIN the
Element of
AFP,
f . the
Element of
AFP,
h . (g . the Element of AFP)
;
contradiction
( the
Element of
AFP,
g . the
Element of
AFP // b,
g . b & the
Element of
AFP,
b // g . the
Element of
AFP,
g . b )
by A3, A4, TRANSGEO:68, TRANSGEO:82;
then
(
LIN the
Element of
AFP,
f . the
Element of
AFP, the
Element of
AFP & not
LIN g . the
Element of
AFP, the
Element of
AFP,
h . (g . the Element of AFP) )
by A14, A16, Lm5, AFF_1:7;
hence
contradiction
by A7, A13, A17, AFF_1:8;
verum
end; then A18:
not
LIN the
Element of
AFP,
f . the
Element of
AFP,
(h * g) . the
Element of
AFP
by FUNCT_2:15;
h * (f * g) =
(h * f) * g
by RELAT_1:36
.=
(f * h) * g
by A2, A9, A10, A11, Th9
.=
f * (h * g)
by RELAT_1:36
.=
(h * g) * f
by A2, A12, A18, Th9
.=
h * (g * f)
by RELAT_1:36
;
hence
f * g = g * f
by TRANSGEO:5;
verum end; hence
f * g = g * f
by A2, A3, Th9;
verum end;
hence
f * g = g * f
by TRANSGEO:4; verum