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))

A is being_line

A // C

a,b // c,d

f .: A // f .: C

f . a,f . b // f . c,f . d

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

A8:
for A being Subset of AFP st f .: A is being_line holds
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;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

A is being_line

proof

A13:
for A, C being Subset of AFP st f .: A // f .: C holds
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;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

A // C

proof

A19:
for a, b, c, d being Element of AFP st f . a,f . b // f . c,f . d holds
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;

end;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 )

hence
A // C
by A16, AFF_1:41; :: thesis: verumassume 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;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

a,b // c,d

proof

A25:
for A, C being Subset of AFP st A // C holds
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

end;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 )

hence
a,b // c,d
by AFF_1:3; :: thesis: verumset 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;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

f .: A // f .: C

proof

for a, b, c, d being Element of AFP st a,b // c,d holds
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 )

end;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

hence
f .: A // f .: C
by A29; :: thesis: verum
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;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

f . a,f . b // f . c,f . d

proof

hence
f is collineation
by A19, Th87; :: thesis: verum
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

end;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 )

hence
f . a,f . b // f . c,f . d
by AFF_1:3; :: thesis: verumset 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;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