[STATEMENT]
lemma normal_vector_span:
  assumes card: "Suc (card D) = n"
    and D: "D \<subseteq> carrier_vec n" and fin: "finite D" and lin: "lin_indpt D"
  shows "span D = { x. x \<in> carrier_vec n \<and> x \<bullet> normal_vector D = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
note nv = normal_vector[OF fin card lin D]
[PROOF STATE]
proof (state)
this:
normal_vector D \<in> carrier_vec n
normal_vector D \<noteq> 0\<^sub>v n
?w \<in> D \<Longrightarrow> ?w \<bullet> normal_vector D = (0::'a)
?w \<in> D \<Longrightarrow> normal_vector D \<bullet> ?w = (0::'a)
lin_indpt (insert (normal_vector D) D)
normal_vector D \<notin> D
\<lbrakk>is_det_bound ?db; D \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int ?Bnd)\<rbrakk> \<Longrightarrow> normal_vector D \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (?db (n - 1) ?Bnd))

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
normal_vector D \<in> carrier_vec n
normal_vector D \<noteq> 0\<^sub>v n
?w \<in> D \<Longrightarrow> ?w \<bullet> normal_vector D = (0::'a)
?w \<in> D \<Longrightarrow> normal_vector D \<bullet> ?w = (0::'a)
lin_indpt (insert (normal_vector D) D)
normal_vector D \<notin> D
\<lbrakk>is_det_bound ?db; D \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int ?Bnd)\<rbrakk> \<Longrightarrow> normal_vector D \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (?db (n - 1) ?Bnd))

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
assume xspan: "x \<in> span D"
[PROOF STATE]
proof (state)
this:
x \<in> local.span D

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
from finite_in_span[OF fin D xspan]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. True \<and> lincomb a D = x
[PROOF STEP]
obtain c where
      "x \<bullet> normal_vector D = lincomb c D \<bullet> normal_vector D"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. True \<and> lincomb a D = x

