[STATEMENT]
lemma lin_indpt_list_add_vec: assumes
      i: "j < length us" "i < length us" "i \<noteq> j"
   and indep: "lin_indpt_list  us"
shows "lin_indpt_list (us [i := us ! i + c \<cdot>\<^sub>v us ! j])" (is "lin_indpt_list ?V")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from indep[unfolded lin_indpt_list_def]
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> carrier_vec n \<and> distinct us \<and> lin_indpt (set us)
[PROOF STEP]
have us: "set us \<subseteq> carrier_vec n"
    and dist: "distinct us" and indep: "lin_indpt (set us)"
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n \<and> distinct us \<and> lin_indpt (set us)

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

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
let ?E = "set us - {us ! i}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
let ?us = "insert (us ! i) ?E"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
let ?v = "us ! i + c \<cdot>\<^sub>v us ! j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lin_indpt_list (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 usi: "us ! i \<in> carrier_vec n" "us ! i \<notin> ?E" "us ! i \<in> set us"
    and usj: "us ! 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 ! i \<notin> set us - {us ! i} &&& us ! i \<in> set us) &&& us ! j \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
us ! i \<in> carrier_vec n
us ! i \<notin> set us - {us ! i}
us ! i \<in> set us
us ! j \<in> carrier_vec n

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from usi usj
[PROOF STATE]
proof (chain)
picking this:
us ! i \<in> carrier_vec n
us ! i \<notin> set us - {us ! i}
us ! i \<in> set us
us ! j \<in> carrier_vec n
[PROOF STEP]
have v: "?v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
us ! i \<in> carrier_vec n
us ! i \<notin> set us - {us ! i}
us ! i \<in> set us
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. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have fin: "finite ?E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set us - {us ! i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set us - {us ! i})

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have id: "set us = insert (us ! i) (set us - {us ! i})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set us = insert (us ! i) (set us - {us ! i})
[PROOF STEP]
using i(2)
[PROOF STATE]
proof (prove)
using this:
i < length us

goal (1 subgoal):
 1. set us = insert (us ! i) (set us - {us ! i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set us = insert (us ! i) (set us - {us ! i})

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from dist i
[PROOF STATE]
proof (chain)
picking this:
distinct us
j < length us
i < length us
i \<noteq> j
[PROOF STEP]
have diff': "us ! i \<noteq> us ! j"
[PROOF STATE]
proof (prove)
using this:
distinct us
j < length us
i < length us
i \<noteq> j

goal (1 subgoal):
 1. us ! i \<noteq> us ! j
[PROOF STEP]
unfolding distinct_conv_nth
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length us. \<forall>j<length us. i \<noteq> j \<longrightarrow> us ! i \<noteq> us ! j
j < length us
i < length us
i \<noteq> j

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

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from subset_li_is_li[OF indep]
[PROOF STATE]
proof (chain)
picking this:
?B \<subseteq> set us \<Longrightarrow> lin_indpt ?B
[PROOF STEP]
have indepE: "lin_indpt ?E"
[PROOF STATE]
proof (prove)
using this:
?B \<subseteq> set us \<Longrightarrow> lin_indpt ?B

goal (1 subgoal):
 1. lin_indpt (set us - {us ! i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lin_indpt (set us - {us ! i})

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have Vid: "set ?V = insert ?v ?E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) = insert (us ! i + c \<cdot>\<^sub>v us ! j) (set us - {us ! i})
[PROOF STEP]
using set_update_distinct[OF dist i(2)]
[PROOF STATE]
proof (prove)
using this:
set (us[i := ?x]) = insert ?x (set us - {us ! i})

goal (1 subgoal):
 1. set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) = insert (us ! i + c \<cdot>\<^sub>v us ! j) (set us - {us ! i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) = insert (us ! i + c \<cdot>\<^sub>v us ! j) (set us - {us ! i})

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have E: "?E \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set us - {us ! i} \<subseteq> carrier_vec n
[PROOF STEP]
using us
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n

goal (1 subgoal):
 1. set us - {us ! i} \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set us - {us ! i} \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have V: "set ?V \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n
[PROOF STEP]
using us v
[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 Vid
[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. insert (us ! i + c \<cdot>\<^sub>v us ! j) (set us - {us ! i}) \<subseteq> carrier_vec n
[PROOF STEP]
by 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. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from dist i
[PROOF STATE]
proof (chain)
picking this:
distinct us
j < length us
i < length us
i \<noteq> j
[PROOF STEP]
have diff: "us ! i \<noteq> us ! j"
[PROOF STATE]
proof (prove)
using this:
distinct us
j < length us
i < length us
i \<noteq> j

goal (1 subgoal):
 1. us ! i \<noteq> us ! j
[PROOF STEP]
unfolding distinct_conv_nth
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length us. \<forall>j<length us. i \<noteq> j \<longrightarrow> us ! i \<noteq> us ! j
j < length us
i < length us
i \<noteq> j

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

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
have vspan: "?v \<notin> span ?E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<notin> local.span (set us - {us ! i})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
assume mem: "?v \<in> span ?E"
[PROOF STATE]
proof (state)
this:
us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i})

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
from diff i
[PROOF STATE]
proof (chain)
picking this:
us ! i \<noteq> us ! j
j < length us
i < length us
i \<noteq> j
[PROOF STEP]
have "us ! j \<in> ?E"
[PROOF STATE]
proof (prove)
using this:
us ! i \<noteq> us ! j
j < length us
i < length us
i \<noteq> j

goal (1 subgoal):
 1. us ! j \<in> set us - {us ! i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
us ! j \<in> set us - {us ! i}

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

goal (1 subgoal):
 1. us ! j \<in> local.span (set us - {us ! i})
[PROOF STEP]
using E
[PROOF STATE]
proof (prove)
using this:
us ! j \<in> set us - {us ! i}
set us - {us ! i} \<subseteq> carrier_vec n

goal (1 subgoal):
 1. us ! j \<in> local.span (set us - {us ! i})
[PROOF STEP]
by (metis span_mem)
[PROOF STATE]
proof (state)
this:
us ! j \<in> local.span (set us - {us ! i})

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

goal (1 subgoal):
 1. - c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i})
[PROOF STEP]
using smult_in_span[OF E]
[PROOF STATE]
proof (prove)
using this:
us ! j \<in> local.span (set us - {us ! i})
?x \<in> local.span (set us - {us ! i}) \<Longrightarrow> ?c \<cdot>\<^sub>v ?x \<in> local.span (set us - {us ! i})

goal (1 subgoal):
 1. - c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i})

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
from span_add1[OF E mem this]
[PROOF STATE]
proof (chain)
picking this:
us ! i + c \<cdot>\<^sub>v us ! j + - c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i})
[PROOF STEP]
have "?v + (- c \<cdot>\<^sub>v us ! j) \<in> span ?E"
[PROOF STATE]
proof (prove)
using this:
us ! i + c \<cdot>\<^sub>v us ! j + - c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i})

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

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

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
have "?v + (- c \<cdot>\<^sub>v us ! j) = us ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j + - c \<cdot>\<^sub>v us ! j = us ! i
[PROOF STEP]
using usi usj
[PROOF STATE]
proof (prove)
using this:
us ! i \<in> carrier_vec n
us ! i \<notin> set us - {us ! i}
us ! i \<in> set us
us ! j \<in> carrier_vec n

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

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
us ! i \<in> local.span (set us - {us ! i})
[PROOF STEP]
have mem: "us ! i \<in> span ?E"
[PROOF STATE]
proof (prove)
using this:
us ! i \<in> local.span (set us - {us ! i})

goal (1 subgoal):
 1. us ! i \<in> local.span (set us - {us ! i})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
