[STATEMENT]
lemma proj2_Col_coeff_unique':
  assumes "a \<noteq> 0" and "r \<noteq> 0" and "proj2_abs a \<noteq> proj2_abs r"
  and "proj2_abs (i *\<^sub>R a + r) = proj2_abs (j *\<^sub>R a + r)"
  shows "i = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
from \<open>a \<noteq> 0\<close> and \<open>r \<noteq> 0\<close> and \<open>proj2_abs a \<noteq> proj2_abs r\<close>
    and dependent_proj2_abs [of a r _ 1]
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> 0
r \<noteq> 0
proj2_abs a \<noteq> proj2_abs r
\<lbrakk>a \<noteq> 0; r \<noteq> 0; ?i \<noteq> 0 \<or> 1 \<noteq> 0; ?i *\<^sub>R a + 1 *\<^sub>R r = 0\<rbrakk> \<Longrightarrow> proj2_abs a = proj2_abs r
[PROOF STEP]
have "i *\<^sub>R a + r \<noteq> 0" and "j *\<^sub>R a + r \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
r \<noteq> 0
proj2_abs a \<noteq> proj2_abs r
\<lbrakk>a \<noteq> 0; r \<noteq> 0; ?i \<noteq> 0 \<or> 1 \<noteq> 0; ?i *\<^sub>R a + 1 *\<^sub>R r = 0\<rbrakk> \<Longrightarrow> proj2_abs a = proj2_abs r

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

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

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

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

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

goal (1 subgoal):
 1. i = j
[PROOF STEP]
hence "(k * i - l * j) *\<^sub>R a + (k - l) *\<^sub>R r = 0"
[PROOF STATE]
proof (prove)
using this:
(k * i) *\<^sub>R a + k *\<^sub>R r = (l * j) *\<^sub>R a + l *\<^sub>R r

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

goal (1 subgoal):
 1. i = j
[PROOF STEP]
with \<open>a \<noteq> 0\<close> and \<open>r \<noteq> 0\<close> and \<open>proj2_abs a \<noteq> proj2_abs r\<close>
    and dependent_proj2_abs [of a r "k * i - l * j" "k - l"]
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> 0
r \<noteq> 0
proj2_abs a \<noteq> proj2_abs r
\<lbrakk>a \<noteq> 0; r \<noteq> 0; k * i - l * j \<noteq> 0 \<or> k - l \<noteq> 0; (k * i - l * j) *\<^sub>R a + (k - l) *\<^sub>R r = 0\<rbrakk> \<Longrightarrow> proj2_abs a = proj2_abs r
(k * i - l * j) *\<^sub>R a + (k - l) *\<^sub>R r = 0
[PROOF STEP]
have "k * i - l * j = 0" and "k - l = 0"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
r \<noteq> 0
proj2_abs a \<noteq> proj2_abs r
\<lbrakk>a \<noteq> 0; r \<noteq> 0; k * i - l * j \<noteq> 0 \<or> k - l \<noteq> 0; (k * i - l * j) *\<^sub>R a + (k - l) *\<^sub>R r = 0\<rbrakk> \<Longrightarrow> proj2_abs a = proj2_abs r
(k * i - l * j) *\<^sub>R a + (k - l) *\<^sub>R r = 0

goal (1 subgoal):
 1. k * i - l * j = 0 &&& k - l = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k * i - l * j = 0
k - l = 0

goal (1 subgoal):
 1. i = j
[PROOF STEP]
from \<open>k - l = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
k - l = 0
[PROOF STEP]
have "k = l"
[PROOF STATE]
proof (prove)
using this:
k - l = 0

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

goal (1 subgoal):
 1. i = j
[PROOF STEP]
with \<open>k * i - l * j = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
k * i - l * j = 0
k = l
[PROOF STEP]
have "k * i = k * j"
[PROOF STATE]
proof (prove)
using this:
k * i - l * j = 0
k = l

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_Col_coeff_unique:
  assumes "a \<noteq> r"
  and "proj2_abs (i *\<^sub>R proj2_rep a + proj2_rep r)
  = proj2_abs (j *\<^sub>R proj2_rep a + proj2_rep r)"
  shows "i = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
let ?a' = "proj2_rep a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
let ?r' = "proj2_rep r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
have "?a' \<noteq> 0" and "?r' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep a \<noteq> 0 &&& proj2_rep r \<noteq> 0
[PROOF STEP]
by (rule proj2_rep_non_zero)+
[PROOF STATE]
proof (state)
this:
proj2_rep a \<noteq> 0
proj2_rep r \<noteq> 0

goal (1 subgoal):
 1. i = j
[PROOF STEP]
from \<open>a \<noteq> r\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> r
[PROOF STEP]
have "proj2_abs ?a' \<noteq> proj2_abs ?r'"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> r

goal (1 subgoal):
 1. proj2_abs (proj2_rep a) \<noteq> proj2_abs (proj2_rep r)
[PROOF STEP]
by (simp add: proj2_abs_rep)
[PROOF STATE]
proof (state)
this:
proj2_abs (proj2_rep a) \<noteq> proj2_abs (proj2_rep r)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L2P_P2L [simp]: "L2P (P2L p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L2P (P2L p) = p
[PROOF STEP]
unfolding L2P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case P2L p of P2L p \<Rightarrow> p) = p
[PROOF STEP]
by simp


[STATEMENT]
lemma P2L_L2P [simp]: "P2L (L2P l) = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P2L (L2P l) = l
[PROOF STEP]
by (induct l) simp


[STATEMENT]
lemma L2P_inj [simp]:
  assumes "L2P l = L2P m"
  shows "l = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = m
[PROOF STEP]
using P2L_L2P [of l] and assms
[PROOF STATE]
proof (prove)
using this:
P2L (L2P l) = l
L2P l = L2P m

goal (1 subgoal):
 1. l = m
[PROOF STEP]
by simp


[STATEMENT]
lemma P2L_to_L2P: "P2L p = l \<longleftrightarrow> p = L2P l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P2L p = l) = (p = L2P l)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P2L p = l \<Longrightarrow> p = L2P l
 2. p = L2P l \<Longrightarrow> P2L p = l
[PROOF STEP]
assume "P2L p = l"
[PROOF STATE]
proof (state)
this:
P2L p = l

goal (2 subgoals):
 1. P2L p = l \<Longrightarrow> p = L2P l
 2. p = L2P l \<Longrightarrow> P2L p = l
[PROOF STEP]
hence "L2P (P2L p) = L2P l"
[PROOF STATE]
proof (prove)
using this:
P2L p = l

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

goal (2 subgoals):
 1. P2L p = l \<Longrightarrow> p = L2P l
 2. p = L2P l \<Longrightarrow> P2L p = l
[PROOF STEP]
thus "p = L2P l"
[PROOF STATE]
proof (prove)
using this:
L2P (P2L p) = L2P l

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

goal (1 subgoal):
 1. p = L2P l \<Longrightarrow> P2L p = l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = L2P l \<Longrightarrow> P2L p = l
[PROOF STEP]
assume "p = L2P l"
[PROOF STATE]
proof (state)
this:
p = L2P l

goal (1 subgoal):
 1. p = L2P l \<Longrightarrow> P2L p = l
[PROOF STEP]
thus "P2L p = l"
[PROOF STATE]
proof (prove)
using this:
p = L2P l

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_line_rep_abs:
  assumes "v \<noteq> 0"
  shows "\<exists> k. k \<noteq> 0 \<and> proj2_line_rep (proj2_line_abs v) = k *\<^sub>R v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_line_rep (proj2_line_abs v) = k *\<^sub>R v
[PROOF STEP]
unfolding proj2_line_rep_def and proj2_line_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep (L2P (P2L (proj2_abs v))) = k *\<^sub>R v
[PROOF STEP]
using proj2_rep_abs2 and \<open>v \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
v \<noteq> 0

goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> proj2_rep (L2P (P2L (proj2_abs v))) = k *\<^sub>R v
[PROOF STEP]
by simp


[STATEMENT]
lemma proj2_line_abs_rep [simp]: "proj2_line_abs (proj2_line_rep l) = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_line_abs (proj2_line_rep l) = l
[PROOF STEP]
unfolding proj2_line_abs_def and proj2_line_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P2L (proj2_abs (proj2_rep (L2P l))) = l
[PROOF STEP]
by (simp add: proj2_abs_rep)


[STATEMENT]
lemma proj2_line_rep_non_zero: "proj2_line_rep l \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_line_rep l \<noteq> 0
[PROOF STEP]
unfolding proj2_line_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep (L2P l) \<noteq> 0
[PROOF STEP]
using proj2_rep_non_zero
[PROOF STATE]
proof (prove)
using this:
proj2_rep ?x \<noteq> 0

goal (1 subgoal):
 1. proj2_rep (L2P l) \<noteq> 0
[PROOF STEP]
by simp


[STATEMENT]
lemma proj2_line_rep_dependent:
  assumes "i *\<^sub>R proj2_line_rep l + j *\<^sub>R proj2_line_rep m = 0"
  and "i \<noteq> 0 \<or> j \<noteq> 0"
  shows "l = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = m
