[STATEMENT]
lemma statement53_existence:
  fixes p :: "proj2^4^2"
  assumes "\<forall> i. proj2_no_3_Col (range (($) (p$i)))"
  shows "\<exists> C. \<forall> j. apply_cltn2 (p$0$j) C = p$1$j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>C. \<forall>j. apply_cltn2 (p $ 0 $ j) C = p $ 1 $ j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>C. \<forall>j. apply_cltn2 (p $ 0 $ j) C = p $ 1 $ j
[PROOF STEP]
let ?q = "\<chi> i. \<chi> j::3. p$i $ (of_int (Rep_bit1 j))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>C. \<forall>j. apply_cltn2 (p $ 0 $ j) C = p $ 1 $ j
[PROOF STEP]
let ?D = "\<chi> i. \<some> D. apply_cltn2 (proj2_abs (vector [1,1,1])) D = p$i$3
    \<and> (\<forall> j'. apply_cltn2 (proj2_abs (axis j' 1)) D = ?q$i$j')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>C. \<forall>j. apply_cltn2 (p $ 0 $ j) C = p $ 1 $ j
[PROOF STEP]
have "\<forall> i. apply_cltn2 (proj2_abs (vector [1,1,1])) (?D$i) = p$i$3
    \<and> (\<forall> j'. apply_cltn2 (proj2_abs (axis j' 1)) (?D$i) = ?q$i$j')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
have "range (($) (p$i)) = insert (p$i$3) (range (($) (?q$i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (($) (p $ i)) = insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. range (($) (p $ i)) \<subseteq> insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
 2. insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i))) \<subseteq> range (($) (p $ i))
[PROOF STEP]
show "range (($) (p$i)) \<supseteq> insert (p$i$3) (range (($) (?q$i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i))) \<subseteq> range (($) (p $ i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i))) \<subseteq> range (($) (p $ i))

goal (1 subgoal):
 1. range (($) (p $ i)) \<subseteq> insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
[PROOF STEP]
show "range (($) (p$i)) \<subseteq> insert (p$i$3) (range (($) (?q$i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (($) (p $ i)) \<subseteq> insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> range (($) (p $ i)) \<Longrightarrow> x \<in> insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> range (($) (p $ i)) \<Longrightarrow> x \<in> insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
[PROOF STEP]
assume "r \<in> range (($) (p$i))"
[PROOF STATE]
proof (state)
this:
r \<in> range (($) (p $ i))

goal (1 subgoal):
 1. \<And>x. x \<in> range (($) (p $ i)) \<Longrightarrow> x \<in> insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> range (($) (p $ i))
[PROOF STEP]
obtain j where "r = p$i$j"
[PROOF STATE]
proof (prove)
using this:
r \<in> range (($) (p $ i))

goal (1 subgoal):
 1. (\<And>j. r = p $ i $ j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r = p $ i $ j

goal (1 subgoal):
 1. \<And>x. x \<in> range (($) (p $ i)) \<Longrightarrow> x \<in> insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
[PROOF STEP]
with eq_3_or_of_3 [of j]
[PROOF STATE]
proof (chain)
picking this:
j = 3 \<or> (\<exists>j'. j = of_int (Rep_bit1 j'))
r = p $ i $ j
[PROOF STEP]
show "r \<in> insert (p$i$3) (range (($) (?q$i)))"
[PROOF STATE]
proof (prove)
using this:
j = 3 \<or> (\<exists>j'. j = of_int (Rep_bit1 j'))
r = p $ i $ j

goal (1 subgoal):
 1. r \<in> insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
range (($) (p $ i)) \<subseteq> insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
range (($) (p $ i)) = insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))

goal (1 subgoal):
 1. \<And>i. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
range (($) (p $ i)) = insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))

goal (1 subgoal):
 1. \<And>i. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
from \<open>\<forall> i. proj2_no_3_Col (range (($) (p$i)))\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. proj2_no_3_Col (range (($) (p $ i)))
[PROOF STEP]
have "proj2_no_3_Col (range (($) (p$i)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. proj2_no_3_Col (range (($) (p $ i)))

goal (1 subgoal):
 1. proj2_no_3_Col (range (($) (p $ i)))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
proj2_no_3_Col (range (($) (p $ i)))

goal (1 subgoal):
 1. \<And>i. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
range (($) (p $ i)) = insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
proj2_no_3_Col (range (($) (p $ i)))
[PROOF STEP]
have "proj2_no_3_Col (insert (p$i$3) (range (($) (?q$i))))"
[PROOF STATE]
proof (prove)
using this:
range (($) (p $ i)) = insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i)))
proj2_no_3_Col (range (($) (p $ i)))

goal (1 subgoal):
 1. proj2_no_3_Col (insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_no_3_Col (insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i))))

goal (1 subgoal):
 1. \<And>i. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
hence "\<exists> D. apply_cltn2 (proj2_abs (vector [1,1,1])) D = p$i$3
      \<and> (\<forall> j'. apply_cltn2 (proj2_abs (axis j' 1)) D = ?q$i$j')"
[PROOF STATE]
proof (prove)
using this:
proj2_no_3_Col (insert (p $ i $ 3) (range (($) ((\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i))))

goal (1 subgoal):
 1. \<exists>D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
by (rule statement52_existence)
[PROOF STATE]
proof (state)
this:
\<exists>D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')

goal (1 subgoal):
 1. \<And>i. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
with someI_ex [of "\<lambda> D. apply_cltn2 (proj2_abs (vector [1,1,1])) D = p$i$3
      \<and> (\<forall> j'. apply_cltn2 (proj2_abs (axis j' 1)) D = ?q$i$j')"]
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. apply_cltn2 (proj2_abs (vector [1, 1, 1])) x = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) x = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j') \<Longrightarrow> apply_cltn2 (proj2_abs (vector [1, 1, 1])) (SOME x. apply_cltn2 (proj2_abs (vector [1, 1, 1])) x = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) x = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) (SOME x. apply_cltn2 (proj2_abs (vector [1, 1, 1])) x = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) x = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
\<exists>D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
show "apply_cltn2 (proj2_abs (vector [1,1,1])) (?D$i) = p$i$3
      \<and> (\<forall> j'. apply_cltn2 (proj2_abs (axis j' 1)) (?D$i) = ?q$i$j')"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. apply_cltn2 (proj2_abs (vector [1, 1, 1])) x = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) x = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j') \<Longrightarrow> apply_cltn2 (proj2_abs (vector [1, 1, 1])) (SOME x. apply_cltn2 (proj2_abs (vector [1, 1, 1])) x = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) x = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) (SOME x. apply_cltn2 (proj2_abs (vector [1, 1, 1])) x = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) x = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
\<exists>D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')

goal (1 subgoal):
 1. \<exists>C. \<forall>j. apply_cltn2 (p $ 0 $ j) C = p $ 1 $ j
[PROOF STEP]
hence "apply_cltn2 (proj2_abs (vector [1,1,1])) (?D$0) = p$0$3"
    and "apply_cltn2 (proj2_abs (vector [1,1,1])) (?D$1) = p$1$3"
    and "\<forall> j'. apply_cltn2 (proj2_abs (axis j' 1)) (?D$0) = ?q$0$j'"
    and "\<forall> j'. apply_cltn2 (proj2_abs (axis j' 1)) (?D$1) = ?q$1$j'"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ i) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')