us ! i \<in> local.span (set us - {us ! i})

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
from in_spanE[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a A. us ! i = lincomb a A \<and> finite A \<and> A \<subseteq> set us - {us ! i}
[PROOF STEP]
obtain a A where lc: "us ! i = lincomb a A" and A: "finite A"
      "A \<subseteq> set us - {us ! i}"
[PROOF STATE]
proof (prove)
using this:
\<exists>a A. us ! i = lincomb a A \<and> finite A \<and> A \<subseteq> set us - {us ! i}

goal (1 subgoal):
 1. (\<And>a A. \<lbrakk>us ! i = lincomb a A; finite A; A \<subseteq> set us - {us ! i}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
us ! i = lincomb a A
finite A
A \<subseteq> set us - {us ! i}

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
let ?a = "a (us ! i := -1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
let ?A = "insert (us ! i) A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
finite A
A \<subseteq> set us - {us ! i}
[PROOF STEP]
have fin: "finite ?A"
[PROOF STATE]
proof (prove)
using this:
finite A
A \<subseteq> set us - {us ! i}

goal (1 subgoal):
 1. finite (insert (us ! i) A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (insert (us ! i) A)

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
have lc: "lincomb ?a A = us ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (a(us ! i := - (1::'a))) A = us ! i
[PROOF STEP]
unfolding lc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (a(lincomb a A := - (1::'a))) A = lincomb a A
[PROOF STEP]
by (rule lincomb_cong, insert A us lc, auto)
[PROOF STATE]
proof (state)
this:
lincomb (a(us ! i := - (1::'a))) A = us ! i

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
have "lincomb ?a ?A = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (a(us ! i := - (1::'a))) (insert (us ! i) A) = 0\<^sub>v n
[PROOF STEP]
by (subst lincomb_insert2[OF A(1)], insert A us lc usi diff, auto)
[PROOF STATE]
proof (state)
this:
lincomb (a(us ! i := - (1::'a))) (insert (us ! i) A) = 0\<^sub>v n

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i}) \<Longrightarrow> False
[PROOF STEP]
from not_lindepD[OF indep _ _ _ this] A usi
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite (insert (us ! i) A); insert (us ! i) A \<subseteq> set us; a(us ! i := - (1::'a)) \<in> insert (us ! i) A \<rightarrow> UNIV\<rbrakk> \<Longrightarrow> a(us ! i := - (1::'a)) \<in> insert (us ! i) A \<rightarrow> {0::'a}
finite A
A \<subseteq> set us - {us ! i}
us ! i \<in> carrier_vec n
us ! i \<notin> set us - {us ! i}
us ! i \<in> set us
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (insert (us ! i) A); insert (us ! i) A \<subseteq> set us; a(us ! i := - (1::'a)) \<in> insert (us ! i) A \<rightarrow> UNIV\<rbrakk> \<Longrightarrow> a(us ! i := - (1::'a)) \<in> insert (us ! i) A \<rightarrow> {0::'a}
finite A
A \<subseteq> set us - {us ! i}
us ! i \<in> carrier_vec n
us ! i \<notin> set us - {us ! i}
us ! i \<in> set us

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
us ! i + c \<cdot>\<^sub>v us ! j \<notin> local.span (set us - {us ! i})

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
hence vmem: "?v \<notin> ?E"
[PROOF STATE]
proof (prove)
using this:
us ! i + c \<cdot>\<^sub>v us ! j \<notin> local.span (set us - {us ! i})

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<notin> set us - {us ! i}
[PROOF STEP]
using span_mem[OF E, of ?v]
[PROOF STATE]
proof (prove)
using this:
us ! i + c \<cdot>\<^sub>v us ! j \<notin> local.span (set us - {us ! i})
us ! i + c \<cdot>\<^sub>v us ! j \<in> set us - {us ! i} \<Longrightarrow> us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i})

goal (1 subgoal):
 1. us ! i + c \<cdot>\<^sub>v us ! j \<notin> set us - {us ! i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
us ! i + c \<cdot>\<^sub>v us ! j \<notin> set us - {us ! i}

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from lin_dep_iff_in_span[OF E indepE v this] vspan
[PROOF STATE]
proof (chain)
picking this:
(us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i})) = lin_dep (set us - {us ! i} \<union> {us ! i + c \<cdot>\<^sub>v us ! j})
us ! i + c \<cdot>\<^sub>v us ! j \<notin> local.span (set us - {us ! i})
[PROOF STEP]
have indep1: "lin_indpt (set ?V)"
[PROOF STATE]
proof (prove)
using this:
(us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i})) = lin_dep (set us - {us ! i} \<union> {us ! i + c \<cdot>\<^sub>v us ! j})
us ! i + c \<cdot>\<^sub>v us ! j \<notin> local.span (set us - {us ! i})

goal (1 subgoal):
 1. lin_indpt (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
[PROOF STEP]
unfolding Vid
[PROOF STATE]
proof (prove)
using this:
(us ! i + c \<cdot>\<^sub>v us ! j \<in> local.span (set us - {us ! i})) = lin_dep (set us - {us ! i} \<union> {us ! i + c \<cdot>\<^sub>v us ! j})
us ! i + c \<cdot>\<^sub>v us ! j \<notin> local.span (set us - {us ! i})

goal (1 subgoal):
 1. lin_indpt (insert (us ! i + c \<cdot>\<^sub>v us ! j) (set us - {us ! i}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lin_indpt (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
from vmem dist
[PROOF STATE]
proof (chain)
picking this:
us ! i + c \<cdot>\<^sub>v us ! j \<notin> set us - {us ! i}
distinct us
[PROOF STEP]
have "distinct ?V"
[PROOF STATE]
proof (prove)
using this:
us ! i + c \<cdot>\<^sub>v us ! j \<notin> set us - {us ! i}
distinct us

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

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
with indep1 V
[PROOF STATE]
proof (chain)
picking this:
lin_indpt (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n
distinct (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lin_indpt (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n
distinct (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

goal (1 subgoal):
 1. lin_indpt_list (us[i := us ! i + c \<cdot>\<^sub>v us ! j])
[PROOF STEP]
unfolding lin_indpt_list_def
[PROOF STATE]
proof (prove)
using this:
lin_indpt (set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]))
set (us[i := us ! i + c \<cdot>\<^sub>v us ! j]) \<subseteq> carrier_vec n
distinct (us[i := us ! i + c \<cdot>\<^sub>v us ! j])

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scalar_prod_lincomb_orthogonal: assumes ortho: "orthogonal gs" and gs: "set gs \<subseteq> carrier_vec n"
  shows "k \<le> length gs \<Longrightarrow> sumlist (map (\<lambda> i. g i \<cdot>\<^sub>v gs ! i) [0 ..< k]) \<bullet> sumlist (map (\<lambda> i. h i \<cdot>\<^sub>v gs ! i) [0 ..< k])
  = sum_list (map (\<lambda> i. g i * h i * (gs ! i \<bullet> gs ! i)) [0 ..< k])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i))
Suc k \<le> length gs

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
note ortho = orthogonalD[OF ortho]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < length gs; ?j < length gs\<rbrakk> \<Longrightarrow> (gs ! ?i \<bullet> gs ! ?j = (0::'a)) = (?i \<noteq> ?j)

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
let ?m = "length gs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
from gs Suc(2)
[PROOF STATE]
proof (chain)
picking this:
set gs \<subseteq> carrier_vec n
Suc k \<le> length gs
[PROOF STEP]
have gsi[simp]: "\<And> i. i \<le> k \<Longrightarrow> gs ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set gs \<subseteq> carrier_vec n
Suc k \<le> length gs

goal (1 subgoal):
 1. \<And>i. i \<le> k \<Longrightarrow> gs ! i \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 \<le> k \<Longrightarrow> gs ! ?i1 \<in> carrier_vec n

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i))
Suc k \<le> length gs
[PROOF STEP]
have kn: "k \<le> ?m" and k: "k < ?m"
[PROOF STATE]
proof (prove)
using this:
k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i))
Suc k \<le> length gs

goal (1 subgoal):
 1. k \<le> length gs &&& k < length gs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<le> length gs
k < length gs

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
let ?v1 = "sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k])"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
let ?v2 = "(g k \<cdot>\<^sub>v gs ! k)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
let ?w1 = "sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k])"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
let ?w2 = "(h k \<cdot>\<^sub>v gs ! k)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i))
Suc k \<le> length gs
[PROOF STEP]
have id: "[0 ..< Suc k] = [0 ..< k] @ [k]"
[PROOF STATE]
proof (prove)
using this:
k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i))
Suc k \<le> length gs

goal (1 subgoal):
 1. [0..<Suc k] = [0..<k] @ [k]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[0..<Suc k] = [0..<k] @ [k]

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have id: "sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = ?v1 + ?v2"
     "sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = ?w1 + ?w2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) + g k \<cdot>\<^sub>v gs ! k &&& M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) + h k \<cdot>\<^sub>v gs ! k
[PROOF STEP]
unfolding id map_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k] @ map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [k]) = M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) + g k \<cdot>\<^sub>v gs ! k &&& M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k] @ map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [k]) = M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) + h k \<cdot>\<^sub>v gs ! k
[PROOF STEP]
by (subst sumlist_append, insert Suc(2), auto)+
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) + g k \<cdot>\<^sub>v gs ! k
M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) + h k \<cdot>\<^sub>v gs ! k

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have v1: "?v1 \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<in> carrier_vec n
[PROOF STEP]
by (rule sumlist_carrier, insert Suc(2), auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<in> carrier_vec n

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have v2: "?v2 \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n
[PROOF STEP]
by (insert Suc(2), auto)
[PROOF STATE]
proof (state)
this:
g k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have w1: "?w1 \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) \<in> carrier_vec n
[PROOF STEP]
by (rule sumlist_carrier, insert Suc(2), auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) \<in> carrier_vec n

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have w2: "?w2 \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n
[PROOF STEP]
by (insert Suc(2), auto)
[PROOF STATE]
proof (state)
this:
h k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have gsk: "gs ! k \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs ! k \<in> carrier_vec n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gs ! k \<in> carrier_vec n

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have v12: "?v1 + ?v2 \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) + g k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n
[PROOF STEP]
using v1 v2
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<in> carrier_vec n
g k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) + g k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) + g k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have w12: "?w1 + ?w2 \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) + h k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n
[PROOF STEP]
using w1 w2
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) \<in> carrier_vec n
h k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) + h k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) + h k \<cdot>\<^sub>v gs ! k \<in> carrier_vec n

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have 0: "\<And> g h. i < k \<Longrightarrow> (g \<cdot>\<^sub>v gs ! i) \<bullet> (h \<cdot>\<^sub>v gs ! k) = 0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g h. i < k \<Longrightarrow> (g \<cdot>\<^sub>v gs ! i) \<bullet> (h \<cdot>\<^sub>v gs ! k) = (0::'a)
[PROOF STEP]
by (subst scalar_prod_smult_distrib[OF _ gsk], (insert k, auto)[1],
    subst smult_scalar_prod_distrib[OF _ gsk], (insert k, auto)[1], insert ortho[of i k] k, auto)