[PROOF STEP]
using proj2_rep_dependent [of i "L2P l" j "L2P m"] and assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i *\<^sub>R proj2_rep (L2P l) + j *\<^sub>R proj2_rep (L2P m) = 0; i \<noteq> 0 \<or> j \<noteq> 0\<rbrakk> \<Longrightarrow> L2P l = L2P m
i *\<^sub>R proj2_line_rep l + j *\<^sub>R proj2_line_rep m = 0
i \<noteq> 0 \<or> j \<noteq> 0

goal (1 subgoal):
 1. l = m
[PROOF STEP]
unfolding proj2_line_rep_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i *\<^sub>R proj2_rep (L2P l) + j *\<^sub>R proj2_rep (L2P m) = 0; i \<noteq> 0 \<or> j \<noteq> 0\<rbrakk> \<Longrightarrow> L2P l = L2P m
i *\<^sub>R proj2_rep (L2P l) + j *\<^sub>R proj2_rep (L2P m) = 0
i \<noteq> 0 \<or> j \<noteq> 0

goal (1 subgoal):
 1. l = m
[PROOF STEP]
by simp


[STATEMENT]
lemma proj2_line_abs_mult:
  assumes "k \<noteq> 0"
  shows "proj2_line_abs (k *\<^sub>R v) = proj2_line_abs v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_line_abs (k *\<^sub>R v) = proj2_line_abs v
[PROOF STEP]
unfolding proj2_line_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P2L (proj2_abs (k *\<^sub>R v)) = P2L (proj2_abs v)
[PROOF STEP]
using \<open>k \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0

goal (1 subgoal):
 1. P2L (proj2_abs (k *\<^sub>R v)) = P2L (proj2_abs v)
[PROOF STEP]
by (subst proj2_abs_mult) simp_all


[STATEMENT]
lemma proj2_line_abs_abs_mult:
  assumes "proj2_line_abs v = proj2_line_abs w" and "w \<noteq> 0"
  shows "\<exists> k. v = k *\<^sub>R w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. v = k *\<^sub>R w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proj2_line_abs v = proj2_line_abs w
w \<noteq> 0

goal (1 subgoal):
 1. \<exists>k. v = k *\<^sub>R w
[PROOF STEP]
by (unfold proj2_line_abs_def) (simp add: proj2_abs_abs_mult)


[STATEMENT]
lemma proj2_points_define_line:
  shows "\<exists> l. proj2_incident p l \<and> proj2_incident q l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
let ?p' = "proj2_rep p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
let ?q' = "proj2_rep q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
let ?B = "{?p', ?q'}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
from card_suc_ge_insert [of ?p' "{?q'}"]
[PROOF STATE]
proof (chain)
picking this:
card {proj2_rep p, proj2_rep q} \<le> card {proj2_rep q} + 1
[PROOF STEP]
have "card ?B \<le> 2"
[PROOF STATE]
proof (prove)
using this:
card {proj2_rep p, proj2_rep q} \<le> card {proj2_rep q} + 1

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

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
with dim_le_card' [of ?B]
[PROOF STATE]
proof (chain)
picking this:
finite {proj2_rep p, proj2_rep q} \<Longrightarrow> dim {proj2_rep p, proj2_rep q} \<le> card {proj2_rep p, proj2_rep q}
card {proj2_rep p, proj2_rep q} \<le> 2
[PROOF STEP]
have "dim ?B < 3"
[PROOF STATE]
proof (prove)
using this:
finite {proj2_rep p, proj2_rep q} \<Longrightarrow> dim {proj2_rep p, proj2_rep q} \<le> card {proj2_rep p, proj2_rep q}
card {proj2_rep p, proj2_rep q} \<le> 2

