[STATEMENT]
lemma line_integral_exists_joinD1:
  assumes "line_integral_exists f basis (g1 +++ g2)" "valid_path g1"
  shows "line_integral_exists f basis g1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists f basis g1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral_exists f basis g1
[PROOF STEP]
obtain s1
    where s1: "finite s1" "\<forall>x\<in>{0..1} - s1. g1 differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>finite s1; \<forall>x\<in>{0..1} - s1. g1 differentiable at x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
line_integral_exists f basis (g1 +++ g2)
valid_path g1

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>finite s1; \<forall>x\<in>{0..1} - s1. g1 differentiable at x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
[PROOF STATE]
proof (state)
this:
finite s1
\<forall>x\<in>{0..1} - s1. g1 differentiable at x

goal (1 subgoal):
 1. line_integral_exists f basis g1
[PROOF STEP]
have "(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x/2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x/2) within {0..1}) \<bullet> b)) integrable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
line_integral_exists f basis (g1 +++ g2)
valid_path g1

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
apply (auto simp: line_integral_exists_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}; valid_path g1\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
apply (drule integrable_on_subcbox [where a=0 and b="1/2"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. valid_path g1 \<Longrightarrow> cbox 0 (1 / 2) \<subseteq> {0..1}
 2. \<lbrakk>valid_path g1; (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) integrable_on cbox 0 (1 / 2)\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists f basis g1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
have *:"(\<lambda>x. \<Sum>b\<in>basis. ((f ((g1 +++ g2) (x/2)) \<bullet> b) / 2)* (vector_derivative (g1 +++ g2) (at (x/2) within {0..1}) \<bullet> b)) integrable_on {0..1}"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2)) \<bullet> b / 2 * (vector_derivative (g1 +++ g2) (at (x / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
by (auto simp: Groups_Big.sum_distrib_left dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2)) \<bullet> b / 2 * (vector_derivative (g1 +++ g2) (at (x / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists f basis g1
[PROOF STEP]
have g1: "\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow>
            vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z within {0..1}) =
            2 *\<^sub>R vector_derivative g1 (at (z*2) within {0..1})" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
have i:"\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow>
              vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
have g1_at_z:"\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow>
                         ((\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) has_vector_derivative
                         2 *\<^sub>R vector_derivative g1 (at (z*2))) (at z)" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> ((\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g1 (at (z * 2))) (at z)
[PROOF STEP]
apply (rule has_vector_derivative_transform_at [of "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g1(2*x))"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> 0 < \<bar>z - 1 / 2\<bar>
 2. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> \<forall>x'. dist x' z < \<bar>z - 1 / 2\<bar> \<longrightarrow> g1 (2 * x') = (if x' * 2 \<le> 1 then g1 (2 * x') else g2 (2 * x' - 1))
 3. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> ((\<lambda>x. g1 (2 * x)) has_vector_derivative 2 *\<^sub>R vector_derivative g1 (at (z * 2))) (at z)
[PROOF STEP]
apply (simp_all add: dist_real_def abs_if split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> ((\<lambda>x. g1 (2 * x)) has_vector_derivative 2 *\<^sub>R vector_derivative g1 (at (z * 2))) (at z)
[PROOF STEP]
apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x" 2 _ g1, simplified o_def])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> ((*) 2 has_vector_derivative 2) (at z)
 2. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> (g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (2 * z))
[PROOF STEP]
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> (g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (2 * z))
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
finite s1
\<forall>x\<in>{0..1} - s1. g1 differentiable at x

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> (g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (2 * z))
[PROOF STEP]
apply (auto simp: algebra_simps vector_derivative_works)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?z; ?z * 2 < 1; ?z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> ((\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g1 (at (?z * 2))) (at ?z)

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
assume ass: "0 \<le> z" "z*2 < 1" "z*2 \<notin> s1"
[PROOF STATE]
proof (state)
this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1
[PROOF STEP]
have z_ge: "z\<le> 1"
[PROOF STATE]
proof (prove)
using this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1

goal (1 subgoal):
 1. z \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<le> 1

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
show "vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
using Derivative.vector_derivative_at_within_ivl[OF g1_at_z[OF ass] ass(1) z_ge]
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?z; ?z * 2 < 1; ?z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at ?z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (?z * 2))

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
assume ass: "0 \<le> z" "z*2 < 1" "z*2 \<notin> s1"
[PROOF STATE]
proof (state)
this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1
[PROOF STEP]
have "(g1 has_vector_derivative ((vector_derivative g1 (at (z*2))))) (at (z*2))"
[PROOF STATE]
proof (prove)
using this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1

goal (1 subgoal):
 1. (g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1
finite s1
\<forall>x\<in>{0..1} - s1. g1 differentiable at x

goal (1 subgoal):
 1. (g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))
[PROOF STEP]
by (auto simp: algebra_simps vector_derivative_works)
[PROOF STATE]
proof (state)
this:
(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))
[PROOF STEP]
have ii: "(vector_derivative g1 (at (z*2) within {0..1})) = (vector_derivative g1 (at (z*2)))"
[PROOF STATE]
proof (prove)
using this:
(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))

goal (1 subgoal):
 1. vector_derivative g1 (at (z * 2) within {0..1}) = vector_derivative g1 (at (z * 2))
[PROOF STEP]
using Derivative.vector_derivative_at_within_ivl ass
[PROOF STATE]
proof (prove)
using this:
(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (z * 2))
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'
0 \<le> z
z * 2 < 1
z * 2 \<notin> s1

goal (1 subgoal):
 1. vector_derivative g1 (at (z * 2) within {0..1}) = vector_derivative g1 (at (z * 2))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vector_derivative g1 (at (z * 2) within {0..1}) = vector_derivative g1 (at (z * 2))

goal (1 subgoal):
 1. \<lbrakk>0 \<le> z; z * 2 < 1; z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
show "vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
using i[OF ass] ii
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2))
vector_derivative g1 (at (z * 2) within {0..1}) = vector_derivative g1 (at (z * 2))

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (z * 2) within {0..1})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?z; ?z * 2 < 1; ?z * 2 \<notin> s1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at ?z within {0..1}) = 2 *\<^sub>R vector_derivative g1 (at (?z * 2) within {0..1})

goal (1 subgoal):
 1. line_integral_exists f basis g1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists f basis g1
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
finite s1
\<forall>x\<in>{0..1} - s1. g1 differentiable at x

goal (1 subgoal):
 1. line_integral_exists f basis g1
[PROOF STEP]
apply (auto simp: line_integral_exists_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite s1; \<forall>x\<in>{0..1} - s1. g1 differentiable at x\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
apply (rule integrable_spike_finite [of "{0,1} \<union> s1", OF _ _ *])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite s1; \<forall>x\<in>{0..1} - s1. g1 differentiable at x\<rbrakk> \<Longrightarrow> finite ({0, 1} \<union> s1)
 2. \<And>x. \<lbrakk>finite s1; \<forall>x\<in>{0..1} - s1. g1 differentiable at x; x \<in> {0..1} - ({0, 1} \<union> s1)\<rbrakk> \<Longrightarrow> (\<Sum>b\<in>basis. f (g1 x) \<bullet> b * (vector_derivative g1 (at x within {0..1}) \<bullet> b)) = (\<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2)) \<bullet> b / 2 * (vector_derivative (g1 +++ g2) (at (x / 2) within {0..1}) \<bullet> b))
