let IPP be 2-dimensional Desarguesian IncProjSp; for a, b, c, d, p, q, pp9 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 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, q, pp9 be 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 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, Q, O, O1, O2, O3 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, Th5;
set X = CHAIN A;
A30:
dom (IncProj A,q,Q) = CHAIN A
by A27, A28, Th5;
then A31:
dom ((IncProj Q,b,B) * (IncProj A,q,Q)) = CHAIN A
by A2, A9, A27, A28, PROJRED1:25;
A32:
O1 <> O2
c <> d
by A5, A6, A7, A15, Def1;
then
p <> c
by A3, A7, A14, A16, A17, A19, INCPROJ:def 9;
then A33:
pp9 <> p
by A6, A8, A10, A18, A25, INCPROJ:def 9;
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 10;
consider Q1 being
LINE of
IPP such that A37:
(
a on Q1 &
x on Q1 )
by INCPROJ:def 10;
consider y being
POINT of
IPP such that A38:
y on Q3
and A39:
y on Q
by INCPROJ:def 14;
consider x9 being
POINT of
IPP such that A40:
x9 on Q1
and A41:
x9 on C
by INCPROJ:def 14;
A42:
now A43:
(
{pp9,y,c} on Q &
{d,x9,c} on C )
by A7, A8, A14, A25, A41, A39, INCSP_1:12;
A44:
(
{p,pp9,q} on O2 &
{pp9,d,b} on O3 )
by A21, A22, A23, A24, INCSP_1:12;
A45:
(
{b,a,q} on O &
{x,y,q} on Q3 )
by A11, A12, A20, A36, A38, INCSP_1:12;
A46:
(
{p,x,c} on A &
{p,d,a} on O1 )
by A6, A16, A17, A18, A19, A35, INCSP_1:12;
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_different )
by A1, A16, A21, A27, A32, A37, A40, INCSP_1:12, 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:14;
A49:
b on R
by A48, INCSP_1:12;
consider x99 being
POINT of
IPP such that A50:
(
x99 on R &
x99 on B )
by INCPROJ:def 14;
x9 on R
by A48, INCSP_1:12;
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:12;
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:23
.=
((IncProj Q,b,B) * (IncProj A,q,Q)) . x
by A52, FUNCT_1:23
;
hence
((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,b,B) * (IncProj A,q,Q)) . x
;
verum end;
now 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:23
.=
((IncProj Q,b,B) * (IncProj A,q,Q)) . x
by A57, FUNCT_1:23
;
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 let y be
set ;
( 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:25;
hence
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,b,B) * (IncProj A,q,Q)
by A31, A59, FUNCT_1:9; verum