[STATEMENT]
lemma cltn2_abs_mult:
  assumes "k \<noteq> 0" and "invertible A"
  shows "cltn2_abs (k *\<^sub>R A) = cltn2_abs A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_abs (k *\<^sub>R A) = cltn2_abs A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_abs (k *\<^sub>R A) = cltn2_abs A
[PROOF STEP]
from \<open>k \<noteq> 0\<close> and \<open>invertible A\<close> and scalar_invertible
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
invertible A
\<lbrakk>?k \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> invertible (?k *\<^sub>R ?A)
[PROOF STEP]
have "invertible (k *\<^sub>R A)"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
invertible A
\<lbrakk>?k \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> invertible (?k *\<^sub>R ?A)

goal (1 subgoal):
 1. invertible (k *\<^sub>R A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible (k *\<^sub>R A)

goal (1 subgoal):
 1. cltn2_abs (k *\<^sub>R A) = cltn2_abs A
[PROOF STEP]
with \<open>invertible A\<close>
[PROOF STATE]
proof (chain)
picking this:
invertible A
invertible (k *\<^sub>R A)
[PROOF STEP]
have "(k *\<^sub>R A, A) \<in> invertible_proportionality"
[PROOF STATE]
proof (prove)
using this:
invertible A
invertible (k *\<^sub>R A)

goal (1 subgoal):
 1. (k *\<^sub>R A, A) \<in> invertible_proportionality
[PROOF STEP]
unfolding invertible_proportionality_def
      and real_vector.proportionality_def
[PROOF STATE]
proof (prove)
using this:
invertible A
invertible (k *\<^sub>R A)

goal (1 subgoal):
 1. (k *\<^sub>R A, A) \<in> Restr {(x, y). x \<noteq> 0 \<and> y \<noteq> 0 \<and> (\<exists>k. x = k *\<^sub>R y)} (Collect invertible)
[PROOF STEP]
by (auto simp add: zero_not_invertible)
[PROOF STATE]
proof (state)
this:
(k *\<^sub>R A, A) \<in> invertible_proportionality

goal (1 subgoal):
 1. cltn2_abs (k *\<^sub>R A) = cltn2_abs A
[PROOF STEP]
with eq_equiv_class_iff
  [of "Collect invertible" invertible_proportionality "k *\<^sub>R A" A]
    and invertible_proportionality_equiv
    and \<open>invertible A\<close> and \<open>invertible (k *\<^sub>R A)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>equiv (Collect invertible) invertible_proportionality; k *\<^sub>R A \<in> Collect invertible; A \<in> Collect invertible\<rbrakk> \<Longrightarrow> (invertible_proportionality `` {k *\<^sub>R A} = invertible_proportionality `` {A}) = ((k *\<^sub>R A, A) \<in> invertible_proportionality)
equiv (Collect invertible) invertible_proportionality
invertible A
invertible (k *\<^sub>R A)
(k *\<^sub>R A, A) \<in> invertible_proportionality
[PROOF STEP]
have "invertible_proportionality `` {k *\<^sub>R A}
    = invertible_proportionality `` {A}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>equiv (Collect invertible) invertible_proportionality; k *\<^sub>R A \<in> Collect invertible; A \<in> Collect invertible\<rbrakk> \<Longrightarrow> (invertible_proportionality `` {k *\<^sub>R A} = invertible_proportionality `` {A}) = ((k *\<^sub>R A, A) \<in> invertible_proportionality)
equiv (Collect invertible) invertible_proportionality
invertible A
invertible (k *\<^sub>R A)
(k *\<^sub>R A, A) \<in> invertible_proportionality

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

goal (1 subgoal):
 1. cltn2_abs (k *\<^sub>R A) = cltn2_abs A
[PROOF STEP]
thus "cltn2_abs (k *\<^sub>R A) = cltn2_abs A"
[PROOF STATE]
proof (prove)
using this:
invertible_proportionality `` {k *\<^sub>R A} = invertible_proportionality `` {A}

goal (1 subgoal):
 1. cltn2_abs (k *\<^sub>R A) = cltn2_abs A
[PROOF STEP]
unfolding cltn2_abs_def
[PROOF STATE]
proof (prove)
using this:
invertible_proportionality `` {k *\<^sub>R A} = invertible_proportionality `` {A}

goal (1 subgoal):
 1. Abs_cltn2 (invertible_proportionality `` {k *\<^sub>R A}) = Abs_cltn2 (invertible_proportionality `` {A})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_abs (k *\<^sub>R A) = cltn2_abs A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_abs_mult_rep:
  assumes "k \<noteq> 0"
  shows "cltn2_abs (k *\<^sub>R cltn2_rep A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_abs (k *\<^sub>R cltn2_rep A) = A
[PROOF STEP]
using cltn2_rep_invertible and cltn2_abs_mult and cltn2_abs_rep and assms
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep ?A)
\<lbrakk>?k \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> cltn2_abs (?k *\<^sub>R ?A) = cltn2_abs ?A
cltn2_abs (cltn2_rep ?A) = ?A
k \<noteq> 0

goal (1 subgoal):
 1. cltn2_abs (k *\<^sub>R cltn2_rep A) = A
[PROOF STEP]
by simp


[STATEMENT]
lemma apply_cltn2_abs:
  assumes "x \<noteq> 0" and "invertible A"
  shows "apply_cltn2 (proj2_abs x) (cltn2_abs A) = proj2_abs (x v* A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2 (proj2_abs x) (cltn2_abs A) = proj2_abs (x v* A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. apply_cltn2 (proj2_abs x) (cltn2_abs A) = proj2_abs (x v* A)
[PROOF STEP]
from proj2_rep_abs2 and \<open>x \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
x \<noteq> 0
[PROOF STEP]
obtain k where "k \<noteq> 0" and "proj2_rep (proj2_abs x) = k *\<^sub>R x"
[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
x \<noteq> 0

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

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs x) (cltn2_abs A) = proj2_abs (x v* A)
[PROOF STEP]
from cltn2_rep_abs2 and \<open>invertible A\<close>
[PROOF STATE]
proof (chain)
picking this:
invertible ?A \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs ?A) = k *\<^sub>R ?A
invertible A
[PROOF STEP]
obtain c where "c \<noteq> 0" and "cltn2_rep (cltn2_abs A) = c *\<^sub>R A"
[PROOF STATE]
proof (prove)
using this:
invertible ?A \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs ?A) = k *\<^sub>R ?A
invertible A

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

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs x) (cltn2_abs A) = proj2_abs (x v* A)
[PROOF STEP]
from \<open>k \<noteq> 0\<close> and \<open>c \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
c \<noteq> 0
[PROOF STEP]
have "k * c \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
c \<noteq> 0

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

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

goal (1 subgoal):
 1. proj2_rep (proj2_abs x) v* cltn2_rep (cltn2_abs A) = (k * c) *\<^sub>R (x v* A)
[PROOF STEP]
by (simp add: scaleR_vector_matrix_assoc vector_scaleR_matrix_ac)
[PROOF STATE]
proof (state)
this:
proj2_rep (proj2_abs x) v* cltn2_rep (cltn2_abs A) = (k * c) *\<^sub>R (x v* A)

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

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs x) (cltn2_abs A) = proj2_abs (x v* A)
[PROOF STEP]
unfolding apply_cltn2_def
[PROOF STATE]
proof (prove)
using this:
k * c \<noteq> 0
proj2_rep (proj2_abs x) v* cltn2_rep (cltn2_abs A) = (k * c) *\<^sub>R (x v* A)

goal (1 subgoal):
 1. proj2_abs (proj2_rep (proj2_abs x) v* cltn2_rep (cltn2_abs A)) = proj2_abs (x v* A)
[PROOF STEP]
by (simp add: proj2_abs_mult)
[PROOF STATE]
proof (state)
this:
apply_cltn2 (proj2_abs x) (cltn2_abs A) = proj2_abs (x v* A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_cltn2_left_abs:
  assumes "v \<noteq> 0"
  shows "apply_cltn2 (proj2_abs v) C = proj2_abs (v v* cltn2_rep C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2 (proj2_abs v) C = proj2_abs (v v* cltn2_rep C)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. apply_cltn2 (proj2_abs v) C = proj2_abs (v v* cltn2_rep C)
[PROOF STEP]
have "cltn2_abs (cltn2_rep C) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_abs (cltn2_rep C) = C
[PROOF STEP]
by (rule cltn2_abs_rep)
[PROOF STATE]
proof (state)
this:
cltn2_abs (cltn2_rep C) = C

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs v) C = proj2_abs (v v* cltn2_rep C)
[PROOF STEP]
with \<open>v \<noteq> 0\<close> and cltn2_rep_invertible and apply_cltn2_abs [of v "cltn2_rep C"]
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> 0
invertible (cltn2_rep ?A)
\<lbrakk>v \<noteq> 0; invertible (cltn2_rep C)\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs v) (cltn2_abs (cltn2_rep C)) = proj2_abs (v v* cltn2_rep C)
cltn2_abs (cltn2_rep C) = C
[PROOF STEP]
show "apply_cltn2 (proj2_abs v) C = proj2_abs (v v* cltn2_rep C)"
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0
invertible (cltn2_rep ?A)
\<lbrakk>v \<noteq> 0; invertible (cltn2_rep C)\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs v) (cltn2_abs (cltn2_rep C)) = proj2_abs (v v* cltn2_rep C)
cltn2_abs (cltn2_rep C) = C

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_cltn2_right_abs:
  assumes "invertible M"
  shows "apply_cltn2 p (cltn2_abs M) = proj2_abs (proj2_rep p v* M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2 p (cltn2_abs M) = proj2_abs (proj2_rep p v* M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. apply_cltn2 p (cltn2_abs M) = proj2_abs (proj2_rep p v* M)