[PROOF STEP]
apply (auto simp: joinpaths_def scaleR_conv_of_real g1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
line_integral_exists f basis g1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_exists_joinD2:
  assumes "line_integral_exists f basis (g1 +++ g2)" "valid_path g2"
  shows "line_integral_exists f basis g2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists f basis g2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral_exists f basis g2
[PROOF STEP]
obtain s2
    where s2: "finite s2" "\<forall>x\<in>{0..1} - s2. g2 differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>finite s2; \<forall>x\<in>{0..1} - s2. g2 differentiable at x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
line_integral_exists f basis (g1 +++ g2)
valid_path g2

goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>finite s2; \<forall>x\<in>{0..1} - s2. g2 differentiable at x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
[PROOF STATE]
proof (state)
this:
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x

goal (1 subgoal):
 1. line_integral_exists f basis g2
[PROOF STEP]
have "(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x/2 + 1/2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x/2 + 1/2) within {0..1}) \<bullet> b)) integrable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
line_integral_exists f basis (g1 +++ g2)
valid_path g2

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
apply (auto simp: line_integral_exists_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}; valid_path g2\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path g2; (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) x) \<bullet> b * (vector_derivative (g1 +++ g2) (at x within {0..1}) \<bullet> b)) integrable_on {1 / 2..1}\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path g2; (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on (\<lambda>x. 2 * x - 1) ` {1 / 2..1}\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
apply (simp add: image_affinity_atLeastAtMost_diff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists f basis g2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
have *:"(\<lambda>x. \<Sum>b\<in>basis. ((f ((g1 +++ g2) (x/2 + 1/2)) \<bullet> b) / 2)* (vector_derivative (g1 +++ g2) (at (x/2 + 1/2) within {0..1}) \<bullet> b)) integrable_on {0..1}"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b / 2 * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
by (auto simp: Groups_Big.sum_distrib_left dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b / 2 * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists f basis g2
[PROOF STEP]
have g2: "\<lbrakk>1 < z*2; z \<le> 1; z*2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow>
            vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z within {0..1}) =
            2 *\<^sub>R vector_derivative g2 (at (z*2 - 1) within {0..1})" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
have i:"\<lbrakk>1 < z*2; z \<le> 1; z*2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow>
              vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1})
                   = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
have g2_at_z:"\<lbrakk>1 < z*2; z \<le> 1; z*2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow>
                      ((\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))) (at z)" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> ((\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))) (at z)
[PROOF STEP]
apply (rule has_vector_derivative_transform_at [of "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g2 (2*x - 1))"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> 0 < \<bar>z - 1 / 2\<bar>
 2. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> \<forall>x'. dist x' z < \<bar>z - 1 / 2\<bar> \<longrightarrow> g2 (2 * x' - 1) = (if x' * 2 \<le> 1 then g1 (2 * x') else g2 (2 * x' - 1))
 3. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> ((\<lambda>x. g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))) (at z)
[PROOF STEP]
apply (simp_all add: dist_real_def abs_if split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> ((\<lambda>x. g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))) (at z)
[PROOF STEP]
apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x - 1" 2 _ g2, simplified o_def])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> ((\<lambda>x. 2 * x - 1) has_vector_derivative 2) (at z)
 2. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> (g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (2 * z - 1))
[PROOF STEP]
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> (g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (2 * z - 1))
[PROOF STEP]
using s2
[PROOF STATE]
proof (prove)
using this:
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> (g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (2 * z - 1))
[PROOF STEP]
apply (auto simp: algebra_simps vector_derivative_works)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>1 < ?z * 2; ?z \<le> 1; ?z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> ((\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) has_vector_derivative 2 *\<^sub>R vector_derivative g2 (at (?z * 2 - 1))) (at ?z)

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
assume ass: "1 < z*2" "z \<le> 1" "z*2 - 1 \<notin> s2"
[PROOF STATE]
proof (state)
this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2
[PROOF STEP]
have z_le: "z\<le> 1"
[PROOF STATE]
proof (prove)
using this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

goal (1 subgoal):
 1. z \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<le> 1

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
have z_ge: "0 \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> z
[PROOF STEP]
using ass
[PROOF STATE]
proof (prove)
using this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

goal (1 subgoal):
 1. 0 \<le> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> z

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
show "vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1})
                                = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
using Derivative.vector_derivative_at_within_ivl[OF g2_at_z[OF ass] z_ge z_le]
[PROOF STATE]
proof (prove)
using this:
0 < 1 \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>1 < ?z * 2; ?z \<le> 1; ?z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at ?z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (?z * 2 - 1))

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
assume ass: "1 < z*2" "z \<le> 1" "z*2 - 1 \<notin> s2"
[PROOF STATE]
proof (state)
this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2
[PROOF STEP]
have "(g2 has_vector_derivative ((vector_derivative g2 (at (z*2 - 1))))) (at (z*2 - 1))"
[PROOF STATE]
proof (prove)
using this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

goal (1 subgoal):
 1. (g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))
[PROOF STEP]
using s2
[PROOF STATE]
proof (prove)
using this:
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x

goal (1 subgoal):
 1. (g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))
[PROOF STEP]
by (auto simp: algebra_simps vector_derivative_works)
[PROOF STATE]
proof (state)
this:
(g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))
[PROOF STEP]
have ii: "(vector_derivative g2 (at (z*2 - 1) within {0..1})) = (vector_derivative g2 (at (z*2 - 1)))"
[PROOF STATE]
proof (prove)
using this:
(g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))

goal (1 subgoal):
 1. vector_derivative g2 (at (z * 2 - 1) within {0..1}) = vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
using Derivative.vector_derivative_at_within_ivl ass
[PROOF STATE]
proof (prove)
using this:
(g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (z * 2 - 1))
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'
1 < z * 2
z \<le> 1
z * 2 - 1 \<notin> s2

goal (1 subgoal):
 1. vector_derivative g2 (at (z * 2 - 1) within {0..1}) = vector_derivative g2 (at (z * 2 - 1))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vector_derivative g2 (at (z * 2 - 1) within {0..1}) = vector_derivative g2 (at (z * 2 - 1))

goal (1 subgoal):
 1. \<lbrakk>1 < z * 2; z \<le> 1; z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
show "vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
using i[OF ass] ii
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1))
vector_derivative g2 (at (z * 2 - 1) within {0..1}) = vector_derivative g2 (at (z * 2 - 1))

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (z * 2 - 1) within {0..1})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>1 < ?z * 2; ?z \<le> 1; ?z * 2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. if x * 2 \<le> 1 then g1 (2 * x) else g2 (2 * x - 1)) (at ?z within {0..1}) = 2 *\<^sub>R vector_derivative g2 (at (?z * 2 - 1) within {0..1})

goal (1 subgoal):
 1. line_integral_exists f basis g2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists f basis g2
[PROOF STEP]
using s2
[PROOF STATE]
proof (prove)
using this:
finite s2
\<forall>x\<in>{0..1} - s2. g2 differentiable at x

goal (1 subgoal):
 1. line_integral_exists f basis g2
[PROOF STEP]
apply (auto simp: line_integral_exists_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite s2; \<forall>x\<in>{0..1} - s2. g2 differentiable at x\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
apply (rule integrable_spike_finite [of "{0,1} \<union> s2", OF _ _ *])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite s2; \<forall>x\<in>{0..1} - s2. g2 differentiable at x\<rbrakk> \<Longrightarrow> finite ({0, 1} \<union> s2)
 2. \<And>x. \<lbrakk>finite s2; \<forall>x\<in>{0..1} - s2. g2 differentiable at x; x \<in> {0..1} - ({0, 1} \<union> s2)\<rbrakk> \<Longrightarrow> (\<Sum>b\<in>basis. f (g2 x) \<bullet> b * (vector_derivative g2 (at x within {0..1}) \<bullet> b)) = (\<Sum>b\<in>basis. f ((g1 +++ g2) (x / 2 + 1 / 2)) \<bullet> b / 2 * (vector_derivative (g1 +++ g2) (at (x / 2 + 1 / 2) within {0..1}) \<bullet> b))
[PROOF STEP]
apply (auto simp: joinpaths_def scaleR_conv_of_real g2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
line_integral_exists f basis g2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_line_integral_on_reverse_path:
  assumes g: "valid_path g" and int:
    "((\<lambda>x. \<Sum>b\<in>basis. F (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) has_integral c){0..1}"
  shows  "((\<lambda>x. \<Sum>b\<in>basis. F ((reversepath g) x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral -c){0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
fix s x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
assume xs: "g C1_differentiable_on ({0..1} - s)" "x \<notin> (-) 1 ` s" "0 \<le> x" "x \<le> 1"
[PROOF STATE]
proof (state)
this:
g C1_differentiable_on {0..1} - s
x \<notin> (-) 1 ` s
0 \<le> x
x \<le> 1

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
have "vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) =
                - vector_derivative g (at (1 - x) within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) = - vector_derivative g (at (1 - x) within {0..1})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) = - vector_derivative g (at (1 - x) within {0..1})
[PROOF STEP]
obtain f' where f': "(g has_vector_derivative f') (at (1 - x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f'. (g has_vector_derivative f') (at (1 - x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using xs
[PROOF STATE]
proof (prove)
using this:
g C1_differentiable_on {0..1} - s
x \<notin> (-) 1 ` s
0 \<le> x
x \<le> 1

goal (1 subgoal):
 1. (\<And>f'. (g has_vector_derivative f') (at (1 - x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp: has_vector_derivative_def C1_differentiable_on_def)
[PROOF STATE]
proof (state)
this:
(g has_vector_derivative f') (at (1 - x))

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) = - vector_derivative g (at (1 - x) within {0..1})
[PROOF STEP]
have "(g o (\<lambda>x. 1 - x) has_vector_derivative -1 *\<^sub>R f') (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<circ> (-) 1 has_vector_derivative - 1 *\<^sub>R f') (at x)
[PROOF STEP]
apply (rule vector_diff_chain_within)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((-) 1 has_vector_derivative - 1) (at x)
 2. (g has_vector_derivative f') (at (1 - x) within range ((-) 1))
[PROOF STEP]
apply (intro vector_diff_chain_within derivative_eq_intros | simp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g has_vector_derivative f') (at (1 - x))
[PROOF STEP]
apply (rule has_vector_derivative_at_within [OF f'])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(g \<circ> (-) 1 has_vector_derivative - 1 *\<^sub>R f') (at x)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) = - vector_derivative g (at (1 - x) within {0..1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(g \<circ> (-) 1 has_vector_derivative - 1 *\<^sub>R f') (at x)
[PROOF STEP]
have mf': "((\<lambda>x. g (1 - x)) has_vector_derivative -f') (at x)"
[PROOF STATE]
proof (prove)
using this:
(g \<circ> (-) 1 has_vector_derivative - 1 *\<^sub>R f') (at x)

goal (1 subgoal):
 1. ((\<lambda>x. g (1 - x)) has_vector_derivative - f') (at x)
[PROOF STEP]
by (simp add: o_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. g (1 - x)) has_vector_derivative - f') (at x)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) = - vector_derivative g (at (1 - x) within {0..1})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) = - vector_derivative g (at (1 - x) within {0..1})
[PROOF STEP]
using xs
[PROOF STATE]
proof (prove)
using this:
g C1_differentiable_on {0..1} - s
x \<notin> (-) 1 ` s
0 \<le> x
x \<le> 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) = - vector_derivative g (at (1 - x) within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>g C1_differentiable_on {0..1} - ?s2; ?x2 \<notin> (-) 1 ` ?s2; 0 \<le> ?x2; ?x2 \<le> 1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. g (1 - x)) (at ?x2 within {0..1}) = - vector_derivative g (at (1 - ?x2) within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>g C1_differentiable_on {0..1} - ?s2; ?x2 \<notin> (-) 1 ` ?s2; 0 \<le> ?x2; ?x2 \<le> 1\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. g (1 - x)) (at ?x2 within {0..1}) = - vector_derivative g (at (1 - ?x2) within {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
obtain S where "continuous_on {0..1} g" "finite S" "g C1_differentiable_on {0..1} - S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S. \<lbrakk>continuous_on {0..1} g; finite S; g C1_differentiable_on {0..1} - S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
valid_path g

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>continuous_on {0..1} g; finite S; g C1_differentiable_on {0..1} - S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} g
finite S
g C1_differentiable_on {0..1} - S

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on {0..1} g
finite S
g C1_differentiable_on {0..1} - S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} g
finite S
g C1_differentiable_on {0..1} - S

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
using has_integral_affinity01 [OF int, where m= "-1" and c=1]
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} g
finite S
g C1_differentiable_on {0..1} - S
- 1 \<noteq> 0 \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. F (g (- 1 * x + 1)) \<bullet> b * (vector_derivative g (at (- 1 * x + 1) within {0..1}) \<bullet> b)) has_integral (1 / \<bar>- 1\<bar>) *\<^sub>R c) ((\<lambda>x. x / - 1 - 1 / - 1) ` {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
unfolding reversepath_def
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} g
finite S
g C1_differentiable_on {0..1} - S
- 1 \<noteq> 0 \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. F (g (- 1 * x + 1)) \<bullet> b * (vector_derivative g (at (- 1 * x + 1) within {0..1}) \<bullet> b)) has_integral (1 / \<bar>- 1\<bar>) *\<^sub>R c) ((\<lambda>x. x / - 1 - 1 / - 1) ` {0..1})

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (g (1 - x)) \<bullet> b * (vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}
[PROOF STEP]
by (rule_tac S = "(\<lambda>x. 1 - x) ` S" in has_integral_spike_finite) (auto simp: * has_integral_neg Groups_Big.sum_negf)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. F (reversepath g x) \<bullet> b * (vector_derivative (reversepath g) (at x within {0..1}) \<bullet> b)) has_integral - c) {0..1}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_on_reverse_path:
  assumes "valid_path \<gamma>" "line_integral_exists F basis \<gamma>"
  shows "line_integral F basis \<gamma> = - (line_integral F basis (reversepath \<gamma>))"
        "line_integral_exists F basis (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>) &&& line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>)
 2. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
obtain i where
    0: "((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral i){0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. ((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral i) {0..1} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
valid_path \<gamma>
line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. (\<And>i. ((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral i) {0..1} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding integrable_on_def line_integral_exists_def
[PROOF STATE]
proof (prove)
using this:
valid_path \<gamma>
\<exists>y. ((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral y) {0..1}

goal (1 subgoal):
 1. (\<And>i. ((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral i) {0..1} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral i) {0..1}

goal (2 subgoals):
 1. line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>)
 2. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral i) {0..1}
[PROOF STEP]
have 1: "((\<lambda>x. \<Sum>b\<in>basis. F ((reversepath \<gamma>) x) \<bullet> b * (vector_derivative (reversepath \<gamma>) (at x within {0..1}) \<bullet> b)) has_integral -i){0..1}"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral i) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath \<gamma> x) \<bullet> b * (vector_derivative (reversepath \<gamma>) (at x within {0..1}) \<bullet> b)) has_integral - i) {0..1}
[PROOF STEP]
using has_line_integral_on_reverse_path assms
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral i) {0..1}
\<lbrakk>valid_path ?g; ((\<lambda>x. \<Sum>b\<in>?basis. ?F (?g x) \<bullet> b * (vector_derivative ?g (at x within {0..1}) \<bullet> b)) has_integral ?c) {0..1}\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>?basis. ?F (reversepath ?g x) \<bullet> b * (vector_derivative (reversepath ?g) (at x within {0..1}) \<bullet> b)) has_integral - ?c) {0..1}
valid_path \<gamma>
line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (reversepath \<gamma> x) \<bullet> b * (vector_derivative (reversepath \<gamma>) (at x within {0..1}) \<bullet> b)) has_integral - i) {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. F (reversepath \<gamma> x) \<bullet> b * (vector_derivative (reversepath \<gamma>) (at x within {0..1}) \<bullet> b)) has_integral - i) {0..1}