goal (1 subgoal):
 1. (apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) = p $ 0 $ 3 &&& apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = p $ 1 $ 3) &&& \<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ 0 $ j' &&& \<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ 1 $ j'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) = p $ 0 $ 3
apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = p $ 1 $ 3
\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ 0 $ j'
\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ 1 $ j'

goal (1 subgoal):
 1. \<exists>C. \<forall>j. apply_cltn2 (p $ 0 $ j) C = p $ 1 $ j
[PROOF STEP]
let ?C = "cltn2_compose (cltn2_inverse (?D$0)) (?D$1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>C. \<forall>j. apply_cltn2 (p $ 0 $ j) C = p $ 1 $ j
[PROOF STEP]
have "\<forall> j. apply_cltn2 (p$0$j) ?C = p$1$j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
show "apply_cltn2 (p$0$j) ?C = p$1$j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
 2. \<not> ?P \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
assume "j = 3"
[PROOF STATE]
proof (state)
this:
j = 3

goal (2 subgoals):
 1. ?P \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
 2. \<not> ?P \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
with \<open>apply_cltn2 (proj2_abs (vector [1,1,1])) (?D$0) = p$0$3\<close>
        and  cltn2.act_inv_iff
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) = p $ 0 $ 3
?g \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr> \<Longrightarrow> (apply_cltn2 ?b (inv\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> ?g) = ?c) = (?b = apply_cltn2 ?c ?g)
j = 3
[PROOF STEP]
have
        "apply_cltn2 (p$0$j) (cltn2_inverse (?D$0)) = proj2_abs (vector [1,1,1])"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) = p $ 0 $ 3
?g \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr> \<Longrightarrow> (apply_cltn2 ?b (inv\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> ?g) = ?c) = (?b = apply_cltn2 ?c ?g)
j = 3

goal (1 subgoal):
 1. apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) = proj2_abs (vector [1, 1, 1])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) = proj2_abs (vector [1, 1, 1])

goal (2 subgoals):
 1. ?P \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
 2. \<not> ?P \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
with \<open>apply_cltn2 (proj2_abs (vector [1,1,1])) (?D$1) = p$1$3\<close>
        and \<open>j = 3\<close>
        and cltn2.act_act [of "cltn2_inverse (?D$0)" "?D$1" "p$0$j"]
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = p $ 1 $ 3
j = 3
\<lbrakk>cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>; (\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1 \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<rbrakk> \<Longrightarrow> apply_cltn2 (apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0))) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) \<otimes>\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> (\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)
apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) = proj2_abs (vector [1, 1, 1])
[PROOF STEP]
show "apply_cltn2 (p$0$j) ?C = p$1$j"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (proj2_abs (vector [1, 1, 1])) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = p $ 1 $ 3
j = 3
\<lbrakk>cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>; (\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1 \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<rbrakk> \<Longrightarrow> apply_cltn2 (apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0))) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) \<otimes>\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> (\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)
apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) = proj2_abs (vector [1, 1, 1])

goal (1 subgoal):
 1. apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j

goal (1 subgoal):
 1. j \<noteq> 3 \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<noteq> 3 \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
assume "j \<noteq> 3"
[PROOF STATE]
proof (state)
this:
j \<noteq> 3

goal (1 subgoal):
 1. j \<noteq> 3 \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
with eq_3_or_of_3
[PROOF STATE]
proof (chain)
picking this:
?j = 3 \<or> (\<exists>j'. ?j = of_int (Rep_bit1 j'))
j \<noteq> 3
[PROOF STEP]
obtain j' :: 3 where "j = of_int (Rep_bit1 j')"
[PROOF STATE]
proof (prove)
using this:
?j = 3 \<or> (\<exists>j'. ?j = of_int (Rep_bit1 j'))
j \<noteq> 3

goal (1 subgoal):
 1. (\<And>j'. j = of_int (Rep_bit1 j') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
j = of_int (Rep_bit1 j')

goal (1 subgoal):
 1. j \<noteq> 3 \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
with \<open>\<forall> j'. apply_cltn2 (proj2_abs (axis j' 1)) (?D$0) = ?q$0$j'\<close>
        and \<open>\<forall> j'. apply_cltn2 (proj2_abs (axis j' 1)) (?D$1) = ?q$1$j'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ 0 $ j'
\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ 1 $ j'
j = of_int (Rep_bit1 j')
[PROOF STEP]
have "p$0$j = apply_cltn2 (proj2_abs (axis j' 1)) (?D$0)"
        and "p$1$j = apply_cltn2 (proj2_abs (axis j' 1)) (?D$1)"
[PROOF STATE]
proof (prove)
using this:
\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ 0 $ j'
\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ 1 $ j'
j = of_int (Rep_bit1 j')

goal (1 subgoal):
 1. p $ 0 $ j = apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) &&& p $ 1 $ j = apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
p $ 0 $ j = apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)
p $ 1 $ j = apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)

goal (1 subgoal):
 1. j \<noteq> 3 \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
from \<open>p$0$j = apply_cltn2 (proj2_abs (axis j' 1)) (?D$0)\<close>
        and cltn2.act_inv_iff
[PROOF STATE]
proof (chain)
picking this:
p $ 0 $ j = apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)
?g \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr> \<Longrightarrow> (apply_cltn2 ?b (inv\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> ?g) = ?c) = (?b = apply_cltn2 ?c ?g)
[PROOF STEP]
have "apply_cltn2 (p$0$j) (cltn2_inverse (?D$0)) = proj2_abs (axis j' 1)"
[PROOF STATE]
proof (prove)
using this:
p $ 0 $ j = apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)
?g \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr> \<Longrightarrow> (apply_cltn2 ?b (inv\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> ?g) = ?c) = (?b = apply_cltn2 ?c ?g)

goal (1 subgoal):
 1. apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) = proj2_abs (axis j' 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) = proj2_abs (axis j' 1)

goal (1 subgoal):
 1. j \<noteq> 3 \<Longrightarrow> apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
with \<open>p$1$j = apply_cltn2 (proj2_abs (axis j' 1)) (?D$1)\<close>
        and cltn2.act_act [of "cltn2_inverse (?D$0)" "?D$1" "p$0$j"]
[PROOF STATE]
proof (chain)
picking this:
p $ 1 $ j = apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)
\<lbrakk>cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>; (\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1 \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<rbrakk> \<Longrightarrow> apply_cltn2 (apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0))) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) \<otimes>\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> (\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)
apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) = proj2_abs (axis j' 1)
[PROOF STEP]
show "apply_cltn2 (p$0$j) ?C = p$1$j"
[PROOF STATE]
proof (prove)
using this:
p $ 1 $ j = apply_cltn2 (proj2_abs (axis j' 1)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)
\<lbrakk>cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>; (\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1 \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<rbrakk> \<Longrightarrow> apply_cltn2 (apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0))) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1) = apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0) \<otimes>\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> (\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)
apply_cltn2 (p $ 0 $ j) (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) = proj2_abs (axis j' 1)

goal (1 subgoal):
 1. apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>j. apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j

goal (1 subgoal):
 1. \<exists>C. \<forall>j. apply_cltn2 (p $ 0 $ j) C = p $ 1 $ j
[PROOF STEP]
thus "\<exists> C. \<forall> j. apply_cltn2 (p$0$j) C = p$1$j"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. apply_cltn2 (p $ 0 $ j) (cltn2_compose (cltn2_inverse ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 0)) ((\<chi>i. SOME D. apply_cltn2 (proj2_abs (vector [1, 1, 1])) D = p $ i $ 3 \<and> (\<forall>j'. apply_cltn2 (proj2_abs (axis j' 1)) D = (\<chi>i j. p $ i $ of_int (Rep_bit1 j)) $ i $ j')) $ 1)) = p $ 1 $ j

goal (1 subgoal):
 1. \<exists>C. \<forall>j. apply_cltn2 (p $ 0 $ j) C = p $ 1 $ j
[PROOF STEP]
by (rule exI [of _ ?C])
[PROOF STATE]
proof (state)
this:
\<exists>C. \<forall>j. apply_cltn2 (p $ 0 $ j) C = p $ 1 $ j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_cltn2_linear:
  assumes "j *\<^sub>R v + k *\<^sub>R w \<noteq> 0"
  shows "j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) \<noteq> 0"
  (is "?u \<noteq> 0")
  and "apply_cltn2 (proj2_abs (j *\<^sub>R v + k *\<^sub>R w)) C
  = proj2_abs (j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) \<noteq> 0 &&& apply_cltn2 (proj2_abs (j *\<^sub>R v + k *\<^sub>R w)) C = proj2_abs (j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) \<noteq> 0
 2. apply_cltn2 (proj2_abs (j *\<^sub>R v + k *\<^sub>R w)) C = proj2_abs (j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C))
[PROOF STEP]
have "?u = (j *\<^sub>R v + k *\<^sub>R w) v* cltn2_rep C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) = (j *\<^sub>R v + k *\<^sub>R w) v* cltn2_rep C
[PROOF STEP]
by (simp only: vector_matrix_left_distrib scaleR_vector_matrix_assoc)
[PROOF STATE]
proof (state)
this:
j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) = (j *\<^sub>R v + k *\<^sub>R w) v* cltn2_rep C

goal (2 subgoals):
 1. j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) \<noteq> 0
 2. apply_cltn2 (proj2_abs (j *\<^sub>R v + k *\<^sub>R w)) C = proj2_abs (j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C))
[PROOF STEP]
with \<open>j *\<^sub>R v + k *\<^sub>R w \<noteq> 0\<close> and non_zero_mult_rep_non_zero
[PROOF STATE]
proof (chain)
picking this:
j *\<^sub>R v + k *\<^sub>R w \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> ?v v* cltn2_rep ?C \<noteq> 0
j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) = (j *\<^sub>R v + k *\<^sub>R w) v* cltn2_rep C
[PROOF STEP]
show "?u \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
j *\<^sub>R v + k *\<^sub>R w \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> ?v v* cltn2_rep ?C \<noteq> 0
j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) = (j *\<^sub>R v + k *\<^sub>R w) v* cltn2_rep C

goal (1 subgoal):
 1. j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) \<noteq> 0

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs (j *\<^sub>R v + k *\<^sub>R w)) C = proj2_abs (j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C))
[PROOF STEP]
from \<open>?u = (j *\<^sub>R v + k *\<^sub>R w) v* cltn2_rep C\<close>
    and \<open>j *\<^sub>R v + k *\<^sub>R w \<noteq> 0\<close>
    and apply_cltn2_left_abs
[PROOF STATE]
proof (chain)
picking this:
j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) = (j *\<^sub>R v + k *\<^sub>R w) v* cltn2_rep C
j *\<^sub>R v + k *\<^sub>R w \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> apply_cltn2 (proj2_abs ?v) ?C = proj2_abs (?v v* cltn2_rep ?C)
[PROOF STEP]
show "apply_cltn2 (proj2_abs (j *\<^sub>R v + k *\<^sub>R w)) C = proj2_abs ?u"
[PROOF STATE]
proof (prove)
using this:
j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C) = (j *\<^sub>R v + k *\<^sub>R w) v* cltn2_rep C
j *\<^sub>R v + k *\<^sub>R w \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> apply_cltn2 (proj2_abs ?v) ?C = proj2_abs (?v v* cltn2_rep ?C)

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs (j *\<^sub>R v + k *\<^sub>R w)) C = proj2_abs (j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (proj2_abs (j *\<^sub>R v + k *\<^sub>R w)) C = proj2_abs (j *\<^sub>R (v v* cltn2_rep C) + k *\<^sub>R (w v* cltn2_rep C))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_cltn2_imp_mult:
  assumes "apply_cltn2 p C = q"
  shows "\<exists> k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q
[PROOF STEP]
have "proj2_rep p v* cltn2_rep C \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep p v* cltn2_rep C \<noteq> 0
[PROOF STEP]
by (rule rep_mult_rep_non_zero)
[PROOF STATE]
proof (state)
this:
proj2_rep p v* cltn2_rep C \<noteq> 0

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q
[PROOF STEP]
from \<open>apply_cltn2 p C = q\<close>
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 p C = q
[PROOF STEP]
have "proj2_abs (proj2_rep p v* cltn2_rep C) = q"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 p C = q

goal (1 subgoal):
 1. proj2_abs (proj2_rep p v* cltn2_rep C) = q
[PROOF STEP]
by (unfold apply_cltn2_def)
[PROOF STATE]
proof (state)
this:
proj2_abs (proj2_rep p v* cltn2_rep C) = q

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q
[PROOF STEP]
hence "proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep C)) = proj2_rep q"
[PROOF STATE]
proof (prove)
using this:
proj2_abs (proj2_rep p v* cltn2_rep C) = q

goal (1 subgoal):
 1. proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep C)) = proj2_rep q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep C)) = proj2_rep q

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q
[PROOF STEP]
with \<open>proj2_rep p v* cltn2_rep C \<noteq> 0\<close> and proj2_rep_abs2 [of "proj2_rep p v* cltn2_rep C"]
[PROOF STATE]
proof (chain)
picking this:
proj2_rep p v* cltn2_rep C \<noteq> 0
proj2_rep p v* cltn2_rep C \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep C)) = k *\<^sub>R (proj2_rep p v* cltn2_rep C)
proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep C)) = proj2_rep q
[PROOF STEP]
have "\<exists> j. j \<noteq> 0 \<and> proj2_rep q = j *\<^sub>R (proj2_rep p v* cltn2_rep C)"
[PROOF STATE]
proof (prove)
using this:
proj2_rep p v* cltn2_rep C \<noteq> 0
proj2_rep p v* cltn2_rep C \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep C)) = k *\<^sub>R (proj2_rep p v* cltn2_rep C)
proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep C)) = proj2_rep q

