[STATEMENT]
lemma invim_of_ideal:"\<lbrakk>Ring R; ideal R I; ideal (qring R I) J \<rbrakk> \<Longrightarrow>
  ideal R (rInvim R (qring R I) (pj R I) J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> ideal R (rInvim R (R /\<^sub>r I) (pj R I) J)
[PROOF STEP]
apply (rule Ring.ideal_condition, assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) J \<subseteq> carrier R
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) J \<noteq> {}
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 4. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add:rInvim_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) J \<noteq> {}
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (subgoal_tac "\<zero>\<^bsub>R\<^esub> \<in> rInvim R (qring R I) (pj R I) J")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; \<zero>\<^bsub>R\<^esub> \<in> rInvim R (R /\<^sub>r I) (pj R I) J\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) J \<noteq> {}
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R\<^esub> \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 4. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add:nonempty)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R\<^esub> \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add:rInvim_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R\<^esub> \<in> carrier R \<and> pj R I \<zero>\<^bsub>R\<^esub> \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add: Ring.ring_zero)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> pj R I \<zero>\<^bsub>R\<^esub> \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (frule Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; aGroup R\<rbrakk> \<Longrightarrow> pj R I \<zero>\<^bsub>R\<^esub> \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (frule pj_Hom [of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; aGroup R; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I \<zero>\<^bsub>R\<^esub> \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (frule Ring.qring_ring [of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; aGroup R; pj R I \<in> rHom R (R /\<^sub>r I); Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I \<zero>\<^bsub>R\<^esub> \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (frule rHom_0_0 [of "R" "R /\<^sub>r I" "pj R I"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; aGroup R; pj R I \<in> rHom R (R /\<^sub>r I); Ring (R /\<^sub>r I); pj R I \<zero>\<^bsub>R\<^esub> = \<zero>\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> pj R I \<zero>\<^bsub>R\<^esub> \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add:Ring.ideal_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. \<forall>y\<in>rInvim R (R /\<^sub>r I) (pj R I) J. x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> rInvim R (R /\<^sub>r I) (pj R I) J; y \<in> rInvim R (R /\<^sub>r I) (pj R I) J\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> rInvim R (R /\<^sub>r I) (pj R I) J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add:rInvim_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R \<and> pj R I x \<in> J; y \<in> carrier R \<and> pj R I y \<in> J\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R \<and> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R \<and> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R
 2. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J\<rbrakk> \<Longrightarrow> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (frule Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R
 2. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J\<rbrakk> \<Longrightarrow> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R
 2. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J\<rbrakk> \<Longrightarrow> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 3. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J\<rbrakk> \<Longrightarrow> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (frule pj_Hom [of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (frule Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; pj R I \<in> rHom R (R /\<^sub>r I); aGroup R\<rbrakk> \<Longrightarrow> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (frule_tac x = y in aGroup.ag_mOp_closed [of "R"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; pj R I \<in> rHom R (R /\<^sub>r I); aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add:rHom_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; pj R I \<in> aHom R (R /\<^sub>r I) \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> pj R I (x \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (subst aHom_add [of "R" "R /\<^sub>r I" "pj R I"], assumption+)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> aGroup (R /\<^sub>r I)
 2. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> pj R I \<in> aHom R (R /\<^sub>r I)
 3. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> x \<in> carrier R
 4. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R
 5. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> pj R I x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I (-\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 6. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add:Ring.qring_ring Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> pj R I \<in> aHom R (R /\<^sub>r I)
 2. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> x \<in> carrier R
 3. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R
 4. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> pj R I x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I (-\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 5. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> pj R I x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I (-\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (frule Ring.qring_ring [of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I (-\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (rule Ring.ideal_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I (-\<^sub>a\<^bsub>R\<^esub> y) \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (subst aHom_inv_inv[of "R" "R /\<^sub>r I" "pj R I"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> aGroup (R /\<^sub>r I)
 2. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I \<in> aHom R (R /\<^sub>r I)
 3. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> y \<in> carrier R
 4. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I y \<in> J
 5. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add:Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I \<in> aHom R (R /\<^sub>r I)
 2. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> y \<in> carrier R
 3. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I y \<in> J
 4. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> carrier R; pj R I x \<in> J; y \<in> carrier R; pj R I y \<in> J; aGroup R; -\<^sub>a\<^bsub>R\<^esub> y \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I y \<in> J
 2. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (frule_tac x = "pj R I y" in Ring.ideal_inv1_closed [of "R /\<^sub>r I" "J"],
                                              assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>rInvim R (R /\<^sub>r I) (pj R I) J. r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> rInvim R (R /\<^sub>r I) (pj R I) J\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add:rInvim_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R \<and> pj R I x \<in> J\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> carrier R \<and> pj R I (r \<cdot>\<^sub>r\<^bsub>R\<^esub> x) \<in> J
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>R\<^esub> x \<in> carrier R \<and> pj R I (r \<cdot>\<^sub>r\<^bsub>R\<^esub> x) \<in> J
[PROOF STEP]
apply (simp add:Ring.ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J\<rbrakk> \<Longrightarrow> pj R I (r \<cdot>\<^sub>r\<^bsub>R\<^esub> x) \<in> J
[PROOF STEP]
apply (frule pj_Hom [of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I (r \<cdot>\<^sub>r\<^bsub>R\<^esub> x) \<in> J
[PROOF STEP]
apply (subst rHom_tOp [of "R" "R /\<^sub>r I" _ _ "pj R I"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> Ring (R /\<^sub>r I)
 2. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> r \<in> carrier R
 3. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> x \<in> carrier R
 4. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I \<in> rHom R (R /\<^sub>r I)
 5. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I x \<in> J
[PROOF STEP]
apply (frule Ring.qring_ring[of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I x \<in> J
[PROOF STEP]
apply (rule Ring.ideal_ring_multiple [of "R /\<^sub>r I" "J"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> Ring (R /\<^sub>r I)
 2. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> ideal (R /\<^sub>r I) J
 3. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I x \<in> J
 4. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I r \<in> carrier (R /\<^sub>r I)
[PROOF STEP]
apply (simp add:Ring.qring_ring)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> ideal (R /\<^sub>r I) J
 2. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I x \<in> J
 3. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I r \<in> carrier (R /\<^sub>r I)
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; r \<in> carrier R; x \<in> carrier R; pj R I x \<in> J; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> pj R I r \<in> carrier (R /\<^sub>r I)
[PROOF STEP]
apply (simp add:rHom_mem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pj_invim_cont_I:"\<lbrakk>Ring R; ideal R I; ideal (qring R I) J\<rbrakk> \<Longrightarrow>
                         I \<subseteq> (rInvim R (qring R I) (pj R I) J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J\<rbrakk> \<Longrightarrow> I \<subseteq> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> I\<rbrakk> \<Longrightarrow> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J
[PROOF STEP]
apply (simp add:rInvim_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> I\<rbrakk> \<Longrightarrow> x \<in> carrier R \<and> pj R I x \<in> J
[PROOF STEP]
apply (frule Ring.ideal_subset [of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<in> carrier R \<and> pj R I x \<in> J
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> I; x \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I x \<in> J
[PROOF STEP]
apply (frule  pj_mem [of "R" "I"  _], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> I; x \<in> carrier R; pj R I x = x \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> pj R I x \<in> J
[PROOF STEP]
apply (simp add:Ring.ar_coset_same4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> I; x \<in> carrier R; pj R I x = I\<rbrakk> \<Longrightarrow> I \<in> J
[PROOF STEP]
apply (frule  Ring.qring_ring[of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> I; x \<in> carrier R; pj R I x = I; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> I \<in> J
[PROOF STEP]
apply (frule Ring.ideal_zero [of "qring R I" "J"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> I; x \<in> carrier R; pj R I x = I; Ring (R /\<^sub>r I); \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> J\<rbrakk> \<Longrightarrow> I \<in> J
[PROOF STEP]
apply (frule Ring.qring_zero[of "R" "I"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J; x \<in> I; x \<in> carrier R; pj R I x = I; Ring (R /\<^sub>r I); \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> J; \<zero>\<^bsub>R /\<^sub>r I\<^esub> = I\<rbrakk> \<Longrightarrow> I \<in> J
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pj_invim_mono1:"\<lbrakk>Ring R; ideal R I; ideal (qring R I) J1;
      ideal (qring R I) J2; J1 \<subseteq> J2 \<rbrakk> \<Longrightarrow>
      (rInvim R (qring R I) (pj R I) J1) \<subseteq> (rInvim R (qring R I) (pj R I) J2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J1; ideal (R /\<^sub>r I) J2; J1 \<subseteq> J2\<rbrakk> \<Longrightarrow> rInvim R (R /\<^sub>r I) (pj R I) J1 \<subseteq> rInvim R (R /\<^sub>r I) (pj R I) J2
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J1; ideal (R /\<^sub>r I) J2; J1 \<subseteq> J2; x \<in> rInvim R (R /\<^sub>r I) (pj R I) J1\<rbrakk> \<Longrightarrow> x \<in> rInvim R (R /\<^sub>r I) (pj R I) J2
[PROOF STEP]
apply (simp add:rInvim_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal (R /\<^sub>r I) J1; ideal (R /\<^sub>r I) J2; J1 \<subseteq> J2; x \<in> carrier R \<and> pj R I x \<in> J1\<rbrakk> \<Longrightarrow> pj R I x \<in> J2
[PROOF STEP]
apply (simp add:subsetD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pj_img_ideal:"\<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow>
                                  ideal (qring R I) ((pj R I)`J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> ideal (R /\<^sub>r I) (pj R I ` J)
[PROOF STEP]
apply (rule Ring.ideal_condition [of "qring R I" "(pj R I) `J"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> Ring (R /\<^sub>r I)
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> pj R I ` J \<subseteq> carrier (R /\<^sub>r I)
 3. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> pj R I ` J \<noteq> {}
 4. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>x\<in>pj R I ` J. \<forall>y\<in>pj R I ` J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 5. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (simp add:Ring.qring_ring)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> pj R I ` J \<subseteq> carrier (R /\<^sub>r I)
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> pj R I ` J \<noteq> {}
 3. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>x\<in>pj R I ` J. \<forall>y\<in>pj R I ` J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 4. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (rule subsetI, simp add:image_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; \<exists>xa\<in>J. x = pj R I xa\<rbrakk> \<Longrightarrow> x \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> pj R I ` J \<noteq> {}
 3. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>x\<in>pj R I ` J. \<forall>y\<in>pj R I ` J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 4. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (erule bexE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; xa \<in> J; x = pj R I xa\<rbrakk> \<Longrightarrow> x \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> pj R I ` J \<noteq> {}
 3. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>x\<in>pj R I ` J. \<forall>y\<in>pj R I ` J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 4. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule_tac h = xa in Ring.ideal_subset [of "R" "J"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; xa \<in> J; x = pj R I xa; xa \<in> carrier R\<rbrakk> \<Longrightarrow> x \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> pj R I ` J \<noteq> {}
 3. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>x\<in>pj R I ` J. \<forall>y\<in>pj R I ` J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 4. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule pj_Hom [of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; xa \<in> J; x = pj R I xa; xa \<in> carrier R; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> x \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> pj R I ` J \<noteq> {}
 3. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>x\<in>pj R I ` J. \<forall>y\<in>pj R I ` J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 4. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (simp add:rHom_mem)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> pj R I ` J \<noteq> {}
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>x\<in>pj R I ` J. \<forall>y\<in>pj R I ` J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 3. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule Ring.ideal_zero [of "R" "J"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; \<zero>\<^bsub>R\<^esub> \<in> J\<rbrakk> \<Longrightarrow> pj R I ` J \<noteq> {}
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>x\<in>pj R I ` J. \<forall>y\<in>pj R I ` J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 3. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (simp add:image_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; \<zero>\<^bsub>R\<^esub> \<in> J\<rbrakk> \<Longrightarrow> \<exists>x. \<exists>xa\<in>J. x = pj R I xa
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>x\<in>pj R I ` J. \<forall>y\<in>pj R I ` J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 3. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>x\<in>pj R I ` J. \<forall>y\<in>pj R I ` J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; x \<in> pj R I ` J; y \<in> pj R I ` J\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y \<in> pj R I ` J
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (simp add:image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; \<exists>xa\<in>J. x = pj R I xa; \<exists>x\<in>J. y = pj R I x\<rbrakk> \<Longrightarrow> \<exists>xa\<in>J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y = pj R I xa
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (erule bexE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y xa xb. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; xa \<in> J; x = pj R I xa; xb \<in> J; y = pj R I xb\<rbrakk> \<Longrightarrow> \<exists>xa\<in>J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y = pj R I xa
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule pj_Hom [of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y xa xb. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; xa \<in> J; x = pj R I xa; xb \<in> J; y = pj R I xb; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y = pj R I xa
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (rename_tac x y s t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; pj R I \<in> rHom R (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y = pj R I xa
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule_tac h = s in Ring.ideal_subset [of "R" "J"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; pj R I \<in> rHom R (R /\<^sub>r I); s \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>xa\<in>J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y = pj R I xa
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule_tac h = t in Ring.ideal_subset [of "R" "J"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; pj R I \<in> rHom R (R /\<^sub>r I); s \<in> carrier R; t \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>xa\<in>J. x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> y = pj R I xa
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (simp add:rHom_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; pj R I \<in> aHom R (R /\<^sub>r I) \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; s \<in> carrier R; t \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I t = pj R I x
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; s \<in> carrier R; t \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I t = pj R I x
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; s \<in> carrier R; t \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; aGroup R\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I t = pj R I x
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule Ring.qring_ring [of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; s \<in> carrier R; t \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; aGroup R; Ring (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I t = pj R I x
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule Ring.ring_is_ag [of "R /\<^sub>r I"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; s \<in> carrier R; t \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; aGroup R; Ring (R /\<^sub>r I); aGroup (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I t = pj R I x
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule_tac x = t in aGroup.ag_mOp_closed [of "R"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; s \<in> carrier R; t \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; aGroup R; Ring (R /\<^sub>r I); aGroup (R /\<^sub>r I); -\<^sub>a\<^bsub>R\<^esub> t \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I t = pj R I x
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule_tac a1 = s and b1 = "-\<^sub>a\<^bsub>R\<^esub> t" in aHom_add [of "R" "R /\<^sub>r I"
  "pj R I", THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; s \<in> carrier R; t \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; aGroup R; Ring (R /\<^sub>r I); aGroup (R /\<^sub>r I); -\<^sub>a\<^bsub>R\<^esub> t \<in> carrier R; pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I (-\<^sub>a\<^bsub>R\<^esub> t) = pj R I (s \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> t)\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I t = pj R I x
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (simp add:aHom_inv_inv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; s \<in> carrier R; t \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; aGroup R; Ring (R /\<^sub>r I); aGroup (R /\<^sub>r I); -\<^sub>a\<^bsub>R\<^esub> t \<in> carrier R; pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I t = pj R I (s \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> t)\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I (s \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> t) = pj R I x
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule_tac x = t in Ring.ideal_inv1_closed [of "R" "J"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; s \<in> carrier R; t \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; aGroup R; Ring (R /\<^sub>r I); aGroup (R /\<^sub>r I); -\<^sub>a\<^bsub>R\<^esub> t \<in> carrier R; pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I t = pj R I (s \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> t); -\<^sub>a\<^bsub>R\<^esub> t \<in> J\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I (s \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> t) = pj R I x
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (frule_tac x = s and y = "-\<^sub>a\<^bsub>R\<^esub> t" in Ring.ideal_pOp_closed [of "R" "J"],
                                             assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y s t. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; s \<in> J; x = pj R I s; t \<in> J; y = pj R I t; s \<in> carrier R; t \<in> carrier R; pj R I \<in> aHom R (R /\<^sub>r I); \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y; pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>; aGroup R; Ring (R /\<^sub>r I); aGroup (R /\<^sub>r I); -\<^sub>a\<^bsub>R\<^esub> t \<in> carrier R; pj R I s \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> pj R I t = pj R I (s \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> t); -\<^sub>a\<^bsub>R\<^esub> t \<in> J; s \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> t \<in> J\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I (s \<plusminus>\<^bsub>R\<^esub> -\<^sub>a\<^bsub>R\<^esub> t) = pj R I x
 2. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier (R /\<^sub>r I). \<forall>x\<in>pj R I ` J. r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; r \<in> carrier (R /\<^sub>r I); x \<in> pj R I ` J\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> x \<in> pj R I ` J
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; r \<in> set_rcs (b_ag R) I; x \<in> pj R I ` J\<rbrakk> \<Longrightarrow> rcostOp R I r x \<in> pj R I ` J
[PROOF STEP]
apply (simp add:Ring.set_r_ar_cos)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; r \<in> set_ar_cos R I; x \<in> pj R I ` J\<rbrakk> \<Longrightarrow> rcostOp R I r x \<in> pj R I ` J
[PROOF STEP]
apply (simp add:set_ar_cos_def, erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; x \<in> pj R I ` J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> rcostOp R I r x \<in> pj R I ` J
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; x \<in> pj R I ` J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> rcostOp R I (a \<uplus>\<^bsub>R\<^esub> I) x \<in> pj R I ` J
[PROOF STEP]
apply (simp add:image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; \<exists>xa\<in>J. x = pj R I xa; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> \<exists>xa\<in>J. rcostOp R I (a \<uplus>\<^bsub>R\<^esub> I) x = pj R I xa
[PROOF STEP]
apply (erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = pj R I xa\<rbrakk> \<Longrightarrow> \<exists>xa\<in>J. rcostOp R I (a \<uplus>\<^bsub>R\<^esub> I) x = pj R I xa
[PROOF STEP]
apply (frule_tac x = xa in pj_mem [of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = pj R I xa\<rbrakk> \<Longrightarrow> xa \<in> carrier R
 2. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = pj R I xa; pj R I xa = xa \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> \<exists>xa\<in>J. rcostOp R I (a \<uplus>\<^bsub>R\<^esub> I) x = pj R I xa
[PROOF STEP]
apply (simp add:Ring.ideal_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = pj R I xa; pj R I xa = xa \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> \<exists>xa\<in>J. rcostOp R I (a \<uplus>\<^bsub>R\<^esub> I) x = pj R I xa
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = xa \<uplus>\<^bsub>R\<^esub> I; pj R I xa = xa \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. rcostOp R I (a \<uplus>\<^bsub>R\<^esub> I) (xa \<uplus>\<^bsub>R\<^esub> I) = pj R I x
[PROOF STEP]
apply (subst Ring.rcostOp, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>r x a xa xb. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = xa \<uplus>\<^bsub>R\<^esub> I; pj R I xa = xa \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> xa \<in> carrier R
 2. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = xa \<uplus>\<^bsub>R\<^esub> I; pj R I xa = xa \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<uplus>\<^bsub>R\<^esub> I = pj R I x
[PROOF STEP]
apply (simp add:Ring.ideal_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = xa \<uplus>\<^bsub>R\<^esub> I; pj R I xa = xa \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<uplus>\<^bsub>R\<^esub> I = pj R I x
[PROOF STEP]
apply (frule_tac x = xa and r = a in Ring.ideal_ring_multiple [of "R" "J"],
                                                  assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = xa \<uplus>\<^bsub>R\<^esub> I; pj R I xa = xa \<uplus>\<^bsub>R\<^esub> I; a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<in> J\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<uplus>\<^bsub>R\<^esub> I = pj R I x
[PROOF STEP]
apply (frule_tac h = "a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa" in Ring.ideal_subset [of "R" "J"],
                                                                 assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = xa \<uplus>\<^bsub>R\<^esub> I; pj R I xa = xa \<uplus>\<^bsub>R\<^esub> I; a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<in> J; a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<uplus>\<^bsub>R\<^esub> I = pj R I x
[PROOF STEP]
apply (frule_tac x1 = "a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa" in pj_mem [THEN sym, of "R" "I"],
                                                                 assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = xa \<uplus>\<^bsub>R\<^esub> I; pj R I xa = xa \<uplus>\<^bsub>R\<^esub> I; a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<in> J; a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<in> carrier R; a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<uplus>\<^bsub>R\<^esub> I = pj R I (a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<uplus>\<^bsub>R\<^esub> I = pj R I x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x a xa. \<lbrakk>Ring R; ideal R I; ideal R J; I \<subseteq> J; a \<in> carrier R; r = a \<uplus>\<^bsub>R\<^esub> I; xa \<in> J; x = xa \<uplus>\<^bsub>R\<^esub> I; pj R I xa = xa \<uplus>\<^bsub>R\<^esub> I; a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<in> J; a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<in> carrier R; a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa \<uplus>\<^bsub>R\<^esub> I = pj R I (a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>J. pj R I (a \<cdot>\<^sub>r\<^bsub>R\<^esub> xa) = pj R I x
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma npQring:"\<lbrakk>Ring R; ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow>
      npow (qring R I) (a \<uplus>\<^bsub>R\<^esub> I) n = (npow R a n) \<uplus>\<^bsub>R\<^esub> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow> (a \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>R /\<^sub>r I n\<^esup> = a^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring R; ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow> (a \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>R /\<^sub>r I 0\<^esup> = a^\<^bsup>R 0\<^esup> \<uplus>\<^bsub>R\<^esub> I
 2. \<And>n. \<lbrakk>Ring R; ideal R I; a \<in> carrier R; (a \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>R /\<^sub>r I n\<^esup> = a^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> (a \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>R /\<^sub>r I Suc n\<^esup> = a^\<^bsup>R Suc n\<^esup> \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring R; ideal R I; a \<in> carrier R; (a \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>R /\<^sub>r I n\<^esup> = a^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> (a \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>R /\<^sub>r I Suc n\<^esup> = a^\<^bsup>R Suc n\<^esup> \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring R; ideal R I; a \<in> carrier R; (a \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>\<lparr>carrier = set_rcs (b_ag R) I, pop = c_top (b_ag R) I, mop = c_iop (b_ag R) I, zero = I, tp = rcostOp R I, un = 1\<^sub>r\<^bsub>R\<^esub> \<uplus>\<^bsub>R\<^esub> I\<rparr> n\<^esup> = a^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> rcostOp R I (a^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I) (a \<uplus>\<^bsub>R\<^esub> I) = a^\<^bsup>R n\<^esup> \<cdot>\<^sub>r\<^bsub>R\<^esub> a \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (rule Ring.rcostOp, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>Ring R; ideal R I; a \<in> carrier R; (a \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>\<lparr>carrier = set_rcs (b_ag R) I, pop = c_top (b_ag R) I, mop = c_iop (b_ag R) I, zero = I, tp = rcostOp R I, un = 1\<^sub>r\<^bsub>R\<^esub> \<uplus>\<^bsub>R\<^esub> I\<rparr> n\<^esup> = a^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> a^\<^bsup>R n\<^esup> \<in> carrier R
 2. \<And>n. \<lbrakk>Ring R; ideal R I; a \<in> carrier R; (a \<uplus>\<^bsub>R\<^esub> I)^\<^bsup>\<lparr>carrier = set_rcs (b_ag R) I, pop = c_top (b_ag R) I, mop = c_iop (b_ag R) I, zero = I, tp = rcostOp R I, un = 1\<^sub>r\<^bsub>R\<^esub> \<uplus>\<^bsub>R\<^esub> I\<rparr> n\<^esup> = a^\<^bsup>R n\<^esup> \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> a \<in> carrier R
[PROOF STEP]
apply (rule Ring.npClose, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) maximal_ideal_ideal:"\<lbrakk>maximal_ideal R mx\<rbrakk> \<Longrightarrow> ideal R mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_ideal R mx \<Longrightarrow> ideal R mx
[PROOF STEP]
by (simp add:maximal_ideal_def)


[STATEMENT]
lemma (in Ring) maximal_ideal_proper:"maximal_ideal R mx \<Longrightarrow> 1\<^sub>r \<notin> mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_ideal R mx \<Longrightarrow> 1\<^sub>r \<notin> mx
[PROOF STEP]
by (simp add:maximal_ideal_def)


[STATEMENT]
lemma (in Ring) prime_ideal_ideal:"prime_ideal R I \<Longrightarrow> ideal R I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_ideal R I \<Longrightarrow> ideal R I
[PROOF STEP]
by (simp add:prime_ideal_def)


[STATEMENT]
lemma (in Ring) prime_ideal_proper:"prime_ideal R I \<Longrightarrow> I \<noteq> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_ideal R I \<Longrightarrow> I \<noteq> carrier R
[PROOF STEP]
apply (simp add:prime_ideal_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; 1\<^sub>r \<notin> I; \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> I \<longrightarrow> x \<in> I \<or> y \<in> I\<rbrakk> \<Longrightarrow> I \<noteq> carrier R
[PROOF STEP]
apply (simp add:proper_ideal)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) prime_ideal_proper1:"prime_ideal R p \<Longrightarrow> 1\<^sub>r \<notin> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_ideal R p \<Longrightarrow> 1\<^sub>r \<notin> p
[PROOF STEP]
by (simp add:prime_ideal_def)


[STATEMENT]
lemma (in Ring) primary_ideal_ideal:"primary_ideal R q \<Longrightarrow> ideal R q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primary_ideal R q \<Longrightarrow> ideal R q
[PROOF STEP]
by (simp add:primary_ideal_def)


[STATEMENT]
lemma (in Ring)  primary_ideal_proper1:"primary_ideal R q \<Longrightarrow> 1\<^sub>r \<notin> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primary_ideal R q \<Longrightarrow> 1\<^sub>r \<notin> q
[PROOF STEP]
by (simp add:primary_ideal_def)


[STATEMENT]
lemma (in Ring) prime_elems_mult_not:"\<lbrakk>prime_ideal R P; x \<in> carrier R;
                y \<in> carrier R; x \<notin> P; y \<notin> P \<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<notin> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime_ideal R P; x \<in> carrier R; y \<in> carrier R; x \<notin> P; y \<notin> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<notin> P
[PROOF STEP]
apply (simp add:prime_ideal_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<notin> P; y \<notin> P; ideal R P; 1\<^sub>r \<notin> P; \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> P \<longrightarrow> x \<in> P \<or> y \<in> P\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r y \<notin> P
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<notin> P; y \<notin> P; ideal R P; 1\<^sub>r \<notin> P; \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> P \<longrightarrow> x \<in> P \<or> y \<in> P; x \<cdot>\<^sub>r y \<in> P\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = x in bspec, assumption,
        thin_tac "\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> P \<longrightarrow> x \<in> P \<or> y \<in> P",
        frule_tac x = y in bspec, assumption,
        thin_tac "\<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> P \<longrightarrow> x \<in> P \<or> y \<in> P", simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) prime_is_primary:"prime_ideal R p \<Longrightarrow> primary_ideal R p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_ideal R p \<Longrightarrow> primary_ideal R p
[PROOF STEP]
apply (unfold primary_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_ideal R p \<Longrightarrow> ideal R p \<and> 1\<^sub>r \<notin> p \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> p \<longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p \<or> y \<in> p))
[PROOF STEP]
apply (rule conjI, simp add:prime_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_ideal R p \<Longrightarrow> 1\<^sub>r \<notin> p \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> p \<longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p \<or> y \<in> p))
[PROOF STEP]
apply (rule conjI, simp add:prime_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_ideal R p \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> p \<longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p \<or> y \<in> p)
[PROOF STEP]
apply ((rule ballI)+, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>prime_ideal R p; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> p\<rbrakk> \<Longrightarrow> \<exists>n. x^\<^bsup>R n\<^esup> \<in> p \<or> y \<in> p
[PROOF STEP]
apply (simp add:prime_ideal_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> p; ideal R p; 1\<^sub>r \<notin> p; \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> p \<longrightarrow> x \<in> p \<or> y \<in> p\<rbrakk> \<Longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p) \<or> y \<in> p
[PROOF STEP]
apply (frule_tac x = x in bspec, assumption,
        thin_tac "\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> p \<longrightarrow> x \<in> p \<or> y \<in> p",
        frule_tac x = y in bspec, assumption,
        thin_tac "\<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> p \<longrightarrow> x \<in> p \<or> y \<in> p", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> p; ideal R p; 1\<^sub>r \<notin> p; x \<in> p \<or> y \<in> p\<rbrakk> \<Longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p) \<or> y \<in> p
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> p; ideal R p; 1\<^sub>r \<notin> p; x \<in> p\<rbrakk> \<Longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p) \<or> y \<in> p
 2. \<And>x y. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> p; ideal R p; 1\<^sub>r \<notin> p; y \<in> p\<rbrakk> \<Longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p) \<or> y \<in> p
[PROOF STEP]
apply (frule_tac t = x in np_1[THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> p; ideal R p; 1\<^sub>r \<notin> p; x \<in> p; x = x^\<^bsup>R Suc 0\<^esup>\<rbrakk> \<Longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p) \<or> y \<in> p
 2. \<And>x y. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> p; ideal R p; 1\<^sub>r \<notin> p; y \<in> p\<rbrakk> \<Longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p) \<or> y \<in> p
[PROOF STEP]
apply (frule_tac a = x and A = p and b = "x^\<^bsup>R (Suc 0)\<^esup>" in eq_elem_in,
                                               assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> p; ideal R p; 1\<^sub>r \<notin> p; x \<in> p; x = x^\<^bsup>R Suc 0\<^esup>; x^\<^bsup>R Suc 0\<^esup> \<in> p\<rbrakk> \<Longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p) \<or> y \<in> p
 2. \<And>x y. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> p; ideal R p; 1\<^sub>r \<notin> p; y \<in> p\<rbrakk> \<Longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p) \<or> y \<in> p
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> p; ideal R p; 1\<^sub>r \<notin> p; y \<in> p\<rbrakk> \<Longrightarrow> (\<exists>n. x^\<^bsup>R n\<^esup> \<in> p) \<or> y \<in> p
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) maximal_prime_Tr0:"\<lbrakk>maximal_ideal R mx; x \<in> carrier R; x \<notin> mx\<rbrakk>
              \<Longrightarrow>  mx \<minusplus> (Rxa R x) = carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; x \<in> carrier R; x \<notin> mx\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
[PROOF STEP]
apply (frule principal_ideal [of "x"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x)\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
[PROOF STEP]
apply (frule maximal_ideal_ideal[of "mx"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
[PROOF STEP]
apply (frule sum_ideals [of "mx" "Rxa R x"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x)\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
[PROOF STEP]
apply (frule sum_ideals_la1 [of "mx" "Rxa R x"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
[PROOF STEP]
apply (simp add:maximal_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1\<^sub>r \<notin> mx \<and> {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}; x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
[PROOF STEP]
apply (subgoal_tac "mx \<minusplus> (Rxa R x) \<in> {J. ideal R J \<and> mx \<subseteq> J}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}; mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
 2. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}; mx \<minusplus> R \<diamondsuit>\<^sub>p x = mx \<or> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
 2. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (frule sum_ideals_la2 [of "mx" "Rxa R x"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}; mx \<minusplus> R \<diamondsuit>\<^sub>p x = mx \<or> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
 2. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (frule a_in_principal [of "x"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}; mx \<minusplus> R \<diamondsuit>\<^sub>p x = mx \<or> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; x \<in> R \<diamondsuit>\<^sub>p x\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
 2. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (frule subsetD [of "Rxa R x" "mx \<minusplus> (Rxa R x)" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}; mx \<minusplus> R \<diamondsuit>\<^sub>p x = mx \<or> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; x \<in> R \<diamondsuit>\<^sub>p x; x \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p x\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
 2. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (thin_tac "{J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; mx \<minusplus> R \<diamondsuit>\<^sub>p x = mx \<or> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R; R \<diamondsuit>\<^sub>p x \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; x \<in> R \<diamondsuit>\<^sub>p x; x \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p x\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
 2. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; R \<diamondsuit>\<^sub>p x \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; x \<in> R \<diamondsuit>\<^sub>p x; x \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p x; mx \<minusplus> R \<diamondsuit>\<^sub>p x = mx\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
 2. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; R \<diamondsuit>\<^sub>p x \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; x \<in> R \<diamondsuit>\<^sub>p x; x \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p x; mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
 3. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; R \<diamondsuit>\<^sub>p x \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; x \<in> R \<diamondsuit>\<^sub>p x; x \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p x; mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R
 2. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (thin_tac "{J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; x \<notin> mx; ideal R (R \<diamondsuit>\<^sub>p x); ideal R mx; ideal R (mx \<minusplus> R \<diamondsuit>\<^sub>p x); mx \<subseteq> mx \<minusplus> R \<diamondsuit>\<^sub>p x; 1\<^sub>r \<notin> mx\<rbrakk> \<Longrightarrow> mx \<minusplus> R \<diamondsuit>\<^sub>p x \<in> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done