goal (2 subgoals):
 1. line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>)
 2. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. \<Sum>b\<in>basis. F (reversepath \<gamma> x) \<bullet> b * (vector_derivative (reversepath \<gamma>) (at x within {0..1}) \<bullet> b)) has_integral - i) {0..1}
[PROOF STEP]
have rev_line_integral:"line_integral F basis (reversepath \<gamma>) = -i"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<Sum>b\<in>basis. F (reversepath \<gamma> x) \<bullet> b * (vector_derivative (reversepath \<gamma>) (at x within {0..1}) \<bullet> b)) has_integral - i) {0..1}

goal (1 subgoal):
 1. line_integral F basis (reversepath \<gamma>) = - i
[PROOF STEP]
using line_integral_def Henstock_Kurzweil_Integration.integral_unique
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<Sum>b\<in>basis. F (reversepath \<gamma> x) \<bullet> b * (vector_derivative (reversepath \<gamma>) (at x within {0..1}) \<bullet> b)) has_integral - i) {0..1}
line_integral ?F ?basis ?g \<equiv> integral {0..1} (\<lambda>x. \<Sum>b\<in>?basis. ?F (?g x) \<bullet> b * (vector_derivative ?g (at x within {0..1}) \<bullet> b))
(?f has_integral ?y) ?k \<Longrightarrow> integral ?k ?f = ?y

