let AFP be AffinPlane; :: thesis: for K being Subset of AFP
for p being Element of AFP
for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & not p in K & f . p = p holds
f = id the carrier of AFP
let K be Subset of AFP; :: thesis: for p being Element of AFP
for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & not p in K & f . p = p holds
f = id the carrier of AFP
let p be Element of AFP; :: thesis: for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & not p in K & f . p = p holds
f = id the carrier of AFP
let f be Permutation of the carrier of AFP; :: thesis: ( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & not p in K & f . p = p implies f = id the carrier of AFP )
assume that
A1: f is collineation and
A2: K is being_line and
A3: for x being Element of AFP st x in K holds
f . x = x and
A4: ( not p in K & f . p = p ) ; :: thesis: f = id the carrier of AFP
A5: for x being Element of AFP holds f . x = x
proof
let x be Element of AFP; :: thesis: f . x = x
now
assume not x in K ; :: thesis: f . x = x
consider a, b being Element of AFP such that
A6: ( a in K & b in K & a <> b ) by A2, AFF_1:31;
set A = Line p,a;
set M = Line p,b;
A7: ( Line p,a is being_line & Line p,b is being_line ) by A4, A6, AFF_1:def 3;
then consider C being Subset of AFP such that
A8: ( x in C & Line p,a // C ) by AFF_1:63;
consider D being Subset of AFP such that
A9: ( x in D & Line p,b // D ) by A7, AFF_1:63;
A10: ( C is being_line & D is being_line & Line p,a is being_line ) by A8, A9, AFF_1:50;
A11: ( p in Line p,a & p in Line p,b ) by AFF_1:26;
A12: ( a in Line p,a & b in Line p,b ) by AFF_1:26;
A13: not C // K
proof
assume C // K ; :: thesis: contradiction
then Line p,a // K by A8, AFF_1:58;
hence contradiction by A4, A6, A11, A12, AFF_1:59; :: thesis: verum
end;
A14: not D // K
proof
assume D // K ; :: thesis: contradiction
then Line p,b // K by A9, AFF_1:58;
hence contradiction by A4, A6, A11, A12, AFF_1:59; :: thesis: verum
end;
consider c being Element of AFP such that
A15: ( c in C & c in K ) by A2, A10, A13, AFF_1:72;
consider d being Element of AFP such that
A16: ( d in D & d in K ) by A2, A10, A14, AFF_1:72;
A17: f .: (Line p,a) = Line p,a
proof
f .: (Line p,a) = Line (f . p),(f . a) by A1, Th113;
hence f .: (Line p,a) = Line p,a by A3, A4, A6; :: thesis: verum
end;
A18: f .: (Line p,b) = Line p,b
proof
f .: (Line p,b) = Line (f . p),(f . b) by A1, Th113;
hence f .: (Line p,b) = Line p,b by A3, A4, A6; :: thesis: verum
end;
A19: f .: C = C
proof
f .: (Line p,a) // f .: C by A1, A8, Th115;
then A20: f .: C // C by A8, A17, AFF_1:58;
f . c = c by A3, A15;
then c in f .: C by A15, Th110;
hence f .: C = C by A15, A20, AFF_1:59; :: thesis: verum
end;
A21: f .: D = D
proof
f .: (Line p,b) // f .: D by A1, A9, Th115;
then A22: f .: D // D by A9, A18, AFF_1:58;
f . d = d by A3, A16;
then d in f .: D by A16, Th110;
hence f .: D = D by A16, A22, AFF_1:59; :: thesis: verum
end;
x = f . x
proof
assume A23: x <> f . x ; :: thesis: contradiction
( f . x in C & f . x in D ) by A8, A9, A19, A21, Th110;
then C = D by A8, A9, A10, A23, AFF_1:30;
then Line p,a // Line p,b by A8, A9, AFF_1:58;
then Line p,a = Line p,b by A11, AFF_1:59;
hence contradiction by A2, A4, A6, A10, A11, A12, AFF_1:30; :: thesis: verum
end;
hence f . x = x ; :: thesis: verum
end;
hence f . x = x by A3; :: thesis: verum
end;
for x being Element of AFP holds f . x = (id the carrier of AFP) . x
proof
let x be Element of AFP; :: thesis: f . x = (id the carrier of AFP) . x
f . x = x by A5;
hence f . x = (id the carrier of AFP) . x by FUNCT_1:35; :: thesis: verum
end;
hence f = id the carrier of AFP by FUNCT_2:113; :: thesis: verum