[STATEMENT]
lemma fi_is_sum_of_mu_gso: assumes i: "i < m"
  shows "fs ! i = sumlist (map (\<lambda> j. \<mu> i j \<cdot>\<^sub>v gso j) [0 ..< Suc i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])
[PROOF STEP]
let ?l = "sumlist (map (\<lambda> j. \<mu> i j \<cdot>\<^sub>v gso j) [0 ..< Suc i])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])
[PROOF STEP]
have "?l \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) \<in> carrier_vec n
[PROOF STEP]
by (rule sumlist_carrier, insert gso_carrier i, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) \<in> carrier_vec n

goal (1 subgoal):
 1. fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])
[PROOF STEP]
hence dim: "dim_vec ?l = n"
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) \<in> carrier_vec n

goal (1 subgoal):
 1. dim_vec (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])) = n
[PROOF STEP]
by (rule carrier_vecD)
[PROOF STATE]
proof (state)
this:
dim_vec (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])) = n

goal (1 subgoal):
 1. fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])
[PROOF STEP]
proof (rule eq_vecI, unfold dim f_dim[OF i])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
assume j: "j < n"
[PROOF STATE]
proof (state)
this:
j < n

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < length fs
[PROOF STEP]
have split: "[0 ..< m] = [0 ..< Suc i] @ [Suc i ..< m]"
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. [0..<length fs] = [0..<Suc i] @ [Suc i..<length fs]
[PROOF STEP]
by (metis Suc_lessI append.assoc append_same_eq less_imp_add_positive order_refl upt_add_eq_append zero_le)
[PROOF STATE]
proof (state)
this:
[0..<length fs] = [0..<Suc i] @ [Suc i..<length fs]

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
let ?prod = "\<lambda> k. \<mu> i k * gso k $ j"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
have "fs ! i $ j = FF $$ (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i $ j = mat_of_rows n fs $$ (i, j)
[PROOF STEP]
using i j
[PROOF STATE]
proof (prove)
using this:
i < length fs
j < n

goal (1 subgoal):
 1. fs ! i $ j = mat_of_rows n fs $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fs ! i $ j = mat_of_rows n fs $$ (i, j)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fs ! i $ j = mat_of_rows n fs $$ (i, j)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
have "\<dots> = ((M m) * Fs) $$ (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
[PROOF STEP]
using matrix_equality
[PROOF STATE]
proof (prove)
using this:
mat_of_rows n fs = M (length fs) * mat_of_rows n (map gso [0..<length fs])

goal (1 subgoal):
 1. mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
have "\<dots> = row (M m) i \<bullet> col Fs j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j
[PROOF STEP]
using i j
[PROOF STATE]
proof (prove)
using this:
i < length fs
j < n

