let AFP be AffinPlane; :: thesis: for f being Permutation of the carrier of AFP st ( for A being Subset of AFP st A is being_line holds
f .: A is being_line ) holds
f is collineation
let f be Permutation of the carrier of AFP; :: thesis: ( ( for A being Subset of AFP st A is being_line holds
f .: A is being_line ) implies f is collineation )
assume A1: for A being Subset of AFP st A is being_line holds
f .: A is being_line ; :: thesis: f is collineation
A2: for a, b being Element of AFP st a <> b holds
f .: (Line (a,b)) = Line ((f . a),(f . b))

proof

let a, b be Element of AFP; :: thesis: ( a <> b implies f .: (Line (a,b)) = Line ((f . a),(f . b)) )
set A = Line (a,b);
set x = f . a;
set y = f . b;
set K = Line ((f . a),(f . b));
set M = f .: (Line (a,b));
assume A3: a <> b ; :: thesis: f .: (Line (a,b)) = Line ((f . a),(f . b))
then f . a <> f . b by FUNCT_2:58;
then A4: Line ((f . a),(f . b)) is being_line by AFF_1:def 3;
Line (a,b) is being_line by A3, AFF_1:def 3;
then A5: f .: (Line (a,b)) is being_line by A1;
a in Line (a,b) by AFF_1:15;
then A6: f . a in f .: (Line (a,b)) by Th90;
b in Line (a,b) by AFF_1:15;
then A7: f . b in f .: (Line (a,b)) by Th90;
( f . a in Line ((f . a),(f . b)) & f . b in Line ((f . a),(f . b)) ) by AFF_1:15;
hence f .: (Line (a,b)) = Line ((f . a),(f . b)) by A3, A4, A5, A6, A7, AFF_1:18, FUNCT_2:58; :: thesis: verum

end;

A8: for A being Subset of AFP st f .: A is being_line holds
A is being_line

proof

let A be Subset of AFP; :: thesis: ( f .: A is being_line implies A is being_line )
set K = f .: A;
assume f .: A is being_line ; :: thesis: A is being_line
then consider x, y being Element of AFP such that
A9: x <> y and
A10: f .: A = Line (x,y) by AFF_1:def 3;
y in f .: A by A10, AFF_1:15;
then consider b being Element of AFP such that
b in A and
A11: f . b = y by Th91;
x in f .: A by A10, AFF_1:15;
then consider a being Element of AFP such that
a in A and
A12: f . a = x by Th91;
set C = Line (a,b);
( Line (a,b) is being_line & f .: (Line (a,b)) = f .: A ) by A2, A9, A10, A12, A11, AFF_1:def 3;
hence A is being_line by Th92; :: thesis: verum

end;

A13: for A, C being Subset of AFP st f .: A // f .: C holds
A // C

proof

let A, C be Subset of AFP; :: thesis: ( f .: A // f .: C implies A // C )
set K = f .: A;
set M = f .: C;
assume A14: f .: A // f .: C ; :: thesis: A // C
then f .: C is being_line by AFF_1:36;
then A15: C is being_line by A8;
f .: A is being_line by A14, AFF_1:36;
then A16: A is being_line by A8;

now :: thesis: ( A <> C implies A // C )

assume A17: A <> C ; :: thesis: A // C
assume not A // C ; :: thesis: contradiction
then consider p being Element of AFP such that
A18: ( p in A & p in C ) by A16, A15, AFF_1:58;
set x = f . p;
( f . p in f .: A & f . p in f .: C ) by A18, Th90;
hence contradiction by A14, A17, Th92, AFF_1:45; :: thesis: verum

end;

hence A // C by A16, AFF_1:41; :: thesis: verum

end;

A19: for a, b, c, d being Element of AFP st f . a,f . b // f . c,f . d holds
a,b // c,d

proof

let a, b, c, d be Element of AFP; :: thesis: ( f . a,f . b // f . c,f . d implies a,b // c,d )
set x = f . a;
set y = f . b;
set z = f . c;
set t = f . d;
assume A20: f . a,f . b // f . c,f . d ; :: thesis: a,b // c,d

now :: thesis: ( a <> b & c <> d implies a,b // c,d )

set C = Line (c,d);
set A = Line (a,b);
set K = f .: (Line (a,b));
set M = f .: (Line (c,d));
A21: ( c in Line (c,d) & d in Line (c,d) ) by AFF_1:15;
assume A22: ( a <> b & c <> d ) ; :: thesis: a,b // c,d
then A23: ( f . a <> f . b & f . c <> f . d ) by FUNCT_2:58;
( f .: (Line (a,b)) = Line ((f . a),(f . b)) & f .: (Line (c,d)) = Line ((f . c),(f . d)) ) by A2, A22;
then A24: f .: (Line (a,b)) // f .: (Line (c,d)) by A20, A23, AFF_1:37;
( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;
hence a,b // c,d by A13, A21, A24, AFF_1:39; :: thesis: verum

end;

hence a,b // c,d by AFF_1:3; :: thesis: verum

end;

A25: for A, C being Subset of AFP st A // C holds
f .: A // f .: C

proof

let A, C be Subset of AFP; :: thesis: ( A // C implies f .: A // f .: C )
assume A26: A // C ; :: thesis: f .: A // f .: C
then C is being_line by AFF_1:36;
then A27: f .: C is being_line by A1;
A is being_line by A26, AFF_1:36;
then A28: f .: A is being_line by A1;
then A29: f .: A // f .: A by AFF_1:41;
( A <> C implies f .: A // f .: C )

proof

assume A30: A <> C ; :: thesis: f .: A // f .: C
assume not f .: A // f .: C ; :: thesis: contradiction
then consider x being Element of AFP such that
A31: x in f .: A and
A32: x in f .: C by A28, A27, AFF_1:58;
consider b being Element of AFP such that
A33: b in C and
A34: x = f . b by A32, Th91;
consider a being Element of AFP such that
A35: a in A and
A36: x = f . a by A31, Th91;
a = b by A36, A34, FUNCT_2:58;
hence contradiction by A26, A30, A35, A33, AFF_1:45; :: thesis: verum

end;

hence f .: A // f .: C by A29; :: thesis: verum

end;

for a, b, c, d being Element of AFP st a,b // c,d holds
f . a,f . b // f . c,f . d

proof

let a, b, c, d be Element of AFP; :: thesis: ( a,b // c,d implies f . a,f . b // f . c,f . d )
assume A37: a,b // c,d ; :: thesis: f . a,f . b // f . c,f . d

now :: thesis: ( a <> b & c <> d implies f . a,f . b // f . c,f . d )

set C = Line (c,d);
set A = Line (a,b);
set K = f .: (Line (a,b));
set M = f .: (Line (c,d));
a in Line (a,b) by AFF_1:15;
then A38: f . a in f .: (Line (a,b)) by Th90;
b in Line (a,b) by AFF_1:15;
then A39: f . b in f .: (Line (a,b)) by Th90;
d in Line (c,d) by AFF_1:15;
then A40: f . d in f .: (Line (c,d)) by Th90;
c in Line (c,d) by AFF_1:15;
then A41: f . c in f .: (Line (c,d)) by Th90;
assume ( a <> b & c <> d ) ; :: thesis: f . a,f . b // f . c,f . d
then Line (a,b) // Line (c,d) by A37, AFF_1:37;
hence f . a,f . b // f . c,f . d by A25, A38, A39, A41, A40, AFF_1:39; :: thesis: verum

end;

hence f . a,f . b // f . c,f . d by AFF_1:3; :: thesis: verum

end;

hence f is collineation by A19, Th87; :: thesis: verum