[PROOF STEP]
from proj2_rep_non_zero and \<open>invertible M\<close> and apply_cltn2_abs
[PROOF STATE]
proof (chain)
picking this:
proj2_rep ?x \<noteq> 0
invertible M
\<lbrakk>?x \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs ?x) (cltn2_abs ?A) = proj2_abs (?x v* ?A)
[PROOF STEP]
have "apply_cltn2 (proj2_abs (proj2_rep p)) (cltn2_abs M)
    = proj2_abs (proj2_rep p v* M)"
[PROOF STATE]
proof (prove)
using this:
proj2_rep ?x \<noteq> 0
invertible M
\<lbrakk>?x \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs ?x) (cltn2_abs ?A) = proj2_abs (?x v* ?A)

goal (1 subgoal):
 1. apply_cltn2 (proj2_abs (proj2_rep p)) (cltn2_abs M) = proj2_abs (proj2_rep p v* M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (proj2_abs (proj2_rep p)) (cltn2_abs M) = proj2_abs (proj2_rep p v* M)

goal (1 subgoal):
 1. apply_cltn2 p (cltn2_abs M) = proj2_abs (proj2_rep p v* M)
[PROOF STEP]
thus "apply_cltn2 p (cltn2_abs M) = proj2_abs (proj2_rep p v* M)"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (proj2_abs (proj2_rep p)) (cltn2_abs M) = proj2_abs (proj2_rep p v* M)

goal (1 subgoal):
 1. apply_cltn2 p (cltn2_abs M) = proj2_abs (proj2_rep p v* M)
[PROOF STEP]
by (simp add: proj2_abs_rep)
[PROOF STATE]
proof (state)
this:
apply_cltn2 p (cltn2_abs M) = proj2_abs (proj2_rep p v* M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma non_zero_mult_rep_non_zero:
  assumes "v \<noteq> 0"
  shows "v v* cltn2_rep C \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v v* cltn2_rep C \<noteq> 0
[PROOF STEP]
using \<open>v \<noteq> 0\<close> and cltn2_rep_invertible and times_invertible_eq_zero
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0
invertible (cltn2_rep ?A)
\<lbrakk>invertible ?A; ?x v* ?A = 0\<rbrakk> \<Longrightarrow> ?x = 0

goal (1 subgoal):
 1. v v* cltn2_rep C \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma rep_mult_rep_non_zero: "proj2_rep p v* cltn2_rep A \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep p v* cltn2_rep A \<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 p v* cltn2_rep A \<noteq> 0
[PROOF STEP]
by (rule non_zero_mult_rep_non_zero)


[STATEMENT]
lemma cltn2_compose_abs:
  assumes "invertible M" and "invertible N"
  shows "cltn2_compose (cltn2_abs M) (cltn2_abs N) = cltn2_abs (M ** N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) (cltn2_abs N) = cltn2_abs (M ** N)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) (cltn2_abs N) = cltn2_abs (M ** N)
[PROOF STEP]
from \<open>invertible M\<close> and \<open>invertible N\<close> and invertible_mult
[PROOF STATE]
proof (chain)
picking this:
invertible M
invertible N
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)
[PROOF STEP]
have "invertible (M ** N)"
[PROOF STATE]
proof (prove)
using this:
invertible M
invertible N
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)

goal (1 subgoal):
 1. invertible (M ** N)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible (M ** N)

goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) (cltn2_abs N) = cltn2_abs (M ** N)
[PROOF STEP]
from \<open>invertible M\<close> and \<open>invertible N\<close> and cltn2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
invertible M
invertible N
invertible ?A \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs ?A) = k *\<^sub>R ?A
[PROOF STEP]
obtain j and k where "j \<noteq> 0" and "k \<noteq> 0"
    and "cltn2_rep (cltn2_abs M) = j *\<^sub>R M"
    and "cltn2_rep (cltn2_abs N) = k *\<^sub>R N"
[PROOF STATE]
proof (prove)
using this:
invertible M
invertible N
invertible ?A \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs ?A) = k *\<^sub>R ?A

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

goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) (cltn2_abs N) = cltn2_abs (M ** N)
[PROOF STEP]
from \<open>j \<noteq> 0\<close> and \<open>k \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
j \<noteq> 0
k \<noteq> 0
[PROOF STEP]
have "j * k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
k \<noteq> 0

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

goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) (cltn2_abs N) = cltn2_abs (M ** N)
[PROOF STEP]
from \<open>cltn2_rep (cltn2_abs M) = j *\<^sub>R M\<close> and \<open>cltn2_rep (cltn2_abs N) = k *\<^sub>R N\<close>
[PROOF STATE]
proof (chain)
picking this:
cltn2_rep (cltn2_abs M) = j *\<^sub>R M
cltn2_rep (cltn2_abs N) = k *\<^sub>R N
[PROOF STEP]
have "cltn2_rep (cltn2_abs M) ** cltn2_rep (cltn2_abs N)
    = (j * k) *\<^sub>R (M ** N)"
[PROOF STATE]
proof (prove)
using this:
cltn2_rep (cltn2_abs M) = j *\<^sub>R M
cltn2_rep (cltn2_abs N) = k *\<^sub>R N

goal (1 subgoal):
 1. cltn2_rep (cltn2_abs M) ** cltn2_rep (cltn2_abs N) = (j * k) *\<^sub>R (M ** N)
[PROOF STEP]
by (simp add: matrix_scalar_ac scalar_matrix_assoc [symmetric])
[PROOF STATE]
proof (state)
this:
cltn2_rep (cltn2_abs M) ** cltn2_rep (cltn2_abs N) = (j * k) *\<^sub>R (M ** N)

goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) (cltn2_abs N) = cltn2_abs (M ** N)
[PROOF STEP]
with \<open>j * k \<noteq> 0\<close> and \<open>invertible (M ** N)\<close>
[PROOF STATE]
proof (chain)
picking this:
j * k \<noteq> 0
invertible (M ** N)
cltn2_rep (cltn2_abs M) ** cltn2_rep (cltn2_abs N) = (j * k) *\<^sub>R (M ** N)
[PROOF STEP]
show "cltn2_compose (cltn2_abs M) (cltn2_abs N) = cltn2_abs (M ** N)"
[PROOF STATE]
proof (prove)
using this:
j * k \<noteq> 0
invertible (M ** N)
cltn2_rep (cltn2_abs M) ** cltn2_rep (cltn2_abs N) = (j * k) *\<^sub>R (M ** N)

goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) (cltn2_abs N) = cltn2_abs (M ** N)
[PROOF STEP]
unfolding cltn2_compose_def
[PROOF STATE]
proof (prove)
using this:
j * k \<noteq> 0
invertible (M ** N)
cltn2_rep (cltn2_abs M) ** cltn2_rep (cltn2_abs N) = (j * k) *\<^sub>R (M ** N)

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs M) ** cltn2_rep (cltn2_abs N)) = cltn2_abs (M ** N)
[PROOF STEP]
by (simp add: cltn2_abs_mult)
[PROOF STATE]
proof (state)
this:
cltn2_compose (cltn2_abs M) (cltn2_abs N) = cltn2_abs (M ** N)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_compose_left_abs:
  assumes "invertible M"
  shows "cltn2_compose (cltn2_abs M) A = cltn2_abs (M ** cltn2_rep A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) A = cltn2_abs (M ** cltn2_rep A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) A = cltn2_abs (M ** cltn2_rep A)
[PROOF STEP]
from \<open>invertible M\<close> and cltn2_rep_invertible and cltn2_compose_abs
[PROOF STATE]
proof (chain)
picking this:
invertible M
invertible (cltn2_rep ?A)
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_compose (cltn2_abs ?M) (cltn2_abs ?N) = cltn2_abs (?M ** ?N)
[PROOF STEP]
have "cltn2_compose (cltn2_abs M) (cltn2_abs (cltn2_rep A))
    = cltn2_abs (M ** cltn2_rep A)"
[PROOF STATE]
proof (prove)
using this:
invertible M
invertible (cltn2_rep ?A)
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_compose (cltn2_abs ?M) (cltn2_abs ?N) = cltn2_abs (?M ** ?N)

goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) (cltn2_abs (cltn2_rep A)) = cltn2_abs (M ** cltn2_rep A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_compose (cltn2_abs M) (cltn2_abs (cltn2_rep A)) = cltn2_abs (M ** cltn2_rep A)

goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) A = cltn2_abs (M ** cltn2_rep A)
[PROOF STEP]
thus "cltn2_compose (cltn2_abs M) A = cltn2_abs (M ** cltn2_rep A)"
[PROOF STATE]
proof (prove)
using this:
cltn2_compose (cltn2_abs M) (cltn2_abs (cltn2_rep A)) = cltn2_abs (M ** cltn2_rep A)

