Theory Localization_Ring.Localization

theory Localization
  imports Main "HOL-Algebra.Group" "HOL-Algebra.Ring" "HOL-Algebra.AbelCoset"
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents: 
▪ We define the localization of a commutative ring R with respect to a multiplicative subset, 
i.e. with respect to a submonoid of R (seen as a multiplicative monoid), cf. [‹rec_rng_of_frac›]. 
▪ We prove that this localization is a commutative ring (cf. [‹crng_rng_of_frac›]) equipped with a 
homomorphism of rings from R (cf. [‹rng_to_rng_of_frac_is_ring_hom›]).
›

section ‹The Localization of a Commutative Ring›

subsection ‹Localization›

locale submonoid = monoid M for M (structure) +
  fixes S
  assumes subset : "S ⊆ carrier M"
    and m_closed [intro, simp] : "⟦x ∈ S; y ∈ S⟧ ⟹ x ⊗ y ∈ S"
    and one_closed [simp] : "𝟭 ∈ S"

lemma (in submonoid) is_submonoid: "submonoid M S"
  by (rule submonoid_axioms)

locale mult_submonoid_of_rng = ring R + submonoid R S for R and S

locale mult_submonoid_of_crng = cring R + mult_submonoid_of_rng R S for R and S

locale eq_obj_rng_of_frac = cring R + mult_submonoid_of_crng R S for R (structure) and S +
  fixes rel
  defines "rel ≡ ⦇carrier = carrier R × S, eq = λ(r,s) (r',s'). ∃t∈S. t ⊗ ((s'⊗ r) ⊖ (s ⊗ r')) = 𝟬⦈"

lemma (in abelian_group) minus_to_eq :
  assumes "abelian_group G" and "x ∈ carrier G" and "y ∈ carrier G" and "x ⊖ y = 𝟬"
  shows "x = y"
  by (metis add.inv_solve_right assms(2) assms(3) assms(4) l_zero minus_eq zero_closed)

lemma (in eq_obj_rng_of_frac) equiv_obj_rng_of_frac:
  shows "equivalence rel"
proof
  show "⋀x. x ∈ carrier rel ⟹ x .=⇘rel⇙ x"
  proof-
    fix x
    assume "x ∈ carrier rel"
    then have f1:"𝟭 ⊗ ((snd x ⊗ fst x) ⊖ (snd x ⊗ fst x)) = 𝟬"
      using rel_def subset l_one minus_eq add.r_inv rev_subsetD 
      by auto
    moreover have "x = (fst x, snd x)"
      by simp
    thus "x .=⇘rel⇙ x" 
      using rel_def one_closed f1 
      by auto
  qed
  show "⋀x y. x .=⇘rel⇙ y ⟹ x ∈ carrier rel ⟹ y ∈ carrier rel ⟹ y .=⇘rel⇙ x"
  proof-
    fix x y
    assume a1:"x .=⇘rel⇙ y" and a2:"x ∈ carrier rel" and a3:"y ∈ carrier rel"
    then obtain t where f1:"t ∈ S" and f2:"t ⊗ ((snd y ⊗ fst x) ⊖ (snd x ⊗ fst y)) = 𝟬"
      using rel_def 
      by fastforce
    then have "(snd x ⊗ fst y) ⊖ (snd y ⊗ fst x) = ⊖ ((snd y ⊗ fst x) ⊖ (snd x ⊗ fst y))"
      using abelian_group.minus_add abelian_group.minus_minus
      by (smt a2 a3 a_minus_def abelian_group.a_inv_closed add.inv_mult_group is_abelian_group 
          mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) prod.collapse 
          rel_def rev_subsetD subset)
    then have "t ⊗ ((snd x ⊗ fst y) ⊖ (snd y ⊗ fst x)) = 𝟬"
      using minus_zero r_minus f2
      by (smt a2 a3 f1 mem_Sigma_iff minus_closed partial_object.select_convs(1) prod.collapse 
          rel_def semiring_simprules(3) rev_subsetD subset)
    thus "y .=⇘rel⇙ x"
      using f1 rel_def 
      by auto
  qed
  show "⋀x y z. 
    x .=⇘rel⇙ y ⟹ y .=⇘rel⇙ z ⟹ x ∈ carrier rel ⟹ y ∈ carrier rel ⟹ z ∈ carrier rel ⟹ x .=⇘rel⇙ z"
  proof-
    fix x y z
    assume a1:"x .=⇘rel⇙ y" and a2:"y .=⇘rel⇙ z" and a3:"x ∈ carrier rel" and a4:"y ∈ carrier rel" 
      and a5:"z ∈ carrier rel"
    then obtain t where f1:"t ∈ S" and f2:"t ⊗ ((snd y ⊗ fst x) ⊖ (snd x ⊗ fst y)) = 𝟬"
      using rel_def 
      by fastforce
    then obtain t' where f3:"t' ∈ S" and f4:"t' ⊗ ((snd z ⊗ fst y) ⊖ (snd y ⊗ fst z)) = 𝟬"
      using rel_def a2 
      by fastforce
    then have "t ⊗ (snd y ⊗ fst x) ⊖ t ⊗ (snd x ⊗ fst y) = 𝟬"
      using f1 subset r_distr f2
      by (smt a3 a4 a_minus_def abelian_group.a_inv_closed is_abelian_group mem_Sigma_iff 
          monoid.m_closed monoid_axioms partial_object.select_convs(1) prod.collapse r_minus rel_def 
          subset_iff)
    then have "t' ⊗ (t ⊗ (snd y ⊗ fst x)) ⊖ t' ⊗ (t ⊗ (snd x ⊗ fst y)) = 𝟬"
      using f3 subset r_distr
      by (smt a3 a4 a_minus_def f1 is_abelian_group mem_Sigma_iff minus_to_eq 
          partial_object.select_convs(1) prod.collapse r_neg rel_def semiring_simprules(3) subset_iff)
    then have f5:"snd z ⊗ (t' ⊗ (t ⊗ (snd y ⊗ fst x))) ⊖ snd z ⊗ (t' ⊗ (t ⊗ (snd x ⊗ fst y))) = 𝟬"
      using a5 rel_def r_distr
      by (smt a3 a4 a_minus_def f1 f3 is_abelian_group mem_Sigma_iff minus_to_eq monoid.m_closed 
          monoid_axioms partial_object.select_convs(1) prod.collapse r_neg subset subset_iff)
    have "t' ⊗ (snd z ⊗ fst y) ⊖ t' ⊗ (snd y ⊗ fst z) = 𝟬"
      using f3 f4 subset r_distr
      by (smt a4 a5 a_minus_def abelian_group.a_inv_closed is_abelian_group mem_Sigma_iff 
          monoid.m_closed monoid_axioms partial_object.select_convs(1) prod.collapse r_minus rel_def 
          rev_subsetD)
    then have "t ⊗ (t' ⊗ (snd z ⊗ fst y)) ⊖ t ⊗ (t' ⊗ (snd y ⊗ fst z)) = 𝟬"
      using f1 subset r_distr
      by (smt a4 a5 a_minus_def f3 is_abelian_group mem_Sigma_iff minus_to_eq monoid.m_closed 
          monoid_axioms partial_object.select_convs(1) prod.collapse r_neg rel_def subset_iff)
    then have f6:"snd x ⊗ (t ⊗ (t' ⊗ (snd z ⊗ fst y))) ⊖ snd x ⊗ (t ⊗ (t' ⊗ (snd y ⊗ fst z))) = 𝟬"
      using a3 rel_def r_distr
      by (smt a4 a5 a_minus_def f1 f3 is_abelian_group mem_Sigma_iff minus_to_eq monoid.m_closed 
          monoid_axioms partial_object.select_convs(1) prod.collapse r_neg subset subset_iff)
    have "snd z ⊗ (t' ⊗ (t ⊗ (snd x ⊗ fst y))) = snd x ⊗ (t ⊗ (t' ⊗ (snd z ⊗ fst y)))"
      using comm_monoid_axioms_def[of R] f1 f3 subset a3 a4 a5 m_assoc
      by (smt m_lcomm mem_Sigma_iff partial_object.select_convs(1) partial_object_ext_def rel_def 
          semiring_simprules(3) rev_subsetD surjective_pairing)
    then have "snd z ⊗ (t' ⊗ (t ⊗ (snd y ⊗ fst x))) ⊖ snd z ⊗ (t' ⊗ (t ⊗ (snd x ⊗ fst y))) ⊕ 
      snd x ⊗ (t ⊗ (t' ⊗ (snd z ⊗ fst y))) ⊖ snd x ⊗ (t ⊗ (t' ⊗ (snd y ⊗ fst z))) = 
      snd z ⊗ (t' ⊗ (t ⊗ (snd y ⊗ fst x))) ⊖ snd x ⊗ (t ⊗ (t' ⊗ (snd y ⊗ fst z)))"
        using add.l_inv
        by (smt a3 a4 a5 f1 f3 f5 is_abelian_group local.semiring_axioms mem_Sigma_iff minus_to_eq 
            monoid.m_closed monoid_axioms partial_object.select_convs(1) prod.collapse rel_def 
            semiring.semiring_simprules(6) subset subset_iff)
    then have f7:"snd z ⊗ (t' ⊗ (t ⊗ (snd y ⊗ fst x))) ⊖ snd x ⊗ (t ⊗ (t' ⊗ (snd y ⊗ fst z))) = 𝟬"
      using f5 f6
      by (smt ‹snd z ⊗ (t' ⊗ (t ⊗ (snd x ⊗ fst y))) = snd x ⊗ (t ⊗ (t' ⊗ (snd z ⊗ fst y)))› 
          ‹t' ⊗ (snd z ⊗ fst y) ⊖ t' ⊗ (snd y ⊗ fst z) = 𝟬› a4 a5 f3 is_abelian_group mem_Sigma_iff 
          minus_to_eq partial_object.select_convs(1) prod.collapse rel_def semiring_simprules(3) 
          subset subset_iff)
    moreover have "(t ⊗ t' ⊗ snd y) ⊗ ((snd z ⊗ fst x) ⊖ (snd x ⊗ fst z)) = ((t ⊗ t' ⊗ snd y) ⊗ (snd z ⊗ fst x)) ⊖ ((t ⊗ t' ⊗ snd y) ⊗ (snd x ⊗ fst z))"
      using r_distr f1 f3 subset a3 a4 a5 rel_def a_minus_def r_minus
      by (smt SigmaE abelian_group.a_inv_closed is_abelian_group monoid.m_closed monoid_axioms 
          partial_object.select_convs(1) prod.sel(1) prod.sel(2) subset_iff)
    moreover have f8:"(t ⊗ t' ⊗ snd y) ⊗ (snd z ⊗ fst x) = snd z ⊗ (t' ⊗ (t ⊗ (snd y ⊗ fst x)))"
      using m_assoc comm_monoid_axioms_def[of R] f1 f3 subset a3 a4 a5 rel_def rev_subsetD
      by (smt SigmaE local.semiring_axioms m_lcomm partial_object.select_convs(1) prod.sel(1) 
          prod.sel(2) semiring.semiring_simprules(3))
    moreover have f9:"(t ⊗ t' ⊗ snd y) ⊗ (snd x ⊗ fst z) = snd x ⊗ (t ⊗ (t' ⊗ (snd y ⊗ fst z)))"
      using m_assoc comm_monoid_axioms_def[of R] f1 f3 subset a3 a4 a5 rel_def rev_subsetD
      by (smt SigmaE m_comm monoid.m_closed monoid_axioms partial_object.select_convs(1) prod.sel(1) 
          prod.sel(2))
    then have f10:"(t ⊗ t' ⊗ snd y) ⊗ (snd z ⊗ fst x) ⊖ (t ⊗ t' ⊗ snd y) ⊗ (snd x ⊗ fst z) = 𝟬"
      using f7 f8 f9 
      by simp
    moreover have "t ⊗ t' ⊗ snd y ∈ S"
      using f1 f3 a4 rel_def m_closed
      by (simp add: mem_Times_iff)
    then have "(t ⊗ t' ⊗ snd y) ⊗ (snd z ⊗ fst x ⊖ snd x ⊗ fst z) = 𝟬"
      using r_distr subset rev_subsetD f10 calculation(2) 
      by auto
    thus " x .=⇘rel⇙ z"
      using rel_def ‹t ⊗ t' ⊗ snd y ∈ S› 
      by auto
  qed
qed

definition  eq_class_of_rng_of_frac:: "_ ⇒ 'a ⇒ 'b ⇒ _set" (infix ‹|ı› 10)
  where "r |⇘rel⇙ s ≡ {(r', s') ∈ carrier rel. (r, s) .=⇘rel⇙ (r', s')}"

lemma class_of_to_rel:
  shows "class_of⇘rel⇙ (r, s) = (r |⇘rel⇙ s)"
  using eq_class_of_def[of rel] eq_class_of_rng_of_frac_def[of rel] 
  by auto

lemma (in eq_obj_rng_of_frac) zero_in_mult_submonoid:
  assumes "𝟬 ∈ S" and "(r, s) ∈ carrier rel" and "(r', s') ∈ carrier rel"
  shows "(r |⇘rel⇙ s) = (r' |⇘rel⇙ s')"
