Theorem: Supremum Metric on Bounded Real Functions on Closed Interval is Metric

Let $\closedint a b \subseteq \R$ be a closed real interval.
Let $A$ be the set of all bounded real functions $f: \closedint a b \to \R$.
Let $d: A \times A \to \R$ be the supremum metric on $A$.
Then $d$ is a metric.

Proof:
We have that the supremum metric on $A \times A$ is defined as:
:$\ds \forall f, g \in A: \map d {f, g} := \sup_{x \mathop \in \closedint a b} \size {\map f x - \map g x}$
where $f$ and $g$ are bounded real functions.
So:
:$\exists K, L \in \R: \size {\map f x} \le K, \size {\map g x} \le L$
for all $x \in \closedint a b$.
First note that we have:
{{begin-eqn}}
{{eqn | l = \size {\map f x - \map g x}
      | r = \size {\map f x + \paren {-\map g x} }
      | c = 
}}
{{eqn | o = \le
      | r = \size {\map f x} + \size {\paren {-\map g x} }
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | r = \size {\map f x} + \size {\map g x}
      | c = {{Defof|Absolute Value}}
}}
{{eqn | o = \le
      | r = K + L
      | c = 
}}
{{end-eqn}}
and so the {{RHS}} exists.
=== Proof of {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map d {f, f}
      | r = \sup_{x \mathop \in \closedint a b} \size {\map f x - \map f x}
      | c = Definition of $d$
}}
{{eqn | r = \sup_{x \mathop \in \closedint a b} \size 0
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|2|nolink}} ===
Let $f, g, h \in A$.
Let $c \in \closedint a b$.
{{begin-eqn}}
{{eqn | l = c
      | o = \in
      | r = \closedint a b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {\map f c - \map h c}
      | o = \le
      | r = \size {\map f c - \map g c} + \size {\map g c - \map h c}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | o = \le
      | r = \sup_{x \mathop \in \closedint a b} \size {\map f c - \map g c} + \sup_{x \mathop \in \closedint a b} \size {\map g c - \map h c}
      | c = {{Defof|Supremum of Real-Valued Function}}
}}
{{eqn | r = \map d {f, g} + \map d {g, h}
      | c = Definition of $d$
}}
{{end-eqn}}
Thus $\map d {f, g} + \map d {g, h}$ is an upper bound for:
:$S := \set {\size {\map f c - \map h c}: c \in \closedint a b}$
So:
:$\map d {f, g} + \map d {g, h} \ge \sup S = \map d {f, h}$
So {{Metric-space-axiom|2}} holds for $d$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|3|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map d {f, g}
      | r = \sup_{x \mathop \in \closedint a b} \size {\map f x - \map g x}
      | c = Definition of $d$
}}
{{eqn | r = \sup_{x \mathop \in \closedint a b} \size {\map g x - \map f x}
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = \map d {g, f}
      | c = Definition of $d$
}}
{{end-eqn}}
So {{Metric-space-axiom|3}} holds for $d$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|4|nolink}} ===
As $d$ is the supremum of the absolute value of the image of the pointwise sum of $f$ and $g$:
:$\forall f, g \in A: \map d {f, g} \ge 0$
Suppose $f, g \in A: \map d {f, g} = 0$.
Then:
{{begin-eqn}}
{{eqn | l = \map d {f, g}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sup_{x \mathop \in \closedint a b} \size {\map f x - \map g x}
      | r = 0
      | c = Definition of $d$
}}
{{eqn | ll= \leadsto
      | q = \forall x \in \closedint a b
      | l = \map f x 
      | r = \map g x
      | c = {{Defof|Absolute Value}}
}}
{{eqn | ll= \leadsto
      | l = f
      | r = g
      | c = Equality of Mappings
}}
{{end-eqn}}
So {{Metric-space-axiom|4}} holds for $d$.
{{qed}}