Theory Basic_Perturbation_Lemma_local_nilpot

(*  Title:      bpl/Basic_Perturbation_Lemma_local_nilpot.thy
    ID:         $Id: Basic_Perturbation_Lemma_local_nilpot.thy $
    Author:     Jesus Aransay
    Comments:
*)

header{*Proof of the Basic Perturbation Lemma*}

theory Basic_Perturbation_Lemma_local_nilpot 
  imports 
  lemma_2_2_19_local_nilpot
  begin

text{*In the following locale we define an abbreviation that we will use later in proofs, and we also join the results obtained in locale
  @{text "lemma_2_2_17"} with the ones reached in @{text "lemma_2_2_11"}. The combination of both locales give us the set of premises in the 
  Basic Perturbation Lemma (from now on, BPL) statement*}

locale BPL = lemma_2_2_17 + lemma_2_2_11

context BPL
begin

definition f' where "f' == (completion 
  (|carrier = kernel D D p, mult = op ⊗, one = \<one>, 
  diff = completion (|carrier = kernel D D p, mult = op ⊗, one = \<one>, diff = differ|)), D (differ)|)), C f)"

end

lemma (in BPL) π_gf: shows "g o f = π"
proof -
  let ?gf = "g o f" 
    (*We have to use this abbreviation ?gf because, otherwise, Isabelle complained about the type of expression "g ⊗R f ∈ carrier R"*)
  from g_f_hom_diff have "?gf ∈ hom_completion D D" unfolding hom_diff_def by simp
  with ring_R have gf_in_R: "?gf ∈ carrier R" by simp
  from gf_dh_hd and ring_R have "?gf ⊕R (differ ⊗R h ⊕R h ⊗R differ) = \<one>R" by simp
  then have "?gf ⊕R (differ ⊗R h ⊕R h ⊗R differ) \<ominus>R (differ ⊗R h ⊕R h ⊗R differ) = \<one>R \<ominus>R (differ ⊗R h ⊕R h ⊗R differ)" by simp
  with gf_in_R and R.one_closed and diff_in_R and h_in_R have "?gf = \<one>R \<ominus>R (differ ⊗R h ⊕R h ⊗R differ)" by algebra
  with π_def and p_def and ring_R show "g o f = π" by simp
qed

subsection{*BPL proof*}