goal (1 subgoal):
 1. cltn2_compose (cltn2_abs M) A = cltn2_abs (M ** cltn2_rep A)
[PROOF STEP]
by (simp add: cltn2_abs_rep)
[PROOF STATE]
proof (state)
this:
cltn2_compose (cltn2_abs M) A = cltn2_abs (M ** cltn2_rep A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_compose_right_abs:
  assumes "invertible M"
  shows "cltn2_compose A (cltn2_abs M) = cltn2_abs (cltn2_rep A ** M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_compose A (cltn2_abs M) = cltn2_abs (cltn2_rep A ** M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose A (cltn2_abs M) = cltn2_abs (cltn2_rep A ** M)
[PROOF STEP]
from \<open>invertible M\<close> and cltn2_rep_invertible and cltn2_compose_abs
[PROOF STATE]
proof (chain)
picking this:
invertible M
invertible (cltn2_rep ?A)
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_compose (cltn2_abs ?M) (cltn2_abs ?N) = cltn2_abs (?M ** ?N)
[PROOF STEP]
have "cltn2_compose (cltn2_abs (cltn2_rep A)) (cltn2_abs M)
    = cltn2_abs (cltn2_rep A ** M)"
[PROOF STATE]
proof (prove)
using this:
invertible M
invertible (cltn2_rep ?A)
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_compose (cltn2_abs ?M) (cltn2_abs ?N) = cltn2_abs (?M ** ?N)

goal (1 subgoal):
 1. cltn2_compose (cltn2_abs (cltn2_rep A)) (cltn2_abs M) = cltn2_abs (cltn2_rep A ** M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_compose (cltn2_abs (cltn2_rep A)) (cltn2_abs M) = cltn2_abs (cltn2_rep A ** M)

goal (1 subgoal):
 1. cltn2_compose A (cltn2_abs M) = cltn2_abs (cltn2_rep A ** M)
[PROOF STEP]
thus "cltn2_compose A (cltn2_abs M) = cltn2_abs (cltn2_rep A ** M)"
[PROOF STATE]
proof (prove)
using this:
cltn2_compose (cltn2_abs (cltn2_rep A)) (cltn2_abs M) = cltn2_abs (cltn2_rep A ** M)

goal (1 subgoal):
 1. cltn2_compose A (cltn2_abs M) = cltn2_abs (cltn2_rep A ** M)
[PROOF STEP]
by (simp add: cltn2_abs_rep)
[PROOF STATE]
proof (state)
this:
cltn2_compose A (cltn2_abs M) = cltn2_abs (cltn2_rep A ** M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_abs_rep_abs_mult:
  assumes "invertible M" and "invertible N"
  shows "cltn2_abs (cltn2_rep (cltn2_abs M) ** N) = cltn2_abs (M ** N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs M) ** N) = cltn2_abs (M ** N)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs M) ** N) = cltn2_abs (M ** N)
[PROOF STEP]
from \<open>invertible M\<close> and \<open>invertible N\<close>
[PROOF STATE]
proof (chain)
picking this:
invertible M
invertible N
[PROOF STEP]
have "invertible (M ** N)"
[PROOF STATE]
proof (prove)
using this:
invertible M
invertible N

goal (1 subgoal):
 1. invertible (M ** N)
[PROOF STEP]
by (simp add: invertible_mult)
[PROOF STATE]
proof (state)
this:
invertible (M ** N)

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs M) ** N) = cltn2_abs (M ** N)
[PROOF STEP]
from \<open>invertible M\<close> and cltn2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
invertible M
invertible ?A \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs ?A) = k *\<^sub>R ?A
[PROOF STEP]
obtain k where "k \<noteq> 0" and "cltn2_rep (cltn2_abs M) = k *\<^sub>R M"
[PROOF STATE]
proof (prove)
using this:
invertible M
invertible ?A \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs ?A) = k *\<^sub>R ?A

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

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs M) ** N) = cltn2_abs (M ** N)
[PROOF STEP]
from \<open>cltn2_rep (cltn2_abs M) = k *\<^sub>R M\<close>
[PROOF STATE]
proof (chain)
picking this:
cltn2_rep (cltn2_abs M) = k *\<^sub>R M
[PROOF STEP]
have "cltn2_rep (cltn2_abs M) ** N = k *\<^sub>R M ** N"
[PROOF STATE]
proof (prove)
using this:
cltn2_rep (cltn2_abs M) = k *\<^sub>R M

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

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs M) ** N) = cltn2_abs (M ** N)
[PROOF STEP]
with \<open>k \<noteq> 0\<close> and \<open>invertible (M ** N)\<close> and cltn2_abs_mult
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
invertible (M ** N)
\<lbrakk>?k \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> cltn2_abs (?k *\<^sub>R ?A) = cltn2_abs ?A
cltn2_rep (cltn2_abs M) ** N = k *\<^sub>R M ** N
[PROOF STEP]
show "cltn2_abs (cltn2_rep (cltn2_abs M) ** N) = cltn2_abs (M ** N)"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
invertible (M ** N)
\<lbrakk>?k \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> cltn2_abs (?k *\<^sub>R ?A) = cltn2_abs ?A
cltn2_rep (cltn2_abs M) ** N = k *\<^sub>R M ** N

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs M) ** N) = cltn2_abs (M ** N)
[PROOF STEP]
by (simp add: scalar_matrix_assoc [symmetric])
[PROOF STATE]
proof (state)
this:
cltn2_abs (cltn2_rep (cltn2_abs M) ** N) = cltn2_abs (M ** N)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_assoc:
  "cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
let ?A' = "cltn2_rep A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
let ?B' = "cltn2_rep B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
let ?C' = "cltn2_rep C"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
from cltn2_rep_invertible
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep ?A)
[PROOF STEP]
have "invertible ?A'" and "invertible ?B'" and "invertible ?C'"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep ?A)

goal (1 subgoal):
 1. invertible (cltn2_rep A) &&& invertible (cltn2_rep B) &&& invertible (cltn2_rep C)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
invertible (cltn2_rep A)
invertible (cltn2_rep B)
invertible (cltn2_rep C)

goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
with invertible_mult
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)
invertible (cltn2_rep A)
invertible (cltn2_rep B)
invertible (cltn2_rep C)
[PROOF STEP]
have "invertible (?A' ** ?B')" and "invertible (?B' ** ?C')"
    and "invertible (?A' ** ?B' ** ?C')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)
invertible (cltn2_rep A)
invertible (cltn2_rep B)
invertible (cltn2_rep C)

goal (1 subgoal):
 1. invertible (cltn2_rep A ** cltn2_rep B) &&& invertible (cltn2_rep B ** cltn2_rep C) &&& invertible (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible (cltn2_rep A ** cltn2_rep B)
invertible (cltn2_rep B ** cltn2_rep C)
invertible (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)

goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
from \<open>invertible (?A' ** ?B')\<close> and \<open>invertible ?C'\<close> and cltn2_abs_rep_abs_mult
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep A ** cltn2_rep B)
invertible (cltn2_rep C)
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_abs (cltn2_rep (cltn2_abs ?M) ** ?N) = cltn2_abs (?M ** ?N)
[PROOF STEP]
have "cltn2_abs (cltn2_rep (cltn2_abs (?A' ** ?B')) ** ?C')
    = cltn2_abs (?A' ** ?B' ** ?C')"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep A ** cltn2_rep B)
invertible (cltn2_rep C)
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_abs (cltn2_rep (cltn2_abs ?M) ** ?N) = cltn2_abs (?M ** ?N)

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs (cltn2_rep A ** cltn2_rep B)) ** cltn2_rep C) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_abs (cltn2_rep (cltn2_abs (cltn2_rep A ** cltn2_rep B)) ** cltn2_rep C) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)

goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
from \<open>invertible (?B' ** ?C')\<close> and cltn2_rep_abs2 [of "?B' ** ?C'"]
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep B ** cltn2_rep C)
invertible (cltn2_rep B ** cltn2_rep C) \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C)) = k *\<^sub>R (cltn2_rep B ** cltn2_rep C)
[PROOF STEP]
obtain k where "k \<noteq> 0"
    and "cltn2_rep (cltn2_abs (?B' ** ?C')) = k *\<^sub>R (?B' ** ?C')"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep B ** cltn2_rep C)
invertible (cltn2_rep B ** cltn2_rep C) \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C)) = k *\<^sub>R (cltn2_rep B ** cltn2_rep C)

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

goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
from \<open>cltn2_rep (cltn2_abs (?B' ** ?C')) = k *\<^sub>R (?B' ** ?C')\<close>
[PROOF STATE]
proof (chain)
picking this:
cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C)) = k *\<^sub>R (cltn2_rep B ** cltn2_rep C)
[PROOF STEP]
have "?A' ** cltn2_rep (cltn2_abs (?B' ** ?C')) = k *\<^sub>R (?A' ** ?B' ** ?C')"
[PROOF STATE]
proof (prove)
using this:
cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C)) = k *\<^sub>R (cltn2_rep B ** cltn2_rep C)

goal (1 subgoal):
 1. cltn2_rep A ** cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C)) = k *\<^sub>R (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
[PROOF STEP]
by (simp add: matrix_scalar_ac matrix_mul_assoc scalar_matrix_assoc)
[PROOF STATE]
proof (state)
this:
cltn2_rep A ** cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C)) = k *\<^sub>R (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)

goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
with \<open>k \<noteq> 0\<close> and \<open>invertible (?A' ** ?B' ** ?C')\<close>
    and cltn2_abs_mult [of k "?A' ** ?B' ** ?C'"]
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
invertible (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
\<lbrakk>k \<noteq> 0; invertible (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)\<rbrakk> \<Longrightarrow> cltn2_abs (k *\<^sub>R (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
cltn2_rep A ** cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C)) = k *\<^sub>R (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
[PROOF STEP]
have "cltn2_abs (?A' ** cltn2_rep (cltn2_abs (?B' ** ?C')))
    = cltn2_abs (?A' ** ?B' ** ?C')"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
invertible (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
\<lbrakk>k \<noteq> 0; invertible (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)\<rbrakk> \<Longrightarrow> cltn2_abs (k *\<^sub>R (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
cltn2_rep A ** cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C)) = k *\<^sub>R (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep A ** cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C))) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_abs (cltn2_rep A ** cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C))) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)

goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
with \<open>cltn2_abs (cltn2_rep (cltn2_abs (?A' ** ?B')) ** ?C')
    = cltn2_abs (?A' ** ?B' ** ?C')\<close>
[PROOF STATE]
proof (chain)
picking this:
cltn2_abs (cltn2_rep (cltn2_abs (cltn2_rep A ** cltn2_rep B)) ** cltn2_rep C) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
cltn2_abs (cltn2_rep A ** cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C))) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
[PROOF STEP]
show
    "cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)"
[PROOF STATE]
proof (prove)
using this:
cltn2_abs (cltn2_rep (cltn2_abs (cltn2_rep A ** cltn2_rep B)) ** cltn2_rep C) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
cltn2_abs (cltn2_rep A ** cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C))) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)

goal (1 subgoal):
 1. cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)
[PROOF STEP]
unfolding cltn2_compose_def
[PROOF STATE]
proof (prove)
using this:
cltn2_abs (cltn2_rep (cltn2_abs (cltn2_rep A ** cltn2_rep B)) ** cltn2_rep C) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)
cltn2_abs (cltn2_rep A ** cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C))) = cltn2_abs (cltn2_rep A ** cltn2_rep B ** cltn2_rep C)

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs (cltn2_rep A ** cltn2_rep B)) ** cltn2_rep C) = cltn2_abs (cltn2_rep A ** cltn2_rep (cltn2_abs (cltn2_rep B ** cltn2_rep C)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_compose (cltn2_compose A B) C = cltn2_compose A (cltn2_compose B C)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_left_id: "cltn2_compose cltn2_id A = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_compose cltn2_id A = A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose cltn2_id A = A
[PROOF STEP]
let ?A' = "cltn2_rep A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_compose cltn2_id A = A
[PROOF STEP]
from cltn2_rep_invertible
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep ?A)
[PROOF STEP]
have "invertible ?A'"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep ?A)

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

goal (1 subgoal):
 1. cltn2_compose cltn2_id A = A
[PROOF STEP]
with matrix_id_invertible and cltn2_abs_rep_abs_mult [of "mat 1" ?A']
[PROOF STATE]
proof (chain)
picking this:
invertible (mat (1::?'a))
\<lbrakk>invertible (mat 1); invertible (cltn2_rep A)\<rbrakk> \<Longrightarrow> cltn2_abs (cltn2_rep (cltn2_abs (mat 1)) ** cltn2_rep A) = cltn2_abs (mat 1 ** cltn2_rep A)
invertible (cltn2_rep A)
[PROOF STEP]
have "cltn2_compose cltn2_id A = cltn2_abs (cltn2_rep A)"
[PROOF STATE]
proof (prove)
using this:
invertible (mat (1::?'a))
\<lbrakk>invertible (mat 1); invertible (cltn2_rep A)\<rbrakk> \<Longrightarrow> cltn2_abs (cltn2_rep (cltn2_abs (mat 1)) ** cltn2_rep A) = cltn2_abs (mat 1 ** cltn2_rep A)
invertible (cltn2_rep A)

goal (1 subgoal):
 1. cltn2_compose cltn2_id A = cltn2_abs (cltn2_rep A)
[PROOF STEP]
unfolding cltn2_compose_def and cltn2_id_def
[PROOF STATE]
proof (prove)
using this:
invertible (mat (1::?'a))
\<lbrakk>invertible (mat 1); invertible (cltn2_rep A)\<rbrakk> \<Longrightarrow> cltn2_abs (cltn2_rep (cltn2_abs (mat 1)) ** cltn2_rep A) = cltn2_abs (mat 1 ** cltn2_rep A)
invertible (cltn2_rep A)

goal (1 subgoal):
 1. cltn2_abs (cltn2_rep (cltn2_abs (mat 1)) ** cltn2_rep A) = cltn2_abs (cltn2_rep A)
[PROOF STEP]
by (auto simp add: matrix_mul_lid)
[PROOF STATE]
proof (state)
this:
cltn2_compose cltn2_id A = cltn2_abs (cltn2_rep A)

goal (1 subgoal):
 1. cltn2_compose cltn2_id A = A
[PROOF STEP]
with cltn2_abs_rep
[PROOF STATE]
proof (chain)
picking this:
cltn2_abs (cltn2_rep ?A) = ?A
cltn2_compose cltn2_id A = cltn2_abs (cltn2_rep A)
[PROOF STEP]
show "cltn2_compose cltn2_id A = A"
[PROOF STATE]
proof (prove)
using this:
cltn2_abs (cltn2_rep ?A) = ?A
cltn2_compose cltn2_id A = cltn2_abs (cltn2_rep A)

goal (1 subgoal):
 1. cltn2_compose cltn2_id A = A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_compose cltn2_id A = A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_left_inverse_ex:
  "\<exists> B. cltn2_compose B A = cltn2_id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B. cltn2_compose B A = cltn2_id
[PROOF STEP]
using cltn2_left_inverse
[PROOF STATE]
proof (prove)
using this:
cltn2_compose (cltn2_inverse ?A) ?A = cltn2_id

goal (1 subgoal):
 1. \<exists>B. cltn2_compose B A = cltn2_id
[PROOF STEP]
..


[STATEMENT]
lemma cltn2_inverse_inv [simp]:
  "inv\<^bsub>(|carrier = UNIV, mult = cltn2_compose, one = cltn2_id|)\<^esub> A
  = cltn2_inverse A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> A = cltn2_inverse A
[PROOF STEP]
using cltn2_left_inverse [of A] and cltn2.inv_equality
[PROOF STATE]
proof (prove)
using this:
cltn2_compose (cltn2_inverse A) A = cltn2_id
\<lbrakk>?y \<otimes>\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> ?x = \<one>\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub>; ?x \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>; ?y \<in> carrier \<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<rbrakk> \<Longrightarrow> inv\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> ?x = ?y

goal (1 subgoal):
 1. inv\<^bsub>\<lparr>carrier = UNIV, monoid.mult = cltn2_compose, one = cltn2_id\<rparr>\<^esub> A = cltn2_inverse A
[PROOF STEP]
by simp


[STATEMENT]
lemma apply_cltn2_id [simp]: "apply_cltn2 p cltn2_id = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2 p cltn2_id = p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. apply_cltn2 p cltn2_id = p
[PROOF STEP]
from matrix_id_invertible and apply_cltn2_right_abs
[PROOF STATE]
proof (chain)
picking this:
invertible (mat (1::?'a))
invertible ?M \<Longrightarrow> apply_cltn2 ?p (cltn2_abs ?M) = proj2_abs (proj2_rep ?p v* ?M)
[PROOF STEP]
have "apply_cltn2 p cltn2_id = proj2_abs (proj2_rep p v* mat 1)"
[PROOF STATE]
proof (prove)
using this:
invertible (mat (1::?'a))
invertible ?M \<Longrightarrow> apply_cltn2 ?p (cltn2_abs ?M) = proj2_abs (proj2_rep ?p v* ?M)

goal (1 subgoal):
 1. apply_cltn2 p cltn2_id = proj2_abs (proj2_rep p v* mat 1)
[PROOF STEP]
unfolding cltn2_id_def
[PROOF STATE]
proof (prove)
using this:
invertible (mat (1::?'a))
invertible ?M \<Longrightarrow> apply_cltn2 ?p (cltn2_abs ?M) = proj2_abs (proj2_rep ?p v* ?M)

goal (1 subgoal):
 1. apply_cltn2 p (cltn2_abs (mat 1)) = proj2_abs (proj2_rep p v* mat 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
apply_cltn2 p cltn2_id = proj2_abs (proj2_rep p v* mat 1)

goal (1 subgoal):
 1. apply_cltn2 p cltn2_id = p
[PROOF STEP]
thus "apply_cltn2 p cltn2_id = p"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 p cltn2_id = proj2_abs (proj2_rep p v* mat 1)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_cltn2_compose:
  "apply_cltn2 (apply_cltn2 p A) B = apply_cltn2 p (cltn2_compose A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 p A) B = apply_cltn2 p (cltn2_compose A B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 p A) B = apply_cltn2 p (cltn2_compose A B)
[PROOF STEP]
from rep_mult_rep_non_zero and cltn2_rep_invertible and apply_cltn2_abs
[PROOF STATE]
proof (chain)
picking this:
proj2_rep ?p v* cltn2_rep ?A \<noteq> 0
invertible (cltn2_rep ?A)
\<lbrakk>?x \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs ?x) (cltn2_abs ?A) = proj2_abs (?x v* ?A)
[PROOF STEP]
have "apply_cltn2 (apply_cltn2 p A) (cltn2_abs (cltn2_rep B))
    = proj2_abs ((proj2_rep p v* cltn2_rep A) v* cltn2_rep B)"
[PROOF STATE]
proof (prove)
using this:
proj2_rep ?p v* cltn2_rep ?A \<noteq> 0
invertible (cltn2_rep ?A)
\<lbrakk>?x \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs ?x) (cltn2_abs ?A) = proj2_abs (?x v* ?A)

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 p A) (cltn2_abs (cltn2_rep B)) = proj2_abs (proj2_rep p v* cltn2_rep A v* cltn2_rep B)
[PROOF STEP]
unfolding apply_cltn2_def [of p A]
[PROOF STATE]
proof (prove)
using this:
proj2_rep ?p v* cltn2_rep ?A \<noteq> 0
invertible (cltn2_rep ?A)
\<lbrakk>?x \<noteq> 0; invertible ?A\<rbrakk> \<Longrightarrow> apply_cltn2 (proj2_abs ?x) (cltn2_abs ?A) = proj2_abs (?x v* ?A)

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

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 p A) B = apply_cltn2 p (cltn2_compose A B)
[PROOF STEP]
hence "apply_cltn2 (apply_cltn2 p A) B
    = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (apply_cltn2 p A) (cltn2_abs (cltn2_rep B)) = proj2_abs (proj2_rep p v* cltn2_rep A v* cltn2_rep B)

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 p A) B = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))
[PROOF STEP]
by (simp add: cltn2_abs_rep vector_matrix_mul_assoc)
[PROOF STATE]
proof (state)
this:
apply_cltn2 (apply_cltn2 p A) B = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 p A) B = apply_cltn2 p (cltn2_compose A B)
[PROOF STEP]
from cltn2_rep_invertible and invertible_mult
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep ?A)
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)
[PROOF STEP]
have "invertible (cltn2_rep A ** cltn2_rep B)"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep ?A)
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)

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

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 p A) B = apply_cltn2 p (cltn2_compose A B)
[PROOF STEP]
with apply_cltn2_right_abs
[PROOF STATE]
proof (chain)
picking this:
invertible ?M \<Longrightarrow> apply_cltn2 ?p (cltn2_abs ?M) = proj2_abs (proj2_rep ?p v* ?M)
invertible (cltn2_rep A ** cltn2_rep B)
[PROOF STEP]
have "apply_cltn2 p (cltn2_compose A B)
    = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))"
