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

hence f = id the carrier of AFP by FUNCT_2:63; :: thesis: verum

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

for x being Element of AFP holds f . x = (id the carrier of AFP) . x
by A6;
let x be Element of AFP; :: thesis: f . x = x

end;now :: thesis: ( not x in K implies f . x = x )

hence
f . x = x
by A3; :: thesis: verumassume
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

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

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

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

then consider c being Element of AFP such that
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 Line (p,a) // K by A13, AFF_1:44;

hence contradiction by A4, A7, A10, A16, AFF_1:45; :: thesis: verum

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

then consider d being Element of AFP such that
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 Line (p,b) // K by A23, AFF_1:44;

hence contradiction by A4, A8, A26, A20, AFF_1:45; :: thesis: verum

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

hence
f . x = x
; :: thesis: verum
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;( 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

hence f = id the carrier of AFP by FUNCT_2:63; :: thesis: verum