let IPP be 2-dimensional Desarguesian IncProjSp; for a, b, c, d, r, s being POINT of IPP
for A, B, C, Q, R, S 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, r, s be POINT of IPP; for A, B, C, Q, R, S 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, Q, R, S 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;
then A23:
c <> s
by A3, A8, A10, A11, A12, A16, INCPROJ:def 4;
A24:
now not b on Qassume
b on Q
;
contradictionthen
R = Q
by A2, A14, A17, A18, A20, INCPROJ:def 4;
hence
contradiction
by A6, A7, A13, A14, A15, A19, A23, INCPROJ:def 4;
verum end;
A25:
d <> r
by A4, A8, A10, A13, A14, A18, A22, INCPROJ:def 4;
A26:
now not a on Qassume
a on Q
;
contradictionthen
S = Q
by A1, A11, A15, A16, A19, INCPROJ:def 4;
hence
contradiction
by A5, A9, A11, A12, A17, A20, A25, INCPROJ:def 4;
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, Th4;
A28:
dom (IncProj (A,b,Q)) = CHAIN A
by A6, A24, Th4;
then A29:
dom ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) = CHAIN A
by A5, A6, A26, A24, PROJRED1:22;
A <> C
by A21, Th1;
then A30:
C,A,R are_mutually_distinct
by A4, A6, A14, ZFMISC_1:def 5;
A31:
c <> d
by A7, A8, A9, A21;
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:19;
A34:
x in dom (IncProj (A,b,Q))
by A28, A33;
A35:
x9 on C
by A1, A3, A33, PROJRED1:20;
then reconsider x99 =
(IncProj (C,b,B)) . x9 as
POINT of
IPP by A2, A4, PROJRED1:19;
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:20;
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:20;
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 ( s <> x implies (IncProj (C,b,B)) . ((IncProj (A,a,C)) . x) = (IncProj (Q,a,B)) . ((IncProj (A,b,Q)) . x) )A42:
(
{y,s,r} on Q &
{d,x99,r} on B )
by A9, A17, A19, A20, A37, A39, INCSP_1:2;
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:2;
A45:
(
{c,b,r} on R &
{b,x,y} on O3 )
by A13, A14, A18, A38, INCSP_1:2;
A46:
(
{b,x99,x9} on O2 &
{x,a,x9} on O1 )
by A36, A40, INCSP_1:2;
(
{c,d,x9} on C &
{c,x,s} on A )
by A7, A8, A10, A15, A33, A35, INCSP_1:2;
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:12;
A48:
y on O4
by A47, INCSP_1:2;
(
x99 on O4 &
a on O4 )
by A47, INCSP_1:2;
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 ( s = x implies (IncProj (C,b,B)) . ((IncProj (A,a,C)) . x) = (IncProj (Q,a,B)) . ((IncProj (A,b,Q)) . x) )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:24;
y = s
by A6, A15, A19, A24, A50, PROJRED1:24;
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:13
.=
((IncProj (Q,a,B)) * (IncProj (A,b,Q))) . x
by A34, FUNCT_1:13
;
hence
((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) . x
;
verum
end;
A52:
now for y being object st y in CHAIN A holds
((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) . ylet y be
object ;
( 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:22;
hence
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,a,B)) * (IncProj (A,b,Q))
by A29, A52, FUNCT_1:2; verum