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

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

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Union> (f ` one_chain1) = subdiv
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}
\<forall>x\<in>one_chain1. finite (f x)
[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>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
\<forall>p\<in>one_chain1. \<forall>p'\<in>one_chain1. p \<noteq> p' \<longrightarrow> f p \<inter> f p' = {}
\<forall>x\<in>one_chain1. finite (f x)

goal (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]
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]
apply (simp add: image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite one_chain1; \<Union> {y. \<exists>x\<in>one_chain1. y = f x} = subdiv; \<forall>x\<in>one_chain1. finite (f x)\<rbrakk> \<Longrightarrow> finite subdiv
[PROOF STEP]
using f_props(1)
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv

goal (1 subgoal):
 1. \<lbrakk>finite one_chain1; \<Union> {y. \<exists>x\<in>one_chain1. y = f x} = subdiv; \<forall>x\<in>one_chain1. finite (f x)\<rbrakk> \<Longrightarrow> 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]
have "\<And> k \<gamma>. (k,\<gamma>) \<in> one_chain1\<Longrightarrow> line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
fix k \<gamma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> 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 (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> one_chain1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
show "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof (cases "k = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
assume k_eq_1: "k = 1"
[PROOF STATE]
proof (state)
this:
k = 1

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

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

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

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

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have iii:"\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<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_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis

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

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

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

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

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

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

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

goal (1 subgoal):
 1. k = - 1
[PROOF STEP]
using 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>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = - 1
[PROOF STEP]
have i:"chain_subdiv_path (reversepath \<gamma>) (f(k,\<gamma>))"
[PROOF STATE]
proof (prove)
using this:
k = - 1

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

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

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

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists F basis \<gamma>
[PROOF STEP]
have iii:"\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<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_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis

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

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

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

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

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> line_integral_exists 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 line_integral_on_path_eq_line_integral_on_equiv_chain(3)[OF i ii iii iv finite_basis]
[PROOF STATE]
proof (prove)
using this:
valid_path (reversepath \<gamma>)

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>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
valid_path (reversepath \<gamma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_path (reversepath \<gamma>)

goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using line_integral_on_reverse_path(2) reversepath_reversepath x
[PROOF STATE]
proof (prove)
using this:
valid_path (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>)

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

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

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

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

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]
by (metis (no_types, opaque_lifting) f_props(3) image_iff)
[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 blast
[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]
proof-
[PROOF STATE]
proof (state)
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]
fix k \<gamma>
[PROOF STATE]
proof (state)
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]
assume ass: "(k, \<gamma>) \<in> (one_chain1 - {p. f p = {}})"
[PROOF STATE]
proof (state)
this:
(k, \<gamma>) \<in> one_chain1 - {p. f p = {}}

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]
have bchain: "boundary_chain (f(k,\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
using f_props(1) boundary_chain2 ass
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
boundary_chain subdiv
(k, \<gamma>) \<in> one_chain1 - {p. f p = {}}

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

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]
have wexist: "\<forall>(k, \<gamma>)\<in>(f(k,\<gamma>)). line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
[PROOF STEP]
using f_props(1) line_integral_exists_on_chain2 ass
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
(k, \<gamma>) \<in> one_chain1 - {p. f p = {}}

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

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]
have vpath: " \<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) assms ass
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis
(k, \<gamma>) \<in> one_chain1 - {p. f p = {}}

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. \<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]
show "one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> 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> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
[PROOF STEP]
using f_props(2) k_eq_1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
k = 1
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> one_chain_line_integral ?F ?basis ?one_chain = line_integral ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> valid_path ?\<gamma>
boundary_chain (f (k, \<gamma>))
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). valid_path \<gamma>
(k, \<gamma>) \<in> one_chain1 - {p. f p = {}}
finite basis

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>

goal (1 subgoal):
 1. 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
k = 1

goal (1 subgoal):
 1. 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:
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> 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> 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> 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 - {p. f p = {}}
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> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)
[PROOF STEP]
using f_props(2) k_eq_neg1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
k = - 1
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> one_chain_line_integral ?F ?basis ?one_chain = line_integral ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> valid_path ?\<gamma>
boundary_chain (f (k, \<gamma>))
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). valid_path \<gamma>
(k, \<gamma>) \<in> one_chain1 - {p. f p = {}}
finite basis

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)
[PROOF STEP]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = - (line_integral F basis \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)

goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
[PROOF STEP]
using line_integral_on_reverse_path(1) ass line_integral_exists_on_chain1
                  valid_subdiv_imp_valid_one_chain[OF chain1_eq_chain2 boundary_chain1 boundary_chain2 valid_path]
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (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>)
(k, \<gamma>) \<in> one_chain1 - {p. f p = {}}
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>

goal (1 subgoal):
 1. 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
k = - 1

goal (1 subgoal):
 1. 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:
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:
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:
(?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>::"one_cube"
[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]
have bchain: "boundary_chain (f(k,\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
using f_props(1) boundary_chain2 ass
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
boundary_chain subdiv
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}

goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
by (auto simp add: boundary_chain_def)
[PROOF STATE]
proof (state)
this:
boundary_chain (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]
have wexist: "\<forall>(k, \<gamma>)\<in>(f(k,\<gamma>)). line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
[PROOF STEP]
using f_props(1) line_integral_exists_on_chain2 ass
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<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]
have vpath: " \<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) assms ass
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}

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

goal (1 subgoal):
 1. \<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]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> 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> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
[PROOF STEP]
using f_props(2) k_eq_1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
k = 1
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> one_chain_line_integral ?F ?basis ?one_chain = line_integral ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> valid_path ?\<gamma>
boundary_chain (f (k, \<gamma>))
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). valid_path \<gamma>
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}
finite basis

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>

goal (1 subgoal):
 1. 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
k = 1

goal (1 subgoal):
 1. 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:
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> 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> 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> 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
f (k, \<gamma>) = {}
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> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)
[PROOF STEP]
using f_props(2) k_eq_neg1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
k = - 1
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> one_chain_line_integral ?F ?basis ?one_chain = line_integral ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> valid_path ?\<gamma>
boundary_chain (f (k, \<gamma>))
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). valid_path \<gamma>
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}
finite basis

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)
[PROOF STEP]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = - (line_integral F basis \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)

goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
[PROOF STEP]
using line_integral_on_reverse_path(1)  ass line_integral_exists_on_chain1
                valid_subdiv_imp_valid_one_chain[OF chain1_eq_chain2 boundary_chain1 boundary_chain2 valid_path]
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (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>)
(k, \<gamma>) \<in> one_chain1
f (k, \<gamma>) = {}
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis (f (k::int, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>

goal (1 subgoal):
 1. 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
k = - 1

goal (1 subgoal):
 1. 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:
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:
one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<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:
one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
show "(k, \<gamma>) \<in> {(k'::int, \<gamma>'). k' * line_integral F basis \<gamma>' = 0}"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>

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
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
one_chain_line_integral F basis (f (k, \<gamma>)) = 0

goal (1 subgoal):
 1. (k, \<gamma>) \<in> {(x, \<gamma>'). real_of_int x * line_integral F basis \<gamma>' = 0}
[PROOF STEP]
by auto
[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]
show "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 = {}})

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 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>::"one_cube"
[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]
have bchain: "boundary_chain (f(k,\<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
using f_props(1) boundary_chain2 ass
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
boundary_chain subdiv
(k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}})

goal (1 subgoal):
 1. boundary_chain (f (k, \<gamma>))
[PROOF STEP]
by (auto simp add: boundary_chain_def)
[PROOF STATE]
proof (state)
this:
boundary_chain (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]
have wexist: "\<forall>(k, \<gamma>)\<in>(f(k,\<gamma>)). line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
[PROOF STEP]
using f_props(1) line_integral_exists_on_chain2 ass
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
(k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}})

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<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]
have vpath: " \<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) assms ass
[PROOF STATE]
proof (prove)
using this:
\<Union> (f ` one_chain1) = subdiv
chain_subdiv_chain one_chain1 subdiv
boundary_chain one_chain1
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>subdiv. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
finite one_chain1
finite basis
(k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}})

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. \<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]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> 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> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
[PROOF STEP]
using f_props(2) k_eq_1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
k = 1
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> one_chain_line_integral ?F ?basis ?one_chain = line_integral ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> valid_path ?\<gamma>
boundary_chain (f (k, \<gamma>))
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). valid_path \<gamma>
(k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}})
finite basis

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

