[STATEMENT]
lemma vec_lambda_eq_sum:
     "(\<chi> k. f k (x $ k)) = (\<Sum>k\<in>Basis. (f (axis_index k) (x \<bullet> k)) *\<^sub>R k)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
have "?lhs = (\<chi> k. f k (x \<bullet> axis k 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<chi>k. f k (x \<bullet> axis k 1))
[PROOF STEP]
by (simp add: cart_eq_inner_axis)
[PROOF STATE]
proof (state)
this:
(\<chi>k. f k (x $ k)) = (\<chi>k. f k (x \<bullet> axis k 1))

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<chi>k. f k (x $ k)) = (\<chi>k. f k (x \<bullet> axis k 1))

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
have "... = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>k. f k (x \<bullet> axis k 1)) = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)
[PROOF STEP]
by (simp add: vec_eq_iff axis_def if_distrib cong: if_cong)
[PROOF STATE]
proof (state)
this:
(\<chi>k. f k (x \<bullet> axis k 1)) = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<chi>k. f k (x \<bullet> axis k 1)) = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
have "... = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
by (simp add: Basis_vec_def UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)

goal:
No subgoals!
[PROOF STEP]
qed