equal
deleted
inserted
replaced
230 note carr = carr hcarr |
230 note carr = carr hcarr |
231 from hsym[symmetric] have "h \<otimes> x = x' \<otimes> (inv x) \<otimes> x" by fast |
231 from hsym[symmetric] have "h \<otimes> x = x' \<otimes> (inv x) \<otimes> x" by fast |
232 also from carr |
232 also from carr |
233 have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc) |
233 have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc) |
234 also from carr |
234 also from carr |
235 have "\<dots> = x' \<otimes> \<one>" by (simp add: l_inv) |
235 have "\<dots> = x' \<otimes> \<one>" by simp |
236 also from carr |
236 also from carr |
237 have "\<dots> = x'" by simp |
237 have "\<dots> = x'" by simp |
238 finally |
238 finally |
239 have "h \<otimes> x = x'" by simp |
239 have "h \<otimes> x = x'" by simp |
240 from this[symmetric] and hH |
240 from this[symmetric] and hH |
518 |
518 |
519 lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H" |
519 lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H" |
520 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def) |
520 apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def) |
521 apply (rule_tac x = x in bexI) |
521 apply (rule_tac x = x in bexI) |
522 apply (rule bexI [of _ "\<one>"]) |
522 apply (rule bexI [of _ "\<one>"]) |
523 apply (auto simp add: subgroup.m_closed subgroup.one_closed |
523 apply (auto simp add: subgroup.one_closed subgroup.subset [THEN subsetD]) |
524 r_one subgroup.subset [THEN subsetD]) |
|
525 done |
524 done |
526 |
525 |
527 |
526 |
528 subsubsection {* Set of Inverses of an @{text r_coset}. *} |
527 subsubsection {* Set of Inverses of an @{text r_coset}. *} |
529 |
528 |
610 show "sym (rcong H)" |
609 show "sym (rcong H)" |
611 proof (simp add: r_congruent_def sym_def, clarify) |
610 proof (simp add: r_congruent_def sym_def, clarify) |
612 fix x y |
611 fix x y |
613 assume [simp]: "x \<in> carrier G" "y \<in> carrier G" |
612 assume [simp]: "x \<in> carrier G" "y \<in> carrier G" |
614 and "inv x \<otimes> y \<in> H" |
613 and "inv x \<otimes> y \<in> H" |
615 hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) |
614 hence "inv (inv x \<otimes> y) \<in> H" by simp |
616 thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group) |
615 thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group) |
617 qed |
616 qed |
618 next |
617 next |
619 show "trans (rcong H)" |
618 show "trans (rcong H)" |
620 proof (simp add: r_congruent_def trans_def, clarify) |
619 proof (simp add: r_congruent_def trans_def, clarify) |
720 next |
719 next |
721 fix a b c |
720 fix a b c |
722 assume abrcong: "(a, b) \<in> rcong H" |
721 assume abrcong: "(a, b) \<in> rcong H" |
723 and ccarr: "c \<in> carrier G" |
722 and ccarr: "c \<in> carrier G" |
724 |
723 |
725 from ccarr have "c \<in> Units G" by (simp add: Units_eq) |
724 from ccarr have "c \<in> Units G" by simp |
726 hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv) |
725 hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv) |
727 |
726 |
728 from abrcong |
727 from abrcong |
729 have acarr: "a \<in> carrier G" |
728 have acarr: "a \<in> carrier G" |
730 and bcarr: "b \<in> carrier G" |
729 and bcarr: "b \<in> carrier G" |