let IPP be 2-dimensional Desarguesian IncProjSp; for a, b, c, d, q, o, o9, o99, oo9 being POINT of IPP
for O1, O2, O3, A, B, C, O, Q 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,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
let a, b, c, d, q, o, o9, o99, oo9 be POINT of IPP; for O1, O2, O3, A, B, C, O, Q 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,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O 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 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,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O 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 a on C
and
A3:
not b on B
and
A4:
not b on C
and
A5:
not b on Q
and
A6:
not A,B,C are_concurrent
and
A7:
a <> b
and
A8:
b <> q
and
A9:
A <> Q
and
A10:
{c,o} on A
and
A11:
{o,o99,d} on B
and
A12:
{c,d,o9} on C
and
A13:
{a,b,d} on O
and
A14:
{c,oo9} on Q
and
A15:
{a,o,o9} on O1
and
A16:
{b,o9,oo9} on O2
and
A17:
{o,oo9,q} on O3
and
A18:
q on O
; (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
A19:
o on A
by A10, INCSP_1:1;
A20:
( c on A & c on Q )
by A10, A14, INCSP_1:1;
A21:
o9 on C
by A12, INCSP_1:2;
A22:
oo9 on O2
by A16, INCSP_1:2;
A23:
b on O
by A13, INCSP_1:2;
A24:
q on O3
by A17, INCSP_1:2;
A25:
( o on O3 & oo9 on O3 )
by A17, INCSP_1:2;
set X = CHAIN A;
set f = IncProj (A,a,C);
set g = IncProj (C,b,B);
set f1 = IncProj (A,q,Q);
set g1 = IncProj (Q,b,B);
A26:
o on B
by A11, INCSP_1:2;
A27:
dom (IncProj (A,a,C)) = CHAIN A
by A1, A2, Th4;
A28:
o9 on O2
by A16, INCSP_1:2;
A29:
q on O3
by A17, INCSP_1:2;
A30:
b on O2
by A16, INCSP_1:2;
A31:
o on B
by A11, INCSP_1:2;
A32:
d on C
by A12, INCSP_1:2;
then A33:
o <> d
by A6, A19, A31;
A34:
d on O
by A13, INCSP_1:2;
A35:
( o on O3 & oo9 on O3 )
by A17, INCSP_1:2;
A36:
o9 on O1
by A15, INCSP_1:2;
A37:
o on A
by A10, INCSP_1:1;
A38:
a on O1
by A15, INCSP_1:2;
A39:
d on B
by A11, INCSP_1:2;
then A40:
q <> o
by A3, A18, A31, A23, A34, A33, INCPROJ:def 4;
A41:
c on C
by A12, INCSP_1:2;
A42:
oo9 on Q
by A14, INCSP_1:1;
A43:
o on O1
by A15, INCSP_1:2;
A44:
c on A
by A10, INCSP_1:1;
then A45:
o <> c
by A6, A31, A41;
then A46:
o9 <> c
by A1, A44, A19, A38, A43, A36, INCPROJ:def 4;
then A47:
c <> oo9
by A4, A41, A21, A30, A28, A22, INCPROJ:def 4;
A48:
not q on A
A49:
a on O
by A13, INCSP_1:2;
o9 <> d
proof
assume
not
o9 <> d
;
contradiction
then
O1 = O
by A2, A32, A49, A34, A38, A36, INCPROJ:def 4;
hence
contradiction
by A3, A31, A39, A23, A34, A43, A33, INCPROJ:def 4;
verum
end;
then
O <> O2
by A2, A32, A21, A49, A34, A28, INCPROJ:def 4;
then A50:
q <> oo9
by A8, A18, A23, A30, A22, INCPROJ:def 4;
A51:
not q on Q
then A52:
dom (IncProj (A,q,Q)) = CHAIN A
by A48, Th4;
then A53:
dom ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) = CHAIN A
by A3, A5, A48, A51, PROJRED1:22;
A54:
( d on B & d on O )
by A11, A13, INCSP_1:2;
A55:
O1 <> O2
proof
assume
not
O1 <> O2
;
contradiction
then
o on O
by A7, A49, A23, A38, A43, A30, INCPROJ:def 4;
then
O = B
by A54, A26, A33, INCPROJ:def 4;
hence
contradiction
by A3, A13, INCSP_1:2;
verum
end;
A56:
( c on Q & oo9 on Q )
by A14, INCSP_1:1;
A57:
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
A58:
(
{o9,b,oo9} on O2 &
{o9,o,a} on O1 )
by A38, A43, A36, A30, A28, A22, INCSP_1:2;
A59:
(
{o,q,oo9} on O3 &
{b,q,a} on O )
by A18, A49, A23, A25, A24, INCSP_1:2;
A60:
O2,
O1,
C are_mutually_distinct
by A2, A4, A38, A30, A55, ZFMISC_1:def 5;
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 A61:
x on A
;
((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
A62:
{c,o,x} on A
by A44, A19, A61, INCSP_1:2;
A63:
x in dom (IncProj (A,q,Q))
by A52, A61;
A64:
x in dom (IncProj (A,a,C))
by A27, A61;
consider Q1 being
LINE of
IPP such that A65:
(
a on Q1 &
x on Q1 )
by INCPROJ:def 5;
consider x9 being
POINT of
IPP such that A66:
x9 on Q1
and A67:
x9 on C
by INCPROJ:def 9;
A68:
{x,a,x9} on Q1
by A65, A66, INCSP_1:2;
A69:
{o9,c,x9} on C
by A41, A21, A67, INCSP_1:2;
consider Q2 being
LINE of
IPP such that A70:
x9 on Q2
and A71:
b on Q2
by INCPROJ:def 5;
consider y being
POINT of
IPP such that A72:
y on Q
and A73:
y on Q2
by INCPROJ:def 9;
A74:
{c,y,oo9} on Q
by A56, A72, INCSP_1:2;
{b,y,x9} on Q2
by A70, A71, A73, INCSP_1:2;
then consider R being
LINE of
IPP such that A75:
{y,q,x} on R
by A1, A2, A4, A19, A21, A46, A58, A69, A62, A74, A68, A59, A60, PROJRED1:12;
A76:
x on R
by A75, INCSP_1:2;
(
y on R &
q on R )
by A75, INCSP_1:2;
then A77:
(IncProj (A,q,Q)) . x = y
by A48, A51, A61, A72, A76, PROJRED1:def 1;
consider x99 being
POINT of
IPP such that A78:
(
x99 on Q2 &
x99 on B )
by INCPROJ:def 9;
A79:
(IncProj (Q,b,B)) . y = x99
by A3, A5, A71, A78, A72, A73, PROJRED1:def 1;
A80:
(IncProj (C,b,B)) . x9 = x99
by A3, A4, A67, A70, A71, A78, PROJRED1:def 1;
(IncProj (A,a,C)) . x = x9
by A1, A2, A61, A65, A66, A67, PROJRED1:def 1;
then ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x =
(IncProj (Q,b,B)) . ((IncProj (A,q,Q)) . x)
by A80, A77, A79, A64, FUNCT_1:13
.=
((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
by A63, FUNCT_1:13
;
hence
((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
;
verum
end;
A81:
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 A57;
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,b,B)) * (IncProj (A,q,Q))
by A53, A81, FUNCT_1:2; verum