[STATEMENT]
lemma one_chain_line_integral_eq_line_integral_on_sudivision':
  assumes chain1_eq_chain2: "chain_subdiv_chain one_chain1 subdiv" and
    boundary_chain1: "boundary_chain one_chain1" and
    boundary_chain2: "boundary_chain subdiv" and
    line_integral_exists_on_chain1: "\<forall>(k, \<gamma>) \<in> one_chain1. line_integral_exists F basis \<gamma>" and
    valid_path: "\<forall>(k, \<gamma>) \<in> subdiv. valid_path \<gamma>" and
    finite_chain1: "finite one_chain1" and
    finite_basis: "finite basis"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv"
    "\<forall>(k, \<gamma>) \<in> subdiv. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv &&& \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
 2. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
[PROOF STEP]
obtain f where f_props:
    "((\<Union>(f ` one_chain1)) = subdiv)"
    "(\<forall>(k,\<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f(k,\<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f(k,\<gamma>)))"
    "(\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {})"
    "(\<forall>x \<in> one_chain1. finite (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<Union> (f ` one_chain1) = subdiv; \<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>)); \<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}; \<forall>x\<in>one_chain1. finite (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using chain1_eq_chain2 chain_subdiv_chain_character
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_chain one_chain1 subdiv
chain_subdiv_chain ?one_chain1.0 ?subdiv = (\<exists>f. \<Union> (f ` ?one_chain1.0) = ?subdiv \<and> (\<forall>(k, \<gamma>)\<in>?one_chain1.0. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))) \<and> (\<forall>p\<in>?one_chain1.0. \<forall>p'\<in>?one_chain1.0. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}) \<and> (\<forall>x\<in>?one_chain1.0. finite (f x)))

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<Union> (f ` one_chain1) = subdiv; \<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>)); \<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}; \<forall>x\<in>one_chain1. finite (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: pairwise_def chain_subdiv_chain_def)
[PROOF STATE]
proof (state)
this:
\<Union> (f ` one_chain1) = subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}
\<forall>x\<in>one_chain1. finite (f x)

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
 2. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
[PROOF STEP]
have finite_chain2: "finite subdiv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite subdiv
[PROOF STEP]
using finite_chain1 f_props(1) f_props(4)
[PROOF STATE]
proof (prove)
using this:
finite one_chain1
\<Union> (f ` one_chain1) = subdiv
\<forall>x\<in>one_chain1. finite (f x)

goal (1 subgoal):
 1. finite subdiv
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite subdiv

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
 2. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
[PROOF STEP]
have "\<And>k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
fix k \<gamma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
assume ass: "(k, \<gamma>) \<in> subdiv"
[PROOF STATE]
proof (state)
this:
(k, \<gamma>) \<in> subdiv

goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(k, \<gamma>) \<in> subdiv
[PROOF STEP]
obtain k' \<gamma>' where kp_gammap: "(k',\<gamma>') \<in> one_chain1" "(k,\<gamma>) \<in> f(k',\<gamma>')"
[PROOF STATE]
proof (prove)
using this:
(k, \<gamma>) \<in> subdiv