[PROOF STATE]
proof (state)
this:
?i2 < k \<Longrightarrow> (?g1 \<cdot>\<^sub>v gs ! ?i2) \<bullet> (?h1 \<cdot>\<^sub>v gs ! k) = (0::'a)

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have 1: "?v1 \<bullet> ?w2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> (h k \<cdot>\<^sub>v gs ! k) = (0::'a)
[PROOF STEP]
by (subst scalar_prod_left_sum_distrib[OF _ w2], (insert Suc(2), auto)[1], rule sum_list_neutral,
        insert 0, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> (h k \<cdot>\<^sub>v gs ! k) = (0::'a)

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
have 2: "?v2 \<bullet> ?w1 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g k \<cdot>\<^sub>v gs ! k) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (0::'a)
[PROOF STEP]
unfolding comm_scalar_prod[OF v2 w1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> (g k \<cdot>\<^sub>v gs ! k) = (0::'a)
[PROOF STEP]
apply (subst scalar_prod_left_sum_distrib[OF _ v2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. v \<in> set (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) \<Longrightarrow> v \<in> carrier_vec n
 2. (\<Sum>v\<leftarrow>map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]. v \<bullet> (g k \<cdot>\<^sub>v gs ! k)) = (0::'a)
[PROOF STEP]
apply ((insert gs, force)[1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<leftarrow>map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]. v \<bullet> (g k \<cdot>\<^sub>v gs ! k)) = (0::'a)
[PROOF STEP]
apply (rule sum_list_neutral)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>v. v \<bullet> (g k \<cdot>\<^sub>v gs ! k)) (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k])) \<Longrightarrow> x = (0::'a)
[PROOF STEP]
by (insert 0, auto)
[PROOF STATE]
proof (state)
this:
(g k \<cdot>\<^sub>v gs ! k) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (0::'a)

goal (2 subgoals):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
 2. \<And>k. \<lbrakk>k \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)); Suc k \<le> length gs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) + g k \<cdot>\<^sub>v gs ! k) \<bullet> (M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) + h k \<cdot>\<^sub>v gs ! k) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
unfolding scalar_prod_add_distrib[OF v12 w1 w2]
      add_scalar_prod_distrib[OF v1 v2 w1]
      add_scalar_prod_distrib[OF v1 v2 w2]
      scalar_prod_smult_distrib[OF w2 gsk]
      smult_scalar_prod_distrib[OF gsk gsk]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) + (g k \<cdot>\<^sub>v gs ! k) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) + (M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> (h k \<cdot>\<^sub>v gs ! k) + (g k \<cdot>\<^sub>v gs ! k) \<bullet> (h k \<cdot>\<^sub>v gs ! k)) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
unfolding Suc(1)[OF kn]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i)) + (g k \<cdot>\<^sub>v gs ! k) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k]) + (M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k]) \<bullet> (h k \<cdot>\<^sub>v gs ! k) + (g k \<cdot>\<^sub>v gs ! k) \<bullet> (h k \<cdot>\<^sub>v gs ! k)) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
by (simp add: 1 2 comm_scalar_prod[OF v2 w1])
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<Suc k]) = (\<Sum>i\<leftarrow>[0..<Suc k]. g i * h i * (gs ! i \<bullet> gs ! i))

