:: PROJRED1 semantic presentation

theorem Th1: :: PROJRED1:1
for b1 being IncProjSp
for b2 being LINE of b1 holds
not for b3 being POINT of b1 holds b3 on b2
proof end;

theorem Th2: :: PROJRED1:2
for b1 being IncProjSp
for b2 being POINT of b1 holds
not for b3 being LINE of b1 holds b2 on b3
proof end;

theorem Th3: :: PROJRED1:3
for b1 being IncProjSp
for b2, b3 being LINE of b1 st b2 <> b3 holds
ex b4, b5 being POINT of b1 st
( b4 on b2 & not b4 on b3 & b5 on b3 & not b5 on b2 )
proof end;

theorem Th4: :: PROJRED1:4
for b1 being IncProjSp
for b2, b3 being POINT of b1 st b2 <> b3 holds
ex b4, b5 being LINE of b1 st
( b2 on b4 & not b2 on b5 & b3 on b5 & not b3 on b4 )
proof end;

theorem Th5: :: PROJRED1:5
for b1 being IncProjSp
for b2 being POINT of b1 ex b3, b4, b5 being LINE of b1 st
( b2 on b3 & b2 on b4 & b2 on b5 & b3 <> b4 & b4 <> b5 & b5 <> b3 )
proof end;

theorem Th6: :: PROJRED1:6
for b1 being IncProjSp
for b2, b3 being LINE of b1 ex b4 being POINT of b1 st
( not b4 on b2 & not b4 on b3 )
proof end;

theorem Th7: :: PROJRED1:7
for b1 being IncProjSp
for b2 being LINE of b1 ex b3 being POINT of b1 st b3 on b2
proof end;

theorem Th8: :: PROJRED1:8
for b1 being IncProjSp
for b2, b3 being POINT of b1
for b4 being LINE of b1 ex b5 being POINT of b1 st
( b5 on b4 & b5 <> b2 & b5 <> b3 )
proof end;

theorem Th9: :: PROJRED1:9
for b1 being IncProjSp
for b2, b3 being POINT of b1 ex b4 being LINE of b1 st
( not b2 on b4 & not b3 on b4 )
proof end;

theorem Th10: :: PROJRED1:10
canceled;

theorem Th11: :: PROJRED1:11
canceled;

theorem Th12: :: PROJRED1:12
for b1 being IncProjSp
for b2, b3, b4, b5 being POINT of b1
for b6, b7, b8, b9 being LINE of b1 st b2 on b6 & b2 on b7 & b6 <> b7 & b3 on b6 & b2 <> b3 & b4 on b7 & b5 on b7 & b4 <> b5 & b3 on b8 & b4 on b8 & b3 on b9 & b5 on b9 holds
b8 <> b9
proof end;

theorem Th13: :: PROJRED1:13
for b1 being IncProjSp
for b2, b3, b4 being POINT of b1
for b5 being LINE of b1 st b2,b3,b4 on b5 holds
( b2,b4,b3 on b5 & b3,b2,b4 on b5 & b3,b4,b2 on b5 & b4,b2,b3 on b5 & b4,b3,b2 on b5 )
proof end;

theorem Th14: :: PROJRED1:14
for b1 being Desarguesian IncProjSp
for b2, b3, b4, b5, b6, b7, b8, b9, b10, b11 being POINT of b1
for b12, b13, b14, b15, b16, b17, b18, b19, b20 being LINE of b1 st b2,b3,b4 on b12 & b2,b6,b5 on b13 & b2,b8,b7 on b14 & b8,b6,b11 on b15 & b8,b9,b4 on b16 & b6,b10,b4 on b17 & b11,b5,b7 on b18 & b3,b9,b7 on b19 & b3,b10,b5 on b20 & b12,b13,b14 are_mutually_different & b2 <> b8 & b2 <> b3 & b2 <> b5 & b6 <> b5 holds
ex b21 being LINE of b1 st b9,b10,b11 on b21
proof end;

Lemma9: for b1 being IncProjSp
for b2, b3, b4, b5 being POINT of b1
for b6, b7 being LINE of b1 st ex b8 being POINT of b1 st
( b8 on b6 & b8 on b7 ) & b2 on b6 & b3 on b6 & b4 on b6 & b5 on b6 & b2,b3,b4,b5 are_mutually_different holds
ex b8, b9, b10, b11 being POINT of b1 st
( b8 on b7 & b9 on b7 & b10 on b7 & b11 on b7 & b8,b9,b10,b11 are_mutually_different )
proof end;

