let IPP be 2-dimensional Desarguesian IncProjSp; for o being POINT of IPP
for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
let o be POINT of IPP; for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
let A, B, C be LINE of IPP; ( not o on A & not o on B & not o on C implies (IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B) )
assume that
A1:
not o on A
and
A2:
not o on B
and
A3:
not o on C
; (IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
set f = IncProj (A,o,B);
set g = IncProj (C,o,B);
set h = IncProj (A,o,C);
A4:
dom (IncProj (A,o,B)) = CHAIN A
by A1, A2, Th4;
set X = CHAIN A;
A5:
dom (IncProj (A,o,C)) = CHAIN A
by A1, A3, Th4;
A6:
for x being POINT of IPP st x on A holds
(IncProj (A,o,B)) . x = ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x
proof
let x be
POINT of
IPP;
( x on A implies (IncProj (A,o,B)) . x = ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x )
assume A7:
x on A
;
(IncProj (A,o,B)) . x = ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x
consider Q1 being
LINE of
IPP such that A8:
o on Q1
and A9:
x on Q1
by INCPROJ:def 5;
consider x9 being
POINT of
IPP such that A10:
(
x9 on Q1 &
x9 on C )
by INCPROJ:def 9;
A11:
(IncProj (A,o,C)) . x = x9
by A1, A3, A7, A8, A9, A10, PROJRED1:def 1;
consider y being
POINT of
IPP such that A12:
(
y on Q1 &
y on B )
by INCPROJ:def 9;
A13:
(IncProj (A,o,B)) . x = y
by A1, A2, A7, A8, A9, A12, PROJRED1:def 1;
x in dom (IncProj (A,o,C))
by A5, A7;
then ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x =
(IncProj (C,o,B)) . ((IncProj (A,o,C)) . x)
by FUNCT_1:13
.=
(IncProj (A,o,B)) . x
by A2, A3, A8, A10, A12, A13, A11, PROJRED1:def 1
;
hence
(IncProj (A,o,B)) . x = ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x
;
verum
end;
A14:
now for y being object st y in CHAIN A holds
((IncProj (C,o,B)) * (IncProj (A,o,C))) . y = (IncProj (A,o,B)) . ylet y be
object ;
( y in CHAIN A implies ((IncProj (C,o,B)) * (IncProj (A,o,C))) . y = (IncProj (A,o,B)) . y )assume
y in CHAIN A
;
((IncProj (C,o,B)) * (IncProj (A,o,C))) . y = (IncProj (A,o,B)) . ythen
ex
x being
POINT of
IPP st
(
y = x &
x on A )
;
hence
((IncProj (C,o,B)) * (IncProj (A,o,C))) . y = (IncProj (A,o,B)) . y
by A6;
verum end;
dom ((IncProj (C,o,B)) * (IncProj (A,o,C))) = CHAIN A
by A1, A2, A3, A5, PROJRED1:22;
hence
(IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
by A4, A14, FUNCT_1:2; verum