:: PROJRED2 semantic presentation

definition
let c1 be IncProjSp;
let c2, c3, c4 be LINE of c1;
pred c2,c3,c4 are_concurrent means :Def1: :: PROJRED2:def 1
ex b1 being Element of the Points of a1 st
( b1 on a2 & b1 on a3 & b1 on a4 );
end;

:: deftheorem Def1 defines are_concurrent PROJRED2:def 1 :
for b1 being IncProjSp
for b2, b3, b4 being LINE of b1 holds
( b2,b3,b4 are_concurrent iff ex b5 being Element of the Points of b1 st
( b5 on b2 & b5 on b3 & b5 on b4 ) );

definition
let c1 be IncProjSp;
let c2 be LINE of c1;
func CHAIN c2 -> Subset of the Points of a1 equals :: PROJRED2:def 2
{ b1 where B is POINT of a1 : b1 on a2 } ;
correctness
coherence
{ b1 where B is POINT of c1 : b1 on c2 } is Subset of the Points of c1;
proof end;
end;

:: deftheorem Def2 defines CHAIN PROJRED2:def 2 :
for b1 being IncProjSp
for b2 being LINE of b1 holds CHAIN b2 = { b3 where B is POINT of b1 : b3 on b2 } ;

definition
let c1 be 2-dimensional Desarguesian IncProjSp;
mode Projection of c1 -> PartFunc of the Points of a1,the Points of a1 means :Def3: :: PROJRED2:def 3
ex b1 being POINT of a1ex b2, b3 being LINE of a1 st
( not b1 on b2 & not b1 on b3 & a2 = IncProj b2,b1,b3 );
existence
ex b1 being PartFunc of the Points of c1,the Points of c1ex b2 being POINT of c1ex b3, b4 being LINE of c1 st
( not b2 on b3 & not b2 on b4 & b1 = IncProj b3,b2,b4 )
proof end;
end;

:: deftheorem Def3 defines Projection PROJRED2:def 3 :
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being PartFunc of the Points of b1,the Points of b1 holds
( b2 is Projection of b1 iff ex b3 being POINT of b1ex b4, b5 being LINE of b1 st
( not b3 on b4 & not b3 on b5 & b2 = IncProj b4,b3,b5 ) );

theorem Th1: :: PROJRED2:1
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4 being LINE of b1 st ( b2 = b3 or b3 = b4 or b4 = b2 ) holds
b2,b3,b4 are_concurrent
proof end;

theorem Th2: :: PROJRED2:2
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4 being LINE of b1 st b2,b3,b4 are_concurrent holds
( b2,b4,b3 are_concurrent & b3,b2,b4 are_concurrent & b3,b4,b2 are_concurrent & b4,b2,b3 are_concurrent & b4,b3,b2 are_concurrent )
proof end;

theorem Th3: :: PROJRED2:3
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 b5 holds
ex b6 being POINT of b1 st
( b6 on b4 & (IncProj b4,b2,b5) . b6 = b3 )
proof end;

theorem Th4: :: PROJRED2:4
canceled;

theorem Th5: :: PROJRED2:5
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being POINT of b1
for b3, b4 being LINE of b1 st not b2 on b3 & not b2 on b4 holds
dom (IncProj b3,b2,b4) = CHAIN b3
proof end;

theorem Th6: :: PROJRED2:6
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being POINT of b1
for b3, b4 being LINE of b1 st not b2 on b3 & not b2 on b4 holds
rng (IncProj b3,b2,b4) = CHAIN b4
proof end;

theorem Th7: :: PROJRED2:7
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being LINE of b1
for b3 being set holds
( b3 in CHAIN b2 iff ex b4 being POINT of b1 st
( b3 = b4 & b4 on b2 ) ) ;

theorem Th8: :: PROJRED2:8
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being POINT of b1
for b3, b4 being LINE of b1 st not b2 on b3 & not b2 on b4 holds
IncProj b3,b2,b4 is one-to-one
proof end;

theorem Th9: :: PROJRED2:9
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being POINT of b1
for b3, b4 being LINE of b1 st not b2 on b3 & not b2 on b4 holds
(IncProj b3,b2,b4) " = IncProj b4,b2,b3
proof end;

theorem Th10: :: PROJRED2:10
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being Projection of b1 holds b2 " is Projection of b1
proof end;

theorem Th11: :: PROJRED2:11
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
IncProj b3,b2,b3 = id (CHAIN b3)
proof end;

theorem Th12: :: PROJRED2:12
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being LINE of b1 holds id (CHAIN b2) is Projection of b1
proof end;

theorem Th13: :: PROJRED2:13
for b1 being 2-dimensional Desarguesian IncProjSp
for b2 being POINT of b1
for b3, b4, b5 being LINE of b1 st not b2 on b3 & not b2 on b4 & not b2 on b5 holds
(IncProj b5,b2,b4) * (IncProj b3,b2,b5) = IncProj b3,b2,b4
proof end;

theorem Th14: :: PROJRED2:14
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 & b4,b5,b6 are_concurrent & b4 <> b6 holds
ex b7 being POINT of b1 st
( not b7 on b4 & not b7 on b6 & (IncProj b5,b3,b6) * (IncProj b4,b2,b5) = IncProj b4,b7,b6 )
proof end;

