[STATEMENT]
lemma direct_lim_is_ring:
  assumes "U \<in> I"
  shows "ring carrier_direct_lim add_rel mult_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring carrier_direct_lim add_rel mult_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor>
[PROOF STEP]
proof unfold_locales
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel a b \<in> carrier_direct_lim
 2. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim
 3. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel (add_rel a b) c = add_rel a (add_rel b c)
 4. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> a = a
 5. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel a \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = a
 6. \<And>u. u \<in> carrier_direct_lim \<Longrightarrow> monoid.invertible carrier_direct_lim add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> u
 7. \<And>x y. \<lbrakk>x \<in> carrier_direct_lim; y \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel x y = add_rel y x
 8. \<And>a b. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel a b \<in> carrier_direct_lim
 9. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim
 10. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel (mult_rel a b) c = mult_rel a (mult_rel b c)
A total of 14 subgoals...
[PROOF STEP]
show add_rel: "add_rel a b \<in> carrier_direct_lim" and mult_rel: "mult_rel a b \<in> carrier_direct_lim"
    if "a \<in> carrier_direct_lim" "b \<in> carrier_direct_lim" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel a b \<in> carrier_direct_lim &&& mult_rel a b \<in> carrier_direct_lim
[PROOF STEP]
using \<open>U \<in> I\<close> that
[PROOF STATE]
proof (prove)
using this:
U \<in> I
a \<in> carrier_direct_lim
b \<in> carrier_direct_lim

goal (1 subgoal):
 1. add_rel a b \<in> carrier_direct_lim &&& mult_rel a b \<in> carrier_direct_lim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a1 \<in> carrier_direct_lim; ?b1 \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel ?a1 ?b1 \<in> carrier_direct_lim
\<lbrakk>?a1 \<in> carrier_direct_lim; ?b1 \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel ?a1 ?b1 \<in> carrier_direct_lim

goal (12 subgoals):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim
 2. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel (add_rel a b) c = add_rel a (add_rel b c)
 3. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> a = a
 4. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel a \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = a
 5. \<And>u. u \<in> carrier_direct_lim \<Longrightarrow> monoid.invertible carrier_direct_lim add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> u
 6. \<And>x y. \<lbrakk>x \<in> carrier_direct_lim; y \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel x y = add_rel y x
 7. \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim
 8. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel (mult_rel a b) c = mult_rel a (mult_rel b c)
 9. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> a = a
 10. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> mult_rel a \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = a
A total of 12 subgoals...
[PROOF STEP]
show zero_rel: "\<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim" and one_rel: "\<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim &&& \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim
[PROOF STEP]
using \<open>U \<in> I\<close>
[PROOF STATE]
proof (prove)
using this:
U \<in> I

goal (1 subgoal):
 1. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim &&& \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim
\<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim

goal (10 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel (add_rel a b) c = add_rel a (add_rel b c)
 2. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> a = a
 3. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel a \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = a
 4. \<And>u. u \<in> carrier_direct_lim \<Longrightarrow> monoid.invertible carrier_direct_lim add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> u
 5. \<And>x y. \<lbrakk>x \<in> carrier_direct_lim; y \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel x y = add_rel y x
 6. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel (mult_rel a b) c = mult_rel a (mult_rel b c)
 7. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> a = a
 8. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> mult_rel a \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = a
 9. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel a (add_rel b c) = add_rel (mult_rel a b) (mult_rel a c)
 10. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel (add_rel b c) a = add_rel (mult_rel b a) (mult_rel c a)
[PROOF STEP]
show add_rel_0: "add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X"
    and "mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X"
    and "mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X"
      if "X \<in> carrier_direct_lim" for X
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X &&& mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X &&& mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
define x where "x=(SOME x. x \<in> X)"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> X)

goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have x:"x\<in>X" "x\<in>Sigma I \<FF>" "fst x\<in>I" and X_alt:"X= \<lfloor>fst x, snd x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> X &&& x \<in> Sigma I \<FF> &&& fst x \<in> I) &&& X = \<lfloor>fst x, snd x\<rfloor>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>X \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. (x \<in> X &&& x \<in> Sigma I \<FF> &&& fst x \<in> I) &&& X = \<lfloor>fst x, snd x\<rfloor>
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. ((SOME x. x \<in> X) \<in> X &&& (SOME x. x \<in> X) \<in> Sigma I \<FF> &&& fst (SOME x. x \<in> X) \<in> I) &&& X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X
x \<in> Sigma I \<FF>
fst x \<in> I
X = \<lfloor>fst x, snd x\<rfloor>

goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
obtain w0 where w0:"w0\<in>I" "w0 \<subseteq> U" "w0 \<subseteq> fst x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; w0 \<subseteq> U; w0 \<subseteq> fst x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using has_lower_bound[OF \<open>U\<in>I\<close> \<open>fst x\<in>I\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>W\<in>I. W \<subseteq> U \<inter> fst x

goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; w0 \<subseteq> U; w0 \<subseteq> fst x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w0 \<in> I
w0 \<subseteq> U
w0 \<subseteq> fst x

goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
interpret uw0:ring_homomorphism "\<rho> U w0" "\<FF> U" "+\<^bsub>U\<^esub>" "\<cdot>\<^bsub>U\<^esub>" "\<zero>\<^bsub>U\<^esub>" "\<one>\<^bsub>U\<^esub>" "\<FF> w0" "+\<^bsub>w0\<^esub>"
                    "\<cdot>\<^bsub>w0\<^esub>" "\<zero>\<^bsub>w0\<^esub>" "\<one>\<^bsub>w0\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> U w0) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
using is_ring_morphism \<open>U\<in>I\<close> w0 subset_of_opens
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
U \<in> I
w0 \<in> I
w0 \<subseteq> U
w0 \<subseteq> fst x
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. ring_homomorphism (\<rho> U w0) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
interpret xw0:ring_homomorphism "\<rho> (fst x) w0" "\<FF> (fst x)" "+\<^bsub>fst x\<^esub>" "\<cdot>\<^bsub>fst x\<^esub>" "\<zero>\<^bsub>fst x\<^esub>"
                    "\<one>\<^bsub>fst x\<^esub>" "\<FF> w0" "+\<^bsub>w0\<^esub>" "\<cdot>\<^bsub>w0\<^esub>" "\<zero>\<^bsub>w0\<^esub>" "\<one>\<^bsub>w0\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst x) w0) (\<FF> (fst x)) +\<^bsub>fst x\<^esub> \<cdot>\<^bsub>fst x\<^esub> \<zero>\<^bsub>fst x\<^esub> \<one>\<^bsub>fst x\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
using is_ring_morphism \<open>fst x\<in>I\<close> w0 subset_of_opens
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
fst x \<in> I
w0 \<in> I
w0 \<subseteq> U
w0 \<subseteq> fst x
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst x) w0) (\<FF> (fst x)) +\<^bsub>fst x\<^esub> \<cdot>\<^bsub>fst x\<^esub> \<zero>\<^bsub>fst x\<^esub> \<one>\<^bsub>fst x\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> U w0 \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> U w0 \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
unfolding X_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<lfloor>fst x, snd x\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> U w0 \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
apply (subst add_rel_class_of)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. (U, \<zero>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>
 2. (fst x, snd x) \<in> Sigma I \<FF>
 3. ?W \<in> I
 4. ?W \<subseteq> U
 5. ?W \<subseteq> fst x
 6. \<lfloor>?W, +\<^bsub>?W\<^esub> (\<rho> U ?W \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) ?W (snd x))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> U w0 \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
using \<open>U \<in> I\<close> w0 x
[PROOF STATE]
proof (prove)
using this:
U \<in> I
w0 \<in> I
w0 \<subseteq> U
w0 \<subseteq> fst x
x \<in> X
x \<in> Sigma I \<FF>
fst x \<in> I