[PROOF STATE]
proof (prove)
using this:
invertible ?M \<Longrightarrow> apply_cltn2 ?p (cltn2_abs ?M) = proj2_abs (proj2_rep ?p v* ?M)
invertible (cltn2_rep A ** cltn2_rep B)

goal (1 subgoal):
 1. apply_cltn2 p (cltn2_compose A B) = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))
[PROOF STEP]
unfolding cltn2_compose_def
[PROOF STATE]
proof (prove)
using this:
invertible ?M \<Longrightarrow> apply_cltn2 ?p (cltn2_abs ?M) = proj2_abs (proj2_rep ?p v* ?M)
invertible (cltn2_rep A ** cltn2_rep B)

goal (1 subgoal):
 1. apply_cltn2 p (cltn2_abs (cltn2_rep A ** cltn2_rep B)) = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 p (cltn2_compose A B) = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 p A) B = apply_cltn2 p (cltn2_compose A B)
[PROOF STEP]
with \<open>apply_cltn2 (apply_cltn2 p A) B
    = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))\<close>
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 (apply_cltn2 p A) B = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))
apply_cltn2 p (cltn2_compose A B) = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))
[PROOF STEP]
show "apply_cltn2 (apply_cltn2 p A) B = apply_cltn2 p (cltn2_compose A B)"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (apply_cltn2 p A) B = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))
apply_cltn2 p (cltn2_compose A B) = proj2_abs (proj2_rep p v* (cltn2_rep A ** cltn2_rep B))

goal (1 subgoal):
 1. apply_cltn2 (apply_cltn2 p A) B = apply_cltn2 p (cltn2_compose A B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (apply_cltn2 p A) B = apply_cltn2 p (cltn2_compose A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_transpose_abs:
  assumes "invertible M"
  shows "cltn2_transpose (cltn2_abs M) = cltn2_abs (transpose M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_transpose (cltn2_abs M) = cltn2_abs (Finite_Cartesian_Product.transpose M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_transpose (cltn2_abs M) = cltn2_abs (Finite_Cartesian_Product.transpose M)
[PROOF STEP]
from \<open>invertible M\<close> and transpose_invertible
[PROOF STATE]
proof (chain)
picking this:
invertible M
invertible ?A \<Longrightarrow> invertible (Finite_Cartesian_Product.transpose ?A)
[PROOF STEP]
have "invertible (transpose M)"
[PROOF STATE]
proof (prove)
using this:
invertible M
invertible ?A \<Longrightarrow> invertible (Finite_Cartesian_Product.transpose ?A)

goal (1 subgoal):
 1. invertible (Finite_Cartesian_Product.transpose M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible (Finite_Cartesian_Product.transpose M)

goal (1 subgoal):
 1. cltn2_transpose (cltn2_abs M) = cltn2_abs (Finite_Cartesian_Product.transpose M)
[PROOF STEP]
from \<open>invertible M\<close> and cltn2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
invertible M
invertible ?A \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs ?A) = k *\<^sub>R ?A
[PROOF STEP]
obtain k where "k \<noteq> 0" and "cltn2_rep (cltn2_abs M) = k *\<^sub>R M"
[PROOF STATE]
proof (prove)
using this:
invertible M
invertible ?A \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> cltn2_rep (cltn2_abs ?A) = k *\<^sub>R ?A

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

goal (1 subgoal):
 1. cltn2_transpose (cltn2_abs M) = cltn2_abs (Finite_Cartesian_Product.transpose M)
[PROOF STEP]
from \<open>cltn2_rep (cltn2_abs M) = k *\<^sub>R M\<close>
[PROOF STATE]
proof (chain)
picking this:
cltn2_rep (cltn2_abs M) = k *\<^sub>R M
[PROOF STEP]
have "transpose (cltn2_rep (cltn2_abs M)) = k *\<^sub>R transpose M"
[PROOF STATE]
proof (prove)
using this:
cltn2_rep (cltn2_abs M) = k *\<^sub>R M

goal (1 subgoal):
 1. Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_abs M)) = k *\<^sub>R Finite_Cartesian_Product.transpose M
[PROOF STEP]
by (simp add: transpose_scalar)
[PROOF STATE]
proof (state)
this:
Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_abs M)) = k *\<^sub>R Finite_Cartesian_Product.transpose M

goal (1 subgoal):
 1. cltn2_transpose (cltn2_abs M) = cltn2_abs (Finite_Cartesian_Product.transpose M)
[PROOF STEP]
with \<open>k \<noteq> 0\<close> and \<open>invertible (transpose M)\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
invertible (Finite_Cartesian_Product.transpose M)
Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_abs M)) = k *\<^sub>R Finite_Cartesian_Product.transpose M
[PROOF STEP]
show "cltn2_transpose (cltn2_abs M) = cltn2_abs (transpose M)"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
invertible (Finite_Cartesian_Product.transpose M)
Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_abs M)) = k *\<^sub>R Finite_Cartesian_Product.transpose M

goal (1 subgoal):
 1. cltn2_transpose (cltn2_abs M) = cltn2_abs (Finite_Cartesian_Product.transpose M)
[PROOF STEP]
unfolding cltn2_transpose_def
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
invertible (Finite_Cartesian_Product.transpose M)
Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_abs M)) = k *\<^sub>R Finite_Cartesian_Product.transpose M

goal (1 subgoal):
 1. cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_abs M))) = cltn2_abs (Finite_Cartesian_Product.transpose M)
[PROOF STEP]
by (simp add: cltn2_abs_mult)
[PROOF STATE]
proof (state)
this:
cltn2_transpose (cltn2_abs M) = cltn2_abs (Finite_Cartesian_Product.transpose M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_transpose_compose:
  "cltn2_transpose (cltn2_compose A B)
  = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
from cltn2_rep_invertible
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep ?A)
[PROOF STEP]
have "invertible (cltn2_rep A)" and "invertible (cltn2_rep B)"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep ?A)

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

goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
with transpose_invertible
[PROOF STATE]
proof (chain)
picking this:
invertible ?A \<Longrightarrow> invertible (Finite_Cartesian_Product.transpose ?A)
invertible (cltn2_rep A)
invertible (cltn2_rep B)
[PROOF STEP]
have "invertible (transpose (cltn2_rep A))"
    and "invertible (transpose (cltn2_rep B))"
[PROOF STATE]
proof (prove)
using this:
invertible ?A \<Longrightarrow> invertible (Finite_Cartesian_Product.transpose ?A)
invertible (cltn2_rep A)
invertible (cltn2_rep B)

