[STATEMENT]
lemma proj2_incident_Col:
  assumes "proj2_incident p l" and "proj2_incident q l" and "proj2_incident r l"
  shows "proj2_Col p q r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col p q r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_Col p q r
[PROOF STEP]
from \<open>proj2_incident p l\<close> and \<open>proj2_incident q l\<close> and \<open>proj2_incident r l\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_incident p l
proj2_incident q l
proj2_incident r l
[PROOF STEP]
have "proj2_set_Col {p,q,r}"
[PROOF STATE]
proof (prove)
using this:
proj2_incident p l
proj2_incident q l
proj2_incident r l

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

goal (1 subgoal):
 1. proj2_Col p q r
[PROOF STEP]
thus "proj2_Col p q r"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_incident_iff_Col:
  assumes "p \<noteq> q" and "proj2_incident p l" and "proj2_incident q l"
  shows "proj2_incident r l \<longleftrightarrow> proj2_Col p q r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident r l = proj2_Col p q r
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_incident r l \<Longrightarrow> proj2_Col p q r
 2. proj2_Col p q r \<Longrightarrow> proj2_incident r l
[PROOF STEP]
assume "proj2_incident r l"
[PROOF STATE]
proof (state)
this:
proj2_incident r l

goal (2 subgoals):
 1. proj2_incident r l \<Longrightarrow> proj2_Col p q r
 2. proj2_Col p q r \<Longrightarrow> proj2_incident r l
[PROOF STEP]
with \<open>proj2_incident p l\<close> and \<open>proj2_incident q l\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_incident p l
proj2_incident q l
proj2_incident r l
[PROOF STEP]
show "proj2_Col p q r"
[PROOF STATE]
proof (prove)
using this:
proj2_incident p l
proj2_incident q l
proj2_incident r l

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

goal (1 subgoal):
 1. proj2_Col p q r \<Longrightarrow> proj2_incident r l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_Col p q r \<Longrightarrow> proj2_incident r l
[PROOF STEP]
assume "proj2_Col p q r"
[PROOF STATE]
proof (state)
this:
proj2_Col p q r

goal (1 subgoal):
 1. proj2_Col p q r \<Longrightarrow> proj2_incident r l
[PROOF STEP]
hence "proj2_set_Col {p,q,r}"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q r

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

goal (1 subgoal):
 1. proj2_Col p q r \<Longrightarrow> proj2_incident r l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {p, q, r}
[PROOF STEP]
obtain m where "\<forall> s\<in>{p,q,r}. proj2_incident s m"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. (\<And>m. \<forall>s\<in>{p, q, r}. proj2_incident s m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding proj2_set_Col_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l. \<forall>p\<in>{p, q, r}. proj2_incident p l

goal (1 subgoal):
 1. (\<And>m. \<forall>s\<in>{p, q, r}. proj2_incident s m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>{p, q, r}. proj2_incident s m

goal (1 subgoal):
 1. proj2_Col p q r \<Longrightarrow> proj2_incident r l
[PROOF STEP]
hence "proj2_incident p m" and "proj2_incident q m" and "proj2_incident r m"
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>{p, q, r}. proj2_incident s m

goal (1 subgoal):
 1. proj2_incident p m &&& proj2_incident q m &&& proj2_incident r m
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
proj2_incident p m
proj2_incident q m
proj2_incident r m

goal (1 subgoal):
 1. proj2_Col p q r \<Longrightarrow> proj2_incident r l
[PROOF STEP]
from \<open>p \<noteq> q\<close> and \<open>proj2_incident p l\<close> and \<open>proj2_incident q l\<close>
    and \<open>proj2_incident p m\<close> and \<open>proj2_incident q m\<close>
    and proj2_incident_unique
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
proj2_incident p l
proj2_incident q l
proj2_incident p m
proj2_incident q m
\<lbrakk>proj2_incident ?p ?l; proj2_incident ?q ?l; proj2_incident ?p ?m; proj2_incident ?q ?m\<rbrakk> \<Longrightarrow> ?p = ?q \<or> ?l = ?m
[PROOF STEP]
have "m = l"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
proj2_incident p l
proj2_incident q l
proj2_incident p m
proj2_incident q m
\<lbrakk>proj2_incident ?p ?l; proj2_incident ?q ?l; proj2_incident ?p ?m; proj2_incident ?q ?m\<rbrakk> \<Longrightarrow> ?p = ?q \<or> ?l = ?m

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

goal (1 subgoal):
 1. proj2_Col p q r \<Longrightarrow> proj2_incident r l
[PROOF STEP]
with \<open>proj2_incident r m\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_incident r m
m = l
[PROOF STEP]
show "proj2_incident r l"
[PROOF STATE]
proof (prove)
using this:
proj2_incident r m
m = l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_incident_iff:
  assumes "p \<noteq> q" and "proj2_incident p l" and "proj2_incident q l"
  shows "proj2_incident r l
  \<longleftrightarrow> r = p \<or> (\<exists> k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident r l = (r = p \<or> (\<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_incident r l = (r = p \<or> (\<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)))
[PROOF STEP]
from \<open>p \<noteq> q\<close> and \<open>proj2_incident p l\<close> and \<open>proj2_incident q l\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
proj2_incident p l
proj2_incident q l
[PROOF STEP]
have "proj2_incident r l \<longleftrightarrow> proj2_Col p q r"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
proj2_incident p l
proj2_incident q l

goal (1 subgoal):
 1. proj2_incident r l = proj2_Col p q r
[PROOF STEP]
by (rule proj2_incident_iff_Col)
[PROOF STATE]
proof (state)
this:
proj2_incident r l = proj2_Col p q r

goal (1 subgoal):
 1. proj2_incident r l = (r = p \<or> (\<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)))
[PROOF STEP]
with \<open>p \<noteq> q\<close> and proj2_Col_iff
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
?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)))
proj2_incident r l = proj2_Col p q r
[PROOF STEP]
show "proj2_incident r l
    \<longleftrightarrow> r = p \<or> (\<exists> k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q))"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
?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)))
proj2_incident r l = proj2_Col p q r

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_proj2_set_Col_iff_span:
  assumes "card S = 3"
  shows "\<not> proj2_set_Col S \<longleftrightarrow> span (proj2_rep ` S) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
from \<open>card S = 3\<close> and choose_3 [of S]
[PROOF STATE]
proof (chain)
picking this:
card S = 3
card S = 3 \<Longrightarrow> \<exists>x y z. S = {x, y, z}
[PROOF STEP]
obtain p and q and r where "S = {p,q,r}"
[PROOF STATE]
proof (prove)
using this:
card S = 3
card S = 3 \<Longrightarrow> \<exists>x y z. S = {x, y, z}

goal (1 subgoal):
 1. (\<And>p q r. S = {p, q, r} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S = {p, q, r}

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
let ?u = "proj2_rep p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
let ?v = "proj2_rep q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
let ?w = "proj2_rep r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
let ?M = "vector [?u, ?v, ?w] :: real^3^3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
from \<open>S = {p,q,r}\<close> and not_invertible_iff_proj2_set_Col [of p q r]
[PROOF STATE]
proof (chain)
picking this:
S = {p, q, r}
(\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}
[PROOF STEP]
have "\<not> proj2_set_Col S \<longleftrightarrow> invertible ?M"
[PROOF STATE]
proof (prove)
using this:
S = {p, q, r}
(\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<not> proj2_set_Col S) = invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<not> proj2_set_Col S) = invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
from left_invertible_iff_invertible
[PROOF STATE]
proof (chain)
picking this:
(\<exists>N. N ** ?M = mat 1) = invertible ?M
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<exists> N. N ** ?M = mat 1)"
[PROOF STATE]
proof (prove)
using this:
(\<exists>N. N ** ?M = mat 1) = invertible ?M

goal (1 subgoal):
 1. invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = (\<exists>N. N ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = (\<exists>N. N ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1)

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = (\<exists>N. N ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1)

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
from matrix_left_invertible_span_rows
[PROOF STATE]
proof (chain)
picking this:
(\<exists>B. B ** ?A = mat 1) = (span (rows ?A) = UNIV)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> span (rows ?M) = UNIV"
[PROOF STATE]
proof (prove)
using this:
(\<exists>B. B ** ?A = mat 1) = (span (rows ?A) = UNIV)

goal (1 subgoal):
 1. (\<exists>N. N ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1) = (span (rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = UNIV)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>N. N ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1) = (span (rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = UNIV)

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<not> proj2_set_Col S) = (span (rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = UNIV)
[PROOF STEP]
have "\<not> proj2_set_Col S \<longleftrightarrow> span (rows ?M) = UNIV"
[PROOF STATE]
proof (prove)
using this:
(\<not> proj2_set_Col S) = (span (rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = UNIV)

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = UNIV)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<not> proj2_set_Col S) = (span (rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = UNIV)

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
have "rows ?M = {?u, ?v, ?w}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = {proj2_rep p, proj2_rep q, proj2_rep r}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}
 2. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}
 2. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}
 2. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
assume "x \<in> rows ?M"
[PROOF STATE]
proof (state)
this:
x \<in> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])

goal (2 subgoals):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}
 2. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
obtain i :: 3  where "x = ?M $ i"
[PROOF STATE]
proof (prove)
using this:
x \<in> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])

goal (1 subgoal):
 1. (\<And>i. x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rows_def and row_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {vec_lambda (($) (vector [proj2_rep p, proj2_rep q, proj2_rep r] $ i)) |i. i \<in> UNIV}

goal (1 subgoal):
 1. (\<And>i. x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: vec_lambda_beta vec_lambda_eta)
[PROOF STATE]
proof (state)
this:
x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ i

goal (2 subgoals):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}
 2. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
with exhaust_3
[PROOF STATE]
proof (chain)
picking this:
?x = 1 \<or> ?x = 2 \<or> ?x = 3
x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ i
[PROOF STEP]
have "x = ?u \<or> x = ?v \<or> x = ?w"
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2 \<or> ?x = 3
x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ i

goal (1 subgoal):
 1. x = proj2_rep p \<or> x = proj2_rep q \<or> x = proj2_rep r
[PROOF STEP]
unfolding vector_def
[PROOF STATE]
proof (prove)
using this:
?x = 1 \<or> ?x = 2 \<or> ?x = 3
x = vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [proj2_rep p, proj2_rep q, proj2_rep r] (\<lambda>n x. 0) 1) $ i

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

goal (2 subgoals):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}
 2. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
hence "x \<in> {?u, ?v, ?w}"
[PROOF STATE]
proof (prove)
using this:
x = proj2_rep p \<or> x = proj2_rep q \<or> x = proj2_rep r

goal (1 subgoal):
 1. x \<in> {proj2_rep p, proj2_rep q, proj2_rep r}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> {proj2_rep p, proj2_rep q, proj2_rep r}

goal (2 subgoals):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}
 2. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<Longrightarrow> ?x2 \<in> {proj2_rep p, proj2_rep q, proj2_rep r}

goal (2 subgoals):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}
 2. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
thus "rows ?M \<subseteq> {?u, ?v, ?w}"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<Longrightarrow> ?x2 \<in> {proj2_rep p, proj2_rep q, proj2_rep r}

goal (1 subgoal):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}

goal (1 subgoal):
 1. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) \<subseteq> {proj2_rep p, proj2_rep q, proj2_rep r}

goal (1 subgoal):
 1. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
assume "x \<in> {?u, ?v, ?w}"
[PROOF STATE]
proof (state)
this:
x \<in> {proj2_rep p, proj2_rep q, proj2_rep r}

goal (1 subgoal):
 1. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
hence "x = ?u \<or> x = ?v \<or> x = ?w"
[PROOF STATE]
proof (prove)
using this:
x \<in> {proj2_rep p, proj2_rep q, proj2_rep r}

goal (1 subgoal):
 1. x = proj2_rep p \<or> x = proj2_rep q \<or> x = proj2_rep r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = proj2_rep p \<or> x = proj2_rep q \<or> x = proj2_rep r

goal (1 subgoal):
 1. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
hence "x = ?M $ 1 \<or> x = ?M $ 2 \<or> x = ?M $ 3"
[PROOF STATE]
proof (prove)
using this:
x = proj2_rep p \<or> x = proj2_rep q \<or> x = proj2_rep r

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

goal (1 subgoal):
 1. x = vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [proj2_rep p, proj2_rep q, proj2_rep r] (\<lambda>n x. 0) 1) $ 1 \<or> x = vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [proj2_rep p, proj2_rep q, proj2_rep r] (\<lambda>n x. 0) 1) $ 2 \<or> x = vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [proj2_rep p, proj2_rep q, proj2_rep r] (\<lambda>n x. 0) 1) $ 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ 1 \<or> x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ 2 \<or> x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ 3

goal (1 subgoal):
 1. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
hence "x \<in> rows ?M"
[PROOF STATE]
proof (prove)
using this:
x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ 1 \<or> x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ 2 \<or> x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ 3

goal (1 subgoal):
 1. x \<in> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
unfolding rows_def row_def vec_lambda_eta
[PROOF STATE]
proof (prove)
using this:
x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ 1 \<or> x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ 2 \<or> x = vector [proj2_rep p, proj2_rep q, proj2_rep r] $ 3

goal (1 subgoal):
 1. x \<in> {vector [proj2_rep p, proj2_rep q, proj2_rep r] $ i |i. i \<in> UNIV}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])

goal (1 subgoal):
 1. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> {proj2_rep p, proj2_rep q, proj2_rep r} \<Longrightarrow> ?x2 \<in> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])

goal (1 subgoal):
 1. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
thus "{?u, ?v, ?w} \<subseteq> rows ?M"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> {proj2_rep p, proj2_rep q, proj2_rep r} \<Longrightarrow> ?x2 \<in> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])

goal (1 subgoal):
 1. {proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
{proj2_rep p, proj2_rep q, proj2_rep r} \<subseteq> rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = {proj2_rep p, proj2_rep q, proj2_rep r}

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
with \<open>S = {p,q,r}\<close>
[PROOF STATE]
proof (chain)
picking this:
S = {p, q, r}
rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = {proj2_rep p, proj2_rep q, proj2_rep r}
[PROOF STEP]
have "rows ?M = proj2_rep ` S"
[PROOF STATE]
proof (prove)
using this:
S = {p, q, r}
rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = {proj2_rep p, proj2_rep q, proj2_rep r}

goal (1 subgoal):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = proj2_rep ` S
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
using this:
S = {p, q, r}
rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = {proj2_rep p, proj2_rep q, proj2_rep r}

goal (1 subgoal):
 1. rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = {y. \<exists>x\<in>S. y = proj2_rep x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = proj2_rep ` S

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
with \<open>\<not> proj2_set_Col S \<longleftrightarrow> span (rows ?M) = UNIV\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<not> proj2_set_Col S) = (span (rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = UNIV)
rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = proj2_rep ` S
[PROOF STEP]
show "\<not> proj2_set_Col S \<longleftrightarrow> span (proj2_rep ` S) = UNIV"
[PROOF STATE]
proof (prove)
using this:
(\<not> proj2_set_Col S) = (span (rows (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = UNIV)
rows (vector [proj2_rep p, proj2_rep q, proj2_rep r]) = proj2_rep ` S

goal (1 subgoal):
 1. (\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<not> proj2_set_Col S) = (span (proj2_rep ` S) = UNIV)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_no_3_Col_span:
  assumes "proj2_no_3_Col S" and "p \<in> S"
  shows "span (proj2_rep ` (S - {p})) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. span (proj2_rep ` (S - {p})) = UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. span (proj2_rep ` (S - {p})) = UNIV