goal (6 subgoals):
 1. (U, \<zero>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>
 2. (fst x, snd x) \<in> Sigma I \<FF>
 3. ?W \<in> I
 4. ?W \<subseteq> U
 5. ?W \<subseteq> fst x
 6. \<lfloor>?W, +\<^bsub>?W\<^esub> (\<rho> U ?W \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) ?W (snd x))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> U w0 \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> U w0 \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>

goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> U w0 \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>

goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "... = \<lfloor>w0, +\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> U w0 \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
by (simp add:uw0.additive.commutes_with_unit )
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> U w0 \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor>

goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> U w0 \<zero>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor>

goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "... = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>
[PROOF STEP]
apply (subst uw0.target.additive.left_unit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>
[PROOF STEP]
using carrier_direct_lim_def rel.block_closed that x(1)
[PROOF STATE]
proof (prove)
using this:
carrier_direct_lim \<equiv> rel.Partition
\<lbrakk>?a \<in> ?A; ?A \<in> rel.Partition\<rbrakk> \<Longrightarrow> ?a \<in> Sigma I \<FF>
X \<in> carrier_direct_lim
x \<in> X

goal (2 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>

goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>

goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "... = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X
[PROOF STEP]
unfolding X_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = \<lfloor>fst x, snd x\<rfloor>
[PROOF STEP]
apply (rule class_of_eqI[where W=w0])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. (w0, \<rho> (fst x) w0 (snd x)) \<in> Sigma I \<FF>
 2. (fst x, snd x) \<in> Sigma I \<FF>
 3. w0 \<in> I
 4. w0 \<subseteq> w0 \<inter> fst x
 5. \<rho> w0 w0 (\<rho> (fst x) w0 (snd x)) = \<rho> (fst x) w0 (snd x)
[PROOF STEP]
using w0 x subset_of_opens
[PROOF STATE]
proof (prove)
using this:
w0 \<in> I
w0 \<subseteq> U
w0 \<subseteq> fst x
x \<in> X
x \<in> Sigma I \<FF>
fst x \<in> I
?U \<in> I \<Longrightarrow> is_open ?U

goal (5 subgoals):
 1. (w0, \<rho> (fst x) w0 (snd x)) \<in> Sigma I \<FF>
 2. (fst x, snd x) \<in> Sigma I \<FF>
 3. w0 \<in> I
 4. w0 \<subseteq> w0 \<inter> fst x
 5. \<rho> w0 w0 (\<rho> (fst x) w0 (snd x)) = \<rho> (fst x) w0 (snd x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X

goal (3 subgoals):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 3. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
[PROOF STEP]
show "add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X"
[PROOF STATE]
proof (prove)
using this:
add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X

goal (1 subgoal):
 1. add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X = X

goal (2 subgoals):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> U w0 \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> U w0 \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
unfolding X_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> \<lfloor>fst x, snd x\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> U w0 \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
apply (subst mult_rel_class_of)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. (U, \<one>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>
 2. (fst x, snd x) \<in> Sigma I \<FF>
 3. ?W \<in> I
 4. ?W \<subseteq> U
 5. ?W \<subseteq> fst x
 6. \<lfloor>?W, \<cdot>\<^bsub>?W\<^esub> (\<rho> U ?W \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) ?W (snd x))\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> U w0 \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
using \<open>U \<in> I\<close> w0 x
[PROOF STATE]
proof (prove)
using this:
U \<in> I
w0 \<in> I
w0 \<subseteq> U
w0 \<subseteq> fst x
x \<in> X
x \<in> Sigma I \<FF>
fst x \<in> I

goal (6 subgoals):
 1. (U, \<one>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>
 2. (fst x, snd x) \<in> Sigma I \<FF>
 3. ?W \<in> I
 4. ?W \<subseteq> U
 5. ?W \<subseteq> fst x
 6. \<lfloor>?W, \<cdot>\<^bsub>?W\<^esub> (\<rho> U ?W \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) ?W (snd x))\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> U w0 \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> U w0 \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>

goal (2 subgoals):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> U w0 \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor>

goal (2 subgoals):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "... = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> U w0 \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
by (simp add: uw0.multiplicative.commutes_with_unit)
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> U w0 \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor>

goal (2 subgoals):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> U w0 \<one>\<^bsub>U\<^esub>) (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor>

goal (2 subgoals):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "... = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>
[PROOF STEP]
apply (subst uw0.target.multiplicative.left_unit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>
[PROOF STEP]
using carrier_direct_lim_def rel.block_closed that x(1)
[PROOF STATE]
proof (prove)
using this:
carrier_direct_lim \<equiv> rel.Partition
\<lbrakk>?a \<in> ?A; ?A \<in> rel.Partition\<rbrakk> \<Longrightarrow> ?a \<in> Sigma I \<FF>
X \<in> carrier_direct_lim
x \<in> X

goal (2 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>

goal (2 subgoals):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>

goal (2 subgoals):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "... = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X
[PROOF STEP]
using X_alt \<open>\<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X\<close>
[PROOF STATE]
proof (prove)
using this:
X = \<lfloor>fst x, snd x\<rfloor>
\<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X

goal (1 subgoal):
 1. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X

goal (2 subgoals):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
 2. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
[PROOF STEP]
show "mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X"
[PROOF STATE]
proof (prove)
using this:
mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X

goal (1 subgoal):
 1. mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> X = X

goal (1 subgoal):
 1. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> U w0 \<one>\<^bsub>U\<^esub>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> U w0 \<one>\<^bsub>U\<^esub>)\<rfloor>
[PROOF STEP]
unfolding X_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel \<lfloor>fst x, snd x\<rfloor> \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> U w0 \<one>\<^bsub>U\<^esub>)\<rfloor>
[PROOF STEP]
apply (subst mult_rel_class_of)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. (fst x, snd x) \<in> Sigma I \<FF>
 2. (U, \<one>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>
 3. ?W \<in> I
 4. ?W \<subseteq> fst x
 5. ?W \<subseteq> U
 6. \<lfloor>?W, \<cdot>\<^bsub>?W\<^esub> (\<rho> (fst x) ?W (snd x)) (\<rho> U ?W \<one>\<^bsub>U\<^esub>)\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> U w0 \<one>\<^bsub>U\<^esub>)\<rfloor>
[PROOF STEP]
using \<open>U \<in> I\<close> w0 x
[PROOF STATE]
proof (prove)
using this:
U \<in> I
w0 \<in> I
w0 \<subseteq> U
w0 \<subseteq> fst x
x \<in> X
x \<in> Sigma I \<FF>
fst x \<in> I

goal (6 subgoals):
 1. (fst x, snd x) \<in> Sigma I \<FF>
 2. (U, \<one>\<^bsub>U\<^esub>) \<in> Sigma I \<FF>
 3. ?W \<in> I
 4. ?W \<subseteq> fst x
 5. ?W \<subseteq> U
 6. \<lfloor>?W, \<cdot>\<^bsub>?W\<^esub> (\<rho> (fst x) ?W (snd x)) (\<rho> U ?W \<one>\<^bsub>U\<^esub>)\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> U w0 \<one>\<^bsub>U\<^esub>)\<rfloor>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> U w0 \<one>\<^bsub>U\<^esub>)\<rfloor>

goal (1 subgoal):
 1. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> U w0 \<one>\<^bsub>U\<^esub>)\<rfloor>

goal (1 subgoal):
 1. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "... = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) \<one>\<^bsub>w0\<^esub> \<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> U w0 \<one>\<^bsub>U\<^esub>)\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) \<one>\<^bsub>w0\<^esub>\<rfloor>
[PROOF STEP]
by (simp add: uw0.multiplicative.commutes_with_unit)
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> U w0 \<one>\<^bsub>U\<^esub>)\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) \<one>\<^bsub>w0\<^esub>\<rfloor>

goal (1 subgoal):
 1. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> U w0 \<one>\<^bsub>U\<^esub>)\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) \<one>\<^bsub>w0\<^esub>\<rfloor>

goal (1 subgoal):
 1. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "... = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) \<one>\<^bsub>w0\<^esub>\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>