proof
  show "(r |⇘rel⇙ s) ⊆ (r' |⇘rel⇙ s')"
  proof
    fix x
    assume a1:"x ∈ (r |⇘rel⇙ s)"
    have " 𝟬 ⊗ (s' ⊗ fst x ⊖ snd x ⊗ r') = 𝟬"
      using l_zero subset rel_def a1 eq_class_of_rng_of_frac_def
      by (smt abelian_group.minus_closed assms(3) is_abelian_group l_null mem_Collect_eq mem_Sigma_iff 
          monoid.m_closed monoid_axioms old.prod.case partial_object.select_convs(1) subset_iff surjective_pairing)
    thus "x ∈ (r' |⇘rel⇙ s')"
      using assms(1) assms(3) rel_def eq_class_of_rng_of_frac_def
      by (smt SigmaE a1 eq_object.select_convs(1) l_null mem_Collect_eq minus_closed old.prod.case 
          partial_object.select_convs(1) prod.collapse semiring_simprules(3) subset subset_iff)
  qed
  show "(r' |⇘rel⇙ s') ⊆ (r |⇘rel⇙ s)"
  proof
    fix x
    assume a1:"x ∈ (r' |⇘rel⇙ s')"
    have " 𝟬 ⊗ (s ⊗ fst x ⊖ snd x ⊗ r) = 𝟬"
      using l_zero subset rel_def a1 eq_class_of_rng_of_frac_def
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD assms(2) l_null mem_Sigma_iff 
          minus_closed partial_object.select_convs(1) semiring_simprules(3) rev_subsetD)
    thus "x ∈ (r |⇘rel⇙ s)"
      using assms(1) assms(2) rel_def eq_class_of_rng_of_frac_def
      by (smt SigmaE a1 eq_object.select_convs(1) l_null mem_Collect_eq minus_closed old.prod.case 
          partial_object.select_convs(1) prod.collapse semiring_simprules(3) subset subset_iff)
  qed
qed

definition set_eq_class_of_rng_of_frac:: "_ ⇒ _set" (‹set'_class'_ofı›)
  where "set_class_of⇘rel⇙ ≡ {(r |⇘rel⇙ s)| r s. (r, s) ∈ carrier rel}"

(* The lemma below should be moved to theory Congruence in HOL-Algebra *)
lemma elem_eq_class:
  assumes "equivalence S" and "x ∈ carrier S" and "y ∈ carrier S" and "x .=⇘S⇙ y"
  shows "class_of⇘S⇙ x = class_of⇘S⇙ y"
proof
  show "class_of⇘S⇙ x ⊆ class_of⇘S⇙ y"
  proof
    fix z
    assume "z ∈ class_of⇘S⇙ x"
    then have "y .=⇘S⇙ z"
      using assms eq_class_of_def[of S x] equivalence.sym[of S x y] equivalence.trans
      by (metis (mono_tags, lifting) mem_Collect_eq)
    thus "z ∈ class_of⇘S⇙ y"
      using ‹z ∈ class_of⇘S⇙ x›
      by (simp add: eq_class_of_def)
  qed
  show "class_of⇘S⇙ y ⊆ class_of⇘S⇙ x"
  proof
    fix z
    assume "z ∈ class_of⇘S⇙ y"
    then have "x .=⇘S⇙ z"
      using assms eq_class_of_def equivalence.trans
      by (metis (mono_tags, lifting) mem_Collect_eq)
    thus "z ∈ class_of⇘S⇙ x"
      using ‹z ∈ class_of⇘S⇙ y›
      by (simp add: eq_class_of_def)
  qed
qed

lemma (in abelian_group) four_elem_comm:
  assumes "a ∈ carrier G" and "b ∈ carrier G" and "c ∈ carrier G" and "d ∈ carrier G"
  shows "a ⊖ c ⊕ b ⊖ d = a ⊕ b ⊖ c ⊖ d"
  using assms a_assoc a_comm
  by (simp add: a_minus_def)

lemma (in abelian_monoid) right_add_eq:
  assumes "a = b"
  shows "c ⊕ a = c ⊕ b"
  using assms 
  by simp

lemma (in abelian_monoid) right_minus_eq:
  assumes "a = b"
  shows "c ⊖ a = c ⊖ b"
  by (simp add: assms)

lemma (in abelian_group) inv_add:
  assumes "a ∈ carrier G" and "b ∈ carrier G"
  shows "⊖ (a ⊕ b) = ⊖ a ⊖ b"
  using assms minus_add
  by (simp add: a_minus_def)

lemma (in abelian_group) right_inv_add:
  assumes "a ∈ carrier G" and "b ∈ carrier G" and "c ∈ carrier G"
  shows "c ⊖ a ⊖ b = c ⊖ (a ⊕ b)" 
  using assms
  by (simp add: a_minus_def add.m_assoc local.minus_add)

context eq_obj_rng_of_frac 
begin

definition carrier_rng_of_frac:: "_ partial_object"
  where "carrier_rng_of_frac ≡ ⦇carrier = set_class_of⇘rel⇙⦈"

definition mult_rng_of_frac:: "[_set, _set] ⇒ _set"
  where "mult_rng_of_frac X Y ≡ 
let x' = (SOME x. x ∈ X) in 
let y' = (SOME y. y ∈ Y) in 
(fst x' ⊗ fst y')|⇘rel⇙ (snd x' ⊗ snd y')"

definition rec_monoid_rng_of_frac:: "_ monoid"
  where "rec_monoid_rng_of_frac ≡  ⦇carrier = set_class_of⇘rel⇙, mult = mult_rng_of_frac, one = (𝟭|⇘rel⇙ 𝟭)⦈"

lemma member_class_to_carrier:
  assumes "x ∈ (r |⇘rel⇙ s)" and "y ∈ (r' |⇘rel⇙ s')"
  shows "(fst x ⊗ fst y, snd x ⊗ snd y) ∈ carrier rel"
  using assms rel_def eq_class_of_rng_of_frac_def
  by (metis (no_types, lifting) Product_Type.Collect_case_prodD m_closed mem_Sigma_iff 
      partial_object.select_convs(1) semiring_simprules(3))

lemma member_class_to_member_class:
  assumes "x ∈ (r |⇘rel⇙ s)" and "y ∈ (r' |⇘rel⇙ s')"
  shows "(fst x ⊗ fst y |⇘rel⇙ snd x ⊗ snd y) ∈ set_class_of⇘rel⇙"
  using assms member_class_to_carrier[of x r s y r' s'] set_eq_class_of_rng_of_frac_def[of rel] 
    eq_class_of_rng_of_frac_def 
  by auto

lemma closed_mult_rng_of_frac :
  assumes "(r, s) ∈ carrier rel" and "(t, u) ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (t |⇘rel⇙ u) ∈ set_class_of⇘rel⇙"
proof-
  have "(r, s) .=⇘rel⇙ (r, s)"
    using assms(1) equiv_obj_rng_of_frac equivalence_def[of "rel"] 
    by blast
  then have "(r, s) ∈ (r |⇘rel⇙ s)"
    using assms(1)
    by (simp add: eq_class_of_rng_of_frac_def)
  then have f1:"∃x. x ∈ (r |⇘rel⇙ s)"
    by auto
  have f2:"∃y. y∈ (t |⇘rel⇙ u)"
    using assms(2) equiv_obj_rng_of_frac equivalence.refl eq_class_of_rng_of_frac_def 
    by fastforce
  show "(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (t |⇘rel⇙ u) ∈ set_class_of⇘rel⇙"
    using f1 f2 rec_monoid_rng_of_frac_def mult_rng_of_frac_def[of "(r |⇘rel⇙ s)" "(t |⇘rel⇙ u)"] 
      set_eq_class_of_rng_of_frac_def[of "rel"] member_class_to_member_class[of x' r s y' t u]
    by (metis (mono_tags, lifting) mem_Collect_eq member_class_to_carrier monoid.select_convs(1) 
        someI_ex)
qed

lemma non_empty_class:
  assumes "(r, s) ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ≠ {}"
  using assms eq_class_of_rng_of_frac_def equiv_obj_rng_of_frac equivalence.refl 
  by fastforce

lemma mult_rng_of_frac_fundamental_lemma:
  assumes "(r, s) ∈ carrier rel" and "(r', s') ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (r' |⇘rel⇙ s') = (r ⊗ r' |⇘rel⇙ s ⊗ s')"