goal (1 subgoal):
 1. (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
have "\<dots> = (\<Sum> k = 0..<m. row (M m) i $ k * col Fs j $ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j = (\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k)
[PROOF STEP]
unfolding scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<dim_vec (col (mat_of_rows n (map gso [0..<length fs])) j). row (M (length fs)) i $ ia * col (mat_of_rows n (map gso [0..<length fs])) j $ ia) = (\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j = (\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j = (\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
have "\<dots> = (\<Sum> k = 0..<m. ?prod k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k) = (\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j)
[PROOF STEP]
by (rule sum.cong[OF refl], insert i j dim, auto simp: mat_of_rows_list_def mat_of_rows_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k) = (\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k) = (\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
have "\<dots> = sum_list (map ?prod [0 ..< m])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j)
[PROOF STEP]
by (subst sum_list_distinct_conv_sum_set, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
have "\<dots> = sum_list (map ?prod [0 ..< Suc i]) + sum_list (map ?prod [Suc i ..< m])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<Suc i]. \<mu> i k * gso k $ j) + (\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j)
[PROOF STEP]
unfolding split
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<leftarrow>[0..<Suc i] @ [Suc i..<length fs]. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<Suc i]. \<mu> i k * gso k $ j) + (\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<Suc i]. \<mu> i k * gso k $ j) + (\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<Suc i]. \<mu> i k * gso k $ j) + (\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
have "sum_list (map ?prod [Suc i ..< m]) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j) = (0::'a)
[PROOF STEP]
by (rule sum_list_neutral, auto simp: \<mu>.simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j) = (0::'a)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j) = (0::'a)

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
have "sum_list (map ?prod [0 ..< Suc i]) = ?l $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<leftarrow>[0..<Suc i]. \<mu> i k * gso k $ j) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ j
[PROOF STEP]
by (subst sumlist_vec_index[OF _ j], (insert i, auto simp: intro!: gso_carrier)[1],
        rule arg_cong[of _ _ sum_list], insert i j, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<leftarrow>[0..<Suc i]. \<mu> i k * gso k $ j) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ j

goal (2 subgoals):
 1. \<And>ia. ia < n \<Longrightarrow> fs ! i $ ia = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ ia
 2. n = n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fs ! i $ j = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ j + (0::'a)
[PROOF STEP]
show "fs ! i $ j = ?l $ j"
[PROOF STATE]
proof (prove)
using this:
fs ! i $ j = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ j + (0::'a)

goal (1 subgoal):
 1. fs ! i $ j = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fs ! i $ j = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) $ j

goal (1 subgoal):
 1. n = n
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gi_is_fi_minus_sum_mu_gso:
  assumes i: "i < m"
  shows "gso i = fs ! i - sumlist (map (\<lambda> j. \<mu> i j \<cdot>\<^sub>v gso j) [0 ..< i])" (is "_ = _ - ?sum")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i = fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gso i = fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
[PROOF STEP]
have sum: "?sum \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n
[PROOF STEP]
by (rule sumlist_carrier, insert gso_carrier i, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n

goal (1 subgoal):
 1. gso i = fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i = fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
[PROOF STEP]
unfolding fs_by_gso_def[OF i]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
[PROOF STEP]
by (intro eq_vecI, insert gso_carrier[OF i] sum, auto)
[PROOF STATE]
proof (state)
this:
gso i = fs ! i - M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det: assumes m: "m = n" shows "det FF = det Fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_of_rows n fs) = det (mat_of_rows n (map gso [0..<length fs]))
[PROOF STEP]
unfolding matrix_equality
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (M (length fs) * mat_of_rows n (map gso [0..<length fs])) = det (mat_of_rows n (map gso [0..<length fs]))
[PROOF STEP]
apply (subst det_mult[OF M_dim(3)], (insert Fs_dim(3) m, auto)[1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (M (length fs)) * det (mat_of_rows n (map gso [0..<length fs])) = det (mat_of_rows n (map gso [0..<length fs]))
[PROOF STEP]
apply (subst det_lower_triangular[OF _ M_dim(3)])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < j; j < length fs\<rbrakk> \<Longrightarrow> M (length fs) $$ (i, j) = (0::'a)
 2. prod_list (diag_mat (M (length fs))) * det (mat_of_rows n (map gso [0..<length fs])) = det (mat_of_rows n (map gso [0..<length fs]))
[PROOF STEP]
by (subst M_index, (auto simp: \<mu>.simps)[3], unfold prod_list_diag_prod, auto simp: \<mu>.simps)


[STATEMENT]
lemma mn:
  shows "m \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length fs \<le> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length fs \<le> n
[PROOF STEP]
have n: "n = dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = local.dim
[PROOF STEP]
by (simp add: dim_is_n)
[PROOF STATE]
proof (state)
this:
n = local.dim

goal (1 subgoal):
 1. length fs \<le> n
[PROOF STEP]
have m: "m = card (set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length fs = card (set fs)
[PROOF STEP]
using distinct_card loc_assms
[PROOF STATE]
proof (prove)
using this:
distinct ?xs \<Longrightarrow> card (set ?xs) = length ?xs
lin_indpt (set fs)
distinct fs

goal (1 subgoal):
 1. length fs = card (set fs)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length fs = card (set fs)

goal (1 subgoal):
 1. length fs \<le> n
[PROOF STEP]
from m n
[PROOF STATE]
proof (chain)
picking this:
length fs = card (set fs)
n = local.dim
[PROOF STEP]
have mn: "m \<le> n \<longleftrightarrow> card (set fs) \<le> dim"
[PROOF STATE]
proof (prove)
using this:
length fs = card (set fs)
n = local.dim

goal (1 subgoal):
 1. (length fs \<le> n) = (card (set fs) \<le> local.dim)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(length fs \<le> n) = (card (set fs) \<le> local.dim)

goal (1 subgoal):
 1. length fs \<le> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length fs \<le> n
[PROOF STEP]
unfolding mn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set fs) \<le> local.dim
[PROOF STEP]
by (rule li_le_dim, use loc_assms fs_carrier in auto)
[PROOF STATE]
proof (state)
this:
length fs \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gso_inj[intro]:
  assumes "i < m"
  shows "inj_on gso {0..<i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on gso {0..<i}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on gso {0..<i}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on gso {0..<i}
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on gso {0..<i}
[PROOF STEP]
assume assms': "i < m" "x \<in> {0..<i}" "y \<in> {0..<i}" "gso x = gso y"
[PROOF STATE]
proof (state)
this:
i < length fs
x \<in> {0..<i}
y \<in> {0..<i}
gso x = gso y

goal (1 subgoal):
 1. inj_on gso {0..<i}
[PROOF STEP]
have "distinct (map gso [0..<m])" "x < length (map gso [0..<m])" "y < length (map gso [0..<m])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map gso [0..<length fs]) &&& x < length (map gso [0..<length fs]) &&& y < length (map gso [0..<length fs])
[PROOF STEP]
using dist_gso assms mn assms'
[PROOF STATE]
proof (prove)
using this:
distinct (map gso [0..<length fs])
i < length fs
length fs \<le> n
i < length fs
x \<in> {0..<i}
y \<in> {0..<i}
gso x = gso y

goal (1 subgoal):
 1. distinct (map gso [0..<length fs]) &&& x < length (map gso [0..<length fs]) &&& y < length (map gso [0..<length fs])
[PROOF STEP]
by (auto intro!: dist_gso)
[PROOF STATE]
proof (state)
this:
distinct (map gso [0..<length fs])
x < length (map gso [0..<length fs])
y < length (map gso [0..<length fs])

goal (1 subgoal):
 1. inj_on gso {0..<i}
[PROOF STEP]
from nth_eq_iff_index_eq[OF this] assms'
[PROOF STATE]
proof (chain)
picking this:
(map gso [0..<length fs] ! x = map gso [0..<length fs] ! y) = (x = y)
i < length fs
x \<in> {0..<i}
y \<in> {0..<i}
gso x = gso y
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
(map gso [0..<length fs] ! x = map gso [0..<length fs] ! y) = (x = y)
i < length fs
x \<in> {0..<i}
y \<in> {0..<i}
gso x = gso y

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

goal (1 subgoal):
 1. inj_on gso {0..<i}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < length fs; ?x3 \<in> {0..<i}; ?y3 \<in> {0..<i}; gso ?x3 = gso ?y3\<rbrakk> \<Longrightarrow> ?x3 = ?y3

goal (1 subgoal):
 1. inj_on gso {0..<i}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i < length fs; ?x3 \<in> {0..<i}; ?y3 \<in> {0..<i}; gso ?x3 = gso ?y3\<rbrakk> \<Longrightarrow> ?x3 = ?y3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < length fs; ?x3 \<in> {0..<i}; ?y3 \<in> {0..<i}; gso ?x3 = gso ?y3\<rbrakk> \<Longrightarrow> ?x3 = ?y3

goal (1 subgoal):
 1. inj_on gso {0..<i}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < length fs; ?x3 \<in> {0..<i}; ?y3 \<in> {0..<i}; gso ?x3 = gso ?y3\<rbrakk> \<Longrightarrow> ?x3 = ?y3
i < length fs

goal (1 subgoal):
 1. inj_on gso {0..<i}
[PROOF STEP]
by (intro inj_onI) auto
[PROOF STATE]
proof (state)
this:
inj_on gso {0..<i}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partial_span:
  assumes i: "i \<le> m"
  shows "span (gso ` {0 ..< i}) = span (set (take i fs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
let ?f = "\<lambda> i. fs ! i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
let ?us = "take i fs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
have len: "length ?us = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (take i fs) = i
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i \<le> length fs

goal (1 subgoal):
 1. length (take i fs) = i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (take i fs) = i

goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
from fs_carrier i
[PROOF STATE]
proof (chain)
picking this:
set fs \<subseteq> carrier_vec n
i \<le> length fs
[PROOF STEP]
have us: "set ?us \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n
i \<le> length fs

goal (1 subgoal):
 1. set (take i fs) \<subseteq> carrier_vec n
[PROOF STEP]
by (meson set_take_subset subset_trans)
[PROOF STATE]
proof (state)
this:
set (take i fs) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
obtain vi where main: "snd (main ?us) = vi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>vi. snd (main (take i fs)) = vi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
snd (main (take i fs)) = vi

goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
from dist
[PROOF STATE]
proof (chain)
picking this:
distinct fs
[PROOF STEP]
have dist: "distinct ?us"
[PROOF STATE]
proof (prove)
using this:
distinct fs

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

goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
from lin_indpt
[PROOF STATE]
proof (chain)
picking this:
lin_indpt (set fs)
[PROOF STEP]
have indpt: "lin_indpt (set ?us)"
[PROOF STATE]
proof (prove)
using this:
lin_indpt (set fs)

goal (1 subgoal):
 1. lin_indpt (set (take i fs))
[PROOF STEP]
using supset_ld_is_ld[of "set ?us", of "set (?us @ drop i fs)"]
[PROOF STATE]
proof (prove)
using this:
lin_indpt (set fs)
\<lbrakk>lin_dep (set (take i fs)); set (take i fs) \<subseteq> set (take i fs @ drop i fs)\<rbrakk> \<Longrightarrow> lin_dep (set (take i fs @ drop i fs))

goal (1 subgoal):
 1. lin_indpt (set (take i fs))
[PROOF STEP]
by (auto simp: set_take_subset)
[PROOF STATE]
proof (state)
this:
lin_indpt (set (take i fs))

goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
from partial_connect[OF _ i mn us main refl fs_carrier] assms
[PROOF STATE]
proof (chain)
picking this:
length fs = length fs \<Longrightarrow> gram_schmidt n (take i fs) = vi
length fs = length fs \<Longrightarrow> vi = map gso [0..<i]
i \<le> length fs
[PROOF STEP]
have gso: "vi = gram_schmidt n ?us" and vi: "vi = map gso [0 ..< i]"
[PROOF STATE]
proof (prove)
using this:
length fs = length fs \<Longrightarrow> gram_schmidt n (take i fs) = vi
length fs = length fs \<Longrightarrow> vi = map gso [0..<i]
i \<le> length fs

goal (1 subgoal):
 1. vi = gram_schmidt n (take i fs) &&& vi = map gso [0..<i]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vi = gram_schmidt n (take i fs)
vi = map gso [0..<i]

goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
from cof_vec_space.gram_schmidt_result(1)[OF us dist indpt gso, unfolded vi]
[PROOF STATE]
proof (chain)
picking this:
local.span (set (take i fs)) = local.span (set (map gso [0..<i]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.span (set (take i fs)) = local.span (set (map gso [0..<i]))

goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span (set (take i fs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.span (gso ` {0..<i}) = local.span (set (take i fs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partial_span':
  assumes i: "i \<le> m"
  shows "span (gso ` {0 ..< i}) = span ((\<lambda> j. fs ! j) ` {0 ..< i})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (gso ` {0..<i}) = local.span ((!) fs ` {0..<i})
[PROOF STEP]
unfolding partial_span[OF i]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (set (take i fs)) = local.span ((!) fs ` {0..<i})
[PROOF STEP]
by (rule arg_cong[of _ _ span], subst nth_image, insert i loc_assms, auto)


[STATEMENT]
lemma orthogonal:
  assumes "i < m" "j < m" "i \<noteq> j"
  shows "gso i \<bullet> gso j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i \<bullet> gso j = (0::'a)
[PROOF STEP]
using assms mn orthogonal_gso[unfolded orthogonal_def]
[PROOF STATE]
proof (prove)
using this:
i < length fs
j < length fs
i \<noteq> j
length fs \<le> n
\<forall>i j. i < length (map gso [0..<length fs]) \<longrightarrow> j < length (map gso [0..<length fs]) \<longrightarrow> (map gso [0..<length fs] ! i \<bullet> map gso [0..<length fs] ! j = (0::'a)) = (i \<noteq> j)

goal (1 subgoal):
 1. gso i \<bullet> gso j = (0::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma same_base:
  shows "span (set fs) = span (gso ` {0..<m})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (set fs) = local.span (gso ` {0..<length fs})
[PROOF STEP]
using span_gso loc_assms
[PROOF STATE]
proof (prove)
using this:
local.span (gso ` {0..<length fs}) = local.span (set fs)
lin_indpt (set fs)
distinct fs

goal (1 subgoal):
 1. local.span (set fs) = local.span (gso ` {0..<length fs})
[PROOF STEP]
by simp


[STATEMENT]
lemma sq_norm_gso_le_f:
  assumes i: "i < m"
  shows "sq_norm (gso i) \<le> sq_norm (fs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have id: "[0 ..< Suc i] = [0 ..< i] @ [i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<Suc i] = [0..<i] @ [i]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[0..<Suc i] = [0..<i] @ [i]

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
let ?sum = "sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have sum: "?sum \<in> carrier_vec n" and gsoi: "gso i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n &&& gso i \<in> carrier_vec n
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n &&& gso i \<in> carrier_vec n
[PROOF STEP]
by (auto intro!: sumlist_carrier gso_carrier)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n
gso i \<in> carrier_vec n

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
from fi_is_sum_of_mu_gso[OF i, unfolded id]
[PROOF STATE]
proof (chain)
picking this:
fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) ([0..<i] @ [i]))
[PROOF STEP]
have "sq_norm (fs ! i) = sq_norm (sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i] @ [gso i]))"
[PROOF STATE]
proof (prove)
using this:
fs ! i = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) ([0..<i] @ [i]))

goal (1 subgoal):
 1. \<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i] @ [gso i])\<parallel>\<^sup>2
[PROOF STEP]
by (simp add: \<mu>.simps)
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i] @ [gso i])\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i] @ [gso i])\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = sq_norm (?sum + gso i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i] @ [gso i])\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i\<parallel>\<^sup>2
[PROOF STEP]
by (subst sumlist_append, insert gso_carrier i, auto)
[PROOF STATE]
proof (state)
this:
\<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i] @ [gso i])\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i] @ [gso i])\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = (?sum + gso i) \<bullet> (?sum + gso i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i\<parallel>\<^sup>2 = (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i)
[PROOF STEP]
by (simp add: sq_norm_vec_as_cscalar_prod)
[PROOF STATE]
proof (state)
this:
\<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i\<parallel>\<^sup>2 = (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i)

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i\<parallel>\<^sup>2 = (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i)

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = ?sum \<bullet> (?sum + gso i) + gso i \<bullet> (?sum + gso i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) + gso i \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i)
[PROOF STEP]
by (rule add_scalar_prod_distrib[OF sum gsoi], insert sum gsoi, auto)
[PROOF STATE]
proof (state)
this:
(M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) + gso i \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i)

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) + gso i \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i)

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = (?sum \<bullet> ?sum + ?sum \<bullet> gso i) + (gso i \<bullet> ?sum + gso i \<bullet> gso i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) + gso i \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i + (gso i \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i \<bullet> gso i)
[PROOF STEP]
by (subst (1 2) scalar_prod_add_distrib[of _ n], insert sum gsoi, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) + gso i \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i + (gso i \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i \<bullet> gso i)

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) + gso i \<bullet> (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i + (gso i \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + gso i \<bullet> gso i)

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have "?sum \<bullet> ?sum = sq_norm ?sum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2
[PROOF STEP]
by (simp add: sq_norm_vec_as_cscalar_prod)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have "gso i \<bullet> gso i = sq_norm (gso i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i \<bullet> gso i = \<parallel>gso i\<parallel>\<^sup>2
[PROOF STEP]
by (simp add: sq_norm_vec_as_cscalar_prod)
[PROOF STATE]
proof (state)
this:
gso i \<bullet> gso i = \<parallel>gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gso i \<bullet> gso i = \<parallel>gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have "gso i \<bullet> ?sum = ?sum \<bullet> gso i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i
[PROOF STEP]
using gsoi sum
[PROOF STATE]
proof (prove)
using this:
gso i \<in> carrier_vec n
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n

goal (1 subgoal):
 1. gso i \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i
[PROOF STEP]
by (simp add: comm_scalar_prod)
[PROOF STATE]
proof (state)
this:
gso i \<bullet> M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) = M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2 + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i + (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i + \<parallel>gso i\<parallel>\<^sup>2)
[PROOF STEP]
have "sq_norm (fs ! i) = sq_norm ?sum + 2 * (?sum \<bullet> gso i) + sq_norm (gso i)"
[PROOF STATE]
proof (prove)
using this:
\<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2 + M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i + (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i + \<parallel>gso i\<parallel>\<^sup>2)