goal (1 subgoal):
 1. (\<And>c. x \<bullet> normal_vector D = lincomb c D \<bullet> normal_vector D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<bullet> normal_vector D = lincomb c D \<bullet> normal_vector D

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<bullet> normal_vector D = lincomb c D \<bullet> normal_vector D

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
have "\<dots> = (\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c D \<bullet> normal_vector D = (\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D))
[PROOF STEP]
by (rule lincomb_scalar_prod_left, insert D nv, auto)
[PROOF STATE]
proof (state)
this:
lincomb c D \<bullet> normal_vector D = (\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D))

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb c D \<bullet> normal_vector D = (\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D))

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D)) = (0::'a)
[PROOF STEP]
apply (rule sum.neutral)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>D. c x * (x \<bullet> normal_vector D) = (0::'a)
[PROOF STEP]
using nv(1,2,3) D comm_scalar_prod[of "normal_vector D"]
[PROOF STATE]
proof (prove)
using this:
normal_vector D \<in> carrier_vec n
normal_vector D \<noteq> 0\<^sub>v n
?w \<in> D \<Longrightarrow> ?w \<bullet> normal_vector D = (0::'a)
D \<subseteq> carrier_vec n
\<lbrakk>normal_vector D \<in> carrier_vec ?n; ?v\<^sub>2 \<in> carrier_vec ?n\<rbrakk> \<Longrightarrow> normal_vector D \<bullet> ?v\<^sub>2 = ?v\<^sub>2 \<bullet> normal_vector D

goal (1 subgoal):
 1. \<forall>x\<in>D. c x * (x \<bullet> normal_vector D) = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D)) = (0::'a)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<bullet> normal_vector D = (0::'a)
[PROOF STEP]
have "x \<in> carrier_vec n"  "x \<bullet> normal_vector D = 0"
[PROOF STATE]
proof (prove)
using this:
x \<bullet> normal_vector D = (0::'a)

goal (1 subgoal):
 1. x \<in> carrier_vec n &&& x \<bullet> normal_vector D = (0::'a)
[PROOF STEP]
using xspan D
[PROOF STATE]
proof (prove)
using this:
x \<bullet> normal_vector D = (0::'a)
x \<in> local.span D
D \<subseteq> carrier_vec n

goal (1 subgoal):
 1. x \<in> carrier_vec n &&& x \<bullet> normal_vector D = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec n
x \<bullet> normal_vector D = (0::'a)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x5 \<in> local.span D \<Longrightarrow> ?x5 \<in> carrier_vec n
?x5 \<in> local.span D \<Longrightarrow> ?x5 \<bullet> normal_vector D = (0::'a)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x5 \<in> local.span D \<Longrightarrow> ?x5 \<in> carrier_vec n
?x5 \<in> local.span D \<Longrightarrow> ?x5 \<bullet> normal_vector D = (0::'a)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?x5 \<in> local.span D \<Longrightarrow> ?x5 \<in> carrier_vec n
?x5 \<in> local.span D \<Longrightarrow> ?x5 \<bullet> normal_vector D = (0::'a)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
let ?n = "normal_vector D"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
assume x: "x \<in> carrier_vec n" and xscal: "x \<bullet> normal_vector D = 0"
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec n
x \<bullet> normal_vector D = (0::'a)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
let ?B = "(insert (normal_vector D) D)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
have "card ?B = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (insert (normal_vector D) D) = n
[PROOF STEP]
using card card_insert_disjoint[OF fin nv(6)]
[PROOF STATE]
proof (prove)
using this:
Suc (card D) = n
card (insert (normal_vector D) D) = Suc (card D)

goal (1 subgoal):
 1. card (insert (normal_vector D) D) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (insert (normal_vector D) D) = n

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (insert (normal_vector D) D) = n

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
have B: "?B \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (normal_vector D) D \<subseteq> carrier_vec n
[PROOF STEP]
using D nv
[PROOF STATE]
proof (prove)
using this:
D \<subseteq> carrier_vec n
normal_vector D \<in> carrier_vec n
normal_vector D \<noteq> 0\<^sub>v n
?w \<in> D \<Longrightarrow> ?w \<bullet> normal_vector D = (0::'a)
?w \<in> D \<Longrightarrow> normal_vector D \<bullet> ?w = (0::'a)
lin_indpt (insert (normal_vector D) D)
normal_vector D \<notin> D
\<lbrakk>is_det_bound ?db; D \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int ?Bnd)\<rbrakk> \<Longrightarrow> normal_vector D \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (?db (n - 1) ?Bnd))

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

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (insert (normal_vector D) D) = n
insert (normal_vector D) D \<subseteq> carrier_vec n
[PROOF STEP]
have "span ?B = carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
card (insert (normal_vector D) D) = n
insert (normal_vector D) D \<subseteq> carrier_vec n

goal (1 subgoal):
 1. local.span (insert (normal_vector D) D) = carrier_vec n
[PROOF STEP]
by (intro span_carrier_lin_indpt_card_n, insert nv(5), auto)
[PROOF STATE]
proof (state)
this:
local.span (insert (normal_vector D) D) = carrier_vec n

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
hence xspan: "x \<in> span ?B"
[PROOF STATE]
proof (prove)
using this:
local.span (insert (normal_vector D) D) = carrier_vec n

goal (1 subgoal):
 1. x \<in> local.span (insert (normal_vector D) D)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
local.span (insert (normal_vector D) D) = carrier_vec n
x \<in> carrier_vec n

goal (1 subgoal):
 1. x \<in> local.span (insert (normal_vector D) D)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> local.span (insert (normal_vector D) D)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
obtain c where "x = lincomb c ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. x = lincomb c (insert (normal_vector D) D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_in_span[OF _ B xspan] fin
[PROOF STATE]
proof (prove)
using this:
finite (insert (normal_vector D) D) \<Longrightarrow> \<exists>a. True \<and> lincomb a (insert (normal_vector D) D) = x
finite D

goal (1 subgoal):
 1. (\<And>c. x = lincomb c (insert (normal_vector D) D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = lincomb c (insert (normal_vector D) D)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
hence "0 = lincomb c ?B \<bullet> normal_vector D"
[PROOF STATE]
proof (prove)
using this:
x = lincomb c (insert (normal_vector D) D)

goal (1 subgoal):
 1. (0::'a) = lincomb c (insert (normal_vector D) D) \<bullet> normal_vector D
[PROOF STEP]
using xscal
[PROOF STATE]
proof (prove)
using this:
x = lincomb c (insert (normal_vector D) D)
x \<bullet> normal_vector D = (0::'a)

goal (1 subgoal):
 1. (0::'a) = lincomb c (insert (normal_vector D) D) \<bullet> normal_vector D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) = lincomb c (insert (normal_vector D) D) \<bullet> normal_vector D

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) = lincomb c (insert (normal_vector D) D) \<bullet> normal_vector D

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
have "\<dots> = (\<Sum>w\<in> ?B. c w * (w \<bullet> normal_vector D))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c (insert (normal_vector D) D) \<bullet> normal_vector D = (\<Sum>w\<in>insert (normal_vector D) D. c w * (w \<bullet> normal_vector D))
[PROOF STEP]
by (subst lincomb_scalar_prod_left, insert B, auto)
[PROOF STATE]
proof (state)
this:
lincomb c (insert (normal_vector D) D) \<bullet> normal_vector D = (\<Sum>w\<in>insert (normal_vector D) D. c w * (w \<bullet> normal_vector D))

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb c (insert (normal_vector D) D) \<bullet> normal_vector D = (\<Sum>w\<in>insert (normal_vector D) D. c w * (w \<bullet> normal_vector D))

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
have "\<dots> = (\<Sum>w\<in> D. c w * (w \<bullet> normal_vector D)) + c ?n * (?n \<bullet> ?n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>w\<in>insert (normal_vector D) D. c w * (w \<bullet> normal_vector D)) = (\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D)) + c (normal_vector D) * (normal_vector D \<bullet> normal_vector D)
[PROOF STEP]
by (subst sum.insert[OF fin nv(6)], auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>insert (normal_vector D) D. c w * (w \<bullet> normal_vector D)) = (\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D)) + c (normal_vector D) * (normal_vector D \<bullet> normal_vector D)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>insert (normal_vector D) D. c w * (w \<bullet> normal_vector D)) = (\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D)) + c (normal_vector D) * (normal_vector D \<bullet> normal_vector D)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
have "(\<Sum>w\<in> D. c w * (w \<bullet> normal_vector D)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D)) = (0::'a)
[PROOF STEP]
apply(rule sum.neutral)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>D. c x * (x \<bullet> normal_vector D) = (0::'a)
[PROOF STEP]
using nv(1,3) comm_scalar_prod[OF nv(1)] D
[PROOF STATE]
proof (prove)
using this:
normal_vector D \<in> carrier_vec n
?w \<in> D \<Longrightarrow> ?w \<bullet> normal_vector D = (0::'a)
?v\<^sub>2 \<in> carrier_vec n \<Longrightarrow> normal_vector D \<bullet> ?v\<^sub>2 = ?v\<^sub>2 \<bullet> normal_vector D
D \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<forall>x\<in>D. c x * (x \<bullet> normal_vector D) = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D)) = (0::'a)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>D. c w * (w \<bullet> normal_vector D)) = (0::'a)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
have "?n \<bullet> ?n = sq_norm ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_vector D \<bullet> normal_vector D = \<parallel>normal_vector D\<parallel>\<^sup>2
[PROOF STEP]
using sq_norm_vec_as_cscalar_prod[of ?n]
[PROOF STATE]
proof (prove)
using this:
\<parallel>normal_vector D\<parallel>\<^sup>2 = normal_vector D \<bullet>c normal_vector D

goal (1 subgoal):
 1. normal_vector D \<bullet> normal_vector D = \<parallel>normal_vector D\<parallel>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
normal_vector D \<bullet> normal_vector D = \<parallel>normal_vector D\<parallel>\<^sup>2

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'a) = (0::'a) + c (normal_vector D) * \<parallel>normal_vector D\<parallel>\<^sup>2
[PROOF STEP]
have "c ?n * sq_norm ?n = 0"
[PROOF STATE]
proof (prove)
using this:
(0::'a) = (0::'a) + c (normal_vector D) * \<parallel>normal_vector D\<parallel>\<^sup>2

goal (1 subgoal):
 1. c (normal_vector D) * \<parallel>normal_vector D\<parallel>\<^sup>2 = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c (normal_vector D) * \<parallel>normal_vector D\<parallel>\<^sup>2 = (0::'a)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
hence ncoord: "c ?n = 0"
[PROOF STATE]
proof (prove)
using this:
c (normal_vector D) * \<parallel>normal_vector D\<parallel>\<^sup>2 = (0::'a)

goal (1 subgoal):
 1. c (normal_vector D) = (0::'a)
[PROOF STEP]
using nv(1-5)
[PROOF STATE]
proof (prove)
using this:
c (normal_vector D) * \<parallel>normal_vector D\<parallel>\<^sup>2 = (0::'a)
normal_vector D \<in> carrier_vec n
normal_vector D \<noteq> 0\<^sub>v n
?w \<in> D \<Longrightarrow> ?w \<bullet> normal_vector D = (0::'a)
?w \<in> D \<Longrightarrow> normal_vector D \<bullet> ?w = (0::'a)
lin_indpt (insert (normal_vector D) D)

goal (1 subgoal):
 1. c (normal_vector D) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c (normal_vector D) = (0::'a)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
have "x = lincomb c ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = lincomb c (insert (normal_vector D) D)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
x = lincomb c (insert (normal_vector D) D)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = lincomb c (insert (normal_vector D) D)

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
have "\<dots> = lincomb c D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c (insert (normal_vector D) D) = lincomb c D
[PROOF STEP]
apply (subst lincomb_insert2[OF fin D _ nv(6,1)])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. c \<in> insert (normal_vector D) D \<rightarrow> UNIV
 2. c (normal_vector D) \<cdot>\<^sub>v normal_vector D + lincomb c D = lincomb c D
[PROOF STEP]
using ncoord nv(1) D
[PROOF STATE]
proof (prove)
using this:
c (normal_vector D) = (0::'a)
normal_vector D \<in> carrier_vec n
D \<subseteq> carrier_vec n

goal (2 subgoals):
 1. c \<in> insert (normal_vector D) D \<rightarrow> UNIV
 2. c (normal_vector D) \<cdot>\<^sub>v normal_vector D + lincomb c D = lincomb c D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb c (insert (normal_vector D) D) = lincomb c D

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x = lincomb c D
[PROOF STEP]
have "x \<in> span D"
[PROOF STATE]
proof (prove)
using this:
x = lincomb c D

goal (1 subgoal):
 1. x \<in> local.span D
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
x = lincomb c D
finite D

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

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x5 \<in> carrier_vec n; ?x5 \<bullet> normal_vector D = (0::'a)\<rbrakk> \<Longrightarrow> ?x5 \<in> local.span D

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x5 \<in> local.span D \<Longrightarrow> ?x5 \<in> carrier_vec n
?x5 \<in> local.span D \<Longrightarrow> ?x5 \<bullet> normal_vector D = (0::'a)
\<lbrakk>?x5 \<in> carrier_vec n; ?x5 \<bullet> normal_vector D = (0::'a)\<rbrakk> \<Longrightarrow> ?x5 \<in> local.span D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x5 \<in> local.span D \<Longrightarrow> ?x5 \<in> carrier_vec n
?x5 \<in> local.span D \<Longrightarrow> ?x5 \<bullet> normal_vector D = (0::'a)
\<lbrakk>?x5 \<in> carrier_vec n; ?x5 \<bullet> normal_vector D = (0::'a)\<rbrakk> \<Longrightarrow> ?x5 \<in> local.span D

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}

goal:
No subgoals!
[PROOF STEP]
qed