goal (1 subgoal):
 1. invertible (Finite_Cartesian_Product.transpose (cltn2_rep A)) &&& invertible (Finite_Cartesian_Product.transpose (cltn2_rep B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible (Finite_Cartesian_Product.transpose (cltn2_rep A))
invertible (Finite_Cartesian_Product.transpose (cltn2_rep B))

goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
from \<open>invertible (cltn2_rep A)\<close> and \<open>invertible (cltn2_rep B)\<close>
    and invertible_mult
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep A)
invertible (cltn2_rep B)
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)
[PROOF STEP]
have "invertible (cltn2_rep A ** cltn2_rep B)"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep A)
invertible (cltn2_rep B)
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)

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

goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
with \<open>invertible (cltn2_rep A ** cltn2_rep B)\<close> and cltn2_transpose_abs
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep A ** cltn2_rep B)
invertible ?M \<Longrightarrow> cltn2_transpose (cltn2_abs ?M) = cltn2_abs (Finite_Cartesian_Product.transpose ?M)
invertible (cltn2_rep A ** cltn2_rep B)
[PROOF STEP]
have "cltn2_transpose (cltn2_compose A B)
    = cltn2_abs (transpose (cltn2_rep A ** cltn2_rep B))"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep A ** cltn2_rep B)
invertible ?M \<Longrightarrow> cltn2_transpose (cltn2_abs ?M) = cltn2_abs (Finite_Cartesian_Product.transpose ?M)
invertible (cltn2_rep A ** cltn2_rep B)

goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A ** cltn2_rep B))
[PROOF STEP]
unfolding cltn2_compose_def
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep A ** cltn2_rep B)
invertible ?M \<Longrightarrow> cltn2_transpose (cltn2_abs ?M) = cltn2_abs (Finite_Cartesian_Product.transpose ?M)
invertible (cltn2_rep A ** cltn2_rep B)

goal (1 subgoal):
 1. cltn2_transpose (cltn2_abs (cltn2_rep A ** cltn2_rep B)) = cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A ** cltn2_rep B))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_transpose (cltn2_compose A B) = cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A ** cltn2_rep B))

goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cltn2_transpose (cltn2_compose A B) = cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A ** cltn2_rep B))

goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
have "\<dots> = cltn2_abs (transpose (cltn2_rep B) ** transpose (cltn2_rep A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A ** cltn2_rep B)) = cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep B) ** Finite_Cartesian_Product.transpose (cltn2_rep A))
[PROOF STEP]
by (simp add: matrix_transpose_mul)
[PROOF STATE]
proof (state)
this:
cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A ** cltn2_rep B)) = cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep B) ** Finite_Cartesian_Product.transpose (cltn2_rep A))

goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A ** cltn2_rep B)) = cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep B) ** Finite_Cartesian_Product.transpose (cltn2_rep A))

goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
from \<open>invertible (transpose (cltn2_rep B))\<close>
    and \<open>invertible (transpose (cltn2_rep A))\<close>
    and cltn2_compose_abs
[PROOF STATE]
proof (chain)
picking this:
invertible (Finite_Cartesian_Product.transpose (cltn2_rep B))
invertible (Finite_Cartesian_Product.transpose (cltn2_rep A))
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_compose (cltn2_abs ?M) (cltn2_abs ?N) = cltn2_abs (?M ** ?N)
[PROOF STEP]
have "\<dots> = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)"
[PROOF STATE]
proof (prove)
using this:
invertible (Finite_Cartesian_Product.transpose (cltn2_rep B))
invertible (Finite_Cartesian_Product.transpose (cltn2_rep A))
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_compose (cltn2_abs ?M) (cltn2_abs ?N) = cltn2_abs (?M ** ?N)

goal (1 subgoal):
 1. cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep B) ** Finite_Cartesian_Product.transpose (cltn2_rep A)) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
unfolding cltn2_transpose_def
[PROOF STATE]
proof (prove)
using this:
invertible (Finite_Cartesian_Product.transpose (cltn2_rep B))
invertible (Finite_Cartesian_Product.transpose (cltn2_rep A))
\<lbrakk>invertible ?M; invertible ?N\<rbrakk> \<Longrightarrow> cltn2_compose (cltn2_abs ?M) (cltn2_abs ?N) = cltn2_abs (?M ** ?N)

goal (1 subgoal):
 1. cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep B) ** Finite_Cartesian_Product.transpose (cltn2_rep A)) = cltn2_compose (cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep B))) (cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep B) ** Finite_Cartesian_Product.transpose (cltn2_rep A)) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)

goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
show "cltn2_transpose (cltn2_compose A B)
    = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)"
[PROOF STATE]
proof (prove)
using this:
cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)

goal (1 subgoal):
 1. cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cltn2_transpose (cltn2_compose A B) = cltn2_compose (cltn2_transpose B) (cltn2_transpose A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_transpose_transpose: "cltn2_transpose (cltn2_transpose A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_transpose (cltn2_transpose A) = A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cltn2_transpose (cltn2_transpose A) = A
[PROOF STEP]
from cltn2_rep_invertible
[PROOF STATE]
proof (chain)
picking this:
invertible (cltn2_rep ?A)
[PROOF STEP]
have "invertible (cltn2_rep A)"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep ?A)

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

goal (1 subgoal):
 1. cltn2_transpose (cltn2_transpose A) = A
[PROOF STEP]
with transpose_invertible
[PROOF STATE]
proof (chain)
picking this:
invertible ?A \<Longrightarrow> invertible (Finite_Cartesian_Product.transpose ?A)
invertible (cltn2_rep A)
[PROOF STEP]
have "invertible (transpose (cltn2_rep A))"
[PROOF STATE]
proof (prove)
using this:
invertible ?A \<Longrightarrow> invertible (Finite_Cartesian_Product.transpose ?A)
invertible (cltn2_rep A)

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

goal (1 subgoal):
 1. cltn2_transpose (cltn2_transpose A) = A
[PROOF STEP]
with cltn2_transpose_abs [of "transpose (cltn2_rep A)"]
[PROOF STATE]
proof (chain)
picking this:
invertible (Finite_Cartesian_Product.transpose (cltn2_rep A)) \<Longrightarrow> cltn2_transpose (cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A))) = cltn2_abs (Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (cltn2_rep A)))
invertible (Finite_Cartesian_Product.transpose (cltn2_rep A))
[PROOF STEP]
have
    "cltn2_transpose (cltn2_transpose A) = cltn2_abs (transpose (transpose (cltn2_rep A)))"
[PROOF STATE]
proof (prove)
using this:
invertible (Finite_Cartesian_Product.transpose (cltn2_rep A)) \<Longrightarrow> cltn2_transpose (cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A))) = cltn2_abs (Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (cltn2_rep A)))
invertible (Finite_Cartesian_Product.transpose (cltn2_rep A))

goal (1 subgoal):
 1. cltn2_transpose (cltn2_transpose A) = cltn2_abs (Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (cltn2_rep A)))
[PROOF STEP]
unfolding cltn2_transpose_def [of A]
[PROOF STATE]
proof (prove)
using this:
invertible (Finite_Cartesian_Product.transpose (cltn2_rep A)) \<Longrightarrow> cltn2_transpose (cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A))) = cltn2_abs (Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (cltn2_rep A)))
invertible (Finite_Cartesian_Product.transpose (cltn2_rep A))

goal (1 subgoal):
 1. cltn2_transpose (cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep A))) = cltn2_abs (Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (cltn2_rep A)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cltn2_transpose (cltn2_transpose A) = cltn2_abs (Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (cltn2_rep A)))

goal (1 subgoal):
 1. cltn2_transpose (cltn2_transpose A) = A
[PROOF STEP]
with cltn2_abs_rep and transpose_transpose [of "cltn2_rep A"]
[PROOF STATE]
proof (chain)
picking this:
cltn2_abs (cltn2_rep ?A) = ?A
Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (cltn2_rep A)) = cltn2_rep A
cltn2_transpose (cltn2_transpose A) = cltn2_abs (Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (cltn2_rep A)))
[PROOF STEP]
show "cltn2_transpose (cltn2_transpose A) = A"
[PROOF STATE]
proof (prove)
using this:
cltn2_abs (cltn2_rep ?A) = ?A
Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (cltn2_rep A)) = cltn2_rep A
cltn2_transpose (cltn2_transpose A) = cltn2_abs (Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose (cltn2_rep A)))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_transpose_id [simp]: "cltn2_transpose cltn2_id = cltn2_id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_transpose cltn2_id = cltn2_id
[PROOF STEP]
using cltn2_transpose_abs
[PROOF STATE]
proof (prove)
using this:
invertible ?M \<Longrightarrow> cltn2_transpose (cltn2_abs ?M) = cltn2_abs (Finite_Cartesian_Product.transpose ?M)

goal (1 subgoal):
 1. cltn2_transpose cltn2_id = cltn2_id
[PROOF STEP]
unfolding cltn2_id_def
[PROOF STATE]
proof (prove)
using this:
invertible ?M \<Longrightarrow> cltn2_transpose (cltn2_abs ?M) = cltn2_abs (Finite_Cartesian_Product.transpose ?M)