text{*The following lemma corresponds to the first part of @{text "Lemma 2.2.20"} (i.e., the BPL) in Aransay's memoir*}
text{*The proof of the BPL is divided into two parts, as it is also in Aransay's memoir. *}
text{*In the first part, proved in @{text "BPL_reduction"}, from the given premises, we buid a new reduction 
  from @{text "D' = (| carrier = carrier D, …, diff = differD ⊕R δ|)),"} into @{text C'}, 
  where @{text "C' = (| carrier = carrier C, … , diff = f' o (τ' o  differdiff_group_ker_p' o τ) o g|)), (f' o (τ' o (\<one>R \<ominus>R p')))"} *}
text{*The reduction is given by the triple @{term [locale=BPL] "f' o (τ' o (\<one>R \<ominus>R p'))"}, @{term [locale=BPL] "(inc_ker_p' o τ o g)"}, 
  @{term [locale=BPL] "h'"}*}
text{*In the second part of the proof of the BPL, here stored in lemma @{text "BPL_simplifications"}, 
  the expressions @{term [locale=BPL] "f' o (τ' o (\<one>R \<ominus>R p'))"}, @{term [locale=BPL] "(inc_ker_p' o τ o g)"}
   and @{term [locale=BPL] "f' o (τ' o  differdiff_group_ker_p' o τ) o g"} are simplified, obtaining the ones in the BPL statement*}
text{*By finally joining @{text "BPL_reduction"} and @{text "BPL_simplifications"}, we complete the proof of the BPL*}

subsection{*Existence of a reduction*}

lemma (in BPL) BPL_reduction:
  shows "reduction D'
  (| carrier = carrier C, mult = mult C, one = one C, diff = f' o (τ' o  differdiff_group_ker_p' o τ) o g|)), (f' o (τ' o (\<one>R \<ominus>R p'))) 
  (inc_ker_p' o τ o g) h'"
proof -
    (*The following shows a way to import in our context the lemmas in locale "reduction"*)
    (*from reduction_D_C interpret reduction [D C f g h] by (rule reduction.axioms)+*)
    (*from reduction_D_C interpret lemma_2_2_11 [D C f g h] by simp*)
  
    (*First reduction:*)
  from lemma_2_2_15 have red_D'_ker_p': " reduction D' diff_group_ker_p' (\<one>R \<ominus>R p') inc_ker_p' h'" by simp
  
  have iso_inv_diff_ker_p'_ker_p: 
    "(τ', τ) ∈ diff_group_ker_p' ≅invdiff  (| carrier = kernel D D p, mult = mult D, one = one D, diff = τ' o differdiff_group_ker_p' o τ|)),"
    (is "(τ', τ) ∈ diff_group_ker_p' ≅invdiff  ?ker_p_pert")
      and diff_group_ker_p_pert: "diff_group  (| carrier = kernel D D p, mult = mult D, one = one D, diff = τ' o differdiff_group_ker_p' o τ|)),"
    (is "diff_group ?ker_p_pert")
  proof -
    from lemma_2_2_17 have iso_inv_compl: "(τ', τ) ∈ diff_group_ker_p' ≅invcompl diff_group_ker_p" unfolding iso_inv_compl_def by simp
    from lemma_2_2_15 have diff_group_ker_p': "diff_group diff_group_ker_p'" unfolding reduction_def diff_group_def by simp
    from lemma_2_2_14 have comm_group_ker_p: "comm_group diff_group_ker_p" unfolding reduction_def diff_group_def comm_group_def by simp
    from lemma_2_2_18 [OF diff_group_ker_p' comm_group_ker_p iso_inv_compl]
    show "(τ', τ) ∈ diff_group_ker_p' ≅invdiff  ?ker_p_pert" and "diff_group ?ker_p_pert" 
      unfolding diff_group_ker_p_def by simp_all
  qed
  
  (*Second reduction:*)
  from reduction.lemma_2_2_19 [OF red_D'_ker_p' diff_group_ker_p_pert iso_inv_diff_ker_p'_ker_p]
  have red_D'_ker_p_pert: "reduction D' ?ker_p_pert (τ' o (\<one>R \<ominus>R p')) (inc_ker_p' o τ) h'" by simp
  
  (*Now we prove the premises for defining the third and last reduction*)
  have ker_p_isom_C: "(f', g) ∈ (diff_group_ker_p ≅invdiff C)"
  proof -
    from iso_inv_diff_rev [OF lemma_2_2_11] have im_gf_isom_C: "(completion diff_group_im_gf C f, g) ∈ (diff_group_im_gf ≅invdiff C)" by simp
    moreover from π_gf have "g o f = π" by simp
    moreover from im_π_ker_p have im_π_ker_p: "π ` carrier D = kernel D D p" by simp
    ultimately show ?thesis unfolding diff_group_im_gf_def im_gf_def diff_group_ker_p_def f'_def by simp
  qed
  then have ker_p_pert_isom_C: "(f', g) ∈ (?ker_p_pert ≅invcompl C)"
    unfolding iso_inv_diff_def iso_inv_compl_def diff_group_ker_p_def iso_diff_def iso_compl_def hom_diff_def hom_completion_def
      hom_def Pi_def completion_fun2_def completion_def by (auto simp add: expand_fun_eq)
  from red_D'_ker_p_pert have diff_group_ker_p_pert: "diff_group ?ker_p_pert" unfolding reduction_def diff_group_def by simp
  from C_diff_group have C: "comm_group C" unfolding diff_group_def comm_group_def by simp
  from lemma_2_2_18 [OF diff_group_ker_p_pert C ker_p_pert_isom_C]
  have f'_g_isom: "(f', g) ∈ (?ker_p_pert ≅invdiff 
    (| carrier = carrier C, mult = op ⊗C, one = \<one>C, diff = f' o  (τ' o differdiff_group_ker_p' o τ) o g|)),)" 
    (is "(f', g) ∈ (?ker_p_pert ≅invdiff ?C')")
      and diff_group_C_pert: 
      "diff_group (|carrier = carrier C, mult = op ⊗C, one = \<one>C, diff = f' o  (τ' o differdiff_group_ker_p' o τ) o g |)),"
    (is "diff_group ?C'") by simp_all
  
  (*Third reduction*)
  from reduction.lemma_2_2_19 [OF red_D'_ker_p_pert diff_group_C_pert f'_g_isom]
  show "reduction D' ?C' (f' o (τ' o \<one>R \<ominus>R p')) (inc_ker_p' o τ o g) h'" by simp
qed

subsection{*BPL previous simplifications*}

text{*In order to prove the simplifications required in the second part of the proof, i.e. lemma @{text "BPL_simplifications"}, 
  we first have to prove some results concerning the composition of some of the homomorphisms and endomorphisms we have already introduced.*}
text{*Therefore, we have the ring @{term [locale=ring_endomorphisms] "R"}
  and we prove that it behaves as expected with some homomorphisms from @{text "Hom (D C)"} and @{text "Hom (C D)"}, 
  where the operation to relate them is the composition*}
text{*We will prove some properties such as distributivity of composition with respect to addition of endomorphisms and the like*}
text{*The results are stated in generic terms*}

lemma (in ring_endomorphisms) add_dist_comp: assumes C: "diff_group C" and g: "g ∈ hom_completion C D" and a: "a ∈ carrier R"
  and b: "b ∈ carrier R" shows "(a ⊕R b) o g = (λx. if x ∈ carrier C then (a o g) x ⊗ (b o g) x else \<one>)"
  using ring_R and g and a and b and hom_completion_closed [OF g] and completion_closed2 [of g C D] and group_hom.hom_one [of D D a]
    group_hom.hom_one [of D D b] and D_diff_group
  unfolding hom_completion_def completion_def diff_group_def comm_group_def group_hom_def group_hom_axioms_def
  by (auto simp add: expand_fun_eq)

lemma (in ring_endomorphisms) comp_hom_compl: assumes C: "diff_group C" and g: "g ∈ hom_completion C D" and a: "a ∈ carrier R"
  shows "a o g = (λx. if x ∈ carrier C then (a o g) x else \<one>)"
  using ring_R and g and a and hom_completion_closed [OF g] and completion_closed2 [of g C D] 
    and group_hom.hom_one [of D D a] and D_diff_group
  unfolding hom_completion_def completion_def diff_group_def comm_group_def group_hom_def group_hom_axioms_def
  by (auto simp add: expand_fun_eq)

lemma (in ring_endomorphisms) one_comp_g: assumes C: "diff_group C" and g: "g ∈ hom_completion C D"
  shows "\<one>R o g = g"
  using ring_R and g and hom_completion_closed [OF g] and completion_closed2 [of g C D]
  unfolding hom_completion_def completion_fun2_def completion_def apply simp by (auto simp add: expand_fun_eq)

lemma (in ring_endomorphisms) minus_dist_comp: assumes C: "diff_group C" and g: "g ∈ hom_completion C D" and a: "a ∈ carrier R"
  and b: "b ∈ carrier R" shows "(a \<ominus>R b) o g = (λx. if x ∈ carrier C then (a o g) x ⊗ ((\<ominus>R b) o g) x else \<one>)"
  using add_dist_comp [OF C g a a_inv_closed [OF b]] unfolding a_minus_def [OF a b] by simp

lemma (in ring_endomorphisms) minus_comp_g: assumes C: "diff_group C" and g: "g ∈ hom_completion C D" and a: "a ∈ carrier R"
  and b: "b ∈ carrier R" and a_eq_b: "a = b" shows "(\<ominus>R a) o g = (\<ominus>R b) o g"
proof -
  from a and b and a_eq_b have "\<ominus>R a = \<ominus>R b" by algebra
  then show ?thesis by simp
qed

lemma (in ring_endomorphisms) minus_comp_g2: assumes C: "diff_group C" and g: "g ∈ hom_completion C D" and a: "a ∈ carrier R"
  and b: "b ∈ carrier R" and a_eq_b: "a o g = b o g" shows "(\<ominus>R a) o g =  (\<ominus>R b) o g"
  using a_eq_b and minus_interpret [OF a] minus_interpret [OF b] and g by (simp add: expand_fun_eq)

lemma (in ring_endomorphisms) l_add_dist_comp: includes diff_group C assumes f: "f ∈ hom_completion D C" and a: "a ∈ carrier R"
  and b: "b ∈ carrier R" shows "f o (a ⊕R b) = (λx. if x ∈ carrier D then (f o a) x ⊗C (f o b) x else \<one>C)"
  using prems ring_R and f and a and b and hom_completion_closed [of a D D] hom_completion_closed [of b D D]
    and hom_completion_mult [of f D C] group_hom.hom_one [of D C f] and D.diff_group_is_group C.diff_group_is_group
 unfolding hom_completion_def [of D C] group_hom_def group_hom_axioms_def by (simp add: expand_fun_eq)

lemma (in ring_endomorphisms) l_comp_hom_compl: assumes C: "diff_group C" and f: "f ∈ hom_completion D C" and a: "a ∈ carrier R"
  shows "f o a = (λx. if x ∈ carrier D then (f o a) x else \<one>C)"
  using ring_R and f and a and hom_completion_closed [of a] and completion_closed2 [of a D D] and group_hom.hom_one [of D C f] and C 
    and D_diff_group
  unfolding diff_group_def comm_group_def hom_completion_def group_hom_def group_hom_axioms_def by (simp add: expand_fun_eq)

lemma (in ring_endomorphisms) l_minus_dist_comp: includes diff_group C assumes f: "f ∈ hom_completion D C" and a: "a ∈ carrier R"
  and b: "b ∈ carrier R" shows "f o (a \<ominus>R b) = (λx. if x ∈ carrier D then (f o a) x ⊗C (f o (\<ominus>R b)) x else \<one>C)"
  using l_add_dist_comp [OF _ f a a_inv_closed [OF b]] unfolding a_minus_def [OF a b] by (simp add: prems)

(*The following result turned to be much harder than the previous version in the right hand:
  whereas a = b implies directly that - a o f = - b o f (proved in lemma minus_comp_g2), when proving a = b implies f (- a) = f (- b)
  the problem appears that the "inv" definition does not have to be coherent with f, i.e. f (inv a x) ≠ inv (f a x). 
  We propose a proof where the commutative group hom_completion D C is introduced, and using that the inverse is unique in this group,
  and also that f o a, f o b, f o (- a) and f o (- b) are elements of such a ring, the proof is possible*)

lemma (in ring_endomorphisms) l_minus_comp_f: assumes C: "diff_group C" and f: "f ∈ hom_completion D C" and a: "a ∈ carrier R"
  and b: "b ∈ carrier R" and a_eq_b: "f o a = f o b" shows "f o (\<ominus>R a) =  f o (\<ominus>R b)"
proof -
  from HomGroupsCompletion.hom_completion_groups_mult_comm_group [of D C] and C and D_diff_group
  have Hom_D_C: "comm_group (|carrier = hom_completion D C, mult = λf g x. if x ∈ carrier D then f x ⊗C g x else \<one>C,
         one = λx. if x ∈ carrier D then \<one>C else \<one>C|))," unfolding diff_group_def comm_group_def by simp
  let ?hom_D_C = "(|carrier = hom_completion D C, mult = λf g x. if x ∈ carrier D then f x ⊗C g x else \<one>C,
         one = λx. if x ∈ carrier D then \<one>C else \<one>C|)),"
  from ring_R and group_hom.hom_one [of D C f] and f and C and D_diff_group have one_fzero: "one ?hom_D_C = f o \<zero>R"
    unfolding diff_group_def comm_group_def group_def hom_completion_def group_hom_def group_hom_axioms_def by (simp add: expand_fun_eq)
  also from R.r_neg [OF a] have "… = f o (a ⊕R \<ominus>R a)" by simp
  also from l_add_dist_comp [OF C f a a_inv_closed [OF a]] have "… = (λx. if x ∈ carrier D then (f o a) x ⊗C (f o \<ominus>R a) x else \<one>C)"
    by simp
  also from a_eq_b have "… = (λx. if x ∈ carrier D then (f o b) x ⊗C (f o \<ominus>R a) x else \<one>C)" by (simp add: expand_fun_eq)
  also from Hom_D_C have "… = (f o b) ⊗?hom_D_C (f o \<ominus>R a)" by simp
  finally have fb_f_minus_a: "one ?hom_D_C = (f o b) ⊗?hom_D_C (f o \<ominus>R a)" by simp
  from one_fzero have "one ?hom_D_C = f o \<zero>R" by simp
  also from R.l_neg [OF b] have "… = f o (\<ominus>R b ⊕R b)" by simp
  also from l_add_dist_comp [OF C f a_inv_closed [OF b] b] and Hom_D_C have "… = (f o \<ominus>R b) ⊗?hom_D_C (f o b)" by simp
  finally have f_minus_b_fb: "one ?hom_D_C = (f o \<ominus>R b) ⊗?hom_D_C (f o b)" by simp
  from monoid.inv_unique [of ?hom_D_C "(f o \<ominus>R b)" "f o b" "(f o \<ominus>R a)"] and a_inv_closed [OF a] b a_inv_closed [OF b] 
    and sym [OF f_minus_b_fb] and sym [OF fb_f_minus_a] and ring_R 
    and lemma_2_2_18_local_nilpot.hom_completion_comp_closed [of D D C "\<ominus>R a" f]
    and lemma_2_2_18_local_nilpot.hom_completion_comp_closed [of D D C b f] 
    and lemma_2_2_18_local_nilpot.hom_completion_comp_closed [of D D C "\<ominus>R b" f]
    and C and D_diff_group and f and Hom_D_C
  show "(f o \<ominus>R a) = (f o \<ominus>R b)" unfolding diff_group_def comm_group_def group_def by simp
qed

text{*The following properties are used later in lemma @{text "BPL_simplifications"}; just in order to make the proof of 
  @{text "BPL_simplification"} shorter, we  have extracted them, as far as they are not generic properties that can 
  be used in other different settings*}

lemma (in BPL) inc_ker_pτ_eq_τ: shows "inc_ker_p' o τ = τ"
proof -
  have "image τ (π ` carrier D) ⊆ kernel D' D' p'"
  proof (unfold image_def τ_def, auto)
    fix x assume x: "x ∈ carrier D" with π_in_R and ring_R and hom_completion_closed [of π D D x] have "π x  ∈ carrier D" by simp
    with im_π_ker_p and D'_def show "π' (π x) ∈ kernel D' D' p'" unfolding image_def by auto
  qed
  with inc_ker_p'_def and τ_def and D'_def show "inc_ker_p' o τ = τ" unfolding completion_def expand_fun_eq by auto
qed

lemma (in BPL) τg_eq_π'g: shows "τ o g = π' o g"
proof -
  from π_gf have im_g_im_π: "image g (carrier C)  ⊆ π` carrier D"
  proof (unfold image_def, auto simp add: expand_fun_eq)
    fix x assume x: "x ∈ carrier C" with fg have fg_x: "f (g x) = x" by (simp add: expand_fun_eq)
    with hom_diff_closed [OF g_hom_diff x] have "g (f (g x)) = g x" and "g x ∈ carrier D" by (simp_all)
    with π_gf show "∃y∈carrier D. g x = π (y)" by (force simp add: expand_fun_eq)
  qed
  show "τ o g = π' o g" 
  proof (rule ext)
    fix x
    show "(τ o g) x = (π' o g) x"
    proof (cases "x ∈ carrier C")
      case True with im_g_im_π and τ_def and g_hom_diff show "(τ o g) x = (π' o g) x"
        unfolding completion_def hom_diff_def hom_completion_def hom_def Pi_def by (auto simp add: expand_fun_eq)
    next
      case False with g_hom_diff and completion_closed2 [of g C D x] have g_x: "g x = \<one>D"
        unfolding hom_diff_def hom_completion_def by simp
      with lemma_2_2_17 and hom_completion_one [of diff_group_ker_p diff_group_ker_p' τ] and lemma_2_2_14 and lemma_2_2_15
      have r_h_s: "τ (g x) = \<one>D"
        unfolding reduction_def diff_group_def comm_group_def group_def 
        unfolding τ_def iso_inv_compl_def iso_compl_def diff_group_ker_p_def diff_group_ker_p'_def by simp
      from C_diff_group D_diff_group and g_x and π'_in_R and ring_R and hom_completion_one [of D D π']
      have l_h_s: "π' (g x) = \<one>D" unfolding diff_group_def comm_group_def group_def by simp
      from r_h_s and l_h_s show "(τ o g) x = (π' o g) x" by simp
    qed
  qed
qed

lemma (in BPL) diff'h'g_eq_zero: shows "(diff' ⊗R h') o g = (λx. if x ∈ carrier C then \<one> else \<one>)"
proof -
  from ring_R have "(diff' ⊗R h') o g = (diff' o h') o g" by simp
  also have "… = diff' o (h' o g)" by (simp add: o_assoc)
  also from h'_def and psi_h_h_phi and ring_R have "… = diff' o ((Ψ o h) o g)" by simp
  also have "… = diff' o (Ψ o (h o g))" by (simp add: o_assoc)
  also from hg have "… = diff' o (Ψ o (λx. if x ∈ carrier C then \<one> else \<one>))" by simp
  also from psi_in_R and diff'_in_R and ring_R and hom_completion_one [of D D diff'] hom_completion_one [of D D Ψ] 
    and C_diff_group and D_diff_group
  have "… = (λx. if x ∈ carrier C then \<one> else \<one>)" unfolding diff_group_def comm_group_def group_def by (simp add: expand_fun_eq)
  finally show ?thesis by simp
qed

lemma (in BPL) h'diff'g_eq_psihdeltag: shows "(h' ⊗R diff') o g = (Ψ ⊗R h ⊗R δ) o g"
proof -
  from ring_R and sym [OF o_assoc [of h' diff' g]] have "(h' ⊗R diff') o g = h' o (diff' o g)" by simp
  also from add_dist_comp [of C g differ δ] and diff'_def and diff_in_R and pert_in_R and C_diff_group and g_hom_diff
  have "… = h' o (λx. if x ∈ carrier C then (differD o g) x ⊗D (δ o g) x else \<one>)" unfolding hom_diff_def by simp
  also from hom_diff_coherent [OF g_hom_diff] 
  have "… = h' o (λx. if x ∈ carrier C then (g o differC) x ⊗D (δ o g) x else \<one>)" by (simp add: expand_fun_eq)
  also have "… = (λx. if x ∈ carrier C then (h' o (g o differC)) x ⊗ (h' o (δ o g)) x else \<one>)"
  proof (auto simp add: expand_fun_eq)
    fix x assume x: "x ∈ carrier C"
    from ring_R and h'_in_R and hom_completion_mult [of h' D D "(g ((differC) x))" "δ (g x)"]
      and hom_completion_closed [OF diff_group.diff_hom [OF C_diff_group] x] 
      and hom_diff_closed [OF g_hom_diff, of "(differC) x"]
      and hom_diff_closed [OF g_hom_diff x] and pert_in_R hom_completion_closed [of "δ" D D "g x"]
    show "h' (g ((differC) x) ⊗ δ (g x)) = h' (g ((differC) x)) ⊗ h' (δ (g x))" by simp
  next
    from D.diff_group_is_group have D: "group D" by simp
    with ring_R and h'_in_R show "h' \<one> = \<one>" by (intro hom_completion_one, simp_all)
  qed
  also have "… =  (λx. if x ∈ carrier C then (h' o g o differC) x ⊗ (h' o (δ o g)) x else \<one>)" by (simp add: expand_fun_eq o_assoc)
  also from h'_def and ring_R have "… = (λx. if x ∈ carrier C then (h o Φ o g o differC) x ⊗ (h o Φ o (δ o g)) x else \<one>)" 
    by (simp add: expand_fun_eq)
  also from psi_h_h_phi and ring_R have "… = (λx. if x ∈ carrier C then (Ψ o h o g o differC) x ⊗ (Ψ o h o (δ o g)) x else \<one>)"
    by (simp add: expand_fun_eq)
  also have "… = (λx. if x ∈ carrier C then (Ψ o h o (δ o g)) x else \<one>)"
  proof (auto simp add: expand_fun_eq)
    fix x assume x: "x ∈ carrier C"
    from hg and psi_in_R and hom_completion_one [of D D Ψ] and ring_R and D.diff_group_is_group
    have " Ψ (h (g ((differC) x))) = \<one>" by (simp add: expand_fun_eq)
    moreover have "Ψ (h (δ (g x))) ∈ carrier D"
    proof -
      from pert_in_R and h_in_R and psi_in_R have "Ψ ⊗R h ⊗R δ ∈ carrier R" by algebra
      with ring_R have psi_h_pert: "Ψ o  h o δ ∈ hom_completion D D" by simp
      from hom_completion_closed [OF psi_h_pert, of "g x"] and hom_diff_closed [OF g_hom_diff x]
      show "Ψ (h (δ (g x))) ∈ carrier D" by simp
    qed
    ultimately show "Ψ (h (g ((differC) x))) ⊗ Ψ (h (δ (g x))) = Ψ (h (δ (g x)))" by (simp add: D.r_one)
  qed
  also from ring_R have "… = (λx. if x ∈ carrier C then (Ψ ⊗R h ⊗R δ  o g) x else \<one>)" by (simp add: expand_fun_eq)
  also from comp_hom_compl [of C g "Ψ ⊗R h ⊗R δ"] and pert_in_R h_in_R psi_in_R and g_hom_diff C_diff_group
  have "… = (Ψ ⊗R h ⊗R δ) o g" unfolding hom_diff_def by simp
  finally show ?thesis by simp
