let AFS be AffinSpace; for a, b being Element of AFS
for f being Permutation of the carrier of AFS st f is collineation holds
f .: (Line (a,b)) = Line ((f . a),(f . b))
let a, b be Element of AFS; for f being Permutation of the carrier of AFS st f is collineation holds
f .: (Line (a,b)) = Line ((f . a),(f . b))
let f be Permutation of the carrier of AFS; ( f is collineation implies f .: (Line (a,b)) = Line ((f . a),(f . b)) )
assume A1:
f is collineation
; f .: (Line (a,b)) = Line ((f . a),(f . b))
now for x being object st x in Line ((f . a),(f . b)) holds
x in f .: (Line (a,b))let x be
object ;
( x in Line ((f . a),(f . b)) implies x in f .: (Line (a,b)) )assume A2:
x in Line (
(f . a),
(f . b))
;
x in f .: (Line (a,b))then reconsider x9 =
x as
Element of
AFS ;
consider y being
Element of
AFS such that A3:
f . y = x9
by Th1;
LIN f . a,
f . b,
f . y
by A2, A3, AFF_1:def 2;
then
LIN a,
b,
y
by A1, Th88;
then
y in Line (
a,
b)
by AFF_1:def 2;
hence
x in f .: (Line (a,b))
by A3, Th91;
verum end;
then A4:
Line ((f . a),(f . b)) c= f .: (Line (a,b))
by TARSKI:def 3;
now for x being object st x in f .: (Line (a,b)) holds
x in Line ((f . a),(f . b))let x be
object ;
( x in f .: (Line (a,b)) implies x in Line ((f . a),(f . b)) )assume A5:
x in f .: (Line (a,b))
;
x in Line ((f . a),(f . b))then reconsider x9 =
x as
Element of
AFS ;
consider y being
Element of
AFS such that A6:
y in Line (
a,
b)
and A7:
f . y = x9
by A5, Th91;
LIN a,
b,
y
by A6, AFF_1:def 2;
then
LIN f . a,
f . b,
x9
by A1, A7, Th88;
hence
x in Line (
(f . a),
(f . b))
by AFF_1:def 2;
verum end;
then
f .: (Line (a,b)) c= Line ((f . a),(f . b))
by TARSKI:def 3;
hence
f .: (Line (a,b)) = Line ((f . a),(f . b))
by A4, XBOOLE_0:def 10; verum