[PROOF STEP]
apply (subst uw0.target.multiplicative.right_unit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>
[PROOF STEP]
using carrier_direct_lim_def rel.block_closed that x(1)
[PROOF STATE]
proof (prove)
using this:
carrier_direct_lim \<equiv> rel.Partition
\<lbrakk>?a \<in> ?A; ?A \<in> rel.Partition\<rbrakk> \<Longrightarrow> ?a \<in> Sigma I \<FF>
X \<in> carrier_direct_lim
x \<in> X

goal (2 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) \<one>\<^bsub>w0\<^esub>\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>

goal (1 subgoal):
 1. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) \<one>\<^bsub>w0\<^esub>\<rfloor> = \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor>

goal (1 subgoal):
 1. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
have "... = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X
[PROOF STEP]
using X_alt \<open>\<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X\<close>
[PROOF STATE]
proof (prove)
using this:
X = \<lfloor>fst x, snd x\<rfloor>
\<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X

goal (1 subgoal):
 1. \<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<rho> (fst x) w0 (snd x)\<rfloor> = X

goal (1 subgoal):
 1. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
show "mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X"
[PROOF STATE]
proof (prove)
using this:
mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X

goal (1 subgoal):
 1. mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mult_rel X \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?X1 \<in> carrier_direct_lim \<Longrightarrow> add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> ?X1 = ?X1
?X1 \<in> carrier_direct_lim \<Longrightarrow> mult_rel \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> ?X1 = ?X1
?X1 \<in> carrier_direct_lim \<Longrightarrow> mult_rel ?X1 \<lfloor>U, \<one>\<^bsub>U\<^esub>\<rfloor> = ?X1

goal (7 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel (add_rel a b) c = add_rel a (add_rel b c)
 2. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel a \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = a
 3. \<And>u. u \<in> carrier_direct_lim \<Longrightarrow> monoid.invertible carrier_direct_lim add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> u
 4. \<And>x y. \<lbrakk>x \<in> carrier_direct_lim; y \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel x y = add_rel y x
 5. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel (mult_rel a b) c = mult_rel a (mult_rel b c)
 6. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel a (add_rel b c) = add_rel (mult_rel a b) (mult_rel a c)
 7. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel (add_rel b c) a = add_rel (mult_rel b a) (mult_rel c a)
[PROOF STEP]
show add_rel_commute: "add_rel X Y = add_rel Y X"
    if "X \<in> carrier_direct_lim" "Y \<in> carrier_direct_lim" for X Y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
define x where "x=(SOME x. x \<in> X)"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> X)

goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
define y where "y=(SOME y. y \<in> Y)"
[PROOF STATE]
proof (state)
this:
y = (SOME y. y \<in> Y)

goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
have x:"x\<in>X" "x\<in>Sigma I \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X &&& x \<in> Sigma I \<FF>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>X \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. x \<in> X &&& x \<in> Sigma I \<FF>
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. (SOME x. x \<in> X) \<in> X &&& (SOME x. x \<in> X) \<in> Sigma I \<FF>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X
x \<in> Sigma I \<FF>

goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
have y:"y\<in>Y" "y \<in> Sigma I \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> Y &&& y \<in> Sigma I \<FF>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>Y \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Y) \<in> Y
(SOME x. x \<in> Y) \<in> Sigma I \<FF>
Y = \<lfloor>fst (SOME x. x \<in> Y), snd (SOME x. x \<in> Y)\<rfloor>

goal (1 subgoal):
 1. y \<in> Y &&& y \<in> Sigma I \<FF>
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Y) \<in> Y
(SOME x. x \<in> Y) \<in> Sigma I \<FF>
Y = \<lfloor>fst (SOME x. x \<in> Y), snd (SOME x. x \<in> Y)\<rfloor>

goal (1 subgoal):
 1. (SOME y. y \<in> Y) \<in> Y &&& (SOME y. y \<in> Y) \<in> Sigma I \<FF>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> Y
y \<in> Sigma I \<FF>

goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
define z where "z=get_lower_bound (fst x) (fst y)"
[PROOF STATE]
proof (state)
this:
z = get_lower_bound (fst x) (fst y)

goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
have z:"z \<in> I" "z \<subseteq> fst x" "z \<subseteq> fst y" and z_alt:"z=get_lower_bound (fst y) (fst x) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<in> I &&& z \<subseteq> fst x &&& z \<subseteq> fst y) &&& z = get_lower_bound (fst y) (fst x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. z \<in> I
 2. z \<subseteq> fst x
 3. z \<subseteq> fst y
 4. z = get_lower_bound (fst y) (fst x)
[PROOF STEP]
have "fst x \<in> I" "fst y \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst x \<in> I &&& fst y \<in> I
[PROOF STEP]
using \<open>x \<in> Sigma I \<FF>\<close> \<open>y \<in> Sigma I \<FF>\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>
y \<in> Sigma I \<FF>

goal (1 subgoal):
 1. fst x \<in> I &&& fst y \<in> I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst x \<in> I
fst y \<in> I

goal (4 subgoals):
 1. z \<in> I
 2. z \<subseteq> fst x
 3. z \<subseteq> fst y
 4. z = get_lower_bound (fst y) (fst x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst x \<in> I
fst y \<in> I
[PROOF STEP]
show "z \<in> I" "z \<subseteq> fst x" "z \<subseteq> fst y"
[PROOF STATE]
proof (prove)
using this:
fst x \<in> I
fst y \<in> I

goal (1 subgoal):
 1. z \<in> I &&& z \<subseteq> fst x &&& z \<subseteq> fst y
[PROOF STEP]
using get_lower_bound[of "fst x" "fst y",folded z_def]
[PROOF STATE]
proof (prove)
using this:
fst x \<in> I
fst y \<in> I
\<lbrakk>fst x \<in> I; fst y \<in> I\<rbrakk> \<Longrightarrow> z \<in> I
\<lbrakk>fst x \<in> I; fst y \<in> I\<rbrakk> \<Longrightarrow> z \<subseteq> fst x
\<lbrakk>fst x \<in> I; fst y \<in> I\<rbrakk> \<Longrightarrow> z \<subseteq> fst y

goal (1 subgoal):
 1. z \<in> I &&& z \<subseteq> fst x &&& z \<subseteq> fst y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> I
z \<subseteq> fst x
z \<subseteq> fst y

goal (1 subgoal):
 1. z = get_lower_bound (fst y) (fst x)
[PROOF STEP]
show "z=get_lower_bound (fst y) (fst x) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = get_lower_bound (fst y) (fst x)
[PROOF STEP]
by (metis (no_types, lifting) Eps_cong get_lower_bound_def z_def)
[PROOF STATE]
proof (state)
this:
z = get_lower_bound (fst y) (fst x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> I
z \<subseteq> fst x
z \<subseteq> fst y
z = get_lower_bound (fst y) (fst x)

goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
interpret xz:ring_homomorphism "(\<rho> (fst x) z)" "(\<FF> (fst x))" "+\<^bsub>fst x\<^esub>" "\<cdot>\<^bsub>fst x\<^esub>"
                      "\<zero>\<^bsub>fst x\<^esub>" "\<one>\<^bsub>fst x\<^esub>" "(\<FF> z)" "+\<^bsub>z\<^esub>" "\<cdot>\<^bsub>z\<^esub>" "\<zero>\<^bsub>z\<^esub>" "\<one>\<^bsub>z\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst x) z) (\<FF> (fst x)) +\<^bsub>fst x\<^esub> \<cdot>\<^bsub>fst x\<^esub> \<zero>\<^bsub>fst x\<^esub> \<one>\<^bsub>fst x\<^esub> (\<FF> z) +\<^bsub>z\<^esub> \<cdot>\<^bsub>z\<^esub> \<zero>\<^bsub>z\<^esub> \<one>\<^bsub>z\<^esub>
[PROOF STEP]
using is_ring_morphism z x subset_of_opens
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
z \<in> I
z \<subseteq> fst x
z \<subseteq> fst y
x \<in> X
x \<in> Sigma I \<FF>
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst x) z) (\<FF> (fst x)) +\<^bsub>fst x\<^esub> \<cdot>\<^bsub>fst x\<^esub> \<zero>\<^bsub>fst x\<^esub> \<one>\<^bsub>fst x\<^esub> (\<FF> z) +\<^bsub>z\<^esub> \<cdot>\<^bsub>z\<^esub> \<zero>\<^bsub>z\<^esub> \<one>\<^bsub>z\<^esub>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
interpret yz:ring_homomorphism "(\<rho> (fst y) z)" "(\<FF> (fst y))" "+\<^bsub>fst y\<^esub>" "\<cdot>\<^bsub>fst y\<^esub>"
                      "\<zero>\<^bsub>fst y\<^esub>" "\<one>\<^bsub>fst y\<^esub>" "(\<FF> z)" "+\<^bsub>z\<^esub>" "\<cdot>\<^bsub>z\<^esub>" "\<zero>\<^bsub>z\<^esub>" "\<one>\<^bsub>z\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst y) z) (\<FF> (fst y)) +\<^bsub>fst y\<^esub> \<cdot>\<^bsub>fst y\<^esub> \<zero>\<^bsub>fst y\<^esub> \<one>\<^bsub>fst y\<^esub> (\<FF> z) +\<^bsub>z\<^esub> \<cdot>\<^bsub>z\<^esub> \<zero>\<^bsub>z\<^esub> \<one>\<^bsub>z\<^esub>
