[STATEMENT]
lemma chain_reparam_chain'_line_integral:
  assumes chain1_eq_chain2: "chain_reparam_chain' one_chain1 subdiv" and
    boundary_chain1: "boundary_chain one_chain1" and
    boundary_chain2: "boundary_chain subdiv" and
    line_integral_exists_on_chain2: "\<forall>b\<in>basis. \<forall>(k::int, \<gamma>) \<in> subdiv. line_integral_exists F {b} \<gamma>" and
    valid_path: "\<forall>(k, \<gamma>) \<in> subdiv. valid_path \<gamma>" and
    valid_path_2: "\<forall>(k, \<gamma>) \<in> one_chain1. valid_path \<gamma>" and
    finite_chain1: "finite one_chain1" and
    finite_basis: "finite basis" and
    cont_field: " \<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv"
    "\<forall>(k, \<gamma>) \<in> one_chain1. 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>one_chain1. 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>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
obtain f where f_props:
    "((\<Union>(f ` one_chain1)) = subdiv)"
    "(\<forall>cube \<in> one_chain1. chain_reparam_weak_path (rec_join [cube]) (f cube))"
    "(\<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>cube\<in>one_chain1. chain_reparam_weak_path (rec_join [cube]) (f cube); \<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
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' one_chain1 subdiv

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>\<Union> (f ` one_chain1) = subdiv; \<forall>cube\<in>one_chain1. chain_reparam_weak_path (rec_join [cube]) (f cube); \<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: chain_reparam_chain'_def)
[PROOF STATE]
proof (state)
this:
\<Union> (f ` one_chain1) = subdiv
\<forall>cube\<in>one_chain1. chain_reparam_weak_path (rec_join [cube]) (f cube)
\<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>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Union> (f ` one_chain1) = subdiv
\<forall>cube\<in>one_chain1. chain_reparam_weak_path (rec_join [cube]) (f cube)
\<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 STEP]
have 0: "one_chain_line_integral F basis subdiv = one_chain_line_integral F basis (\<Union>(f ` one_chain1))"
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
\<forall>cube\<in>one_chain1. chain_reparam_weak_path (rec_join [cube]) (f cube)
\<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 (1 subgoal):
 1. one_chain_line_integral F basis subdiv = one_chain_line_integral F basis (\<Union> (f ` one_chain1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis subdiv = one_chain_line_integral F basis (\<Union> (f ` one_chain1))

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis subdiv = one_chain_line_integral F basis (\<Union> (f ` one_chain1))

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
fix k \<gamma>
[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>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
assume ass:"(k, \<gamma>) \<in> one_chain1"
[PROOF STATE]
proof (state)
this:
(k, \<gamma>) \<in> one_chain1

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have "line_integral_exists F basis \<gamma> \<and>
               one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral 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> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral 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> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = 1
[PROOF STEP]
have i:"chain_reparam_weak_path \<gamma> (f(k,\<gamma>))"
[PROOF STATE]
proof (prove)
using this:
k = 1

goal (1 subgoal):
 1. chain_reparam_weak_path \<gamma> (f (k, \<gamma>))
[PROOF STEP]
using f_props(2) ass
[PROOF STATE]
proof (prove)
using this:
k = 1
\<forall>cube\<in>one_chain1. chain_reparam_weak_path (rec_join [cube]) (f cube)
(k, \<gamma>) \<in> one_chain1

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral 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
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
unfolding boundary_chain_def
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. k = 1 \<or> k = - 1
\<forall>(k, \<gamma>)\<in>subdiv. k = 1 \<or> k = - 1
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have iii:"\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F {b} \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F {b} \<gamma>
[PROOF STEP]
using f_props(1) ass assms
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral 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
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

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> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have v: "\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>f (k, \<gamma>). continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>f (k, \<gamma>). continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using f_props(1) ass assms
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. \<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>f (k, \<gamma>). continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>f (k, \<gamma>). continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have "line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
[PROOF STEP]
using chain_reparam_weak_path_line_integral[OF i ii iii iv finite_basis v] ass f_props(4)
[PROOF STATE]
proof (prove)
using this:
finite (f (k, \<gamma>)) \<Longrightarrow> line_integral F basis \<gamma> = one_chain_line_integral F basis (f (k, \<gamma>))
finite (f (k, \<gamma>)) \<Longrightarrow> line_integral_exists F basis \<gamma>
(k, \<gamma>) \<in> one_chain1
\<forall>x\<in>one_chain1. finite (f x)

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
[PROOF STEP]
show "line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
using k_eq_1
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
k = 1

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral 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> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral 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 ass boundary_chain1
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 1
(k, \<gamma>) \<in> one_chain1
boundary_chain one_chain1

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> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = - 1
[PROOF STEP]
have i:"chain_reparam_weak_path (reversepath \<gamma>) (f(k,\<gamma>))"
[PROOF STATE]
proof (prove)
using this:
k = - 1

goal (1 subgoal):
 1. chain_reparam_weak_path (reversepath \<gamma>) (f (k, \<gamma>))
[PROOF STEP]
using f_props(2) ass
[PROOF STATE]
proof (prove)
using this:
k = - 1
\<forall>cube\<in>one_chain1. chain_reparam_weak_path (rec_join [cube]) (f cube)
(k, \<gamma>) \<in> one_chain1

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral 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
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
unfolding boundary_chain_def
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. k = 1 \<or> k = - 1
\<forall>(k, \<gamma>)\<in>subdiv. k = 1 \<or> k = - 1
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have iii:"\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F {b} \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F {b} \<gamma>
[PROOF STEP]
using f_props(1) ass assms
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral 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
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

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> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have v: "\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>f (k, \<gamma>). continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>f (k, \<gamma>). continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using f_props(1) ass assms
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. \<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>f (k, \<gamma>). continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>f (k, \<gamma>). continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have x:"line_integral_exists F basis (reversepath \<gamma>) \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma>) \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)
[PROOF STEP]
using chain_reparam_weak_path_line_integral[OF i ii iii iv finite_basis v] ass f_props(4)
[PROOF STATE]
proof (prove)
using this:
finite (f (k, \<gamma>)) \<Longrightarrow> line_integral F basis (reversepath \<gamma>) = one_chain_line_integral F basis (f (k, \<gamma>))
finite (f (k, \<gamma>)) \<Longrightarrow> line_integral_exists F basis (reversepath \<gamma>)
(k, \<gamma>) \<in> one_chain1
\<forall>x\<in>one_chain1. finite (f x)

goal (1 subgoal):
 1. line_integral_exists F basis (reversepath \<gamma>) \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis (reversepath \<gamma>) \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have "valid_path (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (reversepath \<gamma>)
[PROOF STEP]
using f_props(1) ass assms
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
(k, \<gamma>) \<in> one_chain1
chain_reparam_chain' one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F {b} \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
finite one_chain1
finite basis
\<forall>b\<in>basis. \<forall>(k, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

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

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

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
[PROOF STEP]
using line_integral_on_reverse_path reversepath_reversepath x ass
[PROOF STATE]
proof (prove)
using this:
valid_path (reversepath \<gamma>)
\<lbrakk>valid_path ?\<gamma>; line_integral_exists ?F ?basis ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral ?F ?basis ?\<gamma> = - line_integral ?F ?basis (reversepath ?\<gamma>)
\<lbrakk>valid_path ?\<gamma>; line_integral_exists ?F ?basis ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis (reversepath ?\<gamma>)
reversepath (reversepath ?g) = ?g
line_integral_exists F basis (reversepath \<gamma>) \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)
(k, \<gamma>) \<in> one_chain1

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
[PROOF STEP]
show "line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k::int, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
using k_eq_neg1
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
k = - 1

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral_exists F basis \<gamma> \<and> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral 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>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?k2, ?\<gamma>2) \<in> one_chain1 \<Longrightarrow> line_integral_exists F basis ?\<gamma>2 \<and> one_chain_line_integral F basis (f (?k2, ?\<gamma>2)) = real_of_int ?k2 * line_integral F basis ?\<gamma>2

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
note cube_line_integ = this
[PROOF STATE]
proof (state)
this:
(?k2, ?\<gamma>2) \<in> one_chain1 \<Longrightarrow> line_integral_exists F basis ?\<gamma>2 \<and> one_chain_line_integral F basis (f (?k2, ?\<gamma>2)) = real_of_int ?k2 * line_integral F basis ?\<gamma>2

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain1. 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 auto
[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>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
show line_integral_exists_on_chain1: "\<forall>(k, \<gamma>) \<in> one_chain1. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using cube_line_integ
[PROOF STATE]
proof (prove)
using this:
(?k2, ?\<gamma>2) \<in> one_chain1 \<Longrightarrow> line_integral_exists F basis ?\<gamma>2 \<and> one_chain_line_integral F basis (f (?k2, ?\<gamma>2)) = real_of_int ?k2 * line_integral F basis ?\<gamma>2

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain1. 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]
have 1: "one_chain_line_integral F basis (\<Union>(f ` one_chain1)) = one_chain_line_integral F basis one_chain1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = one_chain_line_integral F basis one_chain1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = one_chain_line_integral F basis one_chain1
[PROOF STEP]
have 0:"one_chain_line_integral F basis (\<Union>(f ` one_chain1)) =
                           (\<Sum>one_chain \<in> (f ` one_chain1). one_chain_line_integral F basis one_chain)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
have finite: "\<forall>chain \<in> (f ` one_chain1). finite chain"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>chain\<in>f ` one_chain1. finite chain
[PROOF STEP]
using f_props(1) finite_chain2
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
finite subdiv

goal (1 subgoal):
 1. \<forall>chain\<in>f ` one_chain1. finite chain
[PROOF STEP]
by (meson Sup_upper finite_subset)
[PROOF STATE]
proof (state)
this:
\<forall>chain\<in>f ` one_chain1. finite chain

goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
have disj: " \<forall>A\<in>f ` one_chain1. \<forall>B\<in>f ` one_chain1. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>f ` one_chain1. \<forall>B\<in>f ` one_chain1. A \<noteq> B \<longrightarrow> A \<inter> B = {}
[PROOF STEP]
apply(simp add:image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A. (\<exists>x\<in>one_chain1. A = f x) \<longrightarrow> (\<forall>B. (\<exists>x\<in>one_chain1. B = f x) \<longrightarrow> A \<noteq> B \<longrightarrow> A \<inter> B = {})
[PROOF STEP]
using f_props(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}

goal (1 subgoal):
 1. \<forall>A. (\<exists>x\<in>one_chain1. A = f x) \<longrightarrow> (\<forall>B. (\<exists>x\<in>one_chain1. B = f x) \<longrightarrow> A \<noteq> B \<longrightarrow> A \<inter> B = {})
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>f ` one_chain1. \<forall>B\<in>f ` one_chain1. A \<noteq> B \<longrightarrow> A \<inter> B = {}

goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
show "one_chain_line_integral F basis (\<Union>(f ` one_chain1)) =
                                (\<Sum>one_chain \<in> (f ` one_chain1). one_chain_line_integral F basis one_chain)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
using Groups_Big.comm_monoid_add_class.sum.Union_disjoint[OF finite disj]
          one_chain_line_integral_def
[PROOF STATE]
proof (prove)
using this:
sum ?g (\<Union> (f ` one_chain1)) = (sum \<circ> sum) ?g (f ` one_chain1)
one_chain_line_integral ?F ?b ?C \<equiv> \<Sum>(k, g)\<in>?C. real_of_int k * line_integral ?F ?b g

goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = sum (one_chain_line_integral F basis) (f ` one_chain1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = sum (one_chain_line_integral F basis) (f ` one_chain1)

goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = one_chain_line_integral F basis one_chain1
[PROOF STEP]
have 1:"(\<Sum>one_chain \<in> (f ` one_chain1). one_chain_line_integral F basis one_chain) =
                            one_chain_line_integral F basis one_chain1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = one_chain_line_integral F basis one_chain1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = one_chain_line_integral F basis one_chain1
[PROOF STEP]
have "(\<Sum>one_chain \<in> (f ` one_chain1). one_chain_line_integral F basis one_chain) =
                                     (\<Sum>(k,\<gamma>)\<in>one_chain1. k*(line_integral F basis \<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
have i:"(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                       (\<Sum>(k,\<gamma>)\<in>one_chain1 - {p. f p = {}}. k*(line_integral F basis \<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
have "inj_on f (one_chain1 - {p. f p = {}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f (one_chain1 - {p. f p = {}})
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>one_chain1 - {p. f p = {}}. \<forall>y\<in>one_chain1 - {p. f p = {}}. f x = f y \<longrightarrow> x = y
[PROOF STEP]
using f_props(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}

goal (1 subgoal):
 1. \<forall>x\<in>one_chain1 - {p. f p = {}}. \<forall>y\<in>one_chain1 - {p. f p = {}}. f x = f y \<longrightarrow> x = y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
inj_on f (one_chain1 - {p. f p = {}})

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on f (one_chain1 - {p. f p = {}})
[PROOF STEP]
have 0: "(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain)
                                                       = (\<Sum>(k, \<gamma>) \<in> (one_chain1 - {p. f p = {}}). one_chain_line_integral F basis (f (k, \<gamma>)))"
[PROOF STATE]
proof (prove)
using this:
inj_on f (one_chain1 - {p. f p = {}})

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. one_chain_line_integral F basis (f (k, \<gamma>)))
[PROOF STEP]
using Groups_Big.comm_monoid_add_class.sum.reindex
[PROOF STATE]
proof (prove)
using this:
inj_on f (one_chain1 - {p. f p = {}})
inj_on ?h ?A \<Longrightarrow> sum ?g (?h ` ?A) = sum (?g \<circ> ?h) ?A

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. one_chain_line_integral F basis (f (k, \<gamma>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. one_chain_line_integral F basis (f (k, \<gamma>)))

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
have "\<And> k \<gamma>. (k, \<gamma>) \<in> (one_chain1 - {p. f p = {}}) \<Longrightarrow>
                                                     one_chain_line_integral F basis (f(k, \<gamma>)) = k* (line_integral F basis \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 - {p. f p = {}} \<Longrightarrow> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
using cube_line_integ
[PROOF STATE]
proof (prove)
using this:
(?k2, ?\<gamma>2) \<in> one_chain1 \<Longrightarrow> line_integral_exists F basis ?\<gamma>2 \<and> one_chain_line_integral F basis (f (?k2, ?\<gamma>2)) = real_of_int ?k2 * line_integral F basis ?\<gamma>2

goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 - {p. f p = {}} \<Longrightarrow> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(?k, ?\<gamma>) \<in> one_chain1 - {p. f p = {}} \<Longrightarrow> one_chain_line_integral F basis (f (?k, ?\<gamma>)) = real_of_int ?k * line_integral F basis ?\<gamma>

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?k, ?\<gamma>) \<in> one_chain1 - {p. f p = {}} \<Longrightarrow> one_chain_line_integral F basis (f (?k, ?\<gamma>)) = real_of_int ?k * line_integral F basis ?\<gamma>
[PROOF STEP]
have "(\<Sum>(k, \<gamma>) \<in> (one_chain1 - {p. f p = {}}). one_chain_line_integral F basis (f (k, \<gamma>)))
                   = (\<Sum>(k, \<gamma>) \<in> (one_chain1 - {p. f p = {}}). k* (line_integral F basis \<gamma>))"
[PROOF STATE]
proof (prove)
using this:
(?k, ?\<gamma>) \<in> one_chain1 - {p. f p = {}} \<Longrightarrow> one_chain_line_integral F basis (f (?k, ?\<gamma>)) = real_of_int ?k * line_integral F basis ?\<gamma>

goal (1 subgoal):
 1. (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. one_chain_line_integral F basis (f (k, \<gamma>))) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
by (auto intro!: Finite_Cartesian_Product.sum_cong_aux)
[PROOF STATE]
proof (state)
this:
(\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. one_chain_line_integral F basis (f (k, \<gamma>))) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. one_chain_line_integral F basis (f (k, \<gamma>))) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
show "(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                     (\<Sum>(k, \<gamma>) \<in> (one_chain1 - {p. f p = {}}). k* (line_integral F basis \<gamma>))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. one_chain_line_integral F basis (f (k, \<gamma>))) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
(\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. one_chain_line_integral F basis (f (k, \<gamma>))) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. one_chain_line_integral F basis (f (k, \<gamma>)))

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
have "\<And> (k::int) \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> (f (k, \<gamma>) = {}) \<Longrightarrow> (k, \<gamma>) \<in> {(k',\<gamma>'). k'* (line_integral F basis \<gamma>') = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> (k, \<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> (k, \<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}
[PROOF STEP]
fix k::"int"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> (k, \<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}
[PROOF STEP]
fix \<gamma>::"real\<Rightarrow>real*real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> (k, \<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}
[PROOF STEP]
assume ass:"(k, \<gamma>) \<in> one_chain1"
            "(f (k, \<gamma>) = {})"
[PROOF STATE]
proof (state)
this:
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}

goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> (k, \<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}
[PROOF STEP]
have zero_line_integral:"one_chain_line_integral F basis (f (k, \<gamma>)) = 0"
[PROOF STATE]
proof (prove)
using this:
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}

goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = 0
[PROOF STEP]
using one_chain_line_integral_def
[PROOF STATE]
proof (prove)
using this:
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}
one_chain_line_integral ?F ?b ?C \<equiv> \<Sum>(k, g)\<in>?C. real_of_int k * line_integral ?F ?b g

goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0

goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> (k, \<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}
[PROOF STEP]
show "(k, \<gamma>) \<in> {(k'::int, \<gamma>'). k' * line_integral F basis \<gamma>' = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k, \<gamma>) \<in> {(x, \<gamma>'). real_of_int x * line_integral F basis \<gamma>' = 0}
[PROOF STEP]
using zero_line_integral cube_line_integ ass
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0
(?k2, ?\<gamma>2) \<in> one_chain1 \<Longrightarrow> line_integral_exists F basis ?\<gamma>2 \<and> one_chain_line_integral F basis (f (?k2, ?\<gamma>2)) = real_of_int ?k2 * line_integral F basis ?\<gamma>2
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}

goal (1 subgoal):
 1. (k, \<gamma>) \<in> {(x, \<gamma>'). real_of_int x * line_integral F basis \<gamma>' = 0}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(k, \<gamma>) \<in> {(x, \<gamma>'). real_of_int x * line_integral F basis \<gamma>' = 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?k, ?\<gamma>) \<in> one_chain1; f (?k, ?\<gamma>) = {}\<rbrakk> \<Longrightarrow> (?k, ?\<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?k, ?\<gamma>) \<in> one_chain1; f (?k, ?\<gamma>) = {}\<rbrakk> \<Longrightarrow> (?k, ?\<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}
[PROOF STEP]
have ii:"(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                          (\<Sum>one_chain \<in> (f ` (one_chain1)). one_chain_line_integral F basis one_chain)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?k, ?\<gamma>) \<in> one_chain1; f (?k, ?\<gamma>) = {}\<rbrakk> \<Longrightarrow> (?k, ?\<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> (k, \<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}) \<Longrightarrow> sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
have "\<And>one_chain. one_chain \<in> (f ` (one_chain1)) - (f ` (one_chain1 - {p. f p = {}})) \<Longrightarrow>
                                                         one_chain_line_integral F basis one_chain = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>one_chain. one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}}) \<Longrightarrow> one_chain_line_integral F basis one_chain = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>one_chain. one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}}) \<Longrightarrow> one_chain_line_integral F basis one_chain = 0
