let V be RealNormSpace; :: thesis: for V1 being SubRealNormSpace of V holds TopSpaceNorm V1 is SubSpace of TopSpaceNorm V
let V1 be SubRealNormSpace of V; :: thesis: TopSpaceNorm V1 is SubSpace of TopSpaceNorm V
A1: the carrier of (MetricSpaceNorm V1) c= the carrier of (MetricSpaceNorm V) by DUALSP01:def 16;
for x, y being Point of (MetricSpaceNorm V1) holds the distance of (MetricSpaceNorm V1) . (x,y) = the distance of (MetricSpaceNorm V) . (x,y)
proof
let x, y be Point of (MetricSpaceNorm V1); :: thesis: the distance of (MetricSpaceNorm V1) . (x,y) = the distance of (MetricSpaceNorm V) . (x,y)
reconsider x1 = x, y1 = y as Point of V1 ;
reconsider x2 = x, y2 = y as Point of V by A1;
- y1 = (- 1) * y1 by RLVECT_1:16
.= (- 1) * y2 by NORMSP_3:28
.= - y2 by RLVECT_1:16 ;
then A2: x1 - y1 = x2 - y2 by NORMSP_3:28;
thus the distance of (MetricSpaceNorm V1) . (x,y) = ||.(x1 - y1).|| by NORMSP_2:def 1
.= ||.(x2 - y2).|| by A2, NORMSP_3:28
.= the distance of (MetricSpaceNorm V) . (x,y) by NORMSP_2:def 1 ; :: thesis: verum
end;
then MetricSpaceNorm V1 is SubSpace of MetricSpaceNorm V by A1, TOPMETR:def 1;
hence TopSpaceNorm V1 is SubSpace of TopSpaceNorm V by TOPMETR:13; :: thesis: verum