goal (1 subgoal):
 1. dim {proj2_rep p, proj2_rep q} < 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim {proj2_rep p, proj2_rep q} < 3

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
with lowdim_subset_hyperplane [of ?B]
[PROOF STATE]
proof (chain)
picking this:
dim {proj2_rep p, proj2_rep q} < DIM((real, 3) vec) \<Longrightarrow> \<exists>a. a \<noteq> 0 \<and> span {proj2_rep p, proj2_rep q} \<subseteq> {x. a \<bullet> x = 0}
dim {proj2_rep p, proj2_rep q} < 3
[PROOF STEP]
obtain l' where "l' \<noteq> 0" and "span ?B \<subseteq> {x. l' \<bullet> x = 0}"
[PROOF STATE]
proof (prove)
using this:
dim {proj2_rep p, proj2_rep q} < DIM((real, 3) vec) \<Longrightarrow> \<exists>a. a \<noteq> 0 \<and> span {proj2_rep p, proj2_rep q} \<subseteq> {x. a \<bullet> x = 0}
dim {proj2_rep p, proj2_rep q} < 3

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' \<noteq> 0; span {proj2_rep p, proj2_rep q} \<subseteq> {x. l' \<bullet> x = 0}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' \<noteq> 0
span {proj2_rep p, proj2_rep q} \<subseteq> {x. l' \<bullet> x = 0}

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
let ?l = "proj2_line_abs l'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
let ?l'' = "proj2_line_rep ?l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
from proj2_line_rep_abs and \<open>l' \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_line_rep (proj2_line_abs ?v) = k *\<^sub>R ?v
l' \<noteq> 0
[PROOF STEP]
obtain k where "?l'' = k *\<^sub>R l'"
[PROOF STATE]
proof (prove)
using this:
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_line_rep (proj2_line_abs ?v) = k *\<^sub>R ?v
l' \<noteq> 0

goal (1 subgoal):
 1. (\<And>k. proj2_line_rep (proj2_line_abs l') = k *\<^sub>R l' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_line_rep (proj2_line_abs l') = k *\<^sub>R l'

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
have "?p' \<in> ?B" and "?q' \<in> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep p \<in> {proj2_rep p, proj2_rep q} &&& proj2_rep q \<in> {proj2_rep p, proj2_rep q}
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
proj2_rep p \<in> {proj2_rep p, proj2_rep q}
proj2_rep q \<in> {proj2_rep p, proj2_rep q}

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
with span_superset [of ?B] and \<open>span ?B \<subseteq> {x. l' \<bullet> x = 0}\<close>
[PROOF STATE]
proof (chain)
picking this:
{proj2_rep p, proj2_rep q} \<subseteq> span {proj2_rep p, proj2_rep q}
span {proj2_rep p, proj2_rep q} \<subseteq> {x. l' \<bullet> x = 0}
proj2_rep p \<in> {proj2_rep p, proj2_rep q}
proj2_rep q \<in> {proj2_rep p, proj2_rep q}
[PROOF STEP]
have "l' \<bullet> ?p' = 0" and "l' \<bullet> ?q' = 0"
[PROOF STATE]
proof (prove)
using this:
{proj2_rep p, proj2_rep q} \<subseteq> span {proj2_rep p, proj2_rep q}
span {proj2_rep p, proj2_rep q} \<subseteq> {x. l' \<bullet> x = 0}
proj2_rep p \<in> {proj2_rep p, proj2_rep q}
proj2_rep q \<in> {proj2_rep p, proj2_rep q}

goal (1 subgoal):
 1. l' \<bullet> proj2_rep p = 0 &&& l' \<bullet> proj2_rep q = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' \<bullet> proj2_rep p = 0
l' \<bullet> proj2_rep q = 0

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
hence "?p' \<bullet> l' = 0" and "?q' \<bullet> l' = 0"
[PROOF STATE]
proof (prove)
using this:
l' \<bullet> proj2_rep p = 0
l' \<bullet> proj2_rep q = 0

goal (1 subgoal):
 1. proj2_rep p \<bullet> l' = 0 &&& proj2_rep q \<bullet> l' = 0
[PROOF STEP]
by (simp_all add: inner_commute)
[PROOF STATE]
proof (state)
this:
proj2_rep p \<bullet> l' = 0
proj2_rep q \<bullet> l' = 0

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
with dot_scaleR_mult(2) [of _ k l'] and \<open>?l'' = k *\<^sub>R l'\<close>
[PROOF STATE]
proof (chain)
picking this:
?a \<bullet> k *\<^sub>R l' = k * (?a \<bullet> l')
proj2_line_rep (proj2_line_abs l') = k *\<^sub>R l'
proj2_rep p \<bullet> l' = 0
proj2_rep q \<bullet> l' = 0
[PROOF STEP]
have "proj2_incident p ?l \<and> proj2_incident q ?l"
[PROOF STATE]
proof (prove)
using this:
?a \<bullet> k *\<^sub>R l' = k * (?a \<bullet> l')
proj2_line_rep (proj2_line_abs l') = k *\<^sub>R l'
proj2_rep p \<bullet> l' = 0
proj2_rep q \<bullet> l' = 0

goal (1 subgoal):
 1. proj2_incident p (proj2_line_abs l') \<and> proj2_incident q (proj2_line_abs l')
[PROOF STEP]
unfolding proj2_incident_def
[PROOF STATE]
proof (prove)
using this:
?a \<bullet> k *\<^sub>R l' = k * (?a \<bullet> l')
proj2_line_rep (proj2_line_abs l') = k *\<^sub>R l'
proj2_rep p \<bullet> l' = 0
proj2_rep q \<bullet> l' = 0

goal (1 subgoal):
 1. proj2_rep p \<bullet> proj2_line_rep (proj2_line_abs l') = 0 \<and> proj2_rep q \<bullet> proj2_line_rep (proj2_line_abs l') = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_incident p (proj2_line_abs l') \<and> proj2_incident q (proj2_line_abs l')

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l
[PROOF STEP]
thus "\<exists> l. proj2_incident p l \<and> proj2_incident q l"
[PROOF STATE]
proof (prove)
using this:
proj2_incident p (proj2_line_abs l') \<and> proj2_incident q (proj2_line_abs l')

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_line_through_incident:
  shows "proj2_incident p (proj2_line_through p q)"
  and "proj2_incident q (proj2_line_through p q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident p (proj2_line_through p q) &&& proj2_incident q (proj2_line_through p q)
[PROOF STEP]
unfolding proj2_line_through_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident p (SOME l. proj2_incident p l \<and> proj2_incident q l) &&& proj2_incident q (SOME l. proj2_incident p l \<and> proj2_incident q l)
[PROOF STEP]
using proj2_points_define_line
    and someI_ex [of "\<lambda> l. proj2_incident p l \<and> proj2_incident q l"]
[PROOF STATE]
proof (prove)
using this:
\<exists>l. proj2_incident ?p l \<and> proj2_incident ?q l
\<exists>x. proj2_incident p x \<and> proj2_incident q x \<Longrightarrow> proj2_incident p (SOME x. proj2_incident p x \<and> proj2_incident q x) \<and> proj2_incident q (SOME x. proj2_incident p x \<and> proj2_incident q x)

goal (1 subgoal):
 1. proj2_incident p (SOME l. proj2_incident p l \<and> proj2_incident q l) &&& proj2_incident q (SOME l. proj2_incident p l \<and> proj2_incident q l)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma proj2_line_through_unique:
  assumes "p \<noteq> q" and "proj2_incident p l" and "proj2_incident q l"
  shows "l = proj2_line_through p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
let ?l' = "proj2_line_rep l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
let ?m = "proj2_line_through p q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
let ?m' = "proj2_line_rep ?m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
let ?p' = "proj2_rep p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
let ?q' = "proj2_rep q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
let ?A = "{?p', ?q'}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
let ?B = "insert ?m' ?A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
from proj2_line_through_incident
[PROOF STATE]
proof (chain)
picking this:
proj2_incident ?p (proj2_line_through ?p ?q)
proj2_incident ?q (proj2_line_through ?p ?q)
[PROOF STEP]
have "proj2_incident p ?m" and "proj2_incident q ?m"
[PROOF STATE]
proof (prove)
using this:
proj2_incident ?p (proj2_line_through ?p ?q)
proj2_incident ?q (proj2_line_through ?p ?q)

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

goal (1 subgoal):
 1. l = proj2_line_through p q
[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 p (proj2_line_through p q)
proj2_incident q (proj2_line_through p q)
[PROOF STEP]
have ortho: "\<And>w. w\<in>?A \<Longrightarrow> orthogonal ?m' w" "\<And>w. w\<in>?A \<Longrightarrow> orthogonal ?l' w"
[PROOF STATE]
proof (prove)
using this:
proj2_incident p l
proj2_incident q l
proj2_incident p (proj2_line_through p q)
proj2_incident q (proj2_line_through p q)

goal (1 subgoal):
 1. (\<And>w. w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep (proj2_line_through p q)) w) &&& (\<And>w. w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep l) w)
[PROOF STEP]
unfolding proj2_incident_def and orthogonal_def
[PROOF STATE]
proof (prove)
using this:
proj2_rep p \<bullet> proj2_line_rep l = 0
proj2_rep q \<bullet> proj2_line_rep l = 0
proj2_rep p \<bullet> proj2_line_rep (proj2_line_through p q) = 0
proj2_rep q \<bullet> proj2_line_rep (proj2_line_through p q) = 0

goal (1 subgoal):
 1. (\<And>w. w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> proj2_line_rep (proj2_line_through p q) \<bullet> w = 0) &&& (\<And>w. w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> proj2_line_rep l \<bullet> w = 0)
[PROOF STEP]
by (metis empty_iff inner_commute insert_iff)+
[PROOF STATE]
proof (state)
this:
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep (proj2_line_through p q)) ?w
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep l) ?w

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
from proj2_rep_independent and \<open>p \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
?p \<noteq> ?q \<Longrightarrow> independent {proj2_rep ?p, proj2_rep ?q}
p \<noteq> q
[PROOF STEP]
have "independent ?A"
[PROOF STATE]
proof (prove)
using this:
?p \<noteq> ?q \<Longrightarrow> independent {proj2_rep ?p, proj2_rep ?q}
p \<noteq> q

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

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
from proj2_line_rep_non_zero
[PROOF STATE]
proof (chain)
picking this:
proj2_line_rep ?l \<noteq> 0
[PROOF STEP]
have "?m' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
proj2_line_rep ?l \<noteq> 0

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

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
with orthogonal_independent \<open>independent ?A\<close> ortho
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>independent ?S; ?v \<noteq> 0; \<And>w. w \<in> ?S \<Longrightarrow> orthogonal ?v w\<rbrakk> \<Longrightarrow> independent (insert ?v ?S)
independent {proj2_rep p, proj2_rep q}
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep (proj2_line_through p q)) ?w
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep l) ?w
proj2_line_rep (proj2_line_through p q) \<noteq> 0
[PROOF STEP]
have "independent ?B"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>independent ?S; ?v \<noteq> 0; \<And>w. w \<in> ?S \<Longrightarrow> orthogonal ?v w\<rbrakk> \<Longrightarrow> independent (insert ?v ?S)
independent {proj2_rep p, proj2_rep q}
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep (proj2_line_through p q)) ?w
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep l) ?w
proj2_line_rep (proj2_line_through p q) \<noteq> 0

goal (1 subgoal):
 1. independent {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
independent {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
from proj2_rep_inj and \<open>p \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
inj proj2_rep
p \<noteq> q
[PROOF STEP]
have "?p' \<noteq> ?q'"
[PROOF STATE]
proof (prove)
using this:
inj proj2_rep
p \<noteq> q

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

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

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
hence "card ?A = 2"
[PROOF STATE]
proof (prove)
using this:
proj2_rep p \<noteq> proj2_rep q

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

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {proj2_rep p, proj2_rep q} = 2

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
have "?m' \<notin> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_line_rep (proj2_line_through p q) \<notin> {proj2_rep p, proj2_rep q}
[PROOF STEP]
using ortho(1) orthogonal_self proj2_line_rep_non_zero
[PROOF STATE]
proof (prove)
using this:
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep (proj2_line_through p q)) ?w
orthogonal ?x ?x = (?x = (0::?'a))
proj2_line_rep ?l \<noteq> 0

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

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {proj2_rep p, proj2_rep q} = 2
proj2_line_rep (proj2_line_through p q) \<notin> {proj2_rep p, proj2_rep q}
[PROOF STEP]
have "card ?B = 3"
[PROOF STATE]
proof (prove)
using this:
card {proj2_rep p, proj2_rep q} = 2
proj2_line_rep (proj2_line_through p q) \<notin> {proj2_rep p, proj2_rep q}

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

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
with independent_is_basis [of ?B] and \<open>independent ?B\<close>
[PROOF STATE]
proof (chain)
picking this:
(independent {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q} \<and> card {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q} = CARD(3)) = is_basis {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}
independent {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}
card {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q} = 3
[PROOF STEP]
have "is_basis ?B"
[PROOF STATE]
proof (prove)
using this:
(independent {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q} \<and> card {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q} = CARD(3)) = is_basis {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}
independent {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}
card {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q} = 3

goal (1 subgoal):
 1. is_basis {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_basis {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
with basis_expand
[PROOF STATE]
proof (chain)
picking this:
is_basis ?B \<Longrightarrow> \<exists>c. ?v = (\<Sum>w\<in>?B. c w *\<^sub>R w)
is_basis {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}
[PROOF STEP]
obtain c where "?l' = (\<Sum> v\<in>?B. c v *\<^sub>R v)"
[PROOF STATE]
proof (prove)
using this:
is_basis ?B \<Longrightarrow> \<exists>c. ?v = (\<Sum>w\<in>?B. c w *\<^sub>R w)
is_basis {proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}

goal (1 subgoal):
 1. (\<And>c. proj2_line_rep l = (\<Sum>v\<in>{proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}. c v *\<^sub>R v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_line_rep l = (\<Sum>v\<in>{proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}. c v *\<^sub>R v)

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
let ?l'' = "?l' - c ?m' *\<^sub>R ?m'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
from \<open>?l' = (\<Sum> v\<in>?B. c v *\<^sub>R v)\<close> and \<open>?m' \<notin> ?A\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_line_rep l = (\<Sum>v\<in>{proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}. c v *\<^sub>R v)
proj2_line_rep (proj2_line_through p q) \<notin> {proj2_rep p, proj2_rep q}
[PROOF STEP]
have "?l'' = (\<Sum> v\<in>?A. c v *\<^sub>R v)"
[PROOF STATE]
proof (prove)
using this:
proj2_line_rep l = (\<Sum>v\<in>{proj2_line_rep (proj2_line_through p q), proj2_rep p, proj2_rep q}. c v *\<^sub>R v)
proj2_line_rep (proj2_line_through p q) \<notin> {proj2_rep p, proj2_rep q}

goal (1 subgoal):
 1. proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = (\<Sum>v\<in>{proj2_rep p, proj2_rep q}. c v *\<^sub>R v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = (\<Sum>v\<in>{proj2_rep p, proj2_rep q}. c v *\<^sub>R v)

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
with orthogonal_sum [of ?A] ortho
[PROOF STATE]
proof (chain)
picking this:
(\<And>w. w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal ?v w) \<Longrightarrow> orthogonal ?v (\<Sum>w\<in>{proj2_rep p, proj2_rep q}. ?c w *s w)
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep (proj2_line_through p q)) ?w
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep l) ?w
proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = (\<Sum>v\<in>{proj2_rep p, proj2_rep q}. c v *\<^sub>R v)
[PROOF STEP]
have "orthogonal ?l' ?l''" and "orthogonal ?m' ?l''"
[PROOF STATE]
proof (prove)
using this:
(\<And>w. w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal ?v w) \<Longrightarrow> orthogonal ?v (\<Sum>w\<in>{proj2_rep p, proj2_rep q}. ?c w *s w)
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep (proj2_line_through p q)) ?w
?w \<in> {proj2_rep p, proj2_rep q} \<Longrightarrow> orthogonal (proj2_line_rep l) ?w
proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = (\<Sum>v\<in>{proj2_rep p, proj2_rep q}. c v *\<^sub>R v)

goal (1 subgoal):
 1. orthogonal (proj2_line_rep l) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) &&& orthogonal (proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))
[PROOF STEP]
by (simp_all add: scalar_equiv)
[PROOF STATE]
proof (state)
this:
orthogonal (proj2_line_rep l) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))
orthogonal (proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
from \<open>orthogonal ?m' ?l''\<close>
[PROOF STATE]
proof (chain)
picking this:
orthogonal (proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))
[PROOF STEP]
have "orthogonal (c ?m' *\<^sub>R ?m') ?l''"
[PROOF STATE]
proof (prove)
using this:
orthogonal (proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))

goal (1 subgoal):
 1. orthogonal (c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))
[PROOF STEP]
by (simp add: orthogonal_clauses)
[PROOF STATE]
proof (state)
this:
orthogonal (c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
with \<open>orthogonal ?l' ?l''\<close>
[PROOF STATE]
proof (chain)
picking this:
orthogonal (proj2_line_rep l) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))
orthogonal (c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))
[PROOF STEP]
have "orthogonal ?l'' ?l''"
[PROOF STATE]
proof (prove)
using this:
orthogonal (proj2_line_rep l) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))
orthogonal (c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))

goal (1 subgoal):
 1. orthogonal (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))
[PROOF STEP]
by (simp add: orthogonal_clauses)
[PROOF STATE]
proof (state)
this:
orthogonal (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
with orthogonal_self_eq_0 [of ?l'']
[PROOF STATE]
proof (chain)
picking this:
orthogonal (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) \<Longrightarrow> proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = 0
orthogonal (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))
[PROOF STEP]
have "?l'' = 0"
[PROOF STATE]
proof (prove)
using this:
orthogonal (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) \<Longrightarrow> proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = 0
orthogonal (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q)) (proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q))

goal (1 subgoal):
 1. proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = 0

goal (1 subgoal):
 1. l = proj2_line_through p q
[PROOF STEP]
with proj2_line_rep_dependent [of 1 l "- c ?m'" ?m]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>1 *\<^sub>R proj2_line_rep l + - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = 0; 1 \<noteq> 0 \<or> - c (proj2_line_rep (proj2_line_through p q)) \<noteq> 0\<rbrakk> \<Longrightarrow> l = proj2_line_through p q
proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = 0
[PROOF STEP]
show "l = ?m"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 *\<^sub>R proj2_line_rep l + - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = 0; 1 \<noteq> 0 \<or> - c (proj2_line_rep (proj2_line_through p q)) \<noteq> 0\<rbrakk> \<Longrightarrow> l = proj2_line_through p q
proj2_line_rep l - c (proj2_line_rep (proj2_line_through p q)) *\<^sub>R proj2_line_rep (proj2_line_through p q) = 0

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (2 subgoals):
 1. ?P \<Longrightarrow> p = q \<or> l = m
 2. \<not> ?P \<Longrightarrow> p = q \<or> l = m
[PROOF STEP]
thus "p = q \<or> l = m"
[PROOF STATE]
proof (prove)
using this:
p = q

goal (1 subgoal):
 1. p = q \<or> l = m
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
p = q \<or> l = m

goal (1 subgoal):
 1. p \<noteq> q \<Longrightarrow> p = q \<or> l = m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> q \<Longrightarrow> p = q \<or> l = m
[PROOF STEP]
assume "p \<noteq> q"
[PROOF STATE]
proof (state)
this:
p \<noteq> q

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

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

goal (1 subgoal):
 1. p \<noteq> q \<Longrightarrow> p = q \<or> l = m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l = proj2_line_through p q

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

goal (1 subgoal):
 1. m = proj2_line_through p q
[PROOF STEP]
by (rule proj2_line_through_unique)
[PROOF STATE]
proof (state)
this:
m = proj2_line_through p q

goal (1 subgoal):
 1. p \<noteq> q \<Longrightarrow> p = q \<or> l = m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l = proj2_line_through p q
m = proj2_line_through p q
[PROOF STEP]
show "p = q \<or> l = m"
[PROOF STATE]
proof (prove)
using this:
l = proj2_line_through p q
m = proj2_line_through p q

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_lines_define_point: "\<exists> p. proj2_incident p l \<and> proj2_incident p m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. proj2_incident p l \<and> proj2_incident p m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p. proj2_incident p l \<and> proj2_incident p m
[PROOF STEP]
let ?l' = "L2P l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p. proj2_incident p l \<and> proj2_incident p m
[PROOF STEP]
let ?m' = "L2P m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p. proj2_incident p l \<and> proj2_incident p m
[PROOF STEP]
from proj2_points_define_line [of ?l' ?m']
[PROOF STATE]
proof (chain)
picking this:
\<exists>la. proj2_incident (L2P l) la \<and> proj2_incident (L2P m) la
[PROOF STEP]
obtain p' where "proj2_incident ?l' p' \<and> proj2_incident ?m' p'"
[PROOF STATE]
proof (prove)
using this:
\<exists>la. proj2_incident (L2P l) la \<and> proj2_incident (L2P m) la

