projred1.miz
begin
reserve IPP for
IncProjSp;
reserve a,b,c,d,p,q,o,r,s,t,u,v,w,x,y for
POINT of IPP;
reserve A,B,C,D,L,P,Q,S for
LINE of IPP;
theorem ::
PROJRED1:1
Th1: ex a st not a
on A
proof
consider p, L such that
A1: not p
on L by
INCPROJ:def 6;
now
assume
A2: A
<> L;
now
consider q, r, s 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 thesis;
end;
hence thesis;
end;
hence thesis by
A1;
end;
theorem ::
PROJRED1:2
Th2: ex A st not a
on A
proof
consider p, L such that
A1: not p
on L by
INCPROJ:def 6;
now
now
consider q, r, s 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;
A6:
now
consider S such that
A7: s
on S & p
on S by
INCPROJ:def 5;
assume a
<> s;
then not a
on S by
A1,
A5,
A4,
A7,
INCPROJ:def 4;
hence thesis;
end;
now
consider S such that
A8: q
on S & p
on S by
INCPROJ:def 5;
assume a
<> q;
then not a
on S by
A1,
A5,
A3,
A8,
INCPROJ:def 4;
hence thesis;
end;
hence thesis by
A2,
A6;
end;
hence thesis;
end;
hence thesis;
end;
theorem ::
PROJRED1:3
Th3: A
<> B implies ex a, b st a
on A & not a
on B & b
on B & not b
on A
proof
consider a, b, d 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 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;
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 thesis by
A2,
A4,
A6;
end;
theorem ::
PROJRED1:4
a
<> b implies ex A, B st a
on A & not a
on B & b
on B & not b
on A
proof
consider Q such that
A1: a
on Q & b
on Q by
INCPROJ:def 5;
consider q such that
A2: not q
on Q by
Th1;
consider B such that
A3: b
on B and
A4: q
on B by
INCPROJ:def 5;
assume
A5: a
<> b;
then
A6: not a
on B by
A1,
A2,
A3,
A4,
INCPROJ:def 4;
consider A 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 thesis by
A7,
A3,
A6;
end;
theorem ::
PROJRED1:5
ex A, B, C st a
on A & a
on B & a
on C & A
<> B & B
<> C & C
<> A
proof
consider Q such that
A1: not a
on Q by
Th2;
consider b1,b2,b3 be
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 be
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 be
LINE of IPP such that
A10: a
on B2 & b2
on B2 by
INCPROJ:def 5;
consider B3 be
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 thesis by
A8,
A10,
A11,
A12,
A9;
end;
theorem ::
PROJRED1:6
ex a st not a
on A & not a
on B
proof
A1: A
<> B implies ex a st not a
on A & not a
on B
proof
assume A
<> B;
then
consider a, b 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 such that
A4: a
on C & b
on C by
INCPROJ:def 5;
consider c,d,e be
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 thesis;
end;
A
= B implies ex a st not a
on A & not a
on B
proof
assume
A6: A
= B;
ex a st not a
on A by
Th1;
hence thesis by
A6;
end;
hence thesis by
A1;
end;
theorem ::
PROJRED1:7
Th7: ex a st a
on A
proof
consider a, b, c 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;
thus thesis by
A1;
end;
theorem ::
PROJRED1:8
Th8: ex c st c
on A & c
<> a & c
<> b
proof
consider p, q, r 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 thesis by
A2;
end;
theorem ::
PROJRED1:9
ex A st not a
on A & not b
on A
proof
now
consider A such that
A1: a
on A & b
on A by
INCPROJ:def 5;
consider c such that
A2: c
on A & c
<> a & c
<> b by
Th8;
consider d such that
A3: not d
on A by
Th1;
consider B 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 thesis;
end;
hence thesis;
end;
theorem ::
PROJRED1:10
Th10: 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
proof
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;
assume not thesis;
then P
= B by
A2,
A4,
INCPROJ:def 4;
hence contradiction by
A1,
A3,
INCPROJ:def 4;
end;
theorem ::
PROJRED1:11
Th11:
{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
proof
assume
A1:
{a, b, c}
on A;
then
A2: c
on A by
INCSP_1: 2;
a
on A & b
on A by
A1,
INCSP_1: 2;
hence thesis by
A2,
INCSP_1: 2;
end;
theorem ::
PROJRED1:12
Th12: for IPP be
Desarguesian
IncProjSp holds for o,b1,a1,b2,a2,b3,a3,r,s,t be
POINT of IPP, C1,C2,C3,A1,A2,A3,B1,B2,B3 be
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_distinct & o
<> a3 & o
<> b1 & o
<> b2 & a2
<> b2 holds ex O be
LINE of IPP st
{r, s, t}
on O
proof
let IPP be
Desarguesian
IncProjSp;
let o,b1,a1,b2,a2,b3,a3,r,s,t be
POINT of IPP, C1,C2,C3,A1,A2,A3,B1,B2,B3 be
LINE of IPP;
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_distinct and
A11: o
<> a3 and
A12: o
<> b1 and
A13: o
<> b2 and
A14: a2
<> b2;
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
assume that o
<> b3 and o
<> a1 and o
<> a2 and
A31: a1
= b1;
A32:
now
A33: b3
on B2 by
A8,
INCSP_1: 2;
consider O be
LINE of IPP such that
A34: t
on O & s
on O by
INCPROJ:def 5;
assume
A35: a3
<> b3;
take 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;
end;
now
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;
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;
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;
end;
hence thesis by
A32;
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
assume that
A67: o
<> b3 and
A68: o
<> a1 and
A69: o
= a2;
A70:
now
assume
A71: a1
= b1;
A72:
now
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;
take 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;
end;
now
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 be
LINE of IPP such that
A86: t
on O & s
on O by
INCPROJ:def 5;
assume
A87: a3
<> b3;
take 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;
end;
hence thesis by
A72;
end;
now
assume
A90: a1
<> b1;
A91:
now
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 be
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;
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;
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;
end;
now
assume a3
<> b3;
take 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;
end;
hence thesis by
A91;
end;
hence thesis by
A70;
end;
A101: C3
<> C1 by
A10,
ZFMISC_1:def 5;
A102: a2
on C2 by
A2,
INCSP_1: 2;
A103:
now
assume that
A104: o
<> b3 and
A105: o
= a1;
A106:
now
A107:
now
A108: B2
<> C3 by
A12,
A54,
A56,
A64,
A27,
A101,
INCPROJ:def 4;
assume
A109: a3
= b3;
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 be
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;
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;
end;
assume
A116: o
<> a2;
now
assume a3
<> b3;
take 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;
end;
hence thesis by
A107;
end;
now
assume o
= a2;
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 be
LINE of IPP such that
A120: t
on O & s
on O by
INCPROJ:def 5;
take 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;
end;
hence thesis by
A106;
end;
A121: C1
<> B3 by
A13,
A54,
A22,
A58,
A65,
A55,
INCPROJ:def 4;
A122:
now
assume
A123: o
= b3;
A124:
now
assume
A125: a1
= o;
A126:
now
assume o
= a2;
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 be
LINE of IPP such that
A129: t
on O & s
on O by
INCPROJ:def 5;
take 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;
end;
now
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;
then
A131: C2
= A3 by
A22,
A102,
A57,
A24,
A125,
INCPROJ:def 4;
take 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;
end;
hence thesis by
A126;
end;
now
assume
A132: a1
<> o;
A133:
now
assume
A134: o
= a2;
then
A135: A1
= C3 by
A11,
A64,
A60,
A17,
A63,
INCPROJ:def 4;
take 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;
end;
now
assume o
<> a2;
take 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;
end;
hence thesis by
A133;
end;
hence thesis by
A124;
end;
now
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 be
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;
take 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;
end;
hence thesis by
A1,
A2,
A3,
A4,
A5,
A6,
A7,
A8,
A9,
A10,
A11,
A12,
A13,
A14,
A122,
A103,
A66,
A30,
INCPROJ:def 13;
end;
Lm1: (ex o 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_distinct implies ex p, q, r, s st p
on B & q
on B & r
on B & s
on B & (p,q,r,s)
are_mutually_distinct
proof
assume that
A1: ex o 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_distinct ;
consider o such that
A7: o
on A and
A8: o
on B by
A1;
now
assume A
<> B;
then
consider x, y 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 such that
A13: x
on C and
A14: y
on C by
INCPROJ:def 5;
consider w such that
A15: w
on C and
A16: w
<> x and
A17: w
<> y by
Th8;
A18:
now
A19: not w
on B by
A10,
A11,
A13,
A14,
A15,
A17,
INCPROJ:def 4;
let u1,u2,v1,v2 be
POINT of IPP, D1,D2 be
LINE of IPP such 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;
A28: D1
<> A by
A9,
A12,
A13,
A14,
A15,
A16,
A22,
INCPROJ:def 4;
assume
A29: u1
<> u2;
assume v1
= v2;
then D1
= D2 by
A21,
A22,
A24,
A25,
A27,
A19,
INCPROJ:def 4;
hence contradiction by
A20,
A23,
A26,
A29,
A28,
INCPROJ:def 4;
end;
A30:
now
let u;
assume
A31: u
on A;
A32:
now
assume that u
<> o and
A33: x
<> u;
consider D such that
A34: w
on D & u
on D by
INCPROJ:def 5;
not x
on D
proof
assume not thesis;
then u
on C by
A13,
A15,
A16,
A34,
INCPROJ:def 4;
hence contradiction by
A9,
A12,
A13,
A14,
A31,
A33,
INCPROJ:def 4;
end;
then
consider v 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, D;
thus v
on B & w
on D & u
on D & v
on D by
A34,
A35;
end;
now
consider D such that
A36: w
on D & u
on D by
INCPROJ:def 5;
assume
A37: u
= o;
take v = o, D;
thus v
on B & w
on D & u
on D & v
on D by
A8,
A37,
A36;
end;
hence ex v, D st v
on B & w
on D & u
on D & v
on D by
A11,
A13,
A14,
A15,
A32;
end;
then
consider p be
POINT of IPP, D1 be
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 be
POINT of IPP, D3 be
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 be
POINT of IPP, D2 be
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 be
POINT of IPP, D4 be
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_distinct by
A50,
A49,
A46,
A48,
A47,
ZFMISC_1:def 6;
hence thesis by
A38,
A42,
A40,
A44;
end;
hence thesis by
A2,
A3,
A4,
A5,
A6;
end;
theorem ::
PROJRED1:13
Th13: (ex A, a, b, c, d st a
on A & b
on A & c
on A & d
on A & (a,b,c,d)
are_mutually_distinct ) implies for B holds ex p, q, r, s st p
on B & q
on B & r
on B & s
on B & (p,q,r,s)
are_mutually_distinct
proof
given A, a, b, c, d such that
A1: a
on A & b
on A & c
on A & d
on A & (a,b,c,d)
are_mutually_distinct ;
let B;
consider x such that
A2: x
on A by
Th7;
consider y such that
A3: y
on B by
Th7;
consider C such that
A4: x
on C and
A5: y
on C by
INCPROJ:def 5;
ex p1,q1,r1,s1 be
POINT of IPP st p1
on C & q1
on C & r1
on C & s1
on C & (p1,q1,r1,s1)
are_mutually_distinct by
A1,
A2,
A4,
Lm1;
hence thesis by
A3,
A5,
Lm1;
end;
reserve IPP for
Fanoian
IncProjSp;
reserve a,b,c,d,p,q,r,s for
POINT of IPP;
reserve A,B,C,D,L,Q,R,S for
LINE of IPP;
Lm2: ex p, q, r, s, a, b, c, A, B, C, Q, L, R, S, D, d 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_distinct & d
on A & (c,d,p,q)
are_mutually_distinct
proof
consider r, A such that
A1: not r
on A by
INCPROJ:def 6;
consider p, q, c 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 such that
A8: r
on B and
A9: c
on B by
INCPROJ:def 5;
consider s such that
A10: s
on B and
A11: s
<> r and
A12: s
<> c by
Th8;
consider L such that
A13: p
on L and
A14: s
on L by
INCPROJ:def 5;
consider Q 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 not thesis;
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;
end;
then
consider a 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 such that
A23: q
on R and
A24: s
on R by
INCPROJ:def 5;
consider S 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 not thesis;
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;
end;
A34: not p
on R
proof
assume not thesis;
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;
end;
then not c
on R by
A3,
A5,
A6,
A7,
A23,
INCPROJ:def 4;
then
consider b 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 thesis;
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;
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 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 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 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_distinct 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_distinct by
A25,
A34,
A45,
A54,
A56,
A43,
A57,
A47,
ZFMISC_1:def 6;
hence thesis by
A39,
A17,
A32,
A33,
A34,
A19,
A30,
A28,
A22,
A44,
A37,
A41,
A52,
A40,
A53,
A54,
A55,
A56,
A49,
A58;
end;
theorem ::
PROJRED1:14
ex p, q, r, s, a, b, c, A, B, C, Q, L, R, S, D 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
ex p, q, r, s, a, b, c, A, B, C, Q, L, R, S, D, d 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_distinct & d
on A & (c,d,p,q)
are_mutually_distinct by
Lm2;
hence thesis;
end;
theorem ::
PROJRED1:15
ex a, A, B, C, D st a
on A & a
on B & a
on C & a
on D & (A,B,C,D)
are_mutually_distinct
proof
consider p, q, r, s, a, b, c, A, B, C, Q, L, R, S, D, d 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_distinct and d
on A and (c,d,p,q)
are_mutually_distinct by
Lm2;
A5: b
on C by
A2,
INCSP_1: 1;
b
on S & b
on R by
A1,
INCSP_1: 2;
hence thesis by
A3,
A4,
A5;
end;
theorem ::
PROJRED1:16
Th16: ex a, b, c, d, A st a
on A & b
on A & c
on A & d
on A & (a,b,c,d)
are_mutually_distinct
proof
consider p, q, r, s, a, b, c, A, B, C, Q, L, R, S, D, d 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_distinct and
A2: d
on A & (c,d,p,q)
are_mutually_distinct by
Lm2;
A3: q
on A by
A1,
INCSP_1: 2;
c
on A & p
on A by
A1,
INCSP_1: 2;
hence thesis by
A2,
A3;
end;
theorem ::
PROJRED1:17
ex p, q, r, s st p
on B & q
on B & r
on B & s
on B & (p,q,r,s)
are_mutually_distinct
proof
ex a, b, c, d, A st a
on A & b
on A & c
on A & d
on A & (a,b,c,d)
are_mutually_distinct by
Th16;
hence thesis by
Th13;
end;
reserve IPP for
Desarguesian
2-dimensional
IncProjSp;
reserve c,p,q,x,y for
POINT of IPP;
reserve A,B,C,D,K,L,R,X for
LINE of IPP;
reserve f for
PartFunc of the
Points of IPP, the
Points of IPP;
definition
let IPP, K, L, p;
assume that
A1: not p
on K and
A2: not p
on L;
::
PROJRED1:def1
func
IncProj (K,p,L) ->
PartFunc of the
Points of IPP, the
Points of IPP means
:
Def1: (
dom it )
c= the
Points of IPP & (for x holds x
in (
dom it ) iff x
on K) & for x, y st x
on K & y
on L holds (it
. x)
= y iff ex X st p
on X & x
on X & y
on X;
existence
proof
defpred
P[
object,
object] means ex x, y st x
= $1 & y
= $2 & x
on K & y
on L & ex X st p
on X & x
on X & y
on X;
set XX = the
Points of IPP;
A3: for x,y1,y2 be
object st x
in XX &
P[x, y1] &
P[x, y2] holds y1
= y2
proof
let x,y1,y2 be
object such that
A4: x
in XX and
A5:
P[x, y1] and
A6:
P[x, y2];
reconsider x as
POINT of IPP by
A4;
reconsider y1, y2 as
POINT of IPP by
A5,
A6;
consider A1 be
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 thesis by
A2,
A5,
A6,
A7,
A9,
INCPROJ:def 4;
end;
A10: for x,y be
object st x
in XX &
P[x, y] holds y
in XX;
consider f such that
A11: for x be
object holds x
in (
dom f) iff x
in XX & ex y be
object st
P[x, y] and
A12: for x be
object st x
in (
dom f) holds
P[x, (f
. x)] from
PARTFUN1:sch 2(
A10,
A3);
take f;
thus (
dom f)
c= the
Points of IPP;
thus
A13: x
in (
dom f) iff x
on K
proof
A14: x
on K implies x
in (
dom f)
proof
consider X be
LINE of IPP such that
A15: p
on X & x
on X by
INCPROJ:def 5;
assume
A16: x
on K;
ex y st y
on L & y
on X by
INCPROJ:def 9;
hence thesis by
A11,
A16,
A15;
end;
x
in (
dom f) implies x
on K
proof
assume x
in (
dom f);
then
P[x, (f
. x)] by
A12;
hence thesis;
end;
hence thesis by
A14;
end;
let x, y;
assume that
A17: x
on K and
A18: y
on L;
A19: (f
. x)
= y implies ex X st p
on X & x
on X & y
on X
proof
x
in (
dom f) by
A13,
A17;
then
A20:
P[x, (f
. x)] by
A12;
assume (f
. x)
= y;
hence thesis by
A20;
end;
(ex X st p
on X & x
on X & y
on X) implies (f
. x)
= y
proof
x
in (
dom f) by
A13,
A17;
then
A21:
P[x, (f
. x)] by
A12;
assume ex X st p
on X & x
on X & y
on X;
hence thesis by
A3,
A18,
A21;
end;
hence (f
. x)
= y iff ex X st p
on X & x
on X & y
on X by
A19;
end;
uniqueness
proof
let f1,f2 be
PartFunc of the
Points of IPP, the
Points of IPP such that (
dom f1)
c= the
Points of IPP and
A22: for x holds x
in (
dom f1) iff x
on K and
A23: for x, y st x
on K & y
on L holds (f1
. x)
= y iff ex X st p
on X & x
on X & y
on X and (
dom f2)
c= the
Points of IPP and
A24: for x holds x
in (
dom f2) iff x
on K and
A25: for x, y st x
on K & y
on L holds (f2
. x)
= y iff ex X st p
on X & x
on X & y
on X;
for x be
object holds x
in (
dom f1) iff x
in (
dom f2) by
A24,
A22;
then
A26: (
dom f1)
= (
dom f2) by
TARSKI: 2;
for x be
POINT of IPP st x
in (
dom f1) holds (f1
. x)
= (f2
. x)
proof
let x be
POINT of IPP;
consider A2 be
LINE of IPP such that
A27: p
on A2 & x
on A2 by
INCPROJ:def 5;
consider y2 be
POINT of IPP such that
A28: y2
on A2 & y2
on L by
INCPROJ:def 9;
assume x
in (
dom f1);
then
A29: x
on K by
A22;
then (f2
. x)
= y2 by
A25,
A27,
A28;
hence thesis by
A23,
A29,
A27,
A28;
end;
hence thesis by
A26,
PARTFUN1: 5;
end;
end
theorem ::
PROJRED1:18
Th18: not p
on K implies for x st x
on K holds ((
IncProj (K,p,K))
. x)
= x
proof
assume
A1: not p
on K;
let x;
A2: ex X st p
on X & x
on X by
INCPROJ:def 5;
assume x
on K;
hence thesis by
A1,
A2,
Def1;
end;
theorem ::
PROJRED1:19
Th19: not p
on K & not p
on L & x
on K implies ((
IncProj (K,p,L))
. x) is
POINT of IPP
proof
assume ( not p
on K) & not p
on L & x
on K;
then x
in (
dom (
IncProj (K,p,L))) by
Def1;
hence thesis by
PARTFUN1: 4;
end;
theorem ::
PROJRED1:20
Th20: not p
on K & not p
on L & x
on K & y
= ((
IncProj (K,p,L))
. x) implies y
on L
proof
assume
A1: ( not p
on K) & not p
on L & x
on K & y
= ((
IncProj (K,p,L))
. x);
consider X such that
A2: p
on X & x
on X by
INCPROJ:def 5;
ex z be
POINT of IPP st z
on L & z
on X by
INCPROJ:def 9;
hence thesis by
A1,
A2,
Def1;
end;
theorem ::
PROJRED1:21
not p
on K & not p
on L & y
in (
rng (
IncProj (K,p,L))) implies y
on L
proof
assume that
A1: ( not p
on K) & not p
on L and
A2: y
in (
rng (
IncProj (K,p,L)));
consider x be
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 thesis by
A1,
A4,
Th20;
end;
theorem ::
PROJRED1:22
Th22: 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)))
proof
assume that
A1: ( not p
on K) & not p
on L and
A2: ( not q
on L) & not q
on R;
for x be
object holds x
in (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L)))) iff x
in (
dom (
IncProj (K,p,L)))
proof
let x be
object;
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)));
then
reconsider x9 = x as
POINT of IPP;
consider A such that
A4: x9
on A & p
on A by
INCPROJ:def 5;
consider y 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 thesis by
A3,
A7,
FUNCT_1: 11;
end;
hence thesis by
FUNCT_1: 11;
end;
hence (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))))
= (
dom (
IncProj (K,p,L))) by
TARSKI: 2;
for x be
object st x
in (
dom (
IncProj (L,q,R))) holds x
in (
rng (
IncProj (K,p,L)))
proof
let x be
object;
assume
A8: x
in (
dom (
IncProj (L,q,R)));
thus x
in (
rng (
IncProj (K,p,L)))
proof
reconsider x9 = x as
POINT of IPP by
A8;
A9: x9
on L by
A2,
A8,
Def1;
ex y st y
in (
dom (
IncProj (K,p,L))) & x9
= ((
IncProj (K,p,L))
. y)
proof
consider A such that
A10: x9
on A & p
on A by
INCPROJ:def 5;
consider y be
POINT of IPP such that
A11: y
on A and
A12: y
on K by
INCPROJ:def 9;
take y;
thus y
in (
dom (
IncProj (K,p,L))) by
A1,
A12,
Def1;
thus thesis by
A1,
A9,
A10,
A11,
A12,
Def1;
end;
hence thesis by
FUNCT_1:def 3;
end;
end;
then (
dom (
IncProj (L,q,R)))
c= (
rng (
IncProj (K,p,L)));
hence (
rng ((
IncProj (L,q,R))
* (
IncProj (K,p,L))))
= (
rng (
IncProj (L,q,R))) by
RELAT_1: 28;
end;
theorem ::
PROJRED1:23
Th23: for a1,b1,a2,b2 be
POINT of IPP holds 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
proof
let a1,b1,a2,b2 be
POINT of IPP;
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;
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 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 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 thesis by
A1,
A3,
A4,
A9,
A10,
A13,
INCPROJ:def 4;
end;
theorem ::
PROJRED1:24
Th24: not p
on K & not p
on L & x
on K & x
on L implies ((
IncProj (K,p,L))
. x)
= x
proof
A1: ex A 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;
hence thesis by
A1,
Def1;
end;
reserve X for
set;
theorem ::
PROJRED1:25
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 be
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
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;
defpred
P[
object] means ex k be
POINT of IPP st $1
= k & k
on K;
consider X such that
A9: for x be
object holds x
in X iff x
in the
Points of IPP qua
set &
P[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 f)
= (
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;
(
rng f)
= (
rng (
IncProj (L,q,R))) by
A1,
A2,
A3,
A4,
Th22;
hence thesis by
RELAT_1:def 19;
end;
A11:
now
A12:
now
A13: X
c= (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))))
proof
let e be
object;
assume
A14: e
in X;
then
reconsider e as
Element of the
Points of IPP by
A9;
A15: ex e9 be
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 thesis by
A1,
A2,
A15,
Def1;
end;
assume
A16: L
= R;
A17: X
c= (
dom (
IncProj (K,p,R)))
proof
let e be
object;
assume
A18: e
in X;
then
reconsider e as
POINT of IPP by
A9;
ex e9 be
POINT of IPP st e
= e9 & e9
on K by
A9,
A18;
hence thesis by
A1,
A2,
A16,
Def1;
end;
A19: for x be
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;
assume
A20: x
in 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 thesis by
A3,
A16,
A21,
Th18;
end;
(
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))))
c= X
proof
let e be
object;
assume e
in (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))));
then
A23: e
in (
dom (
IncProj (K,p,L))) by
A1,
A2,
A3,
A4,
Th22;
then
reconsider e as
POINT of IPP;
e
on K by
A1,
A2,
A23,
Def1;
hence thesis by
A9;
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;
(
dom (
IncProj (K,p,R)))
c= X
proof
let e be
object;
assume
A26: e
in (
dom (
IncProj (K,p,R)));
then
reconsider e as
POINT of IPP;
e
on K by
A1,
A2,
A16,
A26,
Def1;
hence thesis by
A9;
end;
then X
= (
dom (
IncProj (K,p,R))) by
A17,
XBOOLE_0:def 10;
hence thesis by
A1,
A2,
A16,
A24,
A19,
A25,
PARTFUN1: 5;
end;
consider A such that
A27: p
on A and
A28: q
on A by
INCPROJ:def 5;
consider c1 be
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 be
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;
then
A39: c
= a3 by
A5,
A7,
A8,
A37,
INCPROJ:def 4;
ex C 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 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;
end;
consider B such that
A41: a1
on B & a3
on B by
INCPROJ:def 5;
consider o be
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
assume
A47: o
on R;
then
A48: o
= a3 by
A37,
A41,
A43,
A44,
INCPROJ:def 4;
consider A2 be
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 be
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;
end;
A52:
now
assume
A53: o
on K;
then o
= c1 by
A1,
A27,
A29,
A30,
A42,
INCPROJ:def 4;
hence contradiction by
A33,
A34,
A41,
A43,
A38,
A53,
INCPROJ:def 4;
end;
assume not thesis;
hence thesis by
A52,
A46;
end;
assume
A54: p
<> q;
A55:
now
assume that
A56: L
<> R and K
<> L;
A57: X
c= (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))))
proof
let e be
object;
assume
A58: e
in X;
then
reconsider e as
POINT of IPP by
A9;
A59: ex e9 be
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 thesis by
A1,
A2,
A59,
Def1;
end;
A60: for x be
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;
assume
A61: x
in X;
A62:
now
assume
A63: x
= c;
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 thesis by
A5,
A7,
A45,
A63,
Th24;
end;
A64:
now
assume that x
<> c1 and
A65: x
<> c and x
<> a1;
(((
IncProj (L,q,R))
* (
IncProj (K,p,L)))
. x)
= ((
IncProj (K,o,R))
. x)
proof
A66: a2
<> a3
proof
assume a2
= a3;
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;
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;
((
IncProj (K,p,L))
. c)
= c by
A1,
A2,
A5,
A6,
Th24;
hence contradiction by
A1,
A2,
A5,
A33,
A35,
A70,
Th23;
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 be
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 be
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 be
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 be
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;
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;
end;
then
A87: (A1,L,A3)
are_mutually_distinct 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 be
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 thesis by
A45,
A73,
A80,
A94,
A68,
Def1;
end;
hence thesis;
end;
A95:
now
assume
A96: x
= c1;
(((
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 be
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 be
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 thesis by
A29,
A30,
A42,
A32,
A45,
A96,
A97,
A99,
Def1;
end;
hence thesis;
end;
now
assume
A100: x
= a1;
then (((
IncProj (L,q,R))
* (
IncProj (K,p,L)))
. a1)
= a3 by
A57,
A61,
FUNCT_1: 12;
hence thesis by
A33,
A37,
A41,
A43,
A45,
A100,
Def1;
end;
hence thesis by
A62,
A95,
A64;
end;
A101: (
dom (
IncProj (K,o,R)))
c= X
proof
let e be
object;
assume
A102: e
in (
dom (
IncProj (K,o,R)));
then
reconsider e as
POINT of IPP;
e
on K by
A45,
A102,
Def1;
hence thesis by
A9;
end;
X
c= (
dom (
IncProj (K,o,R)))
proof
let e be
object;
assume
A103: e
in X;
then
reconsider e as
POINT of IPP by
A9;
ex e9 be
POINT of IPP st e
= e9 & e9
on K by
A9,
A103;
hence thesis by
A45,
Def1;
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
object;
assume e
in (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))));
then
A106: e
in (
dom (
IncProj (K,p,L))) by
A1,
A2,
A3,
A4,
Th22;
then
reconsider e as
POINT of IPP;
e
on K by
A1,
A2,
A106,
Def1;
hence thesis by
A9;
end;
then X
= (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L)))) by
A57,
XBOOLE_0:def 10;
hence thesis by
A45,
A60,
A104,
A105,
PARTFUN1: 5;
end;
now
A107: X
c= (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))))
proof
let e be
object;
assume
A108: e
in X;
then
reconsider e as
Element of the
Points of IPP by
A9;
A109: ex e9 be
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 thesis by
A1,
A2,
A109,
Def1;
end;
(
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))))
c= X
proof
let e be
object;
assume e
in (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))));
then
A110: e
in (
dom (
IncProj (K,p,L))) by
A1,
A2,
A3,
A4,
Th22;
then
reconsider e as
POINT of IPP;
e
on K by
A1,
A2,
A110,
Def1;
hence thesis by
A9;
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;
A114: X
c= (
dom (
IncProj (K,q,R)))
proof
let e be
object;
assume
A115: e
in X;
then
reconsider e as
POINT of IPP by
A9;
ex e9 be
POINT of IPP st e
= e9 & e9
on K by
A9,
A115;
hence thesis by
A3,
A4,
A113,
Def1;
end;
A116: for x be
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;
assume x
in 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 thesis by
A1,
A113,
Th18;
end;
take q;
(
dom (
IncProj (K,q,R)))
c= X
proof
let e be
object;
assume
A117: e
in (
dom (
IncProj (K,q,R)));
then
reconsider e as
POINT of IPP;
e
on K by
A3,
A4,
A113,
A117,
Def1;
hence thesis by
A9;
end;
then X
= (
dom (
IncProj (K,q,R))) by
A114,
XBOOLE_0:def 10;
hence thesis by
A3,
A4,
A113,
A111,
A116,
A112,
PARTFUN1: 5;
end;
hence thesis by
A12,
A55;
end;
now
A118: X
c= (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))))
proof
let e be
object;
assume
A119: e
in X;
then
reconsider e as
POINT of IPP by
A9;
A120: ex e9 be
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 thesis by
A1,
A2,
A120,
Def1;
end;
assume
A121: p
= q;
A122: X
c= (
dom (
IncProj (K,p,R)))
proof
let e be
object;
assume
A123: e
in X;
then
reconsider e as
POINT of IPP by
A9;
ex e9 be
POINT of IPP st e
= e9 & e9
on K by
A9,
A123;
hence thesis by
A1,
A4,
A121,
Def1;
end;
A124: for x be
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;
assume
A125: x
in 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 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 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 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 thesis by
A1,
A4,
A121,
A127,
A126,
A134,
A135,
A130,
A132,
A133,
Def1;
end;
(
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))))
c= X
proof
let e be
object;
assume e
in (
dom ((
IncProj (L,q,R))
* (
IncProj (K,p,L))));
then
A137: e
in (
dom (
IncProj (K,p,L))) by
A1,
A2,
A3,
A4,
Th22;
then
reconsider e as
POINT of IPP;
e
on K by
A1,
A2,
A137,
Def1;
hence thesis by
A9;
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
object;
assume
A140: e
in (
dom (
IncProj (K,p,R)));
then
reconsider e as
POINT of IPP;
e
on K by
A1,
A4,
A121,
A140,
Def1;
hence thesis by
A9;
end;
then X
= (
dom (
IncProj (K,p,R))) by
A122,
XBOOLE_0:def 10;
hence thesis by
A1,
A4,
A121,
A138,
A124,
A139,
PARTFUN1: 5;
end;
hence thesis by
A11;
end;