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:85;
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:26;
then A6: f . a in f .: (Line (a,b)) by Th110;
b in Line (a,b) by AFF_1:26;
then A7: f . b in f .: (Line (a,b)) by Th110;
( f . a in Line ((f . a),(f . b)) & f . b in Line ((f . a),(f . b)) ) by AFF_1:26;
hence f .: (Line (a,b)) = Line ((f . a),(f . b)) by A3, A4, A5, A6, A7, AFF_1:30, FUNCT_2:85; :: 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:26;
then consider b being Element of AFP such that
b in A and
A11: f . b = y by Th111;
x in f .: A by A10, AFF_1:26;
then consider a being Element of AFP such that
a in A and
A12: f . a = x by Th111;
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 Th112; :: 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:50;
then A15: C is being_line by A8;
A16: f .: A is being_line by A14, AFF_1:50;
then A17: A is being_line by A8;

now

assume A18: A <> C ; :: thesis: A // C
assume not A // C ; :: thesis: contradiction
then consider p being Element of AFP such that
A19: ( p in A & p in C ) by A17, A15, AFF_1:72;
set x = f . p;
( f . p in f .: A & f . p in f .: C ) by A19, Th110;
hence contradiction by A14, A18, Th112, AFF_1:59; :: thesis: verum

end;

hence A // C by A8, A16, A17, AFF_1:55; :: thesis: verum

end;

A20: 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 A21: f . a,f . b // f . c,f . d ; :: thesis: a,b // c,d

now

set C = Line (c,d);
set A = Line (a,b);
set K = f .: (Line (a,b));
set M = f .: (Line (c,d));
A22: ( c in Line (c,d) & d in Line (c,d) ) by AFF_1:26;
assume A23: ( a <> b & c <> d ) ; :: thesis: a,b // c,d
then A24: ( f . a <> f . b & f . c <> f . d ) by FUNCT_2:85;
( f .: (Line (a,b)) = Line ((f . a),(f . b)) & f .: (Line (c,d)) = Line ((f . c),(f . d)) ) by A2, A23;
then A25: f .: (Line (a,b)) // f .: (Line (c,d)) by A21, A24, AFF_1:51;
( a in Line (a,b) & b in Line (a,b) ) by AFF_1:26;
hence a,b // c,d by A13, A22, A25, AFF_1:53; :: thesis: verum

end;

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

end;

A26: 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 A27: A // C ; :: thesis: f .: A // f .: C
then C is being_line by AFF_1:50;
then A28: f .: C is being_line by A1;
A29: A is being_line by A27, AFF_1:50;
then A30: f .: A is being_line by A1;
then A: f .: A // f .: A by AFF_1:55;
( A <> C implies f .: A // f .: C )

proof

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

end;

hence f .: A // f .: C by A, A1, A29, AFF_1:55; :: 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 A38: a,b // c,d ; :: thesis: f . a,f . b // f . c,f . d

now

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:26;
then A39: f . a in f .: (Line (a,b)) by Th110;
b in Line (a,b) by AFF_1:26;
then A40: f . b in f .: (Line (a,b)) by Th110;
d in Line (c,d) by AFF_1:26;
then A41: f . d in f .: (Line (c,d)) by Th110;
c in Line (c,d) by AFF_1:26;
then A42: f . c in f .: (Line (c,d)) by Th110;
assume ( a <> b & c <> d ) ; :: thesis: f . a,f . b // f . c,f . d
then Line (a,b) // Line (c,d) by A38, AFF_1:51;
hence f . a,f . b // f . c,f . d by A26, A39, A40, A42, A41, AFF_1:53; :: thesis: verum

end;

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

end;

hence f is collineation by A20, Th107; :: thesis: verum