goal (1 subgoal):
 1. (\<And>p'. proj2_incident (L2P l) p' \<and> proj2_incident (L2P m) p' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_incident (L2P l) p' \<and> proj2_incident (L2P m) p'

goal (1 subgoal):
 1. \<exists>p. proj2_incident p l \<and> proj2_incident p m
[PROOF STEP]
hence "proj2_incident (L2P p') l \<and> proj2_incident (L2P p') m"
[PROOF STATE]
proof (prove)
using this:
proj2_incident (L2P l) p' \<and> proj2_incident (L2P m) p'

goal (1 subgoal):
 1. proj2_incident (L2P p') l \<and> proj2_incident (L2P p') m
[PROOF STEP]
unfolding proj2_incident_def and proj2_line_rep_def
[PROOF STATE]
proof (prove)
using this:
proj2_rep (L2P l) \<bullet> proj2_rep (L2P p') = 0 \<and> proj2_rep (L2P m) \<bullet> proj2_rep (L2P p') = 0

goal (1 subgoal):
 1. proj2_rep (L2P p') \<bullet> proj2_rep (L2P l) = 0 \<and> proj2_rep (L2P p') \<bullet> proj2_rep (L2P m) = 0
[PROOF STEP]
by (simp add: inner_commute)
[PROOF STATE]
proof (state)
this:
proj2_incident (L2P p') l \<and> proj2_incident (L2P p') m

goal (1 subgoal):
 1. \<exists>p. proj2_incident p l \<and> proj2_incident p m
[PROOF STEP]
thus "\<exists> p. proj2_incident p l \<and> proj2_incident p m"
[PROOF STATE]
proof (prove)
using this:
proj2_incident (L2P p') l \<and> proj2_incident (L2P p') m

goal (1 subgoal):
 1. \<exists>p. proj2_incident p l \<and> proj2_incident p m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>p. proj2_incident p l \<and> proj2_incident p m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_incident_switch:
  assumes "proj2_incident p l"
  shows "proj2_incident (L2P l) (P2L p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident (L2P l) (P2L p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proj2_incident p l

goal (1 subgoal):
 1. proj2_incident (L2P l) (P2L p)
[PROOF STEP]
unfolding proj2_incident_def and proj2_line_rep_def
[PROOF STATE]
proof (prove)
using this:
proj2_rep p \<bullet> proj2_rep (L2P l) = 0

goal (1 subgoal):
 1. proj2_rep (L2P l) \<bullet> proj2_rep (L2P (P2L p)) = 0
[PROOF STEP]
by (simp add: inner_commute)


[STATEMENT]
lemma proj2_intersection_incident:
  shows "proj2_incident (proj2_intersection l m) l"
  and "proj2_incident (proj2_intersection l m) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident (proj2_intersection l m) l &&& proj2_incident (proj2_intersection l m) m
[PROOF STEP]
using proj2_line_through_incident(1) [of "L2P l" "L2P m"]
    and proj2_line_through_incident(2) [of "L2P m" "L2P l"]
    and proj2_incident_switch [of "L2P l"]
    and proj2_incident_switch [of "L2P m"]
[PROOF STATE]
proof (prove)
using this:
proj2_incident (L2P l) (proj2_line_through (L2P l) (L2P m))
proj2_incident (L2P m) (proj2_line_through (L2P l) (L2P m))
proj2_incident (L2P l) ?l \<Longrightarrow> proj2_incident (L2P ?l) (P2L (L2P l))
proj2_incident (L2P m) ?l \<Longrightarrow> proj2_incident (L2P ?l) (P2L (L2P m))

goal (1 subgoal):
 1. proj2_incident (proj2_intersection l m) l &&& proj2_incident (proj2_intersection l m) m
[PROOF STEP]
unfolding proj2_intersection_def
[PROOF STATE]
proof (prove)
using this:
proj2_incident (L2P l) (proj2_line_through (L2P l) (L2P m))
proj2_incident (L2P m) (proj2_line_through (L2P l) (L2P m))
proj2_incident (L2P l) ?l \<Longrightarrow> proj2_incident (L2P ?l) (P2L (L2P l))
proj2_incident (L2P m) ?l \<Longrightarrow> proj2_incident (L2P ?l) (P2L (L2P m))

goal (1 subgoal):
 1. proj2_incident (L2P (proj2_line_through (L2P l) (L2P m))) l &&& proj2_incident (L2P (proj2_line_through (L2P l) (L2P m))) m
[PROOF STEP]
by simp_all


[STATEMENT]
lemma proj2_intersection_unique:
  assumes "l \<noteq> m" and "proj2_incident p l" and "proj2_incident p m"
  shows "p = proj2_intersection l m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = proj2_intersection l m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = proj2_intersection l m
[PROOF STEP]
from \<open>l \<noteq> m\<close>
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> m
[PROOF STEP]
have "L2P l \<noteq> L2P m"
[PROOF STATE]
proof (prove)
using this:
l \<noteq> m

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

goal (1 subgoal):
 1. p = proj2_intersection l m
[PROOF STEP]
from \<open>proj2_incident p l\<close> and \<open>proj2_incident p m\<close>
    and proj2_incident_switch
[PROOF STATE]
proof (chain)
picking this:
proj2_incident p l
proj2_incident p m
proj2_incident ?p ?l \<Longrightarrow> proj2_incident (L2P ?l) (P2L ?p)
[PROOF STEP]
have "proj2_incident (L2P l) (P2L p)" and "proj2_incident (L2P m) (P2L p)"
[PROOF STATE]
proof (prove)
using this:
proj2_incident p l
proj2_incident p m
proj2_incident ?p ?l \<Longrightarrow> proj2_incident (L2P ?l) (P2L ?p)

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

goal (1 subgoal):
 1. p = proj2_intersection l m
[PROOF STEP]
with \<open>L2P l \<noteq> L2P m\<close> and proj2_line_through_unique
[PROOF STATE]
proof (chain)
picking this:
L2P l \<noteq> L2P m
\<lbrakk>?p \<noteq> ?q; proj2_incident ?p ?l; proj2_incident ?q ?l\<rbrakk> \<Longrightarrow> ?l = proj2_line_through ?p ?q
proj2_incident (L2P l) (P2L p)
proj2_incident (L2P m) (P2L p)
[PROOF STEP]
have "P2L p = proj2_line_through (L2P l) (L2P m)"
[PROOF STATE]
proof (prove)
using this:
L2P l \<noteq> L2P m
\<lbrakk>?p \<noteq> ?q; proj2_incident ?p ?l; proj2_incident ?q ?l\<rbrakk> \<Longrightarrow> ?l = proj2_line_through ?p ?q
proj2_incident (L2P l) (P2L p)
proj2_incident (L2P m) (P2L p)

goal (1 subgoal):
 1. P2L p = proj2_line_through (L2P l) (L2P m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P2L p = proj2_line_through (L2P l) (L2P m)

goal (1 subgoal):
 1. p = proj2_intersection l m
[PROOF STEP]
thus "p = proj2_intersection l m"
[PROOF STATE]
proof (prove)
using this:
P2L p = proj2_line_through (L2P l) (L2P m)

goal (1 subgoal):
 1. p = proj2_intersection l m
[PROOF STEP]
unfolding proj2_intersection_def
[PROOF STATE]
proof (prove)
using this:
P2L p = proj2_line_through (L2P l) (L2P m)

goal (1 subgoal):
 1. p = L2P (proj2_line_through (L2P l) (L2P m))
[PROOF STEP]
by (simp add: P2L_to_L2P)
[PROOF STATE]
proof (state)
this:
p = proj2_intersection l m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_not_self_incident:
  "\<not> (proj2_incident p (P2L p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> proj2_incident p (P2L p)
[PROOF STEP]
unfolding proj2_incident_def and proj2_line_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep p \<bullet> proj2_rep (L2P (P2L p)) \<noteq> 0
[PROOF STEP]
using proj2_rep_non_zero and inner_eq_zero_iff [of "proj2_rep p"]
[PROOF STATE]
proof (prove)
using this:
proj2_rep ?x \<noteq> 0
(proj2_rep p \<bullet> proj2_rep p = 0) = (proj2_rep p = 0)

goal (1 subgoal):
 1. proj2_rep p \<bullet> proj2_rep (L2P (P2L p)) \<noteq> 0
[PROOF STEP]
by simp


[STATEMENT]
lemma proj2_another_point_on_line:
  "\<exists> q. q \<noteq> p \<and> proj2_incident q l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q. q \<noteq> p \<and> proj2_incident q l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>q. q \<noteq> p \<and> proj2_incident q l
[PROOF STEP]
let ?m = "P2L p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>q. q \<noteq> p \<and> proj2_incident q l
[PROOF STEP]
let ?q = "proj2_intersection l ?m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>q. q \<noteq> p \<and> proj2_incident q l
[PROOF STEP]
from proj2_intersection_incident
[PROOF STATE]
proof (chain)
picking this:
proj2_incident (proj2_intersection ?l ?m) ?l
proj2_incident (proj2_intersection ?l ?m) ?m
[PROOF STEP]
have "proj2_incident ?q l" and "proj2_incident ?q ?m"
[PROOF STATE]
proof (prove)
using this:
proj2_incident (proj2_intersection ?l ?m) ?l
proj2_incident (proj2_intersection ?l ?m) ?m

goal (1 subgoal):
 1. proj2_incident (proj2_intersection l (P2L p)) l &&& proj2_incident (proj2_intersection l (P2L p)) (P2L p)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
proj2_incident (proj2_intersection l (P2L p)) l
proj2_incident (proj2_intersection l (P2L p)) (P2L p)

goal (1 subgoal):
 1. \<exists>q. q \<noteq> p \<and> proj2_incident q l
[PROOF STEP]
from \<open>proj2_incident ?q ?m\<close> and proj2_not_self_incident
[PROOF STATE]
proof (chain)
picking this:
proj2_incident (proj2_intersection l (P2L p)) (P2L p)
\<not> proj2_incident ?p (P2L ?p)
[PROOF STEP]
have "?q \<noteq> p"
[PROOF STATE]
proof (prove)
using this:
proj2_incident (proj2_intersection l (P2L p)) (P2L p)
\<not> proj2_incident ?p (P2L ?p)

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

goal (1 subgoal):
 1. \<exists>q. q \<noteq> p \<and> proj2_incident q l
[PROOF STEP]
with \<open>proj2_incident ?q l\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_incident (proj2_intersection l (P2L p)) l
proj2_intersection l (P2L p) \<noteq> p
[PROOF STEP]
show "\<exists> q. q \<noteq> p \<and> proj2_incident q l"
[PROOF STATE]
proof (prove)
using this:
proj2_incident (proj2_intersection l (P2L p)) l
proj2_intersection l (P2L p) \<noteq> p

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_another_line_through_point:
  "\<exists> m. m \<noteq> l \<and> proj2_incident p m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. m \<noteq> l \<and> proj2_incident p m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. m \<noteq> l \<and> proj2_incident p m
[PROOF STEP]
from proj2_another_point_on_line
[PROOF STATE]
proof (chain)
picking this:
\<exists>q. q \<noteq> ?p \<and> proj2_incident q ?l
[PROOF STEP]
obtain q where "q \<noteq> L2P l \<and> proj2_incident q (P2L p)"
[PROOF STATE]
proof (prove)
using this:
\<exists>q. q \<noteq> ?p \<and> proj2_incident q ?l

goal (1 subgoal):
 1. (\<And>q. q \<noteq> L2P l \<and> proj2_incident q (P2L p) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<noteq> L2P l \<and> proj2_incident q (P2L p)

goal (1 subgoal):
 1. \<exists>m. m \<noteq> l \<and> proj2_incident p m
[PROOF STEP]
with proj2_incident_switch [of q "P2L p"]
[PROOF STATE]
proof (chain)
picking this:
proj2_incident q (P2L p) \<Longrightarrow> proj2_incident (L2P (P2L p)) (P2L q)
q \<noteq> L2P l \<and> proj2_incident q (P2L p)
[PROOF STEP]
have "P2L q \<noteq> l \<and> proj2_incident p (P2L q)"
[PROOF STATE]
proof (prove)
using this:
proj2_incident q (P2L p) \<Longrightarrow> proj2_incident (L2P (P2L p)) (P2L q)
q \<noteq> L2P l \<and> proj2_incident q (P2L p)

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

goal (1 subgoal):
 1. \<exists>m. m \<noteq> l \<and> proj2_incident p m
[PROOF STEP]
thus "\<exists> m. m \<noteq> l \<and> proj2_incident p m"
[PROOF STATE]
proof (prove)
using this:
P2L q \<noteq> l \<and> proj2_incident p (P2L q)

goal (1 subgoal):
 1. \<exists>m. m \<noteq> l \<and> proj2_incident p m
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>m. m \<noteq> l \<and> proj2_incident p m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_incident_abs:
  assumes "v \<noteq> 0" and "w \<noteq> 0"
  shows "proj2_incident (proj2_abs v) (proj2_line_abs w) \<longleftrightarrow> v \<bullet> w = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident (proj2_abs v) (proj2_line_abs w) = (v \<bullet> w = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_incident (proj2_abs v) (proj2_line_abs w) = (v \<bullet> w = 0)
[PROOF STEP]
from \<open>v \<noteq> 0\<close> and proj2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
[PROOF STEP]
obtain j where "j \<noteq> 0" and "proj2_rep (proj2_abs v) = j *\<^sub>R v"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v

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

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

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

goal (1 subgoal):
 1. proj2_incident (proj2_abs v) (proj2_line_abs w) = (v \<bullet> w = 0)
[PROOF STEP]
with \<open>j \<noteq> 0\<close> and \<open>proj2_rep (proj2_abs v) = j *\<^sub>R v\<close>
[PROOF STATE]
proof (chain)
picking this:
j \<noteq> 0
proj2_rep (proj2_abs v) = j *\<^sub>R v
k \<noteq> 0
proj2_line_rep (proj2_line_abs w) = k *\<^sub>R w
[PROOF STEP]
show "proj2_incident (proj2_abs v) (proj2_line_abs w) \<longleftrightarrow> v \<bullet> w = 0"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
proj2_rep (proj2_abs v) = j *\<^sub>R v
k \<noteq> 0
proj2_line_rep (proj2_line_abs w) = k *\<^sub>R w

goal (1 subgoal):
 1. proj2_incident (proj2_abs v) (proj2_line_abs w) = (v \<bullet> w = 0)
[PROOF STEP]
unfolding proj2_incident_def
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
proj2_rep (proj2_abs v) = j *\<^sub>R v
k \<noteq> 0
proj2_line_rep (proj2_line_abs w) = k *\<^sub>R w

goal (1 subgoal):
 1. (proj2_rep (proj2_abs v) \<bullet> proj2_line_rep (proj2_line_abs w) = 0) = (v \<bullet> w = 0)
[PROOF STEP]
by (simp add: dot_scaleR_mult)
[PROOF STATE]
proof (state)
this:
proj2_incident (proj2_abs v) (proj2_line_abs w) = (v \<bullet> w = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_incident_left_abs:
  assumes "v \<noteq> 0"
  shows "proj2_incident (proj2_abs v) l \<longleftrightarrow> v \<bullet> (proj2_line_rep l) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident (proj2_abs v) l = (v \<bullet> proj2_line_rep l = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_incident (proj2_abs v) l = (v \<bullet> proj2_line_rep l = 0)
[PROOF STEP]
have "proj2_line_rep l \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_line_rep l \<noteq> 0
[PROOF STEP]
by (rule proj2_line_rep_non_zero)
[PROOF STATE]
proof (state)
this:
proj2_line_rep l \<noteq> 0

goal (1 subgoal):
 1. proj2_incident (proj2_abs v) l = (v \<bullet> proj2_line_rep l = 0)
[PROOF STEP]
with \<open>v \<noteq> 0\<close> and proj2_incident_abs [of v "proj2_line_rep l"]
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> 0
\<lbrakk>v \<noteq> 0; proj2_line_rep l \<noteq> 0\<rbrakk> \<Longrightarrow> proj2_incident (proj2_abs v) (proj2_line_abs (proj2_line_rep l)) = (v \<bullet> proj2_line_rep l = 0)
proj2_line_rep l \<noteq> 0
[PROOF STEP]
show "proj2_incident (proj2_abs v) l \<longleftrightarrow> v \<bullet> (proj2_line_rep l) = 0"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0
\<lbrakk>v \<noteq> 0; proj2_line_rep l \<noteq> 0\<rbrakk> \<Longrightarrow> proj2_incident (proj2_abs v) (proj2_line_abs (proj2_line_rep l)) = (v \<bullet> proj2_line_rep l = 0)
proj2_line_rep l \<noteq> 0

goal (1 subgoal):
 1. proj2_incident (proj2_abs v) l = (v \<bullet> proj2_line_rep l = 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_incident (proj2_abs v) l = (v \<bullet> proj2_line_rep l = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_incident_right_abs:
  assumes "v \<noteq> 0"
  shows "proj2_incident p (proj2_line_abs v) \<longleftrightarrow> (proj2_rep p) \<bullet> v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident p (proj2_line_abs v) = (proj2_rep p \<bullet> v = 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_incident p (proj2_line_abs v) = (proj2_rep p \<bullet> v = 0)
[PROOF STEP]
have "proj2_rep p \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep p \<noteq> 0
[PROOF STEP]
by (rule proj2_rep_non_zero)
[PROOF STATE]
proof (state)
this:
proj2_rep p \<noteq> 0

goal (1 subgoal):
 1. proj2_incident p (proj2_line_abs v) = (proj2_rep p \<bullet> v = 0)
[PROOF STEP]
with \<open>v \<noteq> 0\<close> and proj2_incident_abs [of "proj2_rep p" v]
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> 0
\<lbrakk>proj2_rep p \<noteq> 0; v \<noteq> 0\<rbrakk> \<Longrightarrow> proj2_incident (proj2_abs (proj2_rep p)) (proj2_line_abs v) = (proj2_rep p \<bullet> v = 0)
proj2_rep p \<noteq> 0
[PROOF STEP]
show "proj2_incident p (proj2_line_abs v) \<longleftrightarrow> (proj2_rep p) \<bullet> v = 0"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0
\<lbrakk>proj2_rep p \<noteq> 0; v \<noteq> 0\<rbrakk> \<Longrightarrow> proj2_incident (proj2_abs (proj2_rep p)) (proj2_line_abs v) = (proj2_rep p \<bullet> v = 0)
proj2_rep p \<noteq> 0

goal (1 subgoal):
 1. proj2_incident p (proj2_line_abs v) = (proj2_rep p \<bullet> v = 0)
[PROOF STEP]
by (simp add: proj2_abs_rep)
[PROOF STATE]
proof (state)
this:
proj2_incident p (proj2_line_abs v) = (proj2_rep p \<bullet> v = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_subset_Col:
  assumes "T \<subseteq> S" and "proj2_set_Col S"
  shows "proj2_set_Col T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_set_Col T
[PROOF STEP]
using \<open>T \<subseteq> S\<close> and \<open>proj2_set_Col S\<close>
[PROOF STATE]
proof (prove)
using this:
T \<subseteq> S
proj2_set_Col S

goal (1 subgoal):
 1. proj2_set_Col T
[PROOF STEP]
by (unfold proj2_set_Col_def) auto


[STATEMENT]
lemma proj2_Col_iff_not_invertible:
  "proj2_Col p q r
  \<longleftrightarrow> \<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r] :: real^3^3)"
  (is "_ \<longleftrightarrow> \<not> invertible (vector [?u, ?v, ?w])")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col p q r = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_Col p q r = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))
[PROOF STEP]
let ?M = "vector [?u,?v,?w] :: real^3^3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_Col p q r = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))
[PROOF STEP]
have "proj2_Col p q r \<longleftrightarrow> (\<exists> x. x \<noteq> 0 \<and> x v* ?M = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col p q r = (\<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col p q r \<Longrightarrow> \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
 2. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
assume "proj2_Col p q r"
[PROOF STATE]
proof (state)
this:
proj2_Col p q r

goal (2 subgoals):
 1. proj2_Col p q r \<Longrightarrow> \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
 2. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proj2_Col p q r
[PROOF STEP]
obtain i and j and k
      where "i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0" and "i *\<^sub>R ?u + j *\<^sub>R ?v + k *\<^sub>R ?w = 0"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q r

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

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

goal (2 subgoals):
 1. proj2_Col p q r \<Longrightarrow> \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
 2. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
let ?x = "vector [i,j,k] :: real^3"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col p q r \<Longrightarrow> \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
 2. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
from \<open>i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0
[PROOF STEP]
have "?x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0

goal (1 subgoal):
 1. vector [i, j, k] \<noteq> 0
[PROOF STEP]
unfolding vector_def
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0

goal (1 subgoal):
 1. vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [i, j, k] (\<lambda>n x. 0) 1) \<noteq> 0
[PROOF STEP]
by (simp add: vec_eq_iff forall_3)
[PROOF STATE]
proof (state)
this:
vector [i, j, k] \<noteq> 0

goal (2 subgoals):
 1. proj2_Col p q r \<Longrightarrow> \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
 2. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vector [i, j, k] \<noteq> 0

goal (2 subgoals):
 1. proj2_Col p q r \<Longrightarrow> \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
 2. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
vector [i, j, k] \<noteq> 0

goal (2 subgoals):
 1. proj2_Col p q r \<Longrightarrow> \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
 2. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
from \<open>i *\<^sub>R ?u + j *\<^sub>R ?v + k *\<^sub>R ?w = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q + k *\<^sub>R proj2_rep r = 0
[PROOF STEP]
have "?x v* ?M = 0"
[PROOF STATE]
proof (prove)
using this:
i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q + k *\<^sub>R proj2_rep r = 0

goal (1 subgoal):
 1. vector [i, j, k] v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
[PROOF STEP]
unfolding vector_def and vector_matrix_mult_def
[PROOF STATE]
proof (prove)
using this:
i *\<^sub>R proj2_rep p + j *\<^sub>R proj2_rep q + k *\<^sub>R proj2_rep r = 0

goal (1 subgoal):
 1. (\<chi>ja. \<Sum>ia\<in>UNIV. 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) $ ia $ ja * vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [i, j, k] (\<lambda>n x. 0) 1) $ ia) = 0
