[STATEMENT]
theorem fundamental_property_of_path_slicing_semantically:
  assumes "m \<triangleq> c" and "\<langle>c,[cf]\<rangle> \<Rightarrow> \<langle>c',s'\<rangle>"
  obtains m' as cfs' where "m -as\<rightarrow>\<^sub>\<surd>* m'" and "m' \<triangleq> c'"
  and "preds (slice_kinds {CFG_node m'} as) [(cf,undefined)]"
  and "\<forall>V \<in> Use m'.
  state_val (transfers (slice_kinds {CFG_node m'} as) [(cf,undefined)]) V =
  state_val cfs' V" and "map fst cfs' = s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as m' cfs'. \<lbrakk>m -as\<rightarrow>\<^sub>\<surd>* m'; m' \<triangleq> c'; preds (slice_kinds {CFG_node m'} as) [(cf, undefined)]; \<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as) [(cf, undefined)]) V = state_val cfs' V; map fst cfs' = s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as m' cfs'. m -as\<rightarrow>\<^sub>\<surd>* m' \<and> m' \<triangleq> c' \<and> preds (slice_kinds {CFG_node m'} as) [(cf, undefined)] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as) [(cf, undefined)]) V = state_val cfs' V) \<and> map fst cfs' = s'
[PROOF STEP]
from \<open>m \<triangleq> c\<close> \<open>\<langle>c,[cf]\<rangle> \<Rightarrow> \<langle>c',s'\<rangle>\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<triangleq> c
\<langle>c,[cf]\<rangle> \<Rightarrow> \<langle>c',s'\<rangle>
[PROOF STEP]
obtain m' as cfs' where "m -as\<rightarrow>\<^sub>\<surd>* m'"
    and "transfers (kinds as) [(cf,undefined)] = cfs'"
    and "preds (kinds as) [(cf,undefined)]" and "m' \<triangleq> c'" and "map fst cfs' = s'"
[PROOF STATE]
proof (prove)
using this:
m \<triangleq> c
\<langle>c,[cf]\<rangle> \<Rightarrow> \<langle>c',s'\<rangle>

goal (1 subgoal):
 1. (\<And>as m' cfs'. \<lbrakk>m -as\<rightarrow>\<^sub>\<surd>* m'; transfers (kinds as) [(cf, undefined)] = cfs'; preds (kinds as) [(cf, undefined)]; m' \<triangleq> c'; map fst cfs' = s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest:fundamental_property)
[PROOF STATE]
proof (state)
this:
m -as\<rightarrow>\<^sub>\<surd>* m'
transfers (kinds as) [(cf, undefined)] = cfs'
preds (kinds as) [(cf, undefined)]
m' \<triangleq> c'
map fst cfs' = s'

goal (1 subgoal):
 1. \<exists>as m' cfs'. m -as\<rightarrow>\<^sub>\<surd>* m' \<and> m' \<triangleq> c' \<and> preds (slice_kinds {CFG_node m'} as) [(cf, undefined)] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as) [(cf, undefined)]) V = state_val cfs' V) \<and> map fst cfs' = s'
[PROOF STEP]
from \<open>m -as\<rightarrow>\<^sub>\<surd>* m'\<close> \<open>preds (kinds as) [(cf,undefined)]\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>\<^sub>\<surd>* m'
preds (kinds as) [(cf, undefined)]
[PROOF STEP]
obtain as'
    where "preds (slice_kinds {CFG_node m'} as') [(cf,undefined)]"
    and vals:"\<forall>V \<in> Use m'. state_val (transfers (slice_kinds {CFG_node m'} as')
    [(cf,undefined)]) V = state_val (transfers (kinds as) [(cf,undefined)]) V"
    and "m -as'\<rightarrow>\<^sub>\<surd>* m'"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>\<^sub>\<surd>* m'
preds (kinds as) [(cf, undefined)]

goal (1 subgoal):
 1. (\<And>as'. \<lbrakk>preds (slice_kinds {CFG_node m'} as') [(cf, undefined)]; \<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as') [(cf, undefined)]) V = state_val (transfers (kinds as) [(cf, undefined)]) V; m -as'\<rightarrow>\<^sub>\<surd>* m'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule fundamental_property_of_static_slicing,auto)
[PROOF STATE]
proof (state)
this:
preds (slice_kinds {CFG_node m'} as') [(cf, undefined)]
\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as') [(cf, undefined)]) V = state_val (transfers (kinds as) [(cf, undefined)]) V
m -as'\<rightarrow>\<^sub>\<surd>* m'

goal (1 subgoal):
 1. \<exists>as m' cfs'. m -as\<rightarrow>\<^sub>\<surd>* m' \<and> m' \<triangleq> c' \<and> preds (slice_kinds {CFG_node m'} as) [(cf, undefined)] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as) [(cf, undefined)]) V = state_val cfs' V) \<and> map fst cfs' = s'
[PROOF STEP]
from \<open>transfers (kinds as) [(cf,undefined)] = cfs'\<close> vals
[PROOF STATE]
proof (chain)
picking this:
transfers (kinds as) [(cf, undefined)] = cfs'
\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as') [(cf, undefined)]) V = state_val (transfers (kinds as) [(cf, undefined)]) V
[PROOF STEP]
have "\<forall>V \<in> Use m'.
    state_val (transfers (slice_kinds {CFG_node m'} as') [(cf,undefined)]) V =
    state_val cfs' V"
[PROOF STATE]
proof (prove)
using this:
transfers (kinds as) [(cf, undefined)] = cfs'
\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as') [(cf, undefined)]) V = state_val (transfers (kinds as) [(cf, undefined)]) V

goal (1 subgoal):
 1. \<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as') [(cf, undefined)]) V = state_val cfs' V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as') [(cf, undefined)]) V = state_val cfs' V

goal (1 subgoal):
 1. \<exists>as m' cfs'. m -as\<rightarrow>\<^sub>\<surd>* m' \<and> m' \<triangleq> c' \<and> preds (slice_kinds {CFG_node m'} as) [(cf, undefined)] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as) [(cf, undefined)]) V = state_val cfs' V) \<and> map fst cfs' = s'