goal (1 subgoal):
 1. line_integral F basis (reversepath \<gamma>) = - i
[PROOF STEP]
by (metis (no_types))
[PROOF STATE]
proof (state)
this:
line_integral F basis (reversepath \<gamma>) = - i

goal (2 subgoals):
 1. line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>)
 2. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
have line_integral: "line_integral F basis \<gamma> = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = i
[PROOF STEP]
using line_integral_def 0 Henstock_Kurzweil_Integration.integral_unique
[PROOF STATE]
proof (prove)
using this:
line_integral ?F ?basis ?g \<equiv> integral {0..1} (\<lambda>x. \<Sum>b\<in>?basis. ?F (?g x) \<bullet> b * (vector_derivative ?g (at x within {0..1}) \<bullet> b))
((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral i) {0..1}
(?f has_integral ?y) ?k \<Longrightarrow> integral ?k ?f = ?y

goal (1 subgoal):
 1. line_integral F basis \<gamma> = i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
line_integral F basis \<gamma> = i

goal (2 subgoals):
 1. line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>)
 2. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
show "line_integral F basis \<gamma> = - (line_integral F basis (reversepath \<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>)
[PROOF STEP]
using line_integral rev_line_integral
[PROOF STATE]
proof (prove)
using this:
line_integral F basis \<gamma> = i
line_integral F basis (reversepath \<gamma>) = - i

