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) )
assume A3: a <> b ; :: thesis: f .: (Line a,b) = Line (f . a),(f . b)
set A = Line a,b;
set x = f . a;
set y = f . b;
A4: f . a <> f . b by A3, FUNCT_2:85;
set K = Line (f . a),(f . b);
set M = f .: (Line a,b);
A5: ( Line a,b is being_line & Line (f . a),(f . b) is being_line ) by A4, AFF_1:def 3;
then A6: f .: (Line a,b) is being_line by A1;
( a in Line a,b & b in Line a,b ) by AFF_1:26;
then ( f . a in Line (f . a),(f . b) & f . b in Line (f . a),(f . b) & f . a in f .: (Line a,b) & f . b in f .: (Line a,b) ) by Th110, AFF_1:26;
hence f .: (Line a,b) = Line (f . a),(f . b) by A3, A5, A6, AFF_1:30, FUNCT_2:85; :: thesis: verum

end;

A7: 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 A8: A // C ; :: thesis: f .: A // f .: C
then A9: ( A is being_line & C is being_line ) by AFF_1:50;
then A10: ( f .: A is being_line & f .: C is being_line ) by A1;
( A <> C implies f .: A // f .: C )

proof

assume A11: A <> C ; :: thesis: f .: A // f .: C
assume not f .: A // f .: C ; :: thesis: contradiction
then consider x being Element of AFP such that
A12: ( x in f .: A & x in f .: C ) by A10, AFF_1:72;
consider a being Element of AFP such that
A13: ( a in A & x = f . a ) by A12, Th111;
consider b being Element of AFP such that
A14: ( b in C & x = f . b ) by A12, Th111;
a = b by A13, A14, FUNCT_2:85;
hence contradiction by A8, A11, A13, A14, AFF_1:59; :: thesis: verum

end;

hence f .: A // f .: C by A1, A9, AFF_1:55; :: thesis: verum

end;

A15: 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 )
assume A16: f .: A is being_line ; :: thesis: A is being_line
set K = f .: A;
consider x, y being Element of AFP such that
A17: ( x <> y & f .: A = Line x,y ) by A16, AFF_1:def 3;
A18: ( x in f .: A & y in f .: A ) by A17, AFF_1:26;
then consider a being Element of AFP such that
A19: ( a in A & f . a = x ) by Th111;
consider b being Element of AFP such that
A20: ( b in A & f . b = y ) by A18, Th111;
set C = Line a,b;
A21: Line a,b is being_line by A17, A19, A20, AFF_1:def 3;
f .: (Line a,b) = f .: A by A2, A17, A19, A20;
hence A is being_line by A21, Th112; :: thesis: verum

end;

A22: 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 )
assume A23: f .: A // f .: C ; :: thesis: A // C
set K = f .: A;
set M = f .: C;
A24: ( f .: A is being_line & f .: C is being_line ) by A23, AFF_1:50;
then A25: ( A is being_line & C is being_line ) by A15;

now

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

end;

hence A // C by A15, A24, AFF_1:55; :: thesis: verum

end;

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

now

assume A30: ( a <> b & c <> d ) ; :: thesis: f . a,f . b // f . c,f . d
set A = Line a,b;
set C = Line c,d;
set K = f .: (Line a,b);
set M = f .: (Line c,d);
A31: Line a,b // Line c,d by A29, A30, AFF_1:51;
( a in Line a,b & b in Line a,b & c in Line c,d & d in Line c,d ) by AFF_1:26;
then ( f . a in f .: (Line a,b) & f . b in f .: (Line a,b) & f . c in f .: (Line c,d) & f . d in f .: (Line c,d) ) by Th110;
hence f . a,f . b // f . c,f . d by A7, A31, AFF_1:53; :: thesis: verum

end;

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

end;

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 )
assume A32: f . a,f . b // f . c,f . d ; :: thesis: a,b // c,d
set x = f . a;
set y = f . b;
set z = f . c;
set t = f . d;

now

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

end;

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

end;

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