[STATEMENT]
lemma characterization_prodag:"\<lbrakk>I \<noteq> {}; \<forall>j\<in>(I::'i set). aGroup ((A j)::
    ('a, 'm) aGroup_scheme); aGroup (S::'d aGroup);
    \<forall>j\<in>I. ((g j) \<in> aHom S (A j)); \<exists>ff. ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> (B::'d set) \<and>
          bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B;
    \<forall>(S':: 'd aGroup). aGroup S' \<longrightarrow>
        (\<forall>g'. (\<forall>j\<in>I. (g' j) \<in> aHom S' (A j) \<longrightarrow>
         (\<exists>! f. f \<in> aHom S' S \<and> (\<forall>j\<in>I. compos S' (g j) f =  (g' j)))))\<rbrakk> \<Longrightarrow>
     \<exists>h. bijec\<^bsub>(prodag I A),S\<^esub> h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); \<exists>ff. ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B \<and> bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; \<forall>S'. aGroup S' \<longrightarrow> (\<forall>g'. \<forall>j\<in>I. g' j \<in> aHom S' (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S' S \<and> (\<forall>j\<in>I. compos S' (g j) f = g' j)))\<rbrakk> \<Longrightarrow> \<exists>h. bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> h
[PROOF STEP]
apply (frule prodag_aGroup[of "I" "A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); \<exists>ff. ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B \<and> bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; \<forall>S'. aGroup S' \<longrightarrow> (\<forall>g'. \<forall>j\<in>I. g' j \<in> aHom S' (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S' S \<and> (\<forall>j\<in>I. compos S' (g j) f = g' j))); aGroup (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> \<exists>h. bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> h
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); \<forall>S'. aGroup S' \<longrightarrow> (\<forall>g'. \<forall>j\<in>I. g' j \<in> aHom S' (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S' S \<and> (\<forall>j\<in>I. compos S' (g j) f = g' j))); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B \<and> bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B\<rbrakk> \<Longrightarrow> \<exists>h. bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> h
[PROOF STEP]
apply (frule_tac f = ff in aGroup.Ag_ind_aGroup[of "a\<Pi>\<^bsub>I\<^esub> A" _ "B"], erule conjE,
       assumption, simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); \<forall>S'. aGroup S' \<longrightarrow> (\<forall>g'. \<forall>j\<in>I. g' j \<in> aHom S' (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S' S \<and> (\<forall>j\<in>I. compos S' (g j) f = g' j))); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B\<rbrakk> \<Longrightarrow> \<exists>h. bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> h
[PROOF STEP]
apply (frule aGroup.Ag_ind_aGroup[of "a\<Pi>\<^bsub>I\<^esub> A" _ "B"], assumption+,
       frule_tac a = S in forall_spec, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); \<forall>S'. aGroup S' \<longrightarrow> (\<forall>g'. \<forall>j\<in>I. g' j \<in> aHom S' (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S' S \<and> (\<forall>j\<in>I. compos S' (g j) f = g' j))); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>g'. \<forall>j\<in>I. g' j \<in> aHom S (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g' j))\<rbrakk> \<Longrightarrow> \<exists>h. bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> h
[PROOF STEP]
apply (rotate_tac -1,
       frule_tac x = g in spec,
       thin_tac "\<forall>g'. \<forall>j\<in>I. g' j \<in> aHom S (A j) \<longrightarrow>
              (\<exists>!f. f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g' j))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); \<forall>S'. aGroup S' \<longrightarrow> (\<forall>g'. \<forall>j\<in>I. g' j \<in> aHom S' (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S' S \<and> (\<forall>j\<in>I. compos S' (g j) f = g' j))); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. g j \<in> aHom S (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g j))\<rbrakk> \<Longrightarrow> \<exists>h. bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> h
[PROOF STEP]
apply (frule_tac a = "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff" in forall_spec, assumption+,
       thin_tac "\<forall>S'. aGroup S' \<longrightarrow> (\<forall>g'. \<forall>j\<in>I. g' j \<in> aHom S' (A j) \<longrightarrow>
                (\<exists>!f. f \<in> aHom S' S \<and> (\<forall>j\<in>I. compos S' (g j) f = g' j)))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. g j \<in> aHom S (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g j)); \<forall>g'. \<forall>j\<in>I. g' j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S \<and> (\<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) f = g' j))\<rbrakk> \<Longrightarrow> \<exists>h. bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> h
[PROOF STEP]
apply (frule_tac x = "ProjInd I A ff" in spec,
       thin_tac "\<forall>g'. \<forall>j\<in>I. g' j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j) \<longrightarrow>
                     (\<exists>!f. f \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S \<and>
                          (\<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) f =
                                 g' j))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. g j \<in> aHom S (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g j)); \<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S \<and> (\<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) f = ProjInd I A ff j))\<rbrakk> \<Longrightarrow> \<exists>h. bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> h
[PROOF STEP]
apply (frule_tac f = ff in ProjInd_aHom1[of "I" "A" _ "B"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff. \<lbrakk>I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. g j \<in> aHom S (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g j)); \<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j) \<longrightarrow> (\<exists>!f. f \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S \<and> (\<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) f = ProjInd I A ff j)); \<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j)\<rbrakk> \<Longrightarrow> \<exists>h. bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> h
[PROOF STEP]
apply (simp add:nonempty_ex[of "I"],
       rotate_tac -2,
       frule ex1_implies_ex,
       thin_tac "\<exists>!f. f \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S \<and>
         (\<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) f = ProjInd I A ff j)",
       rotate_tac -1, erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff x. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<exists>!f. f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g j); x \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) x = ProjInd I A ff j\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (rename_tac ff h1,
       frule_tac f = ff in map_family_triangle1[of "I" "A" _  "B" "S" "g"],
           assumption+,
       rotate_tac -1,
       frule ex1_implies_ex,
       thin_tac "\<exists>!h. h \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) \<and>
             (\<forall>j\<in>I. compos S (ProjInd I A ff j) h = g j)",
       rotate_tac -1,
       erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff h1 x. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<exists>!f. f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g j); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; x \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) x = g j\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (rename_tac ff h1 h2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff h1 h2. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<exists>!f. f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g j); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (frule_tac ff = ff and ?h1.0 = h1 and ?h2.0 = h2 in prod_triangle[of "I"
        "A" "S" "g" _ "B"], assumption+,
       frule_tac ?S1.0 = "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff" in map_family_triangle3[of "I"
                "A" "S" _ "g"],
        assumption+,
       frule_tac f = h2 and g = h1 and M =  "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff" in
                aHom_compos[of "S" _ "S" ], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff h1 h2. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<exists>!f. f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g j); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>; \<forall>j\<in>I. compos S (g j) (compos S h1 h2) = g j; compos S h1 h2 \<in> aHom S S\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (erule ex1E)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff h1 h2 f. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>; \<forall>j\<in>I. compos S (g j) (compos S h1 h2) = g j; compos S h1 h2 \<in> aHom S S; f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g j); \<forall>y. y \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) y = g j) \<longrightarrow> y = f\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (rotate_tac -1,
        frule_tac x = "compos S h1 h2" in spec,
        frule map_family_triangle4[of "I" "A" "S" "g"], assumption+,
        frule aGroup.aI_aHom[of "S"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff h1 h2 f. \<lbrakk>\<forall>y. y \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) y = g j) \<longrightarrow> y = f; \<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; \<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); \<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j; compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>; \<forall>j\<in>I. compos S (g j) (compos S h1 h2) = g j; compos S h1 h2 \<in> aHom S S; f \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) f = g j); compos S h1 h2 \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) (compos S h1 h2) = g j) \<longrightarrow> compos S h1 h2 = f; \<forall>j\<in>I. compos S (g j) aI\<^bsub>S\<^esub> = g j; aI\<^bsub>S\<^esub> \<in> aHom S S\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (frule_tac x = "aI\<^bsub>S\<^esub>" in spec,
   thin_tac "\<forall>y. y \<in> aHom S S \<and> (\<forall>j\<in>I. compos S (g j) y = g j) \<longrightarrow> y = f",
   simp,
   thin_tac "\<forall>j\<in>I. compos S (ProjInd I A ff j) h2 = g j",
   thin_tac "\<forall>j\<in>I. compos S (g j) f = g j",
   thin_tac "\<forall>j\<in>I. compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (g j) h1 = ProjInd I A ff j")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff h1 h2 f. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>; f \<in> aHom S S; compos S h1 h2 = f; aI\<^bsub>S\<^esub> = f\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (rotate_tac -1, frule sym, thin_tac "aI\<^bsub>S\<^esub> = f", simp,
        frule_tac A = "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff" and f = h1 and g = h2 in
         compos_aI_inj[of _ "S"], assumption+,
        frule_tac B = "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff" and f = h2 and g = h1 in
         compos_aI_surj[of "S"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff h1 h2 f. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>; aI\<^bsub>S\<^esub> \<in> aHom S S; compos S h1 h2 = aI\<^bsub>S\<^esub>; f = aI\<^bsub>S\<^esub>; injec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1; surjec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (frule_tac f = ff in Ag_ind_bijec[of "a\<Pi>\<^bsub>I\<^esub> A" _ "B"], assumption+,
        frule_tac F = "Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff" and f = "Agii (a\<Pi>\<^bsub>I\<^esub> A) ff" and g = h1
           in compos_bijec[of "a\<Pi>\<^bsub>I\<^esub> A" _ "S"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ff h1 h2 f. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>; aI\<^bsub>S\<^esub> \<in> aHom S S; compos S h1 h2 = aI\<^bsub>S\<^esub>; f = aI\<^bsub>S\<^esub>; injec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1; surjec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1; bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) ff\<rbrakk> \<Longrightarrow> bijec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1
 2. \<And>ff h1 h2 f. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>; aI\<^bsub>S\<^esub> \<in> aHom S S; compos S h1 h2 = aI\<^bsub>S\<^esub>; f = aI\<^bsub>S\<^esub>; injec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1; surjec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1; bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) ff; bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> compos (a\<Pi>\<^bsub>I\<^esub> A) h1 (Agii (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (subst bijec_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff h1 h2 f. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>; aI\<^bsub>S\<^esub> \<in> aHom S S; compos S h1 h2 = aI\<^bsub>S\<^esub>; f = aI\<^bsub>S\<^esub>; injec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1; surjec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1; bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) ff; bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> compos (a\<Pi>\<^bsub>I\<^esub> A) h1 (Agii (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (thin_tac "bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub> Agii (a\<Pi>\<^bsub>I\<^esub> A) ff",
        thin_tac "injec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1",
        thin_tac "surjec\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff,S\<^esub> h1")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ff h1 h2 f. \<lbrakk>\<forall>j\<in>I. ProjInd I A ff j \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) (A j); I \<noteq> {}; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); aGroup (a\<Pi>\<^bsub>I\<^esub> A); ff \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> B; bij_to ff (carrier (a\<Pi>\<^bsub>I\<^esub> A)) B; aGroup (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); h1 \<in> aHom (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) S; h2 \<in> aHom S (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff); compos (Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff) h2 h1 = aI\<^bsub>Ag_ind (a\<Pi>\<^bsub>I\<^esub> A) ff\<^esub>; aI\<^bsub>S\<^esub> \<in> aHom S S; compos S h1 h2 = aI\<^bsub>S\<^esub>; f = aI\<^bsub>S\<^esub>; bijec\<^bsub>(a\<Pi>\<^bsub>I\<^esub> A),S\<^esub> compos (a\<Pi>\<^bsub>I\<^esub> A) h1 (Agii (a\<Pi>\<^bsub>I\<^esub> A) ff)\<rbrakk> \<Longrightarrow> Ex (bijec (a\<Pi>\<^bsub>I\<^esub> A) S)
[PROOF STEP]
apply (rule exI, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_zeroGTr:"(\<forall>j \<le> n. f j = \<zero>) \<longrightarrow> nsum A f n = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>n. f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f n = \<zero>
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>j\<le>0. f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f 0 = \<zero>
 2. \<And>n. (\<forall>j\<le>n. f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f n = \<zero> \<Longrightarrow> (\<forall>j\<le>Suc n. f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<zero>
[PROOF STEP]
apply (rule impI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>j\<le>n. f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f n = \<zero> \<Longrightarrow> (\<forall>j\<le>Suc n. f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<zero>
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<forall>j\<le>n. f j = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f n = \<zero>; \<forall>j\<le>Suc n. f j = \<zero>\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f Suc n = \<zero>
[PROOF STEP]
apply (cut_tac n = n in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A f n = \<zero>; \<forall>j\<le>Suc n. f j = \<zero>\<rbrakk> \<Longrightarrow> \<zero> \<plusminus> \<zero> = \<zero>
[PROOF STEP]
apply (cut_tac ex_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<Sigma>\<^sub>e A f n = \<zero>; \<forall>j\<le>Suc n. f j = \<zero>; \<zero> \<in> carrier A\<rbrakk> \<Longrightarrow> \<zero> \<plusminus> \<zero> = \<zero>
[PROOF STEP]
apply (simp add:l_zero[of \<zero>])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_zeroA:"\<forall>j \<le> n. f j = \<zero> \<Longrightarrow>   nsum A f n = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<le>n. f j = \<zero> \<Longrightarrow> \<Sigma>\<^sub>e A f n = \<zero>
[PROOF STEP]
apply (simp add:nsum_zeroGTr)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Ring: "Ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring R
[PROOF STEP]
..


[STATEMENT]
lemma (in Ring) ring_is_ag:"aGroup R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aGroup R
[PROOF STEP]
apply (rule aGroup.intro,
       rule pop_closed,
       rule pop_aassoc, assumption+,
       rule pop_commute, assumption+,
       rule mop_closed,
       rule l_m, assumption,
       rule ex_zero,
       rule l_zero, assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_zero:"\<zero> \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<in> carrier R
[PROOF STEP]
by (simp add: ex_zero)


[STATEMENT]
lemma (in Ring) ring_one:"1\<^sub>r \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>r \<in> carrier R
[PROOF STEP]
by (simp add:un_closed)


[STATEMENT]
lemma (in Ring) ring_tOp_closed:"\<lbrakk> x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow>
                     x \<cdot>\<^sub>r y \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier R
[PROOF STEP]
apply (cut_tac tp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (\<cdot>\<^sub>r) \<in> carrier R \<rightarrow> carrier R \<rightarrow> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier R
[PROOF STEP]
apply (frule funcset_mem[of "(\<cdot>\<^sub>r)" "carrier R" "carrier R \<rightarrow> carrier R"
            "x"], assumption+,
        thin_tac "(\<cdot>\<^sub>r) \<in> carrier R \<rightarrow> carrier R \<rightarrow> carrier R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (\<cdot>\<^sub>r) x \<in> carrier R \<rightarrow> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> carrier R
[PROOF STEP]
apply (rule funcset_mem[of "(\<cdot>\<^sub>r) x" "carrier R" "carrier R" "y"],
              assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_tOp_commute:"\<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow>
                x \<cdot>\<^sub>r y = y \<cdot>\<^sub>r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = y \<cdot>\<^sub>r x
[PROOF STEP]
by (simp add:tp_commute)


[STATEMENT]
lemma (in Ring) ring_distrib1:"\<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk>
                 \<Longrightarrow> x \<cdot>\<^sub>r (y \<plusminus> z) = x \<cdot>\<^sub>r y \<plusminus> x \<cdot>\<^sub>r z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r (y \<plusminus> z) = x \<cdot>\<^sub>r y \<plusminus> x \<cdot>\<^sub>r z
[PROOF STEP]
by (simp add:rg_distrib)


[STATEMENT]
lemma (in Ring) ring_distrib2:"\<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk>
                \<Longrightarrow> (y \<plusminus> z) \<cdot>\<^sub>r x = y \<cdot>\<^sub>r x \<plusminus>  z \<cdot>\<^sub>r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> (y \<plusminus> z) \<cdot>\<^sub>r x = y \<cdot>\<^sub>r x \<plusminus> z \<cdot>\<^sub>r x
[PROOF STEP]
apply (subst tp_commute[of "y \<plusminus> z" "x"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> y \<plusminus> z \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> x \<in> carrier R
 3. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r (y \<plusminus> z) = y \<cdot>\<^sub>r x \<plusminus> z \<cdot>\<^sub>r x
[PROOF STEP]
apply (cut_tac ring_is_ag, simp add:aGroup.ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r (y \<plusminus> z) = y \<cdot>\<^sub>r x \<plusminus> z \<cdot>\<^sub>r x
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r (y \<plusminus> z) = y \<cdot>\<^sub>r x \<plusminus> z \<cdot>\<^sub>r x
[PROOF STEP]
apply (subst ring_distrib1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<plusminus> x \<cdot>\<^sub>r z = y \<cdot>\<^sub>r x \<plusminus> z \<cdot>\<^sub>r x
[PROOF STEP]
apply (simp add:tp_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_distrib3:"\<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R;
      y \<in> carrier R \<rbrakk> \<Longrightarrow> (a \<plusminus> b) \<cdot>\<^sub>r (x \<plusminus> y) =
                                          a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y \<plusminus> b \<cdot>\<^sub>r x \<plusminus> b \<cdot>\<^sub>r y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> (a \<plusminus> b) \<cdot>\<^sub>r (x \<plusminus> y) = a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y \<plusminus> b \<cdot>\<^sub>r x \<plusminus> b \<cdot>\<^sub>r y
[PROOF STEP]
apply (subst ring_distrib2)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> a \<in> carrier R
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> b \<in> carrier R
 4. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (x \<plusminus> y) \<plusminus> b \<cdot>\<^sub>r (x \<plusminus> y) = a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y \<plusminus> b \<cdot>\<^sub>r x \<plusminus> b \<cdot>\<^sub>r y
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> a \<in> carrier R
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> b \<in> carrier R
 4. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (x \<plusminus> y) \<plusminus> b \<cdot>\<^sub>r (x \<plusminus> y) = a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y \<plusminus> b \<cdot>\<^sub>r x \<plusminus> b \<cdot>\<^sub>r y
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (x \<plusminus> y) \<plusminus> b \<cdot>\<^sub>r (x \<plusminus> y) = a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y \<plusminus> b \<cdot>\<^sub>r x \<plusminus> b \<cdot>\<^sub>r y
[PROOF STEP]
apply ((subst ring_distrib1)+, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y \<plusminus> b \<cdot>\<^sub>r (x \<plusminus> y) = a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y \<plusminus> b \<cdot>\<^sub>r x \<plusminus> b \<cdot>\<^sub>r y
[PROOF STEP]
apply (subst ring_distrib1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y \<plusminus> (b \<cdot>\<^sub>r x \<plusminus> b \<cdot>\<^sub>r y) = a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y \<plusminus> b \<cdot>\<^sub>r x \<plusminus> b \<cdot>\<^sub>r y
[PROOF STEP]
apply (rule pop_aassoc [THEN sym, of "a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y" "b \<cdot>\<^sub>r x" "b \<cdot>\<^sub>r y"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r x \<plusminus> a \<cdot>\<^sub>r y \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> b \<cdot>\<^sub>r x \<in> carrier R
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> b \<cdot>\<^sub>r y \<in> carrier R
[PROOF STEP]
apply (cut_tac ring_is_ag, rule aGroup.ag_pOp_closed, assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r x \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r y \<in> carrier R
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> b \<cdot>\<^sub>r x \<in> carrier R
 4. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> b \<cdot>\<^sub>r y \<in> carrier R
[PROOF STEP]
apply (simp add:ring_tOp_closed)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) rEQMulR:
  "\<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R; x = y \<rbrakk>
        \<Longrightarrow> x \<cdot>\<^sub>r z = y \<cdot>\<^sub>r z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R; x = y\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r z = y \<cdot>\<^sub>r z
[PROOF STEP]
by simp


[STATEMENT]
lemma (in Ring) ring_tOp_assoc:"\<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R \<rbrakk>
 \<Longrightarrow> (x \<cdot>\<^sub>r y) \<cdot>\<^sub>r z = x \<cdot>\<^sub>r (y \<cdot>\<^sub>r z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<cdot>\<^sub>r z = x \<cdot>\<^sub>r (y \<cdot>\<^sub>r z)
[PROOF STEP]
by (simp add:tp_assoc)


[STATEMENT]
lemma (in Ring) ring_l_one:"x \<in> carrier R \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r x = x
[PROOF STEP]
by (simp add:rg_l_unit)


[STATEMENT]
lemma (in Ring) ring_r_one:"x \<in> carrier R  \<Longrightarrow> x \<cdot>\<^sub>r 1\<^sub>r = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> x \<cdot>\<^sub>r 1\<^sub>r = x
[PROOF STEP]
apply (subst ring_tOp_commute, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> carrier R \<Longrightarrow> 1\<^sub>r \<in> carrier R
 2. x \<in> carrier R \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r x = x
[PROOF STEP]
apply (simp add:un_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r x = x
[PROOF STEP]
apply (simp add:ring_l_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_times_0_x:"x \<in> carrier R \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>
[PROOF STEP]
apply (cut_tac ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>
[PROOF STEP]
apply (frule ring_distrib2 [of "x" "\<zero>" "\<zero>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R; \<zero> \<in> carrier R; (\<zero> \<plusminus> \<zero>) \<cdot>\<^sub>r x = \<zero> \<cdot>\<^sub>r x \<plusminus> \<zero> \<cdot>\<^sub>r x\<rbrakk> \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>
[PROOF STEP]
apply (simp add:aGroup.ag_l_zero [of "R" "\<zero>"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R; \<zero> \<in> carrier R; \<zero> \<cdot>\<^sub>r x = \<zero> \<cdot>\<^sub>r x \<plusminus> \<zero> \<cdot>\<^sub>r x\<rbrakk> \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>
[PROOF STEP]
apply (frule ring_tOp_closed [of "\<zero>" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R; \<zero> \<in> carrier R; \<zero> \<cdot>\<^sub>r x = \<zero> \<cdot>\<^sub>r x \<plusminus> \<zero> \<cdot>\<^sub>r x; \<zero> \<cdot>\<^sub>r x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>
[PROOF STEP]
apply (frule sym, thin_tac "\<zero> \<cdot>\<^sub>r x = \<zero> \<cdot>\<^sub>r x \<plusminus> \<zero> \<cdot>\<^sub>r x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R; \<zero> \<in> carrier R; \<zero> \<cdot>\<^sub>r x \<in> carrier R; \<zero> \<cdot>\<^sub>r x \<plusminus> \<zero> \<cdot>\<^sub>r x = \<zero> \<cdot>\<^sub>r x\<rbrakk> \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>
[PROOF STEP]
apply (frule aGroup.ag_eq_sol2 [of "R" "\<zero> \<cdot>\<^sub>r x" "\<zero> \<cdot>\<^sub>r x" "\<zero> \<cdot>\<^sub>r x"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R; \<zero> \<in> carrier R; \<zero> \<cdot>\<^sub>r x \<in> carrier R; \<zero> \<cdot>\<^sub>r x \<plusminus> \<zero> \<cdot>\<^sub>r x = \<zero> \<cdot>\<^sub>r x; \<zero> \<cdot>\<^sub>r x = \<zero> \<cdot>\<^sub>r x \<plusminus> -\<^sub>a \<zero> \<cdot>\<^sub>r x\<rbrakk> \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>
[PROOF STEP]
apply (thin_tac "\<zero> \<cdot>\<^sub>r x \<plusminus> \<zero> \<cdot>\<^sub>r x = \<zero> \<cdot>\<^sub>r x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R; \<zero> \<in> carrier R; \<zero> \<cdot>\<^sub>r x \<in> carrier R; \<zero> \<cdot>\<^sub>r x = \<zero> \<cdot>\<^sub>r x \<plusminus> -\<^sub>a \<zero> \<cdot>\<^sub>r x\<rbrakk> \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>
[PROOF STEP]
apply (simp add:aGroup.ag_r_inv1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_times_x_0:"x \<in> carrier R \<Longrightarrow>  x \<cdot>\<^sub>r \<zero> = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> x \<cdot>\<^sub>r \<zero> = \<zero>
[PROOF STEP]
apply (cut_tac ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<zero> = \<zero>
[PROOF STEP]
apply (subst ring_tOp_commute, assumption+, simp add:ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> \<zero> \<cdot>\<^sub>r x = \<zero>
[PROOF STEP]
apply (simp add:ring_times_0_x)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) rMulZeroDiv:
     "\<lbrakk> x \<in> carrier R; y \<in> carrier R; x = \<zero> \<or> y = \<zero> \<rbrakk> \<Longrightarrow> x  \<cdot>\<^sub>r  y = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x = \<zero> \<or> y = \<zero>\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = \<zero>
[PROOF STEP]
apply (erule disjE, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<zero> \<in> carrier R; y \<in> carrier R; x = \<zero>\<rbrakk> \<Longrightarrow> \<zero> \<cdot>\<^sub>r y = \<zero>
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; y = \<zero>\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = \<zero>
[PROOF STEP]
apply (rule ring_times_0_x, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; y = \<zero>\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y = \<zero>
[PROOF STEP]
apply (simp, rule ring_times_x_0, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_inv1:"\<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow>
      -\<^sub>a (a \<cdot>\<^sub>r b) = (-\<^sub>a a) \<cdot>\<^sub>r b \<and> -\<^sub>a (a \<cdot>\<^sub>r b) = a \<cdot>\<^sub>r (-\<^sub>a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b \<and> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b \<and> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule ring_distrib2 [THEN sym, of "b" "a" "-\<^sub>a a"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = (a \<plusminus> -\<^sub>a a) \<cdot>\<^sub>r b\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed [of "R" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = (a \<plusminus> -\<^sub>a a) \<cdot>\<^sub>r b\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (simp add:aGroup.ag_r_inv1 [of "R" "a"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero> \<cdot>\<^sub>r b\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (simp add:ring_times_0_x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero>\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed [of "R" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero>; -\<^sub>a a \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule ring_tOp_closed [of "a" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero>; -\<^sub>a a \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule ring_tOp_closed [of "-\<^sub>a a" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero>; -\<^sub>a a \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule aGroup.ag_eq_sol1 [of "R" "a \<cdot>\<^sub>r b" "(-\<^sub>a a) \<cdot>\<^sub>r b" "\<zero>"],
           assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero>; -\<^sub>a a \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero>; -\<^sub>a a \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero>
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero>; -\<^sub>a a \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b = -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero>\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 4. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (rule ring_zero, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero>; -\<^sub>a a \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b = -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero>\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (thin_tac "a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a a) \<cdot>\<^sub>r b = \<zero>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; -\<^sub>a a \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b = -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero>\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule sym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; -\<^sub>a a \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b = -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero>; -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero> = (-\<^sub>a a) \<cdot>\<^sub>r b\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (thin_tac "(-\<^sub>a a) \<cdot>\<^sub>r b = -\<^sub>a (a \<cdot>\<^sub>r b) \<plusminus> \<zero>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; -\<^sub>a a \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero> = (-\<^sub>a a) \<cdot>\<^sub>r b\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed [of "R" " a \<cdot>\<^sub>r b"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; -\<^sub>a a \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; (-\<^sub>a a) \<cdot>\<^sub>r b \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero> = (-\<^sub>a a) \<cdot>\<^sub>r b; -\<^sub>a a \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule ring_distrib1 [THEN sym, of "a" "b" "-\<^sub>a b"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a b \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = a \<cdot>\<^sub>r (b \<plusminus> -\<^sub>a b)\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (simp add:aGroup.ag_mOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = a \<cdot>\<^sub>r (b \<plusminus> -\<^sub>a b)\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (simp add:aGroup.ag_r_inv1 [of "R" "b"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = a \<cdot>\<^sub>r \<zero>\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (simp add:ring_times_x_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed [of "R" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>; -\<^sub>a b \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule ring_tOp_closed [of "a" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule ring_tOp_closed [of "a" "-\<^sub>a b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; a \<cdot>\<^sub>r (-\<^sub>a b) \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule aGroup.ag_eq_sol1 [THEN sym, of "R" "a \<cdot>\<^sub>r b" "a \<cdot>\<^sub>r (-\<^sub>a b)" "\<zero>"],
                                                      assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; a \<cdot>\<^sub>r (-\<^sub>a b) \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero> \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; a \<cdot>\<^sub>r (-\<^sub>a b) \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; a \<cdot>\<^sub>r (-\<^sub>a b) \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero> = a \<cdot>\<^sub>r (-\<^sub>a b)\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (simp add:ring_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; a \<cdot>\<^sub>r (-\<^sub>a b) \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; a \<cdot>\<^sub>r (-\<^sub>a b) \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero> = a \<cdot>\<^sub>r (-\<^sub>a b)\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; a \<cdot>\<^sub>r (-\<^sub>a b) \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero> = a \<cdot>\<^sub>r (-\<^sub>a b)\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed [of "R" " a \<cdot>\<^sub>r b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b) = \<zero>; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b \<in> carrier R; a \<cdot>\<^sub>r (-\<^sub>a b) \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b \<plusminus> \<zero> = a \<cdot>\<^sub>r (-\<^sub>a b); -\<^sub>a a \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_inv1_1:"\<lbrakk>a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow>
      -\<^sub>a (a \<cdot>\<^sub>r b) = (-\<^sub>a a) \<cdot>\<^sub>r b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b
[PROOF STEP]
apply (simp add:ring_inv1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_inv1_2:"\<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow>
                                -\<^sub>a (a \<cdot>\<^sub>r b) = a \<cdot>\<^sub>r (-\<^sub>a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule ring_inv1 [of "a" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b \<and> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule conjunct2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b \<and> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b); -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (thin_tac "-\<^sub>a a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r b \<and> -\<^sub>a (a \<cdot>\<^sub>r b) = a \<cdot>\<^sub>r (-\<^sub>a b)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)\<rbrakk> \<Longrightarrow> -\<^sub>a a \<cdot>\<^sub>r b = a \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_times_minusl:"a \<in> carrier R \<Longrightarrow>  -\<^sub>a a = (-\<^sub>a 1\<^sub>r) \<cdot>\<^sub>r a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier R \<Longrightarrow> -\<^sub>a a = (-\<^sub>a 1\<^sub>r) \<cdot>\<^sub>r a
[PROOF STEP]
apply (cut_tac ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; 1\<^sub>r \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a = (-\<^sub>a 1\<^sub>r) \<cdot>\<^sub>r a
[PROOF STEP]
apply (frule ring_inv1_1[of "1\<^sub>r" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; 1\<^sub>r \<in> carrier R; -\<^sub>a 1\<^sub>r \<cdot>\<^sub>r a = (-\<^sub>a 1\<^sub>r) \<cdot>\<^sub>r a\<rbrakk> \<Longrightarrow> -\<^sub>a a = (-\<^sub>a 1\<^sub>r) \<cdot>\<^sub>r a
[PROOF STEP]
apply (simp add:ring_l_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_times_minusr:"a \<in> carrier R \<Longrightarrow>  -\<^sub>a a = a \<cdot>\<^sub>r (-\<^sub>a 1\<^sub>r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier R \<Longrightarrow> -\<^sub>a a = a \<cdot>\<^sub>r (-\<^sub>a 1\<^sub>r)
[PROOF STEP]
apply (cut_tac ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; 1\<^sub>r \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a a = a \<cdot>\<^sub>r (-\<^sub>a 1\<^sub>r)
[PROOF STEP]
apply (frule ring_inv1_2[of "a" "1\<^sub>r"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; 1\<^sub>r \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r 1\<^sub>r = a \<cdot>\<^sub>r (-\<^sub>a 1\<^sub>r)\<rbrakk> \<Longrightarrow> -\<^sub>a a = a \<cdot>\<^sub>r (-\<^sub>a 1\<^sub>r)
[PROOF STEP]
apply (simp add:ring_r_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_inv1_3:"\<lbrakk>a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow>
                           a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r (-\<^sub>a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (subst  aGroup.ag_inv_inv[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> (-\<^sub>a (-\<^sub>a a)) \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed[of "R" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; -\<^sub>a a \<in> carrier R\<rbrakk> \<Longrightarrow> (-\<^sub>a (-\<^sub>a a)) \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (subst ring_inv1_1[THEN sym, of "-\<^sub>a a" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; aGroup R; -\<^sub>a a \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a (-\<^sub>a a) \<cdot>\<^sub>r b = (-\<^sub>a a) \<cdot>\<^sub>r (-\<^sub>a b)
[PROOF STEP]
apply (subst ring_inv1_2[of "-\<^sub>a a" "b"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_distrib4:"\<lbrakk>a \<in> carrier R; b \<in> carrier R;
                                x \<in> carrier R; y \<in> carrier R \<rbrakk> \<Longrightarrow>
      a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a x \<cdot>\<^sub>r y) = a \<cdot>\<^sub>r (b \<plusminus> (-\<^sub>a y)) \<plusminus> (a \<plusminus> (-\<^sub>a x)) \<cdot>\<^sub>r y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r (b \<plusminus> -\<^sub>a y) \<plusminus> (a \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r (b \<plusminus> -\<^sub>a y) \<plusminus> (a \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (subst ring_distrib1, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a y \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a y) \<plusminus> (a \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a y) \<plusminus> (a \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (subst ring_distrib2, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a y) \<plusminus> (a \<cdot>\<^sub>r y \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y)
[PROOF STEP]
apply (rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a y) \<plusminus> (a \<cdot>\<^sub>r y \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y)
[PROOF STEP]
apply (subst aGroup.pOp_assocTr43, assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (-\<^sub>a y) \<in> carrier R
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r y \<in> carrier R
 4. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> (-\<^sub>a x) \<cdot>\<^sub>r y \<in> carrier R
 5. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> (a \<cdot>\<^sub>r (-\<^sub>a y) \<plusminus> a \<cdot>\<^sub>r y) \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (rule ring_tOp_closed, assumption+)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a y \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r y \<in> carrier R
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> (-\<^sub>a x) \<cdot>\<^sub>r y \<in> carrier R
 4. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> (a \<cdot>\<^sub>r (-\<^sub>a y) \<plusminus> a \<cdot>\<^sub>r y) \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r y \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> (-\<^sub>a x) \<cdot>\<^sub>r y \<in> carrier R
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> (a \<cdot>\<^sub>r (-\<^sub>a y) \<plusminus> a \<cdot>\<^sub>r y) \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (rule ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> (-\<^sub>a x) \<cdot>\<^sub>r y \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> (a \<cdot>\<^sub>r (-\<^sub>a y) \<plusminus> a \<cdot>\<^sub>r y) \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (rule ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> y \<in> carrier R
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> (a \<cdot>\<^sub>r (-\<^sub>a y) \<plusminus> a \<cdot>\<^sub>r y) \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (simp add:aGroup.ag_mOp_closed)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> (a \<cdot>\<^sub>r (-\<^sub>a y) \<plusminus> a \<cdot>\<^sub>r y) \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (subst ring_distrib1 [THEN sym, of "a" _], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a y \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> y \<in> carrier R
 3. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a y \<plusminus> y) \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a y \<plusminus> y) \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (simp add:aGroup.ag_l_inv1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r \<zero> \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (simp add:ring_times_x_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> \<zero> \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (subst aGroup.ag_r_zero, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (simp add:ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y = a \<cdot>\<^sub>r b \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y
[PROOF STEP]
apply (simp add: ring_inv1_1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) rMulLC:
     "\<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk>
        \<Longrightarrow> x \<cdot>\<^sub>r (y \<cdot>\<^sub>r z) = y \<cdot>\<^sub>r (x \<cdot>\<^sub>r z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r (y \<cdot>\<^sub>r z) = y \<cdot>\<^sub>r (x \<cdot>\<^sub>r z)
[PROOF STEP]
apply (subst ring_tOp_assoc [THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<cdot>\<^sub>r z = y \<cdot>\<^sub>r (x \<cdot>\<^sub>r z)
[PROOF STEP]
apply (subst ring_tOp_commute [of "x" "y"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> y \<cdot>\<^sub>r x \<cdot>\<^sub>r z = y \<cdot>\<^sub>r (x \<cdot>\<^sub>r z)
[PROOF STEP]
apply (subst ring_tOp_assoc, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; z \<in> carrier R\<rbrakk> \<Longrightarrow> y \<cdot>\<^sub>r (x \<cdot>\<^sub>r z) = y \<cdot>\<^sub>r (x \<cdot>\<^sub>r z)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Zero_ring:"1\<^sub>r = \<zero> \<Longrightarrow> zeroring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>r = \<zero> \<Longrightarrow> zeroring R
[PROOF STEP]
apply (simp add:zeroring_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>r = \<zero> \<Longrightarrow> Ring R \<and> carrier R = {\<zero>}
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 1\<^sub>r = \<zero> \<Longrightarrow> Ring R
 2. 1\<^sub>r = \<zero> \<Longrightarrow> carrier R = {\<zero>}
[PROOF STEP]
apply (rule Ring_axioms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>r = \<zero> \<Longrightarrow> carrier R = {\<zero>}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 1\<^sub>r = \<zero> \<Longrightarrow> carrier R \<subseteq> {\<zero>}
 2. 1\<^sub>r = \<zero> \<Longrightarrow> {\<zero>} \<subseteq> carrier R
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>1\<^sub>r = \<zero>; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<in> {\<zero>}
 2. 1\<^sub>r = \<zero> \<Longrightarrow> {\<zero>} \<subseteq> carrier R
[PROOF STEP]
apply (frule_tac x = x in ring_r_one, simp add:ring_times_x_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>r = \<zero> \<Longrightarrow> {\<zero>} \<subseteq> carrier R
[PROOF STEP]
apply (simp add:ring_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Zero_ring1:"\<not> (zeroring R) \<Longrightarrow>  1\<^sub>r \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> zeroring R \<Longrightarrow> 1\<^sub>r \<noteq> \<zero>
[PROOF STEP]
apply (rule contrapos_pp, simp+,
       cut_tac Zero_ring, simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Sr_one:"sr R S \<Longrightarrow> 1\<^sub>r \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr R S \<Longrightarrow> 1\<^sub>r \<in> S
[PROOF STEP]
apply (simp add:sr_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Sr_zero:"sr R S \<Longrightarrow> \<zero> \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr R S \<Longrightarrow> \<zero> \<in> S
[PROOF STEP]
apply (cut_tac ring_is_ag, frule Sr_one[of "S"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R; 1\<^sub>r \<in> S\<rbrakk> \<Longrightarrow> \<zero> \<in> S
[PROOF STEP]
apply (simp add:sr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> carrier R \<and> (\<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S); aGroup R; 1\<^sub>r \<in> S\<rbrakk> \<Longrightarrow> \<zero> \<in> S
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup R; 1\<^sub>r \<in> S; S \<subseteq> carrier R; \<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S\<rbrakk> \<Longrightarrow> \<zero> \<in> S
[PROOF STEP]
apply (frule_tac x = "1\<^sub>r" in bspec, assumption,
       thin_tac "\<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S",
       frule_tac x = "1\<^sub>r" in bspec, assumption,
       thin_tac "\<forall>y\<in>S. 1\<^sub>r \<plusminus> -\<^sub>a y \<in> S \<and> 1\<^sub>r \<cdot>\<^sub>r y \<in> S",
       erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup R; 1\<^sub>r \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a 1\<^sub>r \<in> S; 1\<^sub>r \<cdot>\<^sub>r 1\<^sub>r \<in> S\<rbrakk> \<Longrightarrow> \<zero> \<in> S
[PROOF STEP]
apply (cut_tac ring_one,
       simp add:aGroup.ag_r_inv1[of "R" "1\<^sub>r"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Sr_mOp_closed:"\<lbrakk>sr R S; x \<in> S\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; x \<in> S\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> S
[PROOF STEP]
apply (frule Sr_zero[of "S"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; x \<in> S; \<zero> \<in> S\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> S
[PROOF STEP]
apply (simp add:sr_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; \<zero> \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; \<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> S
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; \<zero> \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; \<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> S
[PROOF STEP]
apply (frule_tac x = "\<zero>" in bspec, assumption,
        thin_tac "\<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S",
        frule_tac x = x in bspec, assumption,
        thin_tac "\<forall>y\<in>S. \<zero> \<plusminus> -\<^sub>a y \<in> S \<and> \<zero> \<cdot>\<^sub>r y \<in> S", erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; \<zero> \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; aGroup R; \<zero> \<plusminus> -\<^sub>a x \<in> S; \<zero> \<cdot>\<^sub>r x \<in> S\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> S
[PROOF STEP]
apply (frule subsetD[of "S" "carrier R" "\<zero>"], assumption+,
        frule subsetD[of "S" "carrier R" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; \<zero> \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; aGroup R; \<zero> \<plusminus> -\<^sub>a x \<in> S; \<zero> \<cdot>\<^sub>r x \<in> S; \<zero> \<in> carrier R; x \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> S
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed [of "R" "x"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; \<zero> \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; aGroup R; \<zero> \<plusminus> -\<^sub>a x \<in> S; \<zero> \<cdot>\<^sub>r x \<in> S; \<zero> \<in> carrier R; x \<in> carrier R; -\<^sub>a x \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> S
[PROOF STEP]
apply (simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Sr_pOp_closed:"\<lbrakk>sr R S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> S
[PROOF STEP]
apply (frule Sr_mOp_closed[of "S" "y"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; x \<in> S; y \<in> S; -\<^sub>a y \<in> S\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> S
[PROOF STEP]
apply (unfold sr_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; y \<in> S; -\<^sub>a y \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; \<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> S
[PROOF STEP]
apply (frule_tac x = x in bspec, assumption,
        thin_tac "\<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S",
        frule_tac x = "-\<^sub>a y" in bspec, assumption,
        thin_tac "\<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S", erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; y \<in> S; -\<^sub>a y \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; x \<plusminus> -\<^sub>a (-\<^sub>a y) \<in> S; x \<cdot>\<^sub>r (-\<^sub>a y) \<in> S\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> S
[PROOF STEP]
apply (cut_tac ring_is_ag )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; y \<in> S; -\<^sub>a y \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; x \<plusminus> -\<^sub>a (-\<^sub>a y) \<in> S; x \<cdot>\<^sub>r (-\<^sub>a y) \<in> S; aGroup R\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> S
[PROOF STEP]
apply (frule subsetD[of "S" "carrier R" "y"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; y \<in> S; -\<^sub>a y \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; x \<plusminus> -\<^sub>a (-\<^sub>a y) \<in> S; x \<cdot>\<^sub>r (-\<^sub>a y) \<in> S; aGroup R; y \<in> carrier R\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> S
[PROOF STEP]
apply (simp add:aGroup.ag_inv_inv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Sr_tOp_closed:"\<lbrakk>sr R S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<in> S
[PROOF STEP]
by (simp add:sr_def)