[PROOF STEP]
using is_ring_morphism z y subset_of_opens
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
z \<in> I
z \<subseteq> fst x
z \<subseteq> fst y
y \<in> Y
y \<in> Sigma I \<FF>
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst y) z) (\<FF> (fst y)) +\<^bsub>fst y\<^esub> \<cdot>\<^bsub>fst y\<^esub> \<zero>\<^bsub>fst y\<^esub> \<one>\<^bsub>fst y\<^esub> (\<FF> z) +\<^bsub>z\<^esub> \<cdot>\<^bsub>z\<^esub> \<zero>\<^bsub>z\<^esub> \<one>\<^bsub>z\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
have "add_rel X Y = \<lfloor>z, add_str z (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel X Y = \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>
[PROOF STEP]
unfolding add_rel_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y)), +\<^bsub>get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y))\<^esub> (\<rho> (fst (SOME x. x \<in> X)) (get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y))) (snd (SOME x. x \<in> X))) (\<rho> (fst (SOME y. y \<in> Y)) (get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y))) (snd (SOME y. y \<in> Y)))\<rfloor> = \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>
[PROOF STEP]
by (fold x_def y_def z_def,rule)
[PROOF STATE]
proof (state)
this:
add_rel X Y = \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>

goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
add_rel X Y = \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>

goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
have "... = add_rel Y X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = add_rel Y X
[PROOF STEP]
unfolding add_rel_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>get_lower_bound (fst (SOME x. x \<in> Y)) (fst (SOME y. y \<in> X)), +\<^bsub>get_lower_bound (fst (SOME x. x \<in> Y)) (fst (SOME y. y \<in> X))\<^esub> (\<rho> (fst (SOME x. x \<in> Y)) (get_lower_bound (fst (SOME x. x \<in> Y)) (fst (SOME y. y \<in> X))) (snd (SOME x. x \<in> Y))) (\<rho> (fst (SOME y. y \<in> X)) (get_lower_bound (fst (SOME x. x \<in> Y)) (fst (SOME y. y \<in> X))) (snd (SOME y. y \<in> X)))\<rfloor>
[PROOF STEP]
apply (fold x_def y_def z_alt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst y) z (snd y)) (\<rho> (fst x) z (snd x))\<rfloor>
[PROOF STEP]
using \<open>x \<in> Sigma I \<FF>\<close> \<open>y \<in> Sigma I \<FF>\<close> xz.target.additive.commutative
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>
y \<in> Sigma I \<FF>
\<lbrakk>?x \<in> \<FF> z; ?y \<in> \<FF> z\<rbrakk> \<Longrightarrow> +\<^bsub>z\<^esub> ?x ?y = +\<^bsub>z\<^esub> ?y ?x

goal (1 subgoal):
 1. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst y) z (snd y)) (\<rho> (fst x) z (snd x))\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = add_rel Y X

goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
add_rel X Y = add_rel Y X
[PROOF STEP]
show "add_rel X Y = add_rel Y X"
[PROOF STATE]
proof (prove)
using this:
add_rel X Y = add_rel Y X

goal (1 subgoal):
 1. add_rel X Y = add_rel Y X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
add_rel X Y = add_rel Y X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?X1 \<in> carrier_direct_lim; ?Y1 \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel ?X1 ?Y1 = add_rel ?Y1 ?X1

goal (6 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel (add_rel a b) c = add_rel a (add_rel b c)
 2. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel a \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = a
 3. \<And>u. u \<in> carrier_direct_lim \<Longrightarrow> monoid.invertible carrier_direct_lim add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> u
 4. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel (mult_rel a b) c = mult_rel a (mult_rel b c)
 5. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel a (add_rel b c) = add_rel (mult_rel a b) (mult_rel a c)
 6. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel (add_rel b c) a = add_rel (mult_rel b a) (mult_rel c a)
[PROOF STEP]
show add_assoc:"add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)"
       "mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)"
       "mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)"
       "mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)"
    if "X \<in> carrier_direct_lim" "Y \<in> carrier_direct_lim" "Z \<in> carrier_direct_lim" for X Y Z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z) &&& mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)) &&& mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z) &&& mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
define x where "x=(SOME x. x \<in> X)"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> X)

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
define y where "y=(SOME y. y \<in> Y)"
[PROOF STATE]
proof (state)
this:
y = (SOME y. y \<in> Y)

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
define z where "z=(SOME z. z \<in> Z)"
[PROOF STATE]
proof (state)
this:
z = (SOME z. z \<in> Z)

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have x:"x\<in>X" "x\<in>Sigma I \<FF>" and x_alt:"X = \<lfloor>fst x,snd x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> X &&& x \<in> Sigma I \<FF>) &&& X = \<lfloor>fst x, snd x\<rfloor>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>X \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. (x \<in> X &&& x \<in> Sigma I \<FF>) &&& X = \<lfloor>fst x, snd x\<rfloor>
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. ((SOME x. x \<in> X) \<in> X &&& (SOME x. x \<in> X) \<in> Sigma I \<FF>) &&& X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X
x \<in> Sigma I \<FF>
X = \<lfloor>fst x, snd x\<rfloor>

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have y:"y\<in>Y" "y \<in> Sigma I \<FF>" and y_alt:"Y = \<lfloor>fst y,snd y\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y \<in> Y &&& y \<in> Sigma I \<FF>) &&& Y = \<lfloor>fst y, snd y\<rfloor>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>Y \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Y) \<in> Y
(SOME x. x \<in> Y) \<in> Sigma I \<FF>
Y = \<lfloor>fst (SOME x. x \<in> Y), snd (SOME x. x \<in> Y)\<rfloor>

goal (1 subgoal):
 1. (y \<in> Y &&& y \<in> Sigma I \<FF>) &&& Y = \<lfloor>fst y, snd y\<rfloor>
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Y) \<in> Y
(SOME x. x \<in> Y) \<in> Sigma I \<FF>
Y = \<lfloor>fst (SOME x. x \<in> Y), snd (SOME x. x \<in> Y)\<rfloor>

goal (1 subgoal):
 1. ((SOME y. y \<in> Y) \<in> Y &&& (SOME y. y \<in> Y) \<in> Sigma I \<FF>) &&& Y = \<lfloor>fst (SOME y. y \<in> Y), snd (SOME y. y \<in> Y)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> Y