theorem Th15: :: PROJRED1:15
for b1 being IncProjSp st ex b2 being LINE of b1ex b3, b4, b5, b6 being POINT of b1 st
( b3 on b2 & b4 on b2 & b5 on b2 & b6 on b2 & b3,b4,b5,b6 are_mutually_different ) holds
for b2 being LINE of b1 ex b3, b4, b5, b6 being POINT of b1 st
( b3 on b2 & b4 on b2 & b5 on b2 & b6 on b2 & b3,b4,b5,b6 are_mutually_different )
proof end;

Lemma11: for b1 being Fanoian IncProjSp ex b2, b3, b4, b5, b6, b7, b8 being POINT of b1ex b9, b10, b11, b12, b13, b14, b15, b16 being LINE of b1ex b17 being POINT of b1 st
( not b3 on b13 & not b4 on b13 & not b2 on b12 & not b5 on b12 & not b2 on b14 & not b4 on b14 & not b3 on b15 & not b5 on b15 & b6,b2,b5 on b13 & b6,b3,b4 on b12 & b7,b3,b5 on b14 & b7,b2,b4 on b15 & b8,b2,b3 on b9 & b8,b4,b5 on b10 & b6,b7 on b11 & not b8 on b11 & b7 on b16 & b8 on b16 & b11,b16,b14,b15 are_mutually_different & b17 on b9 & b8,b17,b2,b3 are_mutually_different )
proof end;

theorem Th16: :: PROJRED1:16
for b1 being Fanoian IncProjSp ex b2, b3, b4, b5, b6, b7, b8 being POINT of b1ex b9, b10, b11, b12, b13, b14, b15, b16 being LINE of b1 st
( not b3 on b13 & not b4 on b13 & not b2 on b12 & not b5 on b12 & not b2 on b14 & not b4 on b14 & not b3 on b15 & not b5 on b15 & b6,b2,b5 on b13 & b6,b3,b4 on b12 & b7,b3,b5 on b14 & b7,b2,b4 on b15 & b8,b2,b3 on b9 & b8,b4,b5 on b10 & b6,b7 on b11 & not b8 on b11 )
proof end;

theorem Th17: :: PROJRED1:17
for b1 being Fanoian IncProjSp ex b2 being POINT of b1ex b3, b4, b5, b6 being LINE of b1 st
( b2 on b3 & b2 on b4 & b2 on b5 & b2 on b6 & b3,b4,b5,b6 are_mutually_different )
proof end;

theorem Th18: :: PROJRED1:18
for b1 being Fanoian IncProjSp ex b2, b3, b4, b5 being POINT of b1ex b6 being LINE of b1 st
( b2 on b6 & b3 on b6 & b4 on b6 & b5 on b6 & b2,b3,b4,b5 are_mutually_different )
proof end;

theorem Th19: :: PROJRED1:19
for b1 being Fanoian IncProjSp
for b2 being LINE of b1 ex b3, b4, b5, b6 being POINT of b1 st
( b3 on b2 & b4 on b2 & b5 on b2 & b6 on b2 & b3,b4,b5,b6 are_mutually_different )
proof end;

