let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
(IncProj (A,o,B)) " = IncProj (B,o,A)
let o be POINT of IPP; :: thesis: for A, B being LINE of IPP st not o on A & not o on B holds
(IncProj (A,o,B)) " = IncProj (B,o,A)
let A, B be LINE of IPP; :: thesis: ( not o on A & not o on B implies (IncProj (A,o,B)) " = IncProj (B,o,A) )
set f = IncProj (A,o,B);
set g = IncProj (B,o,A);
assume A1: ( not o on A & not o on B ) ; :: thesis: (IncProj (A,o,B)) " = IncProj (B,o,A)
then A2: rng (IncProj (A,o,B)) = CHAIN B by Th5;
A3: dom (IncProj (A,o,B)) = CHAIN A by A1, Th4;
A4: now :: thesis: for y, x being object holds
( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y iff ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x ) )
let y, x be object ; :: thesis: ( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y iff ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x ) )
A5: now :: thesis: ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x implies ( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y ) )
assume that
A6: x in dom (IncProj (A,o,B)) and
A7: y = (IncProj (A,o,B)) . x ; :: thesis: ( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y )
consider x9 being POINT of IPP such that
A8: ( x = x9 & x9 on A ) by A3, A6;
reconsider y9 = y as POINT of IPP by A1, A7, A8, PROJRED1:19;
A9: y9 on B by A1, A7, A8, PROJRED1:20;
then A10: y in CHAIN B ;
ex O being LINE of IPP st
( o on O & x9 on O & y9 on O ) by A1, A7, A8, A9, PROJRED1:def 1;
hence ( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y ) by A1, A8, A9, A10, Th5, PROJRED1:def 1; :: thesis: verum
end;
now :: thesis: ( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y implies ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x ) )
assume that
A11: y in rng (IncProj (A,o,B)) and
A12: x = (IncProj (B,o,A)) . y ; :: thesis: ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x )
consider y9 being POINT of IPP such that
A13: ( y = y9 & y9 on B ) by A2, A11;
reconsider x9 = x as POINT of IPP by A1, A12, A13, PROJRED1:19;
A14: x9 on A by A1, A12, A13, PROJRED1:20;
then ex O being LINE of IPP st
( o on O & y9 on O & x9 on O ) by A1, A12, A13, PROJRED1:def 1;
hence ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x ) by A1, A13, A14, PROJRED1:def 1; :: thesis: verum
end;
hence ( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y iff ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x ) ) by A5; :: thesis: verum
end;
A15: IncProj (A,o,B) is one-to-one by A1, Th7;
dom (IncProj (B,o,A)) = CHAIN B by A1, Th4
.= rng (IncProj (A,o,B)) by A1, Th5 ;
hence (IncProj (A,o,B)) " = IncProj (B,o,A) by A15, A4, FUNCT_1:32; :: thesis: verum