y \<in> Sigma I \<FF>
Y = \<lfloor>fst y, snd y\<rfloor>

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have z:"z\<in>Z" "z \<in> Sigma I \<FF>" and z_alt:"Z = \<lfloor>fst z,snd z\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<in> Z &&& z \<in> Sigma I \<FF>) &&& Z = \<lfloor>fst z, snd z\<rfloor>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>Z \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Z) \<in> Z
(SOME x. x \<in> Z) \<in> Sigma I \<FF>
Z = \<lfloor>fst (SOME x. x \<in> Z), snd (SOME x. x \<in> Z)\<rfloor>

goal (1 subgoal):
 1. (z \<in> Z &&& z \<in> Sigma I \<FF>) &&& Z = \<lfloor>fst z, snd z\<rfloor>
[PROOF STEP]
unfolding z_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Z) \<in> Z
(SOME x. x \<in> Z) \<in> Sigma I \<FF>
Z = \<lfloor>fst (SOME x. x \<in> Z), snd (SOME x. x \<in> Z)\<rfloor>

goal (1 subgoal):
 1. ((SOME z. z \<in> Z) \<in> Z &&& (SOME z. z \<in> Z) \<in> Sigma I \<FF>) &&& Z = \<lfloor>fst (SOME z. z \<in> Z), snd (SOME z. z \<in> Z)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> Z
z \<in> Sigma I \<FF>
Z = \<lfloor>fst z, snd z\<rfloor>

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
obtain w0 where w0:"w0 \<in> I" "w0 \<subseteq> fst x" "w0 \<subseteq> fst y" "w0 \<subseteq> fst z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; w0 \<subseteq> fst x; w0 \<subseteq> fst y; w0 \<subseteq> fst z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_lower_bound_finite[of "{fst x,fst y,fst z}"] x y z
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {fst x, fst y, fst z}; {fst x, fst y, fst z} \<noteq> {}; {fst x, fst y, fst z} \<subseteq> I; \<And>W. \<lbrakk>W \<in> I; \<forall>U\<in>{fst x, fst y, fst z}. W \<subseteq> U\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>

goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; w0 \<subseteq> fst x; w0 \<subseteq> fst y; w0 \<subseteq> fst z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
interpret xw0:ring_homomorphism "\<rho> (fst x) w0" "\<FF> (fst x)" "+\<^bsub>fst x\<^esub>" "\<cdot>\<^bsub>fst x\<^esub>" "\<zero>\<^bsub>fst x\<^esub>"
                    "\<one>\<^bsub>fst x\<^esub>" "\<FF> w0" "+\<^bsub>w0\<^esub>" "\<cdot>\<^bsub>w0\<^esub>" "\<zero>\<^bsub>w0\<^esub>" "\<one>\<^bsub>w0\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst x) w0) (\<FF> (fst x)) +\<^bsub>fst x\<^esub> \<cdot>\<^bsub>fst x\<^esub> \<zero>\<^bsub>fst x\<^esub> \<one>\<^bsub>fst x\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
using is_ring_morphism x w0 subset_of_opens
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
x \<in> X
x \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst x) w0) (\<FF> (fst x)) +\<^bsub>fst x\<^esub> \<cdot>\<^bsub>fst x\<^esub> \<zero>\<^bsub>fst x\<^esub> \<one>\<^bsub>fst x\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
interpret yw0:ring_homomorphism "\<rho> (fst y) w0" "\<FF> (fst y)" "+\<^bsub>fst y\<^esub>" "\<cdot>\<^bsub>fst y\<^esub>" "\<zero>\<^bsub>fst y\<^esub>"
                    "\<one>\<^bsub>fst y\<^esub>" "\<FF> w0" "+\<^bsub>w0\<^esub>" "\<cdot>\<^bsub>w0\<^esub>" "\<zero>\<^bsub>w0\<^esub>" "\<one>\<^bsub>w0\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst y) w0) (\<FF> (fst y)) +\<^bsub>fst y\<^esub> \<cdot>\<^bsub>fst y\<^esub> \<zero>\<^bsub>fst y\<^esub> \<one>\<^bsub>fst y\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
using is_ring_morphism y w0 subset_of_opens
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
y \<in> Y
y \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst y) w0) (\<FF> (fst y)) +\<^bsub>fst y\<^esub> \<cdot>\<^bsub>fst y\<^esub> \<zero>\<^bsub>fst y\<^esub> \<one>\<^bsub>fst y\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
interpret zw0:ring_homomorphism "\<rho> (fst z) w0" "\<FF> (fst z)" "+\<^bsub>fst z\<^esub>" "\<cdot>\<^bsub>fst z\<^esub>" "\<zero>\<^bsub>fst z\<^esub>"
                    "\<one>\<^bsub>fst z\<^esub>" "\<FF> w0" "+\<^bsub>w0\<^esub>" "\<cdot>\<^bsub>w0\<^esub>" "\<zero>\<^bsub>w0\<^esub>" "\<one>\<^bsub>w0\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst z) w0) (\<FF> (fst z)) +\<^bsub>fst z\<^esub> \<cdot>\<^bsub>fst z\<^esub> \<zero>\<^bsub>fst z\<^esub> \<one>\<^bsub>fst z\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
using is_ring_morphism z w0 subset_of_opens
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
z \<in> Z
z \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst z) w0) (\<FF> (fst z)) +\<^bsub>fst z\<^esub> \<cdot>\<^bsub>fst z\<^esub> \<zero>\<^bsub>fst z\<^esub> \<one>\<^bsub>fst z\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "add_rel (add_rel X Y) Z = \<lfloor>w0, +\<^bsub>w0\<^esub> ((+\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))
                                (\<rho> (fst y) w0 (snd y)))) (\<rho> (fst z) w0 (snd z))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel (add_rel X Y) Z = \<lfloor>w0, +\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor>
[PROOF STEP]
unfolding x_alt y_alt z_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel (add_rel \<lfloor>fst x, snd x\<rfloor> \<lfloor>fst y, snd y\<rfloor>) \<lfloor>fst z, snd z\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor>
[PROOF STEP]
using x y z w0 subset_of_opens add_rel_class_of
[PROOF STATE]
proof (prove)
using this:
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
?U \<in> I \<Longrightarrow> is_open ?U
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> add_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, +\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>

goal (1 subgoal):
 1. add_rel (add_rel \<lfloor>fst x, snd x\<rfloor> \<lfloor>fst y, snd y\<rfloor>) \<lfloor>fst z, snd z\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor>
[PROOF STEP]
by (force simp add: add_rel_class_of)
[PROOF STATE]
proof (state)
this:
add_rel (add_rel X Y) Z = \<lfloor>w0, +\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor>

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
add_rel (add_rel X Y) Z = \<lfloor>w0, +\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor>

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "... = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))
                              (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
using x(2) xw0.target.additive.associative y(2) z(2)
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>
\<lbrakk>?a \<in> \<FF> w0; ?b \<in> \<FF> w0; ?c \<in> \<FF> w0\<rbrakk> \<Longrightarrow> +\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> ?a ?b) ?c = +\<^bsub>w0\<^esub> ?a (+\<^bsub>w0\<^esub> ?b ?c)
y \<in> Sigma I \<FF>
z \<in> Sigma I \<FF>

goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "... =  add_rel X (add_rel Y Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = add_rel X (add_rel Y Z)
[PROOF STEP]
unfolding x_alt y_alt z_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = add_rel \<lfloor>fst x, snd x\<rfloor> (add_rel \<lfloor>fst y, snd y\<rfloor> \<lfloor>fst z, snd z\<rfloor>)
[PROOF STEP]
using x y z w0 add_rel_class_of subset_of_opens
[PROOF STATE]
proof (prove)
using this:
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> add_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, +\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = add_rel \<lfloor>fst x, snd x\<rfloor> (add_rel \<lfloor>fst y, snd y\<rfloor> \<lfloor>fst z, snd z\<rfloor>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = add_rel X (add_rel Y Z)

goal (4 subgoals):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
 2. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 3. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 4. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
[PROOF STEP]
show "add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)"
[PROOF STATE]
proof (prove)
using this:
add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)

goal (1 subgoal):
 1. add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
add_rel (add_rel X Y) Z = add_rel X (add_rel Y Z)