goal (1 subgoal):
 1. 0 \<le> length gs \<Longrightarrow> M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<0]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<0]) = (\<Sum>i\<leftarrow>[0..<0]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
qed auto


[STATEMENT]
lemma Gramian_matrix_alt_def: "k \<le> length G \<Longrightarrow>
  Gramian_matrix G k = (let M = mat_of_rows n (take k G) in M * M\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> length G \<Longrightarrow> Gramian_matrix G k = (let M = mat_of_rows n (take k G) in M * M\<^sup>T)
[PROOF STEP]
unfolding Gramian_matrix_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> length G \<Longrightarrow> mat k n (\<lambda>(i, y). G ! i $ y) * (mat k n (\<lambda>(i, y). G ! i $ y))\<^sup>T = mat_of_rows n (take k G) * (mat_of_rows n (take k G))\<^sup>T
[PROOF STEP]
by (rule arg_cong[of _ _ "\<lambda> x. x * x\<^sup>T"], unfold mat_of_rows_def, intro eq_matI, auto)


[STATEMENT]
lemma Gramian_determinant_0 [simp]: "Gramian_determinant G 0 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gramian_determinant G 0 = (1::'b)
[PROOF STEP]
unfolding Gramian_determinant_def Gramian_matrix_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat 0 n (\<lambda>(i, y). G ! i $ y) * (mat 0 n (\<lambda>(i, y). G ! i $ y))\<^sup>T) = (1::'b)
[PROOF STEP]
by (simp add: times_mat_def)


[STATEMENT]
lemma orthogonal_imp_lin_indpt_list:
  assumes ortho: "orthogonal gs" and gs: "set gs \<subseteq> carrier_vec n"
  shows "lin_indpt_list gs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt_list gs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lin_indpt_list gs
[PROOF STEP]
from corthogonal_distinct[of gs] ortho
[PROOF STATE]
proof (chain)
picking this:
corthogonal gs \<Longrightarrow> distinct gs
orthogonal gs
[PROOF STEP]
have dist: "distinct gs"
[PROOF STATE]
proof (prove)
using this:
corthogonal gs \<Longrightarrow> distinct gs
orthogonal gs

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

goal (1 subgoal):
 1. lin_indpt_list gs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt_list gs
[PROOF STEP]
unfolding lin_indpt_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set gs \<subseteq> carrier_vec n \<and> distinct gs \<and> lin_indpt (set gs)
[PROOF STEP]
proof (intro conjI gs dist finite_lin_indpt2 finite_set)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
fix lc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
assume 0: "lincomb lc (set gs) = 0\<^sub>v n" (is "?lc = _")
[PROOF STATE]
proof (state)
this:
lincomb lc (set gs) = 0\<^sub>v n

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
have lc: "?lc \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb lc (set gs) \<in> carrier_vec n
[PROOF STEP]
by (rule lincomb_closed[OF gs])
[PROOF STATE]
proof (state)
this:
lincomb lc (set gs) \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
let ?m = "length gs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
from 0
[PROOF STATE]
proof (chain)
picking this:
lincomb lc (set gs) = 0\<^sub>v n
[PROOF STEP]
have "0 = ?lc \<bullet> ?lc"
[PROOF STATE]
proof (prove)
using this:
lincomb lc (set gs) = 0\<^sub>v n

goal (1 subgoal):
 1. (0::'a) = lincomb lc (set gs) \<bullet> lincomb lc (set gs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) = lincomb lc (set gs) \<bullet> lincomb lc (set gs)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) = lincomb lc (set gs) \<bullet> lincomb lc (set gs)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
have "?lc = lincomb_list (\<lambda>i. lc (gs ! i)) gs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb lc (set gs) = lincomb_list (\<lambda>i. lc (gs ! i)) gs
[PROOF STEP]
unfolding lincomb_as_lincomb_list_distinct[OF gs dist]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>i. lc (gs ! i)) gs = lincomb_list (\<lambda>i. lc (gs ! i)) gs
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
lincomb lc (set gs) = lincomb_list (\<lambda>i. lc (gs ! i)) gs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb lc (set gs) = lincomb_list (\<lambda>i. lc (gs ! i)) gs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
have "\<dots> = sumlist (map (\<lambda>i. lc (gs ! i) \<cdot>\<^sub>v gs ! i) [0..< ?m])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>i. lc (gs ! i)) gs = M.sumlist (map (\<lambda>i. lc (gs ! i) \<cdot>\<^sub>v gs ! i) [0..<length gs])
[PROOF STEP]
unfolding lincomb_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. lc (gs ! i) \<cdot>\<^sub>v gs ! i) [0..<length gs]) = M.sumlist (map (\<lambda>i. lc (gs ! i) \<cdot>\<^sub>v gs ! i) [0..<length gs])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. lc (gs ! i)) gs = M.sumlist (map (\<lambda>i. lc (gs ! i) \<cdot>\<^sub>v gs ! i) [0..<length gs])

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. lc (gs ! i)) gs = M.sumlist (map (\<lambda>i. lc (gs ! i) \<cdot>\<^sub>v gs ! i) [0..<length gs])

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
have "\<dots> \<bullet> \<dots> = (\<Sum>i\<leftarrow>[0..<?m]. (lc (gs ! i) * lc (gs ! i)) * sq_norm (gs ! i))" (is "_ = sum_list ?sum")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. lc (gs ! i) \<cdot>\<^sub>v gs ! i) [0..<length gs]) \<bullet> M.sumlist (map (\<lambda>i. lc (gs ! i) \<cdot>\<^sub>v gs ! i) [0..<length gs]) = (\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2)
[PROOF STEP]
unfolding scalar_prod_lincomb_orthogonal[OF ortho gs le_refl]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * (gs ! i \<bullet> gs ! i)) = (\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2)
[PROOF STEP]
by (auto simp: sq_norm_vec_as_cscalar_prod power2_eq_square)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. lc (gs ! i) \<cdot>\<^sub>v gs ! i) [0..<length gs]) \<bullet> M.sumlist (map (\<lambda>i. lc (gs ! i) \<cdot>\<^sub>v gs ! i) [0..<length gs]) = (\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'a) = (\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2)
[PROOF STEP]
have sum_0: "sum_list ?sum = 0"
[PROOF STATE]
proof (prove)
using this:
(0::'a) = (\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2)

goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) = (0::'a)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) = (0::'a)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
have nonneg: "\<And> x. x \<in> set ?sum \<Longrightarrow> x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs]) \<Longrightarrow> (0::'a) \<le> x
[PROOF STEP]
using zero_le_square[of "lc (gs ! i)" for i] sq_norm_vec_ge_0[of "gs ! i" for i]
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> lc (gs ! ?i5) * lc (gs ! ?i5)
(0::'a) \<le> \<parallel>gs ! ?i5\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs]) \<Longrightarrow> (0::'a) \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x3 \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs]) \<Longrightarrow> (0::'a) \<le> ?x3

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?x3 \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs]) \<Longrightarrow> (0::'a) \<le> ?x3

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
assume x: "x \<in> set gs"
[PROOF STATE]
proof (state)
this:
x \<in> set gs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set gs
[PROOF STEP]
obtain i where i: "i < ?m" and x: "x = gs ! i"
[PROOF STATE]
proof (prove)
using this:
x \<in> set gs

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length gs; x = gs ! i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_conv_nth
[PROOF STATE]
proof (prove)
using this:
x \<in> {gs ! i |i. i < length gs}

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length gs; x = gs ! i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length gs
x = gs ! i

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
hence "lc x * lc x * sq_norm x \<in> set ?sum"
[PROOF STATE]
proof (prove)
using this:
i < length gs
x = gs ! i

goal (1 subgoal):
 1. lc x * lc x * \<parallel>x\<parallel>\<^sup>2 \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lc x * lc x * \<parallel>x\<parallel>\<^sup>2 \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs])

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
with sum_list_nonneg_eq_0_iff[of ?sum, OF nonneg] sum_0
[PROOF STATE]
proof (chain)
picking this:
(\<And>x. x \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs]) \<Longrightarrow> x \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs])) \<Longrightarrow> ((\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) = (0::'a)) = (\<forall>x\<in>set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs]). x = (0::'a))
(\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) = (0::'a)
lc x * lc x * \<parallel>x\<parallel>\<^sup>2 \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs])
[PROOF STEP]
have "lc x = 0 \<or> sq_norm x = 0"
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs]) \<Longrightarrow> x \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs])) \<Longrightarrow> ((\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) = (0::'a)) = (\<forall>x\<in>set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs]). x = (0::'a))
(\<Sum>i\<leftarrow>[0..<length gs]. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) = (0::'a)
lc x * lc x * \<parallel>x\<parallel>\<^sup>2 \<in> set (map (\<lambda>i. lc (gs ! i) * lc (gs ! i) * \<parallel>gs ! i\<parallel>\<^sup>2) [0..<length gs])

goal (1 subgoal):
 1. lc x = (0::'a) \<or> \<parallel>x\<parallel>\<^sup>2 = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lc x = (0::'a) \<or> \<parallel>x\<parallel>\<^sup>2 = (0::'a)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
with orthogonalD[OF ortho, OF i i, folded x]
[PROOF STATE]
proof (chain)
picking this:
(x \<bullet> x = (0::'a)) = (i \<noteq> i)
lc x = (0::'a) \<or> \<parallel>x\<parallel>\<^sup>2 = (0::'a)
[PROOF STEP]
have "lc x = 0"
[PROOF STATE]
proof (prove)
using this:
(x \<bullet> x = (0::'a)) = (i \<noteq> i)
lc x = (0::'a) \<or> \<parallel>x\<parallel>\<^sup>2 = (0::'a)

goal (1 subgoal):
 1. lc x = (0::'a)
[PROOF STEP]
by (auto simp: sq_norm_vec_as_cscalar_prod)
[PROOF STATE]
proof (state)
this:
lc x = (0::'a)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x5 \<in> set gs \<Longrightarrow> lc ?x5 = (0::'a)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>True; lincomb a (set gs) = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>set gs. a v = (0::'a)
[PROOF STEP]
thus "\<forall>v\<in>set gs. lc v = 0"
[PROOF STATE]
proof (prove)
using this:
?x5 \<in> set gs \<Longrightarrow> lc ?x5 = (0::'a)

goal (1 subgoal):
 1. \<forall>v\<in>set gs. lc v = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>set gs. lc v = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lin_indpt_list gs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orthocompl_span:
  assumes "\<And> x. x \<in> S \<Longrightarrow> v \<bullet> x = 0" "S \<subseteq> carrier_vec n" and [intro]: "v \<in> carrier_vec n"
  and "y \<in> span S"
  shows "v \<bullet> y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
fix a A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
assume "y = lincomb a A" "finite A" "A \<subseteq> S"
[PROOF STATE]
proof (state)
this:
y = lincomb a A
finite A
A \<subseteq> S

goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
note assms = assms this
[PROOF STATE]
proof (state)
this:
?x3 \<in> S \<Longrightarrow> v \<bullet> ?x3 = (0::'a)
S \<subseteq> carrier_vec n
v \<in> carrier_vec n
y \<in> local.span S
y = lincomb a A
finite A
A \<subseteq> S

goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
hence [intro!]:"lincomb a A \<in> carrier_vec n" "(\<lambda>v. a v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> S \<Longrightarrow> v \<bullet> ?x3 = (0::'a)
S \<subseteq> carrier_vec n
v \<in> carrier_vec n
y \<in> local.span S
y = lincomb a A
finite A
A \<subseteq> S

goal (1 subgoal):
 1. lincomb a A \<in> carrier_vec n &&& (\<lambda>v. a v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb a A \<in> carrier_vec n
(\<lambda>v. a v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
have "\<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)
[PROOF STEP]
assume "x \<in> A"
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)
[PROOF STEP]
note assms = assms this
[PROOF STATE]
proof (state)
this:
?x3 \<in> S \<Longrightarrow> v \<bullet> ?x3 = (0::'a)
S \<subseteq> carrier_vec n
v \<in> carrier_vec n
y \<in> local.span S
y = lincomb a A
finite A
A \<subseteq> S
x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)
[PROOF STEP]
hence x:"x \<in> S"
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> S \<Longrightarrow> v \<bullet> ?x3 = (0::'a)
S \<subseteq> carrier_vec n
v \<in> carrier_vec n
y \<in> local.span S
y = lincomb a A
finite A
A \<subseteq> S
x \<in> A

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

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
?x3 \<in> S \<Longrightarrow> v \<bullet> ?x3 = (0::'a)
S \<subseteq> carrier_vec n
v \<in> carrier_vec n
y \<in> local.span S
y = lincomb a A
finite A
A \<subseteq> S
x \<in> A
x \<in> S
[PROOF STEP]
have [intro]:"x \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> S \<Longrightarrow> v \<bullet> ?x3 = (0::'a)
S \<subseteq> carrier_vec n
v \<in> carrier_vec n
y \<in> local.span S
y = lincomb a A
finite A
A \<subseteq> S
x \<in> A
x \<in> S

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

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)
[PROOF STEP]
from assms(1)[OF x]
[PROOF STATE]
proof (chain)
picking this:
v \<bullet> x = (0::'a)
[PROOF STEP]
have "x \<bullet> v = 0"
[PROOF STATE]
proof (prove)
using this:
v \<bullet> x = (0::'a)

goal (1 subgoal):
 1. x \<bullet> v = (0::'a)
[PROOF STEP]
by(subst comm_scalar_prod) force+
[PROOF STATE]
proof (state)
this:
x \<bullet> v = (0::'a)

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)
[PROOF STEP]
thus "(a x \<cdot>\<^sub>v x) \<bullet> v = 0"
[PROOF STATE]
proof (prove)
using this:
x \<bullet> v = (0::'a)

goal (1 subgoal):
 1. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)
[PROOF STEP]
apply(subst smult_scalar_prod_distrib)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. x \<bullet> v = (0::'a) \<Longrightarrow> x \<in> carrier_vec ?n1
 2. x \<bullet> v = (0::'a) \<Longrightarrow> v \<in> carrier_vec ?n1
 3. x \<bullet> v = (0::'a) \<Longrightarrow> a x * (x \<bullet> v) = (0::'a)
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
(a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)

goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
hence "v \<bullet> lincomb a A = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a)

goal (1 subgoal):
 1. v \<bullet> lincomb a A = (0::'a)
[PROOF STEP]
apply(subst comm_scalar_prod)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a) \<Longrightarrow> v \<in> carrier_vec ?n1
 2. \<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a) \<Longrightarrow> lincomb a A \<in> carrier_vec ?n1
 3. \<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a) \<Longrightarrow> lincomb a A \<bullet> v = (0::'a)
[PROOF STEP]
apply force+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a) \<Longrightarrow> lincomb a A \<bullet> v = (0::'a)
[PROOF STEP]
unfolding lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a) \<Longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) \<bullet> v = (0::'a)
[PROOF STEP]
apply(subst finsum_scalar_prod_sum)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a) \<Longrightarrow> (\<lambda>v. a v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n
 2. \<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a) \<Longrightarrow> v \<in> carrier_vec n
 3. \<forall>x\<in>A. (a x \<cdot>\<^sub>v x) \<bullet> v = (0::'a) \<Longrightarrow> (\<Sum>u\<in>A. (a u \<cdot>\<^sub>v u) \<bullet> v) = (0::'a)
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
v \<bullet> lincomb a A = (0::'a)

goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>y = lincomb ?a5 ?A5; finite ?A5; ?A5 \<subseteq> S\<rbrakk> \<Longrightarrow> v \<bullet> lincomb ?a5 ?A5 = (0::'a)

goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>y = lincomb ?a5 ?A5; finite ?A5; ?A5 \<subseteq> S\<rbrakk> \<Longrightarrow> v \<bullet> lincomb ?a5 ?A5 = (0::'a)

goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
using \<open>y \<in> span S\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>y = lincomb ?a5 ?A5; finite ?A5; ?A5 \<subseteq> S\<rbrakk> \<Longrightarrow> v \<bullet> lincomb ?a5 ?A5 = (0::'a)
y \<in> local.span S

goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
unfolding span_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>y = lincomb ?a5 ?A5; finite ?A5; ?A5 \<subseteq> S\<rbrakk> \<Longrightarrow> v \<bullet> lincomb ?a5 ?A5 = (0::'a)
y \<in> {lincomb a A |a A. finite A \<and> A \<subseteq> S}

goal (1 subgoal):
 1. v \<bullet> y = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<bullet> y = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orthogonal_sumlist:
  assumes ortho: "\<And> x. x \<in> set S \<Longrightarrow> v \<bullet> x = 0" and S: "set S \<subseteq> carrier_vec n" and v: "v \<in> carrier_vec n"
  shows "v \<bullet> sumlist S = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<bullet> M.sumlist S = (0::'a)
[PROOF STEP]
by (rule orthocompl_span[OF ortho S v sumlist_in_span[OF S span_mem[OF S]]])


[STATEMENT]
lemma oc_projection_alt_def:
  assumes carr:"(W::'a vec set) \<subseteq> carrier_vec n" "x \<in> carrier_vec n"
      and alt1:"y1 \<in> W" "x - y1 \<in> orthogonal_complement W"
      and alt2:"y2 \<in> W" "x - y2 \<in> orthogonal_complement W"
  shows  "y1 = y2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
have carr:"y1 \<in> carrier_vec n" "y2 \<in> carrier_vec n" "x \<in> carrier_vec n" "- y1 \<in> carrier_vec n"
    "0\<^sub>v n \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y1 \<in> carrier_vec n &&& y2 \<in> carrier_vec n) &&& x \<in> carrier_vec n &&& - y1 \<in> carrier_vec n &&& 0\<^sub>v n \<in> carrier_vec n
[PROOF STEP]
using alt1 alt2 carr
[PROOF STATE]
proof (prove)
using this:
y1 \<in> W
x - y1 \<in> orthogonal_complement W
y2 \<in> W
x - y2 \<in> orthogonal_complement W
W \<subseteq> carrier_vec n
x \<in> carrier_vec n

goal (1 subgoal):
 1. (y1 \<in> carrier_vec n &&& y2 \<in> carrier_vec n) &&& x \<in> carrier_vec n &&& - y1 \<in> carrier_vec n &&& 0\<^sub>v n \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
hence "y1 - y2 \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n

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

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
note carr = this carr
[PROOF STATE]
proof (state)
this:
y1 - y2 \<in> carrier_vec n
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
from alt1
[PROOF STATE]
proof (chain)
picking this:
y1 \<in> W
x - y1 \<in> orthogonal_complement W
[PROOF STEP]
have "ya\<in>W \<Longrightarrow> (x - y1) \<bullet> ya = 0" for ya
[PROOF STATE]
proof (prove)
using this:
y1 \<in> W
x - y1 \<in> orthogonal_complement W

goal (1 subgoal):
 1. ya \<in> W \<Longrightarrow> (x - y1) \<bullet> ya = (0::'a)
[PROOF STEP]
unfolding orthogonal_complement_def
[PROOF STATE]
proof (prove)
using this:
y1 \<in> W
x - y1 \<in> {x \<in> carrier_vec n. \<forall>y\<in>W. x \<bullet> y = (0::'a)}

goal (1 subgoal):
 1. ya \<in> W \<Longrightarrow> (x - y1) \<bullet> ya = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?ya4 \<in> W \<Longrightarrow> (x - y1) \<bullet> ?ya4 = (0::'a)

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
hence "(x - y1) \<bullet> y2 = 0" "(x - y1) \<bullet> y1 = 0"
[PROOF STATE]
proof (prove)
using this:
?ya4 \<in> W \<Longrightarrow> (x - y1) \<bullet> ?ya4 = (0::'a)

goal (1 subgoal):
 1. (x - y1) \<bullet> y2 = (0::'a) &&& (x - y1) \<bullet> y1 = (0::'a)
[PROOF STEP]
using alt2 alt1
[PROOF STATE]
proof (prove)
using this:
?ya4 \<in> W \<Longrightarrow> (x - y1) \<bullet> ?ya4 = (0::'a)
y2 \<in> W
x - y2 \<in> orthogonal_complement W
y1 \<in> W
x - y1 \<in> orthogonal_complement W

goal (1 subgoal):
 1. (x - y1) \<bullet> y2 = (0::'a) &&& (x - y1) \<bullet> y1 = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x - y1) \<bullet> y2 = (0::'a)
(x - y1) \<bullet> y1 = (0::'a)

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
hence eq1:"y1 \<bullet> y2 = x \<bullet> y2" "y1 \<bullet> y1 = x \<bullet> y1"
[PROOF STATE]
proof (prove)
using this:
(x - y1) \<bullet> y2 = (0::'a)
(x - y1) \<bullet> y1 = (0::'a)

goal (1 subgoal):
 1. y1 \<bullet> y2 = x \<bullet> y2 &&& y1 \<bullet> y1 = x \<bullet> y1
[PROOF STEP]
using carr minus_scalar_prod_distrib
[PROOF STATE]
proof (prove)
using this:
(x - y1) \<bullet> y2 = (0::'a)
(x - y1) \<bullet> y1 = (0::'a)
y1 - y2 \<in> carrier_vec n
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n
\<lbrakk>?v\<^sub>1 \<in> carrier_vec ?n; ?v\<^sub>2 \<in> carrier_vec ?n; ?v\<^sub>3 \<in> carrier_vec ?n\<rbrakk> \<Longrightarrow> (?v\<^sub>1 - ?v\<^sub>2) \<bullet> ?v\<^sub>3 = ?v\<^sub>1 \<bullet> ?v\<^sub>3 - ?v\<^sub>2 \<bullet> ?v\<^sub>3

goal (1 subgoal):
 1. y1 \<bullet> y2 = x \<bullet> y2 &&& y1 \<bullet> y1 = x \<bullet> y1
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
y1 \<bullet> y2 = x \<bullet> y2
y1 \<bullet> y1 = x \<bullet> y1

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
y1 \<bullet> y2 = x \<bullet> y2
[PROOF STEP]
have eq2:"y2 \<bullet> y1 = x \<bullet> y2"
[PROOF STATE]
proof (prove)
using this:
y1 \<bullet> y2 = x \<bullet> y2

goal (1 subgoal):
 1. y2 \<bullet> y1 = x \<bullet> y2
[PROOF STEP]
using carr comm_scalar_prod
[PROOF STATE]
proof (prove)
using this:
y1 \<bullet> y2 = x \<bullet> y2
y1 - y2 \<in> carrier_vec n
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n
\<lbrakk>?v\<^sub>1 \<in> carrier_vec ?n; ?v\<^sub>2 \<in> carrier_vec ?n\<rbrakk> \<Longrightarrow> ?v\<^sub>1 \<bullet> ?v\<^sub>2 = ?v\<^sub>2 \<bullet> ?v\<^sub>1

goal (1 subgoal):
 1. y2 \<bullet> y1 = x \<bullet> y2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
y2 \<bullet> y1 = x \<bullet> y2

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
from alt2
[PROOF STATE]
proof (chain)
picking this:
y2 \<in> W
x - y2 \<in> orthogonal_complement W
[PROOF STEP]
have "ya\<in>W \<Longrightarrow> (x - y2) \<bullet> ya = 0" for ya
[PROOF STATE]
proof (prove)
using this:
y2 \<in> W
x - y2 \<in> orthogonal_complement W

goal (1 subgoal):
 1. ya \<in> W \<Longrightarrow> (x - y2) \<bullet> ya = (0::'a)
[PROOF STEP]
unfolding orthogonal_complement_def
[PROOF STATE]
proof (prove)
using this:
y2 \<in> W
x - y2 \<in> {x \<in> carrier_vec n. \<forall>y\<in>W. x \<bullet> y = (0::'a)}

goal (1 subgoal):
 1. ya \<in> W \<Longrightarrow> (x - y2) \<bullet> ya = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?ya4 \<in> W \<Longrightarrow> (x - y2) \<bullet> ?ya4 = (0::'a)

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
hence "(x - y2) \<bullet> y1 = 0" "(x - y2) \<bullet> y2 = 0"
[PROOF STATE]
proof (prove)
using this:
?ya4 \<in> W \<Longrightarrow> (x - y2) \<bullet> ?ya4 = (0::'a)

goal (1 subgoal):
 1. (x - y2) \<bullet> y1 = (0::'a) &&& (x - y2) \<bullet> y2 = (0::'a)
[PROOF STEP]
using alt2 alt1
[PROOF STATE]
proof (prove)
using this:
?ya4 \<in> W \<Longrightarrow> (x - y2) \<bullet> ?ya4 = (0::'a)
y2 \<in> W
x - y2 \<in> orthogonal_complement W
y1 \<in> W
x - y1 \<in> orthogonal_complement W

goal (1 subgoal):
 1. (x - y2) \<bullet> y1 = (0::'a) &&& (x - y2) \<bullet> y2 = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x - y2) \<bullet> y1 = (0::'a)
(x - y2) \<bullet> y2 = (0::'a)

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
hence eq3:"y2 \<bullet> y2 = x \<bullet> y2" "y2 \<bullet> y1 = x \<bullet> y1"
[PROOF STATE]
proof (prove)
using this:
(x - y2) \<bullet> y1 = (0::'a)
(x - y2) \<bullet> y2 = (0::'a)

goal (1 subgoal):
 1. y2 \<bullet> y2 = x \<bullet> y2 &&& y2 \<bullet> y1 = x \<bullet> y1
[PROOF STEP]
using carr minus_scalar_prod_distrib
[PROOF STATE]
proof (prove)
using this:
(x - y2) \<bullet> y1 = (0::'a)
(x - y2) \<bullet> y2 = (0::'a)
y1 - y2 \<in> carrier_vec n
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n
\<lbrakk>?v\<^sub>1 \<in> carrier_vec ?n; ?v\<^sub>2 \<in> carrier_vec ?n; ?v\<^sub>3 \<in> carrier_vec ?n\<rbrakk> \<Longrightarrow> (?v\<^sub>1 - ?v\<^sub>2) \<bullet> ?v\<^sub>3 = ?v\<^sub>1 \<bullet> ?v\<^sub>3 - ?v\<^sub>2 \<bullet> ?v\<^sub>3

goal (1 subgoal):
 1. y2 \<bullet> y2 = x \<bullet> y2 &&& y2 \<bullet> y1 = x \<bullet> y1
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
y2 \<bullet> y2 = x \<bullet> y2
y2 \<bullet> y1 = x \<bullet> y1

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
with eq2
[PROOF STATE]
proof (chain)
picking this:
y2 \<bullet> y1 = x \<bullet> y2
y2 \<bullet> y2 = x \<bullet> y2
y2 \<bullet> y1 = x \<bullet> y1
[PROOF STEP]
have eq4:"x \<bullet> y1 = x \<bullet> y2"
[PROOF STATE]
proof (prove)
using this:
y2 \<bullet> y1 = x \<bullet> y2
y2 \<bullet> y2 = x \<bullet> y2
y2 \<bullet> y1 = x \<bullet> y1

goal (1 subgoal):
 1. x \<bullet> y1 = x \<bullet> y2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<bullet> y1 = x \<bullet> y2

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
have "\<parallel>(y1 - y2)\<parallel>\<^sup>2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>y1 - y2\<parallel>\<^sup>2 = (0::'a)
[PROOF STEP]
unfolding sq_norm_vec_as_cscalar_prod cscalar_prod_is_scalar_prod
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y1 - y2) \<bullet> (y1 - y2) = (0::'a)
[PROOF STEP]
using carr
[PROOF STATE]
proof (prove)
using this:
y1 - y2 \<in> carrier_vec n
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n

goal (1 subgoal):
 1. (y1 - y2) \<bullet> (y1 - y2) = (0::'a)
[PROOF STEP]
apply(subst minus_scalar_prod_distrib)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y1 \<in> carrier_vec ?n11
 2. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y2 \<in> carrier_vec ?n11
 3. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y1 - y2 \<in> carrier_vec ?n11
 4. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y1 \<bullet> (y1 - y2) - y2 \<bullet> (y1 - y2) = (0::'a)
[PROOF STEP]
apply force+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y1 \<bullet> (y1 - y2) - y2 \<bullet> (y1 - y2) = (0::'a)
[PROOF STEP]
apply(subst (0 0) scalar_prod_minus_distrib)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y1 \<in> carrier_vec ?n18
 2. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y2 \<in> carrier_vec ?n18
 3. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y2 \<in> carrier_vec ?n19
 4. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y1 \<in> carrier_vec ?n19
 5. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y1 \<bullet> y1 - y1 \<bullet> y2 - (y2 \<bullet> y1 - y2 \<bullet> y2) = (0::'a)
[PROOF STEP]
apply force+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> y1 \<bullet> y1 - y1 \<bullet> y2 - (y2 \<bullet> y1 - y2 \<bullet> y2) = (0::'a)
[PROOF STEP]
unfolding eq1 eq2 eq3 eq4
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y1 - y2 \<in> carrier_vec n; y1 \<in> carrier_vec n; y2 \<in> carrier_vec n; x \<in> carrier_vec n; - y1 \<in> carrier_vec n; 0\<^sub>v n \<in> carrier_vec n\<rbrakk> \<Longrightarrow> x \<bullet> y2 - x \<bullet> y2 - (x \<bullet> y2 - x \<bullet> y2) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>y1 - y2\<parallel>\<^sup>2 = (0::'a)

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
with sq_norm_vec_eq_0[of "(y1 - y2)"] carr
[PROOF STATE]
proof (chain)
picking this:
y1 - y2 \<in> carrier_vec ?n \<Longrightarrow> (\<parallel>y1 - y2\<parallel>\<^sup>2 = (0::'a)) = (y1 - y2 = 0\<^sub>v ?n)
y1 - y2 \<in> carrier_vec n
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n
\<parallel>y1 - y2\<parallel>\<^sup>2 = (0::'a)
[PROOF STEP]
have "y1 - y2 = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
y1 - y2 \<in> carrier_vec ?n \<Longrightarrow> (\<parallel>y1 - y2\<parallel>\<^sup>2 = (0::'a)) = (y1 - y2 = 0\<^sub>v ?n)
y1 - y2 \<in> carrier_vec n
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n
\<parallel>y1 - y2\<parallel>\<^sup>2 = (0::'a)

goal (1 subgoal):
 1. y1 - y2 = 0\<^sub>v n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y1 - y2 = 0\<^sub>v n

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
hence "y1 - y2 + y2 = y2"
[PROOF STATE]
proof (prove)
using this:
y1 - y2 = 0\<^sub>v n

goal (1 subgoal):
 1. y1 - y2 + y2 = y2
[PROOF STEP]
using carr
[PROOF STATE]
proof (prove)
using this:
y1 - y2 = 0\<^sub>v n
y1 - y2 \<in> carrier_vec n
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n

goal (1 subgoal):
 1. y1 - y2 + y2 = y2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y1 - y2 + y2 = y2

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y1 - y2 + y2 = y2

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
have "y1 - y2 + y2 = y1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y1 - y2 + y2 = y1
[PROOF STEP]
using carr
[PROOF STATE]
proof (prove)
using this:
y1 - y2 \<in> carrier_vec n
y1 \<in> carrier_vec n
y2 \<in> carrier_vec n
x \<in> carrier_vec n
- y1 \<in> carrier_vec n
0\<^sub>v n \<in> carrier_vec n

goal (1 subgoal):
 1. y1 - y2 + y2 = y1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y1 - y2 + y2 = y1

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y1 = y2
[PROOF STEP]
show "y1 = y2"
[PROOF STATE]
proof (prove)
using this:
y1 = y2

goal (1 subgoal):
 1. y1 = y2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
y1 = y2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_oc_projection_sq_norm: assumes "is_oc_projection w S v"
  and S: "S \<subseteq> carrier_vec n"
  and v: "v \<in> carrier_vec n"
shows "sq_norm w \<le> sq_norm v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
from assms[unfolded is_oc_projection_def]
[PROOF STATE]
proof (chain)
picking this:
w \<in> carrier_vec n \<and> v - w \<in> local.span S \<and> (\<forall>u. u \<in> S \<longrightarrow> w \<bullet> u = (0::'a))
S \<subseteq> carrier_vec n
v \<in> carrier_vec n
[PROOF STEP]
have w: "w \<in> carrier_vec n"
    and vw: "v - w \<in> span S" and ortho: "\<And> u. u \<in> S \<Longrightarrow> w \<bullet> u = 0"
[PROOF STATE]
proof (prove)
using this:
w \<in> carrier_vec n \<and> v - w \<in> local.span S \<and> (\<forall>u. u \<in> S \<longrightarrow> w \<bullet> u = (0::'a))
S \<subseteq> carrier_vec n
v \<in> carrier_vec n

goal (1 subgoal):
 1. w \<in> carrier_vec n &&& v - w \<in> local.span S &&& (\<And>u. u \<in> S \<Longrightarrow> w \<bullet> u = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> carrier_vec n
v - w \<in> local.span S
?u3 \<in> S \<Longrightarrow> w \<bullet> ?u3 = (0::'a)

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "sq_norm v = sq_norm ((v - w) + w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>v\<parallel>\<^sup>2 = \<parallel>v - w + w\<parallel>\<^sup>2
[PROOF STEP]
using v w
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
w \<in> carrier_vec n

goal (1 subgoal):
 1. \<parallel>v\<parallel>\<^sup>2 = \<parallel>v - w + w\<parallel>\<^sup>2
[PROOF STEP]
by (intro arg_cong[of _ _ sq_norm_vec], auto)
[PROOF STATE]
proof (state)
this:
\<parallel>v\<parallel>\<^sup>2 = \<parallel>v - w + w\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>v\<parallel>\<^sup>2 = \<parallel>v - w + w\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = ((v - w) + w) \<bullet> ((v - w) + w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>v - w + w\<parallel>\<^sup>2 = (v - w + w) \<bullet> (v - w + w)
[PROOF STEP]
unfolding sq_norm_vec_as_cscalar_prod
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v - w + w) \<bullet>c (v - w + w) = (v - w + w) \<bullet> (v - w + w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>v - w + w\<parallel>\<^sup>2 = (v - w + w) \<bullet> (v - w + w)

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>v - w + w\<parallel>\<^sup>2 = (v - w + w) \<bullet> (v - w + w)

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = (v - w) \<bullet> ((v - w) + w) + w \<bullet> ((v - w) + w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v - w + w) \<bullet> (v - w + w) = (v - w) \<bullet> (v - w + w) + w \<bullet> (v - w + w)
[PROOF STEP]
by (rule add_scalar_prod_distrib, insert v w, auto)
[PROOF STATE]
proof (state)
this:
(v - w + w) \<bullet> (v - w + w) = (v - w) \<bullet> (v - w + w) + w \<bullet> (v - w + w)

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(v - w + w) \<bullet> (v - w + w) = (v - w) \<bullet> (v - w + w) + w \<bullet> (v - w + w)

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = ((v - w) \<bullet> (v - w) + (v - w) \<bullet> w) + (w \<bullet> (v - w) + w \<bullet> w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v - w) \<bullet> (v - w + w) + w \<bullet> (v - w + w) = (v - w) \<bullet> (v - w) + (v - w) \<bullet> w + (w \<bullet> (v - w) + w \<bullet> w)
[PROOF STEP]
by (subst (1 2) scalar_prod_add_distrib, insert v w, auto)
[PROOF STATE]
proof (state)
this:
(v - w) \<bullet> (v - w + w) + w \<bullet> (v - w + w) = (v - w) \<bullet> (v - w) + (v - w) \<bullet> w + (w \<bullet> (v - w) + w \<bullet> w)

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(v - w) \<bullet> (v - w + w) + w \<bullet> (v - w + w) = (v - w) \<bullet> (v - w) + (v - w) \<bullet> w + (w \<bullet> (v - w) + w \<bullet> w)

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = sq_norm (v - w) + 2 * (w \<bullet> (v - w)) + sq_norm w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v - w) \<bullet> (v - w) + (v - w) \<bullet> w + (w \<bullet> (v - w) + w \<bullet> w) = \<parallel>v - w\<parallel>\<^sup>2 + (2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2
[PROOF STEP]
unfolding sq_norm_vec_as_cscalar_prod
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v - w) \<bullet> (v - w) + (v - w) \<bullet> w + (w \<bullet> (v - w) + w \<bullet> w) = (v - w) \<bullet>c (v - w) + (2::'a) * (w \<bullet> (v - w)) + w \<bullet>c w
[PROOF STEP]
using v w
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
w \<in> carrier_vec n

goal (1 subgoal):
 1. (v - w) \<bullet> (v - w) + (v - w) \<bullet> w + (w \<bullet> (v - w) + w \<bullet> w) = (v - w) \<bullet>c (v - w) + (2::'a) * (w \<bullet> (v - w)) + w \<bullet>c w
[PROOF STEP]
by (auto simp: comm_scalar_prod[of w _ "v - w"])
[PROOF STATE]
proof (state)
this:
(v - w) \<bullet> (v - w) + (v - w) \<bullet> w + (w \<bullet> (v - w) + w \<bullet> w) = \<parallel>v - w\<parallel>\<^sup>2 + (2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(v - w) \<bullet> (v - w) + (v - w) \<bullet> w + (w \<bullet> (v - w) + w \<bullet> w) = \<parallel>v - w\<parallel>\<^sup>2 + (2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> \<ge> 2 * (w \<bullet> (v - w)) + sq_norm w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v - w\<parallel>\<^sup>2 + (2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2
[PROOF STEP]
using sq_norm_vec_ge_0[of "v - w"]
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> \<parallel>v - w\<parallel>\<^sup>2

goal (1 subgoal):
 1. (2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v - w\<parallel>\<^sup>2 + (2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v - w\<parallel>\<^sup>2 + (2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v - w\<parallel>\<^sup>2 + (2::'a) * (w \<bullet> (v - w)) + \<parallel>w\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "w \<bullet> (v - w) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<bullet> (v - w) = (0::'a)
[PROOF STEP]
using orthocompl_span[OF ortho S w vw]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> S \<Longrightarrow> x \<in> S) \<Longrightarrow> w \<bullet> (v - w) = (0::'a)

goal (1 subgoal):
 1. w \<bullet> (v - w) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<bullet> (v - w) = (0::'a)

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(2::'a) * (0::'a) + \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(2::'a) * (0::'a) + \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>w\<parallel>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed