:: PROJRED2 semantic presentation

definition

let IPS be IncProjSp;
let A, B, C be LINE of IPS;
pred A,B,C are_concurrent means :Def1: :: PROJRED2:def 1
ex o being Element of the Points of IPS st
( o on A & o on B & o on C );

end;

:: deftheorem Def1 defines are_concurrent PROJRED2:def 1 :

definition

let IPS be IncProjSp;
let Z be LINE of IPS;
func CHAIN Z -> Subset of the Points of IPS equals :: PROJRED2:def 2
{ z where z is POINT of IPS : z on Z } ;
correctness

proof end;

end;

:: deftheorem defines CHAIN PROJRED2:def 2 :

definition

let IPP be 2-dimensional Desarguesian IncProjSp;
mode Projection of IPP -> PartFunc of the Points of IPP,the Points of IPP means :Def3: :: PROJRED2:def 3
ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & it = IncProj A,a,B );
existence

proof end;

end;

:: deftheorem Def3 defines Projection PROJRED2:def 3 :

theorem Th1: :: PROJRED2:1

for IPP being 2-dimensional Desarguesian IncProjSp
for A, B, C being LINE of IPP st ( A = B or B = C or C = A ) holds
A,B,C are_concurrent

proof end;

theorem :: PROJRED2:2

for IPP being 2-dimensional Desarguesian IncProjSp
for A, B, C being LINE of IPP st A,B,C are_concurrent holds
( A,C,B are_concurrent & B,A,C are_concurrent & B,C,A are_concurrent & C,A,B are_concurrent & C,B,A are_concurrent )

proof end;

theorem Th3: :: PROJRED2:3

for IPP being 2-dimensional Desarguesian IncProjSp
for o, y being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B & y on B holds
ex x being POINT of IPP st
( x on A & (IncProj A,o,B) . x = y )

proof end;

theorem :: PROJRED2:4

canceled;

theorem Th5: :: PROJRED2:5

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
dom (IncProj A,o,B) = CHAIN A

proof end;

theorem Th6: :: PROJRED2:6

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
rng (IncProj A,o,B) = CHAIN B

proof end;

theorem :: PROJRED2:7

for IPP being 2-dimensional Desarguesian IncProjSp
for A being LINE of IPP
for x being set holds
( x in CHAIN A iff ex a being POINT of IPP st
( x = a & a on A ) ) ;

theorem Th8: :: PROJRED2:8

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
IncProj A,o,B is one-to-one

proof end;

theorem Th9: :: PROJRED2:9

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
(IncProj A,o,B) " = IncProj B,o,A

proof end;

theorem :: PROJRED2:10

for IPP being 2-dimensional Desarguesian IncProjSp
for f being Projection of IPP holds f " is Projection of IPP

proof end;

theorem Th11: :: PROJRED2:11

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A being LINE of IPP st not o on A holds
IncProj A,o,A = id (CHAIN A)

proof end;

theorem :: PROJRED2:12

for IPP being 2-dimensional Desarguesian IncProjSp
for A being LINE of IPP holds id (CHAIN A) is Projection of IPP

proof end;

theorem :: PROJRED2:13

for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj C,o,B) * (IncProj A,o,C) = IncProj A,o,B

proof end;

theorem :: PROJRED2:14

for IPP being 2-dimensional Desarguesian IncProjSp
for o1, o2 being POINT of IPP
for O1, O2, O3 being LINE of IPP st not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 & O1,O2,O3 are_concurrent & O1 <> O3 holds
ex o being POINT of IPP st
( not o on O1 & not o on O3 & (IncProj O2,o2,O3) * (IncProj O1,o1,O2) = IncProj O1,o,O3 )

proof end;

theorem Th15: :: PROJRED2:15

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, q, d, p, pp' being POINT of IPP
for A, B, C, Q, O, O1, O2, O3 being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & c on A & c on C & c on Q & not b on Q & A <> Q & a <> b & b <> q & a on O & b on O & not B,C,O are_concurrent & d on C & d on B & a on O1 & d on O1 & p on A & p on O1 & q on O & q on O2 & p on O2 & pp' on O2 & d on O3 & b on O3 & pp' on O3 & pp' on Q & Q <> C & q <> a & not q on A & not q on Q holds
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q)

proof end;

