[STATEMENT]
lemma col_space_eq:
  assumes A: "A \<in> carrier_mat n nc"
  shows "col_space A = {y\<in>carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
let ?ws = "cols A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
have set_cols_in: "set (cols A) \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (cols A) \<subseteq> carrier_vec n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n nc

goal (1 subgoal):
 1. set (cols A) \<subseteq> carrier_vec n
[PROOF STEP]
unfolding cols_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n nc

goal (1 subgoal):
 1. set (map (col A) [0..<dim_col A]) \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (cols A) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
have "lincomb f S \<in> carrier_vec (dim_row A)" if "finite S" and S: "S \<subseteq> set (cols A)" for f S
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f S \<in> carrier_vec (dim_row A)
[PROOF STEP]
using lincomb_closed A
[PROOF STATE]
proof (prove)
using this:
?S \<subseteq> carrier_vec n \<Longrightarrow> lincomb ?a ?S \<in> carrier_vec n
A \<in> carrier_mat n nc

goal (1 subgoal):
 1. lincomb f S \<in> carrier_vec (dim_row A)
[PROOF STEP]
by (metis (full_types) S carrier_matD(1) cols_dim lincomb_closed subsetCE subsetI)
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite ?S1; ?S1 \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> lincomb ?f1 ?S1 \<in> carrier_vec (dim_row A)

goal (1 subgoal):
 1. col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite ?S1; ?S1 \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> lincomb ?f1 ?S1 \<in> carrier_vec (dim_row A)

goal (1 subgoal):
 1. col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
have "\<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S"
    if fin_S: "finite S" and S: "S \<subseteq> set (cols A)" for f S
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
let ?g = "(\<lambda>v. if v \<in> S then f v else 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
let ?g' = "(\<lambda>i. if \<exists>j<i. ?ws ! i = ?ws ! j then 0 else ?g (?ws ! i))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
let ?Z = "set ?ws - S"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
have union: "set ?ws = S \<union> ?Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (cols A) = S \<union> (set (cols A) - S)
[PROOF STEP]
using S
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> set (cols A)

goal (1 subgoal):
 1. set (cols A) = S \<union> (set (cols A) - S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (cols A) = S \<union> (set (cols A) - S)

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
have inter: "S \<inter> ?Z = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<inter> (set (cols A) - S) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<inter> (set (cols A) - S) = {}

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
have "lincomb f S = lincomb ?g S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f S = lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) S
[PROOF STEP]
by (rule lincomb_cong, insert set_cols_in A S, auto)
[PROOF STATE]
proof (state)
this:
lincomb f S = lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) S

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb f S = lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) S

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
have "... = lincomb ?g (S \<union> ?Z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) S = lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (S \<union> (set (cols A) - S))
[PROOF STEP]
by (rule lincomb_clean[symmetric],insert set_cols_in A S fin_S, auto)
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) S = lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (S \<union> (set (cols A) - S))

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) S = lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (S \<union> (set (cols A) - S))

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
have "... = lincomb ?g (set ?ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (S \<union> (set (cols A) - S)) = lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (set (cols A))
[PROOF STEP]
using union
[PROOF STATE]
proof (prove)
using this:
set (cols A) = S \<union> (set (cols A) - S)

goal (1 subgoal):
 1. lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (S \<union> (set (cols A) - S)) = lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (set (cols A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (S \<union> (set (cols A) - S)) = lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (set (cols A))

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (S \<union> (set (cols A) - S)) = lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (set (cols A))

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
have "... = lincomb_list ?g' ?ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (set (cols A)) = lincomb_list (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a)) (cols A)
[PROOF STEP]
by (rule lincomb_as_lincomb_list[OF set_cols_in])
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (set (cols A)) = lincomb_list (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a)) (cols A)

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>v. if v \<in> S then f v else (0::'a)) (set (cols A)) = lincomb_list (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a)) (cols A)

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
have "... = mat_of_cols n ?ws *\<^sub>v vec (length ?ws) ?g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a)) (cols A) = mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a))
[PROOF STEP]
by (rule lincomb_list_as_mat_mult, insert set_cols_in A, auto)
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a)) (cols A) = mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a))

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a)) (cols A) = mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a))

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
have "... = A *\<^sub>v (vec (length ?ws) ?g')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a)) = A *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a))
[PROOF STEP]
using mat_of_cols_cols A
[PROOF STATE]
proof (prove)
using this:
mat_of_cols (dim_row ?A) (cols ?A) = ?A
A \<in> carrier_mat n nc

goal (1 subgoal):
 1. mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a)) = A *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a)) = A *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a))

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb f S = A *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lincomb f S = A *\<^sub>v vec (length (cols A)) (\<lambda>i. if \<exists>j<i. cols A ! i = cols A ! j then 0::'a else if cols A ! i \<in> S then f (cols A ! i) else (0::'a))

goal (1 subgoal):
 1. \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb f S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite ?S1; ?S1 \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb ?f1 ?S1

goal (1 subgoal):
 1. col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite ?S1; ?S1 \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb ?f1 ?S1

goal (1 subgoal):
 1. col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
have "\<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)"
    if Ax: "A *\<^sub>v x \<in> carrier_vec (dim_row A)" and x: "x \<in> carrier_vec (dim_col A)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
let ?c = "\<lambda>i. x $ i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
have x_vec: "vec (length ?ws) ?c = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec (length (cols A)) (($) x) = x
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier_vec (dim_col A)

goal (1 subgoal):
 1. vec (length (cols A)) (($) x) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec (length (cols A)) (($) x) = x

goal (1 subgoal):
 1. \<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
have "A *\<^sub>v x = mat_of_cols n ?ws *\<^sub>v vec (length ?ws) ?c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>v x = mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (($) x)
[PROOF STEP]
using mat_of_cols_cols A x_vec
[PROOF STATE]
proof (prove)
using this:
mat_of_cols (dim_row ?A) (cols ?A) = ?A
A \<in> carrier_mat n nc
vec (length (cols A)) (($) x) = x

goal (1 subgoal):
 1. A *\<^sub>v x = mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (($) x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A *\<^sub>v x = mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (($) x)

goal (1 subgoal):
 1. \<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A *\<^sub>v x = mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (($) x)

goal (1 subgoal):
 1. \<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
have "... = lincomb_list ?c ?ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (($) x) = lincomb_list (($) x) (cols A)
[PROOF STEP]
by (rule lincomb_list_as_mat_mult[symmetric], insert set_cols_in A, auto)
[PROOF STATE]
proof (state)
this:
mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (($) x) = lincomb_list (($) x) (cols A)

goal (1 subgoal):
 1. \<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_cols n (cols A) *\<^sub>v vec (length (cols A)) (($) x) = lincomb_list (($) x) (cols A)

goal (1 subgoal):
 1. \<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
have "... = lincomb (mk_coeff ?ws ?c) (set ?ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (($) x) (cols A) = lincomb (mk_coeff (cols A) (($) x)) (set (cols A))
[PROOF STEP]
by (rule lincomb_list_as_lincomb, insert set_cols_in A, auto)
[PROOF STATE]
proof (state)
this:
lincomb_list (($) x) (cols A) = lincomb (mk_coeff (cols A) (($) x)) (set (cols A))

goal (1 subgoal):
 1. \<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A *\<^sub>v x = lincomb (mk_coeff (cols A) (($) x)) (set (cols A))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v x = lincomb (mk_coeff (cols A) (($) x)) (set (cols A))

goal (1 subgoal):
 1. \<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>f S. A *\<^sub>v x = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>A *\<^sub>v ?x1 \<in> carrier_vec (dim_row A); ?x1 \<in> carrier_vec (dim_col A)\<rbrakk> \<Longrightarrow> \<exists>f S. A *\<^sub>v ?x1 = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)

goal (1 subgoal):
 1. col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite ?S1; ?S1 \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> lincomb ?f1 ?S1 \<in> carrier_vec (dim_row A)
\<lbrakk>finite ?S1; ?S1 \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb ?f1 ?S1
\<lbrakk>A *\<^sub>v ?x1 \<in> carrier_vec (dim_row A); ?x1 \<in> carrier_vec (dim_col A)\<rbrakk> \<Longrightarrow> \<exists>f S. A *\<^sub>v ?x1 = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?S1; ?S1 \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> lincomb ?f1 ?S1 \<in> carrier_vec (dim_row A)
\<lbrakk>finite ?S1; ?S1 \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb ?f1 ?S1
\<lbrakk>A *\<^sub>v ?x1 \<in> carrier_vec (dim_row A); ?x1 \<in> carrier_vec (dim_col A)\<rbrakk> \<Longrightarrow> \<exists>f S. A *\<^sub>v ?x1 = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)