qed

lemma (in BPL) p'g_eq_psihdeltag: shows "p' o g = (Ψ ⊗R h ⊗R δ) o g"
proof -
  from p'_def and ring_R and diff'_def have "p' o g = ((diff' ⊗R h') ⊕R (h' ⊗R diff')) o g" by (simp add: expand_fun_eq)
  also from add_dist_comp [of C g "(diff' ⊗R h')" "(h' ⊗R diff')"] and g_hom_diff and diff'_in_R h'_in_R and C_diff_group
  have "… =  (λx. if x ∈ carrier C then ((diff' ⊗R h') o g) x ⊗ ((h' ⊗R diff') o g) x else \<one>)" by (unfold hom_diff_def, simp)
  also from diff'h'g_eq_zero and h'diff'g_eq_psihdeltag have "… = (λx. if x ∈ carrier C then (Ψ ⊗R h ⊗R δ o g) x else \<one>)"
  proof (auto simp add: expand_fun_eq, intro D.l_one)
    fix x assume x: "x ∈ carrier C"
    from pert_in_R and h_in_R and psi_in_R have "Ψ ⊗R h ⊗R δ ∈ carrier R" by algebra
    with ring_R have psi_h_pert: "Ψ ⊗R  h ⊗R δ ∈ hom_completion D D" by simp
    from hom_completion_closed [OF psi_h_pert, of "g x"] and hom_diff_closed [OF g_hom_diff x] 
    show "(Ψ ⊗R  h ⊗R δ) (g x) ∈ carrier D" by simp
  qed
  also from comp_hom_compl [of C g "Ψ ⊗R h ⊗R δ"] and pert_in_R h_in_R psi_in_R and g_hom_diff C_diff_group
  have "… = (Ψ ⊗R h ⊗R δ) o g" by (unfold hom_diff_def, simp)
  finally show ?thesis by simp