[PROOF STEP]
fix one_chain
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>one_chain. one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}}) \<Longrightarrow> one_chain_line_integral F basis one_chain = 0
[PROOF STEP]
assume "one_chain \<in> (f ` (one_chain1)) - (f ` (one_chain1 - {p. f p = {}}))"
[PROOF STATE]
proof (state)
this:
one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})

goal (1 subgoal):
 1. \<And>one_chain. one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}}) \<Longrightarrow> one_chain_line_integral F basis one_chain = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})
[PROOF STEP]
have "one_chain = {}"
[PROOF STATE]
proof (prove)
using this:
one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})

goal (1 subgoal):
 1. one_chain = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain = {}

goal (1 subgoal):
 1. \<And>one_chain. one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}}) \<Longrightarrow> one_chain_line_integral F basis one_chain = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_chain = {}
[PROOF STEP]
show "one_chain_line_integral F basis one_chain = 0"
[PROOF STATE]
proof (prove)
using this:
one_chain = {}

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain = 0
[PROOF STEP]
by (auto simp add: one_chain_line_integral_def)
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis one_chain = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}}) \<Longrightarrow> one_chain_line_integral F basis ?one_chain = 0

goal (1 subgoal):
 1. (\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> (k, \<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}) \<Longrightarrow> sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}}) \<Longrightarrow> one_chain_line_integral F basis ?one_chain = 0
