[STATEMENT]
lemma statement52_existence:
  fixes a :: "proj2^3" and a3 :: "proj2"
  assumes "proj2_no_3_Col (insert a3 (range (($) a)))"
  shows "\<exists> A. apply_cltn2 (proj2_abs (vector [1,1,1])) A = a3 \<and>
  (\<forall> j. apply_cltn2 (proj2_abs (axis j 1)) A = a$j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
let ?v = "proj2_rep a3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
let ?B = "proj2_rep ` range (($) a)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
from \<open>proj2_no_3_Col (insert a3 (range (($) a)))\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_no_3_Col (insert a3 (range (($) a)))
[PROOF STEP]
have "card (insert a3 (range (($) a))) = 4"
[PROOF STATE]
proof (prove)
using this:
proj2_no_3_Col (insert a3 (range (($) a)))

goal (1 subgoal):
 1. card (insert a3 (range (($) a))) = 4
[PROOF STEP]
unfolding proj2_no_3_Col_def
[PROOF STATE]
proof (prove)
using this:
card (insert a3 (range (($) a))) = 4 \<and> (\<forall>p\<in>insert a3 (range (($) a)). \<not> proj2_set_Col (insert a3 (range (($) a)) - {p}))

goal (1 subgoal):
 1. card (insert a3 (range (($) a))) = 4
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
card (insert a3 (range (($) a))) = 4

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
from card_image_le [of UNIV "($) a"]
[PROOF STATE]
proof (chain)
picking this:
finite UNIV \<Longrightarrow> card (range (($) a)) \<le> CARD(3)
[PROOF STEP]
have "card (range (($) a)) \<le> 3"
[PROOF STATE]
proof (prove)
using this:
finite UNIV \<Longrightarrow> card (range (($) a)) \<le> CARD(3)

goal (1 subgoal):
 1. card (range (($) a)) \<le> 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (range (($) a)) \<le> 3

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with card_insert_if [of "range (($) a)" a3]
    and \<open>card (insert a3 (range (($) a))) = 4\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (range (($) a)) \<Longrightarrow> card (insert a3 (range (($) a))) = (if a3 \<in> range (($) a) then card (range (($) a)) else Suc (card (range (($) a))))
card (insert a3 (range (($) a))) = 4
card (range (($) a)) \<le> 3
[PROOF STEP]
have "a3 \<notin> range (($) a)"
[PROOF STATE]
proof (prove)
using this:
finite (range (($) a)) \<Longrightarrow> card (insert a3 (range (($) a))) = (if a3 \<in> range (($) a) then card (range (($) a)) else Suc (card (range (($) a))))
card (insert a3 (range (($) a))) = 4
card (range (($) a)) \<le> 3

goal (1 subgoal):
 1. a3 \<notin> range (($) a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a3 \<notin> range (($) a)

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
hence "(insert a3 (range (($) a))) - {a3} = range (($) a)"
[PROOF STATE]
proof (prove)
using this:
a3 \<notin> range (($) a)

goal (1 subgoal):
 1. insert a3 (range (($) a)) - {a3} = range (($) a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert a3 (range (($) a)) - {a3} = range (($) a)

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with \<open>proj2_no_3_Col (insert a3 (range (($) a)))\<close>
    and proj2_no_3_Col_span [of "insert a3 (range (($) a))" a3]
[PROOF STATE]
proof (chain)
picking this:
proj2_no_3_Col (insert a3 (range (($) a)))
\<lbrakk>proj2_no_3_Col (insert a3 (range (($) a))); a3 \<in> insert a3 (range (($) a))\<rbrakk> \<Longrightarrow> span (proj2_rep ` (insert a3 (range (($) a)) - {a3})) = UNIV
insert a3 (range (($) a)) - {a3} = range (($) a)
[PROOF STEP]
have "span ?B = UNIV"
[PROOF STATE]
proof (prove)
using this:
proj2_no_3_Col (insert a3 (range (($) a)))
\<lbrakk>proj2_no_3_Col (insert a3 (range (($) a))); a3 \<in> insert a3 (range (($) a))\<rbrakk> \<Longrightarrow> span (proj2_rep ` (insert a3 (range (($) a)) - {a3})) = UNIV
insert a3 (range (($) a)) - {a3} = range (($) a)

goal (1 subgoal):
 1. span (proj2_rep ` range (($) a)) = UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
span (proj2_rep ` range (($) a)) = UNIV

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
from card_suc_ge_insert [of a3 "range (($) a)"]
    and \<open>card (insert a3 (range (($) a))) = 4\<close>
    and \<open>card (range (($) a)) \<le> 3\<close>
[PROOF STATE]
proof (chain)
picking this:
card (insert a3 (range (($) a))) \<le> card (range (($) a)) + 1
card (insert a3 (range (($) a))) = 4
card (range (($) a)) \<le> 3
[PROOF STEP]
have "card (range (($) a)) = 3"
[PROOF STATE]
proof (prove)
using this:
card (insert a3 (range (($) a))) \<le> card (range (($) a)) + 1
card (insert a3 (range (($) a))) = 4
card (range (($) a)) \<le> 3

goal (1 subgoal):
 1. card (range (($) a)) = 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (range (($) a)) = 3

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with card_image [of proj2_rep "range (($) a)"]
    and proj2_rep_inj
    and subset_inj_on
[PROOF STATE]
proof (chain)
picking this:
inj_on proj2_rep (range (($) a)) \<Longrightarrow> card (proj2_rep ` range (($) a)) = card (range (($) a))
inj proj2_rep
\<lbrakk>inj_on ?f ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> inj_on ?f ?A
card (range (($) a)) = 3
[PROOF STEP]
have "card ?B = 3"
[PROOF STATE]
proof (prove)
using this:
inj_on proj2_rep (range (($) a)) \<Longrightarrow> card (proj2_rep ` range (($) a)) = card (range (($) a))
inj proj2_rep
\<lbrakk>inj_on ?f ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> inj_on ?f ?A
card (range (($) a)) = 3

goal (1 subgoal):
 1. card (proj2_rep ` range (($) a)) = 3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (proj2_rep ` range (($) a)) = 3

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
hence "finite ?B"
[PROOF STATE]
proof (prove)
using this:
card (proj2_rep ` range (($) a)) = 3

goal (1 subgoal):
 1. finite (proj2_rep ` range (($) a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (proj2_rep ` range (($) a))

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with \<open>span ?B = UNIV\<close> and span_finite [of ?B]
[PROOF STATE]
proof (chain)
picking this:
span (proj2_rep ` range (($) a)) = UNIV
finite (proj2_rep ` range (($) a)) \<Longrightarrow> span (proj2_rep ` range (($) a)) = range (\<lambda>u. \<Sum>v\<in>proj2_rep ` range (($) a). u v *\<^sub>R v)
finite (proj2_rep ` range (($) a))
[PROOF STEP]
obtain c where "(\<Sum> w \<in> ?B. (c w) *\<^sub>R w) = ?v"
[PROOF STATE]
proof (prove)
using this:
span (proj2_rep ` range (($) a)) = UNIV
finite (proj2_rep ` range (($) a)) \<Longrightarrow> span (proj2_rep ` range (($) a)) = range (\<lambda>u. \<Sum>v\<in>proj2_rep ` range (($) a). u v *\<^sub>R v)
finite (proj2_rep ` range (($) a))

goal (1 subgoal):
 1. (\<And>c. (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) = proj2_rep a3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: scalar_equiv) (metis (no_types, lifting) UNIV_I rangeE)
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) = proj2_rep a3

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
let ?C = "\<chi> i. c (proj2_rep (a$i)) *\<^sub>R (proj2_rep (a$i))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
let ?A = "cltn2_abs ?C"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
from proj2_rep_inj and \<open>a3 \<notin> range (($) a)\<close>
[PROOF STATE]
proof (chain)
picking this:
inj proj2_rep
a3 \<notin> range (($) a)
[PROOF STEP]
have "?v \<notin> ?B"
[PROOF STATE]
proof (prove)
using this:
inj proj2_rep
a3 \<notin> range (($) a)

goal (1 subgoal):
 1. proj2_rep a3 \<notin> proj2_rep ` range (($) a)
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. proj2_rep x = proj2_rep y \<longrightarrow> x = y
a3 \<notin> range (($) a)

goal (1 subgoal):
 1. proj2_rep a3 \<notin> proj2_rep ` range (($) a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_rep a3 \<notin> proj2_rep ` range (($) a)

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
have "\<forall> i. c (proj2_rep (a$i)) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
let ?Bi = "proj2_rep ` (range (($) a) - {a$i})"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
have "a$i \<in> insert a3 (range (($) a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a $ i \<in> insert a3 (range (($) a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a $ i \<in> insert a3 (range (($) a))

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
have "proj2_rep (a$i) \<in> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep (a $ i) \<in> proj2_rep ` range (($) a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_rep (a $ i) \<in> proj2_rep ` range (($) a)

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
from image_set_diff [of proj2_rep] and proj2_rep_inj
[PROOF STATE]
proof (chain)
picking this:
inj proj2_rep \<Longrightarrow> proj2_rep ` (?A - ?B) = proj2_rep ` ?A - proj2_rep ` ?B
inj proj2_rep
[PROOF STEP]
have "?Bi = ?B - {proj2_rep (a$i)}"
[PROOF STATE]
proof (prove)
using this:
inj proj2_rep \<Longrightarrow> proj2_rep ` (?A - ?B) = proj2_rep ` ?A - proj2_rep ` ?B
inj proj2_rep

goal (1 subgoal):
 1. proj2_rep ` (range (($) a) - {a $ i}) = proj2_rep ` range (($) a) - {proj2_rep (a $ i)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep ` (range (($) a) - {a $ i}) = proj2_rep ` range (($) a) - {proj2_rep (a $ i)}

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
with sum_diff1 [of ?B "\<lambda> w. (c w) *\<^sub>R w"]
      and \<open>finite ?B\<close>
      and \<open>proj2_rep (a$i) \<in> ?B\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (proj2_rep ` range (($) a)) \<Longrightarrow> (\<Sum>w\<in>proj2_rep ` range (($) a) - {?a}. c w *\<^sub>R w) = (if ?a \<in> proj2_rep ` range (($) a) then (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) - c ?a *\<^sub>R ?a else \<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w)
finite (proj2_rep ` range (($) a))
proj2_rep (a $ i) \<in> proj2_rep ` range (($) a)
proj2_rep ` (range (($) a) - {a $ i}) = proj2_rep ` range (($) a) - {proj2_rep (a $ i)}
[PROOF STEP]
have "(\<Sum> w \<in> ?Bi. (c w) *\<^sub>R w) =
      (\<Sum> w \<in> ?B. (c w) *\<^sub>R w) - c (proj2_rep (a$i)) *\<^sub>R proj2_rep (a$i)"
[PROOF STATE]
proof (prove)
using this:
finite (proj2_rep ` range (($) a)) \<Longrightarrow> (\<Sum>w\<in>proj2_rep ` range (($) a) - {?a}. c w *\<^sub>R w) = (if ?a \<in> proj2_rep ` range (($) a) then (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) - c ?a *\<^sub>R ?a else \<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w)
finite (proj2_rep ` range (($) a))
proj2_rep (a $ i) \<in> proj2_rep ` range (($) a)
proj2_rep ` (range (($) a) - {a $ i}) = proj2_rep ` range (($) a) - {proj2_rep (a $ i)}

goal (1 subgoal):
 1. (\<Sum>w\<in>proj2_rep ` (range (($) a) - {a $ i}). c w *\<^sub>R w) = (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) - c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>proj2_rep ` (range (($) a) - {a $ i}). c w *\<^sub>R w) = (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) - c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
from \<open>a3 \<notin> range (($) a)\<close>
[PROOF STATE]
proof (chain)
picking this:
a3 \<notin> range (($) a)
[PROOF STEP]
have "a3 \<noteq> a$i"
[PROOF STATE]
proof (prove)
using this:
a3 \<notin> range (($) a)

goal (1 subgoal):
 1. a3 \<noteq> a $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a3 \<noteq> a $ i

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
hence "insert a3 (range (($) a)) - {a$i} =
      insert a3 (range (($) a) - {a$i})"
[PROOF STATE]
proof (prove)
using this:
a3 \<noteq> a $ i

goal (1 subgoal):
 1. insert a3 (range (($) a)) - {a $ i} = insert a3 (range (($) a) - {a $ i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert a3 (range (($) a)) - {a $ i} = insert a3 (range (($) a) - {a $ i})

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
hence "proj2_rep ` (insert a3 (range (($) a)) - {a$i}) = insert ?v ?Bi"
[PROOF STATE]
proof (prove)
using this:
insert a3 (range (($) a)) - {a $ i} = insert a3 (range (($) a) - {a $ i})

goal (1 subgoal):
 1. proj2_rep ` (insert a3 (range (($) a)) - {a $ i}) = insert (proj2_rep a3) (proj2_rep ` (range (($) a) - {a $ i}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep ` (insert a3 (range (($) a)) - {a $ i}) = insert (proj2_rep a3) (proj2_rep ` (range (($) a) - {a $ i}))

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
proj2_rep ` (insert a3 (range (($) a)) - {a $ i}) = insert (proj2_rep a3) (proj2_rep ` (range (($) a) - {a $ i}))

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
from \<open>proj2_no_3_Col (insert a3 (range (($) a)))\<close>
      and \<open>a$i \<in> insert a3 (range (($) a))\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_no_3_Col (insert a3 (range (($) a)))
a $ i \<in> insert a3 (range (($) a))
[PROOF STEP]
have "span (proj2_rep ` (insert a3 (range (($) a)) - {a$i})) = UNIV"
[PROOF STATE]
proof (prove)
using this:
proj2_no_3_Col (insert a3 (range (($) a)))
a $ i \<in> insert a3 (range (($) a))

goal (1 subgoal):
 1. span (proj2_rep ` (insert a3 (range (($) a)) - {a $ i})) = UNIV
[PROOF STEP]
by (rule proj2_no_3_Col_span)
[PROOF STATE]
proof (state)
this:
span (proj2_rep ` (insert a3 (range (($) a)) - {a $ i})) = UNIV

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
proj2_rep ` (insert a3 (range (($) a)) - {a $ i}) = insert (proj2_rep a3) (proj2_rep ` (range (($) a) - {a $ i}))
span (proj2_rep ` (insert a3 (range (($) a)) - {a $ i})) = UNIV
[PROOF STEP]
have "span (insert ?v ?Bi) = UNIV"
[PROOF STATE]
proof (prove)
using this:
proj2_rep ` (insert a3 (range (($) a)) - {a $ i}) = insert (proj2_rep a3) (proj2_rep ` (range (($) a) - {a $ i}))
span (proj2_rep ` (insert a3 (range (($) a)) - {a $ i})) = UNIV

goal (1 subgoal):
 1. span (insert (proj2_rep a3) (proj2_rep ` (range (($) a) - {a $ i}))) = UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
span (insert (proj2_rep a3) (proj2_rep ` (range (($) a) - {a $ i}))) = UNIV

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
from \<open>?Bi = ?B - {proj2_rep (a$i)}\<close>
      and \<open>proj2_rep (a$i) \<in> ?B\<close>
      and \<open>card ?B = 3\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_rep ` (range (($) a) - {a $ i}) = proj2_rep ` range (($) a) - {proj2_rep (a $ i)}
proj2_rep (a $ i) \<in> proj2_rep ` range (($) a)
card (proj2_rep ` range (($) a)) = 3
[PROOF STEP]
have "card ?Bi = 2"
[PROOF STATE]
proof (prove)
using this:
proj2_rep ` (range (($) a) - {a $ i}) = proj2_rep ` range (($) a) - {proj2_rep (a $ i)}
proj2_rep (a $ i) \<in> proj2_rep ` range (($) a)
card (proj2_rep ` range (($) a)) = 3

goal (1 subgoal):
 1. card (proj2_rep ` (range (($) a) - {a $ i})) = 2
[PROOF STEP]
by (simp add: card_gt_0_diff_singleton)
[PROOF STATE]
proof (state)
this:
card (proj2_rep ` (range (($) a) - {a $ i})) = 2

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
hence "finite ?Bi"
[PROOF STATE]
proof (prove)
using this:
card (proj2_rep ` (range (($) a) - {a $ i})) = 2

goal (1 subgoal):
 1. finite (proj2_rep ` (range (($) a) - {a $ i}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (proj2_rep ` (range (($) a) - {a $ i}))

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
with \<open>card ?Bi = 2\<close> and dim_le_card' [of ?Bi]
[PROOF STATE]
proof (chain)
picking this:
card (proj2_rep ` (range (($) a) - {a $ i})) = 2
finite (proj2_rep ` (range (($) a) - {a $ i})) \<Longrightarrow> dim (proj2_rep ` (range (($) a) - {a $ i})) \<le> card (proj2_rep ` (range (($) a) - {a $ i}))
finite (proj2_rep ` (range (($) a) - {a $ i}))
[PROOF STEP]
have "dim ?Bi \<le> 2"
[PROOF STATE]
proof (prove)
using this:
card (proj2_rep ` (range (($) a) - {a $ i})) = 2
finite (proj2_rep ` (range (($) a) - {a $ i})) \<Longrightarrow> dim (proj2_rep ` (range (($) a) - {a $ i})) \<le> card (proj2_rep ` (range (($) a) - {a $ i}))
finite (proj2_rep ` (range (($) a) - {a $ i}))

goal (1 subgoal):
 1. dim (proj2_rep ` (range (($) a) - {a $ i})) \<le> 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim (proj2_rep ` (range (($) a) - {a $ i})) \<le> 2

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
hence "dim (span ?Bi) \<le> 2"
[PROOF STATE]
proof (prove)
using this:
dim (proj2_rep ` (range (($) a) - {a $ i})) \<le> 2

goal (1 subgoal):
 1. dim (span (proj2_rep ` (range (($) a) - {a $ i}))) \<le> 2
[PROOF STEP]
by (subst dim_span)
[PROOF STATE]
proof (state)
this:
dim (span (proj2_rep ` (range (($) a) - {a $ i}))) \<le> 2

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dim (span (proj2_rep ` (range (($) a) - {a $ i}))) \<le> 2
[PROOF STEP]
have "span ?Bi \<noteq> UNIV"
[PROOF STATE]
proof (prove)
using this:
dim (span (proj2_rep ` (range (($) a) - {a $ i}))) \<le> 2

goal (1 subgoal):
 1. span (proj2_rep ` (range (($) a) - {a $ i})) \<noteq> UNIV
[PROOF STEP]
by clarify (auto simp: dim_UNIV)
[PROOF STATE]
proof (state)
this:
span (proj2_rep ` (range (($) a) - {a $ i})) \<noteq> UNIV

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
with \<open>span (insert ?v ?Bi) = UNIV\<close> and span_redundant
[PROOF STATE]
proof (chain)
picking this:
span (insert (proj2_rep a3) (proj2_rep ` (range (($) a) - {a $ i}))) = UNIV
?x \<in> span ?S \<Longrightarrow> span (insert ?x ?S) = span ?S
span (proj2_rep ` (range (($) a) - {a $ i})) \<noteq> UNIV
[PROOF STEP]
have "?v \<notin> span ?Bi"
[PROOF STATE]
proof (prove)
using this:
span (insert (proj2_rep a3) (proj2_rep ` (range (($) a) - {a $ i}))) = UNIV
?x \<in> span ?S \<Longrightarrow> span (insert ?x ?S) = span ?S
span (proj2_rep ` (range (($) a) - {a $ i})) \<noteq> UNIV

goal (1 subgoal):
 1. proj2_rep a3 \<notin> span (proj2_rep ` (range (($) a) - {a $ i}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_rep a3 \<notin> span (proj2_rep ` (range (($) a) - {a $ i}))

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
proj2_rep a3 \<notin> span (proj2_rep ` (range (($) a) - {a $ i}))

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
assume "c (proj2_rep (a$i)) = 0"
[PROOF STATE]
proof (state)
this:
c (proj2_rep (a $ i)) = 0

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
with \<open>(\<Sum> w \<in> ?Bi. (c w) *\<^sub>R w) =
        (\<Sum> w \<in> ?B. (c w) *\<^sub>R w) - c (proj2_rep (a$i)) *\<^sub>R proj2_rep (a$i)\<close>
        and \<open>(\<Sum> w \<in> ?B. (c w) *\<^sub>R w) = ?v\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>w\<in>proj2_rep ` (range (($) a) - {a $ i}). c w *\<^sub>R w) = (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) - c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)
(\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) = proj2_rep a3
c (proj2_rep (a $ i)) = 0
[PROOF STEP]
have "?v = (\<Sum> w \<in> ?Bi. (c w) *\<^sub>R w)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>w\<in>proj2_rep ` (range (($) a) - {a $ i}). c w *\<^sub>R w) = (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) - c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)
(\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) = proj2_rep a3
c (proj2_rep (a $ i)) = 0

goal (1 subgoal):
 1. proj2_rep a3 = (\<Sum>w\<in>proj2_rep ` (range (($) a) - {a $ i}). c w *\<^sub>R w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep a3 = (\<Sum>w\<in>proj2_rep ` (range (($) a) - {a $ i}). c w *\<^sub>R w)

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
with span_finite [of ?Bi] and \<open>finite ?Bi\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (proj2_rep ` (range (($) a) - {a $ i})) \<Longrightarrow> span (proj2_rep ` (range (($) a) - {a $ i})) = range (\<lambda>u. \<Sum>v\<in>proj2_rep ` (range (($) a) - {a $ i}). u v *\<^sub>R v)
finite (proj2_rep ` (range (($) a) - {a $ i}))
proj2_rep a3 = (\<Sum>w\<in>proj2_rep ` (range (($) a) - {a $ i}). c w *\<^sub>R w)
[PROOF STEP]
have "?v \<in> span ?Bi"
[PROOF STATE]
proof (prove)
using this:
finite (proj2_rep ` (range (($) a) - {a $ i})) \<Longrightarrow> span (proj2_rep ` (range (($) a) - {a $ i})) = range (\<lambda>u. \<Sum>v\<in>proj2_rep ` (range (($) a) - {a $ i}). u v *\<^sub>R v)
finite (proj2_rep ` (range (($) a) - {a $ i}))
proj2_rep a3 = (\<Sum>w\<in>proj2_rep ` (range (($) a) - {a $ i}). c w *\<^sub>R w)

goal (1 subgoal):
 1. proj2_rep a3 \<in> span (proj2_rep ` (range (($) a) - {a $ i}))
[PROOF STEP]
by (simp add: scalar_equiv)
[PROOF STATE]
proof (state)
this:
proj2_rep a3 \<in> span (proj2_rep ` (range (($) a) - {a $ i}))

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
with \<open>?v \<notin> span ?Bi\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_rep a3 \<notin> span (proj2_rep ` (range (($) a) - {a $ i}))
proj2_rep a3 \<in> span (proj2_rep ` (range (($) a) - {a $ i}))
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
proj2_rep a3 \<notin> span (proj2_rep ` (range (($) a) - {a $ i}))
proj2_rep a3 \<in> span (proj2_rep ` (range (($) a) - {a $ i}))

goal (1 subgoal):
 1. False
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c (proj2_rep (a $ i)) = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>i. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
thus "c (proj2_rep (a$i)) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
c (proj2_rep (a $ i)) = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. c (proj2_rep (a $ i)) \<noteq> 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
c (proj2_rep (a $ i)) \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. c (proj2_rep (a $ i)) \<noteq> 0

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
hence "\<forall> w\<in>?B. c w \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. c (proj2_rep (a $ i)) \<noteq> 0

goal (1 subgoal):
 1. \<forall>w\<in>proj2_rep ` range (($) a). c w \<noteq> 0
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. c (proj2_rep (a $ i)) \<noteq> 0

goal (1 subgoal):
 1. \<forall>w\<in>{y. \<exists>x\<in>{y. \<exists>x\<in>UNIV. y = a $ x}. y = proj2_rep x}. c w \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>proj2_rep ` range (($) a). c w \<noteq> 0

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
have "rows ?C = (\<lambda> w. (c w) *\<^sub>R w) ` ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<lambda>w. c w *\<^sub>R w) ` proj2_rep ` range (($) a)
[PROOF STEP]
unfolding rows_def
      and row_def
      and image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {vec_lambda (($) ((\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) $ i)) |i. i \<in> UNIV} = {y. \<exists>x\<in>{y. \<exists>x\<in>{y. \<exists>x\<in>UNIV. y = a $ x}. y = proj2_rep x}. y = c x *\<^sub>R x}
[PROOF STEP]
by (auto simp: vec_lambda_eta)
[PROOF STATE]
proof (state)
this:
rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<lambda>w. c w *\<^sub>R w) ` proj2_rep ` range (($) a)

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
have "\<forall> x. x \<in> span (rows ?C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
fix x :: "real^3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
from \<open>finite ?B\<close> and span_finite [of ?B] and \<open>span ?B = UNIV\<close>
[PROOF STATE]
proof (chain)
picking this:
finite (proj2_rep ` range (($) a))
finite (proj2_rep ` range (($) a)) \<Longrightarrow> span (proj2_rep ` range (($) a)) = range (\<lambda>u. \<Sum>v\<in>proj2_rep ` range (($) a). u v *\<^sub>R v)
span (proj2_rep ` range (($) a)) = UNIV
[PROOF STEP]
obtain ub where "(\<Sum> w\<in>?B. (ub w) *\<^sub>R w) = x"
[PROOF STATE]
proof (prove)
using this:
finite (proj2_rep ` range (($) a))
finite (proj2_rep ` range (($) a)) \<Longrightarrow> span (proj2_rep ` range (($) a)) = range (\<lambda>u. \<Sum>v\<in>proj2_rep ` range (($) a). u v *\<^sub>R v)
span (proj2_rep ` range (($) a)) = UNIV

goal (1 subgoal):
 1. (\<And>ub. (\<Sum>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w) = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: scalar_equiv) (metis (no_types, lifting) UNIV_I rangeE)
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w) = x

goal (1 subgoal):
 1. \<And>x. x \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
have "\<forall> w\<in>?B. (ub w) *\<^sub>R w \<in> span (rows ?C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. w \<in> proj2_rep ` range (($) a) \<Longrightarrow> ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. w \<in> proj2_rep ` range (($) a) \<Longrightarrow> ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
assume "w \<in> ?B"
[PROOF STATE]
proof (state)
this:
w \<in> proj2_rep ` range (($) a)

goal (1 subgoal):
 1. \<And>w. w \<in> proj2_rep ` range (($) a) \<Longrightarrow> ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
with span_superset [of "rows ?C"] and \<open>rows ?C = image (\<lambda> w. (c w) *\<^sub>R w) ?B\<close>
[PROOF STATE]
proof (chain)
picking this:
rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) \<subseteq> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<lambda>w. c w *\<^sub>R w) ` proj2_rep ` range (($) a)
w \<in> proj2_rep ` range (($) a)
[PROOF STEP]
have "(c w) *\<^sub>R w \<in> span (rows ?C)"
[PROOF STATE]
proof (prove)
using this:
rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) \<subseteq> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<lambda>w. c w *\<^sub>R w) ` proj2_rep ` range (($) a)
w \<in> proj2_rep ` range (($) a)

goal (1 subgoal):
 1. c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. \<And>w. w \<in> proj2_rep ` range (($) a) \<Longrightarrow> ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
with span_mul [of "(c w) *\<^sub>R w" "rows ?C" "(ub w)/(c w)"]
[PROOF STATE]
proof (chain)
picking this:
c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) \<Longrightarrow> (ub w / c w) *\<^sub>R c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
have "((ub w)/(c w)) *\<^sub>R ((c w) *\<^sub>R w) \<in> span (rows ?C)"
[PROOF STATE]
proof (prove)
using this:
c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) \<Longrightarrow> (ub w / c w) *\<^sub>R c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. (ub w / c w) *\<^sub>R c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
by (simp add: scalar_equiv)
[PROOF STATE]
proof (state)
this:
(ub w / c w) *\<^sub>R c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. \<And>w. w \<in> proj2_rep ` range (($) a) \<Longrightarrow> ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
with \<open>\<forall> w\<in>?B. c w \<noteq> 0\<close> and \<open>w \<in> ?B\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>proj2_rep ` range (($) a). c w \<noteq> 0
w \<in> proj2_rep ` range (($) a)
(ub w / c w) *\<^sub>R c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
show "(ub w) *\<^sub>R w \<in> span (rows ?C)"
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>proj2_rep ` range (($) a). c w \<noteq> 0
w \<in> proj2_rep ` range (($) a)
(ub w / c w) *\<^sub>R c w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. \<And>x. x \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
with span_sum [of ?B "\<lambda> w. (ub w) *\<^sub>R w"] and \<open>finite ?B\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<And>x. x \<in> proj2_rep ` range (($) a) \<Longrightarrow> ub x *\<^sub>R x \<in> span ?S) \<Longrightarrow> (\<Sum>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w) \<in> span ?S
finite (proj2_rep ` range (($) a))
\<forall>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
have "(\<Sum> w\<in>?B. (ub w) *\<^sub>R w) \<in> span (rows ?C)"
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> proj2_rep ` range (($) a) \<Longrightarrow> ub x *\<^sub>R x \<in> span ?S) \<Longrightarrow> (\<Sum>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w) \<in> span ?S
finite (proj2_rep ` range (($) a))
\<forall>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. (\<Sum>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w) \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w) \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. \<And>x. x \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
with \<open>(\<Sum> w\<in>?B. (ub w) *\<^sub>R w) = x\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w) = x
(\<Sum>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w) \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
show "x \<in> span (rows ?C)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w) = x
(\<Sum>w\<in>proj2_rep ` range (($) a). ub w *\<^sub>R w) \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. x \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
hence "span (rows ?C) = UNIV"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = UNIV

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with matrix_left_invertible_span_rows [of ?C]
[PROOF STATE]
proof (chain)
picking this:
(\<exists>B. B ** (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = mat 1) = (span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = UNIV)
span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = UNIV
[PROOF STEP]
have "\<exists> C'. C' ** ?C = mat 1"
[PROOF STATE]
proof (prove)
using this:
(\<exists>B. B ** (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = mat 1) = (span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = UNIV)
span (rows (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = UNIV

goal (1 subgoal):
 1. \<exists>C'. C' ** (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = mat 1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>C'. C' ** (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = mat 1

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with left_invertible_iff_invertible
[PROOF STATE]
proof (chain)
picking this:
(\<exists>N. N ** ?M = mat 1) = invertible ?M
\<exists>C'. C' ** (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = mat 1
[PROOF STEP]
have "invertible ?C"
[PROOF STATE]
proof (prove)
using this:
(\<exists>N. N ** ?M = mat 1) = invertible ?M
\<exists>C'. C' ** (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = mat 1

goal (1 subgoal):
 1. invertible (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
invertible (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
have "(vector [1,1,1] :: real^3) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector [1, 1, 1] \<noteq> 0
[PROOF STEP]
unfolding vector_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [1, 1, 1] (\<lambda>n x. 0) 1) \<noteq> 0
[PROOF STEP]
by (simp add: vec_eq_iff forall_3)
[PROOF STATE]
proof (state)
this:
vector [1, 1, 1] \<noteq> 0

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with apply_cltn2_abs and \<open>invertible ?C\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs ?x) (cltn2_abs ?A) = proj2_abs (?x v* ?A)
invertible (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))
vector [1, 1, 1] \<noteq> 0
[PROOF STEP]
have "apply_cltn2 (proj2_abs (vector [1,1,1])) ?A =
    proj2_abs (vector [1,1,1] v* ?C)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs ?x) (cltn2_abs ?A) = proj2_abs (?x v* ?A)
invertible (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))
vector [1, 1, 1] \<noteq> 0

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
from inj_on_iff_eq_card [of UNIV "($) a"] and \<open>card (range (($) a)) = 3\<close>
[PROOF STATE]
proof (chain)
picking this:
finite UNIV \<Longrightarrow> inj (($) a) = (card (range (($) a)) = CARD(3))
card (range (($) a)) = 3
[PROOF STEP]
have "inj (($) a)"
[PROOF STATE]
proof (prove)
using this:
finite UNIV \<Longrightarrow> inj (($) a) = (card (range (($) a)) = CARD(3))
card (range (($) a)) = 3

goal (1 subgoal):
 1. inj (($) a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inj (($) a)

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
from exhaust_3
[PROOF STATE]
proof (chain)
picking this:
?x = 1 \<or> ?x = 2 \<or> ?x = 3
[PROOF STEP]
have "\<forall> i::3. (vector [1::real,1,1])$i = 1"
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2 \<or> ?x = 3

goal (1 subgoal):
 1. \<forall>i. vector [1, 1, 1] $ i = 1
[PROOF STEP]
unfolding vector_def
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2 \<or> ?x = 3

goal (1 subgoal):
 1. \<forall>i. vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [1, 1, 1] (\<lambda>n x. 0) 1) $ i = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. vector [1, 1, 1] $ i = 1

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with vector_matrix_row [of "vector [1,1,1]" ?C]
[PROOF STATE]
proof (chain)
picking this:
vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>i\<in>UNIV. vector [1, 1, 1] $ i *s (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) $ i)
\<forall>i. vector [1, 1, 1] $ i = 1
[PROOF STEP]
have "(vector [1,1,1]) v* ?C =
    (\<Sum> i\<in>UNIV. (c (proj2_rep (a$i))) *\<^sub>R (proj2_rep (a$i)))"
[PROOF STATE]
proof (prove)
using this:
vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>i\<in>UNIV. vector [1, 1, 1] $ i *s (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) $ i)
\<forall>i. vector [1, 1, 1] $ i = 1

goal (1 subgoal):
 1. vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>i\<in>UNIV. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>i\<in>UNIV. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>i\<in>UNIV. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
from sum.reindex
  [of "($) a" UNIV "\<lambda> x. (c (proj2_rep x)) *\<^sub>R (proj2_rep x)"]
    and \<open>inj (($) a)\<close>
[PROOF STATE]
proof (chain)
picking this:
inj (($) a) \<Longrightarrow> (\<Sum>x\<in>range (($) a). c (proj2_rep x) *\<^sub>R proj2_rep x) = sum ((\<lambda>x. c (proj2_rep x) *\<^sub>R proj2_rep x) \<circ> ($) a) UNIV
inj (($) a)
[PROOF STEP]
have "\<dots> = (\<Sum> x\<in>(range (($) a)). (c (proj2_rep x)) *\<^sub>R (proj2_rep x))"
[PROOF STATE]
proof (prove)
using this:
inj (($) a) \<Longrightarrow> (\<Sum>x\<in>range (($) a). c (proj2_rep x) *\<^sub>R proj2_rep x) = sum ((\<lambda>x. c (proj2_rep x) *\<^sub>R proj2_rep x) \<circ> ($) a) UNIV
inj (($) a)

goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>x\<in>range (($) a). c (proj2_rep x) *\<^sub>R proj2_rep x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>UNIV. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>x\<in>range (($) a). c (proj2_rep x) *\<^sub>R proj2_rep x)

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>UNIV. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>x\<in>range (($) a). c (proj2_rep x) *\<^sub>R proj2_rep x)

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
from sum.reindex
  [of proj2_rep "range (($) a)" "\<lambda> w. (c w) *\<^sub>R w"]
    and proj2_rep_inj and subset_inj_on [of proj2_rep UNIV "range (($) a)"]
[PROOF STATE]
proof (chain)
picking this:
inj_on proj2_rep (range (($) a)) \<Longrightarrow> (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) = sum ((\<lambda>w. c w *\<^sub>R w) \<circ> proj2_rep) (range (($) a))
inj proj2_rep
\<lbrakk>inj proj2_rep; range (($) a) \<subseteq> UNIV\<rbrakk> \<Longrightarrow> inj_on proj2_rep (range (($) a))
[PROOF STEP]
have "\<dots> = (\<Sum> w\<in>?B. (c w) *\<^sub>R w)"
[PROOF STATE]
proof (prove)
using this:
inj_on proj2_rep (range (($) a)) \<Longrightarrow> (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) = sum ((\<lambda>w. c w *\<^sub>R w) \<circ> proj2_rep) (range (($) a))
inj proj2_rep
\<lbrakk>inj proj2_rep; range (($) a) \<subseteq> UNIV\<rbrakk> \<Longrightarrow> inj_on proj2_rep (range (($) a))

goal (1 subgoal):
 1. (\<Sum>x\<in>range (($) a). c (proj2_rep x) *\<^sub>R proj2_rep x) = (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>range (($) a). c (proj2_rep x) *\<^sub>R proj2_rep x) = (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w)

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>range (($) a). c (proj2_rep x) *\<^sub>R proj2_rep x) = (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w)

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
from \<open>(\<Sum> w \<in> ?B. (c w) *\<^sub>R w) = ?v\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) = proj2_rep a3
[PROOF STEP]
have "\<dots> = ?v"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) = proj2_rep a3

goal (1 subgoal):
 1. (\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) = proj2_rep a3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>w\<in>proj2_rep ` range (($) a). c w *\<^sub>R w) = proj2_rep a3

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = proj2_rep a3
[PROOF STEP]
have "(vector [1,1,1]) v* ?C = ?v"
[PROOF STATE]
proof (prove)
using this:
vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = proj2_rep a3

goal (1 subgoal):
 1. vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = proj2_rep a3
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = proj2_rep a3

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with \<open>apply_cltn2 (proj2_abs (vector [1,1,1])) ?A =
    proj2_abs (vector [1,1,1] v* ?C)\<close>
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = proj2_rep a3
[PROOF STEP]
have "apply_cltn2 (proj2_abs (vector [1,1,1])) ?A = proj2_abs ?v"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
vector [1, 1, 1] v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = proj2_rep a3

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (proj2_rep a3)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (proj2_rep a3)

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with proj2_abs_rep
[PROOF STATE]
proof (chain)
picking this:
proj2_abs (proj2_rep ?x) = ?x
apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (proj2_rep a3)
[PROOF STEP]
have "apply_cltn2 (proj2_abs (vector [1,1,1])) ?A = a3"
[PROOF STATE]
proof (prove)
using this:
proj2_abs (proj2_rep ?x) = ?x
apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (proj2_rep a3)

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a3

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
have "\<forall> j. apply_cltn2 (proj2_abs (axis j 1)) ?A = a$j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j
[PROOF STEP]
fix j :: "3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j
[PROOF STEP]
have "((axis j 1)::real^3) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. axis j 1 \<noteq> 0
[PROOF STEP]
by (simp add: vec_eq_iff axis_def)
[PROOF STATE]
proof (state)
this:
axis j 1 \<noteq> 0

goal (1 subgoal):
 1. \<And>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j
[PROOF STEP]
with apply_cltn2_abs and \<open>invertible ?C\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs ?x) (cltn2_abs ?A) = proj2_abs (?x v* ?A)
invertible (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))
axis j 1 \<noteq> 0
[PROOF STEP]
have "apply_cltn2 (proj2_abs (axis j 1)) ?A = proj2_abs (axis j 1 v* ?C)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs ?x) (cltn2_abs ?A) = proj2_abs (?x v* ?A)
invertible (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))
axis j 1 \<noteq> 0

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))

