let A, B, C, D be real number ; :: thesis: ( A > 0 & C > 0 implies AffineMap A,B,C,D is one-to-one )
assume that
A1:
A > 0
and
A2:
C > 0
; :: thesis: AffineMap A,B,C,D is one-to-one
set ff = AffineMap A,B,C,D;
for x1, x2 being set 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
set ;
:: thesis: ( 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 A3:
(
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 )
;
:: thesis: x1 = x2
then reconsider p1 =
x1 as
Point of
(TOP-REAL 2) ;
reconsider p2 =
x2 as
Point of
(TOP-REAL 2) by A3;
A4:
(AffineMap A,B,C,D) . x1 = |[((A * (p1 `1 )) + B),((C * (p1 `2 )) + D)]|
by Def2;
(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 &
(C * (p1 `2 )) + D = (C * (p2 `2 )) + D )
by A3, A4, SPPOL_2:1;
then
(
p1 `1 = (A * (p2 `1 )) / A &
(C * (p1 `2 )) / C = (C * (p2 `2 )) / C )
by A1, XCMPLX_1:90;
then
(
p1 `1 = p2 `1 &
p1 `2 = (C * (p2 `2 )) / C )
by A1, A2, XCMPLX_1:90;
hence
x1 = x2
by A2, TOPREAL3:11, XCMPLX_1:90;
:: thesis: verum
end;
hence
AffineMap A,B,C,D is one-to-one
by FUNCT_1:def 8; :: thesis: verum