[STATEMENT]
lemma lincomb_as_lincomb_list_distinct:
  assumes s: "set ws \<subseteq> carrier_vec n" and d: "distinct ws"
  shows "lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws
[PROOF STEP]
proof (insert assms, induct ws)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>set [] \<subseteq> carrier_vec n; distinct []\<rbrakk> \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. f ([] ! i)) []
 2. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
set [] \<subseteq> carrier_vec n
distinct []

goal (2 subgoals):
 1. \<lbrakk>set [] \<subseteq> carrier_vec n; distinct []\<rbrakk> \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. f ([] ! i)) []
 2. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set [] \<subseteq> carrier_vec n
distinct []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set [] \<subseteq> carrier_vec n
distinct []

goal (1 subgoal):
 1. lincomb f (set []) = lincomb_list (\<lambda>i. f ([] ! i)) []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb f (set []) = lincomb_list (\<lambda>i. f ([] ! i)) []

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
case (Cons a ws)
[PROOF STATE]
proof (state)
this:
\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws
set (a # ws) \<subseteq> carrier_vec n
distinct (a # ws)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have [simp]: "\<And>v. v \<in> set ws \<Longrightarrow> v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. v \<in> set ws \<Longrightarrow> v \<in> carrier_vec n
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
set (a # ws) \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?v1 \<in> set ws \<Longrightarrow> ?v1 \<in> carrier_vec n
[PROOF STEP]
have ws: "set ws \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
?v1 \<in> set ws \<Longrightarrow> ?v1 \<in> carrier_vec n

goal (1 subgoal):
 1. set ws \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ws \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have hyp: "lincomb f (set (ws)) = lincomb_list (\<lambda>i. f (ws ! i)) ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws
[PROOF STEP]
proof (intro Cons.hyps ws)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct ws
[PROOF STEP]
show "distinct ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct ws
[PROOF STEP]
using Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
distinct (a # ws)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have "(map (\<lambda>i. f (ws ! i) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. f (ws ! i) \<cdot>\<^sub>v ws ! i) [0..<length ws] = map (\<lambda>v. f v \<cdot>\<^sub>v v) ws
[PROOF STEP]
by (intro nth_equalityI, auto)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. f (ws ! i) \<cdot>\<^sub>v ws ! i) [0..<length ws] = map (\<lambda>v. f v \<cdot>\<^sub>v v) ws

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
with ws
[PROOF STATE]
proof (chain)
picking this:
set ws \<subseteq> carrier_vec n
map (\<lambda>i. f (ws ! i) \<cdot>\<^sub>v ws ! i) [0..<length ws] = map (\<lambda>v. f v \<cdot>\<^sub>v v) ws
[PROOF STEP]
have sumlist_rw: "sumlist (map (\<lambda>i. f (ws ! i) \<cdot>\<^sub>v ws ! i) [0..<length ws])
    = sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)"
[PROOF STATE]
proof (prove)
using this:
set ws \<subseteq> carrier_vec n
map (\<lambda>i. f (ws ! i) \<cdot>\<^sub>v ws ! i) [0..<length ws] = map (\<lambda>v. f v \<cdot>\<^sub>v v) ws

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. f (ws ! i) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)
[PROOF STEP]
by (subst (1 2) sumlist_as_summset, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. f (ws ! i) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have "lincomb f (set (a # ws)) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set (a # ws)) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v)
[PROOF STEP]
unfolding lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
lincomb f (set (a # ws)) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb f (set (a # ws)) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have "... = (\<Oplus>\<^bsub>V\<^esub>v\<in> insert a (set ws). f v \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have "... = (f a \<cdot>\<^sub>v a) + (\<Oplus>\<^bsub>V\<^esub>v\<in> (set ws). f v \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v)
[PROOF STEP]
by (rule finsum_insert, insert Cons.prems, auto)
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have "... = f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. f (ws ! i)) ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. f (ws ! i)) ws
[PROOF STEP]
using hyp lincomb_def
[PROOF STATE]
proof (prove)
using this:
lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws
lincomb ?a ?A = (\<Oplus>\<^bsub>V\<^esub>v\<in>?A. ?a v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. f (ws ! i)) ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. f (ws ! i)) ws

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. f (ws ! i)) ws

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have "... = f a \<cdot>\<^sub>v a + sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. f (ws ! i)) ws = f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)
[PROOF STEP]
unfolding lincomb_list_def sumlist_rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. f (ws ! i)) ws = f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. f (ws ! i)) ws = f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have "... = sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
let ?a = "(map (\<lambda>v. f v \<cdot>\<^sub>v v) [a])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
have a: "a \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier_vec n
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
set (a # ws) \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
have "f a \<cdot>\<^sub>v a = sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a])
[PROOF STEP]
using Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
set (a # ws) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a])

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
hence "f a \<cdot>\<^sub>v a + sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)
      = sumlist ?a + sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)"
[PROOF STATE]
proof (prove)
using this:
f a \<cdot>\<^sub>v a = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a])

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a]) + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a]) + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a]) + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
have "... = sumlist (?a @ (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a]) + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a] @ map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)
[PROOF STEP]
by (rule sumlist_append[symmetric], auto simp add: a)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a]) + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a] @ map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a] @ map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) [a] @ map (\<lambda>v. f v \<cdot>\<^sub>v v) ws)

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) ws) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have "... = sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws)) = M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws)) = M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])
[PROOF STEP]
have u: "(map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])
        = (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)] = map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws)