[PROOF STEP]
from \<open>proj2_no_3_Col S\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_no_3_Col S
[PROOF STEP]
have "card S = 4"
[PROOF STATE]
proof (prove)
using this:
proj2_no_3_Col S

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

goal (1 subgoal):
 1. card S = 4
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
card S = 4

goal (1 subgoal):
 1. span (proj2_rep ` (S - {p})) = UNIV
[PROOF STEP]
with \<open>p \<in> S\<close> and \<open>card S = 4\<close> and card_gt_0_diff_singleton [of S p]
[PROOF STATE]
proof (chain)
picking this:
p \<in> S
card S = 4
\<lbrakk>0 < card S; p \<in> S\<rbrakk> \<Longrightarrow> card (S - {p}) = card S - 1
card S = 4
[PROOF STEP]
have "card (S - {p}) = 3"
[PROOF STATE]
proof (prove)
using this:
p \<in> S
card S = 4
\<lbrakk>0 < card S; p \<in> S\<rbrakk> \<Longrightarrow> card (S - {p}) = card S - 1
card S = 4

goal (1 subgoal):
 1. card (S - {p}) = 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (S - {p}) = 3

goal (1 subgoal):
 1. span (proj2_rep ` (S - {p})) = UNIV
[PROOF STEP]
from \<open>proj2_no_3_Col S\<close> and \<open>p \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_no_3_Col S
p \<in> S
[PROOF STEP]
have "\<not> proj2_set_Col (S - {p})"
[PROOF STATE]
proof (prove)
using this:
proj2_no_3_Col S
p \<in> S

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

goal (1 subgoal):
 1. \<not> proj2_set_Col (S - {p})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> proj2_set_Col (S - {p})