goal (1 subgoal):
 1. \<And>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j
[PROOF STEP]
have "\<forall> i\<in>(UNIV-{j}).
      ((axis j 1)$i * c (proj2_rep (a$i))) *\<^sub>R (proj2_rep (a$i)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>UNIV - {j}. (axis j 1 $ i * c (proj2_rep (a $ i))) *\<^sub>R proj2_rep (a $ i) = 0
[PROOF STEP]
by (simp add: axis_def)
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>UNIV - {j}. (axis j 1 $ i * c (proj2_rep (a $ i))) *\<^sub>R proj2_rep (a $ i) = 0

goal (1 subgoal):
 1. \<And>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j
[PROOF STEP]
with sum.mono_neutral_left [of UNIV "{j}"
      "\<lambda> i. ((axis j 1)$i * c (proj2_rep (a$i))) *\<^sub>R (proj2_rep (a$i))"]
      and vector_matrix_row [of "axis j 1" ?C]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite UNIV; {j} \<subseteq> UNIV; \<forall>i\<in>UNIV - {j}. (axis j 1 $ i * c (proj2_rep (a $ i))) *\<^sub>R proj2_rep (a $ i) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i\<in>{j}. (axis j 1 $ i * c (proj2_rep (a $ i))) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>i\<in>UNIV. (axis j 1 $ i * c (proj2_rep (a $ i))) *\<^sub>R proj2_rep (a $ i))
axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>i\<in>UNIV. axis j 1 $ i *s (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) $ i)
\<forall>i\<in>UNIV - {j}. (axis j 1 $ i * c (proj2_rep (a $ i))) *\<^sub>R proj2_rep (a $ i) = 0
[PROOF STEP]
have "(axis j 1) v* ?C = ?C$j"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite UNIV; {j} \<subseteq> UNIV; \<forall>i\<in>UNIV - {j}. (axis j 1 $ i * c (proj2_rep (a $ i))) *\<^sub>R proj2_rep (a $ i) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i\<in>{j}. (axis j 1 $ i * c (proj2_rep (a $ i))) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>i\<in>UNIV. (axis j 1 $ i * c (proj2_rep (a $ i))) *\<^sub>R proj2_rep (a $ i))
axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<Sum>i\<in>UNIV. axis j 1 $ i *s (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) $ i)
\<forall>i\<in>UNIV - {j}. (axis j 1 $ i * c (proj2_rep (a $ i))) *\<^sub>R proj2_rep (a $ i) = 0

goal (1 subgoal):
 1. axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) $ j
[PROOF STEP]
by (simp add: scalar_equiv)
[PROOF STATE]
proof (state)
this:
axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) $ j

goal (1 subgoal):
 1. \<And>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j
