Theory lemma_2_2_17_local_nilpot

(*  Title:      bpl/lemma_2_2_17_local_nilpot.thy
    ID:         $Id: lemma_2_2_17.thy $
    Author:     Jesus Aransay
    Comments:   The set of lemmas proving the equational part of the BPL
*)

header{*Proposition 2.2.16 and Lemma 2.2.17 in Aransay's memoir*}

theory lemma_2_2_17_local_nilpot imports lemma_2_2_15_local_nilpot
begin

subsection{*Previous definitions*}

text{*Locale @{text "proposition_2_2_16"} does not introduce new facts; only some new definitions are given in the locale*}

locale proposition_2_2_16 = lemma_2_2_15

definition (in proposition_2_2_16)
  π where "π = \<one>R \<ominus>R p"

definition (in proposition_2_2_16)
  π' where "π' = \<one>R \<ominus>R p'"

text{*The following lemma has been extracted from the proof of @{text "Proposition 2.2.16"} as stated in the memoir*}

lemma (in proposition_2_2_16) hp'_h [simp]: shows "h ⊗R p' = h" and "p' ⊗R h = h"
  (*These are again nice examples of proofs that could be tried in different environments for automatic theorem proving in rings or also
  even in a term rewriting system*)
proof -
  show "h ⊗R p' = h"
  proof -
    from p'_def and diff'_def have "h ⊗R p' = h ⊗R ((differ ⊕R δ) ⊗R h' ⊕R h' ⊗R (differ ⊕R δ))" by simp
    also from diff_in_R and pert_in_R and h'_in_R and h_in_R
    have "… = h ⊗R ((differ ⊕R δ) ⊗R h') ⊕R h ⊗R (h' ⊗R (differ ⊕R δ))" by algebra
    also from diff_in_R and pert_in_R and h'_in_R and h_in_R
    have "… = h ⊗R (differ ⊗R h' ⊕R δ ⊗R h') ⊕R h ⊗R h' ⊗R (differ ⊕R δ)" by algebra
    also from diff_in_R and pert_in_R and h'_in_R and h_in_R and h'_def
    have "… = h ⊗R (differ ⊗R  (h ⊗R Φ)) ⊕R h ⊗R (δ ⊗R  (h ⊗R Φ)) ⊕R h ⊗R (h ⊗R Φ) ⊗R (differ ⊕R δ)" by algebra
    also from diff_in_R and pert_in_R and h_in_R and phi_in_R
    have "… = h ⊗R differ ⊗R h ⊗R Φ ⊕R h ⊗R (δ ⊗R h ⊗R Φ) ⊕R h ⊗R h ⊗R Φ ⊗R (differ ⊕R δ)" by algebra
    also have "… = h ⊗R Φ ⊕R h ⊗R (\<one>R \<ominus>R Φ)"
    proof -
      from phi_prop have "Φ = \<one>R \<ominus>R δ ⊗R h ⊗R Φ" by simp
      with phi_in_R and h_in_R and pert_in_R have "\<one>R \<ominus>R Φ = \<one>R \<ominus>R (\<one>R \<ominus>R δ ⊗R h ⊗R Φ)" by algebra
      with phi_in_R and h_in_R and pert_in_R have "\<one>R \<ominus>R Φ = δ ⊗R h ⊗R Φ" by algebra
      with diff_in_R and pert_in_R and h'_in_R and h_in_R and phi_in_R and hdh_h and h_nil
      show ?thesis by algebra
    qed
    also from h_in_R and phi_in_R and R.r_one [OF h_in_R] have "… = h" by algebra
    finally show "h ⊗R p' = h" by simp
  qed
next
  show "p' ⊗R h = h"
  proof -
    from p'_def and diff'_def have "p' ⊗R h = ((differ ⊕R δ) ⊗R h' ⊕R h' ⊗R (differ ⊕R δ)) ⊗R h" by simp
    also from diff_in_R and h'_in_R and h_in_R and pert_in_R
    have "… = ((differ ⊕R δ) ⊗R h') ⊗R h ⊕R (h' ⊗R (differ ⊕R δ)) ⊗R h" by algebra
    also from diff_in_R and h'_in_R and h_in_R and pert_in_R
    have "… = (differ ⊕R δ) ⊗R (h' ⊗R h) ⊕R ((h' ⊗R differ) ⊕R  (h' ⊗R δ)) ⊗R h" by algebra
    also from h'_def and diff_in_R and h'_in_R and h_in_R and pert_in_R
    have "… = (differ ⊕R δ) ⊗R (h ⊗R Φ ⊗R h) ⊕R  h' ⊗R differ ⊗R h ⊕R h' ⊗R δ ⊗R h" by algebra
    also from psi_h_h_phi h'_def and diff_in_R and h'_in_R and h_in_R and pert_in_R
    have "… = (differ ⊕R δ) ⊗R (Ψ ⊗R h ⊗R h) ⊕R h ⊗R Φ ⊗R differ ⊗R h ⊕R h ⊗R Φ ⊗R δ ⊗R h" by algebra
    also have "… =  h ⊗R Φ ⊗R differ ⊗R h ⊕R (\<one>R \<ominus>R Ψ) ⊗R h"
    proof -
      from psi_prop have "Ψ = (\<one>R \<ominus>R h ⊗R Φ ⊗R δ)" by simp
      with psi_in_R and h_in_R and phi_in_R and pert_in_R have "\<one>R \<ominus>R Ψ = \<one>R \<ominus>R (\<one>R \<ominus>R h ⊗R Φ ⊗R δ)" by algebra
      with phi_in_R and h_in_R and pert_in_R have "\<one>R \<ominus>R Ψ = h ⊗R Φ ⊗R δ" by algebra
      with diff_in_R and pert_in_R and h_in_R and psi_in_R and phi_in_R and hdh_h and h_nil and R.m_assoc [of Ψ h h]
      show ?thesis by algebra
    qed
    also from psi_h_h_phi have "… = (Ψ ⊗R h) ⊗R differ ⊗R h ⊕R (\<one>R \<ominus>R Ψ) ⊗R h" by algebra
    also from phi_in_R and h_in_R and diff_in_R have "… = Ψ ⊗R (h ⊗R differ ⊗R h) ⊕R (\<one>R \<ominus>R Ψ) ⊗R h" by (simp add: R.m_assoc)
    also from hdh_h have "… = Ψ ⊗R h ⊕R (\<one>R \<ominus>R Ψ) ⊗R h" by simp
    also from psi_in_R and h_in_R and R.l_one [OF h_in_R] have "… = h" by algebra
    finally show "p' ⊗R h = h" by simp
  qed
qed

text{*Another rewriting step that will be later used*}

lemma (in lemma_2_2_14) ph_h[simp]: shows "p ⊗R h = h" and "h ⊗R p = h"
proof -
  from p_def have "p ⊗R h = ((differ ⊗R h ⊕R h ⊗R differ) ⊗R h)" by simp
  also from diff_in_R and h_in_R and hdh_h and h_nil have "… = h" by algebra
  finally show "p ⊗R h = h" by simp
next
  from p_def have "h ⊗R p = (h ⊗R (differ ⊗R h ⊕R h ⊗R differ))" by simp
  also from diff_in_R and h_in_R have "… = h ⊗R (differ ⊗R h) ⊕R h ⊗R (h ⊗R differ)" by algebra
  also from diff_in_R and h_in_R have "… = h ⊗R differ ⊗R h ⊕R h ⊗R h ⊗R differ" by algebra
  also from h_in_R and diff_in_R and hdh_h and h_nil have "… = h" by algebra
  finally show "h ⊗R p = h" by simp
qed

subsection{*Proposition 2.2.16*}

text{*The following lemma corresponds to the @{text "Proposition 2.2.16"} as stated in Aransay's memoir*}
text{*The previous lemmas @{thm [locale=proposition_2_2_16] "hp'_h"} and @{thm [locale=lemma_2_2_14] "ph_h"} are now used*}

lemma (in proposition_2_2_16) proposition_2_2_16[simp]:
  shows h_π': "h ⊗R π' = \<zero>R" and π'_h: "π' ⊗R h = \<zero>R" and π_h': "π ⊗R h' = \<zero>R" and h'_π: "h' ⊗R π = \<zero>R"
proof -
  from π'_def and h_in_R and p'_in_R and R.r_one [OF h_in_R] and hp'_h show "h ⊗R π' = \<zero>R" by algebra
next
  from π'_def and h_in_R and p'_in_R and R.l_one [OF h_in_R] and hp'_h show "π' ⊗R h = \<zero>R" by algebra
next
  from π_def and h'_def have "π ⊗R h' = (\<one>R \<ominus>R p) ⊗R (h ⊗R Φ)" by simp
  also from p_in_R and h_in_R and phi_in_R have "… = (\<one>R \<ominus>R p) ⊗R h ⊗R Φ " by algebra
  also from ph_h and p_in_R and h_in_R and phi_in_R and R.l_one [OF h_in_R] have "… = \<zero>R" by algebra
  finally show "π ⊗R h' = \<zero>R" by simp
next
  from π_def and h'_def have "h' ⊗R π = (h ⊗R Φ) ⊗R  (\<one>R \<ominus>R p)" by simp
  also from psi_h_h_phi have "… = (Ψ ⊗R h) ⊗R (\<one>R \<ominus>R p)" by simp
  also from psi_in_R and p_in_R and h_in_R have "… = Ψ ⊗R (h ⊗R (\<one>R \<ominus>R p))" by algebra
  also from p_in_R and h_in_R and psi_in_R and ph_h and R.r_one [OF h_in_R] have "… = \<zero>R" by algebra
  finally show "h' ⊗R π = \<zero>R" by simp
qed

lemma (in proposition_2_2_16) p'_projector: shows "p' ⊗R p' = p'"
  (*In this lemma, again with the use of some automatic tool for simplifications in rings, the result could maybe be reached in a faster way*)
proof -
  from p'_def and diff'_def
  have "p' ⊗R p' = (diff' ⊗R h' ⊕R h' ⊗R diff') ⊗R (diff' ⊗R h' ⊕R h' ⊗R diff')" by simp
  also have "… = (diff' ⊗R h' ⊕R h' ⊗R diff')" (is "_ = ?d'h' ⊕R ?h'd'")
    (*In a rename command, using the … means assigning this variable to the value it has at this moment*)
  proof (rule ring.idemp_prod)
    from prems show "ring R"
      by (unfold proposition_2_2_16_def lemma_2_2_15_def lemma_2_2_14_def [of D R h] ring_endomorphisms_def, simp)
    from diff'_in_R and h'_in_R show "?d'h' ∈ carrier R" by simp
    from diff'_in_R and  h'_in_R show "?h'd' ∈ carrier R" by simp
    from diff'_in_R h'_in_R and h'd'h'_h' and R.m_assoc [of diff' h' ?d'h'] show "?d'h' ⊗R ?d'h' = ?d'h'" by algebra
    from diff'_in_R h'_in_R and h'd'h'_h' and sym [OF R.m_assoc [of diff' h' diff']] and sym [OF R.m_assoc [of h' ?d'h' diff']]
    show "?h'd' ⊗R ?h'd' = ?h'd'" by algebra
    from diff'_in_R h'_in_R and h'_nil and R.m_assoc [of diff' h' ?h'd'] and sym [OF R.m_assoc [of h' h' diff']]
    show "?d'h' ⊗R ?h'd' = \<zero>R" by algebra
    from diff'_in_R h'_in_R and R.m_assoc [of h' diff' ?d'h'] and sym [OF R.m_assoc [of diff' diff' h']]
      and ring_endomorphisms.diff_nilpot [of D' R] and ring_endomorphisms_pert [OF delta_pert] and diff'_def and D'_def
    show "?h'd' ⊗R ?d'h' = \<zero>R" by simp
  qed
  also from p'_def and diff'_def have "diff' ⊗R h' ⊕R h' ⊗R diff' = p'" by simp
  finally show ?thesis by simp
qed

text{*The following lemmas @{text "π_projector"} and @{text "π'_projector"} correspond to one of the parts of the proof of Lemma 2.2.17,
  as stated in the memoir; here they have been extracted as independent results, because later they will be used to get some other results*}

lemma (in proposition_2_2_16) π_in_R [simp]: shows "π ∈ carrier R"
  using minus_closed [OF R.one_closed p_in_R] and π_def and ring_R by simp

lemma (in proposition_2_2_16) π'_in_R [simp]: shows "π' ∈ carrier R"
  using minus_closed [OF R.one_closed p'_in_R] and π'_def and ring_R by simp

lemma (in proposition_2_2_16) π_projector: shows "π ⊗R π = π"
proof -
  from π_def and p_in_R and minus_closed [OF R.one_closed p_in_R] and r_distr [of "\<one>R" "\<ominus>R p" "\<one>R \<ominus>R p"] and a_inv_closed [OF p_in_R]
    and R.r_one [OF minus_closed [OF R.one_closed p_in_R]]
  have "π ⊗R π = (\<one>R \<ominus>R p) \<ominus>R (\<one>R \<ominus>R p) ⊗R p" by algebra
  also from p_in_R and minus_closed [OF R.one_closed p_in_R] and p_projector and l_distr [of "\<one>R" "\<ominus>R p" p] and a_inv_closed [OF p_in_R]
  and R.l_one [OF p_in_R] have "… = (\<one>R \<ominus>R p) \<ominus>R p ⊕R p" by algebra
  also from π_def and p_in_R have "… = π" by algebra
  finally show ?thesis by simp
qed

lemma (in proposition_2_2_16) π'_projector: shows "π' ⊗R π' = π'"
proof -
  from π'_def and p'_in_R and minus_closed [OF R.one_closed p'_in_R] and r_distr [of "\<one>R" "\<ominus>R p'" "\<one>R \<ominus>R p'"]
    and a_inv_closed [OF p'_in_R] and R.r_one [OF minus_closed [OF R.one_closed p'_in_R]]
  have "π' ⊗R π' = (\<one>R \<ominus>R p') \<ominus>R (\<one>R \<ominus>R p') ⊗R p'" by algebra
  also from p'_in_R and minus_closed [OF R.one_closed p'_in_R] and p'_projector and l_distr [of "\<one>R" "\<ominus>R p'" p']
    and a_inv_closed [OF p'_in_R] and R.l_one [OF p'_in_R] have "… = (\<one>R \<ominus>R p') \<ominus>R p' ⊕R p'" by algebra
  also from π'_def and p'_in_R have "… =  π'" by algebra
  finally show ?thesis by simp
qed

subsection{*Lemma 2.2.17*}

text{*@{text "Lemma 2.2.17"} proves the existence of an isomorphism between the differential
  subgroups @{term [locale=proposition_2_2_16] diff_group_im_π}
  and @{term [locale=proposition_2_2_16] diff_group_im_π'}*}
text{*The isomorphism will be explicitly given*}

text{*Lemma @{text im_π_ker_p} corresponds to the first part of the proof of Lemma 2.2.17 in Aransay's memoir; in this part, we prove both
  @{term [locale=proposition_2_2_16] "im π' = kernel D' D' p'"},
  where @{term [locale=lemma_2_2_15] D'} is the differential group perturbed, i.e.,
  @{term [locale=lemma_2_2_15] "D' = (| carrier = carrier D, mult = mult D, one = one D , diff = differ ⊕R δ|)),"},
  and also @{term [locale=proposition_2_2_16] "im π = kernel D D p"}*}

text{*The reason to prove these equalities between sets is that later, it will be easier to prove the existence of an isomorphism
  between @{term [locale=proposition_2_2_16] diff_group_im_π}
  and @{term [locale=proposition_2_2_16] diff_group_im_π'} than between the kernel sets*}

text{*The two following proofs in lemma @{text im_π_ker_p} are quite similar, but maybe trying to extract the common parts and obtaining
  both goals just by instantiation of the obtained common lemma would have been even, at least, longer*}

lemma (in proposition_2_2_16) im_π_ker_p: shows "image π (carrier D) = kernel D D p" and "image π' (carrier D') = kernel D' D' p'"
proof -
  show "image π (carrier D) = kernel D D p"
  proof (intro equalityI)
    show "π ` carrier D ≤ kernel D D p"
    proof
      fix x
      assume x: "x ∈ π ` carrier D" then obtain y where y: "y ∈ carrier D" and π_y: "π (y) = x" by auto
      show "x ∈ kernel D D p"
      proof (unfold kernel_def, auto)
        from π_in_R and ring_R have "π ∈ hom_completion D D" by simp
        with hom_completion_closed [OF _ y, of π D ] and π_y show "x ∈ carrier D" by simp
      next
          (*The following is a nice example of a guided proof; on it, we have to turn p (x) into p (π y), unfold p (π y) into
          p (p (π y) ⊗ π (π y)), then turn into p (p (π y) ⊗ p (π (π y))), this into p (π y) ⊗ p (π y), and finally arrive at \<one>D*)
          (*I guess this would be quite complicated just automatically*)
        from π_y have "p x = p (π y)" by simp
        also have "… = p (p (π y) ⊗ π (π y))"
        proof -
          from π_def and p_in_R have "\<one>R = p ⊕R π" by algebra
          then have "\<one>R (π y) = (p ⊕R π) (π y)" by simp
          with y and hom_completion_closed [OF _ y, of π D ] and ring_R and π_in_R have "π y = p (π y) ⊗ π (π y)" by simp
          then show ?thesis by simp
        qed
        also from ring_R and y and p_in_R π_in_R and hom_completion_mult [of p D D "p (π y) " "π (π y)"]
          and hom_completion_closed [of π D D y] and hom_completion_closed [of p D D "π y"] and hom_completion_closed [of π D D "π y"]
        have "… = p (p (π y)) ⊗ p (π (π y))" by simp
        also from ring_R and p_projector and π_projector have "… = p (π y) ⊗ p (π y)" by (simp add: expand_fun_eq)
        also have "… = \<one>D"
        proof -
          from π_def and p_in_R and p_projector and R.r_one [OF p_in_R] have "p ⊗R π = \<zero>R" by algebra
          with ring_R and y have "p (π y) = \<one>D" by (simp add: expand_fun_eq)
          then show ?thesis by simp
        qed
        finally show "p x = \<one>D" by simp
      qed
    qed
    show "kernel D D p ≤ π ` carrier D"
    proof (unfold image_def, auto)
      fix x assume x: "x ∈ kernel D D p" then have x_in_D: "x ∈ carrier D" by (unfold kernel_def, simp)
      from π_def and p_in_R have "\<one>R = π ⊕R p" by algebra
      then have "\<one>R x = (π ⊕R p) x" by simp (*Why this simplification step can not be joined with the following one?*)
      with x_in_D and ring_R have "x = π x ⊗D p x" by (simp add: expand_fun_eq)
      with ring_R π_in_R and hom_completion_closed [of π D D x] and x and D.r_one [of "π x"] have "x = π x" by (unfold kernel_def, simp)
      with x_in_D show "∃y∈carrier D. x = π y" by auto
    qed
  qed
next
  show "π' ` carrier D' = kernel D' D' p'"
  proof (intro equalityI)
    show "π' ` carrier D' ≤ kernel D' D' p'"
    proof
      fix x
      assume x: "x ∈ π' ` carrier D'" then obtain y where y: "y ∈ carrier D'" and π'_y: "π' (y) = x" by auto
      show "x ∈ kernel D' D' p'"
      proof (unfold D'_def kernel_def, auto)
        from π'_in_R and ring_R have "π' ∈ hom_completion D D" by simp
        with y and hom_completion_closed [of π' D D y] and π'_y and D'_def show "x ∈ carrier D" by simp
      next
        from π'_y have "p' x = p' (π' y)" by simp
        also have "… = p' (p' (π' y) ⊗ π' (π' y))"
        proof -
          from π'_def and p'_in_R have "\<one>R = p' ⊕R π'" by algebra
          then have "\<one>R (π' y) = (p' ⊕R π') (π' y)" by simp
          with y and D'_def and hom_completion_closed [of π' D D y] and ring_R and π'_in_R have "π' y = p' (π' y) ⊗ π' (π' y)" by simp
          then show ?thesis by simp
        qed
        also from ring_R and y and D'_def and p'_in_R π'_in_R and hom_completion_mult [of p' D D "p' (π' y) " "π' (π' y)"]
          and hom_completion_closed [of π' D D y] and hom_completion_closed [of p' D D "π' y"]
          and hom_completion_closed [of π' D D "π' y"]
        have "… = p' (p' (π' y)) ⊗ p' (π' (π' y))" by simp
        also from ring_R and p'_projector and π'_projector have "… = p' (π' y) ⊗ p' (π' y)" by (simp add: expand_fun_eq)
        also have "… = \<one>D"
        proof -
          from π'_def and p'_in_R and p'_projector and R.r_one [OF p'_in_R] have "p' ⊗R π' = \<zero>R" by algebra
          with ring_R and y and D'_def have "p' (π' y) = \<one>D" by (simp add: expand_fun_eq)
          then show ?thesis by simp
        qed
        finally show "p' x = \<one>D" by simp
      qed
    qed
    show "kernel D' D' p' ≤ π' ` carrier D'"
    proof (unfold image_def, auto)
      fix x assume x: "x ∈ kernel D' D' p'" then have x_in_D: "x ∈ carrier D" by (unfold kernel_def D'_def, simp)
      from π'_def and p'_in_R have "\<one>R = π' ⊕R p'" by algebra
      then have "\<one>R x =  (π' ⊕R p') x" by simp
      with x_in_D and ring_R have "x = π' x ⊗D p' x" by (simp add: expand_fun_eq)
      with ring_R and π'_in_R and hom_completion_closed [of π' D D x] and x and D.r_one [of "π' x"] have "x = π' x"
        by (unfold kernel_def D'_def, simp)
      with x_in_D and D'_def show "∃y∈carrier D'. x = π' y" by auto
    qed
  qed
qed

text{*The following definition is similar to the one of isomorphism given in Isabelle, but here we add the premise that
  the homomorphism has to be also a completion. This is mainly to keep the coherence with the previous work*}

constdefs
  iso_compl :: "_ => _ => ('a => 'b) set"  (infixr "≅compl" 60)
  "D ≅compl C == {h. h ∈ hom_completion D C & bij_betw h (carrier D) (carrier C)}"

text{*The following is an introduction lemma for isomorphisms between groups; maybe it could be introduced in the @{text "Group.thy"} file,
  avoiding the premise on completions!!*}

lemma iso_complI: assumes closed: "!!x. x ∈ carrier D ==> h x ∈ carrier C"
  and mult: "!!x y. [|x ∈ carrier D; y ∈ carrier D|] ==> h (x ⊗D y) = h x ⊗C h y"
  and complect: "∃g. h = (λx. if x ∈ carrier D then g x else \<one>C)"
  and inj_on: "!!x y. [| x ∈ carrier D;  y ∈ carrier D;  h (x) = h (y) |] ==> x=y"
  and image: "!!y. y∈carrier C ==> ∃x ∈ carrier D. y = h (x)"
  shows "h ∈ D ≅compl C"
  using prems by (unfold iso_compl_def hom_completion_def hom_def Pi_def
    completion_fun2_def completion_def bij_betw_def inj_on_def image_def expand_fun_eq, auto)

text{*Lemmas @{text "ππ'π_π"} and @{text "π'ππ'_π"} have been also extracted from the proof of @{text "Lemma 2.2.17"} as stated in the memoir*}text{*They are used in order to prove injectivity and surjection of @{term [locale=proposition_2_2_16] π} and
  @{term [locale=proposition_2_2_16] π'}*}

lemma (in proposition_2_2_16) ππ'π_π: shows "π ⊗R π' ⊗R π = π"
proof -
  from π'_def have "π ⊗R π' ⊗R π = π ⊗R (\<one>R \<ominus>R p') ⊗R π" by simp
  also from π'_in_R π_in_R p'_in_R R.r_one [OF π_in_R] have "… = (π \<ominus>R π ⊗R  p') ⊗R π" by algebra
  also from π'_in_R π_in_R p'_in_R and π_projector have "… = π \<ominus>R π ⊗R  p' ⊗R π" by algebra
  also from p'_def have "… = π \<ominus>R π ⊗R ((differ ⊕R δ) ⊗R h' ⊕R h' ⊗R (differ ⊕R δ)) ⊗R π"
    (is "_ = π \<ominus>R π ⊗R (?diff' ⊗R h' ⊕R h' ⊗R ?diff') ⊗R π") by simp
  also from π_in_R and diff_pert_in_R [OF delta_pert] and h'_in_R and sym [OF R.m_assoc [of π h' ?diff']]
  have "… = π \<ominus>R (π ⊗R (?diff' ⊗R h') ⊕R π ⊗R h' ⊗R ?diff') ⊗R π" by algebra
  also from proposition_2_2_16 and π_in_R and diff_pert_in_R [OF delta_pert] and h'_in_R
  have "… = π \<ominus>R (π ⊗R (?diff' ⊗R h')) ⊗R π" by algebra
  also from π_in_R and diff_pert_in_R [OF delta_pert] and h'_in_R and R.m_assoc [of π "?diff' ⊗R h'" π] and R.m_assoc [of ?diff' h' π]
    and proposition_2_2_16 have "… = π" by algebra
  finally show "π ⊗R π' ⊗R π = π" by simp
qed

lemma (in proposition_2_2_16) π'ππ'_π': shows "π' ⊗R π ⊗R π' = π'"
proof -
  from π_def have "π' ⊗R π ⊗R π' = π' ⊗R (\<one>R \<ominus>R p) ⊗R π'" by simp
  also from π'_in_R π_in_R p_in_R R.r_one [OF π'_in_R] have "… = (π' \<ominus>R π' ⊗R  p) ⊗R π'" by algebra
  also from π'_in_R π_in_R p_in_R and π'_projector have "… = π' \<ominus>R π' ⊗R  p ⊗R π'" by algebra
  also from p_def have "… = π' \<ominus>R π' ⊗R (differ ⊗R h ⊕R h ⊗R differ) ⊗R π'" by simp
  also from π'_in_R and diff_in_R and h_in_R and sym [OF R.m_assoc [of π' h differ]]
  have "… = π' \<ominus>R (π' ⊗R (differ ⊗R h) ⊕R π' ⊗R h ⊗R differ) ⊗R π'" by algebra
  also from proposition_2_2_16 and π'_in_R and diff_in_R and h_in_R have "… = π' \<ominus>R (π' ⊗R (differ ⊗R h)) ⊗R π'" by algebra
  also from π'_in_R and diff_in_R and h_in_R and R.m_assoc [of π' "differ ⊗R h" π'] and R.m_assoc [of differ h π'] and proposition_2_2_16
  have "… = π'" by algebra
  finally show "π' ⊗R π ⊗R π' = π'" by simp
qed

text{*The following locale definition only introduces some new definitions of constants; they will improve the presentation of the results*}

locale lemma_2_2_17 = proposition_2_2_16

definition (in lemma_2_2_17)
  im_π where "im_π == image π (carrier D)"
definition (in lemma_2_2_17)
  im_π' where "im_π' == image π' (carrier D')"
definition (in lemma_2_2_17)
  diff_group_im_π where "diff_group_im_π == (|carrier = image π (carrier D), mult = mult D, one = one D,
  diff = completion (|carrier = image π (carrier D), mult = mult D, one = one D, diff = diff D|)), D (diff D)|)),"
definition (in lemma_2_2_17)
  diff_group_im_π' where "diff_group_im_π' == (|carrier = image π' (carrier D'), mult = mult D, one = one D,
  diff = completion (|carrier = image π' (carrier D'), mult = mult D, one = one D, diff = (differ ⊕R δ)|)),
  (|carrier = carrier D, mult = mult D, one = one D, diff = (differ ⊕R δ)|)), (differ ⊕R δ)|)),"
