[STATEMENT]
lemma (in complex_vec_space) vec_of_basis_enum_cspan:
  fixes X :: "'a::basis_enum set"
  assumes "length (canonical_basis :: 'a list) = n"
  shows "vec_of_basis_enum ` cspan X = span (vec_of_basis_enum ` X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum ` cspan X = local.span (vec_of_basis_enum ` X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec_of_basis_enum ` cspan X = local.span (vec_of_basis_enum ` X)
[PROOF STEP]
have carrier: "vec_of_basis_enum ` X \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum ` X \<subseteq> carrier_vec n
[PROOF STEP]
by (metis assms carrier_vecI dim_vec_of_basis_enum' image_subsetI)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum ` X \<subseteq> carrier_vec n

goal (1 subgoal):
 1. vec_of_basis_enum ` cspan X = local.span (vec_of_basis_enum ` X)
[PROOF STEP]
have lincomb_sum: "lincomb c A = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)"
    if B_def: "B = basis_enum_of_vec ` A" and \<open>finite A\<close>
      and AX: "A \<subseteq> vec_of_basis_enum ` X" and c'_def: "\<And>b. c' b = c (vec_of_basis_enum b)"
    for c c' A and B::"'a set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c A = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c A = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` A. c' b *\<^sub>C b)
[PROOF STEP]
using \<open>finite A\<close> AX
[PROOF STATE]
proof (prove)
using this:
finite A
A \<subseteq> vec_of_basis_enum ` X

goal (1 subgoal):
 1. lincomb c A = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` A. c' b *\<^sub>C b)
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c {} = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` {}. c' b *\<^sub>C b)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<subseteq> vec_of_basis_enum ` X

goal (2 subgoals):
 1. {} \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c {} = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` {}. c' b *\<^sub>C b)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} \<subseteq> vec_of_basis_enum ` X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> vec_of_basis_enum ` X

goal (1 subgoal):
 1. lincomb c {} = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` {}. c' b *\<^sub>C b)
[PROOF STEP]
by (simp add: assms vec_of_basis_enum_zero)
[PROOF STATE]
proof (state)
this:
lincomb c {} = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` {}. c' b *\<^sub>C b)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)
insert x F \<subseteq> vec_of_basis_enum ` X

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)
insert x F \<subseteq> vec_of_basis_enum ` X
[PROOF STEP]
have IH: "lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)"
      (is "_ = ?sum")
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)
insert x F \<subseteq> vec_of_basis_enum ` X

goal (1 subgoal):
 1. lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
have xx: "vec_of_basis_enum (basis_enum_of_vec x :: 'a) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (basis_enum_of_vec x) = x
[PROOF STEP]
apply (rule basis_enum_of_vec_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec x = length canonical_basis
[PROOF STEP]
using assms carrier carrier_vecD insert.prems
[PROOF STATE]
proof (prove)
using this:
length canonical_basis = n
vec_of_basis_enum ` X \<subseteq> carrier_vec n
?v \<in> carrier_vec ?n \<Longrightarrow> dim_vec ?v = ?n
insert x F \<subseteq> vec_of_basis_enum ` X

goal (1 subgoal):
 1. dim_vec x = length canonical_basis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (basis_enum_of_vec x) = x

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
have "lincomb c (insert x F) = c x \<cdot>\<^sub>v x + lincomb c F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c (insert x F) = c x \<cdot>\<^sub>v x + lincomb c F
[PROOF STEP]
apply (rule lincomb_insert2)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. finite F
 2. F \<subseteq> carrier_vec n
 3. c \<in> insert x F \<rightarrow> UNIV
 4. x \<notin> F
 5. x \<in> carrier_vec n
[PROOF STEP]
using insert.hyps insert.prems carrier
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
insert x F \<subseteq> vec_of_basis_enum ` X
vec_of_basis_enum ` X \<subseteq> carrier_vec n

goal (5 subgoals):
 1. finite F
 2. F \<subseteq> carrier_vec n
 3. c \<in> insert x F \<rightarrow> UNIV
 4. x \<notin> F
 5. x \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb c (insert x F) = c x \<cdot>\<^sub>v x + lincomb c F

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb c (insert x F) = c x \<cdot>\<^sub>v x + lincomb c F

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
have "c x \<cdot>\<^sub>v x = vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C (basis_enum_of_vec x :: 'a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c x \<cdot>\<^sub>v x = vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x)
[PROOF STEP]
by (simp add: xx vec_of_basis_enum_scaleC c'_def)
[PROOF STATE]
proof (state)
this:
c x \<cdot>\<^sub>v x = vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c x \<cdot>\<^sub>v x = vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
note IH
[PROOF STATE]
proof (state)
this:
lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
have
      "vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C (basis_enum_of_vec x :: 'a)) + ?sum
          = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x) + vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x) + vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b) = vec_of_basis_enum (\<Sum>b\<in>insert (basis_enum_of_vec x) (basis_enum_of_vec ` F). c' b *\<^sub>C b)
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (\<Sum>b\<in>insert (basis_enum_of_vec x) (basis_enum_of_vec ` F). c' b *\<^sub>C b) = vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x) + vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)
[PROOF STEP]
apply (subst sum.insert)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite (basis_enum_of_vec ` F)
 2. basis_enum_of_vec x \<notin> basis_enum_of_vec ` F
 3. vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x + (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)) = vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x) + vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)
[PROOF STEP]
using \<open>finite F\<close> \<open>x \<notin> F\<close> dim_vec_of_basis_enum' insert.prems
        vec_of_basis_enum_add c'_def
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
dim_vec (vec_of_basis_enum ?v) = length canonical_basis
insert x F \<subseteq> vec_of_basis_enum ` X
vec_of_basis_enum (?b1.0 + ?b2.0) = vec_of_basis_enum ?b1.0 + vec_of_basis_enum ?b2.0
c' ?b1 = c (vec_of_basis_enum ?b1)

goal (3 subgoals):
 1. finite (basis_enum_of_vec ` F)
 2. basis_enum_of_vec x \<notin> basis_enum_of_vec ` F
 3. vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x + (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)) = vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x) + vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (c' (basis_enum_of_vec x) *\<^sub>C basis_enum_of_vec x) + vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> vec_of_basis_enum ` X \<Longrightarrow> lincomb c F = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` F. c' b *\<^sub>C b); insert x F \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)

goal (1 subgoal):
 1. lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
lincomb c (insert x F) = vec_of_basis_enum (\<Sum>b\<in>basis_enum_of_vec ` insert x F. c' b *\<^sub>C b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?B1 = basis_enum_of_vec ` ?A1; finite ?A1; ?A1 \<subseteq> vec_of_basis_enum ` X; \<And>b. ?c'1 b = ?c1 (vec_of_basis_enum b)\<rbrakk> \<Longrightarrow> lincomb ?c1 ?A1 = vec_of_basis_enum (\<Sum>b\<in>?B1. ?c'1 b *\<^sub>C b)

goal (1 subgoal):
 1. vec_of_basis_enum ` cspan X = local.span (vec_of_basis_enum ` X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum ` cspan X = local.span (vec_of_basis_enum ` X)
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
 2. \<And>x. x \<in> local.span (vec_of_basis_enum ` X) \<Longrightarrow> x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
 2. \<And>x. x \<in> local.span (vec_of_basis_enum ` X) \<Longrightarrow> x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
assume "x \<in> local.span (vec_of_basis_enum ` X)"
[PROOF STATE]
proof (state)
this:
x \<in> local.span (vec_of_basis_enum ` X)

goal (2 subgoals):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
 2. \<And>x. x \<in> local.span (vec_of_basis_enum ` X) \<Longrightarrow> x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
obtain c A where xA: "x = lincomb c A" and "finite A" and AX: "A \<subseteq> vec_of_basis_enum ` X"
[PROOF STATE]
proof (prove)
using this:
x \<in> local.span (vec_of_basis_enum ` X)

goal (1 subgoal):
 1. (\<And>c A. \<lbrakk>x = lincomb c A; finite A; A \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding span_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {lincomb a A |a A. finite A \<and> A \<subseteq> vec_of_basis_enum ` X}

