[STATEMENT]
lemma linear_eq_on:
  assumes l: "linear s1 s2 f" "linear s1 s2 g"
  assumes x: "x \<in> vs1.span B" and eq: "\<And>b. b \<in> B \<Longrightarrow> f b = g b"
  shows "f x = g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
interpret d: linear s1 s2 "\<lambda>x. f x - g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear (*a) (*b) (\<lambda>x. f x - g x)
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
linear (*a) (*b) f
linear (*a) (*b) g

goal (1 subgoal):
 1. linear (*a) (*b) (\<lambda>x. f x - g x)
[PROOF STEP]
by (intro linear_compose_sub) (auto simp: module_hom_iff_linear)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
have "f x - g x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x - g x = (0::'c)
[PROOF STEP]
by (rule d.eq_0_on_span[OF _ x]) (auto simp: eq)
[PROOF STATE]
proof (state)
this:
f x - g x = (0::'c)

goal (1 subgoal):
 1. f x = g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f x - g x = (0::'c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f x - g x = (0::'c)

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

goal:
No subgoals!
[PROOF STEP]
qed