goal (3 subgoals):
 1. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 2. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 3. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "mult_rel (mult_rel X Y) Z = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> ((\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))
                                (\<rho> (fst y) w0 (snd y)))) (\<rho> (fst z) w0 (snd z))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel (mult_rel X Y) Z = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor>
[PROOF STEP]
unfolding x_alt y_alt z_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel (mult_rel \<lfloor>fst x, snd x\<rfloor> \<lfloor>fst y, snd y\<rfloor>) \<lfloor>fst z, snd z\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor>
[PROOF STEP]
using x y z w0 mult_rel_class_of subset_of_opens
[PROOF STATE]
proof (prove)
using this:
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> mult_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, \<cdot>\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. mult_rel (mult_rel \<lfloor>fst x, snd x\<rfloor> \<lfloor>fst y, snd y\<rfloor>) \<lfloor>fst z, snd z\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
mult_rel (mult_rel X Y) Z = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor>

goal (3 subgoals):
 1. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 2. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 3. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mult_rel (mult_rel X Y) Z = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor>

goal (3 subgoals):
 1. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 2. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 3. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "... = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))
                              (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
apply (subst xw0.target.multiplicative.associative)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<rho> (fst y) w0 (snd y) \<in> \<FF> w0
 3. \<rho> (fst z) w0 (snd z) \<in> \<FF> w0
 4. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
using w0 x y z
[PROOF STATE]
proof (prove)
using this:
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>

goal (4 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<rho> (fst y) w0 (snd y) \<in> \<FF> w0
 3. \<rho> (fst z) w0 (snd z) \<in> \<FF> w0
 4. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>

goal (3 subgoals):
 1. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 2. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 3. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<rho> (fst z) w0 (snd z))\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>

goal (3 subgoals):
 1. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 2. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 3. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "... =  mult_rel X (mult_rel Y Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = mult_rel X (mult_rel Y Z)
[PROOF STEP]
unfolding x_alt y_alt z_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = mult_rel \<lfloor>fst x, snd x\<rfloor> (mult_rel \<lfloor>fst y, snd y\<rfloor> \<lfloor>fst z, snd z\<rfloor>)
[PROOF STEP]
using x y z w0 mult_rel_class_of subset_of_opens
[PROOF STATE]
proof (prove)
using this:
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> mult_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, \<cdot>\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = mult_rel \<lfloor>fst x, snd x\<rfloor> (mult_rel \<lfloor>fst y, snd y\<rfloor> \<lfloor>fst z, snd z\<rfloor>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = mult_rel X (mult_rel Y Z)

goal (3 subgoals):
 1. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
 2. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 3. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
[PROOF STEP]
show "mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)"
[PROOF STATE]
proof (prove)
using this:
mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)

goal (1 subgoal):
 1. mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mult_rel (mult_rel X Y) Z = mult_rel X (mult_rel Y Z)

goal (2 subgoals):
 1. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 2. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "mult_rel X (add_rel Y Z) = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))
                  (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel X (add_rel Y Z) = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
unfolding x_alt y_alt z_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel \<lfloor>fst x, snd x\<rfloor> (add_rel \<lfloor>fst y, snd y\<rfloor> \<lfloor>fst z, snd z\<rfloor>) = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
using x y z w0 add_rel_class_of mult_rel_class_of subset_of_opens
[PROOF STATE]
proof (prove)
using this:
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> add_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, +\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> mult_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, \<cdot>\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. mult_rel \<lfloor>fst x, snd x\<rfloor> (add_rel \<lfloor>fst y, snd y\<rfloor> \<lfloor>fst z, snd z\<rfloor>) = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
mult_rel X (add_rel Y Z) = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>

goal (2 subgoals):
 1. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 2. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mult_rel X (add_rel Y Z) = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor>

goal (2 subgoals):
 1. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 2. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "... = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y)))
            (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
apply (subst xw0.target.distributive)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<rho> (fst y) w0 (snd y) \<in> \<FF> w0
 3. \<rho> (fst z) w0 (snd z) \<in> \<FF> w0
 4. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
using w0 x y z
[PROOF STATE]
proof (prove)
using this:
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>

goal (4 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<rho> (fst y) w0 (snd y) \<in> \<FF> w0
 3. \<rho> (fst z) w0 (snd z) \<in> \<FF> w0
 4. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor>

goal (2 subgoals):
 1. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 2. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor>

goal (2 subgoals):
 1. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 2. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "... = add_rel (mult_rel X Y) (mult_rel X Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = add_rel (mult_rel X Y) (mult_rel X Z)
[PROOF STEP]
unfolding x_alt y_alt z_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = add_rel (mult_rel \<lfloor>fst x, snd x\<rfloor> \<lfloor>fst y, snd y\<rfloor>) (mult_rel \<lfloor>fst x, snd x\<rfloor> \<lfloor>fst z, snd z\<rfloor>)
[PROOF STEP]
using x y z w0 add_rel_class_of mult_rel_class_of subset_of_opens
[PROOF STATE]
proof (prove)
using this:
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> add_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, +\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> mult_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, \<cdot>\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = add_rel (mult_rel \<lfloor>fst x, snd x\<rfloor> \<lfloor>fst y, snd y\<rfloor>) (mult_rel \<lfloor>fst x, snd x\<rfloor> \<lfloor>fst z, snd z\<rfloor>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst y) w0 (snd y))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst z) w0 (snd z)))\<rfloor> = add_rel (mult_rel X Y) (mult_rel X Z)

goal (2 subgoals):
 1. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
 2. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
[PROOF STEP]
show "mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)"
[PROOF STATE]
proof (prove)
using this:
mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)

goal (1 subgoal):
 1. mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mult_rel X (add_rel Y Z) = add_rel (mult_rel X Y) (mult_rel X Z)

goal (1 subgoal):
 1. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "mult_rel (add_rel Y Z) X = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y))
                                          (\<rho> (fst z) w0 (snd z))) (\<rho> (fst x) w0 (snd x))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel (add_rel Y Z) X = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z))) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
unfolding x_alt y_alt z_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel (add_rel \<lfloor>fst y, snd y\<rfloor> \<lfloor>fst z, snd z\<rfloor>) \<lfloor>fst x, snd x\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z))) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
using x y z w0 add_rel_class_of mult_rel_class_of subset_of_opens
[PROOF STATE]
proof (prove)
using this:
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> add_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, +\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> mult_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, \<cdot>\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. mult_rel (add_rel \<lfloor>fst y, snd y\<rfloor> \<lfloor>fst z, snd z\<rfloor>) \<lfloor>fst x, snd x\<rfloor> = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z))) (\<rho> (fst x) w0 (snd x))\<rfloor>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
mult_rel (add_rel Y Z) X = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z))) (\<rho> (fst x) w0 (snd x))\<rfloor>

goal (1 subgoal):
 1. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mult_rel (add_rel Y Z) X = \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z))) (\<rho> (fst x) w0 (snd x))\<rfloor>

goal (1 subgoal):
 1. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "... = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x)))
            (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z))) (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor>
[PROOF STEP]
apply (subst xw0.target.distributive)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<rho> (fst y) w0 (snd y) \<in> \<FF> w0
 3. \<rho> (fst z) w0 (snd z) \<in> \<FF> w0
 4. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor>
[PROOF STEP]
using w0 x y z
[PROOF STATE]
proof (prove)
using this:
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>

goal (4 subgoals):
 1. \<rho> (fst x) w0 (snd x) \<in> \<FF> w0
 2. \<rho> (fst y) w0 (snd y) \<in> \<FF> w0
 3. \<rho> (fst z) w0 (snd z) \<in> \<FF> w0
 4. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z))) (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor>

goal (1 subgoal):
 1. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<cdot>\<^bsub>w0\<^esub> (+\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst z) w0 (snd z))) (\<rho> (fst x) w0 (snd x))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor>

goal (1 subgoal):
 1. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