definition (in lemma_2_2_17)
  diff_im_π_def: "diff_im_π == completion (|carrier = image π (carrier D), mult = mult D, one = one D, diff = diff D|)), D (diff D)"
definition (in lemma_2_2_17)
  diff_im_π'_def: "diff_im_π' == completion (|carrier = image π' (carrier D'), mult = mult D, one = one D,
  diff =(differ ⊕R δ) |)), (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)), (differ ⊕R δ)"
definition (in lemma_2_2_17)
  τ where "τ == completion
  (| carrier = image π (carrier D), mult = mult D, one = one D,
  diff = completion (|carrier = image π (carrier D), mult = mult D, one = one D, diff = diff D|)), D (diff D)|)),
  (|carrier = image π' (carrier D'), mult = mult D, one = one D,
  diff = completion (|carrier = image π' (carrier D'), mult = mult D, one = one D, diff = differ ⊕R δ|)),
  (|carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)), (differ ⊕R δ) |)), π'"
text{*The following definition of @{term τ'} corresponds to the inverse of @{term τ}*}
definition (in lemma_2_2_17)
  τ'  where "τ' == completion
  (|carrier = image π' (carrier D'), mult = mult D, one = one D,
  diff = completion (|carrier = image π' (carrier D'), mult = mult D, one = one D, diff = differ ⊕R δ|)),
  (|carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)), (differ ⊕R δ) |)),
  (| carrier = image π (carrier D), mult = mult D, one = one D,
  diff = completion (|carrier = image π (carrier D), mult = mult D, one = one D, diff = diff D|)), D (diff D)|)), π"