goal (1 subgoal):
 1. (\<And>c A. \<lbrakk>x = lincomb c A; finite A; A \<subseteq> vec_of_basis_enum ` X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = lincomb c A
finite A
A \<subseteq> vec_of_basis_enum ` X

goal (2 subgoals):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
 2. \<And>x. x \<in> local.span (vec_of_basis_enum ` X) \<Longrightarrow> x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
define B::"'a set" and c' where "B = basis_enum_of_vec ` A"
      and "c' b = c (vec_of_basis_enum b)" for b::'a
[PROOF STATE]
proof (state)
this:
B = basis_enum_of_vec ` A
c' ?b = c (vec_of_basis_enum ?b)

goal (2 subgoals):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
 2. \<And>x. x \<in> local.span (vec_of_basis_enum ` X) \<Longrightarrow> x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
note xA
[PROOF STATE]
proof (state)
this:
x = lincomb c A

goal (2 subgoals):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
 2. \<And>x. x \<in> local.span (vec_of_basis_enum ` X) \<Longrightarrow> x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = lincomb c A

goal (2 subgoals):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
 2. \<And>x. x \<in> local.span (vec_of_basis_enum ` X) \<Longrightarrow> x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
have "lincomb c A = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c A = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)
[PROOF STEP]
using B_def \<open>finite A\<close> AX c'_def
[PROOF STATE]
proof (prove)
using this:
B = basis_enum_of_vec ` A
finite A
A \<subseteq> vec_of_basis_enum ` X
c' ?b = c (vec_of_basis_enum ?b)

goal (1 subgoal):
 1. lincomb c A = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)
[PROOF STEP]
by (rule lincomb_sum)
[PROOF STATE]
proof (state)
this:
lincomb c A = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)

goal (2 subgoals):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
 2. \<And>x. x \<in> local.span (vec_of_basis_enum ` X) \<Longrightarrow> x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb c A = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)

goal (2 subgoals):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
 2. \<And>x. x \<in> local.span (vec_of_basis_enum ` X) \<Longrightarrow> x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
have "\<dots> \<in> vec_of_basis_enum ` cspan X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b) \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
unfolding complex_vector.span_explicit
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b) \<in> vec_of_basis_enum ` {\<Sum>a\<in>t. r a *\<^sub>C a |t r. finite t \<and> t \<subseteq> X}
[PROOF STEP]
apply (rule imageI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>b\<in>B. c' b *\<^sub>C b) \<in> {\<Sum>a\<in>t. r a *\<^sub>C a |t r. finite t \<and> t \<subseteq> X}
[PROOF STEP]
apply (rule CollectI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t r. (\<Sum>b\<in>B. c' b *\<^sub>C b) = (\<Sum>a\<in>t. r a *\<^sub>C a) \<and> finite t \<and> t \<subseteq> X
[PROOF STEP]
apply (rule exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. (\<Sum>b\<in>B. c' b *\<^sub>C b) = (\<Sum>a\<in>?t4. r a *\<^sub>C a) \<and> finite ?t4 \<and> ?t4 \<subseteq> X
[PROOF STEP]
apply (rule exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>b\<in>B. c' b *\<^sub>C b) = (\<Sum>a\<in>?t4. ?r6 a *\<^sub>C a) \<and> finite ?t4 \<and> ?t4 \<subseteq> X
[PROOF STEP]
using \<open>finite A\<close> AX
[PROOF STATE]
proof (prove)
using this:
finite A
A \<subseteq> vec_of_basis_enum ` X

goal (1 subgoal):
 1. (\<Sum>b\<in>B. c' b *\<^sub>C b) = (\<Sum>a\<in>?t4. ?r6 a *\<^sub>C a) \<and> finite ?t4 \<and> ?t4 \<subseteq> X
[PROOF STEP]
by (auto simp: B_def)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b) \<in> vec_of_basis_enum ` cspan X

goal (2 subgoals):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
 2. \<And>x. x \<in> local.span (vec_of_basis_enum ` X) \<Longrightarrow> x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
show "x \<in> vec_of_basis_enum ` cspan X"
[PROOF STATE]
proof (prove)
using this:
x \<in> vec_of_basis_enum ` cspan X

goal (1 subgoal):
 1. x \<in> vec_of_basis_enum ` cspan X
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
x \<in> vec_of_basis_enum ` cspan X

goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
assume "x \<in> cspan X"
[PROOF STATE]
proof (state)
this:
x \<in> cspan X

goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> cspan X
[PROOF STEP]
obtain c' B where x: "x = (\<Sum>b\<in>B. c' b *\<^sub>C b)" and "finite B" and BX: "B \<subseteq> X"
[PROOF STATE]
proof (prove)
using this:
x \<in> cspan X

goal (1 subgoal):
 1. (\<And>c' B. \<lbrakk>x = (\<Sum>b\<in>B. c' b *\<^sub>C b); finite B; B \<subseteq> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding complex_vector.span_explicit
[PROOF STATE]
proof (prove)
using this:
x \<in> {\<Sum>a\<in>t. r a *\<^sub>C a |t r. finite t \<and> t \<subseteq> X}

goal (1 subgoal):
 1. (\<And>c' B. \<lbrakk>x = (\<Sum>b\<in>B. c' b *\<^sub>C b); finite B; B \<subseteq> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (\<Sum>b\<in>B. c' b *\<^sub>C b)
finite B
B \<subseteq> X

goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
define A and c where "A = vec_of_basis_enum ` B"
      and "c b = c' (basis_enum_of_vec b)" for b
[PROOF STATE]
proof (state)
this:
A = vec_of_basis_enum ` B
c ?b = c' (basis_enum_of_vec ?b)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
have "vec_of_basis_enum x = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum x = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x = (\<Sum>b\<in>B. c' b *\<^sub>C b)

goal (1 subgoal):
 1. vec_of_basis_enum x = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum x = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum x = vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
have "\<dots> = lincomb c A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b) = lincomb c A
[PROOF STEP]
apply (rule lincomb_sum[symmetric])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. B = basis_enum_of_vec ` A
 2. finite A
 3. A \<subseteq> vec_of_basis_enum ` X
 4. \<And>b. c' b = c (vec_of_basis_enum b)
[PROOF STEP]
unfolding A_def c_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. B = basis_enum_of_vec ` vec_of_basis_enum ` B
 2. finite (vec_of_basis_enum ` B)
 3. vec_of_basis_enum ` B \<subseteq> vec_of_basis_enum ` X
 4. \<And>b. c' b = c' (basis_enum_of_vec (vec_of_basis_enum b))
[PROOF STEP]
using BX \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> X
finite B

goal (4 subgoals):
 1. B = basis_enum_of_vec ` vec_of_basis_enum ` B
 2. finite (vec_of_basis_enum ` B)
 3. vec_of_basis_enum ` B \<subseteq> vec_of_basis_enum ` X
 4. \<And>b. c' b = c' (basis_enum_of_vec (vec_of_basis_enum b))
[PROOF STEP]
by (auto simp: image_image)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b) = lincomb c A

goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (\<Sum>b\<in>B. c' b *\<^sub>C b) = lincomb c A

goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
have "\<dots> \<in> span (vec_of_basis_enum ` X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c A \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
unfolding span_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c A \<in> {lincomb a A |a A. finite A \<and> A \<subseteq> vec_of_basis_enum ` X}
[PROOF STEP]
apply (rule CollectI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a Aa. lincomb c A = lincomb a Aa \<and> finite Aa \<and> Aa \<subseteq> vec_of_basis_enum ` X
[PROOF STEP]
apply (rule exI, rule exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c A = lincomb ?a2 ?A4 \<and> finite ?A4 \<and> ?A4 \<subseteq> vec_of_basis_enum ` X
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c (vec_of_basis_enum ` B) = lincomb ?a2 ?A4 \<and> finite ?A4 \<and> ?A4 \<subseteq> vec_of_basis_enum ` X
[PROOF STEP]
using \<open>finite B\<close> BX
[PROOF STATE]
proof (prove)
using this:
finite B
B \<subseteq> X

goal (1 subgoal):
 1. lincomb c (vec_of_basis_enum ` B) = lincomb ?a2 ?A4 \<and> finite ?A4 \<and> ?A4 \<subseteq> vec_of_basis_enum ` X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb c A \<in> local.span (vec_of_basis_enum ` X)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cspan X \<Longrightarrow> vec_of_basis_enum xa \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
