:: HOMOTHET semantic presentation
begin
Lm1: for AFP being AffinPlane holds
( AFP is Desarguesian iff for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9 )
proof
let AFP be AffinPlane; ::_thesis: ( AFP is Desarguesian iff for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9 )
thus ( AFP is Desarguesian implies for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9 ) ::_thesis: ( ( for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9 ) implies AFP is Desarguesian )
proof
assume A1: AFP is Desarguesian ; ::_thesis: for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9
let o, a, a9, p, p9, q, q9 be Element of AFP; ::_thesis: ( LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 implies p,q // p9,q9 )
assume that
A2: LIN o,a,a9 and
A3: LIN o,p,p9 and
A4: LIN o,q,q9 and
A5: not LIN o,a,p and
A6: not LIN o,a,q and
A7: a,p // a9,p9 and
A8: a,q // a9,q9 ; ::_thesis: p,q // p9,q9
set A = Line (o,a);
set P = Line (o,p);
set C = Line (o,q);
A9: a in Line (o,a) by AFF_1:15;
A10: o <> a by A5, AFF_1:7;
then A11: Line (o,a) is being_line by AFF_1:def_3;
A12: o in Line (o,a) by AFF_1:15;
then A13: a9 in Line (o,a) by A2, A10, A11, A9, AFF_1:25;
A14: q in Line (o,q) by AFF_1:15;
then A15: Line (o,a) <> Line (o,q) by A6, A11, A12, A9, AFF_1:21;
A16: o in Line (o,p) by AFF_1:15;
A17: p in Line (o,p) by AFF_1:15;
A18: o <> p by A5, AFF_1:7;
then A19: Line (o,p) is being_line by AFF_1:def_3;
then A20: p9 in Line (o,p) by A3, A18, A16, A17, AFF_1:25;
A21: o in Line (o,q) by AFF_1:15;
A22: o <> q by A6, AFF_1:7;
then A23: Line (o,q) is being_line by AFF_1:def_3;
then A24: q9 in Line (o,q) by A4, A22, A21, A14, AFF_1:25;
Line (o,a) <> Line (o,p) by A5, A11, A12, A9, A17, AFF_1:21;
hence p,q // p9,q9 by A1, A7, A8, A10, A18, A22, A11, A19, A23, A12, A9, A16, A17, A21, A14, A13, A20, A24, A15, AFF_2:def_4; ::_thesis: verum
end;
assume A25: for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9 ; ::_thesis: AFP is Desarguesian
now__::_thesis:_for_A,_P,_C_being_Subset_of_AFP
for_o,_a,_b,_c,_a9,_b9,_c9_being_Element_of_AFP_st_o_in_A_&_o_in_P_&_o_in_C_&_o_<>_a_&_o_<>_b_&_o_<>_c_&_a_in_A_&_a9_in_A_&_b_in_P_&_b9_in_P_&_c_in_C_&_c9_in_C_&_A_is_being_line_&_P_is_being_line_&_C_is_being_line_&_A_<>_P_&_A_<>_C_&_a,b_//_a9,b9_&_a,c_//_a9,c9_holds_
b,c_//_b9,c9
let A, P, C be Subset of AFP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AFP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AFP; ::_thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A26: o in A and
A27: o in P and
A28: o in C and
A29: o <> a and
A30: o <> b and
A31: o <> c and
A32: a in A and
A33: a9 in A and
A34: b in P and
A35: b9 in P and
A36: c in C and
A37: c9 in C and
A38: A is being_line and
A39: P is being_line and
A40: C is being_line and
A41: A <> P and
A42: A <> C and
A43: a,b // a9,b9 and
A44: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
A45: LIN o,b,b9 by A27, A34, A35, A39, AFF_1:21;
A46: not LIN o,a,c
proof
assume LIN o,a,c ; ::_thesis: contradiction
then c in A by A26, A29, A32, A38, AFF_1:25;
hence contradiction by A26, A28, A31, A36, A38, A40, A42, AFF_1:18; ::_thesis: verum
end;
A47: not LIN o,a,b
proof
assume LIN o,a,b ; ::_thesis: contradiction
then b in A by A26, A29, A32, A38, AFF_1:25;
hence contradiction by A26, A27, A30, A34, A38, A39, A41, AFF_1:18; ::_thesis: verum
end;
A48: LIN o,c,c9 by A28, A36, A37, A40, AFF_1:21;
LIN o,a,a9 by A26, A32, A33, A38, AFF_1:21;
hence b,c // b9,c9 by A25, A43, A44, A45, A48, A47, A46; ::_thesis: verum
end;
hence AFP is Desarguesian by AFF_2:def_4; ::_thesis: verum
end;
Lm2: for AFP being AffinPlane holds
( AFP is Moufangian iff for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9 )
proof
let AFP be AffinPlane; ::_thesis: ( AFP is Moufangian iff for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9 )
thus ( AFP is Moufangian implies for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9 ) ::_thesis: ( ( for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9 ) implies AFP is Moufangian )
proof
assume A1: AFP is Moufangian ; ::_thesis: for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9
let o be Element of AFP; ::_thesis: for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9
let K be Subset of AFP; ::_thesis: for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9
let c, c9, a, b, a9, b9 be Element of AFP; ::_thesis: ( o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A2: o in K and
A3: c in K and
A4: c9 in K and
A5: K is being_line and
A6: LIN o,a,a9 and
A7: LIN o,b,b9 and
A8: not a in K and
A9: a,b // K and
A10: a9,b9 // K and
A11: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
A12: a,b // a9,b9 by A5, A9, A10, AFF_1:31;
A13: now__::_thesis:_(_o_<>_c_implies_b,c_//_b9,c9_)
A14: now__::_thesis:_(_a_=_b_implies_b,c_//_b9,c9_)
assume A15: a = b ; ::_thesis: b,c // b9,c9
A16: now__::_thesis:_(_a9,o_//_K_implies_not_a9_<>_b9_)
A17: not o,a // K by A2, A8, AFF_1:34, AFF_1:35;
A18: LIN o,b9,b by A7, AFF_1:6;
assume that
A19: a9,o // K and
A20: a9 <> b9 ; ::_thesis: contradiction
o,a // o,a9 by A6, AFF_1:def_1;
then a9,o // o,a by AFF_1:4;
then A21: ( o,a // K or a9 = o ) by A19, AFF_1:32;
then b9 in K by A2, A5, A8, A10, AFF_1:23;
hence contradiction by A2, A5, A8, A15, A20, A21, A17, A18, AFF_1:25; ::_thesis: verum
end;
LIN o,a,o by AFF_1:7;
then LIN a9,b9,o by A2, A6, A7, A8, A15, AFF_1:8;
then a9,b9 // a9,o by AFF_1:def_1;
hence b,c // b9,c9 by A10, A11, A15, A16, AFF_1:32; ::_thesis: verum
end;
assume o <> c ; ::_thesis: b,c // b9,c9
hence b,c // b9,c9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A11, A12, A14, AFF_2:def_7; ::_thesis: verum
end;
now__::_thesis:_(_o_=_c_implies_b,c_//_b9,c9_)
assume A22: o = c ; ::_thesis: b,c // b9,c9
then LIN b,b9,c by A7, AFF_1:6;
then A23: b,b9 // b,c by AFF_1:def_1;
LIN a,c,a9 by A6, A22, AFF_1:6;
then LIN a,c,c9 by A3, A8, A11, AFF_1:9;
then A24: LIN c,c9,a by AFF_1:6;
then LIN c9,b,b9 by A2, A4, A5, A7, A8, A22, AFF_1:25;
then LIN b9,b,c9 by AFF_1:6;
then b9,b // b9,c9 by AFF_1:def_1;
then A25: b,b9 // b9,c9 by AFF_1:4;
c = c9 by A3, A4, A5, A8, A24, AFF_1:25;
then ( b = b9 implies b,c // b9,c9 ) by AFF_1:2;
hence b,c // b9,c9 by A23, A25, AFF_1:5; ::_thesis: verum
end;
hence b,c // b9,c9 by A13; ::_thesis: verum
end;
assume A26: for o being Element of AFP
for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9 ; ::_thesis: AFP is Moufangian
now__::_thesis:_for_K_being_Subset_of_AFP
for_o,_a,_b,_c,_a9,_b9,_c9_being_Element_of_AFP_st_K_is_being_line_&_o_in_K_&_c_in_K_&_c9_in_K_&_not_a_in_K_&_o_<>_c_&_a_<>_b_&_LIN_o,a,a9_&_LIN_o,b,b9_&_a,b_//_a9,b9_&_a,c_//_a9,c9_&_a,b_//_K_holds_
b,c_//_b9,c9
let K be Subset of AFP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AFP; ::_thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K implies b,c // b9,c9 )
assume that
A27: K is being_line and
A28: o in K and
A29: c in K and
A30: c9 in K and
A31: not a in K and
o <> c and
A32: a <> b and
A33: LIN o,a,a9 and
A34: LIN o,b,b9 and
A35: a,b // a9,b9 and
A36: a,c // a9,c9 and
A37: a,b // K ; ::_thesis: b,c // b9,c9
a9,b9 // K by A32, A35, A37, AFF_1:32;
hence b,c // b9,c9 by A26, A27, A28, A29, A30, A31, A33, A34, A36, A37; ::_thesis: verum
end;
hence AFP is Moufangian by AFF_2:def_7; ::_thesis: verum
end;
Lm3: for AFP being AffinPlane st AFP is Moufangian holds
for K being Subset of AFP
for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9
proof
let AFP be AffinPlane; ::_thesis: ( AFP is Moufangian implies for K being Subset of AFP
for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9 )
assume A1: AFP is Moufangian ; ::_thesis: for K being Subset of AFP
for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9
thus for K being Subset of AFP
for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9 ::_thesis: verum
proof
let K be Subset of AFP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9
let o, a, b, c, a9, b9, c9 be Element of AFP; ::_thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K implies LIN o,b,b9 )
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c9 in K and
A6: not a in K and
A7: a <> b and
A8: LIN o,a,a9 and
A9: a,b // a9,b9 and
A10: b,c // b9,c9 and
A11: a,c // a9,c9 and
A12: a,b // K ; ::_thesis: LIN o,b,b9
consider P being Subset of AFP such that
A13: a9 in P and
A14: K // P by A2, AFF_1:49;
A15: P is being_line by A14, AFF_1:36;
set A = Line (o,b);
set C = Line (o,a);
A16: o in Line (o,b) by AFF_1:15;
A17: b in Line (o,b) by AFF_1:15;
assume A18: not LIN o,b,b9 ; ::_thesis: contradiction
then o <> b by AFF_1:7;
then A19: Line (o,b) is being_line by AFF_1:def_3;
A20: not b in K by A6, A12, AFF_1:35;
not Line (o,b) // P
proof
assume Line (o,b) // P ; ::_thesis: contradiction
then Line (o,b) // K by A14, AFF_1:44;
hence contradiction by A3, A20, A16, A17, AFF_1:45; ::_thesis: verum
end;
then consider x being Element of AFP such that
A21: x in Line (o,b) and
A22: x in P by A19, A15, AFF_1:58;
A23: o in Line (o,a) by AFF_1:15;
a,b // P by A12, A14, AFF_1:43;
then a9,b9 // P by A7, A9, AFF_1:32;
then A24: b9 in P by A13, A15, AFF_1:23;
then A25: LIN b9,x,b9 by A15, A22, AFF_1:21;
A26: a in Line (o,a) by AFF_1:15;
A27: LIN o,b,x by A19, A16, A17, A21, AFF_1:21;
A28: Line (o,a) is being_line by A3, A6, AFF_1:def_3;
then A29: a9 in Line (o,a) by A3, A6, A8, A23, A26, AFF_1:25;
A30: b9 <> c9
proof
A31: a9,c9 // c,a by A11, AFF_1:4;
assume A32: b9 = c9 ; ::_thesis: contradiction
then P = K by A5, A14, A24, AFF_1:45;
then a9 = o by A2, A3, A6, A28, A23, A26, A29, A13, AFF_1:18;
then b9 = o by A2, A3, A4, A5, A6, A32, A31, AFF_1:48;
hence contradiction by A18, AFF_1:7; ::_thesis: verum
end;
A33: a9 <> b9
proof
assume A34: a9 = b9 ; ::_thesis: contradiction
A35: now__::_thesis:_not_a9_=_c9
assume a9 = c9 ; ::_thesis: contradiction
then b9 = o by A2, A3, A5, A6, A28, A23, A26, A29, A34, AFF_1:18;
hence contradiction by A18, AFF_1:7; ::_thesis: verum
end;
( a,c // b,c or a9 = c9 ) by A10, A11, A34, AFF_1:5;
then c,a // c,b by A35, AFF_1:4;
then LIN c,a,b by AFF_1:def_1;
then LIN a,c,b by AFF_1:6;
then a,c // a,b by AFF_1:def_1;
then a,b // a,c by AFF_1:4;
then a,c // K by A7, A12, AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2, A4, A6, AFF_1:23; ::_thesis: verum
end;
A36: b <> c by A4, A6, A12, AFF_1:35;
a9,x // K by A13, A14, A22, AFF_1:40;
then b,c // x,c9 by A1, A2, A3, A4, A5, A6, A8, A11, A12, A27, Lm2;
then b9,c9 // x,c9 by A10, A36, AFF_1:5;
then c9,b9 // c9,x by AFF_1:4;
then LIN c9,b9,x by AFF_1:def_1;
then A37: LIN b9,x,c9 by AFF_1:6;
LIN b9,x,a9 by A13, A15, A22, A24, AFF_1:21;
then LIN b9,c9,a9 by A18, A27, A37, A25, AFF_1:8;
then b9,c9 // b9,a9 by AFF_1:def_1;
then b9,c9 // a9,b9 by AFF_1:4;
then b,c // a9,b9 by A10, A30, AFF_1:5;
then a,b // b,c by A9, A33, AFF_1:5;
then b,c // K by A7, A12, AFF_1:32;
then c,b // K by AFF_1:34;
hence contradiction by A2, A4, A20, AFF_1:23; ::_thesis: verum
end;
end;
Lm4: for AFP being AffinPlane st AFP is Moufangian holds
for K, A, C being Subset of AFP
for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds
a,b // a9,b9
proof
let AFP be AffinPlane; ::_thesis: ( AFP is Moufangian implies for K, A, C being Subset of AFP
for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds
a,b // a9,b9 )
assume AFP is Moufangian ; ::_thesis: for K, A, C being Subset of AFP
for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds
a,b // a9,b9
then A1: AFP is translational by AFF_2:14;
let K, A, C be Subset of AFP; ::_thesis: for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds
a,b // a9,b9
let p, q, a, a9, b, b9 be Element of AFP; ::_thesis: ( K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 implies a,b // a9,b9 )
assume that
A2: K // A and
A3: K // C and
A4: K <> A and
A5: K <> C and
A6: p in K and
A7: q in K and
A8: a in A and
A9: a9 in A and
A10: b in C and
A11: b9 in C and
A12: p,a // q,a9 and
A13: p,b // q,b9 ; ::_thesis: a,b // a9,b9
A14: A is being_line by A2, AFF_1:36;
A15: C is being_line by A3, AFF_1:36;
K is being_line by A2, AFF_1:36;
hence a,b // a9,b9 by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A1, A14, A15, AFF_2:def_11; ::_thesis: verum
end;
theorem Th1: :: HOMOTHET:1
for AFP being AffinPlane
for o, a, p, b, x, y, p9, q, q9 being Element of AFP st not LIN o,a,p & LIN o,a,b & LIN o,a,x & LIN o,a,y & LIN o,p,p9 & LIN o,p,q & LIN o,p,q9 & p <> q & o <> q & o <> x & a,p // b,p9 & a,q // b,q9 & x,p // y,p9 & AFP is Desarguesian holds
x,q // y,q9
proof
let AFP be AffinPlane; ::_thesis: for o, a, p, b, x, y, p9, q, q9 being Element of AFP st not LIN o,a,p & LIN o,a,b & LIN o,a,x & LIN o,a,y & LIN o,p,p9 & LIN o,p,q & LIN o,p,q9 & p <> q & o <> q & o <> x & a,p // b,p9 & a,q // b,q9 & x,p // y,p9 & AFP is Desarguesian holds
x,q // y,q9
let o, a, p, b, x, y, p9, q, q9 be Element of AFP; ::_thesis: ( not LIN o,a,p & LIN o,a,b & LIN o,a,x & LIN o,a,y & LIN o,p,p9 & LIN o,p,q & LIN o,p,q9 & p <> q & o <> q & o <> x & a,p // b,p9 & a,q // b,q9 & x,p // y,p9 & AFP is Desarguesian implies x,q // y,q9 )
assume that
A1: not LIN o,a,p and
A2: LIN o,a,b and
A3: LIN o,a,x and
A4: LIN o,a,y and
A5: LIN o,p,p9 and
A6: LIN o,p,q and
A7: LIN o,p,q9 and
A8: p <> q and
A9: o <> q and
A10: o <> x and
A11: a,p // b,p9 and
A12: a,q // b,q9 and
A13: x,p // y,p9 and
A14: AFP is Desarguesian ; ::_thesis: x,q // y,q9
set B9 = Line (o,p);
A15: o in Line (o,p) by AFF_1:15;
A16: o <> p by A1, AFF_1:7;
then consider d being Element of AFP such that
A17: LIN x,p,d and
A18: d <> x and
A19: d <> p by A6, A8, A9, TRANSLAC:1;
A20: Line (o,p) is being_line by A16, AFF_1:def_3;
A21: q9 in Line (o,p) by A7, AFF_1:def_2;
q in Line (o,p) by A6, AFF_1:def_2;
then A22: LIN o,q,q9 by A20, A15, A21, AFF_1:21;
set A = Line (o,a);
o <> a by A1, AFF_1:7;
then A23: Line (o,a) is being_line by AFF_1:def_3;
A24: y in Line (o,a) by A4, AFF_1:def_2;
A25: p,a // p9,b by A11, AFF_1:4;
A26: not LIN o,p,a by A1, AFF_1:6;
set K = Line (x,p);
A27: Line (x,p) is being_line by A1, A3, AFF_1:def_3;
then consider M being Subset of AFP such that
A28: y in M and
A29: Line (x,p) // M by AFF_1:49;
A30: x in Line (x,p) by AFF_1:15;
A31: M is being_line by A29, AFF_1:36;
A32: p in Line (x,p) by AFF_1:15;
A33: d in Line (x,p) by A17, AFF_1:def_2;
A34: x in Line (o,a) by A3, AFF_1:def_2;
A35: not LIN o,a,d
proof
assume LIN o,a,d ; ::_thesis: contradiction
then d in Line (o,a) by AFF_1:def_2;
then Line (o,a) = Line (x,p) by A18, A27, A30, A33, A23, A34, AFF_1:18;
hence contradiction by A1, A32, AFF_1:def_2; ::_thesis: verum
end;
A36: o in Line (o,a) by AFF_1:15;
not o,d // M
proof
assume o,d // M ; ::_thesis: contradiction
then o,d // Line (x,p) by A29, AFF_1:43;
then d,o // Line (x,p) by AFF_1:34;
then o in Line (x,p) by A27, A33, AFF_1:23;
then Line (o,a) = Line (x,p) by A10, A27, A30, A23, A36, A34, AFF_1:18;
hence contradiction by A1, A32, AFF_1:def_2; ::_thesis: verum
end;
then consider d9 being Element of AFP such that
A37: d9 in M and
A38: LIN o,d,d9 by A31, AFF_1:59;
A39: d,x // d9,y by A30, A33, A28, A29, A37, AFF_1:39;
A40: p in Line (o,p) by AFF_1:15;
A41: not LIN o,d,q
proof
assume LIN o,d,q ; ::_thesis: contradiction
then A42: LIN o,q,d by AFF_1:6;
A43: LIN o,q,o by AFF_1:7;
LIN o,q,p by A6, AFF_1:6;
then LIN o,p,d by A9, A43, A42, AFF_1:8;
then d in Line (o,p) by AFF_1:def_2;
then Line (o,p) = Line (x,p) by A19, A27, A32, A33, A20, A40, AFF_1:18;
then Line (o,a) = Line (o,p) by A10, A27, A30, A23, A36, A34, A15, AFF_1:18;
hence contradiction by A1, A40, AFF_1:def_2; ::_thesis: verum
end;
A44: not LIN o,d,x
proof
assume LIN o,d,x ; ::_thesis: contradiction
then LIN o,x,d by AFF_1:6;
then d in Line (o,a) by A10, A23, A36, A34, AFF_1:25;
then Line (o,a) = Line (x,p) by A18, A27, A30, A33, A23, A34, AFF_1:18;
hence contradiction by A1, A32, AFF_1:def_2; ::_thesis: verum
end;
A45: not LIN o,p,d
proof
assume LIN o,p,d ; ::_thesis: contradiction
then d in Line (o,p) by AFF_1:def_2;
then Line (x,p) = Line (o,p) by A19, A27, A32, A33, A20, A40, AFF_1:18;
hence contradiction by A27, A30, A33, A15, A44, AFF_1:21; ::_thesis: verum
end;
A46: q in Line (o,p) by A6, AFF_1:def_2;
A47: not LIN o,a,q
proof
assume LIN o,a,q ; ::_thesis: contradiction
then q in Line (o,a) by AFF_1:def_2;
then Line (o,a) = Line (o,p) by A9, A23, A36, A20, A15, A46, AFF_1:18;
hence contradiction by A1, A40, AFF_1:def_2; ::_thesis: verum
end;
x in Line (o,a) by A3, AFF_1:def_2;
then A48: LIN o,x,y by A23, A36, A24, AFF_1:21;
x,p // Line (x,p) by A27, A30, A32, AFF_1:23;
then x,p // M by A29, AFF_1:43;
then y,p9 // M by A1, A3, A13, AFF_1:32;
then p9 in M by A28, A31, AFF_1:23;
then p,d // p9,d9 by A32, A33, A29, A37, AFF_1:39;
then a,d // b,d9 by A2, A5, A14, A38, A45, A26, A25, Lm1;
then d,q // d9,q9 by A2, A12, A14, A38, A47, A35, A22, Lm1;
hence x,q // y,q9 by A14, A38, A39, A41, A44, A22, A48, Lm1; ::_thesis: verum
end;
theorem Th2: :: HOMOTHET:2
for AFP being AffinPlane st ( for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) ) holds
AFP is Desarguesian
proof
let AFP be AffinPlane; ::_thesis: ( ( for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) ) implies AFP is Desarguesian )
assume A1: for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) ; ::_thesis: AFP is Desarguesian
now__::_thesis:_for_o,_a,_a9,_p,_p9,_q,_q9_being_Element_of_AFP_st_LIN_o,a,a9_&_LIN_o,p,p9_&_LIN_o,q,q9_&_not_LIN_o,a,p_&_not_LIN_o,a,q_&_a,p_//_a9,p9_&_a,q_//_a9,q9_holds_
p,q_//_p9,q9
let o, a, a9, p, p9, q, q9 be Element of AFP; ::_thesis: ( LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 implies p,q // p9,q9 )
assume that
A2: LIN o,a,a9 and
A3: LIN o,p,p9 and
A4: LIN o,q,q9 and
A5: not LIN o,a,p and
A6: not LIN o,a,q and
A7: a,p // a9,p9 and
A8: a,q // a9,q9 ; ::_thesis: p,q // p9,q9
A9: now__::_thesis:_(_o_<>_a9_implies_p,q_//_p9,q9_)
assume A10: o <> a9 ; ::_thesis: p,q // p9,q9
o <> a by A5, AFF_1:7;
then consider f being Permutation of the carrier of AFP such that
A11: f is dilatation and
A12: f . o = o and
A13: f . a = a9 by A1, A2, A10;
set s = f . q;
o,q // o,f . q by A11, A12, TRANSGEO:64;
then A14: LIN o,q,f . q by AFF_1:def_1;
set r = f . p;
o,p // o,f . p by A11, A12, TRANSGEO:64;
then A15: LIN o,p,f . p by AFF_1:def_1;
a,q // a9,f . q by A11, A13, TRANSGEO:64;
then A16: f . q = q9 by A2, A4, A6, A8, A14, AFF_1:56;
a,p // a9,f . p by A11, A13, TRANSGEO:64;
then f . p = p9 by A2, A3, A5, A7, A15, AFF_1:56;
hence p,q // p9,q9 by A11, A16, TRANSGEO:64; ::_thesis: verum
end;
now__::_thesis:_(_o_=_a9_implies_p,q_//_p9,q9_)
assume A17: o = a9 ; ::_thesis: p,q // p9,q9
then o = p9 by A3, A5, A7, AFF_1:55;
then p9 = q9 by A4, A6, A8, A17, AFF_1:55;
hence p,q // p9,q9 by AFF_1:3; ::_thesis: verum
end;
hence p,q // p9,q9 by A9; ::_thesis: verum
end;
hence AFP is Desarguesian by Lm1; ::_thesis: verum
end;
Lm5: for AFP being AffinPlane
for o, a, b, y, x being Element of AFP st o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds
LIN o,a,x
proof
let AFP be AffinPlane; ::_thesis: for o, a, b, y, x being Element of AFP st o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds
LIN o,a,x
let o, a, b, y, x be Element of AFP; ::_thesis: ( o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies LIN o,a,x )
assume that
A1: o <> a and
A2: o <> b and
A3: LIN o,a,b and
A4: LIN o,a,y and
A5: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ; ::_thesis: LIN o,a,x
assume A6: not LIN o,a,x ; ::_thesis: contradiction
then A7: b <> y by A2, A3, A5, AFF_1:54;
set A = Line (o,a);
A8: Line (o,a) is being_line by A1, AFF_1:def_3;
A9: b,y // a,x by A5, A6, AFF_1:4;
A10: a in Line (o,a) by AFF_1:15;
A11: y in Line (o,a) by A4, AFF_1:def_2;
A12: o in Line (o,a) by AFF_1:15;
b in Line (o,a) by A3, AFF_1:def_2;
then Line (o,a) = Line (b,y) by A8, A7, A11, AFF_1:24;
then x in Line (o,a) by A7, A10, A9, AFF_1:22;
hence contradiction by A6, A8, A12, A10, AFF_1:21; ::_thesis: verum
end;
Lm6: for AFP being AffinPlane
for o, a, b, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds
( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
proof
let AFP be AffinPlane; ::_thesis: for o, a, b, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds
( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
let o, a, b, x, y be Element of AFP; ::_thesis: ( o <> a & o <> b & LIN o,a,b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) )
assume that
A1: o <> a and
A2: o <> b and
A3: LIN o,a,b and
A4: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ; ::_thesis: ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
A5: LIN o,b,a by A3, AFF_1:6;
A6: now__::_thesis:_(_LIN_o,a,x_implies_(_o_<>_b_&_o_<>_a_&_LIN_o,b,a_&_(_(_not_LIN_o,b,y_&_LIN_o,y,x_&_b,y_//_a,x_)_or_(_LIN_o,b,y_&_ex_p,_p9_being_Element_of_AFP_st_
(_not_LIN_o,b,p_&_LIN_o,p,p9_&_b,p_//_a,p9_&_p,y_//_p9,x_&_LIN_o,b,x_)_)_)_)_)
assume A7: LIN o,a,x ; ::_thesis: ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
then consider p, q being Element of AFP such that
A8: not LIN o,a,p and
A9: LIN o,p,q and
A10: a,p // b,q and
A11: p,x // q,y and
A12: LIN o,a,y by A4;
A13: not LIN o,p,a by A8, AFF_1:6;
A14: q,y // p,x by A11, AFF_1:4;
A15: b,q // a,p by A10, AFF_1:4;
A16: LIN o,q,p by A9, AFF_1:6;
LIN o,a,o by AFF_1:7;
then A17: LIN o,b,x by A1, A3, A7, AFF_1:8;
set A = Line (o,b);
A18: o in Line (o,b) by AFF_1:15;
A19: a in Line (o,b) by A5, AFF_1:def_2;
A20: Line (o,b) is being_line by A2, AFF_1:def_3;
p,a // q,b by A10, AFF_1:4;
then A21: q <> o by A2, A3, A13, AFF_1:55;
A22: not LIN o,b,q
proof
assume LIN o,b,q ; ::_thesis: contradiction
then q in Line (o,b) by AFF_1:def_2;
then p in Line (o,b) by A21, A20, A18, A16, AFF_1:25;
hence contradiction by A8, A20, A18, A19, AFF_1:21; ::_thesis: verum
end;
y in Line (o,b) by A1, A12, A20, A18, A19, AFF_1:25;
hence ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) by A1, A2, A3, A15, A14, A16, A22, A17, AFF_1:6, AFF_1:def_2; ::_thesis: verum
end;
now__::_thesis:_(_not_LIN_o,a,x_implies_(_o_<>_b_&_o_<>_a_&_LIN_o,b,a_&_(_(_not_LIN_o,b,y_&_LIN_o,y,x_&_b,y_//_a,x_)_or_(_LIN_o,b,y_&_ex_p,_p9_being_Element_of_AFP_st_
(_not_LIN_o,b,p_&_LIN_o,p,p9_&_b,p_//_a,p9_&_p,y_//_p9,x_&_LIN_o,b,x_)_)_)_)_)
assume A23: not LIN o,a,x ; ::_thesis: ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) )
then A24: not LIN o,a,y by A1, A2, A3, A4, Lm5;
not LIN o,b,y
proof
A25: LIN o,b,o by AFF_1:7;
assume A26: LIN o,b,y ; ::_thesis: contradiction
LIN o,b,a by A3, AFF_1:6;
hence contradiction by A2, A24, A26, A25, AFF_1:8; ::_thesis: verum
end;
hence ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) by A1, A2, A3, A4, A23, AFF_1:4, AFF_1:6; ::_thesis: verum
end;
hence ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) by A6; ::_thesis: verum
end;
Lm7: for AFP being AffinPlane
for o, a, x, y, b being Element of AFP st o <> a & x = o & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds
y = o
proof
let AFP be AffinPlane; ::_thesis: for o, a, x, y, b being Element of AFP st o <> a & x = o & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds
y = o
let o, a, x, y, b be Element of AFP; ::_thesis: ( o <> a & x = o & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies y = o )
assume that
A1: o <> a and
A2: x = o and
A3: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ; ::_thesis: y = o
consider p, p9 being Element of AFP such that
A4: not LIN o,a,p and
A5: LIN o,p,p9 and
a,p // b,p9 and
A6: p,x // p9,y and
A7: LIN o,a,y by A2, A3, AFF_1:7;
set K = Line (o,p);
A8: o <> p by A4, AFF_1:7;
p9 in Line (o,p) by A5, AFF_1:def_2;
then A9: y in Line (o,p) by A2, A6, A8, AFF_1:22;
assume A10: y <> o ; ::_thesis: contradiction
A11: o in Line (o,p) by AFF_1:15;
A12: p in Line (o,p) by AFF_1:15;
set A = Line (o,a);
A13: Line (o,a) is being_line by A1, AFF_1:def_3;
A14: a in Line (o,a) by AFF_1:15;
A15: y in Line (o,a) by A7, AFF_1:def_2;
A16: o in Line (o,a) by AFF_1:15;
Line (o,p) is being_line by A8, AFF_1:def_3;
then p in Line (o,a) by A10, A13, A16, A12, A9, A11, A15, AFF_1:18;
hence contradiction by A4, A13, A16, A14, AFF_1:21; ::_thesis: verum
end;
Lm8: for AFP being AffinPlane
for o, a, b, x being Element of AFP st o <> a & LIN o,a,b holds
ex y being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) )
proof
let AFP be AffinPlane; ::_thesis: for o, a, b, x being Element of AFP st o <> a & LIN o,a,b holds
ex y being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) )
let o, a, b, x be Element of AFP; ::_thesis: ( o <> a & LIN o,a,b implies ex y being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) )
assume that
A1: o <> a and
A2: LIN o,a,b ; ::_thesis: ex y being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) )
A3: now__::_thesis:_(_LIN_o,a,x_implies_ex_y_being_Element_of_AFP_st_
(_(_not_LIN_o,a,x_&_LIN_o,x,y_&_a,x_//_b,y_)_or_(_LIN_o,a,x_&_ex_p,_p9_being_Element_of_AFP_st_
(_not_LIN_o,a,p_&_LIN_o,p,p9_&_a,p_//_b,p9_&_p,x_//_p9,y_&_LIN_o,a,y_)_)_)_)
consider p being Element of AFP such that
A4: not LIN o,a,p by A1, AFF_1:13;
set K = Line (o,p);
o <> p by A4, AFF_1:7;
then A5: Line (o,p) is being_line by AFF_1:def_3;
set A = Line (a,p);
a <> p by A4, AFF_1:7;
then Line (a,p) is being_line by AFF_1:def_3;
then consider B9 being Subset of AFP such that
A6: b in B9 and
A7: Line (a,p) // B9 by AFF_1:49;
A8: B9 is being_line by A7, AFF_1:36;
A9: a in Line (a,p) by AFF_1:15;
A10: p in Line (o,p) by AFF_1:15;
A11: p in Line (a,p) by AFF_1:15;
A12: o in Line (o,p) by AFF_1:15;
not B9 // Line (o,p)
proof
assume B9 // Line (o,p) ; ::_thesis: contradiction
then Line (a,p) // Line (o,p) by A7, AFF_1:44;
then Line (a,p) = Line (o,p) by A10, A11, AFF_1:45;
hence contradiction by A4, A12, A10, A9, A5, AFF_1:21; ::_thesis: verum
end;
then consider p9 being Element of AFP such that
A13: p9 in B9 and
A14: p9 in Line (o,p) by A5, A8, AFF_1:58;
A15: a,p // b,p9 by A9, A11, A6, A7, A13, AFF_1:39;
set M = Line (o,a);
A16: o in Line (o,a) by AFF_1:15;
o <> a by A4, AFF_1:7;
then A17: Line (o,a) is being_line by AFF_1:def_3;
set C = Line (p,x);
assume A18: LIN o,a,x ; ::_thesis: ex y being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) )
then A19: Line (p,x) is being_line by A4, AFF_1:def_3;
then consider D being Subset of AFP such that
A20: p9 in D and
A21: Line (p,x) // D by AFF_1:49;
A22: p in Line (p,x) by AFF_1:15;
A23: LIN o,p,p9 by A12, A10, A5, A14, AFF_1:21;
A24: a in Line (o,a) by AFF_1:15;
A25: x in Line (p,x) by AFF_1:15;
A26: x in Line (o,a) by A18, AFF_1:def_2;
A27: not D // Line (o,a)
proof
assume D // Line (o,a) ; ::_thesis: contradiction
then Line (p,x) // Line (o,a) by A21, AFF_1:44;
then Line (p,x) = Line (o,a) by A26, A25, AFF_1:45;
hence contradiction by A4, A16, A24, A22, A19, AFF_1:21; ::_thesis: verum
end;
D is being_line by A21, AFF_1:36;
then consider y being Element of AFP such that
A28: y in D and
A29: y in Line (o,a) by A17, A27, AFF_1:58;
A30: LIN o,a,y by A16, A24, A17, A29, AFF_1:21;
p,x // p9,y by A22, A25, A20, A21, A28, AFF_1:39;
hence ex y being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) by A18, A4, A23, A15, A30; ::_thesis: verum
end;
now__::_thesis:_(_not_LIN_o,a,x_implies_ex_y_being_Element_of_AFP_st_
(_(_not_LIN_o,a,x_&_LIN_o,x,y_&_a,x_//_b,y_)_or_(_LIN_o,a,x_&_ex_p,_p9_being_Element_of_AFP_st_
(_not_LIN_o,a,p_&_LIN_o,p,p9_&_a,p_//_b,p9_&_p,x_//_p9,y_&_LIN_o,a,y_)_)_)_)
o,a // o,b by A2, AFF_1:def_1;
then a,o // o,b by AFF_1:4;
then consider y being Element of AFP such that
A31: x,o // o,y and
A32: x,a // b,y by A1, DIRAF:40;
o,x // o,y by A31, AFF_1:4;
then A33: LIN o,x,y by AFF_1:def_1;
assume A34: not LIN o,a,x ; ::_thesis: ex y being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) )
a,x // b,y by A32, AFF_1:4;
hence ex y being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) by A34, A33; ::_thesis: verum
end;
hence ex y being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) by A3; ::_thesis: verum
end;
Lm9: for AFP being AffinPlane
for o, a, b, y being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex x being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) )
proof
let AFP be AffinPlane; ::_thesis: for o, a, b, y being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex x being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) )
let o, a, b, y be Element of AFP; ::_thesis: ( o <> a & o <> b & LIN o,a,b implies ex x being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) )
assume that
A1: o <> a and
A2: o <> b and
A3: LIN o,a,b ; ::_thesis: ex x being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) )
A4: LIN o,b,a by A3, AFF_1:6;
then consider x being Element of AFP such that
A5: ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) by A2, Lm8;
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) by A1, A2, A4, A5, Lm6;
hence ex x being Element of AFP st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ; ::_thesis: verum
end;
Lm10: for AFP being AffinPlane
for o, a, b, x, y being Element of AFP st o <> a & a = b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds
x = y
proof
let AFP be AffinPlane; ::_thesis: for o, a, b, x, y being Element of AFP st o <> a & a = b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds
x = y
let o, a, b, x, y be Element of AFP; ::_thesis: ( o <> a & a = b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies x = y )
assume that
A1: o <> a and
A2: a = b and
A3: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ; ::_thesis: x = y
A4: now__::_thesis:_(_LIN_o,a,x_&_x_<>_o_implies_x_=_y_)
A5: LIN o,x,x by AFF_1:7;
A6: LIN o,a,a by AFF_1:7;
assume that
A7: LIN o,a,x and
A8: x <> o ; ::_thesis: x = y
consider p, q being Element of AFP such that
A9: not LIN o,a,p and
A10: LIN o,p,q and
A11: a,p // b,q and
A12: p,x // q,y and
A13: LIN o,a,y by A3, A7;
A14: LIN o,p,p by AFF_1:7;
A15: not LIN o,p,x
proof
assume LIN o,p,x ; ::_thesis: contradiction
then A16: LIN o,x,p by AFF_1:6;
A17: LIN o,x,o by AFF_1:7;
LIN o,x,a by A7, AFF_1:6;
hence contradiction by A8, A9, A17, A16, AFF_1:8; ::_thesis: verum
end;
LIN o,a,o by AFF_1:7;
then A18: LIN o,x,y by A1, A7, A13, AFF_1:8;
a,p // a,p by AFF_1:2;
then A19: p,x // p,y by A2, A9, A10, A11, A12, A6, A14, AFF_1:56;
p,x // p,x by AFF_1:2;
hence x = y by A14, A15, A18, A19, A5, AFF_1:56; ::_thesis: verum
end;
now__::_thesis:_(_not_LIN_o,a,x_implies_x_=_y_)
A20: LIN o,x,x by AFF_1:7;
A21: LIN o,a,a by AFF_1:7;
A22: a,x // a,x by AFF_1:2;
assume not LIN o,a,x ; ::_thesis: x = y
hence x = y by A2, A3, A22, A21, A20, AFF_1:56; ::_thesis: verum
end;
hence x = y by A1, A3, A4, Lm7; ::_thesis: verum
end;
Lm11: for AFP being AffinPlane
for o, a, b, x, y, r being Element of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) holds
y = r
proof
let AFP be AffinPlane; ::_thesis: for o, a, b, x, y, r being Element of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) holds
y = r
let o, a, b, x, y, r be Element of AFP; ::_thesis: ( o <> a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) implies y = r )
assume that
A1: o <> a and
A2: LIN o,a,b and
A3: AFP is Desarguesian and
A4: LIN o,a,x and
A5: ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) and
A6: ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) ; ::_thesis: y = r
consider q, q9 being Element of AFP such that
A7: not LIN o,a,q and
A8: LIN o,q,q9 and
A9: a,q // b,q9 and
A10: q,x // q9,r and
A11: LIN o,a,r by A6;
A12: o <> q by A7, AFF_1:7;
consider p, p9 being Element of AFP such that
A13: not LIN o,a,p and
A14: LIN o,p,p9 and
A15: a,p // b,p9 and
A16: p,x // p9,y and
A17: LIN o,a,y by A5;
A18: ( a = x implies y = r )
proof
A19: q,a // q9,b by A9, AFF_1:4;
A20: not LIN o,q,a by A7, AFF_1:6;
A21: p,a // p9,b by A15, AFF_1:4;
assume A22: a = x ; ::_thesis: y = r
not LIN o,p,a by A13, AFF_1:6;
then b = y by A2, A14, A16, A17, A22, A21, AFF_1:56;
hence y = r by A2, A8, A10, A11, A22, A20, A19, AFF_1:56; ::_thesis: verum
end;
A23: o <> p by A13, AFF_1:7;
A24: ( a <> b & a <> x & p <> q & o <> x implies y = r )
proof
assume that
a <> b and
a <> x and
A25: p <> q and
A26: o <> x ; ::_thesis: y = r
A27: now__::_thesis:_(_LIN_o,p,q_implies_y_=_r_)
set K = Line (o,p);
set A = Line (o,a);
A28: LIN o,q,o by AFF_1:7;
A29: o in Line (o,a) by AFF_1:15;
A30: p in Line (o,p) by AFF_1:15;
A31: o in Line (o,p) by AFF_1:15;
A32: Line (o,a) is being_line by A1, AFF_1:def_3;
A33: x in Line (o,a) by A4, AFF_1:def_2;
r in Line (o,a) by A11, AFF_1:def_2;
then A34: LIN o,x,r by A32, A29, A33, AFF_1:21;
A35: x,p // y,p9 by A16, AFF_1:4;
assume A36: LIN o,p,q ; ::_thesis: y = r
then LIN o,q,p by AFF_1:6;
then LIN o,p,q9 by A8, A12, A28, AFF_1:8;
then x,q // y,q9 by A2, A3, A4, A13, A14, A15, A17, A9, A12, A25, A26, A36, A35, Th1;
then A37: q,x // q9,y by AFF_1:4;
A38: Line (o,p) is being_line by A23, AFF_1:def_3;
A39: q in Line (o,p) by A36, AFF_1:def_2;
A40: not LIN o,q,x
proof
assume A41: LIN o,q,x ; ::_thesis: contradiction
Line (o,p) = Line (o,q) by A12, A38, A31, A39, AFF_1:24;
then x in Line (o,p) by A41, AFF_1:def_2;
then A42: p in Line (o,a) by A26, A32, A29, A33, A38, A31, A30, AFF_1:18;
A43: a in Line (o,a) by AFF_1:15;
Line (o,a) is being_line by A1, AFF_1:def_3;
hence contradiction by A13, A29, A43, A42, AFF_1:21; ::_thesis: verum
end;
y in Line (o,a) by A17, AFF_1:def_2;
then LIN o,x,y by A32, A29, A33, AFF_1:21;
hence y = r by A8, A10, A37, A40, A34, AFF_1:56; ::_thesis: verum
end;
now__::_thesis:_(_not_LIN_o,p,q_implies_y_=_r_)
A44: not LIN o,p,x
proof
assume LIN o,p,x ; ::_thesis: contradiction
then A45: LIN o,x,p by AFF_1:6;
LIN o,a,o by AFF_1:7;
hence contradiction by A4, A13, A26, A45, AFF_1:11; ::_thesis: verum
end;
set K = Line (o,q);
set A = Line (o,a);
assume A46: not LIN o,p,q ; ::_thesis: y = r
A47: o in Line (o,a) by AFF_1:15;
A48: q in Line (o,q) by AFF_1:15;
A49: o in Line (o,q) by AFF_1:15;
A50: Line (o,a) is being_line by A1, AFF_1:def_3;
A51: x in Line (o,a) by A4, AFF_1:def_2;
A52: y in Line (o,a) by A17, AFF_1:def_2;
then A53: LIN o,x,y by A50, A47, A51, AFF_1:21;
A54: Line (o,q) is being_line by A12, AFF_1:def_3;
A55: not LIN o,q,x
proof
assume LIN o,q,x ; ::_thesis: contradiction
then x in Line (o,q) by AFF_1:def_2;
then A56: q in Line (o,a) by A26, A50, A47, A51, A54, A49, A48, AFF_1:18;
A57: a in Line (o,a) by AFF_1:15;
Line (o,a) is being_line by A1, AFF_1:def_3;
hence contradiction by A7, A47, A57, A56, AFF_1:21; ::_thesis: verum
end;
r in Line (o,a) by A11, AFF_1:def_2;
then A58: LIN o,x,r by A50, A47, A51, AFF_1:21;
A59: LIN o,x,y by A50, A47, A51, A52, AFF_1:21;
p,q // p9,q9 by A2, A3, A13, A14, A15, A7, A8, A9, Lm1;
then q,x // q9,y by A3, A14, A16, A8, A46, A44, A53, Lm1;
hence y = r by A8, A10, A55, A59, A58, AFF_1:56; ::_thesis: verum
end;
hence y = r by A27; ::_thesis: verum
end;
A60: o <> a by A13, AFF_1:7;
A61: ( p = q & o <> x implies y = r )
proof
assume that
A62: p = q and
A63: o <> x ; ::_thesis: y = r
A64: not LIN o,p,x
proof
assume LIN o,p,x ; ::_thesis: contradiction
then A65: LIN o,x,p by AFF_1:6;
A66: LIN o,x,o by AFF_1:7;
LIN o,x,a by A4, AFF_1:6;
hence contradiction by A13, A63, A66, A65, AFF_1:8; ::_thesis: verum
end;
A67: LIN o,a,o by AFF_1:7;
then A68: LIN o,x,y by A4, A17, A60, AFF_1:8;
A69: LIN o,x,r by A4, A11, A60, A67, AFF_1:8;
p9 = q9 by A2, A13, A14, A15, A8, A9, A62, AFF_1:56;
hence y = r by A14, A16, A10, A62, A68, A69, A64, AFF_1:56; ::_thesis: verum
end;
A70: ( o = x implies y = r )
proof
assume A71: o = x ; ::_thesis: y = r
then y = o by A1, A4, A5, Lm7;
hence y = r by A1, A4, A6, A71, Lm7; ::_thesis: verum
end;
( a = b implies y = r )
proof
assume A72: a = b ; ::_thesis: y = r
then x = y by A1, A4, A5, Lm10;
hence y = r by A1, A4, A6, A72, Lm10; ::_thesis: verum
end;
hence y = r by A70, A61, A18, A24; ::_thesis: verum
end;
Lm12: for AFP being AffinPlane
for o, a, b, x, y, r being Element of AFP st o <> a & o <> b & LIN o,a,b & AFP is Desarguesian & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) & ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) holds
x = r
proof
let AFP be AffinPlane; ::_thesis: for o, a, b, x, y, r being Element of AFP st o <> a & o <> b & LIN o,a,b & AFP is Desarguesian & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) & ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) holds
x = r
let o, a, b, x, y, r be Element of AFP; ::_thesis: ( o <> a & o <> b & LIN o,a,b & AFP is Desarguesian & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) & ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) implies x = r )
assume that
A1: o <> a and
A2: o <> b and
A3: LIN o,a,b and
A4: AFP is Desarguesian and
A5: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) and
A6: ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) ; ::_thesis: x = r
A7: ( ( not LIN o,b,y & LIN o,y,r & b,y // a,r ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,r & LIN o,b,r ) ) ) by A1, A2, A3, A6, Lm6;
A8: LIN o,b,a by A3, AFF_1:6;
( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st
( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) by A1, A2, A3, A5, Lm6;
hence x = r by A2, A4, A8, A7, Lm11, AFF_1:56; ::_thesis: verum
end;
Lm13: for AFP being AffinPlane
for o, a, b being Element of AFP st AFP is Desarguesian & o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) )
proof
let AFP be AffinPlane; ::_thesis: for o, a, b being Element of AFP st AFP is Desarguesian & o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) )
let o, a, b be Element of AFP; ::_thesis: ( AFP is Desarguesian & o <> a & o <> b & LIN o,a,b implies ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) )
defpred S1[ Element of AFP, Element of AFP] means ( ( not LIN o,a,$1 & LIN o,$1,$2 & a,$1 // b,$2 ) or ( LIN o,a,$1 & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,$1 // p9,$2 & LIN o,a,$2 ) ) );
assume that
A1: AFP is Desarguesian and
A2: o <> a and
A3: o <> b and
A4: LIN o,a,b ; ::_thesis: ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) )
A5: for y being Element of AFP ex x being Element of AFP st S1[x,y] by A2, A3, A4, Lm9;
A6: for x being Element of AFP ex y being Element of AFP st S1[x,y] by A2, A4, Lm8;
A7: for x, y, s being Element of AFP st S1[x,y] & S1[x,s] holds
y = s by A1, A2, A4, Lm11, AFF_1:56;
A8: for x, y, r being Element of AFP st S1[x,y] & S1[r,y] holds
x = r by A1, A2, A3, A4, Lm12;
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff S1[x,y] ) from TRANSGEO:sch_1(A6, A5, A8, A7);
hence ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ; ::_thesis: verum
end;
Lm14: for AFP being AffinPlane
for o, a, b, x, y, z, t being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) holds
x,z // y,t
proof
let AFP be AffinPlane; ::_thesis: for o, a, b, x, y, z, t being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) holds
x,z // y,t
let o, a, b, x, y, z, t be Element of AFP; ::_thesis: ( AFP is Desarguesian & o <> a & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) implies x,z // y,t )
assume that
A1: AFP is Desarguesian and
A2: o <> a and
A3: LIN o,a,b and
A4: not LIN o,a,x and
A5: LIN o,x,y and
A6: a,x // b,y and
A7: LIN o,a,z and
A8: ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) ; ::_thesis: x,z // y,t
consider p, p9 being Element of AFP such that
A9: not LIN o,a,p and
A10: LIN o,p,p9 and
A11: a,p // b,p9 and
A12: p,z // p9,t and
A13: LIN o,a,t by A8;
A14: now__::_thesis:_(_a_=_z_implies_x,z_//_y,t_)
A15: p,a // p9,b by A11, AFF_1:4;
assume A16: a = z ; ::_thesis: x,z // y,t
not LIN o,p,a by A9, AFF_1:6;
then z,x // t,y by A3, A6, A10, A12, A13, A16, A15, AFF_1:56;
hence x,z // y,t by AFF_1:4; ::_thesis: verum
end;
A17: p,x // p9,y by A1, A3, A4, A5, A6, A9, A10, A11, Lm1;
A18: now__::_thesis:_(_z_<>_o_&_not_LIN_o,p,x_implies_x,z_//_y,t_)
assume that
A19: z <> o and
A20: not LIN o,p,x ; ::_thesis: x,z // y,t
A21: not LIN o,p,z
proof
A22: LIN o,p,o by AFF_1:7;
assume A23: LIN o,p,z ; ::_thesis: contradiction
LIN o,z,a by A7, AFF_1:6;
then LIN o,p,a by A19, A23, A22, AFF_1:11;
hence contradiction by A9, AFF_1:6; ::_thesis: verum
end;
LIN o,a,o by AFF_1:7;
then LIN o,z,t by A2, A7, A13, AFF_1:8;
hence x,z // y,t by A1, A5, A10, A12, A17, A20, A21, Lm1; ::_thesis: verum
end;
A24: o <> x by A4, AFF_1:7;
A25: now__::_thesis:_(_z_<>_o_&_LIN_o,p,x_&_a_<>_z_implies_x,z_//_y,t_)
assume that
A26: z <> o and
A27: LIN o,p,x and
a <> z ; ::_thesis: x,z // y,t
now__::_thesis:_(_x_<>_p_implies_x,z_//_y,t_)
A28: LIN o,x,o by AFF_1:7;
LIN o,x,p by A27, AFF_1:6;
then A29: LIN o,p,y by A5, A24, A28, AFF_1:8;
assume A30: x <> p ; ::_thesis: x,z // y,t
z,p // t,p9 by A12, AFF_1:4;
then z,x // t,y by A1, A3, A6, A7, A9, A10, A11, A13, A24, A26, A27, A30, A29, Th1;
hence x,z // y,t by AFF_1:4; ::_thesis: verum
end;
hence x,z // y,t by A3, A4, A5, A6, A10, A11, A12, AFF_1:56; ::_thesis: verum
end;
now__::_thesis:_(_z_=_o_implies_x,z_//_y,t_)
A31: o,x // o,y by A5, AFF_1:def_1;
assume A32: z = o ; ::_thesis: x,z // y,t
then t = o by A2, A7, A8, Lm7;
hence x,z // y,t by A32, A31, AFF_1:4; ::_thesis: verum
end;
hence x,z // y,t by A18, A14, A25; ::_thesis: verum
end;
Lm15: for AFP being AffinPlane
for o, a, b, x, y, z, t being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t holds
x,z // y,t
proof
let AFP be AffinPlane; ::_thesis: for o, a, b, x, y, z, t being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t holds
x,z // y,t
let o, a, b, x, y, z, t be Element of AFP; ::_thesis: ( AFP is Desarguesian & o <> a & LIN o,a,b & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t implies x,z // y,t )
assume that
A1: AFP is Desarguesian and
A2: o <> a and
A3: LIN o,a,b and
A4: LIN o,a,x and
A5: ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) and
A6: not LIN o,a,z and
A7: LIN o,z,t and
A8: a,z // b,t ; ::_thesis: x,z // y,t
z,x // t,y by A1, A2, A3, A4, A5, A6, A7, A8, Lm14;
hence x,z // y,t by AFF_1:4; ::_thesis: verum
end;
Lm16: for AFP being AffinPlane
for o, a, x, b, y, z, t being Element of AFP st o <> a & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & LIN o,a,z & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) holds
x,z // y,t
proof
let AFP be AffinPlane; ::_thesis: for o, a, x, b, y, z, t being Element of AFP st o <> a & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & LIN o,a,z & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) holds
x,z // y,t
let o, a, x, b, y, z, t be Element of AFP; ::_thesis: ( o <> a & LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & LIN o,a,z & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) implies x,z // y,t )
assume that
A1: o <> a and
A2: LIN o,a,x and
A3: ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) and
A4: LIN o,a,z and
A5: ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) ; ::_thesis: x,z // y,t
set A = Line (o,a);
A6: x in Line (o,a) by A2, AFF_1:def_2;
A7: z in Line (o,a) by A4, AFF_1:def_2;
A8: y in Line (o,a) by A3, AFF_1:def_2;
A9: t in Line (o,a) by A5, AFF_1:def_2;
A10: Line (o,a) is being_line by A1, AFF_1:def_3;
now__::_thesis:_(_x_<>_z_implies_x,z_//_y,t_)
assume A11: x <> z ; ::_thesis: x,z // y,t
then Line (o,a) = Line (x,z) by A10, A6, A7, AFF_1:24;
hence x,z // y,t by A8, A9, A11, AFF_1:22; ::_thesis: verum
end;
hence x,z // y,t by AFF_1:3; ::_thesis: verum
end;
Lm17: for AFP being AffinPlane
for o, a, b being Element of AFP
for f being Permutation of the carrier of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) holds
( f is dilatation & f . o = o & f . a = b )
proof
let AFP be AffinPlane; ::_thesis: for o, a, b being Element of AFP
for f being Permutation of the carrier of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) holds
( f is dilatation & f . o = o & f . a = b )
let o, a, b be Element of AFP; ::_thesis: for f being Permutation of the carrier of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) holds
( f is dilatation & f . o = o & f . a = b )
let f be Permutation of the carrier of AFP; ::_thesis: ( o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) implies ( f is dilatation & f . o = o & f . a = b ) )
assume that
A1: o <> a and
A2: LIN o,a,b and
A3: AFP is Desarguesian ; ::_thesis: ( ex x, y being Element of AFP st
( ( not f . x = y or ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies ( ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) & not f . x = y ) ) or ( f is dilatation & f . o = o & f . a = b ) )
assume A4: for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ; ::_thesis: ( f is dilatation & f . o = o & f . a = b )
for x, r being Element of AFP holds x,r // f . x,f . r
proof
let x, r be Element of AFP; ::_thesis: x,r // f . x,f . r
set y = f . x;
set s = f . r;
A5: ( ( not LIN o,a,r & LIN o,r,f . r & a,r // b,f . r ) or ( LIN o,a,r & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,f . r & LIN o,a,f . r ) ) ) by A4;
( ( not LIN o,a,x & LIN o,x,f . x & a,x // b,f . x ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,f . x & LIN o,a,f . x ) ) ) by A4;
hence x,r // f . x,f . r by A1, A2, A3, A5, Lm1, Lm14, Lm15, Lm16; ::_thesis: verum
end;
hence f is dilatation by TRANSGEO:64; ::_thesis: ( f . o = o & f . a = b )
thus f . o = o ::_thesis: f . a = b
proof
set y = f . o;
( ( not LIN o,a,o & LIN o,o,f . o & a,o // b,f . o ) or ( LIN o,a,o & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,o // p9,f . o & LIN o,a,f . o ) ) ) by A4;
hence f . o = o by A1, Lm7; ::_thesis: verum
end;
thus f . a = b ::_thesis: verum
proof
set y = f . a;
LIN o,a,a by AFF_1:7;
then consider p, p9 being Element of AFP such that
A6: not LIN o,a,p and
A7: LIN o,p,p9 and
A8: a,p // b,p9 and
A9: p,a // p9,f . a and
A10: LIN o,a,f . a by A4;
A11: p,a // p9,b by A8, AFF_1:4;
not LIN o,p,a by A6, AFF_1:6;
hence f . a = b by A2, A7, A9, A10, A11, AFF_1:56; ::_thesis: verum
end;
end;
theorem Th3: :: HOMOTHET:3
for AFP being AffinPlane st AFP is Desarguesian holds
for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b )
proof
let AFP be AffinPlane; ::_thesis: ( AFP is Desarguesian implies for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) )
assume A1: AFP is Desarguesian ; ::_thesis: for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b )
let o, a, b be Element of AFP; ::_thesis: ( o <> a & o <> b & LIN o,a,b implies ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) )
assume that
A2: o <> a and
A3: o <> b and
A4: LIN o,a,b ; ::_thesis: ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b )
consider f being Permutation of the carrier of AFP such that
A5: for x, y being Element of AFP holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) by A1, A2, A3, A4, Lm13;
A6: f . a = b by A1, A2, A4, A5, Lm17;
A7: f . o = o by A1, A2, A4, A5, Lm17;
f is dilatation by A1, A2, A4, A5, Lm17;
hence ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) by A7, A6; ::_thesis: verum
end;
theorem :: HOMOTHET:4
for AFP being AffinPlane holds
( AFP is Desarguesian iff for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) ) by Th2, Th3;
definition
let AFP be AffinPlane;
let f be Permutation of the carrier of AFP;
let K be Subset of AFP;
predf is_Sc K means :Def1: :: HOMOTHET:def 1
( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & ( for x being Element of AFP holds x,f . x // K ) );
end;
:: deftheorem Def1 defines is_Sc HOMOTHET:def_1_:_
for AFP being AffinPlane
for f being Permutation of the carrier of AFP
for K being Subset of AFP holds
( f is_Sc K iff ( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & ( for x being Element of AFP holds x,f . x // K ) ) );
theorem Th5: :: HOMOTHET:5
for AFP being AffinPlane
for p being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds
f = id the carrier of AFP
proof
let AFP be AffinPlane; ::_thesis: for p being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds
f = id the carrier of AFP
let p be Element of AFP; ::_thesis: for K being Subset of AFP
for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds
f = id the carrier of AFP
let K be Subset of AFP; ::_thesis: for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds
f = id the carrier of AFP
let f be Permutation of the carrier of AFP; ::_thesis: ( f is_Sc K & f . p = p & not p in K implies f = id the carrier of AFP )
assume that
A1: f is_Sc K and
A2: f . p = p and
A3: not p in K ; ::_thesis: f = id the carrier of AFP
A4: K is being_line by A1, Def1;
A5: for x being Element of AFP st x in K holds
f . x = x by A1, Def1;
f is collineation by A1, Def1;
hence f = id the carrier of AFP by A2, A3, A4, A5, TRANSGEO:93; ::_thesis: verum
end;
theorem Th6: :: HOMOTHET:6
for AFP being AffinPlane st ( for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) ) holds
AFP is Moufangian
proof
let AFP be AffinPlane; ::_thesis: ( ( for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) ) implies AFP is Moufangian )
assume A1: for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) ; ::_thesis: AFP is Moufangian
now__::_thesis:_for_o_being_Element_of_AFP
for_K_being_Subset_of_AFP
for_c,_c9,_a,_b,_a9,_b9_being_Element_of_AFP_st_o_in_K_&_c_in_K_&_c9_in_K_&_K_is_being_line_&_LIN_o,a,a9_&_LIN_o,b,b9_&_not_a_in_K_&_a,b_//_K_&_a9,b9_//_K_&_a,c_//_a9,c9_holds_
b,c_//_b9,c9
let o be Element of AFP; ::_thesis: for K being Subset of AFP
for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9
let K be Subset of AFP; ::_thesis: for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds
b,c // b9,c9
let c, c9, a, b, a9, b9 be Element of AFP; ::_thesis: ( o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A2: o in K and
A3: c in K and
A4: c9 in K and
A5: K is being_line and
A6: LIN o,a,a9 and
A7: LIN o,b,b9 and
A8: not a in K and
A9: a,b // K and
A10: a9,b9 // K and
A11: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
consider f being Permutation of the carrier of AFP such that
A12: f is_Sc K and
A13: f . a = b by A1, A8, A9;
A14: f is collineation by A12, Def1;
A15: a,b // a9,b9 by A5, A9, A10, AFF_1:31;
A16: f . a9 = b9
proof
set x = f . a9;
A17: now__::_thesis:_(_a_<>_b_implies_f_._a9_=_b9_)
f . o = o by A2, A12, Def1;
then A18: LIN o,b,f . a9 by A6, A13, A14, TRANSGEO:84;
a9,f . a9 // K by A12, Def1;
then A19: a,b // a9,f . a9 by A5, A9, AFF_1:31;
assume a <> b ; ::_thesis: f . a9 = b9
hence f . a9 = b9 by A2, A6, A7, A8, A9, A15, A19, A18, AFF_1:46, AFF_1:56; ::_thesis: verum
end;
now__::_thesis:_(_a_=_b_implies_f_._a9_=_b9_)
assume A20: a = b ; ::_thesis: f . a9 = b9
then f = id the carrier of AFP by A8, A12, A13, Th5;
then f . a9 = a9 by FUNCT_1:18;
hence f . a9 = b9 by A2, A6, A7, A8, A10, A20, AFF_1:47; ::_thesis: verum
end;
hence f . a9 = b9 by A17; ::_thesis: verum
end;
A21: f . c9 = c9 by A4, A12, Def1;
f . c = c by A3, A12, Def1;
hence b,c // b9,c9 by A11, A13, A14, A21, A16, TRANSGEO:83; ::_thesis: verum
end;
hence AFP is Moufangian by Lm2; ::_thesis: verum
end;
Lm18: for AFP being AffinPlane
for a, b, x, y being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) holds
( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) )
proof
let AFP be AffinPlane; ::_thesis: for a, b, x, y being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) holds
( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) )
let a, b, x, y be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) holds
( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) )
let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) implies ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) ) )
assume that
A1: a,b // K and
A2: not a in K and
A3: ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ; ::_thesis: ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) )
thus ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) ) by A1, A2, A3, AFF_1:34, AFF_1:35; ::_thesis: verum
end;
Lm19: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
for x being Element of AFP ex y being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
proof
let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
for x being Element of AFP ex y being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
let a, b be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K holds
for x being Element of AFP ex y being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K implies for x being Element of AFP ex y being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
assume that
A1: a,b // K and
A2: not a in K ; ::_thesis: for x being Element of AFP ex y being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
A3: not b in K by A1, A2, AFF_1:35;
A4: K is being_line by A1, AFF_1:26;
let x be Element of AFP; ::_thesis: ex y being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
consider p, q being Element of AFP such that
A5: p in K and
q in K and
p <> q by A1, AFF_1:19, AFF_1:26;
A6: p <> b by A1, A2, A5, AFF_1:35;
now__::_thesis:_(_not_x_in_K_implies_ex_y_being_Element_of_AFP_st_
(_(_x_in_K_&_x_=_y_)_or_(_not_x_in_K_&_ex_p,_p9_being_Element_of_AFP_st_
(_p_in_K_&_p9_in_K_&_p,a_//_p9,x_&_p,b_//_p9,y_&_x,y_//_K_)_)_)_)
set B9 = Line (p,b);
set A = Line (p,a);
assume A7: not x in K ; ::_thesis: ex y being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
A8: a in Line (p,a) by AFF_1:15;
Line (p,a) is being_line by A2, A5, AFF_1:def_3;
then consider C being Subset of AFP such that
A9: x in C and
A10: Line (p,a) // C by AFF_1:49;
A11: C is being_line by A10, AFF_1:36;
A12: p in Line (p,a) by AFF_1:15;
then not Line (p,a) // K by A2, A5, A8, AFF_1:45;
then not C // K by A10, AFF_1:44;
then consider p9 being Element of AFP such that
A13: p9 in C and
A14: p9 in K by A4, A11, AFF_1:58;
Line (p,b) is being_line by A6, AFF_1:def_3;
then consider D being Subset of AFP such that
A15: p9 in D and
A16: Line (p,b) // D by AFF_1:49;
A17: b in Line (p,b) by AFF_1:15;
K is being_line by A1, AFF_1:26;
then consider M being Subset of AFP such that
A18: x in M and
A19: K // M by AFF_1:49;
A20: M is being_line by A19, AFF_1:36;
A21: p in Line (p,b) by AFF_1:15;
then A22: not Line (p,b) // K by A5, A3, A17, AFF_1:45;
A23: not D // M
proof
assume D // M ; ::_thesis: contradiction
then Line (p,b) // M by A16, AFF_1:44;
hence contradiction by A22, A19, AFF_1:44; ::_thesis: verum
end;
D is being_line by A16, AFF_1:36;
then consider y being Element of AFP such that
A24: y in D and
A25: y in M by A20, A23, AFF_1:58;
A26: p,b // p9,y by A21, A17, A15, A16, A24, AFF_1:39;
A27: x,y // K by A18, A19, A25, AFF_1:40;
p,a // p9,x by A12, A8, A9, A10, A13, AFF_1:39;
hence ex y being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) by A5, A7, A14, A27, A26; ::_thesis: verum
end;
hence ex y being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ; ::_thesis: verum
end;
Lm20: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
for y being Element of AFP ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
proof
let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
for y being Element of AFP ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
let a, b be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K holds
for y being Element of AFP ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K implies for y being Element of AFP ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
assume that
A1: a,b // K and
A2: not a in K ; ::_thesis: for y being Element of AFP ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
let y be Element of AFP; ::_thesis: ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) )
A3: b,a // K by A1, AFF_1:34;
A4: not b in K by A1, A2, AFF_1:35;
then consider x being Element of AFP such that
A5: ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) by A3, Lm19;
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) by A3, A4, A5, Lm18;
hence ex x being Element of AFP st
( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ; ::_thesis: verum
end;
theorem Th7: :: HOMOTHET:7
for AFP being AffinPlane
for p, q, p9, q9, a, b, x, y being Element of AFP
for K, M being Subset of AFP st K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x holds
q,b // q9,y
proof
let AFP be AffinPlane; ::_thesis: for p, q, p9, q9, a, b, x, y being Element of AFP
for K, M being Subset of AFP st K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x holds
q,b // q9,y
let p, q, p9, q9, a, b, x, y be Element of AFP; ::_thesis: for K, M being Subset of AFP st K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x holds
q,b // q9,y
let K, M be Subset of AFP; ::_thesis: ( K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x implies q,b // q9,y )
assume that
A1: K // M and
A2: p in K and
A3: q in K and
A4: p9 in K and
A5: q9 in K and
A6: AFP is Moufangian and
A7: a in M and
A8: b in M and
A9: x in M and
A10: y in M and
A11: a <> b and
A12: q <> p and
A13: p,a // p9,x and
A14: p,b // p9,y and
A15: q,a // q9,x ; ::_thesis: q,b // q9,y
A16: K is being_line by A1, AFF_1:36;
A17: M is being_line by A1, AFF_1:36;
now__::_thesis:_(_K_<>_M_implies_q,b_//_q9,y_)
set D9 = Line (q9,x);
set B99 = Line (p9,y);
set D = Line (q,a);
set B9 = Line (p,b);
A18: q in Line (q,a) by AFF_1:15;
A19: a in Line (q,a) by AFF_1:15;
A20: x in Line (q9,x) by AFF_1:15;
A21: q9 in Line (q9,x) by AFF_1:15;
A22: LIN p,q,q9 by A2, A3, A5, A16, AFF_1:21;
A23: LIN p,q,p9 by A2, A3, A4, A16, AFF_1:21;
assume A24: K <> M ; ::_thesis: q,b // q9,y
then A25: q9 <> x by A1, A5, A9, AFF_1:45;
A26: not a in K by A1, A7, A24, AFF_1:45;
A27: b <> p by A1, A2, A8, A24, AFF_1:45;
then A28: Line (p,b) is being_line by AFF_1:def_3;
A29: not q in M by A1, A3, A24, AFF_1:45;
A30: not p in M by A1, A2, A24, AFF_1:45;
A31: LIN a,b,x by A7, A8, A9, A17, AFF_1:21;
A32: now__::_thesis:_(_(_for_a,_b,_c_being_Element_of_AFP_holds_
(_not_LIN_a,b,c_or_not_a_<>_b_or_not_a_<>_c_or_not_b_<>_c_)_)_implies_q,b_//_q9,y_)
A33: now__::_thesis:_(_q_=_p9_implies_not_q_=_q9_)
assume that
A34: q = p9 and
A35: q = q9 ; ::_thesis: contradiction
LIN q,a,x by A15, A35, AFF_1:def_1;
then LIN a,x,q by AFF_1:6;
then a = x by A7, A9, A17, A29, AFF_1:25;
then a,q // a,p by A13, A34, AFF_1:4;
then LIN a,q,p by AFF_1:def_1;
then LIN p,q,a by AFF_1:6;
hence contradiction by A2, A3, A12, A16, A26, AFF_1:25; ::_thesis: verum
end;
A36: now__::_thesis:_(_p_=_p9_implies_not_p_=_q9_)
assume that
A37: p = p9 and
A38: p = q9 ; ::_thesis: contradiction
LIN p,a,x by A13, A37, AFF_1:def_1;
then LIN a,x,p by AFF_1:6;
then a = x by A7, A9, A17, A30, AFF_1:25;
then a,q // a,q9 by A15, AFF_1:4;
then LIN a,q,q9 by AFF_1:def_1;
then LIN p,q,a by A38, AFF_1:6;
hence contradiction by A2, A3, A12, A16, A26, AFF_1:25; ::_thesis: verum
end;
assume A39: for a, b, c being Element of AFP holds
( not LIN a,b,c or not a <> b or not a <> c or not b <> c ) ; ::_thesis: q,b // q9,y
A40: now__::_thesis:_(_q_=_p9_&_p_=_q9_implies_q,b_//_q9,y_)
assume that
A41: q = p9 and
A42: p = q9 ; ::_thesis: q,b // q9,y
A43: now__::_thesis:_(_b_=_x_implies_q,b_//_q9,y_)
assume A44: b = x ; ::_thesis: q,b // q9,y
then q,y // q,a by A14, A15, A27, A41, A42, AFF_1:5;
then LIN q,y,a by AFF_1:def_1;
then LIN a,y,q by AFF_1:6;
then q9,y // q,b by A7, A10, A13, A17, A29, A41, A42, A44, AFF_1:25;
hence q,b // q9,y by AFF_1:4; ::_thesis: verum
end;
now__::_thesis:_not_a_=_x
assume a = x ; ::_thesis: contradiction
then a,p // a,q by A13, A41, AFF_1:4;
then LIN a,p,q by AFF_1:def_1;
then LIN p,q,a by AFF_1:6;
hence contradiction by A2, A3, A12, A16, A26, AFF_1:25; ::_thesis: verum
end;
hence q,b // q9,y by A11, A31, A39, A43; ::_thesis: verum
end;
now__::_thesis:_(_p_=_p9_&_q_=_q9_implies_q,b_//_q9,y_)
assume that
A45: p = p9 and
A46: q = q9 ; ::_thesis: q,b // q9,y
LIN p,b,y by A14, A45, AFF_1:def_1;
then LIN b,y,p by AFF_1:6;
then b = y by A8, A10, A17, A30, AFF_1:25;
hence q,b // q9,y by A46, AFF_1:2; ::_thesis: verum
end;
hence q,b // q9,y by A12, A23, A22, A39, A36, A33, A40; ::_thesis: verum
end;
A47: y in Line (p9,y) by AFF_1:15;
A48: p9 in Line (p9,y) by AFF_1:15;
A49: b in Line (p,b) by AFF_1:15;
then A50: Line (p,b) <> K by A1, A8, A24, AFF_1:45;
a <> q by A1, A3, A7, A24, AFF_1:45;
then A51: Line (q,a) // Line (q9,x) by A15, A25, AFF_1:37;
A52: p in Line (p,b) by AFF_1:15;
then A53: Line (p,b) <> M by A1, A2, A24, AFF_1:45;
A54: p9 <> y by A1, A4, A10, A24, AFF_1:45;
then A55: Line (p,b) // Line (p9,y) by A14, A27, AFF_1:37;
A56: Line (p9,y) is being_line by A54, AFF_1:def_3;
now__::_thesis:_(_ex_a,_b,_c_being_Element_of_AFP_st_
(_LIN_a,b,c_&_a_<>_b_&_a_<>_c_&_b_<>_c_)_implies_q,b_//_q9,y_)
A57: a,q // x,q9 by A18, A19, A21, A20, A51, AFF_1:39;
assume ex a, b, c being Element of AFP st
( LIN a,b,c & a <> b & a <> c & b <> c ) ; ::_thesis: q,b // q9,y
then consider d being Element of AFP such that
A58: LIN p,b,d and
A59: d <> p and
A60: d <> b by TRANSLAC:1;
consider N being Subset of AFP such that
A61: d in N and
A62: K // N by A16, AFF_1:49;
A63: d in Line (p,b) by A58, AFF_1:def_2;
then A64: N <> M by A8, A17, A28, A49, A53, A60, A61, AFF_1:18;
A65: not Line (p9,y) // N
proof
assume Line (p9,y) // N ; ::_thesis: contradiction
then Line (p,b) // N by A55, AFF_1:44;
then Line (p,b) // K by A62, AFF_1:44;
hence contradiction by A2, A52, A50, AFF_1:45; ::_thesis: verum
end;
N is being_line by A62, AFF_1:36;
then consider z being Element of AFP such that
A66: z in Line (p9,y) and
A67: z in N by A56, A65, AFF_1:58;
A68: d,b // z,y by A49, A47, A55, A63, A66, AFF_1:39;
A69: N <> K by A2, A16, A28, A52, A50, A59, A63, A61, AFF_1:18;
A70: M // N by A1, A62, AFF_1:44;
A71: K <> N by A2, A16, A28, A52, A50, A59, A63, A61, AFF_1:18;
A72: N // M by A1, A62, AFF_1:44;
p,d // p9,z by A52, A48, A55, A63, A66, AFF_1:39;
then A73: a,d // x,z by A1, A2, A4, A6, A7, A9, A13, A24, A61, A62, A67, A71, Lm4;
M <> N by A8, A17, A28, A49, A53, A60, A63, A61, AFF_1:18;
then d,q // z,q9 by A1, A3, A5, A6, A7, A9, A24, A61, A67, A73, A57, A70, Lm4;
hence q,b // q9,y by A3, A5, A6, A8, A10, A61, A62, A67, A68, A72, A64, A69, Lm4; ::_thesis: verum
end;
hence q,b // q9,y by A32; ::_thesis: verum
end;
hence q,b // q9,y by A1, A3, A5, A8, A10, AFF_1:39; ::_thesis: verum
end;
Lm21: for AFP being AffinPlane
for a, b, x, p, p9, y, q, q9 being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x holds
q,b // q9,y
proof
let AFP be AffinPlane; ::_thesis: for a, b, x, p, p9, y, q, q9 being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x holds
q,b // q9,y
let a, b, x, p, p9, y, q, q9 be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x holds
q,b // q9,y
let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x implies q,b // q9,y )
assume that
A1: a,b // K and
A2: not a in K and
A3: not x in K and
A4: AFP is Moufangian and
A5: p in K and
A6: p9 in K and
A7: p,a // p9,x and
A8: p,b // p9,y and
A9: x,y // K and
A10: q in K and
A11: q9 in K and
A12: q,a // q9,x ; ::_thesis: q,b // q9,y
A13: K is being_line by A1, AFF_1:26;
A14: now__::_thesis:_(_not_a,x_//_K_&_a_<>_b_implies_q,b_//_q9,y_)
A15: a,q // x,q9 by A12, AFF_1:4;
A16: b,p // y,p9 by A8, AFF_1:4;
A17: a,p // x,p9 by A7, AFF_1:4;
set A = Line (a,x);
assume that
A18: not a,x // K and
A19: a <> b ; ::_thesis: q,b // q9,y
a <> x by A13, A18, AFF_1:33;
then A20: Line (a,x) is being_line by AFF_1:def_3;
A21: x in Line (a,x) by AFF_1:15;
A22: a in Line (a,x) by AFF_1:15;
then consider o being Element of AFP such that
A23: o in Line (a,x) and
A24: o in K by A13, A18, A21, A20, AFF_1:40, AFF_1:58;
A25: LIN o,a,x by A22, A21, A20, A23, AFF_1:21;
K is being_line by A1, AFF_1:26;
then a,b // x,y by A1, A9, AFF_1:31;
then LIN o,b,y by A1, A2, A4, A5, A6, A19, A24, A25, A17, A16, Lm3, AFF_1:26;
then b,q // y,q9 by A1, A2, A4, A9, A10, A11, A13, A24, A25, A15, Lm2;
hence q,b // q9,y by AFF_1:4; ::_thesis: verum
end;
A26: now__::_thesis:_(_a,x_//_K_&_a_<>_b_&_p_<>_q_implies_q,b_//_q9,y_)
set M = Line (a,b);
assume that
A27: a,x // K and
A28: a <> b and
A29: p <> q ; ::_thesis: q,b // q9,y
A30: Line (a,b) is being_line by A28, AFF_1:def_3;
K is being_line by A1, AFF_1:26;
then a,b // a,x by A1, A27, AFF_1:31;
then LIN a,b,x by AFF_1:def_1;
then A31: x in Line (a,b) by AFF_1:def_2;
A32: b in Line (a,b) by AFF_1:15;
A33: a in Line (a,b) by AFF_1:15;
A34: Line (a,b) // K by A1, A28, AFF_1:def_5;
then x,y // Line (a,b) by A9, AFF_1:43;
then y in Line (a,b) by A30, A31, AFF_1:23;
hence q,b // q9,y by A4, A5, A6, A7, A8, A10, A11, A12, A28, A29, A33, A32, A34, A31, Th7; ::_thesis: verum
end;
A35: ( a = b implies x = y )
proof
set M = Line (x,y);
A36: x in Line (x,y) by AFF_1:15;
assume a = b ; ::_thesis: x = y
then p9,x // p9,y by A2, A5, A7, A8, AFF_1:5;
then LIN p9,x,y by AFF_1:def_1;
then LIN x,y,p9 by AFF_1:6;
then A37: p9 in Line (x,y) by AFF_1:def_2;
assume x <> y ; ::_thesis: contradiction
then Line (x,y) // K by A9, AFF_1:def_5;
hence contradiction by A3, A6, A36, A37, AFF_1:45; ::_thesis: verum
end;
now__::_thesis:_(_p_=_q_implies_q,b_//_q9,y_)
assume A38: p = q ; ::_thesis: q,b // q9,y
p9 = q9
proof
p9,x // q9,x by A2, A5, A7, A12, A38, AFF_1:5;
then x,p9 // x,q9 by AFF_1:4;
then LIN x,p9,q9 by AFF_1:def_1;
then A39: LIN p9,q9,x by AFF_1:6;
assume p9 <> q9 ; ::_thesis: contradiction
hence contradiction by A1, A3, A6, A11, A39, AFF_1:25, AFF_1:26; ::_thesis: verum
end;
hence q,b // q9,y by A8, A38; ::_thesis: verum
end;
hence q,b // q9,y by A12, A35, A14, A26; ::_thesis: verum
end;
Lm22: for AFP being AffinPlane
for a, b, x, p, p9, y, q, q9, s being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s holds
s = y
proof
let AFP be AffinPlane; ::_thesis: for a, b, x, p, p9, y, q, q9, s being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s holds
s = y
let a, b, x, p, p9, y, q, q9, s be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s holds
s = y
let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s implies s = y )
assume that
A1: a,b // K and
A2: not a in K and
A3: not x in K and
A4: AFP is Moufangian and
A5: p in K and
A6: p9 in K and
A7: p,a // p9,x and
A8: p,b // p9,y and
A9: x,y // K and
A10: q in K and
A11: q9 in K and
A12: q,a // q9,x and
A13: x,s // K and
A14: q,b // q9,s ; ::_thesis: s = y
A15: not b in K by A1, A2, AFF_1:35;
q,b // q9,y by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, Lm21;
then q9,s // q9,y by A10, A14, A15, AFF_1:5;
then LIN q9,s,y by AFF_1:def_1;
then A16: LIN y,s,q9 by AFF_1:6;
assume A17: not s = y ; ::_thesis: contradiction
K is being_line by A1, AFF_1:26;
then consider M being Subset of AFP such that
A18: x in M and
A19: K // M by AFF_1:49;
A20: M is being_line by A19, AFF_1:36;
x,s // M by A13, A19, AFF_1:43;
then A21: s in M by A18, A20, AFF_1:23;
x,y // M by A9, A19, AFF_1:43;
then y in M by A18, A20, AFF_1:23;
then M = Line (y,s) by A17, A20, A21, AFF_1:24;
then q9 in M by A16, AFF_1:def_2;
hence contradiction by A3, A11, A18, A19, AFF_1:45; ::_thesis: verum
end;
Lm23: for AFP being AffinPlane
for a, b, x, y, r being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) holds
x = r
proof
let AFP be AffinPlane; ::_thesis: for a, b, x, y, r being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) holds
x = r
let a, b, x, y, r be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) holds
x = r
let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) implies x = r )
assume that
A1: a,b // K and
A2: not a in K and
A3: AFP is Moufangian and
A4: ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) and
A5: ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) ; ::_thesis: x = r
A6: ( ( y in K & y = r ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,r & y,r // K ) ) ) by A1, A2, A5, Lm18;
A7: b,a // K by A1, AFF_1:34;
A8: not b in K by A1, A2, AFF_1:35;
( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) by A1, A2, A4, Lm18;
hence x = r by A3, A7, A8, A6, Lm22; ::_thesis: verum
end;
Lm24: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
proof
let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
let a, b be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & AFP is Moufangian implies ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) )
defpred S1[ Element of AFP, Element of AFP] means ( ( $1 in K & $1 = $2 ) or ( not $1 in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,$1 & p,b // p9,$2 & $1,$2 // K ) ) );
assume that
A1: a,b // K and
A2: not a in K and
A3: AFP is Moufangian ; ::_thesis: ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) )
A4: for x, y, s being Element of AFP st S1[x,y] & S1[x,s] holds
y = s by A1, A2, A3, Lm22;
A5: for y being Element of AFP ex x being Element of AFP st S1[x,y] by A1, A2, Lm20;
A6: for x being Element of AFP ex y being Element of AFP st S1[x,y] by A1, A2, Lm19;
A7: for x, y, r being Element of AFP st S1[x,y] & S1[r,y] holds
x = r by A1, A2, A3, Lm23;
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff S1[x,y] ) from TRANSGEO:sch_1(A6, A5, A7, A4);
hence ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; ::_thesis: verum
end;
Lm25: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f . a = b
proof
let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f . a = b
let a, b be Element of AFP; ::_thesis: for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f . a = b
let K be Subset of AFP; ::_thesis: for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f . a = b
let f be Permutation of the carrier of AFP; ::_thesis: ( a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) implies f . a = b )
assume that
A1: a,b // K and
A2: not a in K ; ::_thesis: ( ex x, y being Element of AFP st
( ( not f . x = y or ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) implies ( ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & not f . x = y ) ) or f . a = b )
consider p, q being Element of AFP such that
A3: p in K and
q in K and
p <> q by A1, AFF_1:19, AFF_1:26;
A4: p,b // p,b by AFF_1:2;
assume A5: for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; ::_thesis: f . a = b
p,a // p,a by AFF_1:2;
hence f . a = b by A1, A2, A5, A3, A4; ::_thesis: verum
end;
Lm26: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
for x being Element of AFP holds x,f . x // K
proof
let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
for x being Element of AFP holds x,f . x // K
let a, b be Element of AFP; ::_thesis: for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
for x being Element of AFP holds x,f . x // K
let K be Subset of AFP; ::_thesis: for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
for x being Element of AFP holds x,f . x // K
let f be Permutation of the carrier of AFP; ::_thesis: ( a,b // K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) implies for x being Element of AFP holds x,f . x // K )
assume that
A1: a,b // K and
A2: for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; ::_thesis: for x being Element of AFP holds x,f . x // K
let x be Element of AFP; ::_thesis: x,f . x // K
set y = f . x;
A3: K is being_line by A1, AFF_1:26;
A4: now__::_thesis:_(_x_in_K_implies_x,f_._x_//_K_)
assume x in K ; ::_thesis: x,f . x // K
then f . x = x by A2;
hence x,f . x // K by A3, AFF_1:33; ::_thesis: verum
end;
now__::_thesis:_(_not_x_in_K_implies_x,f_._x_//_K_)
assume not x in K ; ::_thesis: x,f . x // K
then ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,f . x & x,f . x // K ) by A2;
hence x,f . x // K ; ::_thesis: verum
end;
hence x,f . x // K by A4; ::_thesis: verum
end;
Lm27: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f is collineation
proof
let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f is collineation
let a, b be Element of AFP; ::_thesis: for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f is collineation
let K be Subset of AFP; ::_thesis: for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f is collineation
let f be Permutation of the carrier of AFP; ::_thesis: ( a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) implies f is collineation )
assume that
A1: a,b // K and
A2: not a in K and
A3: for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; ::_thesis: f is collineation
A4: K is being_line by A1, AFF_1:26;
A5: not b in K by A1, A2, AFF_1:35;
for A being Subset of AFP st A is being_line holds
f .: A is being_line
proof
let A be Subset of AFP; ::_thesis: ( A is being_line implies f .: A is being_line )
assume A6: A is being_line ; ::_thesis: f .: A is being_line
set B9 = f .: A;
A7: now__::_thesis:_(_A_//_K_&_A_<>_K_implies_f_.:_A_is_being_line_)
assume that
A8: A // K and
A9: A <> K ; ::_thesis: f .: A is being_line
now__::_thesis:_for_x_being_Element_of_AFP_st_x_in_A_holds_
x_in_f_.:_A
let x be Element of AFP; ::_thesis: ( x in A implies x in f .: A )
assume A10: x in A ; ::_thesis: x in f .: A
consider y being Element of AFP such that
A11: f . y = x by TRANSGEO:1;
( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,y & p,b // p9,x & y,x // K ) ) ) by A3, A11;
then x,y // K by A8, A9, A10, AFF_1:34, AFF_1:45;
then x,y // A by A8, AFF_1:43;
then y in A by A6, A10, AFF_1:23;
hence x in f .: A by A11, TRANSGEO:87; ::_thesis: verum
end;
then A12: A c= f .: A by SUBSET_1:2;
now__::_thesis:_for_y_being_Element_of_AFP_st_y_in_f_.:_A_holds_
y_in_A
let y be Element of AFP; ::_thesis: ( y in f .: A implies y in A )
assume y in f .: A ; ::_thesis: y in A
then consider x being Element of AFP such that
A13: x in A and
A14: y = f . x by TRANSGEO:87;
not x in K by A8, A9, A13, AFF_1:45;
then ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) by A3, A14;
then x,y // A by A8, AFF_1:43;
hence y in A by A6, A13, AFF_1:23; ::_thesis: verum
end;
then f .: A c= A by SUBSET_1:2;
hence f .: A is being_line by A6, A12, XBOOLE_0:def_10; ::_thesis: verum
end;
A15: now__::_thesis:_(_not_A_//_K_&_A_<>_K_implies_f_.:_A_is_being_line_)
K is being_line by A1, AFF_1:26;
then consider M being Subset of AFP such that
A16: a in M and
A17: K // M by AFF_1:49;
A18: M is being_line by A17, AFF_1:36;
consider A9 being Subset of AFP such that
A19: a in A9 and
A20: A // A9 by A6, AFF_1:49;
A21: A9 is being_line by A20, AFF_1:36;
assume that
A22: not A // K and
A23: A <> K ; ::_thesis: f .: A is being_line
consider p being Element of AFP such that
A24: p in A and
A25: p in K by A4, A6, A22, AFF_1:58;
not A9 // K by A22, A20, AFF_1:44;
then consider q being Element of AFP such that
A26: q in A9 and
A27: q in K by A4, A21, AFF_1:58;
set C9 = Line (q,b);
A28: q in Line (q,b) by AFF_1:15;
a,b // M by A1, A17, AFF_1:43;
then b in M by A16, A18, AFF_1:23;
then q <> b by A2, A16, A17, A27, AFF_1:45;
then Line (q,b) is being_line by AFF_1:def_3;
then consider C being Subset of AFP such that
A29: p in C and
A30: Line (q,b) // C by AFF_1:49;
A31: b in Line (q,b) by AFF_1:15;
A32: C is being_line by A30, AFF_1:36;
now__::_thesis:_for_y_being_Element_of_AFP_st_y_in_C_holds_
y_in_f_.:_A
let y be Element of AFP; ::_thesis: ( y in C implies y in f .: A )
assume A33: y in C ; ::_thesis: y in f .: A
A34: now__::_thesis:_(_y_<>_p_implies_y_in_f_.:_A_)
A35: q,b // p,y by A28, A31, A29, A30, A33, AFF_1:39;
K is being_line by A1, AFF_1:26;
then consider N being Subset of AFP such that
A36: y in N and
A37: K // N by AFF_1:49;
A38: N is being_line by A37, AFF_1:36;
not N // A by A22, A37, AFF_1:44;
then consider x being Element of AFP such that
A39: x in N and
A40: x in A by A6, A38, AFF_1:58;
A41: x,y // K by A36, A37, A39, AFF_1:40;
assume A42: y <> p ; ::_thesis: y in f .: A
A43: not x in K
proof
assume x in K ; ::_thesis: contradiction
then y in K by A36, A37, A39, AFF_1:45;
then Line (q,b) // K by A4, A25, A29, A30, A32, A33, A42, AFF_1:18;
hence contradiction by A5, A27, A28, A31, AFF_1:45; ::_thesis: verum
end;
q,a // p,x by A24, A19, A20, A26, A40, AFF_1:39;
then y = f . x by A3, A25, A27, A43, A35, A41;
hence y in f .: A by A40, TRANSGEO:87; ::_thesis: verum
end;
now__::_thesis:_(_y_=_p_implies_y_in_f_.:_A_)
assume A44: y = p ; ::_thesis: y in f .: A
f . p = p by A3, A25;
hence y in f .: A by A24, A44, TRANSGEO:87; ::_thesis: verum
end;
hence y in f .: A by A34; ::_thesis: verum
end;
then A45: C c= f .: A by SUBSET_1:2;
now__::_thesis:_for_y_being_Element_of_AFP_st_y_in_f_.:_A_holds_
y_in_C
let y be Element of AFP; ::_thesis: ( y in f .: A implies y in C )
assume y in f .: A ; ::_thesis: y in C
then consider x being Element of AFP such that
A46: x in A and
A47: y = f . x by TRANSGEO:87;
now__::_thesis:_(_x_<>_p_implies_y_in_C_)
K is being_line by A1, AFF_1:26;
then consider N being Subset of AFP such that
A48: x in N and
A49: K // N by AFF_1:49;
A50: not C // N
proof
assume C // N ; ::_thesis: contradiction
then Line (q,b) // N by A30, AFF_1:44;
then A51: Line (q,b) // K by A49, AFF_1:44;
q in Line (q,b) by AFF_1:15;
then Line (q,b) = K by A27, A51, AFF_1:45;
hence contradiction by A5, AFF_1:15; ::_thesis: verum
end;
N is being_line by A49, AFF_1:36;
then consider z being Element of AFP such that
A52: z in C and
A53: z in N by A32, A50, AFF_1:58;
A54: x,z // K by A48, A49, A53, AFF_1:40;
assume x <> p ; ::_thesis: y in C
then A55: not x in K by A4, A6, A23, A24, A25, A46, AFF_1:18;
A56: q,a // p,x by A24, A19, A20, A26, A46, AFF_1:39;
q,b // p,z by A28, A31, A29, A30, A52, AFF_1:39;
hence y in C by A3, A25, A27, A47, A55, A52, A56, A54; ::_thesis: verum
end;
hence y in C by A3, A25, A29, A47; ::_thesis: verum
end;
then f .: A c= C by SUBSET_1:2;
hence f .: A is being_line by A32, A45, XBOOLE_0:def_10; ::_thesis: verum
end;
now__::_thesis:_(_A_=_K_implies_f_.:_A_is_being_line_)
assume A57: A = K ; ::_thesis: f .: A is being_line
now__::_thesis:_for_y_being_Element_of_AFP_st_y_in_f_.:_A_holds_
y_in_A
let y be Element of AFP; ::_thesis: ( y in f .: A implies y in A )
assume y in f .: A ; ::_thesis: y in A
then ex x being Element of AFP st
( x in A & y = f . x ) by TRANSGEO:87;
hence y in A by A3, A57; ::_thesis: verum
end;
then A58: f .: A c= A by SUBSET_1:2;
now__::_thesis:_for_x_being_Element_of_AFP_st_x_in_A_holds_
x_in_f_.:_A
let x be Element of AFP; ::_thesis: ( x in A implies x in f .: A )
assume A59: x in A ; ::_thesis: x in f .: A
set y = f . x;
f . x in f .: A by A59, TRANSGEO:86;
hence x in f .: A by A3, A57, A59; ::_thesis: verum
end;
then A c= f .: A by SUBSET_1:2;
hence f .: A is being_line by A6, A58, XBOOLE_0:def_10; ::_thesis: verum
end;
hence f .: A is being_line by A7, A15; ::_thesis: verum
end;
hence f is collineation by TRANSGEO:92; ::_thesis: verum
end;
Lm28: for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f is_Sc K
proof
let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f is_Sc K
let a, b be Element of AFP; ::_thesis: for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f is_Sc K
let K be Subset of AFP; ::_thesis: for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
f is_Sc K
let f be Permutation of the carrier of AFP; ::_thesis: ( a,b // K & not a in K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) implies f is_Sc K )
assume that
A1: a,b // K and
A2: not a in K and
A3: for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; ::_thesis: f is_Sc K
A4: for x being Element of AFP holds x,f . x // K by A1, A3, Lm26;
A5: for x being Element of AFP st x in K holds
f . x = x by A3;
A6: K is being_line by A1, AFF_1:26;
f is collineation by A1, A2, A3, Lm27;
hence f is_Sc K by A6, A5, A4, Def1; ::_thesis: verum
end;
theorem Th8: :: HOMOTHET:8
for AFP being AffinPlane
for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b )
proof
let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b )
let a, b be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b )
let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & AFP is Moufangian implies ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) )
assume that
A1: a,b // K and
A2: not a in K and
A3: AFP is Moufangian ; ::_thesis: ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b )
consider f being Permutation of the carrier of AFP such that
A4: for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) by A1, A2, A3, Lm24;
A5: f . a = b by A1, A2, A4, Lm25;
f is_Sc K by A1, A2, A4, Lm28;
hence ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) by A5; ::_thesis: verum
end;
theorem :: HOMOTHET:9
for AFP being AffinPlane holds
( AFP is Moufangian iff for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) ) by Th6, Th8;