let A, B, C, D be Real; ( A > 0 & C > 0 implies AffineMap (A,B,C,D) is one-to-one )
assume that
A1:
A > 0
and
A2:
C > 0
; AffineMap (A,B,C,D) is one-to-one
set ff = AffineMap (A,B,C,D);
for x1, x2 being object st x1 in dom (AffineMap (A,B,C,D)) & x2 in dom (AffineMap (A,B,C,D)) & (AffineMap (A,B,C,D)) . x1 = (AffineMap (A,B,C,D)) . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom (AffineMap (A,B,C,D)) & x2 in dom (AffineMap (A,B,C,D)) & (AffineMap (A,B,C,D)) . x1 = (AffineMap (A,B,C,D)) . x2 implies x1 = x2 )
assume that A3:
x1 in dom (AffineMap (A,B,C,D))
and A4:
x2 in dom (AffineMap (A,B,C,D))
and A5:
(AffineMap (A,B,C,D)) . x1 = (AffineMap (A,B,C,D)) . x2
;
x1 = x2
reconsider p2 =
x2 as
Point of
(TOP-REAL 2) by A4;
reconsider p1 =
x1 as
Point of
(TOP-REAL 2) by A3;
A6:
(
(AffineMap (A,B,C,D)) . x1 = |[((A * (p1 `1)) + B),((C * (p1 `2)) + D)]| &
(AffineMap (A,B,C,D)) . x2 = |[((A * (p2 `1)) + B),((C * (p2 `2)) + D)]| )
by Def2;
then
(A * (p1 `1)) + B = (A * (p2 `1)) + B
by A5, SPPOL_2:1;
then
p1 `1 = (A * (p2 `1)) / A
by A1, XCMPLX_1:89;
then A7:
p1 `1 = p2 `1
by A1, XCMPLX_1:89;
(C * (p1 `2)) + D = (C * (p2 `2)) + D
by A5, A6, SPPOL_2:1;
then
p1 `2 = (C * (p2 `2)) / C
by A2, XCMPLX_1:89;
hence
x1 = x2
by A2, A7, TOPREAL3:6, XCMPLX_1:89;
verum
end;
hence
AffineMap (A,B,C,D) is one-to-one
by FUNCT_1:def 4; verum