vec_of_basis_enum x \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
show "vec_of_basis_enum x \<in> local.span (vec_of_basis_enum ` X)"
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum x \<in> local.span (vec_of_basis_enum ` X)

goal (1 subgoal):
 1. vec_of_basis_enum x \<in> local.span (vec_of_basis_enum ` X)
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum x \<in> local.span (vec_of_basis_enum ` X)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum ` cspan X = local.span (vec_of_basis_enum ` X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in complex_vec_space) basis_enum_of_vec_span:
  assumes "length (canonical_basis :: 'a list) = n"
  assumes "Y \<subseteq> carrier_vec n"
  shows "basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y :: 'a::basis_enum set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y)
[PROOF STEP]
define X::"'a set" where "X = basis_enum_of_vec ` Y"
[PROOF STATE]
proof (state)
this:
X = basis_enum_of_vec ` Y

goal (1 subgoal):
 1. basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X = basis_enum_of_vec ` Y
[PROOF STEP]
have "cspan (basis_enum_of_vec ` Y :: 'a set) = basis_enum_of_vec ` vec_of_basis_enum ` cspan X"
[PROOF STATE]
proof (prove)
using this:
X = basis_enum_of_vec ` Y

goal (1 subgoal):
 1. cspan (basis_enum_of_vec ` Y) = basis_enum_of_vec ` vec_of_basis_enum ` cspan X
[PROOF STEP]
by (simp add: image_image)
[PROOF STATE]
proof (state)
this:
cspan (basis_enum_of_vec ` Y) = basis_enum_of_vec ` vec_of_basis_enum ` cspan X

goal (1 subgoal):
 1. basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cspan (basis_enum_of_vec ` Y) = basis_enum_of_vec ` vec_of_basis_enum ` cspan X

goal (1 subgoal):
 1. basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y)
[PROOF STEP]
have "\<dots> = basis_enum_of_vec ` local.span (vec_of_basis_enum ` X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec ` vec_of_basis_enum ` cspan X = basis_enum_of_vec ` local.span (vec_of_basis_enum ` X)
[PROOF STEP]
apply (subst vec_of_basis_enum_cspan)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length canonical_basis = n
 2. basis_enum_of_vec ` local.span (vec_of_basis_enum ` X) = basis_enum_of_vec ` local.span (vec_of_basis_enum ` X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length canonical_basis = n
Y \<subseteq> carrier_vec n

goal (2 subgoals):
 1. length canonical_basis = n
 2. basis_enum_of_vec ` local.span (vec_of_basis_enum ` X) = basis_enum_of_vec ` local.span (vec_of_basis_enum ` X)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec ` vec_of_basis_enum ` cspan X = basis_enum_of_vec ` local.span (vec_of_basis_enum ` X)

goal (1 subgoal):
 1. basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec ` vec_of_basis_enum ` cspan X = basis_enum_of_vec ` local.span (vec_of_basis_enum ` X)

goal (1 subgoal):
 1. basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y)
[PROOF STEP]
have "vec_of_basis_enum ` X = Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum ` X = Y
[PROOF STEP]
unfolding X_def image_image
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. vec_of_basis_enum (basis_enum_of_vec x)) ` Y = Y
[PROOF STEP]
apply (rule image_cong[where g=id and M=Y and N=Y, simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec x) = x
[PROOF STEP]
using assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
length canonical_basis = n
Y \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> Y \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec x) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum ` X = Y