[PROOF STEP]
have 0:"(\<Sum>one_chain \<in> f ` (one_chain1) - (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain)
                                                       = 0"
[PROOF STATE]
proof (prove)
using this:
?one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}}) \<Longrightarrow> one_chain_line_integral F basis ?one_chain = 0

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})) = 0
[PROOF STEP]
using Groups_Big.comm_monoid_add_class.sum.neutral
[PROOF STATE]
proof (prove)
using this:
?one_chain \<in> f ` one_chain1 - f ` (one_chain1 - {p. f p = {}}) \<Longrightarrow> one_chain_line_integral F basis ?one_chain = 0
\<forall>x\<in>?A. ?g x = (0::?'a) \<Longrightarrow> sum ?g ?A = (0::?'a)

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})) = 0

goal (1 subgoal):
 1. (\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> (k, \<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}) \<Longrightarrow> sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum (one_chain_line_integral F basis) (f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})) = 0
[PROOF STEP]
have "(\<Sum>one_chain \<in> f ` (one_chain1). one_chain_line_integral F basis one_chain)
                                                      - (\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain)
                                                       = 0"
[PROOF STATE]
proof (prove)
using this:
sum (one_chain_line_integral F basis) (f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})) = 0

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) - sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})) = 0 \<Longrightarrow> sum (one_chain_line_integral F basis) (f ` one_chain1) - sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = 0
[PROOF STEP]
have finte: "finite (f ` one_chain1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (f ` one_chain1)
[PROOF STEP]
using finite_chain1
[PROOF STATE]
proof (prove)
using this:
finite one_chain1

goal (1 subgoal):
 1. finite (f ` one_chain1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (f ` one_chain1)

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})) = 0 \<Longrightarrow> sum (one_chain_line_integral F basis) (f ` one_chain1) - sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) - sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = 0
[PROOF STEP]
using Groups_Big.sum_diff[OF finte, of " (f ` (one_chain1 - {p. f p = {}}))"
                  "one_chain_line_integral F basis"]
                0
[PROOF STATE]
proof (prove)
using this:
f ` (one_chain1 - {p. f p = {}}) \<subseteq> f ` one_chain1 \<Longrightarrow> sum (one_chain_line_integral F basis) (f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})) = sum (one_chain_line_integral F basis) (f ` one_chain1) - sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}}))
sum (one_chain_line_integral F basis) (f ` one_chain1 - f ` (one_chain1 - {p. f p = {}})) = 0

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) - sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` one_chain1) - sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` one_chain1) - sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = 0

goal (1 subgoal):
 1. (\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> (k, \<gamma>) \<in> {(k', \<gamma>'). real_of_int k' * line_integral F basis \<gamma>' = 0}) \<Longrightarrow> sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum (one_chain_line_integral F basis) (f ` one_chain1) - sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = 0