[PROOF STEP]
by (simp add: sum_3 vec_eq_iff algebra_simps)
[PROOF STATE]
proof (state)
this:
vector [i, j, k] v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0

goal (2 subgoals):
 1. proj2_Col p q r \<Longrightarrow> \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
 2. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
vector [i, j, k] v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0

goal (2 subgoals):
 1. proj2_Col p q r \<Longrightarrow> \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
 2. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vector [i, j, k] \<noteq> 0
vector [i, j, k] v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
[PROOF STEP]
show "\<exists> x. x \<noteq> 0 \<and> x v* ?M = 0"
[PROOF STATE]
proof (prove)
using this:
vector [i, j, k] \<noteq> 0
vector [i, j, k] v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0

goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0

goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
assume "\<exists> x. x \<noteq> 0 \<and> x v* ?M = 0"
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0

goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
[PROOF STEP]
obtain x where "x \<noteq> 0" and "x v* ?M = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<noteq> 0; x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> 0
x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0

goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
let ?i = "x$1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
let ?j = "x$2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
let ?k = "x$3"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
from \<open>x \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
[PROOF STEP]
have "?i \<noteq> 0 \<or> ?j \<noteq> 0 \<or> ?k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. x $ 1 \<noteq> 0 \<or> x $ 2 \<noteq> 0 \<or> x $ 3 \<noteq> 0
[PROOF STEP]
by (simp add: vec_eq_iff forall_3)
[PROOF STATE]
proof (state)
this:
x $ 1 \<noteq> 0 \<or> x $ 2 \<noteq> 0 \<or> x $ 3 \<noteq> 0

goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x $ 1 \<noteq> 0 \<or> x $ 2 \<noteq> 0 \<or> x $ 3 \<noteq> 0

goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x $ 1 \<noteq> 0 \<or> x $ 2 \<noteq> 0 \<or> x $ 3 \<noteq> 0

goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
from \<open>x v* ?M = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0
[PROOF STEP]
have "?i *\<^sub>R ?u + ?j *\<^sub>R ?v + ?k *\<^sub>R ?w = 0"
[PROOF STATE]
proof (prove)
using this:
x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0

goal (1 subgoal):
 1. x $ 1 *\<^sub>R proj2_rep p + x $ 2 *\<^sub>R proj2_rep q + x $ 3 *\<^sub>R proj2_rep r = 0
[PROOF STEP]
unfolding vector_matrix_mult_def and sum_3 and vector_def
[PROOF STATE]
proof (prove)
using this:
(\<chi>j. 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 $ j * x $ 1 + 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 $ j * x $ 2 + 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 $ j * x $ 3) = 0

goal (1 subgoal):
 1. x $ 1 *\<^sub>R proj2_rep p + x $ 2 *\<^sub>R proj2_rep q + x $ 3 *\<^sub>R proj2_rep r = 0
[PROOF STEP]
by (simp add: vec_eq_iff algebra_simps)
[PROOF STATE]
proof (state)
this:
x $ 1 *\<^sub>R proj2_rep p + x $ 2 *\<^sub>R proj2_rep q + x $ 3 *\<^sub>R proj2_rep r = 0

goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x $ 1 *\<^sub>R proj2_rep p + x $ 2 *\<^sub>R proj2_rep q + x $ 3 *\<^sub>R proj2_rep r = 0

goal (1 subgoal):
 1. \<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<Longrightarrow> proj2_Col p q r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x $ 1 \<noteq> 0 \<or> x $ 2 \<noteq> 0 \<or> x $ 3 \<noteq> 0
x $ 1 *\<^sub>R proj2_rep p + x $ 2 *\<^sub>R proj2_rep q + x $ 3 *\<^sub>R proj2_rep r = 0
[PROOF STEP]
show "proj2_Col p q r"
[PROOF STATE]
proof (prove)
using this:
x $ 1 \<noteq> 0 \<or> x $ 2 \<noteq> 0 \<or> x $ 3 \<noteq> 0
x $ 1 *\<^sub>R proj2_rep p + x $ 2 *\<^sub>R proj2_rep q + x $ 3 *\<^sub>R proj2_rep r = 0

goal (1 subgoal):
 1. proj2_Col p q r
[PROOF STEP]
unfolding proj2_Col_def
[PROOF STATE]
proof (prove)
using this:
x $ 1 \<noteq> 0 \<or> x $ 2 \<noteq> 0 \<or> x $ 3 \<noteq> 0
x $ 1 *\<^sub>R proj2_rep p + x $ 2 *\<^sub>R proj2_rep q + x $ 3 *\<^sub>R proj2_rep r = 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proj2_Col p q r = (\<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0)

goal (1 subgoal):
 1. proj2_Col p q r = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proj2_Col p q r = (\<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0)

goal (1 subgoal):
 1. proj2_Col p q r = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))
[PROOF STEP]
from matrix_right_invertible_ker [of ?M]
[PROOF STATE]
proof (chain)
picking this:
(\<exists>M'. vector [proj2_rep p, proj2_rep q, proj2_rep r] ** M' = mat 1) = (\<forall>x. x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<longrightarrow> x = 0)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> \<not> (\<exists> M'. ?M ** M' = mat 1)"
[PROOF STATE]
proof (prove)
using this:
(\<exists>M'. vector [proj2_rep p, proj2_rep q, proj2_rep r] ** M' = mat 1) = (\<forall>x. x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0 \<longrightarrow> x = 0)

goal (1 subgoal):
 1. (\<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0) = (\<nexists>M'. vector [proj2_rep p, proj2_rep q, proj2_rep r] ** M' = mat 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0) = (\<nexists>M'. vector [proj2_rep p, proj2_rep q, proj2_rep r] ** M' = mat 1)

goal (1 subgoal):
 1. proj2_Col p q r = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>x. x \<noteq> 0 \<and> x v* vector [proj2_rep p, proj2_rep q, proj2_rep r] = 0) = (\<nexists>M'. vector [proj2_rep p, proj2_rep q, proj2_rep r] ** M' = mat 1)

goal (1 subgoal):
 1. proj2_Col p q r = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))
[PROOF STEP]
from matrix_left_right_inverse
[PROOF STATE]
proof (chain)
picking this:
(?A ** ?A' = mat (1::?'a)) = (?A' ** ?A = mat (1::?'a))
[PROOF STEP]
have "\<dots> \<longleftrightarrow> \<not> invertible ?M"
[PROOF STATE]
proof (prove)
using this:
(?A ** ?A' = mat (1::?'a)) = (?A' ** ?A = mat (1::?'a))

goal (1 subgoal):
 1. (\<nexists>M'. vector [proj2_rep p, proj2_rep q, proj2_rep r] ** M' = mat 1) = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))
[PROOF STEP]
unfolding invertible_def
[PROOF STATE]
proof (prove)
using this:
(?A ** ?A' = mat (1::?'a)) = (?A' ** ?A = mat (1::?'a))