goal (1 subgoal):
 1. \<exists>j. j \<noteq> 0 \<and> proj2_rep q = j *\<^sub>R (proj2_rep p v* cltn2_rep C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>j. j \<noteq> 0 \<and> proj2_rep q = j *\<^sub>R (proj2_rep p v* cltn2_rep C)

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. j \<noteq> 0 \<and> proj2_rep q = j *\<^sub>R (proj2_rep p v* cltn2_rep C)
[PROOF STEP]
obtain j where "j \<noteq> 0"
    and "proj2_rep q = j *\<^sub>R (proj2_rep p v* cltn2_rep C)"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. j \<noteq> 0 \<and> proj2_rep q = j *\<^sub>R (proj2_rep p v* cltn2_rep C)

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<noteq> 0; proj2_rep q = j *\<^sub>R (proj2_rep p v* cltn2_rep C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<noteq> 0
proj2_rep q = j *\<^sub>R (proj2_rep p v* cltn2_rep C)

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q
[PROOF STEP]
hence "proj2_rep p v* cltn2_rep C = (1/j) *\<^sub>R proj2_rep q"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
proj2_rep q = j *\<^sub>R (proj2_rep p v* cltn2_rep C)

goal (1 subgoal):
 1. proj2_rep p v* cltn2_rep C = (1 / j) *\<^sub>R proj2_rep q
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
proj2_rep p v* cltn2_rep C = (1 / j) *\<^sub>R proj2_rep q

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q
[PROOF STEP]
with \<open>j \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
j \<noteq> 0
proj2_rep p v* cltn2_rep C = (1 / j) *\<^sub>R proj2_rep q
[PROOF STEP]
show "\<exists> k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
proj2_rep p v* cltn2_rep C = (1 / j) *\<^sub>R proj2_rep q

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q
[PROOF STEP]
by (simp add: exI [of _ "1/j"])
[PROOF STATE]
proof (state)
this:
\<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma statement55:
  assumes "p \<noteq> q"
  and "apply_cltn2 p C = q"
  and "apply_cltn2 q C = p"
  and "proj2_incident p l"
  and "proj2_incident q l"
  and "proj2_incident r l"
  shows "apply_cltn2 (apply_cltn2 r C) C = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
 2. \<not> ?P \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
assume "r = p"
[PROOF STATE]
proof (state)
this:
r = p

goal (2 subgoals):
 1. ?P \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
 2. \<not> ?P \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
with \<open>apply_cltn2 p C = q\<close> and \<open>apply_cltn2 q C = p\<close>
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 p C = q
apply_cltn2 q C = p
r = p
[PROOF STEP]
show "apply_cltn2 (apply_cltn2 r C) C = r"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 p C = q
apply_cltn2 q C = p
r = p

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (apply_cltn2 r C) C = r

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
assume "r \<noteq> p"
[PROOF STATE]
proof (state)
this:
r \<noteq> p

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
from \<open>apply_cltn2 p C = q\<close> and apply_cltn2_imp_mult [of p C q]
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 p C = q
apply_cltn2 p C = q \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q
[PROOF STEP]
obtain i where "i \<noteq> 0" and "proj2_rep p v* cltn2_rep C = i *\<^sub>R proj2_rep q"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 p C = q
apply_cltn2 p C = q \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep p v* cltn2_rep C = k *\<^sub>R proj2_rep q

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<noteq> 0; proj2_rep p v* cltn2_rep C = i *\<^sub>R proj2_rep q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<noteq> 0
proj2_rep p v* cltn2_rep C = i *\<^sub>R proj2_rep q

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
from \<open>apply_cltn2 q C = p\<close> and apply_cltn2_imp_mult [of q C p]
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 q C = p
apply_cltn2 q C = p \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep q v* cltn2_rep C = k *\<^sub>R proj2_rep p
[PROOF STEP]
obtain j where "j \<noteq> 0" and "proj2_rep q v* cltn2_rep C = j *\<^sub>R proj2_rep p"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 q C = p
apply_cltn2 q C = p \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep q v* cltn2_rep C = k *\<^sub>R proj2_rep p

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<noteq> 0; proj2_rep q v* cltn2_rep C = j *\<^sub>R proj2_rep p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<noteq> 0
proj2_rep q v* cltn2_rep C = j *\<^sub>R proj2_rep p

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
from \<open>p \<noteq> q\<close>
    and \<open>proj2_incident p l\<close>
    and \<open>proj2_incident q l\<close>
    and \<open>proj2_incident r l\<close>
    and proj2_incident_iff
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
proj2_incident p l
proj2_incident q l
proj2_incident r l
\<lbrakk>?p \<noteq> ?q; proj2_incident ?p ?l; proj2_incident ?q ?l\<rbrakk> \<Longrightarrow> proj2_incident ?r ?l = (?r = ?p \<or> (\<exists>k. ?r = proj2_abs (k *\<^sub>R proj2_rep ?p + proj2_rep ?q)))
[PROOF STEP]
have "r = p \<or> (\<exists> k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q))"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
proj2_incident p l
proj2_incident q l
proj2_incident r l
\<lbrakk>?p \<noteq> ?q; proj2_incident ?p ?l; proj2_incident ?q ?l\<rbrakk> \<Longrightarrow> proj2_incident ?r ?l = (?r = ?p \<or> (\<exists>k. ?r = proj2_abs (k *\<^sub>R proj2_rep ?p + proj2_rep ?q)))

goal (1 subgoal):
 1. r = p \<or> (\<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
r = p \<or> (\<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q))

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
with \<open>r \<noteq> p\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> p
r = p \<or> (\<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q))
[PROOF STEP]
obtain k where "r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)"
[PROOF STATE]
proof (prove)
using this:
r \<noteq> p
r = p \<or> (\<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q))

goal (1 subgoal):
 1. (\<And>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
from \<open>p \<noteq> q\<close> and proj2_rep_dependent [of k p 1 q]
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
\<lbrakk>k *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q = 0; k \<noteq> 0 \<or> 1 \<noteq> 0\<rbrakk> \<Longrightarrow> p = q
[PROOF STEP]
have "k *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
\<lbrakk>k *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q = 0; k \<noteq> 0 \<or> 1 \<noteq> 0\<rbrakk> \<Longrightarrow> p = q

goal (1 subgoal):
 1. k *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
with \<open>r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)\<close>
    and apply_cltn2_linear [of k "proj2_rep p" 1 "proj2_rep q"]
[PROOF STATE]
proof (chain)
picking this:
r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)
k *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> k *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C) \<noteq> 0
k *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> apply_cltn2 (proj2_abs (k *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q)) ?C = proj2_abs (k *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C))
k *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
[PROOF STEP]
have "k *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C \<noteq> 0"
    and "apply_cltn2 r C
    = proj2_abs
    (k *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)"
[PROOF STATE]
proof (prove)
using this:
r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)
k *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> k *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C) \<noteq> 0
k *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> apply_cltn2 (proj2_abs (k *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q)) ?C = proj2_abs (k *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C))
k *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0

