[STATEMENT]
lemma line_integral_primitive_lemma: (*Only for real normed fields, i.e. vectors with products*)
  fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a::{euclidean_space,real_normed_field}" and
        g :: "real \<Rightarrow> 'a"
  assumes "\<And>(a::'a). a \<in> s \<Longrightarrow> (f has_field_derivative (f' a)) (at a within s)"
      and "g piecewise_differentiable_on {0::real..1}"  "\<And>x. x \<in> {0..1} \<Longrightarrow> g x \<in> s"
      and "base_vec \<in> Basis"
    shows "((\<lambda>x. ((f'(g x)) * (vector_derivative g (at x within {0..1}))) \<bullet> base_vec)
             has_integral (((f(g 1)) \<bullet> base_vec - (f(g 0)) \<bullet> base_vec))) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
obtain k where k: "finite k" "\<forall>x\<in>{0..1} - k. g differentiable (at x within {0..1})" and cg: "continuous_on {0..1} g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. \<lbrakk>finite k; \<forall>x\<in>{0..1} - k. g differentiable at x within {0..1}; continuous_on {0..1} g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> s \<Longrightarrow> (f has_field_derivative f' ?a) (at ?a within s)
g piecewise_differentiable_on {0..1}
?x \<in> {0..1} \<Longrightarrow> g ?x \<in> s
base_vec \<in> Basis

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>finite k; \<forall>x\<in>{0..1} - k. g differentiable at x within {0..1}; continuous_on {0..1} g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: piecewise_differentiable_on_def)
[PROOF STATE]
proof (state)
this:
finite k
\<forall>x\<in>{0..1} - k. g differentiable at x within {0..1}
continuous_on {0..1} g

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
have cfg: "continuous_on {0..1} (\<lambda>x. f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. f (g x))
[PROOF STEP]
apply (rule continuous_on_compose [OF cg, unfolded o_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (g ` {0..1}) f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> s \<Longrightarrow> (f has_field_derivative f' ?a) (at ?a within s)
g piecewise_differentiable_on {0..1}
?x \<in> {0..1} \<Longrightarrow> g ?x \<in> s
base_vec \<in> Basis

goal (1 subgoal):
 1. continuous_on (g ` {0..1}) f
[PROOF STEP]
apply (metis field_differentiable_def field_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>x. f (g x))

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>x. f (g x))

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
fix x::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
assume a: "0 < x" and b: "x < 1" and xk: "x \<notin> k"
[PROOF STATE]
proof (state)
this:
0 < x
x < 1
x \<notin> k

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < x
x < 1
x \<notin> k
[PROOF STEP]
have "g differentiable at x within {0..1}"
[PROOF STATE]
proof (prove)
using this:
0 < x
x < 1
x \<notin> k

goal (1 subgoal):
 1. g differentiable at x within {0..1}
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
0 < x
x < 1
x \<notin> k
finite k
\<forall>x\<in>{0..1} - k. g differentiable at x within {0..1}

goal (1 subgoal):
 1. g differentiable at x within {0..1}
[PROOF STEP]
by (simp add: differentiable_at_withinI)
[PROOF STATE]
proof (state)
this:
g differentiable at x within {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g differentiable at x within {0..1}
[PROOF STEP]
have "(g has_vector_derivative vector_derivative g (at x within {0..1})) (at x within {0..1})"
[PROOF STATE]
proof (prove)
using this:
g differentiable at x within {0..1}

goal (1 subgoal):
 1. (g has_vector_derivative vector_derivative g (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
by (simp add: vector_derivative_works has_field_derivative_def scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
(g has_vector_derivative vector_derivative g (at x within {0..1})) (at x within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(g has_vector_derivative vector_derivative g (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
have gdiff: "(g has_derivative (\<lambda>u. of_real u * vector_derivative g (at x within {0..1}))) (at x within {0..1})"
[PROOF STATE]
proof (prove)
using this:
(g has_vector_derivative vector_derivative g (at x within {0..1})) (at x within {0..1})

goal (1 subgoal):
 1. (g has_derivative (\<lambda>u. of_real u * vector_derivative g (at x within {0..1}))) (at x within {0..1})
[PROOF STEP]
by (simp add: has_vector_derivative_def scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
(g has_derivative (\<lambda>u. of_real u * vector_derivative g (at x within {0..1}))) (at x within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_field_derivative f' (g x)) (at (g x) within g ` {0..1})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> s \<Longrightarrow> (f has_field_derivative f' ?a) (at ?a within s)
g piecewise_differentiable_on {0..1}
?x \<in> {0..1} \<Longrightarrow> g ?x \<in> s
base_vec \<in> Basis

goal (1 subgoal):
 1. (f has_field_derivative f' (g x)) (at (g x) within g ` {0..1})
[PROOF STEP]
by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def)
[PROOF STATE]
proof (state)
this:
(f has_field_derivative f' (g x)) (at (g x) within g ` {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(f has_field_derivative f' (g x)) (at (g x) within g ` {0..1})
[PROOF STEP]
have fdiff: "(f has_derivative (*) (f' (g x))) (at (g x) within g ` {0..1})"
[PROOF STATE]
proof (prove)
using this:
(f has_field_derivative f' (g x)) (at (g x) within g ` {0..1})

goal (1 subgoal):
 1. (f has_derivative (*) (f' (g x))) (at (g x) within g ` {0..1})
[PROOF STEP]
by (simp add: has_field_derivative_def)
[PROOF STATE]
proof (state)
this:
(f has_derivative (*) (f' (g x))) (at (g x) within g ` {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
have "((\<lambda>x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {0..1})) (at x within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
using diff_chain_within [OF gdiff fdiff]
[PROOF STATE]
proof (prove)
using this:
(f \<circ> g has_derivative (*) (f' (g x)) \<circ> (\<lambda>u. of_real u * vector_derivative g (at x within {0..1}))) (at x within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
by (simp add: has_vector_derivative_def scaleR_conv_of_real o_def mult_ac)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {0..1})) (at x within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?x2; ?x2 < 1; ?x2 \<notin> k\<rbrakk> \<Longrightarrow> ((\<lambda>x. f (g x)) has_vector_derivative f' (g ?x2) * vector_derivative g (at ?x2 within {0..1})) (at ?x2 within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < ?x2; ?x2 < 1; ?x2 \<notin> k\<rbrakk> \<Longrightarrow> ((\<lambda>x. f (g x)) has_vector_derivative f' (g ?x2) * vector_derivative g (at ?x2 within {0..1})) (at ?x2 within {0..1})
[PROOF STEP]
have *: "\<And>x. x\<in>{0<..<1} - k \<Longrightarrow> ((\<lambda>x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {0..1})) (at x within {0..1})"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?x2; ?x2 < 1; ?x2 \<notin> k\<rbrakk> \<Longrightarrow> ((\<lambda>x. f (g x)) has_vector_derivative f' (g ?x2) * vector_derivative g (at ?x2 within {0..1})) (at ?x2 within {0..1})

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - k \<Longrightarrow> ((\<lambda>x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {0..1})) (at x within {0..1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> {0<..<1} - k \<Longrightarrow> ((\<lambda>x. f (g x)) has_vector_derivative f' (g ?x) * vector_derivative g (at ?x within {0..1})) (at ?x within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
have "((\<lambda>x. ((f'(g x))) * ((vector_derivative g (at x within {0..1}))))
             has_integral (((f(g 1)) - (f(g 0))))) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f' (g x) * vector_derivative g (at x within {0..1})) has_integral f (g 1) - f (g 0)) {0..1}
[PROOF STEP]
using fundamental_theorem_of_calculus_interior_strong[OF k(1) zero_le_one _ cfg]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> {0<..<1} - k \<Longrightarrow> ((\<lambda>x. f (g x)) has_vector_derivative ?f' x) (at x)) \<Longrightarrow> (?f' has_integral f (g 1) - f (g 0)) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. f' (g x) * vector_derivative g (at x within {0..1})) has_integral f (g 1) - f (g 0)) {0..1}
[PROOF STEP]
using k assms cfg *
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> {0<..<1} - k \<Longrightarrow> ((\<lambda>x. f (g x)) has_vector_derivative ?f' x) (at x)) \<Longrightarrow> (?f' has_integral f (g 1) - f (g 0)) {0..1}
finite k
\<forall>x\<in>{0..1} - k. g differentiable at x within {0..1}
?a \<in> s \<Longrightarrow> (f has_field_derivative f' ?a) (at ?a within s)
g piecewise_differentiable_on {0..1}
?x \<in> {0..1} \<Longrightarrow> g ?x \<in> s
base_vec \<in> Basis
continuous_on {0..1} (\<lambda>x. f (g x))
?x \<in> {0<..<1} - k \<Longrightarrow> ((\<lambda>x. f (g x)) has_vector_derivative f' (g ?x) * vector_derivative g (at ?x within {0..1})) (at ?x within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. f' (g x) * vector_derivative g (at x within {0..1})) has_integral f (g 1) - f (g 0)) {0..1}
[PROOF STEP]
by (auto simp: at_within_Icc_at)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f' (g x) * vector_derivative g (at x within {0..1})) has_integral f (g 1) - f (g 0)) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. f' (g x) * vector_derivative g (at x within {0..1})) has_integral f (g 1) - f (g 0)) {0..1}
[PROOF STEP]
have "((\<lambda>x. (((f'(g x))) * ((vector_derivative g (at x within {0..1})))) \<bullet> base_vec)
             has_integral (((f(g 1)) - (f(g 0)))) \<bullet> base_vec) {0..1}"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f' (g x) * vector_derivative g (at x within {0..1})) has_integral f (g 1) - f (g 0)) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral (f (g 1) - f (g 0)) \<bullet> base_vec) {0..1}
[PROOF STEP]
using has_integral_componentwise_iff assms(4)
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f' (g x) * vector_derivative g (at x within {0..1})) has_integral f (g 1) - f (g 0)) {0..1}
(?f has_integral ?y) ?A = (\<forall>b\<in>Basis. ((\<lambda>x. ?f x \<bullet> b) has_integral ?y \<bullet> b) ?A)
base_vec \<in> Basis

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral (f (g 1) - f (g 0)) \<bullet> base_vec) {0..1}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral (f (g 1) - f (g 0)) \<bullet> base_vec) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral (f (g 1) - f (g 0)) \<bullet> base_vec) {0..1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral (f (g 1) - f (g 0)) \<bullet> base_vec) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
using inner_mult_left'
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral (f (g 1) - f (g 0)) \<bullet> base_vec) {0..1}
(?a * of_real ?m) \<bullet> ?b = ?m * (?a \<bullet> ?b)

goal (1 subgoal):
 1. ((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}
[PROOF STEP]
by (simp add: inner_mult_left' inner_diff_left)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. (f' (g x) * vector_derivative g (at x within {0..1})) \<bullet> base_vec) has_integral f (g 1) \<bullet> base_vec - f (g 0) \<bullet> base_vec) {0..1}

goal:
No subgoals!
[PROOF STEP]
qed