goal (1 subgoal):
 1. \<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2 + (2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2 + (2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! i\<parallel>\<^sup>2 = \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2 + (2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> \<ge> 2 * (?sum \<bullet> gso i) + sq_norm (gso i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2 + (2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2
[PROOF STEP]
using sq_norm_vec_ge_0[of ?sum]
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2

goal (1 subgoal):
 1. (2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2 + (2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2 + (2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<parallel>\<^sup>2 + (2::'a) * (M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i) + \<parallel>gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have "?sum \<bullet> gso i = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. v \<bullet> gso i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. v \<bullet> gso i)
[PROOF STEP]
by (subst scalar_prod_left_sum_distrib[OF _ gsoi], insert i gso_carrier, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. v \<bullet> gso i)

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<bullet> gso i = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. v \<bullet> gso i)

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. v \<bullet> gso i) = (0::'a)
[PROOF STEP]
proof (rule sum_list_neutral, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>v. v \<bullet> gso i) (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) \<Longrightarrow> x = (0::'a)
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
x \<in> set (map (\<lambda>v. v \<bullet> gso i) (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]))

goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>v. v \<bullet> gso i) (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) \<Longrightarrow> x = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (map (\<lambda>v. v \<bullet> gso i) (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]))
[PROOF STEP]
obtain j where j: "j < i" and x: "x = (\<mu> i j \<cdot>\<^sub>v gso j) \<bullet> gso i"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (map (\<lambda>v. v \<bullet> gso i) (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]))

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j < i; x = (\<mu> i j \<cdot>\<^sub>v gso j) \<bullet> gso i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < i
x = (\<mu> i j \<cdot>\<^sub>v gso j) \<bullet> gso i

goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>v. v \<bullet> gso i) (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) \<Longrightarrow> x = (0::'a)
[PROOF STEP]
from j i
[PROOF STATE]
proof (chain)
picking this:
j < i
i < length fs
[PROOF STEP]
have gsoj: "gso j \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
j < i
i < length fs

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

goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>v. v \<bullet> gso i) (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) \<Longrightarrow> x = (0::'a)
[PROOF STEP]
have "x = \<mu> i j * (gso j \<bullet> gso i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = \<mu> i j * (gso j \<bullet> gso i)
[PROOF STEP]
using gsoi gsoj
[PROOF STATE]
proof (prove)
using this:
gso i \<in> carrier_vec n
gso j \<in> carrier_vec n

goal (1 subgoal):
 1. x = \<mu> i j * (gso j \<bullet> gso i)
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
gso i \<in> carrier_vec n
gso j \<in> carrier_vec n

goal (1 subgoal):
 1. (\<mu> i j \<cdot>\<^sub>v gso j) \<bullet> gso i = \<mu> i j * (gso j \<bullet> gso i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = \<mu> i j * (gso j \<bullet> gso i)

goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>v. v \<bullet> gso i) (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) \<Longrightarrow> x = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = \<mu> i j * (gso j \<bullet> gso i)

goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>v. v \<bullet> gso i) (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) \<Longrightarrow> x = (0::'a)
[PROOF STEP]
have "gso j \<bullet> gso i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso j \<bullet> gso i = (0::'a)
[PROOF STEP]
by (rule orthogonal, insert j i assms, auto)
[PROOF STATE]
proof (state)
this:
gso j \<bullet> gso i = (0::'a)

goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>v. v \<bullet> gso i) (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) \<Longrightarrow> x = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x = \<mu> i j * (0::'a)
[PROOF STEP]
show "x = 0"
[PROOF STATE]
proof (prove)
using this:
x = \<mu> i j * (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. v \<bullet> gso i) = (0::'a)

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

goal (1 subgoal):
 1. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>fs ! i\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma oc_projection_exist:
  assumes i: "i < m"
  shows "fs ! i - gso i \<in> span (gso ` {0..<i})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i - gso i \<in> local.span (gso ` {0..<i})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. fs ! i - gso i = lincomb ?a ?A
 2. finite ?A
 3. ?A \<subseteq> gso ` {0..<i}
[PROOF STEP]
let ?A = "gso ` {0..<i}"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. fs ! i - gso i = lincomb ?a ?A
 2. finite ?A
 3. ?A \<subseteq> gso ` {0..<i}
[PROOF STEP]
show finA:"finite ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (gso ` {0..<i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (gso ` {0..<i})

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
have carA[intro!]:"?A \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso ` {0..<i} \<subseteq> carrier_vec n
[PROOF STEP]
using gso_dim assms
[PROOF STATE]
proof (prove)
using this:
?i < length fs \<Longrightarrow> dim_vec (gso ?i) = n
i < length fs

goal (1 subgoal):
 1. gso ` {0..<i} \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gso ` {0..<i} \<subseteq> carrier_vec n

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
let "?a v" = "\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else 0"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
have d:"(sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n
[PROOF STEP]
using gso.simps[of i] gso_dim[OF i]
[PROOF STATE]
proof (prove)
using this:
gso i = fs ! i + M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
dim_vec (gso i) = n

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n
[PROOF STEP]
unfolding carrier_vec_def
[PROOF STATE]
proof (prove)
using this:
gso i = fs ! i + M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
dim_vec (gso i) = n

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> {v. dim_vec v = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
note [intro] = f_carrier[OF i] gso_carrier[OF i] d
[PROOF STATE]
proof (state)
this:
fs ! i \<in> carrier_vec n
gso i \<in> carrier_vec n
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
have [intro!]:"(\<lambda>v. ?a v \<cdot>\<^sub>v v) \<in> gso ` {0..<i} \<rightarrow> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) \<in> gso ` {0..<i} \<rightarrow> carrier_vec n
[PROOF STEP]
using gso_carrier assms
[PROOF STATE]
proof (prove)
using this:
?i < length fs \<Longrightarrow> gso ?i \<in> carrier_vec n
i < length fs

goal (1 subgoal):
 1. (\<lambda>v. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) \<in> gso ` {0..<i} \<rightarrow> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>v. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) \<in> gso ` {0..<i} \<rightarrow> carrier_vec n

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<lambda>v. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) \<in> gso ` {0..<i} \<rightarrow> carrier_vec n

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
fix ia
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
assume ia[intro]:"ia < n"
[PROOF STATE]
proof (state)
this:
ia < n

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
have "(\<Sum>x\<in>gso ` {0..<i}. (?a x \<cdot>\<^sub>v x) $ ia) =
      - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia)
[PROOF STEP]
unfolding map_map comm_monoid_add_class.sum.reindex[OF gso_inj[OF assms]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((\<lambda>x. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) \<circ> gso) {0..<i} = - sum_list (map ((\<lambda>x. x $ ia) \<circ> (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j)) [0..<i])
[PROOF STEP]
unfolding atLeastLessThan_upt sum_set_upt_conv_sum_list_nat uminus_sum_list_map o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>[0..<i]. ((\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v gso x) $ ia) = (\<Sum>x\<leftarrow>[0..<i]. - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia)
[PROOF STEP]
proof(rule arg_cong[OF map_cong, OF refl],goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set [0..<i] \<Longrightarrow> ((\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v gso x) $ ia = - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
x \<in> set [0..<i]

goal (1 subgoal):
 1. \<And>x. x \<in> set [0..<i] \<Longrightarrow> ((\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v gso x) $ ia = - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia
[PROOF STEP]
hence x:"x < m" "x < i"
[PROOF STATE]
proof (prove)
using this:
x \<in> set [0..<i]

goal (1 subgoal):
 1. x < length fs &&& x < i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> set [0..<i]
i < length fs

goal (1 subgoal):
 1. x < length fs &&& x < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < length fs
x < i

goal (1 subgoal):
 1. \<And>x. x \<in> set [0..<i] \<Longrightarrow> ((\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v gso x) $ ia = - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia
[PROOF STEP]
hence d:"insert x (set [0..<i]) = {0..<i}"
              "count (mset [0..<i]) x = 1"
[PROOF STATE]
proof (prove)
using this:
x < length fs
x < i

goal (1 subgoal):
 1. insert x (set [0..<i]) = {0..<i} &&& count (mset [0..<i]) x = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert x (set [0..<i]) = {0..<i}
count (mset [0..<i]) x = 1

goal (1 subgoal):
 1. \<And>x. x \<in> set [0..<i] \<Longrightarrow> ((\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v gso x) $ ia = - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia
[PROOF STEP]
hence "inj_on gso (insert x (set [0..<i]))"
[PROOF STATE]
proof (prove)
using this:
insert x (set [0..<i]) = {0..<i}
count (mset [0..<i]) x = 1

goal (1 subgoal):
 1. inj_on gso (insert x (set [0..<i]))
[PROOF STEP]
using gso_inj[OF assms]
[PROOF STATE]
proof (prove)
using this:
insert x (set [0..<i]) = {0..<i}
count (mset [0..<i]) x = 1
inj_on gso {0..<i}

goal (1 subgoal):
 1. inj_on gso (insert x (set [0..<i]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on gso (insert x (set [0..<i]))

goal (1 subgoal):
 1. \<And>x. x \<in> set [0..<i] \<Longrightarrow> ((\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v gso x) $ ia = - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia
[PROOF STEP]
from inj_on_filter_key_eq[OF this,folded replicate_count_mset_eq_filter_eq]
[PROOF STATE]
proof (chain)
picking this:
filter (\<lambda>xa. gso x = gso xa) [0..<i] = replicate (count (mset [0..<i]) x) x
[PROOF STEP]
have "[n\<leftarrow>[0..<i] . gso x = gso n] = [x]"
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>xa. gso x = gso xa) [0..<i] = replicate (count (mset [0..<i]) x) x

goal (1 subgoal):
 1. filter (\<lambda>n. gso x = gso n) [0..<i] = [x]
[PROOF STEP]
using x assms d replicate.simps(2)[of 0]
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>xa. gso x = gso xa) [0..<i] = replicate (count (mset [0..<i]) x) x
x < length fs
x < i
i < length fs
insert x (set [0..<i]) = {0..<i}
count (mset [0..<i]) x = 1
replicate (Suc 0) ?x = ?x # replicate 0 ?x

goal (1 subgoal):
 1. filter (\<lambda>n. gso x = gso n) [0..<i] = [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
filter (\<lambda>n. gso x = gso n) [0..<i] = [x]

goal (1 subgoal):
 1. \<And>x. x \<in> set [0..<i] \<Longrightarrow> ((\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v gso x) $ ia = - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia
[PROOF STEP]
hence "(\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else 0) = \<mu> i x"
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>n. gso x = gso n) [0..<i] = [x]

goal (1 subgoal):
 1. (\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) = \<mu> i x
[PROOF STEP]
unfolding sum_list_map_filter'[symmetric]
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>n. gso x = gso n) [0..<i] = [x]

goal (1 subgoal):
 1. sum_list (map (\<mu> i) (filter (\<lambda>n. gso x = gso n) [0..<i])) = \<mu> i x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) = \<mu> i x

goal (1 subgoal):
 1. \<And>x. x \<in> set [0..<i] \<Longrightarrow> ((\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v gso x) $ ia = - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia
[PROOF STEP]
with ia gso_dim x
[PROOF STATE]
proof (chain)
picking this:
ia < n
?i < length fs \<Longrightarrow> dim_vec (gso ?i) = n
x < length fs
x < i
(\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) = \<mu> i x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ia < n
?i < length fs \<Longrightarrow> dim_vec (gso ?i) = n
x < length fs
x < i
(\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) = \<mu> i x

goal (1 subgoal):
 1. ((\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v gso x) $ ia = - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia
[PROOF STEP]
apply(subst index_smult_vec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ia < n; \<And>i. i < length fs \<Longrightarrow> dim_vec (gso i) = n; x < length fs; x < i; (\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) = \<mu> i x\<rbrakk> \<Longrightarrow> ia < dim_vec (gso x)
 2. \<lbrakk>ia < n; \<And>i. i < length fs \<Longrightarrow> dim_vec (gso i) = n; x < length fs; x < i; (\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) = \<mu> i x\<rbrakk> \<Longrightarrow> (\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) * gso x $ ia = - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
((\<Sum>n\<leftarrow>[0..<i]. if gso x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v gso x) $ ia = - (- \<mu> i x \<cdot>\<^sub>v gso x) $ ia

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia)

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
hence "(\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. ?a v \<cdot>\<^sub>v v) $ ia =
          (- local.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) $ ia"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia)

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) $ ia = (- M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) $ ia
[PROOF STEP]
using d assms
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia)
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n
i < length fs

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) $ ia = (- M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) $ ia
[PROOF STEP]
apply (subst (0 0) finsum_index index_uminus_vec)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia); M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n; i < length fs\<rbrakk> \<Longrightarrow> ia < n
 2. \<lbrakk>(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia); M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n; i < length fs\<rbrakk> \<Longrightarrow> (\<lambda>v. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) \<in> gso ` {0..<i} \<rightarrow> carrier_vec n
 3. \<lbrakk>(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia); M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n; i < length fs\<rbrakk> \<Longrightarrow> gso ` {0..<i} \<subseteq> carrier_vec n
 4. \<lbrakk>(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia); M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n; i < length fs\<rbrakk> \<Longrightarrow> ia < dim_vec (M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]))
 5. \<lbrakk>(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia); M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n; i < length fs\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) $ ia
[PROOF STEP]
apply force+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia); M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n; i < length fs\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) $ ia
[PROOF STEP]
apply (subst sumlist_vec_index)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia); M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n; i < length fs; x \<in> set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])\<rbrakk> \<Longrightarrow> x \<in> carrier_vec n
 2. \<lbrakk>(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia); M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n; i < length fs\<rbrakk> \<Longrightarrow> ia < n
 3. \<lbrakk>(\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia); M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n; i < length fs\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>gso ` {0..<i}. ((\<Sum>n\<leftarrow>[0..<i]. if x = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v x) $ ia) = - (\<Sum>x\<leftarrow>map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]. x $ ia)
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) $ ia = (- M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) $ ia

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?ia3 < n \<Longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) $ ?ia3 = (- M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) $ ?ia3

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
hence id: "(\<Oplus>\<^bsub>V\<^esub>v\<in>?A. ?a v \<cdot>\<^sub>v v) = - sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])"
[PROOF STATE]
proof (prove)
using this:
?ia3 < n \<Longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) $ ?ia3 = (- M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) $ ?ia3

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) = - M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
[PROOF STEP]
using d lincomb_dim[OF finA carA,unfolded lincomb_def]
[PROOF STATE]
proof (prove)
using this:
?ia3 < n \<Longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) $ ?ia3 = (- M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) $ ?ia3
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) \<in> carrier_vec n
dim_vec (\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. ?a v \<cdot>\<^sub>v v) = n

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) = - M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
[PROOF STEP]
by(intro eq_vecI,auto)
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>gso ` {0..<i}. (\<Sum>n\<leftarrow>[0..<i]. if v = gso n then \<mu> i n else (0::'a)) \<cdot>\<^sub>v v) = - M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])

goal (2 subgoals):
 1. fs ! i - gso i = lincomb ?a (gso ` {0..<i})
 2. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
show "fs ! i - gso i = lincomb ?a ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i - gso i = lincomb (\<lambda>a. \<Sum>n\<leftarrow>[0..<i]. if a = gso n then \<mu> i n else (0::'a)) (gso ` {0..<i})
[PROOF STEP]
unfolding lincomb_def gso.simps[of i] id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i - (fs ! i + M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])) = - M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
[PROOF STEP]
by (rule eq_vecI, auto)
[PROOF STATE]
proof (state)
this:
fs ! i - gso i = lincomb (\<lambda>a. \<Sum>n\<leftarrow>[0..<i]. if a = gso n then \<mu> i n else (0::'a)) (gso ` {0..<i})

goal (1 subgoal):
 1. gso ` {0..<i} \<subseteq> gso ` {0..<i}
[PROOF STEP]
qed auto


[STATEMENT]
lemma oc_projection_unique:
  assumes "i < m"
          "v \<in> carrier_vec n"
          "\<And> x. x \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> x = 0"
          "fs ! i - v \<in> span (gso ` {0..<i})"
  shows "v = gso i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
have carr_span:"span (gso ` {0..<i}) \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})

goal (1 subgoal):
 1. local.span (gso ` {0..<i}) \<subseteq> carrier_vec n
[PROOF STEP]
by(intro span_is_subset2) auto
[PROOF STATE]
proof (state)
this:
local.span (gso ` {0..<i}) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
have carr: "gso ` {0..<i} \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})

goal (1 subgoal):
 1. gso ` {0..<i} \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gso ` {0..<i} \<subseteq> carrier_vec n

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
have eq:"fs ! i - (fs ! i - v) = v" for v
[PROOF STATE]
proof (prove)
using this:
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})

goal (1 subgoal):
 1. fs ! i - (fs ! i - v) = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fs ! i - (fs ! i - ?v1) = ?v1

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
from orthocompl_span[OF _ carr] assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x. x \<in> gso ` {0..<i} \<Longrightarrow> ?v \<bullet> x = (0::'a); ?v \<in> carrier_vec n; ?y \<in> local.span (gso ` {0..<i})\<rbrakk> \<Longrightarrow> ?v \<bullet> ?y = (0::'a)
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
have "y \<in> span (gso ` {0..<i}) \<Longrightarrow> v \<bullet> y = 0" for y
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> gso ` {0..<i} \<Longrightarrow> ?v \<bullet> x = (0::'a); ?v \<in> carrier_vec n; ?y \<in> local.span (gso ` {0..<i})\<rbrakk> \<Longrightarrow> ?v \<bullet> ?y = (0::'a)
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})

goal (1 subgoal):
 1. y \<in> local.span (gso ` {0..<i}) \<Longrightarrow> v \<bullet> y = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?y1 \<in> local.span (gso ` {0..<i}) \<Longrightarrow> v \<bullet> ?y1 = (0::'a)

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
hence oc1:"fs ! i - (fs ! i - v) \<in> orthogonal_complement (span (gso ` {0..< i}))"
[PROOF STATE]
proof (prove)
using this:
?y1 \<in> local.span (gso ` {0..<i}) \<Longrightarrow> v \<bullet> ?y1 = (0::'a)

goal (1 subgoal):
 1. fs ! i - (fs ! i - v) \<in> orthogonal_complement (local.span (gso ` {0..<i}))
[PROOF STEP]
unfolding eq orthogonal_complement_def
[PROOF STATE]
proof (prove)
using this:
?y1 \<in> local.span (gso ` {0..<i}) \<Longrightarrow> v \<bullet> ?y1 = (0::'a)

goal (1 subgoal):
 1. v \<in> {x \<in> carrier_vec n. \<forall>y\<in>local.span (gso ` {0..<i}). x \<bullet> y = (0::'a)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?y1 \<in> local.span (gso ` {0..<i}) \<Longrightarrow> v \<bullet> ?y1 = (0::'a)
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})

