let IPP be 2-dimensional Desarguesian IncProjSp; for p, q being POINT of IPP
for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds
( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) )
let p, q be POINT of IPP; for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R holds
( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) )
let K, L, R be LINE of IPP; ( not p on K & not p on L & not q on L & not q on R implies ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) ) )
assume that
A1:
( not p on K & not p on L )
and
A2:
( not q on L & not q on R )
; ( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) )
for x being object holds
( x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) iff x in dom (IncProj (K,p,L)) )
proof
let x be
object ;
( x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) iff x in dom (IncProj (K,p,L)) )
(
x in dom (IncProj (K,p,L)) implies
x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) )
proof
assume A3:
x in dom (IncProj (K,p,L))
;
x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
then reconsider x9 =
x as
POINT of
IPP ;
consider A being
LINE of
IPP such that A4:
(
x9 on A &
p on A )
by INCPROJ:def 5;
consider y being
POINT of
IPP such that A5:
y on A
and A6:
y on L
by INCPROJ:def 9;
A7:
y in dom (IncProj (L,q,R))
by A2, A6, Def1;
x9 on K
by A1, A3, Def1;
then
(IncProj (K,p,L)) . x = y
by A1, A4, A5, A6, Def1;
hence
x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
by A3, A7, FUNCT_1:11;
verum
end;
hence
(
x in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) iff
x in dom (IncProj (K,p,L)) )
by FUNCT_1:11;
verum
end;
hence
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L))
by TARSKI:2; rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R))
for x being object st x in dom (IncProj (L,q,R)) holds
x in rng (IncProj (K,p,L))
proof
let x be
object ;
( x in dom (IncProj (L,q,R)) implies x in rng (IncProj (K,p,L)) )
assume A8:
x in dom (IncProj (L,q,R))
;
x in rng (IncProj (K,p,L))
thus
x in rng (IncProj (K,p,L))
verumproof
reconsider x9 =
x as
POINT of
IPP by A8;
A9:
x9 on L
by A2, A8, Def1;
ex
y being
POINT of
IPP st
(
y in dom (IncProj (K,p,L)) &
x9 = (IncProj (K,p,L)) . y )
proof
consider A being
LINE of
IPP such that A10:
(
x9 on A &
p on A )
by INCPROJ:def 5;
consider y being
POINT of
IPP such that A11:
y on A
and A12:
y on K
by INCPROJ:def 9;
take
y
;
( y in dom (IncProj (K,p,L)) & x9 = (IncProj (K,p,L)) . y )
thus
y in dom (IncProj (K,p,L))
by A1, A12, Def1;
x9 = (IncProj (K,p,L)) . y
thus
x9 = (IncProj (K,p,L)) . y
by A1, A9, A10, A11, A12, Def1;
verum
end;
hence
x in rng (IncProj (K,p,L))
by FUNCT_1:def 3;
verum
end;
end;
then
dom (IncProj (L,q,R)) c= rng (IncProj (K,p,L))
;
hence
rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R))
by RELAT_1:28; verum