goal (1 subgoal):
 1. line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral F basis \<gamma> = - line_integral F basis (reversepath \<gamma>)

goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
show "line_integral_exists F basis (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
using 1 line_integral_exists_def
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<Sum>b\<in>basis. F (reversepath \<gamma> x) \<bullet> b * (vector_derivative (reversepath \<gamma>) (at x within {0..1}) \<bullet> b)) has_integral - i) {0..1}
line_integral_exists ?F ?basis ?\<gamma> \<equiv> (\<lambda>x. \<Sum>b\<in>?basis. ?F (?\<gamma> x) \<bullet> b * (vector_derivative ?\<gamma> (at x within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (reversepath \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_exists_on_degenerate_path:
  assumes "finite basis"
  shows "line_integral_exists F basis (\<lambda>x. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (\<lambda>x. c)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral_exists F basis (\<lambda>x. c)
[PROOF STEP]
have every_component_integrable:
    "\<forall>b\<in>basis. (\<lambda>x. F ((\<lambda>x. c) x) \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. (\<lambda>x. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> (\<lambda>x. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> (\<lambda>x. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
assume b_in_basis: "b \<in> basis"
[PROOF STATE]
proof (state)
this:
b \<in> basis

goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> (\<lambda>x. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
have cont_field_zero_one: "continuous_on {0..1} (\<lambda>x. F ((\<lambda>x. c) x) \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0::'b..1::'b} (\<lambda>x. F c \<bullet> b)
[PROOF STEP]
using continuous_on_const
[PROOF STATE]
proof (prove)
using this:
continuous_on ?s (\<lambda>x. ?c)

goal (1 subgoal):
 1. continuous_on {0::'b..1::'b} (\<lambda>x. F c \<bullet> b)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
continuous_on {0::?'b1..1::?'b1} (\<lambda>x. F c \<bullet> b)

goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> (\<lambda>x. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
have cont_path_zero_one:
      "continuous_on {0..1} (\<lambda>x. (vector_derivative (\<lambda>x. c) (at x within {0..1})) \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)
[PROOF STEP]
have "((vector_derivative (\<lambda>x. c) (at x within {0..1})) \<bullet> b) = 0" if "x \<in> {0..1}" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0
[PROOF STEP]
have "vector_derivative (\<lambda>x. c) (at x within {0..1}) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) = (0::'a)
[PROOF STEP]
using that gamma_deriv_at_within[of "0" "1"] differentiable_const vector_derivative_const_at
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1}
\<lbrakk>0 < 1; ?x \<in> {0..1}; \<forall>x\<in>{0..1}. ?\<gamma> differentiable at x\<rbrakk> \<Longrightarrow> vector_derivative ?\<gamma> (at ?x within {0..1}) = vector_derivative ?\<gamma> (at ?x)
(\<lambda>z. ?a) differentiable ?F
vector_derivative (\<lambda>x. ?c) (at ?a) = (0::?'a)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. c) (at x within {0..1}) = (0::'a)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vector_derivative (\<lambda>x. c) (at x within {0..1}) = (0::'a)
[PROOF STEP]
show "vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0"
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. c) (at x within {0..1}) = (0::'a)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x1 \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. c) (at ?x1 within {0..1}) \<bullet> b = 0

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x1 \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. c) (at ?x1 within {0..1}) \<bullet> b = 0
[PROOF STEP]
show "continuous_on {0..1} (\<lambda>x. (vector_derivative (\<lambda>x. c) (at x within {0..1})) \<bullet> b)"
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. c) (at ?x1 within {0..1}) \<bullet> b = 0

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)
[PROOF STEP]
using continuous_on_const[of "{0..1}" "0"] continuous_on_eq[of "{0..1}" "\<lambda>x. 0" "(\<lambda>x. (vector_derivative (\<lambda>x. c) (at x within {0..1})) \<bullet> b)"]
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. c) (at ?x1 within {0..1}) \<bullet> b = 0
continuous_on {0::?'b1..1::?'b1} (\<lambda>x. 0::?'c1)
\<lbrakk>continuous_on {0..1} (\<lambda>x. 0); \<And>x. x \<in> {0..1} \<Longrightarrow> 0 = vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b\<rbrakk> \<Longrightarrow> continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)

goal (1 subgoal):
 1. \<And>b. b \<in> basis \<Longrightarrow> (\<lambda>x. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
show "(\<lambda>x. F (c) \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
using cont_field_zero_one cont_path_zero_one continuous_on_mult integrable_continuous_real
[PROOF STATE]
proof (prove)
using this:
continuous_on {0::?'b1..1::?'b1} (\<lambda>x. F c \<bullet> b)
continuous_on {0..1} (\<lambda>x. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)
\<lbrakk>continuous_on ?s ?f; continuous_on ?s ?g\<rbrakk> \<Longrightarrow> continuous_on ?s (\<lambda>x. ?f x * ?g x)
continuous_on {?a..?b} ?f \<Longrightarrow> ?f integrable_on {?a..?b}

goal (1 subgoal):
 1. (\<lambda>x. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. (\<lambda>x. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists F basis (\<lambda>x. c)
[PROOF STEP]
have integrable_sum': "\<And>t f s. finite t \<Longrightarrow>
                \<forall>a\<in>t. f a integrable_on s \<Longrightarrow> (\<lambda>x. \<Sum>a\<in>t. f a x) integrable_on s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t f s. \<lbrakk>finite t; \<forall>a\<in>t. f a integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>a\<in>t. f a x) integrable_on s
[PROOF STEP]
using integrable_sum
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?I; \<And>a. a \<in> ?I \<Longrightarrow> ?f a integrable_on ?S\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>a\<in>?I. ?f a x) integrable_on ?S

goal (1 subgoal):
 1. \<And>t f s. \<lbrakk>finite t; \<forall>a\<in>t. f a integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>a\<in>t. f a x) integrable_on s
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite ?t; \<forall>a\<in>?t. ?f a integrable_on ?s\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>a\<in>?t. ?f a x) integrable_on ?s

goal (1 subgoal):
 1. line_integral_exists F basis (\<lambda>x. c)
[PROOF STEP]
have field_integrable_on_basis:
    "(\<lambda>x. \<Sum>b\<in>basis. F (c) \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
using integrable_sum'[OF assms(1) every_component_integrable]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<Sum>a\<in>basis. F c \<bullet> a * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> a)) integrable_on {0..1}

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists F basis (\<lambda>x. c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists F basis (\<lambda>x. c)
[PROOF STEP]
using line_integral_exists_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
line_integral_exists ?F ?basis ?\<gamma> \<equiv> (\<lambda>x. \<Sum>b\<in>?basis. ?F (?\<gamma> x) \<bullet> b * (vector_derivative ?\<gamma> (at x within {0..1}) \<bullet> b)) integrable_on {0..1}

goal (1 subgoal):
 1. line_integral_exists F basis (\<lambda>x. c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (\<lambda>x. c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degenerate_path_is_valid_path: "valid_path (\<lambda>x. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (\<lambda>x. c)
[PROOF STEP]
by (auto simp add: valid_path_def piecewise_C1_differentiable_on_def continuous_on_const)


[STATEMENT]
lemma line_integral_degenerate_path:
  assumes "finite basis"
  shows "line_integral F basis (\<lambda>x. c) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (\<lambda>x. c) = 0
[PROOF STEP]
proof (simp add: line_integral_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
have "((vector_derivative (\<lambda>x. c) (at x within {0..1})) \<bullet> b) = 0" if "x \<in> {0..1}" for x b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0
[PROOF STEP]
have "vector_derivative (\<lambda>x. c) (at x within {0..1}) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) = (0::'a)
[PROOF STEP]
using that gamma_deriv_at_within[of "0" "1"] differentiable_const vector_derivative_const_at
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1}
\<lbrakk>0 < 1; ?x \<in> {0..1}; \<forall>x\<in>{0..1}. ?\<gamma> differentiable at x\<rbrakk> \<Longrightarrow> vector_derivative ?\<gamma> (at ?x within {0..1}) = vector_derivative ?\<gamma> (at ?x)
(\<lambda>z. ?a) differentiable ?F
vector_derivative (\<lambda>x. ?c) (at ?a) = (0::?'a)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. c) (at x within {0..1}) = (0::'a)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vector_derivative (\<lambda>x. c) (at x within {0..1}) = (0::'a)
[PROOF STEP]
show "vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0"
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. c) (at x within {0..1}) = (0::'a)

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. c) (at ?x within {0..1}) \<bullet> ?b = 0

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. c) (at ?x within {0..1}) \<bullet> ?b = 0
[PROOF STEP]
have 0: "\<And>x. x \<in> {0..1} \<Longrightarrow> (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) x = (\<lambda>x. 0) x"
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} \<Longrightarrow> vector_derivative (\<lambda>x. c) (at ?x within {0..1}) \<bullet> ?b = 0

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> (\<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} \<Longrightarrow> (\<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at ?x within {0..1}) \<bullet> b)) = 0

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> {0..1} \<Longrightarrow> (\<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at ?x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
show "integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) = 0"
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} \<Longrightarrow> (\<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at ?x within {0..1}) \<bullet> b)) = 0

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
using integral_cong[of "{0..1}", OF 0] integral_0
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} \<Longrightarrow> (\<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at ?x within {0..1}) \<bullet> b)) = 0
(\<And>x. x \<in> {0::?'b1..1::?'b1} \<Longrightarrow> ?x2 x \<in> {0..1}) \<Longrightarrow> integral {0::?'b1..1::?'b1} (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at (?x2 x) within {0..1}) \<bullet> b)) = integral {0::?'b1..1::?'b1} (\<lambda>x. 0)
integral ?S (\<lambda>x. 0::?'m) = (0::?'m)

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F c \<bullet> b * (vector_derivative (\<lambda>x. c) (at x within {0..1}) \<bullet> b)) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_point_path:
  assumes "point_path \<gamma>"
  assumes "finite basis"
  shows "line_integral F basis \<gamma> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = 0
