(* Title: HOL/Algebra/Subrings.thy Authors: Martin Baillon and Paulo Emílio de Vilhena *) theory Subrings imports Ring RingHom QuotRing Multiplicative_Group begin section ‹Subrings› subsection ‹Definitions› locale subring = subgroup H "add_monoid R" + submonoid H R for H and R (structure) locale subcring = subring + assumes sub_m_comm: "⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗ h2 = h2 ⊗ h1" locale subdomain = subcring + assumes sub_one_not_zero [simp]: "𝟭 ≠ 𝟬" assumes subintegral: "⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗ h2 = 𝟬 ⟹ h1 = 𝟬 ∨ h2 = 𝟬" locale subfield = subdomain K R for K and R (structure) + assumes subfield_Units: "Units (R ⦇ carrier := K ⦈) = K - { 𝟬 }" subsection ‹Basic Properties› subsubsection ‹Subrings› lemma (in ring) subringI: assumes "H ⊆ carrier R" and "𝟭 ∈ H" and "⋀h. h ∈ H ⟹ ⊖ h ∈ H" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗ h2 ∈ H" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊕ h2 ∈ H" shows "subring H R" using add.subgroupI[OF assms(1) _ assms(3, 5)] assms(2) submonoid.intro[OF assms(1, 4, 2)] unfolding subring_def by auto lemma subringE: assumes "subring H R" shows "H ⊆ carrier R" and "𝟬⇘R⇙ ∈ H" and "𝟭⇘R⇙ ∈ H" and "H ≠ {}" and "⋀h. h ∈ H ⟹ ⊖⇘R⇙ h ∈ H" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗⇘R⇙ h2 ∈ H" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊕⇘R⇙ h2 ∈ H" using subring.axioms[OF assms] unfolding submonoid_def subgroup_def a_inv_def by auto lemma (in ring) carrier_is_subring: "subring (carrier R) R" by (simp add: subringI) lemma (in ring) subring_inter: assumes "subring I R" and "subring J R" shows "subring (I ∩ J) R" using subringE[OF assms(1)] subringE[OF assms(2)] subringI[of "I ∩ J"] by auto lemma (in ring) subring_Inter: assumes "⋀I. I ∈ S ⟹ subring I R" and "S ≠ {}" shows "subring (⋂S) R" proof (rule subringI, auto simp add: assms subringE[of _ R]) fix x assume "∀I ∈ S. x ∈ I" thus "x ∈ carrier R" using assms subringE(1)[of _ R] by blast qed lemma (in ring) subring_is_ring: assumes "subring H R" shows "ring (R ⦇ carrier := H ⦈)" proof - interpret group "add_monoid (R ⦇ carrier := H ⦈)" + monoid "R ⦇ carrier := H ⦈" using subgroup.subgroup_is_group[OF subring.axioms(1) add.is_group] assms submonoid.submonoid_is_monoid[OF subring.axioms(2) monoid_axioms] by auto show ?thesis using subringE(1)[OF assms] by (unfold_locales, simp_all add: subringE(1)[OF assms] add.m_comm subset_eq l_distr r_distr) qed lemma (in ring) ring_incl_imp_subring: assumes "H ⊆ carrier R" and "ring (R ⦇ carrier := H ⦈)" shows "subring H R" using group.group_incl_imp_subgroup[OF add.group_axioms, of H] assms(1) monoid.monoid_incl_imp_submonoid[OF monoid_axioms assms(1)] ring.axioms(1, 2)[OF assms(2)] abelian_group.a_group[of "R ⦇ carrier := H ⦈"] unfolding subring_def by auto lemma (in ring) subring_iff: assumes "H ⊆ carrier R" shows "subring H R ⟷ ring (R ⦇ carrier := H ⦈)" using subring_is_ring ring_incl_imp_subring[OF assms] by auto subsubsection ‹Subcrings› lemma (in ring) subcringI: assumes "subring H R" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗ h2 = h2 ⊗ h1" shows "subcring H R" unfolding subcring_def subcring_axioms_def using assms by simp+ lemma (in cring) subcringI': assumes "subring H R" shows "subcring H R" using subcringI[OF assms] subringE(1)[OF assms] m_comm by auto lemma subcringE: assumes "subcring H R" shows "H ⊆ carrier R" and "𝟬⇘R⇙ ∈ H" and "𝟭⇘R⇙ ∈ H" and "H ≠ {}" and "⋀h. h ∈ H ⟹ ⊖⇘R⇙ h ∈ H" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗⇘R⇙ h2 ∈ H" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊕⇘R⇙ h2 ∈ H" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗⇘R⇙ h2 = h2 ⊗⇘R⇙ h1" using subringE[OF subcring.axioms(1)[OF assms]] subcring.sub_m_comm[OF assms] by simp+ lemma (in cring) carrier_is_subcring: "subcring (carrier R) R" by (simp add: subcringI' carrier_is_subring) lemma (in ring) subcring_inter: assumes "subcring I R" and "subcring J R" shows "subcring (I ∩ J) R" using subcringE[OF assms(1)] subcringE[OF assms(2)] subcringI[of "I ∩ J"] subringI[of "I ∩ J"] by auto lemma (in ring) subcring_Inter: assumes "⋀I. I ∈ S ⟹ subcring I R" and "S ≠ {}" shows "subcring (⋂S) R" proof (rule subcringI) show "subring (⋂S) R" using subcring.axioms(1)[of _ R] subring_Inter[of S] assms by auto next fix h1 h2 assume h1: "h1 ∈ ⋂S" and h2: "h2 ∈ ⋂S" obtain S' where S': "S' ∈ S" using assms(2) by blast hence "h1 ∈ S'" "h2 ∈ S'" using h1 h2 by blast+ thus "h1 ⊗ h2 = h2 ⊗ h1" using subcring.sub_m_comm[OF assms(1)[OF S']] by simp qed lemma (in ring) subcring_iff: assumes "H ⊆ carrier R" shows "subcring H R ⟷ cring (R ⦇ carrier := H ⦈)" proof assume A: "subcring H R" hence ring: "ring (R ⦇ carrier := H ⦈)" using subring_iff[OF assms] subcring.axioms(1)[OF A] by simp moreover have "comm_monoid (R ⦇ carrier := H ⦈)" using monoid.monoid_comm_monoidI[OF ring.is_monoid[OF ring]] subcring.sub_m_comm[OF A] by auto ultimately show "cring (R ⦇ carrier := H ⦈)" using cring_def by blast next assume A: "cring (R ⦇ carrier := H ⦈)" hence "subring H R" using cring.axioms(1) subring_iff[OF assms] by simp moreover have "comm_monoid (R ⦇ carrier := H ⦈)" using A unfolding cring_def by simp hence"⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗ h2 = h2 ⊗ h1" using comm_monoid.m_comm[of "R ⦇ carrier := H ⦈"] by auto ultimately show "subcring H R" unfolding subcring_def subcring_axioms_def by auto qed subsubsection ‹Subdomains› lemma (in ring) subdomainI: assumes "subcring H R" and "𝟭 ≠ 𝟬" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗ h2 = 𝟬 ⟹ h1 = 𝟬 ∨ h2 = 𝟬" shows "subdomain H R" unfolding subdomain_def subdomain_axioms_def using assms by simp+ lemma (in domain) subdomainI': assumes "subring H R" shows "subdomain H R" proof (rule subdomainI[OF subcringI[OF assms]], simp_all) show "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗ h2 = h2 ⊗ h1" using m_comm subringE(1)[OF assms] by auto show "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H; h1 ⊗ h2 = 𝟬 ⟧ ⟹ (h1 = 𝟬) ∨ (h2 = 𝟬)" using integral subringE(1)[OF assms] by auto qed lemma subdomainE: assumes "subdomain H R" shows "H ⊆ carrier R" and "𝟬⇘R⇙ ∈ H" and "𝟭⇘R⇙ ∈ H" and "H ≠ {}" and "⋀h. h ∈ H ⟹ ⊖⇘R⇙ h ∈ H" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗⇘R⇙ h2 ∈ H" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊕⇘R⇙ h2 ∈ H" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗⇘R⇙ h2 = h2 ⊗⇘R⇙ h1" and "⋀h1 h2. ⟦ h1 ∈ H; h2 ∈ H ⟧ ⟹ h1 ⊗⇘R⇙ h2 = 𝟬⇘R⇙ ⟹ h1 = 𝟬⇘R⇙ ∨ h2 = 𝟬⇘R⇙" and "𝟭⇘R⇙ ≠ 𝟬⇘R⇙" using subcringE[OF subdomain.axioms(1)[OF assms]] assms unfolding subdomain_def subdomain_axioms_def by auto lemma (in ring) subdomain_iff: assumes "H ⊆ carrier R" shows "subdomain H R ⟷ domain (R ⦇ carrier := H ⦈)" proof assume A: "subdomain H R" hence cring: "cring (R ⦇ carrier := H ⦈)" using subcring_iff[OF assms] subdomain.axioms(1)[OF A] by simp thus "domain (R ⦇ carrier := H ⦈)" using domain.intro[OF cring] subdomain.subintegral[OF A] subdomain.sub_one_not_zero[OF A] unfolding domain_axioms_def by auto next assume A: "domain (R ⦇ carrier := H ⦈)" hence subcring: "subcring H R" using subcring_iff[OF assms] unfolding domain_def by simp thus "subdomain H R" using subdomain.intro[OF subcring] domain.integral[OF A] domain.one_not_zero[OF A] unfolding subdomain_axioms_def by auto qed lemma (in domain) subring_is_domain: assumes "subring H R" shows "domain (R ⦇ carrier := H ⦈)" using subdomainI'[OF assms] unfolding subdomain_iff[OF subringE(1)[OF assms]] . (* NEW ====================== *) lemma (in ring) subdomain_is_domain: assumes "subdomain H R" shows "domain (R ⦇ carrier := H ⦈)" using assms unfolding subdomain_iff[OF subdomainE(1)[OF assms]] . subsubsection ‹Subfields› lemma (in ring) subfieldI: assumes "subcring K R" and "Units (R ⦇ carrier := K ⦈) = K - { 𝟬 }" shows "subfield K R" proof (rule subfield.intro) show "subfield_axioms K R" using assms(2) unfolding subfield_axioms_def . show "subdomain K R" proof (rule subdomainI[OF assms(1)], auto) have subM: "submonoid K R" using subring.axioms(2)[OF subcring.axioms(1)[OF assms(1)]] . show contr: "𝟭 = 𝟬 ⟹ False" proof - assume one_eq_zero: "𝟭 = 𝟬" have "𝟭 ∈ K" and "𝟭 ⊗ 𝟭 = 𝟭" using submonoid.one_closed[OF subM] by simp+ hence "𝟭 ∈ Units (R ⦇ carrier := K ⦈)" unfolding Units_def by (simp, blast) hence "𝟭 ≠ 𝟬" using assms(2) by simp thus False using one_eq_zero by simp qed fix k1 k2 assume k1: "k1 ∈ K" and k2: "k2 ∈ K" "k2 ≠ 𝟬" and k12: "k1 ⊗ k2 = 𝟬" obtain k2' where k2': "k2' ∈ K" "k2' ⊗ k2 = 𝟭" "k2 ⊗ k2' = 𝟭" using assms(2) k2 unfolding Units_def by auto have "𝟬 = (k1 ⊗ k2) ⊗ k2'" using k12 k2'(1) submonoid.mem_carrier[OF subM] by fastforce also have "... = k1" using k1 k2(1) k2'(1,3) submonoid.mem_carrier[OF subM] by (simp add: m_assoc) finally have "𝟬 = k1" . thus "k1 = 𝟬" by simp qed qed lemma (in field) subfieldI': assumes "subring K R" and "⋀k. k ∈ K - { 𝟬 } ⟹ inv k ∈ K" shows "subfield K R" proof (rule subfieldI) show "subcring K R" using subcringI[OF assms(1)] m_comm subringE(1)[OF assms(1)] by auto show "Units (R ⦇ carrier := K ⦈) = K - { 𝟬 }" proof show "K - { 𝟬 } ⊆ Units (R ⦇ carrier := K ⦈)" proof fix k assume k: "k ∈ K - { 𝟬 }" hence inv_k: "inv k ∈ K" using assms(2) by simp moreover have "k ∈ carrier R - { 𝟬 }" using subringE(1)[OF assms(1)] k by auto ultimately have "k ⊗ inv k = 𝟭" "inv k ⊗ k = 𝟭" by (simp add: field_Units)+ thus "k ∈ Units (R ⦇ carrier := K ⦈)" unfolding Units_def using k inv_k by auto qed next show "Units (R ⦇ carrier := K ⦈) ⊆ K - { 𝟬 }" proof fix k assume k: "k ∈ Units (R ⦇ carrier := K ⦈)" then obtain k' where k': "k' ∈ K" "k ⊗ k' = 𝟭" unfolding Units_def by auto hence "k ∈ carrier R" and "k' ∈ carrier R" using k subringE(1)[OF assms(1)] unfolding Units_def by auto hence "𝟬 = 𝟭" if "k = 𝟬" using that k'(2) by auto thus "k ∈ K - { 𝟬 }" using k unfolding Units_def by auto qed qed qed lemma (in field) carrier_is_subfield: "subfield (carrier R) R" by (auto intro: subfieldI[OF carrier_is_subcring] simp add: field_Units) lemma subfieldE: assumes "subfield K R" shows "subring K R" and "subcring K R" and "K ⊆ carrier R" and "⋀k1 k2. ⟦ k1 ∈ K; k2 ∈ K ⟧ ⟹ k1 ⊗⇘R⇙ k2 = k2 ⊗⇘R⇙ k1" and "⋀k1 k2. ⟦ k1 ∈ K; k2 ∈ K ⟧ ⟹ k1 ⊗⇘R⇙ k2 = 𝟬⇘R⇙ ⟹ k1 = 𝟬⇘R⇙ ∨ k2 = 𝟬⇘R⇙" and "𝟭⇘R⇙ ≠ 𝟬⇘R⇙" using subdomain.axioms(1)[OF subfield.axioms(1)[OF assms]] subcring_def subdomainE(1, 8, 9, 10)[OF subfield.axioms(1)[OF assms]] by auto lemma (in ring) subfield_m_inv: assumes "subfield K R" and "k ∈ K - { 𝟬 }" shows "inv k ∈ K - { 𝟬 }" and "k ⊗ inv k = 𝟭" and "inv k ⊗ k = 𝟭" proof - have K: "subring K R" "submonoid K R" using subfieldE(1)[OF assms(1)] subring.axioms(2) by auto have monoid: "monoid (R ⦇ carrier := K ⦈)" using submonoid.submonoid_is_monoid[OF subring.axioms(2)[OF K(1)] is_monoid] . have "monoid R" by (simp add: monoid_axioms) hence k: "k ∈ Units (R ⦇ carrier := K ⦈)" using subfield.subfield_Units[OF assms(1)] assms(2) by blast hence unit_of_R: "k ∈ Units R" using assms(2) subringE(1)[OF subfieldE(1)[OF assms(1)]] unfolding Units_def by auto have "inv⇘(R ⦇ carrier := K ⦈)⇙ k ∈ Units (R ⦇ carrier := K ⦈)" by (simp add: k monoid monoid.Units_inv_Units) hence "inv⇘(R ⦇ carrier := K ⦈)⇙ k ∈ K - { 𝟬 }" using subfield.subfield_Units[OF assms(1)] by blast thus "inv k ∈ K - { 𝟬 }" and "k ⊗ inv k = 𝟭" and "inv k ⊗ k = 𝟭" using Units_l_inv[OF unit_of_R] Units_r_inv[OF unit_of_R] using monoid.m_inv_monoid_consistent[OF monoid_axioms k K(2)] by auto qed lemma (in ring) subfield_m_inv_simprule: assumes "subfield K R" shows "⟦ k ∈ K - { 𝟬 }; a ∈ carrier R ⟧ ⟹ k ⊗ a ∈ K ⟹ a ∈ K" proof - note subring_props = subringE[OF subfieldE(1)[OF assms]] assume A: "k ∈ K - { 𝟬 }" "a ∈ carrier R" "k ⊗ a ∈ K" then obtain k' where k': "k' ∈ K" "k ⊗ a = k'" by blast have inv_k: "inv k ∈ K" "inv k ⊗ k = 𝟭" using subfield_m_inv[OF assms A(1)] by auto hence "inv k ⊗ (k ⊗ a) ∈ K" using k' A(3) subring_props(6) by auto thus "a ∈ K" using m_assoc[of "inv k" k a] A(2) inv_k subring_props(1) by (metis (no_types, opaque_lifting) A(1) Diff_iff l_one subsetCE) qed lemma (in ring) subfield_iff: shows "⟦ field (R ⦇ carrier := K ⦈); K ⊆ carrier R ⟧ ⟹ subfield K R" and "subfield K R ⟹ field (R ⦇ carrier := K ⦈)" proof- assume A: "field (R ⦇ carrier := K ⦈)" "K ⊆ carrier R" have "⋀k1 k2. ⟦ k1 ∈ K; k2 ∈ K ⟧ ⟹ k1 ⊗ k2 = k2 ⊗ k1" using comm_monoid.m_comm[OF cring.axioms(2)[OF fieldE(1)[OF A(1)]]] by simp moreover have "subring K R" using ring_incl_imp_subring[OF A(2) cring.axioms(1)[OF fieldE(1)[OF A(1)]]] . ultimately have "subcring K R" using subcringI by simp thus "subfield K R" using field.field_Units[OF A(1)] subfieldI by auto next assume A: "subfield K R" have cring: "cring (R ⦇ carrier := K ⦈)" using subcring_iff[OF subringE(1)[OF subfieldE(1)[OF A]]] subfieldE(2)[OF A] by simp thus "field (R ⦇ carrier := K ⦈)" using cring.cring_fieldI[OF cring] subfield.subfield_Units[OF A] by simp qed lemma (in field) subgroup_mult_of : assumes "subfield K R" shows "subgroup (K - {𝟬}) (mult_of R)" proof (intro group.group_incl_imp_subgroup[OF field_mult_group]) show "K - {𝟬} ⊆ carrier (mult_of R)" by (simp add: Diff_mono assms carrier_mult_of subfieldE(3)) show "group ((mult_of R) ⦇ carrier := K - {𝟬} ⦈)" using field.field_mult_group[OF subfield_iff(2)[OF assms]] unfolding mult_of_def by simp qed subsection ‹Subring Homomorphisms› lemma (in ring) hom_imp_img_subring: assumes "h ∈ ring_hom R S" and "subring K R" shows "ring (S ⦇ carrier := h ` K, one := h 𝟭, zero := h 𝟬 ⦈)" proof - have [simp]: "h 𝟭 = 𝟭⇘S⇙" using assms ring_hom_one by blast have "ring (R ⦇ carrier := K ⦈)" by (simp add: assms(2) subring_is_ring) moreover have "h ∈ ring_hom (R ⦇ carrier := K ⦈) S" using assms subringE(1)[OF assms (2)] unfolding ring_hom_def apply simp apply blast done ultimately show ?thesis using ring.ring_hom_imp_img_ring[of "R ⦇ carrier := K ⦈" h S] by simp qed lemma (in ring_hom_ring) img_is_subring: assumes "subring K R" shows "subring (h ` K) S" proof - have "ring (S ⦇ carrier := h ` K ⦈)" using R.hom_imp_img_subring[OF homh assms] hom_zero hom_one by simp moreover have "h ` K ⊆ carrier S" using ring_hom_memE(1)[OF homh] subringE(1)[OF assms] by auto ultimately show ?thesis using ring_incl_imp_subring by simp qed lemma (in ring_hom_ring) img_is_subfield: assumes "subfield K R" and "𝟭⇘S⇙ ≠ 𝟬⇘S⇙" shows "inj_on h K" and "subfield (h ` K) S" proof - have K: "K ⊆ carrier R" "subring K R" "subring (h ` K) S" using subfieldE(1)[OF assms(1)] subringE(1) img_is_subring by auto have field: "field (R ⦇ carrier := K ⦈)" using R.subfield_iff(2) ‹subfield K R› by blast moreover have ring: "ring (R ⦇ carrier := K ⦈)" using K R.ring_axioms R.subring_is_ring by blast moreover have ringS: "ring (S ⦇ carrier := h ` K ⦈)" using subring_is_ring K by simp ultimately have h: "h ∈ ring_hom (R ⦇ carrier := K ⦈) (S ⦇ carrier := h ` K ⦈)" unfolding ring_hom_def apply auto using ring_hom_memE[OF homh] K by (meson contra_subsetD)+ hence ring_hom: "ring_hom_ring (R ⦇ carrier := K ⦈) (S ⦇ carrier := h ` K ⦈) h" using ring_axioms ring ringS ring_hom_ringI2 by blast have "h ` K ≠ { 𝟬⇘S⇙ }" using subfieldE(1, 5)[OF assms(1)] subringE(3) assms(2) by (metis hom_one image_eqI singletonD) thus "inj_on h K" using ring_hom_ring.non_trivial_field_hom_imp_inj[OF ring_hom field] by auto hence "h ∈ ring_iso (R ⦇ carrier := K ⦈) (S ⦇ carrier := h ` K ⦈)" using h unfolding ring_iso_def bij_betw_def by auto hence "field (S ⦇ carrier := h ` K ⦈)" using field.ring_iso_imp_img_field[OF field, of h "S ⦇ carrier := h ` K ⦈"] by auto thus "subfield (h ` K) S" using S.subfield_iff[of "h ` K"] K(1) ring_hom_memE(1)[OF homh] by blast qed (* NEW ========================================================================== *) lemma (in ring_hom_ring) induced_ring_hom: assumes "subring K R" shows "ring_hom_ring (R ⦇ carrier := K ⦈) S h" proof - have "h ∈ ring_hom (R ⦇ carrier := K ⦈) S" using homh subringE(1)[OF assms] unfolding ring_hom_def by (auto, meson hom_mult hom_add subsetCE)+ thus ?thesis using R.subring_is_ring[OF assms] ring_axioms unfolding ring_hom_ring_def ring_hom_ring_axioms_def by auto qed (* NEW ========================================================================== *) lemma (in ring_hom_ring) inj_on_subgroup_iff_trivial_ker: assumes "subring K R" shows "inj_on h K ⟷ a_kernel (R ⦇ carrier := K ⦈) S h = { 𝟬 }" using ring_hom_ring.inj_iff_trivial_ker[OF induced_ring_hom[OF assms]] by simp lemma (in ring_hom_ring) inv_ring_hom: assumes "inj_on h K" and "subring K R" shows "ring_hom_ring (S ⦇ carrier := h ` K ⦈) R (inv_into K h)" proof (intro ring_hom_ringI[OF _ R.ring_axioms], auto) show "ring (S ⦇ carrier := h ` K ⦈)" using subring_is_ring[OF img_is_subring[OF assms(2)]] . next show "inv_into K h 𝟭⇘S⇙ = 𝟭⇘R⇙" using assms(1) subringE(3)[OF assms(2)] hom_one by (simp add: inv_into_f_eq) next fix k1 k2 assume k1: "k1 ∈ K" and k2: "k2 ∈ K" with ‹k1 ∈ K› show "inv_into K h (h k1) ∈ carrier R" using assms(1) subringE(1)[OF assms(2)] by (simp add: subset_iff) from ‹k1 ∈ K› and ‹k2 ∈ K› have "h k1 ⊕⇘S⇙ h k2 = h (k1 ⊕⇘R⇙ k2)" and "k1 ⊕⇘R⇙ k2 ∈ K" and "h k1 ⊗⇘S⇙ h k2 = h (k1 ⊗⇘R⇙ k2)" and "k1 ⊗⇘R⇙ k2 ∈ K" using subringE(1,6,7)[OF assms(2)] by (simp add: subset_iff)+ thus "inv_into K h (h k1 ⊕⇘S⇙ h k2) = inv_into K h (h k1) ⊕⇘R⇙ inv_into K h (h k2)" and "inv_into K h (h k1 ⊗⇘S⇙ h k2) = inv_into K h (h k1) ⊗⇘R⇙ inv_into K h (h k2)" using assms(1) k1 k2 by simp+ qed end