defpred S1[ object , object , object ] means $3 = [$2,$1];
A1:
for x being Element of the carrier of X
for y being Element of the carrier of Y ex z being Element of the carrier of [:Y,X:] st S1[x,y,z]
proof
let x be
Element of the
carrier of
X;
for y being Element of the carrier of Y ex z being Element of the carrier of [:Y,X:] st S1[x,y,z]let y be
Element of the
carrier of
Y;
ex z being Element of the carrier of [:Y,X:] st S1[x,y,z]
[y,x] is
Point of
[:Y,X:]
;
hence
ex
z being
Element of the
carrier of
[:Y,X:] st
S1[
x,
y,
z]
;
verum
end;
consider f being Function of [: the carrier of X, the carrier of Y:], the carrier of [:Y,X:] such that
A2:
for x being Element of the carrier of X
for y being Element of the carrier of Y holds S1[x,y,f . (x,y)]
from BINOP_1:sch 3(A1);
reconsider f = f as Function of [:X,Y:],[:Y,X:] ;
for p1, p2 being Point of [:X,Y:] holds f . (p1 + p2) = (f . p1) + (f . p2)
proof
let p1,
p2 be
Point of
[:X,Y:];
f . (p1 + p2) = (f . p1) + (f . p2)
consider x1 being
Point of
X,
y1 being
Point of
Y such that A4:
p1 = [x1,y1]
by PRVECT_3:18;
consider x2 being
Point of
X,
y2 being
Point of
Y such that A5:
p2 = [x2,y2]
by PRVECT_3:18;
reconsider q1 =
[y1,x1] as
Point of
[:Y,X:] ;
reconsider q2 =
[y2,x2] as
Point of
[:Y,X:] ;
A8:
f . p1 =
f . (
x1,
y1)
by A4
.=
q1
by A2
;
A9:
f . p2 =
f . (
x2,
y2)
by A5
.=
q2
by A2
;
thus f . (p1 + p2) =
f . (
(x1 + x2),
(y1 + y2))
by A4, A5, PRVECT_3:18
.=
[(y1 + y2),(x1 + x2)]
by A2
.=
(f . p1) + (f . p2)
by A8, A9, PRVECT_3:18
;
verum
end;
then A10:
f is additive
;
for p being Point of [:X,Y:]
for r being Real holds f . (r * p) = r * (f . p)
proof
let p be
Point of
[:X,Y:];
for r being Real holds f . (r * p) = r * (f . p)let r be
Real;
f . (r * p) = r * (f . p)
consider x being
Point of
X,
y being
Point of
Y such that A11:
p = [x,y]
by PRVECT_3:18;
reconsider q =
[y,x] as
Point of
[:Y,X:] ;
reconsider rq =
[(r * y),(r * x)] as
Point of
[:Y,X:] ;
A12:
f . p =
f . (
x,
y)
by A11
.=
q
by A2
;
thus f . (r * p) =
f . (
(r * x),
(r * y))
by A11, PRVECT_3:18
.=
[(r * y),(r * x)]
by A2
.=
r * (f . p)
by A12, PRVECT_3:18
;
verum
end;
then reconsider f = f as LinearOperator of [:X,Y:],[:Y,X:] by A10, LOPBAN_1:def 5;
take
f
; ( f is one-to-one & f is onto & f is isometric & ( for x being Point of X
for y being Point of Y holds f . (x,y) = [y,x] ) )
A14:
for p1, p2 being object st p1 in the carrier of [:X,Y:] & p2 in the carrier of [:X,Y:] & f . p1 = f . p2 holds
p1 = p2
proof
let p1,
p2 be
object ;
( p1 in the carrier of [:X,Y:] & p2 in the carrier of [:X,Y:] & f . p1 = f . p2 implies p1 = p2 )
assume A15:
(
p1 in the
carrier of
[:X,Y:] &
p2 in the
carrier of
[:X,Y:] &
f . p1 = f . p2 )
;
p1 = p2
consider x1 being
Point of
X,
y1 being
Point of
Y such that A16:
p1 = [x1,y1]
by A15, PRVECT_3:18;
consider x2 being
Point of
X,
y2 being
Point of
Y such that A17:
p2 = [x2,y2]
by A15, PRVECT_3:18;
A18:
f . p1 =
f . (
x1,
y1)
by A16
.=
[y1,x1]
by A2
;
f . p2 =
f . (
x2,
y2)
by A17
.=
[y2,x2]
by A2
;
then
(
x1 = x2 &
y1 = y2 )
by A15, A18, XTUPLE_0:1;
hence
p1 = p2
by A16, A17;
verum
end;
for q being object st q in the carrier of [:Y,X:] holds
q in rng f
then
rng f = the carrier of [:Y,X:]
by TARSKI:def 3;
hence
( f is one-to-one & f is onto )
by A14, FUNCT_2:19; ( f is isometric & ( for x being Point of X
for y being Point of Y holds f . (x,y) = [y,x] ) )
for p being Point of [:X,Y:] holds ||.(f . p).|| = ||.p.||
proof
let p be
Point of
[:X,Y:];
||.(f . p).|| = ||.p.||
consider x being
Point of
X,
y being
Point of
Y such that A23:
p = [x,y]
by PRVECT_3:18;
reconsider q =
[y,x] as
Point of
[:Y,X:] ;
A24:
f . p =
f . (
x,
y)
by A23
.=
q
by A2
;
consider u being
Element of
REAL 2
such that A25:
(
u = <*||.x.||,||.y.||*> &
||.p.|| = |.u.| )
by A23, PRVECT_3:18;
consider v being
Element of
REAL 2
such that A26:
(
v = <*||.y.||,||.x.||*> &
||.q.|| = |.v.| )
by PRVECT_3:18;
thus
||.(f . p).|| = ||.p.||
by A24, A25, A26, Th6;
verum
end;
hence
f is isometric
by NDIFF_7:7; for x being Point of X
for y being Point of Y holds f . (x,y) = [y,x]
thus
for x being Point of X
for y being Point of Y holds f . (x,y) = [y,x]
by A2; verum