goal (1 subgoal):
 1. v \<in> {x \<in> carrier_vec n. \<forall>y\<in>local.span (gso ` {0..<i}). x \<bullet> y = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fs ! i - (fs ! i - v) \<in> orthogonal_complement (local.span (gso ` {0..<i}))

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
have "x \<in> gso ` {0..<i} \<Longrightarrow> gso i \<bullet> x = 0" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> gso ` {0..<i} \<Longrightarrow> gso i \<bullet> x = (0::'a)
[PROOF STEP]
using assms orthogonal
[PROOF STATE]
proof (prove)
using this:
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})
\<lbrakk>?i < length fs; ?j < length fs; ?i \<noteq> ?j\<rbrakk> \<Longrightarrow> gso ?i \<bullet> gso ?j = (0::'a)

goal (1 subgoal):
 1. x \<in> gso ` {0..<i} \<Longrightarrow> gso i \<bullet> x = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> gso ` {0..<i} \<Longrightarrow> gso i \<bullet> ?x1 = (0::'a)

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
hence "y \<in> span (gso ` {0..<i}) \<Longrightarrow> gso i \<bullet> y = 0" for y
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> gso ` {0..<i} \<Longrightarrow> gso i \<bullet> ?x1 = (0::'a)

goal (1 subgoal):
 1. y \<in> local.span (gso ` {0..<i}) \<Longrightarrow> gso i \<bullet> y = (0::'a)
[PROOF STEP]
by (rule orthocompl_span) (use carr gso_carrier assms in auto)
[PROOF STATE]
proof (state)
this:
?y1 \<in> local.span (gso ` {0..<i}) \<Longrightarrow> gso i \<bullet> ?y1 = (0::'a)

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
hence oc2:"fs ! i - (fs ! i - gso i) \<in> orthogonal_complement (span (gso ` {0..< i}))"
[PROOF STATE]
proof (prove)
using this:
?y1 \<in> local.span (gso ` {0..<i}) \<Longrightarrow> gso i \<bullet> ?y1 = (0::'a)

goal (1 subgoal):
 1. fs ! i - (fs ! i - gso i) \<in> orthogonal_complement (local.span (gso ` {0..<i}))