proof-
  have f1:"(r |⇘rel⇙ s) ≠ {}"
    using assms(1) non_empty_class 
    by auto
  have "(r' |⇘rel⇙ s') ≠ {}"
    using assms(2) non_empty_class 
    by auto
  then have "∃x ∈ (r |⇘rel⇙ s). ∃x' ∈ (r' |⇘rel⇙ s'). (r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (r' |⇘rel⇙ s') =
    (fst x ⊗ fst x' |⇘rel⇙ snd x ⊗ snd x')"
      using f1 rec_monoid_rng_of_frac_def
      by (metis monoid.select_convs(1) mult_rng_of_frac_def some_in_eq)
  then obtain x and x' where f2:"x ∈ (r |⇘rel⇙ s)" and f3:"x' ∈ (r' |⇘rel⇙ s')" 
    and "(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (r' |⇘rel⇙ s') = (fst x ⊗ fst x' |⇘rel⇙ snd x ⊗ snd x')"
    by blast
  then have "(r, s) .=⇘rel⇙ (fst x, snd x)"
    using rel_def
    by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def)
  then obtain t where f4:"t ∈ S" and f5:"t ⊗ ((snd x ⊗ r) ⊖ (s ⊗ fst x)) = 𝟬"
    using rel_def 
    by auto
  have "(r', s') .=⇘rel⇙ (fst x', snd x')"
    using rel_def f3
    by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def)
  then obtain t' where f6:"t' ∈ S" and f7:"t' ⊗ (snd x' ⊗ r' ⊖ s' ⊗ fst x') = 𝟬"
    using rel_def 
    by auto
  have f8:"t ∈ carrier R"
    using f4 subset rev_subsetD 
    by auto
  have f9:"snd x ⊗ r ∈ carrier R" 
    using subset rev_subsetD f2 assms(1)
    by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff 
        partial_object.select_convs(1) rel_def semiring_simprules(3))
  have f10:"⊖ (s ⊗ fst x) ∈ carrier R"
    using assms(1) subset rev_subsetD f2
    by (metis (no_types, lifting) BNF_Def.Collect_case_prodD abelian_group.a_inv_closed 
        eq_class_of_rng_of_frac_def is_abelian_group mem_Sigma_iff monoid.m_closed monoid_axioms 
        partial_object.select_convs(1) rel_def)
  then have "t ⊗ (snd x ⊗ r) ⊖ t ⊗ (s ⊗ fst x) = 𝟬"
    using f8 f9 f10 f5 r_distr[of "snd x ⊗ r" "⊖ (s ⊗ fst x)" t] a_minus_def r_minus[of t "s ⊗ fst x"]
    by (smt BNF_Def.Collect_case_prodD assms(1) eq_class_of_rng_of_frac_def f2 mem_Sigma_iff 
        partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
  then have f11:"t ⊗ (snd x ⊗ r) = t ⊗ (s ⊗ fst x)"
    by (smt BNF_Def.Collect_case_prodD assms(1) eq_class_of_rng_of_frac_def f2 f8 is_abelian_group 
        mem_Sigma_iff minus_to_eq monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
  have f12:"t' ∈ carrier R"
    using f6 subset rev_subsetD 
    by auto
  have f13:"snd x' ⊗ r' ∈ carrier R"
    using assms(2) f3 subset rev_subsetD
    by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def 
        mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def)
  have f14:"⊖ (s' ⊗ fst x') ∈ carrier R"
    using assms(2) f3 subset rev_subsetD
    by (metis (no_types, lifting) BNF_Def.Collect_case_prodD abelian_group.a_inv_closed 
        eq_class_of_rng_of_frac_def is_abelian_group mem_Sigma_iff monoid.m_closed monoid_axioms 
        partial_object.select_convs(1) rel_def)
  then have "t' ⊗ (snd x' ⊗ r') ⊖ t' ⊗ (s' ⊗ fst x') = 𝟬"
    using f12 f13 f14 f7 r_distr[of "snd x' ⊗ r'" "⊖ (s' ⊗ fst x')" t'] a_minus_def 
      r_minus[of t' "s' ⊗ fst x'"]
    by (smt BNF_Def.Collect_case_prodD assms(2) eq_class_of_rng_of_frac_def f3 mem_Sigma_iff 
        partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
  then have f15:"t' ⊗ (snd x' ⊗ r') = t' ⊗ (s' ⊗ fst x')"
    by (smt BNF_Def.Collect_case_prodD assms(2) eq_class_of_rng_of_frac_def f3 f12 is_abelian_group 
        mem_Sigma_iff minus_to_eq monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
  have "t' ⊗ t ∈ S"
    using f4 f6 m_closed 
    by auto
  then have f16:"t' ⊗ t ∈ carrier R"
    using subset rev_subsetD 
    by auto
  have f17:"(snd x ⊗ snd x') ⊗ (r ⊗ r') ∈ carrier R"
    using assms f2 f3
    by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff 
        monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
  have f18:"(s ⊗ s') ⊗ (fst x ⊗ fst x') ∈ carrier R"
    using assms f2 f3
    by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff 
        monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
  then have f19:"(t' ⊗ t) ⊗ ((snd x ⊗ snd x') ⊗ (r ⊗ r') ⊖ (s ⊗ s') ⊗ (fst x ⊗ fst x')) = 
    ((t' ⊗ t) ⊗ (snd x ⊗ snd x')) ⊗ (r ⊗ r') ⊖ (t' ⊗ t) ⊗ ((s ⊗ s') ⊗ (fst x ⊗ fst x'))"
      using f16 f17 f18 r_distr m_assoc r_minus a_minus_def
      by (smt BNF_Def.Collect_case_prodD assms(1) assms(2) eq_class_of_rng_of_frac_def f14 f2 f3 
          m_comm mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def 
          subset subset_iff)
  then have f20:"(t' ⊗ t) ⊗ (snd x ⊗ snd x') ⊗ (r ⊗ r') = (t' ⊗ t) ⊗ (snd x ⊗ r ⊗ snd x' ⊗ r')"
    using m_assoc m_comm f16 assms rel_def f2 f3
    by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff 
        partial_object.select_convs(1) semiring_simprules(3) subset subset_iff)
  then have "((t' ⊗ t) ⊗ (snd x ⊗ snd x')) ⊗ (r ⊗ r') = t' ⊗ ((t ⊗ snd x ⊗ r) ⊗ snd x' ⊗ r')"
    using m_assoc assms f2 f3 rel_def f8 f12
    by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff monoid.m_closed 
        monoid_axioms partial_object.select_convs(1) subset subset_iff)
  then have f21:"((t' ⊗ t) ⊗ (snd x ⊗ snd x')) ⊗ (r ⊗ r') = t' ⊗ (t ⊗ s ⊗ fst x) ⊗ snd x' ⊗ r'"
    using f11 m_assoc
    by (smt BNF_Def.Collect_case_prodD assms(1) assms(2) eq_class_of_rng_of_frac_def f12 f2 f3 f8 
        mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
  moreover have "(t' ⊗ t) ⊗ ((s ⊗ s') ⊗ (fst x ⊗ fst x')) = (t' ⊗ s' ⊗ fst x') ⊗ t ⊗ s ⊗ fst x"
    using assms f2 f3 f8 f12 m_assoc m_comm rel_def
    by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff monoid.m_closed 
        monoid_axioms partial_object.select_convs(1) subset subset_iff)
  then have "(t' ⊗ t) ⊗ ((s ⊗ s') ⊗ (fst x ⊗ fst x')) = (t' ⊗ snd x' ⊗ r') ⊗ t ⊗ s ⊗ fst x"
    using f15 m_assoc
    by (smt BNF_Def.Collect_case_prodD assms(2) eq_class_of_rng_of_frac_def f12 f3 mem_Sigma_iff 
        partial_object.select_convs(1) rel_def subset subset_iff)
  then have f22:"(t' ⊗ t) ⊗ ((s ⊗ s') ⊗ (fst x ⊗ fst x')) = t' ⊗ ((t ⊗ snd x ⊗ r) ⊗ snd x' ⊗ r')"
    using m_assoc m_comm assms
    by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def f12 f2 f21 f3 f8 mem_Sigma_iff 
        partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
  then have f23:"(t' ⊗ t) ⊗ ((snd x ⊗ snd x') ⊗ (r ⊗ r') ⊖ (s ⊗ s') ⊗ (fst x ⊗ fst x')) = 𝟬"
    using f19 f21 f22
    by (metis ‹t' ⊗ t ⊗ (snd x ⊗ snd x') ⊗ (r ⊗ r') = t' ⊗ (t ⊗ snd x ⊗ r ⊗ snd x' ⊗ r')› 
        a_minus_def f16 f18 r_neg semiring_simprules(3))
  have f24:"(r ⊗ r', s ⊗ s') ∈ carrier rel"
    using assms rel_def 
    by auto
  have f25: "(fst x ⊗ fst x', snd x ⊗ snd x') ∈ carrier rel"
    using f2 f3 member_class_to_carrier 
    by auto
  then have "(r ⊗ r', s ⊗ s') .=⇘rel⇙ (fst x ⊗ fst x', snd x ⊗ snd x')"
    using f23 f24 rel_def ‹t' ⊗ t ∈ S› 
    by auto
  then have "class_of⇘rel⇙ (r ⊗ r', s ⊗ s') = class_of⇘rel⇙ (fst x ⊗ fst x', snd x ⊗ snd x')"
    using f24 f25 equiv_obj_rng_of_frac elem_eq_class[of rel "(r ⊗ r', s ⊗ s')" "(fst x ⊗ fst x', snd x ⊗ snd x')"] 
      eq_class_of_rng_of_frac_def 
    by auto
  then have "(r ⊗ r' |⇘rel⇙ s ⊗ s') = (fst x ⊗ fst x' |⇘rel⇙ snd x ⊗ snd x')"
    using class_of_to_rel[of rel] 
    by auto
  thus ?thesis
    using ‹(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (r' |⇘rel⇙ s') = (fst x ⊗ fst x' |⇘rel⇙ snd x ⊗ snd x')› 
      trans sym 
    by auto
qed

lemma member_class_to_assoc:
  assumes "x ∈ (r |⇘rel⇙ s)" and "y ∈ (t |⇘rel⇙ u)" and "z ∈ (v |⇘rel⇙ w)"
  shows "((fst x ⊗ fst y) ⊗ fst z |⇘rel⇙ (snd x ⊗ snd y) ⊗ snd z) = (fst x ⊗ (fst y ⊗ fst z) |⇘rel⇙ snd x ⊗ (snd y ⊗ snd z))"
  using assms m_assoc subset rel_def rev_subsetD
  by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff partial_object.select_convs(1))

lemma assoc_mult_rng_of_frac:
  assumes "(r, s) ∈ carrier rel" and "(t, u) ∈ carrier rel" and "(v, w) ∈ carrier rel"
  shows "((r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (t |⇘rel⇙ u)) ⊗⇘rec_monoid_rng_of_frac⇙ (v |⇘rel⇙ w) =
         (r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ ((t |⇘rel⇙ u) ⊗⇘rec_monoid_rng_of_frac⇙ (v |⇘rel⇙ w))"
proof-
  have "((r ⊗ t) ⊗ v, (s ⊗ u) ⊗ w) = (r ⊗ (t ⊗ v), s ⊗ (u ⊗ w))"
    using assms m_assoc
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1) rel_def rev_subsetD subset)
  then have f1:"((r ⊗ t) ⊗ v |⇘rel⇙ (s ⊗ u) ⊗ w) = (r ⊗ (t ⊗ v) |⇘rel⇙ s ⊗ (u ⊗ w))"
    by simp
  have f2:"((r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (t |⇘rel⇙ u)) ⊗⇘rec_monoid_rng_of_frac⇙ (v |⇘rel⇙ w) =
    ((r ⊗ t) ⊗ v |⇘rel⇙ (s ⊗ u) ⊗ w)"
    using assms mult_rng_of_frac_fundamental_lemma rel_def 
    by auto
  have f3:"(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ ((t |⇘rel⇙ u) ⊗⇘rec_monoid_rng_of_frac⇙ (v |⇘rel⇙ w)) =
    (r ⊗ (t ⊗ v) |⇘rel⇙ s ⊗ (u ⊗ w))"
    using assms mult_rng_of_frac_fundamental_lemma rel_def 
    by auto
  thus ?thesis
    using f1 f2 f3 
    by simp
qed

lemma left_unit_mult_rng_of_frac:
  assumes "(r, s) ∈ carrier rel"
  shows "𝟭⇘rec_monoid_rng_of_frac⇙ ⊗⇘rec_monoid_rng_of_frac⇙ (r |⇘rel⇙ s) = (r |⇘rel⇙ s)"
  using assms subset rev_subsetD rec_monoid_rng_of_frac_def mult_rng_of_frac_fundamental_lemma[of 𝟭 𝟭 r s] 
    l_one[of r] l_one[of s] rel_def 
  by auto

lemma right_unit_mult_rng_of_frac:
  assumes "(r, s) ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ 𝟭⇘rec_monoid_rng_of_frac⇙ = (r |⇘rel⇙ s)"
  using assms subset rev_subsetD rec_monoid_rng_of_frac_def mult_rng_of_frac_fundamental_lemma[of r s 𝟭 𝟭]
    r_one[of r] r_one[of s] rel_def 
  by auto

lemma monoid_rng_of_frac:
  shows "monoid (rec_monoid_rng_of_frac)"
proof
  show "⋀x y. x ∈ carrier rec_monoid_rng_of_frac ⟹
           y ∈ carrier rec_monoid_rng_of_frac ⟹ x ⊗⇘rec_monoid_rng_of_frac⇙ y ∈ carrier rec_monoid_rng_of_frac"
    using rec_monoid_rng_of_frac_def closed_mult_rng_of_frac
    by (smt mem_Collect_eq partial_object.select_convs(1) set_eq_class_of_rng_of_frac_def)
  show "⋀x y z. x ∈ carrier rec_monoid_rng_of_frac ⟹
             y ∈ carrier rec_monoid_rng_of_frac ⟹
             z ∈ carrier rec_monoid_rng_of_frac ⟹
             x ⊗⇘rec_monoid_rng_of_frac⇙ y ⊗⇘rec_monoid_rng_of_frac⇙ z =
             x ⊗⇘rec_monoid_rng_of_frac⇙ (y ⊗⇘rec_monoid_rng_of_frac⇙ z)"
    using assoc_mult_rng_of_frac
    by (smt mem_Collect_eq partial_object.select_convs(1) rec_monoid_rng_of_frac_def 
        set_eq_class_of_rng_of_frac_def)
  show "𝟭⇘rec_monoid_rng_of_frac⇙ ∈ carrier rec_monoid_rng_of_frac"
    using rec_monoid_rng_of_frac_def rel_def set_eq_class_of_rng_of_frac_def 
    by fastforce
  show "⋀x. x ∈ carrier rec_monoid_rng_of_frac ⟹ 𝟭⇘rec_monoid_rng_of_frac⇙ ⊗⇘rec_monoid_rng_of_frac⇙ x = x"
    using left_unit_mult_rng_of_frac
    by (smt mem_Collect_eq partial_object.select_convs(1) rec_monoid_rng_of_frac_def set_eq_class_of_rng_of_frac_def)
  show "⋀x. x ∈ carrier rec_monoid_rng_of_frac ⟹ x ⊗⇘rec_monoid_rng_of_frac⇙ 𝟭⇘rec_monoid_rng_of_frac⇙ = x"
    using right_unit_mult_rng_of_frac
    by (smt mem_Collect_eq partial_object.select_convs(1) rec_monoid_rng_of_frac_def set_eq_class_of_rng_of_frac_def)
qed

lemma comm_mult_rng_of_frac:
  assumes "(r, s) ∈ carrier rel" and "(r', s') ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (r' |⇘rel⇙ s') = (r' |⇘rel⇙ s') ⊗⇘rec_monoid_rng_of_frac⇙ (r |⇘rel⇙ s)"
proof-
  have f1:"(r |⇘rel⇙ s) ⊗⇘rec_monoid_rng_of_frac⇙ (r' |⇘rel⇙ s') = (r ⊗ r' |⇘rel⇙ s ⊗ s')"
    using assms mult_rng_of_frac_fundamental_lemma 
    by simp
  have f2:"(r' |⇘rel⇙ s') ⊗⇘rec_monoid_rng_of_frac⇙ (r |⇘rel⇙ s) = (r' ⊗ r |⇘rel⇙ s' ⊗ s)"
    using assms mult_rng_of_frac_fundamental_lemma 
    by simp
  have f3:"r ⊗ r' = r' ⊗ r"
    using assms rel_def m_comm 
    by simp
  have f4:"s ⊗ s' = s' ⊗ s"
    using assms rel_def subset rev_subsetD m_comm
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1))
  thus ?thesis
    using f1 f2 f3 f4 
    by simp
qed

lemma comm_monoid_rng_of_frac:
  shows "comm_monoid (rec_monoid_rng_of_frac)"
  using comm_monoid_def Group.comm_monoid_axioms_def monoid_rng_of_frac comm_mult_rng_of_frac
  by (smt mem_Collect_eq partial_object.select_convs(1) rec_monoid_rng_of_frac_def set_eq_class_of_rng_of_frac_def)

definition add_rng_of_frac:: "[_set, _set] ⇒ _set"
  where "add_rng_of_frac X Y ≡ 