have "... = add_rel (mult_rel Y X) (mult_rel Z X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor> = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
unfolding x_alt y_alt z_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor> = add_rel (mult_rel \<lfloor>fst y, snd y\<rfloor> \<lfloor>fst x, snd x\<rfloor>) (mult_rel \<lfloor>fst z, snd z\<rfloor> \<lfloor>fst x, snd x\<rfloor>)
[PROOF STEP]
using x y z w0 add_rel_class_of mult_rel_class_of subset_of_opens
[PROOF STATE]
proof (prove)
using this:
x \<in> X
x \<in> Sigma I \<FF>
y \<in> Y
y \<in> Sigma I \<FF>
z \<in> Z
z \<in> Sigma I \<FF>
w0 \<in> I
w0 \<subseteq> fst x
w0 \<subseteq> fst y
w0 \<subseteq> fst z
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> add_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, +\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
\<lbrakk>(?U, ?x) \<in> Sigma I \<FF>; (?V, ?y) \<in> Sigma I \<FF>; ?W \<in> I; ?W \<subseteq> ?U; ?W \<subseteq> ?V\<rbrakk> \<Longrightarrow> mult_rel \<lfloor>?U, ?x\<rfloor> \<lfloor>?V, ?y\<rfloor> = \<lfloor>?W, \<cdot>\<^bsub>?W\<^esub> (\<rho> ?U ?W ?x) (\<rho> ?V ?W ?y)\<rfloor>
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor> = add_rel (mult_rel \<lfloor>fst y, snd y\<rfloor> \<lfloor>fst x, snd x\<rfloor>) (mult_rel \<lfloor>fst z, snd z\<rfloor> \<lfloor>fst x, snd x\<rfloor>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst y) w0 (snd y)) (\<rho> (fst x) w0 (snd x))) (\<cdot>\<^bsub>w0\<^esub> (\<rho> (fst z) w0 (snd z)) (\<rho> (fst x) w0 (snd x)))\<rfloor> = add_rel (mult_rel Y X) (mult_rel Z X)

goal (1 subgoal):
 1. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
show "mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)"
[PROOF STATE]
proof (prove)
using this:
mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)

goal (1 subgoal):
 1. mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mult_rel (add_rel Y Z) X = add_rel (mult_rel Y X) (mult_rel Z X)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?X1 \<in> carrier_direct_lim; ?Y1 \<in> carrier_direct_lim; ?Z1 \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel (add_rel ?X1 ?Y1) ?Z1 = add_rel ?X1 (add_rel ?Y1 ?Z1)
\<lbrakk>?X1 \<in> carrier_direct_lim; ?Y1 \<in> carrier_direct_lim; ?Z1 \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel (mult_rel ?X1 ?Y1) ?Z1 = mult_rel ?X1 (mult_rel ?Y1 ?Z1)
\<lbrakk>?X1 \<in> carrier_direct_lim; ?Y1 \<in> carrier_direct_lim; ?Z1 \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel ?X1 (add_rel ?Y1 ?Z1) = add_rel (mult_rel ?X1 ?Y1) (mult_rel ?X1 ?Z1)
\<lbrakk>?X1 \<in> carrier_direct_lim; ?Y1 \<in> carrier_direct_lim; ?Z1 \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> mult_rel (add_rel ?Y1 ?Z1) ?X1 = add_rel (mult_rel ?Y1 ?X1) (mult_rel ?Z1 ?X1)

goal (2 subgoals):
 1. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel a \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = a
 2. \<And>u. u \<in> carrier_direct_lim \<Longrightarrow> monoid.invertible carrier_direct_lim add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> u
[PROOF STEP]
show add_rel_0':"\<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel a \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel a \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = a
[PROOF STEP]
using add_rel_0 add_rel_commute zero_rel
[PROOF STATE]
proof (prove)
using this:
?X1 \<in> carrier_direct_lim \<Longrightarrow> add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> ?X1 = ?X1
\<lbrakk>?X1 \<in> carrier_direct_lim; ?Y1 \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel ?X1 ?Y1 = add_rel ?Y1 ?X1
\<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim

goal (1 subgoal):
 1. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel a \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = a
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?a1 \<in> carrier_direct_lim \<Longrightarrow> add_rel ?a1 \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = ?a1

goal (1 subgoal):
 1. \<And>u. u \<in> carrier_direct_lim \<Longrightarrow> monoid.invertible carrier_direct_lim add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> u
[PROOF STEP]
interpret Group_Theory.monoid carrier_direct_lim add_rel "\<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid carrier_direct_lim add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel a b \<in> carrier_direct_lim
 2. \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<in> carrier_direct_lim
 3. \<And>a b c. \<lbrakk>a \<in> carrier_direct_lim; b \<in> carrier_direct_lim; c \<in> carrier_direct_lim\<rbrakk> \<Longrightarrow> add_rel (add_rel a b) c = add_rel a (add_rel b c)
 4. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> a = a
 5. \<And>a. a \<in> carrier_direct_lim \<Longrightarrow> add_rel a \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> = a
[PROOF STEP]
by (simp_all add: zero_rel add_rel_carrier add_assoc add_rel_0 add_rel_0')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> carrier_direct_lim \<Longrightarrow> invertible u
[PROOF STEP]
show "monoid.invertible carrier_direct_lim add_rel \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> X"
    if "X \<in> carrier_direct_lim" for X
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invertible X
[PROOF STEP]
define x where "x=(SOME x. x \<in> X)"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> X)

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
have x:"x\<in>X" "x\<in>Sigma I \<FF>" "fst x\<in>I" and X_alt:"X= \<lfloor>fst x, snd x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> X &&& x \<in> Sigma I \<FF> &&& fst x \<in> I) &&& X = \<lfloor>fst x, snd x\<rfloor>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>X \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. (x \<in> X &&& x \<in> Sigma I \<FF> &&& fst x \<in> I) &&& X = \<lfloor>fst x, snd x\<rfloor>
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. ((SOME x. x \<in> X) \<in> X &&& (SOME x. x \<in> X) \<in> Sigma I \<FF> &&& fst (SOME x. x \<in> X) \<in> I) &&& X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X
x \<in> Sigma I \<FF>
fst x \<in> I
X = \<lfloor>fst x, snd x\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
obtain w0 where w0: "w0 \<in> I" "w0 \<subseteq> U" "w0 \<subseteq> fst x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; w0 \<subseteq> U; w0 \<subseteq> fst x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using has_lower_bound[OF \<open>U\<in>I\<close> \<open>fst x\<in>I\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>W\<in>I. W \<subseteq> U \<inter> fst x

goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; w0 \<subseteq> U; w0 \<subseteq> fst x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w0 \<in> I
w0 \<subseteq> U
w0 \<subseteq> fst x

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
interpret uw0:ring_homomorphism "\<rho> U w0" "\<FF> U" "+\<^bsub>U\<^esub>" "\<cdot>\<^bsub>U\<^esub>" "\<zero>\<^bsub>U\<^esub>" "\<one>\<^bsub>U\<^esub>" "\<FF> w0" "+\<^bsub>w0\<^esub>"
                    "\<cdot>\<^bsub>w0\<^esub>" "\<zero>\<^bsub>w0\<^esub>" "\<one>\<^bsub>w0\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> U w0) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
using is_ring_morphism \<open>U\<in>I\<close> w0 subset_of_opens
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
U \<in> I
w0 \<in> I
w0 \<subseteq> U
w0 \<subseteq> fst x
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. ring_homomorphism (\<rho> U w0) (\<FF> U) +\<^bsub>U\<^esub> \<cdot>\<^bsub>U\<^esub> \<zero>\<^bsub>U\<^esub> \<one>\<^bsub>U\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invertible X
[PROOF STEP]
interpret xw0:ring_homomorphism "\<rho> (fst x) w0" "\<FF> (fst x)" "+\<^bsub>fst x\<^esub>" "\<cdot>\<^bsub>fst x\<^esub>" "\<zero>\<^bsub>fst x\<^esub>"
                    "\<one>\<^bsub>fst x\<^esub>" "\<FF> w0" "+\<^bsub>w0\<^esub>" "\<cdot>\<^bsub>w0\<^esub>" "\<zero>\<^bsub>w0\<^esub>" "\<one>\<^bsub>w0\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst x) w0) (\<FF> (fst x)) +\<^bsub>fst x\<^esub> \<cdot>\<^bsub>fst x\<^esub> \<zero>\<^bsub>fst x\<^esub> \<one>\<^bsub>fst x\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