definition
let c1 be 2-dimensional Desarguesian IncProjSp;
let c2, c3 be LINE of c1;
let c4 be POINT of c1;
assume E13: ( not c4 on c2 & not c4 on c3 ) ;
func IncProj c2,c4,c3 -> PartFunc of the Points of a1,the Points of a1 means :Def1: :: PROJRED1:def 1
( dom a5 c= the Points of a1 & ( for b1 being POINT of a1 holds
( b1 in dom a5 iff b1 on a2 ) ) & ( for b1, b2 being POINT of a1 st b1 on a2 & b2 on a3 holds
( a5 . b1 = b2 iff ex b3 being LINE of a1 st
( a4 on b3 & b1 on b3 & b2 on b3 ) ) ) );
existence
ex b1 being PartFunc of the Points of c1,the Points of c1 st
( dom b1 c= the Points of c1 & ( for b2 being POINT of c1 holds
( b2 in dom b1 iff b2 on c2 ) ) & ( for b2, b3 being POINT of c1 st b2 on c2 & b3 on c3 holds
( b1 . b2 = b3 iff ex b4 being LINE of c1 st
( c4 on b4 & b2 on b4 & b3 on b4 ) ) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of the Points of c1,the Points of c1 st dom b1 c= the Points of c1 & ( for b3 being POINT of c1 holds
( b3 in dom b1 iff b3 on c2 ) ) & ( for b3, b4 being POINT of c1 st b3 on c2 & b4 on c3 holds
( b1 . b3 = b4 iff ex b5 being LINE of c1 st
( c4 on b5 & b3 on b5 & b4 on b5 ) ) ) & dom b2 c= the Points of c1 & ( for b3 being POINT of c1 holds
( b3 in dom b2 iff b3 on c2 ) ) & ( for b3, b4 being POINT of c1 st b3 on c2 & b4 on c3 holds
( b2 . b3 = b4 iff ex b5 being LINE of c1 st
( c4 on b5 & b3 on b5 & b4 on b5 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines IncProj PROJRED1:def 1 :
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3 being LINE of b1
for b4 being POINT of b1 st not b4 on b2 & not b4 on b3 holds
for b5 being PartFunc of the Points of b1,the Points of b1 holds
( b5 = IncProj b2,b4,b3 iff ( dom b5 c= the Points of b1 & ( for b6 being POINT of b1 holds
( b6 in dom b5 iff b6 on b2 ) ) & ( for b6, b7 being POINT of b1 st b6 on b2 & b7 on b3 holds
( b5 . b6 = b7 iff ex b8 being LINE of b1 st
( b4 on b8 & b6 on b8 & b7 on b8 ) ) ) ) );

theorem Th20: :: PROJRED1:20
canceled;

theorem Th21: :: PROJRED1:21
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being POINT of b1
for b3 being LINE of b1 st not b2 on b3 holds
for b4 being POINT of b1 st b4 on b3 holds
(IncProj b3,b2,b3) . b4 = b4
proof end;

theorem Th22: :: PROJRED1:22
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3 being POINT of b1
for b4, b5 being LINE of b1 st not b2 on b4 & not b2 on b5 & b3 on b4 holds
(IncProj b4,b2,b5) . b3 is POINT of b1
proof end;

theorem Th23: :: PROJRED1:23
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4 being POINT of b1
for b5, b6 being LINE of b1 st not b2 on b5 & not b2 on b6 & b3 on b5 & b4 = (IncProj b5,b2,b6) . b3 holds
b4 on b6
proof end;

theorem Th24: :: PROJRED1:24
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3 being POINT of b1
for b4, b5 being LINE of b1 st not b2 on b4 & not b2 on b5 & b3 in rng (IncProj b4,b2,b5) holds
b3 on b5
proof end;

theorem Th25: :: PROJRED1:25
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3 being POINT of b1
for b4, b5, b6 being LINE of b1 st not b2 on b4 & not b2 on b5 & not b3 on b5 & not b3 on b6 holds
( dom ((IncProj b5,b3,b6) * (IncProj b4,b2,b5)) = dom (IncProj b4,b2,b5) & rng ((IncProj b5,b3,b6) * (IncProj b4,b2,b5)) = rng (IncProj b5,b3,b6) )
proof end;

theorem Th26: :: PROJRED1:26
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being POINT of b1
for b3, b4 being LINE of b1
for b5, b6, b7, b8 being POINT of b1 st not b2 on b3 & not b2 on b4 & b5 on b3 & b6 on b3 & (IncProj b3,b2,b4) . b5 = b7 & (IncProj b3,b2,b4) . b6 = b8 & b7 = b8 holds
b5 = b6
proof end;

theorem Th27: :: PROJRED1:27
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3 being POINT of b1
for b4, b5 being LINE of b1 st not b2 on b4 & not b2 on b5 & b3 on b4 & b3 on b5 holds
(IncProj b4,b2,b5) . b3 = b3
proof end;

theorem Th28: :: PROJRED1:28
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4 being POINT of b1
for b5, b6, b7 being LINE of b1 st not b2 on b5 & not b2 on b6 & not b3 on b6 & not b3 on b7 & b4 on b5 & b4 on b6 & b4 on b7 & b5 <> b7 holds
ex b8 being POINT of b1 st
( not b8 on b5 & not b8 on b7 & (IncProj b6,b3,b7) * (IncProj b5,b2,b6) = IncProj b5,b8,b7 )
proof end;