goal (1 subgoal):
 1. span (proj2_rep ` (S - {p})) = UNIV
[PROOF STEP]
with \<open>card (S - {p}) = 3\<close> and not_proj2_set_Col_iff_span
[PROOF STATE]
proof (chain)
picking this:
card (S - {p}) = 3
card ?S = 3 \<Longrightarrow> (\<not> proj2_set_Col ?S) = (span (proj2_rep ` ?S) = UNIV)
\<not> proj2_set_Col (S - {p})
[PROOF STEP]
show "span (proj2_rep ` (S - {p})) = UNIV"
[PROOF STATE]
proof (prove)
using this:
card (S - {p}) = 3
card ?S = 3 \<Longrightarrow> (\<not> proj2_set_Col ?S) = (span (proj2_rep ` ?S) = UNIV)
\<not> proj2_set_Col (S - {p})

goal (1 subgoal):
 1. span (proj2_rep ` (S - {p})) = UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
span (proj2_rep ` (S - {p})) = UNIV

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fourth_proj2_no_3_Col:
  assumes "\<not> proj2_Col p q r"
  shows "\<exists> s. proj2_no_3_Col {s,r,p,q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
from \<open>\<not> proj2_Col p q r\<close> and proj2_Col_coincide
[PROOF STATE]
proof (chain)
picking this:
\<not> proj2_Col p q r
proj2_Col ?a ?a ?c
[PROOF STEP]
have "p \<noteq> q"
[PROOF STATE]
proof (prove)
using this:
\<not> proj2_Col p q r
proj2_Col ?a ?a ?c

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

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
hence "card {p,q} = 2"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q

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

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
from \<open>\<not> proj2_Col p q r\<close> and proj2_Col_coincide and proj2_Col_permute
[PROOF STATE]
proof (chain)
picking this:
\<not> proj2_Col p q r
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
[PROOF STEP]
have "r \<notin> {p,q}"
[PROOF STATE]
proof (prove)
using this:
\<not> proj2_Col p q r
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

goal (1 subgoal):
 1. r \<notin> {p, q}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
r \<notin> {p, q}

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
with \<open>card {p,q} = 2\<close>
[PROOF STATE]
proof (chain)
picking this:
card {p, q} = 2
r \<notin> {p, q}
[PROOF STEP]
have "card {r,p,q} = 3"
[PROOF STATE]
proof (prove)
using this:
card {p, q} = 2
r \<notin> {p, q}

goal (1 subgoal):
 1. card {r, p, q} = 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {r, p, q} = 3

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
have "finite {r,p,q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {r, p, q}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {r, p, q}

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
let ?s = "proj2_abs (\<Sum> t\<in>{r,p,q}. proj2_rep t)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
have "\<exists> j. (\<Sum> t\<in>{r,p,q}. proj2_rep t) = j *\<^sub>R proj2_rep ?s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
 2. \<not> ?P \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
assume "(\<Sum> t\<in>{r,p,q}. proj2_rep t) = 0"
[PROOF STATE]
proof (state)
this:
sum proj2_rep {r, p, q} = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
 2. \<not> ?P \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
hence "(\<Sum> t\<in>{r,p,q}. proj2_rep t) = 0 *\<^sub>R proj2_rep ?s"
[PROOF STATE]
proof (prove)
using this:
sum proj2_rep {r, p, q} = 0

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
 2. \<not> ?P \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
thus "\<exists> j. (\<Sum> t\<in>{r,p,q}. proj2_rep t) = j *\<^sub>R proj2_rep ?s"
[PROOF STATE]
proof (prove)
using this:
sum proj2_rep {r, p, q} = 0 *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))

goal (1 subgoal):
 1. \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))

goal (1 subgoal):
 1. sum proj2_rep {r, p, q} \<noteq> 0 \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum proj2_rep {r, p, q} \<noteq> 0 \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
assume "(\<Sum> t\<in>{r,p,q}. proj2_rep t) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
sum proj2_rep {r, p, q} \<noteq> 0

goal (1 subgoal):
 1. sum proj2_rep {r, p, q} \<noteq> 0 \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
with proj2_rep_abs2
[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
sum proj2_rep {r, p, q} \<noteq> 0
[PROOF STEP]
obtain k where "k \<noteq> 0"
      and "proj2_rep ?s = k *\<^sub>R (\<Sum> t\<in>{r,p,q}. proj2_rep t)"
[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
sum proj2_rep {r, p, q} \<noteq> 0

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

goal (1 subgoal):
 1. sum proj2_rep {r, p, q} \<noteq> 0 \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
hence "(1/k) *\<^sub>R proj2_rep ?s = (\<Sum> t\<in>{r,p,q}. proj2_rep t)"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) = k *\<^sub>R sum proj2_rep {r, p, q}

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

goal (1 subgoal):
 1. sum proj2_rep {r, p, q} \<noteq> 0 \<Longrightarrow> \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
from this [symmetric]
[PROOF STATE]
proof (chain)
picking this:
sum proj2_rep {r, p, q} = (1 / k) *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
show "\<exists> j. (\<Sum> t\<in>{r,p,q}. proj2_rep t) = j *\<^sub>R proj2_rep ?s"
[PROOF STATE]
proof (prove)
using this:
sum proj2_rep {r, p, q} = (1 / k) *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))

goal (1 subgoal):
 1. \<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
obtain j where "(\<Sum> t\<in>{r,p,q}. proj2_rep t) = j *\<^sub>R proj2_rep ?s"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))

goal (1 subgoal):
 1. (\<And>j. sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
let ?c = "\<lambda> t. if t = ?s then 1 - j else 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
from \<open>p \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
[PROOF STEP]
have "?c p \<noteq> 0 \<or> ?c q \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q

goal (1 subgoal):
 1. (if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) \<noteq> 0 \<or> (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) \<noteq> 0 \<or> (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) \<noteq> 0

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
let ?d = "\<lambda> t. if t = ?s then j else -1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
let ?S = "{?s,r,p,q}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
have "?s \<notin> {r,p,q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
assume "?s \<in> {r,p,q}"
[PROOF STATE]
proof (state)
this:
proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q}

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
from \<open>r \<notin> {p,q}\<close> and \<open>p \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<notin> {p, q}
p \<noteq> q
[PROOF STEP]
have "?c r *\<^sub>R proj2_rep r + ?c p *\<^sub>R proj2_rep p + ?c q *\<^sub>R proj2_rep q
      = (\<Sum> t\<in>{r,p,q}. ?c t *\<^sub>R proj2_rep t)"
[PROOF STATE]
proof (prove)
using this:
r \<notin> {p, q}
p \<noteq> q

goal (1 subgoal):
 1. (if r = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep r + (if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep p + (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep q = (\<Sum>t\<in>{r, p, q}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t)
[PROOF STEP]
by (simp add: sum.insert [of _ _ "\<lambda> t. ?c t *\<^sub>R proj2_rep t"])
[PROOF STATE]
proof (state)
this:
(if r = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep r + (if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep p + (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep q = (\<Sum>t\<in>{r, p, q}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if r = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep r + (if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep p + (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep q = (\<Sum>t\<in>{r, p, q}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
from \<open>finite {r,p,q}\<close> and \<open>?s \<in> {r,p,q}\<close>
[PROOF STATE]
proof (chain)
picking this:
finite {r, p, q}
proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q}
[PROOF STEP]
have "\<dots> = ?c ?s *\<^sub>R proj2_rep ?s + (\<Sum> t\<in>{r,p,q}-{?s}. ?c t *\<^sub>R proj2_rep t)"
[PROOF STATE]
proof (prove)
using this:
finite {r, p, q}
proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q}

goal (1 subgoal):
 1. (\<Sum>t\<in>{r, p, q}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t) = (if proj2_abs (sum proj2_rep {r, p, q}) = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t)
[PROOF STEP]
by (simp only:
        sum.remove [of "{r,p,q}" ?s "\<lambda> t. ?c t *\<^sub>R proj2_rep t"])
[PROOF STATE]
proof (state)
this:
(\<Sum>t\<in>{r, p, q}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t) = (if proj2_abs (sum proj2_rep {r, p, q}) = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>t\<in>{r, p, q}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t) = (if proj2_abs (sum proj2_rep {r, p, q}) = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
have "\<dots>
      = -j *\<^sub>R proj2_rep ?s + (proj2_rep ?s + (\<Sum> t\<in>{r,p,q}-{?s}. proj2_rep t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if proj2_abs (sum proj2_rep {r, p, q}) = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t) = - j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep ({r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})}))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
(if proj2_abs (sum proj2_rep {r, p, q}) = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t) = - j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep ({r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})}))

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if proj2_abs (sum proj2_rep {r, p, q}) = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep t) = - j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep ({r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})}))

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
from \<open>finite {r,p,q}\<close> and \<open>?s \<in> {r,p,q}\<close>
[PROOF STATE]
proof (chain)
picking this:
finite {r, p, q}
proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q}
[PROOF STEP]
have "\<dots> = -j *\<^sub>R proj2_rep ?s + (\<Sum> t\<in>{r,p,q}. proj2_rep t)"
[PROOF STATE]
proof (prove)
using this:
finite {r, p, q}
proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q}

goal (1 subgoal):
 1. - j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep ({r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})})) = - j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep {r, p, q}
[PROOF STEP]
by (simp only:
        sum.remove [of "{r,p,q}" ?s "\<lambda> t. proj2_rep t",symmetric])
[PROOF STATE]
proof (state)
this:
- j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep ({r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})})) = - j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep {r, p, q}

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep ({r, p, q} - {proj2_abs (sum proj2_rep {r, p, q})})) = - j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep {r, p, q}

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
from \<open>(\<Sum> t\<in>{r,p,q}. proj2_rep t) = j *\<^sub>R proj2_rep ?s\<close>
[PROOF STATE]
proof (chain)
picking this:
sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
using this:
sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))

goal (1 subgoal):
 1. - j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep {r, p, q} = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + sum proj2_rep {r, p, q} = 0

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(if r = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep r + (if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep p + (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep q = 0
[PROOF STEP]
have "?c r *\<^sub>R proj2_rep r + ?c p *\<^sub>R proj2_rep p + ?c q *\<^sub>R proj2_rep q = 0"
[PROOF STATE]
proof (prove)
using this:
(if r = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep r + (if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep p + (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep q = 0

goal (1 subgoal):
 1. (if r = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep r + (if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep p + (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep q = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(if r = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep r + (if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep p + (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep q = 0

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
with \<open>?c p \<noteq> 0 \<or> ?c q \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
(if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) \<noteq> 0 \<or> (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) \<noteq> 0
(if r = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep r + (if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep p + (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep q = 0
[PROOF STEP]
have "proj2_Col p q r"
[PROOF STATE]
proof (prove)
using this:
(if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) \<noteq> 0 \<or> (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) \<noteq> 0
(if r = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep r + (if p = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep p + (if q = proj2_abs (sum proj2_rep {r, p, q}) then 1 - j else 1) *\<^sub>R proj2_rep q = 0

goal (1 subgoal):
 1. proj2_Col p q r
[PROOF STEP]
by (unfold proj2_Col_def) (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
proj2_Col p q r

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<in> {r, p, q} \<Longrightarrow> False
[PROOF STEP]
with \<open>\<not> proj2_Col p q r\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> proj2_Col p q r
proj2_Col p q r
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> proj2_Col p q r
proj2_Col p q 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:
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q}

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
with \<open>card {r,p,q} = 3\<close>
[PROOF STATE]
proof (chain)
picking this:
card {r, p, q} = 3
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q}
[PROOF STEP]
have "card ?S = 4"
[PROOF STATE]
proof (prove)
using this:
card {r, p, q} = 3
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q}

goal (1 subgoal):
 1. card {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} = 4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} = 4

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
from \<open>\<not> proj2_Col p q r\<close> and proj2_Col_permute
[PROOF STATE]
proof (chain)
picking this:
\<not> proj2_Col p q r
proj2_Col ?a ?b ?c \<Longrightarrow> proj2_Col ?a ?c ?b
proj2_Col ?a ?b ?c \<Longrightarrow> proj2_Col ?b ?a ?c
[PROOF STEP]
have "\<not> proj2_Col r p q"
[PROOF STATE]
proof (prove)
using this:
\<not> proj2_Col p q r
proj2_Col ?a ?b ?c \<Longrightarrow> proj2_Col ?a ?c ?b
proj2_Col ?a ?b ?c \<Longrightarrow> proj2_Col ?b ?a ?c

goal (1 subgoal):
 1. \<not> proj2_Col r p q
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<not> proj2_Col r p q

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
hence "\<not> proj2_set_Col {r,p,q}"
[PROOF STATE]
proof (prove)
using this:
\<not> proj2_Col r p q

goal (1 subgoal):
 1. \<not> proj2_set_Col {r, p, q}
[PROOF STEP]
by (subst proj2_Col_iff_set_Col [symmetric])
[PROOF STATE]
proof (state)
this:
\<not> proj2_set_Col {r, p, q}

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
have "\<forall> u\<in>?S. \<not> proj2_set_Col (?S - {u})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q}. \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
assume "u \<in> ?S"
[PROOF STATE]
proof (state)
this:
u \<in> {proj2_abs (sum proj2_rep {r, p, q}), r, p, q}

goal (1 subgoal):
 1. \<And>u. u \<in> {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
with \<open>card ?S = 4\<close>
[PROOF STATE]
proof (chain)
picking this:
card {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} = 4
u \<in> {proj2_abs (sum proj2_rep {r, p, q}), r, p, q}
[PROOF STEP]
have "card (?S - {u}) = 3"
[PROOF STATE]
proof (prove)
using this:
card {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} = 4
u \<in> {proj2_abs (sum proj2_rep {r, p, q}), r, p, q}

goal (1 subgoal):
 1. card ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}) = 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}) = 3

goal (1 subgoal):
 1. \<And>u. u \<in> {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
show "\<not> proj2_set_Col (?S - {u})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
 2. \<not> ?P \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
assume "u = ?s"
[PROOF STATE]
proof (state)
this:
u = proj2_abs (sum proj2_rep {r, p, q})

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
 2. \<not> ?P \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
with \<open>?s \<notin> {r,p,q}\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q}
u = proj2_abs (sum proj2_rep {r, p, q})
[PROOF STEP]
have "?S - {u} = {r,p,q}"
[PROOF STATE]
proof (prove)
using this:
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q}
u = proj2_abs (sum proj2_rep {r, p, q})

goal (1 subgoal):
 1. {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u} = {r, p, q}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u} = {r, p, q}

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
 2. \<not> ?P \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
with \<open>\<not> proj2_set_Col {r,p,q}\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> proj2_set_Col {r, p, q}
{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u} = {r, p, q}
[PROOF STEP]
show "\<not> proj2_set_Col (?S - {u})"
[PROOF STATE]
proof (prove)
using this:
\<not> proj2_set_Col {r, p, q}
{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u} = {r, p, q}

goal (1 subgoal):
 1. \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
assume "u \<noteq> ?s"
[PROOF STATE]
proof (state)
this:
u \<noteq> proj2_abs (sum proj2_rep {r, p, q})

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
hence "insert ?s ({r,p,q} - {u}) = ?S - {u}"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> proj2_abs (sum proj2_rep {r, p, q})

goal (1 subgoal):
 1. insert (proj2_abs (sum proj2_rep {r, p, q})) ({r, p, q} - {u}) = {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert (proj2_abs (sum proj2_rep {r, p, q})) ({r, p, q} - {u}) = {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
from \<open>finite {r,p,q}\<close>
[PROOF STATE]
proof (chain)
picking this:
finite {r, p, q}
[PROOF STEP]
have "finite ({r,p,q} - {u})"
[PROOF STATE]
proof (prove)
using this:
finite {r, p, q}

goal (1 subgoal):
 1. finite ({r, p, q} - {u})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite ({r, p, q} - {u})

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
from \<open>?s \<notin> {r,p,q}\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q}
[PROOF STEP]
have "?s \<notin> {r,p,q} - {u}"
[PROOF STATE]
proof (prove)
using this:
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q}

goal (1 subgoal):
 1. proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q} - {u}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q} - {u}

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
hence "\<forall> t\<in>{r,p,q}-{u}. ?d t = -1"
[PROOF STATE]
proof (prove)
using this:
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q} - {u}

goal (1 subgoal):
 1. \<forall>t\<in>{r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) = - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) = - 1

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
from \<open>u \<noteq> ?s\<close> and  \<open>u \<in> ?S\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> proj2_abs (sum proj2_rep {r, p, q})
u \<in> {proj2_abs (sum proj2_rep {r, p, q}), r, p, q}
[PROOF STEP]
have "u \<in> {r,p,q}"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> proj2_abs (sum proj2_rep {r, p, q})
u \<in> {proj2_abs (sum proj2_rep {r, p, q}), r, p, q}

goal (1 subgoal):
 1. u \<in> {r, p, q}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<in> {r, p, q}

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
hence "(\<Sum> t\<in>{r,p,q}. proj2_rep t)
        = proj2_rep u + (\<Sum> t\<in>{r,p,q}-{u}. proj2_rep t)"
[PROOF STATE]
proof (prove)
using this:
u \<in> {r, p, q}

goal (1 subgoal):
 1. sum proj2_rep {r, p, q} = proj2_rep u + sum proj2_rep ({r, p, q} - {u})
[PROOF STEP]
by (simp add: sum.remove)
[PROOF STATE]
proof (state)
this:
sum proj2_rep {r, p, q} = proj2_rep u + sum proj2_rep ({r, p, q} - {u})

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
with \<open>(\<Sum> t\<in>{r,p,q}. proj2_rep t) = j *\<^sub>R proj2_rep ?s\<close>
[PROOF STATE]
proof (chain)
picking this:
sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
sum proj2_rep {r, p, q} = proj2_rep u + sum proj2_rep ({r, p, q} - {u})
[PROOF STEP]
have "proj2_rep u
        = j *\<^sub>R proj2_rep ?s - (\<Sum> t\<in>{r,p,q}-{u}. proj2_rep t)"
[PROOF STATE]
proof (prove)
using this:
sum proj2_rep {r, p, q} = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q}))
sum proj2_rep {r, p, q} = proj2_rep u + sum proj2_rep ({r, p, q} - {u})

goal (1 subgoal):
 1. proj2_rep u = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) - sum proj2_rep ({r, p, q} - {u})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep u = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) - sum proj2_rep ({r, p, q} - {u})

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proj2_rep u = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) - sum proj2_rep ({r, p, q} - {u})

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
from \<open>\<forall> t\<in>{r,p,q}-{u}. ?d t = -1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>{r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) = - 1
[PROOF STEP]
have "\<dots> = j *\<^sub>R proj2_rep ?s + (\<Sum> t\<in>{r,p,q}-{u}. ?d t *\<^sub>R proj2_rep t)"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>{r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) = - 1

goal (1 subgoal):
 1. j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) - sum proj2_rep ({r, p, q} - {u}) = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)
[PROOF STEP]
by (simp add: sum_negf)
[PROOF STATE]
proof (state)
this:
j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) - sum proj2_rep ({r, p, q} - {u}) = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) - sum proj2_rep ({r, p, q} - {u}) = j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
from \<open>finite ({r,p,q} - {u})\<close>  and \<open>?s \<notin> {r,p,q} - {u}\<close>
[PROOF STATE]
proof (chain)
picking this:
finite ({r, p, q} - {u})
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q} - {u}
[PROOF STEP]
have "\<dots> = (\<Sum> t\<in>insert ?s ({r,p,q}-{u}). ?d t *\<^sub>R proj2_rep t)"
[PROOF STATE]
proof (prove)
using this:
finite ({r, p, q} - {u})
proj2_abs (sum proj2_rep {r, p, q}) \<notin> {r, p, q} - {u}

goal (1 subgoal):
 1. j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t) = (\<Sum>t\<in>insert (proj2_abs (sum proj2_rep {r, p, q})) ({r, p, q} - {u}). (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)
[PROOF STEP]
by (simp add: sum.insert)
[PROOF STATE]
proof (state)
this:
j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t) = (\<Sum>t\<in>insert (proj2_abs (sum proj2_rep {r, p, q})) ({r, p, q} - {u}). (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
j *\<^sub>R proj2_rep (proj2_abs (sum proj2_rep {r, p, q})) + (\<Sum>t\<in>{r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t) = (\<Sum>t\<in>insert (proj2_abs (sum proj2_rep {r, p, q})) ({r, p, q} - {u}). (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
from \<open>insert ?s ({r,p,q} - {u}) = ?S - {u}\<close>
[PROOF STATE]
proof (chain)
picking this:
insert (proj2_abs (sum proj2_rep {r, p, q})) ({r, p, q} - {u}) = {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}
[PROOF STEP]
have "\<dots> = (\<Sum> t\<in>?S-{u}. ?d t *\<^sub>R proj2_rep t)"
[PROOF STATE]
proof (prove)
using this:
insert (proj2_abs (sum proj2_rep {r, p, q})) ({r, p, q} - {u}) = {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}

goal (1 subgoal):
 1. (\<Sum>t\<in>insert (proj2_abs (sum proj2_rep {r, p, q})) ({r, p, q} - {u}). (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t) = (\<Sum>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>t\<in>insert (proj2_abs (sum proj2_rep {r, p, q})) ({r, p, q} - {u}). (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t) = (\<Sum>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
proj2_rep u = (\<Sum>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)
[PROOF STEP]
have "proj2_rep u = (\<Sum> t\<in>?S-{u}. ?d t *\<^sub>R proj2_rep t)"
[PROOF STATE]
proof (prove)
using this:
proj2_rep u = (\<Sum>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. proj2_rep u = (\<Sum>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
proj2_rep u = (\<Sum>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
proj2_rep u = (\<Sum>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
have "\<forall> t\<in>?S-{u}. ?d t *\<^sub>R proj2_rep t \<in> span (proj2_rep ` (?S - {u}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
by (simp add: span_clauses)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
proj2_rep u = (\<Sum>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)
\<forall>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
have "proj2_rep u \<in> span (proj2_rep ` (?S - {u}))"
[PROOF STATE]
proof (prove)
using this:
proj2_rep u = (\<Sum>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t)
\<forall>t\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}. (if t = proj2_abs (sum proj2_rep {r, p, q}) then j else - 1) *\<^sub>R proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. proj2_rep u \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
by (metis (no_types, lifting) span_sum)
[PROOF STATE]
proof (state)
this:
proj2_rep u \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
have "\<forall> t\<in>{r,p,q}. proj2_rep t \<in> span (proj2_rep ` (?S - {u}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>{r, p, q}. proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> {r, p, q} \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> {r, p, q} \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
assume "t \<in> {r,p,q}"
[PROOF STATE]
proof (state)
this:
t \<in> {r, p, q}

goal (1 subgoal):
 1. \<And>t. t \<in> {r, p, q} \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
show "proj2_rep t \<in> span (proj2_rep ` (?S - {u}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
 2. \<not> ?P \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
assume "t = u"
[PROOF STATE]
proof (state)
this:
t = u

goal (2 subgoals):
 1. ?P \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
 2. \<not> ?P \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
from \<open>proj2_rep u \<in> span (image proj2_rep (?S - {u}))\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_rep u \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
show "proj2_rep t \<in> span (proj2_rep ` (?S - {u}))"
[PROOF STATE]
proof (prove)
using this:
proj2_rep u \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
by (subst \<open>t = u\<close>)
[PROOF STATE]
proof (state)
this:
proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. t \<noteq> u \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<noteq> u \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
assume "t \<noteq> u"
[PROOF STATE]
proof (state)
this:
t \<noteq> u

goal (1 subgoal):
 1. t \<noteq> u \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
with \<open>t \<in> {r,p,q}\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<in> {r, p, q}
t \<noteq> u
[PROOF STEP]
have "proj2_rep t \<in> proj2_rep ` (?S - {u})"
[PROOF STATE]
proof (prove)
using this:
t \<in> {r, p, q}
t \<noteq> u

goal (1 subgoal):
 1. proj2_rep t \<in> proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep t \<in> proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})