[PROOF STEP]
using assms(1) point_path_def line_integral_degenerate_path[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
point_path \<gamma>
point_path ?\<gamma> \<equiv> \<exists>c. ?\<gamma> = (\<lambda>x. c)
line_integral ?F basis (\<lambda>x. ?c) = 0

goal (1 subgoal):
 1. line_integral F basis \<gamma> = 0
[PROOF STEP]
by force


[STATEMENT]
lemma line_integral_exists_point_path:
  assumes "finite basis" "point_path \<gamma>"
  shows "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite basis
point_path \<gamma>

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
apply(simp add: point_path_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite basis; \<exists>c. \<gamma> = (\<lambda>x. c)\<rbrakk> \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
using line_integral_exists_on_degenerate_path
[PROOF STATE]
proof (prove)
using this:
finite ?basis \<Longrightarrow> line_integral_exists ?F ?basis (\<lambda>x. ?c)

goal (1 subgoal):
 1. \<lbrakk>finite basis; \<exists>c. \<gamma> = (\<lambda>x. c)\<rbrakk> \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
by auto


[STATEMENT]
lemma line_integral_exists_subpath:
  assumes f: "line_integral_exists f basis g" and g: "valid_path g"
    and uv: "u \<in> {0..1}" "v \<in> {0..1}" "u \<le> v"
  shows "(line_integral_exists f basis (subpath u v g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists f basis (subpath u v g)
[PROOF STEP]
proof (cases "v=u")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
 2. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
case tr: True
[PROOF STATE]
proof (state)
this:
v = u

goal (2 subgoals):
 1. v = u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
 2. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
have zero: "(\<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) = 0" if "x \<in> {0..1}" for x::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
have "(vector_derivative (\<lambda>x. g u) (at x within {0..1})) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<lambda>x. g u) (at x within {0..1}) = (0::'a)
[PROOF STEP]
using Deriv.has_vector_derivative_const that Derivative.vector_derivative_at_within_ivl
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. ?c) has_vector_derivative (0::?'a)) ?net
x \<in> {0..1}
\<lbrakk>(?f has_vector_derivative ?f') (at ?x); ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative ?f (at ?x within {?a..?b}) = ?f'

goal (1 subgoal):
 1. vector_derivative (\<lambda>x. g u) (at x within {0..1}) = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
vector_derivative (\<lambda>x. g u) (at x within {0..1}) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vector_derivative (\<lambda>x. g u) (at x within {0..1}) = (0::'a)
[PROOF STEP]
show "(\<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) = 0"
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<lambda>x. g u) (at x within {0..1}) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} \<Longrightarrow> (\<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at ?x within {0..1}) \<bullet> b)) = 0