goal (1 subgoal):
 1. cltn2_transpose (cltn2_abs (mat 1)) = cltn2_abs (mat 1)
[PROOF STEP]
by (simp add: transpose_mat matrix_id_invertible)


[STATEMENT]
lemma apply_cltn2_line_id [simp]: "apply_cltn2_line l cltn2_id = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2_line l cltn2_id = l
[PROOF STEP]
unfolding apply_cltn2_line_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P2L (apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse cltn2_id))) = l
[PROOF STEP]
by simp


[STATEMENT]
lemma apply_cltn2_line_compose:
  "apply_cltn2_line (apply_cltn2_line l A) B
  = apply_cltn2_line l (cltn2_compose A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2_line (apply_cltn2_line l A) B = apply_cltn2_line l (cltn2_compose A B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. apply_cltn2_line (apply_cltn2_line l A) B = apply_cltn2_line l (cltn2_compose A B)
[PROOF STEP]
have "cltn2_compose
    (cltn2_transpose (cltn2_inverse A)) (cltn2_transpose (cltn2_inverse B))
    = cltn2_transpose (cltn2_inverse (cltn2_compose A B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_compose (cltn2_transpose (cltn2_inverse A)) (cltn2_transpose (cltn2_inverse B)) = cltn2_transpose (cltn2_inverse (cltn2_compose A B))
[PROOF STEP]
by (simp add: cltn2_transpose_compose cltn2_inverse_compose)
[PROOF STATE]
proof (state)
this:
cltn2_compose (cltn2_transpose (cltn2_inverse A)) (cltn2_transpose (cltn2_inverse B)) = cltn2_transpose (cltn2_inverse (cltn2_compose A B))

goal (1 subgoal):
 1. apply_cltn2_line (apply_cltn2_line l A) B = apply_cltn2_line l (cltn2_compose A B)
[PROOF STEP]
thus "apply_cltn2_line (apply_cltn2_line l A) B
    = apply_cltn2_line l (cltn2_compose A B)"
[PROOF STATE]
proof (prove)
using this:
cltn2_compose (cltn2_transpose (cltn2_inverse A)) (cltn2_transpose (cltn2_inverse B)) = cltn2_transpose (cltn2_inverse (cltn2_compose A B))

goal (1 subgoal):
 1. apply_cltn2_line (apply_cltn2_line l A) B = apply_cltn2_line l (cltn2_compose A B)
[PROOF STEP]
unfolding apply_cltn2_line_def
[PROOF STATE]
proof (prove)
using this:
cltn2_compose (cltn2_transpose (cltn2_inverse A)) (cltn2_transpose (cltn2_inverse B)) = cltn2_transpose (cltn2_inverse (cltn2_compose A B))

goal (1 subgoal):
 1. P2L (apply_cltn2 (L2P (P2L (apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A))))) (cltn2_transpose (cltn2_inverse B))) = P2L (apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse (cltn2_compose A B))))
[PROOF STEP]
by (simp add: apply_cltn2_compose)
[PROOF STATE]
proof (state)
this:
apply_cltn2_line (apply_cltn2_line l A) B = apply_cltn2_line l (cltn2_compose A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_cltn2_line_alt_def:
  "apply_cltn2_line l A
  = proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2_line l A = proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. apply_cltn2_line l A = proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)
[PROOF STEP]
have "invertible (cltn2_rep (cltn2_inverse A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible (cltn2_rep (cltn2_inverse A))
[PROOF STEP]
by (rule cltn2_rep_invertible)
[PROOF STATE]
proof (state)
this:
invertible (cltn2_rep (cltn2_inverse A))

goal (1 subgoal):
 1. apply_cltn2_line l A = proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)
[PROOF STEP]
hence "invertible (transpose (cltn2_rep (cltn2_inverse A)))"
[PROOF STATE]
proof (prove)
using this:
invertible (cltn2_rep (cltn2_inverse A))

goal (1 subgoal):
 1. invertible (Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_inverse A)))
[PROOF STEP]
by (rule transpose_invertible)
[PROOF STATE]
proof (state)
this:
invertible (Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_inverse A)))

goal (1 subgoal):
 1. apply_cltn2_line l A = proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)
[PROOF STEP]
hence
    "apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A))
    = proj2_abs (proj2_rep (L2P l) v* transpose (cltn2_rep (cltn2_inverse A)))"
[PROOF STATE]
proof (prove)
using this:
invertible (Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_inverse A)))

goal (1 subgoal):
 1. apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A)) = proj2_abs (proj2_rep (L2P l) v* Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_inverse A)))
[PROOF STEP]
unfolding cltn2_transpose_def
[PROOF STATE]
proof (prove)
using this:
invertible (Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_inverse A)))

goal (1 subgoal):
 1. apply_cltn2 (L2P l) (cltn2_abs (Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_inverse A)))) = proj2_abs (proj2_rep (L2P l) v* Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_inverse A)))
[PROOF STEP]
by (rule apply_cltn2_right_abs)
[PROOF STATE]
proof (state)
this:
apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A)) = proj2_abs (proj2_rep (L2P l) v* Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_inverse A)))

goal (1 subgoal):
 1. apply_cltn2_line l A = proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)
[PROOF STEP]
hence "apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A))
    = proj2_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A)) = proj2_abs (proj2_rep (L2P l) v* Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_inverse A)))

goal (1 subgoal):
 1. apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A)) = proj2_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)
[PROOF STEP]
unfolding proj2_line_rep_def
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A)) = proj2_abs (proj2_rep (L2P l) v* Finite_Cartesian_Product.transpose (cltn2_rep (cltn2_inverse A)))

goal (1 subgoal):
 1. apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A)) = proj2_abs (cltn2_rep (cltn2_inverse A) *v proj2_rep (L2P l))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A)) = proj2_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)

goal (1 subgoal):
 1. apply_cltn2_line l A = proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)
[PROOF STEP]
thus "apply_cltn2_line l A
    = proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A)) = proj2_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)

goal (1 subgoal):
 1. apply_cltn2_line l A = proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)
[PROOF STEP]
unfolding apply_cltn2_line_def and proj2_line_abs_def
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A)) = proj2_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)

goal (1 subgoal):
 1. P2L (apply_cltn2 (L2P l) (cltn2_transpose (cltn2_inverse A))) = P2L (proj2_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
apply_cltn2_line l A = proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_cltn2_incident:
  "proj2_incident p (apply_cltn2_line l A)
  \<longleftrightarrow> proj2_incident (apply_cltn2 p (cltn2_inverse A)) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
have "proj2_rep p v* cltn2_rep (cltn2_inverse A) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep p v* cltn2_rep (cltn2_inverse A) \<noteq> 0
[PROOF STEP]
by (rule rep_mult_rep_non_zero)
[PROOF STATE]
proof (state)
this:
proj2_rep p v* cltn2_rep (cltn2_inverse A) \<noteq> 0

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
with proj2_rep_abs2
[PROOF STATE]
proof (chain)
picking this:
?v \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_rep (proj2_abs ?v) = k *\<^sub>R ?v
proj2_rep p v* cltn2_rep (cltn2_inverse A) \<noteq> 0
[PROOF STEP]
obtain j where "j \<noteq> 0"
    and "proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep (cltn2_inverse A)))
    = j *\<^sub>R (proj2_rep p v* cltn2_rep (cltn2_inverse A))"
[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
proj2_rep p v* cltn2_rep (cltn2_inverse A) \<noteq> 0

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

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
let ?v = "cltn2_rep (cltn2_inverse A) *v proj2_line_rep l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
have "?v \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cltn2_rep (cltn2_inverse A) *v proj2_line_rep l \<noteq> 0
[PROOF STEP]
by (rule rep_mult_line_rep_non_zero)
[PROOF STATE]
proof (state)
this:
cltn2_rep (cltn2_inverse A) *v proj2_line_rep l \<noteq> 0

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
with proj2_line_rep_abs [of ?v]
[PROOF STATE]
proof (chain)
picking this:
cltn2_rep (cltn2_inverse A) *v proj2_line_rep l \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_line_rep (proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)) = k *\<^sub>R (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)
cltn2_rep (cltn2_inverse A) *v proj2_line_rep l \<noteq> 0
[PROOF STEP]
obtain k where "k \<noteq> 0"
    and "proj2_line_rep (proj2_line_abs ?v) = k *\<^sub>R ?v"
[PROOF STATE]
proof (prove)
using this:
cltn2_rep (cltn2_inverse A) *v proj2_line_rep l \<noteq> 0 \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> proj2_line_rep (proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)) = k *\<^sub>R (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)
cltn2_rep (cltn2_inverse A) *v proj2_line_rep l \<noteq> 0

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

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
hence "proj2_incident p (apply_cltn2_line l A)
    \<longleftrightarrow> proj2_rep p \<bullet> (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l) = 0"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
proj2_line_rep (proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)) = k *\<^sub>R (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = (proj2_rep p \<bullet> (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l) = 0)
[PROOF STEP]
unfolding proj2_incident_def and apply_cltn2_line_alt_def
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
proj2_line_rep (proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)) = k *\<^sub>R (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)

goal (1 subgoal):
 1. (proj2_rep p \<bullet> proj2_line_rep (proj2_line_abs (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l)) = 0) = (proj2_rep p \<bullet> (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l) = 0)
