:: PROJRED1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: PROJRED1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for IPP being IncProjSp
for A being LINE of IPP holds
not for a being POINT of IPP holds a on A
proof end;

theorem Th2: :: PROJRED1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for IPP being IncProjSp
for a being POINT of IPP holds
not for A being LINE of IPP holds a on A
proof end;

theorem Th3: :: PROJRED1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PROJRED1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PROJRED1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PROJRED1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th7: :: PROJRED1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for IPP being IncProjSp
for A being LINE of IPP ex a being POINT of IPP st a on A
proof end;

theorem Th8: :: PROJRED1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PROJRED1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PROJRED1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PROJRED1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th12: :: PROJRED1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & a on Q & c on Q holds
P <> Q
proof end;

theorem Th13: :: PROJRED1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th14: :: PROJRED1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;

theorem Th15: :: PROJRED1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;

theorem :: PROJRED1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PROJRED1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th18: :: PROJRED1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PROJRED1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let IPP be 2-dimensional Desarguesian IncProjSp;
let K, L be LINE of IPP;
let p be POINT of IPP;
assume A1: ( not p on K & 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 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 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 :: PROJRED1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th21: :: PROJRED1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th22: :: PROJRED1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th23: :: PROJRED1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PROJRED1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th25: :: PROJRED1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th26: :: PROJRED1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th27: :: PROJRED1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PROJRED1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;