goal (2 subgoals):
 1. v = u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
 2. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> {0..1} \<Longrightarrow> (\<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at ?x within {0..1}) \<bullet> b)) = 0
[PROOF STEP]
have "((\<lambda>x. \<Sum>b\<in>basis. f (g u)  \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1})  \<bullet> b)) has_integral 0) {0..1}"
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} \<Longrightarrow> (\<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at ?x within {0..1}) \<bullet> b)) = 0

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}
[PROOF STEP]
by (meson has_integral_is_0)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}

goal (2 subgoals):
 1. v = u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
 2. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. \<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}

goal (1 subgoal):
 1. line_integral_exists f basis (subpath u v g)
[PROOF STEP]
using f tr
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<Sum>b\<in>basis. f (g u) \<bullet> b * (vector_derivative (\<lambda>x. g u) (at x within {0..1}) \<bullet> b)) has_integral 0) {0..1}
line_integral_exists f basis g
v = u

goal (1 subgoal):
 1. line_integral_exists f basis (subpath u v g)
[PROOF STEP]
by (auto simp add: line_integral_def line_integral_exists_def subpath_def)
[PROOF STATE]
proof (state)
this:
line_integral_exists f basis (subpath u v g)

goal (1 subgoal):
 1. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<noteq> u

goal (1 subgoal):
 1. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
obtain s where s: "\<And>x. x \<in> {0..1} - s \<Longrightarrow> g differentiable at x" and fs: "finite s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>\<And>x. x \<in> {0..1} - s \<Longrightarrow> g differentiable at x; finite s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
valid_path g

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>\<And>x. x \<in> {0..1} - s \<Longrightarrow> g differentiable at x; finite s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding piecewise_C1_differentiable_on_def C1_differentiable_on_eq valid_path_def
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} g \<and> (\<exists>S. finite S \<and> (\<forall>x\<in>{0..1} - S. g differentiable at x) \<and> continuous_on ({0..1} - S) (\<lambda>x. vector_derivative g (at x)))

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>\<And>x. x \<in> {0..1} - s \<Longrightarrow> g differentiable at x; finite s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} - s \<Longrightarrow> g differentiable at ?x
finite s

goal (1 subgoal):
 1. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
have *: "((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u))  \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1})  \<bullet> b))
            has_integral (1 / (v - u)) * integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g (x))  \<bullet> b * (vector_derivative g (at x within {0..1})  \<bullet> b)))
           {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b)) has_integral 1 / (v - u) * integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
using f uv
[PROOF STATE]
proof (prove)
using this:
line_integral_exists f basis g
u \<in> {0..1}
v \<in> {0..1}
u \<le> v

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b)) has_integral 1 / (v - u) * integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
apply (simp add: line_integral_exists_def subpath_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) integrable_on {0..1}; 0 \<le> u; v \<le> 1; u \<le> v\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) / (v - u)) {0..1}
[PROOF STEP]
apply (drule integrable_on_subcbox [where a=u and b=v, simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> u; v \<le> 1; u \<le> v\<rbrakk> \<Longrightarrow> {u..v} \<subseteq> {0..1}
 2. \<lbrakk>0 \<le> u; v \<le> 1; u \<le> v; (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) integrable_on {u..v}\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) / (v - u)) {0..1}
