let X, Y, Z be RealNormSpace; :: thesis: 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; :: thesis: 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:]; :: thesis: 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:]; :: thesis: ( ( 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] ; :: thesis: 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; :: thesis: 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; :: thesis: 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:]; :: thesis: 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:]; :: thesis: ( 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] ) ; :: thesis: ( 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 ; :: thesis: ( 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)) ; :: thesis: 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; :: thesis: verum
end;
( x in dom ((f * I) * (reproj2 v)) implies x in dom (f * (reproj1 u)) )
proof
assume A10: x in dom ((f * I) * (reproj2 v)) ; :: thesis: x in dom (f * (reproj1 u))
then A11: ( x in dom (reproj2 v) & (reproj2 v) . x in dom (f * I) ) by FUNCT_1:11;
reconsider x = x as Point of X by A10;
(reproj2 v) . x = [(v `1),x] by NDIFF_7:def 2
.= [b,x] by A2 ;
then I . ((reproj2 v) . x) = I . (b,x)
.= [x,(u `2)] by A1, A2
.= (reproj1 u) . x by NDIFF_7:def 1 ;
then A12: (reproj1 u) . x in dom f by A11, FUNCT_1:11;
dom (reproj1 u) = the carrier of X by FUNCT_2:def 1;
hence x in dom (f * (reproj1 u)) by A12, FUNCT_1:11; :: thesis: verum
end;
hence ( x in dom (f * (reproj1 u)) iff x in dom ((f * I) * (reproj2 v)) ) by A5; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: 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; :: thesis: verum
end;
( y in dom ((f * I) * (reproj1 v)) implies y in dom (f * (reproj2 u)) )
proof
assume A20: y in dom ((f * I) * (reproj1 v)) ; :: thesis: y in dom (f * (reproj2 u))
then A21: ( y in dom (reproj1 v) & (reproj1 v) . y in dom (f * I) ) by FUNCT_1:11;
reconsider y = y as Point of Y by A20;
(reproj1 v) . y = [y,(v `2)] by NDIFF_7:def 1
.= [y,a] by A2 ;
then I . ((reproj1 v) . y) = I . (y,a)
.= [(u `1),y] by A1, A2
.= (reproj2 u) . y by NDIFF_7:def 2 ;
then A22: (reproj2 u) . y in dom f by A21, FUNCT_1:11;
dom (reproj2 u) = the carrier of Y by FUNCT_2:def 1;
hence y in dom (f * (reproj2 u)) by A22, FUNCT_1:11; :: thesis: verum
end;
hence ( y in dom (f * (reproj2 u)) iff y in dom ((f * I) * (reproj1 v)) ) by A15; :: thesis: verum
end;
for x being object st x in dom (f * (reproj1 u)) holds
(f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x
proof
let x be object ; :: thesis: ( x in dom (f * (reproj1 u)) implies (f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x )
assume A23: x in dom (f * (reproj1 u)) ; :: thesis: (f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x
then reconsider x = x as Point of X ;
A24: (reproj1 u) . x = [x,(u `2)] by NDIFF_7:def 1
.= I . (b,x) by A1, A2
.= I . [(v `1),x] by A2
.= I . ((reproj2 v) . x) by NDIFF_7:def 2 ;
(reproj2 v) . x in the carrier of [:Y,X:] ;
then A25: (reproj2 v) . x in dom I by FUNCT_2:def 1;
A26: dom (reproj2 v) = the carrier of X by FUNCT_2:def 1;
(f * (reproj1 u)) . x = f . (I . ((reproj2 v) . x)) by A23, A24, FUNCT_1:12
.= (f * I) . ((reproj2 v) . x) by A25, FUNCT_1:13
.= ((f * I) * (reproj2 v)) . x by A26, FUNCT_1:13 ;
hence (f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x ; :: thesis: verum
end;
hence f * (reproj1 u) = (f * I) * (reproj2 v) by A3, FUNCT_1:2, TARSKI:2; :: thesis: 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
proof
let y be object ; :: thesis: ( y in dom (f * (reproj2 u)) implies (f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y )
assume A27: y in dom (f * (reproj2 u)) ; :: thesis: (f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y
then reconsider y = y as Point of Y ;
A28: (reproj2 u) . y = [(u `1),y] by NDIFF_7:def 2
.= I . (y,a) by A1, A2
.= I . [y,(v `2)] by A2
.= I . ((reproj1 v) . y) by NDIFF_7:def 1 ;
(reproj1 v) . y in the carrier of [:Y,X:] ;
then A29: (reproj1 v) . y in dom I by FUNCT_2:def 1;
A30: dom (reproj1 v) = the carrier of Y by FUNCT_2:def 1;
(f * (reproj2 u)) . y = f . (I . ((reproj1 v) . y)) by A27, A28, FUNCT_1:12
.= (f * I) . ((reproj1 v) . y) by A29, FUNCT_1:13
.= ((f * I) * (reproj1 v)) . y by A30, FUNCT_1:13 ;
hence (f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y ; :: thesis: verum
end;
hence f * (reproj2 u) = (f * I) * (reproj1 v) by A13, FUNCT_1:2, TARSKI:2; :: thesis: verum