let AFP be AffinPlane; 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; ( ( 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
; 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;
( 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
;
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;
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;
( f .: A is being_line implies A is being_line )
set K =
f .: A;
assume
f .: A is
being_line
;
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;
verum
end;
A13:
for A, C being Subset of AFP st f .: A // f .: C holds
A // C
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;
( 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
;
a,b // c,d
now ( 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 )
;
a,b // c,dthen 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;
verum end;
hence
a,
b // c,
d
by AFF_1:3;
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;
( A // C implies f .: A // f .: C )
assume A26:
A // C
;
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
;
f .: A // f .: C
assume
not
f .: A // f .: C
;
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;
verum
end;
hence
f .: A // f .: C
by A29;
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;
( a,b // c,d implies f . a,f . b // f . c,f . d )
assume A37:
a,
b // c,
d
;
f . a,f . b // f . c,f . d
now ( 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 )
;
f . a,f . b // f . c,f . dthen
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;
verum end;
hence
f . a,
f . b // f . c,
f . d
by AFF_1:3;
verum
end;
hence
f is collineation
by A19, Th87; verum