[STATEMENT]
lemma cat_GRPH_is_iso_arrD:
  assumes "\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>"
  shows "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
from is_iso_arrD[OF assms]
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
\<exists>g. is_inverse (cat_GRPH \<alpha>) g \<FF>
[PROOF STEP]
have \<FF>: "\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>"
    and "(\<exists>\<GG>. is_inverse (cat_GRPH \<alpha>) \<GG> \<FF>)"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
\<exists>g. is_inverse (cat_GRPH \<alpha>) g \<FF>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB> &&& \<exists>\<GG>. is_inverse (cat_GRPH \<alpha>) \<GG> \<FF>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
\<exists>\<GG>. is_inverse (cat_GRPH \<alpha>) \<GG> \<FF>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
\<exists>\<GG>. is_inverse (cat_GRPH \<alpha>) \<GG> \<FF>
[PROOF STEP]
obtain \<GG> where \<GG>\<FF>: "is_inverse (cat_GRPH \<alpha>) \<GG> \<FF>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
\<exists>\<GG>. is_inverse (cat_GRPH \<alpha>) \<GG> \<FF>

goal (1 subgoal):
 1. (\<And>\<GG>. is_inverse (cat_GRPH \<alpha>) \<GG> \<FF> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
is_inverse (cat_GRPH \<alpha>) \<GG> \<FF>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_inverse (cat_GRPH \<alpha>) \<GG> \<FF>
[PROOF STEP]
obtain \<AA>' \<BB>' where \<GG>': "\<GG> : \<BB>' \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<AA>'"
    and \<FF>': "\<FF> : \<AA>' \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>'"
    and \<GG>\<FF>: "\<GG> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>'\<rparr>"
    and \<FF>\<GG>: "\<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<GG> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>'\<rparr>"
[PROOF STATE]
proof (prove)
using this:
is_inverse (cat_GRPH \<alpha>) \<GG> \<FF>

goal (1 subgoal):
 1. (\<And>\<BB>' \<AA>'. \<lbrakk>\<GG> : \<BB>' \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<AA>'; \<FF> : \<AA>' \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>'; \<GG> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>'\<rparr>; \<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<GG> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>'\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<GG> : \<BB>' \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<AA>'
\<FF> : \<AA>' \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>'
\<GG> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>'\<rparr>
\<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<GG> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>'\<rparr>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
from \<FF> \<FF>'
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
\<FF> : \<AA>' \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>'
[PROOF STEP]
have \<AA>': "\<AA>' = \<AA>" and \<BB>': "\<BB>' = \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
\<FF> : \<AA>' \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>'

goal (1 subgoal):
 1. \<AA>' = \<AA> &&& \<BB>' = \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<AA>' = \<AA>
\<BB>' = \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
from \<FF>
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
[PROOF STEP]
have \<FF>: "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding cat_GRPH_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have \<AA>: "digraph \<alpha> \<AA>" and \<BB>: "digraph \<alpha> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. digraph \<alpha> \<AA> &&& digraph \<alpha> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
from \<GG>'
[PROOF STATE]
proof (chain)
picking this:
\<GG> : \<BB>' \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<AA>'
[PROOF STEP]
have "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB>' \<mapsto>\<^bsub>cat_GRPH \<alpha>\<^esub> \<AA>'

goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
unfolding \<AA>' \<BB>' cat_GRPH_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
from \<GG>\<FF>
[PROOF STATE]
proof (chain)
picking this:
\<GG> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>'\<rparr>
[PROOF STEP]
have "\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<GG> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<FF> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>'\<rparr>

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
[PROOF STEP]
unfolding \<AA>' cat_GRPH_Comp_app[OF \<GG>' \<FF>'] cat_GRPH_CId_app[OF \<AA>]
[PROOF STATE]
proof (prove)
using this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
from \<FF>\<GG>
[PROOF STATE]
proof (chain)
picking this:
\<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<GG> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>'\<rparr>
[PROOF STEP]
have "\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = dghm_id \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> \<circ>\<^sub>A\<^bsub>cat_GRPH \<alpha>\<^esub> \<GG> = cat_GRPH \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>'\<rparr>

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = dghm_id \<BB>
[PROOF STEP]
unfolding \<BB>' cat_GRPH_Comp_app[OF \<FF>' \<GG>'] cat_GRPH_CId_app[OF \<BB>]
[PROOF STATE]
proof (prove)
using this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = dghm_id \<BB>

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = dghm_id \<BB>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = dghm_id \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = dghm_id \<BB>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = dghm_id \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using \<FF>
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = dghm_id \<BB>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (elim is_iso_arr_is_iso_dghm)
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_GRPH_is_iso_arrE:
  assumes "\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>"
  obtains "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. (\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: cat_GRPH_is_iso_arrD)


[STATEMENT]
lemma cat_GRPH_is_iso_arr_iff[cat_GRPH_simps]:
  "\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB> \<longleftrightarrow> \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB> = \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using cat_GRPH_is_iso_arrI cat_GRPH_is_iso_arrD
[PROOF STATE]
proof (prove)
using this:
?\<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>?\<alpha>\<^esub> ?\<BB> \<Longrightarrow> ?\<FF> : ?\<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH ?\<alpha>\<^esub> ?\<BB>
?\<FF> : ?\<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH ?\<alpha>\<^esub> ?\<BB> \<Longrightarrow> ?\<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>?\<alpha>\<^esub> ?\<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB> = \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto


[STATEMENT]
lemma cat_GRPH_obj_isoI:
  assumes "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
[PROOF STEP]
from iso_digraphD[OF assms]
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
obtain \<FF> where "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. (\<And>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
[PROOF STEP]
from cat_GRPH_is_iso_arrI[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule obj_isoI)
[PROOF STATE]
proof (state)
this:
\<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_GRPH_obj_isoD:
  assumes "\<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>"
  shows "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
from obj_isoD[OF assms]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. f : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>
[PROOF STEP]
obtain \<FF> where "\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. f : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. (\<And>\<FF>. \<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
from cat_GRPH_is_iso_arrD[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule iso_digraphI)
[PROOF STATE]
proof (state)
this:
\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_GRPH_obj_isoE:
  assumes "\<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>"
  obtains "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. (\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: cat_GRPH_obj_isoD)


[STATEMENT]
lemma cat_GRPH_obj_iso_iff: "\<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB> \<longleftrightarrow> \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB> = (\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>)
[PROOF STEP]
using cat_GRPH_obj_isoI cat_GRPH_obj_isoD
[PROOF STATE]
proof (prove)
using this:
?\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB> \<Longrightarrow> ?\<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH ?\<alpha>\<^esub> ?\<BB>
?\<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH ?\<alpha>\<^esub> ?\<BB> \<Longrightarrow> ?\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>

goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>o\<^sub>b\<^sub>j\<^bsub>cat_GRPH \<alpha>\<^esub> \<BB> = (\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>)
[PROOF STEP]
by (intro iffI) auto


[STATEMENT]
lemma eigenvector_pow: assumes A: "A \<in> carrier_mat n n"
  and ev: "eigenvector A v (k :: 'a :: comm_ring_1)"
  shows "A ^\<^sub>m i *\<^sub>v v = k^i \<cdot>\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v
[PROOF STEP]
let ?G = "monoid_vec TYPE ('a) n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have dim: "dim_row A = n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. dim_row A = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = n

goal (1 subgoal):
 1. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v
[PROOF STEP]
from ev[unfolded eigenvector_def dim]
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> A *\<^sub>v v = k \<cdot>\<^sub>v v
[PROOF STEP]
have v: "v \<in> carrier_vec n" and Av: "A *\<^sub>v v = k \<cdot>\<^sub>v v"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> A *\<^sub>v v = k \<cdot>\<^sub>v v

goal (1 subgoal):
 1. v \<in> carrier_vec n &&& A *\<^sub>v v = k \<cdot>\<^sub>v v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
A *\<^sub>v v = k \<cdot>\<^sub>v v

goal (1 subgoal):
 1. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v
[PROOF STEP]
interpret v: comm_group ?G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_group (monoid_vec TYPE('a) n)
[PROOF STEP]
by (rule comm_group_vec)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v
[PROOF STEP]
proof (induct i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A ^\<^sub>m 0 *\<^sub>v v = k ^ 0 \<cdot>\<^sub>v v
 2. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. A ^\<^sub>m 0 *\<^sub>v v = k ^ 0 \<cdot>\<^sub>v v
 2. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ^\<^sub>m 0 *\<^sub>v v = k ^ 0 \<cdot>\<^sub>v v
[PROOF STEP]
using v dim
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
dim_row A = n

goal (1 subgoal):
 1. A ^\<^sub>m 0 *\<^sub>v v = k ^ 0 \<cdot>\<^sub>v v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A ^\<^sub>m 0 *\<^sub>v v = k ^ 0 \<cdot>\<^sub>v v

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
define P where "P = A ^\<^sub>m i"
[PROOF STATE]
proof (state)
this:
P = A ^\<^sub>m i

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
have P: "P \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat n n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. P \<in> carrier_mat n n
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. A ^\<^sub>m i \<in> carrier_mat n n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat n n

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
have "A ^\<^sub>m Suc i = P * A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ^\<^sub>m Suc i = P * A
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ^\<^sub>m Suc i = A ^\<^sub>m i * A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A ^\<^sub>m Suc i = P * A

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A ^\<^sub>m Suc i = P * A

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
have "\<dots> *\<^sub>v v = P *\<^sub>v (A *\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * A *\<^sub>v v = P *\<^sub>v (A *\<^sub>v v)
[PROOF STEP]
using P A v
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat n n
A \<in> carrier_mat n n
v \<in> carrier_vec n

goal (1 subgoal):
 1. P * A *\<^sub>v v = P *\<^sub>v (A *\<^sub>v v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P * A *\<^sub>v v = P *\<^sub>v (A *\<^sub>v v)

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P * A *\<^sub>v v = P *\<^sub>v (A *\<^sub>v v)

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
have "A *\<^sub>v v = k \<cdot>\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>v v = k \<cdot>\<^sub>v v
[PROOF STEP]
by (rule Av)
[PROOF STATE]
proof (state)
this:
A *\<^sub>v v = k \<cdot>\<^sub>v v

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A *\<^sub>v v = k \<cdot>\<^sub>v v

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
have "P *\<^sub>v (k \<cdot>\<^sub>v v) = k \<cdot>\<^sub>v (P *\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P *\<^sub>v (k \<cdot>\<^sub>v v) = k \<cdot>\<^sub>v (P *\<^sub>v v)
[PROOF STEP]
by (rule eq_vecI, insert v P, auto)
[PROOF STATE]
proof (state)
this:
P *\<^sub>v (k \<cdot>\<^sub>v v) = k \<cdot>\<^sub>v (P *\<^sub>v v)

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P *\<^sub>v (k \<cdot>\<^sub>v v) = k \<cdot>\<^sub>v (P *\<^sub>v v)

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
have "(P *\<^sub>v v) = (k ^ i) \<cdot>\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P *\<^sub>v v = k ^ i \<cdot>\<^sub>v v
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v
[PROOF STEP]
by (rule Suc)
[PROOF STATE]
proof (state)
this:
P *\<^sub>v v = k ^ i \<cdot>\<^sub>v v

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P *\<^sub>v v = k ^ i \<cdot>\<^sub>v v

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
have "k \<cdot>\<^sub>v ((k ^ i) \<cdot>\<^sub>v v) = (k * k ^ i) \<cdot>\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<cdot>\<^sub>v (k ^ i \<cdot>\<^sub>v v) = k * k ^ i \<cdot>\<^sub>v v
[PROOF STEP]
by (rule eq_vecI, insert v, auto)
[PROOF STATE]
proof (state)
this:
k \<cdot>\<^sub>v (k ^ i \<cdot>\<^sub>v v) = k * k ^ i \<cdot>\<^sub>v v

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
k \<cdot>\<^sub>v (k ^ i \<cdot>\<^sub>v v) = k * k ^ i \<cdot>\<^sub>v v

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
have "k * k ^ i = k ^ (Suc i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k * k ^ i = k ^ Suc i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k * k ^ i = k ^ Suc i

goal (1 subgoal):
 1. \<And>i. A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v \<Longrightarrow> A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v

goal (1 subgoal):
 1. A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A ^\<^sub>m Suc i *\<^sub>v v = k ^ Suc i \<cdot>\<^sub>v v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A ^\<^sub>m i *\<^sub>v v = k ^ i \<cdot>\<^sub>v v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eigenvector_char_matrix: assumes A: "(A :: 'a :: field mat) \<in> carrier_mat n n"
  shows "eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have dim: "dim_row A = n" "dim_col A = n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. dim_row A = n &&& dim_col A = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = n
dim_col A = n

goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
dim_row A = n
dim_col A = n

goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
assume v: "v \<in> carrier_vec n"
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n

goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
hence dimv: "dim_vec v = n"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n

goal (1 subgoal):
 1. dim_vec v = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec v = n

goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
have "(A *\<^sub>v v = e \<cdot>\<^sub>v v) = (A *\<^sub>v v + (-e) \<cdot>\<^sub>v v = 0\<^sub>v n)" (is "?id1 = ?id2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A *\<^sub>v v = e \<cdot>\<^sub>v v) = (A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A *\<^sub>v v = e \<cdot>\<^sub>v v \<Longrightarrow> A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n
 2. A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n \<Longrightarrow> A *\<^sub>v v = e \<cdot>\<^sub>v v
[PROOF STEP]
assume ?id1
[PROOF STATE]
proof (state)
this:
A *\<^sub>v v = e \<cdot>\<^sub>v v

goal (2 subgoals):
 1. A *\<^sub>v v = e \<cdot>\<^sub>v v \<Longrightarrow> A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n
 2. A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n \<Longrightarrow> A *\<^sub>v v = e \<cdot>\<^sub>v v
[PROOF STEP]
from arg_cong[OF this, of "\<lambda> w. w + (-e) \<cdot>\<^sub>v v"]
[PROOF STATE]
proof (chain)
picking this:
A *\<^sub>v v + - e \<cdot>\<^sub>v v = e \<cdot>\<^sub>v v + - e \<cdot>\<^sub>v v
[PROOF STEP]
show ?id2
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v v + - e \<cdot>\<^sub>v v = e \<cdot>\<^sub>v v + - e \<cdot>\<^sub>v v

goal (1 subgoal):
 1. A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
using A v
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v v + - e \<cdot>\<^sub>v v = e \<cdot>\<^sub>v v + - e \<cdot>\<^sub>v v
A \<in> carrier_mat n n
v \<in> carrier_vec n

goal (1 subgoal):
 1. A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n \<Longrightarrow> A *\<^sub>v v = e \<cdot>\<^sub>v v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n \<Longrightarrow> A *\<^sub>v v = e \<cdot>\<^sub>v v
[PROOF STEP]
assume ?id2
[PROOF STATE]
proof (state)
this:
A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n \<Longrightarrow> A *\<^sub>v v = e \<cdot>\<^sub>v v
[PROOF STEP]
have "A *\<^sub>v v + - e \<cdot>\<^sub>v v + e \<cdot>\<^sub>v v = A *\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>v v + - e \<cdot>\<^sub>v v + e \<cdot>\<^sub>v v = A *\<^sub>v v
[PROOF STEP]
using A v
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
v \<in> carrier_vec n

goal (1 subgoal):
 1. A *\<^sub>v v + - e \<cdot>\<^sub>v v + e \<cdot>\<^sub>v v = A *\<^sub>v v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A *\<^sub>v v + - e \<cdot>\<^sub>v v + e \<cdot>\<^sub>v v = A *\<^sub>v v

goal (1 subgoal):
 1. A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n \<Longrightarrow> A *\<^sub>v v = e \<cdot>\<^sub>v v
[PROOF STEP]
from arg_cong[OF \<open>?id2\<close>, of "\<lambda> w. w + e \<cdot>\<^sub>v v", unfolded this]
[PROOF STATE]
proof (chain)
picking this:
A *\<^sub>v v = 0\<^sub>v n + e \<cdot>\<^sub>v v
[PROOF STEP]
show ?id1
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v v = 0\<^sub>v n + e \<cdot>\<^sub>v v

goal (1 subgoal):
 1. A *\<^sub>v v = e \<cdot>\<^sub>v v
[PROOF STEP]
using A v
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v v = 0\<^sub>v n + e \<cdot>\<^sub>v v
A \<in> carrier_mat n n
v \<in> carrier_vec n

goal (1 subgoal):
 1. A *\<^sub>v v = e \<cdot>\<^sub>v v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A *\<^sub>v v = e \<cdot>\<^sub>v v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A *\<^sub>v v = e \<cdot>\<^sub>v v) = (A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n)

goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A *\<^sub>v v = e \<cdot>\<^sub>v v) = (A *\<^sub>v v + - e \<cdot>\<^sub>v v = 0\<^sub>v n)

goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
have "(A *\<^sub>v v + (-e) \<cdot>\<^sub>v v) = char_matrix A e *\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>v v + - e \<cdot>\<^sub>v v = char_matrix A e *\<^sub>v v
[PROOF STEP]
unfolding char_matrix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>v v + - e \<cdot>\<^sub>v v = (A + - e \<cdot>\<^sub>m 1\<^sub>m (dim_row A)) *\<^sub>v v
[PROOF STEP]
by (rule eq_vecI, insert v A dim, auto simp: add_scalar_prod_distrib[of _ n])
[PROOF STATE]
proof (state)
this:
A *\<^sub>v v + - e \<cdot>\<^sub>v v = char_matrix A e *\<^sub>v v

goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(A *\<^sub>v v = e \<cdot>\<^sub>v v) = (char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
have "(A *\<^sub>v v = e \<cdot>\<^sub>v v) = (char_matrix A e *\<^sub>v v = 0\<^sub>v n)"
[PROOF STATE]
proof (prove)
using this:
(A *\<^sub>v v = e \<cdot>\<^sub>v v) = (char_matrix A e *\<^sub>v v = 0\<^sub>v n)

goal (1 subgoal):
 1. (A *\<^sub>v v = e \<cdot>\<^sub>v v) = (char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(A *\<^sub>v v = e \<cdot>\<^sub>v v) = (char_matrix A e *\<^sub>v v = 0\<^sub>v n)

goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n \<Longrightarrow> (A *\<^sub>v v = e \<cdot>\<^sub>v v) = (char_matrix A e *\<^sub>v v = 0\<^sub>v n)

goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n \<Longrightarrow> (A *\<^sub>v v = e \<cdot>\<^sub>v v) = (char_matrix A e *\<^sub>v v = 0\<^sub>v n)

goal (1 subgoal):
 1. eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
unfolding eigenvector_def dim
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n \<Longrightarrow> (A *\<^sub>v v = e \<cdot>\<^sub>v v) = (char_matrix A e *\<^sub>v v = 0\<^sub>v n)

goal (1 subgoal):
 1. (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> A *\<^sub>v v = e \<cdot>\<^sub>v v) = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eigenvector A v e = (v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eigenvalue_char_matrix: assumes A: "(A :: 'a :: field mat) \<in> carrier_mat n n"
  shows "eigenvalue A e = (\<exists> v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenvalue A e = (\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
unfolding eigenvalue_def eigenvector_char_matrix[OF A]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n) = (\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
..


[STATEMENT]
lemma find_eigenvector: assumes A: "A \<in> carrier_mat n n"
  and ev: "eigenvalue A e"
  shows "eigenvector A (find_eigenvector A e) e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
define B where "B = char_matrix A e"
[PROOF STATE]
proof (state)
this:
B = char_matrix A e

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
from ev[unfolded eigenvalue_char_matrix[OF A]]
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
obtain v where
    v: "v \<in> carrier_vec n" "v \<noteq> 0\<^sub>v n" and Bv: "B *\<^sub>v v = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> carrier_vec n; v \<noteq> 0\<^sub>v n; B *\<^sub>v v = 0\<^sub>v n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> carrier_vec n; v \<noteq> 0\<^sub>v n; char_matrix A e *\<^sub>v v = 0\<^sub>v n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
B *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
have B: "B \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<in> carrier_mat n n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. B \<in> carrier_mat n n
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. char_matrix A e \<in> carrier_mat n n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B \<in> carrier_mat n n

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
let ?z = "0\<^sub>m (dim_row A) 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
obtain C D where gauss: "gauss_jordan B ?z = (C,D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C D. gauss_jordan B (0\<^sub>m (dim_row A) 0) = (C, D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
gauss_jordan B (0\<^sub>m (dim_row A) 0) = (C, D)

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
define w where "w = find_base_vector C"
[PROOF STATE]
proof (state)
this:
w = find_base_vector C

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
have res: "find_eigenvector A e = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_eigenvector A e = w
[PROOF STEP]
unfolding w_def find_eigenvector_def Let_def gauss B_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_base_vector (fst (C, D)) = find_base_vector C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_eigenvector A e = w

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
have "?z \<in> carrier_mat n 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>m (dim_row A) 0 \<in> carrier_mat n 0
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. 0\<^sub>m (dim_row A) 0 \<in> carrier_mat n 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0\<^sub>m (dim_row A) 0 \<in> carrier_mat n 0

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
note gauss_0 = gauss_jordan[OF B this gauss]
[PROOF STATE]
proof (state)
this:
?x \<in> carrier_vec n \<Longrightarrow> (B *\<^sub>v ?x = 0\<^sub>v n) = (C *\<^sub>v ?x = 0\<^sub>v n)
?X \<in> carrier_mat n 0 \<Longrightarrow> (B * ?X = 0\<^sub>m (dim_row A) 0) = (C * ?X = D)
C \<in> carrier_mat n n
D \<in> carrier_mat n 0

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
hence C: "C \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier_vec n \<Longrightarrow> (B *\<^sub>v ?x = 0\<^sub>v n) = (C *\<^sub>v ?x = 0\<^sub>v n)
?X \<in> carrier_mat n 0 \<Longrightarrow> (B * ?X = 0\<^sub>m (dim_row A) 0) = (C * ?X = D)
C \<in> carrier_mat n n
D \<in> carrier_mat n 0

goal (1 subgoal):
 1. C \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> carrier_mat n n

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
from gauss_0(1)[OF v(1)] Bv
[PROOF STATE]
proof (chain)
picking this:
(B *\<^sub>v v = 0\<^sub>v n) = (C *\<^sub>v v = 0\<^sub>v n)
B *\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
have Cv: "C *\<^sub>v v = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
(B *\<^sub>v v = 0\<^sub>v n) = (C *\<^sub>v v = 0\<^sub>v n)
B *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. C *\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
C *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
assume C: "C = 1\<^sub>m n"
[PROOF STATE]
proof (state)
this:
C = 1\<^sub>m n

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using id Cv v
[PROOF STATE]
proof (prove)
using this:
swapidseq 0 id
C *\<^sub>v v = 0\<^sub>v n
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding C
[PROOF STATE]
proof (prove)
using this:
swapidseq 0 id
1\<^sub>m n *\<^sub>v v = 0\<^sub>v n
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
C = 1\<^sub>m n \<Longrightarrow> False

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
hence C1: "C \<noteq> 1\<^sub>m n"
[PROOF STATE]
proof (prove)
using this:
C = 1\<^sub>m n \<Longrightarrow> False

goal (1 subgoal):
 1. C \<noteq> 1\<^sub>m n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<noteq> 1\<^sub>m n

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
from find_base_vector_not_1[OF gauss_jordan_row_echelon[OF B gauss] C C1]
[PROOF STATE]
proof (chain)
picking this:
find_base_vector C \<in> carrier_vec n
find_base_vector C \<noteq> 0\<^sub>v n
C *\<^sub>v find_base_vector C = 0\<^sub>v n
[PROOF STEP]
have w: "w \<in> carrier_vec n" "w \<noteq> 0\<^sub>v n" and id: "C *\<^sub>v w = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
find_base_vector C \<in> carrier_vec n
find_base_vector C \<noteq> 0\<^sub>v n
C *\<^sub>v find_base_vector C = 0\<^sub>v n

goal (1 subgoal):
 1. (w \<in> carrier_vec n &&& w \<noteq> 0\<^sub>v n) &&& C *\<^sub>v w = 0\<^sub>v n
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
using this:
find_base_vector C \<in> carrier_vec n
find_base_vector C \<noteq> 0\<^sub>v n
C *\<^sub>v find_base_vector C = 0\<^sub>v n

goal (1 subgoal):
 1. (find_base_vector C \<in> carrier_vec n &&& find_base_vector C \<noteq> 0\<^sub>v n) &&& C *\<^sub>v find_base_vector C = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> carrier_vec n
w \<noteq> 0\<^sub>v n
C *\<^sub>v w = 0\<^sub>v n

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
from gauss_0(1)[OF w(1)] id
[PROOF STATE]
proof (chain)
picking this:
(B *\<^sub>v w = 0\<^sub>v n) = (C *\<^sub>v w = 0\<^sub>v n)
C *\<^sub>v w = 0\<^sub>v n
[PROOF STEP]
have Bw: "B *\<^sub>v w = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
(B *\<^sub>v w = 0\<^sub>v n) = (C *\<^sub>v w = 0\<^sub>v n)
C *\<^sub>v w = 0\<^sub>v n

goal (1 subgoal):
 1. B *\<^sub>v w = 0\<^sub>v n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B *\<^sub>v w = 0\<^sub>v n

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
from w Bw
[PROOF STATE]
proof (chain)
picking this:
w \<in> carrier_vec n
w \<noteq> 0\<^sub>v n
B *\<^sub>v w = 0\<^sub>v n
[PROOF STEP]
have "eigenvector A w e"
[PROOF STATE]
proof (prove)
using this:
w \<in> carrier_vec n
w \<noteq> 0\<^sub>v n
B *\<^sub>v w = 0\<^sub>v n

goal (1 subgoal):
 1. eigenvector A w e
[PROOF STEP]
unfolding eigenvector_char_matrix[OF A] B_def
[PROOF STATE]
proof (prove)
using this:
w \<in> carrier_vec n
w \<noteq> 0\<^sub>v n
char_matrix A e *\<^sub>v w = 0\<^sub>v n

goal (1 subgoal):
 1. w \<in> carrier_vec n \<and> w \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v w = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigenvector A w e

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
eigenvector A w e

goal (1 subgoal):
 1. eigenvector A (find_eigenvector A e) e
[PROOF STEP]
unfolding res
[PROOF STATE]
proof (prove)
using this:
eigenvector A w e

goal (1 subgoal):
 1. eigenvector A w e
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eigenvector A (find_eigenvector A e) e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eigenvalue_imp_nonzero_dim: assumes "A \<in> carrier_mat n n"
  and "eigenvalue A ev"
  shows "n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> 0 < n
 2. \<And>nat. n = Suc nat \<Longrightarrow> 0 < n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> 0 < n
 2. \<And>nat. n = Suc nat \<Longrightarrow> 0 < n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
eigenvalue A ev
[PROOF STEP]
obtain v where "eigenvector A v ev"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
eigenvalue A ev

goal (1 subgoal):
 1. (\<And>v. eigenvector A v ev \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eigenvalue_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
\<exists>v. eigenvector A v ev

goal (1 subgoal):
 1. (\<And>v. eigenvector A v ev \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigenvector A v ev

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> 0 < n
 2. \<And>nat. n = Suc nat \<Longrightarrow> 0 < n
[PROOF STEP]
from this[unfolded eigenvector_def] assms 0
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec (dim_row A) \<and> v \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v v = ev \<cdot>\<^sub>v v
A \<in> carrier_mat n n
eigenvalue A ev
n = 0
[PROOF STEP]
have "v \<in> carrier_vec 0" "v \<noteq> 0\<^sub>v 0"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec (dim_row A) \<and> v \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v v = ev \<cdot>\<^sub>v v
A \<in> carrier_mat n n
eigenvalue A ev
n = 0

goal (1 subgoal):
 1. v \<in> carrier_vec 0 &&& v \<noteq> 0\<^sub>v 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec 0
v \<noteq> 0\<^sub>v 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> 0 < n
 2. \<And>nat. n = Suc nat \<Longrightarrow> 0 < n
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec 0
v \<noteq> 0\<^sub>v 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> 0 < n
 2. \<And>nat. n = Suc nat \<Longrightarrow> 0 < n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> 0 < n
[PROOF STEP]
qed simp


[STATEMENT]
lemma eigenvalue_det: assumes A: "(A :: 'a :: field mat) \<in> carrier_mat n n" shows
  "eigenvalue A e = (det (char_matrix A e) = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenvalue A e = (det (char_matrix A e) = (0::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvalue A e = (det (char_matrix A e) = (0::'a))
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have cA: "char_matrix A e \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. char_matrix A e \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
char_matrix A e \<in> carrier_mat n n

goal (1 subgoal):
 1. eigenvalue A e = (det (char_matrix A e) = (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenvalue A e = (det (char_matrix A e) = (0::'a))
[PROOF STEP]
unfolding eigenvalue_char_matrix[OF A]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n) = (det (char_matrix A e) = (0::'a))
[PROOF STEP]
unfolding id det_0_negate[OF cA] det_0_iff_vec_prod_zero[OF cA]
      eigenvalue_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n) = (\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A e *\<^sub>v v = 0\<^sub>v n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigenvalue A e = (det (char_matrix A e) = (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma char_poly_matrix_closed[simp]: "A \<in> carrier_mat n n \<Longrightarrow> char_poly_matrix A \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> carrier_mat n n \<Longrightarrow> char_poly_matrix A \<in> carrier_mat n n
[PROOF STEP]
unfolding char_poly_matrix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> carrier_mat n n \<Longrightarrow> [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A \<in> carrier_mat n n
[PROOF STEP]
by auto


[STATEMENT]
lemma (in comm_ring_hom) char_poly_matrix_hom: assumes A: "A \<in> carrier_mat n n"
  shows "char_poly_matrix (mat\<^sub>h A) = map_mat (map_poly hom) (char_poly_matrix A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly_matrix (mat\<^sub>h A) = map_mat (map_poly hom) (char_poly_matrix A)
[PROOF STEP]
unfolding char_poly_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'b, 1::'b:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (mat\<^sub>h A)) + map_mat (\<lambda>a. [:- a:]) (mat\<^sub>h A) = map_mat (map_poly hom) ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A)
[PROOF STEP]
by (rule eq_matI, insert A, auto simp: smult_mat_def hom_distribs)


[STATEMENT]
lemma (in comm_ring_hom) char_poly_hom: assumes A: "A \<in> carrier_mat n n"
  shows "char_poly (map_mat hom A) = map_poly hom (char_poly A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly (mat\<^sub>h A) = map_poly hom (char_poly A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly (mat\<^sub>h A) = map_poly hom (char_poly A)
[PROOF STEP]
interpret map_poly_hom: map_poly_comm_ring_hom hom
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly_comm_ring_hom hom
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly (mat\<^sub>h A) = map_poly hom (char_poly A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly (mat\<^sub>h A) = map_poly hom (char_poly A)
[PROOF STEP]
unfolding char_poly_def map_poly_hom.hom_det[symmetric] char_poly_matrix_hom[OF A]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (map_poly_hom.mat_hom (char_poly_matrix A)) = det (map_poly_hom.mat_hom (char_poly_matrix A))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
char_poly (mat\<^sub>h A) = map_poly hom (char_poly A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eigenvector_hom: assumes A: "A \<in> carrier_mat n n"
  and ev: "eigenvector A v ev"
  shows "eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
let ?A = "mat\<^sub>h A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
let ?v = "vec\<^sub>h v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
let ?ev = "hom ev"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
from ev[unfolded eigenvector_def] A
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec (dim_row A) \<and> v \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v v = ev \<cdot>\<^sub>v v
A \<in> carrier_mat n n
[PROOF STEP]
have v: "v \<in> carrier_vec n" "v \<noteq> 0\<^sub>v n" "A *\<^sub>v v = ev \<cdot>\<^sub>v v"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec (dim_row A) \<and> v \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v v = ev \<cdot>\<^sub>v v
A \<in> carrier_mat n n

goal (1 subgoal):
 1. v \<in> carrier_vec n &&& v \<noteq> 0\<^sub>v n &&& A *\<^sub>v v = ev \<cdot>\<^sub>v v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
A *\<^sub>v v = ev \<cdot>\<^sub>v v

goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
from v(1)
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n
[PROOF STEP]
have v1: "?v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n

goal (1 subgoal):
 1. vec\<^sub>h v \<in> carrier_vec n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec\<^sub>h v \<in> carrier_vec n

goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
from v(1-2)
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
[PROOF STEP]
obtain i where "i < n" and "v $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < n; v $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
i < n
v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
with v(1)
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n
i < n
v $ i \<noteq> (0::'a)
[PROOF STEP]
have "?v $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
i < n
v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. vec\<^sub>h v $ i \<noteq> (0::'b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec\<^sub>h v $ i \<noteq> (0::'b)

goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
hence v2: "?v \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
vec\<^sub>h v $ i \<noteq> (0::'b)

goal (1 subgoal):
 1. vec\<^sub>h v \<noteq> 0\<^sub>v n
[PROOF STEP]
using \<open>i < n\<close> v(1)
[PROOF STATE]
proof (prove)
using this:
vec\<^sub>h v $ i \<noteq> (0::'b)
i < n
v \<in> carrier_vec n

goal (1 subgoal):
 1. vec\<^sub>h v \<noteq> 0\<^sub>v n
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vec\<^sub>h v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
from arg_cong[OF v(3), of "vec\<^sub>h", unfolded mult_mat_vec_hom[OF A v(1)] vec_hom_smult]
[PROOF STATE]
proof (chain)
picking this:
mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v
[PROOF STEP]
have v3: "?A *\<^sub>v ?v = ?ev \<cdot>\<^sub>v ?v"
[PROOF STATE]
proof (prove)
using this:
mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v

goal (1 subgoal):
 1. mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v

goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
from v1 v2 v3
[PROOF STATE]
proof (chain)
picking this:
vec\<^sub>h v \<in> carrier_vec n
vec\<^sub>h v \<noteq> 0\<^sub>v n
mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vec\<^sub>h v \<in> carrier_vec n
vec\<^sub>h v \<noteq> 0\<^sub>v n
mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v

goal (1 subgoal):
 1. eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)
[PROOF STEP]
unfolding eigenvector_def
[PROOF STATE]
proof (prove)
using this:
vec\<^sub>h v \<in> carrier_vec n
vec\<^sub>h v \<noteq> 0\<^sub>v n
mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v

goal (1 subgoal):
 1. vec\<^sub>h v \<in> carrier_vec (dim_row (mat\<^sub>h A)) \<and> vec\<^sub>h v \<noteq> 0\<^sub>v (dim_row (mat\<^sub>h A)) \<and> mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
vec\<^sub>h v \<in> carrier_vec n
vec\<^sub>h v \<noteq> 0\<^sub>v n
mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v
A \<in> carrier_mat n n

goal (1 subgoal):
 1. vec\<^sub>h v \<in> carrier_vec (dim_row (mat\<^sub>h A)) \<and> vec\<^sub>h v \<noteq> 0\<^sub>v (dim_row (mat\<^sub>h A)) \<and> mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eigenvalue_hom: assumes A: "A \<in> carrier_mat n n"
  and ev: "eigenvalue A ev"
  shows "eigenvalue (mat\<^sub>h A) (hom ev)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenvalue (mat\<^sub>h A) (hom ev)
[PROOF STEP]
using eigenvector_hom[OF A, of _ ev] ev
[PROOF STATE]
proof (prove)
using this:
eigenvector A ?v ev \<Longrightarrow> eigenvector (mat\<^sub>h A) (vec\<^sub>h ?v) (hom ev)
eigenvalue A ev

goal (1 subgoal):
 1. eigenvalue (mat\<^sub>h A) (hom ev)
[PROOF STEP]
unfolding eigenvalue_def
[PROOF STATE]
proof (prove)
using this:
eigenvector A ?v ev \<Longrightarrow> eigenvector (mat\<^sub>h A) (vec\<^sub>h ?v) (hom ev)
\<exists>v. eigenvector A v ev

goal (1 subgoal):
 1. \<exists>v. eigenvector (mat\<^sub>h A) v (hom ev)
[PROOF STEP]
by auto


[STATEMENT]
lemma eigenvector_hom_rev: assumes A: "A \<in> carrier_mat n n"
  and ev: "eigenvector (mat\<^sub>h A) (vec\<^sub>h v) (hom ev)"
  shows "eigenvector A v ev"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
let ?A = "mat\<^sub>h A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
let ?v = "vec\<^sub>h v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
let ?ev = "hom ev"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
from ev[unfolded eigenvector_def] A
[PROOF STATE]
proof (chain)
picking this:
vec\<^sub>h v \<in> carrier_vec (dim_row (mat\<^sub>h A)) \<and> vec\<^sub>h v \<noteq> 0\<^sub>v (dim_row (mat\<^sub>h A)) \<and> mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v
A \<in> carrier_mat n n
[PROOF STEP]
have v: "v \<in> carrier_vec n" "?v \<noteq> 0\<^sub>v n" "?A *\<^sub>v ?v = ?ev \<cdot>\<^sub>v ?v"
[PROOF STATE]
proof (prove)
using this:
vec\<^sub>h v \<in> carrier_vec (dim_row (mat\<^sub>h A)) \<and> vec\<^sub>h v \<noteq> 0\<^sub>v (dim_row (mat\<^sub>h A)) \<and> mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v
A \<in> carrier_mat n n

goal (1 subgoal):
 1. v \<in> carrier_vec n &&& vec\<^sub>h v \<noteq> 0\<^sub>v n &&& mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
vec\<^sub>h v \<noteq> 0\<^sub>v n
mat\<^sub>h A *\<^sub>v vec\<^sub>h v = hom ev \<cdot>\<^sub>v vec\<^sub>h v

goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
from v(1-2)
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n
vec\<^sub>h v \<noteq> 0\<^sub>v n
[PROOF STEP]
obtain i where "i < n" and "v $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
vec\<^sub>h v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < n; v $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
i < n
v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
with v(1)
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n
i < n
v $ i \<noteq> (0::'a)
[PROOF STEP]
have "v $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
i < n
v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. v $ i \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
hence v2: "v \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. v \<noteq> 0\<^sub>v n
[PROOF STEP]
using \<open>i < n\<close> v(1)
[PROOF STATE]
proof (prove)
using this:
v $ i \<noteq> (0::'a)
i < n
v \<in> carrier_vec n

goal (1 subgoal):
 1. v \<noteq> 0\<^sub>v n
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
from vec_hom_inj[OF v(3)[folded mult_mat_vec_hom[OF A v(1)] vec_hom_smult]]
[PROOF STATE]
proof (chain)
picking this:
A *\<^sub>v v = ev \<cdot>\<^sub>v v
[PROOF STEP]
have v3: "A *\<^sub>v v = ev \<cdot>\<^sub>v v"
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v v = ev \<cdot>\<^sub>v v

goal (1 subgoal):
 1. A *\<^sub>v v = ev \<cdot>\<^sub>v v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A *\<^sub>v v = ev \<cdot>\<^sub>v v

goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
from v(1) v2 v3
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
A *\<^sub>v v = ev \<cdot>\<^sub>v v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
A *\<^sub>v v = ev \<cdot>\<^sub>v v

goal (1 subgoal):
 1. eigenvector A v ev
[PROOF STEP]
unfolding eigenvector_def
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
A *\<^sub>v v = ev \<cdot>\<^sub>v v

goal (1 subgoal):
 1. v \<in> carrier_vec (dim_row A) \<and> v \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v v = ev \<cdot>\<^sub>v v
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
A *\<^sub>v v = ev \<cdot>\<^sub>v v
A \<in> carrier_mat n n

goal (1 subgoal):
 1. v \<in> carrier_vec (dim_row A) \<and> v \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v v = ev \<cdot>\<^sub>v v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigenvector A v ev

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_det_cong: assumes A: "A \<in> carrier_mat n n"
  and B: "B \<in> carrier_mat n n"
  and poly: "\<And> i j. i < n \<Longrightarrow> j < n \<Longrightarrow> poly (B $$ (i,j)) k = A $$ (i,j)"
  shows "poly (det B) k = det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (det B) k = det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly (det B) k = det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (det B) k = det A
[PROOF STEP]
unfolding det_def'[OF A] det_def'[OF B] poly_sum poly_mult poly_prod
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ka\<in>{p. p permutes {0..<n}}. poly (of_int (sign ka)) k * (\<Prod>kb = 0..<n. poly (B $$ (kb, ka kb)) k)) = (\<Sum>p | p permutes {0..<n}. of_int (sign p) * (\<Prod>i = 0..<n. A $$ (i, p i)))
[PROOF STEP]
proof (rule sum.cong[OF refl])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {p. p permutes {0..<n}} \<Longrightarrow> poly (of_int (sign x)) k * (\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k) = of_int (sign x) * (\<Prod>i = 0..<n. A $$ (i, x i))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {p. p permutes {0..<n}} \<Longrightarrow> poly (of_int (sign x)) k * (\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k) = of_int (sign x) * (\<Prod>i = 0..<n. A $$ (i, x i))
[PROOF STEP]
assume x: "x \<in> {p. p permutes {0..<n}}"
[PROOF STATE]
proof (state)
this:
x \<in> {p. p permutes {0..<n}}

goal (1 subgoal):
 1. \<And>x. x \<in> {p. p permutes {0..<n}} \<Longrightarrow> poly (of_int (sign x)) k * (\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k) = of_int (sign x) * (\<Prod>i = 0..<n. A $$ (i, x i))
[PROOF STEP]
let ?l = "\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {p. p permutes {0..<n}} \<Longrightarrow> poly (of_int (sign x)) k * (\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k) = of_int (sign x) * (\<Prod>i = 0..<n. A $$ (i, x i))
[PROOF STEP]
let ?r = "\<Prod>i = 0..<n. A $$ (i, x i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {p. p permutes {0..<n}} \<Longrightarrow> poly (of_int (sign x)) k * (\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k) = of_int (sign x) * (\<Prod>i = 0..<n. A $$ (i, x i))
[PROOF STEP]
have id: "?l = ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k) = (\<Prod>i = 0..<n. A $$ (i, x i))
[PROOF STEP]
by (rule prod.cong[OF refl poly], insert x, auto)
[PROOF STATE]
proof (state)
this:
(\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k) = (\<Prod>i = 0..<n. A $$ (i, x i))

goal (1 subgoal):
 1. \<And>x. x \<in> {p. p permutes {0..<n}} \<Longrightarrow> poly (of_int (sign x)) k * (\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k) = of_int (sign x) * (\<Prod>i = 0..<n. A $$ (i, x i))
[PROOF STEP]
show "poly (signof x) k * ?l = signof x * ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int (sign x)) k * (\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k) = of_int (sign x) * (\<Prod>i = 0..<n. A $$ (i, x i))
[PROOF STEP]
by (cases x rule: sign_cases) (simp_all add: id)
[PROOF STATE]
proof (state)
this:
poly (of_int (sign x)) k * (\<Prod>ka = 0..<n. poly (B $$ (ka, x ka)) k) = of_int (sign x) * (\<Prod>i = 0..<n. A $$ (i, x i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly (det B) k = det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma char_poly_matrix: assumes A: "(A :: 'a :: field mat) \<in> carrier_mat n n"
  shows "poly (char_poly A) k = det (- (char_matrix A k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (char_poly A) k = det (- char_matrix A k)
[PROOF STEP]
unfolding char_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (det (char_poly_matrix A)) k = det (- char_matrix A k)
[PROOF STEP]
by (rule poly_det_cong[of _ n], insert A, auto simp: char_poly_matrix_def char_matrix_def)


[STATEMENT]
lemma eigenvalue_root_char_poly: assumes A: "(A :: 'a :: field mat) \<in> carrier_mat n n"
  shows "eigenvalue A k \<longleftrightarrow> poly (char_poly A) k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenvalue A k = (poly (char_poly A) k = (0::'a))
[PROOF STEP]
unfolding eigenvalue_det[OF A] char_poly_matrix[OF A]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (det (char_matrix A k) = (0::'a)) = (det (- char_matrix A k) = (0::'a))
[PROOF STEP]
by (subst det_0_negate[of _ n], insert A, auto)


[STATEMENT]
lemma char_poly_matrix_upper_triangular: "upper_triangular (char_poly_matrix A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular (char_poly_matrix A)
[PROOF STEP]
using A ut
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
upper_triangular A

goal (1 subgoal):
 1. upper_triangular (char_poly_matrix A)
[PROOF STEP]
unfolding upper_triangular_def char_poly_matrix_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
\<forall>i<dim_row A. \<forall>j<i. A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. \<forall>i<dim_row ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A). \<forall>j<i. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A) $$ (i, j) = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma char_poly_upper_triangular:
  "char_poly A = (\<Prod> a \<leftarrow> diag_mat A. [:- a, 1:])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly A = (\<Prod>a\<leftarrow>diag_mat A. [:- a, 1::'a:])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = (\<Prod>a\<leftarrow>diag_mat A. [:- a, 1::'a:])
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have cA: "char_poly_matrix A \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. char_poly_matrix A \<in> carrier_mat n n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
char_poly_matrix A \<in> carrier_mat n n

goal (1 subgoal):
 1. char_poly A = (\<Prod>a\<leftarrow>diag_mat A. [:- a, 1::'a:])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly A = (\<Prod>a\<leftarrow>diag_mat A. [:- a, 1::'a:])
[PROOF STEP]
unfolding char_poly_def det_upper_triangular [OF char_poly_matrix_upper_triangular cA]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (diag_mat (char_poly_matrix A)) = (\<Prod>a\<leftarrow>diag_mat A. [:- a, 1::'a:])
[PROOF STEP]
by (rule arg_cong[where f = prod_list], unfold list_eq_iff_nth_eq, insert cA A, auto simp: diag_mat_def
      char_poly_matrix_def)
[PROOF STATE]
proof (state)
this:
char_poly A = (\<Prod>a\<leftarrow>diag_mat A. [:- a, 1::'a:])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_poly_mult: assumes A: "A \<in> carrier_mat nr n"
  and B: "B \<in> carrier_mat n nc"
  shows
    "map_mat (\<lambda> a. [: a :]) (A * B) = map_mat (\<lambda> a. [: a :]) A * map_mat (\<lambda> a. [: a :]) B" (is "?id")
    "map_mat (\<lambda> a. [: a :] * p) (A * B) = map_mat (\<lambda> a. [: a :] * p) A * map_mat (\<lambda> a. [: a :]) B" (is "?left")
    "map_mat (\<lambda> a. [: a :] * p) (A * B) = map_mat (\<lambda> a. [: a :]) A * map_mat (\<lambda> a. [: a :] * p) B" (is "?right")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B &&& map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B &&& map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
from A B
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat nr n
B \<in> carrier_mat n nc
[PROOF STEP]
have dim: "dim_row A = nr" "dim_col A = n" "dim_row B = n" "dim_col B = nc"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr n
B \<in> carrier_mat n nc

goal (1 subgoal):
 1. (dim_row A = nr &&& dim_col A = n) &&& dim_row B = n &&& dim_col B = nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = nr
dim_col A = n
dim_row B = n
dim_col B = nc

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
dim_row A = nr
dim_col A = n
dim_row B = n
dim_col B = nc

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
have "i < nr \<Longrightarrow> j < nc \<Longrightarrow>
      row (map_mat (\<lambda>a. [:a:]) A) i \<bullet> col (map_mat (\<lambda>a. [:a:]) B) j = [:(row A i \<bullet> col B j):]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < nr; j < nc\<rbrakk> \<Longrightarrow> row (map_mat (\<lambda>a. [:a:]) A) i \<bullet> col (map_mat (\<lambda>a. [:a:]) B) j = [:row A i \<bullet> col B j:]
[PROOF STEP]
unfolding scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < nr; j < nc\<rbrakk> \<Longrightarrow> (\<Sum>ia = 0..<dim_vec (col (map_mat (\<lambda>a. [:a:]) B) j). row (map_mat (\<lambda>a. [:a:]) A) i $ ia * col (map_mat (\<lambda>a. [:a:]) B) j $ ia) = [:\<Sum>ia = 0..<dim_vec (col B j). row A i $ ia * col B j $ ia:]
[PROOF STEP]
by (auto simp: dim ac_simps, induct n, auto)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < nr; j < nc\<rbrakk> \<Longrightarrow> row (map_mat (\<lambda>a. [:a:]) A) i \<bullet> col (map_mat (\<lambda>a. [:a:]) B) j = [:row A i \<bullet> col B j:]

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < nr; ?j2 < nc\<rbrakk> \<Longrightarrow> row (map_mat (\<lambda>a. [:a:]) A) ?i2 \<bullet> col (map_mat (\<lambda>a. [:a:]) B) ?j2 = [:row A ?i2 \<bullet> col B ?j2:]

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
note id = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < nr; ?j2 < nc\<rbrakk> \<Longrightarrow> row (map_mat (\<lambda>a. [:a:]) A) ?i2 \<bullet> col (map_mat (\<lambda>a. [:a:]) B) ?j2 = [:row A ?i2 \<bullet> col B ?j2:]

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < nr; ?j2 < nc\<rbrakk> \<Longrightarrow> row (map_mat (\<lambda>a. [:a:]) A) ?i2 \<bullet> col (map_mat (\<lambda>a. [:a:]) B) ?j2 = [:row A ?i2 \<bullet> col B ?j2:]

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
have "i < nr \<Longrightarrow> j < nc \<Longrightarrow>
      [:(row A i \<bullet> col B j):] * p = row (map_mat (\<lambda> a. [: a :] * p) A) i \<bullet> col (map_mat (\<lambda>a. [:a:]) B) j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < nr; j < nc\<rbrakk> \<Longrightarrow> [:row A i \<bullet> col B j:] * p = row (map_mat (\<lambda>a. [:a:] * p) A) i \<bullet> col (map_mat (\<lambda>a. [:a:]) B) j
[PROOF STEP]
unfolding scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < nr; j < nc\<rbrakk> \<Longrightarrow> [:\<Sum>ia = 0..<dim_vec (col B j). row A i $ ia * col B j $ ia:] * p = (\<Sum>ia = 0..<dim_vec (col (map_mat (\<lambda>a. [:a:]) B) j). row (map_mat (\<lambda>a. [:a:] * p) A) i $ ia * col (map_mat (\<lambda>a. [:a:]) B) j $ ia)
[PROOF STEP]
by (auto simp: dim ac_simps smult_sum)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < nr; j < nc\<rbrakk> \<Longrightarrow> [:row A i \<bullet> col B j:] * p = row (map_mat (\<lambda>a. [:a:] * p) A) i \<bullet> col (map_mat (\<lambda>a. [:a:]) B) j

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < nr; ?j2 < nc\<rbrakk> \<Longrightarrow> [:row A ?i2 \<bullet> col B ?j2:] * p = row (map_mat (\<lambda>a. [:a:] * p) A) ?i2 \<bullet> col (map_mat (\<lambda>a. [:a:]) B) ?j2

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
note left = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < nr; ?j2 < nc\<rbrakk> \<Longrightarrow> [:row A ?i2 \<bullet> col B ?j2:] * p = row (map_mat (\<lambda>a. [:a:] * p) A) ?i2 \<bullet> col (map_mat (\<lambda>a. [:a:]) B) ?j2

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < nr; ?j2 < nc\<rbrakk> \<Longrightarrow> [:row A ?i2 \<bullet> col B ?j2:] * p = row (map_mat (\<lambda>a. [:a:] * p) A) ?i2 \<bullet> col (map_mat (\<lambda>a. [:a:]) B) ?j2

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
have "i < nr \<Longrightarrow> j < nc \<Longrightarrow>
      [:(row A i \<bullet> col B j):] * p = row (map_mat (\<lambda> a. [: a :]) A) i \<bullet> col (map_mat (\<lambda>a. [:a:] * p) B) j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < nr; j < nc\<rbrakk> \<Longrightarrow> [:row A i \<bullet> col B j:] * p = row (map_mat (\<lambda>a. [:a:]) A) i \<bullet> col (map_mat (\<lambda>a. [:a:] * p) B) j
[PROOF STEP]
unfolding scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < nr; j < nc\<rbrakk> \<Longrightarrow> [:\<Sum>ia = 0..<dim_vec (col B j). row A i $ ia * col B j $ ia:] * p = (\<Sum>ia = 0..<dim_vec (col (map_mat (\<lambda>a. [:a:] * p) B) j). row (map_mat (\<lambda>a. [:a:]) A) i $ ia * col (map_mat (\<lambda>a. [:a:] * p) B) j $ ia)
[PROOF STEP]
by (auto simp: dim ac_simps smult_sum)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < nr; j < nc\<rbrakk> \<Longrightarrow> [:row A i \<bullet> col B j:] * p = row (map_mat (\<lambda>a. [:a:]) A) i \<bullet> col (map_mat (\<lambda>a. [:a:] * p) B) j

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < nr; ?j2 < nc\<rbrakk> \<Longrightarrow> [:row A ?i2 \<bullet> col B ?j2:] * p = row (map_mat (\<lambda>a. [:a:]) A) ?i2 \<bullet> col (map_mat (\<lambda>a. [:a:] * p) B) ?j2

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
note right = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < nr; ?j2 < nc\<rbrakk> \<Longrightarrow> [:row A ?i2 \<bullet> col B ?j2:] * p = row (map_mat (\<lambda>a. [:a:]) A) ?i2 \<bullet> col (map_mat (\<lambda>a. [:a:] * p) B) ?j2

goal (3 subgoals):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 3. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
show ?id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B
[PROOF STEP]
by (rule eq_matI, insert id, auto simp: dim)
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:]) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:]) B

goal (2 subgoals):
 1. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
 2. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
show ?left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B
[PROOF STEP]
by (rule eq_matI, insert left, auto simp: dim)
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:] * p) A * map_mat (\<lambda>a. [:a:]) B

goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
show ?right
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B
[PROOF STEP]
by (rule eq_matI, insert right, auto simp: dim)
[PROOF STATE]
proof (state)
this:
map_mat (\<lambda>a. [:a:] * p) (A * B) = map_mat (\<lambda>a. [:a:]) A * map_mat (\<lambda>a. [:a:] * p) B

goal:
No subgoals!
[PROOF STEP]
qed