[STATEMENT]
lemma index_mat_multrow[simp]: 
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> mat_multrow_gen mul k a A $$ (i,j) = (if k = i then mul a (A $$ (i,j)) else A $$ (i,j))"
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> mat_multrow_gen mul i a A $$ (i,j) = mul a (A $$ (i,j))"
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> k \<noteq> i \<Longrightarrow> mat_multrow_gen mul k a A $$ (i,j) = A $$ (i,j)"
  "dim_row (mat_multrow_gen mul k a A) = dim_row A" "dim_col (mat_multrow_gen mul k a A) = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat_multrow_gen mul k a A $$ (i, j) = (if k = i then mul a (A $$ (i, j)) else A $$ (i, j))) &&& (\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat_multrow_gen mul i a A $$ (i, j) = mul a (A $$ (i, j)))) &&& (\<lbrakk>i < dim_row A; j < dim_col A; k \<noteq> i\<rbrakk> \<Longrightarrow> mat_multrow_gen mul k a A $$ (i, j) = A $$ (i, j)) &&& dim_row (mat_multrow_gen mul k a A) = dim_row A &&& dim_col (mat_multrow_gen mul k a A) = dim_col A
[PROOF STEP]
unfolding mat_multrow_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then mul a (A $$ (i, j)) else A $$ (i, j)) $$ (i, j) = (if k = i then mul a (A $$ (i, j)) else A $$ (i, j))) &&& (\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>(ia, j). if i = ia then mul a (A $$ (ia, j)) else A $$ (ia, j)) $$ (i, j) = mul a (A $$ (i, j)))) &&& (\<lbrakk>i < dim_row A; j < dim_col A; k \<noteq> i\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then mul a (A $$ (i, j)) else A $$ (i, j)) $$ (i, j) = A $$ (i, j)) &&& dim_row (mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then mul a (A $$ (i, j)) else A $$ (i, j))) = dim_row A &&& dim_col (mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then mul a (A $$ (i, j)) else A $$ (i, j))) = dim_col A
[PROOF STEP]
by auto