[PROOF STEP]
apply (simp_all add: has_integral_integral)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> u; v \<le> 1; u \<le> v; ((\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {u..v}\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) / (v - u)) {0..1}
[PROOF STEP]
apply (drule has_integral_affinity [where m="v-u" and c=u, simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> u; v \<le> 1; u \<le> v\<rbrakk> \<Longrightarrow> v \<noteq> u
 2. \<lbrakk>0 \<le> u; v \<le> 1; u \<le> v; ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b)) has_integral (1 / \<bar>v - u\<bar>) *\<^sub>R integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) ((\<lambda>x. x / (v - u) - u / (v - u)) ` {u..v})\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) / (v - u)) {0..1}
[PROOF STEP]
apply (simp_all add: False image_affinity_atLeastAtMost_div_diff scaleR_conv_of_real)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> u; v \<le> 1; u \<le> v; ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) / (v - u)) {0..v / (v - u) - u / (v - u)}\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) / (v - u)) {0..1}
[PROOF STEP]
apply (simp add: divide_simps False)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b)) has_integral 1 / (v - u) * integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}

goal (1 subgoal):
 1. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
have vd:"\<And>x. x \<in> {0..1} \<Longrightarrow>
           x \<notin> (\<lambda>t. (v-u) *\<^sub>R t + u) -` s \<Longrightarrow>
           vector_derivative (\<lambda>x. g ((v-u) * x + u)) (at x within {0..1}) = (v-u) *\<^sub>R vector_derivative g (at ((v-u) * x + u) within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {0..1}; x \<notin> (\<lambda>t. (v - u) *\<^sub>R t + u) -` s\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1}) = (v - u) *\<^sub>R vector_derivative g (at ((v - u) * x + u) within {0..1})
[PROOF STEP]
using test2[OF s fs uv]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> {0..1} - s \<Longrightarrow> x \<in> {0..1} - s; ?x \<in> {0..1}; ?x \<notin> (\<lambda>t. (v - u) *\<^sub>R t + u) -` s\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at ?x within {0..1}) = (v - u) *\<^sub>R vector_derivative g (at ((v - u) * ?x + u) within {0..1})

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {0..1}; x \<notin> (\<lambda>t. (v - u) *\<^sub>R t + u) -` s\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1}) = (v - u) *\<^sub>R vector_derivative g (at ((v - u) * x + u) within {0..1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> {0..1}; ?x \<notin> (\<lambda>t. (v - u) *\<^sub>R t + u) -` s\<rbrakk> \<Longrightarrow> vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at ?x within {0..1}) = (v - u) *\<^sub>R vector_derivative g (at ((v - u) * ?x + u) within {0..1})

goal (1 subgoal):
 1. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
have arg:"\<And>x. (\<Sum>n\<in>basis. (v - u) * (f (g ((v - u) * x + u)) \<bullet> n) * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> n))
              =    (\<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (v - u) * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<Sum>n\<in>basis. (v - u) * (f (g ((v - u) * x + u)) \<bullet> n) * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> n)) = (\<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (v - u) * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b))
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
(\<Sum>n\<in>basis. (v - u) * (f (g ((v - u) * ?x + u)) \<bullet> n) * (vector_derivative g (at ((v - u) * ?x + u) within {0..1}) \<bullet> n)) = (\<Sum>b\<in>basis. f (g ((v - u) * ?x + u)) \<bullet> b * (v - u) * (vector_derivative g (at ((v - u) * ?x + u) within {0..1}) \<bullet> b))

goal (1 subgoal):
 1. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
have"((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u))  \<bullet> b * (vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1})  \<bullet> b)) has_integral
          (integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g (x))  \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)))) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
apply (cut_tac Henstock_Kurzweil_Integration.has_integral_mult_right [OF *, where c = "v-u"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. (v - u) * (\<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b))) has_integral (v - u) * (1 / (v - u) * integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)))) {0..1} \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
using fs assms
[PROOF STATE]
proof (prove)
using this:
finite s
line_integral_exists f basis g
valid_path g
u \<in> {0..1}
v \<in> {0..1}
u \<le> v

goal (1 subgoal):
 1. ((\<lambda>x. (v - u) * (\<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b))) has_integral (v - u) * (1 / (v - u) * integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)))) {0..1} \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
apply (simp add: False subpath_def line_integral_exists_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((\<lambda>x. (v - u) * (\<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b))) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}; finite s; (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) integrable_on {0..1}; valid_path g; 0 \<le> u; v \<le> 1; u \<le> v\<rbrakk> \<Longrightarrow> ((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
apply (rule_tac S = "(\<lambda>t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>((\<lambda>x. (v - u) * (\<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b))) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}; finite s; (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) integrable_on {0..1}; valid_path g; 0 \<le> u; v \<le> 1; u \<le> v\<rbrakk> \<Longrightarrow> finite ((\<lambda>t. (v - u) *\<^sub>R t + u) -` s)
 2. \<And>x. \<lbrakk>((\<lambda>x. (v - u) * (\<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b))) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}; finite s; (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) integrable_on {0..1}; valid_path g; 0 \<le> u; v \<le> 1; u \<le> v; x \<in> {0..1} - (\<lambda>t. (v - u) *\<^sub>R t + u) -` s\<rbrakk> \<Longrightarrow> (\<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1}) \<bullet> b)) = ?f8 x
 3. \<lbrakk>((\<lambda>x. (v - u) * (\<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative g (at ((v - u) * x + u) within {0..1}) \<bullet> b))) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}; finite s; (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b)) integrable_on {0..1}; valid_path g; 0 \<le> u; v \<le> 1; u \<le> v\<rbrakk> \<Longrightarrow> (?f8 has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
apply (auto simp: inj_on_def False vd finite_vimageI scaleR_conv_of_real Groups_Big.sum_distrib_left
        mult.assoc[symmetric] arg)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}

goal (1 subgoal):
 1. v \<noteq> u \<Longrightarrow> line_integral_exists f basis (subpath u v g)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
show "(line_integral_exists f basis (subpath u v g))"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. \<Sum>b\<in>basis. f (g ((v - u) * x + u)) \<bullet> b * (vector_derivative (\<lambda>x. g ((v - u) * x + u)) (at x within {0..1}) \<bullet> b)) has_integral integral {u..v} (\<lambda>x. \<Sum>b\<in>basis. f (g x) \<bullet> b * (vector_derivative g (at x within {0..1}) \<bullet> b))) {0..1}

goal (1 subgoal):
 1. line_integral_exists f basis (subpath u v g)
[PROOF STEP]
by(auto simp add: line_integral_exists_def subpath_def integrable_on_def)
[PROOF STATE]
proof (state)
this:
line_integral_exists f basis (subpath u v g)

goal:
No subgoals!
[PROOF STEP]
qed