let X, Y, Z be RealNormSpace; for f being PartFunc of [:X,Y:],Z
for U being Subset of [:X,Y:]
for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y
for x being Point of X holds I . (y,x) = [x,y] ) holds
for a being Point of X
for b being Point of Y
for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )
let f be PartFunc of [:X,Y:],Z; for U being Subset of [:X,Y:]
for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y
for x being Point of X holds I . (y,x) = [x,y] ) holds
for a being Point of X
for b being Point of Y
for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )
let U be Subset of [:X,Y:]; for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y
for x being Point of X holds I . (y,x) = [x,y] ) holds
for a being Point of X
for b being Point of Y
for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )
let I be Function of [:Y,X:],[:X,Y:]; ( ( for y being Point of Y
for x being Point of X holds I . (y,x) = [x,y] ) implies for a being Point of X
for b being Point of Y
for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) ) )
assume A1:
for y being Point of Y
for x being Point of X holds I . (y,x) = [x,y]
; for a being Point of X
for b being Point of Y
for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )
let a be Point of X; for b being Point of Y
for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )
let b be Point of Y; for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )
let u be Point of [:X,Y:]; for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )
let v be Point of [:Y,X:]; ( u in U & u = [a,b] & v = [b,a] implies ( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) ) )
assume A2:
( u in U & u = [a,b] & v = [b,a] )
; ( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )
A3:
for x being object holds
( x in dom (f * (reproj1 u)) iff x in dom ((f * I) * (reproj2 v)) )
proof
let x be
object ;
( x in dom (f * (reproj1 u)) iff x in dom ((f * I) * (reproj2 v)) )
A4:
(
x in dom (f * (reproj1 u)) iff (
x in dom (reproj1 u) &
(reproj1 u) . x in dom f ) )
by FUNCT_1:11;
A5:
(
x in dom (f * (reproj1 u)) implies
x in dom ((f * I) * (reproj2 v)) )
proof
assume A6:
x in dom (f * (reproj1 u))
;
x in dom ((f * I) * (reproj2 v))
then A7:
x in the
carrier of
X
;
reconsider x =
x as
Point of
X by A6;
A8:
x in dom (reproj2 v)
by A7, FUNCT_2:def 1;
(reproj2 v) . x =
[(v `1),x]
by NDIFF_7:def 2
.=
[b,x]
by A2
;
then A9:
I . ((reproj2 v) . x) =
I . (
b,
x)
.=
[x,(u `2)]
by A1, A2
.=
(reproj1 u) . x
by NDIFF_7:def 1
;
(reproj2 v) . x in the
carrier of
[:Y,X:]
;
then
(reproj2 v) . x in dom I
by FUNCT_2:def 1;
then
(reproj2 v) . x in dom (f * I)
by A4, A6, A9, FUNCT_1:11;
hence
x in dom ((f * I) * (reproj2 v))
by A8, FUNCT_1:11;
verum
end;
(
x in dom ((f * I) * (reproj2 v)) implies
x in dom (f * (reproj1 u)) )
hence
(
x in dom (f * (reproj1 u)) iff
x in dom ((f * I) * (reproj2 v)) )
by A5;
verum
end;
A13:
for y being object holds
( y in dom (f * (reproj2 u)) iff y in dom ((f * I) * (reproj1 v)) )
proof
let y be
object ;
( y in dom (f * (reproj2 u)) iff y in dom ((f * I) * (reproj1 v)) )
A14:
(
y in dom (f * (reproj2 u)) iff (
y in dom (reproj2 u) &
(reproj2 u) . y in dom f ) )
by FUNCT_1:11;
A15:
(
y in dom (f * (reproj2 u)) implies
y in dom ((f * I) * (reproj1 v)) )
proof
assume A16:
y in dom (f * (reproj2 u))
;
y in dom ((f * I) * (reproj1 v))
then A17:
y in the
carrier of
Y
;
reconsider y =
y as
Point of
Y by A16;
A18:
y in dom (reproj1 v)
by A17, FUNCT_2:def 1;
(reproj1 v) . y =
[y,(v `2)]
by NDIFF_7:def 1
.=
[y,a]
by A2
;
then A19:
I . ((reproj1 v) . y) =
I . (
y,
a)
.=
[(u `1),y]
by A1, A2
.=
(reproj2 u) . y
by NDIFF_7:def 2
;
(reproj1 v) . y in the
carrier of
[:Y,X:]
;
then
(reproj1 v) . y in dom I
by FUNCT_2:def 1;
then
(reproj1 v) . y in dom (f * I)
by A14, A16, A19, FUNCT_1:11;
hence
y in dom ((f * I) * (reproj1 v))
by A18, FUNCT_1:11;
verum
end;
(
y in dom ((f * I) * (reproj1 v)) implies
y in dom (f * (reproj2 u)) )
hence
(
y in dom (f * (reproj2 u)) iff
y in dom ((f * I) * (reproj1 v)) )
by A15;
verum
end;
for x being object st x in dom (f * (reproj1 u)) holds
(f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x
hence
f * (reproj1 u) = (f * I) * (reproj2 v)
by A3, FUNCT_1:2, TARSKI:2; f * (reproj2 u) = (f * I) * (reproj1 v)
for y being object st y in dom (f * (reproj2 u)) holds
(f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y
hence
f * (reproj2 u) = (f * I) * (reproj1 v)
by A13, FUNCT_1:2, TARSKI:2; verum