goal (1 subgoal):
 1. t \<noteq> u \<Longrightarrow> proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
with span_superset [of "proj2_rep ` (?S - {u})"]
[PROOF STATE]
proof (chain)
picking this:
proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}) \<subseteq> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
proj2_rep t \<in> proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
show "proj2_rep t \<in> span (proj2_rep ` (?S - {u}))"
[PROOF STATE]
proof (prove)
using this:
proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}) \<subseteq> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
proj2_rep t \<in> proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})

goal (1 subgoal):
 1. proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>{r, p, q}. proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
hence "proj2_rep ` {r,p,q} \<subseteq> span (proj2_rep ` (?S - {u}))"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>{r, p, q}. proj2_rep t \<in> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. proj2_rep ` {r, p, q} \<subseteq> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
by (simp only: image_subset_iff)
[PROOF STATE]
proof (state)
this:
proj2_rep ` {r, p, q} \<subseteq> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
hence
        "span (proj2_rep ` {r,p,q}) \<subseteq> span (span (proj2_rep ` (?S - {u})))"
[PROOF STATE]
proof (prove)
using this:
proj2_rep ` {r, p, q} \<subseteq> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. span (proj2_rep ` {r, p, q}) \<subseteq> span (span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})))
[PROOF STEP]
by (simp only: span_mono)
[PROOF STATE]
proof (state)
this:
span (proj2_rep ` {r, p, q}) \<subseteq> span (span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})))

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
hence "span (proj2_rep ` {r,p,q}) \<subseteq> span (proj2_rep ` (?S - {u}))"
[PROOF STATE]
proof (prove)
using this:
span (proj2_rep ` {r, p, q}) \<subseteq> span (span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})))