[PROOF STEP]
show "(\<Sum>one_chain \<in> (f ` (one_chain1 - {p. f p = {}})). one_chain_line_integral F basis one_chain) =
                                                          (\<Sum>one_chain \<in> (f ` (one_chain1)). one_chain_line_integral F basis one_chain)"
[PROOF STATE]
proof (prove)
using this:
sum (one_chain_line_integral F basis) (f ` one_chain1) - sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = 0

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = sum (one_chain_line_integral F basis) (f ` one_chain1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = sum (one_chain_line_integral F basis) (f ` one_chain1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = sum (one_chain_line_integral F basis) (f ` one_chain1)

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
have "\<And> (k::int) \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> (f (k, \<gamma>) = {}) \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}
[PROOF STEP]
fix k::"int"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}
[PROOF STEP]
fix \<gamma>::"real\<Rightarrow>real*real"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}
[PROOF STEP]
assume ass:"(k, \<gamma>) \<in> one_chain1"  "(f (k, \<gamma>) = {})"
[PROOF STATE]
proof (state)
this:
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}

goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}
[PROOF STEP]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = 0"
[PROOF STATE]
proof (prove)
using this:
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}

goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = 0
[PROOF STEP]
using one_chain_line_integral_def
[PROOF STATE]
proof (prove)
using this:
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}
one_chain_line_integral ?F ?b ?C \<equiv> \<Sum>(k, g)\<in>?C. real_of_int k * line_integral ?F ?b g

goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0

goal (1 subgoal):
 1. \<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0
[PROOF STEP]
show "f (k, \<gamma>) \<in> {p'. (one_chain_line_integral F basis p' = 0)}"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0

goal (1 subgoal):
 1. f (k, \<gamma>) \<in> {p'. one_chain_line_integral F basis p' = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (k, \<gamma>) \<in> {p'. one_chain_line_integral F basis p' = 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?k, ?\<gamma>) \<in> one_chain1; f (?k, ?\<gamma>) = {}\<rbrakk> \<Longrightarrow> f (?k, ?\<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?k, ?\<gamma>) \<in> one_chain1; f (?k, ?\<gamma>) = {}\<rbrakk> \<Longrightarrow> f (?k, ?\<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}
[PROOF STEP]
have iii:"(\<Sum>(k::int,\<gamma>)\<in>one_chain1 - {p. f p = {}}. k*(line_integral F basis \<gamma>))
                                                 = (\<Sum>(k::int,\<gamma>)\<in>one_chain1. k*(line_integral F basis \<gamma>))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?k, ?\<gamma>) \<in> one_chain1; f (?k, ?\<gamma>) = {}\<rbrakk> \<Longrightarrow> f (?k, ?\<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}

goal (1 subgoal):
 1. (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}) \<Longrightarrow> (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
have "\<And> k \<gamma>. (k,\<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}})
                                                    \<Longrightarrow> k* (line_integral F basis \<gamma>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}}) \<Longrightarrow> real_of_int k * line_integral F basis \<gamma> = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}}) \<Longrightarrow> real_of_int k * line_integral F basis \<gamma> = 0
[PROOF STEP]
fix k \<gamma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}}) \<Longrightarrow> real_of_int k * line_integral F basis \<gamma> = 0
[PROOF STEP]
assume ass: "(k,\<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}})"
[PROOF STATE]
proof (state)
this:
(k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}})

goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}}) \<Longrightarrow> real_of_int k * line_integral F basis \<gamma> = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}})
[PROOF STEP]
have "f(k, \<gamma>) = {}"
[PROOF STATE]
proof (prove)
using this:
(k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}})

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

goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}}) \<Longrightarrow> real_of_int k * line_integral F basis \<gamma> = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f (k, \<gamma>) = {}
[PROOF STEP]
have "one_chain_line_integral F basis (f(k, \<gamma>)) = 0"
[PROOF STATE]
proof (prove)
using this:
f (k, \<gamma>) = {}

goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = 0
[PROOF STEP]
by (auto simp add: one_chain_line_integral_def)
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0

goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}}) \<Longrightarrow> real_of_int k * line_integral F basis \<gamma> = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0
[PROOF STEP]
have zero_line_integral:"one_chain_line_integral F basis (f (k, \<gamma>)) = 0"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0

goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = 0
[PROOF STEP]
using one_chain_line_integral_def
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0
one_chain_line_integral ?F ?b ?C \<equiv> \<Sum>(k, g)\<in>?C. real_of_int k * line_integral ?F ?b g

goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0

goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}}) \<Longrightarrow> real_of_int k * line_integral F basis \<gamma> = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0
[PROOF STEP]
show "k* (line_integral F basis \<gamma>) = 0"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0

goal (1 subgoal):
 1. real_of_int k * line_integral F basis \<gamma> = 0
[PROOF STEP]
using zero_line_integral cube_line_integ ass
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = 0
one_chain_line_integral F basis (f (k, \<gamma>)) = 0
(?k2, ?\<gamma>2) \<in> one_chain1 \<Longrightarrow> line_integral_exists F basis ?\<gamma>2 \<and> one_chain_line_integral F basis (f (?k2, ?\<gamma>2)) = real_of_int ?k2 * line_integral F basis ?\<gamma>2
(k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}})

goal (1 subgoal):
 1. real_of_int k * line_integral F basis \<gamma> = 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
real_of_int k * line_integral F basis \<gamma> = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?k, ?\<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}}) \<Longrightarrow> real_of_int ?k * line_integral F basis ?\<gamma> = 0

goal (1 subgoal):
 1. (\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}) \<Longrightarrow> (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?k, ?\<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}}) \<Longrightarrow> real_of_int ?k * line_integral F basis ?\<gamma> = 0
[PROOF STEP]
have "\<forall>(k::int,\<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}).
                       k* (line_integral F basis \<gamma>) = 0"
[PROOF STATE]
proof (prove)
using this:
(?k, ?\<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}}) \<Longrightarrow> real_of_int ?k * line_integral F basis ?\<gamma> = 0

goal (1 subgoal):
 1. \<forall>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma> = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma> = 0

goal (1 subgoal):
 1. (\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}) \<Longrightarrow> (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma> = 0
[PROOF STEP]
have "(\<Sum>(k::int,\<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). k*(line_integral F basis \<gamma>)) = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma> = 0

goal (1 subgoal):
 1. (\<Sum>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma>) = 0
[PROOF STEP]
using Groups_Big.comm_monoid_add_class.sum.neutral
              [of "one_chain1 - (one_chain1 - {p. f p = {}})" "(\<lambda>(k::int,\<gamma>). k* (line_integral F basis \<gamma>))"]
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma> = 0
\<forall>x\<in>one_chain1 - (one_chain1 - {p. f p = {}}). (case x of (x, \<gamma>) \<Rightarrow> real_of_int x * line_integral F basis \<gamma>) = 0 \<Longrightarrow> (\<Sum>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma>) = 0

goal (1 subgoal):
 1. (\<Sum>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma>) = 0
[PROOF STEP]
by (simp add: split_beta)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma>) = 0

goal (1 subgoal):
 1. (\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}) \<Longrightarrow> (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma>) = 0
[PROOF STEP]
have "(\<Sum>(k::int,\<gamma>)\<in>one_chain1. k*(line_integral F basis \<gamma>)) -
                                                    (\<Sum>(k::int,\<gamma>)\<in> (one_chain1 - {p. f p = {}}). k*(line_integral F basis \<gamma>))  = 0"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma>) = 0

goal (1 subgoal):
 1. (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>) - (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = 0
[PROOF STEP]
using Groups_Big.sum_diff[OF finite_chain1]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>(x, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). real_of_int x * line_integral F basis \<gamma>) = 0
?B \<subseteq> one_chain1 \<Longrightarrow> sum ?f (one_chain1 - ?B) = sum ?f one_chain1 - sum ?f ?B

goal (1 subgoal):
 1. (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>) - (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = 0
[PROOF STEP]
by (metis (no_types) Diff_subset \<open>(\<Sum>(k, \<gamma>)\<in>one_chain1 - (one_chain1 - {p. f p = {}}). k * line_integral F basis \<gamma>) = 0\<close> \<open>\<And>f B. B \<subseteq> one_chain1 \<Longrightarrow> sum f (one_chain1 - B) = sum f one_chain1 - sum f B\<close>)
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>) - (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = 0

goal (1 subgoal):
 1. (\<And>k \<gamma>. \<lbrakk>(k, \<gamma>) \<in> one_chain1; f (k, \<gamma>) = {}\<rbrakk> \<Longrightarrow> f (k, \<gamma>) \<in> {chain. one_chain_line_integral F basis chain = 0}) \<Longrightarrow> (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>) - (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>) - (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = 0

goal (1 subgoal):
 1. (\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
using i ii iii
[PROOF STATE]
proof (prove)
using this:
sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = (\<Sum>(k, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int k * line_integral F basis \<gamma>)
sum (one_chain_line_integral F basis) (f ` (one_chain1 - {p. f p = {}})) = sum (one_chain_line_integral F basis) (f ` one_chain1)
(\<Sum>(x, \<gamma>)\<in>one_chain1 - {p. f p = {}}. real_of_int x * line_integral F basis \<gamma>) = (\<Sum>(x, \<gamma>)\<in>one_chain1. real_of_int x * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = one_chain_line_integral F basis one_chain1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)

goal (1 subgoal):
 1. sum (one_chain_line_integral F basis) (f ` one_chain1) = one_chain_line_integral F basis one_chain1
[PROOF STEP]
using one_chain_line_integral_def
[PROOF STATE]
proof (prove)
using this:
sum (one_chain_line_integral F basis) (f ` one_chain1) = (\<Sum>(k, \<gamma>)\<in>one_chain1. real_of_int k * line_integral F basis \<gamma>)
one_chain_line_integral ?F ?b ?C \<equiv> \<Sum>(k, g)\<in>?C. real_of_int k * line_integral ?F ?b g

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (one_chain_line_integral F basis) (f ` one_chain1) = one_chain_line_integral F basis one_chain1

goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = one_chain_line_integral F basis one_chain1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = one_chain_line_integral F basis one_chain1
[PROOF STEP]
using 0 1
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = sum (one_chain_line_integral F basis) (f ` one_chain1)
sum (one_chain_line_integral F basis) (f ` one_chain1) = one_chain_line_integral F basis one_chain1

goal (1 subgoal):
 1. one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = one_chain_line_integral F basis one_chain1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = one_chain_line_integral F basis one_chain1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = one_chain_line_integral F basis one_chain1

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
[PROOF STEP]
show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
[PROOF STEP]
using 0 1
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis subdiv = one_chain_line_integral F basis (\<Union> (f ` one_chain1))
one_chain_line_integral F basis (\<Union> (f ` one_chain1)) = one_chain_line_integral F basis one_chain1

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 chain_reparam_chain'_line_integral_smooth_cubes:
  assumes "chain_reparam_chain' one_chain1 one_chain2"
    "\<forall>(k2,\<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}"
    "\<forall>b\<in>basis.\<forall>(k2,\<gamma>2)\<in>one_chain2. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    "finite basis"
    "finite one_chain1"
    "boundary_chain one_chain1"
    "boundary_chain one_chain2"
    "\<forall>(k,\<gamma>)\<in>one_chain1. valid_path \<gamma>"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain1. 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_chain1. 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_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
{
[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_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
fix b
[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_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
assume "b \<in> basis"
[PROOF STATE]
proof (state)
this:
b \<in> basis

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_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
fix k \<gamma>
[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_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
assume "(k, \<gamma>)\<in>one_chain2"
[PROOF STATE]
proof (state)
this:
(k, \<gamma>) \<in> one_chain2

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_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have "line_integral_exists F {b} \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F {b} \<gamma>
[PROOF STEP]
apply(rule line_integral_exists_smooth)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<gamma> C1_differentiable_on {0..1}
 2. \<forall>b\<in>{b}. continuous_on (path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
 3. finite {b}
[PROOF STEP]
using \<open>(k, \<gamma>) \<in> one_chain2\<close> assms(2)
[PROOF STATE]
proof (prove)
using this:
(k, \<gamma>) \<in> one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}

goal (3 subgoals):
 1. \<gamma> C1_differentiable_on {0..1}
 2. \<forall>b\<in>{b}. continuous_on (path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
 3. finite {b}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>b\<in>{b}. continuous_on (path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
 2. finite {b}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
\<forall>b\<in>basis. \<forall>(k2, \<gamma>2)\<in>one_chain2. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
finite one_chain1
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>

goal (2 subgoals):
 1. \<forall>b\<in>{b}. continuous_on (path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
 2. finite {b}
[PROOF STEP]
using \<open>(k, \<gamma>) \<in> one_chain2\<close> \<open>b \<in> basis\<close>
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
\<forall>b\<in>basis. \<forall>(k2, \<gamma>2)\<in>one_chain2. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
finite one_chain1
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
(k, \<gamma>) \<in> one_chain2
b \<in> basis

goal (2 subgoals):
 1. \<forall>b\<in>{b}. continuous_on (path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
 2. finite {b}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {b}
[PROOF STEP]
using \<open>b \<in> basis\<close>
[PROOF STATE]
proof (prove)
using this:
b \<in> basis

goal (1 subgoal):
 1. finite {b}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
line_integral_exists F {b} \<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_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?b2 \<in> basis; (?k2, ?\<gamma>2) \<in> one_chain2\<rbrakk> \<Longrightarrow> line_integral_exists F {?b2} ?\<gamma>2

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_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?b2 \<in> basis; (?k2, ?\<gamma>2) \<in> one_chain2\<rbrakk> \<Longrightarrow> line_integral_exists F {?b2} ?\<gamma>2
[PROOF STEP]
have a: "\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F {b} \<gamma>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?b2 \<in> basis; (?k2, ?\<gamma>2) \<in> one_chain2\<rbrakk> \<Longrightarrow> line_integral_exists F {?b2} ?\<gamma>2

goal (1 subgoal):
 1. \<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F {b} \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. \<forall>(k, \<gamma>)\<in>one_chain2. line_integral_exists F {b} \<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_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have b: "\<forall>(k2,\<gamma>2)\<in>one_chain2. valid_path \<gamma>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k2, \<gamma>2)\<in>one_chain2. valid_path \<gamma>2
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}

goal (1 subgoal):
 1. \<forall>(k2, \<gamma>2)\<in>one_chain2. valid_path \<gamma>2
[PROOF STEP]
by (simp add: C1_differentiable_imp_piecewise case_prod_beta valid_path_def)
[PROOF STATE]
proof (state)
this:
\<forall>(k2, \<gamma>2)\<in>one_chain2. valid_path \<gamma>2

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_chain1. 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]
by (rule chain_reparam_chain'_line_integral[OF assms(1) assms(6) assms(7) a b assms(8) assms(5) assms(4) assms(3)])
[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_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
by (rule chain_reparam_chain'_line_integral[OF assms(1) assms(6) assms(7) a b assms(8) assms(5) assms(4) assms(3)])
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_subdiv_path_pathimg_subset:
  assumes "chain_subdiv_path \<gamma> subdiv"
  shows "\<forall>(k',\<gamma>')\<in>subdiv. (path_image \<gamma>') \<subseteq> path_image \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k', \<gamma>')\<in>subdiv. path_image \<gamma>' \<subseteq> path_image \<gamma>
[PROOF STEP]
using assms chain_subdiv_path.simps path_image_rec_join
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_path \<gamma> subdiv
chain_subdiv_path ?a1.0 ?a2.0 = (\<exists>l \<gamma>. ?a1.0 = \<gamma> \<and> ?a2.0 = set l \<and> distinct l \<and> rec_join l = \<gamma> \<and> valid_chain_list l)
\<lbrakk>(?k, ?\<gamma>) \<in> set ?l; valid_chain_list ?l\<rbrakk> \<Longrightarrow> path_image ?\<gamma> \<subseteq> path_image (rec_join ?l)

goal (1 subgoal):
 1. \<forall>(k', \<gamma>')\<in>subdiv. path_image \<gamma>' \<subseteq> path_image \<gamma>
[PROOF STEP]
by(auto simp add: chain_subdiv_path.simps)


[STATEMENT]
lemma reparam_path_image:
  assumes "reparam \<gamma>1 \<gamma>2"
  shows "path_image \<gamma>1 = path_image \<gamma>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_image \<gamma>1 = path_image \<gamma>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reparam \<gamma>1 \<gamma>2

goal (1 subgoal):
 1. path_image \<gamma>1 = path_image \<gamma>2
[PROOF STEP]
apply (auto simp add: reparam_def path_image_def image_def bij_betw_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<phi> xa. \<lbrakk>\<forall>x\<in>{0..1}. \<gamma>1 x = \<gamma>2 (\<phi> x); \<phi> piecewise_C1_differentiable_on {0..1}; \<phi> 0 = 0; \<phi> 1 = 1; inj_on \<phi> {0..1}; {y. \<exists>x\<in>{0..1}. y = \<phi> x} = {0..1}; \<phi> -` {0..1} \<subseteq> {0..1}; \<forall>x\<in>{0..1}. finite (\<phi> -` {x}); 0 \<le> xa; xa \<le> 1\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..1}. \<gamma>2 xa = \<gamma>2 (\<phi> x)
[PROOF STEP]
apply (force dest!: equalityD2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma chain_reparam_weak_path_pathimg_subset:
  assumes "chain_reparam_weak_path \<gamma> subdiv"
  shows "\<forall>(k',\<gamma>')\<in>subdiv. (path_image \<gamma>') \<subseteq> path_image \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k', \<gamma>')\<in>subdiv. path_image \<gamma>' \<subseteq> path_image \<gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_weak_path \<gamma> subdiv

goal (1 subgoal):
 1. \<forall>(k', \<gamma>')\<in>subdiv. path_image \<gamma>' \<subseteq> path_image \<gamma>
[PROOF STEP]
apply(auto simp add: chain_reparam_weak_path_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba l. \<lbrakk>(a, b) \<in> set l; (aa, ba) \<in> path_image b; subdiv = set l; distinct l; reparam \<gamma> (rec_join l); valid_chain_list l; l \<noteq> []\<rbrakk> \<Longrightarrow> (aa, ba) \<in> path_image \<gamma>
[PROOF STEP]
using path_image_rec_join reparam_path_image
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?k, ?\<gamma>) \<in> set ?l; valid_chain_list ?l\<rbrakk> \<Longrightarrow> path_image ?\<gamma> \<subseteq> path_image (rec_join ?l)
reparam ?\<gamma>1.0 ?\<gamma>2.0 \<Longrightarrow> path_image ?\<gamma>1.0 = path_image ?\<gamma>2.0

goal (1 subgoal):
 1. \<And>a b aa ba l. \<lbrakk>(a, b) \<in> set l; (aa, ba) \<in> path_image b; subdiv = set l; distinct l; reparam \<gamma> (rec_join l); valid_chain_list l; l \<noteq> []\<rbrakk> \<Longrightarrow> (aa, ba) \<in> path_image \<gamma>
[PROOF STEP]
by blast


[STATEMENT]
lemma chain_subdiv_chain_pathimg_subset':
  assumes "chain_subdiv_chain one_chain subdiv"
  assumes "(k,\<gamma>)\<in> subdiv"
  shows " \<exists>k' \<gamma>'. (k',\<gamma>')\<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_chain one_chain subdiv
(k, \<gamma>) \<in> subdiv

goal (1 subgoal):
 1. \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
unfolding chain_subdiv_chain_def  pairwise_def
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<Union> (f ` one_chain) = subdiv \<and> (\<forall>c\<in>one_chain. chain_subdiv_path (coeff_cube_to_path c) (f c)) \<and> (\<forall>x\<in>one_chain. \<forall>y\<in>one_chain. x \<noteq> y \<longrightarrow> f x \<inter> f y = {}) \<and> (\<forall>x\<in>one_chain. finite (f x))
(k, \<gamma>) \<in> subdiv

goal (1 subgoal):
 1. \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f a b. \<lbrakk>subdiv = \<Union> (f ` one_chain); (a, b) \<in> one_chain; (k, \<gamma>) \<in> f (a, b); \<forall>c\<in>one_chain. chain_subdiv_path (coeff_cube_to_path c) (f c); \<forall>x\<in>one_chain. \<forall>y\<in>one_chain. x \<noteq> y \<longrightarrow> f x \<inter> f y = {}; \<forall>x\<in>one_chain. finite (f x)\<rbrakk> \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
by (metis chain_subdiv_path.cases coeff_cube_to_path.simps path_image_rec_join path_image_reversepath)


[STATEMENT]
lemma chain_subdiv_chain_pathimg_subset:
  assumes "chain_subdiv_chain one_chain subdiv"
  shows "\<Union> (path_image ` {\<gamma>. \<exists>k. (k,\<gamma>)\<in> subdiv}) \<subseteq> \<Union> (path_image ` {\<gamma>. \<exists>k. (k,\<gamma>)\<in> one_chain})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (path_image ` {\<gamma>. \<exists>k. (k, \<gamma>) \<in> subdiv}) \<subseteq> \<Union> (path_image ` {\<gamma>. \<exists>k. (k, \<gamma>) \<in> one_chain})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
chain_subdiv_chain one_chain subdiv

goal (1 subgoal):
 1. \<Union> (path_image ` {\<gamma>. \<exists>k. (k, \<gamma>) \<in> subdiv}) \<subseteq> \<Union> (path_image ` {\<gamma>. \<exists>k. (k, \<gamma>) \<in> one_chain})
[PROOF STEP]
unfolding chain_subdiv_chain_def pairwise_def
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<Union> (f ` one_chain) = subdiv \<and> (\<forall>c\<in>one_chain. chain_subdiv_path (coeff_cube_to_path c) (f c)) \<and> (\<forall>x\<in>one_chain. \<forall>y\<in>one_chain. x \<noteq> y \<longrightarrow> f x \<inter> f y = {}) \<and> (\<forall>x\<in>one_chain. finite (f x))

goal (1 subgoal):
 1. \<Union> (path_image ` {\<gamma>. \<exists>k. (k, \<gamma>) \<in> subdiv}) \<subseteq> \<Union> (path_image ` {\<gamma>. \<exists>k. (k, \<gamma>) \<in> one_chain})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x f k aa ba. \<lbrakk>(a, b) \<in> path_image x; subdiv = \<Union> (f ` one_chain); (aa, ba) \<in> one_chain; (k, x) \<in> f (aa, ba); \<forall>c\<in>one_chain. chain_subdiv_path (coeff_cube_to_path c) (f c); \<forall>x\<in>one_chain. \<forall>y\<in>one_chain. x \<noteq> y \<longrightarrow> f x \<inter> f y = {}; \<forall>x\<in>one_chain. finite (f x)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>k. (k, x) \<in> one_chain) \<and> (a, b) \<in> path_image x
[PROOF STEP]
by (metis UN_iff assms chain_subdiv_chain_pathimg_subset' subsetCE case_prodI2)