qed

lemma (in BPL) τ'π'_eq_ππ': shows "τ' o π' = π o π'"
proof (rule ext)
  fix x
  show "(τ' o π') x = (π o π') x"
  proof (cases "x ∈ carrier D")
    case True with π'_in_R ring_R and hom_completion_closed [of π' D D x] 
    have π'_im: "π' x ∈ π'`(carrier D)" and π'_D: "π' x ∈ carrier D" unfolding image_def by auto
    with τ'_def and D'_def show "(τ' o π') x = (π o π') x" by (simp add: expand_fun_eq)
  next
    case False with π'_in_R and ring_R and completion_closed2 [of π' D D x] have π'_x: "π' x = \<one>" unfolding hom_completion_def by simp
    with lemma_2_2_17 and hom_completion_one [of diff_group_ker_p' diff_group_ker_p τ'] and lemma_2_2_14 and lemma_2_2_15
    have r_h_s: "τ' (π' x) = \<one>D"
      unfolding reduction_def diff_group_def comm_group_def group_def τ'_def 
      unfolding iso_inv_compl_def iso_compl_def diff_group_ker_p_def diff_group_ker_p'_def by simp
    from π_in_R and ring_R and hom_completion_one [of D D π] and π'_x and D.diff_group_is_group
    have l_h_s: "π (π' x) = \<one>" by simp
    from r_h_s and l_h_s show ?thesis by simp
  qed