[PROOF STEP]
by (simp add: dot_scaleR_mult)
[PROOF STATE]
proof (state)
this:
proj2_incident p (apply_cltn2_line l A) = (proj2_rep p \<bullet> (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l) = 0)

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proj2_incident p (apply_cltn2_line l A) = (proj2_rep p \<bullet> (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l) = 0)

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
from dot_lmul_matrix [of "proj2_rep p" "cltn2_rep (cltn2_inverse A)"]
[PROOF STATE]
proof (chain)
picking this:
(proj2_rep p v* cltn2_rep (cltn2_inverse A)) \<bullet> ?y = proj2_rep p \<bullet> (cltn2_rep (cltn2_inverse A) *v ?y)
[PROOF STEP]
have
    "\<dots> \<longleftrightarrow> (proj2_rep p v* cltn2_rep (cltn2_inverse A)) \<bullet> proj2_line_rep l = 0"
[PROOF STATE]
proof (prove)
using this:
(proj2_rep p v* cltn2_rep (cltn2_inverse A)) \<bullet> ?y = proj2_rep p \<bullet> (cltn2_rep (cltn2_inverse A) *v ?y)

goal (1 subgoal):
 1. (proj2_rep p \<bullet> (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l) = 0) = ((proj2_rep p v* cltn2_rep (cltn2_inverse A)) \<bullet> proj2_line_rep l = 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(proj2_rep p \<bullet> (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l) = 0) = ((proj2_rep p v* cltn2_rep (cltn2_inverse A)) \<bullet> proj2_line_rep l = 0)

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(proj2_rep p \<bullet> (cltn2_rep (cltn2_inverse A) *v proj2_line_rep l) = 0) = ((proj2_rep p v* cltn2_rep (cltn2_inverse A)) \<bullet> proj2_line_rep l = 0)

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
from \<open>j \<noteq> 0\<close>
    and \<open>proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep (cltn2_inverse A)))
    = j *\<^sub>R (proj2_rep p v* cltn2_rep (cltn2_inverse A))\<close>
[PROOF STATE]
proof (chain)
picking this:
j \<noteq> 0
proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep (cltn2_inverse A))) = j *\<^sub>R (proj2_rep p v* cltn2_rep (cltn2_inverse A))
[PROOF STEP]
have "\<dots> \<longleftrightarrow> proj2_incident (apply_cltn2 p (cltn2_inverse A)) l"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep (cltn2_inverse A))) = j *\<^sub>R (proj2_rep p v* cltn2_rep (cltn2_inverse A))

goal (1 subgoal):
 1. ((proj2_rep p v* cltn2_rep (cltn2_inverse A)) \<bullet> proj2_line_rep l = 0) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
unfolding proj2_incident_def and apply_cltn2_def
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep (cltn2_inverse A))) = j *\<^sub>R (proj2_rep p v* cltn2_rep (cltn2_inverse A))

goal (1 subgoal):
 1. ((proj2_rep p v* cltn2_rep (cltn2_inverse A)) \<bullet> proj2_line_rep l = 0) = (proj2_rep (proj2_abs (proj2_rep p v* cltn2_rep (cltn2_inverse A))) \<bullet> proj2_line_rep l = 0)
[PROOF STEP]
by (simp add: dot_scaleR_mult)
[PROOF STATE]
proof (state)
this:
((proj2_rep p v* cltn2_rep (cltn2_inverse A)) \<bullet> proj2_line_rep l = 0) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l

goal (1 subgoal):
 1. proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
proj2_incident p (apply_cltn2_line l A) = proj2_incident (apply_cltn2 p (cltn2_inverse A)) l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_cltn2_preserve_incident [iff]:
  "proj2_incident (apply_cltn2 p A) (apply_cltn2_line l A)
  \<longleftrightarrow> proj2_incident p l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident (apply_cltn2 p A) (apply_cltn2_line l A) = proj2_incident p l
[PROOF STEP]
by (simp add: apply_cltn2_incident)


[STATEMENT]
lemma apply_cltn2_preserve_set_Col:
  assumes "proj2_set_Col S"
  shows "proj2_set_Col {apply_cltn2 p C | p. p \<in> S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_set_Col {apply_cltn2 p C |p. p \<in> S}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_set_Col {apply_cltn2 p C |p. p \<in> S}
[PROOF STEP]
from \<open>proj2_set_Col S\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col S
[PROOF STEP]
obtain l where "\<forall> p\<in>S. proj2_incident p l"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col S

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

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

goal (1 subgoal):
 1. proj2_set_Col {apply_cltn2 p C |p. p \<in> S}
[PROOF STEP]
hence "\<forall> q \<in> {apply_cltn2 p C | p. p \<in> S}.
    proj2_incident q (apply_cltn2_line l C)"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>S. proj2_incident p l

goal (1 subgoal):
 1. \<forall>q\<in>{apply_cltn2 p C |p. p \<in> S}. proj2_incident q (apply_cltn2_line l C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>q\<in>{apply_cltn2 p C |p. p \<in> S}. proj2_incident q (apply_cltn2_line l C)

goal (1 subgoal):
 1. proj2_set_Col {apply_cltn2 p C |p. p \<in> S}
[PROOF STEP]
thus "proj2_set_Col {apply_cltn2 p C | p. p \<in> S}"
[PROOF STATE]
proof (prove)
using this:
\<forall>q\<in>{apply_cltn2 p C |p. p \<in> S}. proj2_incident q (apply_cltn2_line l C)

goal (1 subgoal):
 1. proj2_set_Col {apply_cltn2 p C |p. p \<in> S}
[PROOF STEP]
unfolding proj2_set_Col_def
[PROOF STATE]
proof (prove)
using this:
\<forall>q\<in>{apply_cltn2 p C |p. p \<in> S}. proj2_incident q (apply_cltn2_line l C)

goal (1 subgoal):
 1. \<exists>l. \<forall>p\<in>{apply_cltn2 p C |p. p \<in> S}. proj2_incident p l
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
proj2_set_Col {apply_cltn2 p C |p. p \<in> S}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_cltn2_injective:
  assumes "apply_cltn2 p C = apply_cltn2 q C"
  shows "p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
from \<open>apply_cltn2 p C = apply_cltn2 q C\<close>
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 p C = apply_cltn2 q C
[PROOF STEP]
have "apply_cltn2 (apply_cltn2 p C) (cltn2_inverse C)
    = apply_cltn2 (apply_cltn2 q C) (cltn2_inverse C)"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 p C = apply_cltn2 q C

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

goal (1 subgoal):
 1. p = q
[PROOF STEP]
thus "p = q"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 (apply_cltn2 p C) (cltn2_inverse C) = apply_cltn2 (apply_cltn2 q C) (cltn2_inverse C)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_cltn2_line_injective:
  assumes "apply_cltn2_line l C = apply_cltn2_line m C"
  shows "l = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l = m
[PROOF STEP]
from \<open>apply_cltn2_line l C = apply_cltn2_line m C\<close>
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2_line l C = apply_cltn2_line m C
[PROOF STEP]
have "apply_cltn2_line (apply_cltn2_line l C) (cltn2_inverse C)
    = apply_cltn2_line (apply_cltn2_line m C) (cltn2_inverse C)"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2_line l C = apply_cltn2_line m C

goal (1 subgoal):
 1. apply_cltn2_line (apply_cltn2_line l C) (cltn2_inverse C) = apply_cltn2_line (apply_cltn2_line m C) (cltn2_inverse C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2_line (apply_cltn2_line l C) (cltn2_inverse C) = apply_cltn2_line (apply_cltn2_line m C) (cltn2_inverse C)

goal (1 subgoal):
 1. l = m
[PROOF STEP]
thus "l = m"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2_line (apply_cltn2_line l C) (cltn2_inverse C) = apply_cltn2_line (apply_cltn2_line m C) (cltn2_inverse C)

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. proj2_incident (apply_cltn2 p C) (apply_cltn2_line l C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_incident (apply_cltn2 p C) (apply_cltn2_line l C)

goal (1 subgoal):
 1. apply_cltn2_line l C = m
[PROOF STEP]
from \<open>proj2_incident q l\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_incident q l
[PROOF STEP]
have "proj2_incident (apply_cltn2 q C) (apply_cltn2_line l C)"
[PROOF STATE]
proof (prove)
using this:
proj2_incident q l

goal (1 subgoal):
 1. proj2_incident (apply_cltn2 q C) (apply_cltn2_line l C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_incident (apply_cltn2 q C) (apply_cltn2_line l C)

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. proj2_incident (apply_cltn2 p C) (apply_cltn2_line l C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_incident (apply_cltn2 p C) (apply_cltn2_line l C)

goal (1 subgoal):
 1. apply_cltn2 p C = q
[PROOF STEP]
from \<open>proj2_incident p m\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_incident p m
[PROOF STEP]
have "proj2_incident (apply_cltn2 p C) (apply_cltn2_line m C)"
[PROOF STATE]
proof (prove)
using this:
proj2_incident p m

goal (1 subgoal):
 1. proj2_incident (apply_cltn2 p C) (apply_cltn2_line m C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_incident (apply_cltn2 p C) (apply_cltn2_line m C)

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed