[STATEMENT]
lemma reparam_weak_eq_line_integrals:
  assumes "reparam_weak \<gamma>1 \<gamma>2"
    "\<gamma>2 C1_differentiable_on {0..1}" (*To generalise this to valid_path we need a version of has_integral_substitution_strong that allows finite discontinuities of f*)
    "continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
  shows "line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2"
    "line_integral_exists F {b} \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2 &&& line_integral_exists F {b} \<gamma>1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
obtain \<phi> where phi: "(\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 o \<phi>) x)"" \<phi> piecewise_C1_differentiable_on {0..1}"" \<phi>(0) = 0"" \<phi>(1) = 1"" \<phi> ` {0..1} = {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x; \<phi> piecewise_C1_differentiable_on {0..1}; \<phi> 0 = 0; \<phi> 1 = 1; \<phi> ` {0..1} = {0..1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
reparam_weak \<gamma>1 \<gamma>2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x; \<phi> piecewise_C1_differentiable_on {0..1}; \<phi> 0 = 0; \<phi> 1 = 1; \<phi> ` {0..1} = {0..1}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: reparam_weak_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x
\<phi> piecewise_C1_differentiable_on {0..1}
\<phi> 0 = 0
\<phi> 1 = 1
\<phi> ` {0..1} = {0..1}

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
obtain s where s: "finite s" "\<phi> C1_differentiable_on {0..1} - s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>finite s; \<phi> C1_differentiable_on {0..1} - s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using phi
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x
\<phi> piecewise_C1_differentiable_on {0..1}
\<phi> 0 = 0
\<phi> 1 = 1
\<phi> ` {0..1} = {0..1}

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

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
have cont_phi: "continuous_on {0..1} \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} \<phi>
[PROOF STEP]
using phi
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x
\<phi> piecewise_C1_differentiable_on {0..1}
\<phi> 0 = 0
\<phi> 1 = 1
\<phi> ` {0..1} = {0..1}

goal (1 subgoal):
 1. continuous_on {0..1} \<phi>
[PROOF STEP]
by(auto simp add: reparam_weak_def piecewise_C1_differentiable_on_imp_continuous_on)
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} \<phi>

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
have gamma2_differentiable: "(\<forall>x \<in> {0 .. 1}. \<gamma>2 differentiable at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. \<gamma>2 differentiable at x
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<gamma>2 C1_differentiable_on {0..1}

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. \<gamma>2 differentiable at x
[PROOF STEP]
by (auto simp add: valid_path_def C1_differentiable_on_eq)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. \<gamma>2 differentiable at x

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1}. \<gamma>2 differentiable at x
[PROOF STEP]
have gamma2_b_component_differentiable: "(\<forall>x \<in> {0 .. 1}. (\<lambda>x. (\<gamma>2 x) \<bullet> b) differentiable at x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. \<gamma>2 differentiable at x

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. (\<lambda>x. \<gamma>2 x \<bullet> b) differentiable at x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. (\<lambda>x. \<gamma>2 x \<bullet> b) differentiable at x

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1}. (\<lambda>x. \<gamma>2 x \<bullet> b) differentiable at x
[PROOF STEP]
have "(\<lambda>x. (\<gamma>2 x) \<bullet> b) differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. (\<lambda>x. \<gamma>2 x \<bullet> b) differentiable at x

goal (1 subgoal):
 1. (\<lambda>x. \<gamma>2 x \<bullet> b) differentiable_on {0..1}
[PROOF STEP]
using differentiable_at_withinI
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. (\<lambda>x. \<gamma>2 x \<bullet> b) differentiable at x
?f differentiable at ?x \<Longrightarrow> ?f differentiable at ?x within ?s

goal (1 subgoal):
 1. (\<lambda>x. \<gamma>2 x \<bullet> b) differentiable_on {0..1}
[PROOF STEP]
by (auto simp add: differentiable_on_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<gamma>2 x \<bullet> b) differentiable_on {0..1}

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. \<gamma>2 x \<bullet> b) differentiable_on {0..1}
[PROOF STEP]
have gama2_cont_comp: "continuous_on {0..1} (\<lambda>x. (\<gamma>2 x) \<bullet> b)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<gamma>2 x \<bullet> b) differentiable_on {0..1}

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. \<gamma>2 x \<bullet> b)
[PROOF STEP]
using differentiable_imp_continuous_on
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<gamma>2 x \<bullet> b) differentiable_on {0..1}
?f differentiable_on ?s \<Longrightarrow> continuous_on ?s ?f

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

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
have gamma2_cont:"continuous_on {0..1} \<gamma>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} \<gamma>2
[PROOF STEP]
using assms(2) C1_differentiable_imp_continuous_on
[PROOF STATE]
proof (prove)
using this:
\<gamma>2 C1_differentiable_on {0..1}
?f C1_differentiable_on ?S \<Longrightarrow> continuous_on ?S ?f

goal (1 subgoal):
 1. continuous_on {0..1} \<gamma>2
[PROOF STEP]
by (auto simp add: valid_path_def)
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} \<gamma>2

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
have iii: "continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
have 0: "continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b)
[PROOF STEP]
using assms(3) continuous_on_compose[OF gamma2_cont]
[PROOF STATE]
proof (prove)
using this:
continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
continuous_on (\<gamma>2 ` {0..1}) ?g \<Longrightarrow> continuous_on {0..1} (?g \<circ> \<gamma>2)

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b)
[PROOF STEP]
by (auto simp add: path_image_def)
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b)

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
obtain D where D: "(\<forall>x\<in>{0..1}. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D. (\<forall>x\<in>{0..1}. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<gamma>2 C1_differentiable_on {0..1}

goal (1 subgoal):
 1. (\<And>D. (\<forall>x\<in>{0..1}. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: C1_differentiable_on_def)
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>{0..1}. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x\<in>{0..1}. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D
[PROOF STEP]
have *:"\<forall>x\<in>{0..1}. vector_derivative \<gamma>2 (at x within{0..1}) = D x"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>{0..1}. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. vector_derivative \<gamma>2 (at x within {0..1}) = D x
[PROOF STEP]
using vector_derivative_at vector_derivative_at_within_ivl
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>{0..1}. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D
(?f has_vector_derivative ?f') (at ?x) \<Longrightarrow> vector_derivative ?f (at ?x) = ?f'
\<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. \<forall>x\<in>{0..1}. vector_derivative \<gamma>2 (at x within {0..1}) = D x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. vector_derivative \<gamma>2 (at x within {0..1}) = D x

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1}. vector_derivative \<gamma>2 (at x within {0..1}) = D x
[PROOF STEP]
have "continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma>2 (at x within{0..1}))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. vector_derivative \<gamma>2 (at x within {0..1}) = D x

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma>2 (at x within {0..1}))
[PROOF STEP]
using continuous_on_eq D
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. vector_derivative \<gamma>2 (at x within {0..1}) = D x
\<lbrakk>continuous_on ?s ?f; \<And>x. x \<in> ?s \<Longrightarrow> ?f x = ?g x\<rbrakk> \<Longrightarrow> continuous_on ?s ?g
(\<forall>x\<in>{0..1}. (\<gamma>2 has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D

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

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma>2 (at x within {0..1}))
[PROOF STEP]
have 1: "continuous_on {0..1} (\<lambda>x. (vector_derivative \<gamma>2 (at x within{0..1})) \<bullet> b)"
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma>2 (at x within {0..1}))

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

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
using continuous_on_mult[OF 0 1]
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))

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

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

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
have iv: "\<phi>(0) \<le> \<phi>(1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> 0 \<le> \<phi> 1
[PROOF STEP]
using phi(3) phi(4)
[PROOF STATE]
proof (prove)
using this:
\<phi> 0 = 0
\<phi> 1 = 1

goal (1 subgoal):
 1. \<phi> 0 \<le> \<phi> 1
[PROOF STEP]
by (simp add: reparam_weak_def)
[PROOF STATE]
proof (state)
this:
\<phi> 0 \<le> \<phi> 1

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
have v: "\<phi>`{0..1} \<subseteq> {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` {0..1} \<subseteq> {0..1}
[PROOF STEP]
using phi(5)
[PROOF STATE]
proof (prove)
using this:
\<phi> ` {0..1} = {0..1}

goal (1 subgoal):
 1. \<phi> ` {0..1} \<subseteq> {0..1}
[PROOF STEP]
by (simp add: reparam_weak_def)
[PROOF STATE]
proof (state)
this:
\<phi> ` {0..1} \<subseteq> {0..1}

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
obtain D where D_props: "(\<forall>x\<in>{0..1} - s. (\<phi> has_vector_derivative D x) (at x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D. \<forall>x\<in>{0..1} - s. (\<phi> has_vector_derivative D x) (at x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
finite s
\<phi> C1_differentiable_on {0..1} - s

goal (1 subgoal):
 1. (\<And>D. \<forall>x\<in>{0..1} - s. (\<phi> has_vector_derivative D x) (at x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: C1_differentiable_on_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - s. (\<phi> has_vector_derivative D x) (at x)

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1} - s. (\<phi> has_vector_derivative D x) (at x)
[PROOF STEP]
have "(\<And>x. x \<in> ({0..1} -s) \<Longrightarrow> (\<phi> has_vector_derivative D x) (at x within {0..1}))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. (\<phi> has_vector_derivative D x) (at x)

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> (\<phi> has_vector_derivative D x) (at x within {0..1})
[PROOF STEP]
using has_vector_derivative_at_within
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. (\<phi> has_vector_derivative D x) (at x)
(?f has_vector_derivative ?f') (at ?x) \<Longrightarrow> (?f has_vector_derivative ?f') (at ?x within ?S)

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> (\<phi> has_vector_derivative D x) (at x within {0..1})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} - s \<Longrightarrow> (\<phi> has_vector_derivative D ?x) (at ?x within {0..1})

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> {0..1} - s \<Longrightarrow> (\<phi> has_vector_derivative D ?x) (at ?x within {0..1})
[PROOF STEP]
have vi: "(\<And>x. x \<in> ({0..1} - s) \<Longrightarrow> (\<phi> has_real_derivative D x) (at x within {0..1}))"
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} - s \<Longrightarrow> (\<phi> has_vector_derivative D ?x) (at ?x within {0..1})

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> (\<phi> has_real_derivative D x) (at x within {0..1})
[PROOF STEP]
using has_real_derivative_iff_has_vector_derivative
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} - s \<Longrightarrow> (\<phi> has_vector_derivative D ?x) (at ?x within {0..1})
(?f has_real_derivative ?y) ?F = (?f has_vector_derivative ?y) ?F

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> (\<phi> has_real_derivative D x) (at x within {0..1})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} - s \<Longrightarrow> (\<phi> has_real_derivative D ?x) (at ?x within {0..1})

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
have a:"((\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) has_integral
              integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b)))
              {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
using has_integral_substitution_strong[OF s(1) zero_le_one iv v iii cont_phi vi]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> {0..1} - s \<Longrightarrow> x \<in> {0..1} - s) \<Longrightarrow> ((\<lambda>x. D x *\<^sub>R (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}

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

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

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
have gamma2_vec_diffable: "\<And>x::real. x \<in> {0..1} -s \<Longrightarrow> ((\<gamma>2 o \<phi>) has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
fix x::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
assume ass: "x \<in> {0..1} -s"
[PROOF STATE]
proof (state)
this:
x \<in> {0..1} - s

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
have zer_le_x_le_1:"0\<le> x \<and> x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> x \<and> x \<le> 1
[PROOF STEP]
using ass
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1} - s

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

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
show "((\<gamma>2 o \<phi>) has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
have **: "\<gamma>2 differentiable at (\<phi> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma>2 differentiable at (\<phi> x)
[PROOF STEP]
using phi gamma2_differentiable
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x
\<phi> piecewise_C1_differentiable_on {0..1}
\<phi> 0 = 0
\<phi> 1 = 1
\<phi> ` {0..1} = {0..1}
\<forall>x\<in>{0..1}. \<gamma>2 differentiable at x

goal (1 subgoal):
 1. \<gamma>2 differentiable at (\<phi> x)
[PROOF STEP]
by (auto simp add: zer_le_x_le_1)
[PROOF STATE]
proof (state)
this:
\<gamma>2 differentiable at (\<phi> x)

goal (1 subgoal):
 1. (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
have ***: " \<phi> differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> differentiable at x
[PROOF STEP]
using s ass
[PROOF STATE]
proof (prove)
using this:
finite s
\<phi> C1_differentiable_on {0..1} - s
x \<in> {0..1} - s

goal (1 subgoal):
 1. \<phi> differentiable at x
[PROOF STEP]
by (auto simp add: C1_differentiable_on_eq)
[PROOF STATE]
proof (state)
this:
\<phi> differentiable at x

goal (1 subgoal):
 1. (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> differentiable at x
[PROOF STEP]
show "((\<gamma>2 o \<phi>) has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)"
[PROOF STATE]
proof (prove)
using this:
\<phi> differentiable at x

goal (1 subgoal):
 1. (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
using differentiable_chain_at[OF *** **]
[PROOF STATE]
proof (prove)
using this:
\<phi> differentiable at x
\<gamma>2 \<circ> \<phi> differentiable at x

goal (1 subgoal):
 1. (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)
[PROOF STEP]
by (auto simp add: vector_derivative_works)
[PROOF STATE]
proof (state)
this:
(\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x)) (at x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} - s \<Longrightarrow> (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x)) (at ?x)

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> {0..1} - s \<Longrightarrow> (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x)) (at ?x)
[PROOF STEP]
have gamma2_vec_deriv_within: "\<And>x::real. x \<in> {0..1} -s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})"
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} - s \<Longrightarrow> (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x)) (at ?x)

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})
[PROOF STEP]
using vector_derivative_at_within_ivl[OF gamma2_vec_diffable]
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} - s \<Longrightarrow> (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x)) (at ?x)
\<lbrakk>?x \<in> {0..1} - s; ?a \<le> ?x; ?x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x within {?a..?b}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x)

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x within {0..1})

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
have "\<forall>x\<in>{0..1} - s. D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - s. D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
fix x::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
assume ass: "x \<in> {0..1} -s"
[PROOF STATE]
proof (state)
this:
x \<in> {0..1} - s

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {0..1} - s
[PROOF STEP]
have 0: "\<phi> differentiable (at x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1} - s

goal (1 subgoal):
 1. \<phi> differentiable at x
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
x \<in> {0..1} - s
finite s
\<phi> C1_differentiable_on {0..1} - s

goal (1 subgoal):
 1. \<phi> differentiable at x
[PROOF STEP]
by (auto simp add: C1_differentiable_on_def differentiable_def has_vector_derivative_def)
[PROOF STATE]
proof (state)
this:
\<phi> differentiable at x

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
obtain D2 where "(\<phi> has_vector_derivative D2) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D2. (\<phi> has_vector_derivative D2) (at x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using D_props ass
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. (\<phi> has_vector_derivative D x) (at x)
x \<in> {0..1} - s

goal (1 subgoal):
 1. (\<And>D2. (\<phi> has_vector_derivative D2) (at x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<phi> has_vector_derivative D2) (at x)

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
have "\<phi> x \<in> {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> x \<in> {0..1}
[PROOF STEP]
using phi(5) ass
[PROOF STATE]
proof (prove)
using this:
\<phi> ` {0..1} = {0..1}
x \<in> {0..1} - s

goal (1 subgoal):
 1. \<phi> x \<in> {0..1}
[PROOF STEP]
by (auto simp add: reparam_weak_def)
[PROOF STATE]
proof (state)
this:
\<phi> x \<in> {0..1}

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> x \<in> {0..1}
[PROOF STEP]
have 1: "\<gamma>2 differentiable (at (\<phi> x))"
[PROOF STATE]
proof (prove)
using this:
\<phi> x \<in> {0..1}

goal (1 subgoal):
 1. \<gamma>2 differentiable at (\<phi> x)
[PROOF STEP]
using gamma2_differentiable
[PROOF STATE]
proof (prove)
using this:
\<phi> x \<in> {0..1}
\<forall>x\<in>{0..1}. \<gamma>2 differentiable at x

goal (1 subgoal):
 1. \<gamma>2 differentiable at (\<phi> x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<gamma>2 differentiable at (\<phi> x)

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
have 3:" vector_derivative \<gamma>2 (at (\<phi> x)) =  vector_derivative \<gamma>2 (at (\<phi> x) within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative \<gamma>2 (at (\<phi> x)) = vector_derivative \<gamma>2 (at (\<phi> x) within {0..1})
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vector_derivative \<gamma>2 (at (\<phi> x)) = vector_derivative \<gamma>2 (at (\<phi> x) within {0..1})
[PROOF STEP]
have *:"0\<le> \<phi> x \<and> \<phi> x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<phi> x \<and> \<phi> x \<le> 1
[PROOF STEP]
using phi(5) ass
[PROOF STATE]
proof (prove)
using this:
\<phi> ` {0..1} = {0..1}
x \<in> {0..1} - s

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

goal (1 subgoal):
 1. vector_derivative \<gamma>2 (at (\<phi> x)) = vector_derivative \<gamma>2 (at (\<phi> x) within {0..1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> \<phi> x \<and> \<phi> x \<le> 1
[PROOF STEP]
have **:"(\<gamma>2 has_vector_derivative (vector_derivative \<gamma>2 (at (\<phi> x)))) (at (\<phi> x))"
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<phi> x \<and> \<phi> x \<le> 1

goal (1 subgoal):
 1. (\<gamma>2 has_vector_derivative vector_derivative \<gamma>2 (at (\<phi> x))) (at (\<phi> x))
[PROOF STEP]
using 1 vector_derivative_works
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<phi> x \<and> \<phi> x \<le> 1
\<gamma>2 differentiable at (\<phi> x)
(?f differentiable ?net) = (?f has_vector_derivative vector_derivative ?f ?net) ?net

goal (1 subgoal):
 1. (\<gamma>2 has_vector_derivative vector_derivative \<gamma>2 (at (\<phi> x))) (at (\<phi> x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<gamma>2 has_vector_derivative vector_derivative \<gamma>2 (at (\<phi> x))) (at (\<phi> x))

goal (1 subgoal):
 1. vector_derivative \<gamma>2 (at (\<phi> x)) = vector_derivative \<gamma>2 (at (\<phi> x) within {0..1})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative \<gamma>2 (at (\<phi> x)) = vector_derivative \<gamma>2 (at (\<phi> x) within {0..1})
[PROOF STEP]
using * vector_derivative_at_within_ivl[OF **]
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<phi> x \<and> \<phi> x \<le> 1
\<lbrakk>?a \<le> \<phi> x; \<phi> x \<le> ?b; ?a < ?b\<rbrakk> \<Longrightarrow> vector_derivative \<gamma>2 (at (\<phi> x) within {?a..?b}) = vector_derivative \<gamma>2 (at (\<phi> x))

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
show "D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
using vector_derivative_chain_at[OF 0 1]
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<gamma>2 \<circ> \<phi>) (at x) = vector_derivative \<phi> (at x) *\<^sub>R vector_derivative \<gamma>2 (at (\<phi> x))

goal (1 subgoal):
 1. D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
apply (auto simp add: gamma2_vec_deriv_within[OF ass, symmetric] 3[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vector_derivative (\<gamma>2 \<circ> \<phi>) (at x) = vector_derivative \<phi> (at x) *\<^sub>R vector_derivative \<gamma>2 (at (\<phi> x)); D x \<noteq> vector_derivative \<phi> (at x)\<rbrakk> \<Longrightarrow> vector_derivative \<gamma>2 (at (\<phi> x)) \<bullet> b = 0
[PROOF STEP]
using D_props ass vector_derivative_at
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. (\<phi> has_vector_derivative D x) (at x)
x \<in> {0..1} - s
(?f has_vector_derivative ?f') (at ?x) \<Longrightarrow> vector_derivative ?f (at ?x) = ?f'

goal (1 subgoal):
 1. \<lbrakk>vector_derivative (\<gamma>2 \<circ> \<phi>) (at x) = vector_derivative \<phi> (at x) *\<^sub>R vector_derivative \<gamma>2 (at (\<phi> x)); D x \<noteq> vector_derivative \<phi> (at x)\<rbrakk> \<Longrightarrow> vector_derivative \<gamma>2 (at (\<phi> x)) \<bullet> b = 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - s. D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0..1} - s. D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b
[PROOF STEP]
have c:"\<And>x.  x\<in>({0..1} -s) \<Longrightarrow> D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b)) =
                                    F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - s. D x * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} - s \<Longrightarrow> D ?x * (F (\<gamma>2 (\<phi> ?x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> ?x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> ?x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x within {0..1}) \<bullet> b)

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> {0..1} - s \<Longrightarrow> D ?x * (F (\<gamma>2 (\<phi> ?x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> ?x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> ?x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x within {0..1}) \<bullet> b)
[PROOF STEP]
have d: "integral ({0..1}) (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) =
                                            integral ({0..1}) (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b))"
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} - s \<Longrightarrow> D ?x * (F (\<gamma>2 (\<phi> ?x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> ?x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> ?x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x within {0..1}) \<bullet> b)

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) \<Longrightarrow> integral {0..1} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b))
[PROOF STEP]
have "negligible s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. negligible s
[PROOF STEP]
using s(1)
[PROOF STATE]
proof (prove)
using this:
finite s

goal (1 subgoal):
 1. negligible s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
negligible s

goal (1 subgoal):
 1. (\<And>x. x \<in> {0..1} - s \<Longrightarrow> D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) \<Longrightarrow> integral {0..1} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
negligible s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
negligible s

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b))
[PROOF STEP]
using c integral_spike
[PROOF STATE]
proof (prove)
using this:
negligible s
?x \<in> {0..1} - s \<Longrightarrow> D ?x * (F (\<gamma>2 (\<phi> ?x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> ?x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> ?x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x within {0..1}) \<bullet> b)
\<lbrakk>negligible ?S; \<And>x. x \<in> ?T - ?S \<Longrightarrow> ?g x = ?f x\<rbrakk> \<Longrightarrow> integral ?T ?f = integral ?T ?g

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b))
[PROOF STEP]
by (metis(no_types,lifting))
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b))

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
have phi_in_int: "(\<And>x. x \<in> {0..1} \<Longrightarrow> \<phi> x \<in> {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> \<phi> x \<in> {0..1}
[PROOF STEP]
using phi
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x
\<phi> piecewise_C1_differentiable_on {0..1}
\<phi> 0 = 0
\<phi> 1 = 1
\<phi> ` {0..1} = {0..1}

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> \<phi> x \<in> {0..1}
[PROOF STEP]
by(auto simp add:)
[PROOF STATE]
proof (state)
this:
?x \<in> {0..1} \<Longrightarrow> \<phi> ?x \<in> {0..1}

goal (2 subgoals):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
 2. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> {0..1} \<Longrightarrow> \<phi> ?x \<in> {0..1}
[PROOF STEP]
have e: "((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral
                             integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))){0..1}"
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} \<Longrightarrow> \<phi> ?x \<in> {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x. x \<in> {0..1} \<Longrightarrow> \<phi> x \<in> {0..1}) \<Longrightarrow> ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
have 0:"negligible s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. negligible s
[PROOF STEP]
using s(1)
[PROOF STATE]
proof (prove)
using this:
finite s

goal (1 subgoal):
 1. negligible s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
negligible s

goal (1 subgoal):
 1. (\<And>x. x \<in> {0..1} \<Longrightarrow> \<phi> x \<in> {0..1}) \<Longrightarrow> ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
have c':"\<forall> x\<in> {0..1} -s. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b)) =
                                    F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - s. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
?x \<in> {0..1} - s \<Longrightarrow> D ?x * (F (\<gamma>2 (\<phi> ?x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> ?x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> ?x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x within {0..1}) \<bullet> b)

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - s. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - s. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b)) = F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)

goal (1 subgoal):
 1. (\<And>x. x \<in> {0..1} \<Longrightarrow> \<phi> x \<in> {0..1}) \<Longrightarrow> ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
have has_integral_spike_eq': "\<And>s t f g y. negligible s \<Longrightarrow>
                                               \<forall>x\<in>t - s. g x = f x \<Longrightarrow> (f has_integral y) t = (g has_integral y) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t f g y. \<lbrakk>negligible s; \<forall>x\<in>t - s. g x = f x\<rbrakk> \<Longrightarrow> (f has_integral y) t = (g has_integral y) t
[PROOF STEP]
using has_integral_spike_eq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>negligible ?S; \<And>x. x \<in> ?T - ?S \<Longrightarrow> ?g x = ?f x\<rbrakk> \<Longrightarrow> (?f has_integral ?y) ?T = (?g has_integral ?y) ?T

goal (1 subgoal):
 1. \<And>s t f g y. \<lbrakk>negligible s; \<forall>x\<in>t - s. g x = f x\<rbrakk> \<Longrightarrow> (f has_integral y) t = (g has_integral y) t
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<lbrakk>negligible ?s; \<forall>x\<in>?t - ?s. ?g x = ?f x\<rbrakk> \<Longrightarrow> (?f has_integral ?y) ?t = (?g has_integral ?y) ?t

goal (1 subgoal):
 1. (\<And>x. x \<in> {0..1} \<Longrightarrow> \<phi> x \<in> {0..1}) \<Longrightarrow> ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
using a has_integral_spike_eq'[OF 0 c']
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral ?y) {0..1} = ((\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) has_integral ?y) {0..1}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}

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

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1} \<Longrightarrow> ((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
assume ass: "((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral
                            integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b)))
                             {0..1}"
[PROOF STATE]
proof (state)
this:
((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1} \<Longrightarrow> ((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
have *:"\<forall>x\<in>{0..1} - (s\<union>{0,1}). (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative  (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) x =
                                                  (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)
[PROOF STEP]
have "\<forall>x\<in>{0<..<1} - s. (vector_derivative  (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = (vector_derivative  (\<gamma>1) (at x within {0..1}) \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0<..<1} - s. vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
have i: "open ({0<..<1} - s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open ({0<..<1} - s)
[PROOF STEP]
using open_diff s open_greaterThanLessThan
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?t; open ?s\<rbrakk> \<Longrightarrow> open (?s - ?t)
finite s
\<phi> C1_differentiable_on {0..1} - s
open {?a<..<?b}

goal (1 subgoal):
 1. open ({0<..<1} - s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
open ({0<..<1} - s)

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
have ii: "\<forall>x\<in>{0<..<1::real} - s. (\<gamma>2 \<circ> \<phi>) x = \<gamma>1 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0<..<1} - s. (\<gamma>2 \<circ> \<phi>) x = \<gamma>1 x
[PROOF STEP]
using phi(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x

goal (1 subgoal):
 1. \<forall>x\<in>{0<..<1} - s. (\<gamma>2 \<circ> \<phi>) x = \<gamma>1 x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0<..<1} - s. (\<gamma>2 \<circ> \<phi>) x = \<gamma>1 x

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
fix x::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
assume ass: " x \<in> {0<..<1::real} - s"
[PROOF STATE]
proof (state)
this:
x \<in> {0<..<1} - s

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> {0<..<1} - s
[PROOF STEP]
have iii: "(\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> {0<..<1} - s

goal (1 subgoal):
 1. (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)
[PROOF STEP]
using has_vector_derivative_at_within gamma2_vec_deriv_within gamma2_vec_diffable
[PROOF STATE]
proof (prove)
using this:
x \<in> {0<..<1} - s
(?f has_vector_derivative ?f') (at ?x) \<Longrightarrow> (?f has_vector_derivative ?f') (at ?x within ?S)
?x \<in> {0..1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x within {0..1})
?x \<in> {0..1} - s \<Longrightarrow> (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at ?x)) (at ?x)

goal (1 subgoal):
 1. (\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
(*Most crucial but annoying step*)
[PROOF STATE]
proof (state)
this:
(\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)
[PROOF STEP]
have iv:"(\<gamma>1 has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)"
[PROOF STATE]
proof (prove)
using this:
(\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)

goal (1 subgoal):
 1. (\<gamma>1 has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)
[PROOF STEP]
using has_derivative_transform_within_open i ii ass
[PROOF STATE]
proof (prove)
using this:
(\<gamma>2 \<circ> \<phi> has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)
\<lbrakk>(?f has_derivative ?f') (at ?x within ?t); open ?s; ?x \<in> ?s; \<And>x. x \<in> ?s \<Longrightarrow> ?f x = ?g x\<rbrakk> \<Longrightarrow> (?g has_derivative ?f') (at ?x within ?t)
open ({0<..<1} - s)
\<forall>x\<in>{0<..<1} - s. (\<gamma>2 \<circ> \<phi>) x = \<gamma>1 x
x \<in> {0<..<1} - s

goal (1 subgoal):
 1. (\<gamma>1 has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)
[PROOF STEP]
apply(auto simp add: has_vector_derivative_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<gamma>2 \<circ> \<phi> has_derivative (\<lambda>xa. xa *\<^sub>R vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}))) (at x); \<And>f f' x t s g. \<lbrakk>(f has_derivative f') (at x within t); open s; x \<in> s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> (g has_derivative f') (at x within t); open ({0<..<1} - s); \<forall>x\<in>{0<..<1} - s. \<gamma>2 (\<phi> x) = \<gamma>1 x; 0 < x; x < 1; x \<notin> s\<rbrakk> \<Longrightarrow> (\<gamma>1 has_derivative (\<lambda>xa. xa *\<^sub>R vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}))) (at x)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<gamma>1 has_vector_derivative vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})) (at x)

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
have v: "0 \<le> x" "x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> x &&& x \<le> 1
[PROOF STEP]
using ass
[PROOF STATE]
proof (prove)
using this:
x \<in> {0<..<1} - s

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

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
have 0: "vector_derivative \<gamma>1 (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative \<gamma>1 (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})
[PROOF STEP]
using vector_derivative_at_within_ivl[OF iv v(1) v(2) zero_less_one]
[PROOF STATE]
proof (prove)
using this:
vector_derivative \<gamma>1 (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})

goal (1 subgoal):
 1. vector_derivative \<gamma>1 (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vector_derivative \<gamma>1 (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
have 1: "vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})
[PROOF STEP]
using vector_derivative_at_within_ivl[OF iii v(1) v(2) zero_less_one]
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})

goal (1 subgoal):
 1. vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})
[PROOF STEP]
have "vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative \<gamma>1 (at x within {0..1})"
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})

goal (1 subgoal):
 1. vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative \<gamma>1 (at x within {0..1})
[PROOF STEP]
using 0 1
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})
vector_derivative \<gamma>1 (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})
vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1})

goal (1 subgoal):
 1. vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative \<gamma>1 (at x within {0..1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative \<gamma>1 (at x within {0..1})

goal (1 subgoal):
 1. \<And>x. x \<in> {0<..<1} - s \<Longrightarrow> vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative \<gamma>1 (at x within {0..1})
[PROOF STEP]
show "vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b"
[PROOF STATE]
proof (prove)
using this:
vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) = vector_derivative \<gamma>1 (at x within {0..1})

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0<..<1} - s. vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>{0<..<1} - s. vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
have i: "\<forall>x\<in>{0..1} - (s\<union>{0,1}). (vector_derivative  (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = (vector_derivative  (\<gamma>1) (at x within {0..1}) \<bullet> b)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0<..<1} - s. vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - (s \<union> {0, 1}). vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - (s \<union> {0, 1}). vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)
[PROOF STEP]
have ii: "\<forall>x\<in>{0..1} - (s\<union>{0,1}).  F (\<gamma>1 x) \<bullet> b =  F (\<gamma>2 (\<phi> x)) \<bullet> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>1 x) \<bullet> b = F (\<gamma>2 (\<phi> x)) \<bullet> b
[PROOF STEP]
using phi(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>1 x) \<bullet> b = F (\<gamma>2 (\<phi> x)) \<bullet> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>1 x) \<bullet> b = F (\<gamma>2 (\<phi> x)) \<bullet> b

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)
[PROOF STEP]
using i ii
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{0..1} - (s \<union> {0, 1}). vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b = vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b
\<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>1 x) \<bullet> b = F (\<gamma>2 (\<phi> x)) \<bullet> b