goal (2 subgoals):
 1. k = 1 \<Longrightarrow> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
 2. k \<noteq> 1 \<Longrightarrow> 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>

goal (1 subgoal):
 1. 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis \<gamma>
k = 1

goal (1 subgoal):
 1. 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:
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> 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> 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> 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 - (one_chain1 - {p. f p = {}})
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> one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[PROOF STEP]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)
[PROOF STEP]
using f_props(2) k_eq_neg1 line_integral_on_path_eq_line_integral_on_equiv_chain bchain wexist vpath ass finite_basis
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1. if k = 1 then chain_subdiv_path \<gamma> (f (k, \<gamma>)) else chain_subdiv_path (reversepath \<gamma>) (f (k, \<gamma>))
k = - 1
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> one_chain_line_integral ?F ?basis ?one_chain = line_integral ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis ?\<gamma>
\<lbrakk>chain_subdiv_path ?\<gamma> ?one_chain; boundary_chain ?one_chain; \<forall>(k, \<gamma>)\<in>?one_chain. line_integral_exists ?F ?basis \<gamma>; \<forall>(k, \<gamma>)\<in>?one_chain. valid_path \<gamma>; finite ?basis\<rbrakk> \<Longrightarrow> valid_path ?\<gamma>
boundary_chain (f (k, \<gamma>))
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>f (k, \<gamma>). valid_path \<gamma>
(k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}})
finite basis

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)
[PROOF STEP]
have "one_chain_line_integral F basis (f (k, \<gamma>)) = - (line_integral F basis \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (reversepath \<gamma>)

goal (1 subgoal):
 1. one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
[PROOF STEP]
using line_integral_on_reverse_path(1)  ass line_integral_exists_on_chain1
                  valid_subdiv_imp_valid_one_chain[OF chain1_eq_chain2 boundary_chain1 boundary_chain2 valid_path]
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = line_integral F basis (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>)
(k, \<gamma>) \<in> one_chain1 - (one_chain1 - {p. f p = {}})
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>

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

goal (1 subgoal):
 1. k \<noteq> 1 \<Longrightarrow> 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis (f (k, \<gamma>)) = k * line_integral F basis \<gamma>"
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>

goal (1 subgoal):
 1. 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:
one_chain_line_integral F basis (f (k, \<gamma>)) = - line_integral F basis \<gamma>
k = - 1

goal (1 subgoal):
 1. 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:
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:
one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<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:
one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
[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>)) = real_of_int k * line_integral F basis \<gamma>

goal (1 subgoal):
 1. real_of_int k * line_integral F basis \<gamma> = 0
[PROOF STEP]
using zero_line_integral
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (f (k, \<gamma>)) = real_of_int k * line_integral F basis \<gamma>
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]
by auto
[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