text{*As with @{text "Lemma 2.2.14"}, we divide the proof of @{text "Lemma 2.2.17"} in four parts.
  First we prove that there are two homomorphisms, one in each direction, satisfying that they are isomorphisms.
  Then, in other two lemmas, we prove that their compositions, also in both directions, are equal to the corresponding identities*}

lemma (in lemma_2_2_17) lemma_2_2_17_first_part: shows "τ ∈ (diff_group_im_π ≅compl diff_group_im_π')"
proof (intro iso_complI)
  fix x assume "x ∈ carrier diff_group_im_π" then have x: "x ∈ π` (carrier D)" by (unfold diff_group_im_π_def, simp)
  then obtain y where y: "y ∈ carrier D" and π_y: "π y = x" by auto
  with ring_R and π_in_R π'_in_R and hom_completion_closed [of π D D y] hom_completion_closed [of π' D D "π y"]
  have "π' x ∈ π' ` carrier D" by (unfold image_def, auto)
  with diff_group_im_π'_def and τ_def and x and D'_def
  show "τ x ∈ carrier diff_group_im_π'" by (unfold completion_def image_def, auto)
next
  fix x y assume "x ∈ carrier diff_group_im_π" and "y ∈ carrier diff_group_im_π"
  then have x: "x ∈ π` (carrier D)" and y: "y ∈ π` (carrier D)" by (unfold diff_group_im_π_def, simp_all)
  then obtain x' y' where x': "x' ∈ carrier D" and y': "y' ∈ carrier D" and π_x': "π x' = x" and π_y': "π y' = y" by auto
  with ring_R and π'_in_R and π_in_R and hom_completion_closed [of π D D x']  hom_completion_closed [of π D D y']
    and D.m_closed [of "(π x')" "(π y')"] and hom_completion_mult [of π' D D x y] and x y and sym [OF hom_completion_mult [of π D D x' y']]
    and τ_def and diff_group_im_π_def and diff_group_im_π'_def
  show "τ (x ⊗diff_group_im_π y) = τ x ⊗diff_group_im_π' τ y" by (unfold completion_def, simp)
next
  from exI [of _ τ] show "∃g. τ = (λx. if x ∈ carrier diff_group_im_π then g x else \<one>diff_group_im_π')"
    by (unfold τ_def diff_group_im_π_def diff_group_im_π'_def completion_def, auto)
next
  fix x y assume "x ∈ carrier diff_group_im_π" and "y ∈ carrier diff_group_im_π" and τ_eq: "τ x = τ y"
  then have x: "x ∈ π` (carrier D)" and y: "y ∈ π` (carrier D)" by (unfold diff_group_im_π_def, simp_all)
  then obtain x' y' where x': "x' ∈ carrier D" and y': "y' ∈ carrier D" and π_x': "π x' = x" and π_y': "π y' = y" by auto
  with τ_eq and x y have "π' (π x') = π' (π y')" by (unfold τ_def completion_def image_def, auto)
  then have "π (π' (π x')) = π (π' (π y'))" by simp
  with ring_R and π_in_R and π'_in_R and ππ'π_π have "π x' = π y'" by (simp add: expand_fun_eq)
  with π_x' and π_y' show "x = y" by simp
next
  fix y assume "y ∈ carrier diff_group_im_π'"
  then have "y ∈ π' ` (carrier D')" by (unfold diff_group_im_π'_def, simp)
  with D'_def obtain y' where y': "y' ∈ carrier D" and π'_y': "π' y' = y" by auto
  with π'ππ'_π' and ring_R and π_in_R and π'_in_R have "π' (π (π' y')) = π' y'" by (auto simp add: expand_fun_eq)
  with π'_y' and y' and ring_R π_in_R π'_in_R and hom_completion_closed [of π' D D y'] hom_completion_closed [of π D D "π' y'"]
  have "π' (π y) = y" and "π y ∈ π` (carrier D)" by (unfold image_def, auto)
  with diff_group_im_π_def τ_def show "∃x∈carrier diff_group_im_π. y = τ x" by (unfold completion_def, auto)
qed

    (* The following is just an example of the previous statements of the lemmas, before making use of the locales for abbreviations
    lemma (in lemma_2_2_16) lemma_2_2_17_first_part: shows "completion ((| carrier = image π (carrier D),
    mult = mult D, one = one D, diff = completion (D(|carrier :=(kernel D D p)|)),) D (diff D)|)),)
    ((|carrier = image π' (carrier (D(|diff := differ ⊕R δ|)),)), mult = op ⊗D(|diff := differ ⊕R δ|)),,
    one = \<one>D(|diff := differ ⊕R δ|)),,
    diff = completion (D(|diff := differ ⊕R δ, carrier := kernel (D(|diff := differ ⊕R δ|)),) (D(|diff := differ ⊕R δ|)),) p'|)),)
    (D(|diff := differ ⊕R δ|)),) (differD(|diff := differ ⊕R δ|)),)|)),)
    π' ∈
    ( (| carrier = image π (carrier D),
    mult = mult D, one = one D, diff = completion (D(|carrier :=(kernel D D p)|)),) D (diff D)|)),  ≅compl
    (|carrier = image π' (carrier (D(|diff := differ ⊕R δ|)),)), mult = op ⊗D(|diff := differ ⊕R δ|)),,
    one = \<one>D(|diff := differ ⊕R δ|)),,
    diff = completion (D(|diff := differ ⊕R δ, carrier := kernel (D(|diff := differ ⊕R δ|)),) (D(|diff := differ ⊕R δ|)),) p'|)),)
    (D(|diff := differ ⊕R δ|)),) (differD(|diff := differ ⊕R δ|)),)|)), )"
    (is "completion ((|carrier = ?im_π, mult = mult D, one = one D , diff = ?compl_diff|)),)
    ((|carrier = ?im_π', mult = op ⊗D(|diff := differ ⊕R δ|)),,
    one = \<one>D(|diff := differ ⊕R δ|)), , diff = ?compl_diff'|)),) π'
    ∈ ( (|carrier = ?im_π, mult = mult D, one = one D , diff = ?compl_diff|)),
    ≅compl (|carrier = ?im_π', mult = op ⊗D(|diff := differ ⊕R δ|)),,
    one = \<one>D(|diff := differ ⊕R δ|)), , diff = ?compl_diff'|)),)"
    is "?compl_π' ∈ (?IM_π ≅compl ?IM_π')")
    *)