goal (1 subgoal):
 1. \<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1} - (s \<union> {0, 1}). F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b) = F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1} \<Longrightarrow> ((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
have **: "negligible (s\<union>{0,1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. negligible (s \<union> {0, 1})
[PROOF STEP]
using s(1)
[PROOF STATE]
proof (prove)
using this:
finite s

goal (1 subgoal):
 1. negligible (s \<union> {0, 1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
negligible (s \<union> {0, 1})

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1} \<Longrightarrow> ((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
have has_integral_spike_eq': "\<And>s t g f y. negligible s \<Longrightarrow>
                                \<forall>x\<in>t - s. g x = f x \<Longrightarrow> (f has_integral y) t = (g has_integral y) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t g f y. \<lbrakk>negligible s; \<forall>x\<in>t - s. g x = f x\<rbrakk> \<Longrightarrow> (f has_integral y) t = (g has_integral y) t
[PROOF STEP]
using has_integral_spike_eq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>negligible ?S; \<And>x. x \<in> ?T - ?S \<Longrightarrow> ?g x = ?f x\<rbrakk> \<Longrightarrow> (?f has_integral ?y) ?T = (?g has_integral ?y) ?T

goal (1 subgoal):
 1. \<And>s t g f y. \<lbrakk>negligible s; \<forall>x\<in>t - s. g x = f x\<rbrakk> \<Longrightarrow> (f has_integral y) t = (g has_integral y) t
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<lbrakk>negligible ?s; \<forall>x\<in>?t - ?s. ?g x = ?f x\<rbrakk> \<Longrightarrow> (?f has_integral ?y) ?t = (?g has_integral ?y) ?t

goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1} \<Longrightarrow> ((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
using has_integral_spike_eq'[OF ** *] ass
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral ?y) {0..1} = ((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral ?y) {0..1}
((\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}

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

goal (1 subgoal):
 1. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
using phi
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) has_integral integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))) {0..1}
\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x
\<phi> piecewise_C1_differentiable_on {0..1}
\<phi> 0 = 0
\<phi> 1 = 1
\<phi> ` {0..1} = {0..1}

goal (1 subgoal):
 1. line_integral_exists F {b} \<gamma>1
[PROOF STEP]
by(auto simp add: line_integral_exists_def)
[PROOF STATE]
proof (state)
this:
line_integral_exists F {b} \<gamma>1

goal (1 subgoal):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
[PROOF STEP]
have "integral ({0..1}) (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) =
                      integral ({0..1}) (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1  (at x within {0..1}) \<bullet> b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
using integral_unique[OF e] integral_unique[OF f]
[PROOF STATE]
proof (prove)
using this:
integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
integral {0..1} (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b)) = integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b))

goal (1 subgoal):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b))

goal (1 subgoal):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
[PROOF STEP]
have "integral ({0..1}) (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) =
                         integral ({0..1}) (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
using b d phi
[PROOF STATE]
proof (prove)
using this:
integral {0..1} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = integral {\<phi> 0..\<phi> 1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
integral {0..1} (\<lambda>x. D x * (F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative \<gamma>2 (at (\<phi> x) within {0..1}) \<bullet> b))) = integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b))
\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x
\<phi> piecewise_C1_differentiable_on {0..1}
\<phi> 0 = 0
\<phi> 1 = 1
\<phi> ` {0..1} = {0..1}

goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
by (auto simp add:)
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))

goal (1 subgoal):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b))
integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
[PROOF STEP]
show "line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2"
[PROOF STATE]
proof (prove)
using this:
integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b))
integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))

goal (1 subgoal):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
[PROOF STEP]
using phi
[PROOF STATE]
proof (prove)
using this:
integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>1 x) \<bullet> b * (vector_derivative \<gamma>1 (at x within {0..1}) \<bullet> b))
integral {0..1} (\<lambda>x. F (\<gamma>2 (\<phi> x)) \<bullet> b * (vector_derivative (\<gamma>2 \<circ> \<phi>) (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. F (\<gamma>2 x) \<bullet> b * (vector_derivative \<gamma>2 (at x within {0..1}) \<bullet> b))
\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>2 \<circ> \<phi>) x
\<phi> piecewise_C1_differentiable_on {0..1}
\<phi> 0 = 0
\<phi> 1 = 1
\<phi> ` {0..1} = {0..1}

goal (1 subgoal):
 1. line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2
[PROOF STEP]
by(auto simp add: line_integral_def)
[PROOF STATE]
proof (state)
this:
line_integral F {b} \<gamma>1 = line_integral F {b} \<gamma>2

goal:
No subgoals!
[PROOF STEP]
qed