goal (1 subgoal):
 1. (\<And>k' \<gamma>'. \<lbrakk>(k', \<gamma>') \<in> one_chain1; (k, \<gamma>) \<in> f (k', \<gamma>')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f_props(1)
[PROOF STATE]
proof (prove)
using this:
(k, \<gamma>) \<in> subdiv
\<Union> (f ` one_chain1) = subdiv

goal (1 subgoal):
 1. (\<And>k' \<gamma>'. \<lbrakk>(k', \<gamma>') \<in> one_chain1; (k, \<gamma>) \<in> f (k', \<gamma>')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
show "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof (cases "k' = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k' = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
assume k_eq_1: "k' = 1"
[PROOF STATE]
proof (state)
this:
k' = 1

goal (2 subgoals):
 1. k' = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' = 1
[PROOF STEP]
have i:"chain_subdiv_path \<gamma>' (f(k',\<gamma>'))"
[PROOF STATE]
proof (prove)
using this:
k' = 1

goal (1 subgoal):
 1. chain_subdiv_path \<gamma>' (f (k', \<gamma>'))
[PROOF STEP]
using f_props(2) kp_gammap ass
[PROOF STATE]
proof (prove)
using this:
k' = 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')
(k, \<gamma>) \<in> subdiv

goal (1 subgoal):
 1. chain_subdiv_path \<gamma>' (f (k', \<gamma>'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
chain_subdiv_path \<gamma>' (f (k', \<gamma>'))

goal (2 subgoals):
 1. k' = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have ii:"boundary_chain (f(k',\<gamma>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (f (k', \<gamma>'))
[PROOF STEP]
using f_props(1) ass assms kp_gammap
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> subdiv
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

goal (1 subgoal):
 1. boundary_chain (f (k', \<gamma>'))
[PROOF STEP]
by (meson UN_I boundary_chain_def)
[PROOF STATE]
proof (state)
this:
boundary_chain (f (k', \<gamma>'))

goal (2 subgoals):
 1. k' = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have iii:"line_integral_exists F basis \<gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>'
[PROOF STEP]
using assms kp_gammap
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

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

goal (2 subgoals):
 1. k' = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have "iv": " \<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). valid_path \<gamma>
[PROOF STEP]
using f_props(1) ass assms kp_gammap
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> subdiv
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). valid_path \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). valid_path \<gamma>

goal (2 subgoals):
 1. k' = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using line_integral_on_path_eq_line_integral_on_equiv_chain'(2)[OF i ii iii iv finite_basis] kp_gammap
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). line_integral_exists F basis \<gamma>
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

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

goal (1 subgoal):
 1. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
assume "k' \<noteq> 1"
[PROOF STATE]
proof (state)
this:
k' \<noteq> 1

goal (1 subgoal):
 1. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' \<noteq> 1
[PROOF STEP]
have k_eq_neg1: "k' = -1"
[PROOF STATE]
proof (prove)
using this:
k' \<noteq> 1

goal (1 subgoal):
 1. k' = - 1
[PROOF STEP]
using boundary_chain1 kp_gammap
[PROOF STATE]
proof (prove)
using this:
k' \<noteq> 1
boundary_chain one_chain1
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

goal (1 subgoal):
 1. k' = - 1
[PROOF STEP]
by (auto simp add: boundary_chain_def)
[PROOF STATE]
proof (state)
this:
k' = - 1

goal (1 subgoal):
 1. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' = - 1
[PROOF STEP]
have i:"chain_subdiv_path (reversepath \<gamma>') (f(k',\<gamma>'))"
[PROOF STATE]
proof (prove)
using this:
k' = - 1

goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>') (f (k', \<gamma>'))
[PROOF STEP]
using f_props(2) kp_gammap
[PROOF STATE]
proof (prove)
using this:
k' = - 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>') (f (k', \<gamma>'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
chain_subdiv_path (reversepath \<gamma>') (f (k', \<gamma>'))

goal (1 subgoal):
 1. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have ii:"boundary_chain (f(k',\<gamma>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (f (k', \<gamma>'))
[PROOF STEP]
using f_props(1) assms kp_gammap
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

goal (1 subgoal):
 1. boundary_chain (f (k', \<gamma>'))
[PROOF STEP]
by (meson UN_I boundary_chain_def)
[PROOF STATE]
proof (state)
this:
boundary_chain (f (k', \<gamma>'))

goal (1 subgoal):
 1. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have iii: " \<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). valid_path \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). valid_path \<gamma>
[PROOF STEP]
using f_props(1) ass assms kp_gammap
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> subdiv
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). valid_path \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). valid_path \<gamma>

goal (1 subgoal):
 1. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have iv: "valid_path (reversepath \<gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (reversepath \<gamma>')
[PROOF STEP]
using valid_path_equiv_valid_chain_list[OF i ii iii]
[PROOF STATE]
proof (prove)
using this:
valid_path (reversepath \<gamma>')

goal (1 subgoal):
 1. valid_path (reversepath \<gamma>')
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
valid_path (reversepath \<gamma>')

goal (1 subgoal):
 1. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have "line_integral_exists F basis \<gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>'
[PROOF STEP]
using assms kp_gammap
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

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

goal (1 subgoal):
 1. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
line_integral_exists F basis \<gamma>'
[PROOF STEP]
have x: "line_integral_exists F basis (reversepath \<gamma>')"
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma>'

goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma>')
[PROOF STEP]
using iv line_integral_on_reverse_path(2) valid_path_reversepath
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma>'
valid_path (reversepath \<gamma>')
\<lbrakk>valid_path ?\<gamma>; line_integral_exists ?F ?basis ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (reversepath ?\<gamma>)
valid_path (reversepath ?g) = valid_path ?g

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

goal (1 subgoal):
 1. k' \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using line_integral_on_path_eq_line_integral_on_equiv_chain'(2)[OF i ii x iii finite_basis] kp_gammap
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>f (k', \<gamma>'). line_integral_exists F basis \<gamma>
(k', \<gamma>') \<in> one_chain1
(k, \<gamma>) \<in> f (k', \<gamma>')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?k, ?\<gamma>) \<in> subdiv \<Longrightarrow> line_integral_exists F basis ?\<gamma>

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
 2. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?k, ?\<gamma>) \<in> subdiv \<Longrightarrow> line_integral_exists F basis ?\<gamma>
[PROOF STEP]
show "\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
(?k, ?\<gamma>) \<in> subdiv \<Longrightarrow> line_integral_exists F basis ?\<gamma>

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

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv"
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
[PROOF STEP]
using one_chain_line_integral_eq_line_integral_on_sudivision(1) assms
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
\<lbrakk>chain_subdiv_chain ?one_chain1.0 ?subdiv; boundary_chain ?one_chain1.0; boundary_chain ?subdiv; \<forall>(k, \<gamma>)\<in>?subdiv. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?subdiv. valid_path \<gamma>; finite ?one_chain1.0; finite ?basis\<rbrakk> \<Longrightarrow> one_chain_line_integral ?F ?basis ?one_chain1.0 = one_chain_line_integral ?F ?basis ?subdiv
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_sum_gen:
  assumes finite_basis:
    "finite basis" and
    line_integral_exists:
    "line_integral_exists F basis1 \<gamma>"
    "line_integral_exists F basis2 \<gamma>" and
    basis_partition:
    "basis1 \<union> basis2 = basis" "basis1 \<inter> basis2 = {}"
  shows "line_integral F basis \<gamma> = (line_integral F  basis1 \<gamma>) + (line_integral F basis2 \<gamma>)"
    "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = line_integral F basis1 \<gamma> + line_integral F basis2 \<gamma> &&& line_integral_exists F basis \<gamma>
[PROOF STEP]
apply (simp add: line_integral_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))
 2. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))
 2. line_integral_exists F basis \<gamma>
[PROOF STEP]
have 0: "integral {0..1} (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                                       (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) =
                    integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                           integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) = integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))
[PROOF STEP]
using Henstock_Kurzweil_Integration.integral_add line_integral_exists
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f integrable_on ?S; ?g integrable_on ?S\<rbrakk> \<Longrightarrow> integral ?S (\<lambda>x. ?f x + ?g x) = integral ?S ?f + integral ?S ?g
line_integral_exists F basis1 \<gamma>
line_integral_exists F basis2 \<gamma>

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

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))
 2. line_integral_exists F basis \<gamma>
[PROOF STEP]
have 1: "integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) =
                       integral {0..1} (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                                            (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))
[PROOF STEP]
by (metis (mono_tags, lifting) basis_partition finite_Un finite_basis sum.union_disjoint)
[PROOF STATE]
proof (state)
this:
integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))

goal (2 subgoals):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))
 2. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) =
                  integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                  integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))
[PROOF STEP]
using 0 1
[PROOF STATE]
proof (prove)
using this:
integral {0..1} (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) = integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))
integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = integral {0..1} (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))

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

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have 2: "((\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                                       (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) has_integral
                    integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                           integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
using Henstock_Kurzweil_Integration.has_integral_add line_integral_exists has_integral_integral
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?f has_integral ?k) ?S; (?g has_integral ?l) ?S\<rbrakk> \<Longrightarrow> ((\<lambda>x. ?f x + ?g x) has_integral ?k + ?l) ?S
line_integral_exists F basis1 \<gamma>
line_integral_exists F basis2 \<gamma>
(?f integrable_on ?s) = (?f has_integral integral ?s ?f) ?s

goal (1 subgoal):
 1. ((\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
apply (auto simp add: line_integral_exists_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f k S g l. \<lbrakk>(f has_integral k) S; (g has_integral l) S\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) has_integral k + l) S; (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) integrable_on {0..1}; (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) integrable_on {0..1}; \<And>f s. (f integrable_on s) = (f has_integral integral s f) s\<rbrakk> \<Longrightarrow> ((\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) {0..1}

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have 3: "(\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) =
                       (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) +
                                            (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))
[PROOF STEP]
by (metis (mono_tags, lifting) basis_partition finite_Un finite_basis sum.union_disjoint)
[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)) = (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
apply(auto simp add: line_integral_exists_def has_integral_integral)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) {0..1}
(\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) {0..1}
[PROOF STEP]
using has_integral_integrable_integral
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) has_integral integral {0..1} (\<lambda>x. \<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + integral {0..1} (\<lambda>x. \<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))) {0..1}
(\<lambda>x. \<Sum>b\<in>basis. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) = (\<lambda>x. (\<Sum>b\<in>basis1. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) + (\<Sum>b\<in>basis2. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)))
(?f has_integral ?i) ?s = (?f integrable_on ?s \<and> integral ?s ?f = ?i)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma common_boundary_sudivision_commutative:
  "(common_boundary_sudivision_exists one_chain1 one_chain2) = (common_boundary_sudivision_exists one_chain2 one_chain1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. common_boundary_sudivision_exists one_chain1 one_chain2 = common_boundary_sudivision_exists one_chain2 one_chain1
[PROOF STEP]
apply (simp add: common_boundary_sudivision_exists_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>subdiv. chain_subdiv_chain one_chain1 subdiv \<and> chain_subdiv_chain one_chain2 subdiv \<and> (\<forall>x\<in>subdiv. case x of (k, \<gamma>) \<Rightarrow> valid_path \<gamma>) \<and> boundary_chain subdiv) = (\<exists>subdiv. chain_subdiv_chain one_chain2 subdiv \<and> chain_subdiv_chain one_chain1 subdiv \<and> (\<forall>x\<in>subdiv. case x of (k, \<gamma>) \<Rightarrow> valid_path \<gamma>) \<and> boundary_chain subdiv)
[PROOF STEP]
by blast


[STATEMENT]
lemma common_subdivision_imp_eq_line_integral:
  assumes "(common_boundary_sudivision_exists one_chain1 one_chain2)"
    "boundary_chain one_chain1"
    "boundary_chain one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
    "finite one_chain1"
    "finite one_chain2"
    "finite basis"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2 &&& \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
obtain subdiv where subdiv_props:
    "chain_subdiv_chain one_chain1 subdiv"
    "chain_subdiv_chain one_chain2 subdiv"
    "(\<forall>(k, \<gamma>) \<in> subdiv. valid_path \<gamma>)"
    "(boundary_chain subdiv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>subdiv. \<lbrakk>chain_subdiv_chain one_chain1 subdiv; chain_subdiv_chain one_chain2 subdiv; \<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>; boundary_chain subdiv\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
common_boundary_sudivision_exists one_chain1 one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
finite one_chain1
finite one_chain2
finite basis

goal (1 subgoal):
 1. (\<And>subdiv. \<lbrakk>chain_subdiv_chain one_chain1 subdiv; chain_subdiv_chain one_chain2 subdiv; \<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>; boundary_chain subdiv\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: common_boundary_sudivision_exists_def)
[PROOF STATE]
proof (state)
this:
chain_subdiv_chain one_chain1 subdiv
chain_subdiv_chain one_chain2 subdiv
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
boundary_chain subdiv

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
have i: "\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
[PROOF STEP]
using one_chain_line_integral_eq_line_integral_on_sudivision'(2)[OF subdiv_props(1) assms(2) subdiv_props(4) assms(4) subdiv_props(3) assms(5) assms(7)]
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>

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

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
using one_chain_line_integral_eq_line_integral_on_sudivision'(1)[OF subdiv_props(1) assms(2) subdiv_props(4) assms(4) subdiv_props(3) assms(5) assms(7)]
      one_chain_line_integral_eq_line_integral_on_sudivision(1)[OF subdiv_props(2) assms(3) subdiv_props(4) i subdiv_props(3) assms(6) assms(7)]
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
one_chain_line_integral F basis one_chain2 = one_chain_line_integral F basis subdiv

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "\<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
using one_chain_line_integral_eq_line_integral_on_sudivision(2)[OF subdiv_props(2) assms(3) subdiv_props(4) i subdiv_props(3) assms(6) assms(7)]
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma common_sudiv_exists_comm:
  shows "common_sudiv_exists C1 C2 = common_sudiv_exists C2 C1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. common_sudiv_exists C1 C2 = common_sudiv_exists C2 C1
[PROOF STEP]
by (auto simp add: common_sudiv_exists_def)


[STATEMENT]
lemma line_integral_degenerate_chain:
  assumes "(\<forall>(k, \<gamma>) \<in> chain. point_path \<gamma>)"
  assumes "finite basis"
  shows "one_chain_line_integral F basis chain = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis chain = 0
[PROOF STEP]
proof (simp add: one_chain_line_integral_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x\<in>chain. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g) = 0
[PROOF STEP]
have "\<forall>(k,g)\<in>chain. line_integral F basis g = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, g)\<in>chain. line_integral F basis g = 0
[PROOF STEP]
using assms line_integral_point_path
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>chain. point_path \<gamma>
finite basis
\<lbrakk>point_path ?\<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> line_integral ?F ?basis ?\<gamma> = 0

goal (1 subgoal):
 1. \<forall>(k, g)\<in>chain. line_integral F basis g = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, g)\<in>chain. line_integral F basis g = 0

goal (1 subgoal):
 1. (\<Sum>x\<in>chain. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(k, g)\<in>chain. line_integral F basis g = 0
[PROOF STEP]
have "\<forall>(k,g)\<in>chain. real_of_int k * line_integral F basis g = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, g)\<in>chain. line_integral F basis g = 0

goal (1 subgoal):
 1. \<forall>(k, g)\<in>chain. real_of_int k * line_integral F basis g = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(k, g)\<in>chain. real_of_int k * line_integral F basis g = 0

goal (1 subgoal):
 1. (\<Sum>x\<in>chain. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(k, g)\<in>chain. real_of_int k * line_integral F basis g = 0
[PROOF STEP]
have "\<And>p. p \<in> chain \<Longrightarrow> (case p of (i, f) \<Rightarrow> real_of_int i * line_integral F basis f) = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, g)\<in>chain. real_of_int k * line_integral F basis g = 0

goal (1 subgoal):
 1. \<And>p. p \<in> chain \<Longrightarrow> (case p of (i, f) \<Rightarrow> real_of_int i * line_integral F basis f) = 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?p \<in> chain \<Longrightarrow> (case ?p of (i, f) \<Rightarrow> real_of_int i * line_integral F basis f) = 0

goal (1 subgoal):
 1. (\<Sum>x\<in>chain. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?p \<in> chain \<Longrightarrow> (case ?p of (i, f) \<Rightarrow> real_of_int i * line_integral F basis f) = 0
[PROOF STEP]
show "(\<Sum>x\<in>chain. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g) = 0"
[PROOF STATE]
proof (prove)
using this:
?p \<in> chain \<Longrightarrow> (case ?p of (i, f) \<Rightarrow> real_of_int i * line_integral F basis f) = 0

goal (1 subgoal):
 1. (\<Sum>x\<in>chain. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>chain. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gen_common_subdiv_imp_common_subdiv:
  shows "(common_sudiv_exists one_chain1 one_chain2) = (\<exists>ps1 ps2. (common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2)) \<and> (\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>) \<and> (\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. common_sudiv_exists one_chain1 one_chain2 = (\<exists>ps1 ps2. common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2) \<and> (\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>) \<and> (\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>))
[PROOF STEP]
by (auto simp add: common_sudiv_exists_def common_boundary_sudivision_exists_def)


[STATEMENT]
lemma common_subdiv_imp_gen_common_subdiv:
  assumes "(common_boundary_sudivision_exists one_chain1 one_chain2)"
  shows "(common_sudiv_exists one_chain1 one_chain2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. common_sudiv_exists one_chain1 one_chain2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
common_boundary_sudivision_exists one_chain1 one_chain2

goal (1 subgoal):
 1. common_sudiv_exists one_chain1 one_chain2
[PROOF STEP]
apply (auto simp add: common_sudiv_exists_def common_boundary_sudivision_exists_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>subdiv. \<lbrakk>chain_subdiv_chain one_chain1 subdiv; chain_subdiv_chain one_chain2 subdiv; \<forall>x\<in>subdiv. case x of (k, \<gamma>) \<Rightarrow> valid_path \<gamma>; boundary_chain subdiv\<rbrakk> \<Longrightarrow> \<exists>subdiv ps1. chain_subdiv_chain (one_chain1 - ps1) subdiv \<and> (\<exists>ps2. chain_subdiv_chain (one_chain2 - ps2) subdiv \<and> (\<forall>x\<in>subdiv. case x of (k, x) \<Rightarrow> valid_path x) \<and> boundary_chain subdiv \<and> (\<forall>x\<in>ps1. case x of (k, x) \<Rightarrow> point_path x) \<and> (\<forall>x\<in>ps2. case x of (k, x) \<Rightarrow> point_path x))
[PROOF STEP]
by (metis Diff_empty all_not_in_conv)


[STATEMENT]
lemma one_chain_line_integral_point_paths:
  assumes "finite one_chain"
  assumes "finite basis"
  assumes "(\<forall>(k, \<gamma>)\<in>ps. point_path \<gamma>)"
  shows "one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis (one_chain)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis one_chain
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis one_chain
[PROOF STEP]
have 0:"(\<forall>x\<in>ps. case x of (k, g) \<Rightarrow>  (real_of_int k * line_integral F basis g) = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>ps. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g = 0
[PROOF STEP]
using line_integral_point_path assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>point_path ?\<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> line_integral ?F ?basis ?\<gamma> = 0
finite one_chain
finite basis
\<forall>(k, \<gamma>)\<in>ps. point_path \<gamma>

goal (1 subgoal):
 1. \<forall>x\<in>ps. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g = 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>ps. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g = 0

goal (1 subgoal):
 1. one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis one_chain
[PROOF STEP]
show "one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis one_chain"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis one_chain
[PROOF STEP]
unfolding one_chain_line_integral_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(k, g)\<in>one_chain - ps. real_of_int k * line_integral F basis g) = (\<Sum>(k, g)\<in>one_chain. real_of_int k * line_integral F basis g)
[PROOF STEP]
using 0 \<open>finite one_chain\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>ps. case x of (k, g) \<Rightarrow> real_of_int k * line_integral F basis g = 0
finite one_chain

goal (1 subgoal):
 1. (\<Sum>(k, g)\<in>one_chain - ps. real_of_int k * line_integral F basis g) = (\<Sum>(k, g)\<in>one_chain. real_of_int k * line_integral F basis g)
[PROOF STEP]
by (force simp add:  intro: comm_monoid_add_class.sum.mono_neutral_left)
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (one_chain - ps) = one_chain_line_integral F basis one_chain

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma boundary_chain_diff:
  assumes "boundary_chain one_chain"
  shows "boundary_chain (one_chain - s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (one_chain - s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
boundary_chain one_chain

goal (1 subgoal):
 1. boundary_chain (one_chain - s)
[PROOF STEP]
by (auto simp add: boundary_chain_def)


[STATEMENT]
lemma gen_common_subdivision_imp_eq_line_integral:
  assumes "(common_sudiv_exists one_chain1 one_chain2)"
    "boundary_chain one_chain1"
    "boundary_chain one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
    "finite one_chain1"
    "finite one_chain2"
    "finite basis"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2 &&& \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
obtain ps1 ps2 where gen_subdiv: "(common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2))" "(\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>)" " (\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps1 ps2. \<lbrakk>common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2); \<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>; \<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) gen_common_subdiv_imp_common_subdiv
[PROOF STATE]
proof (prove)
using this:
common_sudiv_exists one_chain1 one_chain2
common_sudiv_exists ?one_chain1.0 ?one_chain2.0 = (\<exists>ps1 ps2. common_boundary_sudivision_exists (?one_chain1.0 - ps1) (?one_chain2.0 - ps2) \<and> (\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>) \<and> (\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>))

goal (1 subgoal):
 1. (\<And>ps1 ps2. \<lbrakk>common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2); \<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>; \<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2)
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
using one_chain_line_integral_point_paths gen_common_subdiv_imp_common_subdiv
      assms(2-7) gen_subdiv
      common_subdivision_imp_eq_line_integral(1)[OF gen_subdiv(1) boundary_chain_diff[OF assms(2)] boundary_chain_diff[OF assms(3)]]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?one_chain; finite ?basis; \<forall>(k, \<gamma>)\<in>?ps. point_path \<gamma>\<rbrakk> \<Longrightarrow> one_chain_line_integral ?F ?basis (?one_chain - ?ps) = one_chain_line_integral ?F ?basis ?one_chain
common_sudiv_exists ?one_chain1.0 ?one_chain2.0 = (\<exists>ps1 ps2. common_boundary_sudivision_exists (?one_chain1.0 - ps1) (?one_chain2.0 - ps2) \<and> (\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>) \<and> (\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>))
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
finite one_chain1
finite one_chain2
finite basis
common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2)
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
\<lbrakk>\<forall>(k, \<gamma>)\<in>one_chain1 - ps1. line_integral_exists ?F ?basis \<gamma>; finite (one_chain1 - ps1); finite (one_chain2 - ps2); finite ?basis\<rbrakk> \<Longrightarrow> one_chain_line_integral ?F ?basis (one_chain1 - ps1) = one_chain_line_integral ?F ?basis (one_chain2 - ps2)

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "\<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
obtain subdiv where subdiv_props:
      "chain_subdiv_chain (one_chain1-ps1) subdiv"
      "chain_subdiv_chain (one_chain2-ps2) subdiv"
      "(\<forall>(k, \<gamma>) \<in> subdiv. valid_path \<gamma>)"
      "(boundary_chain subdiv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>subdiv. \<lbrakk>chain_subdiv_chain (one_chain1 - ps1) subdiv; chain_subdiv_chain (one_chain2 - ps2) subdiv; \<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>; boundary_chain subdiv\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using gen_subdiv(1)
[PROOF STATE]
proof (prove)
using this:
common_boundary_sudivision_exists (one_chain1 - ps1) (one_chain2 - ps2)

goal (1 subgoal):
 1. (\<And>subdiv. \<lbrakk>chain_subdiv_chain (one_chain1 - ps1) subdiv; chain_subdiv_chain (one_chain2 - ps2) subdiv; \<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>; boundary_chain subdiv\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: common_boundary_sudivision_exists_def)
[PROOF STATE]
proof (state)
this:
chain_subdiv_chain (one_chain1 - ps1) subdiv
chain_subdiv_chain (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
boundary_chain subdiv

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
have "\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
[PROOF STEP]
using one_chain_line_integral_eq_line_integral_on_sudivision'(2)[OF subdiv_props(1) boundary_chain_diff[OF assms(2)] subdiv_props(4)] assms(4) subdiv_props(3) assms(5) assms(7)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>(k, \<gamma>)\<in>one_chain1 - ps1. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>; finite (one_chain1 - ps1); finite ?basis\<rbrakk> \<Longrightarrow> \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists ?F ?basis \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
[PROOF STEP]
have i: "\<forall>(k, \<gamma>)\<in>one_chain2-ps2. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists F basis \<gamma>
[PROOF STEP]
using one_chain_line_integral_eq_line_integral_on_sudivision(2)[OF subdiv_props(2) boundary_chain_diff[OF assms(3)] subdiv_props(4)] subdiv_props(3) assms(6) assms(7)
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
\<lbrakk>\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>; finite (one_chain2 - ps2); finite ?basis\<rbrakk> \<Longrightarrow> \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists ?F ?basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain2
finite basis

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists F basis \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists F basis \<gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
using  gen_subdiv(3) line_integral_exists_point_path[OF assms(7)]
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
point_path ?\<gamma> \<Longrightarrow> line_integral_exists ?F basis ?\<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma common_sudiv_exists_refl:
      assumes "common_sudiv_exists C1 C2"
      shows "common_sudiv_exists C2 C1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. common_sudiv_exists C2 C1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
common_sudiv_exists C1 C2

goal (1 subgoal):
 1. common_sudiv_exists C2 C1
[PROOF STEP]
apply(simp add: common_sudiv_exists_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>subdiv ps1. chain_subdiv_chain (C1 - ps1) subdiv \<and> (\<exists>ps2. chain_subdiv_chain (C2 - ps2) subdiv \<and> (\<forall>x\<in>subdiv. case x of (k, x) \<Rightarrow> valid_path x) \<and> boundary_chain subdiv \<and> (\<forall>x\<in>ps1. case x of (k, x) \<Rightarrow> point_path x) \<and> (\<forall>x\<in>ps2. case x of (k, x) \<Rightarrow> point_path x)) \<Longrightarrow> \<exists>subdiv ps1. chain_subdiv_chain (C2 - ps1) subdiv \<and> (\<exists>ps2. chain_subdiv_chain (C1 - ps2) subdiv \<and> (\<forall>x\<in>subdiv. case x of (k, x) \<Rightarrow> valid_path x) \<and> boundary_chain subdiv \<and> (\<forall>x\<in>ps1. case x of (k, x) \<Rightarrow> point_path x) \<and> (\<forall>x\<in>ps2. case x of (k, x) \<Rightarrow> point_path x))
[PROOF STEP]
by auto


[STATEMENT]
lemma chain_subdiv_path_singleton:
  shows "chain_subdiv_path \<gamma> {(1,\<gamma>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain_subdiv_path \<gamma> {(1, \<gamma>)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. chain_subdiv_path \<gamma> {(1, \<gamma>)}
[PROOF STEP]
have "rec_join [(1,\<gamma>)] = \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_join [(1, \<gamma>)] = \<gamma>
[PROOF STEP]
by (simp add: joinpaths_def)
[PROOF STATE]
proof (state)
this:
rec_join [(1, \<gamma>)] = \<gamma>

goal (1 subgoal):
 1. chain_subdiv_path \<gamma> {(1, \<gamma>)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rec_join [(1, \<gamma>)] = \<gamma>
[PROOF STEP]
have "set [(1,\<gamma>)] = {(1, \<gamma>)}" "distinct [(1,\<gamma>)]" "rec_join [(1,\<gamma>)] = \<gamma>" "valid_chain_list [(1,\<gamma>)]"
[PROOF STATE]
proof (prove)
using this:
rec_join [(1, \<gamma>)] = \<gamma>

goal (1 subgoal):
 1. (set [(1::'a, \<gamma>)] = {(1::'a, \<gamma>)} &&& distinct [(1::'b, \<gamma>)]) &&& rec_join [(1, \<gamma>)] = \<gamma> &&& valid_chain_list [(1, \<gamma>)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set [(1::?'a, \<gamma>)] = {(1::?'a, \<gamma>)}
distinct [(1::?'b, \<gamma>)]
rec_join [(1, \<gamma>)] = \<gamma>
valid_chain_list [(1, \<gamma>)]

goal (1 subgoal):
 1. chain_subdiv_path \<gamma> {(1, \<gamma>)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set [(1::?'a, \<gamma>)] = {(1::?'a, \<gamma>)}
distinct [(1::?'b, \<gamma>)]
rec_join [(1, \<gamma>)] = \<gamma>
valid_chain_list [(1, \<gamma>)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set [(1::?'a, \<gamma>)] = {(1::?'a, \<gamma>)}
distinct [(1::?'b, \<gamma>)]
rec_join [(1, \<gamma>)] = \<gamma>
valid_chain_list [(1, \<gamma>)]

goal (1 subgoal):
 1. chain_subdiv_path \<gamma> {(1, \<gamma>)}
[PROOF STEP]
by (metis (no_types) chain_subdiv_path.intros)
[PROOF STATE]
proof (state)
this:
chain_subdiv_path \<gamma> {(1, \<gamma>)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_subdiv_path_singleton_reverse:
  shows "chain_subdiv_path (reversepath \<gamma>) {(-1,\<gamma>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>) {(- 1, \<gamma>)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>) {(- 1, \<gamma>)}
[PROOF STEP]
have "rec_join [(-1,\<gamma>)] = reversepath \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_join [(- 1, \<gamma>)] = reversepath \<gamma>
[PROOF STEP]
by (simp add: joinpaths_def)
[PROOF STATE]
proof (state)
this:
rec_join [(- 1, \<gamma>)] = reversepath \<gamma>

goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>) {(- 1, \<gamma>)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rec_join [(- 1, \<gamma>)] = reversepath \<gamma>
[PROOF STEP]
have "set [(-1,\<gamma>)] = {(- 1, \<gamma>)}" "distinct [(-1,\<gamma>)]"
             "rec_join [(-1,\<gamma>)] = reversepath \<gamma>" "valid_chain_list [(-1,\<gamma>)]"
[PROOF STATE]
proof (prove)
using this:
rec_join [(- 1, \<gamma>)] = reversepath \<gamma>

goal (1 subgoal):
 1. (set [(- (1::'a), \<gamma>)] = {(- (1::'a), \<gamma>)} &&& distinct [(- (1::'b), \<gamma>)]) &&& rec_join [(- 1, \<gamma>)] = reversepath \<gamma> &&& valid_chain_list [(- 1, \<gamma>)]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set [(- (1::?'a), \<gamma>)] = {(- (1::?'a), \<gamma>)}
distinct [(- (1::?'b), \<gamma>)]
rec_join [(- 1, \<gamma>)] = reversepath \<gamma>
valid_chain_list [(- 1, \<gamma>)]

goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>) {(- 1, \<gamma>)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set [(- (1::?'a), \<gamma>)] = {(- (1::?'a), \<gamma>)}
distinct [(- (1::?'b), \<gamma>)]
rec_join [(- 1, \<gamma>)] = reversepath \<gamma>
valid_chain_list [(- 1, \<gamma>)]
[PROOF STEP]
have "chain_subdiv_path (reversepath \<gamma>) (set [(- 1, \<gamma>)])"
[PROOF STATE]
proof (prove)
using this:
set [(- (1::?'a), \<gamma>)] = {(- (1::?'a), \<gamma>)}
distinct [(- (1::?'b), \<gamma>)]
rec_join [(- 1, \<gamma>)] = reversepath \<gamma>
valid_chain_list [(- 1, \<gamma>)]

goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>) (set [(- 1, \<gamma>)])
[PROOF STEP]
using chain_subdiv_path.intros
[PROOF STATE]
proof (prove)
using this:
set [(- (1::?'a), \<gamma>)] = {(- (1::?'a), \<gamma>)}
distinct [(- (1::?'b), \<gamma>)]
rec_join [(- 1, \<gamma>)] = reversepath \<gamma>
valid_chain_list [(- 1, \<gamma>)]
\<lbrakk>distinct ?l; rec_join ?l = ?\<gamma>; valid_chain_list ?l\<rbrakk> \<Longrightarrow> chain_subdiv_path ?\<gamma> (set ?l)

goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>) (set [(- 1, \<gamma>)])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
chain_subdiv_path (reversepath \<gamma>) (set [(- 1, \<gamma>)])

goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>) {(- 1, \<gamma>)}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
chain_subdiv_path (reversepath \<gamma>) (set [(- 1, \<gamma>)])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_path (reversepath \<gamma>) (set [(- 1, \<gamma>)])

goal (1 subgoal):
 1. chain_subdiv_path (reversepath \<gamma>) {(- 1, \<gamma>)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
chain_subdiv_path (reversepath \<gamma>) {(- 1, \<gamma>)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_subdiv_chain_refl:
  assumes "boundary_chain C"
  shows "chain_subdiv_chain C C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain_subdiv_chain C C
[PROOF STEP]
using chain_subdiv_path_singleton chain_subdiv_path_singleton_reverse assms
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_path ?\<gamma> {(1, ?\<gamma>)}
chain_subdiv_path (reversepath ?\<gamma>) {(- 1, ?\<gamma>)}
boundary_chain C

goal (1 subgoal):
 1. chain_subdiv_chain C C
[PROOF STEP]
unfolding chain_subdiv_chain_def boundary_chain_def pairwise_def
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_path ?\<gamma> {(1, ?\<gamma>)}
chain_subdiv_path (reversepath ?\<gamma>) {(- 1, ?\<gamma>)}
\<forall>(k, \<gamma>)\<in>C. k = 1 \<or> k = - 1

goal (1 subgoal):
 1. \<exists>f. \<Union> (f ` C) = C \<and> (\<forall>c\<in>C. chain_subdiv_path (coeff_cube_to_path c) (f c)) \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<noteq> y \<longrightarrow> f x \<inter> f y = {}) \<and> (\<forall>x\<in>C. finite (f x))