[PROOF STEP]
hence "(axis j 1) v* ?C = c (proj2_rep (a$j)) *\<^sub>R (proj2_rep (a$j))"
[PROOF STATE]
proof (prove)
using this:
axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) $ j

goal (1 subgoal):
 1. axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = c (proj2_rep (a $ j)) *\<^sub>R proj2_rep (a $ j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = c (proj2_rep (a $ j)) *\<^sub>R proj2_rep (a $ j)

goal (1 subgoal):
 1. \<And>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j
[PROOF STEP]
with proj2_abs_mult_rep and \<open>\<forall> i. c (proj2_rep (a$i)) \<noteq> 0\<close>
      and \<open>apply_cltn2 (proj2_abs (axis j 1)) ?A = proj2_abs (axis j 1 v* ?C)\<close>
[PROOF STATE]
proof (chain)
picking this:
?c \<noteq> 0 \<Longrightarrow> proj2_abs (?c *\<^sub>R proj2_rep ?x) = ?x
\<forall>i. c (proj2_rep (a $ i)) \<noteq> 0
apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = c (proj2_rep (a $ j)) *\<^sub>R proj2_rep (a $ j)
[PROOF STEP]
show "apply_cltn2 (proj2_abs (axis j 1)) ?A = a$j"
[PROOF STATE]
proof (prove)
using this:
?c \<noteq> 0 \<Longrightarrow> proj2_abs (?c *\<^sub>R proj2_rep ?x) = ?x
\<forall>i. c (proj2_rep (a $ i)) \<noteq> 0
apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = proj2_abs (axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)))
axis j 1 v* (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i)) = c (proj2_rep (a $ j)) *\<^sub>R proj2_rep (a $ j)

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
with \<open>apply_cltn2 (proj2_abs (vector [1,1,1])) ?A = a3\<close>
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a3
\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j
[PROOF STEP]
show "\<exists> A. apply_cltn2 (proj2_abs (vector [1,1,1])) A = a3 \<and>
    (\<forall> j. apply_cltn2 (proj2_abs (axis j 1)) A = a$j)"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a3
\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) (cltn2_abs (\<chi>i. c (proj2_rep (a $ i)) *\<^sub>R proj2_rep (a $ i))) = a $ j

goal (1 subgoal):
 1. \<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>A. apply_cltn2 (proj2_abs (vector [1, 1, 1])) A = a3 \<and> (\<forall>j. apply_cltn2 (proj2_abs (axis j 1)) A = a $ j)

goal:
No subgoals!
[PROOF STEP]
qed