[STATEMENT]
lemma similar_matrix_rotation: assumes ev: "eigen_value cA \<alpha>" and \<alpha>: "cmod \<alpha> = sr"
  shows "similar_matrix (cis (Arg \<alpha>) *k cA) cA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
from ev
[PROOF STATE]
proof (chain)
picking this:
eigen_value cA \<alpha>
[PROOF STEP]
obtain y where ev: "eigen_vector cA y \<alpha>"
[PROOF STATE]
proof (prove)
using this:
eigen_value cA \<alpha>

goal (1 subgoal):
 1. (\<And>y. eigen_vector cA y \<alpha> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eigen_value_def
[PROOF STATE]
proof (prove)
using this:
\<exists>v. eigen_vector cA v \<alpha>

goal (1 subgoal):
 1. (\<And>y. eigen_vector cA y \<alpha> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_vector cA y \<alpha>

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
let ?y = "norm_v y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
note maps = map_vector_def map_matrix_def
[PROOF STATE]
proof (state)
this:
map_vector ?f ?v \<equiv> \<chi>i. ?f (?v $h i)
HMA_Connect.map_matrix ?f ?A \<equiv> \<chi>i. map_vector ?f (?A $h i)

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
define yp where "yp = norm_v y"
[PROOF STATE]
proof (state)
this:
yp = map_vector cmod y

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
let ?yp = "map_vector c yp"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have yp: "yp \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yp \<in> X
[PROOF STEP]
unfolding yp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vector cmod y \<in> X
[PROOF STEP]
by (rule norm_v_X[OF ev])
[PROOF STATE]
proof (state)
this:
yp \<in> X

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
from ev[unfolded eigen_vector_def]
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> 0 \<and> cA *v y = \<alpha> *s y
[PROOF STEP]
have ev_y: "cA *v y = \<alpha> *s y"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> 0 \<and> cA *v y = \<alpha> *s y

goal (1 subgoal):
 1. cA *v y = \<alpha> *s y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cA *v y = \<alpha> *s y

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
from ev_le_vec[OF ev, unfolded \<alpha>, folded yp_def]
[PROOF STATE]
proof (chain)
picking this:
le_vec (sr *s yp) (A *v yp)
[PROOF STEP]
have 1: "le_vec (sr *s yp) (A *v yp)"
[PROOF STATE]
proof (prove)
using this:
le_vec (sr *s yp) (A *v yp)

goal (1 subgoal):
 1. le_vec (sr *s yp) (A *v yp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
le_vec (sr *s yp) (A *v yp)

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
from rho_le_x_Ax_imp_rho_le_rx[OF yp 1]
[PROOF STATE]
proof (chain)
picking this:
sr \<le> r yp
[PROOF STEP]
have "sr \<le> r yp"
[PROOF STATE]
proof (prove)
using this:
sr \<le> r yp

goal (1 subgoal):
 1. sr \<le> r yp
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sr \<le> r yp

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
with ev_inequalities[OF ev, folded yp_def]
[PROOF STATE]
proof (chain)
picking this:
cmod \<alpha> \<le> r yp
r yp \<le> sr
sr \<le> r yp
[PROOF STEP]
have 2: "r yp = sr"
[PROOF STATE]
proof (prove)
using this:
cmod \<alpha> \<le> r yp
r yp \<le> sr
sr \<le> r yp

goal (1 subgoal):
 1. r yp = sr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r yp = sr

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have ev_yp: "A *v yp = sr *s yp"
    and pos_yp: "lt_vec 0 yp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v yp = sr *s yp &&& lt_vec 0 yp
[PROOF STEP]
using sr_imp_eigen_vector_main[OF yp 2] sr_u_pos[OF yp 2]
[PROOF STATE]
proof (prove)
using this:
sr *s yp = A *v yp
lt_vec 0 yp

goal (1 subgoal):
 1. A *v yp = sr *s yp &&& lt_vec 0 yp
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A *v yp = sr *s yp
lt_vec 0 yp

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
define D where "D = diagvector (\<lambda> j. cis (Arg (y $ j)))"
[PROOF STATE]
proof (state)
this:
D = diagvector (\<lambda>j. cis (Arg (y $h j)))

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
define inv_D where "inv_D = diagvector (\<lambda> j. cis (- Arg (y $ j)))"
[PROOF STATE]
proof (state)
this:
inv_D = diagvector (\<lambda>j. cis (- Arg (y $h j)))

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have DD: "inv_D ** D = mat 1" "D ** inv_D = mat 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_D ** D = mat 1 &&& D ** inv_D = mat 1
[PROOF STEP]
unfolding D_def inv_D_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diagvector (\<lambda>j. cis (- Arg (y $h j))) ** diagvector (\<lambda>j. cis (Arg (y $h j))) = mat 1 &&& diagvector (\<lambda>j. cis (Arg (y $h j))) ** diagvector (\<lambda>j. cis (- Arg (y $h j))) = mat 1
[PROOF STEP]
by (auto simp add: diagvector_eq_mat cis_mult)
[PROOF STATE]
proof (state)
this:
inv_D ** D = mat 1
D ** inv_D = mat 1

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inv_D ** D = mat 1
D ** inv_D = mat 1

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "(D *v ?yp) $ i = cis (Arg (y $ i)) * c (cmod (y $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (D *v map_vector complex_of_real yp) $h i = cis (Arg (y $h i)) * complex_of_real (cmod (y $h i))
[PROOF STEP]
unfolding D_def yp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (diagvector (\<lambda>j. cis (Arg (y $h j))) *v map_vector complex_of_real (map_vector cmod y)) $h i = cis (Arg (y $h i)) * complex_of_real (cmod (y $h i))
[PROOF STEP]
by (simp add: maps)
[PROOF STATE]
proof (state)
this:
(D *v map_vector complex_of_real yp) $h i = cis (Arg (y $h i)) * complex_of_real (cmod (y $h i))

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(D *v map_vector complex_of_real yp) $h i = cis (Arg (y $h i)) * complex_of_real (cmod (y $h i))

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "\<dots> = y $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (Arg (y $h i)) * complex_of_real (cmod (y $h i)) = y $h i
[PROOF STEP]
by (simp add: cis_mult_cmod_id)
[PROOF STATE]
proof (state)
this:
cis (Arg (y $h i)) * complex_of_real (cmod (y $h i)) = y $h i

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cis (Arg (y $h i)) * complex_of_real (cmod (y $h i)) = y $h i

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
note calculation
[PROOF STATE]
proof (state)
this:
(D *v map_vector complex_of_real yp) $h i = y $h i

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(D *v map_vector complex_of_real yp) $h ?i2 = y $h ?i2

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
hence y_D_yp: "y = D *v ?yp"
[PROOF STATE]
proof (prove)
using this:
(D *v map_vector complex_of_real yp) $h ?i2 = y $h ?i2

goal (1 subgoal):
 1. y = D *v map_vector complex_of_real yp
[PROOF STEP]
by (auto simp: vec_eq_iff)
[PROOF STATE]
proof (state)
this:
y = D *v map_vector complex_of_real yp

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
define \<phi> where "\<phi> = Arg \<alpha>"
[PROOF STATE]
proof (state)
this:
\<phi> = Arg \<alpha>

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
let ?\<phi> = "cis (- \<phi>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have [simp]: "cis (- \<phi>) * rcis sr \<phi> = sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (- \<phi>) * rcis sr \<phi> = complex_of_real sr
[PROOF STEP]
unfolding cis_rcis_eq rcis_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rcis (1 * sr) (- \<phi> + \<phi>) = complex_of_real sr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cis (- \<phi>) * rcis sr \<phi> = complex_of_real sr

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have \<alpha>: "\<alpha> = rcis sr \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = rcis sr \<phi>
[PROOF STEP]
unfolding \<phi>_def \<alpha>[symmetric] rcis_cmod_Arg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = \<alpha>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<alpha> = rcis sr \<phi>

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
define F where "F = ?\<phi> *k (inv_D ** cA ** D)"
[PROOF STATE]
proof (state)
this:
F = cis (- \<phi>) *k (inv_D ** cA ** D)

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "cA *v (D *v ?yp) = \<alpha> *s y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cA *v (D *v map_vector complex_of_real yp) = \<alpha> *s y
[PROOF STEP]
unfolding y_D_yp[symmetric] ev_y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> *s y = \<alpha> *s y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cA *v (D *v map_vector complex_of_real yp) = \<alpha> *s y

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cA *v (D *v map_vector complex_of_real yp) = \<alpha> *s y

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "inv_D *v \<dots> = \<alpha> *s ?yp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_D *v (\<alpha> *s y) = \<alpha> *s map_vector complex_of_real yp
[PROOF STEP]
unfolding vector_smult_distrib y_D_yp matrix_vector_mul_assoc DD matrix_vector_mul_lid
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> *s map_vector complex_of_real yp = \<alpha> *s map_vector complex_of_real yp
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
inv_D *v (\<alpha> *s y) = \<alpha> *s map_vector complex_of_real yp

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inv_D *v (\<alpha> *s y) = \<alpha> *s map_vector complex_of_real yp

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "?\<phi> *s \<dots> = sr *s ?yp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (- \<phi>) *s (\<alpha> *s map_vector complex_of_real yp) = complex_of_real sr *s map_vector complex_of_real yp
[PROOF STEP]
unfolding \<alpha>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (- \<phi>) *s (rcis sr \<phi> *s map_vector complex_of_real yp) = complex_of_real sr *s map_vector complex_of_real yp
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cis (- \<phi>) *s (\<alpha> *s map_vector complex_of_real yp) = complex_of_real sr *s map_vector complex_of_real yp

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cis (- \<phi>) *s (\<alpha> *s map_vector complex_of_real yp) = complex_of_real sr *s map_vector complex_of_real yp

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "\<dots> = map_vector c (sr *s yp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real sr *s map_vector complex_of_real yp = map_vector complex_of_real (sr *s yp)
[PROOF STEP]
unfolding vec_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (complex_of_real sr *s map_vector complex_of_real yp) $h i = map_vector complex_of_real (sr *s yp) $h i
[PROOF STEP]
by (auto simp: maps)
[PROOF STATE]
proof (state)
this:
complex_of_real sr *s map_vector complex_of_real yp = map_vector complex_of_real (sr *s yp)

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
complex_of_real sr *s map_vector complex_of_real yp = map_vector complex_of_real (sr *s yp)

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "\<dots> = cA *v ?yp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vector complex_of_real (sr *s yp) = cA *v map_vector complex_of_real yp
[PROOF STEP]
unfolding ev_yp[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vector complex_of_real (A *v yp) = cA *v map_vector complex_of_real yp
[PROOF STEP]
by (auto simp: maps matrix_vector_mult_def)
[PROOF STATE]
proof (state)
this:
map_vector complex_of_real (sr *s yp) = cA *v map_vector complex_of_real yp

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cis (- \<phi>) *s (inv_D *v (cA *v (D *v map_vector complex_of_real yp))) = cA *v map_vector complex_of_real yp
[PROOF STEP]
have F: "F *v ?yp = cA *v ?yp"
[PROOF STATE]
proof (prove)
using this:
cis (- \<phi>) *s (inv_D *v (cA *v (D *v map_vector complex_of_real yp))) = cA *v map_vector complex_of_real yp

goal (1 subgoal):
 1. F *v map_vector complex_of_real yp = cA *v map_vector complex_of_real yp
[PROOF STEP]
unfolding F_def matrix_scalar_vector_ac[symmetric]
[PROOF STATE]
proof (prove)
using this:
cis (- \<phi>) *s (inv_D *v (cA *v (D *v map_vector complex_of_real yp))) = cA *v map_vector complex_of_real yp

goal (1 subgoal):
 1. inv_D ** cA ** D *v (cis (- \<phi>) *s map_vector complex_of_real yp) = cA *v map_vector complex_of_real yp
[PROOF STEP]
unfolding matrix_vector_mul_assoc[symmetric] vector_smult_distrib
[PROOF STATE]
proof (prove)
using this:
cis (- \<phi>) *s (inv_D *v (cA *v (D *v map_vector complex_of_real yp))) = cA *v map_vector complex_of_real yp

goal (1 subgoal):
 1. cis (- \<phi>) *s (inv_D *v (cA *v (D *v map_vector complex_of_real yp))) = cA *v map_vector complex_of_real yp
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
F *v map_vector complex_of_real yp = cA *v map_vector complex_of_real yp

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have prod: "inv_D ** cA ** D = (\<chi> i j. cis (- Arg (y $ i)) * cA $ i $ j * cis (Arg (y $ j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_D ** cA ** D = (\<chi>i j. cis (- Arg (y $h i)) * cA $h i $h j * cis (Arg (y $h j)))
[PROOF STEP]
unfolding inv_D_def D_def diagvector_mult_right diagvector_mult_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. (\<chi>i j. cis (- Arg (y $h i)) * cA $h i $h j) $h i $h j * cis (Arg (y $h j))) = (\<chi>i j. cis (- Arg (y $h i)) * cA $h i $h j * cis (Arg (y $h j)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inv_D ** cA ** D = (\<chi>i j. cis (- Arg (y $h i)) * cA $h i $h j * cis (Arg (y $h j)))

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inv_D ** cA ** D = (\<chi>i j. cis (- Arg (y $h i)) * cA $h i $h j * cis (Arg (y $h j)))

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "cmod (F $ i $ j) = cmod (?\<phi> * cA $h i $h j * (cis (- Arg (y $h i)) * cis (Arg (y $h j))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (F $h i $h j) = cmod (cis (- \<phi>) * cA $h i $h j * (cis (- Arg (y $h i)) * cis (Arg (y $h j))))
[PROOF STEP]
unfolding F_def prod vec_lambda_beta matrix_scalar_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (cis (- \<phi>) * (cis (- Arg (y $h i)) * cA $h i $h j * cis (Arg (y $h j)))) = cmod (cis (- \<phi>) * cA $h i $h j * (cis (- Arg (y $h i)) * cis (Arg (y $h j))))
[PROOF STEP]
by (simp only: ac_simps)
[PROOF STATE]
proof (state)
this:
cmod (F $h i $h j) = cmod (cis (- \<phi>) * cA $h i $h j * (cis (- Arg (y $h i)) * cis (Arg (y $h j))))

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (F $h i $h j) = cmod (cis (- \<phi>) * cA $h i $h j * (cis (- Arg (y $h i)) * cis (Arg (y $h j))))

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "\<dots> = A $ i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (cis (- \<phi>) * cA $h i $h j * (cis (- Arg (y $h i)) * cis (Arg (y $h j)))) = A $h i $h j
[PROOF STEP]
unfolding cis_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (cis (- \<phi>) * cA $h i $h j * cis (- Arg (y $h i) + Arg (y $h j))) = A $h i $h j
[PROOF STEP]
unfolding norm_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (cis (- \<phi>)) * cmod (cA $h i $h j) * cmod (cis (- Arg (y $h i) + Arg (y $h j))) = A $h i $h j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod (cis (- \<phi>) * cA $h i $h j * (cis (- Arg (y $h i)) * cis (Arg (y $h j)))) = A $h i $h j

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (cis (- \<phi>) * cA $h i $h j * (cis (- Arg (y $h i)) * cis (Arg (y $h j)))) = A $h i $h j

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
note calculation
[PROOF STATE]
proof (state)
this:
cmod (F $h i $h j) = A $h i $h j

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
cmod (F $h ?i2 $h ?j2) = A $h ?i2 $h ?j2

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
hence FA: "map_matrix norm F = A"
[PROOF STATE]
proof (prove)
using this:
cmod (F $h ?i2 $h ?j2) = A $h ?i2 $h ?j2

goal (1 subgoal):
 1. HMA_Connect.map_matrix cmod F = A
[PROOF STEP]
unfolding maps
[PROOF STATE]
proof (prove)
using this:
cmod (F $h ?i2 $h ?j2) = A $h ?i2 $h ?j2

goal (1 subgoal):
 1. (\<chi>i ia. cmod (F $h i $h ia)) = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HMA_Connect.map_matrix cmod F = A

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
let ?F = "map_matrix c (map_matrix norm F)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
let ?G = "?F - F"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
let ?Re = "map_matrix Re"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
from F[folded FA]
[PROOF STATE]
proof (chain)
picking this:
F *v map_vector complex_of_real yp = HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) *v map_vector complex_of_real yp
[PROOF STEP]
have 0: "?G *v ?yp = 0"
[PROOF STATE]
proof (prove)
using this:
F *v map_vector complex_of_real yp = HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) *v map_vector complex_of_real yp

goal (1 subgoal):
 1. (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v map_vector complex_of_real yp = 0
[PROOF STEP]
unfolding matrix_diff_vect_distrib
[PROOF STATE]
proof (prove)
using this:
F *v map_vector complex_of_real yp = HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) *v map_vector complex_of_real yp

goal (1 subgoal):
 1. HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) *v map_vector complex_of_real yp - F *v map_vector complex_of_real yp = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v map_vector complex_of_real yp = 0

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "?Re ?G *v yp = map_vector Re (?G *v ?yp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_Connect.map_matrix Re (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v yp = map_vector Re ((HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v map_vector complex_of_real yp)
[PROOF STEP]
unfolding maps matrix_vector_mult_def vec_lambda_beta Re_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. \<Sum>j\<in>UNIV. Re (((\<chi>i ia. complex_of_real (cmod (F $h i $h ia))) - F) $h i $h j) * yp $h j) = (\<chi>i. \<Sum>x\<in>UNIV. Re (((\<chi>i ia. complex_of_real (cmod (F $h i $h ia))) - F) $h i $h x * complex_of_real (yp $h x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HMA_Connect.map_matrix Re (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v yp = map_vector Re ((HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v map_vector complex_of_real yp)

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
HMA_Connect.map_matrix Re (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v yp = map_vector Re ((HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v map_vector complex_of_real yp)

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vector Re ((HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v map_vector complex_of_real yp) = 0
[PROOF STEP]
unfolding 0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vector Re 0 = 0
[PROOF STEP]
by (simp add: vec_eq_iff maps)
[PROOF STATE]
proof (state)
this:
map_vector Re ((HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v map_vector complex_of_real yp) = 0

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
HMA_Connect.map_matrix Re (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v yp = 0
[PROOF STEP]
have 0: "?Re ?G *v yp = 0"
[PROOF STATE]
proof (prove)
using this:
HMA_Connect.map_matrix Re (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v yp = 0

goal (1 subgoal):
 1. HMA_Connect.map_matrix Re (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v yp = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
HMA_Connect.map_matrix Re (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) *v yp = 0

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "?Re ?G = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_Connect.map_matrix Re (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) = 0
[PROOF STEP]
by (rule pos_matrix_mult_0[OF _ pos_yp 0], auto simp: maps complex_Re_le_cmod)
[PROOF STATE]
proof (state)
this:
HMA_Connect.map_matrix Re (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) = 0

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
hence "?F = F"
[PROOF STATE]
proof (prove)
using this:
HMA_Connect.map_matrix Re (HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) - F) = 0

goal (1 subgoal):
 1. HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) = F
[PROOF STEP]
by (auto simp: maps vec_eq_iff cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) = F

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
with FA
[PROOF STATE]
proof (chain)
picking this:
HMA_Connect.map_matrix cmod F = A
HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) = F
[PROOF STEP]
have AF: "cA = F"
[PROOF STATE]
proof (prove)
using this:
HMA_Connect.map_matrix cmod F = A
HMA_Connect.map_matrix complex_of_real (HMA_Connect.map_matrix cmod F) = F

goal (1 subgoal):
 1. cA = F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cA = F

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
from arg_cong[OF this, of "\<lambda> A. cis \<phi> *k A"]
[PROOF STATE]
proof (chain)
picking this:
cis \<phi> *k cA = cis \<phi> *k F
[PROOF STEP]
have sim: "cis \<phi> *k cA = inv_D ** cA ** D"
[PROOF STATE]
proof (prove)
using this:
cis \<phi> *k cA = cis \<phi> *k F

goal (1 subgoal):
 1. cis \<phi> *k cA = inv_D ** cA ** D
[PROOF STEP]
unfolding F_def matrix.scale_scale cis_mult
[PROOF STATE]
proof (prove)
using this:
cis \<phi> *k cA = cis (\<phi> + - \<phi>) *k (inv_D ** cA ** D)

goal (1 subgoal):
 1. cis \<phi> *k cA = inv_D ** cA ** D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cis \<phi> *k cA = inv_D ** cA ** D

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "similar_matrix (cis \<phi> *k cA) cA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. similar_matrix (cis \<phi> *k cA) cA
[PROOF STEP]
unfolding similar_matrix_def similar_matrix_wit_def
     sim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P Q. P ** Q = mat 1 \<and> Q ** P = mat 1 \<and> inv_D ** cA ** D = P ** cA ** Q
[PROOF STEP]
by (rule exI[of _ inv_D], rule exI[of _ D], auto simp: DD)
[PROOF STATE]
proof (state)
this:
similar_matrix (cis \<phi> *k cA) cA

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
similar_matrix (cis \<phi> *k cA) cA

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
unfolding \<phi>_def
[PROOF STATE]
proof (prove)
using this:
similar_matrix (cis (Arg \<alpha>) *k cA) cA

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
similar_matrix (cis (Arg \<alpha>) *k cA) cA

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma assumes ev: "eigen_value cA \<alpha>" and \<alpha>: "cmod \<alpha> = sr"
  shows maximal_eigen_value_order_1: "order \<alpha> (charpoly cA) = 1"
    and maximal_eigen_value_rotation: "eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x"
      "eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order \<alpha> (charpoly cA) = 1 &&& eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x &&& eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
let ?a = "cis (Arg \<alpha>)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
let ?p = "charpoly cA"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
from similar_matrix_rotation[OF ev \<alpha>]
[PROOF STATE]
proof (chain)
picking this:
similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
have "similar_matrix (?a *k cA) cA"
[PROOF STATE]
proof (prove)
using this:
similar_matrix (cis (Arg \<alpha>) *k cA) cA

goal (1 subgoal):
 1. similar_matrix (cis (Arg \<alpha>) *k cA) cA
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
similar_matrix (cis (Arg \<alpha>) *k cA) cA

goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
from similar_matrix_charpoly[OF this]
[PROOF STATE]
proof (chain)
picking this:
charpoly (cis (Arg \<alpha>) *k cA) = charpoly cA
[PROOF STEP]
have id: "charpoly (?a *k cA) = ?p"
[PROOF STATE]
proof (prove)
using this:
charpoly (cis (Arg \<alpha>) *k cA) = charpoly cA

goal (1 subgoal):
 1. charpoly (cis (Arg \<alpha>) *k cA) = charpoly cA
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
charpoly (cis (Arg \<alpha>) *k cA) = charpoly cA

goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
have a: "?a \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (Arg \<alpha>) \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cis (Arg \<alpha>) \<noteq> 0

goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
from order_charpoly_smult[OF this, of _ cA, unfolded id]
[PROOF STATE]
proof (chain)
picking this:
order ?x (charpoly cA) = order (?x / cis (Arg \<alpha>)) (charpoly cA)
[PROOF STEP]
have order_neg: "order x ?p = order (x / ?a) ?p" for x
[PROOF STATE]
proof (prove)
using this:
order ?x (charpoly cA) = order (?x / cis (Arg \<alpha>)) (charpoly cA)

goal (1 subgoal):
 1. order x (charpoly cA) = order (x / cis (Arg \<alpha>)) (charpoly cA)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
order ?x (charpoly cA) = order (?x / cis (Arg \<alpha>)) (charpoly cA)

goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
have order_pos: "order x ?p = order (x * ?a) ?p" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order x (charpoly cA) = order (x * cis (Arg \<alpha>)) (charpoly cA)
[PROOF STEP]
using order_neg[symmetric, of "x * ?a"]
[PROOF STATE]
proof (prove)
using this:
order (x * cis (Arg \<alpha>) / cis (Arg \<alpha>)) (charpoly cA) = order (x * cis (Arg \<alpha>)) (charpoly cA)

goal (1 subgoal):
 1. order x (charpoly cA) = order (x * cis (Arg \<alpha>)) (charpoly cA)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
order ?x (charpoly cA) = order (?x * cis (Arg \<alpha>)) (charpoly cA)

goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
note order_neg[of \<alpha>]
[PROOF STATE]
proof (state)
this:
order \<alpha> (charpoly cA) = order (\<alpha> / cis (Arg \<alpha>)) (charpoly cA)

goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
order \<alpha> (charpoly cA) = order (\<alpha> / cis (Arg \<alpha>)) (charpoly cA)

goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
have id: "\<alpha> / ?a = sr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> / cis (Arg \<alpha>) = complex_of_real sr
[PROOF STEP]
unfolding \<alpha>[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> / cis (Arg \<alpha>) = complex_of_real (cmod \<alpha>)
[PROOF STEP]
by (metis a cis_mult_cmod_id nonzero_mult_div_cancel_left)
[PROOF STATE]
proof (state)
this:
\<alpha> / cis (Arg \<alpha>) = complex_of_real sr

goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<alpha> / cis (Arg \<alpha>) = complex_of_real sr

goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
have sr: "order \<dots> ?p = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (complex_of_real sr) (charpoly cA) = 1
[PROOF STEP]
unfolding multiplicity_sr_1[symmetric] charpoly_of_real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (complex_of_real sr) (map_poly complex_of_real (charpoly A)) = order sr (charpoly A)
[PROOF STEP]
by (rule map_poly_inj_idom_divide_hom.order_hom, unfold_locales)
[PROOF STATE]
proof (state)
this:
order (complex_of_real sr) (charpoly cA) = 1

goal (3 subgoals):
 1. order \<alpha> (charpoly cA) = 1
 2. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 3. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
order \<alpha> (charpoly cA) = 1
[PROOF STEP]
show *: "order \<alpha> ?p = 1"
[PROOF STATE]
proof (prove)
using this:
order \<alpha> (charpoly cA) = 1

goal (1 subgoal):
 1. order \<alpha> (charpoly cA) = 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
order \<alpha> (charpoly cA) = 1

goal (2 subgoals):
 1. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
 2. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
show "eigen_value cA (x * ?a) = eigen_value cA x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
using order_pos
[PROOF STATE]
proof (prove)
using this:
order ?x (charpoly cA) = order (?x * cis (Arg \<alpha>)) (charpoly cA)

goal (1 subgoal):
 1. eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
unfolding eigen_value_root_charpoly order_root
[PROOF STATE]
proof (prove)
using this:
order ?x (charpoly cA) = order (?x * cis (Arg \<alpha>)) (charpoly cA)

goal (1 subgoal):
 1. (charpoly cA = 0 \<or> order (x * cis (Arg \<alpha>)) (charpoly cA) \<noteq> 0) = (charpoly cA = 0 \<or> order x (charpoly cA) \<noteq> 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_value cA (x * cis (Arg \<alpha>)) = eigen_value cA x

goal (1 subgoal):
 1. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
show "eigen_value cA (x / ?a) = eigen_value cA x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
using order_neg
[PROOF STATE]
proof (prove)
using this:
order ?x (charpoly cA) = order (?x / cis (Arg \<alpha>)) (charpoly cA)

goal (1 subgoal):
 1. eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x
[PROOF STEP]
unfolding eigen_value_root_charpoly order_root
[PROOF STATE]
proof (prove)
using this:
order ?x (charpoly cA) = order (?x / cis (Arg \<alpha>)) (charpoly cA)

goal (1 subgoal):
 1. (charpoly cA = 0 \<or> order (x / cis (Arg \<alpha>)) (charpoly cA) \<noteq> 0) = (charpoly cA = 0 \<or> order x (charpoly cA) \<noteq> 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_value cA (x / cis (Arg \<alpha>)) = eigen_value cA x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma maximal_eigen_values_group: assumes M: "M = {ev :: complex. eigen_value cA ev \<and> cmod ev = sr}"
  and a: "rcis sr \<alpha> \<in> M"
  and b: "rcis sr \<beta> \<in> M"
shows "rcis sr (\<alpha> + \<beta>) \<in> M" "rcis sr (\<alpha> - \<beta>) \<in> M" "rcis sr 0 \<in> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rcis sr (\<alpha> + \<beta>) \<in> M &&& rcis sr (\<alpha> - \<beta>) \<in> M &&& rcis sr 0 \<in> M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rcis sr (\<alpha> + \<beta>) \<in> M
 2. rcis sr (\<alpha> - \<beta>) \<in> M
 3. rcis sr 0 \<in> M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rcis sr (\<alpha> + \<beta>) \<in> M
 2. rcis sr (\<alpha> - \<beta>) \<in> M
 3. rcis sr 0 \<in> M
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rcis sr (\<alpha> + \<beta>) \<in> M
 2. rcis sr (\<alpha> - \<beta>) \<in> M
 3. rcis sr 0 \<in> M
[PROOF STEP]
assume *: "rcis sr a \<in> M"
[PROOF STATE]
proof (state)
this:
rcis sr a \<in> M

goal (3 subgoals):
 1. rcis sr (\<alpha> + \<beta>) \<in> M
 2. rcis sr (\<alpha> - \<beta>) \<in> M
 3. rcis sr 0 \<in> M
[PROOF STEP]
have id: "cis (Arg (rcis sr a)) = cis a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (Arg (rcis sr a)) = cis a
[PROOF STEP]
by (smt * M mem_Collect_eq nonzero_mult_div_cancel_left of_real_eq_0_iff
         rcis_cmod_Arg rcis_def sr_pos)
[PROOF STATE]
proof (state)
this:
cis (Arg (rcis sr a)) = cis a

goal (3 subgoals):
 1. rcis sr (\<alpha> + \<beta>) \<in> M
 2. rcis sr (\<alpha> - \<beta>) \<in> M
 3. rcis sr 0 \<in> M
[PROOF STEP]
from *[unfolded assms]
[PROOF STATE]
proof (chain)
picking this:
rcis sr a \<in> {ev. eigen_value cA ev \<and> cmod ev = sr}
[PROOF STEP]
have "eigen_value cA (rcis sr a)" "cmod (rcis sr a) = sr"
[PROOF STATE]
proof (prove)
using this:
rcis sr a \<in> {ev. eigen_value cA ev \<and> cmod ev = sr}

goal (1 subgoal):
 1. eigen_value cA (rcis sr a) &&& cmod (rcis sr a) = sr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_value cA (rcis sr a)
cmod (rcis sr a) = sr

goal (3 subgoals):
 1. rcis sr (\<alpha> + \<beta>) \<in> M
 2. rcis sr (\<alpha> - \<beta>) \<in> M
 3. rcis sr 0 \<in> M
[PROOF STEP]
from maximal_eigen_value_rotation[OF this, unfolded id]
[PROOF STATE]
proof (chain)
picking this:
eigen_value cA (?x * cis a) = eigen_value cA ?x
eigen_value cA (?x / cis a) = eigen_value cA ?x
[PROOF STEP]
have "eigen_value cA (x * cis a) = eigen_value cA x"
      "eigen_value cA (x / cis a) = eigen_value cA x" for x
[PROOF STATE]
proof (prove)
using this:
eigen_value cA (?x * cis a) = eigen_value cA ?x
eigen_value cA (?x / cis a) = eigen_value cA ?x

goal (1 subgoal):
 1. eigen_value cA (x * cis a) = eigen_value cA x &&& eigen_value cA (x / cis a) = eigen_value cA x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eigen_value cA (?x * cis a) = eigen_value cA ?x
eigen_value cA (?x / cis a) = eigen_value cA ?x

goal (3 subgoals):
 1. rcis sr (\<alpha> + \<beta>) \<in> M
 2. rcis sr (\<alpha> - \<beta>) \<in> M
 3. rcis sr 0 \<in> M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
rcis sr ?a3 \<in> M \<Longrightarrow> eigen_value cA (?x * cis ?a3) = eigen_value cA ?x
rcis sr ?a3 \<in> M \<Longrightarrow> eigen_value cA (?x / cis ?a3) = eigen_value cA ?x

goal (3 subgoals):
 1. rcis sr (\<alpha> + \<beta>) \<in> M
 2. rcis sr (\<alpha> - \<beta>) \<in> M
 3. rcis sr 0 \<in> M
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
rcis sr ?a3 \<in> M \<Longrightarrow> eigen_value cA (?x * cis ?a3) = eigen_value cA ?x
rcis sr ?a3 \<in> M \<Longrightarrow> eigen_value cA (?x / cis ?a3) = eigen_value cA ?x

goal (3 subgoals):
 1. rcis sr (\<alpha> + \<beta>) \<in> M
 2. rcis sr (\<alpha> - \<beta>) \<in> M
 3. rcis sr 0 \<in> M
[PROOF STEP]
from *(1)[OF b, of "rcis sr \<alpha>"] a
[PROOF STATE]
proof (chain)
picking this:
eigen_value cA (rcis sr \<alpha> * cis \<beta>) = eigen_value cA (rcis sr \<alpha>)
rcis sr \<alpha> \<in> M
[PROOF STEP]
show "rcis sr (\<alpha> + \<beta>) \<in> M"
[PROOF STATE]
proof (prove)
using this:
eigen_value cA (rcis sr \<alpha> * cis \<beta>) = eigen_value cA (rcis sr \<alpha>)
rcis sr \<alpha> \<in> M

goal (1 subgoal):
 1. rcis sr (\<alpha> + \<beta>) \<in> M
[PROOF STEP]
unfolding M
[PROOF STATE]
proof (prove)
using this:
eigen_value cA (rcis sr \<alpha> * cis \<beta>) = eigen_value cA (rcis sr \<alpha>)
rcis sr \<alpha> \<in> {ev. eigen_value cA ev \<and> cmod ev = sr}

goal (1 subgoal):
 1. rcis sr (\<alpha> + \<beta>) \<in> {ev. eigen_value cA ev \<and> cmod ev = sr}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rcis sr (\<alpha> + \<beta>) \<in> M

goal (2 subgoals):
 1. rcis sr (\<alpha> - \<beta>) \<in> M
 2. rcis sr 0 \<in> M
[PROOF STEP]
from *(2)[OF a, of "rcis sr \<alpha>"] a
[PROOF STATE]
proof (chain)
picking this:
eigen_value cA (rcis sr \<alpha> / cis \<alpha>) = eigen_value cA (rcis sr \<alpha>)
rcis sr \<alpha> \<in> M
[PROOF STEP]
show "rcis sr 0 \<in> M"
[PROOF STATE]
proof (prove)
using this:
eigen_value cA (rcis sr \<alpha> / cis \<alpha>) = eigen_value cA (rcis sr \<alpha>)
rcis sr \<alpha> \<in> M

goal (1 subgoal):
 1. rcis sr 0 \<in> M
[PROOF STEP]
unfolding M
[PROOF STATE]
proof (prove)
using this:
eigen_value cA (rcis sr \<alpha> / cis \<alpha>) = eigen_value cA (rcis sr \<alpha>)
rcis sr \<alpha> \<in> {ev. eigen_value cA ev \<and> cmod ev = sr}

goal (1 subgoal):
 1. rcis sr 0 \<in> {ev. eigen_value cA ev \<and> cmod ev = sr}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rcis sr 0 \<in> M

goal (1 subgoal):
 1. rcis sr (\<alpha> - \<beta>) \<in> M
[PROOF STEP]
from *(2)[OF b, of "rcis sr \<alpha>"] a
[PROOF STATE]
proof (chain)
picking this:
eigen_value cA (rcis sr \<alpha> / cis \<beta>) = eigen_value cA (rcis sr \<alpha>)
rcis sr \<alpha> \<in> M
[PROOF STEP]
show "rcis sr (\<alpha> - \<beta>) \<in> M"
[PROOF STATE]
proof (prove)
using this:
eigen_value cA (rcis sr \<alpha> / cis \<beta>) = eigen_value cA (rcis sr \<alpha>)
rcis sr \<alpha> \<in> M

goal (1 subgoal):
 1. rcis sr (\<alpha> - \<beta>) \<in> M
[PROOF STEP]
unfolding M
[PROOF STATE]
proof (prove)
using this:
eigen_value cA (rcis sr \<alpha> / cis \<beta>) = eigen_value cA (rcis sr \<alpha>)
rcis sr \<alpha> \<in> {ev. eigen_value cA ev \<and> cmod ev = sr}

goal (1 subgoal):
 1. rcis sr (\<alpha> - \<beta>) \<in> {ev. eigen_value cA ev \<and> cmod ev = sr}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rcis sr (\<alpha> - \<beta>) \<in> M

goal:
No subgoals!
[PROOF STEP]
qed