[PROOF STEP]
using case_prodI2 coeff_cube_to_path.simps
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_path ?\<gamma> {(1, ?\<gamma>)}
chain_subdiv_path (reversepath ?\<gamma>) {(- 1, ?\<gamma>)}
\<forall>(k, \<gamma>)\<in>C. k = 1 \<or> k = - 1
(\<And>a b. ?p = (a, b) \<Longrightarrow> ?c a b) \<Longrightarrow> case ?p of (a, b) \<Rightarrow> ?c a b
coeff_cube_to_path (?k, ?\<gamma>) = (if ?k = 1 then ?\<gamma> else reversepath ?\<gamma>)

goal (1 subgoal):
 1. \<exists>f. \<Union> (f ` C) = C \<and> (\<forall>c\<in>C. chain_subdiv_path (coeff_cube_to_path c) (f c)) \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<noteq> y \<longrightarrow> f x \<inter> f y = {}) \<and> (\<forall>x\<in>C. finite (f x))
[PROOF STEP]
by (rule_tac x="\<lambda>x. {x}" in exI) auto


[STATEMENT]
lemma reparam_weak_eq_refl:
  shows "reparam_weak \<gamma>1 \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reparam_weak \<gamma>1 \<gamma>1
[PROOF STEP]
unfolding reparam_weak_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>1 \<circ> \<phi>) x) \<and> \<phi> piecewise_C1_differentiable_on {0..1} \<and> \<phi> 0 = 0 \<and> \<phi> 1 = 1 \<and> \<phi> ` {0..1} = {0..1}
[PROOF STEP]
apply (rule_tac x="id" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>{0..1}. \<gamma>1 x = (\<gamma>1 \<circ> id) x) \<and> id piecewise_C1_differentiable_on {0..1} \<and> id 0 = 0 \<and> id 1 = 1 \<and> id ` {0..1} = {0..1}
[PROOF STEP]
by (auto simp add: id_def piecewise_C1_differentiable_on_def C1_differentiable_on_def continuous_on_id)


[STATEMENT]
lemma line_integral_exists_smooth_one_base:
  assumes "\<gamma> 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>) (\<lambda>x. F x \<bullet> b)"
  shows "line_integral_exists F {b} \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F {b} \<gamma>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral_exists F {b} \<gamma>
[PROOF STEP]
have gamma2_differentiable: "(\<forall>x \<in> {0 .. 1}. \<gamma> differentiable at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. \<gamma> differentiable at x
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<gamma> C1_differentiable_on {0..1}

goal (1 subgoal):
 1. \<forall>x\<in>{0..1}. \<gamma> 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> differentiable at x

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

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

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

goal (1 subgoal):
 1. (\<lambda>x. \<gamma> 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> x \<bullet> b) differentiable at x
?f differentiable at ?x \<Longrightarrow> ?f differentiable at ?x within ?s

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

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

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. \<gamma> x \<bullet> b)
[PROOF STEP]
using differentiable_imp_continuous_on
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<gamma> 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> x \<bullet> b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on {0..1} (\<lambda>x. \<gamma> x \<bullet> b)

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

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

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

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma> 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> x) \<bullet> b)

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

goal (1 subgoal):
 1. (\<And>D. (\<forall>x\<in>{0..1}. (\<gamma> 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> 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> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x\<in>{0..1}. (\<gamma> has_vector_derivative D x) (at x)) \<and> continuous_on {0..1} D
[PROOF STEP]
have *:"\<forall>x\<in>{0..1}. vector_derivative \<gamma> (at x within{0..1}) = D x"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>{0..1}. (\<gamma> 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> (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> 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> (at x within {0..1}) = D x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{0..1}. vector_derivative \<gamma> (at x within {0..1}) = D x

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

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

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (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> (at x within {0..1}))
[PROOF STEP]
have 1: "continuous_on {0..1} (\<lambda>x. (vector_derivative \<gamma> (at x within{0..1})) \<bullet> b)"
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma> (at x within {0..1}))

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. vector_derivative \<gamma> (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> (at x within {0..1}) \<bullet> b)

goal (1 subgoal):
 1. continuous_on {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (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> x) \<bullet> b * (vector_derivative \<gamma> (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> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))

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

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

goal (1 subgoal):
 1. (\<lambda>x. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
using integrable_continuous_real
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..1} (\<lambda>x. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b))
continuous_on {?a..?b} ?f \<Longrightarrow> ?f integrable_on {?a..?b}

goal (1 subgoal):
 1. (\<lambda>x. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. 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 {b} \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. F (\<gamma> x) \<bullet> b * (vector_derivative \<gamma> (at x within {0..1}) \<bullet> b)) integrable_on {0..1}
[PROOF STEP]
show "line_integral_exists F {b} \<gamma>"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. 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 {b} \<gamma>
[PROOF STEP]
by(auto simp add: line_integral_exists_def)
[PROOF STATE]
proof (state)
this:
line_integral_exists F {b} \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma contour_integral_primitive_lemma:
  fixes f :: "complex \<Rightarrow> complex" and g :: "real \<Rightarrow> complex"
  assumes "a \<le> b"
      and "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)"
      and "g piecewise_differentiable_on {a..b}"  "\<And>x. x \<in> {a..b} \<Longrightarrow> g x \<in> s"
    shows "((\<lambda>x. f'(g x) * vector_derivative g (at x within {a..b}))
             has_integral (f(g b) - f(g a))) {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f' (g x) * vector_derivative g (at x within {a..b})) has_integral f (g b) - f (g a)) {a..b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. f' (g x) * vector_derivative g (at x within {a..b})) has_integral f (g b) - f (g a)) {a..b}
[PROOF STEP]
obtain k where k: "finite k" "\<forall>x\<in>{a..b} - k. g differentiable (at x within {a..b})" and cg: "continuous_on {a..b} g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. \<lbrakk>finite k; \<forall>x\<in>{a..b} - k. g differentiable at x within {a..b}; continuous_on {a..b} g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<le> b
?x \<in> s \<Longrightarrow> (f has_field_derivative f' ?x) (at ?x within s)
g piecewise_differentiable_on {a..b}
?x \<in> {a..b} \<Longrightarrow> g ?x \<in> s

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. ((\<lambda>x. f' (g x) * vector_derivative g (at x within {a..b})) has_integral f (g b) - f (g a)) {a..b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f' (g x) * vector_derivative g (at x within {a..b})) has_integral f (g b) - f (g a)) {a..b}
[PROOF STEP]
apply (rule fundamental_theorem_of_calculus_interior_strong)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. finite ?S
 2. a \<le> b
 3. \<And>x. x \<in> {a<..<b} - ?S \<Longrightarrow> ((\<lambda>a. f (g a)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x)
 4. continuous_on {a..b} (\<lambda>a. f (g a))
[PROOF STEP]
using k assms cfg *
[PROOF STATE]
proof (prove)
using this:
finite k
\<forall>x\<in>{a..b} - k. g differentiable at x within {a..b}
a \<le> b
?x \<in> s \<Longrightarrow> (f has_field_derivative f' ?x) (at ?x within s)
g piecewise_differentiable_on {a..b}
?x \<in> {a..b} \<Longrightarrow> g ?x \<in> s
continuous_on {a..b} (\<lambda>x. f (g x))
\<lbrakk>a < ?x2; ?x2 < b; ?x2 \<notin> k\<rbrakk> \<Longrightarrow> ((\<lambda>x. f (g x)) has_vector_derivative f' (g ?x2) * vector_derivative g (at ?x2 within {a..b})) (at ?x2 within {a..b})

goal (4 subgoals):
 1. finite ?S
 2. a \<le> b
 3. \<And>x. x \<in> {a<..<b} - ?S \<Longrightarrow> ((\<lambda>a. f (g a)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x)
 4. continuous_on {a..b} (\<lambda>a. f (g a))
[PROOF STEP]
apply (auto simp: at_within_Icc_at)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f' (g x) * vector_derivative g (at x within {a..b})) has_integral f (g b) - f (g a)) {a..b}

goal:
No subgoals!
[PROOF STEP]
qed