[STATEMENT]
lemma line_integral_sum_basis:
  assumes "finite (basis::('a::euclidean_space) set)"  "\<forall>b\<in>basis. line_integral_exists F {b} \<gamma>"
  shows "line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)"
        "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>) &&& line_integral_exists F basis \<gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite basis
\<forall>b\<in>basis. line_integral_exists F {b} \<gamma>

goal (1 subgoal):
 1. line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>) &&& line_integral_exists F basis \<gamma>
[PROOF STEP]
proof(induction basis)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>b\<in>{}. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F {} \<gamma> = (\<Sum>b\<in>{}. line_integral F {b} \<gamma>)
 2. \<forall>b\<in>{}. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F {} \<gamma>
 3. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 4. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
show "line_integral F {} \<gamma> = (\<Sum>b\<in>{}. line_integral F {b} \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F {} \<gamma> = (\<Sum>b\<in>{}. line_integral F {b} \<gamma>)
[PROOF STEP]
by(auto simp add: line_integral_def)
[PROOF STATE]
proof (state)
this:
line_integral F {} \<gamma> = (\<Sum>b\<in>{}. line_integral F {b} \<gamma>)

goal (3 subgoals):
 1. \<forall>b\<in>{}. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F {} \<gamma>
 2. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 3. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
show "\<forall>b\<in>{}. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F {} \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>{}. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F {} \<gamma>
[PROOF STEP]
by(simp add: line_integral_exists_def integrable_0)
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>{}. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F {} \<gamma>

goal (2 subgoals):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 2. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 2. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
fix basis::"('a::euclidean_space) set"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 2. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
fix x::"'a::euclidean_space"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 2. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
fix  \<gamma>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 2. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
assume ind_hyp: "(\<forall>b\<in>basis. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F basis \<gamma>)"
    "(\<forall>b\<in>basis. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>))"
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F basis \<gamma>
\<forall>b\<in>basis. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)

goal (2 subgoals):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 2. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
assume step: "finite basis"
    "x \<notin> basis"
    "\<forall>b\<in>insert x basis. line_integral_exists F {b} \<gamma>"
[PROOF STATE]
proof (state)
this:
finite basis
x \<notin> basis
\<forall>b\<in>insert x basis. line_integral_exists F {b} \<gamma>

goal (2 subgoals):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 2. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite basis
x \<notin> basis
\<forall>b\<in>insert x basis. line_integral_exists F {b} \<gamma>
[PROOF STEP]
have 0: "line_integral_exists F {x} \<gamma>"
[PROOF STATE]
proof (prove)
using this:
finite basis
x \<notin> basis
\<forall>b\<in>insert x basis. line_integral_exists F {b} \<gamma>

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

goal (2 subgoals):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 2. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
have 1:"line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using ind_hyp step
[PROOF STATE]
proof (prove)
using this:
\<forall>b\<in>basis. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F basis \<gamma>
\<forall>b\<in>basis. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)
finite basis
x \<notin> basis
\<forall>b\<in>insert x basis. line_integral_exists F {b} \<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 (2 subgoals):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
 2. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists F (insert x Fa) \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
line_integral_exists F basis \<gamma>
[PROOF STEP]
show "line_integral_exists F (insert x basis) \<gamma>"
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. line_integral_exists F (insert x basis) \<gamma>
[PROOF STEP]
using step(1) step(2) line_integral_sum_gen(2)[OF _ 0 1]
[PROOF STATE]
proof (prove)
using this:
line_integral_exists F basis \<gamma>
finite basis
x \<notin> basis
\<lbrakk>finite ?basis; {x} \<union> basis = ?basis; {x} \<inter> basis = {}\<rbrakk> \<Longrightarrow> line_integral_exists F ?basis \<gamma>

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

goal (1 subgoal):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
[PROOF STEP]
have 3: "finite (insert x basis)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (insert x basis)
[PROOF STEP]
using step(1)
[PROOF STATE]
proof (prove)
using this:
finite basis