let x' = (SOME x. x ∈ X) in 
let y' = (SOME y. y ∈ Y) in 
(snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y') |⇘rel⇙ (snd x' ⊗ snd y')"

definition rec_rng_of_frac:: "_ ring"
  where "rec_rng_of_frac ≡ 
⦇carrier = set_class_of⇘rel⇙, mult = mult_rng_of_frac, one = (𝟭|⇘rel⇙ 𝟭), zero = (𝟬 |⇘rel⇙ 𝟭), add = add_rng_of_frac ⦈"

lemma add_rng_of_frac_fundamental_lemma:
  assumes "(r, s) ∈ carrier rel" and "(r', s') ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') = (s' ⊗ r ⊕ s ⊗ r' |⇘rel⇙ s ⊗ s')"
proof-
  have "∃x' ∈ (r |⇘rel⇙ s). ∃y' ∈ (r' |⇘rel⇙ s'). (r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') = 
    (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y' |⇘rel⇙ snd x' ⊗ snd y')"
    using assms rec_rng_of_frac_def add_rng_of_frac_def[of "(r |⇘rel⇙ s)" "(r' |⇘rel⇙ s')"]
    by (metis non_empty_class ring_record_simps(12) some_in_eq)
  then obtain x' and y' where f1:"x' ∈ (r |⇘rel⇙ s)" and f2:"y' ∈ (r' |⇘rel⇙ s')" and 
    f3:"(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') = (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y' |⇘rel⇙ snd x' ⊗ snd y')"
    by auto
  then have "(r, s) .=⇘rel⇙ x'"
    using f1 rel_def eq_class_of_rng_of_frac_def[of rel r s]
    by auto
  then obtain t where f4:"t ∈ S" and f5:"t ⊗ (snd x' ⊗ r ⊖ s ⊗ fst x') = 𝟬"
    using rel_def 
    by auto
  have "(r', s') .=⇘rel⇙ y'"
    using f2 rel_def eq_class_of_rng_of_frac_def[of rel r' s']
    by auto
  then obtain t' where f6:"t' ∈ S" and f7:"t' ⊗ (snd y' ⊗ r' ⊖ s' ⊗ fst y') = 𝟬"
    using rel_def 
    by auto
  then have f8:"t ⊗ t' ∈ S"
    using m_closed f4 f6
    by simp
  then have "(s' ⊗ r ⊕ s ⊗ r', s ⊗ s') .=⇘rel⇙ (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y', snd x' ⊗ snd y')"
  proof-
    have f9:"t' ⊗ s' ⊗ snd y' ∈ carrier R"
      using f6 assms(2) f2 subset rev_subsetD eq_class_of_rng_of_frac_def rel_def 
      by fastforce
    have f10:"snd x' ⊗ r ∈ carrier R"
      using assms(1) f1 rel_def subset rev_subsetD
      by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
    have f11:"s ⊗ fst x' ∈ carrier R"
      using assms(1) subset rev_subsetD f1 rel_def
      by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3)) 
    have "t ⊗ (snd x' ⊗ r ⊖ s ⊗ fst x') = t ⊗ (snd x' ⊗ r) ⊖ t ⊗ (s ⊗ fst x')"
      using f9 f10 f11 f4 subset rev_subsetD r_distr[of "snd x' ⊗ r" "s ⊗ fst x'" t] a_minus_def 
        r_minus[of t "s ⊗ fst x'"]
      by (smt add.inv_closed monoid.m_closed monoid_axioms r_distr)
    then have f12:"(t' ⊗ s' ⊗ snd y') ⊗ (t ⊗ (snd x' ⊗ r ⊖ s ⊗ fst x')) =
      t' ⊗ s' ⊗ snd y' ⊗ t ⊗ (snd x' ⊗ r) ⊖ (t' ⊗ s' ⊗ snd y' ⊗ t ⊗ (s ⊗ fst x'))"
      using f9 r_distr[of _ _ "t' ⊗ s' ⊗ snd y'"] rel_def r_minus a_minus_def
      by (smt abelian_group.minus_to_eq f10 f11 f4 f5 is_abelian_group m_assoc monoid.m_closed 
          monoid_axioms r_neg r_null subset subset_iff)
    have f13:"(snd x' ⊗ snd y') ⊗ (s' ⊗ r) ∈ carrier R"
      using assms f1 f2 subset rev_subsetD
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def)
    have f14:"(s ⊗ s') ⊗ (snd y' ⊗ fst x') ∈ carrier R"
      using assms f1 f2 subset rev_subsetD
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def)
    then have "(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x')) =
      (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r)) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd y' ⊗ fst x'))"
      using f13 f14 f8 subset rev_subsetD r_distr rel_def r_minus a_minus_def
      by (smt add.inv_closed semiring_simprules(3))
    have f15:"s ⊗ s' ∈ carrier R"
      using assms rel_def subset rev_subsetD 
      by auto
    have f16:"snd y' ⊗ fst x' ∈ carrier R"
      using f1 f2 rel_def subset rev_subsetD[of _ S] monoid.m_closed[of R "snd y'" "fst x'"]
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff monoid_axioms partial_object.select_convs(1))
    have f17:"t ∈ carrier R"
      using f4 subset rev_subsetD 
      by auto
    have f18:"t' ∈ carrier R"
      using f6 subset rev_subsetD 
      by auto
    have f19:"s ∈ carrier R"
      using assms(1) rel_def subset 
      by auto
    have f20:"s' ∈ carrier R"
      using assms(2) rel_def subset 
      by auto
    have f21:"snd y' ∈ carrier R"
      using f2 rel_def subset rev_subsetD
      by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff partial_object.select_convs(1))
    have f22:"fst x' ∈ carrier R"
      using f1 rel_def
      by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff 
          partial_object.select_convs(1))
    then have f23:"(t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd y' ⊗ fst x')) = t' ⊗ s' ⊗ snd y' ⊗ t ⊗ (s ⊗ fst x')"
      using f17 f18 f19 f20 f21 m_assoc m_comm 
      by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def f1 f4 f6 mem_Sigma_iff 
          partial_object.select_convs(1) rel_def semiring_simprules(3) subset_iff) 
    have f24:"(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r)) = t' ⊗ s' ⊗ snd y' ⊗ t ⊗ (snd x' ⊗ r)"
      using f17 f18 f20 f21 m_assoc m_comm
      by (smt BNF_Def.Collect_case_prodD assms(1) eq_class_of_rng_of_frac_def f1 f2 f4 f6 
          mem_Sigma_iff partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff) 
    then have "(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r)) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd y' ⊗ fst x'))=
      (t' ⊗ s' ⊗ snd y' ⊗ t ⊗ (snd x' ⊗ r)) ⊖ (t' ⊗ s' ⊗ snd y' ⊗ t ⊗ (s ⊗ fst x'))"
      using f23 f24 
      by simp
    then have f25:"(t' ⊗ s' ⊗ snd y') ⊗ (t ⊗ (snd x' ⊗ r ⊖ s ⊗ fst x')) = 
      (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r)) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd y' ⊗ fst x'))"
      using f12 
      by simp
    have f26:"(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s ⊗ r')) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd x' ⊗ fst y')) =
      t ⊗ s ⊗ snd x' ⊗ t' ⊗ (snd y' ⊗ r') ⊖ (t ⊗ s ⊗ snd x' ⊗ t' ⊗ (s' ⊗ fst y'))"
      by (smt BNF_Def.Collect_case_prodD assms(2) eq_class_of_rng_of_frac_def f1 f17 f18 f19 f2 
          m_assoc m_comm mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
    have f27:"snd y' ⊗ r' ∈ carrier R"
      using assms(2) f21 rel_def 
      by auto
    have f28:"s' ⊗ fst y' ∈ carrier R"
      using f20 assms(2)
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def f2 
          mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def)
    then have "t' ⊗ (snd y' ⊗ r' ⊖ s' ⊗ fst y') = t' ⊗ (snd y' ⊗ r') ⊖ t' ⊗ (s' ⊗ fst y')"
      using f18 f27 f28 r_minus[of t' "s' ⊗ fst y'"]
      by (simp add: a_minus_def r_distr)
    then have f29:"(t ⊗ s ⊗ snd x') ⊗ (t' ⊗ (snd y' ⊗ r' ⊖ s' ⊗ fst y')) = 
      (t ⊗ s ⊗ snd x') ⊗ (t' ⊗ (snd y' ⊗ r') ⊖ t' ⊗ (s' ⊗ fst y'))"
      by simp
    have "t ⊗ s ⊗ snd x' ∈ carrier R"
      using f17 f19 f1 subset assms(1) eq_class_of_rng_of_frac_def f4 rel_def 
      by fastforce
    then have f30:"(t ⊗ s ⊗ snd x') ⊗ (t' ⊗ (snd y' ⊗ r' ⊖ s' ⊗ fst y')) = 
      (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s ⊗ r')) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd x' ⊗ fst y'))"
      using f26 f29 r_distr
      by (smt ‹t' ⊗ (snd y' ⊗ r' ⊖ s' ⊗ fst y') = t' ⊗ (snd y' ⊗ r') ⊖ t' ⊗ (s' ⊗ fst y')› 
          a_minus_def abelian_group.minus_to_eq f18 f27 f28 f7 is_abelian_group m_assoc monoid.m_closed 
          monoid_axioms r_neg semiring_simprules(15))
    then have f31:"((t' ⊗ s' ⊗ snd y') ⊗ (t ⊗ (snd x' ⊗ r ⊖ s ⊗ fst x'))) ⊕ ((t ⊗ s ⊗ snd x') ⊗ (t' ⊗ (snd y' ⊗ r' ⊖ s' ⊗ fst y')))
      = ((t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r)) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd y' ⊗ fst x'))) ⊕ 
      ((t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s ⊗ r')) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd x' ⊗ fst y')))"
      using f25 f30 
      by simp
    have f32:"(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r)) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd y' ⊗ fst x'))
      = (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x'))"
      using f17 f18 r_distr
      by (simp add: ‹t ⊗ t' ⊗ (snd x' ⊗ snd y' ⊗ (s' ⊗ r) ⊖ s ⊗ s' ⊗ (snd y' ⊗ fst x')) = t ⊗ t' ⊗ (snd x' ⊗ snd y' ⊗ (s' ⊗ r)) ⊖ t ⊗ t' ⊗ (s ⊗ s' ⊗ (snd y' ⊗ fst x'))›)
    have f33:"(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s ⊗ r')) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd x' ⊗ fst y')) =
      (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y'))"
      using r_distr[of _ _ "t ⊗ t'"] f17 f18 a_minus_def r_minus
      by (smt BNF_Def.Collect_case_prodD abelian_group.a_inv_closed assms(1) assms(2) 
          eq_class_of_rng_of_frac_def f1 f2 is_abelian_group mem_Sigma_iff partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
    have f34:"(snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') = (snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊕ (snd x' ⊗ snd y') ⊗ (s ⊗ r')"
      using r_distr
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD assms(1) assms(2) eq_class_of_rng_of_frac_def 
          f1 f2 mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def 
          subset subset_iff)
    then have "(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r')) = 
      (t ⊗ t') ⊗ (snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊕ (t ⊗ t') ⊗ (snd x' ⊗ snd y') ⊗ (s ⊗ r')"
      by (smt BNF_Def.Collect_case_prodD assms(1) assms(2) eq_class_of_rng_of_frac_def f1 f17 f18 
          f2 m_assoc mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) 
          r_distr rel_def subset subset_iff)
    have f35:"(s ⊗ s') ⊗ (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y') = (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊕ (s ⊗ s') ⊗ (snd x' ⊗ fst y')"
      using r_distr f19 f20
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def f1 f2 
          mem_Sigma_iff partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
    then have f36:"(t ⊗ t') ⊗ (s ⊗ s') ⊗ (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y') = 
      (t ⊗ t') ⊗ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊕ (t ⊗ t') ⊗ (s ⊗ s') ⊗ (snd x' ⊗ fst y')"
      by (smt BNF_Def.Collect_case_prodD assms(1) assms(2) eq_class_of_rng_of_frac_def f1 f17 f18 f2 
          mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) r_distr rel_def 
          subset subset_iff)
    have f37:"(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x')) ∈ carrier R"
      by (simp add: f13 f14 f17 f18)
    have f38:"(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')) ∈ carrier R"
      using ‹t ⊗ s ⊗ snd x' ∈ carrier R› f30 f33 f7 zero_closed 
      by auto
    have f39:"(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r)) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd y' ⊗ fst x')) ∈ carrier R"
      by (simp add: f32 f37)
    have "snd x' ⊗ snd y' ∈ carrier R"
      using f1 f2 subset rev_subsetD
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff partial_object.select_convs(1) rel_def semiring_simprules(3))
    have "(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x')) ⊕
      (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')) =
      (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r)) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd y' ⊗ fst x')) ⊕ 
      (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s ⊗ r')) ⊖ (t ⊗ t') ⊗ ((s ⊗ s') ⊗ (snd x' ⊗ fst y'))"
      using f32 f33 ‹snd x' ⊗ snd y' ∈ carrier R› ‹t ⊗ s ⊗ snd x' ∈ carrier R› assms(2) f17 f18 f19 
        f25 f30 f5 f7 f9 l_zero r_null rel_def zero_closed 
      apply clarsimp
      using l_zero semiring_simprules(3) by presburger
    then have f40:"((t' ⊗ s' ⊗ snd y') ⊗ (t ⊗ (snd x' ⊗ r ⊖ s ⊗ fst x'))) ⊕ 
      ((t ⊗ s ⊗ snd x') ⊗ (t' ⊗ (snd y' ⊗ r' ⊖ s' ⊗ fst y'))) = 
      ((t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x'))) ⊕ 
      ((t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')))"
      using f31
      by (simp add: f32 f33)
    have f41:"(snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ∈ carrier R"
      by (simp add: f13 f14)
    have f42:"(snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y') ∈ carrier R"
      by (smt BNF_Def.Collect_case_prodD abelian_group.minus_closed assms(1) assms(2) 
          eq_class_of_rng_of_frac_def f1 f2 is_abelian_group mem_Sigma_iff partial_object.select_convs(1) 
          rel_def semiring_simprules(3) subset subset_iff)
    then have "(t' ⊗ s' ⊗ snd y') ⊗ (t ⊗ (snd x' ⊗ r ⊖ s ⊗ fst x')) ⊕ 
      (t ⊗ s ⊗ snd x') ⊗ (t' ⊗ (snd y' ⊗ r' ⊖ s' ⊗ fst y')) = 
      (t ⊗ t') ⊗ (((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x')) ⊕ ((snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')))"
      using r_distr[of "(snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x')" "(snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')" "t ⊗ t'"]
      f17 f18  f40 f41 f42 
      by simp
    have "(snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊕ (snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y') =
      (snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊕ (snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')"
      using four_elem_comm[of "(snd x' ⊗ snd y') ⊗ (s' ⊗ r)" "(snd x' ⊗ snd y') ⊗ (s ⊗ r')" "(s ⊗ s') ⊗ (snd y' ⊗ fst x')" "(s ⊗ s') ⊗ (snd x' ⊗ fst y')"]
      by (smt BNF_Def.Collect_case_prodD assms eq_class_of_rng_of_frac_def f1 f2 
          mem_Sigma_iff partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
    then have "(snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊕ (snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y') =
      ((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊕ (snd x' ⊗ snd y') ⊗ (s ⊗ r')) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')"
      by blast
    then have f43:"(snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊕ (snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y') =
      (snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')"
      using f34 
      by simp
    have "(snd x' ⊗ snd y') ⊗ (s ⊗ r') ∈ carrier R"
      using ‹snd x' ⊗ snd y' ∈ carrier R› assms(2) f19 rel_def 
      by auto
    have "(s ⊗ s') ⊗ (snd x' ⊗ fst y') ∈ carrier R"
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD assms 
          eq_class_of_rng_of_frac_def f1 f2 mem_Sigma_iff partial_object.select_convs(1) rel_def 
          semiring_simprules(3) subset subset_iff)
    then have f43bis:"((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x')) ⊕ ((snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')) =
      (snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')"
      using a_assoc a_minus_def f41 f43
      by (smt ‹snd x' ⊗ snd y' ⊗ (s ⊗ r') ∈ carrier R› add.l_inv_ex add.m_closed minus_equality)
    have f44:"s ⊗ s' ⊗ (snd y' ⊗ fst x') ∈ carrier R"
      by (simp add: f14)
    have f45:"s ⊗ s' ⊗ (snd x' ⊗ fst y') ∈ carrier R"
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD assms 
          eq_class_of_rng_of_frac_def f1 f2 mem_Sigma_iff partial_object.select_convs(1) rel_def 
          semiring_simprules(3) subset subset_iff)
    then have "⊖ ((s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊕ (s ⊗ s') ⊗ (snd x' ⊗ fst y')) =
      ⊖ ((s ⊗ s') ⊗ (snd y' ⊗ fst x')) ⊖ ((s ⊗ s') ⊗ (snd x' ⊗ fst y'))"
      using f44 f45 inv_add  
      by auto
    then have "⊖ ((s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊕ (s ⊗ s') ⊗ (snd x' ⊗ fst y')) =
      ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')"
      using l_minus[of "s ⊗ s'"]
      by (simp add: a_minus_def f15 f16 f45)
    then have "(snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y') =
      (snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ ((s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊕ (s ⊗ s') ⊗ (snd x' ⊗ fst y'))"
      using right_inv_add ‹snd x' ⊗ snd y' ∈ carrier R› assms(2) f13 f19 f34 f44 f45 rel_def 
      by auto
    then have "(snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y') =
      (snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ ((s ⊗ s') ⊗ (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y'))"
      using r_distr
      by (simp add: f35)
    then have "((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x')) ⊕ ((snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')) 
      = (snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ ((s ⊗ s') ⊗ (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y'))"
      using f43bis 
      by simp
    then have "(t ⊗ t') ⊗ (((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x')) ⊕ ((snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')))
      = (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ ((s ⊗ s') ⊗ (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y')))"
      by simp
    then have "(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r) ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x')) ⊕
      (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd x' ⊗ fst y')) =
      (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ ((s ⊗ s') ⊗ (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y')))"
      using r_distr[of _ _ "t ⊗ t'"] f17 f18 ‹t' ⊗ s' ⊗ snd y' ⊗ (t ⊗ (snd x' ⊗ r ⊖ s ⊗ fst x')) ⊕ t ⊗ s ⊗ snd x' ⊗ (t' ⊗ (snd y' ⊗ r' ⊖ s' ⊗ fst y')) = t ⊗ t' ⊗ (snd x' ⊗ snd y' ⊗ (s' ⊗ r) ⊖ s ⊗ s' ⊗ (snd y' ⊗ fst x') ⊕ (snd x' ⊗ snd y' ⊗ (s ⊗ r') ⊖ s ⊗ s' ⊗ (snd x' ⊗ fst y')))› f40 
      by auto
    then have "(t' ⊗ s' ⊗ snd y') ⊗ (t ⊗ (snd x' ⊗ r ⊖ s ⊗ fst x')) ⊕ 
      (t ⊗ s ⊗ snd x') ⊗ (t' ⊗ (snd y' ⊗ r' ⊖ s' ⊗ fst y')) = 
      (t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y'))"
      using f40 
      by simp
    then have "(t ⊗ t') ⊗ ((snd x' ⊗ snd y') ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊖ (s ⊗ s') ⊗ (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y')) = 𝟬"
      using f5 f7
      by (simp add: ‹t ⊗ s ⊗ snd x' ∈ carrier R› f9)
    thus ?thesis
      using rel_def f8 
      by auto
  qed
  then have "(s' ⊗ r ⊕ s ⊗ r' |⇘rel⇙ s ⊗ s') = (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y' |⇘rel⇙ snd x' ⊗ snd y')"
  proof-
    have "(s' ⊗ r ⊕ s ⊗ r', s ⊗ s') ∈ carrier rel"
      using assms rel_def submonoid.m_closed
      by (smt add.m_closed m_closed mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) 
          rev_subsetD subset)
    have "(snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y', snd x' ⊗ snd y') ∈ carrier rel"
      using rel_def f1 f2 subset submonoid.m_closed eq_class_of_rng_of_frac_def
      by (smt Product_Type.Collect_case_prodD add.m_closed mem_Sigma_iff member_class_to_carrier 
          partial_object.select_convs(1) semiring_simprules(3) rev_subsetD)
    thus ?thesis
      using elem_eq_class[of rel] equiv_obj_rng_of_frac
      by (metis ‹(s' ⊗ r ⊕ s ⊗ r', s ⊗ s') .=⇘rel⇙ (snd y' ⊗ fst x' ⊕ snd x' ⊗ fst y', snd x' ⊗ snd y')› 
          ‹(s' ⊗ r ⊕ s ⊗ r', s ⊗ s') ∈ carrier rel› class_of_to_rel)
  qed
  thus ?thesis
    using f3 
    by simp
qed

lemma closed_add_rng_of_frac:
  assumes "(r, s) ∈ carrier rel" and "(r', s') ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') ∈ set_class_of⇘rel⇙"
proof-
  have f1:"(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') = (s' ⊗ r ⊕ s ⊗ r' |⇘rel⇙ s ⊗ s')"
    using assms add_rng_of_frac_fundamental_lemma 
    by simp
  have f2:"s' ⊗ r ⊕ s ⊗ r' ∈ carrier R"
    using assms rel_def
    by (metis (no_types, lifting) add.m_closed mem_Sigma_iff monoid.m_closed monoid_axioms 
        partial_object.select_convs(1) rev_subsetD subset)
  have f3:"s ⊗ s' ∈ S"
    using assms rel_def submonoid.m_closed 
    by simp
  from f2 and f3 have "(s' ⊗ r ⊕ s ⊗ r', s ⊗ s') ∈ carrier rel"
    by (simp add: rel_def)
  thus ?thesis
    using set_eq_class_of_rng_of_frac_def f1 
    by auto
qed

lemma closed_rel_add:
  assumes "(r, s) ∈ carrier rel" and "(r', s') ∈ carrier rel"
  shows "(s' ⊗ r ⊕ s ⊗ r', s ⊗ s') ∈ carrier rel"
proof-
  have "s ⊗ s' ∈ S"
    using assms rel_def submonoid.m_closed 
    by simp
  have "s' ⊗ r ⊕ s ⊗ r' ∈ carrier R"
    using assms rel_def
    by (metis (no_types, lifting) add.m_closed mem_Sigma_iff monoid.m_closed monoid_axioms 
        partial_object.select_convs(1) rev_subsetD subset)
  thus ?thesis
    using rel_def
    by (simp add: ‹s ⊗ s' ∈ S›)
qed

lemma assoc_add_rng_of_frac:
  assumes "(r, s) ∈ carrier rel" and "(r', s') ∈ carrier rel" and "(r'', s'') ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') ⊕⇘rec_rng_of_frac⇙ (r''|⇘rel⇙ s'') =
  (r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ ((r' |⇘rel⇙ s') ⊕⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s''))"
proof-
  have "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') = (s' ⊗ r ⊕ s ⊗ r' |⇘rel⇙ s ⊗ s')"
    using assms(1) assms(2) add_rng_of_frac_fundamental_lemma 
    by simp
  then have f1:"(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') ⊕⇘rec_rng_of_frac⇙ (r''|⇘rel⇙ s'') =
    (s'' ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊕ (s ⊗ s') ⊗ r'' |⇘rel⇙ (s ⊗ s') ⊗ s'')"
    using assms add_rng_of_frac_fundamental_lemma closed_rel_add 
    by simp
  have "(r' |⇘rel⇙ s') ⊕⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'') = (s'' ⊗ r' ⊕ s' ⊗ r'' |⇘rel⇙ s' ⊗ s'')"
    using assms(2) assms(3) add_rng_of_frac_fundamental_lemma 
    by simp
  then have f2:"(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ ((r' |⇘rel⇙ s') ⊕⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'')) =
    ((s' ⊗ s'') ⊗ r ⊕ s ⊗ (s'' ⊗ r' ⊕ s' ⊗ r'') |⇘rel⇙ s ⊗ (s' ⊗ s''))"
    using assms add_rng_of_frac_fundamental_lemma closed_rel_add 
    by simp
  have f3:"(s ⊗ s') ⊗ s'' = s ⊗ (s' ⊗ s'')"
    using m_assoc subset assms rel_def
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1) rev_subsetD)
  have "s'' ⊗ (s' ⊗ r ⊕ s ⊗ r') ⊕ (s ⊗ s') ⊗ r'' = (s' ⊗ s'') ⊗ r ⊕ s ⊗ (s'' ⊗ r' ⊕ s' ⊗ r'')"
    by (smt a_assoc assms m_comm mem_Sigma_iff monoid.m_assoc monoid.m_closed monoid_axioms 
        partial_object.select_convs(1) r_distr rel_def subset subset_iff)
  thus ?thesis
    using f1 f2 f3 
    by simp
qed

lemma add_rng_of_frac_zero:
  shows "(𝟬 |⇘rel⇙ 𝟭) ∈ set_class_of⇘rel⇙"
  by (metis (no_types, lifting) closed_mult_rng_of_frac mem_Sigma_iff monoid.simps(2) one_closed 
      partial_object.select_convs(1) rec_monoid_rng_of_frac_def rel_def right_unit_mult_rng_of_frac semiring_simprules(4) zero_closed)

lemma l_unit_add_rng_of_frac:
  assumes "(r, s) ∈ carrier rel"
  shows "𝟬⇘rec_rng_of_frac⇙ ⊕⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = (r |⇘rel⇙ s)"
proof-
  have "(𝟬 |⇘rel⇙ 𝟭) ⊕⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = (s ⊗ 𝟬 ⊕ 𝟭 ⊗ r |⇘rel⇙ 𝟭 ⊗ s)"
    using assms add_rng_of_frac_fundamental_lemma
    by (simp add: rel_def)
  then have "(𝟬 |⇘rel⇙ 𝟭) ⊕⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = (r |⇘rel⇙ s)"
    using assms rel_def subset 
    by auto
  thus ?thesis
    using rec_rng_of_frac_def 
    by simp
qed

lemma r_unit_add_rng_of_frac:
  assumes "(r, s) ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ 𝟬⇘rec_rng_of_frac⇙ = (r |⇘rel⇙ s)"
proof-
  have "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (𝟬 |⇘rel⇙ 𝟭) = (𝟭 ⊗ r ⊕ s ⊗ 𝟬 |⇘rel⇙ s ⊗ 𝟭)"
    using assms add_rng_of_frac_fundamental_lemma
    by (simp add: rel_def)
  then have "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (𝟬 |⇘rel⇙ 𝟭) = (r |⇘rel⇙ s)"
    using assms rel_def subset 
    by auto
  thus ?thesis
    using rec_rng_of_frac_def 
    by simp
qed

lemma comm_add_rng_of_frac:
  assumes "(r, s) ∈ carrier rel" and "(r', s') ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') = (r' |⇘rel⇙ s') ⊕⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s)"
proof-
  have f1:"(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') = (s' ⊗ r ⊕ s ⊗ r' |⇘rel⇙ s ⊗ s')"
    using assms add_rng_of_frac_fundamental_lemma 
    by simp
 have f2:"(r' |⇘rel⇙ s') ⊕⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = (s ⊗ r' ⊕ s' ⊗ r |⇘rel⇙ s' ⊗ s)"
   using assms add_rng_of_frac_fundamental_lemma 
   by simp
  thus ?thesis
    using f1 f2
    by (metis (no_types, lifting) add.m_comm assms(1) assms(2) m_comm mem_Sigma_iff 
        partial_object.select_convs(1) rel_def semiring_simprules(3) rev_subsetD subset)
qed

lemma class_of_zero_rng_of_frac:
  assumes "s ∈ S"
  shows "(𝟬 |⇘rel⇙ s) = 𝟬⇘rec_rng_of_frac⇙"
proof-
  have f1:"(𝟬, s) ∈ carrier rel"
    using assms rel_def 
    by simp
  have "𝟭 ⊗ (𝟭 ⊗ 𝟬 ⊖ s ⊗ 𝟬) = 𝟬"
    using assms local.ring_axioms rev_subsetD ring.ring_simprules(14) subset 
    by fastforce
  then have "(𝟬, s) .=⇘rel⇙ (𝟬, 𝟭)"
    using rel_def submonoid.one_closed 
    by auto
  thus ?thesis
    using elem_eq_class equiv_obj_rng_of_frac f1 rec_rng_of_frac_def
    by (metis (no_types, lifting) class_of_to_rel mem_Sigma_iff one_closed partial_object.select_convs(1) 
        rel_def ring_record_simps(11))
qed

lemma r_inv_add_rng_of_frac:
  assumes "(r, s) ∈ carrier rel"
  shows "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (⊖ r |⇘rel⇙ s) = 𝟬⇘rec_rng_of_frac⇙"
proof-
  have "(⊖ r, s) ∈ carrier rel"
    using assms rel_def 
    by simp
  then have "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (⊖ r |⇘rel⇙ s) = (s ⊗ r ⊕ s ⊗ ⊖ r |⇘rel⇙ s ⊗ s)"
    using assms add_rng_of_frac_fundamental_lemma 
    by simp
  then have "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (⊖ r |⇘rel⇙ s) = (𝟬 |⇘rel⇙ s ⊗ s)"
    using r_minus[of s r] assms rel_def subset rev_subsetD r_neg 
    by auto
  thus ?thesis
    using class_of_zero_rng_of_frac assms rel_def submonoid.m_closed 
    by simp
qed

lemma l_inv_add_rng_of_frac:
  assumes "(r, s) ∈ carrier rel"
  shows "(⊖ r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = 𝟬⇘rec_rng_of_frac⇙"
proof-
  have "(⊖ r, s) ∈ carrier rel"
    using assms rel_def 
    by simp
  then have "(⊖ r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = (s ⊗ ⊖ r ⊕ s ⊗ r |⇘rel⇙ s ⊗ s)"
    using assms add_rng_of_frac_fundamental_lemma 
    by simp
  then have "(⊖ r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = (𝟬 |⇘rel⇙ s ⊗ s)"
    using r_minus[of s r] assms rel_def subset rev_subsetD l_neg 
    by auto
  thus ?thesis
    using class_of_zero_rng_of_frac assms rel_def submonoid.m_closed 
    by simp
qed

lemma abelian_group_rng_of_frac:
  shows "abelian_group (rec_rng_of_frac)"
proof
  show "⋀x y. ⟦x ∈ carrier (add_monoid rec_rng_of_frac);
            y ∈ carrier (add_monoid rec_rng_of_frac)⟧
           ⟹ x ⊗⇘add_monoid rec_rng_of_frac⇙ y
               ∈ carrier (add_monoid rec_rng_of_frac)"
    using closed_add_rng_of_frac
    by (smt mem_Collect_eq monoid.select_convs(1) partial_object.select_convs(1) rec_rng_of_frac_def 
        set_eq_class_of_rng_of_frac_def)
  show "⋀x y z.
       ⟦x ∈ carrier (add_monoid rec_rng_of_frac);
        y ∈ carrier (add_monoid rec_rng_of_frac);
        z ∈ carrier (add_monoid rec_rng_of_frac)⟧
       ⟹ x ⊗⇘add_monoid rec_rng_of_frac⇙ y ⊗⇘add_monoid rec_rng_of_frac⇙ z =
           x ⊗⇘add_monoid rec_rng_of_frac⇙ (y ⊗⇘add_monoid rec_rng_of_frac⇙ z)"
    using assoc_add_rng_of_frac
    by (smt mem_Collect_eq monoid.simps(1) partial_object.select_convs(1) rec_rng_of_frac_def 
        set_eq_class_of_rng_of_frac_def)
  show "𝟭⇘add_monoid rec_rng_of_frac⇙ ∈ carrier (add_monoid rec_rng_of_frac)"
    using add_rng_of_frac_zero by (simp add: rec_rng_of_frac_def)
  show "⋀x. x ∈ carrier (add_monoid rec_rng_of_frac) ⟹
         𝟭⇘add_monoid rec_rng_of_frac⇙ ⊗⇘add_monoid rec_rng_of_frac⇙ x = x"
    using l_unit_add_rng_of_frac
    by (smt mem_Collect_eq monoid.select_convs(1) monoid.select_convs(2) partial_object.select_convs(1) 
        rec_rng_of_frac_def set_eq_class_of_rng_of_frac_def)
  show "⋀x. x ∈ carrier (add_monoid rec_rng_of_frac) ⟹
         x ⊗⇘add_monoid rec_rng_of_frac⇙ 𝟭⇘add_monoid rec_rng_of_frac⇙ = x"
    using r_unit_add_rng_of_frac
    by (smt mem_Collect_eq monoid.select_convs(1) monoid.select_convs(2) partial_object.select_convs(1) 
        rec_rng_of_frac_def set_eq_class_of_rng_of_frac_def)
  show "⋀x y. ⟦x ∈ carrier (add_monoid rec_rng_of_frac); y ∈ carrier (add_monoid rec_rng_of_frac)⟧
           ⟹ x ⊗⇘add_monoid rec_rng_of_frac⇙ y = y ⊗⇘add_monoid rec_rng_of_frac⇙ x"
    using comm_add_rng_of_frac
    by (smt mem_Collect_eq monoid.select_convs(1) partial_object.select_convs(1) rec_rng_of_frac_def 
        set_eq_class_of_rng_of_frac_def)
  show "carrier (add_monoid rec_rng_of_frac) ⊆ Units (add_monoid rec_rng_of_frac)"
  proof
    show "x ∈ Units (add_monoid rec_rng_of_frac)" if "x ∈ carrier (add_monoid rec_rng_of_frac)" for x
    proof-
      have "x ∈ set_class_of⇘rel⇙"
        using that rec_rng_of_frac_def by simp
      then obtain r and s where f1:"(r, s) ∈ carrier rel" and f2:"x = (r |⇘rel⇙ s)"
        using set_eq_class_of_rng_of_frac_def
        by (smt mem_Collect_eq)
      then have f3:"(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (⊖ r |⇘rel⇙ s) = 𝟬⇘rec_rng_of_frac⇙"
        using f1 r_inv_add_rng_of_frac[of r s] 
        by simp
      have f4:"(⊖ r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = 𝟬⇘rec_rng_of_frac⇙"
        using f1 l_inv_add_rng_of_frac[of r s] 
        by simp
      then have "∃y ∈ set_class_of⇘rel⇙. y ⊕⇘rec_rng_of_frac⇙ x = 𝟬⇘rec_rng_of_frac⇙ ∧ x ⊕⇘rec_rng_of_frac⇙ y = 𝟬⇘rec_rng_of_frac⇙"
        using f2 f3 f4
        by (metis (no_types, lifting) abelian_group.a_inv_closed class_of_zero_rng_of_frac 
            closed_add_rng_of_frac f1 is_abelian_group mem_Sigma_iff partial_object.select_convs(1) 
            rel_def r_unit_add_rng_of_frac zero_closed) 
      thus "x ∈ Units (add_monoid rec_rng_of_frac)"
        using rec_rng_of_frac_def that by (simp add: Units_def)
    qed
  qed
qed

lemma r_distr_rng_of_frac:
  assumes "(r, s) ∈ carrier rel" and "(r', s') ∈ carrier rel" and "(r'', s'') ∈ carrier rel"
  shows "((r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s')) ⊗⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'') = 
    (r |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'') ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') ⊗⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'')"
proof-
  have "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') = (s' ⊗ r ⊕ s ⊗ r' |⇘rel⇙ s ⊗ s')"
    using assms(1) assms(2) add_rng_of_frac_fundamental_lemma 
    by simp
  then have f1:"((r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s')) ⊗⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'') =
    ((s' ⊗ r ⊕ s ⊗ r') ⊗ r'' |⇘rel⇙ (s ⊗ s') ⊗ s'')"
    using assms mult_rng_of_frac_fundamental_lemma
    by (simp add: closed_rel_add rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f2:"(r |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'') = (r ⊗ r'' |⇘rel⇙ s ⊗ s'')"
    using assms(1) assms(3) mult_rng_of_frac_fundamental_lemma
    by (simp add: rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f3:"(r' |⇘rel⇙ s') ⊗⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'') = (r' ⊗ r'' |⇘rel⇙ s' ⊗ s'')"
    using assms(2) assms(3) mult_rng_of_frac_fundamental_lemma
    by (simp add: rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f4:"(r ⊗ r'', s ⊗ s'') ∈ carrier rel"
    using rel_def assms(1) assms(3) submonoid.m_closed 
    by simp
  have f5:"(r' ⊗ r'', s' ⊗ s'') ∈ carrier rel"
    using rel_def assms(2) assms(3) submonoid.m_closed 
    by simp
  from f2 and f3 have f6:"(r |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'') ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') ⊗⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'')
    = ((s' ⊗ s'') ⊗ (r ⊗ r'') ⊕ (s ⊗ s'') ⊗ (r' ⊗ r'') |⇘rel⇙ (s ⊗ s'') ⊗ (s' ⊗ s''))"
    using assms f4 f5 submonoid.m_closed add_rng_of_frac_fundamental_lemma 
    by simp
  have "(s ⊗ s'' ⊗ (s' ⊗ s'')) ⊗ ((s' ⊗ r ⊕ s ⊗ r') ⊗ r'') = (s ⊗ s'' ⊗ (s' ⊗ s'')) ⊗ (s' ⊗ r  ⊗ r'' ⊕ s ⊗ r' ⊗ r'')"
    using assms rel_def subset rev_subsetD l_distr
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  then have f7:"(s ⊗ s'' ⊗ (s' ⊗ s'')) ⊗ ((s' ⊗ r ⊕ s ⊗ r') ⊗ r'') = 
    (s ⊗ s'' ⊗ (s' ⊗ s'')) ⊗ (s' ⊗ r  ⊗ r'') ⊕ (s ⊗ s'' ⊗ (s' ⊗ s'')) ⊗ (s ⊗ r' ⊗ r'')"
    using assms rel_def subset rev_subsetD submonoid.m_closed r_distr
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  have f8:"(s ⊗ s' ⊗ s'') ⊗ (s' ⊗ s'' ⊗ (r ⊗ r'') ⊕ s ⊗ s'' ⊗ (r' ⊗ r'')) = 
    (s ⊗ s' ⊗ s'') ⊗ (s' ⊗ s'' ⊗ (r ⊗ r'')) ⊕ (s ⊗ s' ⊗ s'') ⊗ (s ⊗ s'' ⊗ (r' ⊗ r''))"
    using assms rel_def subset rev_subsetD submonoid.m_closed r_distr
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  have "(s ⊗ s'' ⊗ (s' ⊗ s'')) = (s ⊗ (s'' ⊗ s') ⊗ s'')"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_assoc
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  then have f9:"(s ⊗ s'' ⊗ (s' ⊗ s'')) = (s ⊗ s' ⊗ (s'' ⊗ s''))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_comm m_assoc
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  then have f10:"(s ⊗ s'' ⊗ (s' ⊗ s'')) ⊗ (s' ⊗ r  ⊗ r'') = (s ⊗ s' ⊗ s'') ⊗ (s' ⊗ s'' ⊗ (r ⊗ r''))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_assoc m_comm
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  have "(s ⊗ s'' ⊗ (r' ⊗ r'')) = (s'' ⊗ s ⊗ (r' ⊗ r''))"
    using assms rel_def subset rev_subsetD m_comm
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1))
  then have "(s ⊗ s'' ⊗ (s' ⊗ s'')) ⊗ (s ⊗ r' ⊗ r'') = (s ⊗ s' ⊗ s'') ⊗ (s ⊗ s'' ⊗ (r' ⊗ r''))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_comm m_assoc f9
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  then have "((s ⊗ s'' ⊗ (s' ⊗ s'')) ⊗ ((s' ⊗ r ⊕ s ⊗ r') ⊗ r'') = (s ⊗ s' ⊗ s'') ⊗ (s' ⊗ s'' ⊗ (r ⊗ r'') ⊕ s ⊗ s'' ⊗ (r' ⊗ r'')))"
    using  f7 f8 f10 
    by presburger
  then have "((s ⊗ s'' ⊗ (s' ⊗ s'')) ⊗ ((s' ⊗ r ⊕ s ⊗ r') ⊗ r'') ⊖ (s ⊗ s' ⊗ s'') ⊗ (s' ⊗ s'' ⊗ (r ⊗ r'') ⊕ s ⊗ s'' ⊗ (r' ⊗ r''))) = 𝟬"
    by (smt a_minus_def assms(1) assms(2) assms(3) closed_rel_add mem_Sigma_iff 
        partial_object.select_convs(1) r_neg rel_def semiring_simprules(3) rev_subsetD subset)
  then have f11:"𝟭 ⊗ (((s ⊗ s'' ⊗ (s' ⊗ s'')) ⊗ ((s' ⊗ r ⊕ s ⊗ r') ⊗ r'') ⊖ (s ⊗ s' ⊗ s'') ⊗ (s' ⊗ s'' ⊗ (r ⊗ r'') ⊕ s ⊗ s'' ⊗ (r' ⊗ r'')))) = 𝟬"
    by simp
  have f12:"((s' ⊗ r ⊕ s ⊗ r') ⊗ r'', s ⊗ s' ⊗ s'') ∈ carrier rel"
    using assms closed_rel_add rel_def 
    by auto
  have f13:"(s' ⊗ s'' ⊗ (r ⊗ r'') ⊕ s ⊗ s'' ⊗ (r' ⊗ r''), s ⊗ s'' ⊗ (s' ⊗ s'')) ∈ carrier rel"
    by (simp add: closed_rel_add f4 f5)
  have "𝟭 ∈ S"
    using submonoid.one_closed 
    by simp
  then have "((s' ⊗ r ⊕ s ⊗ r') ⊗ r'', s ⊗ s' ⊗ s'') .=⇘rel⇙ (s' ⊗ s'' ⊗ (r ⊗ r'') ⊕ s ⊗ s'' ⊗ (r' ⊗ r''), s ⊗ s'' ⊗ (s' ⊗ s''))"
    using rel_def f11 f13 f12 
    by auto
  then have "((s' ⊗ r ⊕ s ⊗ r') ⊗ r''|⇘rel⇙ s ⊗ s' ⊗ s'') = (s' ⊗ s'' ⊗ (r ⊗ r'') ⊕ s ⊗ s'' ⊗ (r' ⊗ r'') |⇘rel⇙ s ⊗ s'' ⊗ (s' ⊗ s''))"
    using elem_eq_class
    by (metis class_of_to_rel equiv_obj_rng_of_frac f12 f13)
  thus ?thesis
    using f1 f6 
    by simp
qed

lemma l_distr_rng_of_frac:
  assumes "(r, s) ∈ carrier rel" and "(r', s') ∈ carrier rel" and "(r'', s'') ∈ carrier rel"
  shows "(r'' |⇘rel⇙ s'') ⊗⇘rec_rng_of_frac⇙ ((r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s')) = 
    (r'' |⇘rel⇙ s'') ⊗⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'') ⊗⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s')"
proof-
  have "(r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') = (s' ⊗ r ⊕ s ⊗ r' |⇘rel⇙ s ⊗ s')"
    using assms(1) assms(2) add_rng_of_frac_fundamental_lemma 
    by simp
  then have f1:"(r'' |⇘rel⇙ s'') ⊗⇘rec_rng_of_frac⇙ ((r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s')) =
    (r'' ⊗ (s' ⊗ r ⊕ s ⊗ r') |⇘rel⇙ s'' ⊗ (s ⊗ s'))"
    using assms mult_rng_of_frac_fundamental_lemma
    by (simp add: closed_rel_add rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f2:"(r'' |⇘rel⇙ s'') ⊗⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) = (r'' ⊗ r |⇘rel⇙ s'' ⊗ s)"
    using assms(1) assms(3) mult_rng_of_frac_fundamental_lemma
    by (simp add: rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f3:"(r'' |⇘rel⇙ s'') ⊗⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s') = (r'' ⊗ r' |⇘rel⇙ s'' ⊗ s')"
    using assms(2) assms(3) mult_rng_of_frac_fundamental_lemma
    by (simp add: rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f4:"(r'' ⊗ r, s'' ⊗ s) ∈ carrier rel"
    using rel_def assms(1) assms(3) submonoid.m_closed 
    by simp
  have f5:"(r'' ⊗ r', s'' ⊗ s') ∈ carrier rel"
    using rel_def assms(2) assms(3) submonoid.m_closed 
    by simp
  from f2 and f3 have f6:"(r'' |⇘rel⇙ s'') ⊗⇘rec_rng_of_frac⇙ (r |⇘rel⇙ s) ⊕⇘rec_rng_of_frac⇙ (r'' |⇘rel⇙ s'') ⊗⇘rec_rng_of_frac⇙ (r' |⇘rel⇙ s')
    = ((s'' ⊗ s') ⊗ (r'' ⊗ r) ⊕ (s'' ⊗ s) ⊗ (r'' ⊗ r') |⇘rel⇙ (s'' ⊗ s) ⊗ (s'' ⊗ s'))"
    using assms f4 f5 submonoid.m_closed add_rng_of_frac_fundamental_lemma 
    by simp
  have "(s'' ⊗ s ⊗ (s'' ⊗ s')) ⊗ (r'' ⊗ (s' ⊗ r ⊕ s ⊗ r')) = (s'' ⊗ s ⊗ (s'' ⊗ s')) ⊗ (r'' ⊗ (s' ⊗ r) ⊕ r'' ⊗ (s ⊗ r'))"
    using assms rel_def subset rev_subsetD r_distr
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  then have f7:"(s'' ⊗ s ⊗ (s'' ⊗ s')) ⊗ (r'' ⊗ (s' ⊗ r ⊕ s ⊗ r')) = 
    (s'' ⊗ s ⊗ (s'' ⊗ s')) ⊗ (r'' ⊗ (s' ⊗ r)) ⊕ (s'' ⊗ s ⊗ (s'' ⊗ s')) ⊗ (r'' ⊗ (s ⊗ r'))"
    using assms rel_def subset rev_subsetD submonoid.m_closed r_distr
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  have f8:"(s'' ⊗ s ⊗ s') ⊗ (s'' ⊗ s' ⊗ (r'' ⊗ r) ⊕ s'' ⊗ s ⊗ (r'' ⊗ r')) = 
    (s'' ⊗ s ⊗ s') ⊗ (s'' ⊗ s' ⊗ (r'' ⊗ r)) ⊕ (s'' ⊗ s ⊗ s') ⊗ (s'' ⊗ s ⊗ (r'' ⊗ r'))"
    using assms rel_def subset rev_subsetD submonoid.m_closed r_distr
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  have "(s'' ⊗ s ⊗ (s'' ⊗ s')) = (s'' ⊗ (s ⊗ s'') ⊗ s')"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_assoc
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  then have f9:"(s'' ⊗ s ⊗ (s'' ⊗ s')) = (s'' ⊗ s'' ⊗ (s ⊗ s'))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_comm m_assoc
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  then have f10:"(s'' ⊗ s ⊗ (s'' ⊗ s')) ⊗ (r'' ⊗ s' ⊗ r) = (s'' ⊗ s ⊗ s') ⊗ (s'' ⊗ s' ⊗ (r'' ⊗ r))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_assoc m_comm
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  have "(s'' ⊗ s ⊗ (r'' ⊗ r')) = (s ⊗ s'' ⊗ (r'' ⊗ r'))"
    using assms rel_def subset rev_subsetD m_comm
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1))
  then have "(s'' ⊗ s ⊗ (s'' ⊗ s')) ⊗ (r'' ⊗ s ⊗ r') = (s'' ⊗ s ⊗ s') ⊗ (s'' ⊗ s ⊗ (r'' ⊗ r'))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_comm m_assoc f9
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  then have "((s'' ⊗ s ⊗ (s'' ⊗ s')) ⊗ (r'' ⊗ (s' ⊗ r ⊕ s ⊗ r')) = (s'' ⊗ (s ⊗ s')) ⊗ (s'' ⊗ s' ⊗ (r'' ⊗ r) ⊕ s'' ⊗ s ⊗ (r'' ⊗ r')))"
    using  f7 f8 f10
    by (smt assms(1) assms(2) assms(3) m_assoc mem_Sigma_iff partial_object.select_convs(1) rel_def 
        rev_subsetD subset)
  then have "((s'' ⊗ s ⊗ (s'' ⊗ s')) ⊗ (r'' ⊗ (s' ⊗ r ⊕ s ⊗ r')) ⊖ (s'' ⊗ (s ⊗ s')) ⊗ (s'' ⊗ s' ⊗ (r'' ⊗ r) ⊕ s'' ⊗ s ⊗ (r'' ⊗ r'))) = 𝟬"
    by (smt a_minus_def assms(1) assms(2) assms(3) closed_rel_add mem_Sigma_iff partial_object.select_convs(1) 
        r_neg rel_def semiring_simprules(3) rev_subsetD subset)
  then have f11:"𝟭 ⊗ (((s'' ⊗ s ⊗ (s'' ⊗ s')) ⊗ (r'' ⊗ (s' ⊗ r ⊕ s ⊗ r')) ⊖ (s'' ⊗ (s ⊗ s')) ⊗ (s'' ⊗ s' ⊗ (r'' ⊗ r) ⊕ s'' ⊗ s ⊗ (r'' ⊗ r')))) = 𝟬"
    by simp
  have f12:"(r'' ⊗ (s' ⊗ r ⊕ s ⊗ r'), s'' ⊗ (s ⊗ s')) ∈ carrier rel"
    using assms closed_rel_add rel_def 
    by auto
  have f13:"(s'' ⊗ s' ⊗ (r'' ⊗ r) ⊕ s'' ⊗ s ⊗ (r'' ⊗ r'), s'' ⊗ s ⊗ (s'' ⊗ s')) ∈ carrier rel"
    by (simp add: closed_rel_add f4 f5)
  have "𝟭 ∈ S"
    using submonoid.one_closed 
    by simp
  then have "(r'' ⊗ (s' ⊗ r ⊕ s ⊗ r'), s'' ⊗ (s ⊗ s')) .=⇘rel⇙ (s'' ⊗ s' ⊗ (r'' ⊗ r) ⊕ s'' ⊗ s ⊗ (r'' ⊗ r'), s'' ⊗ s ⊗ (s'' ⊗ s'))"
    using rel_def f11 f13 f12 
    by auto
  then have "(r'' ⊗ (s' ⊗ r ⊕ s ⊗ r') |⇘rel⇙ s'' ⊗ (s ⊗ s')) = (s'' ⊗ s' ⊗ (r'' ⊗ r) ⊕ s'' ⊗ s ⊗ (r'' ⊗ r') |⇘rel⇙ s'' ⊗ s ⊗ (s'' ⊗ s'))"
    using elem_eq_class
    by (metis class_of_to_rel equiv_obj_rng_of_frac f12 f13)
  thus ?thesis
    using f1 f6 
    by simp
qed

lemma rng_rng_of_frac:
  shows "ring (rec_rng_of_frac)"
proof-
  have f1:"∀x y z. x ∈ carrier rec_rng_of_frac ⟶ y ∈ carrier rec_rng_of_frac ⟶ z ∈ carrier rec_rng_of_frac 
    ⟶ (x ⊕⇘rec_rng_of_frac⇙ y) ⊗⇘rec_rng_of_frac⇙ z = x ⊗⇘rec_rng_of_frac⇙ z ⊕⇘rec_rng_of_frac⇙ y ⊗⇘rec_rng_of_frac⇙ z"
    using r_distr_rng_of_frac rec_rng_of_frac_def
    by (smt mem_Collect_eq partial_object.select_convs(1) set_eq_class_of_rng_of_frac_def)
  have f2:"∀x y z. x ∈ carrier rec_rng_of_frac ⟶ y ∈ carrier rec_rng_of_frac ⟶ z ∈ carrier rec_rng_of_frac 
    ⟶ z ⊗⇘rec_rng_of_frac⇙ (x ⊕⇘rec_rng_of_frac⇙ y) = z ⊗⇘rec_rng_of_frac⇙ x ⊕⇘rec_rng_of_frac⇙ z ⊗⇘rec_rng_of_frac⇙ y"
    using l_distr_rng_of_frac rec_rng_of_frac_def
    by (smt mem_Collect_eq partial_object.select_convs(1) set_eq_class_of_rng_of_frac_def)
  then have "ring_axioms (rec_rng_of_frac)"
    using ring_axioms_def f1 f2 
    by auto
  thus ?thesis  
    using ring_def[of rec_rng_of_frac] abelian_group_rng_of_frac monoid_rng_of_frac rec_rng_of_frac_def 
      abelian_group_axioms_def rec_monoid_rng_of_frac_def eq_class_of_rng_of_frac_def
    by (simp add: Group.monoid_def)
qed

lemma crng_rng_of_frac:
  shows "cring (rec_rng_of_frac)"
  using cring_def[of rec_rng_of_frac] rng_rng_of_frac comm_monoid_rng_of_frac rec_rng_of_frac_def 
    rec_monoid_rng_of_frac_def eq_class_of_rng_of_frac_def
  by (metis (no_types, lifting) comm_monoid.m_comm monoid.monoid_comm_monoidI monoid.select_convs(1) 
      partial_object.select_convs(1) ring.is_monoid)

lemma simp_in_frac:
  assumes "(r, s) ∈ carrier rel" and "s' ∈ S"
  shows "(r |⇘rel⇙ s) = (s' ⊗ r |⇘rel⇙ s' ⊗ s)"
proof-
  have f1:"(s' ⊗ r, s' ⊗ s) ∈ carrier rel"
    using assms rel_def submonoid.m_closed subset rev_subsetD 
    by auto
  have "(s' ⊗ s) ⊗ r ⊖ s ⊗ (s' ⊗ r) = (s' ⊗ s) ⊗ r ⊖ (s ⊗ s') ⊗ r"
    using assms subset rev_subsetD m_assoc[of s s' r] rel_def
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1))
  then have "(s' ⊗ s) ⊗ r ⊖ s ⊗ (s' ⊗ r) = (s' ⊗ s) ⊗ r ⊖ (s' ⊗ s) ⊗ r"
    using m_comm[of s s'] assms subset rev_subsetD rel_def
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1))
  then have "(s' ⊗ s) ⊗ r ⊖ s ⊗ (s' ⊗ r) = 𝟬"
    by (metis (no_types, lifting) a_minus_def assms mem_Sigma_iff partial_object.select_convs(1) 
        r_neg rel_def semiring_simprules(3) rev_subsetD subset)
  then have "𝟭 ⊗ ((s' ⊗ s) ⊗ r ⊖ s ⊗ (s' ⊗ r)) = 𝟬"
    by simp
  then have "(r, s) .=⇘rel⇙ (s' ⊗ r, s' ⊗ s)"
    using assms(1) f1 rel_def one_closed 
    by auto
  thus ?thesis
    using elem_eq_class
    by (metis assms(1) class_of_to_rel equiv_obj_rng_of_frac f1)
qed

subsection ‹The Natural Homomorphism from a Ring to Its Localization›

definition rng_to_rng_of_frac :: "'a ⇒ ('a × 'a) set" where
"rng_to_rng_of_frac r ≡ (r |⇘rel⇙ 𝟭)"

lemma rng_to_rng_of_frac_is_ring_hom :
  shows "rng_to_rng_of_frac ∈ ring_hom R rec_rng_of_frac"
proof-
  have f1:"rng_to_rng_of_frac ∈ carrier R → carrier rec_rng_of_frac"
    using rng_to_rng_of_frac_def rec_rng_of_frac_def set_eq_class_of_rng_of_frac_def rel_def 
    by fastforce
  have f2:"∀x y. x ∈ carrier R ∧ y ∈ carrier R 
    ⟶ rng_to_rng_of_frac (x ⊗⇘R⇙ y) = rng_to_rng_of_frac x ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac y"
  proof(rule allI, rule allI, rule impI)
    fix x y
    assume "x ∈ carrier R ∧ y ∈ carrier R"
    have f1:"rng_to_rng_of_frac (x ⊗⇘R⇙ y) = (x ⊗ y |⇘rel⇙ 𝟭)"
      using rng_to_rng_of_frac_def 
      by simp
    have "rng_to_rng_of_frac x ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac y = (x |⇘rel⇙ 𝟭) ⊗⇘rec_rng_of_frac⇙ (y |⇘rel⇙ 𝟭)"
      using rng_to_rng_of_frac_def 
      by simp
    then have "rng_to_rng_of_frac x ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac y = (x ⊗ y |⇘rel⇙ 𝟭)"
      using mult_rng_of_frac_fundamental_lemma
      by (simp add: ‹x ∈ carrier R ∧ y ∈ carrier R› rec_monoid_rng_of_frac_def rec_rng_of_frac_def rel_def)
    thus "rng_to_rng_of_frac (x ⊗⇘R⇙ y) = rng_to_rng_of_frac x ⊗⇘rec_rng_of_frac⇙ rng_to_rng_of_frac y"
      using f1 
      by auto
  qed
  have f3:"∀x y. x ∈ carrier R ∧ y ∈ carrier R
    ⟶ rng_to_rng_of_frac (x ⊕⇘R⇙ y) = rng_to_rng_of_frac x ⊕⇘rec_rng_of_frac⇙ rng_to_rng_of_frac y"
  proof(rule allI, rule allI, rule impI)
    fix x y
    assume a:"x ∈ carrier R ∧ y ∈ carrier R"
    have f1:"rng_to_rng_of_frac (x ⊕⇘R⇙ y) = (x ⊕ y |⇘rel⇙ 𝟭)"
      using rng_to_rng_of_frac_def 
      by simp
    have "rng_to_rng_of_frac x ⊕⇘rec_rng_of_frac⇙ rng_to_rng_of_frac y = (x |⇘rel⇙ 𝟭) ⊕⇘rec_rng_of_frac⇙ (y |⇘rel⇙ 𝟭)"
      using rng_to_rng_of_frac_def 
      by simp
    then have "rng_to_rng_of_frac x ⊕⇘rec_rng_of_frac⇙ rng_to_rng_of_frac y = (𝟭 ⊗ x ⊕ 𝟭 ⊗ y |⇘rel⇙ 𝟭 ⊗ 𝟭)"
      using mult_rng_of_frac_fundamental_lemma a 
        eq_obj_rng_of_frac.add_rng_of_frac_fundamental_lemma eq_obj_rng_of_frac.rng_to_rng_of_frac_def 
        eq_obj_rng_of_frac_axioms f1 
      by fastforce
    then have "rng_to_rng_of_frac x ⊕⇘rec_rng_of_frac⇙ rng_to_rng_of_frac y = (x ⊕ y |⇘rel⇙ 𝟭)"
      using l_one a 
      by simp     
    thus "rng_to_rng_of_frac (x ⊕⇘R⇙ y) = rng_to_rng_of_frac x ⊕⇘rec_rng_of_frac⇙ rng_to_rng_of_frac y"
      using f1 
      by auto
  qed
  have "rng_to_rng_of_frac 𝟭 = (𝟭 |⇘rel⇙ 𝟭)"
    using rng_to_rng_of_frac_def 
    by simp
  then have f4:"rng_to_rng_of_frac 𝟭⇘R⇙ = 𝟭⇘rec_rng_of_frac⇙"
    using rec_rng_of_frac_def 
    by simp
  thus ?thesis
    using ring_hom_def[of R rec_rng_of_frac] f1 f2 f3 f4 
    by simp
qed

lemma Im_rng_to_rng_of_frac_unit:
  assumes "x ∈ rng_to_rng_of_frac ` S"
  shows "x ∈ Units rec_rng_of_frac"
proof-
  obtain s where a1:"s ∈ S" and a2:"x = (s |⇘rel⇙ 𝟭)"
    using assms rng_to_rng_of_frac_def rel_def
    by auto
  then have "(s |⇘rel⇙ 𝟭) ⊗⇘rec_rng_of_frac⇙ (𝟭 |⇘rel⇙ s) = (s ⊗ 𝟭 |⇘rel⇙ s ⊗ 𝟭)"
    using mult_rng_of_frac_fundamental_lemma rec_monoid_rng_of_frac_def rec_rng_of_frac_def rel_def subset 
    by auto
  then have f1:"(s |⇘rel⇙ 𝟭) ⊗⇘rec_rng_of_frac⇙ (𝟭 |⇘rel⇙ s) = (𝟭 |⇘rel⇙ 𝟭)"
    using simp_in_frac a1 rel_def 
    by auto
  have "(𝟭 |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ (s |⇘rel⇙ 𝟭) = (s ⊗ 𝟭 |⇘rel⇙ s ⊗ 𝟭)"
    using mult_rng_of_frac_fundamental_lemma rec_monoid_rng_of_frac_def rec_rng_of_frac_def rel_def 
      subset a1 
    by auto
  then have f2:"(𝟭 |⇘rel⇙ s) ⊗⇘rec_rng_of_frac⇙ (s |⇘rel⇙ 𝟭) = (𝟭 |⇘rel⇙ 𝟭)"
    using simp_in_frac  a1 rel_def
    by auto
  then have f3:"∃y∈carrier rec_rng_of_frac. y ⊗⇘rec_rng_of_frac⇙ x = 𝟭⇘rec_rng_of_frac⇙ ∧ 
    x ⊗⇘rec_rng_of_frac⇙ y = 𝟭⇘rec_rng_of_frac⇙"
    using rec_rng_of_frac_def f1 f2 a2 rel_def a1
    by (metis (no_types, lifting) class_of_zero_rng_of_frac closed_add_rng_of_frac l_unit_add_rng_of_frac 
        mem_Sigma_iff monoid.select_convs(2) partial_object.select_convs(1) semiring_simprules(4) zero_closed)
  have "x ∈ carrier rec_rng_of_frac"
    using a2 a1 subset rev_subsetD rec_rng_of_frac_def
    by (metis (no_types, opaque_lifting) ring_hom_closed rng_to_rng_of_frac_def rng_to_rng_of_frac_is_ring_hom)
  thus ?thesis
    using Units_def[of rec_rng_of_frac] f3 
    by auto
qed

lemma eq_class_to_rel:
  assumes "(r, s) ∈ carrier R × S" and "(r', s') ∈ carrier R × S" and "(r |⇘rel⇙ s) = (r' |⇘rel⇙ s')"
  shows "(r, s) .=⇘rel⇙ (r', s')"
proof-
  have "(r, s) ∈ (r |⇘rel⇙ s)"
    using assms(1) equiv_obj_rng_of_frac equivalence_def
    by (metis (no_types, lifting) CollectI case_prodI eq_class_of_rng_of_frac_def 
        partial_object.select_convs(1) rel_def)
  then have "(r, s) ∈ (r' |⇘rel⇙ s')"
    using assms(3) 
    by simp
  then have "(r', s') .=⇘rel⇙ (r, s)"
    by (simp add: eq_class_of_rng_of_frac_def)
  thus ?thesis
    using equiv_obj_rng_of_frac equivalence_def
    by (metis (no_types, lifting) assms(1) assms(2) partial_object.select_convs(1) rel_def)
qed

lemma rng_to_rng_of_frac_without_zero_div_is_inj:
  assumes "𝟬 ∉ S" and "∀a ∈ carrier R.∀b ∈ carrier R. a ⊗ b = 𝟬 ⟶ a = 𝟬 ∨ b = 𝟬"
  shows "a_kernel R rec_rng_of_frac rng_to_rng_of_frac = {𝟬}"
proof-
  have "{r∈ carrier R. rng_to_rng_of_frac r = 𝟬⇘rec_rng_of_frac⇙} ⊆ {𝟬}"
  proof(rule subsetI)
    fix x
    assume a1:"x ∈ {r ∈ carrier R. rng_to_rng_of_frac r = 𝟬⇘rec_rng_of_frac⇙}"
    then have "(x, 𝟭) .=⇘rel⇙ (𝟬, 𝟭)"
      using rng_to_rng_of_frac_def rec_rng_of_frac_def eq_class_to_rel 
      by simp
    then obtain t where f1:"t ∈ S" and f2:"t ⊗ (𝟭 ⊗ x ⊖ 𝟭 ⊗ 𝟬) = 𝟬"
      using rel_def 
      by auto
    have f3:"x∈ carrier R"
      using a1 
      by simp
    then have f4:"t ⊗ x = 𝟬"
      using l_one r_zero f2 
      by (simp add: a_minus_def)
    have "t ≠ 𝟬"
      using f1 assms(1) 
      by auto
    then have "x = 𝟬"
      using assms(2) f1 f3 f4 subset rev_subsetD 
      by auto
    thus "x ∈ {𝟬}"
      by simp
  qed
  have "{𝟬} ⊆ {r∈ carrier R. rng_to_rng_of_frac r = 𝟬⇘rec_rng_of_frac⇙}"
    using subsetI rng_to_rng_of_frac_def rec_rng_of_frac_def 
    by simp
  then have "{r∈ carrier R. rng_to_rng_of_frac r = 𝟬⇘rec_rng_of_frac⇙} = {𝟬}"
    using ‹{r∈ carrier R. rng_to_rng_of_frac r = 𝟬⇘rec_rng_of_frac⇙} ⊆ {𝟬}› 
    by auto
  thus ?thesis
    by (simp add: a_kernel_def kernel_def)
qed

end


end