let IPP be 2-dimensional Desarguesian IncProjSp; for a, b, c, d, p, pp9, q being POINT of IPP
for O1, O2, O3, A, B, C, O, Q 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 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 & pp9 on O2 & d on O3 & b on O3 & pp9 on O3 & pp9 on Q & 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))
let a, b, c, d, p, pp9, q be POINT of IPP; for O1, O2, O3, A, B, C, O, Q 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 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 & pp9 on O2 & d on O3 & b on O3 & pp9 on O3 & pp9 on Q & 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))
let O1, O2, O3, A, B, C, O, Q be LINE of IPP; ( 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 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 & pp9 on O2 & d on O3 & b on O3 & pp9 on O3 & pp9 on Q & q <> a & not q on A & not q on Q implies (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )
assume that
A1:
not a on A
and
A2:
not b on B
and
A3:
not a on C
and
A4:
not b on C
and
A5:
not A,B,C are_concurrent
and
A6:
c on A
and
A7:
c on C
and
A8:
c on Q
and
A9:
not b on Q
and
A10:
A <> Q
and
A11:
a on O
and
A12:
b on O
and
A13:
not B,C,O are_concurrent
and
A14:
d on C
and
A15:
d on B
and
A16:
a on O1
and
A17:
d on O1
and
A18:
p on A
and
A19:
p on O1
and
A20:
q on O
and
A21:
q on O2
and
A22:
( p on O2 & pp9 on O2 )
and
A23:
( d on O3 & b on O3 )
and
A24:
pp9 on O3
and
A25:
pp9 on Q
and
A26:
q <> a
and
A27:
not q on A
and
A28:
not q on Q
; (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
set f = IncProj (A,a,C);
set g = IncProj (C,b,B);
set g1 = IncProj (Q,b,B);
set f1 = IncProj (A,q,Q);
A29:
dom (IncProj (A,a,C)) = CHAIN A
by A1, A3, Th4;
set X = CHAIN A;
A30:
dom (IncProj (A,q,Q)) = CHAIN A
by A27, A28, Th4;
then A31:
dom ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) = CHAIN A
by A2, A9, A27, A28, PROJRED1:22;
A32:
O1 <> O2
c <> d
by A5, A6, A7, A15;
then
p <> c
by A3, A7, A14, A16, A17, A19, INCPROJ:def 4;
then A33:
pp9 <> p
by A6, A8, A10, A18, A25, INCPROJ:def 4;
A34:
for x being POINT of IPP st x on A holds
((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
proof
let x be
POINT of
IPP;
( x on A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x )
assume A35:
x on A
;
((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
consider Q3 being
LINE of
IPP such that A36:
(
q on Q3 &
x on Q3 )
by INCPROJ:def 5;
consider Q1 being
LINE of
IPP such that A37:
(
a on Q1 &
x on Q1 )
by INCPROJ:def 5;
consider y being
POINT of
IPP such that A38:
y on Q3
and A39:
y on Q
by INCPROJ:def 9;
consider x9 being
POINT of
IPP such that A40:
x9 on Q1
and A41:
x9 on C
by INCPROJ:def 9;
A42:
now ( p <> x implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x )A43:
(
{pp9,y,c} on Q &
{d,x9,c} on C )
by A7, A8, A14, A25, A41, A39, INCSP_1:2;
A44:
(
{p,pp9,q} on O2 &
{pp9,d,b} on O3 )
by A21, A22, A23, A24, INCSP_1:2;
A45:
(
{b,a,q} on O &
{x,y,q} on Q3 )
by A11, A12, A20, A36, A38, INCSP_1:2;
A46:
(
{p,x,c} on A &
{p,d,a} on O1 )
by A6, A16, A17, A18, A19, A35, INCSP_1:2;
assume A47:
p <> x
;
((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
(
{x,x9,a} on Q1 &
A,
O1,
O2 are_mutually_distinct )
by A1, A16, A21, A27, A32, A37, A40, INCSP_1:2, ZFMISC_1:def 5;
then consider R being
LINE of
IPP such that A48:
{y,x9,b} on R
by A1, A3, A14, A18, A33, A47, A46, A44, A43, A45, PROJRED1:12;
A49:
b on R
by A48, INCSP_1:2;
consider x99 being
POINT of
IPP such that A50:
(
x99 on R &
x99 on B )
by INCPROJ:def 9;
x9 on R
by A48, INCSP_1:2;
then A51:
(IncProj (C,b,B)) . x9 = x99
by A2, A4, A41, A50, A49, PROJRED1:def 1;
A52:
x in dom (IncProj (A,q,Q))
by A30, A35;
y on R
by A48, INCSP_1:2;
then A53:
(IncProj (Q,b,B)) . y = x99
by A2, A9, A39, A50, A49, PROJRED1:def 1;
A54:
x in dom (IncProj (A,a,C))
by A29, A35;
(
(IncProj (A,a,C)) . x = x9 &
(IncProj (A,q,Q)) . x = y )
by A1, A3, A27, A28, A35, A37, A40, A41, A36, A38, A39, PROJRED1:def 1;
then ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x =
(IncProj (Q,b,B)) . ((IncProj (A,q,Q)) . x)
by A51, A53, A54, FUNCT_1:13
.=
((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
by A52, FUNCT_1:13
;
hence
((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
;
verum end;
now ( p = x implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x )A55:
(
(IncProj (A,q,Q)) . p = pp9 &
(IncProj (Q,b,B)) . pp9 = d )
by A2, A9, A15, A18, A21, A22, A23, A24, A25, A27, A28, PROJRED1:def 1;
assume A56:
p = x
;
((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . xA57:
x in dom (IncProj (A,q,Q))
by A30, A35;
A58:
x in dom (IncProj (A,a,C))
by A29, A35;
(
(IncProj (A,a,C)) . p = d &
(IncProj (C,b,B)) . d = d )
by A1, A2, A3, A4, A14, A15, A16, A17, A18, A19, A23, PROJRED1:def 1;
then ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x =
(IncProj (Q,b,B)) . ((IncProj (A,q,Q)) . x)
by A56, A55, A58, FUNCT_1:13
.=
((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
by A57, FUNCT_1:13
;
hence
((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
;
verum end;
hence
((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
by A42;
verum
end;
A59:
now for y being object st y in CHAIN A holds
((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . ylet y be
object ;
( y in CHAIN A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y )assume
y in CHAIN A
;
((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . ythen
ex
x being
POINT of
IPP st
(
y = x &
x on A )
;
hence
((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y
by A34;
verum end;
dom ((IncProj (C,b,B)) * (IncProj (A,a,C))) = CHAIN A
by A1, A2, A3, A4, A29, PROJRED1:22;
hence
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
by A31, A59, FUNCT_1:2; verum