let S, T be RealNormSpace; :: thesis: for f being LinearOperator of S,T holds
( f is isometric iff for x being Element of S holds ||.(f . x).|| = ||.x.|| )
let f be LinearOperator of S,T; :: thesis: ( f is isometric iff for x being Element of S holds ||.(f . x).|| = ||.x.|| )
hereby :: thesis: ( ( for x being Element of S holds ||.(f . x).|| = ||.x.|| ) implies f is isometric )
assume A1: f is isometric ; :: thesis: for x being Element of S holds ||.(f . x).|| = ||.x.||
thus for x being Element of S holds ||.(f . x).|| = ||.x.|| :: thesis: verum
proof
let x be Element of S; :: thesis: ||.(f . x).|| = ||.x.||
thus ||.(f . x).|| = ||.(f . (x - (0. S))).|| by RLVECT_1:13
.= ||.((f . x) - (f . (0. S))).|| by LM001
.= ||.(x - (0. S)).|| by A1
.= ||.x.|| by RLVECT_1:13 ; :: thesis: verum
end;
end;
assume A2: for x being Element of S holds ||.(f . x).|| = ||.x.|| ; :: thesis: f is isometric
for a, b being Point of S holds ||.((f . a) - (f . b)).|| = ||.(a - b).||
proof
let a, b be Point of S; :: thesis: ||.((f . a) - (f . b)).|| = ||.(a - b).||
thus ||.((f . a) - (f . b)).|| = ||.(f . (a - b)).|| by LM001
.= ||.(a - b).|| by A2 ; :: thesis: verum
end;
hence f is isometric ; :: thesis: verum