Theorem: Supremum Metric on Differentiability Class is Metric

Let $\closedint a b \subseteq \R$ be a closed real interval.
Let $r \in \N$ be a natural number.
Let $A := \mathscr D^r \closedint a b$ be the set of all continuous functions $f: \closedint a b \to \R$ which are of differentiability class $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_{\substack {x \mathop \in \closedint a b \\ i \mathop \in \set {0, 1, 2, \ldots, r} } } \size {\map {f^{\paren i} } x - \map {g^{\paren i} } x}$
where $f$ and $g$ are continuous functions on $\closedint a b$ which are of differentiability class $r$.
=== Proof of {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map d {f, f}
      | r = \sup_{\substack {x \mathop \in \closedint a b \\ i \mathop \in \set {0, 1, 2, \ldots, r} } } \size {\map {f^{\paren i} } x - \map {f^{\paren i} } x}
      | c = Definition of $d$
}}
{{eqn | r = \sup_{\substack {x \mathop \in \closedint a b \\ i \mathop \in \set {0, 1, 2, \ldots, r} } } \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 = \sup_{i \mathop \in \set {0, 1, 2, \ldots, r} } \size {\map {f^{\paren i} } c - \map {h^{\paren i} } c}
      | o = \le
      | r = \sup_{i \mathop \in \set {0, 1, 2, \ldots, r} } \size {\map {f^{\paren i} } c - \map {g^{\paren i} } c} + \sup_{i \mathop \in \set {0, 1, 2, \ldots, r} } \size {\map {g^{\paren i} } c - \map {h^{\paren i} } c}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | o = \le
      | r = \sup_{\substack {x \mathop \in \closedint a b \\ i \mathop \in \set {0, 1, 2, \ldots, r} } } \size {\map {f^{\paren i} } x - \map {g^{\paren i} } x} + \sup_{\substack {x \mathop \in \closedint a b \\ i \mathop \in \set {0, 1, 2, \ldots, r} } } \size {\map {g^{\paren i} } x - \map {h^{\paren i} } x}
      | 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:
:$\ds S := \set {\sup_{i \mathop \in \set {0, 1, 2, \ldots, r} } \size {\map {f^{\paren i} } c - \map {g^{\paren i} } 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_{\substack {x \mathop \in \closedint a b \\ i \mathop \in \set {0, 1, 2, \ldots, r} } } \size {\map {f^{\paren i} } x - \map {g^{\paren i} } x}
      | c = Definition of $d$
}}
{{eqn | r = \sup_{\substack {x \mathop \in \closedint a b \\ i \mathop \in \set {0, 1, 2, \ldots, r} } } \size {\map {g^{\paren i} } x - \map {f^{\paren i} } 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_{\substack {x \mathop \in \closedint a b \\ i \mathop \in \set {0, 1, 2, \ldots, r} } } \size {\map {f^{\paren i} } x - \map {f^{\paren i} } 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}}