[STATEMENT]
lemma split_block_hermitian_4:
  assumes "hermitian A"
  and "n \<le> dim_row A"
and "(A1, A2, A3, A4) = split_block A n n"
shows "hermitian A4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hermitian A4
[PROOF STEP]
unfolding hermitian_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex_Matrix.adjoint A4 = A4
[PROOF STEP]
proof (rule eq_matI, auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
 2. dim_col A4 = dim_row A4
 3. dim_row A4 = dim_col A4
[PROOF STEP]
have arc: "dim_row A = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A = dim_col A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n

goal (1 subgoal):
 1. dim_row A = dim_col A
[PROOF STEP]
by (metis carrier_matD(2) hermitian_square)
[PROOF STATE]
proof (state)
this:
dim_row A = dim_col A

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
 2. dim_col A4 = dim_row A4
 3. dim_row A4 = dim_col A4
[PROOF STEP]
thus "dim_col A4 = dim_row A4"
[PROOF STATE]
proof (prove)
using this:
dim_row A = dim_col A

goal (1 subgoal):
 1. dim_col A4 = dim_row A4
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dim_row A = dim_col A
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n

goal (1 subgoal):
 1. dim_col A4 = dim_row A4
[PROOF STEP]
unfolding split_block_def Let_def
[PROOF STATE]
proof (prove)
using this:
dim_row A = dim_col A
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = (Matrix.mat n n (($$) A), Matrix.mat n (dim_col A - n) (\<lambda>(i, j). A $$ (i, j + n)), Matrix.mat (dim_row A - n) n (\<lambda>(i, j). A $$ (i + n, j)), Matrix.mat (dim_row A - n) (dim_col A - n) (\<lambda>(i, j). A $$ (i + n, j + n)))

goal (1 subgoal):
 1. dim_col A4 = dim_row A4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_col A4 = dim_row A4

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
 2. dim_row A4 = dim_col A4
[PROOF STEP]
thus "dim_row A4 = dim_col A4"
[PROOF STATE]
proof (prove)
using this:
dim_col A4 = dim_row A4

goal (1 subgoal):
 1. dim_row A4 = dim_col A4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_row A4 = dim_col A4

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
show "\<And>i j. i < dim_row A4 \<Longrightarrow> j < dim_col A4 \<Longrightarrow> 
    Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
assume "i < dim_row A4" and "j < dim_col A4"
[PROOF STATE]
proof (state)
this:
i < dim_row A4
j < dim_col A4

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
note ij = this
[PROOF STATE]
proof (state)
this:
i < dim_row A4
j < dim_col A4

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have r: "dim_row A4 = dim_row A - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A4 = dim_row A - n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n

goal (1 subgoal):
 1. dim_row A4 = dim_row A - n
[PROOF STEP]
unfolding split_block_def Let_def
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = (Matrix.mat n n (($$) A), Matrix.mat n (dim_col A - n) (\<lambda>(i, j). A $$ (i, j + n)), Matrix.mat (dim_row A - n) n (\<lambda>(i, j). A $$ (i + n, j)), Matrix.mat (dim_row A - n) (dim_col A - n) (\<lambda>(i, j). A $$ (i + n, j + n)))

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have c: "dim_col A4 = dim_col A - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col A4 = dim_col A - n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n

goal (1 subgoal):
 1. dim_col A4 = dim_col A - n
[PROOF STEP]
unfolding split_block_def Let_def
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = (Matrix.mat n n (($$) A), Matrix.mat n (dim_col A - n) (\<lambda>(i, j). A $$ (i, j + n)), Matrix.mat (dim_row A - n) n (\<lambda>(i, j). A $$ (i + n, j)), Matrix.mat (dim_row A - n) (dim_col A - n) (\<lambda>(i, j). A $$ (i + n, j + n)))

goal (1 subgoal):
 1. dim_col A4 = dim_col A - n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_col A4 = dim_col A - n

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have "Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j,i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j, i))
[PROOF STEP]
using ij r c arc
[PROOF STATE]
proof (prove)
using this:
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j, i))
[PROOF STEP]
unfolding Complex_Matrix.adjoint_def
[PROOF STATE]
proof (prove)
using this:
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. Matrix.mat (dim_col A4) (dim_row A4) (\<lambda>(i, j). conjugate (A4 $$ (j, i))) $$ (i, j) = conjugate (A4 $$ (j, i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j, i))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j, i))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have "... = conjugate (A $$ (j +n ,i+n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (A4 $$ (j, i)) = conjugate (A $$ (j + n, i + n))
[PROOF STEP]
using assms ij r c arc
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. conjugate (A4 $$ (j, i)) = conjugate (A $$ (j + n, i + n))
[PROOF STEP]
unfolding split_block_def Let_def
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = (Matrix.mat n n (($$) A), Matrix.mat n (dim_col A - n) (\<lambda>(i, j). A $$ (i, j + n)), Matrix.mat (dim_row A - n) n (\<lambda>(i, j). A $$ (i + n, j)), Matrix.mat (dim_row A - n) (dim_col A - n) (\<lambda>(i, j). A $$ (i + n, j + n)))
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. conjugate (A4 $$ (j, i)) = conjugate (A $$ (j + n, i + n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
conjugate (A4 $$ (j, i)) = conjugate (A $$ (j + n, i + n))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
conjugate (A4 $$ (j, i)) = conjugate (A $$ (j + n, i + n))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have "... = A $$ (i+n,j+n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (A $$ (j + n, i + n)) = A $$ (i + n, j + n)
[PROOF STEP]
using assms ij r c arc
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. conjugate (A $$ (j + n, i + n)) = A $$ (i + n, j + n)
[PROOF STEP]
unfolding hermitian_def Complex_Matrix.adjoint_def
[PROOF STATE]
proof (prove)
using this:
Matrix.mat (dim_col A) (dim_row A) (\<lambda>(i, j). conjugate (A $$ (j, i))) = A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n
dim_row A = dim_col A

goal (1 subgoal):
 1. conjugate (A $$ (j + n, i + n)) = A $$ (i + n, j + n)
[PROOF STEP]
by (metis index_mat(1) less_diff_conv split_conv)
[PROOF STATE]
proof (state)
this:
conjugate (A $$ (j + n, i + n)) = A $$ (i + n, j + n)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
conjugate (A $$ (j + n, i + n)) = A $$ (i + n, j + n)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
have "... = A4 $$(i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i + n, j + n) = A4 $$ (i, j)
[PROOF STEP]
using assms ij r c
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = split_block A n n
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n

goal (1 subgoal):
 1. A $$ (i + n, j + n) = A4 $$ (i, j)
[PROOF STEP]
unfolding split_block_def Let_def
[PROOF STATE]
proof (prove)
using this:
hermitian A
n \<le> dim_row A
(A1, A2, A3, A4) = (Matrix.mat n n (($$) A), Matrix.mat n (dim_col A - n) (\<lambda>(i, j). A $$ (i, j + n)), Matrix.mat (dim_row A - n) n (\<lambda>(i, j). A $$ (i + n, j)), Matrix.mat (dim_row A - n) (dim_col A - n) (\<lambda>(i, j). A $$ (i + n, j + n)))
i < dim_row A4
j < dim_col A4
dim_row A4 = dim_row A - n
dim_col A4 = dim_col A - n

goal (1 subgoal):
 1. A $$ (i + n, j + n) = A4 $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $$ (i + n, j + n) = A4 $$ (i, j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row A4; j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
show "Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)"
[PROOF STATE]
proof (prove)
using this:
Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)

goal (1 subgoal):
 1. Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < dim_row A4; ?j < dim_col A4\<rbrakk> \<Longrightarrow> Complex_Matrix.adjoint A4 $$ (?i, ?j) = A4 $$ (?i, ?j)

goal:
No subgoals!
[PROOF STEP]
qed