goal (1 subgoal):
 1. col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
unfolding col_space_def span_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?S1; ?S1 \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> lincomb ?f1 ?S1 \<in> carrier_vec (dim_row A)
\<lbrakk>finite ?S1; ?S1 \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = lincomb ?f1 ?S1
\<lbrakk>A *\<^sub>v ?x1 \<in> carrier_vec (dim_row A); ?x1 \<in> carrier_vec (dim_col A)\<rbrakk> \<Longrightarrow> \<exists>f S. A *\<^sub>v ?x1 = lincomb f S \<and> finite S \<and> S \<subseteq> set (cols A)

goal (1 subgoal):
 1. {lincomb a Aa |a Aa. finite Aa \<and> Aa \<subseteq> set (cols A)} = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col_space A = {y \<in> carrier_vec (dim_row A). \<exists>x\<in>carrier_vec (dim_col A). A *\<^sub>v x = y}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vector_space_row_space:
  assumes A: "A \<in> carrier_mat nr n"
  shows "vectorspace class_ring (vs (row_space A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace class_ring (vs (row_space A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vectorspace class_ring (vs (row_space A))
[PROOF STEP]
have fin: "finite (set (rows A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set (rows A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set (rows A))

goal (1 subgoal):
 1. vectorspace class_ring (vs (row_space A))
[PROOF STEP]
have s: "set (rows A) \<subseteq> carrier V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rows A) \<subseteq> carrier V
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr n

goal (1 subgoal):
 1. set (rows A) \<subseteq> carrier V
[PROOF STEP]
unfolding rows_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr n

goal (1 subgoal):
 1. set (map (row A) [0..<dim_row A]) \<subseteq> carrier V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (rows A) \<subseteq> carrier V

goal (1 subgoal):
 1. vectorspace class_ring (vs (row_space A))
[PROOF STEP]
have "span_vs (set (rows A)) = vs (span (set (rows A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs (local.span (set (rows A))) = vs (local.span (set (rows A)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vs (local.span (set (rows A))) = vs (local.span (set (rows A)))

goal (1 subgoal):
 1. vectorspace class_ring (vs (row_space A))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vs (local.span (set (rows A))) = vs (local.span (set (rows A)))

goal (1 subgoal):
 1. vectorspace class_ring (vs (row_space A))
[PROOF STEP]
have "vectorspace class_ring (span_vs (set (rows A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace class_ring (vs (local.span (set (rows A))))
[PROOF STEP]
using fin s span_is_subspace subspace_def subspace_is_vs
[PROOF STATE]
proof (prove)
using this:
finite (set (rows A))
set (rows A) \<subseteq> carrier V
?S \<subseteq> carrier_vec n \<Longrightarrow> subspace class_ring (local.span ?S) V
subspace ?K ?W ?V \<equiv> vectorspace ?K ?V \<and> LinearCombinations.submodule ?K ?W ?V
subspace class_ring ?W V \<Longrightarrow> vectorspace class_ring (vs ?W)

