let A, B, C, D be Real; for h, g being Function of (TOP-REAL 2),(TOP-REAL 2) st A > 0 & C > 0 & h = AffineMap (A,B,C,D) & g = AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C))) holds
( g = h " & h = g " )
let h, g be Function of (TOP-REAL 2),(TOP-REAL 2); ( A > 0 & C > 0 & h = AffineMap (A,B,C,D) & g = AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C))) implies ( g = h " & h = g " ) )
assume that
A1:
A > 0
and
A2:
C > 0
and
A3:
h = AffineMap (A,B,C,D)
and
A4:
g = AffineMap ((1 / A),(- (B / A)),(1 / C),(- (D / C)))
; ( g = h " & h = g " )
A5:
h is one-to-one
by A1, A2, A3, JGRAPH_2:44;
A6:
for x, y being object st x in dom h & y in dom g holds
( h . x = y iff g . y = x )
proof
let x,
y be
object ;
( x in dom h & y in dom g implies ( h . x = y iff g . y = x ) )
assume that A7:
x in dom h
and A8:
y in dom g
;
( h . x = y iff g . y = x )
reconsider py =
y as
Point of
(TOP-REAL 2) by A8;
reconsider px =
x as
Point of
(TOP-REAL 2) by A7;
A9:
(
h . x = y implies
g . y = x )
proof
assume A10:
h . x = y
;
g . y = x
A11:
h . px = |[((A * (px `1)) + B),((C * (px `2)) + D)]|
by A3, JGRAPH_2:def 2;
then
py `1 = (A * (px `1)) + B
by A10, EUCLID:52;
then A12:
((1 / A) * (py `1)) + (- (B / A)) =
((((1 / A) * A) * (px `1)) + ((1 / A) * B)) + (- (B / A))
.=
((1 * (px `1)) + ((1 / A) * B)) + (- (B / A))
by A1, XCMPLX_1:106
.=
((px `1) + (B / A)) + (- (B / A))
by XCMPLX_1:99
.=
px `1
;
py `2 = (C * (px `2)) + D
by A10, A11, EUCLID:52;
then A13:
((1 / C) * (py `2)) + (- (D / C)) =
((((1 / C) * C) * (px `2)) + ((1 / C) * D)) + (- (D / C))
.=
((1 * (px `2)) + ((1 / C) * D)) + (- (D / C))
by A2, XCMPLX_1:106
.=
((px `2) + (D / C)) + (- (D / C))
by XCMPLX_1:99
.=
px `2
;
g . py = |[(((1 / A) * (py `1)) + (- (B / A))),(((1 / C) * (py `2)) + (- (D / C)))]|
by A4, JGRAPH_2:def 2;
hence
g . y = x
by A12, A13, EUCLID:53;
verum
end;
(
g . y = x implies
h . x = y )
proof
assume A14:
g . y = x
;
h . x = y
A15:
g . py = |[(((1 / A) * (py `1)) + (- (B / A))),(((1 / C) * (py `2)) + (- (D / C)))]|
by A4, JGRAPH_2:def 2;
then
px `1 = ((1 / A) * (py `1)) + (- (B / A))
by A14, EUCLID:52;
then A16:
(A * (px `1)) + B =
(((A * (1 / A)) * (py `1)) + (A * (- (B / A)))) + B
.=
((1 * (py `1)) + (A * (- (B / A)))) + B
by A1, XCMPLX_1:106
.=
((py `1) + (A * ((- B) / A))) + B
by XCMPLX_1:187
.=
((py `1) + (- B)) + B
by A1, XCMPLX_1:87
.=
py `1
;
px `2 = ((1 / C) * (py `2)) + (- (D / C))
by A14, A15, EUCLID:52;
then A17:
(C * (px `2)) + D =
(((C * (1 / C)) * (py `2)) + (C * (- (D / C)))) + D
.=
((1 * (py `2)) + (C * (- (D / C)))) + D
by A2, XCMPLX_1:106
.=
((py `2) + (C * ((- D) / C))) + D
by XCMPLX_1:187
.=
((py `2) + (- D)) + D
by A2, XCMPLX_1:87
.=
py `2
;
h . px = |[((A * (px `1)) + B),((C * (px `2)) + D)]|
by A3, JGRAPH_2:def 2;
hence
h . x = y
by A16, A17, EUCLID:53;
verum
end;
hence
(
h . x = y iff
g . y = x )
by A9;
verum
end;
A18:
dom g = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
reconsider RD = D as Real ;
reconsider RC = C as Real ;
reconsider RB = B as Real ;
reconsider RA = A as Real ;
A19:
g = AffineMap ((1 / RA),(- (RB / RA)),(1 / RC),(- (RD / RC)))
by A4;
h = AffineMap (RA,RB,RC,RD)
by A3;
then
h is onto
by A1, A2, JORDAN1K:36;
then A20:
rng h = the carrier of (TOP-REAL 2)
by FUNCT_2:def 3;
A21:
1 / C > 0
by A2, XREAL_1:139;
1 / A > 0
by A1, XREAL_1:139;
then
g is onto
by A21, A19, JORDAN1K:36;
then A22:
rng g = the carrier of (TOP-REAL 2)
by FUNCT_2:def 3;
dom h = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
then
g = h "
by A5, A18, A20, A22, A6, FUNCT_1:38;
hence
( g = h " & h = g " )
by A5, FUNCT_1:43; verum