goal (1 subgoal):
 1. span (proj2_rep ` {r, p, q}) \<subseteq> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
[PROOF STEP]
by (simp only: span_span)
[PROOF STATE]
proof (state)
this:
span (proj2_rep ` {r, p, q}) \<subseteq> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
span (proj2_rep ` {r, p, q}) \<subseteq> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
from \<open>\<not> proj2_set_Col {r,p,q}\<close>
        and \<open>card {r,p,q} = 3\<close>
        and not_proj2_set_Col_iff_span
[PROOF STATE]
proof (chain)
picking this:
\<not> proj2_set_Col {r, p, q}
card {r, p, q} = 3
card ?S = 3 \<Longrightarrow> (\<not> proj2_set_Col ?S) = (span (proj2_rep ` ?S) = UNIV)
[PROOF STEP]
have "span (proj2_rep ` {r,p,q}) = UNIV"
[PROOF STATE]
proof (prove)
using this:
\<not> proj2_set_Col {r, p, q}
card {r, p, q} = 3
card ?S = 3 \<Longrightarrow> (\<not> proj2_set_Col ?S) = (span (proj2_rep ` ?S) = UNIV)

goal (1 subgoal):
 1. span (proj2_rep ` {r, p, q}) = UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
span (proj2_rep ` {r, p, q}) = UNIV

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
span (proj2_rep ` {r, p, q}) \<subseteq> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
span (proj2_rep ` {r, p, q}) = UNIV
[PROOF STEP]
have "span (proj2_rep ` (?S - {u})) = UNIV"
[PROOF STATE]
proof (prove)
using this:
span (proj2_rep ` {r, p, q}) \<subseteq> span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}))
span (proj2_rep ` {r, p, q}) = UNIV

goal (1 subgoal):
 1. span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})) = UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})) = UNIV

goal (1 subgoal):
 1. u \<noteq> proj2_abs (sum proj2_rep {r, p, q}) \<Longrightarrow> \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