text{*@{text lemma_2_2_17_second_part} proves that @{term [locale=lemma_2_2_17] "τ' ∈ (diff_group_im_π' ≅compl diff_group_im_π)"}*}

lemma (in lemma_2_2_17) lemma_2_2_17_second_part: shows "τ' ∈ (diff_group_im_π' ≅compl diff_group_im_π)"
  (is "τ' ∈ (?IM_π' ≅compl ?IM_π)")
proof (intro iso_complI)
  fix x assume "x ∈ carrier ?IM_π'" with diff_group_im_π'_def have x: "x ∈ π' ` carrier D'" by simp
  with D'_def obtain y where y: "y ∈ carrier D" and π_y: "π' y = x" by auto
  with ring_R and π_in_R π'_in_R and hom_completion_closed [of π' D D y] hom_completion_closed [of π D D "π' y"]
  have "π x ∈ π ` carrier D" by (unfold image_def, auto)
  with diff_group_im_π_def and τ'_def and x
  show "τ' x ∈ carrier diff_group_im_π" by (unfold completion_def image_def, auto)
next
  fix x y assume "x ∈ carrier ?IM_π'" and "y ∈ carrier ?IM_π'"
  then have x: "x ∈ π' ` (carrier D')" and y: "y ∈ π' ` (carrier D')" by (unfold diff_group_im_π'_def, simp_all)
  with D'_def obtain x' y' where x': "x' ∈ carrier D" and y': "y' ∈ carrier D" and π_x': "π' x' = x" and π_y': "π' y' = y" by auto
  with ring_R and π'_in_R and π_in_R and hom_completion_closed [of π' D D x']  hom_completion_closed [of π' D D y']
    and D.m_closed [of "π' x'" "π' y'"] and hom_completion_mult [of π D D x y] and x y and sym [OF hom_completion_mult [of π' D D x' y']]
    and τ'_def and diff_group_im_π_def diff_group_im_π'_def and D'_def
  show "τ' (x ⊗?IM_π' y) = τ' x ⊗?IM_π τ' y" by (unfold completion_def, simp)
next
  from exI [of _ τ'] show "∃g. τ' = (λx. if x ∈ carrier diff_group_im_π' then g x else \<one>diff_group_im_π)"
    by (unfold τ'_def diff_group_im_π_def diff_group_im_π'_def completion_def, auto)
next
  fix x y assume "x ∈ carrier diff_group_im_π'" and "y ∈ carrier diff_group_im_π'" and τ'_eq: "τ' x = τ' y"
  then have x: "x ∈ π'` (carrier D')" and y: "y ∈ π'` (carrier D')" by (unfold diff_group_im_π'_def, simp_all)
  with D'_def obtain x' y' where x': "x' ∈ carrier D" and y': "y' ∈ carrier D" and π'_x': "π' x' = x" and π'_y': "π' y' = y" by auto
  with τ'_eq and x y have "π (π' x') = π (π' y')" by (unfold τ'_def completion_def image_def, auto)
  then have "π' (π (π' x')) = π' (π (π' y'))" by simp
  with ring_R and π_in_R and π'_in_R and π'ππ'_π' have "π' x' = π' y'" by (simp add: expand_fun_eq)
  with π'_x' and π'_y' show "x = y" by simp
next
  fix y assume "y ∈ carrier ?IM_π"
  then have "y ∈ π ` (carrier D)" by (unfold diff_group_im_π_def, simp)
  then obtain y' where y': "y' ∈ carrier D" and π_y': "π y' = y" by auto
  with ππ'π_π and ring_R and π_in_R and π'_in_R have "π (π' (π y')) = π y'" by (auto simp add: expand_fun_eq)
  with π_y' and y' and ring_R π_in_R π'_in_R and hom_completion_closed [of π D D y'] hom_completion_closed [of π' D D "π y'"]
  and D'_def have "π (π' y) = y" and "π' y ∈ π'` (carrier D')" by (unfold image_def, auto)
  with diff_group_im_π'_def τ'_def show "∃x∈carrier diff_group_im_π'. y = τ' x" by (unfold completion_def, auto)
qed

    (* This was the previous statement:
    lemma (in lemma_2_2_16) lemma_2_2_17_second_part: shows "completion  ((|carrier = image π' (carrier (D(|diff := differ ⊕R δ|)),)),
    mult = op ⊗D(|diff := differ ⊕R δ|)),,
    one = \<one>D(|diff := differ ⊕R δ|)),,
    diff = completion (D(|diff := differ ⊕R δ, carrier := kernel (D(|diff := differ ⊕R δ|)),) (D(|diff := differ ⊕R δ|)),) p'|)),)
    (D(|diff := differ ⊕R δ|)),) (differD(|diff := differ ⊕R δ|)),)|)),)
    ((| carrier = image π (carrier D),
    mult = mult D, one = one D, diff = completion (D(|carrier :=(kernel D D p)|)),) D (diff D)|)),)
    π ∈
    ( (|carrier = image π' (carrier (D(|diff := differ ⊕R δ|)),)), mult = op ⊗D(|diff := differ ⊕R δ|)),,
    one = \<one>D(|diff := differ ⊕R δ|)),,
    diff = completion (D(|diff := differ ⊕R δ, carrier := kernel (D(|diff := differ ⊕R δ|)),) (D(|diff := differ ⊕R δ|)),) p'|)),)
    (D(|diff := differ ⊕R δ|)),) (differD(|diff := differ ⊕R δ|)),)|)),
    ≅compl (| carrier = image π (carrier D),
    mult = mult D, one = one D, diff = completion (D(|carrier :=(kernel D D p)|)),) D (diff D)|)), )"
    (is "completion ((|carrier = ?im_π', mult = op ⊗D(|diff := differ ⊕R δ|)),,
    one = \<one>D(|diff := differ ⊕R δ|)), , diff = ?compl_diff'|)),) ((|carrier = ?im_π, mult = mult D, one = one D , diff = ?compl_diff|)),)
    π
    ∈ ( (|carrier = ?im_π', mult = op ⊗D(|diff := differ ⊕R δ|)),,
    one = \<one>D(|diff := differ ⊕R δ|)), , diff = ?compl_diff'|)), ≅compl
    (|carrier = ?im_π, mult = mult D, one = one D , diff = ?compl_diff|)),)"
    is "?compl_π ∈ (?IM_π' ≅compl ?IM_π)")
    *)

text{*In @{text lemma_2_2_17_first_part} and @{text lemma_2_2_17_second_part} we have proved the isomorphism between
  @{term [locale=lemma_2_2_17] diff_group_im_π} and @{term [locale=lemma_2_2_17] diff_group_im_π'};
  now, with the help of @{thm  [locale=proposition_2_2_16] im_π_ker_p}, where we have proved both that
  @{term [locale=lemma_2_2_17] "im π = ker p"} and also that @{term [locale=lemma_2_2_17] "im π' = ker p'"},
  we prove that @{term [locale=lemma_2_2_17] "ker p"} and @{term [locale=lemma_2_2_17] "ker p'"} are also isomorphic.
  Then we obtain the statement as it is presented in @{text "Lemma 2.2.17"} in Aransay's memoir*}

lemma (in lemma_2_2_17) lemma_2_2_17_kernel: shows "τ ∈ (diff_group_ker_p ≅compl diff_group_ker_p')"
  and "τ' ∈ (diff_group_ker_p' ≅compl diff_group_ker_p)"
  using diff_group_ker_p_def diff_group_ker_p'_def diff_group_im_π_def diff_group_im_π'_def im_π_ker_p
    and lemma_2_2_17_first_part lemma_2_2_17_second_part and D'_def by simp_all

(*The following proof is again done over the image sets, and then transferred to the kernels*)
(*When using the image sets, we can make use of the properties ππ'π_π and π'ππ'_π'*)

lemma (in lemma_2_2_17) lemma_2_2_17_third_part:
  shows "τ o τ' = (λx. if x ∈ carrier diff_group_im_π' then id x else \<one>diff_group_im_π')"
  (is "τ o τ'  = ?id_image_π'")
proof (rule ext)
  fix x
  show "(τ o τ') x = ?id_image_π' x"
  proof (cases "x ∈ carrier diff_group_im_π'")
    case True with diff_group_im_π'_def and D'_def have x: "x ∈ π'`(carrier D)" by simp
    then obtain y where y: "y ∈ carrier D" and π'_y: "π' y = x" by auto
    with x and τ'_def and D'_def have "(τ o τ') x = τ (π (π' y))" by (unfold completion_def, simp)
    also from τ_def and π'_in_R and ring_R hom_completion_closed [of π' D D y] and y and imageI [of "π' y" "carrier D" π]
    have "… = π' (π (π' y))" by (unfold completion_def, simp)
    also with π'ππ'_π' and π_in_R and π'_in_R and ring_R have "… = π' y" by (unfold expand_fun_eq, simp)
    also with π'_y and True have "… = ?id_image_π' x" by simp
    finally show "(τ o τ') x = ?id_image_π' x" by simp
  next
    case False with τ'_def and diff_group_im_π'_def have "(τ o τ') x = τ \<one>" by (unfold completion_def, simp)
    also from τ_def group_hom.hom_one [of D D π] and π_in_R and π'_in_R and ring_R and imageI [OF D.one_closed, of π]
      and group_hom.hom_one [of D D π'] and D_diff_group have "… = \<one>"
      by (unfold group_hom_def group_hom_axioms_def diff_group_def comm_group_def group_def hom_completion_def completion_def, simp)
    also from False and diff_group_im_π'_def have "… = ?id_image_π' x" by simp
    finally show "(τ o τ') x = ?id_image_π' x" by simp
  qed
qed

lemma (in lemma_2_2_17) lemma_2_2_17_fourth_part:
  shows "τ' o τ = (λx. if x ∈ carrier diff_group_im_π then id x else \<one>diff_group_im_π)"
  (is "τ' o τ  = ?id_image_π")
proof (rule ext)
  fix x
  show "(τ' o τ) x = ?id_image_π x"
  proof (cases "x ∈ carrier diff_group_im_π")
    case True with diff_group_im_π_def have x: "x ∈ π` (carrier D)" by simp
    then obtain y where y: "y ∈ carrier D" and π_y: "π y = x" by auto
    with x and τ_def have "(τ' o τ) x = τ' (π' (π y))" by simp
    also from τ'_def and D'_def and π_in_R and ring_R hom_completion_closed [of π D D y] and y and imageI [of "π y" "carrier D" π']
    have "… = π (π' (π y))" by (unfold completion_def, simp)
    also with ππ'π_π and π_in_R and π'_in_R and ring_R have "… = π y" by (unfold expand_fun_eq, simp)
    also with π_y and True have "… = ?id_image_π x" by simp
    finally show "(τ' o τ) x = ?id_image_π x" by simp
  next
    case False with τ_def and diff_group_im_π_def have "(τ' o τ) x = τ' \<one>" by (unfold completion_def, simp)
    also from τ'_def and group_hom.hom_one [of D D π'] and π'_in_R and π_in_R and ring_R and imageI [OF D.one_closed, of π']
      and group_hom.hom_one [of D D π] D_diff_group and prems have "… = \<one>"
      by (unfold group_hom_def group_hom_axioms_def diff_group_def comm_group_def group_def hom_completion_def completion_def, simp)
    also from False and diff_group_im_π_def have "… = ?id_image_π x" by simp
    finally show "(τ' o τ) x = ?id_image_π x" by simp
  qed
qed

text{*In the following lemma, again we transfer the result obtained in @{thm [locale=lemma_2_2_17] lemma_2_2_17_third_part} and
  @{thm [locale=lemma_2_2_17] lemma_2_2_17_fourth_part} from the image sets to the kernel sets*}

lemma (in lemma_2_2_17) lemma_2_2_17_identities: shows "τ' o τ = (λx. if x ∈ carrier diff_group_ker_p then id x else \<one>diff_group_ker_p)"
  and "τ o τ' = (λx. if x ∈ carrier diff_group_ker_p' then id x else \<one>diff_group_ker_p')"
  using diff_group_ker_p_def diff_group_ker_p'_def diff_group_im_π_def diff_group_im_π'_def im_π_ker_p D'_def
    and lemma_2_2_17_third_part lemma_2_2_17_fourth_part by (simp_all add: expand_fun_eq)

text{*We now define what we consider inverse isomorphisms between differential groups (actually the definition also holds for monoids)
  by means of homomorphism*}
text{*The previous definition, @{term "op ≅invdiff"}, defined an isomorphism by means of \emph{differential} homomorphisms*}

constdefs
  iso_inv_compl :: "('a, 'c) monoid_scheme => ('b, 'd) monoid_scheme => (('a => 'b) × ('b => 'a)) set"  (infixr "≅invcompl" 60)
  "D ≅invcompl C == {(f, g). f ∈ (D ≅compl C) & g ∈ (C ≅compl D) & (f o g = completion C C id) & (g o f = completion D D id)}"

lemma iso_inv_complI: assumes f: "f ∈ (D ≅compl C)" and g: "g ∈ (C ≅compl D)" and fg_id: "(f o g = completion C C id)"
  and gf_id: "(g o f = completion D D id)" shows "(f, g) ∈ (D ≅invcompl C)"
  using f g fg_id gf_id by (unfold iso_inv_compl_def, simp)

lemma iso_inv_diff_impl_iso_inv_compl: assumes f_g: "(f, g) ∈ (D ≅invdiff C)" shows "(f, g) ∈ (D ≅invcompl C)"
  using f_g by (unfold iso_inv_diff_def iso_diff_def iso_inv_compl_def iso_compl_def hom_diff_def hom_completion_def) auto

lemma iso_inv_compl_iso_compl: assumes f_f': "(f, f') ∈ (D ≅invcompl C)" shows "f ∈ (D ≅compl C)"
  using f_f' by (unfold iso_inv_compl_def, simp)

lemma iso_inv_compl_iso_compl2: assumes f_f': "(f, f') ∈ (D ≅invcompl C)" shows "f' ∈ (C ≅compl D)"
  using f_f' by (unfold iso_inv_compl_def, simp)

lemma iso_inv_compl_id: assumes f_f': "(f, f') ∈ (D ≅invcompl C)" shows "f' o f = completion D D id"
  using f_f' by (unfold iso_inv_compl_def, simp)

lemma iso_inv_compl_id2: assumes f_f': "(f, f') ∈ (D ≅invcompl C)" shows "f o f' = completion C C id"
  using f_f' by (unfold iso_inv_compl_def, simp)

lemma (in lemma_2_2_17) lemma_2_2_17: shows "(τ, τ') ∈ (diff_group_ker_p ≅invcompl diff_group_ker_p')"
  using lemma_2_2_17_identities and lemma_2_2_17_kernel and iso_inv_complI by (unfold completion_def, auto)

end