let IPP be 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)
let a, b, c, d, s, r be 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)
let A, B, C, S, R, Q be LINE of IPP; ( 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 implies (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,a,B) * (IncProj A,b,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 on B
and
A6:
not b on A
and
A7:
c on A
and
A8:
c on C
and
A9:
d on B
and
A10:
d on C
and
A11:
a on S
and
A12:
d on S
and
A13:
c on R
and
A14:
b on R
and
A15:
s on A
and
A16:
s on S
and
A17:
r on B
and
A18:
r on R
and
A19:
s on Q
and
A20:
r on Q
and
A21:
not A,B,C are_concurrent
; (IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,a,B) * (IncProj A,b,Q)
A22:
c <> d
by A7, A8, A9, A21, Def1;
then A23:
c <> s
by A3, A8, A10, A11, A12, A16, INCPROJ:def 9;
A24:
now assume
b on Q
;
contradictionthen
R = Q
by A2, A14, A17, A18, A20, INCPROJ:def 9;
hence
contradiction
by A6, A7, A13, A14, A15, A19, A23, INCPROJ:def 9;
verum end;
A25:
d <> r
by A4, A8, A10, A13, A14, A18, A22, INCPROJ:def 9;
A26:
now assume
a on Q
;
contradictionthen
S = Q
by A1, A11, A15, A16, A19, INCPROJ:def 9;
hence
contradiction
by A5, A9, A11, A12, A17, A20, A25, INCPROJ:def 9;
verum end;
set X = CHAIN A;
set f = IncProj A,a,C;
set g = IncProj C,b,B;
set g1 = IncProj Q,a,B;
set f1 = IncProj A,b,Q;
A27:
dom (IncProj A,a,C) = CHAIN A
by A1, A3, Th5;
A28:
dom (IncProj A,b,Q) = CHAIN A
by A6, A24, Th5;
then A29:
dom ((IncProj Q,a,B) * (IncProj A,b,Q)) = CHAIN A
by A5, A6, A26, A24, PROJRED1:25;
A <> C
by A21, Th1;
then A30:
C,A,R are_mutually_different
by A4, A6, A14, ZFMISC_1:def 5;
A31:
c <> d
by A7, A8, A9, A21, Def1;
A32:
for x being POINT of IPP st x on A holds
((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,a,B) * (IncProj A,b,Q)) . x
proof
let x be
POINT of
IPP;
( x on A implies ((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,a,B) * (IncProj A,b,Q)) . x )
assume A33:
x on A
;
((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,a,B) * (IncProj A,b,Q)) . x
then reconsider x9 =
(IncProj A,a,C) . x,
y =
(IncProj A,b,Q) . x as
POINT of
IPP by A1, A3, A6, A24, PROJRED1:22;
A34:
x in dom (IncProj A,b,Q)
by A28, A33;
A35:
x9 on C
by A1, A3, A33, PROJRED1:23;
then reconsider x99 =
(IncProj C,b,B) . x9 as
POINT of
IPP by A2, A4, PROJRED1:22;
consider O1 being
LINE of
IPP such that A36:
(
a on O1 &
x on O1 &
x9 on O1 )
by A1, A3, A33, A35, PROJRED1:def 1;
A37:
y on Q
by A6, A24, A33, PROJRED1:23;
then consider O3 being
LINE of
IPP such that A38:
(
b on O3 &
x on O3 &
y on O3 )
by A6, A24, A33, PROJRED1:def 1;
A39:
x99 on B
by A2, A4, A35, PROJRED1:23;
then consider O2 being
LINE of
IPP such that A40:
(
b on O2 &
x9 on O2 &
x99 on O2 )
by A2, A4, A35, PROJRED1:def 1;
A41:
now A42:
(
{y,s,r} on Q &
{d,x99,r} on B )
by A9, A17, A19, A20, A37, A39, INCSP_1:12;
assume A43:
s <> x
;
(IncProj C,b,B) . ((IncProj A,a,C) . x) = (IncProj Q,a,B) . ((IncProj A,b,Q) . x)A44:
{d,a,s} on S
by A11, A12, A16, INCSP_1:12;
A45:
(
{c,b,r} on R &
{b,x,y} on O3 )
by A13, A14, A18, A38, INCSP_1:12;
A46:
(
{b,x99,x9} on O2 &
{x,a,x9} on O1 )
by A36, A40, INCSP_1:12;
(
{c,d,x9} on C &
{c,x,s} on A )
by A7, A8, A10, A15, A33, A35, INCSP_1:12;
then consider O4 being
LINE of
IPP such that A47:
{x99,a,y} on O4
by A6, A7, A31, A23, A30, A43, A45, A46, A42, A44, PROJRED1:14;
A48:
y on O4
by A47, INCSP_1:12;
(
x99 on O4 &
a on O4 )
by A47, INCSP_1:12;
hence
(IncProj C,b,B) . ((IncProj A,a,C) . x) = (IncProj Q,a,B) . ((IncProj A,b,Q) . x)
by A5, A26, A37, A39, A48, PROJRED1:def 1;
verum end;
A49:
now assume A50:
s = x
;
(IncProj C,b,B) . ((IncProj A,a,C) . x) = (IncProj Q,a,B) . ((IncProj A,b,Q) . x)then
x9 = d
by A1, A3, A10, A11, A12, A15, A16, PROJRED1:def 1;
then A51:
x99 = d
by A2, A4, A9, A10, PROJRED1:27;
y = s
by A6, A15, A19, A24, A50, PROJRED1:27;
hence
(IncProj C,b,B) . ((IncProj A,a,C) . x) = (IncProj Q,a,B) . ((IncProj A,b,Q) . x)
by A5, A9, A11, A12, A16, A19, A26, A51, PROJRED1:def 1;
verum end;
x in dom (IncProj A,a,C)
by A27, A33;
then ((IncProj C,b,B) * (IncProj A,a,C)) . x =
(IncProj Q,a,B) . ((IncProj A,b,Q) . x)
by A49, A41, FUNCT_1:23
.=
((IncProj Q,a,B) * (IncProj A,b,Q)) . x
by A34, FUNCT_1:23
;
hence
((IncProj C,b,B) * (IncProj A,a,C)) . x = ((IncProj Q,a,B) * (IncProj A,b,Q)) . x
;
verum
end;
A52:
now let y be
set ;
( y in CHAIN A implies ((IncProj C,b,B) * (IncProj A,a,C)) . y = ((IncProj Q,a,B) * (IncProj A,b,Q)) . y )assume
y in CHAIN A
;
((IncProj C,b,B) * (IncProj A,a,C)) . y = ((IncProj Q,a,B) * (IncProj A,b,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,a,B) * (IncProj A,b,Q)) . y
by A32;
verum end;
dom ((IncProj C,b,B) * (IncProj A,a,C)) = CHAIN A
by A1, A2, A3, A4, A27, PROJRED1:25;
hence
(IncProj C,b,B) * (IncProj A,a,C) = (IncProj Q,a,B) * (IncProj A,b,Q)
by A29, A52, FUNCT_1:9; verum