theorem Th15: :: PROJRED2:15
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4, b5, b6, b7, b8 being POINT of b1
for b9, b10, b11, b12, b13, b14, b15, b16 being LINE of b1 st not b2 on b9 & not b3 on b10 & not b2 on b11 & not b3 on b11 & not b9,b10,b11 are_concurrent & b4 on b9 & b4 on b11 & b4 on b12 & not b3 on b12 & b9 <> b12 & b2 <> b3 & b3 <> b5 & b2 on b13 & b3 on b13 & not b10,b11,b13 are_concurrent & b6 on b11 & b6 on b10 & b2 on b14 & b6 on b14 & b7 on b9 & b7 on b14 & b5 on b13 & b5 on b15 & b7 on b15 & b8 on b15 & b6 on b16 & b3 on b16 & b8 on b16 & b8 on b12 & b12 <> b11 & b5 <> b2 & not b5 on b9 & not b5 on b12 holds
(IncProj b11,b3,b10) * (IncProj b9,b2,b11) = (IncProj b12,b3,b10) * (IncProj b9,b5,b12)
proof end;

theorem Th16: :: PROJRED2:16
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being POINT of b1
for b11, b12, b13, b14, b15, b16, b17, b18 being LINE of b1 st not b2 on b11 & not b2 on b12 & not b3 on b13 & not b3 on b12 & not b3 on b14 & not b11,b13,b12 are_concurrent & b2 <> b3 & b3 <> b4 & b11 <> b14 & b5,b6 on b11 & b6,b7,b8 on b13 & b5,b8,b9 on b12 & b2,b3,b8 on b15 & b5,b10 on b14 & b2,b6,b9 on b16 & b3,b9,b10 on b17 & b6,b10,b4 on b18 & b4 on b15 holds
(IncProj b12,b3,b13) * (IncProj b11,b2,b12) = (IncProj b14,b3,b13) * (IncProj b11,b4,b14)
proof end;

theorem Th17: :: PROJRED2:17
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4, b5, b6, b7, b8 being POINT of b1
for b9, b10, b11, b12, b13, b14, b15, b16 being LINE of b1 st not b2 on b9 & not b2 on b10 & not b3 on b11 & not b3 on b10 & not b3 on b12 & not b9,b11,b10 are_concurrent & not b11,b10,b13 are_concurrent & b9 <> b12 & b12 <> b10 & b2 <> b3 & b4,b5 on b9 & b6 on b11 & b4,b6 on b10 & b2,b3,b7 on b13 & b4,b8 on b12 & b2,b6,b5 on b14 & b7,b5,b8 on b15 & b3,b6,b8 on b16 holds
( b7 <> b2 & b7 <> b3 & not b7 on b9 & not b7 on b12 )
proof end;

theorem Th18: :: PROJRED2:18
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being POINT of b1
for b11, b12, b13, b14, b15, b16, b17, b18 being LINE of b1 st not b2 on b11 & not b2 on b12 & not b3 on b13 & not b3 on b12 & not b3 on b14 & not b11,b13,b12 are_concurrent & b2 <> b3 & b11 <> b14 & b4,b5 on b11 & b5,b6,b7 on b13 & b4,b7,b8 on b12 & b2,b3,b7 on b15 & b4,b9 on b14 & b2,b5,b8 on b16 & b3,b8,b9 on b17 & b5,b9,b10 on b18 & b10 on b15 holds
( not b10 on b11 & not b10 on b14 & b3 <> b10 )
proof end;

theorem Th19: :: PROJRED2:19
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4, b5, b6, b7, b8 being POINT of b1
for b9, b10, b11, b12, b13, b14, b15, b16 being LINE of b1 st not b2 on b9 & not b2 on b10 & not b3 on b11 & not b3 on b10 & not b4 on b9 & not b9,b11,b10 are_concurrent & not b11,b10,b12 are_concurrent & b2 <> b3 & b3 <> b4 & b4 <> b2 & b5,b6 on b9 & b7 on b11 & b5,b7 on b10 & b2,b3,b4 on b12 & b5,b8 on b13 & b2,b7,b6 on b14 & b4,b6,b8 on b15 & b3,b7,b8 on b16 holds
( b13 <> b9 & b13 <> b10 & not b4 on b13 & not b3 on b13 )
proof end;

theorem Th20: :: PROJRED2:20
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4, b5, b6, b7, b8, b9, b10 being POINT of b1
for b11, b12, b13, b14, b15, b16, b17, b18 being LINE of b1 st not b2 on b11 & not b2 on b12 & not b3 on b13 & not b3 on b12 & not b4 on b11 & not b11,b13,b12 are_concurrent & b2 <> b3 & b3 <> b4 & b5,b6 on b11 & b6,b7,b8 on b13 & b5,b8,b9 on b12 & b2,b3,b8 on b14 & b5,b10 on b15 & b2,b6,b9 on b16 & b3,b9,b10 on b17 & b6,b10,b4 on b18 & b4 on b14 holds
( not b3 on b15 & not b4 on b15 & b11 <> b15 )
proof end;

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

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

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

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

theorem Th23: :: PROJRED2:23
for b1 being 2-dimensional Desarguesian IncProjSp
for b2, b3, b4, b5, b6, b7 being POINT of b1
for b8, b9, b10, b11, b12, b13 being LINE of b1 st not b2 on b8 & not b3 on b9 & not b2 on b10 & not b3 on b10 & not b2 on b9 & not b3 on b8 & b4 on b8 & b4 on b10 & b5 on b9 & b5 on b10 & b2 on b11 & b5 on b11 & b4 on b12 & b3 on b12 & b6 on b8 & b6 on b11 & b7 on b9 & b7 on b12 & b6 on b13 & b7 on b13 & not b8,b9,b10 are_concurrent holds
(IncProj b10,b3,b9) * (IncProj b8,b2,b10) = (IncProj b13,b2,b9) * (IncProj b8,b3,b13)
proof end;

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

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

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

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