qed

lemma (in BPL) f'π_eq_fπ: shows "f' o π = f o π"
proof (rule ext)
  fix x
  show "(f' o π) x = (f o π) x"
  proof (cases "x ∈ carrier D")
    case True with π_in_R and ring_R and hom_completion_closed [of π D D] have π_im: "π x ∈ π`(carrier D)" 
      and π_D: "π x ∈ carrier D" by (unfold image_def, auto)
    then have "π x ∈ kernel D D p" using im_π_ker_p by simp
    then show "(f' o π) x = (f o π) x" unfolding f'_def by (simp add: expand_fun_eq)
  next
    case False with π_in_R and ring_R and completion_closed2 [of π D D x] have π_x: "π x = \<one>" unfolding hom_completion_def by simp
    from iso_inv_diff_rev [OF lemma_2_2_11] and π_gf im_π_ker_p
    have "(f', g) ∈ (diff_group_im_gf ≅invdiff C)" unfolding f'_def diff_group_im_gf_def im_gf_def by simp
    with hom_completion_one [of diff_group_im_gf C f'] and π_x and C.diff_group_is_group and image_g_f_diff_group 
    have r_h_s: "f' (π x) = \<one>C" unfolding diff_group_im_gf_def im_gf_def diff_group_def comm_group_def 
      iso_inv_diff_def iso_diff_def hom_diff_def by simp
    from hom_diff_is_hom_completion [OF f_hom_diff] and hom_completion_one [of D C f] and π_x 
      and D.diff_group_is_group C.diff_group_is_group have l_h_s: "f (π x) = \<one>C" by simp
    from r_h_s and l_h_s show ?thesis by simp
  qed
qed

lemma (in BPL) fπ_eq_f: shows "f o π = f"
proof -
  from sym [OF π_gf] have "f o π = f o g o f" by (simp add: o_assoc)
  also from fg have "… = (λx. if x ∈ carrier C then id x else \<one>C) o f" by simp
  also from f_hom_diff have "… = f" 
    unfolding hom_diff_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def by (auto simp add: expand_fun_eq)
  finally have "f o π = f" by simp
  then show ?thesis by (simp add: expand_fun_eq)
qed

lemma (in BPL) fh'diff'_eq_zero: shows "f o (h' ⊗R diff') = (λx. if x ∈ carrier D then \<one>C else \<one>C)"
proof -
  from ring_R have "f o (h' ⊗R diff') = f o h' o diff'" by (simp add: o_assoc)
  also from ring_R and h'_def and o_assoc [of f h Φ] have "… = f o h o Φ o diff'" by simp
  also from fh have "… = (λx. if x ∈ carrier D then \<one>C else \<one>C)" by (simp add: expand_fun_eq)
  finally show "f o (h' ⊗R diff') = (λx. if x ∈ carrier D then \<one>C else \<one>C)" by simp
qed

lemma (in BPL) fdiff'h'_eq_fdeltahphi: shows "f o (diff' ⊗R h') = f o δ ⊗R h ⊗R Φ"
proof -
  from diff'_def have "f o (diff' ⊗R h') = f o (differ ⊕R δ) ⊗R h'" by simp
  also from diff_in_R and pert_in_R and h'_in_R have "… = f o (differ ⊗R h' ⊕R δ ⊗R h')" by algebra
  also from l_add_dist_comp [OF C_diff_group, of f "differ ⊗R h'" "δ ⊗R h'"] and diff_in_R and pert_in_R and h'_in_R and f_hom_diff
  have "… = (λx. if x ∈ carrier D then (f o differ ⊗R h') x ⊗C (f o δ ⊗R h') x else \<one>C)" unfolding hom_diff_def by simp
  also from ring_R have "… = (λx. if x ∈ carrier D then (f o differ o h') x ⊗C (f o δ ⊗R h') x else \<one>C)" by (simp add: expand_fun_eq)
  also from hom_diff_coherent [OF f_hom_diff] 
  have "… = (λx. if x ∈ carrier D then (differC o f o h') x ⊗C (f o δ ⊗R h') x else \<one>C)" by (simp add: expand_fun_eq)
  also from h'_def and ring_R have "… = (λx. if x ∈ carrier D then (differC o f o h o Φ) x ⊗C (f o δ ⊗R h') x else \<one>C)" 
    by (simp add: expand_fun_eq)
  also from fh and hom_completion_one [OF _ _ diff_hom] C.diff_group_is_group and l_one and hom_completion_closed [of h' D D]
    and hom_completion_closed [of δ D D] and hom_diff_closed [OF f_hom_diff] and ring_R and h'_in_R and pert_in_R
  have "… = (λx. if x ∈ carrier D then (f o δ ⊗R h') x else \<one>C)" by (simp add: expand_fun_eq)
  also from l_comp_hom_compl [OF C_diff_group, of f "δ ⊗R h'"] and f_hom_diff have "… = f o δ ⊗R h'" unfolding hom_diff_def by simp
  also from h'_def and pert_in_R and h_in_R and phi_in_R have "… = f o δ ⊗R h ⊗R Φ" by algebra
  finally show ?thesis by simp
qed

lemma (in BPL) fp'_eq_fdeltahphi: shows "f o p' = f o δ ⊗R h ⊗R Φ"
proof -
  from p'_def and diff'_def and l_add_dist_comp [OF C_diff_group, of f "diff' ⊗R h'" "h' ⊗R diff'"] f_hom_diff 
    and diff'_in_R pert_in_R h'_in_R
  have "f o p' = (λx. if x ∈ carrier D then (f o diff' ⊗R h') x ⊗C (f o h' ⊗R diff') x else \<one>C)" by (unfold hom_diff_def, simp)
  also from fh'diff'_eq_zero and fdiff'h'_eq_fdeltahphi and r_one and hom_completion_closed [of h D D] and hom_completion_closed [of Φ D D]
    and hom_completion_closed [of δ D D] and hom_diff_closed [OF f_hom_diff] and ring_R and h_in_R and phi_in_R and pert_in_R
  have "… = (λx. if x ∈ carrier D then (f o δ ⊗R h ⊗R Φ) x else \<one>C)" by (simp add: expand_fun_eq)
  also from l_comp_hom_compl [OF C_diff_group, of f "δ ⊗R h ⊗R Φ"] and h_in_R and phi_in_R and pert_in_R f_hom_diff
  have "… = f o δ ⊗R h ⊗R Φ" unfolding hom_diff_def by simp
  finally show ?thesis by simp
qed

lemma (in BPL) diff_ker_p'π'_eq_diff'π': shows "differdiff_group_ker_p' o π' = diff' o π'"
proof (rule ext)
  fix x
  show "(differdiff_group_ker_p' o π') x = (diff' o π') x"
  proof (cases "x ∈ carrier D")
    case True from im_π_ker_p and D'_def have im_π'_ker_p': "image π' (carrier D) ⊆ kernel D' D' p'" by simp
    with True show "(differdiff_group_ker_p' o π') x = (diff' o π') x"
      unfolding diff_group_ker_p'_def diff'_def D'_def completion_def image_def by (auto simp add: expand_fun_eq)
  next
    case False with π'_in_R and ring_R and completion_closed2 [of π' D D x] have π'_x: "π' x = \<one>" unfolding hom_completion_def by simp
    with diff'_in_R and ring_R and hom_completion_one [of D D diff'] and D.diff_group_is_group 
    have l_h_s: "(diff' o π') x = \<one>" by simp
    from reduction.C_diff_group [OF lemma_2_2_15] and diff_group.diff_hom
    have diff_ker_p': "differdiff_group_ker_p' ∈ hom_completion diff_group_ker_p' diff_group_ker_p'" by auto
    from π'_x and hom_completion_one [OF _ _ diff_ker_p'] and reduction.C_diff_group [OF lemma_2_2_15]
    have r_h_s: "(differdiff_group_ker_p' o π') x = \<one>" unfolding diff_group_ker_p'_def diff_group_def comm_group_def group_def by simp
    from l_h_s and r_h_s show ?thesis by simp
  qed