[PROOF STEP]
proof (intro nth_equalityI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)]) = length (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
 2. \<And>i. i < length (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)]) \<Longrightarrow> map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)] ! i = map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws) ! i
[PROOF STEP]
case (2 i)
[PROOF STATE]
proof (state)
this:
i < length (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])

goal (2 subgoals):
 1. length (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)]) = length (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
 2. \<And>i. i < length (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)]) \<Longrightarrow> map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)] ! i = map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws) ! i
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
i < length (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])

goal (1 subgoal):
 1. map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)] ! i = map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws) ! i
[PROOF STEP]
by (smt length_map map_nth nth_map)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)] ! i = map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws) ! i

goal (1 subgoal):
 1. length (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)]) = length (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)] = map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws)

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws)) = M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws)) = M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])
[PROOF STEP]
unfolding u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws)) = M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws)) = M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws)) = M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>v. f v \<cdot>\<^sub>v v) (a # ws)) = M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
have "... = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)]) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
unfolding lincomb_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)]) = M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)])
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. f ((a # ws) ! i) \<cdot>\<^sub>v (a # ws) ! i) [0..<length (a # ws)]) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)

goal (1 subgoal):
 1. \<And>a ws. \<lbrakk>\<lbrakk>set ws \<subseteq> carrier_vec n; distinct ws\<rbrakk> \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws; set (a # ws) \<subseteq> carrier_vec n; distinct (a # ws)\<rbrakk> \<Longrightarrow> lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)

goal (1 subgoal):
 1. lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lincomb f (set (a # ws)) = lincomb_list (\<lambda>i. f ((a # ws) ! i)) (a # ws)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lin_dep_cols_imp_det_0':
  fixes ws
  defines "A \<equiv> mat_of_cols n ws"
  assumes dimv_ws: "\<forall>w\<in>set ws. dim_vec w = n"
  assumes A: "A \<in> carrier_mat n n" and ld_cols: "lin_dep (set (cols A))"
  shows  "det A = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A = (0::'a)
[PROOF STEP]
proof (cases "distinct ws")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
 2. \<not> distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> distinct ws

goal (2 subgoals):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
 2. \<not> distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
obtain i j where ij: "i\<noteq>j" and c: "col A i = col A j" and i: "i<n" and j: "j<n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i \<noteq> j; col A i = col A j; i < n; j < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using False A
[PROOF STATE]
proof (prove)
using this:
\<not> distinct ws
A \<in> carrier_mat n n

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i \<noteq> j; col A i = col A j; i < n; j < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
\<not> distinct ws
mat_of_cols n ws \<in> carrier_mat n n

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i \<noteq> j; col (mat_of_cols n ws) i = col (mat_of_cols n ws) j; i < n; j < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis dimv_ws distinct_conv_nth carrier_matD(2)
        col_mat_of_cols mat_of_cols_carrier(3) nth_mem carrier_vecI)
[PROOF STATE]
proof (state)
this:
i \<noteq> j
col A i = col A j
i < n
j < n

goal (2 subgoals):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
 2. \<not> distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A = (0::'a)
[PROOF STEP]
by (rule det_identical_columns[OF A ij i j c])
[PROOF STATE]
proof (state)
this:
det A = (0::'a)

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
distinct ws

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
have d1[simp]: "\<And>x. x \<in> set ws \<Longrightarrow> x \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set ws \<Longrightarrow> x \<in> carrier_vec n
[PROOF STEP]
using dimv_ws
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set ws. dim_vec w = n

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

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
obtain A' f' v where f'_in: "f' \<in> A' \<rightarrow> UNIV"
    and lc_f': "lincomb f' A' = 0\<^sub>v n" and f'_v: "f' v \<noteq> 0"
    and v_A': "v \<in> A'" and A'_in_rows: "A' \<subseteq> set (cols A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f' A' v. \<lbrakk>f' \<in> A' \<rightarrow> UNIV; lincomb f' A' = 0\<^sub>v n; f' v \<noteq> (0::'a); v \<in> A'; A' \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ld_cols
[PROOF STATE]
proof (prove)
using this:
lin_dep (set (cols A))

goal (1 subgoal):
 1. (\<And>f' A' v. \<lbrakk>f' \<in> A' \<rightarrow> UNIV; lincomb f' A' = 0\<^sub>v n; f' v \<noteq> (0::'a); v \<in> A'; A' \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding lin_dep_def
[PROOF STATE]
proof (prove)
using this:
\<exists>Aa a v. finite Aa \<and> Aa \<subseteq> set (cols A) \<and> True \<and> lincomb a Aa = 0\<^sub>v n \<and> v \<in> Aa \<and> a v \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<And>f' A' v. \<lbrakk>f' \<in> A' \<rightarrow> UNIV; lincomb f' A' = 0\<^sub>v n; f' v \<noteq> (0::'a); v \<in> A'; A' \<subseteq> set (cols A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' \<in> A' \<rightarrow> UNIV
lincomb f' A' = 0\<^sub>v n
f' v \<noteq> (0::'a)
v \<in> A'
A' \<subseteq> set (cols A)

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
define f where "f \<equiv> \<lambda>x. if x \<notin> A' then 0 else f' x"
[PROOF STATE]
proof (state)
this:
f \<equiv> \<lambda>x. if x \<notin> A' then 0::'a else f' x

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
have f_in: "f \<in> (set (cols A)) \<rightarrow> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> set (cols A) \<rightarrow> UNIV
[PROOF STEP]
using f'_in
[PROOF STATE]
proof (prove)
using this:
f' \<in> A' \<rightarrow> UNIV

goal (1 subgoal):
 1. f \<in> set (cols A) \<rightarrow> UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> set (cols A) \<rightarrow> UNIV

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
have A'_in_carrier: "A' \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' \<subseteq> carrier_vec n
[PROOF STEP]
by (metis (no_types) A'_in_rows A_def cols_dim carrier_matD(1) mat_of_cols_carrier(1) subset_trans)
[PROOF STATE]
proof (state)
this:
A' \<subseteq> carrier_vec n

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
have lc_f: "lincomb f (set (cols A)) = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set (cols A)) = 0\<^sub>v n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lincomb f (set (cols A)) = 0\<^sub>v n
[PROOF STEP]
have l1: "lincomb f (set (cols A) - A') = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set (cols A) - A') = 0\<^sub>v n
[PROOF STEP]
by (rule lincomb_zero, auto simp add: f_def, insert A cols_dim, blast)
[PROOF STATE]
proof (state)
this:
lincomb f (set (cols A) - A') = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb f (set (cols A)) = 0\<^sub>v n
[PROOF STEP]
have l2: "lincomb f A' = 0\<^sub>v n "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f A' = 0\<^sub>v n
[PROOF STEP]
using lc_f'
[PROOF STATE]
proof (prove)
using this:
lincomb f' A' = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb f A' = 0\<^sub>v n
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
lincomb f' A' = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb (\<lambda>x. if x \<notin> A' then 0::'a else f' x) A' = 0\<^sub>v n
[PROOF STEP]
using A'_in_carrier
[PROOF STATE]
proof (prove)
using this:
lincomb f' A' = 0\<^sub>v n
A' \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb (\<lambda>x. if x \<notin> A' then 0::'a else f' x) A' = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb f A' = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb f (set (cols A)) = 0\<^sub>v n
[PROOF STEP]
have "lincomb f (set (cols A)) = lincomb f (set (cols A) - A') + lincomb f A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set (cols A)) = lincomb f (set (cols A) - A') + lincomb f A'
[PROOF STEP]
proof (rule lincomb_vec_diff_add)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. set (cols A) \<subseteq> carrier_vec n
 2. A' \<subseteq> set (cols A)
 3. finite (set (cols A))
 4. f \<in> set (cols A) \<rightarrow> UNIV
[PROOF STEP]
show "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 cols_dim
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
set (cols ?A) \<subseteq> carrier_vec (dim_row ?A)

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

goal (3 subgoals):
 1. A' \<subseteq> set (cols A)
 2. finite (set (cols A))
 3. f \<in> set (cols A) \<rightarrow> UNIV
[PROOF STEP]
show "A' \<subseteq> set (cols A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' \<subseteq> set (cols A)
[PROOF STEP]
using A'_in_rows
[PROOF STATE]
proof (prove)
using this:
A' \<subseteq> set (cols A)

goal (1 subgoal):
 1. A' \<subseteq> set (cols A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A' \<subseteq> set (cols A)

goal (2 subgoals):
 1. finite (set (cols A))
 2. f \<in> set (cols A) \<rightarrow> UNIV
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
lincomb f (set (cols A)) = lincomb f (set (cols A) - A') + lincomb f A'

goal (1 subgoal):
 1. lincomb f (set (cols A)) = 0\<^sub>v n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb f (set (cols A)) = lincomb f (set (cols A) - A') + lincomb f A'

goal (1 subgoal):
 1. lincomb f (set (cols A)) = 0\<^sub>v n
[PROOF STEP]
have "... =  0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set (cols A) - A') + lincomb f A' = 0\<^sub>v n
[PROOF STEP]
using l1 l2
[PROOF STATE]
proof (prove)
using this:
lincomb f (set (cols A) - A') = 0\<^sub>v n
lincomb f A' = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb f (set (cols A) - A') + lincomb f A' = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb f (set (cols A) - A') + lincomb f A' = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb f (set (cols A)) = 0\<^sub>v n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb f (set (cols A)) = 0\<^sub>v n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lincomb f (set (cols A)) = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb f (set (cols A)) = 0\<^sub>v n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lincomb f (set (cols A)) = 0\<^sub>v n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lincomb f (set (cols A)) = 0\<^sub>v n

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
have v_in: "v \<in> (set (cols A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> set (cols A)
[PROOF STEP]
using v_A' A'_in_rows
[PROOF STATE]
proof (prove)
using this:
v \<in> A'
A' \<subseteq> set (cols A)

goal (1 subgoal):
 1. v \<in> set (cols A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> set (cols A)

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
have fv: "f v \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f v \<noteq> (0::'a)
[PROOF STEP]
using f'_v v_A'
[PROOF STATE]
proof (prove)
using this:
f' v \<noteq> (0::'a)
v \<in> A'

goal (1 subgoal):
 1. f v \<noteq> (0::'a)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
f' v \<noteq> (0::'a)
v \<in> A'

goal (1 subgoal):
 1. (if v \<notin> A' then 0::'a else f' v) \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f v \<noteq> (0::'a)

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
let ?c = "(\<lambda>i. f (ws ! i))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
have "lincomb f (set ws) = lincomb_list ?c ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws
[PROOF STEP]
by (rule lincomb_as_lincomb_list_distinct[OF _ True], auto)
[PROOF STATE]
proof (state)
this:
lincomb f (set ws) = lincomb_list (\<lambda>i. f (ws ! i)) ws

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
have "\<exists>v.  v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> A *\<^sub>v v = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> A *\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
proof (rule exI[of _ " vec (length ws) ?c"], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<in> carrier_vec n
 2. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
show "vec (length ws) ?c \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<in> carrier_vec n
[PROOF STEP]
using A A_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
A \<equiv> mat_of_cols n ws

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec (length ws) (\<lambda>i. f (ws ! i)) \<in> carrier_vec n

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
have vec_not0: "vec (length ws) ?c \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n
[PROOF STEP]
obtain i where ws_i: "(ws ! i) = v" and i: "i<length ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>ws ! i = v; i < length ws\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using v_in
[PROOF STATE]
proof (prove)
using this:
v \<in> set (cols A)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>ws ! i = v; i < length ws\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
v \<in> set (cols (mat_of_cols n ws))

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>ws ! i = v; i < length ws\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis d1 cols_mat_of_cols in_set_conv_nth subset_eq)
[PROOF STATE]
proof (state)
this:
ws ! i = v
i < length ws

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n
[PROOF STEP]
have "vec (length ws) ?c $ i = ?c i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) $ i = f (ws ! i)
[PROOF STEP]
by (rule index_vec[OF i])
[PROOF STATE]
proof (state)
this:
vec (length ws) (\<lambda>i. f (ws ! i)) $ i = f (ws ! i)

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec (length ws) (\<lambda>i. f (ws ! i)) $ i = f (ws ! i)

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n
[PROOF STEP]
have "... = f v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (ws ! i) = f v
[PROOF STEP]
using ws_i
[PROOF STATE]
proof (prove)
using this:
ws ! i = v

goal (1 subgoal):
 1. f (ws ! i) = f v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (ws ! i) = f v

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (ws ! i) = f v

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n
[PROOF STEP]
have "... \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f v \<noteq> (0::'a)
[PROOF STEP]
using fv
[PROOF STATE]
proof (prove)
using this:
f v \<noteq> (0::'a)

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

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
vec (length ws) (\<lambda>i. f (ws ! i)) $ i \<noteq> (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vec (length ws) (\<lambda>i. f (ws ! i)) $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n
[PROOF STEP]
using A A_def i
[PROOF STATE]
proof (prove)
using this:
vec (length ws) (\<lambda>i. f (ws ! i)) $ i \<noteq> (0::'a)
A \<in> carrier_mat n n
A \<equiv> mat_of_cols n ws
i < length ws

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
have "A *\<^sub>v vec (length ws) ?c = mat_of_cols n ws *\<^sub>v vec (length ws) ?c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = mat_of_cols n ws *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i))
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cols n ws *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = mat_of_cols n ws *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = mat_of_cols n ws *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i))

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = mat_of_cols n ws *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i))

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
have "... = lincomb_list ?c ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cols n ws *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = lincomb_list (\<lambda>i. f (ws ! i)) ws
[PROOF STEP]
by (rule lincomb_list_as_mat_mult[symmetric, OF dimv_ws])
[PROOF STATE]
proof (state)
this:
mat_of_cols n ws *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = lincomb_list (\<lambda>i. f (ws ! i)) ws

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_cols n ws *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = lincomb_list (\<lambda>i. f (ws ! i)) ws

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
have "... = lincomb f (set ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>i. f (ws ! i)) ws = lincomb f (set ws)
[PROOF STEP]
by (rule lincomb_as_lincomb_list_distinct[symmetric, OF _ True], auto)
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. f (ws ! i)) ws = lincomb f (set ws)

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. f (ws ! i)) ws = lincomb f (set ws)

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
have "... =  0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set ws) = 0\<^sub>v n
[PROOF STEP]
using lc_f
[PROOF STATE]
proof (prove)
using this:
lincomb f (set (cols A)) = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb f (set ws) = 0\<^sub>v n
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
lincomb f (set (cols (mat_of_cols n ws))) = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb f (set ws) = 0\<^sub>v n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
lincomb f (set (cols (mat_of_cols n ws))) = 0\<^sub>v n
A \<in> carrier_mat n n

goal (1 subgoal):
 1. lincomb f (set ws) = 0\<^sub>v n
[PROOF STEP]
by (simp add: subset_code(1))
[PROOF STATE]
proof (state)
this:
lincomb f (set ws) = 0\<^sub>v n

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
show "vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
using vec_not0
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
vec (length ws) (\<lambda>i. f (ws ! i)) \<noteq> 0\<^sub>v n \<and> A *\<^sub>v vec (length ws) (\<lambda>i. f (ws ! i)) = 0\<^sub>v n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> A *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. distinct ws \<Longrightarrow> det A = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> A *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. det A = (0::'a)
[PROOF STEP]
unfolding det_0_iff_vec_prod_zero[OF A]
[PROOF STATE]
proof (prove)
using this:
\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> A *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> A *\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det A = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lin_dep_cols_imp_det_0:
  assumes A: "A \<in> carrier_mat n n" and ld: "lin_dep (set (cols A))"
  shows "det A = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det A = (0::'a)
[PROOF STEP]
have col_rw: "(cols (mat_of_cols n (cols A))) = cols A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cols (mat_of_cols n (cols A)) = cols A
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

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

goal (1 subgoal):
 1. det A = (0::'a)
[PROOF STEP]
have m: "mat_of_cols n (cols A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cols n (cols A) = A
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

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

goal (1 subgoal):
 1. det A = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A = (0::'a)
[PROOF STEP]
by (rule A lin_dep_cols_imp_det_0'[of "cols A", unfolded col_rw, unfolded m, OF _ A ld])
     (metis A cols_dim carrier_matD(1) subsetCE carrier_vecD)
[PROOF STATE]
proof (state)
this:
det A = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_not_0_imp_lin_indpt_rows:
  assumes A: "A \<in> carrier_mat n n" and det: "det A \<noteq> 0"
  shows "lin_indpt (set (rows A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt (set (rows A))
[PROOF STEP]
using lin_dep_rows_imp_det_0[OF A] det
[PROOF STATE]
proof (prove)
using this:
lin_dep (set (rows A)) \<Longrightarrow> det A = (0::'a)
det A \<noteq> (0::'a)

goal (1 subgoal):
 1. lin_indpt (set (rows A))
[PROOF STEP]
by auto


[STATEMENT]
lemma upper_triangular_imp_lin_indpt_rows:
  assumes A: "A \<in> carrier_mat n n"
    and tri: "upper_triangular A"
    and diag: "0 \<notin> set (diag_mat A)"
  shows "lin_indpt (set (rows A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt (set (rows A))
[PROOF STEP]
using det_not_0_imp_lin_indpt_rows upper_triangular_imp_det_eq_0_iff assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat n n; det ?A \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> lin_indpt (set (rows ?A))
\<lbrakk>?A \<in> carrier_mat ?n ?n; upper_triangular ?A\<rbrakk> \<Longrightarrow> (det ?A = (0::?'a)) = ((0::?'a) \<in> set (diag_mat ?A))
A \<in> carrier_mat n n
upper_triangular A
(0::'a) \<notin> set (diag_mat A)

goal (1 subgoal):
 1. lin_indpt (set (rows A))
[PROOF STEP]
by auto