[STATEMENT]
lemma gso_oc_projection_span:
  assumes "i < m"
  shows "gso i = oc_projection (span (gso ` {0..<i})) (fs ! i)"
    and "is_oc_projection (gso i) (span (gso ` {0..<i})) (fs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i = oc_projection (local.span (gso ` {0..<i})) (fs ! i) &&& is_oc_projection (gso i) (local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a))) &&& gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> u = (0::'a))
[PROOF STEP]
proof (rule some_equality[symmetric,OF _ oc_projection_unique[OF assms]])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
 5. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> u = (0::'a))
[PROOF STEP]
let ?P = "\<lambda>v. v \<in> carrier_vec n \<and> fs ! i - v \<in> span (span (gso ` {0..<i}))
    \<and> (\<forall>x. x \<in> span (gso ` {0..<i}) \<longrightarrow> v \<bullet> x = 0)"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
 5. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> u = (0::'a))
[PROOF STEP]
have carr:"gso ` {0..<i} \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso ` {0..<i} \<subseteq> carrier_vec n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
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 (5 subgoals):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
 5. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> u = (0::'a))
[PROOF STEP]
have *:  "\<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 (5 subgoals):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
 5. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> u = (0::'a))
[PROOF STEP]
have orthogonal:"\<And>x. x \<in> span (gso ` {0..<i}) \<Longrightarrow> gso i \<bullet> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> local.span (gso ` {0..<i}) \<Longrightarrow> gso i \<bullet> x = (0::'a)
[PROOF STEP]
apply(rule orthocompl_span)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> local.span (gso ` {0..<i}); xa \<in> ?S x\<rbrakk> \<Longrightarrow> gso i \<bullet> xa = (0::'a)
 2. \<And>x. x \<in> local.span (gso ` {0..<i}) \<Longrightarrow> ?S x \<subseteq> carrier_vec n
 3. \<And>x. x \<in> local.span (gso ` {0..<i}) \<Longrightarrow> gso i \<in> carrier_vec n
 4. \<And>x. x \<in> local.span (gso ` {0..<i}) \<Longrightarrow> x \<in> local.span (?S x)
[PROOF STEP]
using assms *
[PROOF STATE]
proof (prove)
using this:
i < length fs
?xa1 < i \<Longrightarrow> gso i \<bullet> gso ?xa1 = (0::'a)

goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> local.span (gso ` {0..<i}); xa \<in> ?S x\<rbrakk> \<Longrightarrow> gso i \<bullet> xa = (0::'a)
 2. \<And>x. x \<in> local.span (gso ` {0..<i}) \<Longrightarrow> ?S x \<subseteq> carrier_vec n
 3. \<And>x. x \<in> local.span (gso ` {0..<i}) \<Longrightarrow> gso i \<in> carrier_vec n
 4. \<And>x. x \<in> local.span (gso ` {0..<i}) \<Longrightarrow> x \<in> local.span (?S x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> local.span (gso ` {0..<i}) \<Longrightarrow> gso i \<bullet> ?x1 = (0::'a)

goal (5 subgoals):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
 5. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> u = (0::'a))
[PROOF STEP]
show "?P (gso i)" "?P (gso i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>x. x \<in> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> x = (0::'a)) &&& gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>x. x \<in> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> x = (0::'a))
[PROOF STEP]
unfolding span_span[OF carr]
[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> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> x = (0::'a)) &&& gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (gso ` {0..<i}) \<and> (\<forall>x. x \<in> local.span (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
?x1 \<in> local.span (gso ` {0..<i}) \<Longrightarrow> gso i \<bullet> ?x1 = (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> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> x = (0::'a)) &&& gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (gso ` {0..<i}) \<and> (\<forall>x. x \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>x. x \<in> local.span (gso ` {0..<i}) \<longrightarrow> gso i \<bullet> x = (0::'a))
gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>x. x \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>v. v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
assume p:"?P v"
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>x. x \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> x = (0::'a))

goal (3 subgoals):
 1. \<And>v. v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (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 (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>x. x \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> x = (0::'a))
[PROOF STEP]
show "v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>x. x \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> x = (0::'a))

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

goal (2 subgoals):
 1. \<And>v xa. \<lbrakk>v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)); xa \<in> gso ` {0..<i}\<rbrakk> \<Longrightarrow> v \<bullet> xa = (0::'a)
 2. \<And>v. v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)) \<Longrightarrow> fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>x. x \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> x = (0::'a))
[PROOF STEP]
show "fs ! i - v \<in> span (gso ` {0..<i})"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>x. x \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> x = (0::'a))

goal (1 subgoal):
 1. fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
unfolding span_span[OF carr]
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (gso ` {0..<i}) \<and> (\<forall>x. x \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> x = (0::'a))

goal (1 subgoal):
 1. fs ! i - v \<in> local.span (gso ` {0..<i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fs ! i - v \<in> local.span (gso ` {0..<i})

goal (1 subgoal):
 1. \<And>v xa. \<lbrakk>v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)); xa \<in> gso ` {0..<i}\<rbrakk> \<Longrightarrow> v \<bullet> xa = (0::'a)
[PROOF STEP]
fix xa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v xa. \<lbrakk>v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)); xa \<in> gso ` {0..<i}\<rbrakk> \<Longrightarrow> v \<bullet> xa = (0::'a)
[PROOF STEP]
assume "xa \<in> gso ` {0..<i}"
[PROOF STATE]
proof (state)
this:
xa \<in> gso ` {0..<i}

goal (1 subgoal):
 1. \<And>v xa. \<lbrakk>v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)); xa \<in> gso ` {0..<i}\<rbrakk> \<Longrightarrow> v \<bullet> xa = (0::'a)
[PROOF STEP]
hence "xa \<in> span (gso ` {0..<i})"
[PROOF STATE]
proof (prove)
using this:
xa \<in> gso ` {0..<i}

goal (1 subgoal):
 1. xa \<in> local.span (gso ` {0..<i})
[PROOF STEP]
using in_own_span[OF carr]
[PROOF STATE]
proof (prove)
using this:
xa \<in> gso ` {0..<i}
gso ` {0..<i} \<subseteq> local.span (gso ` {0..<i})

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

goal (1 subgoal):
 1. \<And>v xa. \<lbrakk>v \<in> carrier_vec n \<and> fs ! i - v \<in> local.span (local.span (gso ` {0..<i})) \<and> (\<forall>u. u \<in> local.span (gso ` {0..<i}) \<longrightarrow> v \<bullet> u = (0::'a)); xa \<in> gso ` {0..<i}\<rbrakk> \<Longrightarrow> v \<bullet> xa = (0::'a)
[PROOF STEP]
thus "v \<bullet> xa = 0"
[PROOF STATE]
proof (prove)
using this:
xa \<in> local.span (gso ` {0..<i})

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gso_is_oc_projection:
  assumes "i < m"
  shows "is_oc_projection (gso i) (set (take i fs)) (fs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_oc_projection (gso i) (set (take i fs)) (fs ! i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_oc_projection (gso i) (set (take i fs)) (fs ! i)
[PROOF STEP]
have [simp]: "v \<in> carrier_vec n" if "v \<in> set (take i fs)" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> carrier_vec n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
v \<in> set (take i fs)

goal (1 subgoal):
 1. v \<in> carrier_vec n
[PROOF STEP]
by (meson contra_subsetD fs_carrier in_set_takeD)
[PROOF STATE]
proof (state)
this:
?v1 \<in> set (take i fs) \<Longrightarrow> ?v1 \<in> carrier_vec n

goal (1 subgoal):
 1. is_oc_projection (gso i) (set (take i fs)) (fs ! i)
[PROOF STEP]
have "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]
by (rule partial_span) (auto simp add: assms less_or_eq_imp_le)
[PROOF STATE]
proof (state)
this:
local.span (gso ` {0..<i}) = local.span (set (take i fs))

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

goal (1 subgoal):
 1. is_oc_projection (gso i) (set (take i fs)) (fs ! i)
[PROOF STEP]
have "is_oc_projection (gso i) (span (gso ` {0..<i})) (fs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_oc_projection (gso i) (local.span (gso ` {0..<i})) (fs ! i)
[PROOF STEP]
by (rule gso_oc_projection_span) (auto simp add: assms less_or_eq_imp_le)
[PROOF STATE]
proof (state)
this:
is_oc_projection (gso i) (local.span (gso ` {0..<i})) (fs ! i)

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

goal (1 subgoal):
 1. is_oc_projection (gso i) (local.span (set (take i fs))) (fs ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_oc_projection (gso i) (local.span (set (take i fs))) (fs ! i)

goal (1 subgoal):
 1. is_oc_projection (gso i) (set (take i fs)) (fs ! i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_oc_projection (gso i) (local.span (set (take i fs))) (fs ! i)

goal (1 subgoal):
 1. is_oc_projection (gso i) (set (take i fs)) (fs ! i)
[PROOF STEP]
have "set (take i fs) \<subseteq> span (set (take i fs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (take i fs) \<subseteq> local.span (set (take i fs))
[PROOF STEP]
by (auto intro!: span_mem)
[PROOF STATE]
proof (state)
this:
set (take i fs) \<subseteq> local.span (set (take i fs))

goal (1 subgoal):
 1. is_oc_projection (gso i) (set (take i fs)) (fs ! i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_oc_projection (gso i) (local.span (set (take i fs))) (fs ! i)
set (take i fs) \<subseteq> local.span (set (take i fs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_oc_projection (gso i) (local.span (set (take i fs))) (fs ! i)
set (take i fs) \<subseteq> local.span (set (take i fs))

goal (1 subgoal):
 1. is_oc_projection (gso i) (set (take i fs)) (fs ! i)
[PROOF STEP]
unfolding is_oc_projection_def
[PROOF STATE]
proof (prove)
using this:
gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (local.span (set (take i fs))) \<and> (\<forall>u. u \<in> local.span (set (take i fs)) \<longrightarrow> gso i \<bullet> u = (0::'a))
set (take i fs) \<subseteq> local.span (set (take i fs))

goal (1 subgoal):
 1. gso i \<in> carrier_vec n \<and> fs ! i - gso i \<in> local.span (set (take i fs)) \<and> (\<forall>u. u \<in> set (take i fs) \<longrightarrow> gso i \<bullet> u = (0::'a))
[PROOF STEP]
by (subst (asm) span_span) (auto)
[PROOF STATE]
proof (state)
this:
is_oc_projection (gso i) (set (take i fs)) (fs ! i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fi_scalar_prod_gso:
  assumes i: "i < m" and j: "j < m"
  shows "fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
let ?mu = "\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < length fs
[PROOF STEP]
have list1: "[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 (intro nth_equalityI, auto simp: nth_append, rename_tac j, case_tac "j - i", auto)
[PROOF STATE]
proof (state)
this:
[0..<length fs] = [0..<Suc i] @ [Suc i..<length fs]

goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
from j
[PROOF STATE]
proof (chain)
picking this:
j < length fs
[PROOF STEP]
have list2: "[0..< m] = [0..< j] @ [j] @ [Suc j ..< m]"
[PROOF STATE]
proof (prove)
using this:
j < length fs

goal (1 subgoal):
 1. [0..<length fs] = [0..<j] @ [j] @ [Suc j..<length fs]
[PROOF STEP]
by (intro nth_equalityI, auto simp: nth_append, rename_tac k, case_tac "k - j", auto)
[PROOF STATE]
proof (state)
this:
[0..<length fs] = [0..<j] @ [j] @ [Suc j..<length fs]

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

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

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

goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<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..<Suc i]) \<bullet> gso j = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]. v \<bullet> gso j) + (0::'a)

goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = (\<Sum>v\<leftarrow>map ?mu [0..<Suc i]. v \<bullet> gso j) + (\<Sum>v\<leftarrow>map ?mu [Suc i..<m]. v \<bullet> gso j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]. v \<bullet> gso j) + (0::'a) = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]. v \<bullet> gso j) + (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [Suc i..<length fs]. v \<bullet> gso j)
[PROOF STEP]
by (subst (3) sum_list_neutral, insert assms gso_carrier, auto intro!: orthogonal simp: \<mu>.simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]. v \<bullet> gso j) + (0::'a) = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]. v \<bullet> gso j) + (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [Suc i..<length fs]. v \<bullet> gso j)

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

goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = (\<Sum>v\<leftarrow>map ?mu [0..< m]. v \<bullet> gso j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]. v \<bullet> gso j) + (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [Suc i..<length fs]. v \<bullet> gso j) = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<length fs]. v \<bullet> gso j)
[PROOF STEP]
unfolding list1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]. v \<bullet> gso j) + (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [Suc i..<length fs]. v \<bullet> gso j) = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) ([0..<Suc i] @ [Suc i..<length fs]). v \<bullet> gso j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]. v \<bullet> gso j) + (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [Suc i..<length fs]. v \<bullet> gso j) = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<length fs]. v \<bullet> gso j)

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

goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = (\<Sum>v\<leftarrow>map ?mu [0..< j]. v \<bullet> gso j) + ?mu j \<bullet> gso j + (\<Sum>v\<leftarrow>map ?mu [Suc j..< m]. v \<bullet> gso j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<length fs]. v \<bullet> gso j) = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]. v \<bullet> gso j) + (\<mu> i j \<cdot>\<^sub>v gso j) \<bullet> gso j + (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [Suc j..<length fs]. v \<bullet> gso j)
[PROOF STEP]
unfolding list2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) ([0..<j] @ [j] @ [Suc j..<length fs]). v \<bullet> gso j) = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]. v \<bullet> gso j) + (\<mu> i j \<cdot>\<^sub>v gso j) \<bullet> gso j + (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [Suc j..<length fs]. v \<bullet> gso j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<length fs]. v \<bullet> gso j) = (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]. v \<bullet> gso j) + (\<mu> i j \<cdot>\<^sub>v gso j) \<bullet> gso j + (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [Suc j..<length fs]. v \<bullet> gso j)

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

goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
have "(\<Sum>v\<leftarrow>map ?mu [0..< j]. v \<bullet> gso j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]. v \<bullet> gso j) = (0::'a)
[PROOF STEP]
by (rule sum_list_neutral, insert assms gso_carrier, auto intro!: orthogonal)
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]. v \<bullet> gso j) = (0::'a)

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

goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
have "(\<Sum>v\<leftarrow>map ?mu [Suc j..< m]. v \<bullet> gso j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [Suc j..<length fs]. v \<bullet> gso j) = (0::'a)
[PROOF STEP]
by (rule sum_list_neutral, insert assms gso_carrier, auto intro!: orthogonal)
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<leftarrow>map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [Suc j..<length fs]. v \<bullet> gso j) = (0::'a)

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

goal (1 subgoal):
 1. fs ! i \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
have "?mu j \<bullet> gso j = \<mu> i j * sq_norm (gso j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> i j \<cdot>\<^sub>v gso j) \<bullet> gso j = \<mu> i j * \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
using gso_carrier[OF j]
[PROOF STATE]
proof (prove)
using this:
gso j \<in> carrier_vec n

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gso_scalar_zero:
  assumes "k < m" "i < k"
  shows "(gso k) \<bullet> (fs ! i) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso k \<bullet> fs ! i = (0::'a)
[PROOF STEP]
by (subst comm_scalar_prod[OF gso_carrier]; (subst fi_scalar_prod_gso)?,
  insert assms, auto simp: \<mu>.simps)


[STATEMENT]
lemma scalar_prod_lincomb_gso:
  assumes k: "k \<le> m"
  shows "sumlist (map (\<lambda> i. g i \<cdot>\<^sub>v gso i) [0 ..< k]) \<bullet> sumlist (map (\<lambda> i. h i \<cdot>\<^sub>v gso i) [0 ..< k])
    = sum_list (map (\<lambda> i. g i * h i * (gso i \<bullet> gso i)) [0 ..< k])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
have id1: "map (\<lambda>i. g i \<cdot>\<^sub>v map (gso) [0..<m] ! i) [0..<k] = map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]" for g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. g i \<cdot>\<^sub>v map gso [0..<length fs] ! i) [0..<k] = map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
k \<le> length fs

goal (1 subgoal):
 1. map (\<lambda>i. g i \<cdot>\<^sub>v map gso [0..<length fs] ! i) [0..<k] = map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. ?g1 i \<cdot>\<^sub>v map gso [0..<length fs] ! i) [0..<k] = map (\<lambda>i. ?g1 i \<cdot>\<^sub>v gso i) [0..<k]

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
have id2: "(\<Sum>i\<leftarrow>[0..<k]. g i * h i * (map (gso) [0..<m] ! i \<bullet> map (gso) [0..<m] ! i))
    = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (map gso [0..<length fs] ! i \<bullet> map gso [0..<length fs] ! i)) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
k \<le> length fs

goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (map gso [0..<length fs] ! i \<bullet> map gso [0..<length fs] ! i)) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
by (intro arg_cong[OF map_cong], auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<leftarrow>[0..<k]. g i * h i * (map gso [0..<length fs] ! i \<bullet> map gso [0..<length fs] ! i)) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
define gs where "gs = map (gso) [0..<m]"
[PROOF STATE]
proof (state)
this:
gs = map gso [0..<length fs]

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
have gs_gso: "gs ! i = gso i" if "i < k" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs ! i = gso i
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
i < k
k \<le> length fs

goal (1 subgoal):
 1. gs ! i = gso i
[PROOF STEP]
unfolding gs_def
[PROOF STATE]
proof (prove)
using this:
i < k
k \<le> length fs

goal (1 subgoal):
 1. map gso [0..<length fs] ! i = gso i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < k \<Longrightarrow> gs ! ?i1 = gso ?i1

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
have "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 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]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gs ! i \<bullet> gs ! i))
[PROOF STEP]
unfolding gs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v map gso [0..<length fs] ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v map gso [0..<length fs] ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (map gso [0..<length fs] ! i \<bullet> map gso [0..<length fs] ! i))
[PROOF STEP]
using  assms  orthogonal_gso
[PROOF STATE]
proof (prove)
using this:
k \<le> length fs
orthogonal (map gso [0..<length fs])

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v map gso [0..<length fs] ! i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v map gso [0..<length fs] ! i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (map gso [0..<length fs] ! i \<bullet> map gso [0..<length fs] ! i))
[PROOF STEP]
by (intro scalar_prod_lincomb_orthogonal) auto
[PROOF STATE]
proof (state)
this:
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))

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
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))

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
have "map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k] = map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k] = map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]
[PROOF STEP]
using gs_gso
[PROOF STATE]
proof (prove)
using this:
?i1 < k \<Longrightarrow> gs ! ?i1 = gso ?i1

goal (1 subgoal):
 1. map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k] = map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]
[PROOF STEP]
by (intro map_cong) (auto)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k] = map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. g i \<cdot>\<^sub>v gs ! i) [0..<k] = map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
have "map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k] = map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k] = map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]
[PROOF STEP]
using gs_gso
[PROOF STATE]
proof (prove)
using this:
?i1 < k \<Longrightarrow> gs ! ?i1 = gso ?i1

goal (1 subgoal):
 1. map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k] = map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]
[PROOF STEP]
by (intro map_cong) (auto)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k] = map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. h i \<cdot>\<^sub>v gs ! i) [0..<k] = map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
have "map (\<lambda>i. g i * h i * (gs ! i \<bullet> gs ! i)) [0..<k] = map (\<lambda>i. g i * h i * (gso i \<bullet> gso i)) [0..<k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. g i * h i * (gs ! i \<bullet> gs ! i)) [0..<k] = map (\<lambda>i. g i * h i * (gso i \<bullet> gso i)) [0..<k]
[PROOF STEP]
using gs_gso
[PROOF STATE]
proof (prove)
using this:
?i1 < k \<Longrightarrow> gs ! ?i1 = gso ?i1

goal (1 subgoal):
 1. map (\<lambda>i. g i * h i * (gs ! i \<bullet> gs ! i)) [0..<k] = map (\<lambda>i. g i * h i * (gso i \<bullet> gso i)) [0..<k]
[PROOF STEP]
by (intro map_cong) (auto)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. g i * h i * (gs ! i \<bullet> gs ! i)) [0..<k] = map (\<lambda>i. g i * h i * (gso i \<bullet> gso i)) [0..<k]

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. g i \<cdot>\<^sub>v gso i) [0..<k]) \<bullet> M.sumlist (map (\<lambda>i. h i \<cdot>\<^sub>v gso i) [0..<k]) = (\<Sum>i\<leftarrow>[0..<k]. g i * h i * (gso i \<bullet> gso i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gso_times_self_is_norm:
  assumes "j < m"
  shows "fs ! j \<bullet> gso j = sq_norm (gso j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! j \<bullet> gso j = \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
by (subst fi_scalar_prod_gso, insert assms, auto simp: \<mu>.simps)