with \<open>card (?S - {u}) = 3\<close> and not_proj2_set_Col_iff_span
[PROOF STATE]
proof (chain)
picking this:
card ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}) = 3
card ?S = 3 \<Longrightarrow> (\<not> proj2_set_Col ?S) = (span (proj2_rep ` ?S) = UNIV)
span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})) = UNIV
[PROOF STEP]
show "\<not> proj2_set_Col (?S - {u})"
[PROOF STATE]
proof (prove)
using this:
card ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u}) = 3
card ?S = 3 \<Longrightarrow> (\<not> proj2_set_Col ?S) = (span (proj2_rep ` ?S) = UNIV)
span (proj2_rep ` ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})) = UNIV

goal (1 subgoal):
 1. \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q}. \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
with \<open>card ?S = 4\<close>
[PROOF STATE]
proof (chain)
picking this:
card {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} = 4
\<forall>u\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q}. \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})
[PROOF STEP]
have "proj2_no_3_Col ?S"
[PROOF STATE]
proof (prove)
using this:
card {proj2_abs (sum proj2_rep {r, p, q}), r, p, q} = 4
\<forall>u\<in>{proj2_abs (sum proj2_rep {r, p, q}), r, p, q}. \<not> proj2_set_Col ({proj2_abs (sum proj2_rep {r, p, q}), r, p, q} - {u})

goal (1 subgoal):
 1. proj2_no_3_Col {proj2_abs (sum proj2_rep {r, p, q}), r, p, q}
[PROOF STEP]
by (unfold proj2_no_3_Col_def) fast
[PROOF STATE]
proof (state)
this:
proj2_no_3_Col {proj2_abs (sum proj2_rep {r, p, q}), r, p, q}

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
thus "\<exists> s. proj2_no_3_Col {s,r,p,q}"
[PROOF STATE]
proof (prove)
using this:
proj2_no_3_Col {proj2_abs (sum proj2_rep {r, p, q}), r, p, q}

goal (1 subgoal):
 1. \<exists>s. proj2_no_3_Col {s, r, p, q}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>s. proj2_no_3_Col {s, r, p, q}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_set_Col_expand:
  assumes "proj2_set_Col S" and "{p,q,r} \<subseteq> S" and "p \<noteq> q" and "r \<noteq> p"
  shows "\<exists> k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
from \<open>proj2_set_Col S\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col S
[PROOF STEP]
obtain l where "\<forall> t\<in>S. proj2_incident t l"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col S

goal (1 subgoal):
 1. (\<And>l. \<forall>t\<in>S. proj2_incident t l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding proj2_set_Col_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l. \<forall>p\<in>S. proj2_incident p l

goal (1 subgoal):
 1. (\<And>l. \<forall>t\<in>S. proj2_incident t l \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>S. proj2_incident t l

goal (1 subgoal):
 1. \<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
with \<open>{p,q,r} \<subseteq> S\<close> and \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and proj2_incident_iff [of p q l r]
[PROOF STATE]
proof (chain)
picking this:
{p, q, r} \<subseteq> S
p \<noteq> q
r \<noteq> p
\<lbrakk>p \<noteq> q; proj2_incident p l; proj2_incident q l\<rbrakk> \<Longrightarrow> proj2_incident r l = (r = p \<or> (\<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)))
\<forall>t\<in>S. proj2_incident t l
[PROOF STEP]
show "\<exists> k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)"
[PROOF STATE]
proof (prove)
using this:
{p, q, r} \<subseteq> S
p \<noteq> q
r \<noteq> p
\<lbrakk>p \<noteq> q; proj2_incident p l; proj2_incident q l\<rbrakk> \<Longrightarrow> proj2_incident r l = (r = p \<or> (\<exists>k. r = proj2_abs (k *\<^sub>R proj2_rep p + proj2_rep q)))
\<forall>t\<in>S. proj2_incident t l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_rep_in: "cltn2_rep B \<in> Rep_cltn2 B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_rep B \<in> Rep_cltn2 B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_rep B \<in> Rep_cltn2 B
[PROOF STEP]
let ?A = "cltn2_rep B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_rep B \<in> Rep_cltn2 B
[PROOF STEP]
from quotient_element_nonempty and
    invertible_proportionality_equiv and
    Rep_cltn2 [of B]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>equiv ?A ?r; ?X \<in> ?A // ?r\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> ?X
equiv (Collect invertible) invertible_proportionality
Rep_cltn2 B \<in> Collect invertible // invertible_proportionality
[PROOF STEP]
have "\<exists> C. C \<in> Rep_cltn2 B"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>equiv ?A ?r; ?X \<in> ?A // ?r\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> ?X
equiv (Collect invertible) invertible_proportionality
Rep_cltn2 B \<in> Collect invertible // invertible_proportionality

goal (1 subgoal):
 1. \<exists>C. C \<in> Rep_cltn2 B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>C. C \<in> Rep_cltn2 B

goal (1 subgoal):
 1. cltn2_rep B \<in> Rep_cltn2 B
[PROOF STEP]
with someI_ex [of "\<lambda> C. C \<in> Rep_cltn2 B"]
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> Rep_cltn2 B \<Longrightarrow> (SOME x. x \<in> Rep_cltn2 B) \<in> Rep_cltn2 B
\<exists>C. C \<in> Rep_cltn2 B
[PROOF STEP]
show "?A \<in> Rep_cltn2 B"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> Rep_cltn2 B \<Longrightarrow> (SOME x. x \<in> Rep_cltn2 B) \<in> Rep_cltn2 B
\<exists>C. C \<in> Rep_cltn2 B

goal (1 subgoal):
 1. cltn2_rep B \<in> Rep_cltn2 B
[PROOF STEP]
unfolding cltn2_rep_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> Rep_cltn2 B \<Longrightarrow> (SOME x. x \<in> Rep_cltn2 B) \<in> Rep_cltn2 B
\<exists>C. C \<in> Rep_cltn2 B

goal (1 subgoal):
 1. (SOME Ba. Ba \<in> Rep_cltn2 B) \<in> Rep_cltn2 B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_rep B \<in> Rep_cltn2 B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_rep_invertible: "invertible (cltn2_rep A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible (cltn2_rep A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invertible (cltn2_rep A)
[PROOF STEP]
from
    Union_quotient [of "Collect invertible" invertible_proportionality]
    and invertible_proportionality_equiv
    and Rep_cltn2 [of A] and cltn2_rep_in [of A]
[PROOF STATE]
proof (chain)
picking this:
equiv (Collect invertible) invertible_proportionality \<Longrightarrow> \<Union> (Collect invertible // invertible_proportionality) = Collect invertible
equiv (Collect invertible) invertible_proportionality
Rep_cltn2 A \<in> Collect invertible // invertible_proportionality
cltn2_rep A \<in> Rep_cltn2 A
[PROOF STEP]
have "cltn2_rep A \<in> Collect invertible"
[PROOF STATE]
proof (prove)
using this:
equiv (Collect invertible) invertible_proportionality \<Longrightarrow> \<Union> (Collect invertible // invertible_proportionality) = Collect invertible
equiv (Collect invertible) invertible_proportionality
Rep_cltn2 A \<in> Collect invertible // invertible_proportionality
cltn2_rep A \<in> Rep_cltn2 A

goal (1 subgoal):
 1. cltn2_rep A \<in> Collect invertible
[PROOF STEP]
unfolding quotient_def
[PROOF STATE]
proof (prove)
using this:
equiv (Collect invertible) invertible_proportionality \<Longrightarrow> \<Union> (\<Union>x\<in>Collect invertible. {invertible_proportionality `` {x}}) = Collect invertible
equiv (Collect invertible) invertible_proportionality
Rep_cltn2 A \<in> (\<Union>x\<in>Collect invertible. {invertible_proportionality `` {x}})
cltn2_rep A \<in> Rep_cltn2 A

goal (1 subgoal):
 1. cltn2_rep A \<in> Collect invertible
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cltn2_rep A \<in> Collect invertible

goal (1 subgoal):
 1. invertible (cltn2_rep A)
[PROOF STEP]
thus "invertible (cltn2_rep A)"
[PROOF STATE]
proof (prove)
using this:
cltn2_rep A \<in> Collect invertible

goal (1 subgoal):
 1. invertible (cltn2_rep A)
[PROOF STEP]
unfolding invertible_proportionality_def
[PROOF STATE]
proof (prove)
using this:
cltn2_rep A \<in> Collect invertible

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_rep_abs:
  fixes A :: "real^3^3"
  assumes "invertible A"
  shows "(A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality
[PROOF STEP]
from \<open>invertible A\<close>
[PROOF STATE]
proof (chain)
picking this:
invertible A
[PROOF STEP]
have "invertible_proportionality `` {A} \<in> (Collect invertible :: (real^3^3) set)//invertible_proportionality"
[PROOF STATE]
proof (prove)
using this:
invertible A

goal (1 subgoal):
 1. invertible_proportionality `` {A} \<in> Collect invertible // invertible_proportionality
[PROOF STEP]
unfolding quotient_def
[PROOF STATE]
proof (prove)
using this:
invertible A

goal (1 subgoal):
 1. invertible_proportionality `` {A} \<in> (\<Union>x\<in>Collect invertible. {invertible_proportionality `` {x}})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible_proportionality `` {A} \<in> Collect invertible // invertible_proportionality

goal (1 subgoal):
 1. (A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality
[PROOF STEP]
with Abs_cltn2_inverse
[PROOF STATE]
proof (chain)
picking this:
?y \<in> Collect invertible // invertible_proportionality \<Longrightarrow> Rep_cltn2 (Abs_cltn2 ?y) = ?y
invertible_proportionality `` {A} \<in> Collect invertible // invertible_proportionality
[PROOF STEP]
have "Rep_cltn2 (cltn2_abs A) = invertible_proportionality `` {A}"
[PROOF STATE]
proof (prove)
using this:
?y \<in> Collect invertible // invertible_proportionality \<Longrightarrow> Rep_cltn2 (Abs_cltn2 ?y) = ?y
invertible_proportionality `` {A} \<in> Collect invertible // invertible_proportionality

goal (1 subgoal):
 1. Rep_cltn2 (cltn2_abs A) = invertible_proportionality `` {A}
[PROOF STEP]
unfolding cltn2_abs_def
[PROOF STATE]
proof (prove)
using this:
?y \<in> Collect invertible // invertible_proportionality \<Longrightarrow> Rep_cltn2 (Abs_cltn2 ?y) = ?y
invertible_proportionality `` {A} \<in> Collect invertible // invertible_proportionality

goal (1 subgoal):
 1. Rep_cltn2 (Abs_cltn2 (invertible_proportionality `` {A})) = invertible_proportionality `` {A}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rep_cltn2 (cltn2_abs A) = invertible_proportionality `` {A}

goal (1 subgoal):
 1. (A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality
[PROOF STEP]
with cltn2_rep_in
[PROOF STATE]
proof (chain)
picking this:
cltn2_rep ?B \<in> Rep_cltn2 ?B
Rep_cltn2 (cltn2_abs A) = invertible_proportionality `` {A}
[PROOF STEP]
have "cltn2_rep (cltn2_abs A) \<in> invertible_proportionality `` {A}"
[PROOF STATE]
proof (prove)
using this:
cltn2_rep ?B \<in> Rep_cltn2 ?B
Rep_cltn2 (cltn2_abs A) = invertible_proportionality `` {A}

goal (1 subgoal):
 1. cltn2_rep (cltn2_abs A) \<in> invertible_proportionality `` {A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cltn2_rep (cltn2_abs A) \<in> invertible_proportionality `` {A}

goal (1 subgoal):
 1. (A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality
[PROOF STEP]
thus "(A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality"
[PROOF STATE]
proof (prove)
using this:
cltn2_rep (cltn2_abs A) \<in> invertible_proportionality `` {A}

goal (1 subgoal):
 1. (A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_rep_abs2:
  assumes "invertible A"
  shows "\<exists> k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs A) = k *\<^sub>R A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs A) = k *\<^sub>R A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs A) = k *\<^sub>R A
[PROOF STEP]
from \<open>invertible A\<close> and cltn2_rep_abs
[PROOF STATE]
proof (chain)
picking this:
invertible A
invertible ?A \<Longrightarrow> (?A, cltn2_rep (cltn2_abs ?A)) \<in> invertible_proportionality
[PROOF STEP]
have "(A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality"
[PROOF STATE]
proof (prove)
using this:
invertible A
invertible ?A \<Longrightarrow> (?A, cltn2_rep (cltn2_abs ?A)) \<in> invertible_proportionality

goal (1 subgoal):
 1. (A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(A, cltn2_rep (cltn2_abs A)) \<in> invertible_proportionality

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

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

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

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

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> cltn2_rep (cltn2_abs A) = k *\<^sub>R A
[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> cltn2_rep (cltn2_abs A) = k *\<^sub>R A
[PROOF STEP]
let ?k = "1/c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs A) = k *\<^sub>R A
[PROOF STEP]
from \<open>A = c *\<^sub>R cltn2_rep (cltn2_abs A)\<close>
[PROOF STATE]
proof (chain)
picking this:
A = c *\<^sub>R cltn2_rep (cltn2_abs A)
[PROOF STEP]
have "?k *\<^sub>R A = ?k *\<^sub>R c *\<^sub>R cltn2_rep (cltn2_abs A)"
[PROOF STATE]
proof (prove)
using this:
A = c *\<^sub>R cltn2_rep (cltn2_abs A)

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_abs_rep: "cltn2_abs (cltn2_rep A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_abs (cltn2_rep A) = A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_abs (cltn2_rep A) = A
[PROOF STEP]
from partition_Image_element
  [of "Collect invertible"
    invertible_proportionality
    "Rep_cltn2 A"
    "cltn2_rep A"]
    and invertible_proportionality_equiv
    and Rep_cltn2 [of A] and cltn2_rep_in [of A]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>equiv (Collect invertible) invertible_proportionality; Rep_cltn2 A \<in> Collect invertible // invertible_proportionality; cltn2_rep A \<in> Rep_cltn2 A\<rbrakk> \<Longrightarrow> invertible_proportionality `` {cltn2_rep A} = Rep_cltn2 A
equiv (Collect invertible) invertible_proportionality
Rep_cltn2 A \<in> Collect invertible // invertible_proportionality
cltn2_rep A \<in> Rep_cltn2 A
[PROOF STEP]
have "invertible_proportionality `` {cltn2_rep A} = Rep_cltn2 A"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>equiv (Collect invertible) invertible_proportionality; Rep_cltn2 A \<in> Collect invertible // invertible_proportionality; cltn2_rep A \<in> Rep_cltn2 A\<rbrakk> \<Longrightarrow> invertible_proportionality `` {cltn2_rep A} = Rep_cltn2 A
equiv (Collect invertible) invertible_proportionality
Rep_cltn2 A \<in> Collect invertible // invertible_proportionality
cltn2_rep A \<in> Rep_cltn2 A

goal (1 subgoal):
 1. invertible_proportionality `` {cltn2_rep A} = Rep_cltn2 A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invertible_proportionality `` {cltn2_rep A} = Rep_cltn2 A

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep A) = A
[PROOF STEP]
with Rep_cltn2_inverse
[PROOF STATE]
proof (chain)
picking this:
Abs_cltn2 (Rep_cltn2 ?x) = ?x
invertible_proportionality `` {cltn2_rep A} = Rep_cltn2 A
[PROOF STEP]
show "cltn2_abs (cltn2_rep A) = A"
[PROOF STATE]
proof (prove)
using this:
Abs_cltn2 (Rep_cltn2 ?x) = ?x
invertible_proportionality `` {cltn2_rep A} = Rep_cltn2 A

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep A) = A
[PROOF STEP]
unfolding cltn2_abs_def
[PROOF STATE]
proof (prove)
using this:
Abs_cltn2 (Rep_cltn2 ?x) = ?x
invertible_proportionality `` {cltn2_rep A} = Rep_cltn2 A

goal (1 subgoal):
 1. Abs_cltn2 (invertible_proportionality `` {cltn2_rep A}) = A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_abs (cltn2_rep A) = A

goal:
No subgoals!
[PROOF STEP]
qed