goal (1 subgoal):
 1. finite (insert x basis)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (insert x basis)

goal (1 subgoal):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
[PROOF STEP]
have "line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)
[PROOF STEP]
using ind_hyp step
[PROOF STATE]
proof (prove)
using this:
\<forall>b\<in>basis. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F basis \<gamma>
\<forall>b\<in>basis. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)
finite basis
x \<notin> basis
\<forall>b\<in>insert x basis. line_integral_exists F {b} \<gamma>

goal (1 subgoal):
 1. line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)

goal (1 subgoal):
 1. \<And>x Fa. \<lbrakk>finite Fa; x \<notin> Fa; \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral F Fa \<gamma> = (\<Sum>b\<in>Fa. line_integral F {b} \<gamma>); \<forall>b\<in>Fa. line_integral_exists F {b} \<gamma> \<Longrightarrow> line_integral_exists F Fa \<gamma>; \<forall>b\<in>insert x Fa. line_integral_exists F {b} \<gamma>\<rbrakk> \<Longrightarrow> line_integral F (insert x Fa) \<gamma> = (\<Sum>b\<in>insert x Fa. line_integral F {b} \<gamma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)
[PROOF STEP]
show "line_integral F (insert x basis) \<gamma> = (\<Sum>b\<in>insert x basis. line_integral F {b} \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)

goal (1 subgoal):
 1. line_integral F (insert x basis) \<gamma> = (\<Sum>b\<in>insert x basis. line_integral F {b} \<gamma>)
[PROOF STEP]
using step(1) step(2) line_integral_sum_gen(1)[OF 3 0 1]
[PROOF STATE]
proof (prove)
using this:
line_integral F basis \<gamma> = (\<Sum>b\<in>basis. line_integral F {b} \<gamma>)
finite basis
x \<notin> basis
\<lbrakk>{x} \<union> basis = insert x basis; {x} \<inter> basis = {}\<rbrakk> \<Longrightarrow> line_integral F (insert x basis) \<gamma> = line_integral F {x} \<gamma> + line_integral F basis \<gamma>