theorem Th16: :: PROJRED2:16

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q, c, o, o'', d, o', oo' being POINT of IPP
for A, C, B, Q, O, O1, O2, O3 being LINE of IPP st not a on A & not a on C & not b on B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & b <> q & A <> Q & c,o on A & o,o'',d on B & c,d,o' on C & a,b,d on O & c,oo' on Q & a,o,o' on O1 & b,o',oo' on O2 & o,oo',q on O3 & q on O holds
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q)

proof end;

theorem Th17: :: PROJRED2:17

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, p, d, q, pp' being POINT of IPP
for A, C, B, Q, O, O1, O2, O3 being LINE of IPP st not a on A & not a on C & not b on B & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & c,p on A & d on B & c,d on C & a,b,q on O & c,pp' on Q & a,d,p on O1 & q,p,pp' on O2 & b,d,pp' on O3 holds
( q <> a & q <> b & not q on A & not q on Q )

proof end;

theorem Th18: :: PROJRED2:18

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, o, o'', d, o', oo', q being POINT of IPP
for A, C, B, Q, O, O1, O2, O3 being LINE of IPP st not a on A & not a on C & not b on B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & c,o on A & o,o'',d on B & c,d,o' on C & a,b,d on O & c,oo' on Q & a,o,o' on O1 & b,o',oo' on O2 & o,oo',q on O3 & q on O holds
( not q on A & not q on Q & b <> q )

proof end;

theorem Th19: :: PROJRED2:19

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q, c, p, d, pp' being POINT of IPP
for A, C, B, O, Q, O1, O2, O3 being LINE of IPP st not a on A & not a on C & not b on B & not b on C & not q on A & not A,B,C are_concurrent & not B,C,O are_concurrent & a <> b & b <> q & q <> a & c,p on A & d on B & c,d on C & a,b,q on O & c,pp' on Q & a,d,p on O1 & q,p,pp' on O2 & b,d,pp' on O3 holds
( Q <> A & Q <> C & not q on Q & not b on Q )

proof end;

theorem Th20: :: PROJRED2:20

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q, c, o, o'', d, o', oo' being POINT of IPP
for A, C, B, O, Q, O1, O2, O3 being LINE of IPP st not a on A & not a on C & not b on B & not b on C & not q on A & not A,B,C are_concurrent & a <> b & b <> q & c,o on A & o,o'',d on B & c,d,o' on C & a,b,d on O & c,oo' on Q & a,o,o' on O1 & b,o',oo' on O2 & o,oo',q on O3 & q on O holds
( not b on Q & not q on Q & A <> Q )

proof end;

Lm1: for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & not B,C,O are_concurrent holds
ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )

proof end;

Lm2: for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & B,C,O are_concurrent holds
ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )

proof end;

theorem Th21: :: PROJRED2:21

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & A,C,Q are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O holds
ex q being POINT of IPP st
( q on O & not q on A & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )

proof end;

theorem :: PROJRED2:22

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not A,B,C are_concurrent & B,C,Q are_concurrent & not a on Q & B <> Q & a <> b & a on O & b on O holds
ex q being POINT of IPP st
( q on O & not q on B & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )

proof end;

theorem :: PROJRED2:23

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, s, r being POINT of IPP
for A, B, C, S, R, Q being LINE of IPP st not a on A & not b on B & not a on C & not b on C & not a on B & not b on A & c on A & c on C & d on B & d on C & a on S & d on S & c on R & b on R & s on A & s on S & r on B & r on R & s on Q & r on Q & not A,B,C are_concurrent holds
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,a,B) * (IncProj A,b,Q)

proof end;

Lm3: for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & c on A & c on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not A,B,C are_concurrent & not B,C,O are_concurrent holds
ex Q being LINE of IPP st
( c on Q & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )

proof end;

Lm4: for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & c on A & c on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not A,B,C are_concurrent & B,C,O are_concurrent holds
ex Q being LINE of IPP st
( c on Q & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )

proof end;

theorem Th24: :: PROJRED2:24

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not A,B,C are_concurrent holds
ex Q being LINE of IPP st
( A,C,Q are_concurrent & not b on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q) )

proof end;

theorem :: PROJRED2:25

for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q being POINT of IPP
for A, B, C, O being LINE of IPP st not a on A & not b on B & not a on C & not b on C & a <> b & a on O & b on O & q on O & not q on B & q <> a & not A,B,C are_concurrent holds
ex Q being LINE of IPP st
( B,C,Q are_concurrent & not a on Q & not q on Q & (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,q,B) * (IncProj A,a,Q) )

proof end;