goal (1 subgoal):
 1. (\<nexists>M'. vector [proj2_rep p, proj2_rep q, proj2_rep r] ** M' = mat 1) = (\<nexists>A'. vector [proj2_rep p, proj2_rep q, proj2_rep r] ** A' = mat 1 \<and> A' ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<nexists>M'. vector [proj2_rep p, proj2_rep q, proj2_rep r] ** M' = mat 1) = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))

goal (1 subgoal):
 1. proj2_Col p q r = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
proj2_Col p q r = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))
[PROOF STEP]
show "proj2_Col p q r \<longleftrightarrow> \<not> invertible ?M"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q r = (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r]))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_invertible_iff_proj2_set_Col:
  "\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r] :: real^3^3)
  \<longleftrightarrow> proj2_set_Col {p,q,r}"
  (is "\<not> invertible ?M \<longleftrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}
[PROOF STEP]
from left_invertible_iff_invertible
[PROOF STATE]
proof (chain)
picking this:
(\<exists>N. N ** ?M = mat 1) = invertible ?M
[PROOF STEP]
have "\<not> invertible ?M  \<longleftrightarrow> \<not> (\<exists> M'. M' ** ?M = mat 1)"
[PROOF STATE]
proof (prove)
using this:
(\<exists>N. N ** ?M = mat 1) = invertible ?M

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

goal (1 subgoal):
 1. (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = (\<nexists>M'. M' ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1)

goal (1 subgoal):
 1. (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}
[PROOF STEP]
from matrix_left_invertible_ker [of ?M]
[PROOF STATE]
proof (chain)
picking this:
(\<exists>B. B ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1) = (\<forall>x. vector [proj2_rep p, proj2_rep q, proj2_rep r] *v x = 0 \<longrightarrow> x = 0)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<exists> y. y \<noteq> 0 \<and> ?M *v y = 0)"
[PROOF STATE]
proof (prove)
using this:
(\<exists>B. B ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1) = (\<forall>x. vector [proj2_rep p, proj2_rep q, proj2_rep r] *v x = 0 \<longrightarrow> x = 0)

goal (1 subgoal):
 1. (\<nexists>M'. M' ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1) = (\<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<nexists>M'. M' ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1) = (\<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0)

goal (1 subgoal):
 1. (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<nexists>M'. M' ** vector [proj2_rep p, proj2_rep q, proj2_rep r] = mat 1) = (\<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0)

goal (1 subgoal):
 1. (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<exists> l. \<forall> s\<in>{p,q,r}. proj2_incident s l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0) = (\<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0 \<Longrightarrow> \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l
 2. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
assume "\<exists> y. y \<noteq> 0 \<and> ?M *v y = 0"
[PROOF STATE]
proof (state)
this:
\<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0

goal (2 subgoals):
 1. \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0 \<Longrightarrow> \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l
 2. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
obtain y where "y \<noteq> 0" and "?M *v y = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<noteq> 0; vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<noteq> 0
vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0

goal (2 subgoals):
 1. \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0 \<Longrightarrow> \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l
 2. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
let ?l = "proj2_line_abs y"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0 \<Longrightarrow> \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l
 2. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
from \<open>?M *v y = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
have "\<forall> s\<in>{p,q,r}. proj2_rep s \<bullet> y = 0"
[PROOF STATE]
proof (prove)
using this:
vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0

goal (1 subgoal):
 1. \<forall>s\<in>{p, q, r}. proj2_rep s \<bullet> y = 0
[PROOF STEP]
unfolding vector_def
        and matrix_vector_mult_def
        and inner_vec_def
        and sum_3
[PROOF STATE]
proof (prove)
using this:
(\<chi>i. 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 $ 1 * y $ 1 + 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 $ 2 * y $ 2 + 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 $ 3 * y $ 3) = 0

goal (1 subgoal):
 1. \<forall>s\<in>{p, q, r}. proj2_rep s $ 1 \<bullet> y $ 1 + proj2_rep s $ 2 \<bullet> y $ 2 + proj2_rep s $ 3 \<bullet> y $ 3 = 0
[PROOF STEP]
by (simp add: vec_eq_iff forall_3)
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>{p, q, r}. proj2_rep s \<bullet> y = 0

goal (2 subgoals):
 1. \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0 \<Longrightarrow> \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l
 2. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
with \<open>y \<noteq> 0\<close> and proj2_incident_right_abs
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> proj2_incident ?p (proj2_line_abs ?v) = (proj2_rep ?p \<bullet> ?v = 0)
\<forall>s\<in>{p, q, r}. proj2_rep s \<bullet> y = 0
[PROOF STEP]
have "\<forall> s\<in>{p,q,r}. proj2_incident s ?l"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> 0
?v \<noteq> 0 \<Longrightarrow> proj2_incident ?p (proj2_line_abs ?v) = (proj2_rep ?p \<bullet> ?v = 0)
\<forall>s\<in>{p, q, r}. proj2_rep s \<bullet> y = 0

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

goal (2 subgoals):
 1. \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0 \<Longrightarrow> \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l
 2. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
thus "\<exists> l. \<forall> s\<in>{p,q,r}. proj2_incident s l"
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>{p, q, r}. proj2_incident s (proj2_line_abs y)

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

goal (1 subgoal):
 1. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
assume "\<exists> l. \<forall> s\<in>{p,q,r}. proj2_incident s l"
[PROOF STATE]
proof (state)
this:
\<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l

goal (1 subgoal):
 1. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l
[PROOF STEP]
obtain l where "\<forall> s\<in>{p,q,r}. proj2_incident s l"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l

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

goal (1 subgoal):
 1. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
let ?y = "proj2_line_rep l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
have "?y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_line_rep l \<noteq> 0
[PROOF STEP]
by (rule proj2_line_rep_non_zero)
[PROOF STATE]
proof (state)
this:
proj2_line_rep l \<noteq> 0

goal (1 subgoal):
 1. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
proj2_line_rep l \<noteq> 0

goal (1 subgoal):
 1. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
proj2_line_rep l \<noteq> 0

goal (1 subgoal):
 1. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
from \<open>\<forall> s\<in>{p,q,r}. proj2_incident s l\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>s\<in>{p, q, r}. proj2_incident s l
[PROOF STEP]
have "?M *v ?y = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>{p, q, r}. proj2_incident s l

goal (1 subgoal):
 1. vector [proj2_rep p, proj2_rep q, proj2_rep r] *v proj2_line_rep l = 0
[PROOF STEP]
unfolding vector_def
          and matrix_vector_mult_def
          and inner_vec_def
          and sum_3
          and proj2_incident_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>{p, q, r}. proj2_rep s $ 1 \<bullet> proj2_line_rep l $ 1 + proj2_rep s $ 2 \<bullet> proj2_line_rep l $ 2 + proj2_rep s $ 3 \<bullet> proj2_line_rep l $ 3 = 0

goal (1 subgoal):
 1. (\<chi>i. 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 $ 1 * proj2_line_rep l $ 1 + 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 $ 2 * proj2_line_rep l $ 2 + 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 $ 3 * proj2_line_rep l $ 3) = 0
[PROOF STEP]
by (simp add: vec_eq_iff)
[PROOF STATE]
proof (state)
this:
vector [proj2_rep p, proj2_rep q, proj2_rep r] *v proj2_line_rep l = 0

goal (1 subgoal):
 1. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
vector [proj2_rep p, proj2_rep q, proj2_rep r] *v proj2_line_rep l = 0

goal (1 subgoal):
 1. \<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l \<Longrightarrow> \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
proj2_line_rep l \<noteq> 0
vector [proj2_rep p, proj2_rep q, proj2_rep r] *v proj2_line_rep l = 0
[PROOF STEP]
show "\<exists> y. y \<noteq> 0 \<and> ?M *v y = 0"
[PROOF STATE]
proof (prove)
using this:
proj2_line_rep l \<noteq> 0
vector [proj2_rep p, proj2_rep q, proj2_rep r] *v proj2_line_rep l = 0

goal (1 subgoal):
 1. \<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>y. y \<noteq> 0 \<and> vector [proj2_rep p, proj2_rep q, proj2_rep r] *v y = 0) = (\<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l)

goal (1 subgoal):
 1. (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = (\<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l)
[PROOF STEP]
show "\<not> invertible ?M \<longleftrightarrow> proj2_set_Col {p,q,r}"
[PROOF STATE]
proof (prove)
using this:
(\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = (\<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l)

goal (1 subgoal):
 1. (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}
[PROOF STEP]
unfolding proj2_set_Col_def
[PROOF STATE]
proof (prove)
using this:
(\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = (\<exists>l. \<forall>s\<in>{p, q, r}. proj2_incident s l)

goal (1 subgoal):
 1. (\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = (\<exists>l. \<forall>p\<in>{p, q, r}. proj2_incident p l)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<not> invertible (vector [proj2_rep p, proj2_rep q, proj2_rep r])) = proj2_set_Col {p, q, r}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_Col_iff_set_Col:
  "proj2_Col p q r \<longleftrightarrow> proj2_set_Col {p,q,r}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col p q r = proj2_set_Col {p, q, r}
[PROOF STEP]
by (simp add: proj2_Col_iff_not_invertible
    not_invertible_iff_proj2_set_Col)