goal (1 subgoal):
 1. k *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C \<noteq> 0 &&& apply_cltn2 r C = proj2_abs (k *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
k *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C \<noteq> 0
apply_cltn2 r C = proj2_abs (k *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
with \<open>proj2_rep p v* cltn2_rep C = i *\<^sub>R proj2_rep q\<close>
    and \<open>proj2_rep q v* cltn2_rep C = j *\<^sub>R proj2_rep p\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_rep p v* cltn2_rep C = i *\<^sub>R proj2_rep q
proj2_rep q v* cltn2_rep C = j *\<^sub>R proj2_rep p
k *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C \<noteq> 0
apply_cltn2 r C = proj2_abs (k *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)
[PROOF STEP]
have "(k * i) *\<^sub>R proj2_rep q + j *\<^sub>R proj2_rep p \<noteq> 0"
    and "apply_cltn2 r C
    = proj2_abs ((k * i) *\<^sub>R proj2_rep q + j *\<^sub>R proj2_rep p)"
[PROOF STATE]
proof (prove)
using this:
proj2_rep p v* cltn2_rep C = i *\<^sub>R proj2_rep q
proj2_rep q v* cltn2_rep C = j *\<^sub>R proj2_rep p
k *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C \<noteq> 0
apply_cltn2 r C = proj2_abs (k *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)

goal (1 subgoal):
 1. (k * i) *\<^sub>R proj2_rep q + j *\<^sub>R proj2_rep p \<noteq> 0 &&& apply_cltn2 r C = proj2_abs ((k * i) *\<^sub>R proj2_rep q + j *\<^sub>R proj2_rep p)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
(k * i) *\<^sub>R proj2_rep q + j *\<^sub>R proj2_rep p \<noteq> 0
apply_cltn2 r C = proj2_abs ((k * i) *\<^sub>R proj2_rep q + j *\<^sub>R proj2_rep p)

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
with apply_cltn2_linear
[PROOF STATE]
proof (chain)
picking this:
?j *\<^sub>R ?v + ?k *\<^sub>R ?w \<noteq> 0 \<Longrightarrow> ?j *\<^sub>R (?v v* cltn2_rep ?C) + ?k *\<^sub>R (?w v* cltn2_rep ?C) \<noteq> 0
?j *\<^sub>R ?v + ?k *\<^sub>R ?w \<noteq> 0 \<Longrightarrow> apply_cltn2 (proj2_abs (?j *\<^sub>R ?v + ?k *\<^sub>R ?w)) ?C = proj2_abs (?j *\<^sub>R (?v v* cltn2_rep ?C) + ?k *\<^sub>R (?w v* cltn2_rep ?C))
(k * i) *\<^sub>R proj2_rep q + j *\<^sub>R proj2_rep p \<noteq> 0
apply_cltn2 r C = proj2_abs ((k * i) *\<^sub>R proj2_rep q + j *\<^sub>R proj2_rep p)
[PROOF STEP]
have "apply_cltn2 (apply_cltn2 r C) C
    = proj2_abs
    ((k * i) *\<^sub>R (proj2_rep q v* cltn2_rep C)
    + j *\<^sub>R (proj2_rep p v* cltn2_rep C))"
[PROOF STATE]
proof (prove)
using this:
?j *\<^sub>R ?v + ?k *\<^sub>R ?w \<noteq> 0 \<Longrightarrow> ?j *\<^sub>R (?v v* cltn2_rep ?C) + ?k *\<^sub>R (?w v* cltn2_rep ?C) \<noteq> 0
?j *\<^sub>R ?v + ?k *\<^sub>R ?w \<noteq> 0 \<Longrightarrow> apply_cltn2 (proj2_abs (?j *\<^sub>R ?v + ?k *\<^sub>R ?w)) ?C = proj2_abs (?j *\<^sub>R (?v v* cltn2_rep ?C) + ?k *\<^sub>R (?w v* cltn2_rep ?C))
(k * i) *\<^sub>R proj2_rep q + j *\<^sub>R proj2_rep p \<noteq> 0
apply_cltn2 r C = proj2_abs ((k * i) *\<^sub>R proj2_rep q + j *\<^sub>R proj2_rep p)

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 r C) C = proj2_abs ((k * i) *\<^sub>R (proj2_rep q v* cltn2_rep C) + j *\<^sub>R (proj2_rep p v* cltn2_rep C))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (apply_cltn2 r C) C = proj2_abs ((k * i) *\<^sub>R (proj2_rep q v* cltn2_rep C) + j *\<^sub>R (proj2_rep p v* cltn2_rep C))

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
with \<open>proj2_rep p v* cltn2_rep C = i *\<^sub>R proj2_rep q\<close>
    and \<open>proj2_rep q v* cltn2_rep C = j *\<^sub>R proj2_rep p\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_rep p v* cltn2_rep C = i *\<^sub>R proj2_rep q
proj2_rep q v* cltn2_rep C = j *\<^sub>R proj2_rep p
apply_cltn2 (apply_cltn2 r C) C = proj2_abs ((k * i) *\<^sub>R (proj2_rep q v* cltn2_rep C) + j *\<^sub>R (proj2_rep p v* cltn2_rep C))
[PROOF STEP]
have "apply_cltn2 (apply_cltn2 r C) C
    = proj2_abs ((k * i * j) *\<^sub>R proj2_rep p + (j * i) *\<^sub>R proj2_rep q)"
[PROOF STATE]
proof (prove)
using this:
proj2_rep p v* cltn2_rep C = i *\<^sub>R proj2_rep q
proj2_rep q v* cltn2_rep C = j *\<^sub>R proj2_rep p
apply_cltn2 (apply_cltn2 r C) C = proj2_abs ((k * i) *\<^sub>R (proj2_rep q v* cltn2_rep C) + j *\<^sub>R (proj2_rep p v* cltn2_rep C))

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 r C) C = proj2_abs ((k * i * j) *\<^sub>R proj2_rep p + (j * i) *\<^sub>R proj2_rep q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (apply_cltn2 r C) C = proj2_abs ((k * i * j) *\<^sub>R proj2_rep p + (j * i) *\<^sub>R proj2_rep q)

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
apply_cltn2 (apply_cltn2 r C) C = proj2_abs ((k * i * j) *\<^sub>R proj2_rep p + (j * i) *\<^sub>R proj2_rep q)

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
have "\<dots> = proj2_abs ((i * j) *\<^sub>R (k *\<^sub>R proj2_rep p + proj2_rep q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_abs ((k * i * j) *\<^sub>R proj2_rep p + (j * i) *\<^sub>R proj2_rep q) = proj2_abs ((i * j) *\<^sub>R (k *\<^sub>R proj2_rep p + proj2_rep q))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
proj2_abs ((k * i * j) *\<^sub>R proj2_rep p + (j * i) *\<^sub>R proj2_rep q) = proj2_abs ((i * j) *\<^sub>R (k *\<^sub>R proj2_rep p + proj2_rep q))

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proj2_abs ((k * i * j) *\<^sub>R proj2_rep p + (j * i) *\<^sub>R proj2_rep q) = proj2_abs ((i * j) *\<^sub>R (k *\<^sub>R proj2_rep p + proj2_rep q))

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
from \<open>i \<noteq> 0\<close> and \<open>j \<noteq> 0\<close> and proj2_abs_mult
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> 0
j \<noteq> 0
?c \<noteq> 0 \<Longrightarrow> proj2_abs (?c *\<^sub>R ?v) = proj2_abs ?v
[PROOF STEP]
have "\<dots> = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0
j \<noteq> 0
?c \<noteq> 0 \<Longrightarrow> proj2_abs (?c *\<^sub>R ?v) = proj2_abs ?v

goal (1 subgoal):
 1. proj2_abs ((i * j) *\<^sub>R (k *\<^sub>R proj2_rep p + proj2_rep q)) = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_abs ((i * j) *\<^sub>R (k *\<^sub>R proj2_rep p + proj2_rep q)) = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proj2_abs ((i * j) *\<^sub>R (k *\<^sub>R proj2_rep p + proj2_rep q)) = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
from \<open>r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)\<close>
[PROOF STATE]
proof (chain)
picking this:
r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
have "\<dots> = r"
[PROOF STATE]
proof (prove)
using this:
r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q) = r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q) = r