using is_ring_morphism \<open>fst x\<in>I\<close> w0 subset_of_opens
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
fst x \<in> I
w0 \<in> I
w0 \<subseteq> U
w0 \<subseteq> fst x
?U \<in> I \<Longrightarrow> is_open ?U

goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst x) w0) (\<FF> (fst x)) +\<^bsub>fst x\<^esub> \<cdot>\<^bsub>fst x\<^esub> \<zero>\<^bsub>fst x\<^esub> \<one>\<^bsub>fst x\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invertible X
[PROOF STEP]
define Y where "Y=\<lfloor>fst x, xw0.source.additive.inverse (snd x)\<rfloor>"
[PROOF STATE]
proof (state)
this:
Y = \<lfloor>fst x, xw0.source.additive.inverse (snd x)\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
have "add_rel X Y  = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x))
                                  (\<rho> (fst x) w0 (xw0.source.additive.inverse (snd x)))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel X Y = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst x) w0 (xw0.source.additive.inverse (snd x)))\<rfloor>
[PROOF STEP]
unfolding X_alt Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel \<lfloor>fst x, snd x\<rfloor> \<lfloor>fst x, xw0.source.additive.inverse (snd x)\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst x) w0 (xw0.source.additive.inverse (snd x)))\<rfloor>
[PROOF STEP]
proof (subst add_rel_class_of)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. (fst x, snd x) \<in> Sigma I \<FF>
 2. (fst x, xw0.source.additive.inverse (snd x)) \<in> Sigma I \<FF>
 3. ?W \<in> I
 4. ?W \<subseteq> fst x
 5. \<lfloor>?W, +\<^bsub>?W\<^esub> (\<rho> (fst x) ?W (snd x)) (\<rho> (fst x) ?W (xw0.source.additive.inverse (snd x)))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst x) w0 (xw0.source.additive.inverse (snd x)))\<rfloor>
[PROOF STEP]
show "(fst x, xw0.source.additive.inverse (snd x)) \<in> Sigma I \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst x, xw0.source.additive.inverse (snd x)) \<in> Sigma I \<FF>
[PROOF STEP]
using x(2) xw0.source.additive.invertible xw0.source.additive.invertible_inverse_closed
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>
?u \<in> \<FF> (fst x) \<Longrightarrow> xw0.source.additive.invertible ?u
\<lbrakk>xw0.source.additive.invertible ?u; ?u \<in> \<FF> (fst x)\<rbrakk> \<Longrightarrow> xw0.source.additive.inverse ?u \<in> \<FF> (fst x)

goal (1 subgoal):
 1. (fst x, xw0.source.additive.inverse (snd x)) \<in> Sigma I \<FF>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(fst x, xw0.source.additive.inverse (snd x)) \<in> Sigma I \<FF>

goal (4 subgoals):
 1. (fst x, snd x) \<in> Sigma I \<FF>
 2. ?W \<in> I
 3. ?W \<subseteq> fst x
 4. \<lfloor>?W, +\<^bsub>?W\<^esub> (\<rho> (fst x) ?W (snd x)) (\<rho> (fst x) ?W (xw0.source.additive.inverse (snd x)))\<rfloor> = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst x) w0 (xw0.source.additive.inverse (snd x)))\<rfloor>
[PROOF STEP]
qed (use x w0 in auto)
[PROOF STATE]
proof (state)
this:
add_rel X Y = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst x) w0 (xw0.source.additive.inverse (snd x)))\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
add_rel X Y = \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst x) w0 (xw0.source.additive.inverse (snd x)))\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
have "... =  \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst x) w0 (xw0.source.additive.inverse (snd x)))\<rfloor> = \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor>
[PROOF STEP]
apply (subst xw0.additive.invertible_image_lemma)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. xw0.source.additive.invertible (snd x)
 2. snd x \<in> \<FF> (fst x)
 3. \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor> = \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor>
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xw0.source.additive.invertible (snd x)
[PROOF STEP]
using x(2) xw0.source.additive.invertible
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>
?u \<in> \<FF> (fst x) \<Longrightarrow> xw0.source.additive.invertible ?u

goal (1 subgoal):
 1. xw0.source.additive.invertible (snd x)
[PROOF STEP]
by force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. snd x \<in> \<FF> (fst x)
 2. \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor> = \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor>
[PROOF STEP]
using x(2)
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>

goal (2 subgoals):
 1. snd x \<in> \<FF> (fst x)
 2. \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor> = \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst x) w0 (xw0.source.additive.inverse (snd x)))\<rfloor> = \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, +\<^bsub>w0\<^esub> (\<rho> (fst x) w0 (snd x)) (\<rho> (fst x) w0 (xw0.source.additive.inverse (snd x)))\<rfloor> = \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
have "... =  \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor> = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
[PROOF STEP]
by (simp add: assms class_of_0_eq w0(1))
[PROOF STATE]
proof (state)
this:
\<lfloor>w0, \<zero>\<^bsub>w0\<^esub>\<rfloor> = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
[PROOF STEP]
have "add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>

goal (1 subgoal):
 1. add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
have "Y \<in> carrier_direct_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<in> carrier_direct_lim
[PROOF STEP]
using Group_Theory.group_def Y_def carrier_direct_lim_def class_of_def
        monoid.invertible_inverse_closed x(2) xw0.source.additive.group_axioms
        xw0.source.additive.invertible
[PROOF STATE]
proof (prove)
using this:
Group_Theory.group ?G ?composition ?unit \<equiv> Group_Theory.monoid ?G ?composition ?unit \<and> Group_Theory.group_axioms ?G ?composition ?unit
Y = \<lfloor>fst x, xw0.source.additive.inverse (snd x)\<rfloor>
carrier_direct_lim \<equiv> rel.Partition
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)
\<lbrakk>Group_Theory.monoid ?M ?composition ?unit; monoid.invertible ?M ?composition ?unit ?u; ?u \<in> ?M\<rbrakk> \<Longrightarrow> monoid.inverse ?M ?composition ?unit ?u \<in> ?M
x \<in> Sigma I \<FF>
Group_Theory.group (\<FF> (fst x)) +\<^bsub>fst x\<^esub> \<zero>\<^bsub>fst x\<^esub>
?u \<in> \<FF> (fst x) \<Longrightarrow> xw0.source.additive.invertible ?u

goal (1 subgoal):
 1. Y \<in> carrier_direct_lim
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Y \<in> carrier_direct_lim

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Y \<in> carrier_direct_lim

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
have "add_rel Y X = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel Y X = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
[PROOF STEP]
using \<open>Y \<in> carrier_direct_lim\<close> \<open>add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>\<close>
[PROOF STATE]
proof (prove)
using this:
Y \<in> carrier_direct_lim
add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>

goal (1 subgoal):
 1. add_rel Y X = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
[PROOF STEP]
by (simp add: add_rel_commute that)
[PROOF STATE]
proof (state)
this:
add_rel Y X = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
Y \<in> carrier_direct_lim
add_rel Y X = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
Y \<in> carrier_direct_lim
add_rel Y X = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>

goal (1 subgoal):
 1. invertible X
[PROOF STEP]
unfolding invertible_def[OF that]
[PROOF STATE]
proof (prove)
using this:
add_rel X Y = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
Y \<in> carrier_direct_lim
add_rel Y X = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>

goal (1 subgoal):
 1. \<exists>v\<in>carrier_direct_lim. add_rel X v = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor> \<and> add_rel v X = \<lfloor>U, \<zero>\<^bsub>U\<^esub>\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?X1 \<in> carrier_direct_lim \<Longrightarrow> invertible ?X1

goal:
No subgoals!
[PROOF STEP]
qed