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;

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 :: thesis: ( f <> id the carrier of AFP & g <> id the carrier of AFP implies f * g = g * f )

hence
f * g = g * f
by TRANSGEO:4; :: thesis: verumset a = the Element of AFP;

assume that

A5: f <> id the carrier of AFP and

A6: g <> id the carrier of AFP ; :: thesis: f * g = g * f

A7: 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;

end;assume that

A5: f <> id the carrier of AFP and

A6: g <> id the carrier of AFP ; :: thesis: f * g = g * f

A7: 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 :: thesis: ( LIN the Element of AFP,f . the Element of AFP,g . the Element of AFP implies f * g = g * f )

hence
f * g = g * f
by A2, A3, Th9; :: thesis: verumconsider 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 ; :: thesis: f * g = g * f

not LIN the Element of AFP,f . the Element of AFP,h . (g . the Element of AFP)

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; :: thesis: verum

end;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 ; :: thesis: f * g = g * f

not LIN the Element of AFP,f . the Element of AFP,h . (g . the Element of AFP)

proof

then A18:
not LIN the Element of AFP,f . the Element of AFP,(h * g) . the Element of AFP
by FUNCT_2:15;
A14:
not LIN the Element of AFP,g . the Element of AFP,b

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) ; :: thesis: 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; :: thesis: verum

end;proof

then
(g * h) . the Element of AFP = (h * g) . the Element of AFP
by A3, A10, A11, Th9;
assume A15:
LIN the Element of AFP,g . the Element of AFP,b
; :: thesis: 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; :: thesis: verum

end;( 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; :: thesis: verum

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) ; :: thesis: 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; :: thesis: verum

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; :: thesis: verum