goal (1 subgoal):
 1. line_integral F (insert x basis) \<gamma> = (\<Sum>b\<in>insert x basis. line_integral F {b} \<gamma>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
line_integral F (insert x basis) \<gamma> = (\<Sum>b\<in>insert x basis. line_integral F {b} \<gamma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reparam_weak_eq_line_integrals_basis:
  assumes "reparam_weak \<gamma>1 \<gamma>2"
    "\<gamma>2 C1_differentiable_on {0..1}" (*To generalise this to valid_path we need a version of has_integral_substitution_strong that allows finite discontinuities*)
    "\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    "finite basis"
  shows "line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2"
    "line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2 &&& line_integral_exists F basis \<gamma>1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2
 2. line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>1
[PROOF STEP]
using reparam_weak_eq_line_integrals(2)[OF assms(1) assms(2)] assms(3-4) line_integral_sum_basis(2)[OF assms(4)]
[PROOF STATE]
proof (prove)
using this:
continuous_on (path_image \<gamma>2) (\<lambda>x. ?F x \<bullet> ?b) \<Longrightarrow> line_integral_exists ?F {?b} \<gamma>1
\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
\<forall>b\<in>basis. line_integral_exists ?F {b} ?\<gamma> \<Longrightarrow> line_integral_exists ?F basis ?\<gamma>

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

goal (1 subgoal):
 1. line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2
[PROOF STEP]
show "line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2
[PROOF STEP]
using reparam_weak_eq_line_integrals[OF assms(1) assms(2)] assms(3-4) line_integral_sum_basis(1)[OF assms(4)]
      line_integral_exists_smooth_one_base[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
continuous_on (path_image \<gamma>2) (\<lambda>x. ?F x \<bullet> ?b) \<Longrightarrow> line_integral ?F {?b} \<gamma>1 = line_integral ?F {?b} \<gamma>2
continuous_on (path_image \<gamma>2) (\<lambda>x. ?F x \<bullet> ?b) \<Longrightarrow> line_integral_exists ?F {?b} \<gamma>1
\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
\<forall>b\<in>basis. line_integral_exists ?F {b} ?\<gamma> \<Longrightarrow> line_integral ?F basis ?\<gamma> = (\<Sum>b\<in>basis. line_integral ?F {b} ?\<gamma>)
continuous_on (path_image \<gamma>2) (\<lambda>x. ?F x \<bullet> ?b) \<Longrightarrow> line_integral_exists ?F {?b} \<gamma>2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reparam_eq_line_integrals_basis:
  assumes "reparam \<gamma>1 \<gamma>2"
    "\<gamma>2 piecewise_C1_differentiable_on {0..1}"
    "\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    "finite basis"
    "\<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2" (*We need to remove this and work on special cases like conservative fields and field/line combinations that satisfy the improper integrals theorem assumptions*)
  shows "line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2"
    "line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2 &&& line_integral_exists F basis \<gamma>1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2
 2. line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>1
[PROOF STEP]
using reparam_eq_line_integrals(2)[OF assms(1) assms(2)] assms(3-5) line_integral_sum_basis(2)[OF assms(4)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_on (path_image \<gamma>2) (\<lambda>x. ?F x \<bullet> ?b); line_integral_exists ?F {?b} \<gamma>2\<rbrakk> \<Longrightarrow> line_integral_exists ?F {?b} \<gamma>1
\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
\<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2
\<forall>b\<in>basis. line_integral_exists ?F {b} ?\<gamma> \<Longrightarrow> line_integral_exists ?F basis ?\<gamma>

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

goal (1 subgoal):
 1. line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2
[PROOF STEP]
show "line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis \<gamma>1 = line_integral F basis \<gamma>2
[PROOF STEP]
using reparam_eq_line_integrals[OF assms(1) assms(2)] assms(3-5) line_integral_sum_basis(1)[OF assms(4)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_on (path_image \<gamma>2) (\<lambda>x. ?F x \<bullet> ?b); line_integral_exists ?F {?b} \<gamma>2\<rbrakk> \<Longrightarrow> line_integral ?F {?b} \<gamma>1 = line_integral ?F {?b} \<gamma>2
\<lbrakk>continuous_on (path_image \<gamma>2) (\<lambda>x. ?F x \<bullet> ?b); line_integral_exists ?F {?b} \<gamma>2\<rbrakk> \<Longrightarrow> line_integral_exists ?F {?b} \<gamma>1
\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
\<forall>b\<in>basis. line_integral_exists F {b} \<gamma>2
\<forall>b\<in>basis. line_integral_exists ?F {b} ?\<gamma> \<Longrightarrow> line_integral ?F basis ?\<gamma> = (\<Sum>b\<in>basis. line_integral ?F {b} ?\<gamma>)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma line_integral_exists_smooth:
  assumes "\<gamma> C1_differentiable_on {0..1}" (*To generalise this to valid_path we need a version of has_integral_substitution_strong that allows finite discontinuities*)
    "\<forall>(b::'a::euclidean_space) \<in>basis. continuous_on (path_image \<gamma>) (\<lambda>x. F x \<bullet> b)"
    "finite basis"
  shows "line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using reparam_weak_eq_line_integrals_basis(2)[OF reparam_weak_eq_refl[where ?\<gamma>1.0 = \<gamma>]] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<gamma> C1_differentiable_on {0..1}; \<forall>b\<in>?basis. continuous_on (path_image \<gamma>) (\<lambda>x. ?F x \<bullet> b); finite ?basis\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis \<gamma>
\<gamma> C1_differentiable_on {0..1}
\<forall>b\<in>basis. continuous_on (path_image \<gamma>) (\<lambda>x. F x \<bullet> b)
finite basis

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


[STATEMENT]
lemma smooth_path_imp_reverse:
  assumes "g C1_differentiable_on {0..1}"
  shows "(reversepath g) C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reversepath g C1_differentiable_on {0..1}
[PROOF STEP]
using assms continuous_on_const
[PROOF STATE]
proof (prove)
using this:
g C1_differentiable_on {0..1}
continuous_on ?s (\<lambda>x. ?c)

goal (1 subgoal):
 1. reversepath g C1_differentiable_on {0..1}
[PROOF STEP]
apply (auto simp: reversepath_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g C1_differentiable_on {0..1} \<Longrightarrow> (\<lambda>x. g (1 - x)) C1_differentiable_on {0..1}
[PROOF STEP]
apply (rule C1_differentiable_compose [of "\<lambda>x::real. 1-x" _ g, unfolded o_def])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. g C1_differentiable_on {0..1} \<Longrightarrow> (-) 1 C1_differentiable_on {0..1}
 2. g C1_differentiable_on {0..1} \<Longrightarrow> g C1_differentiable_on (-) 1 ` {0..1}
 3. \<And>x. g C1_differentiable_on {0..1} \<Longrightarrow> finite ({0..1} \<inter> (-) 1 -` {x})
[PROOF STEP]
apply (auto simp: C1_differentiable_on_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>{0..1}. g differentiable at x; continuous_on {0..1} (\<lambda>x. vector_derivative g (at x))\<rbrakk> \<Longrightarrow> finite ({0..1} \<inter> (-) 1 -` {x})
[PROOF STEP]
apply (simp add: finite_vimageI inj_on_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma piecewise_smooth_path_imp_reverse:
  assumes "g piecewise_C1_differentiable_on {0..1}"
  shows "(reversepath g) piecewise_C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reversepath g piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
using assms valid_path_reversepath
[PROOF STATE]
proof (prove)
using this:
g piecewise_C1_differentiable_on {0..1}
valid_path (reversepath ?g) = valid_path ?g

goal (1 subgoal):
 1. reversepath g piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
using valid_path_def
[PROOF STATE]
proof (prove)
using this:
g piecewise_C1_differentiable_on {0..1}
valid_path (reversepath ?g) = valid_path ?g
valid_path ?f \<equiv> ?f piecewise_C1_differentiable_on {0..1}

goal (1 subgoal):
 1. reversepath g piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
by blast


[STATEMENT]
lemma chain_reparam_weak_chain_line_integral:
  assumes "chain_reparam_weak_chain one_chain1 one_chain2"
    "\<forall>(k2,\<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}"
    "\<forall>(k2,\<gamma>2)\<in>one_chain2.\<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    "finite basis"
  and bound1: "boundary_chain one_chain1"
  and bound2: "boundary_chain one_chain2"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2 &&& \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
obtain f where f: "bij f"
    "(\<forall>(k,\<gamma>)\<in>one_chain1. if k = fst (f(k,\<gamma>)) then reparam_weak \<gamma> (snd (f(k,\<gamma>))) else reparam_weak \<gamma> (reversepath (snd (f(k,\<gamma>)))))"
    "f ` one_chain1 = one_chain2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>bij f; \<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam_weak \<gamma> (snd (f (k, \<gamma>))) else reparam_weak \<gamma> (reversepath (snd (f (k, \<gamma>)))); f ` one_chain1 = one_chain2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
chain_reparam_weak_chain one_chain1 one_chain2

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>bij f; \<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam_weak \<gamma> (snd (f (k, \<gamma>))) else reparam_weak \<gamma> (reversepath (snd (f (k, \<gamma>)))); f ` one_chain1 = one_chain2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: chain_reparam_weak_chain_def)
[PROOF STATE]
proof (state)
this:
bij f
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam_weak \<gamma> (snd (f (k, \<gamma>))) else reparam_weak \<gamma> (reversepath (snd (f (k, \<gamma>))))
f ` one_chain1 = one_chain2

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have 0:" \<forall>x\<in>one_chain1. (case x of (k, \<gamma>) \<Rightarrow> (real_of_int k * line_integral F basis \<gamma>) = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and>
                                                        line_integral_exists F basis \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>one_chain1. case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
fix k1 \<gamma>1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
assume ass1: "(k1,\<gamma>1) \<in>one_chain1"
[PROOF STATE]
proof (state)
this:
(k1, \<gamma>1) \<in> one_chain1

goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
have "real_of_int k1 * line_integral F basis \<gamma>1 = (case (f (k1,\<gamma>1)) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and>
                      line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume ass2: "k1 = 1"
[PROOF STATE]
proof (state)
this:
k1 = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
let ?k2 = "fst (f (k1, \<gamma>1))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
let ?\<gamma>2 = "snd (f (k1, \<gamma>1))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2\<and>
                              line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume ass3: "?k2 = 1"
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) = 1
[PROOF STEP]
have 0: "reparam_weak \<gamma>1 ?\<gamma>2"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = 1

goal (1 subgoal):
 1. reparam_weak \<gamma>1 (snd (f (k1, \<gamma>1)))
[PROOF STEP]
using ass1 ass2 f(2)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = 1
(k1, \<gamma>1) \<in> one_chain1
k1 = 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam_weak \<gamma> (snd (f (k, \<gamma>))) else reparam_weak \<gamma> (reversepath (snd (f (k, \<gamma>))))

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 1: "?\<gamma>2 C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (f (k1, \<gamma>1)) C1_differentiable_on {0..1}
[PROOF STEP]
using f(3) assms(2) ass1
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
(k1, \<gamma>1) \<in> one_chain1

goal (1 subgoal):
 1. snd (f (k1, \<gamma>1)) C1_differentiable_on {0..1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
snd (f (k1, \<gamma>1)) C1_differentiable_on {0..1}

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 2: "\<forall>b\<in>basis. continuous_on (path_image ?\<gamma>2) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (snd (f (k1, \<gamma>1)))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using f(3) assms(3) ass1
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
(k1, \<gamma>1) \<in> one_chain1

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                                     line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
using assms reparam_weak_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3
[PROOF STATE]
proof (prove)
using this:
chain_reparam_weak_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2
line_integral F basis \<gamma>1 = line_integral F basis (snd (f (k1, \<gamma>1)))
line_integral_exists F basis \<gamma>1
k1 = 1
fst (f (k1, \<gamma>1)) = 1

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

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume "?k2 \<noteq> 1"
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) \<noteq> 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) \<noteq> 1
[PROOF STEP]
have ass3: "?k2 = -1"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
using bound2 ass1 f(3)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1
boundary_chain one_chain2
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
unfolding boundary_chain_def
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1
\<forall>(k, \<gamma>)\<in>one_chain2. k = 1 \<or> k = - 1
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) = - 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
have 0: "reparam_weak \<gamma>1 (reversepath ?\<gamma>2)"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = - 1

goal (1 subgoal):
 1. reparam_weak \<gamma>1 (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using ass1 ass2 f(2)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = - 1
(k1, \<gamma>1) \<in> one_chain1
k1 = 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam_weak \<gamma> (snd (f (k, \<gamma>))) else reparam_weak \<gamma> (reversepath (snd (f (k, \<gamma>))))

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

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 1: "(reversepath ?\<gamma>2) C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reversepath (snd (f (k1, \<gamma>1))) C1_differentiable_on {0..1}
[PROOF STEP]
using f(3) assms(2) ass1 smooth_path_imp_reverse
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
(k1, \<gamma>1) \<in> one_chain1
?g C1_differentiable_on {0..1} \<Longrightarrow> reversepath ?g C1_differentiable_on {0..1}

goal (1 subgoal):
 1. reversepath (snd (f (k1, \<gamma>1))) C1_differentiable_on {0..1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
reversepath (snd (f (k1, \<gamma>1))) C1_differentiable_on {0..1}

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 2: "\<forall>b\<in>basis. continuous_on (path_image (reversepath ?\<gamma>2)) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (reversepath (snd (f (k1, \<gamma>1))))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using f(3) assms(3) ass1 path_image_reversepath
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
(k1, \<gamma>1) \<in> one_chain1
path_image (reversepath ?g) = path_image ?g

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

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 3: "line_integral F basis ?\<gamma>2 = - line_integral F basis (reversepath ?\<gamma>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
have i:"valid_path (reversepath ?\<gamma>2) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using 1 C1_differentiable_imp_piecewise
[PROOF STATE]
proof (prove)
using this:
reversepath (snd (f (k1, \<gamma>1))) C1_differentiable_on {0..1}
?f C1_differentiable_on ?S \<Longrightarrow> ?f piecewise_C1_differentiable_on ?S

goal (1 subgoal):
 1. valid_path (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
by (auto simp add: valid_path_def)
[PROOF STATE]
proof (state)
this:
valid_path (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using line_integral_on_reverse_path(1)[OF i line_integral_exists_smooth[OF 1 2 ]] assms
[PROOF STATE]
proof (prove)
using this:
finite basis \<Longrightarrow> line_integral F basis (reversepath (snd (f (k1, \<gamma>1)))) = - line_integral F basis (reversepath (reversepath (snd (f (k1, \<gamma>1)))))
chain_reparam_weak_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                                     line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
using assms reparam_weak_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3 3
[PROOF STATE]
proof (prove)
using this:
chain_reparam_weak_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2
line_integral F basis \<gamma>1 = line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
line_integral_exists F basis \<gamma>1
k1 = 1
fst (f (k1, \<gamma>1)) = - 1
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and>
                                   line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
using this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
by (simp add: case_prod_beta')
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume "k1 \<noteq> 1"
[PROOF STATE]
proof (state)
this:
k1 \<noteq> 1

goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k1 \<noteq> 1
[PROOF STEP]
have ass2: "k1 = -1"
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> 1

goal (1 subgoal):
 1. k1 = - 1
[PROOF STEP]
using bound1 ass1 f(3)
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> 1
boundary_chain one_chain1
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. k1 = - 1
[PROOF STEP]
unfolding boundary_chain_def
[PROOF STATE]
proof (prove)
using this:
k1 \<noteq> 1
\<forall>(k, \<gamma>)\<in>one_chain1. k = 1 \<or> k = - 1
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. k1 = - 1
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
k1 = - 1

goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
let ?k2 = "fst (f (k1, \<gamma>1))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
let ?\<gamma>2 = "snd (f (k1, \<gamma>1))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                              line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume ass3: "?k2 = 1"
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) = 1
[PROOF STEP]
have 0: "reparam_weak \<gamma>1 (reversepath ?\<gamma>2)"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = 1

goal (1 subgoal):
 1. reparam_weak \<gamma>1 (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using ass1 ass2 f(2)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = 1
(k1, \<gamma>1) \<in> one_chain1
k1 = - 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam_weak \<gamma> (snd (f (k, \<gamma>))) else reparam_weak \<gamma> (reversepath (snd (f (k, \<gamma>))))

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 1: "(reversepath ?\<gamma>2) C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reversepath (snd (f (k1, \<gamma>1))) C1_differentiable_on {0..1}
[PROOF STEP]
using f(3) assms(2) ass1 smooth_path_imp_reverse
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
(k1, \<gamma>1) \<in> one_chain1
?g C1_differentiable_on {0..1} \<Longrightarrow> reversepath ?g C1_differentiable_on {0..1}

goal (1 subgoal):
 1. reversepath (snd (f (k1, \<gamma>1))) C1_differentiable_on {0..1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
reversepath (snd (f (k1, \<gamma>1))) C1_differentiable_on {0..1}

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 2: "\<forall>b\<in>basis. continuous_on (path_image (reversepath ?\<gamma>2)) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (reversepath (snd (f (k1, \<gamma>1))))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using f(3) assms(3) ass1 path_image_reversepath
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
(k1, \<gamma>1) \<in> one_chain1
path_image (reversepath ?g) = path_image ?g

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 3: "line_integral F basis ?\<gamma>2 = - line_integral F basis (reversepath ?\<gamma>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
have i:"valid_path (reversepath ?\<gamma>2) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using 1 C1_differentiable_imp_piecewise
[PROOF STATE]
proof (prove)
using this:
reversepath (snd (f (k1, \<gamma>1))) C1_differentiable_on {0..1}
?f C1_differentiable_on ?S \<Longrightarrow> ?f piecewise_C1_differentiable_on ?S

goal (1 subgoal):
 1. valid_path (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
by (auto simp add: valid_path_def)
[PROOF STATE]
proof (state)
this:
valid_path (reversepath (snd (f (k1, \<gamma>1))))

goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
[PROOF STEP]
using line_integral_on_reverse_path(1)[OF i line_integral_exists_smooth[OF 1 2 assms(4)]]
[PROOF STATE]
proof (prove)
using this:
line_integral F basis (reversepath (snd (f (k1, \<gamma>1)))) = - line_integral F basis (reversepath (reversepath (snd (f (k1, \<gamma>1)))))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))

goal (2 subgoals):
 1. ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
 2. \<not> ?P \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                                     line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
using assms reparam_weak_eq_line_integrals_basis[OF 0 1 2 assms(4)]
              ass2 ass3 3
[PROOF STATE]
proof (prove)
using this:
chain_reparam_weak_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2
line_integral F basis \<gamma>1 = line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))
line_integral_exists F basis \<gamma>1
k1 = - 1
fst (f (k1, \<gamma>1)) = 1
line_integral F basis (snd (f (k1, \<gamma>1))) = - line_integral F basis (reversepath (snd (f (k1, \<gamma>1))))

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

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
assume "?k2 \<noteq> 1"
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) \<noteq> 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) \<noteq> 1
[PROOF STEP]
have ass3: "?k2 = -1"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
using bound2 ass1 f(3)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1
boundary_chain one_chain2
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
unfolding boundary_chain_def
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) \<noteq> 1
\<forall>(k, \<gamma>)\<in>one_chain2. k = 1 \<or> k = - 1
(k1, \<gamma>1) \<in> one_chain1
f ` one_chain1 = one_chain2

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (f (k1, \<gamma>1)) = - 1

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (f (k1, \<gamma>1)) = - 1
[PROOF STEP]
have 0: "reparam_weak \<gamma>1 ?\<gamma>2"
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = - 1

goal (1 subgoal):
 1. reparam_weak \<gamma>1 (snd (f (k1, \<gamma>1)))
[PROOF STEP]
using ass1 ass2 f(2)
[PROOF STATE]
proof (prove)
using this:
fst (f (k1, \<gamma>1)) = - 1
(k1, \<gamma>1) \<in> one_chain1
k1 = - 1
\<forall>(k, \<gamma>)\<in>one_chain1. if k = fst (f (k, \<gamma>)) then reparam_weak \<gamma> (snd (f (k, \<gamma>))) else reparam_weak \<gamma> (reversepath (snd (f (k, \<gamma>))))

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

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 1: "?\<gamma>2 C1_differentiable_on {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (f (k1, \<gamma>1)) C1_differentiable_on {0..1}
[PROOF STEP]
using f(3) assms(2) ass1
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
(k1, \<gamma>1) \<in> one_chain1

goal (1 subgoal):
 1. snd (f (k1, \<gamma>1)) C1_differentiable_on {0..1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
snd (f (k1, \<gamma>1)) C1_differentiable_on {0..1}

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
have 2: "\<forall>b\<in>basis. continuous_on (path_image ?\<gamma>2) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<in>basis. continuous_on (path_image (snd (f (k1, \<gamma>1)))) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using f(3) assms(3) ass1
[PROOF STATE]
proof (prove)
using this:
f ` one_chain1 = one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
(k1, \<gamma>1) \<in> one_chain1

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

goal (1 subgoal):
 1. fst (f (k1, \<gamma>1)) \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int ?k2 * line_integral F basis ?\<gamma>2 \<and>
                                     line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
using assms reparam_weak_eq_line_integrals_basis[OF 0 1 2 assms(4)]  ass2 ass3
[PROOF STATE]
proof (prove)
using this:
chain_reparam_weak_chain one_chain1 one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<gamma>2 C1_differentiable_on {0..1}
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
finite basis
boundary_chain one_chain1
boundary_chain one_chain2
line_integral F basis \<gamma>1 = line_integral F basis (snd (f (k1, \<gamma>1)))
line_integral_exists F basis \<gamma>1
k1 = - 1
fst (f (k1, \<gamma>1)) = - 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. k1 \<noteq> 1 \<Longrightarrow> real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
show "real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and>
                                   line_integral_exists F basis \<gamma>1"
[PROOF STATE]
proof (prove)
using this:
real_of_int k1 * line_integral F basis \<gamma>1 = real_of_int (fst (f (k1, \<gamma>1))) * line_integral F basis (snd (f (k1, \<gamma>1))) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1
[PROOF STEP]
by (simp add: case_prod_beta')
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int k1 * line_integral F basis \<gamma>1 = (case f (k1, \<gamma>1) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis \<gamma>1

goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?k1.2, ?\<gamma>1.2) \<in> one_chain1 \<Longrightarrow> real_of_int ?k1.2 * line_integral F basis ?\<gamma>1.2 = (case f (?k1.2, ?\<gamma>1.2) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis ?\<gamma>1.2

goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?k1.2, ?\<gamma>1.2) \<in> one_chain1 \<Longrightarrow> real_of_int ?k1.2 * line_integral F basis ?\<gamma>1.2 = (case f (?k1.2, ?\<gamma>1.2) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis ?\<gamma>1.2
[PROOF STEP]
show "\<And>x. x \<in> one_chain1 \<Longrightarrow>
                                (case x of (k, \<gamma>) \<Rightarrow> (real_of_int k * line_integral F basis \<gamma>) = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and>
                                                        line_integral_exists F basis \<gamma>)"
[PROOF STATE]
proof (prove)
using this:
(?k1.2, ?\<gamma>1.2) \<in> one_chain1 \<Longrightarrow> real_of_int ?k1.2 * line_integral F basis ?\<gamma>1.2 = (case f (?k1.2, ?\<gamma>1.2) of (k2, \<gamma>2) \<Rightarrow> real_of_int k2 * line_integral F basis \<gamma>2) \<and> line_integral_exists F basis ?\<gamma>1.2

goal (1 subgoal):
 1. \<And>x. x \<in> one_chain1 \<Longrightarrow> case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>
[PROOF STEP]
by (auto simp add: case_prod_beta')
[PROOF STATE]
proof (state)
this:
?x \<in> one_chain1 \<Longrightarrow> case ?x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f ?x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>one_chain1. case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>one_chain1. case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
by(simp add: one_chain_line_integral_def sum_bij[OF f(1) _ f(3)] split_beta)
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>one_chain1. case x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma> = (case f x of (k, \<gamma>) \<Rightarrow> real_of_int k * line_integral F basis \<gamma>) \<and> 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 blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed