[STATEMENT]
lemma sum_zero_representation:
  "v = 0"
  if "\<And>b. b \<in> B \<Longrightarrow> representation B v b = 0" and v: "v \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v = (0::'a)
[PROOF STEP]
have empty: "{b. representation B v b \<noteq> 0} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {b. representation B v b \<noteq> 0} = {}
[PROOF STEP]
using that(1) representation_ne_zero
[PROOF STATE]
proof (prove)
using this:
?b \<in> B \<Longrightarrow> representation B v ?b = 0
representation ?basis ?v ?b \<noteq> 0 \<Longrightarrow> ?b \<in> ?basis

goal (1 subgoal):
 1. {b. representation B v b \<noteq> 0} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{b. representation B v b \<noteq> 0} = {}

goal (1 subgoal):
 1. v = (0::'a)
[PROOF STEP]
have "v \<in> span B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> span B
[PROOF STEP]
using B v
[PROOF STATE]
proof (prove)
using this:
independent B
span B = S
v \<in> S

goal (1 subgoal):
 1. v \<in> span B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> span B

goal (1 subgoal):
 1. v = (0::'a)
[PROOF STEP]
from sum_nonzero_representation_eq[OF B(1) this]
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>b | representation B v b \<noteq> 0. representation B v b *\<^sub>R b) = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>b | representation B v b \<noteq> 0. representation B v b *\<^sub>R b) = v

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

goal:
No subgoals!
[PROOF STEP]
qed