goal (1 subgoal):
 1. vectorspace class_ring (vs (local.span (set (rows A))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vectorspace class_ring (vs (local.span (set (rows A))))

goal (1 subgoal):
 1. vectorspace class_ring (vs (row_space A))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vs (local.span (set (rows A))) = vs (local.span (set (rows A)))
vectorspace class_ring (vs (local.span (set (rows A))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vs (local.span (set (rows A))) = vs (local.span (set (rows A)))
vectorspace class_ring (vs (local.span (set (rows A))))

goal (1 subgoal):
 1. vectorspace class_ring (vs (row_space A))
[PROOF STEP]
unfolding row_space_def
[PROOF STATE]
proof (prove)
using this:
vs (local.span (set (rows A))) = vs (local.span (set (rows A)))
vectorspace class_ring (vs (local.span (set (rows A))))

goal (1 subgoal):
 1. vectorspace class_ring (vs (local.span (set (rows A))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vectorspace class_ring (vs (row_space A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_space_eq:
  assumes A: "A \<in> carrier_mat nr n"
  shows "row_space A = {w\<in>carrier_vec (dim_col A). \<exists>y\<in>carrier_vec (dim_row A). A\<^sup>T *\<^sub>v y = w}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_space A = {w \<in> carrier_vec (dim_col A). \<exists>y\<in>carrier_vec (dim_row A). A\<^sup>T *\<^sub>v y = w}
[PROOF STEP]
using A col_space_eq
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr n
?A \<in> carrier_mat n ?nc \<Longrightarrow> col_space ?A = {y \<in> carrier_vec (dim_row ?A). \<exists>x\<in>carrier_vec (dim_col ?A). ?A *\<^sub>v x = y}

goal (1 subgoal):
 1. row_space A = {w \<in> carrier_vec (dim_col A). \<exists>y\<in>carrier_vec (dim_row A). A\<^sup>T *\<^sub>v y = w}
[PROOF STEP]
unfolding row_space_eq_col_space_transpose
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr n
?A \<in> carrier_mat n ?nc \<Longrightarrow> col_space ?A = {y \<in> carrier_vec (dim_row ?A). \<exists>x\<in>carrier_vec (dim_col ?A). ?A *\<^sub>v x = y}

goal (1 subgoal):
 1. col_space A\<^sup>T = {w \<in> carrier_vec (dim_col A). \<exists>y\<in>carrier_vec (dim_row A). A\<^sup>T *\<^sub>v y = w}
[PROOF STEP]
by auto


[STATEMENT]
lemma row_space_is_preserved:
  assumes inv_P: "invertible_mat P" and P: "P \<in> carrier_mat m m" and A: "A \<in> carrier_mat m n"
  shows "row_space (P*A) = row_space A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_space (P * A) = row_space A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row_space (P * A) = row_space A
[PROOF STEP]
have At: "A\<^sup>T \<in> carrier_mat n m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sup>T \<in> carrier_mat n m
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat m n

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

goal (1 subgoal):
 1. row_space (P * A) = row_space A
[PROOF STEP]
have Pt: "P\<^sup>T \<in> carrier_mat m m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>T \<in> carrier_mat m m
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat m m

goal (1 subgoal):
 1. P\<^sup>T \<in> carrier_mat m m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P\<^sup>T \<in> carrier_mat m m

goal (1 subgoal):
 1. row_space (P * A) = row_space A
[PROOF STEP]
have PA: "P*A \<in> carrier_mat m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * A \<in> carrier_mat m n
[PROOF STEP]
using P A
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat m m
A \<in> carrier_mat m n

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

goal (1 subgoal):
 1. row_space (P * A) = row_space A
[PROOF STEP]
have "w \<in> row_space A" if w: "w \<in> row_space (P*A)" for w
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
have w_carrier: "w \<in> carrier_vec (dim_col (P*A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> carrier_vec (dim_col (P * A))
[PROOF STEP]
using w mult_carrier_mat[OF P A] row_space_eq
[PROOF STATE]
proof (prove)
using this:
w \<in> row_space (P * A)
P * A \<in> carrier_mat m n
?A \<in> carrier_mat ?nr n \<Longrightarrow> row_space ?A = {w \<in> carrier_vec (dim_col ?A). \<exists>y\<in>carrier_vec (dim_row ?A). ?A\<^sup>T *\<^sub>v y = w}

goal (1 subgoal):
 1. w \<in> carrier_vec (dim_col (P * A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> carrier_vec (dim_col (P * A))

goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
from that and this
[PROOF STATE]
proof (chain)
picking this:
w \<in> row_space (P * A)
w \<in> carrier_vec (dim_col (P * A))
[PROOF STEP]
obtain y where y: "y \<in> carrier_vec (dim_row (P * A))"
      and w_By: "w = (P*A)\<^sup>T *\<^sub>v y"
[PROOF STATE]
proof (prove)
using this:
w \<in> row_space (P * A)
w \<in> carrier_vec (dim_col (P * A))

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> carrier_vec (dim_row (P * A)); w = (P * A)\<^sup>T *\<^sub>v y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding row_space_eq[OF PA]
[PROOF STATE]
proof (prove)
using this:
w \<in> {w \<in> carrier_vec (dim_col (P * A)). \<exists>y\<in>carrier_vec (dim_row (P * A)). (P * A)\<^sup>T *\<^sub>v y = w}
w \<in> carrier_vec (dim_col (P * A))

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> carrier_vec (dim_row (P * A)); w = (P * A)\<^sup>T *\<^sub>v y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> carrier_vec (dim_row (P * A))
w = (P * A)\<^sup>T *\<^sub>v y

goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
have ym: "y \<in> carrier_vec m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> carrier_vec m
[PROOF STEP]
using y Pt
[PROOF STATE]
proof (prove)
using this:
y \<in> carrier_vec (dim_row (P * A))
P\<^sup>T \<in> carrier_mat m m

goal (1 subgoal):
 1. y \<in> carrier_vec m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> carrier_vec m

goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
have "w=((P*A)\<^sup>T) *\<^sub>v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = (P * A)\<^sup>T *\<^sub>v y
[PROOF STEP]
using w_By
[PROOF STATE]
proof (prove)
using this:
w = (P * A)\<^sup>T *\<^sub>v y

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

goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w = (P * A)\<^sup>T *\<^sub>v y

goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
have "... = (A\<^sup>T * P\<^sup>T) *\<^sub>v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P * A)\<^sup>T *\<^sub>v y = A\<^sup>T * P\<^sup>T *\<^sub>v y
[PROOF STEP]
using transpose_mult[OF P A]
[PROOF STATE]
proof (prove)
using this:
(P * A)\<^sup>T = A\<^sup>T * P\<^sup>T

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

goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(P * A)\<^sup>T *\<^sub>v y = A\<^sup>T * P\<^sup>T *\<^sub>v y

goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
have "... = A\<^sup>T *\<^sub>v (P\<^sup>T *\<^sub>v y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sup>T * P\<^sup>T *\<^sub>v y = A\<^sup>T *\<^sub>v (P\<^sup>T *\<^sub>v y)
[PROOF STEP]
by (rule assoc_mult_mat_vec[OF At Pt], insert Pt y, auto)
[PROOF STATE]
proof (state)
this:
A\<^sup>T * P\<^sup>T *\<^sub>v y = A\<^sup>T *\<^sub>v (P\<^sup>T *\<^sub>v y)

goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w = A\<^sup>T *\<^sub>v (P\<^sup>T *\<^sub>v y)
[PROOF STEP]
show "w \<in> row_space A"
[PROOF STATE]
proof (prove)
using this:
w = A\<^sup>T *\<^sub>v (P\<^sup>T *\<^sub>v y)

goal (1 subgoal):
 1. w \<in> row_space A
[PROOF STEP]
unfolding row_space_eq[OF A]
[PROOF STATE]
proof (prove)
using this:
w = A\<^sup>T *\<^sub>v (P\<^sup>T *\<^sub>v y)

goal (1 subgoal):
 1. w \<in> {w \<in> carrier_vec (dim_col A). \<exists>y\<in>carrier_vec (dim_row A). A\<^sup>T *\<^sub>v y = w}
[PROOF STEP]
using At Pt ym
[PROOF STATE]
proof (prove)
using this:
w = A\<^sup>T *\<^sub>v (P\<^sup>T *\<^sub>v y)
A\<^sup>T \<in> carrier_mat n m
P\<^sup>T \<in> carrier_mat m m
y \<in> carrier_vec m

goal (1 subgoal):
 1. w \<in> {w \<in> carrier_vec (dim_col A). \<exists>y\<in>carrier_vec (dim_row A). A\<^sup>T *\<^sub>v y = w}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> row_space A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?w1 \<in> row_space (P * A) \<Longrightarrow> ?w1 \<in> row_space A

goal (1 subgoal):
 1. row_space (P * A) = row_space A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?w1 \<in> row_space (P * A) \<Longrightarrow> ?w1 \<in> row_space A

goal (1 subgoal):
 1. row_space (P * A) = row_space A
[PROOF STEP]
have "w \<in> row_space (P*A)" if w: "w \<in> row_space A" for w
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
have w_carrier: "w \<in> carrier_vec (dim_col A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> carrier_vec (dim_col A)
[PROOF STEP]
using w A
[PROOF STATE]
proof (prove)
using this:
w \<in> row_space A
A \<in> carrier_mat m n

goal (1 subgoal):
 1. w \<in> carrier_vec (dim_col A)
[PROOF STEP]
unfolding row_space_eq[OF A]
[PROOF STATE]
proof (prove)
using this:
w \<in> {w \<in> carrier_vec (dim_col A). \<exists>y\<in>carrier_vec (dim_row A). A\<^sup>T *\<^sub>v y = w}
A \<in> carrier_mat m n

goal (1 subgoal):
 1. w \<in> carrier_vec (dim_col A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> carrier_vec (dim_col A)

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
obtain P' where PP': "inverts_mat P P'" and P'P: "inverts_mat P' P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>inverts_mat P P'; inverts_mat P' P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inv_P P
[PROOF STATE]
proof (prove)
using this:
invertible_mat P
P \<in> carrier_mat m m

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>inverts_mat P P'; inverts_mat P' P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding invertible_mat_def
[PROOF STATE]
proof (prove)
using this:
square_mat P \<and> (\<exists>B. inverts_mat P B \<and> inverts_mat B P)
P \<in> carrier_mat m m

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>inverts_mat P P'; inverts_mat P' P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inverts_mat P P'
inverts_mat P' P

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
have P': "P' \<in> carrier_mat m m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P' \<in> carrier_mat m m
[PROOF STEP]
using PP' P'P P
[PROOF STATE]
proof (prove)
using this:
inverts_mat P P'
inverts_mat P' P
P \<in> carrier_mat m m

goal (1 subgoal):
 1. P' \<in> carrier_mat m m
[PROOF STEP]
unfolding inverts_mat_def
[PROOF STATE]
proof (prove)
using this:
P * P' = 1\<^sub>m (dim_row P)
P' * P = 1\<^sub>m (dim_row P')
P \<in> carrier_mat m m

goal (1 subgoal):
 1. P' \<in> carrier_mat m m
[PROOF STEP]
by (metis carrier_matD(1) carrier_matD(2) carrier_mat_triv index_mult_mat(3) index_one_mat(3))
[PROOF STATE]
proof (state)
this:
P' \<in> carrier_mat m m

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
w \<in> row_space A
[PROOF STEP]
obtain y where y: "y \<in> carrier_vec (dim_row A)" and
        w_Ay: "w = A\<^sup>T *\<^sub>v y"
[PROOF STATE]
proof (prove)
using this:
w \<in> row_space A

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> carrier_vec (dim_row A); w = A\<^sup>T *\<^sub>v y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding row_space_eq[OF A]
[PROOF STATE]
proof (prove)
using this:
w \<in> {w \<in> carrier_vec (dim_col A). \<exists>y\<in>carrier_vec (dim_row A). A\<^sup>T *\<^sub>v y = w}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> carrier_vec (dim_row A); w = A\<^sup>T *\<^sub>v y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> carrier_vec (dim_row A)
w = A\<^sup>T *\<^sub>v y

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
have Py: "(P'\<^sup>T *\<^sub>v y) \<in> carrier_vec m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P'\<^sup>T *\<^sub>v y \<in> carrier_vec m
[PROOF STEP]
using P' y A
[PROOF STATE]
proof (prove)
using this:
P' \<in> carrier_mat m m
y \<in> carrier_vec (dim_row A)
A \<in> carrier_mat m n

goal (1 subgoal):
 1. P'\<^sup>T *\<^sub>v y \<in> carrier_vec m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P'\<^sup>T *\<^sub>v y \<in> carrier_vec m

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
have "w = A\<^sup>T *\<^sub>v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = A\<^sup>T *\<^sub>v y
[PROOF STEP]
using w_Ay
[PROOF STATE]
proof (prove)
using this:
w = A\<^sup>T *\<^sub>v y

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

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w = A\<^sup>T *\<^sub>v y

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
have "... = ((P' * P)*A)\<^sup>T *\<^sub>v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sup>T *\<^sub>v y = (P' * P * A)\<^sup>T *\<^sub>v y
[PROOF STEP]
using P'P left_mult_one_mat A P'
[PROOF STATE]
proof (prove)
using this:
inverts_mat P' P
?A \<in> carrier_mat ?nr ?nc \<Longrightarrow> 1\<^sub>m ?nr * ?A = ?A
A \<in> carrier_mat m n
P' \<in> carrier_mat m m

goal (1 subgoal):
 1. A\<^sup>T *\<^sub>v y = (P' * P * A)\<^sup>T *\<^sub>v y
[PROOF STEP]
unfolding inverts_mat_def
[PROOF STATE]
proof (prove)
using this:
P' * P = 1\<^sub>m (dim_row P')
?A \<in> carrier_mat ?nr ?nc \<Longrightarrow> 1\<^sub>m ?nr * ?A = ?A
A \<in> carrier_mat m n
P' \<in> carrier_mat m m

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

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A\<^sup>T *\<^sub>v y = (P' * P * A)\<^sup>T *\<^sub>v y

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
have "... = ((P' * (P*A))\<^sup>T) *\<^sub>v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P' * P * A)\<^sup>T *\<^sub>v y = (P' * (P * A))\<^sup>T *\<^sub>v y
[PROOF STEP]
using assoc_mult_mat_vec P' P A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?n\<^sub>1 ?n\<^sub>2; ?B \<in> carrier_mat ?n\<^sub>2 ?n\<^sub>3; ?v \<in> carrier_vec ?n\<^sub>3\<rbrakk> \<Longrightarrow> ?A * ?B *\<^sub>v ?v = ?A *\<^sub>v (?B *\<^sub>v ?v)
P' \<in> carrier_mat m m
P \<in> carrier_mat m m
A \<in> carrier_mat m n

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

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(P' * P * A)\<^sup>T *\<^sub>v y = (P' * (P * A))\<^sup>T *\<^sub>v y

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
have "... = ((P*A)\<^sup>T * P'\<^sup>T) *\<^sub>v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P' * (P * A))\<^sup>T *\<^sub>v y = (P * A)\<^sup>T * P'\<^sup>T *\<^sub>v y
[PROOF STEP]
using transpose_mult P A P' mult_carrier_mat
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?nr ?n; ?B \<in> carrier_mat ?n ?nc\<rbrakk> \<Longrightarrow> (?A * ?B)\<^sup>T = ?B\<^sup>T * ?A\<^sup>T
P \<in> carrier_mat m m
A \<in> carrier_mat m n
P' \<in> carrier_mat m m
\<lbrakk>?A \<in> carrier_mat ?nr ?n; ?B \<in> carrier_mat ?n ?nc\<rbrakk> \<Longrightarrow> ?A * ?B \<in> carrier_mat ?nr ?nc

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

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(P' * (P * A))\<^sup>T *\<^sub>v y = (P * A)\<^sup>T * P'\<^sup>T *\<^sub>v y

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
have "... = (P*A)\<^sup>T *\<^sub>v (P'\<^sup>T *\<^sub>v y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P * A)\<^sup>T * P'\<^sup>T *\<^sub>v y = (P * A)\<^sup>T *\<^sub>v (P'\<^sup>T *\<^sub>v y)
[PROOF STEP]
using assoc_mult_mat_vec A P P' y mult_carrier_mat
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?n\<^sub>1 ?n\<^sub>2; ?B \<in> carrier_mat ?n\<^sub>2 ?n\<^sub>3; ?v \<in> carrier_vec ?n\<^sub>3\<rbrakk> \<Longrightarrow> ?A * ?B *\<^sub>v ?v = ?A *\<^sub>v (?B *\<^sub>v ?v)
A \<in> carrier_mat m n
P \<in> carrier_mat m m
P' \<in> carrier_mat m m
y \<in> carrier_vec (dim_row A)
\<lbrakk>?A \<in> carrier_mat ?nr ?n; ?B \<in> carrier_mat ?n ?nc\<rbrakk> \<Longrightarrow> ?A * ?B \<in> carrier_mat ?nr ?nc

goal (1 subgoal):
 1. (P * A)\<^sup>T * P'\<^sup>T *\<^sub>v y = (P * A)\<^sup>T *\<^sub>v (P'\<^sup>T *\<^sub>v y)
[PROOF STEP]
by (smt carrier_matD(1) transpose_carrier_mat)
[PROOF STATE]
proof (state)
this:
(P * A)\<^sup>T * P'\<^sup>T *\<^sub>v y = (P * A)\<^sup>T *\<^sub>v (P'\<^sup>T *\<^sub>v y)

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w = (P * A)\<^sup>T *\<^sub>v (P'\<^sup>T *\<^sub>v y)
[PROOF STEP]
show "w \<in> row_space (P*A)"
[PROOF STATE]
proof (prove)
using this:
w = (P * A)\<^sup>T *\<^sub>v (P'\<^sup>T *\<^sub>v y)

goal (1 subgoal):
 1. w \<in> row_space (P * A)
[PROOF STEP]
unfolding row_space_eq[OF PA]
[PROOF STATE]
proof (prove)
using this:
w = (P * A)\<^sup>T *\<^sub>v (P'\<^sup>T *\<^sub>v y)

goal (1 subgoal):
 1. w \<in> {w \<in> carrier_vec (dim_col (P * A)). \<exists>y\<in>carrier_vec (dim_row (P * A)). (P * A)\<^sup>T *\<^sub>v y = w}
[PROOF STEP]
using Py w_carrier A P
[PROOF STATE]
proof (prove)
using this:
w = (P * A)\<^sup>T *\<^sub>v (P'\<^sup>T *\<^sub>v y)
P'\<^sup>T *\<^sub>v y \<in> carrier_vec m
w \<in> carrier_vec (dim_col A)
A \<in> carrier_mat m n
P \<in> carrier_mat m m

goal (1 subgoal):
 1. w \<in> {w \<in> carrier_vec (dim_col (P * A)). \<exists>y\<in>carrier_vec (dim_row (P * A)). (P * A)\<^sup>T *\<^sub>v y = w}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
w \<in> row_space (P * A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?w1 \<in> row_space A \<Longrightarrow> ?w1 \<in> row_space (P * A)

goal (1 subgoal):
 1. row_space (P * A) = row_space A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?w1 \<in> row_space (P * A) \<Longrightarrow> ?w1 \<in> row_space A
?w1 \<in> row_space A \<Longrightarrow> ?w1 \<in> row_space (P * A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?w1 \<in> row_space (P * A) \<Longrightarrow> ?w1 \<in> row_space A
?w1 \<in> row_space A \<Longrightarrow> ?w1 \<in> row_space (P * A)

goal (1 subgoal):
 1. row_space (P * A) = row_space A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_space (P * A) = row_space A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R_sumlist[simp]: "R.sumlist = sum_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R.sumlist = sum_list
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. R.sumlist x = sum_list x
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. R.sumlist x = sum_list x
[PROOF STEP]
show "R.sumlist xs = sum_list xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R.sumlist xs = sum_list xs
[PROOF STEP]
by (induct xs, auto)
[PROOF STATE]
proof (state)
this:
R.sumlist xs = sum_list xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumlist_dim: assumes "\<And> x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n"
  shows "dim_vec (sumlist xs) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (M.sumlist xs) = n
[PROOF STEP]
using sumlist_carrier assms
[PROOF STATE]
proof (prove)
using this:
set ?xs \<subseteq> carrier_vec n \<Longrightarrow> M.sumlist ?xs \<in> carrier_vec n
?x1 \<in> set xs \<Longrightarrow> ?x1 \<in> carrier_vec n

goal (1 subgoal):
 1. dim_vec (M.sumlist xs) = n
[PROOF STEP]
by fastforce


[STATEMENT]
lemma sumlist_vec_index: assumes "\<And> x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n"
  and "i < n"
shows "sumlist xs $ i = sum_list (map (\<lambda> x. x $ i) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist xs $ i = (\<Sum>x\<leftarrow>xs. x $ i)
[PROOF STEP]
unfolding M.sumlist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> set xs \<Longrightarrow> ?x1 \<in> carrier_vec n

goal (1 subgoal):
 1. foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i)
[PROOF STEP]
proof(induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i); \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> foldr (+) (a # xs) (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>a # xs. x $ i)
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i)
?x1 \<in> set (a # xs) \<Longrightarrow> ?x1 \<in> carrier_vec n

goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i); \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> foldr (+) (a # xs) (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>a # xs. x $ i)
[PROOF STEP]
hence cond:"\<And> x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i)
?x1 \<in> set (a # xs) \<Longrightarrow> ?x1 \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> set xs \<Longrightarrow> ?x1 \<in> carrier_vec n

goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i); \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> foldr (+) (a # xs) (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>a # xs. x $ i)
[PROOF STEP]
from Cons(1)[OF cond]
[PROOF STATE]
proof (chain)
picking this:
(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> set xs) \<Longrightarrow> foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i)
[PROOF STEP]
have IH:"foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i)"
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> set xs) \<Longrightarrow> foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i)

goal (1 subgoal):
 1. foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i)

goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i); \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> foldr (+) (a # xs) (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>a # xs. x $ i)
[PROOF STEP]
have "(a + foldr (+) xs (0\<^sub>v n)) $ i = a $ i + (\<Sum>x\<leftarrow>xs. x $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a + foldr (+) xs (0\<^sub>v n)) $ i = a $ i + (\<Sum>x\<leftarrow>xs. x $ i)
[PROOF STEP]
apply(subst index_add_vec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < dim_vec (foldr (+) xs (0\<^sub>v n))
 2. a $ i + foldr (+) xs (0\<^sub>v n) $ i = a $ i + (\<Sum>x\<leftarrow>xs. x $ i)
[PROOF STEP]
unfolding IH
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i < dim_vec (foldr (+) xs (0\<^sub>v n))
 2. a $ i + (\<Sum>x\<leftarrow>xs. x $ i) = a $ i + (\<Sum>x\<leftarrow>xs. x $ i)
[PROOF STEP]
using sumlist_dim[OF cond,unfolded M.sumlist_def] assms
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> set ?xs \<Longrightarrow> x \<in> set xs) \<Longrightarrow> dim_vec (foldr (+) ?xs (0\<^sub>v n)) = n
?x1 \<in> set xs \<Longrightarrow> ?x1 \<in> carrier_vec n
i < n

goal (2 subgoals):
 1. i < dim_vec (foldr (+) xs (0\<^sub>v n))
 2. a $ i + (\<Sum>x\<leftarrow>xs. x $ i) = a $ i + (\<Sum>x\<leftarrow>xs. x $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a + foldr (+) xs (0\<^sub>v n)) $ i = a $ i + (\<Sum>x\<leftarrow>xs. x $ i)

goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) xs (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>xs. x $ i); \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> foldr (+) (a # xs) (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>a # xs. x $ i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a + foldr (+) xs (0\<^sub>v n)) $ i = a $ i + (\<Sum>x\<leftarrow>xs. x $ i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(a + foldr (+) xs (0\<^sub>v n)) $ i = a $ i + (\<Sum>x\<leftarrow>xs. x $ i)

goal (1 subgoal):
 1. foldr (+) (a # xs) (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>a # xs. x $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldr (+) (a # xs) (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>a # xs. x $ i)

goal (1 subgoal):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
?x1 \<in> set [] \<Longrightarrow> ?x1 \<in> carrier_vec n

goal (1 subgoal):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> x \<in> carrier_vec n) \<Longrightarrow> foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> set [] \<Longrightarrow> ?x1 \<in> carrier_vec n

goal (1 subgoal):
 1. foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> set [] \<Longrightarrow> ?x1 \<in> carrier_vec n
?x1 \<in> set xs \<Longrightarrow> ?x1 \<in> carrier_vec n
i < n

goal (1 subgoal):
 1. foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldr (+) [] (0\<^sub>v n) $ i = (\<Sum>x\<leftarrow>[]. x $ i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scalar_prod_left_sum_distrib:
  assumes vs: "\<And> v. v \<in> set vvs \<Longrightarrow> v \<in> carrier_vec n" and w: "w \<in> carrier_vec n"
  shows "sumlist vvs \<bullet> w = sum_list (map (\<lambda> v. v \<bullet> w) vvs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist vvs \<bullet> w = (\<Sum>v\<leftarrow>vvs. v \<bullet> w)
[PROOF STEP]
using vs
[PROOF STATE]
proof (prove)
using this:
?v1 \<in> set vvs \<Longrightarrow> ?v1 \<in> carrier_vec n

goal (1 subgoal):
 1. M.sumlist vvs \<bullet> w = (\<Sum>v\<leftarrow>vvs. v \<bullet> w)
[PROOF STEP]
proof (induct vvs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>v. v \<in> set [] \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist [] \<bullet> w = (\<Sum>v\<leftarrow>[]. v \<bullet> w)
 2. \<And>a vvs. \<lbrakk>(\<And>v. v \<in> set vvs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vvs \<bullet> w = (\<Sum>v\<leftarrow>vvs. v \<bullet> w); \<And>v. v \<in> set (a # vvs) \<Longrightarrow> v \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.sumlist (a # vvs) \<bullet> w = (\<Sum>v\<leftarrow>a # vvs. v \<bullet> w)
[PROOF STEP]
case (Cons v vs)
[PROOF STATE]
proof (state)
this:
(\<And>v. v \<in> set vs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vs \<bullet> w = (\<Sum>v\<leftarrow>vs. v \<bullet> w)
?v1 \<in> set (v # vs) \<Longrightarrow> ?v1 \<in> carrier_vec n

goal (2 subgoals):
 1. (\<And>v. v \<in> set [] \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist [] \<bullet> w = (\<Sum>v\<leftarrow>[]. v \<bullet> w)
 2. \<And>a vvs. \<lbrakk>(\<And>v. v \<in> set vvs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vvs \<bullet> w = (\<Sum>v\<leftarrow>vvs. v \<bullet> w); \<And>v. v \<in> set (a # vvs) \<Longrightarrow> v \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.sumlist (a # vvs) \<bullet> w = (\<Sum>v\<leftarrow>a # vvs. v \<bullet> w)
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
(\<And>v. v \<in> set vs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vs \<bullet> w = (\<Sum>v\<leftarrow>vs. v \<bullet> w)
?v1 \<in> set (v # vs) \<Longrightarrow> ?v1 \<in> carrier_vec n
[PROOF STEP]
have v: "v \<in> carrier_vec n" and vs: "sumlist vs \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
(\<And>v. v \<in> set vs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vs \<bullet> w = (\<Sum>v\<leftarrow>vs. v \<bullet> w)
?v1 \<in> set (v # vs) \<Longrightarrow> ?v1 \<in> carrier_vec n

goal (1 subgoal):
 1. v \<in> carrier_vec n &&& M.sumlist vs \<in> carrier_vec n
[PROOF STEP]
by (auto intro!: sumlist_carrier)
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
M.sumlist vs \<in> carrier_vec n

goal (2 subgoals):
 1. (\<And>v. v \<in> set [] \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist [] \<bullet> w = (\<Sum>v\<leftarrow>[]. v \<bullet> w)
 2. \<And>a vvs. \<lbrakk>(\<And>v. v \<in> set vvs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vvs \<bullet> w = (\<Sum>v\<leftarrow>vvs. v \<bullet> w); \<And>v. v \<in> set (a # vvs) \<Longrightarrow> v \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.sumlist (a # vvs) \<bullet> w = (\<Sum>v\<leftarrow>a # vvs. v \<bullet> w)
[PROOF STEP]
have "sumlist (v # vs) \<bullet> w = sumlist ([v] @ vs) \<bullet> w "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (v # vs) \<bullet> w = M.sumlist ([v] @ vs) \<bullet> w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M.sumlist (v # vs) \<bullet> w = M.sumlist ([v] @ vs) \<bullet> w

goal (2 subgoals):
 1. (\<And>v. v \<in> set [] \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist [] \<bullet> w = (\<Sum>v\<leftarrow>[]. v \<bullet> w)
 2. \<And>a vvs. \<lbrakk>(\<And>v. v \<in> set vvs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vvs \<bullet> w = (\<Sum>v\<leftarrow>vvs. v \<bullet> w); \<And>v. v \<in> set (a # vvs) \<Longrightarrow> v \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.sumlist (a # vvs) \<bullet> w = (\<Sum>v\<leftarrow>a # vvs. v \<bullet> w)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (v # vs) \<bullet> w = M.sumlist ([v] @ vs) \<bullet> w

goal (2 subgoals):
 1. (\<And>v. v \<in> set [] \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist [] \<bullet> w = (\<Sum>v\<leftarrow>[]. v \<bullet> w)
 2. \<And>a vvs. \<lbrakk>(\<And>v. v \<in> set vvs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vvs \<bullet> w = (\<Sum>v\<leftarrow>vvs. v \<bullet> w); \<And>v. v \<in> set (a # vvs) \<Longrightarrow> v \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.sumlist (a # vvs) \<bullet> w = (\<Sum>v\<leftarrow>a # vvs. v \<bullet> w)
[PROOF STEP]
have "\<dots> = (v + sumlist vs) \<bullet> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist ([v] @ vs) \<bullet> w = (v + M.sumlist vs) \<bullet> w
[PROOF STEP]
by (subst sumlist_append, insert Cons v vs, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist ([v] @ vs) \<bullet> w = (v + M.sumlist vs) \<bullet> w

goal (2 subgoals):
 1. (\<And>v. v \<in> set [] \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist [] \<bullet> w = (\<Sum>v\<leftarrow>[]. v \<bullet> w)
 2. \<And>a vvs. \<lbrakk>(\<And>v. v \<in> set vvs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vvs \<bullet> w = (\<Sum>v\<leftarrow>vvs. v \<bullet> w); \<And>v. v \<in> set (a # vvs) \<Longrightarrow> v \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.sumlist (a # vvs) \<bullet> w = (\<Sum>v\<leftarrow>a # vvs. v \<bullet> w)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist ([v] @ vs) \<bullet> w = (v + M.sumlist vs) \<bullet> w

goal (2 subgoals):
 1. (\<And>v. v \<in> set [] \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist [] \<bullet> w = (\<Sum>v\<leftarrow>[]. v \<bullet> w)
 2. \<And>a vvs. \<lbrakk>(\<And>v. v \<in> set vvs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vvs \<bullet> w = (\<Sum>v\<leftarrow>vvs. v \<bullet> w); \<And>v. v \<in> set (a # vvs) \<Longrightarrow> v \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.sumlist (a # vvs) \<bullet> w = (\<Sum>v\<leftarrow>a # vvs. v \<bullet> w)
[PROOF STEP]
have "\<dots> = v \<bullet> w + (sumlist vs \<bullet> w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v + M.sumlist vs) \<bullet> w = v \<bullet> w + M.sumlist vs \<bullet> w
[PROOF STEP]
by (rule add_scalar_prod_distrib[OF v vs w])
[PROOF STATE]
proof (state)
this:
(v + M.sumlist vs) \<bullet> w = v \<bullet> w + M.sumlist vs \<bullet> w

goal (2 subgoals):
 1. (\<And>v. v \<in> set [] \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist [] \<bullet> w = (\<Sum>v\<leftarrow>[]. v \<bullet> w)
 2. \<And>a vvs. \<lbrakk>(\<And>v. v \<in> set vvs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vvs \<bullet> w = (\<Sum>v\<leftarrow>vvs. v \<bullet> w); \<And>v. v \<in> set (a # vvs) \<Longrightarrow> v \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.sumlist (a # vvs) \<bullet> w = (\<Sum>v\<leftarrow>a # vvs. v \<bullet> w)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M.sumlist (v # vs) \<bullet> w = v \<bullet> w + M.sumlist vs \<bullet> w
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
M.sumlist (v # vs) \<bullet> w = v \<bullet> w + M.sumlist vs \<bullet> w

goal (1 subgoal):
 1. M.sumlist (v # vs) \<bullet> w = (\<Sum>v\<leftarrow>v # vs. v \<bullet> w)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
M.sumlist (v # vs) \<bullet> w = v \<bullet> w + M.sumlist vs \<bullet> w
(\<And>v. v \<in> set vs \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist vs \<bullet> w = (\<Sum>v\<leftarrow>vs. v \<bullet> w)
?v1 \<in> set (v # vs) \<Longrightarrow> ?v1 \<in> carrier_vec n

goal (1 subgoal):
 1. M.sumlist (v # vs) \<bullet> w = (\<Sum>v\<leftarrow>v # vs. v \<bullet> w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M.sumlist (v # vs) \<bullet> w = (\<Sum>v\<leftarrow>v # vs. v \<bullet> w)

goal (1 subgoal):
 1. (\<And>v. v \<in> set [] \<Longrightarrow> v \<in> carrier_vec n) \<Longrightarrow> M.sumlist [] \<bullet> w = (\<Sum>v\<leftarrow>[]. v \<bullet> w)
[PROOF STEP]
qed (insert w, auto)


[STATEMENT]
lemma scalar_prod_right_sum_distrib:
  assumes vs: "\<And> v. v \<in> set vvs \<Longrightarrow> v \<in> carrier_vec n" and w: "w \<in> carrier_vec n"
  shows "w \<bullet> sumlist vvs = sum_list (map (\<lambda> v. w \<bullet> v) vvs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<bullet> M.sumlist vvs = sum_list (map ((\<bullet>) w) vvs)
[PROOF STEP]
by (subst comm_scalar_prod[OF w sumlist_carrier], insert vs w, force,
  subst scalar_prod_left_sum_distrib[OF vs w], force,
  rule arg_cong[of _ _ sum_list], rule nth_equalityI,
  auto simp: set_conv_nth intro!: comm_scalar_prod)


[STATEMENT]
lemma lincomb_list_add_vec_2: assumes us: "set us \<subseteq> carrier_vec n"
  and x: "x = lincomb_list lc (us [i := us ! i + c \<cdot>\<^sub>v us ! j])"
  and i: "j < length us" "i < length us" "i \<noteq> j"
shows "x = lincomb_list (lc (j := lc j + lc i * c)) us" (is "_ = ?x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
let ?xx = "lc j + lc i * c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
let ?i = "us ! i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
let ?j = "us ! j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
let ?v = "?i + c \<cdot>\<^sub>v ?j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
let ?ws = "us [i := us ! i + c \<cdot>\<^sub>v us ! j]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
from us
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> carrier_vec n
[PROOF STEP]
have usk: "k < length us \<Longrightarrow> us ! k \<in> carrier_vec n" for k
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n

goal (1 subgoal):
 1. k < length us \<Longrightarrow> us ! k \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k1 < length us \<Longrightarrow> us ! ?k1 \<in> carrier_vec n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
from usk i
[PROOF STATE]
proof (chain)
picking this:
?k1 < length us \<Longrightarrow> us ! ?k1 \<in> carrier_vec n
j < length us
i < length us
i \<noteq> j
[PROOF STEP]
have ij: "?i \<in> carrier_vec n" "?j \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
?k1 < length us \<Longrightarrow> us ! ?k1 \<in> carrier_vec n
j < length us
i < length us
i \<noteq> j

goal (1 subgoal):
 1. us ! i \<in> carrier_vec n &&& us ! j \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
us ! i \<in> carrier_vec n
us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
hence v: "c \<cdot>\<^sub>v ?j \<in> carrier_vec n" "?v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
us ! i \<in> carrier_vec n
us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. c \<cdot>\<^sub>v us ! j \<in> carrier_vec n &&& us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
with us
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> carrier_vec n
c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
[PROOF STEP]
have ws: "set ?ws \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n
c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n
[PROOF STEP]
unfolding set_conv_nth
[PROOF STATE]
proof (prove)
using this:
{us ! i |i. i < length us} \<subseteq> carrier_vec n
c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. {us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia |ia. ia < length (us[i := us ! i + c \<cdot>\<^sub>v us ! j])} \<subseteq> carrier_vec n
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
{us ! i |i. i < length us} \<subseteq> carrier_vec n
c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
j < length us
i < length us
i \<noteq> j

goal (1 subgoal):
 1. {us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia |ia. ia < length (us[i := us ! i + c \<cdot>\<^sub>v us ! j])} \<subseteq> carrier_vec n
[PROOF STEP]
by (auto, rename_tac k, case_tac "k = i", auto)
[PROOF STATE]
proof (state)
this:
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
from us
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> carrier_vec n
[PROOF STEP]
have us': "\<forall>w\<in>set us. dim_vec w = n"
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<forall>w\<in>set us. dim_vec w = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set us. dim_vec w = n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
from ws
[PROOF STATE]
proof (chain)
picking this:
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n
[PROOF STEP]
have ws': "\<forall>w\<in>set ?ws. dim_vec w = n"
[PROOF STATE]
proof (prove)
using this:
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<forall>w\<in>set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]). dim_vec w = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]). dim_vec w = n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
have mset: "mset_set {0..<length us} = {#i#} + {#j#} + (mset_set ({0..<length us} - {i,j}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_set {0..<length us} = {#i#} + {#j#} + mset_set ({0..<length us} - {i, j})
[PROOF STEP]
by (rule multiset_eqI, insert i, auto, rename_tac x, case_tac "x \<in> {0 ..< length us}", auto)
[PROOF STATE]
proof (state)
this:
mset_set {0..<length us} = {#i#} + {#j#} + mset_set ({0..<length us} - {i, j})

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
define M2 where "M2 = M.summset
      {#lc ia \<cdot>\<^sub>v ?ws ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#}"
[PROOF STATE]
proof (state)
this:
M2 = M.summset {#lc ia \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#}

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
define M1 where "M1 = M.summset {#(if i = j then ?xx else lc i) \<cdot>\<^sub>v us ! i. i \<in># mset_set ({0..<length us} - {i, j})#}"
[PROOF STATE]
proof (state)
this:
M1 = M.summset {#(if ia = j then lc j + lc i * c else lc ia) \<cdot>\<^sub>v us ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#}

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
have M1: "M1 \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M1 \<in> carrier_vec n
[PROOF STEP]
unfolding M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.summset {#(if ia = j then lc j + lc i * c else lc ia) \<cdot>\<^sub>v us ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#} \<in> carrier_vec n
[PROOF STEP]
using usk
[PROOF STATE]
proof (prove)
using this:
?k1 < length us \<Longrightarrow> us ! ?k1 \<in> carrier_vec n

goal (1 subgoal):
 1. M.summset {#(if ia = j then lc j + lc i * c else lc ia) \<cdot>\<^sub>v us ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#} \<in> carrier_vec n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
M1 \<in> carrier_vec n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
have M2: "M1 = M2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M1 = M2
[PROOF STEP]
unfolding M2_def M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.summset {#(if ia = j then lc j + lc i * c else lc ia) \<cdot>\<^sub>v us ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#} = M.summset {#lc ia \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#}
[PROOF STEP]
by (rule arg_cong[of _ _ M.summset], rule multiset.map_cong0, insert i usk, auto)
[PROOF STATE]
proof (state)
this:
M1 = M2

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
have x1: "x = lc j \<cdot>\<^sub>v ?j + (lc i \<cdot>\<^sub>v ?i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v ?j) + M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M1)
[PROOF STEP]
unfolding x lincomb_list_def M2 M2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>ia. lc ia \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia) [0..<length (us[i := us ! i + c \<cdot>\<^sub>v us ! j])]) = lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M.summset {#lc ia \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#})
[PROOF STEP]
apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk,
      simp add: mset smult_add_distrib_vec[OF ij(1) v(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j < length us; i < length us; i \<noteq> j; set us \<subseteq> carrier_vec n; set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n; \<And>k. k < length us \<Longrightarrow> us ! k \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.summset (add_mset (lc j \<cdot>\<^sub>v us ! j) (add_mset (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j)) {#lc ia \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#})) = lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M.summset {#lc ia \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#})
[PROOF STEP]
by (subst M.summset_add_mset, auto)+
[PROOF STATE]
proof (state)
this:
x = lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M1)

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
have x2: "?x = ?xx \<cdot>\<^sub>v ?j + (lc i \<cdot>\<^sub>v ?i + M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (lc(j := lc j + lc i * c)) us = (lc j + lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M1)
[PROOF STEP]
unfolding x lincomb_list_def M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>ia. (lc(j := lc j + lc i * c)) ia \<cdot>\<^sub>v us ! ia) [0..<length us]) = (lc j + lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M.summset {#(if ia = j then lc j + lc i * c else lc ia) \<cdot>\<^sub>v us ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#})
[PROOF STEP]
apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk,
      simp add: mset smult_add_distrib_vec[OF ij(1) v(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j < length us; i < length us; i \<noteq> j; set us \<subseteq> carrier_vec n; set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n; \<And>k. k < length us \<Longrightarrow> us ! k \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.summset (add_mset ((lc j + lc i * c) \<cdot>\<^sub>v us ! j) (add_mset (lc i \<cdot>\<^sub>v us ! i) {#(if ia = j then lc j + lc i * c else lc ia) \<cdot>\<^sub>v us ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#})) = (lc j + lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M.summset {#(if ia = j then lc j + lc i * c else lc ia) \<cdot>\<^sub>v us ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#})
[PROOF STEP]
by (subst M.summset_add_mset, auto)+
[PROOF STATE]
proof (state)
this:
lincomb_list (lc(j := lc j + lc i * c)) us = (lc j + lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M1)

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
unfolding x1 x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M1) = (lc j + lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M1)
[PROOF STEP]
using M1 ij
[PROOF STATE]
proof (prove)
using this:
M1 \<in> carrier_vec n
us ! i \<in> carrier_vec n
us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M1) = (lc j + lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M1)
[PROOF STEP]
by (intro eq_vecI, auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
x = lincomb_list (lc(j := lc j + lc i * c)) us

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lincomb_list_add_vec_1: assumes us: "set us \<subseteq> carrier_vec n"
  and x: "x = lincomb_list lc us"
  and i: "j < length us" "i < length us" "i \<noteq> j"
shows "x = lincomb_list (lc (j := lc j - lc i * c)) (us [i := us ! i + c \<cdot>\<^sub>v us ! j])" (is "_ = ?x")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
let ?i = "us ! i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
let ?j = "us ! j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
let ?v = "?i + c \<cdot>\<^sub>v ?j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
let ?ws = "us [i := us ! i + c \<cdot>\<^sub>v us ! j]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from us
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> carrier_vec n
[PROOF STEP]
have usk: "k < length us \<Longrightarrow> us ! k \<in> carrier_vec n" for k
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n

goal (1 subgoal):
 1. k < length us \<Longrightarrow> us ! k \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k1 < length us \<Longrightarrow> us ! ?k1 \<in> carrier_vec n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from usk i
[PROOF STATE]
proof (chain)
picking this:
?k1 < length us \<Longrightarrow> us ! ?k1 \<in> carrier_vec n
j < length us
i < length us
i \<noteq> j
[PROOF STEP]
have ij: "?i \<in> carrier_vec n" "?j \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
?k1 < length us \<Longrightarrow> us ! ?k1 \<in> carrier_vec n
j < length us
i < length us
i \<noteq> j

goal (1 subgoal):
 1. us ! i \<in> carrier_vec n &&& us ! j \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
us ! i \<in> carrier_vec n
us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
hence v: "c \<cdot>\<^sub>v ?j \<in> carrier_vec n" "?v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
us ! i \<in> carrier_vec n
us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. c \<cdot>\<^sub>v us ! j \<in> carrier_vec n &&& us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
with us
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> carrier_vec n
c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
[PROOF STEP]
have ws: "set ?ws \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n
c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n
[PROOF STEP]
unfolding set_conv_nth
[PROOF STATE]
proof (prove)
using this:
{us ! i |i. i < length us} \<subseteq> carrier_vec n
c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. {us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia |ia. ia < length (us[i := us ! i + c \<cdot>\<^sub>v us ! j])} \<subseteq> carrier_vec n
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
{us ! i |i. i < length us} \<subseteq> carrier_vec n
c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
j < length us
i < length us
i \<noteq> j

goal (1 subgoal):
 1. {us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia |ia. ia < length (us[i := us ! i + c \<cdot>\<^sub>v us ! j])} \<subseteq> carrier_vec n
[PROOF STEP]
by (auto, rename_tac k, case_tac "k = i", auto)
[PROOF STATE]
proof (state)
this:
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from us
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> carrier_vec n
[PROOF STEP]
have us': "\<forall>w\<in>set us. dim_vec w = n"
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<forall>w\<in>set us. dim_vec w = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set us. dim_vec w = n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from ws
[PROOF STATE]
proof (chain)
picking this:
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n
[PROOF STEP]
have ws': "\<forall>w\<in>set ?ws. dim_vec w = n"
[PROOF STATE]
proof (prove)
using this:
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<forall>w\<in>set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]). dim_vec w = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]). dim_vec w = n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have mset: "mset_set {0..<length us} = {#i#} + {#j#} + (mset_set ({0..<length us} - {i,j}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_set {0..<length us} = {#i#} + {#j#} + mset_set ({0..<length us} - {i, j})
[PROOF STEP]
by (rule multiset_eqI, insert i, auto, rename_tac x, case_tac "x \<in> {0 ..< length us}", auto)
[PROOF STATE]
proof (state)
this:
mset_set {0..<length us} = {#i#} + {#j#} + mset_set ({0..<length us} - {i, j})

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
define M2 where "M2 = M.summset
      {#(if ia = j then lc j - lc i * c else lc ia) \<cdot>\<^sub>v ?ws ! ia
      . ia \<in># mset_set ({0..<length us} - {i, j})#}"
[PROOF STATE]
proof (state)
this:
M2 = M.summset {#(if ia = j then lc j - lc i * c else lc ia) \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#}

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
define M1 where "M1 = M.summset {#lc i \<cdot>\<^sub>v us ! i. i \<in># mset_set ({0..<length us} - {i, j})#}"
[PROOF STATE]
proof (state)
this:
M1 = M.summset {#lc i \<cdot>\<^sub>v us ! i. i \<in># mset_set ({0..<length us} - {i, j})#}

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have M1: "M1 \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M1 \<in> carrier_vec n
[PROOF STEP]
unfolding M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.summset {#lc i \<cdot>\<^sub>v us ! i. i \<in># mset_set ({0..<length us} - {i, j})#} \<in> carrier_vec n
[PROOF STEP]
using usk
[PROOF STATE]
proof (prove)
using this:
?k1 < length us \<Longrightarrow> us ! ?k1 \<in> carrier_vec n

goal (1 subgoal):
 1. M.summset {#lc i \<cdot>\<^sub>v us ! i. i \<in># mset_set ({0..<length us} - {i, j})#} \<in> carrier_vec n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
M1 \<in> carrier_vec n

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have M2: "M1 = M2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M1 = M2
[PROOF STEP]
unfolding M2_def M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.summset {#lc i \<cdot>\<^sub>v us ! i. i \<in># mset_set ({0..<length us} - {i, j})#} = M.summset {#(if ia = j then lc j - lc i * c else lc ia) \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#}
[PROOF STEP]
by (rule arg_cong[of _ _ M.summset], rule multiset.map_cong0, insert i usk, auto)
[PROOF STATE]
proof (state)
this:
M1 = M2

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have x1: "x = lc j \<cdot>\<^sub>v ?j + (lc i \<cdot>\<^sub>v ?i + M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M1)
[PROOF STEP]
unfolding x lincomb_list_def M1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. lc i \<cdot>\<^sub>v us ! i) [0..<length us]) = lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M.summset {#lc i \<cdot>\<^sub>v us ! i. i \<in># mset_set ({0..<length us} - {i, j})#})
[PROOF STEP]
apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk,
      simp add: mset smult_add_distrib_vec[OF ij(1) v(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j < length us; i < length us; i \<noteq> j; set us \<subseteq> carrier_vec n; set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n; \<And>k. k < length us \<Longrightarrow> us ! k \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.summset (add_mset (lc j \<cdot>\<^sub>v us ! j) (add_mset (lc i \<cdot>\<^sub>v us ! i) {#lc i \<cdot>\<^sub>v us ! i. i \<in># mset_set ({0..<length us} - {i, j})#})) = lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M.summset {#lc i \<cdot>\<^sub>v us ! i. i \<in># mset_set ({0..<length us} - {i, j})#})
[PROOF STEP]
by (subst M.summset_add_mset, auto)+
[PROOF STATE]
proof (state)
this:
x = lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M1)

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have x2: "?x = (lc j - lc i * c) \<cdot>\<^sub>v ?j + (lc i \<cdot>\<^sub>v ?i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v ?j) + M1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) = (lc j - lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M1)
[PROOF STEP]
unfolding x lincomb_list_def M2 M2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>ia. (lc(j := lc j - lc i * c)) ia \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia) [0..<length (us[i := us ! i + c \<cdot>\<^sub>v us ! j])]) = (lc j - lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M.summset {#(if ia = j then lc j - lc i * c else lc ia) \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#})
[PROOF STEP]
apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk,
      simp add: mset smult_add_distrib_vec[OF ij(1) v(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j < length us; i < length us; i \<noteq> j; set us \<subseteq> carrier_vec n; set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n; \<And>k. k < length us \<Longrightarrow> us ! k \<in> carrier_vec n\<rbrakk> \<Longrightarrow> M.summset (add_mset ((lc j - lc i * c) \<cdot>\<^sub>v us ! j) (add_mset (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j)) {#(if ia = j then lc j - lc i * c else lc ia) \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#})) = (lc j - lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M.summset {#(if ia = j then lc j - lc i * c else lc ia) \<cdot>\<^sub>v us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia. ia \<in># mset_set ({0..<length us} - {i, j})#})
[PROOF STEP]
by (subst M.summset_add_mset, auto)+
[PROOF STATE]
proof (state)
this:
lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) = (lc j - lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M1)

goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
unfolding x1 x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M1) = (lc j - lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M1)
[PROOF STEP]
using M1 ij
[PROOF STATE]
proof (prove)
using this:
M1 \<in> carrier_vec n
us ! i \<in> carrier_vec n
us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. lc j \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + M1) = (lc j - lc i * c) \<cdot>\<^sub>v us ! j + (lc i \<cdot>\<^sub>v us ! i + lc i \<cdot>\<^sub>v (c \<cdot>\<^sub>v us ! j) + M1)
[PROOF STEP]
by (intro eq_vecI, auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_vec_span: assumes us: "set us \<subseteq> carrier_vec n"
  and i: "j < length us" "i < length us" "i \<noteq> j"
shows "span (set us) = span (set (us [i := us ! i + c \<cdot>\<^sub>v us ! j]))" (is "_ = span (set ?ws)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
let ?i = "us ! i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
let ?j = "us ! j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
let ?v = "?i + c \<cdot>\<^sub>v ?j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
from us i
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> carrier_vec n
j < length us
i < length us
i \<noteq> j
[PROOF STEP]
have ij: "?i \<in> carrier_vec n" "?j \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n
j < length us
i < length us
i \<noteq> j

goal (1 subgoal):
 1. us ! i \<in> carrier_vec n &&& us ! j \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
us ! i \<in> carrier_vec n
us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
hence v: "?v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
us ! i \<in> carrier_vec n
us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
with us
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
[PROOF STEP]
have ws: "set ?ws \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n
[PROOF STEP]
unfolding set_conv_nth
[PROOF STATE]
proof (prove)
using this:
{us ! i |i. i < length us} \<subseteq> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. {us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia |ia. ia < length (us[i := us ! i + c \<cdot>\<^sub>v us ! j])} \<subseteq> carrier_vec n
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
{us ! i |i. i < length us} \<subseteq> carrier_vec n
us ! i + c \<cdot>\<^sub>v us ! j \<in> carrier_vec n
j < length us
i < length us
i \<noteq> j

goal (1 subgoal):
 1. {us[i := us ! i + c \<cdot>\<^sub>v us ! j] ! ia |ia. ia < length (us[i := us ! i + c \<cdot>\<^sub>v us ! j])} \<subseteq> carrier_vec n
[PROOF STEP]
by (auto, rename_tac k, case_tac "k = i", auto)
[PROOF STATE]
proof (state)
this:
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
have "span (set us) = span_list us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (set us) = span_list us
[PROOF STEP]
unfolding span_list_as_span[OF us]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (set us) = local.span (set us)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
local.span (set us) = span_list us

goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.span (set us) = span_list us

goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
have "\<dots> = span_list ?ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
assume "x \<in> span_list us"
[PROOF STATE]
proof (state)
this:
x \<in> span_list us

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> span_list us
[PROOF STEP]
obtain lc where "x = lincomb_list lc us"
[PROOF STATE]
proof (prove)
using this:
x \<in> span_list us

goal (1 subgoal):
 1. (\<And>lc. x = lincomb_list lc us \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis in_span_listE)
[PROOF STATE]
proof (state)
this:
x = lincomb_list lc us

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from lincomb_list_add_vec_1[OF us this i, of c]
[PROOF STATE]
proof (chain)
picking this:
x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have "x \<in> span_list ?ws"
[PROOF STATE]
proof (prove)
using this:
x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. x \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
unfolding span_list_def
[PROOF STATE]
proof (prove)
using this:
x = lincomb_list (lc(j := lc j - lc i * c)) (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. x \<in> {uu_. \<exists>ca. uu_ = lincomb_list ca (us[i := us ! i + c \<cdot>\<^sub>v us ! j])}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x3 \<in> span_list us \<Longrightarrow> ?x3 \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x3 \<in> span_list us \<Longrightarrow> ?x3 \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?x3 \<in> span_list us \<Longrightarrow> ?x3 \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
assume "x \<in> span_list ?ws"
[PROOF STATE]
proof (state)
this:
x \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
obtain lc where "x = lincomb_list lc ?ws"
[PROOF STATE]
proof (prove)
using this:
x \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. (\<And>lc. x = lincomb_list lc (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis in_span_listE)
[PROOF STATE]
proof (state)
this:
x = lincomb_list lc (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from lincomb_list_add_vec_2[OF us this i]
[PROOF STATE]
proof (chain)
picking this:
x = lincomb_list (lc(j := lc j + lc i * c)) us
[PROOF STEP]
have "x \<in> span_list us"
[PROOF STATE]
proof (prove)
using this:
x = lincomb_list (lc(j := lc j + lc i * c)) us

goal (1 subgoal):
 1. x \<in> span_list us
[PROOF STEP]
unfolding span_list_def
[PROOF STATE]
proof (prove)
using this:
x = lincomb_list (lc(j := lc j + lc i * c)) us

goal (1 subgoal):
 1. x \<in> {uu_. \<exists>c. uu_ = lincomb_list c us}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> span_list us

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x3 \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<Longrightarrow> ?x3 \<in> span_list us

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x3 \<in> span_list us \<Longrightarrow> ?x3 \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
?x3 \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<Longrightarrow> ?x3 \<in> span_list us
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> span_list us \<Longrightarrow> ?x3 \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
?x3 \<in> span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<Longrightarrow> ?x3 \<in> span_list us

goal (1 subgoal):
 1. span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
span_list us = span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
have "\<dots> = span (set ?ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
unfolding span_list_as_span[OF ws]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j])) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
span_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))

goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))

goal (1 subgoal):
 1. local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
local.span (set us) = local.span (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))

goal:
No subgoals!
[PROOF STEP]
qed