:: PROJRED1 semantic presentation
begin
theorem Th1: :: PROJRED1:1
for IPP being IncProjSp
for A being LINE of IPP holds
not for a being POINT of IPP holds a on A
proof
let IPP be IncProjSp; ::_thesis: for A being LINE of IPP holds
not for a being POINT of IPP holds a on A
let A be LINE of IPP; ::_thesis: not for a being POINT of IPP holds a on A
consider p being POINT of IPP, L being LINE of IPP such that
A1: not p on L by INCPROJ:def_6;
now__::_thesis:_(_A_<>_L_implies_ex_a_being_POINT_of_IPP_st_not_a_on_A_)
assume A2: A <> L ; ::_thesis: not for a being POINT of IPP holds a on A
now__::_thesis:_not_for_a_being_POINT_of_IPP_holds_a_on_A
consider q, r, s being POINT of IPP such that
A3: q <> r and
r <> s and
s <> q and
A4: ( q on L & r on L ) and
s on L by INCPROJ:def_7;
( not q on A or not r on A ) by A2, A3, A4, INCPROJ:def_4;
hence not for a being POINT of IPP holds a on A ; ::_thesis: verum
end;
hence not for a being POINT of IPP holds a on A ; ::_thesis: verum
end;
hence not for a being POINT of IPP holds a on A by A1; ::_thesis: verum
end;
theorem Th2: :: PROJRED1:2
for IPP being IncProjSp
for a being POINT of IPP holds
not for A being LINE of IPP holds a on A
proof
let IPP be IncProjSp; ::_thesis: for a being POINT of IPP holds
not for A being LINE of IPP holds a on A
let a be POINT of IPP; ::_thesis: not for A being LINE of IPP holds a on A
consider p being POINT of IPP, L being LINE of IPP such that
A1: not p on L by INCPROJ:def_6;
now__::_thesis:_not_for_A_being_LINE_of_IPP_holds_a_on_A
now__::_thesis:_(_a_on_L_implies_ex_A_being_LINE_of_IPP_st_not_a_on_A_)
consider q, r, s being POINT of IPP such that
q <> r and
r <> s and
A2: s <> q and
A3: q on L and
r on L and
A4: s on L by INCPROJ:def_7;
assume A5: a on L ; ::_thesis: not for A being LINE of IPP holds a on A
A6: now__::_thesis:_(_a_<>_s_implies_ex_A_being_LINE_of_IPP_st_not_a_on_A_)
consider S being LINE of IPP such that
A7: ( s on S & p on S ) by INCPROJ:def_5;
assume a <> s ; ::_thesis: not for A being LINE of IPP holds a on A
then not a on S by A1, A5, A4, A7, INCPROJ:def_4;
hence not for A being LINE of IPP holds a on A ; ::_thesis: verum
end;
now__::_thesis:_(_a_<>_q_implies_ex_A_being_LINE_of_IPP_st_not_a_on_A_)
consider S being LINE of IPP such that
A8: ( q on S & p on S ) by INCPROJ:def_5;
assume a <> q ; ::_thesis: not for A being LINE of IPP holds a on A
then not a on S by A1, A5, A3, A8, INCPROJ:def_4;
hence not for A being LINE of IPP holds a on A ; ::_thesis: verum
end;
hence not for A being LINE of IPP holds a on A by A2, A6; ::_thesis: verum
end;
hence not for A being LINE of IPP holds a on A ; ::_thesis: verum
end;
hence not for A being LINE of IPP holds a on A ; ::_thesis: verum
end;
theorem Th3: :: PROJRED1:3
for IPP being IncProjSp
for A, B being LINE of IPP st A <> B holds
ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A )
proof
let IPP be IncProjSp; ::_thesis: for A, B being LINE of IPP st A <> B holds
ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A )
let A, B be LINE of IPP; ::_thesis: ( A <> B implies ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A ) )
consider a, b, d being POINT of IPP such that
A1: a <> b and
b <> d and
d <> a and
A2: ( a on A & b on A ) and
d on A by INCPROJ:def_7;
consider r, s, t being POINT of IPP such that
A3: r <> s and
s <> t and
t <> r and
A4: ( r on B & s on B ) and
t on B by INCPROJ:def_7;
assume A5: A <> B ; ::_thesis: ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A )
then A6: ( not r on A or not s on A ) by A3, A4, INCPROJ:def_4;
( not a on B or not b on B ) by A5, A1, A2, INCPROJ:def_4;
hence ex a, b being POINT of IPP st
( a on A & not a on B & b on B & not b on A ) by A2, A4, A6; ::_thesis: verum
end;
theorem :: PROJRED1:4
for IPP being IncProjSp
for a, b being POINT of IPP st a <> b holds
ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A )
proof
let IPP be IncProjSp; ::_thesis: for a, b being POINT of IPP st a <> b holds
ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A )
let a, b be POINT of IPP; ::_thesis: ( a <> b implies ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A ) )
consider Q being LINE of IPP such that
A1: ( a on Q & b on Q ) by INCPROJ:def_5;
consider q being POINT of IPP such that
A2: not q on Q by Th1;
consider B being LINE of IPP such that
A3: b on B and
A4: q on B by INCPROJ:def_5;
assume A5: a <> b ; ::_thesis: ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A )
then A6: not a on B by A1, A2, A3, A4, INCPROJ:def_4;
consider A being LINE of IPP such that
A7: a on A and
A8: q on A by INCPROJ:def_5;
not b on A by A5, A1, A2, A7, A8, INCPROJ:def_4;
hence ex A, B being LINE of IPP st
( a on A & not a on B & b on B & not b on A ) by A7, A3, A6; ::_thesis: verum
end;
theorem :: PROJRED1:5
for IPP being IncProjSp
for a being POINT of IPP ex A, B, C being LINE of IPP st
( a on A & a on B & a on C & A <> B & B <> C & C <> A )
proof
let IPP be IncProjSp; ::_thesis: for a being POINT of IPP ex A, B, C being LINE of IPP st
( a on A & a on B & a on C & A <> B & B <> C & C <> A )
let a be POINT of IPP; ::_thesis: ex A, B, C being LINE of IPP st
( a on A & a on B & a on C & A <> B & B <> C & C <> A )
consider Q being LINE of IPP such that
A1: not a on Q by Th2;
consider b1, b2, b3 being Element of the Points of IPP such that
A2: b1 <> b2 and
A3: b2 <> b3 and
A4: b3 <> b1 and
A5: b1 on Q and
A6: b2 on Q and
A7: b3 on Q by INCPROJ:def_7;
consider B1 being LINE of IPP such that
A8: ( a on B1 & b1 on B1 ) by INCPROJ:def_5;
A9: not b3 on B1 by A1, A4, A5, A7, A8, INCPROJ:def_4;
consider B2 being LINE of IPP such that
A10: ( a on B2 & b2 on B2 ) by INCPROJ:def_5;
consider B3 being Element of the Lines of IPP such that
A11: ( a on B3 & b3 on B3 ) by INCPROJ:def_5;
A12: not b2 on B3 by A1, A3, A6, A7, A11, INCPROJ:def_4;
not b1 on B2 by A1, A2, A5, A6, A10, INCPROJ:def_4;
hence ex A, B, C being LINE of IPP st
( a on A & a on B & a on C & A <> B & B <> C & C <> A ) by A8, A10, A11, A12, A9; ::_thesis: verum
end;
theorem :: PROJRED1:6
for IPP being IncProjSp
for A, B being LINE of IPP ex a being POINT of IPP st
( not a on A & not a on B )
proof
let IPP be IncProjSp; ::_thesis: for A, B being LINE of IPP ex a being POINT of IPP st
( not a on A & not a on B )
let A, B be LINE of IPP; ::_thesis: ex a being POINT of IPP st
( not a on A & not a on B )
A1: ( A <> B implies ex a being POINT of IPP st
( not a on A & not a on B ) )
proof
assume A <> B ; ::_thesis: ex a being POINT of IPP st
( not a on A & not a on B )
then consider a, b being POINT of IPP such that
a on A and
A2: not a on B and
b on B and
A3: not b on A by Th3;
consider C being LINE of IPP such that
A4: ( a on C & b on C ) by INCPROJ:def_5;
consider c, d, e being Element of the Points of IPP such that
A5: ( c <> d & d <> e & e <> c & c on C & d on C & e on C ) by INCPROJ:def_7;
( ( not c on A & not c on B ) or ( not d on A & not d on B ) or ( not e on A & not e on B ) ) by A2, A3, A4, A5, INCPROJ:def_4;
hence ex a being POINT of IPP st
( not a on A & not a on B ) ; ::_thesis: verum
end;
( A = B implies ex a being POINT of IPP st
( not a on A & not a on B ) )
proof
assume A6: A = B ; ::_thesis: ex a being POINT of IPP st
( not a on A & not a on B )
not for a being POINT of IPP holds a on A by Th1;
hence ex a being POINT of IPP st
( not a on A & not a on B ) by A6; ::_thesis: verum
end;
hence ex a being POINT of IPP st
( not a on A & not a on B ) by A1; ::_thesis: verum
end;
theorem Th7: :: PROJRED1:7
for IPP being IncProjSp
for A being LINE of IPP ex a being POINT of IPP st a on A
proof
let IPP be IncProjSp; ::_thesis: for A being LINE of IPP ex a being POINT of IPP st a on A
let A be LINE of IPP; ::_thesis: ex a being POINT of IPP st a on A
consider a, b, c being POINT of IPP such that
a <> b and
b <> c and
c <> a and
A1: a on A and
b on A and
c on A by INCPROJ:def_7;
take a ; ::_thesis: a on A
thus a on A by A1; ::_thesis: verum
end;
theorem Th8: :: PROJRED1:8
for IPP being IncProjSp
for a, b being POINT of IPP
for A being LINE of IPP ex c being POINT of IPP st
( c on A & c <> a & c <> b )
proof
let IPP be IncProjSp; ::_thesis: for a, b being POINT of IPP
for A being LINE of IPP ex c being POINT of IPP st
( c on A & c <> a & c <> b )
let a, b be POINT of IPP; ::_thesis: for A being LINE of IPP ex c being POINT of IPP st
( c on A & c <> a & c <> b )
let A be LINE of IPP; ::_thesis: ex c being POINT of IPP st
( c on A & c <> a & c <> b )
consider p, q, r being POINT of IPP such that
A1: ( p <> q & q <> r & r <> p ) and
A2: ( p on A & q on A & r on A ) by INCPROJ:def_7;
( ( p <> a & p <> b ) or ( q <> a & q <> b ) or ( r <> a & r <> b ) ) by A1;
hence ex c being POINT of IPP st
( c on A & c <> a & c <> b ) by A2; ::_thesis: verum
end;
theorem :: PROJRED1:9
for IPP being IncProjSp
for a, b being POINT of IPP ex A being LINE of IPP st
( not a on A & not b on A )
proof
let IPP be IncProjSp; ::_thesis: for a, b being POINT of IPP ex A being LINE of IPP st
( not a on A & not b on A )
let a, b be POINT of IPP; ::_thesis: ex A being LINE of IPP st
( not a on A & not b on A )
now__::_thesis:_ex_A_being_LINE_of_IPP_st_
(_not_a_on_A_&_not_b_on_A_)
consider A being LINE of IPP such that
A1: ( a on A & b on A ) by INCPROJ:def_5;
consider c being POINT of IPP such that
A2: ( c on A & c <> a & c <> b ) by Th8;
consider d being POINT of IPP such that
A3: not d on A by Th1;
consider B being LINE of IPP such that
A4: ( d on B & c on B ) by INCPROJ:def_5;
( not a on B & not b on B ) by A1, A2, A3, A4, INCPROJ:def_4;
hence ex A being LINE of IPP st
( not a on A & not b on A ) ; ::_thesis: verum
end;
hence ex A being LINE of IPP st
( not a on A & not b on A ) ; ::_thesis: verum
end;
theorem Th10: :: PROJRED1:10
for IPP being IncProjSp
for o, a, b, c being POINT of IPP
for A, B, P, Q being LINE of IPP st o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q holds
P <> Q
proof
let IPP be IncProjSp; ::_thesis: for o, a, b, c being POINT of IPP
for A, B, P, Q being LINE of IPP st o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q holds
P <> Q
let o, a, b, c be POINT of IPP; ::_thesis: for A, B, P, Q being LINE of IPP st o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q holds
P <> Q
let A, B, P, Q be LINE of IPP; ::_thesis: ( o on A & o on B & A <> B & a on A & o <> a & b on B & c on B & b <> c & a on P & b on P & c on Q implies P <> Q )
assume that
A1: ( o on A & o on B & A <> B & a on A & o <> a ) and
A2: ( b on B & c on B & b <> c ) and
A3: a on P and
A4: ( b on P & c on Q ) ; ::_thesis: P <> Q
assume not P <> Q ; ::_thesis: contradiction
then P = B by A2, A4, INCPROJ:def_4;
hence contradiction by A1, A3, INCPROJ:def_4; ::_thesis: verum
end;
theorem Th11: :: PROJRED1:11
for IPP being IncProjSp
for a, b, c being POINT of IPP
for A being LINE of IPP st {a,b,c} on A holds
( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A )
proof
let IPP be IncProjSp; ::_thesis: for a, b, c being POINT of IPP
for A being LINE of IPP st {a,b,c} on A holds
( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A )
let a, b, c be POINT of IPP; ::_thesis: for A being LINE of IPP st {a,b,c} on A holds
( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A )
let A be LINE of IPP; ::_thesis: ( {a,b,c} on A implies ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A ) )
assume A1: {a,b,c} on A ; ::_thesis: ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A )
then A2: c on A by INCSP_1:2;
( a on A & b on A ) by A1, INCSP_1:2;
hence ( {a,c,b} on A & {b,a,c} on A & {b,c,a} on A & {c,a,b} on A & {c,b,a} on A ) by A2, INCSP_1:2; ::_thesis: verum
end;
theorem Th12: :: PROJRED1:12
for IPP being Desarguesian IncProjSp
for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of IPP
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IPP st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 holds
ex O being LINE of IPP st {r,s,t} on O
proof
let IPP be Desarguesian IncProjSp; ::_thesis: for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of IPP
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IPP st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 holds
ex O being LINE of IPP st {r,s,t} on O
let o, b1, a1, b2, a2, b3, a3, r, s, t be POINT of IPP; ::_thesis: for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IPP st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 holds
ex O being LINE of IPP st {r,s,t} on O
let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of IPP; ::_thesis: ( {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a3 & o <> b1 & o <> b2 & a2 <> b2 implies ex O being LINE of IPP st {r,s,t} on O )
assume that
A1: {o,b1,a1} on C1 and
A2: {o,a2,b2} on C2 and
A3: {o,a3,b3} on C3 and
A4: {a3,a2,t} on A1 and
A5: {a3,r,a1} on A2 and
A6: {a2,s,a1} on A3 and
A7: {t,b2,b3} on B1 and
A8: {b1,r,b3} on B2 and
A9: {b1,s,b2} on B3 and
A10: C1,C2,C3 are_mutually_different and
A11: o <> a3 and
A12: o <> b1 and
A13: o <> b2 and
A14: a2 <> b2 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
A15: ( r on A2 & r on B2 ) by A5, A8, INCSP_1:2;
A16: s on B3 by A9, INCSP_1:2;
A17: a3 on A1 by A4, INCSP_1:2;
A18: b3 on B1 by A7, INCSP_1:2;
A19: b2 on B1 by A7, INCSP_1:2;
A20: b3 on C3 by A3, INCSP_1:2;
A21: a1 on C1 by A1, INCSP_1:2;
A22: o on C2 by A2, INCSP_1:2;
A23: s on A3 by A6, INCSP_1:2;
A24: a1 on A3 by A6, INCSP_1:2;
A25: a1 on A2 by A5, INCSP_1:2;
A26: t on A1 by A4, INCSP_1:2;
A27: b1 on B2 by A8, INCSP_1:2;
A28: t on B1 by A7, INCSP_1:2;
A29: b1 on B3 by A9, INCSP_1:2;
A30: now__::_thesis:_(_o_<>_b3_&_o_<>_a1_&_o_<>_a2_&_a1_=_b1_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
assume that
o <> b3 and
o <> a1 and
o <> a2 and
A31: a1 = b1 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
A32: now__::_thesis:_(_a3_<>_b3_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
A33: b3 on B2 by A8, INCSP_1:2;
consider O being LINE of IPP such that
A34: ( t on O & s on O ) by INCPROJ:def_5;
assume A35: a3 <> b3 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
take O = O; ::_thesis: {r,s,t} on O
A36: ( b2 on C2 & o on C2 ) by A2, INCSP_1:2;
A37: ( o on C1 & a2 on C2 ) by A1, A2, INCSP_1:2;
A38: ( b1 on B3 & b2 on B3 ) by A9, INCSP_1:2;
A39: ( b1 on A2 & a3 on A2 ) by A5, A31, INCSP_1:2;
A40: ( a3 on C3 & b3 on C3 ) by A3, INCSP_1:2;
A41: ( o on C1 & o on C3 ) by A1, A3, INCSP_1:2;
A42: a2 on A3 by A6, INCSP_1:2;
( C1 <> C2 & b1 on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5;
then A3 <> B3 by A12, A14, A37, A36, A38, A42, Th10;
then A43: b1 = s by A23, A24, A29, A16, A31, INCPROJ:def_4;
( C1 <> C3 & b1 on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5;
then A2 <> B2 by A12, A35, A41, A40, A39, A33, Th10;
then s = r by A25, A27, A15, A31, A43, INCPROJ:def_4;
hence {r,s,t} on O by A34, INCSP_1:2; ::_thesis: verum
end;
now__::_thesis:_(_a3_=_b3_implies_ex_B2_being_LINE_of_IPP_st_{r,s,t}_on_B2_)
A44: ( a2 on A3 & b1 on A3 ) by A6, A31, INCSP_1:2;
A45: ( C2 <> C3 & o on C2 ) by A2, A10, INCSP_1:2, ZFMISC_1:def_5;
A46: ( a2 on C2 & b2 on C2 ) by A2, INCSP_1:2;
A47: ( o on C1 & a2 on C2 ) by A1, A2, INCSP_1:2;
A48: b2 on B3 by A9, INCSP_1:2;
A49: ( a2 on A1 & b2 on B1 ) by A4, A7, INCSP_1:2;
A50: ( o on C3 & b3 on C3 ) by A3, INCSP_1:2;
assume A51: a3 = b3 ; ::_thesis: ex B2 being LINE of IPP st {r,s,t} on B2
then b3 on A1 by A4, INCSP_1:2;
then A1 <> B1 by A11, A14, A51, A45, A46, A50, A49, Th10;
then A52: t = b3 by A17, A26, A28, A18, A51, INCPROJ:def_4;
take B2 = B2; ::_thesis: {r,s,t} on B2
A53: ( b2 on C2 & o on C2 ) by A2, INCSP_1:2;
( C1 <> C2 & b1 on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5;
then A3 <> B3 by A12, A14, A47, A53, A44, A48, Th10;
then {s,r,t} on B2 by A8, A23, A24, A29, A16, A31, A52, INCPROJ:def_4;
hence {r,s,t} on B2 by Th11; ::_thesis: verum
end;
hence ex O being LINE of IPP st {r,s,t} on O by A32; ::_thesis: verum
end;
A54: o on C1 by A1, INCSP_1:2;
A55: C1 <> C2 by A10, ZFMISC_1:def_5;
A56: b1 on C1 by A1, INCSP_1:2;
A57: a2 on A3 by A6, INCSP_1:2;
A58: b2 on C2 by A2, INCSP_1:2;
A59: C2 <> C3 by A10, ZFMISC_1:def_5;
A60: a3 on C3 by A3, INCSP_1:2;
A61: b3 on B2 by A8, INCSP_1:2;
A62: a3 on A2 by A5, INCSP_1:2;
A63: a2 on A1 by A4, INCSP_1:2;
A64: o on C3 by A3, INCSP_1:2;
A65: b2 on B3 by A9, INCSP_1:2;
A66: now__::_thesis:_(_o_<>_b3_&_o_<>_a1_&_o_=_a2_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
assume that
A67: o <> b3 and
A68: o <> a1 and
A69: o = a2 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
A70: now__::_thesis:_(_a1_=_b1_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
assume A71: a1 = b1 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
A72: now__::_thesis:_(_a3_=_b3_implies_ex_B2_being_LINE_of_IPP_st_{r,s,t}_on_B2_)
A73: ( a2 on A1 & b2 on B1 ) by A4, A7, INCSP_1:2;
A74: ( b2 on C2 & b3 on C3 ) by A2, A3, INCSP_1:2;
A75: ( b2 on C2 & a2 on A3 ) by A2, A6, INCSP_1:2;
A76: ( o on C2 & b1 on C1 ) by A1, A2, INCSP_1:2;
A77: ( C1 <> C2 & o on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5;
assume A78: a3 = b3 ; ::_thesis: ex B2 being LINE of IPP st {r,s,t} on B2
take B2 = B2; ::_thesis: {r,s,t} on B2
A79: b2 on B3 by A9, INCSP_1:2;
( b1 on A3 & a2 on C2 ) by A2, A6, A71, INCSP_1:2;
then A3 <> B3 by A12, A14, A77, A76, A75, A79, Th10;
then A80: s = b1 by A23, A24, A29, A16, A71, INCPROJ:def_4;
A81: ( o on C3 & a2 on C2 ) by A2, A3, INCSP_1:2;
A82: ( C2 <> C3 & o on C2 ) by A2, A10, INCSP_1:2, ZFMISC_1:def_5;
b3 on A1 by A4, A78, INCSP_1:2;
then A1 <> B1 by A11, A14, A78, A82, A81, A74, A73, Th10;
then {s,r,t} on B2 by A8, A17, A26, A28, A18, A78, A80, INCPROJ:def_4;
hence {r,s,t} on B2 by Th11; ::_thesis: verum
end;
now__::_thesis:_(_a3_<>_b3_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
A83: ( o on C3 & a1 on C1 ) by A1, A3, INCSP_1:2;
A84: ( a1 on A2 & a3 on A2 ) by A5, INCSP_1:2;
A85: b3 on B2 by A8, INCSP_1:2;
consider O being LINE of IPP such that
A86: ( t on O & s on O ) by INCPROJ:def_5;
assume A87: a3 <> b3 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
take O = O; ::_thesis: {r,s,t} on O
A88: ( a3 on C3 & b3 on C3 ) by A3, INCSP_1:2;
( C1 <> C3 & o on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5;
then A2 <> B2 by A12, A71, A87, A83, A88, A84, A85, Th10;
then A89: r = b1 by A25, A27, A15, A71, INCPROJ:def_4;
( A3 = C1 & B3 <> C1 ) by A13, A54, A21, A22, A58, A57, A24, A65, A55, A68, A69, INCPROJ:def_4;
then r = s by A23, A24, A29, A16, A71, A89, INCPROJ:def_4;
hence {r,s,t} on O by A86, INCSP_1:2; ::_thesis: verum
end;
hence ex O being LINE of IPP st {r,s,t} on O by A72; ::_thesis: verum
end;
now__::_thesis:_(_a1_<>_b1_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
assume A90: a1 <> b1 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
A91: now__::_thesis:_(_a3_=_b3_implies_ex_O_being_Element_of_the_Lines_of_IPP_st_{r,s,t}_on_O_)
A92: B1 <> C3 by A13, A22, A58, A64, A19, A59, INCPROJ:def_4;
A93: ( o on C3 & a1 on C1 ) by A1, A3, INCSP_1:2;
consider O being Element of the Lines of IPP such that
A94: ( t on O & s on O ) by INCPROJ:def_5;
A95: ( C1 <> C3 & o on C1 ) by A1, A10, INCSP_1:2, ZFMISC_1:def_5;
A96: ( a1 on A2 & b1 on B2 ) by A5, A8, INCSP_1:2;
A97: ( b1 on C1 & b3 on C3 ) by A1, A3, INCSP_1:2;
assume A98: a3 = b3 ; ::_thesis: ex O being Element of the Lines of IPP st {r,s,t} on O
then b3 on A2 by A5, INCSP_1:2;
then A2 <> B2 by A11, A90, A98, A95, A93, A97, A96, Th10;
then A99: r = b3 by A62, A15, A61, A98, INCPROJ:def_4;
take O = O; ::_thesis: {r,s,t} on O
A1 = C3 by A64, A60, A17, A63, A67, A69, A98, INCPROJ:def_4;
then r = t by A20, A26, A28, A18, A92, A99, INCPROJ:def_4;
hence {r,s,t} on O by A94, INCSP_1:2; ::_thesis: verum
end;
now__::_thesis:_(_a3_<>_b3_implies_ex_B2_being_LINE_of_IPP_st_{r,s,t}_on_B2_)
assume a3 <> b3 ; ::_thesis: ex B2 being LINE of IPP st {r,s,t} on B2
take B2 = B2; ::_thesis: {r,s,t} on B2
( A3 = C1 & B3 <> C1 ) by A13, A54, A21, A22, A58, A57, A24, A65, A55, A68, A69, INCPROJ:def_4;
then A100: b1 = s by A56, A23, A29, A16, INCPROJ:def_4;
( A1 = C3 & B1 <> C3 ) by A11, A13, A22, A58, A64, A60, A17, A63, A19, A59, A69, INCPROJ:def_4;
then {s,r,t} on B2 by A8, A20, A26, A28, A18, A100, INCPROJ:def_4;
hence {r,s,t} on B2 by Th11; ::_thesis: verum
end;
hence ex O being LINE of IPP st {r,s,t} on O by A91; ::_thesis: verum
end;
hence ex O being LINE of IPP st {r,s,t} on O by A70; ::_thesis: verum
end;
A101: C3 <> C1 by A10, ZFMISC_1:def_5;
A102: a2 on C2 by A2, INCSP_1:2;
A103: now__::_thesis:_(_o_<>_b3_&_o_=_a1_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
assume that
A104: o <> b3 and
A105: o = a1 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
A106: now__::_thesis:_(_o_<>_a2_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
A107: now__::_thesis:_(_a3_=_b3_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
A108: B2 <> C3 by A12, A54, A56, A64, A27, A101, INCPROJ:def_4;
assume A109: a3 = b3 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
then A2 = C3 by A64, A60, A62, A25, A104, A105, INCPROJ:def_4;
then A110: r = b3 by A20, A15, A61, A108, INCPROJ:def_4;
A111: ( b2 on C2 & b3 on C3 ) by A2, A3, INCSP_1:2;
A112: ( o on C3 & a2 on C2 ) by A2, A3, INCSP_1:2;
A113: ( a2 on A1 & b2 on B1 ) by A4, A7, INCSP_1:2;
consider O being LINE of IPP such that
A114: ( t on O & s on O ) by INCPROJ:def_5;
A115: ( C2 <> C3 & o on C2 ) by A2, A10, INCSP_1:2, ZFMISC_1:def_5;
take O = O; ::_thesis: {r,s,t} on O
b3 on A1 by A4, A109, INCSP_1:2;
then A1 <> B1 by A11, A14, A109, A115, A112, A111, A113, Th10;
then r = t by A17, A26, A28, A18, A109, A110, INCPROJ:def_4;
hence {r,s,t} on O by A114, INCSP_1:2; ::_thesis: verum
end;
assume A116: o <> a2 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
now__::_thesis:_(_a3_<>_b3_implies_ex_B1_being_LINE_of_IPP_st_{r,s,t}_on_B1_)
assume a3 <> b3 ; ::_thesis: ex B1 being LINE of IPP st {r,s,t} on B1
take B1 = B1; ::_thesis: {r,s,t} on B1
( A3 = C2 & B3 <> C2 ) by A12, A54, A56, A22, A102, A57, A24, A29, A55, A105, A116, INCPROJ:def_4;
then A117: s = b2 by A58, A23, A16, A65, INCPROJ:def_4;
( A2 = C3 & B2 <> C3 ) by A11, A12, A54, A56, A64, A60, A62, A25, A27, A101, A105, INCPROJ:def_4;
then {t,s,r} on B1 by A7, A20, A15, A61, A117, INCPROJ:def_4;
hence {r,s,t} on B1 by Th11; ::_thesis: verum
end;
hence ex O being LINE of IPP st {r,s,t} on O by A107; ::_thesis: verum
end;
now__::_thesis:_(_o_=_a2_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
assume o = a2 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
then A118: A1 = C3 by A11, A64, A60, A17, A63, INCPROJ:def_4;
( A2 = C3 & B2 <> C3 ) by A11, A12, A54, A56, A64, A60, A62, A25, A27, A101, A105, INCPROJ:def_4;
then A119: r = b3 by A20, A15, A61, INCPROJ:def_4;
consider O being LINE of IPP such that
A120: ( t on O & s on O ) by INCPROJ:def_5;
take O = O; ::_thesis: {r,s,t} on O
B1 <> C3 by A13, A22, A58, A64, A19, A59, INCPROJ:def_4;
then r = t by A20, A26, A28, A18, A118, A119, INCPROJ:def_4;
hence {r,s,t} on O by A120, INCSP_1:2; ::_thesis: verum
end;
hence ex O being LINE of IPP st {r,s,t} on O by A106; ::_thesis: verum
end;
A121: C1 <> B3 by A13, A54, A22, A58, A65, A55, INCPROJ:def_4;
A122: now__::_thesis:_(_o_=_b3_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
assume A123: o = b3 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
A124: now__::_thesis:_(_a1_=_o_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
assume A125: a1 = o ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
A126: now__::_thesis:_(_o_=_a2_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
assume o = a2 ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
then A127: A1 = C3 by A11, A64, A60, A17, A63, INCPROJ:def_4;
( A2 = C3 & B2 = C1 ) by A11, A12, A54, A56, A64, A60, A62, A25, A27, A61, A123, A125, INCPROJ:def_4;
then A128: o = r by A54, A64, A15, A101, INCPROJ:def_4;
consider O being LINE of IPP such that
A129: ( t on O & s on O ) by INCPROJ:def_5;
take O = O; ::_thesis: {r,s,t} on O
B1 = C2 by A13, A22, A58, A19, A18, A123, INCPROJ:def_4;
then r = t by A22, A64, A26, A28, A59, A128, A127, INCPROJ:def_4;
hence {r,s,t} on O by A129, INCSP_1:2; ::_thesis: verum
end;
now__::_thesis:_(_o_<>_a2_implies_ex_C2_being_LINE_of_IPP_st_{r,s,t}_on_C2_)
( B2 = C1 & A2 = C3 ) by A11, A12, A54, A56, A64, A60, A62, A25, A27, A61, A123, A125, INCPROJ:def_4;
then A130: r = o by A54, A64, A15, A101, INCPROJ:def_4;
assume o <> a2 ; ::_thesis: ex C2 being LINE of IPP st {r,s,t} on C2
then A131: C2 = A3 by A22, A102, A57, A24, A125, INCPROJ:def_4;
take C2 = C2; ::_thesis: {r,s,t} on C2
C2 = B1 by A13, A22, A58, A19, A18, A123, INCPROJ:def_4;
hence {r,s,t} on C2 by A22, A23, A28, A131, A130, INCSP_1:2; ::_thesis: verum
end;
hence ex O being LINE of IPP st {r,s,t} on O by A126; ::_thesis: verum
end;
now__::_thesis:_(_a1_<>_o_implies_ex_O_being_LINE_of_IPP_st_{r,s,t}_on_O_)
assume A132: a1 <> o ; ::_thesis: ex O being LINE of IPP st {r,s,t} on O
A133: now__::_thesis:_(_o_=_a2_implies_ex_B2_being_LINE_of_IPP_st_{r,s,t}_on_B2_)
assume A134: o = a2 ; ::_thesis: ex B2 being LINE of IPP st {r,s,t} on B2
then A135: A1 = C3 by A11, A64, A60, A17, A63, INCPROJ:def_4;
take B2 = B2; ::_thesis: {r,s,t} on B2
C1 = A3 by A54, A21, A57, A24, A132, A134, INCPROJ:def_4;
then A136: b1 = s by A56, A23, A29, A16, A121, INCPROJ:def_4;
B1 = C2 by A13, A22, A58, A19, A18, A123, INCPROJ:def_4;
then {s,r,t} on B2 by A8, A20, A26, A28, A18, A59, A136, A135, INCPROJ:def_4;
hence {r,s,t} on B2 by Th11; ::_thesis: verum
end;
now__::_thesis:_(_o_<>_a2_implies_ex_A3_being_LINE_of_IPP_st_{r,s,t}_on_A3_)
assume o <> a2 ; ::_thesis: ex A3 being LINE of IPP st {r,s,t} on A3
take A3 = A3; ::_thesis: {r,s,t} on A3
( B2 = C1 & A2 <> C1 ) by A11, A12, A54, A56, A64, A60, A62, A27, A61, A101, A123, INCPROJ:def_4;
then A137: r = a1 by A21, A25, A15, INCPROJ:def_4;
( B1 = C2 & A1 <> C2 ) by A11, A13, A22, A58, A64, A60, A17, A19, A18, A59, A123, INCPROJ:def_4;
then {t,s,r} on A3 by A6, A102, A63, A26, A28, A137, INCPROJ:def_4;
hence {r,s,t} on A3 by Th11; ::_thesis: verum
end;
hence ex O being LINE of IPP st {r,s,t} on O by A133; ::_thesis: verum
end;
hence ex O being LINE of IPP st {r,s,t} on O by A124; ::_thesis: verum
end;
now__::_thesis:_(_o_<>_b3_&_o_<>_a1_&_o_<>_a2_&_a1_<>_b1_&_a3_=_b3_implies_ex_O_being_Element_of_the_Lines_of_IPP_st_{r,s,t}_on_O_)
A138: ( b2 on B1 & a2 on C2 ) by A2, A7, INCSP_1:2;
A139: ( o on C3 & b3 on C3 ) by A3, INCSP_1:2;
A140: ( a1 on A2 & b1 on B2 ) by A5, A8, INCSP_1:2;
A141: ( b2 on C2 & o on C2 ) by A2, INCSP_1:2;
A142: ( b3 on B1 & t on A1 ) by A4, A7, INCSP_1:2;
A143: t on B1 by A7, INCSP_1:2;
consider O being Element of the Lines of IPP such that
A144: ( t on O & s on O ) by INCPROJ:def_5;
assume that
A145: o <> b3 and
o <> a1 and
o <> a2 and
A146: a1 <> b1 and
A147: a3 = b3 ; ::_thesis: ex O being Element of the Lines of IPP st {r,s,t} on O
take O = O; ::_thesis: {r,s,t} on O
A148: C1 <> C3 by A10, ZFMISC_1:def_5;
b3 on A2 by A5, A147, INCSP_1:2;
then A2 <> B2 by A54, A56, A21, A64, A20, A145, A146, A140, A148, Th10;
then A149: b3 = r by A62, A15, A61, A147, INCPROJ:def_4;
A150: b3 on A1 by A4, A147, INCSP_1:2;
( C2 <> C3 & a2 on A1 ) by A4, A10, INCSP_1:2, ZFMISC_1:def_5;
then A1 <> B1 by A14, A145, A150, A138, A141, A139, Th10;
then r = t by A150, A142, A143, A149, INCPROJ:def_4;
hence {r,s,t} on O by A144, INCSP_1:2; ::_thesis: verum
end;
hence ex O being LINE of IPP st {r,s,t} on O by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A122, A103, A66, A30, INCPROJ:def_13; ::_thesis: verum
end;
Lm1: for IPP being IncProjSp
for a, b, c, d being POINT of IPP
for A, B being LINE of IPP st ex o being POINT of IPP st
( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different holds
ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
proof
let IPP be IncProjSp; ::_thesis: for a, b, c, d being POINT of IPP
for A, B being LINE of IPP st ex o being POINT of IPP st
( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different holds
ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
let a, b, c, d be POINT of IPP; ::_thesis: for A, B being LINE of IPP st ex o being POINT of IPP st
( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different holds
ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
let A, B be LINE of IPP; ::_thesis: ( ex o being POINT of IPP st
( o on A & o on B ) & a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different implies ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) )
assume that
A1: ex o being POINT of IPP st
( o on A & o on B ) and
A2: a on A and
A3: b on A and
A4: c on A and
A5: d on A and
A6: a,b,c,d are_mutually_different ; ::_thesis: ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
consider o being POINT of IPP such that
A7: o on A and
A8: o on B by A1;
now__::_thesis:_(_A_<>_B_implies_ex_p,_q,_r,_s_being_POINT_of_IPP_st_
(_p_on_B_&_q_on_B_&_r_on_B_&_s_on_B_&_p,q,r,s_are_mutually_different_)_)
assume A <> B ; ::_thesis: ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
then consider x, y being POINT of IPP such that
A9: x on A and
A10: not x on B and
A11: y on B and
A12: not y on A by Th3;
consider C being LINE of IPP such that
A13: x on C and
A14: y on C by INCPROJ:def_5;
consider w being POINT of IPP such that
A15: w on C and
A16: w <> x and
A17: w <> y by Th8;
A18: now__::_thesis:_for_u1,_u2,_v1,_v2_being_POINT_of_IPP
for_D1,_D2_being_LINE_of_IPP_st_u1_on_A_&_u2_on_A_&_v1_on_B_&_w_on_D1_&_u1_on_D1_&_v1_on_D1_&_v2_on_B_&_w_on_D2_&_u2_on_D2_&_v2_on_D2_&_u1_<>_u2_holds_
not_v1_=_v2
A19: not w on B by A10, A11, A13, A14, A15, A17, INCPROJ:def_4;
let u1, u2, v1, v2 be POINT of IPP; ::_thesis: for D1, D2 being LINE of IPP st u1 on A & u2 on A & v1 on B & w on D1 & u1 on D1 & v1 on D1 & v2 on B & w on D2 & u2 on D2 & v2 on D2 & u1 <> u2 holds
not v1 = v2
let D1, D2 be LINE of IPP; ::_thesis: ( u1 on A & u2 on A & v1 on B & w on D1 & u1 on D1 & v1 on D1 & v2 on B & w on D2 & u2 on D2 & v2 on D2 & u1 <> u2 implies not v1 = v2 )
assume that
A20: ( u1 on A & u2 on A ) and
A21: v1 on B and
A22: w on D1 and
A23: u1 on D1 and
A24: v1 on D1 and
v2 on B and
A25: w on D2 and
A26: u2 on D2 and
A27: v2 on D2 ; ::_thesis: ( u1 <> u2 implies not v1 = v2 )
A28: D1 <> A by A9, A12, A13, A14, A15, A16, A22, INCPROJ:def_4;
assume A29: u1 <> u2 ; ::_thesis: not v1 = v2
assume v1 = v2 ; ::_thesis: contradiction
then D1 = D2 by A21, A22, A24, A25, A27, A19, INCPROJ:def_4;
hence contradiction by A20, A23, A26, A29, A28, INCPROJ:def_4; ::_thesis: verum
end;
A30: now__::_thesis:_for_u_being_POINT_of_IPP_st_u_on_A_holds_
ex_v_being_POINT_of_IPP_ex_D_being_LINE_of_IPP_st_
(_v_on_B_&_w_on_D_&_u_on_D_&_v_on_D_)
let u be POINT of IPP; ::_thesis: ( u on A implies ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D ) )
assume A31: u on A ; ::_thesis: ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )
A32: now__::_thesis:_(_u_<>_o_&_x_<>_u_implies_ex_v_being_POINT_of_IPP_ex_D_being_LINE_of_IPP_st_
(_v_on_B_&_w_on_D_&_u_on_D_&_v_on_D_)_)
assume that
u <> o and
A33: x <> u ; ::_thesis: ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )
consider D being LINE of IPP such that
A34: ( w on D & u on D ) by INCPROJ:def_5;
not x on D
proof
assume x on D ; ::_thesis: contradiction
then u on C by A13, A15, A16, A34, INCPROJ:def_4;
hence contradiction by A9, A12, A13, A14, A31, A33, INCPROJ:def_4; ::_thesis: verum
end;
then consider v being POINT of IPP such that
A35: ( v on B & v on D ) by A7, A8, A9, A10, A11, A12, A13, A14, A15, A31, A34, INCPROJ:def_8;
take v = v; ::_thesis: ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )
take D = D; ::_thesis: ( v on B & w on D & u on D & v on D )
thus ( v on B & w on D & u on D & v on D ) by A34, A35; ::_thesis: verum
end;
now__::_thesis:_(_u_=_o_implies_ex_v_being_POINT_of_IPP_ex_D_being_LINE_of_IPP_st_
(_v_on_B_&_w_on_D_&_u_on_D_&_v_on_D_)_)
consider D being LINE of IPP such that
A36: ( w on D & u on D ) by INCPROJ:def_5;
assume A37: u = o ; ::_thesis: ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )
take v = o; ::_thesis: ex D being LINE of IPP st
( v on B & w on D & u on D & v on D )
take D = D; ::_thesis: ( v on B & w on D & u on D & v on D )
thus ( v on B & w on D & u on D & v on D ) by A8, A37, A36; ::_thesis: verum
end;
hence ex v being POINT of IPP ex D being LINE of IPP st
( v on B & w on D & u on D & v on D ) by A11, A13, A14, A15, A32; ::_thesis: verum
end;
then consider p being POINT of IPP, D1 being Element of the Lines of IPP such that
A38: p on B and
A39: ( w on D1 & a on D1 & p on D1 ) by A2;
consider r being POINT of IPP, D3 being Element of the Lines of IPP such that
A40: r on B and
A41: ( w on D3 & c on D3 & r on D3 ) by A4, A30;
consider q being POINT of IPP, D2 being Element of the Lines of IPP such that
A42: q on B and
A43: ( w on D2 & b on D2 & q on D2 ) by A3, A30;
consider s being POINT of IPP, D4 being Element of the Lines of IPP such that
A44: s on B and
A45: ( w on D4 & d on D4 & s on D4 ) by A5, A30;
d <> a by A6, ZFMISC_1:def_6;
then A46: s <> p by A2, A5, A18, A38, A39, A45;
a <> c by A6, ZFMISC_1:def_6;
then A47: p <> r by A2, A4, A18, A38, A39, A41;
d <> b by A6, ZFMISC_1:def_6;
then A48: s <> q by A3, A5, A18, A42, A43, A45;
c <> d by A6, ZFMISC_1:def_6;
then A49: r <> s by A4, A5, A18, A40, A41, A45;
b <> c by A6, ZFMISC_1:def_6;
then A50: q <> r by A3, A4, A18, A42, A43, A41;
a <> b by A6, ZFMISC_1:def_6;
then p <> q by A2, A3, A18, A38, A39, A43;
then p,q,r,s are_mutually_different by A50, A49, A46, A48, A47, ZFMISC_1:def_6;
hence ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) by A38, A42, A40, A44; ::_thesis: verum
end;
hence ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) by A2, A3, A4, A5, A6; ::_thesis: verum
end;
theorem Th13: :: PROJRED1:13
for IPP being IncProjSp st ex A being LINE of IPP ex a, b, c, d being POINT of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) holds
for B being LINE of IPP ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
proof
let IPP be IncProjSp; ::_thesis: ( ex A being LINE of IPP ex a, b, c, d being POINT of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) implies for B being LINE of IPP ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) )
given A being LINE of IPP, a, b, c, d being POINT of IPP such that A1: ( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) ; ::_thesis: for B being LINE of IPP ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
let B be LINE of IPP; ::_thesis: ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
consider x being POINT of IPP such that
A2: x on A by Th7;
consider y being POINT of IPP such that
A3: y on B by Th7;
consider C being LINE of IPP such that
A4: x on C and
A5: y on C by INCPROJ:def_5;
ex p1, q1, r1, s1 being POINT of IPP st
( p1 on C & q1 on C & r1 on C & s1 on C & p1,q1,r1,s1 are_mutually_different ) by A1, A2, A4, Lm1;
hence ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) by A3, A5, Lm1; ::_thesis: verum
end;
Lm2: for IPP being Fanoian IncProjSp ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_different & d on A & c,d,p,q are_mutually_different )
proof
let IPP be Fanoian IncProjSp; ::_thesis: ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_different & d on A & c,d,p,q are_mutually_different )
consider r being POINT of IPP, A being LINE of IPP such that
A1: not r on A by INCPROJ:def_6;
consider p, q, c being POINT of IPP such that
A2: p <> q and
A3: q <> c and
A4: c <> p and
A5: p on A and
A6: q on A and
A7: c on A by INCPROJ:def_7;
consider B being LINE of IPP such that
A8: r on B and
A9: c on B by INCPROJ:def_5;
consider s being POINT of IPP such that
A10: s on B and
A11: s <> r and
A12: s <> c by Th8;
consider L being LINE of IPP such that
A13: p on L and
A14: s on L by INCPROJ:def_5;
consider Q being LINE of IPP such that
A15: r on Q and
A16: q on Q by INCPROJ:def_5;
A17: not p on Q by A1, A2, A5, A6, A15, A16, INCPROJ:def_4;
A18: not c on Q by A1, A3, A6, A7, A15, A16, INCPROJ:def_4;
then A19: not s on Q by A8, A9, A10, A11, A15, INCPROJ:def_4;
not c on L
proof
assume c on L ; ::_thesis: contradiction
then p on B by A9, A10, A12, A13, A14, INCPROJ:def_4;
hence contradiction by A1, A4, A5, A7, A8, A9, INCPROJ:def_4; ::_thesis: verum
end;
then consider a being POINT of IPP such that
A20: a on Q and
A21: a on L by A1, A5, A6, A7, A8, A9, A10, A15, A16, A13, A14, A18, INCPROJ:def_8;
A22: {a,p,s} on L by A13, A14, A21, INCSP_1:2;
consider R being LINE of IPP such that
A23: q on R and
A24: s on R by INCPROJ:def_5;
consider S being LINE of IPP such that
A25: p on S and
A26: r on S by INCPROJ:def_5;
A27: not c on S by A1, A4, A5, A7, A25, A26, INCPROJ:def_4;
then A28: not s on S by A8, A9, A10, A11, A26, INCPROJ:def_4;
A29: S <> L by A8, A9, A10, A11, A14, A26, A27, INCPROJ:def_4;
then A30: not r on L by A1, A5, A13, A25, A26, INCPROJ:def_4;
A31: S <> Q by A1, A2, A5, A6, A15, A16, A25, INCPROJ:def_4;
A32: not q on S by A1, A2, A5, A6, A25, A26, INCPROJ:def_4;
A33: not q on L
proof
assume q on L ; ::_thesis: contradiction
then s on A by A2, A5, A6, A13, A14, INCPROJ:def_4;
hence contradiction by A1, A7, A8, A9, A10, A12, INCPROJ:def_4; ::_thesis: verum
end;
A34: not p on R
proof
assume p on R ; ::_thesis: contradiction
then s on A by A2, A5, A6, A23, A24, INCPROJ:def_4;
hence contradiction by A1, A7, A8, A9, A10, A12, INCPROJ:def_4; ::_thesis: verum
end;
then not c on R by A3, A5, A6, A7, A23, INCPROJ:def_4;
then consider b being POINT of IPP such that
A35: b on R and
A36: b on S by A1, A5, A6, A7, A8, A9, A10, A25, A26, A23, A24, A27, INCPROJ:def_8;
A37: {b,q,s} on R by A23, A24, A35, INCSP_1:2;
A38: R <> Q
proof
assume not R <> Q ; ::_thesis: contradiction
then B = Q by A8, A10, A11, A15, A24, INCPROJ:def_4;
hence contradiction by A1, A3, A6, A7, A8, A9, A16, INCPROJ:def_4; ::_thesis: verum
end;
then A39: not r on R by A1, A6, A15, A16, A23, INCPROJ:def_4;
A40: {c,r,s} on B by A8, A9, A10, INCSP_1:2;
A41: {b,p,r} on S by A25, A26, A36, INCSP_1:2;
A42: a <> r by A1, A5, A13, A25, A26, A21, A29, INCPROJ:def_4;
then A43: not a on S by A15, A16, A26, A32, A20, INCPROJ:def_4;
A44: {a,q,r} on Q by A15, A16, A20, INCSP_1:2;
consider C being LINE of IPP such that
A45: a on C and
A46: b on C by INCPROJ:def_5;
a <> s by A8, A9, A10, A11, A15, A18, A20, INCPROJ:def_4;
then A47: R <> C by A13, A14, A24, A34, A21, A45, INCPROJ:def_4;
A48: not b on Q by A16, A23, A38, A32, A35, A36, INCPROJ:def_4;
then not r on C by A15, A20, A45, A46, A42, INCPROJ:def_4;
then consider d being POINT of IPP such that
A49: d on A and
A50: d on C by A1, A5, A6, A15, A16, A25, A26, A20, A36, A45, A46, A31, INCPROJ:def_8;
S <> C by A15, A16, A26, A32, A20, A45, A42, INCPROJ:def_4;
then A51: d <> p by A25, A34, A35, A36, A46, A50, INCPROJ:def_4;
A52: {c,p,q} on A by A5, A6, A7, INCSP_1:2;
A53: {a,b} on C by A45, A46, INCSP_1:1;
then A54: not c on C by A39, A17, A32, A33, A34, A19, A30, A28, A22, A44, A37, A41, A52, A40, INCPROJ:def_12;
consider D being LINE of IPP such that
A55: b on D and
A56: c on D by INCPROJ:def_5;
A57: R <> D by A3, A5, A6, A7, A23, A34, A56, INCPROJ:def_4;
d <> q by A16, A33, A20, A21, A45, A46, A48, A50, INCPROJ:def_4;
then A58: c,d,p,q are_mutually_different by A2, A3, A4, A54, A50, A51, ZFMISC_1:def_6;
S <> D by A1, A4, A5, A7, A25, A26, A56, INCPROJ:def_4;
then C,D,R,S are_mutually_different by A25, A34, A45, A54, A56, A43, A57, A47, ZFMISC_1:def_6;
hence ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_different & d on A & c,d,p,q are_mutually_different ) by A39, A17, A32, A33, A34, A19, A30, A28, A22, A44, A37, A41, A52, A40, A53, A54, A55, A56, A49, A58; ::_thesis: verum
end;
theorem :: PROJRED1:14
for IPP being Fanoian IncProjSp ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C )
proof
let IPP be Fanoian IncProjSp; ::_thesis: ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C )
ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP ex d being POINT of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C & b on D & c on D & C,D,R,S are_mutually_different & d on A & c,d,p,q are_mutually_different ) by Lm2;
hence ex p, q, r, s, a, b, c being POINT of IPP ex A, B, C, Q, L, R, S, D being LINE of IPP st
( not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C & not c on C ) ; ::_thesis: verum
end;
theorem :: PROJRED1:15
for IPP being Fanoian IncProjSp ex a being POINT of IPP ex A, B, C, D being LINE of IPP st
( a on A & a on B & a on C & a on D & A,B,C,D are_mutually_different )
proof
let IPP be Fanoian IncProjSp; ::_thesis: ex a being POINT of IPP ex A, B, C, D being LINE of IPP st
( a on A & a on B & a on C & a on D & A,B,C,D are_mutually_different )
consider p, q, r, s, a, b, c being POINT of IPP, A, B, C, Q, L, R, S, D being LINE of IPP, d being POINT of IPP such that
not q on L and
not r on L and
not p on Q and
not s on Q and
not p on R and
not r on R and
not q on S and
not s on S and
{a,p,s} on L and
{a,q,r} on Q and
A1: ( {b,q,s} on R & {b,p,r} on S ) and
{c,p,q} on A and
{c,r,s} on B and
A2: {a,b} on C and
not c on C and
A3: b on D and
c on D and
A4: C,D,R,S are_mutually_different and
d on A and
c,d,p,q are_mutually_different by Lm2;
A5: b on C by A2, INCSP_1:1;
( b on S & b on R ) by A1, INCSP_1:2;
hence ex a being POINT of IPP ex A, B, C, D being LINE of IPP st
( a on A & a on B & a on C & a on D & A,B,C,D are_mutually_different ) by A3, A4, A5; ::_thesis: verum
end;
theorem Th16: :: PROJRED1:16
for IPP being Fanoian IncProjSp ex a, b, c, d being POINT of IPP ex A being LINE of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different )
proof
let IPP be Fanoian IncProjSp; ::_thesis: ex a, b, c, d being POINT of IPP ex A being LINE of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different )
consider p, q, r, s, a, b, c being POINT of IPP, A, B, C, Q, L, R, S, D being LINE of IPP, d being POINT of IPP such that
not q on L and
not r on L and
not p on Q and
not s on Q and
not p on R and
not r on R and
not q on S and
not s on S and
{a,p,s} on L and
{a,q,r} on Q and
{b,q,s} on R and
{b,p,r} on S and
A1: {c,p,q} on A and
{c,r,s} on B and
{a,b} on C and
not c on C and
b on D and
c on D and
C,D,R,S are_mutually_different and
A2: ( d on A & c,d,p,q are_mutually_different ) by Lm2;
A3: q on A by A1, INCSP_1:2;
( c on A & p on A ) by A1, INCSP_1:2;
hence ex a, b, c, d being POINT of IPP ex A being LINE of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) by A2, A3; ::_thesis: verum
end;
theorem :: PROJRED1:17
for IPP being Fanoian IncProjSp
for B being LINE of IPP ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
proof
let IPP be Fanoian IncProjSp; ::_thesis: for B being LINE of IPP ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
let B be LINE of IPP; ::_thesis: ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different )
ex a, b, c, d being POINT of IPP ex A being LINE of IPP st
( a on A & b on A & c on A & d on A & a,b,c,d are_mutually_different ) by Th16;
hence ex p, q, r, s being POINT of IPP st
( p on B & q on B & r on B & s on B & p,q,r,s are_mutually_different ) by Th13; ::_thesis: verum
end;
definition
let IPP be 2-dimensional Desarguesian IncProjSp;
let K, L be LINE of IPP;
let p be POINT of IPP;
assume that
A1: not p on K and
A2: not p on L ;
func IncProj (K,p,L) -> PartFunc of the Points of IPP, the Points of IPP means :Def1: :: PROJRED1:def 1
( dom it c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom it iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( it . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) );
existence
ex b1 being PartFunc of the Points of IPP, the Points of IPP st
( dom b1 c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom b1 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( b1 . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) )
proof
defpred S1[ set , set ] means ex x, y being POINT of IPP st
( x = $1 & y = $2 & x on K & y on L & ex X being LINE of IPP st
( p on X & x on X & y on X ) );
set XX = the Points of IPP;
A3: for x, y1, y2 being set st x in the Points of IPP & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( x in the Points of IPP & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume that
A4: x in the Points of IPP and
A5: S1[x,y1] and
A6: S1[x,y2] ; ::_thesis: y1 = y2
reconsider x = x as POINT of IPP by A4;
reconsider y1 = y1, y2 = y2 as POINT of IPP by A5, A6;
consider A1 being Element of the Lines of IPP such that
A7: p on A1 and
A8: x on A1 and
A9: y1 on A1 by A5;
y2 on A1 by A1, A6, A7, A8, INCPROJ:def_4;
hence y1 = y2 by A2, A5, A6, A7, A9, INCPROJ:def_4; ::_thesis: verum
end;
A10: for x, y being set st x in the Points of IPP & S1[x,y] holds
y in the Points of IPP ;
consider f being PartFunc of the Points of IPP, the Points of IPP such that
A11: for x being set holds
( x in dom f iff ( x in the Points of IPP & ex y being set st S1[x,y] ) ) and
A12: for x being set st x in dom f holds
S1[x,f . x] from PARTFUN1:sch_2(A10, A3);
take f ; ::_thesis: ( dom f c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom f iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) )
thus dom f c= the Points of IPP ; ::_thesis: ( ( for x being POINT of IPP holds
( x in dom f iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) )
thus A13: for x being POINT of IPP holds
( x in dom f iff x on K ) ::_thesis: for x, y being POINT of IPP st x on K & y on L holds
( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) )
proof
let x be POINT of IPP; ::_thesis: ( x in dom f iff x on K )
A14: ( x on K implies x in dom f )
proof
consider X being LINE of IPP such that
A15: ( p on X & x on X ) by INCPROJ:def_5;
assume A16: x on K ; ::_thesis: x in dom f
ex y being POINT of IPP st
( y on L & y on X ) by INCPROJ:def_9;
hence x in dom f by A11, A16, A15; ::_thesis: verum
end;
( x in dom f implies x on K )
proof
assume x in dom f ; ::_thesis: x on K
then S1[x,f . x] by A12;
hence x on K ; ::_thesis: verum
end;
hence ( x in dom f iff x on K ) by A14; ::_thesis: verum
end;
let x, y be POINT of IPP; ::_thesis: ( x on K & y on L implies ( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) )
assume that
A17: x on K and
A18: y on L ; ::_thesis: ( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) )
A19: ( f . x = y implies ex X being LINE of IPP st
( p on X & x on X & y on X ) )
proof
x in dom f by A13, A17;
then A20: S1[x,f . x] by A12;
assume f . x = y ; ::_thesis: ex X being LINE of IPP st
( p on X & x on X & y on X )
hence ex X being LINE of IPP st
( p on X & x on X & y on X ) by A20; ::_thesis: verum
end;
( ex X being LINE of IPP st
( p on X & x on X & y on X ) implies f . x = y )
proof
x in dom f by A13, A17;
then A21: S1[x,f . x] by A12;
assume ex X being LINE of IPP st
( p on X & x on X & y on X ) ; ::_thesis: f . x = y
hence f . x = y by A3, A18, A21; ::_thesis: verum
end;
hence ( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) by A19; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of the Points of IPP, the Points of IPP st dom b1 c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom b1 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( b1 . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) & dom b2 c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom b2 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( b2 . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) holds
b1 = b2
proof
let f1, f2 be PartFunc of the Points of IPP, the Points of IPP; ::_thesis: ( dom f1 c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom f1 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( f1 . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) & dom f2 c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom f2 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( f2 . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) implies f1 = f2 )
assume that
dom f1 c= the Points of IPP and
A22: for x being POINT of IPP holds
( x in dom f1 iff x on K ) and
A23: for x, y being POINT of IPP st x on K & y on L holds
( f1 . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) and
dom f2 c= the Points of IPP and
A24: for x being POINT of IPP holds
( x in dom f2 iff x on K ) and
A25: for x, y being POINT of IPP st x on K & y on L holds
( f2 . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ; ::_thesis: f1 = f2
for x being set holds
( x in dom f1 iff x in dom f2 )
proof
let x be set ; ::_thesis: ( x in dom f1 iff x in dom f2 )
A26: ( x in dom f2 implies x in dom f1 )
proof
assume A27: x in dom f2 ; ::_thesis: x in dom f1
then reconsider x = x as Element of the Points of IPP ;
x on K by A24, A27;
hence x in dom f1 by A22; ::_thesis: verum
end;
( x in dom f1 implies x in dom f2 )
proof
assume A28: x in dom f1 ; ::_thesis: x in dom f2
then reconsider x = x as Element of the Points of IPP ;
x on K by A22, A28;
hence x in dom f2 by A24; ::_thesis: verum
end;
hence ( x in dom f1 iff x in dom f2 ) by A26; ::_thesis: verum
end;
then A29: dom f1 = dom f2 by TARSKI:1;
for x being POINT of IPP st x in dom f1 holds
f1 . x = f2 . x
proof
let x be POINT of IPP; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x )
consider A2 being LINE of IPP such that
A30: ( p on A2 & x on A2 ) by INCPROJ:def_5;
consider y2 being POINT of IPP such that
A31: ( y2 on A2 & y2 on L ) by INCPROJ:def_9;
assume x in dom f1 ; ::_thesis: f1 . x = f2 . x
then A32: x on K by A22;
then f2 . x = y2 by A25, A30, A31;
hence f1 . x = f2 . x by A23, A32, A30, A31; ::_thesis: verum
end;
hence f1 = f2 by A29, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines IncProj PROJRED1:def_1_:_
for IPP being 2-dimensional Desarguesian IncProjSp
for K, L being LINE of IPP
for p being POINT of IPP st not p on K & not p on L holds
for b5 being PartFunc of the Points of IPP, the Points of IPP holds
( b5 = IncProj (K,p,L) iff ( dom b5 c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom b5 iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( b5 . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) ) );
theorem Th18: :: PROJRED1:18
for IPP being 2-dimensional Desarguesian IncProjSp
for p being POINT of IPP
for K being LINE of IPP st not p on K holds
for x being POINT of IPP st x on K holds
(IncProj (K,p,K)) . x = x
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p being POINT of IPP
for K being LINE of IPP st not p on K holds
for x being POINT of IPP st x on K holds
(IncProj (K,p,K)) . x = x
let p be POINT of IPP; ::_thesis: for K being LINE of IPP st not p on K holds
for x being POINT of IPP st x on K holds
(IncProj (K,p,K)) . x = x
let K be LINE of IPP; ::_thesis: ( not p on K implies for x being POINT of IPP st x on K holds
(IncProj (K,p,K)) . x = x )
assume A1: not p on K ; ::_thesis: for x being POINT of IPP st x on K holds
(IncProj (K,p,K)) . x = x
let x be POINT of IPP; ::_thesis: ( x on K implies (IncProj (K,p,K)) . x = x )
A2: ex X being LINE of IPP st
( p on X & x on X ) by INCPROJ:def_5;
assume x on K ; ::_thesis: (IncProj (K,p,K)) . x = x
hence (IncProj (K,p,K)) . x = x by A1, A2, Def1; ::_thesis: verum
end;
theorem Th19: :: PROJRED1:19
for IPP being 2-dimensional Desarguesian IncProjSp
for p, x being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & x on K holds
(IncProj (K,p,L)) . x is POINT of IPP
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, x being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & x on K holds
(IncProj (K,p,L)) . x is POINT of IPP
let p, x be POINT of IPP; ::_thesis: for K, L being LINE of IPP st not p on K & not p on L & x on K holds
(IncProj (K,p,L)) . x is POINT of IPP
let K, L be LINE of IPP; ::_thesis: ( not p on K & not p on L & x on K implies (IncProj (K,p,L)) . x is POINT of IPP )
assume ( not p on K & not p on L & x on K ) ; ::_thesis: (IncProj (K,p,L)) . x is POINT of IPP
then x in dom (IncProj (K,p,L)) by Def1;
hence (IncProj (K,p,L)) . x is POINT of IPP by PARTFUN1:4; ::_thesis: verum
end;
theorem Th20: :: PROJRED1:20
for IPP being 2-dimensional Desarguesian IncProjSp
for p, x, y being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x holds
y on L
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, x, y being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x holds
y on L
let p, x, y be POINT of IPP; ::_thesis: for K, L being LINE of IPP st not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x holds
y on L
let K, L be LINE of IPP; ::_thesis: ( not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x implies y on L )
assume A1: ( not p on K & not p on L & x on K & y = (IncProj (K,p,L)) . x ) ; ::_thesis: y on L
consider X being LINE of IPP such that
A2: ( p on X & x on X ) by INCPROJ:def_5;
ex z being POINT of IPP st
( z on L & z on X ) by INCPROJ:def_9;
hence y on L by A1, A2, Def1; ::_thesis: verum
end;
theorem :: PROJRED1:21
for IPP being 2-dimensional Desarguesian IncProjSp
for p, y being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & y in rng (IncProj (K,p,L)) holds
y on L
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, y being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & y in rng (IncProj (K,p,L)) holds
y on L
let p, y be POINT of IPP; ::_thesis: for K, L being LINE of IPP st not p on K & not p on L & y in rng (IncProj (K,p,L)) holds
y on L
let K, L be LINE of IPP; ::_thesis: ( not p on K & not p on L & y in rng (IncProj (K,p,L)) implies y on L )
assume that
A1: ( not p on K & not p on L ) and
A2: y in rng (IncProj (K,p,L)) ; ::_thesis: y on L
consider x being POINT of IPP such that
A3: x in dom (IncProj (K,p,L)) and
A4: y = (IncProj (K,p,L)) . x by A2, PARTFUN1:3;
x on K by A1, A3, Def1;
hence y on L by A1, A4, Th20; ::_thesis: verum
end;
theorem Th22: :: PROJRED1:22
for IPP being 2-dimensional Desarguesian IncProjSp
for p, q being POINT of IPP
for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds
( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) )
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, q being POINT of IPP
for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds
( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) )
let p, q be POINT of IPP; ::_thesis: for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds
( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) )
let K, L, R be LINE of IPP; ::_thesis: ( not p on K & not p on L & not q on L & not q on R implies ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) ) )
assume that
A1: ( not p on K & not p on L ) and
A2: ( not q on L & not q on R ) ; ::_thesis: ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) )
for x being set holds
( x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) iff x in dom (IncProj (K,p,L)) )
proof
let x be set ; ::_thesis: ( x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) iff x in dom (IncProj (K,p,L)) )
( x in dom (IncProj (K,p,L)) implies x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) )
proof
assume A3: x in dom (IncProj (K,p,L)) ; ::_thesis: x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
then reconsider x9 = x as POINT of IPP ;
consider A being LINE of IPP such that
A4: ( x9 on A & p on A ) by INCPROJ:def_5;
consider y being POINT of IPP such that
A5: y on A and
A6: y on L by INCPROJ:def_9;
A7: y in dom (IncProj (L,q,R)) by A2, A6, Def1;
x9 on K by A1, A3, Def1;
then (IncProj (K,p,L)) . x = y by A1, A4, A5, A6, Def1;
hence x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A3, A7, FUNCT_1:11; ::_thesis: verum
end;
hence ( x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) iff x in dom (IncProj (K,p,L)) ) by FUNCT_1:11; ::_thesis: verum
end;
hence dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by TARSKI:1; ::_thesis: rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R))
for x being set st x in dom (IncProj (L,q,R)) holds
x in rng (IncProj (K,p,L))
proof
let x be set ; ::_thesis: ( x in dom (IncProj (L,q,R)) implies x in rng (IncProj (K,p,L)) )
assume A8: x in dom (IncProj (L,q,R)) ; ::_thesis: x in rng (IncProj (K,p,L))
thus x in rng (IncProj (K,p,L)) ::_thesis: verum
proof
reconsider x9 = x as POINT of IPP by A8;
A9: x9 on L by A2, A8, Def1;
ex y being POINT of IPP st
( y in dom (IncProj (K,p,L)) & x9 = (IncProj (K,p,L)) . y )
proof
consider A being LINE of IPP such that
A10: ( x9 on A & p on A ) by INCPROJ:def_5;
consider y being POINT of IPP such that
A11: y on A and
A12: y on K by INCPROJ:def_9;
take y ; ::_thesis: ( y in dom (IncProj (K,p,L)) & x9 = (IncProj (K,p,L)) . y )
thus y in dom (IncProj (K,p,L)) by A1, A12, Def1; ::_thesis: x9 = (IncProj (K,p,L)) . y
thus x9 = (IncProj (K,p,L)) . y by A1, A9, A10, A11, A12, Def1; ::_thesis: verum
end;
hence x in rng (IncProj (K,p,L)) by FUNCT_1:def_3; ::_thesis: verum
end;
end;
then dom (IncProj (L,q,R)) c= rng (IncProj (K,p,L)) by TARSKI:def_3;
hence rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) by RELAT_1:28; ::_thesis: verum
end;
theorem Th23: :: PROJRED1:23
for IPP being 2-dimensional Desarguesian IncProjSp
for p being POINT of IPP
for K, L being LINE of IPP
for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 holds
a1 = b1
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p being POINT of IPP
for K, L being LINE of IPP
for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 holds
a1 = b1
let p be POINT of IPP; ::_thesis: for K, L being LINE of IPP
for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 holds
a1 = b1
let K, L be LINE of IPP; ::_thesis: for a1, b1, a2, b2 being POINT of IPP st not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 holds
a1 = b1
let a1, b1, a2, b2 be POINT of IPP; ::_thesis: ( not p on K & not p on L & a1 on K & b1 on K & (IncProj (K,p,L)) . a1 = a2 & (IncProj (K,p,L)) . b1 = b2 & a2 = b2 implies a1 = b1 )
assume that
A1: not p on K and
A2: not p on L and
A3: a1 on K and
A4: b1 on K and
A5: (IncProj (K,p,L)) . a1 = a2 and
A6: (IncProj (K,p,L)) . b1 = b2 and
A7: a2 = b2 ; ::_thesis: a1 = b1
reconsider a2 = (IncProj (K,p,L)) . a1 as POINT of IPP by A5;
A8: a2 on L by A1, A2, A3, Th20;
then consider A being LINE of IPP such that
A9: p on A and
A10: a1 on A and
A11: a2 on A by A1, A2, A3, Def1;
reconsider b2 = (IncProj (K,p,L)) . b1 as Element of the Points of IPP by A6;
b2 on L by A1, A2, A4, Th20;
then consider B being LINE of IPP such that
A12: p on B and
A13: b1 on B and
A14: b2 on B by A1, A2, A4, Def1;
A = B by A2, A5, A6, A7, A8, A9, A11, A12, A14, INCPROJ:def_4;
hence a1 = b1 by A1, A3, A4, A9, A10, A13, INCPROJ:def_4; ::_thesis: verum
end;
theorem Th24: :: PROJRED1:24
for IPP being 2-dimensional Desarguesian IncProjSp
for p, x being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & x on K & x on L holds
(IncProj (K,p,L)) . x = x
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, x being POINT of IPP
for K, L being LINE of IPP st not p on K & not p on L & x on K & x on L holds
(IncProj (K,p,L)) . x = x
let p, x be POINT of IPP; ::_thesis: for K, L being LINE of IPP st not p on K & not p on L & x on K & x on L holds
(IncProj (K,p,L)) . x = x
let K, L be LINE of IPP; ::_thesis: ( not p on K & not p on L & x on K & x on L implies (IncProj (K,p,L)) . x = x )
A1: ex A being LINE of IPP st
( p on A & x on A ) by INCPROJ:def_5;
assume ( not p on K & not p on L & x on K & x on L ) ; ::_thesis: (IncProj (K,p,L)) . x = x
hence (IncProj (K,p,L)) . x = x by A1, Def1; ::_thesis: verum
end;
theorem :: PROJRED1:25
for IPP being 2-dimensional Desarguesian IncProjSp
for p, q, c being POINT of IPP
for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R holds
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for p, q, c being POINT of IPP
for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R holds
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
let p, q, c be POINT of IPP; ::_thesis: for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R holds
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
let K, L, R be LINE of IPP; ::_thesis: ( not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R implies ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) )
assume that
A1: not p on K and
A2: not p on L and
A3: not q on L and
A4: not q on R and
A5: c on K and
A6: c on L and
A7: c on R and
A8: K <> R ; ::_thesis: ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
defpred S1[ set ] means ex k being POINT of IPP st
( $1 = k & k on K );
consider X being set such that
A9: for x being set holds
( x in X iff ( x in the Points of IPP & S1[x] ) ) from XBOOLE_0:sch_1();
A10: ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP )
proof
set f = (IncProj (L,q,R)) * (IncProj (K,p,L));
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
hence dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP ; ::_thesis: rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP
rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) by A1, A2, A3, A4, Th22;
hence rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP by RELAT_1:def_19; ::_thesis: verum
end;
A11: now__::_thesis:_(_p_<>_q_implies_ex_o_being_POINT_of_IPP_st_
(_not_o_on_K_&_not_o_on_R_&_(IncProj_(L,q,R))_*_(IncProj_(K,p,L))_=_IncProj_(K,o,R)_)_)
A12: now__::_thesis:_(_L_=_R_implies_ex_p,_o_being_POINT_of_IPP_st_
(_not_o_on_K_&_not_o_on_R_&_(IncProj_(L,q,R))_*_(IncProj_(K,p,L))_=_IncProj_(K,o,R)_)_)
A13: X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) )
assume A14: e in X ; ::_thesis: e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
then reconsider e = e as Element of the Points of IPP by A9;
A15: ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A14;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A15, Def1; ::_thesis: verum
end;
assume A16: L = R ; ::_thesis: ex p, o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
A17: X c= dom (IncProj (K,p,R))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom (IncProj (K,p,R)) )
assume A18: e in X ; ::_thesis: e in dom (IncProj (K,p,R))
then reconsider e = e as POINT of IPP by A9;
ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A18;
hence e in dom (IncProj (K,p,R)) by A1, A2, A16, Def1; ::_thesis: verum
end;
A19: for x being POINT of IPP st x in X holds
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x
proof
let x be Element of the Points of IPP; ::_thesis: ( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x )
assume A20: x in X ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x
then A21: ((IncProj (R,q,R)) * (IncProj (K,p,R))) . x = (IncProj (R,q,R)) . ((IncProj (K,p,R)) . x) by A16, A13, FUNCT_1:12;
A22: x on K by A1, A2, A16, A17, A20, Def1;
then reconsider y = (IncProj (K,p,R)) . x as POINT of IPP by A1, A2, A16, Th19;
y on R by A1, A2, A16, A22, Th20;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x by A3, A16, A21, Th18; ::_thesis: verum
end;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X )
assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; ::_thesis: e in X
then A23: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
then reconsider e = e as POINT of IPP ;
e on K by A1, A2, A23, Def1;
hence e in X by A9; ::_thesis: verum
end;
then A24: X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A13, XBOOLE_0:def_10;
A25: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4;
take p = p; ::_thesis: ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
dom (IncProj (K,p,R)) c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom (IncProj (K,p,R)) or e in X )
assume A26: e in dom (IncProj (K,p,R)) ; ::_thesis: e in X
then reconsider e = e as POINT of IPP ;
e on K by A1, A2, A16, A26, Def1;
hence e in X by A9; ::_thesis: verum
end;
then X = dom (IncProj (K,p,R)) by A17, XBOOLE_0:def_10;
hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A1, A2, A16, A24, A19, A25, PARTFUN1:5; ::_thesis: verum
end;
consider A being LINE of IPP such that
A27: p on A and
A28: q on A by INCPROJ:def_5;
consider c1 being POINT of IPP such that
A29: c1 on K and
A30: c1 on A by INCPROJ:def_9;
reconsider c2 = (IncProj (K,p,L)) . c1 as Element of the Points of IPP by A1, A2, A29, Th19;
A31: c2 on L by A1, A2, A29, Th20;
then reconsider c3 = (IncProj (L,q,R)) . c2 as POINT of IPP by A3, A4, Th19;
A32: c3 on R by A3, A4, A31, Th20;
consider a1 being POINT of IPP such that
A33: a1 on K and
A34: c1 <> a1 and
A35: c <> a1 by Th8;
reconsider a2 = (IncProj (K,p,L)) . a1 as POINT of IPP by A1, A2, A33, Th19;
A36: a2 on L by A1, A2, A33, Th20;
then reconsider a3 = (IncProj (L,q,R)) . a2 as POINT of IPP by A3, A4, Th19;
A37: a3 on R by A3, A4, A36, Th20;
A38: not a3 on K
proof
assume a3 on K ; ::_thesis: contradiction
then A39: c = a3 by A5, A7, A8, A37, INCPROJ:def_4;
ex C being LINE of IPP st
( q on C & c on C ) by INCPROJ:def_5;
then (IncProj (L,q,R)) . c = a3 by A3, A4, A6, A7, A39, Def1;
then A40: c = a2 by A3, A4, A6, A36, Th23;
ex D being LINE of IPP st
( p on D & c on D ) by INCPROJ:def_5;
then (IncProj (K,p,L)) . c = a2 by A1, A2, A5, A6, A40, Def1;
hence contradiction by A1, A2, A5, A33, A35, Th23; ::_thesis: verum
end;
consider B being LINE of IPP such that
A41: ( a1 on B & a3 on B ) by INCPROJ:def_5;
consider o being POINT of IPP such that
A42: o on A and
A43: o on B by INCPROJ:def_9;
A44: not a1 on R by A5, A7, A8, A33, A35, INCPROJ:def_4;
A45: ( not o on K & not o on R )
proof
A46: now__::_thesis:_not_o_on_R
assume A47: o on R ; ::_thesis: contradiction
then A48: o = a3 by A37, A41, A43, A44, INCPROJ:def_4;
consider A2 being LINE of IPP such that
A49: q on A2 and
A50: c2 on A2 and
A51: c3 on A2 by A3, A4, A31, A32, Def1;
ex A1 being LINE of IPP st
( p on A1 & c1 on A1 & c2 on A1 ) by A1, A2, A29, A31, Def1;
then c2 on A by A1, A27, A29, A30, INCPROJ:def_4;
then A = A2 by A3, A28, A31, A49, A50, INCPROJ:def_4;
then o = c3 by A4, A42, A32, A47, A49, A51, INCPROJ:def_4;
then c2 = a2 by A3, A4, A36, A31, A48, Th23;
hence contradiction by A1, A2, A29, A33, A34, Th23; ::_thesis: verum
end;
A52: now__::_thesis:_not_o_on_K
assume A53: o on K ; ::_thesis: contradiction
then o = c1 by A1, A27, A29, A30, A42, INCPROJ:def_4;
hence contradiction by A33, A34, A41, A43, A38, A53, INCPROJ:def_4; ::_thesis: verum
end;
assume ( o on K or o on R ) ; ::_thesis: contradiction
hence contradiction by A52, A46; ::_thesis: verum
end;
assume A54: p <> q ; ::_thesis: ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
A55: now__::_thesis:_(_L_<>_R_&_K_<>_L_implies_ex_o_being_POINT_of_IPP_st_
(_not_o_on_K_&_not_o_on_R_&_(IncProj_(L,q,R))_*_(IncProj_(K,p,L))_=_IncProj_(K,o,R)_)_)
assume that
A56: L <> R and
K <> L ; ::_thesis: ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
A57: X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) )
assume A58: e in X ; ::_thesis: e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
then reconsider e = e as POINT of IPP by A9;
A59: ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A58;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A59, Def1; ::_thesis: verum
end;
A60: for x being POINT of IPP st x in X holds
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
proof
let x be Element of the Points of IPP; ::_thesis: ( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x )
assume A61: x in X ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
A62: now__::_thesis:_(_x_=_c_implies_((IncProj_(L,q,R))_*_(IncProj_(K,p,L)))_._x_=_(IncProj_(K,o,R))_._x_)
assume A63: x = c ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = (IncProj (L,q,R)) . ((IncProj (K,p,L)) . c) by A57, A61, FUNCT_1:12;
then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = (IncProj (L,q,R)) . c by A1, A2, A5, A6, Th24;
then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = c by A3, A4, A6, A7, Th24;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A5, A7, A45, A63, Th24; ::_thesis: verum
end;
A64: now__::_thesis:_(_x_<>_c1_&_x_<>_c_&_x_<>_a1_implies_((IncProj_(L,q,R))_*_(IncProj_(K,p,L)))_._x_=_(IncProj_(K,o,R))_._x_)
assume that
x <> c1 and
A65: x <> c and
x <> a1 ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
proof
A66: a2 <> a3
proof
assume a2 = a3 ; ::_thesis: contradiction
then A67: (IncProj (K,p,L)) . a1 = c by A6, A7, A36, A37, A56, INCPROJ:def_4;
(IncProj (K,p,L)) . c = c by A1, A2, A5, A6, Th24;
hence contradiction by A1, A2, A5, A33, A35, A67, Th23; ::_thesis: verum
end;
A68: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (L,q,R)) . ((IncProj (K,p,L)) . x) by A57, A61, FUNCT_1:12;
A69: a2 <> c
proof
assume A70: a2 = c ; ::_thesis: contradiction
(IncProj (K,p,L)) . c = c by A1, A2, A5, A6, Th24;
hence contradiction by A1, A2, A5, A33, A35, A70, Th23; ::_thesis: verum
end;
A71: a3 on R by A3, A4, A36, Th20;
A72: dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
then A73: x on K by A1, A2, A57, A61, Def1;
then reconsider y = (IncProj (K,p,L)) . x as POINT of IPP by A1, A2, Th19;
A74: y on L by A1, A2, A73, Th20;
then reconsider z = (IncProj (L,q,R)) . y as POINT of IPP by A3, A4, Th19;
consider B3 being LINE of IPP such that
A75: ( p on B3 & x on B3 & y on B3 ) by A1, A2, A73, A74, Def1;
x on K by A1, A2, A57, A61, A72, Def1;
then A76: c <> y by A1, A5, A65, A75, INCPROJ:def_4;
consider A1 being LINE of IPP such that
A77: q on A1 and
A78: ( a2 on A1 & a3 on A1 ) by A3, A4, A36, A37, Def1;
A79: {a2,a3,q} on A1 by A77, A78, INCSP_1:2;
A80: z on R by A3, A4, A74, Th20;
then consider B1 being LINE of IPP such that
A81: ( q on B1 & y on B1 & z on B1 ) by A3, A4, A74, Def1;
x on K by A1, A2, A57, A61, A72, Def1;
then A82: {x,c,a1} on K by A5, A33, INCSP_1:2;
consider A3 being Element of the Lines of IPP such that
A83: p on A3 and
A84: a1 on A3 and
A85: a2 on A3 by A1, A2, A33, A36, Def1;
A86: {a2,p,a1} on A3 by A83, A84, A85, INCSP_1:2;
A1 <> A3
proof
assume A1 = A3 ; ::_thesis: contradiction
then A = A3 by A54, A27, A28, A77, A83, INCPROJ:def_4;
hence contradiction by A1, A29, A30, A33, A34, A83, A84, INCPROJ:def_4; ::_thesis: verum
end;
then A87: A1,L,A3 are_mutually_different by A2, A3, A77, A83, ZFMISC_1:def_5;
A88: {a2,y,c} on L by A6, A36, A74, INCSP_1:2;
A89: {p,y,x} on B3 by A75, INCSP_1:2;
z on R by A3, A4, A74, Th20;
then A90: {a3,z,c} on R by A7, A71, INCSP_1:2;
A91: ( {p,o,q} on A & {a3,o,a1} on B ) by A27, A28, A41, A42, A43, INCSP_1:2;
A92: a2 <> p by A1, A2, A33, Th20;
{y,z,q} on B1 by A81, INCSP_1:2;
then consider O being LINE of IPP such that
A93: {o,z,x} on O by A69, A66, A76, A88, A79, A86, A89, A91, A82, A90, A87, A92, Th12;
A94: o on O by A93, INCSP_1:2;
( x on O & z on O ) by A93, INCSP_1:2;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A45, A73, A80, A94, A68, Def1; ::_thesis: verum
end;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x ; ::_thesis: verum
end;
A95: now__::_thesis:_(_x_=_c1_implies_((IncProj_(L,q,R))_*_(IncProj_(K,p,L)))_._x_=_(IncProj_(K,o,R))_._x_)
assume A96: x = c1 ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
proof
A97: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c1 = c3 by A57, A61, A96, FUNCT_1:12;
consider A2 being LINE of IPP such that
A98: ( q on A2 & c2 on A2 ) and
A99: c3 on A2 by A3, A4, A31, A32, Def1;
ex A1 being Element of the Lines of IPP st
( p on A1 & c1 on A1 & c2 on A1 ) by A1, A2, A29, A31, Def1;
then c2 on A by A1, A27, A29, A30, INCPROJ:def_4;
then A = A2 by A3, A28, A31, A98, INCPROJ:def_4;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A29, A30, A42, A32, A45, A96, A97, A99, Def1; ::_thesis: verum
end;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x ; ::_thesis: verum
end;
now__::_thesis:_(_x_=_a1_implies_((IncProj_(L,q,R))_*_(IncProj_(K,p,L)))_._x_=_(IncProj_(K,o,R))_._x_)
assume A100: x = a1 ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . a1 = a3 by A57, A61, FUNCT_1:12;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A33, A37, A41, A43, A45, A100, Def1; ::_thesis: verum
end;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A62, A95, A64; ::_thesis: verum
end;
A101: dom (IncProj (K,o,R)) c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom (IncProj (K,o,R)) or e in X )
assume A102: e in dom (IncProj (K,o,R)) ; ::_thesis: e in X
then reconsider e = e as POINT of IPP ;
e on K by A45, A102, Def1;
hence e in X by A9; ::_thesis: verum
end;
X c= dom (IncProj (K,o,R))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom (IncProj (K,o,R)) )
assume A103: e in X ; ::_thesis: e in dom (IncProj (K,o,R))
then reconsider e = e as POINT of IPP by A9;
ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A103;
hence e in dom (IncProj (K,o,R)) by A45, Def1; ::_thesis: verum
end;
then A104: X = dom (IncProj (K,o,R)) by A101, XBOOLE_0:def_10;
A105: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X )
assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; ::_thesis: e in X
then A106: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
then reconsider e = e as POINT of IPP ;
e on K by A1, A2, A106, Def1;
hence e in X by A9; ::_thesis: verum
end;
then X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A57, XBOOLE_0:def_10;
hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A45, A60, A104, A105, PARTFUN1:5; ::_thesis: verum
end;
now__::_thesis:_(_K_=_L_implies_ex_q,_o_being_POINT_of_IPP_st_
(_not_o_on_K_&_not_o_on_R_&_(IncProj_(L,q,R))_*_(IncProj_(K,p,L))_=_IncProj_(K,o,R)_)_)
A107: X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) )
assume A108: e in X ; ::_thesis: e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
then reconsider e = e as Element of the Points of IPP by A9;
A109: ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A108;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A109, Def1; ::_thesis: verum
end;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X )
assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; ::_thesis: e in X
then A110: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
then reconsider e = e as POINT of IPP ;
e on K by A1, A2, A110, Def1;
hence e in X by A9; ::_thesis: verum
end;
then A111: X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A107, XBOOLE_0:def_10;
A112: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4;
assume A113: K = L ; ::_thesis: ex q, o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
A114: X c= dom (IncProj (K,q,R))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom (IncProj (K,q,R)) )
assume A115: e in X ; ::_thesis: e in dom (IncProj (K,q,R))
then reconsider e = e as POINT of IPP by A9;
ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A115;
hence e in dom (IncProj (K,q,R)) by A3, A4, A113, Def1; ::_thesis: verum
end;
A116: for x being POINT of IPP st x in X holds
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x
proof
let x be Element of the Points of IPP; ::_thesis: ( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x )
assume x in X ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x
then ( x on K & ((IncProj (K,q,R)) * (IncProj (K,p,K))) . x = (IncProj (K,q,R)) . ((IncProj (K,p,K)) . x) ) by A3, A4, A113, A107, A114, Def1, FUNCT_1:12;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x by A1, A113, Th18; ::_thesis: verum
end;
take q = q; ::_thesis: ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
dom (IncProj (K,q,R)) c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom (IncProj (K,q,R)) or e in X )
assume A117: e in dom (IncProj (K,q,R)) ; ::_thesis: e in X
then reconsider e = e as POINT of IPP ;
e on K by A3, A4, A113, A117, Def1;
hence e in X by A9; ::_thesis: verum
end;
then X = dom (IncProj (K,q,R)) by A114, XBOOLE_0:def_10;
hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A3, A4, A113, A111, A116, A112, PARTFUN1:5; ::_thesis: verum
end;
hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A12, A55; ::_thesis: verum
end;
now__::_thesis:_(_p_=_q_implies_ex_o_being_POINT_of_IPP_st_
(_not_o_on_K_&_not_o_on_R_&_(IncProj_(L,q,R))_*_(IncProj_(K,p,L))_=_IncProj_(K,o,R)_)_)
A118: X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) )
assume A119: e in X ; ::_thesis: e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
then reconsider e = e as POINT of IPP by A9;
A120: ex e9 being Element of the Points of IPP st
( e = e9 & e9 on K ) by A9, A119;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A120, Def1; ::_thesis: verum
end;
assume A121: p = q ; ::_thesis: ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
A122: X c= dom (IncProj (K,p,R))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in dom (IncProj (K,p,R)) )
assume A123: e in X ; ::_thesis: e in dom (IncProj (K,p,R))
then reconsider e = e as POINT of IPP by A9;
ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A123;
hence e in dom (IncProj (K,p,R)) by A1, A4, A121, Def1; ::_thesis: verum
end;
A124: for x being POINT of IPP st x in X holds
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x
proof
let x be POINT of IPP; ::_thesis: ( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x )
assume A125: x in X ; ::_thesis: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x
then A126: ((IncProj (L,p,R)) * (IncProj (K,p,L))) . x = (IncProj (L,p,R)) . ((IncProj (K,p,L)) . x) by A121, A118, FUNCT_1:12;
A127: x on K by A1, A4, A121, A122, A125, Def1;
then reconsider y = (IncProj (K,p,L)) . x as POINT of IPP by A1, A2, Th19;
A128: y on L by A1, A2, A127, Th20;
then reconsider z = (IncProj (L,p,R)) . y as POINT of IPP by A2, A4, A121, Th19;
consider A being LINE of IPP such that
A129: ( p on A & y on A ) by INCPROJ:def_5;
A130: z on R by A2, A4, A121, A128, Th20;
then consider C being LINE of IPP such that
A131: ( p on C & y on C ) and
A132: z on C by A2, A4, A121, A128, Def1;
A133: A = C by A2, A128, A129, A131, INCPROJ:def_4;
consider B being LINE of IPP such that
A134: p on B and
A135: x on B and
A136: y on B by A1, A2, A127, A128, Def1;
A = B by A2, A128, A129, A134, A136, INCPROJ:def_4;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x by A1, A4, A121, A127, A126, A134, A135, A130, A132, A133, Def1; ::_thesis: verum
end;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X )
assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; ::_thesis: e in X
then A137: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
then reconsider e = e as POINT of IPP ;
e on K by A1, A2, A137, Def1;
hence e in X by A9; ::_thesis: verum
end;
then A138: X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A118, XBOOLE_0:def_10;
A139: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4;
dom (IncProj (K,p,R)) c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in dom (IncProj (K,p,R)) or e in X )
assume A140: e in dom (IncProj (K,p,R)) ; ::_thesis: e in X
then reconsider e = e as POINT of IPP ;
e on K by A1, A4, A121, A140, Def1;
hence e in X by A9; ::_thesis: verum
end;
then X = dom (IncProj (K,p,R)) by A122, XBOOLE_0:def_10;
hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A1, A4, A121, A138, A124, A139, PARTFUN1:5; ::_thesis: verum
end;
hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) by A11; ::_thesis: verum
end;