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 and
A5: f . p = p ; :: thesis: f = id the carrier of AFP
A6: for x being Element of AFP holds f . x = x
proof
let x be Element of AFP; :: thesis: f . x = x
now :: thesis: ( not x in K implies f . x = x )
assume not x in K ; :: thesis: f . x = x
consider a, b being Element of AFP such that
A7: a in K and
A8: b in K and
A9: a <> b by A2, AFF_1:19;
set A = Line (p,a);
A10: p in Line (p,a) by AFF_1:15;
f .: (Line (p,a)) = Line ((f . p),(f . a)) by A1, Th93;
then A11: f .: (Line (p,a)) = Line (p,a) by A3, A5, A7;
Line (p,a) is being_line by A4, A7, AFF_1:def 3;
then consider C being Subset of AFP such that
A12: x in C and
A13: Line (p,a) // C by AFF_1:49;
A14: C is being_line by A13, AFF_1:36;
f .: (Line (p,a)) // f .: C by A1, A13, Th95;
then A15: f .: C // C by A13, A11, AFF_1:44;
A16: a in Line (p,a) by AFF_1:15;
not C // K
proof
assume C // K ; :: thesis: contradiction
then Line (p,a) // K by A13, AFF_1:44;
hence contradiction by A4, A7, A10, A16, AFF_1:45; :: thesis: verum
end;
then consider c being Element of AFP such that
A17: c in C and
A18: c in K by A2, A14, AFF_1:58;
f . c = c by A3, A18;
then c in f .: C by A17, Th90;
then A19: f .: C = C by A17, A15, AFF_1:45;
set M = Line (p,b);
A20: b in Line (p,b) by AFF_1:15;
f .: (Line (p,b)) = Line ((f . p),(f . b)) by A1, Th93;
then A21: f .: (Line (p,b)) = Line (p,b) by A3, A5, A8;
Line (p,b) is being_line by A4, A8, AFF_1:def 3;
then consider D being Subset of AFP such that
A22: x in D and
A23: Line (p,b) // D by AFF_1:49;
A24: D is being_line by A23, AFF_1:36;
f .: (Line (p,b)) // f .: D by A1, A23, Th95;
then A25: f .: D // D by A23, A21, AFF_1:44;
A26: p in Line (p,b) by AFF_1:15;
not D // K
proof
assume D // K ; :: thesis: contradiction
then Line (p,b) // K by A23, AFF_1:44;
hence contradiction by A4, A8, A26, A20, AFF_1:45; :: thesis: verum
end;
then consider d being Element of AFP such that
A27: d in D and
A28: d in K by A2, A24, AFF_1:58;
f . d = d by A3, A28;
then d in f .: D by A27, Th90;
then A29: f .: D = D by A27, A25, AFF_1:45;
A30: Line (p,a) is being_line by A13, AFF_1:36;
x = f . x
proof
assume A31: x <> f . x ; :: thesis: contradiction
( f . x in C & f . x in D ) by A12, A22, A19, A29, Th90;
then C = D by A12, A22, A14, A24, A31, AFF_1:18;
then Line (p,a) // Line (p,b) by A13, A23, AFF_1:44;
then Line (p,a) = Line (p,b) by A10, A26, AFF_1:45;
hence contradiction by A2, A4, A7, A8, A9, A30, A10, A16, A20, AFF_1:18; :: 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 by A6;
hence f = id the carrier of AFP by FUNCT_2:63; :: thesis: verum