qed

lemma (in BPL) τ'diff'_eq_πdiff': shows "τ' o differdiff_group_ker_p' = π o differdiff_group_ker_p'"
proof (rule ext)
  fix x
  show "(τ' o differdiff_group_ker_p') x = (π o differdiff_group_ker_p') x"
  proof (cases "x ∈ kernel D' D' p'")
    case True from reduction.C_diff_group [OF lemma_2_2_15] and diff_group.diff_hom
    have "differdiff_group_ker_p' ∈ hom_completion diff_group_ker_p' diff_group_ker_p'" by auto
    then have "image (differdiff_group_ker_p') (kernel D' D' p') ⊆ kernel D' D' p'"
      unfolding diff_group_ker_p'_def hom_completion_def hom_def Pi_def image_def kernel_def D'_def by auto
    with im_π_ker_p and D'_def have "image (differdiff_group_ker_p') (kernel D' D' p') ⊆ image π' (carrier D)" by simp
    with True and τ'_def show "(τ' o differdiff_group_ker_p') x = (π o differdiff_group_ker_p') x"
      unfolding completion_def image_def D'_def by (auto simp add: expand_fun_eq)
  next
    case False from reduction.C_diff_group [OF lemma_2_2_15] and diff_group.diff_hom
    have "differdiff_group_ker_p' ∈ hom_completion diff_group_ker_p' diff_group_ker_p'" by auto
    with completion_closed2 [of "differdiff_group_ker_p'" diff_group_ker_p' diff_group_ker_p' x] and False and D'_def
    have diff'_x: "(differdiff_group_ker_p') x = \<one>" unfolding hom_completion_def diff_group_ker_p'_def by simp
    with lemma_2_2_17 and hom_completion_one [of diff_group_ker_p' diff_group_ker_p τ'] and lemma_2_2_14 and lemma_2_2_15
    have r_h_s: "τ' ((differdiff_group_ker_p') x) = \<one>D"
      unfolding reduction_def diff_group_def comm_group_def group_def τ'_def iso_inv_compl_def iso_compl_def diff_group_ker_p_def 
        diff_group_ker_p'_def by simp
    from π_in_R and ring_R and hom_completion_one [of D D π] and diff'_x and D.diff_group_is_group
    have l_h_s: "π ((differdiff_group_ker_p') x) = \<one>" by simp
    from r_h_s and l_h_s show ?thesis by simp
  qed
qed