goal (1 subgoal):
 1. basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cspan (basis_enum_of_vec ` Y) = basis_enum_of_vec ` local.span Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cspan (basis_enum_of_vec ` Y) = basis_enum_of_vec ` local.span Y

goal (1 subgoal):
 1. basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec ` local.span Y = cspan (basis_enum_of_vec ` Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_basis_enum_canonical_basis:
  assumes "i < length (canonical_basis :: 'a list)"
  shows "vec_of_basis_enum (canonical_basis!i :: 'a)
       = unit_vec (length (canonical_basis :: 'a::basis_enum list)) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (canonical_basis ! i) = unit_vec (length canonical_basis) i
[PROOF STEP]
by (metis assms basis_enum_of_vec_inverse basis_enum_of_vec_unit_vec index_unit_vec(3))


[STATEMENT]
lemma vec_of_basis_enum_times:
  fixes \<psi> \<phi> :: "'a::one_dim"
  shows "vec_of_basis_enum (\<psi> * \<phi>)
   = vec_of_list [vec_index (vec_of_basis_enum \<psi>) 0 * vec_index (vec_of_basis_enum \<phi>) 0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (\<psi> * \<phi>) = vec_of_list [vec_of_basis_enum \<psi> $ 0 * vec_of_basis_enum \<phi> $ 0]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec_of_basis_enum (\<psi> * \<phi>) = vec_of_list [vec_of_basis_enum \<psi> $ 0 * vec_of_basis_enum \<phi> $ 0]
[PROOF STEP]
have [simp]: \<open>crepresentation {1} x 1 = one_dim_iso x\<close> for x :: 'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation {1::'a} x (1::'a) = one_dim_iso x
[PROOF STEP]
apply (subst one_dim_scaleC_1[where x=x, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation {1::'a} (one_dim_iso x *\<^sub>C (1::'a)) (1::'a) = one_dim_iso x
[PROOF STEP]
apply (subst complex_vector.representation_scale)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. cindependent {1::'a}
 2. (1::'a) \<in> cspan {1::'a}
 3. one_dim_iso x * crepresentation {1::'a} (1::'a) (1::'a) = one_dim_iso x
[PROOF STEP]
by (auto simp add: complex_vector.span_base complex_vector.representation_basis)
[PROOF STATE]
proof (state)
this:
crepresentation {1::'a} ?x (1::'a) = one_dim_iso ?x

goal (1 subgoal):
 1. vec_of_basis_enum (\<psi> * \<phi>) = vec_of_list [vec_of_basis_enum \<psi> $ 0 * vec_of_basis_enum \<phi> $ 0]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (\<psi> * \<phi>) = vec_of_list [vec_of_basis_enum \<psi> $ 0 * vec_of_basis_enum \<phi> $ 0]
[PROOF STEP]
apply (rule eq_vecI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (vec_of_list [vec_of_basis_enum \<psi> $ 0 * vec_of_basis_enum \<phi> $ 0]) \<Longrightarrow> vec_of_basis_enum (\<psi> * \<phi>) $ i = vec_of_list [vec_of_basis_enum \<psi> $ 0 * vec_of_basis_enum \<phi> $ 0] $ i
 2. dim_vec (vec_of_basis_enum (\<psi> * \<phi>)) = dim_vec (vec_of_list [vec_of_basis_enum \<psi> $ 0 * vec_of_basis_enum \<phi> $ 0])
[PROOF STEP]
by (auto simp: vec_of_basis_enum_def)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (\<psi> * \<phi>) = vec_of_list [vec_of_basis_enum \<psi> $ 0 * vec_of_basis_enum \<phi> $ 0]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_basis_enum_to_inverse:
  fixes \<psi> :: "'a::one_dim"
  shows "vec_of_basis_enum (inverse \<psi>) = vec_of_list [inverse (vec_index (vec_of_basis_enum \<psi>) 0)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (inverse \<psi>) = vec_of_list [inverse (vec_of_basis_enum \<psi> $ 0)]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec_of_basis_enum (inverse \<psi>) = vec_of_list [inverse (vec_of_basis_enum \<psi> $ 0)]
[PROOF STEP]
have [simp]: \<open>crepresentation {1} x 1 = one_dim_iso x\<close> for x :: 'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation {1::'a} x (1::'a) = one_dim_iso x
[PROOF STEP]
apply (subst one_dim_scaleC_1[where x=x, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation {1::'a} (one_dim_iso x *\<^sub>C (1::'a)) (1::'a) = one_dim_iso x
[PROOF STEP]
apply (subst complex_vector.representation_scale)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. cindependent {1::'a}
 2. (1::'a) \<in> cspan {1::'a}
 3. one_dim_iso x * crepresentation {1::'a} (1::'a) (1::'a) = one_dim_iso x
[PROOF STEP]
by (auto simp add: complex_vector.span_base complex_vector.representation_basis)
[PROOF STATE]
proof (state)
this:
crepresentation {1::'a} ?x (1::'a) = one_dim_iso ?x

goal (1 subgoal):
 1. vec_of_basis_enum (inverse \<psi>) = vec_of_list [inverse (vec_of_basis_enum \<psi> $ 0)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (inverse \<psi>) = vec_of_list [inverse (vec_of_basis_enum \<psi> $ 0)]
[PROOF STEP]
apply (rule eq_vecI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (vec_of_list [inverse (vec_of_basis_enum \<psi> $ 0)]) \<Longrightarrow> vec_of_basis_enum (inverse \<psi>) $ i = vec_of_list [inverse (vec_of_basis_enum \<psi> $ 0)] $ i
 2. dim_vec (vec_of_basis_enum (inverse \<psi>)) = dim_vec (vec_of_list [inverse (vec_of_basis_enum \<psi> $ 0)])
[PROOF STEP]
apply (auto simp: vec_of_basis_enum_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_dim_iso (inverse \<psi>) = inverse (one_dim_iso \<psi>)
[PROOF STEP]
by (metis complex_vector.scale_cancel_right one_dim_inverse one_dim_scaleC_1 zero_neq_one)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (inverse \<psi>) = vec_of_list [inverse (vec_of_basis_enum \<psi> $ 0)]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_basis_enum_divide:
  fixes \<psi> \<phi> :: "'a::one_dim"
  shows "vec_of_basis_enum (\<psi> / \<phi>)
   = vec_of_list [vec_index (vec_of_basis_enum \<psi>) 0 / vec_index (vec_of_basis_enum \<phi>) 0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (\<psi> / \<phi>) = vec_of_list [vec_of_basis_enum \<psi> $ 0 / vec_of_basis_enum \<phi> $ 0]
[PROOF STEP]
by (simp add: divide_inverse vec_of_basis_enum_to_inverse vec_of_basis_enum_times)


[STATEMENT]
lemma vec_of_basis_enum_1: "vec_of_basis_enum (1 :: 'a::one_dim) = vec_of_list [1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (1::'a) = vec_of_list [1]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec_of_basis_enum (1::'a) = vec_of_list [1]
[PROOF STEP]
have [simp]: \<open>crepresentation {1} x 1 = one_dim_iso x\<close> for x :: 'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation {1::'a} x (1::'a) = one_dim_iso x
[PROOF STEP]
apply (subst one_dim_scaleC_1[where x=x, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation {1::'a} (one_dim_iso x *\<^sub>C (1::'a)) (1::'a) = one_dim_iso x
[PROOF STEP]
apply (subst complex_vector.representation_scale)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. cindependent {1::'a}
 2. (1::'a) \<in> cspan {1::'a}
 3. one_dim_iso x * crepresentation {1::'a} (1::'a) (1::'a) = one_dim_iso x
[PROOF STEP]
by (auto simp add: complex_vector.span_base complex_vector.representation_basis)
[PROOF STATE]
proof (state)
this:
crepresentation {1::'a} ?x (1::'a) = one_dim_iso ?x

goal (1 subgoal):
 1. vec_of_basis_enum (1::'a) = vec_of_list [1]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (1::'a) = vec_of_list [1]
[PROOF STEP]
apply (rule eq_vecI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (vec_of_list [1]) \<Longrightarrow> vec_of_basis_enum (1::'a) $ i = vec_of_list [1] $ i
 2. dim_vec (vec_of_basis_enum (1::'a)) = dim_vec (vec_of_list [1])
[PROOF STEP]
by (auto simp: vec_of_basis_enum_def)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (1::'a) = vec_of_list [1]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_basis_enum_ell2_component:
  fixes \<psi> :: \<open>'a::enum ell2\<close>
  assumes [simp]: \<open>i < CARD('a)\<close>
  shows \<open>vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (Enum.enum ! i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
let ?i = \<open>Enum.enum ! i\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
have \<open>Rep_ell2 \<psi> (Enum.enum ! i) = ket ?i \<bullet>\<^sub>C \<psi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_ell2 \<psi> (enum_class.enum ! i) = ket (enum_class.enum ! i) \<bullet>\<^sub>C \<psi>
[PROOF STEP]
by (simp add: cinner_ket_left)
[PROOF STATE]
proof (state)
this:
Rep_ell2 \<psi> (enum_class.enum ! i) = ket (enum_class.enum ! i) \<bullet>\<^sub>C \<psi>

goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_ell2 \<psi> (enum_class.enum ! i) = ket (enum_class.enum ! i) \<bullet>\<^sub>C \<psi>

goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
have \<open>\<dots> = vec_of_basis_enum \<psi> \<bullet>c vec_of_basis_enum (ket ?i :: 'a ell2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket (enum_class.enum ! i) \<bullet>\<^sub>C \<psi> = vec_of_basis_enum \<psi> \<bullet>c vec_of_basis_enum (ket (enum_class.enum ! i))
[PROOF STEP]
by (rule cscalar_prod_vec_of_basis_enum[symmetric])
[PROOF STATE]
proof (state)
this:
ket (enum_class.enum ! i) \<bullet>\<^sub>C \<psi> = vec_of_basis_enum \<psi> \<bullet>c vec_of_basis_enum (ket (enum_class.enum ! i))

goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ket (enum_class.enum ! i) \<bullet>\<^sub>C \<psi> = vec_of_basis_enum \<psi> \<bullet>c vec_of_basis_enum (ket (enum_class.enum ! i))

goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
have \<open>\<dots> = vec_of_basis_enum \<psi> \<bullet>c unit_vec (CARD('a)) i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum \<psi> \<bullet>c vec_of_basis_enum (ket (enum_class.enum ! i)) = vec_of_basis_enum \<psi> \<bullet>c unit_vec CARD('a) i
[PROOF STEP]
by (simp add: vec_of_basis_enum_ket enum_idx_enum)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum \<psi> \<bullet>c vec_of_basis_enum (ket (enum_class.enum ! i)) = vec_of_basis_enum \<psi> \<bullet>c unit_vec CARD('a) i

goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum \<psi> \<bullet>c vec_of_basis_enum (ket (enum_class.enum ! i)) = vec_of_basis_enum \<psi> \<bullet>c unit_vec CARD('a) i

goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
have \<open>\<dots> = vec_of_basis_enum \<psi> \<bullet> unit_vec (CARD('a)) i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum \<psi> \<bullet>c unit_vec CARD('a) i = vec_of_basis_enum \<psi> \<bullet> unit_vec CARD('a) i
[PROOF STEP]
by (smt (verit, best) assms carrier_vecI conjugate_conjugate_sprod conjugate_id conjugate_vec_sprod_comm dim_vec_conjugate eq_vecI index_unit_vec(3) scalar_prod_left_unit vec_index_conjugate)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum \<psi> \<bullet>c unit_vec CARD('a) i = vec_of_basis_enum \<psi> \<bullet> unit_vec CARD('a) i

goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum \<psi> \<bullet>c unit_vec CARD('a) i = vec_of_basis_enum \<psi> \<bullet> unit_vec CARD('a) i

goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
have \<open>\<dots> = vec_of_basis_enum \<psi> $ i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum \<psi> \<bullet> unit_vec CARD('a) i = vec_of_basis_enum \<psi> $ i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum \<psi> \<bullet> unit_vec CARD('a) i = vec_of_basis_enum \<psi> $ i

goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Rep_ell2 \<psi> (enum_class.enum ! i) = vec_of_basis_enum \<psi> $ i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Rep_ell2 \<psi> (enum_class.enum ! i) = vec_of_basis_enum \<psi> $ i

goal (1 subgoal):
 1. vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum \<psi> $ i = Rep_ell2 \<psi> (enum_class.enum ! i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma corthogonal_vec_of_basis_enum:
  fixes S :: "'a::onb_enum list"
  shows "corthogonal (map vec_of_basis_enum S) \<longleftrightarrow> is_ortho_set (set S) \<and> distinct S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. corthogonal (map vec_of_basis_enum S) = (is_ortho_set (set S) \<and> distinct S)
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. corthogonal (map vec_of_basis_enum S) \<Longrightarrow> is_ortho_set (set S)
 2. corthogonal (map vec_of_basis_enum S) \<Longrightarrow> distinct S
 3. \<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> corthogonal (map vec_of_basis_enum S)
[PROOF STEP]
assume assm: \<open>corthogonal (map vec_of_basis_enum S)\<close>
[PROOF STATE]
proof (state)
this:
corthogonal (map vec_of_basis_enum S)

goal (3 subgoals):
 1. corthogonal (map vec_of_basis_enum S) \<Longrightarrow> is_ortho_set (set S)
 2. corthogonal (map vec_of_basis_enum S) \<Longrightarrow> distinct S
 3. \<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> corthogonal (map vec_of_basis_enum S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
corthogonal (map vec_of_basis_enum S)
[PROOF STEP]
show \<open>is_ortho_set (set S)\<close>
[PROOF STATE]
proof (prove)
using this:
corthogonal (map vec_of_basis_enum S)

goal (1 subgoal):
 1. is_ortho_set (set S)
[PROOF STEP]
by (smt (verit, ccfv_SIG) cinner_eq_zero_iff corthogonal_def cscalar_prod_vec_of_basis_enum in_set_conv_nth is_ortho_set_def length_map nth_map)
[PROOF STATE]
proof (state)
this:
is_ortho_set (set S)

goal (2 subgoals):
 1. corthogonal (map vec_of_basis_enum S) \<Longrightarrow> distinct S
 2. \<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> corthogonal (map vec_of_basis_enum S)
[PROOF STEP]
show \<open>distinct S\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct S
[PROOF STEP]
using assm corthogonal_distinct distinct_map
[PROOF STATE]
proof (prove)
using this:
corthogonal (map vec_of_basis_enum S)
corthogonal ?us \<Longrightarrow> distinct ?us
distinct (map ?f ?xs) = (distinct ?xs \<and> inj_on ?f (set ?xs))

goal (1 subgoal):
 1. distinct S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct S

goal (1 subgoal):
 1. \<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> corthogonal (map vec_of_basis_enum S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> corthogonal (map vec_of_basis_enum S)
[PROOF STEP]
assume \<open>is_ortho_set (set S)\<close> and \<open>distinct S\<close>
[PROOF STATE]
proof (state)
this:
is_ortho_set (set S)
distinct S

goal (1 subgoal):
 1. \<lbrakk>is_ortho_set (set S); distinct S\<rbrakk> \<Longrightarrow> corthogonal (map vec_of_basis_enum S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_ortho_set (set S)
distinct S
[PROOF STEP]
show \<open>corthogonal (map vec_of_basis_enum S)\<close>
[PROOF STATE]
proof (prove)
using this:
is_ortho_set (set S)
distinct S

goal (1 subgoal):
 1. corthogonal (map vec_of_basis_enum S)
[PROOF STEP]
by (smt (verit, ccfv_threshold) cinner_eq_zero_iff corthogonalI cscalar_prod_vec_of_basis_enum is_ortho_set_def length_map length_map nth_eq_iff_index_eq nth_map nth_map nth_mem nth_mem)
[PROOF STATE]
proof (state)
this:
corthogonal (map vec_of_basis_enum S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_of_cblinfun_ell2_carrier[simp]: \<open>mat_of_cblinfun (a::'a::enum ell2 \<Rightarrow>\<^sub>C\<^sub>L 'b::enum ell2) \<in> carrier_mat CARD('b) CARD('a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun a \<in> carrier_mat CARD('b) CARD('a)
[PROOF STEP]
by (simp add: mat_of_cblinfun_def)


[STATEMENT]
lemma dim_row_mat_of_cblinfun[simp]: \<open>dim_row (mat_of_cblinfun (a::'a::enum ell2 \<Rightarrow>\<^sub>C\<^sub>L 'b::enum ell2)) = CARD('b)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat_of_cblinfun a) = CARD('b)
[PROOF STEP]
by (simp add: mat_of_cblinfun_def)


[STATEMENT]
lemma dim_col_mat_of_cblinfun[simp]: \<open>dim_col (mat_of_cblinfun (a::'a::enum ell2 \<Rightarrow>\<^sub>C\<^sub>L 'b::enum ell2)) = CARD('a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (mat_of_cblinfun a) = CARD('a)
[PROOF STEP]
by (simp add: mat_of_cblinfun_def)


[STATEMENT]
lemma mat_of_cblinfun_cblinfun_apply:
  "vec_of_basis_enum (F *\<^sub>V u) = mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u"
  for F::"'a::{basis_enum,complex_normed_vector}  \<Rightarrow>\<^sub>C\<^sub>L 'b::{basis_enum,complex_normed_vector}" and u::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (F *\<^sub>V u) = mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u
[PROOF STEP]
proof (rule eq_vecI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
 2. dim_vec (vec_of_basis_enum (F *\<^sub>V u)) = dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u)
[PROOF STEP]
show \<open>dim_vec (vec_of_basis_enum (F *\<^sub>V u)) = dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_basis_enum (F *\<^sub>V u)) = dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u)
[PROOF STEP]
by (simp add: dim_vec_of_basis_enum' mat_of_cblinfun_def)
[PROOF STATE]
proof (state)
this:
dim_vec (vec_of_basis_enum (F *\<^sub>V u)) = dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
define BasisA where "BasisA = (canonical_basis::'a list)"
[PROOF STATE]
proof (state)
this:
BasisA = canonical_basis

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
define BasisB where "BasisB = (canonical_basis::'b list)"
[PROOF STATE]
proof (state)
this:
BasisB = canonical_basis

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
define nA where "nA = length (canonical_basis :: 'a list)"
[PROOF STATE]
proof (state)
this:
nA = length canonical_basis

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
define nB where "nB = length (canonical_basis :: 'b list)"
[PROOF STATE]
proof (state)
this:
nB = length canonical_basis

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
assume \<open>i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u)\<close>
[PROOF STATE]
proof (state)
this:
i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u)
[PROOF STEP]
have [simp]: \<open>i < nB\<close>
[PROOF STATE]
proof (prove)
using this:
i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u)

goal (1 subgoal):
 1. i < nB
[PROOF STEP]
by (simp add: mat_of_cblinfun_def nB_def)
[PROOF STATE]
proof (state)
this:
i < nB

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
define v where \<open>v = BasisB ! i\<close>
[PROOF STATE]
proof (state)
this:
v = BasisB ! i

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have [simp]: \<open>dim_row (mat_of_cblinfun F) = nB\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat_of_cblinfun F) = nB
[PROOF STEP]
by (simp add: mat_of_cblinfun_def nB_def)
[PROOF STATE]
proof (state)
this:
dim_row (mat_of_cblinfun F) = nB

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have [simp]: \<open>length BasisB = nB\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length BasisB = nB
[PROOF STEP]
by (simp add: nB_def BasisB_def)
[PROOF STATE]
proof (state)
this:
length BasisB = nB

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have [simp]: \<open>length BasisA = nA\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length BasisA = nA
[PROOF STEP]
using BasisA_def nA_def
[PROOF STATE]
proof (prove)
using this:
BasisA = canonical_basis
nA = length canonical_basis

goal (1 subgoal):
 1. length BasisA = nA
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length BasisA = nA

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have [simp]: \<open>cindependent (set BasisA)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindependent (set BasisA)
[PROOF STEP]
using BasisA_def is_cindependent_set
[PROOF STATE]
proof (prove)
using this:
BasisA = canonical_basis
cindependent (set canonical_basis)

goal (1 subgoal):
 1. cindependent (set BasisA)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cindependent (set BasisA)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have [simp]: \<open>cindependent (set BasisB)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindependent (set BasisB)
[PROOF STEP]
using BasisB_def is_cindependent_set
[PROOF STATE]
proof (prove)
using this:
BasisB = canonical_basis
cindependent (set canonical_basis)

goal (1 subgoal):
 1. cindependent (set BasisB)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cindependent (set BasisB)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have [simp]: \<open>cspan (set BasisB) = UNIV\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan (set BasisB) = UNIV
[PROOF STEP]
by (simp add: BasisB_def is_generator_set)
[PROOF STATE]
proof (state)
this:
cspan (set BasisB) = UNIV

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have [simp]: \<open>cspan (set BasisA) = UNIV\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan (set BasisA) = UNIV
[PROOF STEP]
by (simp add: BasisA_def is_generator_set)
[PROOF STATE]
proof (state)
this:
cspan (set BasisA) = UNIV

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have \<open>(mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i =
          (\<Sum>j = 0..<nA. row (mat_of_cblinfun F) i $ j * crepresentation (set BasisA) u (vec_of_list BasisA $ j))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i = (\<Sum>j = 0..<nA. row (mat_of_cblinfun F) i $ j * crepresentation (set BasisA) u (vec_of_list BasisA $ j))
[PROOF STEP]
by (auto simp: vec_of_basis_enum_def scalar_prod_def simp flip: BasisA_def)
[PROOF STATE]
proof (state)
this:
(mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i = (\<Sum>j = 0..<nA. row (mat_of_cblinfun F) i $ j * crepresentation (set BasisA) u (vec_of_list BasisA $ j))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i = (\<Sum>j = 0..<nA. row (mat_of_cblinfun F) i $ j * crepresentation (set BasisA) u (vec_of_list BasisA $ j))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have \<open>\<dots> = (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) v
                                 * crepresentation (set BasisA) u (BasisA ! j))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..<nA. row (mat_of_cblinfun F) i $ j * crepresentation (set BasisA) u (vec_of_list BasisA $ j)) = (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) v * crepresentation (set BasisA) u (BasisA ! j))
[PROOF STEP]
apply (rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..<nA} \<Longrightarrow> row (mat_of_cblinfun F) i $ x * crepresentation (set BasisA) u (vec_of_list BasisA $ x) = crepresentation (set BasisB) (F *\<^sub>V BasisA ! x) v * crepresentation (set BasisA) u (BasisA ! x)
[PROOF STEP]
by (auto simp: vec_of_list_index mat_of_cblinfun_def scalar_prod_def v_def simp flip: BasisA_def BasisB_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<nA. row (mat_of_cblinfun F) i $ j * crepresentation (set BasisA) u (vec_of_list BasisA $ j)) = (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) v * crepresentation (set BasisA) u (BasisA ! j))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<nA. row (mat_of_cblinfun F) i $ j * crepresentation (set BasisA) u (vec_of_list BasisA $ j)) = (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) v * crepresentation (set BasisA) u (BasisA ! j))

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have \<open>\<dots> = crepresentation (set BasisB) (F *\<^sub>V u) v\<close> (is \<open>(\<Sum>j=_..<_. ?lhs v j) = _\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) v * crepresentation (set BasisA) u (BasisA ! j)) = crepresentation (set BasisB) (F *\<^sub>V u) v
[PROOF STEP]
proof (rule complex_vector.representation_eqI[symmetric, THEN fun_cong])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. cindependent (set BasisB)
 2. F *\<^sub>V u \<in> cspan (set BasisB)
 3. \<And>b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0 \<Longrightarrow> b \<in> set BasisB
 4. finite {b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0}
 5. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
show \<open>cindependent (set BasisB)\<close> \<open>F *\<^sub>V u \<in> cspan (set BasisB)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindependent (set BasisB) &&& F *\<^sub>V u \<in> cspan (set BasisB)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
cindependent (set BasisB)
F *\<^sub>V u \<in> cspan (set BasisB)

goal (3 subgoals):
 1. \<And>b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0 \<Longrightarrow> b \<in> set BasisB
 2. finite {b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0}
 3. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
show only_basis: \<open>(\<Sum>j = 0..<nA. ?lhs b j) \<noteq> 0 \<Longrightarrow> b \<in> set BasisB\<close> for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0 \<Longrightarrow> b \<in> set BasisB
[PROOF STEP]
by (metis (mono_tags, lifting) complex_vector.representation_ne_zero mult_not_zero sum.not_neutral_contains_not_neutral)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) ?b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0 \<Longrightarrow> ?b \<in> set BasisB

goal (2 subgoals):
 1. finite {b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0}
 2. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) ?b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0 \<Longrightarrow> ?b \<in> set BasisB
[PROOF STEP]
show \<open>finite {b. (\<Sum>j = 0..<nA. ?lhs b j) \<noteq> 0}\<close>
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) ?b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0 \<Longrightarrow> ?b \<in> set BasisB

goal (1 subgoal):
 1. finite {b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0}
[PROOF STEP]
by (smt (z3) List.finite_set finite_subset mem_Collect_eq subsetI)
[PROOF STATE]
proof (state)
this:
finite {b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0}

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
have \<open>(\<Sum>b | (\<Sum>j = 0..<nA. ?lhs b j) \<noteq> 0. (\<Sum>j = 0..<nA. ?lhs b j) *\<^sub>C b) =
            (\<Sum>b\<in>set BasisB. (\<Sum>j = 0..<nA. ?lhs b j) *\<^sub>C b)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = (\<Sum>b\<in>set BasisB. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b)
[PROOF STEP]
apply (rule sum.mono_neutral_left)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite (set BasisB)
 2. {b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0} \<subseteq> set BasisB
 3. \<forall>i\<in>set BasisB - {b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0}. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) i * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C i = (0::'b)
[PROOF STEP]
using only_basis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) ?b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0 \<Longrightarrow> ?b \<in> set BasisB

goal (3 subgoals):
 1. finite (set BasisB)
 2. {b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0} \<subseteq> set BasisB
 3. \<forall>i\<in>set BasisB - {b. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0}. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) i * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C i = (0::'b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = (\<Sum>b\<in>set BasisB. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b)

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = (\<Sum>b\<in>set BasisB. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b)

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
have \<open>\<dots> = (\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>b\<in>set BasisB. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = (\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b)
[PROOF STEP]
apply (subst sum.reindex_bij_betw[where h=\<open>nth BasisA\<close> and T=\<open>set BasisA\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. bij_betw ((!) BasisA) {0..<nA} (set BasisA)
 2. (\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b) = (\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b)
[PROOF STEP]
apply (metis BasisA_def \<open>length BasisA = nA\<close> atLeast0LessThan bij_betw_nth distinct_canonical_basis)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b) = (\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>b\<in>set BasisB. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = (\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b)

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>b\<in>set BasisB. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = (\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b)

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
have \<open>\<dots> = (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (\<Sum>b\<in>set BasisB. crepresentation (set BasisB) (F *\<^sub>V a) b *\<^sub>C b))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b) = (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (\<Sum>b\<in>set BasisB. crepresentation (set BasisB) (F *\<^sub>V a) b *\<^sub>C b))
[PROOF STEP]
apply (simp add: scaleC_sum_left scaleC_sum_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>b\<in>set BasisB. \<Sum>a\<in>set BasisA. (crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b) = (\<Sum>a\<in>set BasisA. \<Sum>x\<in>set BasisB. (crepresentation (set BasisA) u a * crepresentation (set BasisB) (F *\<^sub>V a) x) *\<^sub>C x)
[PROOF STEP]
apply (subst sum.swap)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>set BasisA. \<Sum>i\<in>set BasisB. (crepresentation (set BasisB) (F *\<^sub>V j) i * crepresentation (set BasisA) u j) *\<^sub>C i) = (\<Sum>a\<in>set BasisA. \<Sum>x\<in>set BasisB. (crepresentation (set BasisA) u a * crepresentation (set BasisB) (F *\<^sub>V a) x) *\<^sub>C x)
[PROOF STEP]
by (metis (no_types, lifting) mult.commute sum.cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b) = (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (\<Sum>b\<in>set BasisB. crepresentation (set BasisB) (F *\<^sub>V a) b *\<^sub>C b))

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>b\<in>set BasisB. (\<Sum>a\<in>set BasisA. crepresentation (set BasisB) (F *\<^sub>V a) b * crepresentation (set BasisA) u a) *\<^sub>C b) = (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (\<Sum>b\<in>set BasisB. crepresentation (set BasisB) (F *\<^sub>V a) b *\<^sub>C b))

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
have \<open>\<dots> = (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (F *\<^sub>V a))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (\<Sum>b\<in>set BasisB. crepresentation (set BasisB) (F *\<^sub>V a) b *\<^sub>C b)) = (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (F *\<^sub>V a))
[PROOF STEP]
apply (subst complex_vector.sum_representation_eq)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a. cindependent (set BasisB)
 2. \<And>a. F *\<^sub>V a \<in> cspan (set BasisB)
 3. \<And>a. finite (set BasisB)
 4. \<And>a. set BasisB \<subseteq> set BasisB
 5. (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (F *\<^sub>V a)) = (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (F *\<^sub>V a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (\<Sum>b\<in>set BasisB. crepresentation (set BasisB) (F *\<^sub>V a) b *\<^sub>C b)) = (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (F *\<^sub>V a))

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (\<Sum>b\<in>set BasisB. crepresentation (set BasisB) (F *\<^sub>V a) b *\<^sub>C b)) = (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (F *\<^sub>V a))

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
have \<open>\<dots> = F *\<^sub>V (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (F *\<^sub>V a)) = F *\<^sub>V (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C a)
[PROOF STEP]
by (simp flip: cblinfun.scaleC_right cblinfun.sum_right)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (F *\<^sub>V a)) = F *\<^sub>V (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C a)

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C (F *\<^sub>V a)) = F *\<^sub>V (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C a)

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
have \<open>\<dots> = F *\<^sub>V u\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F *\<^sub>V (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C a) = F *\<^sub>V u
[PROOF STEP]
apply (subst complex_vector.sum_representation_eq)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. cindependent (set BasisA)
 2. u \<in> cspan (set BasisA)
 3. finite (set BasisA)
 4. set BasisA \<subseteq> set BasisA
 5. F *\<^sub>V u = F *\<^sub>V u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F *\<^sub>V (\<Sum>a\<in>set BasisA. crepresentation (set BasisA) u a *\<^sub>C a) = F *\<^sub>V u

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
show \<open>(\<Sum>b | (\<Sum>j = 0..<nA. ?lhs b j) \<noteq> 0. (\<Sum>j = 0..<nA. ?lhs b j) *\<^sub>C b) = F *\<^sub>V u\<close>
[PROOF STATE]
proof (prove)
using this:
(\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u

goal (1 subgoal):
 1. (\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>b | (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) \<noteq> 0. (\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) b * crepresentation (set BasisA) u (BasisA ! j)) *\<^sub>C b) = F *\<^sub>V u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) v * crepresentation (set BasisA) u (BasisA ! j)) = crepresentation (set BasisB) (F *\<^sub>V u) v

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<nA. crepresentation (set BasisB) (F *\<^sub>V BasisA ! j) v * crepresentation (set BasisA) u (BasisA ! j)) = crepresentation (set BasisB) (F *\<^sub>V u) v

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
have \<open>crepresentation (set BasisB) (F *\<^sub>V u) v = vec_of_basis_enum (F *\<^sub>V u) $ i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation (set BasisB) (F *\<^sub>V u) v = vec_of_basis_enum (F *\<^sub>V u) $ i
[PROOF STEP]
by (auto simp: vec_of_list_index vec_of_basis_enum_def v_def simp flip: BasisB_def)
[PROOF STATE]
proof (state)
this:
crepresentation (set BasisB) (F *\<^sub>V u) v = vec_of_basis_enum (F *\<^sub>V u) $ i

goal (1 subgoal):
 1. \<And>i. i < dim_vec (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) \<Longrightarrow> vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i = vec_of_basis_enum (F *\<^sub>V u) $ i
[PROOF STEP]
show \<open>vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i\<close>
[PROOF STATE]
proof (prove)
using this:
(mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i = vec_of_basis_enum (F *\<^sub>V u) $ i

goal (1 subgoal):
 1. vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (F *\<^sub>V u) $ i = (mat_of_cblinfun F *\<^sub>v vec_of_basis_enum u) $ i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_enum_of_vec_cblinfun_apply:
  fixes M :: "complex mat"
  defines "nA \<equiv> length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB \<equiv> length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
  assumes "M \<in> carrier_mat nB nA" and "dim_vec x = nA"
  shows "basis_enum_of_vec (M *\<^sub>v x) = (cblinfun_of_mat M :: 'a \<Rightarrow>\<^sub>C\<^sub>L 'b) *\<^sub>V basis_enum_of_vec x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec (M *\<^sub>v x) = cblinfun_of_mat M *\<^sub>V basis_enum_of_vec x
[PROOF STEP]
by (metis assms basis_enum_of_vec_inverse cblinfun_of_mat.rep_eq)


[STATEMENT]
lemma mat_of_cblinfun_inverse:
  "cblinfun_of_mat (mat_of_cblinfun B) = B"
  for B::"'a::{basis_enum,complex_normed_vector}  \<Rightarrow>\<^sub>C\<^sub>L 'b::{basis_enum,complex_normed_vector}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat (mat_of_cblinfun B) = B
[PROOF STEP]
proof (rule cblinfun_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V i = B *\<^sub>V i
[PROOF STEP]
fix x :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V i = B *\<^sub>V i
[PROOF STEP]
define y where \<open>y = vec_of_basis_enum x\<close>
[PROOF STATE]
proof (state)
this:
y = vec_of_basis_enum x

goal (1 subgoal):
 1. \<And>i. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V i = B *\<^sub>V i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = vec_of_basis_enum x
[PROOF STEP]
have \<open>cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V x = ((cblinfun_of_mat (mat_of_cblinfun B) :: 'a\<Rightarrow>\<^sub>C\<^sub>L'b) *\<^sub>V basis_enum_of_vec y)\<close>
[PROOF STATE]
proof (prove)
using this:
y = vec_of_basis_enum x

goal (1 subgoal):
 1. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V x = cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V basis_enum_of_vec y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V x = cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V basis_enum_of_vec y

goal (1 subgoal):
 1. \<And>i. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V i = B *\<^sub>V i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V x = cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V basis_enum_of_vec y

goal (1 subgoal):
 1. \<And>i. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V i = B *\<^sub>V i
[PROOF STEP]
have \<open>\<dots> = basis_enum_of_vec (mat_of_cblinfun B *\<^sub>v vec_of_basis_enum (basis_enum_of_vec y :: 'a))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V basis_enum_of_vec y = basis_enum_of_vec (mat_of_cblinfun B *\<^sub>v vec_of_basis_enum (basis_enum_of_vec y))
[PROOF STEP]
apply (transfer fixing: B)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. (if mat_of_cblinfun B \<in> carrier_mat (length canonical_basis) (length canonical_basis) then basis_enum_of_vec (mat_of_cblinfun B *\<^sub>v vec_of_basis_enum (basis_enum_of_vec y)) else (0::'b)) = basis_enum_of_vec (mat_of_cblinfun B *\<^sub>v vec_of_basis_enum (basis_enum_of_vec y))
[PROOF STEP]
by (simp add: mat_of_cblinfun_def)
[PROOF STATE]
proof (state)
this:
cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V basis_enum_of_vec y = basis_enum_of_vec (mat_of_cblinfun B *\<^sub>v vec_of_basis_enum (basis_enum_of_vec y))

goal (1 subgoal):
 1. \<And>i. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V i = B *\<^sub>V i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V basis_enum_of_vec y = basis_enum_of_vec (mat_of_cblinfun B *\<^sub>v vec_of_basis_enum (basis_enum_of_vec y))

goal (1 subgoal):
 1. \<And>i. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V i = B *\<^sub>V i
[PROOF STEP]
have \<open>\<dots> = basis_enum_of_vec (vec_of_basis_enum (B *\<^sub>V x))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec (mat_of_cblinfun B *\<^sub>v vec_of_basis_enum (basis_enum_of_vec y)) = basis_enum_of_vec (vec_of_basis_enum (B *\<^sub>V x))
[PROOF STEP]
by (simp add: mat_of_cblinfun_cblinfun_apply y_def)
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (mat_of_cblinfun B *\<^sub>v vec_of_basis_enum (basis_enum_of_vec y)) = basis_enum_of_vec (vec_of_basis_enum (B *\<^sub>V x))

goal (1 subgoal):
 1. \<And>i. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V i = B *\<^sub>V i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (mat_of_cblinfun B *\<^sub>v vec_of_basis_enum (basis_enum_of_vec y)) = basis_enum_of_vec (vec_of_basis_enum (B *\<^sub>V x))

goal (1 subgoal):
 1. \<And>i. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V i = B *\<^sub>V i
[PROOF STEP]
have \<open>\<dots> = B *\<^sub>V x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec (vec_of_basis_enum (B *\<^sub>V x)) = B *\<^sub>V x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (vec_of_basis_enum (B *\<^sub>V x)) = B *\<^sub>V x

goal (1 subgoal):
 1. \<And>i. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V i = B *\<^sub>V i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V x = B *\<^sub>V x
[PROOF STEP]
show \<open>cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V x = B *\<^sub>V x\<close>
[PROOF STATE]
proof (prove)
using this:
cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V x = B *\<^sub>V x

goal (1 subgoal):
 1. cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V x = B *\<^sub>V x
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
cblinfun_of_mat (mat_of_cblinfun B) *\<^sub>V x = B *\<^sub>V x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_of_cblinfun_inj: "inj mat_of_cblinfun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj mat_of_cblinfun
[PROOF STEP]
by (metis inj_on_def mat_of_cblinfun_inverse)


[STATEMENT]
lemma cblinfun_of_mat_inverse:
  fixes M::"complex mat"
  defines "nA \<equiv> length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB \<equiv> length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
  assumes "M \<in> carrier_mat nB nA"
  shows "mat_of_cblinfun (cblinfun_of_mat M :: 'a \<Rightarrow>\<^sub>C\<^sub>L 'b) = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (cblinfun_of_mat M) = M
[PROOF STEP]
by (smt (verit) assms(3) basis_enum_of_vec_inverse carrier_matD(1) carrier_vecD cblinfun_of_mat.rep_eq dim_mult_mat_vec eq_mat_on_vecI mat_carrier mat_of_cblinfun_def mat_of_cblinfun_cblinfun_apply nA_def nB_def)


[STATEMENT]
lemma cblinfun_of_mat_inj: "inj_on (cblinfun_of_mat::complex mat \<Rightarrow> 'a \<Rightarrow>\<^sub>C\<^sub>L 'b)
      (carrier_mat (length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list))
                   (length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on cblinfun_of_mat (carrier_mat (length canonical_basis) (length canonical_basis))
[PROOF STEP]
using cblinfun_of_mat_inverse
[PROOF STATE]
proof (prove)
using this:
?M \<in> carrier_mat (length canonical_basis) (length canonical_basis) \<Longrightarrow> mat_of_cblinfun (cblinfun_of_mat ?M) = ?M

goal (1 subgoal):
 1. inj_on cblinfun_of_mat (carrier_mat (length canonical_basis) (length canonical_basis))
[PROOF STEP]
by (metis inj_onI)


[STATEMENT]
lemma cblinfun_eq_mat_of_cblinfunI:
  assumes "mat_of_cblinfun a = mat_of_cblinfun b"
  shows "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (metis assms mat_of_cblinfun_inverse)


[STATEMENT]
lemma cblinfun_of_mat_plus:
  defines "nA \<equiv> length (canonical_basis :: 'a::{basis_enum,complex_normed_vector} list)"
    and "nB \<equiv> length (canonical_basis :: 'b::{basis_enum,complex_normed_vector} list)"
  assumes [simp,intro]: "M \<in> carrier_mat nB nA" and [simp,intro]: "N \<in> carrier_mat nB nA"
  shows "(cblinfun_of_mat (M + N) :: 'a \<Rightarrow>\<^sub>C\<^sub>L 'b) = ((cblinfun_of_mat M + cblinfun_of_mat N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat (M + N) = cblinfun_of_mat M + cblinfun_of_mat N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cblinfun_of_mat (M + N) = cblinfun_of_mat M + cblinfun_of_mat N
[PROOF STEP]
have [simp]: \<open>vec_of_basis_enum (v :: 'a) \<in> carrier_vec nA\<close> for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum v \<in> carrier_vec nA
[PROOF STEP]
by (auto simp add: carrier_dim_vec dim_vec_of_basis_enum' nA_def)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum ?v \<in> carrier_vec nA

goal (1 subgoal):
 1. cblinfun_of_mat (M + N) = cblinfun_of_mat M + cblinfun_of_mat N
[PROOF STEP]
have [simp]: \<open>dim_row M = nB\<close> \<open>dim_row N = nB\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row M = nB &&& dim_row N = nB
[PROOF STEP]
using carrier_matD(1)
[PROOF STATE]
proof (prove)
using this:
?A \<in> carrier_mat ?nr ?nc \<Longrightarrow> dim_row ?A = ?nr

goal (1 subgoal):
 1. dim_row M = nB &&& dim_row N = nB
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row M = nB
dim_row N = nB

goal (1 subgoal):
 1. cblinfun_of_mat (M + N) = cblinfun_of_mat M + cblinfun_of_mat N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_of_mat (M + N) = cblinfun_of_mat M + cblinfun_of_mat N
[PROOF STEP]
apply (transfer fixing: M N)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. if M + N \<in> carrier_mat (length canonical_basis) (length canonical_basis) then basis_enum_of_vec ((M + N) *\<^sub>v vec_of_basis_enum v) else (0::'b)) = (\<lambda>x. (if M \<in> carrier_mat (length canonical_basis) (length canonical_basis) then basis_enum_of_vec (M *\<^sub>v vec_of_basis_enum x) else (0::'b)) + (if N \<in> carrier_mat (length canonical_basis) (length canonical_basis) then basis_enum_of_vec (N *\<^sub>v vec_of_basis_enum x) else (0::'b)))
[PROOF STEP]
by (auto intro!: ext simp add: add_mult_distrib_mat_vec nA_def[symmetric] nB_def[symmetric]
        add_mult_distrib_mat_vec[where nr=nB and nc=nA] basis_enum_of_vec_add)
[PROOF STATE]
proof (state)
this:
cblinfun_of_mat (M + N) = cblinfun_of_mat M + cblinfun_of_mat N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_of_cblinfun_zero:
  "mat_of_cblinfun (0 :: ('a::{basis_enum,complex_normed_vector}  \<Rightarrow>\<^sub>C\<^sub>L 'b::{basis_enum,complex_normed_vector}))
  = 0\<^sub>m (length (canonical_basis :: 'b list)) (length (canonical_basis :: 'a list))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun 0 = 0\<^sub>m (length canonical_basis) (length canonical_basis)
[PROOF STEP]
unfolding mat_of_cblinfun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (length canonical_basis) (length canonical_basis) (\<lambda>(i, j). crepresentation (set canonical_basis) (0 *\<^sub>V canonical_basis ! j) (canonical_basis ! i)) = 0\<^sub>m (length canonical_basis) (length canonical_basis)
[PROOF STEP]
by (auto simp: complex_vector.representation_zero)


[STATEMENT]
lemma mat_of_cblinfun_plus:
  "mat_of_cblinfun (F + G) = mat_of_cblinfun F + mat_of_cblinfun G"
  for F G::"'a::{basis_enum,complex_normed_vector} \<Rightarrow>\<^sub>C\<^sub>L'b::{basis_enum,complex_normed_vector}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (F + G) = mat_of_cblinfun F + mat_of_cblinfun G
[PROOF STEP]
by (auto simp add: mat_of_cblinfun_def cblinfun.add_left complex_vector.representation_add)


[STATEMENT]
lemma mat_of_cblinfun_id:
  "mat_of_cblinfun (id_cblinfun :: ('a::{basis_enum,complex_normed_vector} \<Rightarrow>\<^sub>C\<^sub>L'a)) = 1\<^sub>m (length (canonical_basis :: 'a list))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun id_cblinfun = 1\<^sub>m (length canonical_basis)
[PROOF STEP]
apply (rule eq_matI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (length canonical_basis)); j < dim_col (1\<^sub>m (length canonical_basis))\<rbrakk> \<Longrightarrow> mat_of_cblinfun id_cblinfun $$ (i, j) = 1\<^sub>m (length canonical_basis) $$ (i, j)
 2. dim_row (mat_of_cblinfun id_cblinfun) = dim_row (1\<^sub>m (length canonical_basis))
 3. dim_col (mat_of_cblinfun id_cblinfun) = dim_col (1\<^sub>m (length canonical_basis))
[PROOF STEP]
by (auto simp: mat_of_cblinfun_def complex_vector.representation_basis is_cindependent_set nth_eq_iff_index_eq)


[STATEMENT]
lemma mat_of_cblinfun_1:
  "mat_of_cblinfun (1 :: ('a::one_dim \<Rightarrow>\<^sub>C\<^sub>L'b::one_dim)) = 1\<^sub>m 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun 1 = 1\<^sub>m 1
[PROOF STEP]
apply (rule eq_matI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m 1); j < dim_col (1\<^sub>m 1)\<rbrakk> \<Longrightarrow> mat_of_cblinfun 1 $$ (i, j) = 1\<^sub>m 1 $$ (i, j)
 2. dim_row (mat_of_cblinfun 1) = dim_row (1\<^sub>m 1)
 3. dim_col (mat_of_cblinfun 1) = dim_col (1\<^sub>m 1)
[PROOF STEP]
by (auto simp: mat_of_cblinfun_def complex_vector.representation_basis nth_eq_iff_index_eq)