goal (1 subgoal):
 1. r \<noteq> p \<Longrightarrow> apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
show "apply_cltn2 (apply_cltn2 r C) C = r"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (apply_cltn2 r C) C = r

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 r C) C = r
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
apply_cltn2 (apply_cltn2 r C) C = r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_Col_coeff_abs:
  assumes "p \<noteq> q" and "j \<noteq> 0"
  shows "proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q))
  = i/j"
  (is "proj2_Col_coeff p q ?r = i/j")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
from \<open>j \<noteq> 0\<close>
    and proj2_abs_mult [of "1/j" "i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q"]
[PROOF STATE]
proof (chain)
picking this:
j \<noteq> 0
1 / j \<noteq> 0 \<Longrightarrow> proj2_abs ((1 / j) *\<^sub>R (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)
[PROOF STEP]
have "?r = proj2_abs ((i/j) *\<^sub>R proj2_rep p + proj2_rep q)"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
1 / j \<noteq> 0 \<Longrightarrow> proj2_abs ((1 / j) *\<^sub>R (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)

goal (1 subgoal):
 1. proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = proj2_abs ((i / j) *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
by (simp add: scaleR_right_distrib)
[PROOF STATE]
proof (state)
this:
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = proj2_abs ((i / j) *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
from \<open>p \<noteq> q\<close> and proj2_rep_dependent [of _ p 1 q]
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
\<lbrakk>?i *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q = 0; ?i \<noteq> 0 \<or> 1 \<noteq> 0\<rbrakk> \<Longrightarrow> p = q
[PROOF STEP]
have "(i/j) *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
\<lbrakk>?i *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q = 0; ?i \<noteq> 0 \<or> 1 \<noteq> 0\<rbrakk> \<Longrightarrow> p = q

goal (1 subgoal):
 1. (i / j) *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i / j) *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0

goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
with \<open>?r = proj2_abs ((i/j) *\<^sub>R proj2_rep p + proj2_rep q)\<close>
    and proj2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = proj2_abs ((i / j) *\<^sub>R proj2_rep p + proj2_rep q)
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
(i / j) *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
[PROOF STEP]
obtain k where "k \<noteq> 0"
    and "proj2_rep ?r = k *\<^sub>R ((i/j) *\<^sub>R proj2_rep p + proj2_rep q)"
[PROOF STATE]
proof (prove)
using this:
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = proj2_abs ((i / j) *\<^sub>R proj2_rep p + proj2_rep q)
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
(i / j) *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<noteq> 0; proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = k *\<^sub>R ((i / j) *\<^sub>R proj2_rep p + proj2_rep q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<noteq> 0
proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = k *\<^sub>R ((i / j) *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
hence "(k*i/j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q - proj2_rep ?r = 0"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = k *\<^sub>R ((i / j) *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. (k * i / j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q - proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = 0
[PROOF STEP]
by (simp add: scaleR_right_distrib)
[PROOF STATE]
proof (state)
this:
(k * i / j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q - proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = 0

goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
hence "\<exists> l. (k*i/j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q + l *\<^sub>R proj2_rep ?r = 0
    \<and> (k*i/j \<noteq> 0 \<or> k \<noteq> 0 \<or> l \<noteq> 0)"
[PROOF STATE]
proof (prove)
using this:
(k * i / j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q - proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = 0

goal (1 subgoal):
 1. \<exists>l. (k * i / j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q + l *\<^sub>R proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = 0 \<and> (k * i / j \<noteq> 0 \<or> k \<noteq> 0 \<or> l \<noteq> 0)
[PROOF STEP]
by (simp add: exI [of _ "-1"])
[PROOF STATE]
proof (state)
this:
\<exists>l. (k * i / j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q + l *\<^sub>R proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = 0 \<and> (k * i / j \<noteq> 0 \<or> k \<noteq> 0 \<or> l \<noteq> 0)

goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
hence "proj2_Col p q ?r"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. (k * i / j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q + l *\<^sub>R proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = 0 \<and> (k * i / j \<noteq> 0 \<or> k \<noteq> 0 \<or> l \<noteq> 0)

goal (1 subgoal):
 1. proj2_Col p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q))
[PROOF STEP]
by (unfold proj2_Col_def) auto
[PROOF STATE]
proof (state)
this:
proj2_Col p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q))

goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
have "?r \<noteq> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) \<noteq> p
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = p \<Longrightarrow> False
[PROOF STEP]
assume "?r = p"
[PROOF STATE]
proof (state)
this:
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = p

goal (1 subgoal):
 1. proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = p \<Longrightarrow> False
[PROOF STEP]
with \<open>(k*i/j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q - proj2_rep ?r = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
(k * i / j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q - proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = 0
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = p
[PROOF STEP]
have "(k*i/j - 1) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q = 0"
[PROOF STATE]
proof (prove)
using this:
(k * i / j) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q - proj2_rep (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = 0
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = p

goal (1 subgoal):
 1. (k * i / j - 1) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q = 0
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
(k * i / j - 1) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q = 0

goal (1 subgoal):
 1. proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = p \<Longrightarrow> False
[PROOF STEP]
with \<open>k \<noteq> 0\<close> and proj2_rep_dependent
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
\<lbrakk>?i *\<^sub>R proj2_rep ?v + ?j *\<^sub>R proj2_rep ?w = 0; ?i \<noteq> 0 \<or> ?j \<noteq> 0\<rbrakk> \<Longrightarrow> ?v = ?w
(k * i / j - 1) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q = 0
[PROOF STEP]
have "p = q"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
\<lbrakk>?i *\<^sub>R proj2_rep ?v + ?j *\<^sub>R proj2_rep ?w = 0; ?i \<noteq> 0 \<or> ?j \<noteq> 0\<rbrakk> \<Longrightarrow> ?v = ?w
(k * i / j - 1) *\<^sub>R proj2_rep p + k *\<^sub>R proj2_rep q = 0

goal (1 subgoal):
 1. p = q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p = q

goal (1 subgoal):
 1. proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = p \<Longrightarrow> False
[PROOF STEP]
with \<open>p \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
p = q
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
p = q

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) \<noteq> p

goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
with \<open>proj2_Col p q ?r\<close> and \<open>p \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_Col p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q))
p \<noteq> q
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) \<noteq> p
[PROOF STEP]
have "?r = proj2_abs (proj2_Col_coeff p q ?r *\<^sub>R proj2_rep p + proj2_rep q)"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q))
p \<noteq> q
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) \<noteq> p

goal (1 subgoal):
 1. proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = proj2_abs (proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
by (rule proj2_Col_coeff)
[PROOF STATE]
proof (state)
this:
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = proj2_abs (proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
with \<open>p \<noteq> q\<close> and \<open>?r = proj2_abs ((i/j) *\<^sub>R proj2_rep p + proj2_rep q)\<close>
    and proj2_Col_coeff_unique
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = proj2_abs ((i / j) *\<^sub>R proj2_rep p + proj2_rep q)
\<lbrakk>?a \<noteq> ?r; proj2_abs (?i *\<^sub>R proj2_rep ?a + proj2_rep ?r) = proj2_abs (?j *\<^sub>R proj2_rep ?a + proj2_rep ?r)\<rbrakk> \<Longrightarrow> ?i = ?j
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = proj2_abs (proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
show "proj2_Col_coeff p q ?r = i/j"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = proj2_abs ((i / j) *\<^sub>R proj2_rep p + proj2_rep q)
\<lbrakk>?a \<noteq> ?r; proj2_abs (?i *\<^sub>R proj2_rep ?a + proj2_rep ?r) = proj2_abs (?j *\<^sub>R proj2_rep ?a + proj2_rep ?r)\<rbrakk> \<Longrightarrow> ?i = ?j
proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q) = proj2_abs (proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q (proj2_abs (i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q)) = i / j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_set_Col_coeff:
  assumes "proj2_set_Col S" and "{p,q,r} \<subseteq> S" and "p \<noteq> q" and "r \<noteq> p"
  shows "r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)"
  (is "r = proj2_abs (?i *\<^sub>R ?u + ?v)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
from \<open>{p,q,r} \<subseteq> S\<close> and \<open>proj2_set_Col S\<close>
[PROOF STATE]
proof (chain)
picking this:
{p, q, r} \<subseteq> S
proj2_set_Col S
[PROOF STEP]
have "proj2_set_Col {p,q,r}"
[PROOF STATE]
proof (prove)
using this:
{p, q, r} \<subseteq> S
proj2_set_Col S

goal (1 subgoal):
 1. proj2_set_Col {p, q, r}
[PROOF STEP]
by (rule proj2_subset_Col)
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
hence "proj2_Col p q r"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. proj2_Col p q r
[PROOF STEP]
by (subst proj2_Col_iff_set_Col)
[PROOF STATE]
proof (state)
this:
proj2_Col p q r

goal (1 subgoal):
 1. r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
with \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and proj2_Col_coeff
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
r \<noteq> p
\<lbrakk>proj2_Col ?a ?r ?t; ?a \<noteq> ?r; ?t \<noteq> ?a\<rbrakk> \<Longrightarrow> ?t = proj2_abs (proj2_Col_coeff ?a ?r ?t *\<^sub>R proj2_rep ?a + proj2_rep ?r)
proj2_Col p q r
[PROOF STEP]
show "r = proj2_abs (?i *\<^sub>R ?u + ?v)"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
r \<noteq> p
\<lbrakk>proj2_Col ?a ?r ?t; ?a \<noteq> ?r; ?t \<noteq> ?a\<rbrakk> \<Longrightarrow> ?t = proj2_abs (proj2_Col_coeff ?a ?r ?t *\<^sub>R proj2_rep ?a + proj2_rep ?r)
proj2_Col p q r

goal (1 subgoal):
 1. r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cross_ratio_abs:
  fixes u v :: "real^3" and i j k l :: real
  assumes "u \<noteq> 0" and "v \<noteq> 0" and "proj2_abs u \<noteq> proj2_abs v"
  and "j \<noteq> 0" and "l \<noteq> 0"
  shows "cross_ratio (proj2_abs u) (proj2_abs v)
  (proj2_abs (i *\<^sub>R u + j *\<^sub>R v))
  (proj2_abs (k *\<^sub>R u + l *\<^sub>R v))
  = j * k / (i * l)"
  (is "cross_ratio ?p ?q ?r ?s = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = j * k / (i * l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = j * k / (i * l)
[PROOF STEP]
from \<open>u \<noteq> 0\<close> and proj2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
[PROOF STEP]
obtain g where "g \<noteq> 0" and "proj2_rep ?p = g *\<^sub>R u"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<noteq> 0; proj2_rep (proj2_abs u) = g *\<^sub>R u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<noteq> 0
proj2_rep (proj2_abs u) = g *\<^sub>R u

goal (1 subgoal):
 1. cross_ratio (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = j * k / (i * l)
[PROOF STEP]
from \<open>v \<noteq> 0\<close> and proj2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
[PROOF STEP]
obtain h where "h \<noteq> 0" and "proj2_rep ?q = h *\<^sub>R v"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<noteq> 0; proj2_rep (proj2_abs v) = h *\<^sub>R v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h \<noteq> 0
proj2_rep (proj2_abs v) = h *\<^sub>R v

goal (1 subgoal):
 1. cross_ratio (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = j * k / (i * l)
[PROOF STEP]
with \<open>g \<noteq> 0\<close> and \<open>proj2_rep ?p = g *\<^sub>R u\<close>
[PROOF STATE]
proof (chain)
picking this:
g \<noteq> 0
proj2_rep (proj2_abs u) = g *\<^sub>R u
h \<noteq> 0
proj2_rep (proj2_abs v) = h *\<^sub>R v
[PROOF STEP]
have "?r = proj2_abs ((i/g) *\<^sub>R proj2_rep ?p + (j/h) *\<^sub>R proj2_rep ?q)"
    and "?s = proj2_abs ((k/g) *\<^sub>R proj2_rep ?p + (l/h) *\<^sub>R proj2_rep ?q)"
[PROOF STATE]
proof (prove)
using this:
g \<noteq> 0
proj2_rep (proj2_abs u) = g *\<^sub>R u
h \<noteq> 0
proj2_rep (proj2_abs v) = h *\<^sub>R v

goal (1 subgoal):
 1. proj2_abs (i *\<^sub>R u + j *\<^sub>R v) = proj2_abs ((i / g) *\<^sub>R proj2_rep (proj2_abs u) + (j / h) *\<^sub>R proj2_rep (proj2_abs v)) &&& proj2_abs (k *\<^sub>R u + l *\<^sub>R v) = proj2_abs ((k / g) *\<^sub>R proj2_rep (proj2_abs u) + (l / h) *\<^sub>R proj2_rep (proj2_abs v))
[PROOF STEP]
by (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
proj2_abs (i *\<^sub>R u + j *\<^sub>R v) = proj2_abs ((i / g) *\<^sub>R proj2_rep (proj2_abs u) + (j / h) *\<^sub>R proj2_rep (proj2_abs v))
proj2_abs (k *\<^sub>R u + l *\<^sub>R v) = proj2_abs ((k / g) *\<^sub>R proj2_rep (proj2_abs u) + (l / h) *\<^sub>R proj2_rep (proj2_abs v))

goal (1 subgoal):
 1. cross_ratio (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = j * k / (i * l)
[PROOF STEP]
with \<open>?p \<noteq> ?q\<close> and \<open>h \<noteq> 0\<close> and \<open>j \<noteq> 0\<close> and \<open>l \<noteq> 0\<close> and proj2_Col_coeff_abs
[PROOF STATE]
proof (chain)
picking this:
proj2_abs u \<noteq> proj2_abs v
h \<noteq> 0
j \<noteq> 0
l \<noteq> 0
\<lbrakk>?p \<noteq> ?q; ?j \<noteq> 0\<rbrakk> \<Longrightarrow> proj2_Col_coeff ?p ?q (proj2_abs (?i *\<^sub>R proj2_rep ?p + ?j *\<^sub>R proj2_rep ?q)) = ?i / ?j
proj2_abs (i *\<^sub>R u + j *\<^sub>R v) = proj2_abs ((i / g) *\<^sub>R proj2_rep (proj2_abs u) + (j / h) *\<^sub>R proj2_rep (proj2_abs v))
proj2_abs (k *\<^sub>R u + l *\<^sub>R v) = proj2_abs ((k / g) *\<^sub>R proj2_rep (proj2_abs u) + (l / h) *\<^sub>R proj2_rep (proj2_abs v))
[PROOF STEP]
have "proj2_Col_coeff ?p ?q ?r = h*i/(g*j)"
    and "proj2_Col_coeff ?p ?q ?s = h*k/(g*l)"
[PROOF STATE]
proof (prove)
using this:
proj2_abs u \<noteq> proj2_abs v
h \<noteq> 0
j \<noteq> 0
l \<noteq> 0
\<lbrakk>?p \<noteq> ?q; ?j \<noteq> 0\<rbrakk> \<Longrightarrow> proj2_Col_coeff ?p ?q (proj2_abs (?i *\<^sub>R proj2_rep ?p + ?j *\<^sub>R proj2_rep ?q)) = ?i / ?j
proj2_abs (i *\<^sub>R u + j *\<^sub>R v) = proj2_abs ((i / g) *\<^sub>R proj2_rep (proj2_abs u) + (j / h) *\<^sub>R proj2_rep (proj2_abs v))
proj2_abs (k *\<^sub>R u + l *\<^sub>R v) = proj2_abs ((k / g) *\<^sub>R proj2_rep (proj2_abs u) + (l / h) *\<^sub>R proj2_rep (proj2_abs v))

goal (1 subgoal):
 1. proj2_Col_coeff (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) = h * i / (g * j) &&& proj2_Col_coeff (proj2_abs u) (proj2_abs v) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = h * k / (g * l)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) = h * i / (g * j)
proj2_Col_coeff (proj2_abs u) (proj2_abs v) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = h * k / (g * l)

goal (1 subgoal):
 1. cross_ratio (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = j * k / (i * l)
[PROOF STEP]
with \<open>g \<noteq> 0\<close> and \<open>h \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
g \<noteq> 0
h \<noteq> 0
proj2_Col_coeff (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) = h * i / (g * j)
proj2_Col_coeff (proj2_abs u) (proj2_abs v) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = h * k / (g * l)
[PROOF STEP]
show "cross_ratio ?p ?q ?r ?s = j*k/(i*l)"
[PROOF STATE]
proof (prove)
using this:
g \<noteq> 0
h \<noteq> 0
proj2_Col_coeff (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) = h * i / (g * j)
proj2_Col_coeff (proj2_abs u) (proj2_abs v) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = h * k / (g * l)

goal (1 subgoal):
 1. cross_ratio (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = j * k / (i * l)
[PROOF STEP]
by (unfold cross_ratio_def) (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
cross_ratio (proj2_abs u) (proj2_abs v) (proj2_abs (i *\<^sub>R u + j *\<^sub>R v)) (proj2_abs (k *\<^sub>R u + l *\<^sub>R v)) = j * k / (i * l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cross_ratio_abs2:
  assumes "p \<noteq> q"
  shows "cross_ratio p q
  (proj2_abs (i *\<^sub>R proj2_rep p + proj2_rep q))
  (proj2_abs (j *\<^sub>R proj2_rep p + proj2_rep q))
  = j/i"
  (is "cross_ratio p q ?r ?s = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio p q (proj2_abs (i *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (j *\<^sub>R proj2_rep p + proj2_rep q)) = j / i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio p q (proj2_abs (i *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (j *\<^sub>R proj2_rep p + proj2_rep q)) = j / i
[PROOF STEP]
let ?u = "proj2_rep p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio p q (proj2_abs (i *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (j *\<^sub>R proj2_rep p + proj2_rep q)) = j / i
[PROOF STEP]
let ?v = "proj2_rep q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio p q (proj2_abs (i *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (j *\<^sub>R proj2_rep p + proj2_rep q)) = j / i
[PROOF STEP]
have "?u \<noteq> 0" and "?v \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep p \<noteq> 0 &&& proj2_rep q \<noteq> 0
[PROOF STEP]
by (rule proj2_rep_non_zero)+
[PROOF STATE]
proof (state)
this:
proj2_rep p \<noteq> 0
proj2_rep q \<noteq> 0

goal (1 subgoal):
 1. cross_ratio p q (proj2_abs (i *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (j *\<^sub>R proj2_rep p + proj2_rep q)) = j / i
[PROOF STEP]
have "proj2_abs ?u = p" and "proj2_abs ?v = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_abs (proj2_rep p) = p &&& proj2_abs (proj2_rep q) = q
[PROOF STEP]
by (rule proj2_abs_rep)+
[PROOF STATE]
proof (state)
this:
proj2_abs (proj2_rep p) = p
proj2_abs (proj2_rep q) = q

goal (1 subgoal):
 1. cross_ratio p q (proj2_abs (i *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (j *\<^sub>R proj2_rep p + proj2_rep q)) = j / i
[PROOF STEP]
with \<open>?u \<noteq> 0\<close> and \<open>?v \<noteq> 0\<close> and \<open>p \<noteq> q\<close> and cross_ratio_abs [of ?u ?v 1 1 i j]
[PROOF STATE]
proof (chain)
picking this:
proj2_rep p \<noteq> 0
proj2_rep q \<noteq> 0
p \<noteq> q
\<lbrakk>proj2_rep p \<noteq> 0; proj2_rep q \<noteq> 0; proj2_abs (proj2_rep p) \<noteq> proj2_abs (proj2_rep q); 1 \<noteq> 0; 1 \<noteq> 0\<rbrakk> \<Longrightarrow> cross_ratio (proj2_abs (proj2_rep p)) (proj2_abs (proj2_rep q)) (proj2_abs (i *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q)) (proj2_abs (j *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q)) = 1 * j / (i * 1)
proj2_abs (proj2_rep p) = p
proj2_abs (proj2_rep q) = q
[PROOF STEP]
show "cross_ratio p q ?r ?s = j/i"
[PROOF STATE]
proof (prove)
using this:
proj2_rep p \<noteq> 0
proj2_rep q \<noteq> 0
p \<noteq> q
\<lbrakk>proj2_rep p \<noteq> 0; proj2_rep q \<noteq> 0; proj2_abs (proj2_rep p) \<noteq> proj2_abs (proj2_rep q); 1 \<noteq> 0; 1 \<noteq> 0\<rbrakk> \<Longrightarrow> cross_ratio (proj2_abs (proj2_rep p)) (proj2_abs (proj2_rep q)) (proj2_abs (i *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q)) (proj2_abs (j *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q)) = 1 * j / (i * 1)
proj2_abs (proj2_rep p) = p
proj2_abs (proj2_rep q) = q

goal (1 subgoal):
 1. cross_ratio p q (proj2_abs (i *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (j *\<^sub>R proj2_rep p + proj2_rep q)) = j / i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cross_ratio p q (proj2_abs (i *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (j *\<^sub>R proj2_rep p + proj2_rep q)) = j / i

goal:
No subgoals!
[PROOF STEP]
qed