let A, B, C, D be Real; :: thesis: for h being Function of (TOP-REAL 2),(TOP-REAL 2) st A > 0 & C > 0 & h = AffineMap (A,B,C,D) holds
( h is being_homeomorphism & ( for p1, p2 being Point of (TOP-REAL 2) st p1 `1 < p2 `1 holds
(h . p1) `1 < (h . p2) `1 ) )
let h be Function of (TOP-REAL 2),(TOP-REAL 2); :: thesis: ( A > 0 & C > 0 & h = AffineMap (A,B,C,D) implies ( h is being_homeomorphism & ( for p1, p2 being Point of (TOP-REAL 2) st p1 `1 < p2 `1 holds
(h . p1) `1 < (h . p2) `1 ) ) )
assume that
A1: A > 0 and
A2: C > 0 and
A3: h = AffineMap (A,B,C,D) ; :: thesis: ( h is being_homeomorphism & ( for p1, p2 being Point of (TOP-REAL 2) st p1 `1 < p2 `1 holds
(h . p1) `1 < (h . p2) `1 ) )
A4: h is one-to-one by A1, A2, A3, JGRAPH_2:44;
set g = AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C)));
A5: AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C))) = h " by A1, A2, A3, Th49;
A6: for p1, p2 being Point of (TOP-REAL 2) st p1 `1 < p2 `1 holds
(h . p1) `1 < (h . p2) `1
proof
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 `1 < p2 `1 implies (h . p1) `1 < (h . p2) `1 )
h . p1 = |[((A * (p1 `1)) + B),((C * (p1 `2)) + D)]| by A3, JGRAPH_2:def 2;
then A7: (h . p1) `1 = (A * (p1 `1)) + B by EUCLID:52;
h . p2 = |[((A * (p2 `1)) + B),((C * (p2 `2)) + D)]| by A3, JGRAPH_2:def 2;
then A8: (h . p2) `1 = (A * (p2 `1)) + B by EUCLID:52;
assume p1 `1 < p2 `1 ; :: thesis: (h . p1) `1 < (h . p2) `1
then A * (p1 `1) < A * (p2 `1) by A1, XREAL_1:68;
hence (h . p1) `1 < (h . p2) `1 by A7, A8, XREAL_1:8; :: thesis: verum
end;
A9: dom h = [#] (TOP-REAL 2) by FUNCT_2:def 1;
dom (AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C)))) = [#] (TOP-REAL 2) by FUNCT_2:def 1;
then A10: rng h = [#] (TOP-REAL 2) by A4, A5, FUNCT_1:32;
then ( h is onto & h is one-to-one ) by A1, A2, A3, FUNCT_2:def 3, JGRAPH_2:44;
then h /" is continuous by A5, TOPS_2:def 4;
hence ( h is being_homeomorphism & ( for p1, p2 being Point of (TOP-REAL 2) st p1 `1 < p2 `1 holds
(h . p1) `1 < (h . p2) `1 ) ) by A3, A4, A9, A10, A6, TOPS_2:def 5; :: thesis: verum