lemma (in BPL) fπ'g_eq_id: shows "f o π' o g = (λx. if x ∈ carrier C then id x else \<one>C)"
proof -
  have "f o π' o g = f o (\<one>R \<ominus>R p') o g" unfolding π'_def by simp
  also from l_minus_dist_comp [OF C_diff_group _ R.one_closed, of f p'] and p'_in_R and f_hom_diff and C_diff_group
  have "… = (λx. if x ∈ carrier D then (f o \<one>R) x ⊗C (f o (\<ominus>R p')) x else \<one>C) o g" unfolding hom_diff_def by simp
  also from phi_in_R h_in_R pert_in_R and l_minus_comp_f [OF C_diff_group, of f p' "δ ⊗R h ⊗R Φ"]  and fp'_eq_fdeltahphi and f_hom_diff
  have "… = (λx. if x ∈ carrier D then (f o \<one>R) x ⊗C (f o \<ominus>R (δ ⊗R h ⊗R Φ)) x else \<one>C) o g"
    unfolding hom_diff_def by (auto simp add: expand_fun_eq)
  also from sym [OF l_minus_dist_comp [OF C_diff_group _ R.one_closed, of f "(δ ⊗R h ⊗R Φ)"]] and f_hom_diff and pert_in_R h_in_R phi_in_R
  have "… = f o (\<one>R \<ominus>R (δ ⊗R h ⊗R Φ)) o g" unfolding hom_diff_def by simp
  also from phi_prop have "… = f o (\<one>R \<ominus>R Φ ⊗R δ ⊗R h) o g" by simp
  also from minus_dist_comp [OF C_diff_group _ R.one_closed, of g "Φ ⊗R δ ⊗R h"] and g_hom_diff and phi_in_R pert_in_R h_in_R
  have "… = f o (λx. if x ∈ carrier C then (\<one>R o g) x ⊗ (\<ominus>R (Φ ⊗R δ ⊗R h) o g) x else \<one>)" 
    by (unfold hom_diff_def, simp add: expand_fun_eq)
  also have "… = f o (λx. if x ∈ carrier C then (\<one>R o g) x else \<one>)"
  proof -
    have "(\<ominus>R (Φ ⊗R δ ⊗R h) o g) = \<ominus>R \<zero>R o g" 
    proof -
      from hg and ring_R and hom_completion_one [of D D δ] hom_completion_one [of D D Φ] and D.diff_group_is_group and pert_in_R and phi_in_R
      have "(Φ ⊗R δ ⊗R h) o g = \<zero>R o g" by (simp add: expand_fun_eq)
      with minus_comp_g2 [OF C_diff_group _ _ R.zero_closed, of g "Φ ⊗R δ ⊗R h"] and g_hom_diff and phi_in_R pert_in_R h_in_R
      show "(\<ominus>R (Φ ⊗R δ ⊗R h) o g) = \<ominus>R \<zero>R o g" unfolding hom_diff_def by simp
    qed
    also have "… = \<zero>R o g" by simp
    also from ring_R have "… = (λx. \<one>)" by (simp add: expand_fun_eq)
    finally have "\<ominus>R (Φ ⊗R δ ⊗R h) o g = (λx. \<one>)" by simp
    with D.r_one and g_hom_diff and hom_completion_closed [of g C D] and ring_R show ?thesis by (simp add: expand_fun_eq)
  qed
  also from comp_hom_compl [OF C_diff_group _ R.one_closed, of g] and g_hom_diff have "… = f o (\<one>R o g)" unfolding hom_diff_def by simp
  also from g_hom_diff and hom_completion_closed [of g C D] and ring_R have "… = f o g"
  proof -
    from g_hom_diff and hom_completion_closed [of g C D] and ring_R have "(\<one>R o g) = g"
      unfolding hom_diff_def hom_completion_def completion_fun2_def completion_def by (auto simp add: expand_fun_eq)
    then show ?thesis by simp
  qed
  also from fg have "… = (λx. if x ∈ carrier C then id x else \<one>C)" by simp
  finally show "f o π' o g = (λx. if x ∈ carrier C then id x else \<one>C)" by simp
qed

lemma (in BPL) π'g_eq_psig: shows "π' o g  = Ψ o g"
proof -
  from π'_def have "π' o g = (\<one>R \<ominus>R p') o g" by simp
  also from minus_dist_comp [of C g "\<one>R" p'] and p'_in_R and R.one_closed and g_hom_diff and C_diff_group
  have "… = (λx. if x ∈ carrier C then (\<one>R o g) x ⊗ ((\<ominus>R p') o g) x else \<one>)" by (unfold hom_diff_def, simp)
  also from psi_in_R h_in_R pert_in_R and minus_comp_g2 [OF C_diff_group, of g p' "Ψ ⊗R h ⊗R δ"]  and p'g_eq_psihdeltag and g_hom_diff
  have "… = (λx. if x ∈ carrier C then (\<one>R o g) x ⊗ (\<ominus>R (Ψ ⊗R h ⊗R δ) o g) x else \<one>)"
    unfolding hom_diff_def by (auto simp add: expand_fun_eq)
  also from sym [OF minus_dist_comp [OF C_diff_group _ R.one_closed, of g "(Ψ ⊗R h ⊗R δ)"]] and g_hom_diff and pert_in_R h_in_R phi_in_R
  have "… = (\<one>R \<ominus>R (Ψ ⊗R h ⊗R δ)) o g" unfolding hom_diff_def by simp
  also from psi_prop have "… = Ψ o g" by simp
  finally show ?thesis by simp
qed

subsection{*BPL simplification*}

text{*Now we can prove the simplifications of the terms in the reduction; these simplification processes correspond 
  to the ones in pages 56 and 57 of Aransay's memoir*}

lemma (in BPL) BPL_simplifications: shows f: "(f' o (τ' o \<one>R \<ominus>R p')) = f o Φ" and g: "(inc_ker_p' o τ o g) = Ψ o g" 
  and diff_C: "f' o (τ' o differdiff_group_ker_p' o τ) o g = (λx. if x ∈ carrier C then (differC) x ⊗C (f o δ o Ψ o g) x else \<one>C)"
proof -
  show "f' o (τ' o \<one>R \<ominus>R p') = f o Φ" 
    (*The proof is divided into 3 parts; first we prove f' o (τ' o \<one>R \<ominus>R p') = f' o (π o \<one>R \<ominus>R p')*)
    (*Then we prove that f' o (π o \<one>R \<ominus>R p') = f o (π o \<one>R \<ominus>R p')*)
    (*Then we deal with this expression, proving that f o π = f, and finally, the hardest part, that f o \<one>R \<ominus>R p' = f o Φ*)
  proof -
    have "f' o (τ' o \<one>R \<ominus>R p') = f' o (τ' o π')" unfolding π'_def by simp
    also have "… = f' o (π o π')" unfolding τ'π'_eq_ππ' by simp
    also have "… = f o π o π'" unfolding o_assoc unfolding f'π_eq_fπ by simp
    also have "… = f o π'" unfolding fπ_eq_f by simp
    also have "… = f o (\<one>R \<ominus>R p')" unfolding π'_def by simp
    also from l_minus_dist_comp [OF C_diff_group _ R.one_closed, of f p'] and p'_in_R and f_hom_diff and C_diff_group
    have "… = (λx. if x ∈ carrier D then (f o \<one>R) x ⊗C (f o (\<ominus>R p')) x else \<one>C)" unfolding hom_diff_def by simp
    also from phi_in_R h_in_R pert_in_R and l_minus_comp_f [OF C_diff_group, of f p' "δ ⊗R h ⊗R Φ"]  and fp'_eq_fdeltahphi and f_hom_diff
    have "… = (λx. if x ∈ carrier D then (f o \<one>R) x ⊗C (f o \<ominus>R (δ ⊗R h ⊗R Φ)) x else \<one>C)"
      unfolding hom_diff_def by (auto simp add: expand_fun_eq)
    also from sym [OF l_minus_dist_comp [OF C_diff_group _ R.one_closed, of f "(δ ⊗R h ⊗R Φ)"]] and f_hom_diff and pert_in_R h_in_R phi_in_R
    have "… = f o (\<one>R \<ominus>R (δ ⊗R h ⊗R Φ))" unfolding hom_diff_def by simp
    also from phi_prop have "… = f o Φ" by simp
    finally show ?thesis by simp
  qed
next
  show "(inc_ker_p' o τ o g) = Ψ o g"
  proof -
    have "inc_ker_p' o τ o g = τ o g" unfolding inc_ker_pτ_eq_τ by simp
    also have "… = π' o g" unfolding τg_eq_π'g by simp
    (*This part of the proof corresponds exactly to lemma π'g_eq_psig; the reason for maintaining it here is for keeping the similarity 
      to the proof in the memoir*)
    also have "π' o g = (\<one>R \<ominus>R p') o g" unfolding π'_def by simp
    also from minus_dist_comp [of C g "\<one>R" p'] and p'_in_R and R.one_closed and g_hom_diff and C_diff_group
    have "… = (λx. if x ∈ carrier C then (\<one>R o g) x ⊗ ((\<ominus>R p') o g) x else \<one>)" unfolding hom_diff_def by simp
    also from psi_in_R h_in_R pert_in_R and minus_comp_g2 [OF C_diff_group, of g p' "Ψ ⊗R h ⊗R δ"]  and p'g_eq_psihdeltag and g_hom_diff
    have "… = (λx. if x ∈ carrier C then (\<one>R o g) x ⊗ (\<ominus>R (Ψ ⊗R h ⊗R δ) o g) x else \<one>)"
      unfolding hom_diff_def by (auto simp add: expand_fun_eq)
    also from sym [OF minus_dist_comp [OF C_diff_group _ R.one_closed, of g "(Ψ ⊗R h ⊗R δ)"]] and g_hom_diff and pert_in_R h_in_R phi_in_R
    have "… = (\<one>R \<ominus>R (Ψ ⊗R h ⊗R δ)) o g" unfolding hom_diff_def by simp
    also from psi_prop have "… = Ψ o g" by simp
    finally show ?thesis by simp
  qed
next
  show "f' o (τ' o differdiff_group_ker_p' o τ) o g = (λx. if x ∈ carrier C then (differC) x ⊗C (f o δ o Ψ o g) x else \<one>C)"
    (is "f' o (τ' o ?diff_ker_p' o τ) o g = ?diff_C_pert")
  proof -
    have "f' o (τ' o ?diff_ker_p' o τ) o g = (f' o τ') o ?diff_ker_p' o (τ o g)" by (simp add: o_assoc)
    also from τg_eq_π'g have "… = (f' o τ') o ?diff_ker_p' o (π' o g)" by simp
    also have "… = f' o (τ' o ?diff_ker_p') o π' o g" by (simp add: o_assoc)
    also from τ'diff'_eq_πdiff' have "… = f' o (π o differdiff_group_ker_p') o π' o g" by (simp add: expand_fun_eq)
    also have "… = f' o π o (differdiff_group_ker_p' o π') o g" by (simp add: o_assoc)
    also from diff_ker_p'π'_eq_diff'π' have "… = f' o π o (diff' o π') o g" by (simp add: expand_fun_eq)
    also from f'π_eq_fπ have "… = f o π o (diff' o π') o g" by simp
    also from fπ_eq_f have "… = f o (diff' o π') o g" by simp
    also have "… = f o diff' o (π' o g)" by (simp add: o_assoc)
    also from diff'_def have "… = f o (differ ⊕R δ) o (π' o g)" by simp
    also have "… = f o ((differ ⊕R δ) o π') o g" by (simp add: o_assoc)
    also from ring_R have "… = f o ((differ ⊕R δ) ⊗R π') o g" by simp
    also from π'_in_R and diff_in_R and pert_in_R and R.one_closed have "… = f o (differ ⊗R π' ⊕R δ ⊗R π') o g" by algebra
    also from l_add_dist_comp [OF C_diff_group, of f "differ ⊗R π'" "δ ⊗R π'"] f_hom_diff diff_in_R π'_in_R pert_in_R
    have "… = (λx. if x ∈ carrier D then (f o (differ ⊗R π')) x ⊗C  (f o (δ ⊗R π')) x else \<one>C) o g" by (unfold hom_diff_def, simp)
    also from ring_R and o_assoc have "… = (λx. if x ∈ carrier D then (f o differ o π') x ⊗C  (f o (δ ⊗R π')) x else \<one>C) o g" 
      by (simp add: expand_fun_eq)
    also from hom_diff_coherent [OF f_hom_diff] 
    have "… =  (λx. if x ∈ carrier D then (differC o f o π') x ⊗C  (f o (δ ⊗R π')) x else \<one>C) o g" by (simp add: expand_fun_eq)
    also have "… = (λx. if x ∈ carrier C then ((differC o f o π') o g) x ⊗C  ((f o (δ ⊗R π')) o g) x else \<one>C)"
    proof (auto simp add: expand_fun_eq)
      fix x
      assume x: "x ∈ carrier C" and "g x ∉ carrier D" with g_hom_diff and hom_completion_closed [of g C D] 
      show "\<one>C = (differC) (f (π' (g x))) ⊗C f ((δ ⊗R π') (g x))" by (unfold hom_diff_def, simp)
    next
      fix x
      assume "x ∉ carrier C" with completion_closed2 [of g C D x] and g_hom_diff have g_x: "g x = \<one>"
        by (unfold hom_diff_def hom_completion_def, simp)
      with hom_completion_one [of D D π'] and π'_in_R and ring_R and D.diff_group_is_group
        and hom_completion_one [of D C f] and C.diff_group_is_group and f_hom_diff
        and hom_completion_one [of C C "differC"] and diff_group.diff_hom [OF C_diff_group]
        and hom_completion_one [of D D "δ ⊗R π'"] and pert_in_R and R.m_closed [of δ π']
      show " (differC) (f (π' (g x))) ⊗C f ((δ ⊗R π') (g x)) = \<one>C" by (unfold hom_diff_def, auto)
    qed
    also from ring_R have "… = (λx. if x ∈ carrier C then (differC o (f o π' o g)) x ⊗C (f o δ o π' o g) x else \<one>C)"
      by (simp add: o_assoc expand_fun_eq)
    also from fπ'g_eq_id and diff_group.diff_hom [OF C_diff_group] 
    have "… = (λx. if x ∈ carrier C then (differC) x ⊗C (f o δ o π' o g) x else \<one>C)"
      by (unfold hom_completion_def completion_fun2_def completion_def, auto simp add: expand_fun_eq)
    also from π'g_eq_psig have "… = (λx. if x ∈ carrier C then (differC) x ⊗C (f o δ o Ψ o g) x else \<one>C)" by (simp add: expand_fun_eq)
    finally show " f' o (τ' o differdiff_group_ker_p' o τ) o g = (λx. if x ∈ carrier C then (differC) x ⊗C (f o δ o Ψ o g) x else \<one>C)"
      by simp
  qed
qed

text{*By joining @{thm [locale=BPL] BPL_reduction} and @{thm [locale=BPL] BPL_simplifications} we get the proof of the BPL, 
  stated as in @{text "Lemma 2.2.20"} in Aransay's memoir*}

lemma (in BPL) BPL: shows "reduction D' 
  (| carrier = carrier C, mult = mult C, one = one C, diff = (λx. if x ∈ carrier C then (differC) x ⊗C (f o δ o Ψ o g) x else \<one>C)|)), 
  (f o Φ) (Ψ o g) h'"
using BPL_reduction and BPL_simplifications by simp

end