Theorem: Kelvin-Stokes Theorem

Let $S$ be some orientable smooth surface with boundary in $\R^3$.
Let $\mathbf F:\R^3 \to \R^3$ be a vector-valued function with Euclidean coordinate expression:
:$\mathbf F = f_1 \mathbf i + f_2 \mathbf j + f_3 \mathbf k$
where $f_i: \R^3 \to \R$.
Then:
:$\ds \oint_{\partial S} f_1 \rd x + f_2 \rd y + f_3 \rd z = \iint_S \paren {\nabla \times \mathbf F} \cdot \mathbf n \rd A$
where $\mathbf n$ is the unit normal to $S$ and $\d A$ is the area element on the surface.

Proof:
Let $\mathbf r:\R^2 \to \R^3, \map {\mathbf r} {s, t}$ be a smooth parametrization of $S$ from some region $R$ in the $st$-plane, so that:
:$\map {\mathbf r} R = S$
and:
:$\map {\mathbf r} {\partial R} = \partial S$
First, we convert the {{LHS}} into a line integral:
{{begin-eqn}}
{{eqn | l = \oint_{\partial S} f_1 \rd x + f_2 \rd y + f_3 \rd z
      | r = \oint_{\partial S} \mathbf F \cdot \rd \mathbf r
      | c = 
}}
{{eqn | r = \oint_{\partial R} \mathbf F \cdot \frac {\partial \mathbf r} {\partial s} \rd s + \mathbf F \cdot \frac {\partial \mathbf r} {\partial t} \rd t
      | c = 
}}
{{end-eqn}}
so that if we define:
:$\mathbf G = \paren {G_1, G_2} = \paren {\mathbf F \cdot \dfrac {\partial \mathbf r} {\partial s}, \mathbf F \cdot \dfrac {\partial \mathbf r} {\partial t} }$
then:
:$\ds \int_{\partial S} \mathbf F \cdot \rd \mathbf r = \int_{\partial R} \mathbf G \cdot \rd \mathbf s$
where $\mathbf s$ is the position vector in the $s t$-plane. 
Note that:
{{begin-eqn}}
{{eqn | l = \frac {\partial G_2} {\partial s}
      | r = \mathbf F \cdot \map {\frac \partial {\partial s} } {\frac {\partial \mathbf r} {\partial t} } + \frac {\partial \mathbf r} {\partial t} \cdot \frac {\partial \mathbf F} {\partial s}
      | c = Derivative of Dot Product of Vector-Valued Functions
}}
{{eqn | l = \frac {\partial G_1} {\partial t}
      | r = \mathbf F \cdot \map {\frac \partial {\partial t} } {\frac {\partial \mathbf r} {\partial s} } + \frac {\partial \mathbf r} {\partial s} \cdot \frac {\partial \mathbf F} {\partial t}
      | c = Derivative of Dot Product of Vector-Valued Functions
}}
{{eqn | l = \frac {\partial G_2} {\partial s} - \frac {\partial G_1} {\partial t}
      | r = \mathbf F \cdot \map {\frac \partial {\partial s} } {\frac {\partial \mathbf r} {\partial t} } + \frac {\partial \mathbf r} {\partial t} \cdot \frac {\partial \mathbf F} {\partial s}
      | c =
}}
{{eqn | o =
      | ro= -
      | r = \mathbf F \cdot \map {\frac \partial {\partial t} } {\frac {\partial \mathbf r} {\partial s} } - \frac {\partial \mathbf r} {\partial s} \cdot \frac {\partial \mathbf F} {\partial t}       
      | c =
}}
{{eqn | r = \frac {\partial \mathbf r} {\partial t} \cdot \frac {\partial \mathbf F} {\partial s} - \frac {\partial \mathbf r} {\partial s} \cdot \frac {\partial \mathbf F} {\partial t}
      | c = Symmetry of Second Derivatives
}}
{{end-eqn}}
We turn now to the expression on the {{RHS}} and write it in terms of $s$ and $t$:
{{begin-eqn}}
{{eqn | o = 
      | r = \iint_S \paren {\nabla \times \mathbf F} \cdot \mathbf n \rd A
      | c = 
}}
{{eqn | r = \iint_R \paren {\nabla \times \mathbf F \cdot \paren {\frac {\partial \mathbf r} {\partial s} \times \frac {\partial \mathbf r} {\partial t} } } \rd s \rd t
      | c = 
}}
{{end-eqn}}
Let us investigate the integrand:
{{begin-eqn}}
{{eqn | o =  
      | r = \nabla \times \mathbf F \cdot \paren {\frac {\partial \mathbf r} {\partial s} \times \frac {\partial \mathbf r} {\partial t} }
      | c = 
}}
{{eqn | r = <nowiki>\paren {\paren {\dfrac {\partial f_3} {\partial y} - \dfrac {\partial f_2} {\partial z} } \mathbf i
          + \paren {\dfrac {\partial f_1} {\partial z} - \dfrac {\partial f_3} {\partial x} } \mathbf j
          + \paren {\dfrac {\partial f_2} {\partial x} - \dfrac {\partial f_1} {\partial y} } \mathbf k}</nowiki>
      | c = {{Defof|Curl Operator}}
}}
{{eqn | o =  
      | ro= \cdot 
      | r = <nowiki>\paren {\paren {\dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t} - \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t} } \mathbf i + \paren {\dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t} - \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t} } \mathbf j + \paren {\dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t} - \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t} } \mathbf k}</nowiki>
      | c = {{Defof|Cross Product}}
}}
{{eqn | r = \paren {\dfrac {\partial f_3} {\partial y} - \dfrac {\partial f_2} {\partial z} } \paren {\dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t} - \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t} }
}}
{{eqn | o =
      | ro= +
      | r = \paren {\dfrac {\partial f_1} {\partial z} - \dfrac {\partial f_3} {\partial x} } \paren {\dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t} - \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t} }
}}
{{eqn | o =
      | ro= + 
      | r = \paren {\dfrac {\partial f_2} {\partial x} - \dfrac {\partial f_1} {\partial y} } \paren {\dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t} - \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t} }
      | c = {{Defof|Dot Product}}
}}
{{eqn | r = <nowiki>\dfrac {\partial f_3} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
          - \dfrac {\partial f_3} {\partial y} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}
          - \dfrac {\partial f_2} {\partial z} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_2} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= + 
      | r = <nowiki>\dfrac {\partial f_1} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}
          - \dfrac {\partial f_1} {\partial z} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t}
          - \dfrac {\partial f_3} {\partial x} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_3} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t}</nowiki>              
}}
{{eqn | o =
      | ro= + 
      | r = <nowiki>\dfrac {\partial f_2} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
          - \dfrac {\partial f_2} {\partial x} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}
          - \dfrac {\partial f_1} {\partial y} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_1} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}</nowiki>
      | c = 
}}
{{eqn | r = <nowiki>\dfrac {\partial f_1} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}
          - \dfrac {\partial f_1} {\partial z} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t}
          - \dfrac {\partial f_1} {\partial y} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_1} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= - 
      | r = <nowiki>\dfrac {\partial f_2} {\partial z} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_2} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_2} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
          - \dfrac {\partial f_2} {\partial x} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= + 
      | r = <nowiki>\dfrac {\partial f_3} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
          - \dfrac {\partial f_3} {\partial y} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}
          - \dfrac {\partial f_3} {\partial x} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_3} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t}</nowiki>
      | c = grouping the terms that reference like components of $\mathbf F$ together
}}
{{eqn | r = <nowiki>\dfrac {\partial f_1} {\partial z} \dfrac {\partial z} {\partial s} \dfrac{\partial x}{\partial t}
          - \dfrac {\partial f_1} {\partial z} \dfrac {\partial x} {\partial s} \dfrac{\partial z}{\partial t}
          - \dfrac {\partial f_1} {\partial y} \dfrac {\partial x} {\partial s} \dfrac{\partial y}{\partial t}
          + \dfrac {\partial f_1} {\partial y} \dfrac {\partial y} {\partial s} \dfrac{\partial x}{\partial t}</nowiki>
}}
{{eqn | o = 
      | ro= +
      | r = <nowiki>\paren {\dfrac {\partial f_1} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial x} {\partial t}
                  - \dfrac {\partial f_1} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial x} {\partial t} }</nowiki>
}}
{{eqn | o = 
      | ro= -
      | r = <nowiki>\dfrac {\partial f_2} {\partial z} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_2} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_2} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
          - \dfrac {\partial f_2} {\partial x} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}</nowiki>
}}
{{eqn | o = 
      | ro= +
      | r = <nowiki>\paren {\dfrac {\partial f_2} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial y} {\partial t}
                  - \dfrac {\partial f_2} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial y} {\partial t} }</nowiki>
}}
{{eqn | o = 
      | ro= +
      | r = <nowiki>\dfrac {\partial f_3} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
          - \dfrac {\partial f_3} {\partial y} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}
          - \dfrac {\partial f_3} {\partial x} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_3} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t}</nowiki>
}}
{{eqn | o = 
      | ro= +
      | r = <nowiki>\paren {\dfrac {\partial f_3} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial z} {\partial t}
                  - \dfrac {\partial f_3} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial z} {\partial t} }</nowiki>
      | c = introducing terms that themselves sum to zero, in order to complete the parts of the derivatives of $\mathbf F$ in a later step
}}
{{eqn | r = <nowiki>\dfrac {\partial f_1} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_1} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_1} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial x} {\partial t}</nowiki>
}}
{{eqn | o = 
      | ro= +
      | r = <nowiki>\paren {- \dfrac {\partial f_1} {\partial z} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t}
                    - \dfrac {\partial f_1} {\partial y} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
                    - \dfrac {\partial f_1} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial x} {\partial t} }</nowiki>
}}
{{eqn | o = 
      | ro= +
      | r = <nowiki>\dfrac {\partial f_2} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_2} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_2} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial y} {\partial t}</nowiki>
}}
{{eqn | o = 
      | ro= +
      | r = <nowiki>\paren {- \dfrac {\partial f_2} {\partial z} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
                    - \dfrac {\partial f_2} {\partial x} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}
                    - \dfrac {\partial f_2} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial y} {\partial t} }</nowiki>
}}
{{eqn | o = 
      | ro= +
      | r = <nowiki>\dfrac {\partial f_3} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_3} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_3} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial z} {\partial t}</nowiki>
}}
{{eqn | o = 
      | ro= +
      | r = <nowiki>\paren {- \dfrac {\partial f_3} {\partial y} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}
                    - \dfrac {\partial f_3} {\partial x} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}
                    - \dfrac {\partial f_3} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial z} {\partial t} }</nowiki>
      | c = grouping terms by sign, but keeping terms that reference like components of $\mathbf F$ together
}}
{{eqn | r = <nowiki>\dfrac {\partial f_1} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_1} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_1} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial x} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= +
      | r = <nowiki>\dfrac {\partial f_2} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_2} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_2} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial y} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= +
      | r = <nowiki>\dfrac {\partial f_3} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_3} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_3} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial z} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= -
      | r = <nowiki>\leftparen {\dfrac {\partial f_1} {\partial z} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_1} {\partial y} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_1} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial x} {\partial t} }</nowiki>
}}
{{eqn | o =
      | ro= +
      | r = <nowiki>\dfrac {\partial f_2} {\partial z} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_2} {\partial x} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_2} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial y} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= +
      | r = <nowiki>\rightparen {\dfrac {\partial f_3} {\partial y} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_3} {\partial x} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_3} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial z} {\partial t} }</nowiki>
      | c = grouping all negative terms together and factoring out the negative sign
}} 
{{eqn | r = <nowiki>\dfrac {\partial f_1} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_1} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_1} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= +
      | r = <nowiki>\dfrac {\partial f_2} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_2} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_2} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= +
      | r = <nowiki>\dfrac {\partial f_3} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_3} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}
          + \dfrac {\partial f_3} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial z} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= - 
      | r = <nowiki>\leftparen {\dfrac {\partial f_1} {\partial x} \dfrac {\partial x} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_1} {\partial y} \dfrac {\partial x} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_1} {\partial z} \dfrac {\partial x} {\partial s} \dfrac {\partial z} {\partial t} }</nowiki>
}}
{{eqn | o =
      | ro= +
      | r = <nowiki>\dfrac {\partial f_2} {\partial x} \dfrac {\partial y} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_2} {\partial y} \dfrac {\partial y} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_2} {\partial z} \dfrac {\partial y} {\partial s} \dfrac {\partial z} {\partial t}</nowiki>
}}
{{eqn | o =
      | ro= +
      | r = <nowiki>\rightparen {\dfrac {\partial f_3} {\partial x} \dfrac {\partial z} {\partial s} \dfrac {\partial x} {\partial t}
          + \dfrac {\partial f_3} {\partial y} \dfrac {\partial z} {\partial s} \dfrac {\partial y} {\partial t}
          + \dfrac {\partial f_3} {\partial z} \dfrac {\partial z} {\partial s} \dfrac {\partial z} {\partial t} }</nowiki>
      | c = rearranging into groups, in order to clarify use of the Chain Rule for Real-Valued Functions in the next step
}} 
{{eqn | r = <nowiki>\paren {\dfrac {\partial f_1} {\partial s} \dfrac {\partial x} {\partial t}
                  + \dfrac {\partial f_2} {\partial s} \dfrac {\partial y} {\partial t}
                  + \dfrac {\partial f_3} {\partial s} \dfrac {\partial z} {\partial t} }</nowiki>
}}
{{eqn | o =
      | ro= -
      | r = <nowiki>\paren {\dfrac {\partial f_1} {\partial t} \dfrac {\partial x} {\partial t}
                  + \dfrac {\partial f_2} {\partial t} \dfrac {\partial y} {\partial t}
                  + \dfrac {\partial f_3} {\partial t} \dfrac {\partial z} {\partial t} }</nowiki>
      | c = Chain Rule for Real-Valued Functions
}}
{{eqn | r = <nowiki>\dfrac {\partial \mathbf F} {\partial s} \cdot \dfrac {\partial \mathbf r} {\partial t}
          - \dfrac {\partial \mathbf F} {\partial t} \cdot \dfrac {\partial \mathbf r} {\partial s}</nowiki>
      | c = {{Defof|Dot Product}}
}}
{{eqn | r = \frac {\partial G_2} {\partial s} - \frac {\partial G_1} {\partial t}
      | c =
}}
{{end-eqn}}
That is:
:$\ds \iint_S \paren {\nabla \times \mathbf F} \cdot \mathbf n \rd A = \iint_R \paren {\frac {\partial G_2} {\partial s} - \frac {\partial G_1} {\partial t} } \rd s \rd t$
By Green's Theorem, this can be written as:
:$\ds \int_{\partial R} \mathbf G \cdot \rd \mathbf s$
Hence both sides of the theorem equation are equal.
{{qed}}