[PROOF STEP]
with \<open>preds (slice_kinds {CFG_node m'} as') [(cf,undefined)]\<close> \<open>m -as'\<rightarrow>\<^sub>\<surd>* m'\<close>
    \<open>m' \<triangleq> c'\<close> \<open>map fst cfs' = s'\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (slice_kinds {CFG_node m'} as') [(cf, undefined)]
m -as'\<rightarrow>\<^sub>\<surd>* m'
m' \<triangleq> c'
map fst cfs' = s'
\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as') [(cf, undefined)]) V = state_val cfs' V
[PROOF STEP]
show "\<exists>as m' cfs'. m -as\<rightarrow>\<^sub>\<surd>* m' \<and> m' \<triangleq> c' \<and>
    preds (slice_kinds {CFG_node m'} as) [(cf, undefined)] \<and>
    (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as)
    [(cf, undefined)]) V = state_val cfs' V) \<and> map fst cfs' = s'"
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds {CFG_node m'} as') [(cf, undefined)]
m -as'\<rightarrow>\<^sub>\<surd>* m'
m' \<triangleq> c'
map fst cfs' = s'
\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as') [(cf, undefined)]) V = state_val cfs' V

goal (1 subgoal):
 1. \<exists>as m' cfs'. m -as\<rightarrow>\<^sub>\<surd>* m' \<and> m' \<triangleq> c' \<and> preds (slice_kinds {CFG_node m'} as) [(cf, undefined)] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as) [(cf, undefined)]) V = state_val cfs' V) \<and> map fst cfs' = s'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>as m' cfs'. m -as\<rightarrow>\<^sub>\<surd>* m' \<and> m' \<triangleq> c' \<and> preds (slice_kinds {CFG_node m'} as) [(cf, undefined)] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds {CFG_node m'} as) [(cf, undefined)]) V = state_val cfs' V) \<and> map fst cfs' = s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proportionality_refl_on: "refl_on local.non_zero_vectors local.proportionality"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on local.non_zero_vectors local.proportionality
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. refl_on local.non_zero_vectors local.proportionality
[PROOF STEP]
have "local.proportionality \<subseteq> local.non_zero_vectors \<times> local.non_zero_vectors"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.proportionality \<subseteq> local.non_zero_vectors \<times> local.non_zero_vectors
[PROOF STEP]
unfolding proportionality_def non_zero_vectors_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). x \<noteq> (0::'b) \<and> y \<noteq> (0::'b) \<and> (\<exists>k. x = k *s y)} \<subseteq> {x. x \<noteq> (0::'b)} \<times> {x. x \<noteq> (0::'b)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.proportionality \<subseteq> local.non_zero_vectors \<times> local.non_zero_vectors

goal (1 subgoal):
 1. refl_on local.non_zero_vectors local.proportionality
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.proportionality \<subseteq> local.non_zero_vectors \<times> local.non_zero_vectors

goal (1 subgoal):
 1. refl_on local.non_zero_vectors local.proportionality
[PROOF STEP]
have "\<forall>x\<in>local.non_zero_vectors. (x, x) \<in> local.proportionality"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>local.non_zero_vectors. (x, x) \<in> local.proportionality
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> local.non_zero_vectors \<Longrightarrow> (x, x) \<in> local.proportionality
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> local.non_zero_vectors \<Longrightarrow> (x, x) \<in> local.proportionality
[PROOF STEP]
assume "x \<in> local.non_zero_vectors"
[PROOF STATE]
proof (state)
this:
x \<in> local.non_zero_vectors

goal (1 subgoal):
 1. \<And>x. x \<in> local.non_zero_vectors \<Longrightarrow> (x, x) \<in> local.proportionality
[PROOF STEP]
hence "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> local.non_zero_vectors

goal (1 subgoal):
 1. x \<noteq> (0::'b)
[PROOF STEP]
unfolding non_zero_vectors_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. x \<noteq> (0::'b)}

goal (1 subgoal):
 1. x \<noteq> (0::'b)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x \<noteq> (0::'b)

goal (1 subgoal):
 1. \<And>x. x \<in> local.non_zero_vectors \<Longrightarrow> (x, x) \<in> local.proportionality
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<noteq> (0::'b)

goal (1 subgoal):
 1. \<And>x. x \<in> local.non_zero_vectors \<Longrightarrow> (x, x) \<in> local.proportionality
[PROOF STEP]
have "x = scale 1 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (1::'a) *s x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = (1::'a) *s x

goal (1 subgoal):
 1. \<And>x. x \<in> local.non_zero_vectors \<Longrightarrow> (x, x) \<in> local.proportionality
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> (0::'b)
x = (1::'a) *s x
[PROOF STEP]
show "(x, x) \<in> local.proportionality"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'b)
x = (1::'a) *s x

goal (1 subgoal):
 1. (x, x) \<in> local.proportionality
[PROOF STEP]
unfolding proportionality_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'b)
x = (1::'a) *s x

goal (1 subgoal):
 1. (x, x) \<in> {(x, y). x \<noteq> (0::'b) \<and> y \<noteq> (0::'b) \<and> (\<exists>k. x = k *s y)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, x) \<in> local.proportionality

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>local.non_zero_vectors. (x, x) \<in> local.proportionality

goal (1 subgoal):
 1. refl_on local.non_zero_vectors local.proportionality
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.proportionality \<subseteq> local.non_zero_vectors \<times> local.non_zero_vectors
\<forall>x\<in>local.non_zero_vectors. (x, x) \<in> local.proportionality
[PROOF STEP]
show "refl_on local.non_zero_vectors local.proportionality"
[PROOF STATE]
proof (prove)
using this:
local.proportionality \<subseteq> local.non_zero_vectors \<times> local.non_zero_vectors
\<forall>x\<in>local.non_zero_vectors. (x, x) \<in> local.proportionality

goal (1 subgoal):
 1. refl_on local.non_zero_vectors local.proportionality
[PROOF STEP]
unfolding refl_on_def
[PROOF STATE]
proof (prove)
using this:
local.proportionality \<subseteq> local.non_zero_vectors \<times> local.non_zero_vectors
\<forall>x\<in>local.non_zero_vectors. (x, x) \<in> local.proportionality

goal (1 subgoal):
 1. local.proportionality \<subseteq> local.non_zero_vectors \<times> local.non_zero_vectors \<and> (\<forall>x\<in>local.non_zero_vectors. (x, x) \<in> local.proportionality)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
refl_on local.non_zero_vectors local.proportionality

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proportionality_sym: "sym local.proportionality"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
assume "(x, y) \<in> local.proportionality"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> local.proportionality

goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
hence "x \<noteq> 0" and "y \<noteq> 0" and "\<exists>k. x = scale k y"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> local.proportionality

goal (1 subgoal):
 1. x \<noteq> (0::'b) &&& y \<noteq> (0::'b) &&& \<exists>k. x = k *s y
[PROOF STEP]
unfolding proportionality_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). x \<noteq> (0::'b) \<and> y \<noteq> (0::'b) \<and> (\<exists>k. x = k *s y)}

goal (1 subgoal):
 1. x \<noteq> (0::'b) &&& y \<noteq> (0::'b) &&& \<exists>k. x = k *s y
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
x \<noteq> (0::'b)
y \<noteq> (0::'b)
\<exists>k. x = k *s y

goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
from \<open>\<exists>k. x = scale k y\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. x = k *s y
[PROOF STEP]
obtain k where "x = scale k y"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. x = k *s y

goal (1 subgoal):
 1. (\<And>k. x = k *s y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = k *s y

goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
with \<open>x \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> (0::'b)
x = k *s y
[PROOF STEP]
have "k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'b)
x = k *s y

goal (1 subgoal):
 1. k \<noteq> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k \<noteq> (0::'a)

goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
with \<open>x = scale k y\<close>
[PROOF STATE]
proof (chain)
picking this:
x = k *s y
k \<noteq> (0::'a)
[PROOF STEP]
have "y = scale (1/k) x"
[PROOF STATE]
proof (prove)
using this:
x = k *s y
k \<noteq> (0::'a)

goal (1 subgoal):
 1. y = ((1::'a) / k) *s x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y = ((1::'a) / k) *s x

goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
with \<open>x \<noteq> 0\<close> and \<open>y \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> (0::'b)
y \<noteq> (0::'b)
y = ((1::'a) / k) *s x
[PROOF STEP]
have "(y, x) \<in> local.proportionality"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'b)
y \<noteq> (0::'b)
y = ((1::'a) / k) *s x

goal (1 subgoal):
 1. (y, x) \<in> local.proportionality
[PROOF STEP]
unfolding proportionality_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'b)
y \<noteq> (0::'b)
y = ((1::'a) / k) *s x

goal (1 subgoal):
 1. (y, x) \<in> {(x, y). x \<noteq> (0::'b) \<and> y \<noteq> (0::'b) \<and> (\<exists>k. x = k *s y)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y, x) \<in> local.proportionality

goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?x2, ?y2) \<in> local.proportionality \<Longrightarrow> (?y2, ?x2) \<in> local.proportionality

goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
thus "sym local.proportionality"
[PROOF STATE]
proof (prove)
using this:
(?x2, ?y2) \<in> local.proportionality \<Longrightarrow> (?y2, ?x2) \<in> local.proportionality

goal (1 subgoal):
 1. sym local.proportionality
[PROOF STEP]
unfolding sym_def
[PROOF STATE]
proof (prove)
using this:
(?x2, ?y2) \<in> local.proportionality \<Longrightarrow> (?y2, ?x2) \<in> local.proportionality

goal (1 subgoal):
 1. \<forall>x y. (x, y) \<in> local.proportionality \<longrightarrow> (y, x) \<in> local.proportionality
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sym local.proportionality

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proportionality_trans: "trans local.proportionality"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
fix x y z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
assume "(x, y) \<in> local.proportionality" and "(y, z) \<in> local.proportionality"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> local.proportionality
(y, z) \<in> local.proportionality

goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
hence "x \<noteq> 0" and "z \<noteq> 0" and "\<exists>j. x = scale j y" and "\<exists>k. y = scale k z"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> local.proportionality
(y, z) \<in> local.proportionality

goal (1 subgoal):
 1. (x \<noteq> (0::'b) &&& z \<noteq> (0::'b)) &&& \<exists>j. x = j *s y &&& \<exists>k. y = k *s z
[PROOF STEP]
unfolding proportionality_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). x \<noteq> (0::'b) \<and> y \<noteq> (0::'b) \<and> (\<exists>k. x = k *s y)}
(y, z) \<in> {(x, y). x \<noteq> (0::'b) \<and> y \<noteq> (0::'b) \<and> (\<exists>k. x = k *s y)}

goal (1 subgoal):
 1. (x \<noteq> (0::'b) &&& z \<noteq> (0::'b)) &&& \<exists>j. x = j *s y &&& \<exists>k. y = k *s z
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
x \<noteq> (0::'b)
z \<noteq> (0::'b)
\<exists>j. x = j *s y
\<exists>k. y = k *s z

goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
from \<open>\<exists>j. x = scale j y\<close> and \<open>\<exists>k. y = scale k z\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. x = j *s y
\<exists>k. y = k *s z
[PROOF STEP]
obtain j and k where "x = scale j y" and "y = scale k z"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. x = j *s y
\<exists>k. y = k *s z

goal (1 subgoal):
 1. (\<And>j k. \<lbrakk>x = j *s y; y = k *s z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto+
[PROOF STATE]
proof (state)
this:
x = j *s y
y = k *s z

goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
hence "x = scale (j * k) z"
[PROOF STATE]
proof (prove)
using this:
x = j *s y
y = k *s z

goal (1 subgoal):
 1. x = (j * k) *s z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = (j * k) *s z

goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
with \<open>x \<noteq> 0\<close> and \<open>z \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> (0::'b)
z \<noteq> (0::'b)
x = (j * k) *s z
[PROOF STEP]
have "(x, z) \<in> local.proportionality"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'b)
z \<noteq> (0::'b)
x = (j * k) *s z

goal (1 subgoal):
 1. (x, z) \<in> local.proportionality
[PROOF STEP]
unfolding proportionality_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> (0::'b)
z \<noteq> (0::'b)
x = (j * k) *s z

goal (1 subgoal):
 1. (x, z) \<in> {(x, y). x \<noteq> (0::'b) \<and> y \<noteq> (0::'b) \<and> (\<exists>k. x = k *s y)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, z) \<in> local.proportionality

goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?x2, ?y2) \<in> local.proportionality; (?y2, ?z2) \<in> local.proportionality\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> local.proportionality

goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
thus "trans local.proportionality"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> local.proportionality; (?y2, ?z2) \<in> local.proportionality\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> local.proportionality

goal (1 subgoal):
 1. trans local.proportionality
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> local.proportionality; (?y2, ?z2) \<in> local.proportionality\<rbrakk> \<Longrightarrow> (?x2, ?z2) \<in> local.proportionality

goal (1 subgoal):
 1. \<forall>x y z. (x, y) \<in> local.proportionality \<longrightarrow> (y, z) \<in> local.proportionality \<longrightarrow> (x, z) \<in> local.proportionality
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
trans local.proportionality

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem proportionality_equiv: "equiv local.non_zero_vectors local.proportionality"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equiv local.non_zero_vectors local.proportionality
[PROOF STEP]
unfolding equiv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on local.non_zero_vectors local.proportionality \<and> sym local.proportionality \<and> trans local.proportionality
[PROOF STEP]
by (simp add:
      proportionality_refl_on
      proportionality_sym
      proportionality_trans)


[STATEMENT]
lemma invertible_proportionality_equiv:
  "equiv (Collect invertible :: (real^('n::finite)^'n) set)
  invertible_proportionality"
  (is "equiv ?invs _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equiv (Collect invertible) invertible_proportionality
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. equiv (Collect invertible) invertible_proportionality
[PROOF STEP]
from zero_not_invertible
[PROOF STATE]
proof (chain)
picking this:
\<not> invertible 0
[PROOF STEP]
have "real_vector.non_zero_vectors \<inter> ?invs = ?invs"
[PROOF STATE]
proof (prove)
using this:
\<not> invertible 0

goal (1 subgoal):
 1. non_zero_vectors \<inter> Collect invertible = Collect invertible
[PROOF STEP]
unfolding real_vector.non_zero_vectors_def
[PROOF STATE]
proof (prove)
using this:
\<not> invertible 0

goal (1 subgoal):
 1. {x. x \<noteq> 0} \<inter> Collect invertible = Collect invertible
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
non_zero_vectors \<inter> Collect invertible = Collect invertible

goal (1 subgoal):
 1. equiv (Collect invertible) invertible_proportionality
[PROOF STEP]
from equiv_restrict and real_vector.proportionality_equiv
[PROOF STATE]
proof (chain)
picking this:
equiv ?A ?r \<Longrightarrow> equiv (?A \<inter> ?B) (Restr ?r ?B)
equiv non_zero_vectors proportionality
[PROOF STEP]
have "equiv (real_vector.non_zero_vectors \<inter> ?invs) invertible_proportionality"
[PROOF STATE]
proof (prove)
using this:
equiv ?A ?r \<Longrightarrow> equiv (?A \<inter> ?B) (Restr ?r ?B)
equiv non_zero_vectors proportionality

goal (1 subgoal):
 1. equiv (non_zero_vectors \<inter> Collect invertible) invertible_proportionality
[PROOF STEP]
unfolding invertible_proportionality_def
[PROOF STATE]
proof (prove)
using this:
equiv ?A ?r \<Longrightarrow> equiv (?A \<inter> ?B) (Restr ?r ?B)
equiv non_zero_vectors proportionality

goal (1 subgoal):
 1. equiv (non_zero_vectors \<inter> Collect invertible) (Restr proportionality (Collect invertible))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
equiv (non_zero_vectors \<inter> Collect invertible) invertible_proportionality

goal (1 subgoal):
 1. equiv (Collect invertible) invertible_proportionality
[PROOF STEP]
with \<open>real_vector.non_zero_vectors \<inter> ?invs = ?invs\<close>
[PROOF STATE]
proof (chain)
picking this:
non_zero_vectors \<inter> Collect invertible = Collect invertible
equiv (non_zero_vectors \<inter> Collect invertible) invertible_proportionality
[PROOF STEP]
show "equiv ?invs invertible_proportionality"
[PROOF STATE]
proof (prove)
using this:
non_zero_vectors \<inter> Collect invertible = Collect invertible
equiv (non_zero_vectors \<inter> Collect invertible) invertible_proportionality

goal (1 subgoal):
 1. equiv (Collect invertible) invertible_proportionality
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
equiv (Collect invertible) invertible_proportionality

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_rep_in: "proj2_rep x \<in> Rep_proj2 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep x \<in> Rep_proj2 x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_rep x \<in> Rep_proj2 x
[PROOF STEP]
let ?v = "proj2_rep x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_rep x \<in> Rep_proj2 x
[PROOF STEP]
from quotient_element_nonempty and
    real_vector.proportionality_equiv and
    Rep_proj2 [of x]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>equiv ?A ?r; ?X \<in> ?A // ?r\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> ?X
equiv non_zero_vectors proportionality
Rep_proj2 x \<in> non_zero_vectors // proportionality
[PROOF STEP]
have "\<exists> w. w \<in> Rep_proj2 x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>equiv ?A ?r; ?X \<in> ?A // ?r\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> ?X
equiv non_zero_vectors proportionality
Rep_proj2 x \<in> non_zero_vectors // proportionality

goal (1 subgoal):
 1. \<exists>w. w \<in> Rep_proj2 x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>w. w \<in> Rep_proj2 x

goal (1 subgoal):
 1. proj2_rep x \<in> Rep_proj2 x
[PROOF STEP]
with someI_ex [of "\<lambda> z. z \<in> Rep_proj2 x"]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xa. xa \<in> Rep_proj2 x \<Longrightarrow> (SOME xa. xa \<in> Rep_proj2 x) \<in> Rep_proj2 x
\<exists>w. w \<in> Rep_proj2 x
[PROOF STEP]
show "?v \<in> Rep_proj2 x"
[PROOF STATE]
proof (prove)
using this:
\<exists>xa. xa \<in> Rep_proj2 x \<Longrightarrow> (SOME xa. xa \<in> Rep_proj2 x) \<in> Rep_proj2 x
\<exists>w. w \<in> Rep_proj2 x

goal (1 subgoal):
 1. proj2_rep x \<in> Rep_proj2 x
[PROOF STEP]
unfolding proj2_rep_def
[PROOF STATE]
proof (prove)
using this:
\<exists>xa. xa \<in> Rep_proj2 x \<Longrightarrow> (SOME xa. xa \<in> Rep_proj2 x) \<in> Rep_proj2 x
\<exists>w. w \<in> Rep_proj2 x

goal (1 subgoal):
 1. (SOME v. v \<in> Rep_proj2 x) \<in> Rep_proj2 x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep x \<in> Rep_proj2 x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_rep_non_zero: "proj2_rep x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep x \<noteq> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_rep x \<noteq> 0
[PROOF STEP]
from
    Union_quotient [of real_vector.non_zero_vectors real_vector.proportionality]
    and real_vector.proportionality_equiv
    and Rep_proj2 [of x] and proj2_rep_in [of x]
[PROOF STATE]
proof (chain)
picking this:
equiv non_zero_vectors proportionality \<Longrightarrow> \<Union> (non_zero_vectors // proportionality) = non_zero_vectors
equiv non_zero_vectors proportionality
Rep_proj2 x \<in> non_zero_vectors // proportionality
proj2_rep x \<in> Rep_proj2 x
[PROOF STEP]
have "proj2_rep x \<in> real_vector.non_zero_vectors"
[PROOF STATE]
proof (prove)
using this:
equiv non_zero_vectors proportionality \<Longrightarrow> \<Union> (non_zero_vectors // proportionality) = non_zero_vectors
equiv non_zero_vectors proportionality
Rep_proj2 x \<in> non_zero_vectors // proportionality
proj2_rep x \<in> Rep_proj2 x

goal (1 subgoal):
 1. proj2_rep x \<in> non_zero_vectors
[PROOF STEP]
unfolding quotient_def
[PROOF STATE]
proof (prove)
using this:
equiv non_zero_vectors proportionality \<Longrightarrow> \<Union> (\<Union>x\<in>non_zero_vectors. {proportionality `` {x}}) = non_zero_vectors
equiv non_zero_vectors proportionality
Rep_proj2 x \<in> (\<Union>x\<in>non_zero_vectors. {proportionality `` {x}})
proj2_rep x \<in> Rep_proj2 x

goal (1 subgoal):
 1. proj2_rep x \<in> non_zero_vectors
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_rep x \<in> non_zero_vectors

goal (1 subgoal):
 1. proj2_rep x \<noteq> 0
[PROOF STEP]
thus "proj2_rep x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
proj2_rep x \<in> non_zero_vectors

goal (1 subgoal):
 1. proj2_rep x \<noteq> 0
[PROOF STEP]
unfolding real_vector.non_zero_vectors_def
[PROOF STATE]
proof (prove)
using this:
proj2_rep x \<in> {x. x \<noteq> 0}

goal (1 subgoal):
 1. proj2_rep x \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep x \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_rep_abs:
  fixes v :: "real^3"
  assumes "v \<in> real_vector.non_zero_vectors"
  shows "(v, proj2_rep (proj2_abs v)) \<in> real_vector.proportionality"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, proj2_rep (proj2_abs v)) \<in> proportionality
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v, proj2_rep (proj2_abs v)) \<in> proportionality
[PROOF STEP]
from \<open>v \<in> real_vector.non_zero_vectors\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<in> non_zero_vectors
[PROOF STEP]
have "real_vector.proportionality `` {v} \<in> (real_vector.non_zero_vectors :: (real^3) set)//real_vector.proportionality"
[PROOF STATE]
proof (prove)
using this:
v \<in> non_zero_vectors

goal (1 subgoal):
 1. proportionality `` {v} \<in> non_zero_vectors // proportionality
[PROOF STEP]
unfolding quotient_def
[PROOF STATE]
proof (prove)
using this:
v \<in> non_zero_vectors

goal (1 subgoal):
 1. proportionality `` {v} \<in> (\<Union>x\<in>non_zero_vectors. {proportionality `` {x}})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proportionality `` {v} \<in> non_zero_vectors // proportionality

goal (1 subgoal):
 1. (v, proj2_rep (proj2_abs v)) \<in> proportionality
[PROOF STEP]
with Abs_proj2_inverse
[PROOF STATE]
proof (chain)
picking this:
?y \<in> non_zero_vectors // proportionality \<Longrightarrow> Rep_proj2 (Abs_proj2 ?y) = ?y
proportionality `` {v} \<in> non_zero_vectors // proportionality
[PROOF STEP]
have "Rep_proj2 (proj2_abs v) = real_vector.proportionality `` {v}"
[PROOF STATE]
proof (prove)
using this:
?y \<in> non_zero_vectors // proportionality \<Longrightarrow> Rep_proj2 (Abs_proj2 ?y) = ?y
proportionality `` {v} \<in> non_zero_vectors // proportionality

goal (1 subgoal):
 1. Rep_proj2 (proj2_abs v) = proportionality `` {v}
[PROOF STEP]
unfolding proj2_abs_def
[PROOF STATE]
proof (prove)
using this:
?y \<in> non_zero_vectors // proportionality \<Longrightarrow> Rep_proj2 (Abs_proj2 ?y) = ?y
proportionality `` {v} \<in> non_zero_vectors // proportionality

goal (1 subgoal):
 1. Rep_proj2 (Abs_proj2 (proportionality `` {v})) = proportionality `` {v}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rep_proj2 (proj2_abs v) = proportionality `` {v}

goal (1 subgoal):
 1. (v, proj2_rep (proj2_abs v)) \<in> proportionality
[PROOF STEP]
with proj2_rep_in
[PROOF STATE]
proof (chain)
picking this:
proj2_rep ?x \<in> Rep_proj2 ?x
Rep_proj2 (proj2_abs v) = proportionality `` {v}
[PROOF STEP]
have "proj2_rep (proj2_abs v) \<in> real_vector.proportionality `` {v}"
[PROOF STATE]
proof (prove)
using this:
proj2_rep ?x \<in> Rep_proj2 ?x
Rep_proj2 (proj2_abs v) = proportionality `` {v}

goal (1 subgoal):
 1. proj2_rep (proj2_abs v) \<in> proportionality `` {v}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_rep (proj2_abs v) \<in> proportionality `` {v}

goal (1 subgoal):
 1. (v, proj2_rep (proj2_abs v)) \<in> proportionality
[PROOF STEP]
thus "(v, proj2_rep (proj2_abs v)) \<in> real_vector.proportionality"
[PROOF STATE]
proof (prove)
using this:
proj2_rep (proj2_abs v) \<in> proportionality `` {v}

goal (1 subgoal):
 1. (v, proj2_rep (proj2_abs v)) \<in> proportionality
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v, proj2_rep (proj2_abs v)) \<in> proportionality

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_abs_rep: "proj2_abs (proj2_rep x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_abs (proj2_rep x) = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_abs (proj2_rep x) = x
[PROOF STEP]
from partition_Image_element
  [of real_vector.non_zero_vectors
    real_vector.proportionality
    "Rep_proj2 x"
    "proj2_rep x"]
    and real_vector.proportionality_equiv
    and Rep_proj2 [of x] and proj2_rep_in [of x]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>equiv non_zero_vectors proportionality; Rep_proj2 x \<in> non_zero_vectors // proportionality; proj2_rep x \<in> Rep_proj2 x\<rbrakk> \<Longrightarrow> proportionality `` {proj2_rep x} = Rep_proj2 x
equiv non_zero_vectors proportionality
Rep_proj2 x \<in> non_zero_vectors // proportionality
proj2_rep x \<in> Rep_proj2 x
[PROOF STEP]
have "real_vector.proportionality `` {proj2_rep x} = Rep_proj2 x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>equiv non_zero_vectors proportionality; Rep_proj2 x \<in> non_zero_vectors // proportionality; proj2_rep x \<in> Rep_proj2 x\<rbrakk> \<Longrightarrow> proportionality `` {proj2_rep x} = Rep_proj2 x
equiv non_zero_vectors proportionality
Rep_proj2 x \<in> non_zero_vectors // proportionality
proj2_rep x \<in> Rep_proj2 x

goal (1 subgoal):
 1. proportionality `` {proj2_rep x} = Rep_proj2 x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proportionality `` {proj2_rep x} = Rep_proj2 x

goal (1 subgoal):
 1. proj2_abs (proj2_rep x) = x
[PROOF STEP]
with Rep_proj2_inverse
[PROOF STATE]
proof (chain)
picking this:
Abs_proj2 (Rep_proj2 ?x) = ?x
proportionality `` {proj2_rep x} = Rep_proj2 x
[PROOF STEP]
show "proj2_abs (proj2_rep x) = x"
[PROOF STATE]
proof (prove)
using this:
Abs_proj2 (Rep_proj2 ?x) = ?x
proportionality `` {proj2_rep x} = Rep_proj2 x

goal (1 subgoal):
 1. proj2_abs (proj2_rep x) = x
[PROOF STEP]
unfolding proj2_abs_def
[PROOF STATE]
proof (prove)
using this:
Abs_proj2 (Rep_proj2 ?x) = ?x
proportionality `` {proj2_rep x} = Rep_proj2 x

goal (1 subgoal):
 1. Abs_proj2 (proportionality `` {proj2_rep x}) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_abs (proj2_rep x) = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_abs_mult:
  assumes "c \<noteq> 0"
  shows "proj2_abs (c *\<^sub>R v) = proj2_abs v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_abs (c *\<^sub>R v) = proj2_abs v
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> proj2_abs (c *\<^sub>R v) = proj2_abs v
 2. \<not> ?P \<Longrightarrow> proj2_abs (c *\<^sub>R v) = proj2_abs v
[PROOF STEP]
assume "v = 0"
[PROOF STATE]
proof (state)
this:
v = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> proj2_abs (c *\<^sub>R v) = proj2_abs v
 2. \<not> ?P \<Longrightarrow> proj2_abs (c *\<^sub>R v) = proj2_abs v
[PROOF STEP]
thus "proj2_abs (c *\<^sub>R v) = proj2_abs v"
[PROOF STATE]
proof (prove)
using this:
v = 0

goal (1 subgoal):
 1. proj2_abs (c *\<^sub>R v) = proj2_abs v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_abs (c *\<^sub>R v) = proj2_abs v

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> proj2_abs (c *\<^sub>R v) = proj2_abs v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> proj2_abs (c *\<^sub>R v) = proj2_abs v
[PROOF STEP]
assume "v \<noteq> 0"
[PROOF STATE]
proof (state)
this:
v \<noteq> 0

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> proj2_abs (c *\<^sub>R v) = proj2_abs v
[PROOF STEP]
with \<open>c \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> 0
v \<noteq> 0
[PROOF STEP]
have "(c *\<^sub>R v, v) \<in> real_vector.proportionality"
    and "c *\<^sub>R v \<in> real_vector.non_zero_vectors"
    and "v \<in> real_vector.non_zero_vectors"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
v \<noteq> 0

goal (1 subgoal):
 1. (c *\<^sub>R v, v) \<in> proportionality &&& c *\<^sub>R v \<in> non_zero_vectors &&& v \<in> non_zero_vectors
[PROOF STEP]
unfolding real_vector.proportionality_def
      and real_vector.non_zero_vectors_def
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
v \<noteq> 0

goal (1 subgoal):
 1. (c *\<^sub>R v, v) \<in> {(x, y). x \<noteq> 0 \<and> y \<noteq> 0 \<and> (\<exists>k. x = k *\<^sub>R y)} &&& c *\<^sub>R v \<in> {x. x \<noteq> 0} &&& v \<in> {x. x \<noteq> 0}
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
(c *\<^sub>R v, v) \<in> proportionality
c *\<^sub>R v \<in> non_zero_vectors
v \<in> non_zero_vectors

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> proj2_abs (c *\<^sub>R v) = proj2_abs v
[PROOF STEP]
with eq_equiv_class_iff
  [of real_vector.non_zero_vectors
    real_vector.proportionality
    "c *\<^sub>R v"
    v]
    and real_vector.proportionality_equiv
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>equiv non_zero_vectors proportionality; c *\<^sub>R v \<in> non_zero_vectors; v \<in> non_zero_vectors\<rbrakk> \<Longrightarrow> (proportionality `` {c *\<^sub>R v} = proportionality `` {v}) = ((c *\<^sub>R v, v) \<in> proportionality)
equiv non_zero_vectors proportionality
(c *\<^sub>R v, v) \<in> proportionality
c *\<^sub>R v \<in> non_zero_vectors
v \<in> non_zero_vectors
[PROOF STEP]
have "real_vector.proportionality `` {c *\<^sub>R v} =
    real_vector.proportionality `` {v}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>equiv non_zero_vectors proportionality; c *\<^sub>R v \<in> non_zero_vectors; v \<in> non_zero_vectors\<rbrakk> \<Longrightarrow> (proportionality `` {c *\<^sub>R v} = proportionality `` {v}) = ((c *\<^sub>R v, v) \<in> proportionality)
equiv non_zero_vectors proportionality
(c *\<^sub>R v, v) \<in> proportionality
c *\<^sub>R v \<in> non_zero_vectors
v \<in> non_zero_vectors

goal (1 subgoal):
 1. proportionality `` {c *\<^sub>R v} = proportionality `` {v}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proportionality `` {c *\<^sub>R v} = proportionality `` {v}

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> proj2_abs (c *\<^sub>R v) = proj2_abs v
[PROOF STEP]
thus "proj2_abs (c *\<^sub>R v) = proj2_abs v"
[PROOF STATE]
proof (prove)
using this:
proportionality `` {c *\<^sub>R v} = proportionality `` {v}

goal (1 subgoal):
 1. proj2_abs (c *\<^sub>R v) = proj2_abs v
[PROOF STEP]
unfolding proj2_abs_def
[PROOF STATE]
proof (prove)
using this:
proportionality `` {c *\<^sub>R v} = proportionality `` {v}

goal (1 subgoal):
 1. Abs_proj2 (proportionality `` {c *\<^sub>R v}) = Abs_proj2 (proportionality `` {v})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_abs (c *\<^sub>R v) = proj2_abs v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_abs_mult_rep:
  assumes "c \<noteq> 0"
  shows "proj2_abs (c *\<^sub>R proj2_rep x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_abs (c *\<^sub>R proj2_rep x) = x
[PROOF STEP]
using proj2_abs_mult and proj2_abs_rep and assms
[PROOF STATE]
proof (prove)
using this:
?c \<noteq> 0 \<Longrightarrow> proj2_abs (?c *\<^sub>R ?v) = proj2_abs ?v
proj2_abs (proj2_rep ?x) = ?x
c \<noteq> 0

goal (1 subgoal):
 1. proj2_abs (c *\<^sub>R proj2_rep x) = x
[PROOF STEP]
by simp


[STATEMENT]
lemma proj2_rep_inj: "inj proj2_rep"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj proj2_rep
[PROOF STEP]
by (simp add: inj_on_inverseI [of UNIV proj2_abs proj2_rep] proj2_abs_rep)


[STATEMENT]
lemma proj2_rep_abs2:
  assumes "v \<noteq> 0"
  shows "\<exists> k. k \<noteq> 0 \<and> proj2_rep (proj2_abs v) = k *\<^sub>R v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs v) = k *\<^sub>R v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs v) = k *\<^sub>R v
[PROOF STEP]
from proj2_rep_abs [of v] and \<open>v \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<in> non_zero_vectors \<Longrightarrow> (v, proj2_rep (proj2_abs v)) \<in> proportionality
v \<noteq> 0
[PROOF STEP]
have "(v, proj2_rep (proj2_abs v)) \<in> real_vector.proportionality"
[PROOF STATE]
proof (prove)
using this:
v \<in> non_zero_vectors \<Longrightarrow> (v, proj2_rep (proj2_abs v)) \<in> proportionality
v \<noteq> 0

goal (1 subgoal):
 1. (v, proj2_rep (proj2_abs v)) \<in> proportionality
[PROOF STEP]
unfolding real_vector.non_zero_vectors_def
[PROOF STATE]
proof (prove)
using this:
v \<in> {x. x \<noteq> 0} \<Longrightarrow> (v, proj2_rep (proj2_abs v)) \<in> proportionality
v \<noteq> 0

goal (1 subgoal):
 1. (v, proj2_rep (proj2_abs v)) \<in> proportionality
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v, proj2_rep (proj2_abs v)) \<in> proportionality

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs v) = k *\<^sub>R v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, proj2_rep (proj2_abs v)) \<in> proportionality
[PROOF STEP]
obtain c where "v = c *\<^sub>R proj2_rep (proj2_abs v)"
[PROOF STATE]
proof (prove)
using this:
(v, proj2_rep (proj2_abs v)) \<in> proportionality

goal (1 subgoal):
 1. (\<And>c. v = c *\<^sub>R proj2_rep (proj2_abs v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding real_vector.proportionality_def
[PROOF STATE]
proof (prove)
using this:
(v, proj2_rep (proj2_abs v)) \<in> {(x, y). x \<noteq> 0 \<and> y \<noteq> 0 \<and> (\<exists>k. x = k *\<^sub>R y)}

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

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

goal (1 subgoal):
 1. c \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

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

goal (1 subgoal):
 1. 1 / c \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 / c \<noteq> 0

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

goal (1 subgoal):
 1. (1 / c) *\<^sub>R v = (1 / c) *\<^sub>R c *\<^sub>R proj2_rep (proj2_abs v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1 / c) *\<^sub>R v = (1 / c) *\<^sub>R c *\<^sub>R proj2_rep (proj2_abs v)

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

goal (1 subgoal):
 1. proj2_rep (proj2_abs v) = (1 / c) *\<^sub>R v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep (proj2_abs v) = (1 / c) *\<^sub>R v

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

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs v) = k *\<^sub>R v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs v) = k *\<^sub>R v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_abs_abs_mult:
  assumes "proj2_abs v = proj2_abs w" and "w \<noteq> 0"
  shows "\<exists> c. v = c *\<^sub>R w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
 2. \<not> ?P \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
assume "v = 0"
[PROOF STATE]
proof (state)
this:
v = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
 2. \<not> ?P \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
hence "v = 0 *\<^sub>R w"
[PROOF STATE]
proof (prove)
using this:
v = 0

goal (1 subgoal):
 1. v = 0 *\<^sub>R w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v = 0 *\<^sub>R w

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
 2. \<not> ?P \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
thus "\<exists> c. v = c *\<^sub>R w"
[PROOF STATE]
proof (prove)
using this:
v = 0 *\<^sub>R w

goal (1 subgoal):
 1. \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>c. v = c *\<^sub>R w

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
assume "v \<noteq> 0"
[PROOF STATE]
proof (state)
this:
v \<noteq> 0

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
from \<open>proj2_abs v = proj2_abs w\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_abs v = proj2_abs w
[PROOF STEP]
have "proj2_rep (proj2_abs v) = proj2_rep (proj2_abs w)"
[PROOF STATE]
proof (prove)
using this:
proj2_abs v = proj2_abs w

goal (1 subgoal):
 1. proj2_rep (proj2_abs v) = proj2_rep (proj2_abs w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep (proj2_abs v) = proj2_rep (proj2_abs w)

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

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

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

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

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
hence "(1/j) *\<^sub>R j *\<^sub>R v = (1/j) *\<^sub>R k *\<^sub>R w"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
j *\<^sub>R v = k *\<^sub>R w

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

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
with \<open>j \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
j \<noteq> 0
(1 / j) *\<^sub>R j *\<^sub>R v = (1 / j) *\<^sub>R k *\<^sub>R w
[PROOF STEP]
have "v = (k/j) *\<^sub>R w"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
(1 / j) *\<^sub>R j *\<^sub>R v = (1 / j) *\<^sub>R k *\<^sub>R w

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

goal (1 subgoal):
 1. v \<noteq> 0 \<Longrightarrow> \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
thus "\<exists> c. v = c *\<^sub>R w"
[PROOF STATE]
proof (prove)
using this:
v = (k / j) *\<^sub>R w

goal (1 subgoal):
 1. \<exists>c. v = c *\<^sub>R w
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>c. v = c *\<^sub>R w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dependent_proj2_abs:
  assumes "p \<noteq> 0" and "q \<noteq> 0" and "i \<noteq> 0 \<or> j \<noteq> 0" and "i *\<^sub>R p + j *\<^sub>R q = 0"
  shows "proj2_abs p = proj2_abs q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_abs p = proj2_abs q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_abs p = proj2_abs q
[PROOF STEP]
have "i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = 0 \<Longrightarrow> False
[PROOF STEP]
assume "i = 0"
[PROOF STATE]
proof (state)
this:
i = 0

goal (1 subgoal):
 1. i = 0 \<Longrightarrow> False
[PROOF STEP]
with \<open>i \<noteq> 0 \<or> j \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> 0 \<or> j \<noteq> 0
i = 0
[PROOF STEP]
have "j \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0 \<or> j \<noteq> 0
i = 0

goal (1 subgoal):
 1. j \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j \<noteq> 0

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i \<noteq> 0

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

goal (1 subgoal):
 1. j \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<noteq> 0

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

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

goal (1 subgoal):
 1. proj2_abs p = proj2_abs q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proj2_abs p = proj2_abs (i *\<^sub>R p)

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

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

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

goal (1 subgoal):
 1. proj2_abs p = proj2_abs q
[PROOF STEP]
from \<open>j \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
j \<noteq> 0
[PROOF STEP]
have "\<dots> = proj2_abs q"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0

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

goal (1 subgoal):
 1. proj2_abs p = proj2_abs q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
proj2_abs p = proj2_abs q
[PROOF STEP]
show "proj2_abs p = proj2_abs q"
[PROOF STATE]
proof (prove)
using this:
proj2_abs p = proj2_abs q

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_rep_dependent:
  assumes "i *\<^sub>R proj2_rep v + j *\<^sub>R proj2_rep w = 0"
  (is "i *\<^sub>R ?p + j *\<^sub>R ?q = 0")
  and "i \<noteq> 0 \<or> j \<noteq> 0"
  shows "v = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v = w
[PROOF STEP]
have "?p \<noteq> 0" and "?q \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep v \<noteq> 0 &&& proj2_rep w \<noteq> 0
[PROOF STEP]
by (rule proj2_rep_non_zero)+
[PROOF STATE]
proof (state)
this:
proj2_rep v \<noteq> 0
proj2_rep w \<noteq> 0

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

goal (1 subgoal):
 1. proj2_abs (proj2_rep v) = proj2_abs (proj2_rep w)
[PROOF STEP]
by (simp add: dependent_proj2_abs)
[PROOF STATE]
proof (state)
this:
proj2_abs (proj2_rep v) = proj2_abs (proj2_rep w)

goal (1 subgoal):
 1. v = w
[PROOF STEP]
thus "v = w"
[PROOF STATE]
proof (prove)
using this:
proj2_abs (proj2_rep v) = proj2_abs (proj2_rep w)

goal (1 subgoal):
 1. v = w
[PROOF STEP]
by (simp add: proj2_abs_rep)
[PROOF STATE]
proof (state)
this:
v = w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_rep_independent:
  assumes "p \<noteq> q"
  shows "independent {proj2_rep p, proj2_rep q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. independent {proj2_rep p, proj2_rep q}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dependent {proj2_rep p, proj2_rep q} \<Longrightarrow> False
[PROOF STEP]
let ?p' = "proj2_rep p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dependent {proj2_rep p, proj2_rep q} \<Longrightarrow> False
[PROOF STEP]
let ?q' = "proj2_rep q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dependent {proj2_rep p, proj2_rep q} \<Longrightarrow> False
[PROOF STEP]
let ?S = "{?p', ?q'}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dependent {proj2_rep p, proj2_rep q} \<Longrightarrow> False
[PROOF STEP]
assume "dependent ?S"
[PROOF STATE]
proof (state)
this:
dependent {proj2_rep p, proj2_rep q}

goal (1 subgoal):
 1. dependent {proj2_rep p, proj2_rep q} \<Longrightarrow> False
[PROOF STEP]
from proj2_rep_inj and \<open>p \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
inj proj2_rep
p \<noteq> q
[PROOF STEP]
have "?p' \<noteq> ?q'"
[PROOF STATE]
proof (prove)
using this:
inj proj2_rep
p \<noteq> q

goal (1 subgoal):
 1. proj2_rep p \<noteq> proj2_rep q
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. proj2_rep x = proj2_rep y \<longrightarrow> x = y
p \<noteq> q

goal (1 subgoal):
 1. proj2_rep p \<noteq> proj2_rep q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_rep p \<noteq> proj2_rep q

goal (1 subgoal):
 1. dependent {proj2_rep p, proj2_rep q} \<Longrightarrow> False
[PROOF STEP]
with dependent_explicit_2 [of ?p' ?q'] and \<open>dependent ?S\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_rep p \<noteq> proj2_rep q \<Longrightarrow> dependent {proj2_rep p, proj2_rep q} = (\<exists>i j. (i \<noteq> 0 \<or> j \<noteq> 0) \<and> i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q = 0)
dependent {proj2_rep p, proj2_rep q}
proj2_rep p \<noteq> proj2_rep q
[PROOF STEP]
obtain i and j where "i *\<^sub>R ?p' + j *\<^sub>R ?q' = 0" and "i \<noteq> 0 \<or> j \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
proj2_rep p \<noteq> proj2_rep q \<Longrightarrow> dependent {proj2_rep p, proj2_rep q} = (\<exists>i j. (i \<noteq> 0 \<or> j \<noteq> 0) \<and> i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q = 0)
dependent {proj2_rep p, proj2_rep q}
proj2_rep p \<noteq> proj2_rep q

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

goal (1 subgoal):
 1. dependent {proj2_rep p, proj2_rep q} \<Longrightarrow> False
[PROOF STEP]
with proj2_rep_dependent
[PROOF STATE]
proof (chain)
picking this:
\<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
i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q = 0
i \<noteq> 0 \<or> j \<noteq> 0
[PROOF STEP]
have "p = q"
[PROOF STATE]
proof (prove)
using this:
\<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
i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q = 0
i \<noteq> 0 \<or> j \<noteq> 0

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

goal (1 subgoal):
 1. dependent {proj2_rep p, proj2_rep q} \<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


[STATEMENT]
lemma proj2_Col_abs:
  assumes "p \<noteq> 0" and "q \<noteq> 0" and "r \<noteq> 0" and "i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0"
  and "i *\<^sub>R p + j *\<^sub>R q + k *\<^sub>R r = 0"
  shows "proj2_Col (proj2_abs p) (proj2_abs q) (proj2_abs r)"
  (is "proj2_Col ?pp ?pq ?pr")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col (proj2_abs p) (proj2_abs q) (proj2_abs r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_Col (proj2_abs p) (proj2_abs q) (proj2_abs r)
[PROOF STEP]
from \<open>p \<noteq> 0\<close> and proj2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
[PROOF STEP]
obtain i' where "i' \<noteq> 0" and "proj2_rep ?pp = i' *\<^sub>R p" (is "?rp = _")
[PROOF STATE]
proof (prove)
using this:
p \<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>i'. \<lbrakk>i' \<noteq> 0; proj2_rep (proj2_abs p) = i' *\<^sub>R p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' \<noteq> 0
proj2_rep (proj2_abs p) = i' *\<^sub>R p

goal (1 subgoal):
 1. proj2_Col (proj2_abs p) (proj2_abs q) (proj2_abs r)
[PROOF STEP]
from \<open>q \<noteq> 0\<close> and proj2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
[PROOF STEP]
obtain j' where "j' \<noteq> 0" and "proj2_rep ?pq = j' *\<^sub>R q" (is "?rq = _")
[PROOF STATE]
proof (prove)
using this:
q \<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>j'. \<lbrakk>j' \<noteq> 0; proj2_rep (proj2_abs q) = j' *\<^sub>R q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j' \<noteq> 0
proj2_rep (proj2_abs q) = j' *\<^sub>R q

goal (1 subgoal):
 1. proj2_Col (proj2_abs p) (proj2_abs q) (proj2_abs r)
[PROOF STEP]
from \<open>r \<noteq> 0\<close> and proj2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
[PROOF STEP]
obtain k' where "k' \<noteq> 0" and "proj2_rep ?pr = k' *\<^sub>R r" (is "?rr = _")
[PROOF STATE]
proof (prove)
using this:
r \<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>k'. \<lbrakk>k' \<noteq> 0; proj2_rep (proj2_abs r) = k' *\<^sub>R r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k' \<noteq> 0
proj2_rep (proj2_abs r) = k' *\<^sub>R r

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

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

goal (1 subgoal):
 1. proj2_Col (proj2_abs p) (proj2_abs q) (proj2_abs r)
[PROOF STEP]
from \<open>i' \<noteq> 0\<close> and \<open>j' \<noteq> 0\<close> and \<open>k' \<noteq> 0\<close> and \<open>i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
i' \<noteq> 0
j' \<noteq> 0
k' \<noteq> 0
i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0
[PROOF STEP]
have "i/i' \<noteq> 0 \<or> j/j' \<noteq> 0 \<or> k/k' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
i' \<noteq> 0
j' \<noteq> 0
k' \<noteq> 0
i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0

goal (1 subgoal):
 1. i / i' \<noteq> 0 \<or> j / j' \<noteq> 0 \<or> k / k' \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i / i' \<noteq> 0 \<or> j / j' \<noteq> 0 \<or> k / k' \<noteq> 0

goal (1 subgoal):
 1. proj2_Col (proj2_abs p) (proj2_abs q) (proj2_abs r)
[PROOF STEP]
with \<open>(i/i') *\<^sub>R ?rp + (j/j') *\<^sub>R ?rq + (k/k') *\<^sub>R ?rr = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
(i / i') *\<^sub>R proj2_rep (proj2_abs p) + (j / j') *\<^sub>R proj2_rep (proj2_abs q) + (k / k') *\<^sub>R proj2_rep (proj2_abs r) = 0
i / i' \<noteq> 0 \<or> j / j' \<noteq> 0 \<or> k / k' \<noteq> 0
[PROOF STEP]
show "proj2_Col ?pp ?pq ?pr"
[PROOF STATE]
proof (prove)
using this:
(i / i') *\<^sub>R proj2_rep (proj2_abs p) + (j / j') *\<^sub>R proj2_rep (proj2_abs q) + (k / k') *\<^sub>R proj2_rep (proj2_abs r) = 0
i / i' \<noteq> 0 \<or> j / j' \<noteq> 0 \<or> k / k' \<noteq> 0

goal (1 subgoal):
 1. proj2_Col (proj2_abs p) (proj2_abs q) (proj2_abs r)
[PROOF STEP]
by (unfold proj2_Col_def, best)
[PROOF STATE]
proof (state)
this:
proj2_Col (proj2_abs p) (proj2_abs q) (proj2_abs r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_Col_permute:
  assumes "proj2_Col a b c"
  shows "proj2_Col a c b"
  and "proj2_Col b a c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col a c b &&& proj2_Col b a c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col a c b
 2. proj2_Col b a c
[PROOF STEP]
let ?a' = "proj2_rep a"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col a c b
 2. proj2_Col b a c
[PROOF STEP]
let ?b' = "proj2_rep b"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col a c b
 2. proj2_Col b a c
[PROOF STEP]
let ?c' = "proj2_rep c"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col a c b
 2. proj2_Col b a c
[PROOF STEP]
from \<open>proj2_Col a b c\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_Col a b c
[PROOF STEP]
obtain i and j and k where
    "i *\<^sub>R ?a' + j *\<^sub>R ?b' + k *\<^sub>R ?c' = 0"
    and "i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
proj2_Col a b c

goal (1 subgoal):
 1. (\<And>i j k. \<lbrakk>i *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep b + k *\<^sub>R proj2_rep c = 0; i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding proj2_Col_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i j k. i *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep b + k *\<^sub>R proj2_rep c = 0 \<and> (i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)

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

goal (2 subgoals):
 1. proj2_Col a c b
 2. proj2_Col b a c
[PROOF STEP]
from \<open>i *\<^sub>R ?a' + j *\<^sub>R ?b' + k *\<^sub>R ?c' = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
i *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep b + k *\<^sub>R proj2_rep c = 0
[PROOF STEP]
have "i *\<^sub>R ?a' + k *\<^sub>R ?c' + j *\<^sub>R ?b' = 0"
    and "j *\<^sub>R ?b' + i *\<^sub>R ?a' + k *\<^sub>R ?c' = 0"
[PROOF STATE]
proof (prove)
using this:
i *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep b + k *\<^sub>R proj2_rep c = 0

goal (1 subgoal):
 1. i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c + j *\<^sub>R proj2_rep b = 0 &&& j *\<^sub>R proj2_rep b + i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c = 0
[PROOF STEP]
by (simp_all add: ac_simps)
[PROOF STATE]
proof (state)
this:
i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c + j *\<^sub>R proj2_rep b = 0
j *\<^sub>R proj2_rep b + i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c = 0

goal (2 subgoals):
 1. proj2_Col a c b
 2. proj2_Col b a c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c + j *\<^sub>R proj2_rep b = 0
j *\<^sub>R proj2_rep b + i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c = 0

goal (2 subgoals):
 1. proj2_Col a c b
 2. proj2_Col b a c
[PROOF STEP]
from \<open>i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0
[PROOF STEP]
have "i \<noteq> 0 \<or> k \<noteq> 0 \<or> j \<noteq> 0" and "j \<noteq> 0 \<or> i \<noteq> 0 \<or> k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0

goal (1 subgoal):
 1. i \<noteq> 0 \<or> k \<noteq> 0 \<or> j \<noteq> 0 &&& j \<noteq> 0 \<or> i \<noteq> 0 \<or> k \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<noteq> 0 \<or> k \<noteq> 0 \<or> j \<noteq> 0
j \<noteq> 0 \<or> i \<noteq> 0 \<or> k \<noteq> 0

goal (2 subgoals):
 1. proj2_Col a c b
 2. proj2_Col b a c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c + j *\<^sub>R proj2_rep b = 0
j *\<^sub>R proj2_rep b + i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c = 0
i \<noteq> 0 \<or> k \<noteq> 0 \<or> j \<noteq> 0
j \<noteq> 0 \<or> i \<noteq> 0 \<or> k \<noteq> 0
[PROOF STEP]
show "proj2_Col a c b" and "proj2_Col b a c"
[PROOF STATE]
proof (prove)
using this:
i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c + j *\<^sub>R proj2_rep b = 0
j *\<^sub>R proj2_rep b + i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c = 0
i \<noteq> 0 \<or> k \<noteq> 0 \<or> j \<noteq> 0
j \<noteq> 0 \<or> i \<noteq> 0 \<or> k \<noteq> 0

goal (1 subgoal):
 1. proj2_Col a c b &&& proj2_Col b a c
[PROOF STEP]
unfolding proj2_Col_def
[PROOF STATE]
proof (prove)
using this:
i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c + j *\<^sub>R proj2_rep b = 0
j *\<^sub>R proj2_rep b + i *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c = 0
i \<noteq> 0 \<or> k \<noteq> 0 \<or> j \<noteq> 0
j \<noteq> 0 \<or> i \<noteq> 0 \<or> k \<noteq> 0

goal (1 subgoal):
 1. \<exists>i j k. i *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep c + k *\<^sub>R proj2_rep b = 0 \<and> (i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0) &&& \<exists>i j k. i *\<^sub>R proj2_rep b + j *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c = 0 \<and> (i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_Col a c b
proj2_Col b a c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_Col_coincide: "proj2_Col a a c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col a a c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_Col a a c
[PROOF STEP]
have "1 *\<^sub>R proj2_rep a + (-1) *\<^sub>R proj2_rep a + 0 *\<^sub>R proj2_rep c = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 *\<^sub>R proj2_rep a + - 1 *\<^sub>R proj2_rep a + 0 *\<^sub>R proj2_rep c = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 *\<^sub>R proj2_rep a + - 1 *\<^sub>R proj2_rep a + 0 *\<^sub>R proj2_rep c = 0

goal (1 subgoal):
 1. proj2_Col a a c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 *\<^sub>R proj2_rep a + - 1 *\<^sub>R proj2_rep a + 0 *\<^sub>R proj2_rep c = 0

goal (1 subgoal):
 1. proj2_Col a a c
[PROOF STEP]
have "(1::real) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<noteq> 0

goal (1 subgoal):
 1. proj2_Col a a c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 *\<^sub>R proj2_rep a + - 1 *\<^sub>R proj2_rep a + 0 *\<^sub>R proj2_rep c = 0
1 \<noteq> 0
[PROOF STEP]
show "proj2_Col a a c"
[PROOF STATE]
proof (prove)
using this:
1 *\<^sub>R proj2_rep a + - 1 *\<^sub>R proj2_rep a + 0 *\<^sub>R proj2_rep c = 0
1 \<noteq> 0

goal (1 subgoal):
 1. proj2_Col a a c
[PROOF STEP]
unfolding proj2_Col_def
[PROOF STATE]
proof (prove)
using this:
1 *\<^sub>R proj2_rep a + - 1 *\<^sub>R proj2_rep a + 0 *\<^sub>R proj2_rep c = 0
1 \<noteq> 0

goal (1 subgoal):
 1. \<exists>i j k. i *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep a + k *\<^sub>R proj2_rep c = 0 \<and> (i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
proj2_Col a a c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_Col_iff:
  assumes "a \<noteq> r"
  shows "proj2_Col a r t \<longleftrightarrow>
  t = a \<or> (\<exists> i. t = proj2_abs (i *\<^sub>R (proj2_rep a) + (proj2_rep r)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col a r t = (t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col a r t \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
let ?a' = "proj2_rep a"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col a r t \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
let ?r' = "proj2_rep r"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col a r t \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
let ?t' = "proj2_rep t"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col a r t \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col a r t \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
assume "proj2_Col a r t"
[PROOF STATE]
proof (state)
this:
proj2_Col a r t

goal (2 subgoals):
 1. proj2_Col a r t \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proj2_Col a r t
[PROOF STEP]
obtain h and j and k where
      "h *\<^sub>R ?a' + j *\<^sub>R ?r' + k *\<^sub>R ?t' = 0"
      and "h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
proj2_Col a r t

goal (1 subgoal):
 1. (\<And>h j k. \<lbrakk>h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0; h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding proj2_Col_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i j k. i *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0 \<and> (i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)

goal (1 subgoal):
 1. (\<And>h j k. \<lbrakk>h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0; h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0
h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0

goal (2 subgoals):
 1. proj2_Col a r t \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
show "t = a \<or> (\<exists> i. t = proj2_abs (i *\<^sub>R ?a' + ?r'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. \<not> ?P \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
assume "j = 0"
[PROOF STATE]
proof (state)
this:
j = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. \<not> ?P \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
with \<open>h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0
j = 0
[PROOF STEP]
have "h \<noteq> 0 \<or> k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0
j = 0

goal (1 subgoal):
 1. h \<noteq> 0 \<or> k \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h \<noteq> 0 \<or> k \<noteq> 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. \<not> ?P \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
with proj2_rep_dependent
        and \<open>h *\<^sub>R ?a' + j *\<^sub>R ?r' + k *\<^sub>R ?t' = 0\<close>
        and \<open>j = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
\<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
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0
j = 0
h \<noteq> 0 \<or> k \<noteq> 0
[PROOF STEP]
have "t = a"
[PROOF STATE]
proof (prove)
using this:
\<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
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0
j = 0
h \<noteq> 0 \<or> k \<noteq> 0

goal (1 subgoal):
 1. t = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = a

goal (2 subgoals):
 1. ?P \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
 2. \<not> ?P \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
thus "t = a \<or> (\<exists> i. t = proj2_abs (i *\<^sub>R ?a' + ?r'))"
[PROOF STATE]
proof (prove)
using this:
t = a

goal (1 subgoal):
 1. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
assume "j \<noteq> 0"
[PROOF STATE]
proof (state)
this:
j \<noteq> 0

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
have "k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> k \<noteq> 0"
[PROOF STATE]
proof (state)
this:
\<not> k \<noteq> 0

goal (1 subgoal):
 1. \<not> k \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
with proj2_rep_dependent
          and \<open>h *\<^sub>R ?a' + j *\<^sub>R ?r' + k *\<^sub>R ?t' = 0\<close>
          and \<open>j \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
\<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
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0
j \<noteq> 0
\<not> k \<noteq> 0
[PROOF STEP]
have "a = r"
[PROOF STATE]
proof (prove)
using this:
\<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
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0
j \<noteq> 0
\<not> k \<noteq> 0

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

goal (1 subgoal):
 1. \<not> k \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
with \<open>a \<noteq> r\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> r
a = r
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
a \<noteq> r
a = r

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
from \<open>h *\<^sub>R ?a' + j *\<^sub>R ?r' + k *\<^sub>R ?t' = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0
[PROOF STEP]
have "h *\<^sub>R ?a' + j *\<^sub>R ?r' + k *\<^sub>R ?t' - k *\<^sub>R ?t' = -k *\<^sub>R ?t'"
[PROOF STATE]
proof (prove)
using this:
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0

goal (1 subgoal):
 1. h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t - k *\<^sub>R proj2_rep t = - k *\<^sub>R proj2_rep t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t - k *\<^sub>R proj2_rep t = - k *\<^sub>R proj2_rep t

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
hence "h *\<^sub>R ?a' + j *\<^sub>R ?r' = -k *\<^sub>R ?t'"
[PROOF STATE]
proof (prove)
using this:
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t - k *\<^sub>R proj2_rep t = - k *\<^sub>R proj2_rep t

goal (1 subgoal):
 1. h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r = - k *\<^sub>R proj2_rep t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r = - k *\<^sub>R proj2_rep t

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
with proj2_abs_mult_rep [of "-k"] and \<open>k \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
- k \<noteq> 0 \<Longrightarrow> proj2_abs (- k *\<^sub>R proj2_rep ?x) = ?x
k \<noteq> 0
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r = - k *\<^sub>R proj2_rep t
[PROOF STEP]
have "proj2_abs (h *\<^sub>R ?a' + j *\<^sub>R ?r') = t"
[PROOF STATE]
proof (prove)
using this:
- k \<noteq> 0 \<Longrightarrow> proj2_abs (- k *\<^sub>R proj2_rep ?x) = ?x
k \<noteq> 0
h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r = - k *\<^sub>R proj2_rep t

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

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
with proj2_abs_mult [of "1/j" "h *\<^sub>R ?a' + j *\<^sub>R ?r'"] and \<open>j \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
1 / j \<noteq> 0 \<Longrightarrow> proj2_abs ((1 / j) *\<^sub>R (h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r)) = proj2_abs (h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r)
j \<noteq> 0
proj2_abs (h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r) = t
[PROOF STEP]
have "proj2_abs ((h/j) *\<^sub>R ?a' + ?r') = t"
[PROOF STATE]
proof (prove)
using this:
1 / j \<noteq> 0 \<Longrightarrow> proj2_abs ((1 / j) *\<^sub>R (h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r)) = proj2_abs (h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r)
j \<noteq> 0
proj2_abs (h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r) = t

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

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
hence "\<exists> i. t = proj2_abs (i *\<^sub>R ?a' + ?r')"
[PROOF STATE]
proof (prove)
using this:
proj2_abs ((h / j) *\<^sub>R proj2_rep a + proj2_rep r) = t

goal (1 subgoal):
 1. \<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
thus "t = a \<or> (\<exists> i. t = proj2_abs (i *\<^sub>R ?a' + ?r'))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)

goal (1 subgoal):
 1. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))

goal (1 subgoal):
 1. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
proj2_Col a r t \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))

goal (1 subgoal):
 1. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
proj2_Col a r t \<Longrightarrow> t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))

goal (1 subgoal):
 1. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
assume "t = a \<or> (\<exists> i. t = proj2_abs (i *\<^sub>R ?a' + ?r'))"
[PROOF STATE]
proof (state)
this:
t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))

goal (1 subgoal):
 1. t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
show "proj2_Col a r t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col a r t
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> proj2_Col a r t
 2. \<not> ?P \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
assume "t = a"
[PROOF STATE]
proof (state)
this:
t = a

goal (2 subgoals):
 1. ?P \<Longrightarrow> proj2_Col a r t
 2. \<not> ?P \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
with proj2_Col_coincide and proj2_Col_permute
[PROOF STATE]
proof (chain)
picking this:
proj2_Col ?a ?a ?c
proj2_Col ?a ?b ?c \<Longrightarrow> proj2_Col ?a ?c ?b
proj2_Col ?a ?b ?c \<Longrightarrow> proj2_Col ?b ?a ?c
t = a
[PROOF STEP]
show "proj2_Col a r t"
[PROOF STATE]
proof (prove)
using this:
proj2_Col ?a ?a ?c
proj2_Col ?a ?b ?c \<Longrightarrow> proj2_Col ?a ?c ?b
proj2_Col ?a ?b ?c \<Longrightarrow> proj2_Col ?b ?a ?c
t = a

goal (1 subgoal):
 1. proj2_Col a r t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
proj2_Col a r t

goal (1 subgoal):
 1. t \<noteq> a \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<noteq> a \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
assume "t \<noteq> a"
[PROOF STATE]
proof (state)
this:
t \<noteq> a

goal (1 subgoal):
 1. t \<noteq> a \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
with \<open>t = a \<or> (\<exists> i. t = proj2_abs (i *\<^sub>R ?a' + ?r'))\<close>
[PROOF STATE]
proof (chain)
picking this:
t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
t \<noteq> a
[PROOF STEP]
obtain i where "t = proj2_abs (i *\<^sub>R ?a' + ?r')"
[PROOF STATE]
proof (prove)
using this:
t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r))
t \<noteq> a

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

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

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

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

goal (1 subgoal):
 1. (\<And>j. proj2_rep t = j *\<^sub>R (i *\<^sub>R proj2_rep a + proj2_rep r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_rep t = j *\<^sub>R (i *\<^sub>R proj2_rep a + proj2_rep r)

goal (1 subgoal):
 1. t \<noteq> a \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
hence "?t' - ?t' = (j * i) *\<^sub>R ?a' + j *\<^sub>R ?r' + (-1) *\<^sub>R ?t'"
[PROOF STATE]
proof (prove)
using this:
proj2_rep t = j *\<^sub>R (i *\<^sub>R proj2_rep a + proj2_rep r)

goal (1 subgoal):
 1. proj2_rep t - proj2_rep t = (j * i) *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + - 1 *\<^sub>R proj2_rep t
[PROOF STEP]
by (simp add: scaleR_right_distrib)
[PROOF STATE]
proof (state)
this:
proj2_rep t - proj2_rep t = (j * i) *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + - 1 *\<^sub>R proj2_rep t

goal (1 subgoal):
 1. t \<noteq> a \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
hence "(j * i) *\<^sub>R ?a' + j *\<^sub>R ?r' + (-1) *\<^sub>R ?t' = 0"
[PROOF STATE]
proof (prove)
using this:
proj2_rep t - proj2_rep t = (j * i) *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + - 1 *\<^sub>R proj2_rep t

goal (1 subgoal):
 1. (j * i) *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + - 1 *\<^sub>R proj2_rep t = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(j * i) *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + - 1 *\<^sub>R proj2_rep t = 0

goal (1 subgoal):
 1. t \<noteq> a \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
have "\<exists> h j k. h *\<^sub>R ?a' + j *\<^sub>R ?r' + k *\<^sub>R ?t' = 0
        \<and> (h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h j k. h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0 \<and> (h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)
[PROOF STEP]
proof standard+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?h *\<^sub>R proj2_rep a + ?j2 *\<^sub>R proj2_rep r + ?k4 *\<^sub>R proj2_rep t = 0
 2. ?h \<noteq> 0 \<or> ?j2 \<noteq> 0 \<or> ?k4 \<noteq> 0
[PROOF STEP]
from \<open>(j * i) *\<^sub>R ?a' + j *\<^sub>R ?r' + (-1) *\<^sub>R ?t' = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
(j * i) *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + - 1 *\<^sub>R proj2_rep t = 0
[PROOF STEP]
show "(j * i) *\<^sub>R ?a' + j *\<^sub>R ?r' + (-1) *\<^sub>R ?t' = 0"
[PROOF STATE]
proof (prove)
using this:
(j * i) *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + - 1 *\<^sub>R proj2_rep t = 0

goal (1 subgoal):
 1. (j * i) *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + - 1 *\<^sub>R proj2_rep t = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(j * i) *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + - 1 *\<^sub>R proj2_rep t = 0

goal (1 subgoal):
 1. j * i \<noteq> 0 \<or> j \<noteq> 0 \<or> - 1 \<noteq> 0
[PROOF STEP]
show "j * i \<noteq> 0 \<or> j \<noteq> 0 \<or> (-1::real) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j * i \<noteq> 0 \<or> j \<noteq> 0 \<or> - 1 \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j * i \<noteq> 0 \<or> j \<noteq> 0 \<or> - 1 \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>h j k. h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0 \<and> (h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)

goal (1 subgoal):
 1. t \<noteq> a \<Longrightarrow> proj2_Col a r t
[PROOF STEP]
thus "proj2_Col a r t"
[PROOF STATE]
proof (prove)
using this:
\<exists>h j k. h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0 \<and> (h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)

goal (1 subgoal):
 1. proj2_Col a r t
[PROOF STEP]
unfolding proj2_Col_def
[PROOF STATE]
proof (prove)
using this:
\<exists>h j k. h *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0 \<and> (h \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)

goal (1 subgoal):
 1. \<exists>i j k. i *\<^sub>R proj2_rep a + j *\<^sub>R proj2_rep r + k *\<^sub>R proj2_rep t = 0 \<and> (i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
proj2_Col a r t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proj2_Col a r t

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
t = a \<or> (\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)) \<Longrightarrow> proj2_Col a r t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_Col_coeff:
  assumes "proj2_Col a r t" and "a \<noteq> r" and "t \<noteq> a"
  shows "t = proj2_abs ((proj2_Col_coeff a r t) *\<^sub>R proj2_rep a + proj2_rep r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = proj2_abs (proj2_Col_coeff a r t *\<^sub>R proj2_rep a + proj2_rep r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t = proj2_abs (proj2_Col_coeff a r t *\<^sub>R proj2_rep a + proj2_rep r)
[PROOF STEP]
from \<open>a \<noteq> r\<close> and \<open>proj2_Col a r t\<close> and \<open>t \<noteq> a\<close> and proj2_Col_iff
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> r
proj2_Col a r t
t \<noteq> a
?a \<noteq> ?r \<Longrightarrow> proj2_Col ?a ?r ?t = (?t = ?a \<or> (\<exists>i. ?t = proj2_abs (i *\<^sub>R proj2_rep ?a + proj2_rep ?r)))
[PROOF STEP]
have "\<exists> i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> r
proj2_Col a r t
t \<noteq> a
?a \<noteq> ?r \<Longrightarrow> proj2_Col ?a ?r ?t = (?t = ?a \<or> (\<exists>i. ?t = proj2_abs (i *\<^sub>R proj2_rep ?a + proj2_rep ?r)))

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

goal (1 subgoal):
 1. t = proj2_abs (proj2_Col_coeff a r t *\<^sub>R proj2_rep a + proj2_rep r)
[PROOF STEP]
thus "t = proj2_abs ((proj2_Col_coeff a r t) *\<^sub>R proj2_rep a + proj2_rep r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. t = proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)

goal (1 subgoal):
 1. t = proj2_abs (proj2_Col_coeff a r t *\<^sub>R proj2_rep a + proj2_rep r)
[PROOF STEP]
by (unfold proj2_Col_coeff_def) (rule someI_ex)
[PROOF STATE]
proof (state)
this:
t = proj2_abs (proj2_Col_coeff a r t *\<^sub>R proj2_rep a + proj2_rep r)

goal:
No subgoals!
[PROOF STEP]
qed