let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1:
( not p on K & not p on L & not q on L & not q on R )
; :: thesis: ( 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) )
thus
dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L)
:: thesis: rng ((IncProj L,q,R) * (IncProj K,p,L)) = rng (IncProj L,q,R)proof
for
x being
set holds
(
x in dom ((IncProj L,q,R) * (IncProj K,p,L)) iff
x in dom (IncProj K,p,L) )
proof
let x be
set ;
:: thesis: ( 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 A2:
x in dom (IncProj K,p,L)
;
:: thesis: x in dom ((IncProj L,q,R) * (IncProj K,p,L))
then reconsider x' =
x as
POINT of
IPP ;
A3:
x' on K
by A1, A2, Def1;
consider A being
LINE of
IPP such that A4:
(
x' on A &
p on A )
by INCPROJ:def 10;
consider y being
POINT of
IPP such that A5:
(
y on A &
y on L )
by INCPROJ:def 14;
(
(IncProj K,p,L) . x = y &
y in dom (IncProj L,q,R) )
by A1, A3, A4, A5, Def1;
hence
x in dom ((IncProj L,q,R) * (IncProj K,p,L))
by A2, FUNCT_1:21;
:: thesis: 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:21;
:: thesis: verum
end;
hence
dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L)
by TARSKI:2;
:: thesis: verum
end;
thus
rng ((IncProj L,q,R) * (IncProj K,p,L)) = rng (IncProj L,q,R)
:: thesis: verumproof
dom (IncProj L,q,R) c= rng (IncProj K,p,L)
proof
for
x being
set st
x in dom (IncProj L,q,R) holds
x in rng (IncProj K,p,L)
proof
let x be
set ;
:: thesis: ( x in dom (IncProj L,q,R) implies x in rng (IncProj K,p,L) )
assume A6:
x in dom (IncProj L,q,R)
;
:: thesis: x in rng (IncProj K,p,L)
thus
x in rng (IncProj K,p,L)
:: thesis: verumproof
reconsider x' =
x as
POINT of
IPP by A6;
A7:
x' on L
by A1, A6, Def1;
ex
y being
POINT of
IPP st
(
y in dom (IncProj K,p,L) &
x' = (IncProj K,p,L) . y )
proof
consider A being
LINE of
IPP such that A8:
(
x' on A &
p on A )
by INCPROJ:def 10;
consider y being
POINT of
IPP such that A9:
(
y on A &
y on K )
by INCPROJ:def 14;
take
y
;
:: thesis: ( y in dom (IncProj K,p,L) & x' = (IncProj K,p,L) . y )
thus
y in dom (IncProj K,p,L)
by A1, A9, Def1;
:: thesis: x' = (IncProj K,p,L) . y
thus
x' = (IncProj K,p,L) . y
by A1, A7, A8, A9, Def1;
:: thesis: verum
end;
hence
x in rng (IncProj K,p,L)
by FUNCT_1:def 5;
:: thesis: verum
end;
end;
hence
dom (IncProj L,q,R) c= rng (IncProj K,p,L)
by TARSKI:def 3;
:: thesis: verum
end;
hence
rng ((IncProj L,q,R) * (IncProj K,p,L)) = rng (IncProj L,q,R)
by RELAT_1:47;
:: thesis: verum
end;