[PROOF STEP]
unfolding eq orthogonal_complement_def
[PROOF STATE]
proof (prove)
using this:
?y1 \<in> local.span (gso ` {0..<i}) \<Longrightarrow> gso i \<bullet> ?y1 = (0::'a)

goal (1 subgoal):
 1. gso i \<in> {x \<in> carrier_vec n. \<forall>y\<in>local.span (gso ` {0..<i}). x \<bullet> y = (0::'a)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?y1 \<in> local.span (gso ` {0..<i}) \<Longrightarrow> gso i \<bullet> ?y1 = (0::'a)
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})

goal (1 subgoal):
 1. gso i \<in> {x \<in> carrier_vec n. \<forall>y\<in>local.span (gso ` {0..<i}). x \<bullet> y = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fs ! i - (fs ! i - gso i) \<in> orthogonal_complement (local.span (gso ` {0..<i}))

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
note pe= oc_projection_exist[OF assms(1)]
[PROOF STATE]
proof (state)
this:
fs ! i - gso i \<in> local.span (gso ` {0..<i})

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
note prerec = carr_span f_carrier[OF assms(1)] assms(4) oc1 oc_projection_exist[OF assms(1)] oc2
[PROOF STATE]
proof (state)
this:
local.span (gso ` {0..<i}) \<subseteq> carrier_vec n
fs ! i \<in> carrier_vec n
fs ! i - v \<in> local.span (gso ` {0..<i})
fs ! i - (fs ! i - v) \<in> orthogonal_complement (local.span (gso ` {0..<i}))
fs ! i - gso i \<in> local.span (gso ` {0..<i})
fs ! i - (fs ! i - gso i) \<in> orthogonal_complement (local.span (gso ` {0..<i}))

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
note prerec = carr_span f_carrier[OF assms(1)] assms(4) oc1 oc_projection_exist[OF assms(1)] oc2
[PROOF STATE]
proof (state)
this:
local.span (gso ` {0..<i}) \<subseteq> carrier_vec n
fs ! i \<in> carrier_vec n
fs ! i - v \<in> local.span (gso ` {0..<i})
fs ! i - (fs ! i - v) \<in> orthogonal_complement (local.span (gso ` {0..<i}))
fs ! i - gso i \<in> local.span (gso ` {0..<i})
fs ! i - (fs ! i - gso i) \<in> orthogonal_complement (local.span (gso ` {0..<i}))

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
have gsoi: "gso i \<in> carrier_vec n" "fs ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i \<in> carrier_vec n &&& fs ! i \<in> carrier_vec n
[PROOF STEP]
by (rule gso_carrier[OF \<open>i < m\<close>], rule f_carrier[OF \<open>i < m\<close>])
[PROOF STATE]
proof (state)
this:
gso i \<in> carrier_vec n
fs ! i \<in> carrier_vec n

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
note main = arg_cong[OF oc_projection_alt_def[OF carr_span f_carrier[OF assms(1)] assms(4) oc1 pe oc2],
     of "\<lambda> v. - v $ j + fs ! i $ j" for j]
[PROOF STATE]
proof (state)
this:
- (fs ! i - v) $ ?j3 + fs ! i $ ?j3 = - (fs ! i - gso i) $ ?j3 + fs ! i $ ?j3

goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
show "v = gso i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = gso i
[PROOF STEP]
proof (intro eq_vecI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. ia < dim_vec (gso i) \<Longrightarrow> v $ ia = gso i $ ia
 2. dim_vec v = dim_vec (gso i)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. ia < dim_vec (gso i) \<Longrightarrow> v $ ia = gso i $ ia
 2. dim_vec v = dim_vec (gso i)
[PROOF STEP]
show "j < dim_vec (gso i) \<Longrightarrow> v $ j = gso i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < dim_vec (gso i) \<Longrightarrow> v $ j = gso i $ j
[PROOF STEP]
using assms gsoi main[of j]
[PROOF STATE]
proof (prove)
using this:
i < length fs
v \<in> carrier_vec n
?x1 \<in> gso ` {0..<i} \<Longrightarrow> v \<bullet> ?x1 = (0::'a)
fs ! i - v \<in> local.span (gso ` {0..<i})
gso i \<in> carrier_vec n
fs ! i \<in> carrier_vec n
- (fs ! i - v) $ j + fs ! i $ j = - (fs ! i - gso i) $ j + fs ! i $ j

goal (1 subgoal):
 1. j < dim_vec (gso i) \<Longrightarrow> v $ j = gso i $ j
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
j < dim_vec (gso i) \<Longrightarrow> v $ j = gso i $ j

goal (1 subgoal):
 1. dim_vec v = dim_vec (gso i)
[PROOF STEP]
qed (insert assms gsoi, auto)
[PROOF STATE]
proof (state)
this:
v = gso i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gso_oc_projection:
  assumes "i < m"
  shows "gso i = oc_projection (gso ` {0..<i}) (fs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i = oc_projection (gso ` {0..<i}) (fs ! i)
[PROOF STEP]
unfolding oc_projection_def is_oc_projection_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i = (SOME v. v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> v \<bullet> u = (0::'a)))
[PROOF STEP]
proof (rule some_equality[symmetric,OF _ oc_projection_unique[OF assms]])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> gso i \<bullet> u = (0::'a))
 2. \<And>v. v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> v \<in> carrier_vec n
 3. \<And>v xa. \<lbrakk>v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> v \<bullet> u = (0::'a)); xa \<in> gso ` {0..<i}\<rbrakk> \<Longrightarrow> v \<bullet> xa = (0::'a)
 4. \<And>v. v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
have orthogonal:"\<And> xa. xa < i \<Longrightarrow> gso i \<bullet> gso xa = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa < i \<Longrightarrow> gso i \<bullet> gso xa = (0::'a)
[PROOF STEP]
by (rule orthogonal,insert assms, auto)
[PROOF STATE]
proof (state)
this:
?xa1 < i \<Longrightarrow> gso i \<bullet> gso ?xa1 = (0::'a)

goal (4 subgoals):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> gso i \<bullet> u = (0::'a))
 2. \<And>v. v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> v \<in> carrier_vec n
 3. \<And>v xa. \<lbrakk>v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> v \<bullet> u = (0::'a)); xa \<in> gso ` {0..<i}\<rbrakk> \<Longrightarrow> v \<bullet> xa = (0::'a)
 4. \<And>v. v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
show "gso i \<in> carrier_vec n \<and>
        fs ! i - gso i \<in> span (gso ` {0..<i}) \<and>
        (\<forall>x. x \<in> gso ` {0..<i} \<longrightarrow> gso i \<bullet> x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (gso ` {0..<i}) \<and> (\<forall>x. x \<in> gso ` {0..<i} \<longrightarrow> gso i \<bullet> x = (0::'a))
[PROOF STEP]
using gso_carrier oc_projection_exist assms orthogonal
[PROOF STATE]
proof (prove)
using this:
?i < length fs \<Longrightarrow> gso ?i \<in> carrier_vec n
?i < length fs \<Longrightarrow> fs ! ?i - gso ?i \<in> local.span (gso ` {0..<?i})
i < length fs
?xa1 < i \<Longrightarrow> gso i \<bullet> gso ?xa1 = (0::'a)

goal (1 subgoal):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (gso ` {0..<i}) \<and> (\<forall>x. x \<in> gso ` {0..<i} \<longrightarrow> gso i \<bullet> x = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (gso ` {0..<i}) \<and> (\<forall>x. x \<in> gso ` {0..<i} \<longrightarrow> gso i \<bullet> x = (0::'a))

goal (3 subgoals):
 1. \<And>v. v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> v \<in> carrier_vec n
 2. \<And>v xa. \<lbrakk>v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> v \<bullet> u = (0::'a)); xa \<in> gso ` {0..<i}\<rbrakk> \<Longrightarrow> v \<bullet> xa = (0::'a)
 3. \<And>v. v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>u. u \<in> gso ` {0..<i} \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
qed auto