[STATEMENT]
lemma rref_col_rank:
  fixes A::"'a::{field}^'m::{mod_type}^'n::{mod_type}"
  assumes rref_A: "reduced_row_echelon_form A"
  shows "col_rank A = card {column (LEAST n. A $ i $ n \<noteq> 0) A | i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col_rank A = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
proof (unfold col_rank_def, rule vec.dim_unique[of "{column (LEAST n. A $ i $ n \<noteq> 0) A | i. row i A \<noteq> 0}"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<subseteq> col_space A
 2. col_space A \<subseteq> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
 3. vec.independent {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
 4. card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
show "{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0} \<subseteq> col_space A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<subseteq> col_space A
[PROOF STEP]
by (auto simp add: col_space_def, rule vec.span_base, unfold columns_def, auto)
[PROOF STATE]
proof (state)
this:
{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<subseteq> col_space A

goal (3 subgoals):
 1. col_space A \<subseteq> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
 2. vec.independent {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
 3. card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
show "vec.independent {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.independent {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
proof (rule vec.independent_if_scalars_zero, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
fix f i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
let ?x = "column (LEAST n. A $ i $ n \<noteq> 0) A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
have sum0: "(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0} - {?x}. f x * (x $ i)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A}. f x * x $ i) = (0::'a)
[PROOF STEP]
proof (rule sum.neutral, rule ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A} \<Longrightarrow> f x * x $ i = (0::'a)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A} \<Longrightarrow> f x * x $ i = (0::'a)
[PROOF STEP]
assume x: "x \<in> {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0} - {?x}"
[PROOF STATE]
proof (state)
this:
x \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A}

goal (1 subgoal):
 1. \<And>x. x \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A} \<Longrightarrow> f x * x $ i = (0::'a)
[PROOF STEP]
obtain j where x_eq: "x=column (LEAST n. A $ j $ n \<noteq> 0) A" and row_j_not_0: "row j A \<noteq> 0"
          and j_not_i: "j\<noteq>i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. \<lbrakk>x = column (LEAST n. A $ j $ n \<noteq> (0::'a)) A; row j A \<noteq> 0; j \<noteq> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A}

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>x = column (LEAST n. A $ j $ n \<noteq> (0::'a)) A; row j A \<noteq> 0; j \<noteq> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = column (LEAST n. A $ j $ n \<noteq> (0::'a)) A
row j A \<noteq> 0
j \<noteq> i

goal (1 subgoal):
 1. \<And>x. x \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A} \<Longrightarrow> f x * x $ i = (0::'a)
[PROOF STEP]
have "x$i=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ i = (0::'a)
[PROOF STEP]
unfolding x_eq column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. A $ i $ (LEAST n. A $ j $ n \<noteq> (0::'a))) $ i = (0::'a)
[PROOF STEP]
by (auto, metis is_zero_row_eq_row_zero j_not_i row_j_not_0 rref_A rref_condition4_explicit)
[PROOF STATE]
proof (state)
this:
x $ i = (0::'a)

goal (1 subgoal):
 1. \<And>x. x \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A} \<Longrightarrow> f x * x $ i = (0::'a)
[PROOF STEP]
thus "f x * x $ i = 0"
[PROOF STATE]
proof (prove)
using this:
x $ i = (0::'a)

goal (1 subgoal):
 1. f x * x $ i = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f x * x $ i = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A}. f x * x $ i) = (0::'a)

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
assume eq_0: "(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}. f x *s x) = 0"
        and i: "row i A \<noteq> 0"
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0
row i A \<noteq> 0

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
have xi_1: "(?x $ i) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i = (1::'a)
[PROOF STEP]
unfolding column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia. A $ ia $ (LEAST n. A $ i $ n \<noteq> (0::'a))) $ i = (1::'a)
[PROOF STEP]
by (auto, metis i is_zero_row_eq_row_zero rref_A rref_condition2_explicit)
[PROOF STATE]
proof (state)
this:
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i = (1::'a)

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
have "0 = (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}. f x *s x) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) = (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) $ i
[PROOF STEP]
using eq_0
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0

goal (1 subgoal):
 1. (0::'a) = (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) = (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) $ i

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) = (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) $ i

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
have "... = (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}. f x * (x $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) $ i = (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x * x $ i)
[PROOF STEP]
unfolding sum_component vector_smult_component
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x * x $ i) = (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x * x $ i)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) $ i = (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x * x $ i)

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) $ i = (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x * x $ i)

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
have "... = f ?x * (?x $ i)
      + (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0} - {?x}. f x * (x $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x * x $ i) = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i + (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A}. f x * x $ i)
[PROOF STEP]
by (rule sum.remove, auto, rule exI[of _ i], simp add: i)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x * x $ i) = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i + (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A}. f x * x $ i)

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x * x $ i) = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i + (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A}. f x * x $ i)

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
have "... = f ?x * (?x $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i + (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A}. f x * x $ i) = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i
[PROOF STEP]
unfolding sum0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i + (0::'a) = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i + (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A}. f x * x $ i) = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i + (\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A}. f x * x $ i) = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
have "... = f (column (LEAST n. A $ i $ n \<noteq> 0) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A)
[PROOF STEP]
unfolding xi_1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * (1::'a) = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) * column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A)

goal (1 subgoal):
 1. \<And>f i. \<lbrakk>(\<Sum>x\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. f x *s x) = 0; row i A \<noteq> 0\<rbrakk> \<Longrightarrow> f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'a) = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A)
[PROOF STEP]
show "f (column (LEAST n. A $ i $ n \<noteq> 0) A) = 0"
[PROOF STATE]
proof (prove)
using this:
(0::'a) = f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A)

goal (1 subgoal):
 1. f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (column (LEAST n. A $ i $ n \<noteq> (0::'a)) A) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vec.independent {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal (2 subgoals):
 1. col_space A \<subseteq> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
 2. card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
show "col_space A \<subseteq> vec.span {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col_space A \<subseteq> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
unfolding col_space_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.span (columns A) \<subseteq> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
proof (rule vec.span_mono[of "(columns A)"
        "vec.span {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}", unfolded vec.span_span], auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> columns A \<Longrightarrow> x \<in> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> columns A \<Longrightarrow> x \<in> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
assume x: "x \<in> columns A"
[PROOF STATE]
proof (state)
this:
x \<in> columns A

goal (1 subgoal):
 1. \<And>x. x \<in> columns A \<Longrightarrow> x \<in> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
have f: "finite {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. \<And>x. x \<in> columns A \<Longrightarrow> x \<in> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
let ?f="\<lambda>v. x $ (THE i. v $ i \<noteq> 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> columns A \<Longrightarrow> x \<in> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
show "x \<in> vec.span {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
unfolding vec.span_finite[OF f] image_iff bex_UNIV
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xa. x = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. xa v *s v)
[PROOF STEP]
proof (rule exI[of _ ?f], subst (1) vec_eq_iff, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
show "x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> 0) *s v) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
proof (cases "\<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
 2. \<nexists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a)

goal (2 subgoals):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
 2. \<nexists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have xi_0: "x $ i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ i = (0::'a)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x $ i \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
assume xi_not_0: "x $ i \<noteq> 0"
[PROOF STATE]
proof (state)
this:
x $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. x $ i \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
hence row_iA_not_zero: "row i A \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. row i A \<noteq> 0
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x $ i \<noteq> (0::'a)
x \<in> columns A

goal (1 subgoal):
 1. row i A \<noteq> 0
[PROOF STEP]
unfolding columns_def column_def row_def
[PROOF STATE]
proof (prove)
using this:
x $ i \<noteq> (0::'a)
x \<in> {\<chi>ia. A $ ia $ i |i. i \<in> UNIV}

goal (1 subgoal):
 1. vec_lambda (($) (A $ i)) \<noteq> 0
[PROOF STEP]
by (vector, metis vec_lambda_unique)
[PROOF STATE]
proof (state)
this:
row i A \<noteq> 0

goal (1 subgoal):
 1. x $ i \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
let ?v="column (LEAST n. A $ i $ n \<noteq> 0) A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x $ i \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
have "?v \<in> {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
using row_iA_not_zero
[PROOF STATE]
proof (prove)
using this:
row i A \<noteq> 0

goal (1 subgoal):
 1. column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. x $ i \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. x $ i \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
have "?v $ i = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i = (1::'a)
[PROOF STEP]
unfolding column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia. A $ ia $ (LEAST n. A $ i $ n \<noteq> (0::'a))) $ i = (1::'a)
[PROOF STEP]
by (auto, metis is_zero_row_eq_row_zero row_iA_not_zero rref_A rref_condition2)
[PROOF STATE]
proof (state)
this:
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i = (1::'a)

goal (1 subgoal):
 1. x $ i \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i = (1::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i = (1::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A $ i = (1::'a)
\<nexists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x $ i = (0::'a)

goal (2 subgoals):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
 2. \<nexists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
unfolding xi_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
proof (unfold sum_component vector_smult_component, rule sum.neutral[symmetric], rule ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<Longrightarrow> x $ (THE i. xa $ i \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
fix xa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<Longrightarrow> x $ (THE i. xa $ i \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
assume xa: "xa \<in> {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (state)
this:
xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<Longrightarrow> x $ (THE i. xa $ i \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
have "xa $ i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa $ i = (0::'a)
[PROOF STEP]
using False xa
[PROOF STATE]
proof (prove)
using this:
\<nexists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a)
xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. xa $ i = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xa $ i = (0::'a)

goal (1 subgoal):
 1. \<And>xa. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<Longrightarrow> x $ (THE i. xa $ i \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
thus "x $ (THE i. xa $ i \<noteq> 0) * xa $ i = 0"
[PROOF STATE]
proof (prove)
using this:
xa $ i = (0::'a)

goal (1 subgoal):
 1. x $ (THE i. xa $ i \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x $ (THE i. xa $ i \<noteq> (0::'a)) * xa $ i = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
obtain v where v: "v \<in> {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}" and vi: "v $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}; v $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
\<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}; v $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
obtain b where b: "v = column (LEAST n. A $ b $ n \<noteq> 0) A" and row_b: "row b A \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b. \<lbrakk>v = column (LEAST n. A $ b $ n \<noteq> (0::'a)) A; row b A \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>v = column (LEAST n. A $ b $ n \<noteq> (0::'a)) A; row b A \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v = column (LEAST n. A $ b $ n \<noteq> (0::'a)) A
row b A \<noteq> 0

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have vb: "v $ b \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v $ b \<noteq> (0::'a)
[PROOF STEP]
unfolding b column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. A $ i $ (LEAST n. A $ b $ n \<noteq> (0::'a))) $ b \<noteq> (0::'a)
[PROOF STEP]
by (auto, metis is_zero_row_eq_row_zero row_b rref_A rref_condition2 zero_neq_one)
[PROOF STATE]
proof (state)
this:
v $ b \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have b_eq_i: "b = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = i
[PROOF STEP]
by (rule column_leading_coefficient_component_eq[OF rref_A v vb vi])
[PROOF STATE]
proof (state)
this:
b = i

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have the_vi: "(THE a. v $ a \<noteq> 0) = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE a. v $ a \<noteq> (0::'a)) = i
[PROOF STEP]
proof (rule the_equality, rule vi)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. v $ a \<noteq> (0::'a) \<Longrightarrow> a = i
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. v $ a \<noteq> (0::'a) \<Longrightarrow> a = i
[PROOF STEP]
assume va: "v $ a \<noteq> 0"
[PROOF STATE]
proof (state)
this:
v $ a \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>a. v $ a \<noteq> (0::'a) \<Longrightarrow> a = i
[PROOF STEP]
show "a=i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = i
[PROOF STEP]
by (rule column_leading_coefficient_component_eq[OF rref_A v va vi])
[PROOF STATE]
proof (state)
this:
a = i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(THE a. v $ a \<noteq> (0::'a)) = i

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have vi_1: "v $ i = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v $ i = (1::'a)
[PROOF STEP]
by (rule column_leading_coefficient_component_1[OF rref_A v vi])
[PROOF STATE]
proof (state)
this:
v $ i = (1::'a)

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have sum0: "(\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0} - {v}. x $ (THE a. v $ a \<noteq> 0) * (v $ i)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i) = (0::'a)
[PROOF STEP]
proof (rule sum.neutral, rule ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v} \<Longrightarrow> x $ (THE a. xa $ a \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
fix xa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v} \<Longrightarrow> x $ (THE a. xa $ a \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
assume xa: "xa \<in> {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0} - {v}"
[PROOF STATE]
proof (state)
this:
xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v} \<Longrightarrow> x $ (THE a. xa $ a \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
obtain y where y: "xa = column (LEAST n. A $ y $ n \<noteq> 0) A" and row_b: "row y A \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>xa = column (LEAST n. A $ y $ n \<noteq> (0::'a)) A; row y A \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using xa
[PROOF STATE]
proof (prove)
using this:
xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>xa = column (LEAST n. A $ y $ n \<noteq> (0::'a)) A; row y A \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xa = column (LEAST n. A $ y $ n \<noteq> (0::'a)) A
row y A \<noteq> 0

goal (1 subgoal):
 1. \<And>xa. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v} \<Longrightarrow> x $ (THE a. xa $ a \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
have xa_in_V: "xa \<in> {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
using xa
[PROOF STATE]
proof (prove)
using this:
xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}

goal (1 subgoal):
 1. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v} \<Longrightarrow> x $ (THE a. xa $ a \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
have "xa $ i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa $ i = (0::'a)
[PROOF STEP]
proof (rule column_leading_coefficient_component_0[OF rref_A xa_in_V])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xa $ ?x \<noteq> (0::'a)
 2. ?x \<noteq> i
[PROOF STEP]
show "xa $ y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa $ y \<noteq> (0::'a)
[PROOF STEP]
unfolding y column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i. A $ i $ (LEAST n. A $ y $ n \<noteq> (0::'a))) $ y \<noteq> (0::'a)
[PROOF STEP]
by (auto, metis (lifting, full_types) LeastI2_ex is_zero_row_def' is_zero_row_eq_row_zero row_b)
[PROOF STATE]
proof (state)
this:
xa $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. y \<noteq> i
[PROOF STEP]
have "y \<noteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<noteq> b
[PROOF STEP]
by (metis (mono_tags) Diff_iff b mem_Collect_eq singleton_conv2 xa y)
[PROOF STATE]
proof (state)
this:
y \<noteq> b

goal (1 subgoal):
 1. y \<noteq> i
[PROOF STEP]
thus "y \<noteq> i"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> b

goal (1 subgoal):
 1. y \<noteq> i
[PROOF STEP]
unfolding b_eq_i[symmetric]
[PROOF STATE]
proof (prove)
using this:
y \<noteq> b

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xa $ i = (0::'a)

goal (1 subgoal):
 1. \<And>xa. xa \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v} \<Longrightarrow> x $ (THE a. xa $ a \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
thus "x $ (THE a. xa $ a \<noteq> 0) * xa $ i = 0"
[PROOF STATE]
proof (prove)
using this:
xa $ i = (0::'a)

goal (1 subgoal):
 1. x $ (THE a. xa $ a \<noteq> (0::'a)) * xa $ i = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x $ (THE a. xa $ a \<noteq> (0::'a)) * xa $ i = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i) = (0::'a)

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have "(\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> 0) *s v) $ i =
          (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> 0) * (v $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) *s v) $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i)
[PROOF STEP]
unfolding sum_component vector_smult_component
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>xa\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. xa $ a \<noteq> (0::'a)) * xa $ i) = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) *s v) $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i)

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) *s v) $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i)

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have "... = x $ (THE a. v $ a \<noteq> 0) * (v $ i)
          + (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0} - {v}. x $ (THE a. v $ a \<noteq> 0) * (v $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i) = x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i + (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i)
[PROOF STEP]
by (simp add: sum.remove[OF _ v])
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i) = x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i + (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i)

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i) = x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i + (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i)

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have "... = x $ (THE a. v $ a \<noteq> 0) * (v $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i + (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i) = x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i
[PROOF STEP]
unfolding sum0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i + (0::'a) = x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i + (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i) = x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i + (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} - {v}. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i) = x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have "... = x $ (THE a. v $ a \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i = x $ (THE a. v $ a \<noteq> (0::'a))
[PROOF STEP]
unfolding vi_1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ (THE a. v $ a \<noteq> (0::'a)) * (1::'a) = x $ (THE a. v $ a \<noteq> (0::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i = x $ (THE a. v $ a \<noteq> (0::'a))

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x $ (THE a. v $ a \<noteq> (0::'a)) * v $ i = x $ (THE a. v $ a \<noteq> (0::'a))

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
have "... = x $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ (THE a. v $ a \<noteq> (0::'a)) = x $ i
[PROOF STEP]
unfolding the_vi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x $ i = x $ i
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x $ (THE a. v $ a \<noteq> (0::'a)) = x $ i

goal (1 subgoal):
 1. \<exists>v. v \<in> {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} \<and> v $ i \<noteq> (0::'a) \<Longrightarrow> x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) *s v) $ i = x $ i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE a. v $ a \<noteq> (0::'a)) *s v) $ i = x $ i

goal (1 subgoal):
 1. x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x $ i = (\<Sum>v\<in>{column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}. x $ (THE i. v $ i \<noteq> (0::'a)) *s v) $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
col_space A \<subseteq> vec.span {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
qed (simp)


[STATEMENT]
lemma rref_row_rank:
  fixes A::"'a::{field}^'m::{mod_type}^'n::{finite,one,plus,ord}"
  assumes rref_A: "reduced_row_echelon_form A"
  shows "row_rank A = card {column (LEAST n. A $ i $ n \<noteq> 0) A | i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_rank A = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row_rank A = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
let ?f="\<lambda>x. column ((LEAST n. x $ n \<noteq> 0)) A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row_rank A = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_rank A = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
unfolding rref_rank[OF rref_A, unfolded rank_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {row i A |i. row i A \<noteq> 0} = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
proof (rule bij_betw_same_card[of ?f], unfold bij_betw_def, auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inj_on (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) {row i A |i. row i A \<noteq> 0}
 2. \<And>i. row i A \<noteq> 0 \<Longrightarrow> \<exists>ia. column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. A $ ia $ n \<noteq> (0::'a)) A \<and> row ia A \<noteq> 0
 3. \<And>i. row i A \<noteq> 0 \<Longrightarrow> column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
show "inj_on (\<lambda>x. column (LEAST n. x $ n \<noteq> 0) A) {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{row i A |i. row i A \<noteq> 0}. \<forall>y\<in>{row i A |i. row i A \<noteq> 0}. column (LEAST n. x $ n \<noteq> (0::'a)) A = column (LEAST n. y $ n \<noteq> (0::'a)) A \<longrightarrow> x = y
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>row i A \<noteq> 0; row ia A \<noteq> 0; column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. row ia A $ n \<noteq> (0::'a)) A\<rbrakk> \<Longrightarrow> row i A = row ia A
[PROOF STEP]
fix i ia
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>row i A \<noteq> 0; row ia A \<noteq> 0; column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. row ia A $ n \<noteq> (0::'a)) A\<rbrakk> \<Longrightarrow> row i A = row ia A
[PROOF STEP]
assume i: "row i A \<noteq> 0" and ia: "row ia A \<noteq> 0"
         and c_eq: "column (LEAST n. row i A $ n \<noteq> 0) A = column (LEAST n. row ia A $ n \<noteq> 0) A"
[PROOF STATE]
proof (state)
this:
row i A \<noteq> 0
row ia A \<noteq> 0
column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. row ia A $ n \<noteq> (0::'a)) A

goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>row i A \<noteq> 0; row ia A \<noteq> 0; column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. row ia A $ n \<noteq> (0::'a)) A\<rbrakk> \<Longrightarrow> row i A = row ia A
[PROOF STEP]
show "row i A = row ia A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row i A = row ia A
[PROOF STEP]
using c_eq
[PROOF STATE]
proof (prove)
using this:
column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. row ia A $ n \<noteq> (0::'a)) A

goal (1 subgoal):
 1. row i A = row ia A
[PROOF STEP]
unfolding column_def
[PROOF STATE]
proof (prove)
using this:
(\<chi>ia. A $ ia $ (LEAST n. row i A $ n \<noteq> (0::'a))) = (\<chi>i. A $ i $ (LEAST n. row ia A $ n \<noteq> (0::'a)))

goal (1 subgoal):
 1. row i A = row ia A
[PROOF STEP]
unfolding row_def vec_nth_inverse
[PROOF STATE]
proof (prove)
using this:
(\<chi>ia. A $ ia $ (LEAST n. A $ i $ n \<noteq> (0::'a))) = (\<chi>i. A $ i $ (LEAST n. A $ ia $ n \<noteq> (0::'a)))

goal (1 subgoal):
 1. A $ i = A $ ia
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<chi>ia. A $ ia $ (LEAST n. A $ i $ n \<noteq> (0::'a))) = (\<chi>i. A $ i $ (LEAST n. A $ ia $ n \<noteq> (0::'a))) \<Longrightarrow> A $ i = A $ ia
[PROOF STEP]
have "transpose_row A (LEAST R. A $ ia $ R \<noteq> 0) = transpose_row A (LEAST R. A $ i $ R \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transpose_row A (LEAST R. A $ ia $ R \<noteq> (0::'a)) = transpose_row A (LEAST R. A $ i $ R \<noteq> (0::'a))
[PROOF STEP]
by (metis c_eq column_def row_def transpose_row_def vec_nth_inverse)
[PROOF STATE]
proof (state)
this:
transpose_row A (LEAST R. A $ ia $ R \<noteq> (0::'a)) = transpose_row A (LEAST R. A $ i $ R \<noteq> (0::'a))

goal (1 subgoal):
 1. (\<chi>ia. A $ ia $ (LEAST n. A $ i $ n \<noteq> (0::'a))) = (\<chi>i. A $ i $ (LEAST n. A $ ia $ n \<noteq> (0::'a))) \<Longrightarrow> A $ i = A $ ia
[PROOF STEP]
hence f1: "\<And>x\<^sub>1. A $ x\<^sub>1 $ (LEAST R. A $ ia $ R \<noteq> 0) = A $ x\<^sub>1 $ (LEAST R. A $ i $ R \<noteq> 0)"
[PROOF STATE]
proof (prove)
using this:
transpose_row A (LEAST R. A $ ia $ R \<noteq> (0::'a)) = transpose_row A (LEAST R. A $ i $ R \<noteq> (0::'a))

goal (1 subgoal):
 1. \<And>x\<^sub>1. A $ x\<^sub>1 $ (LEAST R. A $ ia $ R \<noteq> (0::'a)) = A $ x\<^sub>1 $ (LEAST R. A $ i $ R \<noteq> (0::'a))
[PROOF STEP]
by (metis (no_types) transpose_row_def vec_lambda_beta)
[PROOF STATE]
proof (state)
this:
A $ ?x\<^sub>11 $ (LEAST R. A $ ia $ R \<noteq> (0::'a)) = A $ ?x\<^sub>11 $ (LEAST R. A $ i $ R \<noteq> (0::'a))

goal (1 subgoal):
 1. (\<chi>ia. A $ ia $ (LEAST n. A $ i $ n \<noteq> (0::'a))) = (\<chi>i. A $ i $ (LEAST n. A $ ia $ n \<noteq> (0::'a))) \<Longrightarrow> A $ i = A $ ia
[PROOF STEP]
have f2: "is_zero_row ia A = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row ia A = False
[PROOF STEP]
using ia is_zero_row_eq_row_zero
[PROOF STATE]
proof (prove)
using this:
row ia A \<noteq> 0
is_zero_row ?a ?A = (row ?a ?A = 0)

goal (1 subgoal):
 1. is_zero_row ia A = False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_zero_row ia A = False

goal (1 subgoal):
 1. (\<chi>ia. A $ ia $ (LEAST n. A $ i $ n \<noteq> (0::'a))) = (\<chi>i. A $ i $ (LEAST n. A $ ia $ n \<noteq> (0::'a))) \<Longrightarrow> A $ i = A $ ia
[PROOF STEP]
have f3: "\<not> is_zero_row i A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row i A
[PROOF STEP]
using i is_zero_row_eq_row_zero
[PROOF STATE]
proof (prove)
using this:
row i A \<noteq> 0
is_zero_row ?a ?A = (row ?a ?A = 0)

goal (1 subgoal):
 1. \<not> is_zero_row i A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row i A

goal (1 subgoal):
 1. (\<chi>ia. A $ ia $ (LEAST n. A $ i $ n \<noteq> (0::'a))) = (\<chi>i. A $ i $ (LEAST n. A $ ia $ n \<noteq> (0::'a))) \<Longrightarrow> A $ i = A $ ia
[PROOF STEP]
have "A $ ia $ (LEAST R. A $ i $ R \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ ia $ (LEAST R. A $ i $ R \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using f1 f2 rref_A rref_condition2
[PROOF STATE]
proof (prove)
using this:
A $ ?x\<^sub>11 $ (LEAST R. A $ ia $ R \<noteq> (0::'a)) = A $ ?x\<^sub>11 $ (LEAST R. A $ i $ R \<noteq> (0::'a))
is_zero_row ia A = False
reduced_row_echelon_form A
reduced_row_echelon_form ?A \<Longrightarrow> \<forall>i. \<not> is_zero_row i ?A \<longrightarrow> ?A $ i $ (LEAST k. ?A $ i $ k \<noteq> (0::?'a)) = (1::?'a)

goal (1 subgoal):
 1. A $ ia $ (LEAST R. A $ i $ R \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A $ ia $ (LEAST R. A $ i $ R \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. (\<chi>ia. A $ ia $ (LEAST n. A $ i $ n \<noteq> (0::'a))) = (\<chi>i. A $ i $ (LEAST n. A $ ia $ n \<noteq> (0::'a))) \<Longrightarrow> A $ i = A $ ia
[PROOF STEP]
thus "A $ i = A $ ia"
[PROOF STATE]
proof (prove)
using this:
A $ ia $ (LEAST R. A $ i $ R \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. A $ i = A $ ia
[PROOF STEP]
using f3 rref_A rref_condition4_explicit
[PROOF STATE]
proof (prove)
using this:
A $ ia $ (LEAST R. A $ i $ R \<noteq> (0::'a)) = (1::'a)
\<not> is_zero_row i A
reduced_row_echelon_form A
\<lbrakk>reduced_row_echelon_form ?A; \<not> is_zero_row ?i ?A; ?i \<noteq> ?j\<rbrakk> \<Longrightarrow> ?A $ ?j $ (LEAST n. ?A $ ?i $ n \<noteq> (0::?'a)) = (0::?'a)

goal (1 subgoal):
 1. A $ i = A $ ia
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A $ i = A $ ia

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row i A = row ia A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) {row i A |i. row i A \<noteq> 0}

goal (2 subgoals):
 1. \<And>i. row i A \<noteq> 0 \<Longrightarrow> \<exists>ia. column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. A $ ia $ n \<noteq> (0::'a)) A \<and> row ia A \<noteq> 0
 2. \<And>i. row i A \<noteq> 0 \<Longrightarrow> column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. row i A \<noteq> 0 \<Longrightarrow> \<exists>ia. column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. A $ ia $ n \<noteq> (0::'a)) A \<and> row ia A \<noteq> 0
 2. \<And>i. row i A \<noteq> 0 \<Longrightarrow> column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. row i A \<noteq> 0 \<Longrightarrow> \<exists>ia. column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. A $ ia $ n \<noteq> (0::'a)) A \<and> row ia A \<noteq> 0
 2. \<And>i. row i A \<noteq> 0 \<Longrightarrow> column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
assume i: "row i A \<noteq> 0"
[PROOF STATE]
proof (state)
this:
row i A \<noteq> 0

goal (2 subgoals):
 1. \<And>i. row i A \<noteq> 0 \<Longrightarrow> \<exists>ia. column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. A $ ia $ n \<noteq> (0::'a)) A \<and> row ia A \<noteq> 0
 2. \<And>i. row i A \<noteq> 0 \<Longrightarrow> column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
show "\<exists>ia. column (LEAST n. row i A $ n \<noteq> 0) A = column (LEAST n. A $ ia $ n \<noteq> 0) A \<and> row ia A \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ia. column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. A $ ia $ n \<noteq> (0::'a)) A \<and> row ia A \<noteq> 0
[PROOF STEP]
by (rule exI[of _ "i"], simp add: row_def vec_lambda_eta)
         (metis i is_zero_row_def' is_zero_row_eq_row_zero zero_index)
[PROOF STATE]
proof (state)
this:
\<exists>ia. column (LEAST n. row i A $ n \<noteq> (0::'a)) A = column (LEAST n. A $ ia $ n \<noteq> (0::'a)) A \<and> row ia A \<noteq> 0

goal (1 subgoal):
 1. \<And>i. row i A \<noteq> 0 \<Longrightarrow> column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. row i A \<noteq> 0 \<Longrightarrow> column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. row i A \<noteq> 0 \<Longrightarrow> column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
assume i: "row i A \<noteq> 0"
[PROOF STATE]
proof (state)
this:
row i A \<noteq> 0

goal (1 subgoal):
 1. \<And>i. row i A \<noteq> 0 \<Longrightarrow> column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
show "column (LEAST n. A $ i $ n \<noteq> 0) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> 0) A) ` {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
unfolding column_def row_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia. A $ ia $ (LEAST n. A $ i $ n \<noteq> (0::'a))) \<in> {y. \<exists>x\<in>{vec_lambda (($) (A $ i)) |i. vec_lambda (($) (A $ i)) \<noteq> 0}. y = (\<chi>i. A $ i $ (LEAST n. x $ n \<noteq> (0::'a)))}
[PROOF STEP]
by (auto, metis i row_def vec_lambda_eta)
[PROOF STATE]
proof (state)
this:
column (LEAST n. A $ i $ n \<noteq> (0::'a)) A \<in> (\<lambda>x. column (LEAST n. x $ n \<noteq> (0::'a)) A) ` {row i A |i. row i A \<noteq> 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_rank A = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_rank_eq_col_rank_rref:
  fixes A::"'a::{field}^'m::{mod_type}^'n::{mod_type}"
assumes r: "reduced_row_echelon_form A"
shows "row_rank A = col_rank A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_rank A = col_rank A
[PROOF STEP]
unfolding rref_row_rank[OF r] rref_col_rank[OF r]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0} = card {column (LEAST n. A $ i $ n \<noteq> (0::'a)) A |i. row i A \<noteq> 0}
[PROOF STEP]
..


[STATEMENT]
lemma row_rank_eq_col_rank:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "row_rank A = col_rank A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_rank A = col_rank A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row_rank A = col_rank A
[PROOF STEP]
obtain P where inv_P: "invertible P" and G_PA: "(Gauss_Jordan A) = P**A"
  and rref_G: "reduced_row_echelon_form (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrakk>invertible P; Gauss_Jordan A = P ** A; reduced_row_echelon_form (Gauss_Jordan A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using invertible_Gauss_Jordan rref_Gauss_Jordan
[PROOF STATE]
proof (prove)
using this:
\<exists>P. invertible P \<and> Gauss_Jordan ?A = P ** ?A
reduced_row_echelon_form (Gauss_Jordan ?A)

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>invertible P; Gauss_Jordan A = P ** A; reduced_row_echelon_form (Gauss_Jordan A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invertible P
Gauss_Jordan A = P ** A
reduced_row_echelon_form (Gauss_Jordan A)

goal (1 subgoal):
 1. row_rank A = col_rank A
[PROOF STEP]
have "row_rank A = row_rank (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_rank A = row_rank (Gauss_Jordan A)
[PROOF STEP]
by (metis row_space_is_preserved invertible_Gauss_Jordan row_rank_def)
[PROOF STATE]
proof (state)
this:
row_rank A = row_rank (Gauss_Jordan A)

goal (1 subgoal):
 1. row_rank A = col_rank A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
row_rank A = row_rank (Gauss_Jordan A)

goal (1 subgoal):
 1. row_rank A = col_rank A
[PROOF STEP]
have "col_rank A = col_rank (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col_rank A = col_rank (Gauss_Jordan A)
[PROOF STEP]
by (metis invertible_Gauss_Jordan crk_is_preserved)
[PROOF STATE]
proof (state)
this:
col_rank A = col_rank (Gauss_Jordan A)

goal (1 subgoal):
 1. row_rank A = col_rank A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
col_rank A = col_rank (Gauss_Jordan A)

goal (1 subgoal):
 1. row_rank A = col_rank A
[PROOF STEP]
have "col_rank (Gauss_Jordan A) = row_rank (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col_rank (Gauss_Jordan A) = row_rank (Gauss_Jordan A)
[PROOF STEP]
using row_rank_eq_col_rank_rref[OF rref_G]
[PROOF STATE]
proof (prove)
using this:
row_rank (Gauss_Jordan A) = col_rank (Gauss_Jordan A)

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

goal (1 subgoal):
 1. row_rank A = col_rank A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
row_rank A = row_rank (Gauss_Jordan A)
col_rank A = col_rank (Gauss_Jordan A)
col_rank (Gauss_Jordan A) = row_rank (Gauss_Jordan A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
row_rank A = row_rank (Gauss_Jordan A)
col_rank A = col_rank (Gauss_Jordan A)
col_rank (Gauss_Jordan A) = row_rank (Gauss_Jordan A)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem rank_col_rank:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "rank A = col_rank A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = col_rank A
[PROOF STEP]
unfolding rank_def row_rank_eq_col_rank
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col_rank A = col_rank A
[PROOF STEP]
..


[STATEMENT]
theorem rank_eq_dim_image:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "rank A = vec.dim (range (\<lambda>x. A *v x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = vec.dim (range ((*v) A))
[PROOF STEP]
unfolding rank_col_rank col_rank_def col_space_eq'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (range ((*v) A)) = vec.dim (range ((*v) A))
[PROOF STEP]
..


[STATEMENT]
theorem rank_eq_dim_col_space:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "rank A = vec.dim (col_space A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = vec.dim (col_space A)
[PROOF STEP]
using rank_col_rank
[PROOF STATE]
proof (prove)
using this:
rank ?A = col_rank ?A

goal (1 subgoal):
 1. rank A = vec.dim (col_space A)
[PROOF STEP]
unfolding col_rank_def
[PROOF STATE]
proof (prove)
using this:
rank ?A = vec.dim (col_space ?A)

goal (1 subgoal):
 1. rank A = vec.dim (col_space A)
[PROOF STEP]
.


[STATEMENT]
lemma rank_transpose:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows  "rank (transpose A) = rank A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank (Finite_Cartesian_Product.transpose A) = rank A
[PROOF STEP]
by (metis rank_def rank_eq_dim_col_space row_rank_def row_space_eq_col_space_transpose)


[STATEMENT]
lemma rank_le_nrows:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "rank A \<le> nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A \<le> nrows A
[PROOF STEP]
unfolding rank_eq_dim_col_space nrows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (col_space A) \<le> CARD('m)
[PROOF STEP]
by (metis top_greatest vec.dim_subset vec_dim_card)


[STATEMENT]
lemma rank_le_ncols:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "rank A \<le> ncols A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A \<le> ncols A
[PROOF STEP]
unfolding rank_def row_rank_def ncols_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (row_space A) \<le> CARD('n)
[PROOF STEP]
by (metis top_greatest vec.dim_subset vec_dim_card)


[STATEMENT]
lemma rank_Gauss_Jordan:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "rank A = rank (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = rank (Gauss_Jordan A)
[PROOF STEP]
by (metis Gauss_Jordan_def invertible_Gauss_Jordan_up_to_k
      row_rank_eq_col_rank rank_def crk_is_preserved)


[STATEMENT]
lemma A_0_imp_Gauss_Jordan_0:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  assumes "A=0"
  shows "Gauss_Jordan A = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gauss_Jordan A = 0
[PROOF STEP]
obtain P where PA: "Gauss_Jordan A = P ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. Gauss_Jordan A = P ** A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using invertible_Gauss_Jordan
[PROOF STATE]
proof (prove)
using this:
\<exists>P. invertible P \<and> Gauss_Jordan ?A = P ** ?A

goal (1 subgoal):
 1. (\<And>P. Gauss_Jordan A = P ** A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A = P ** A

goal (1 subgoal):
 1. Gauss_Jordan A = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A = P ** A

goal (1 subgoal):
 1. Gauss_Jordan A = 0
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ** A = 0
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ** 0 = 0
[PROOF STEP]
by (metis eq_add_iff matrix_add_ldistrib)
[PROOF STATE]
proof (state)
this:
P ** A = 0

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

goal (1 subgoal):
 1. Gauss_Jordan A = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_0: "rank 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank 0 = 0
[PROOF STEP]
unfolding rank_def row_rank_def row_space_def rows_def row_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (vec.span {vec_lambda (($) (0 $ i)) |i. i \<in> UNIV}) = 0
[PROOF STEP]
by (simp add: vec.dim_span vec.dim_zero_eq' vec_nth_inverse)


[STATEMENT]
lemma rank_greater_zero:
  assumes "A \<noteq> 0"
  shows "rank A > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < rank A
[PROOF STEP]
proof (rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank A = 0 \<Longrightarrow> False
[PROOF STEP]
assume "rank A = 0"
[PROOF STATE]
proof (state)
this:
rank A = 0

goal (1 subgoal):
 1. rank A = 0 \<Longrightarrow> False
[PROOF STEP]
hence "row_space A = {} \<or> row_space A = {0}"
[PROOF STATE]
proof (prove)
using this:
rank A = 0

goal (1 subgoal):
 1. row_space A = {} \<or> row_space A = {0}
[PROOF STEP]
unfolding rank_def row_rank_def
[PROOF STATE]
proof (prove)
using this:
vec.dim (row_space A) = 0

goal (1 subgoal):
 1. row_space A = {} \<or> row_space A = {0}
[PROOF STEP]
using vec.dim_zero_eq
[PROOF STATE]
proof (prove)
using this:
vec.dim (row_space A) = 0
vec.dim ?A = 0 \<Longrightarrow> ?A = {} \<or> ?A = {0}

goal (1 subgoal):
 1. row_space A = {} \<or> row_space A = {0}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
row_space A = {} \<or> row_space A = {0}

goal (1 subgoal):
 1. rank A = 0 \<Longrightarrow> False
[PROOF STEP]
hence "row_space A = {0}"
[PROOF STATE]
proof (prove)
using this:
row_space A = {} \<or> row_space A = {0}

goal (1 subgoal):
 1. row_space A = {0}
[PROOF STEP]
unfolding row_space_def
[PROOF STATE]
proof (prove)
using this:
vec.span (rows A) = {} \<or> vec.span (rows A) = {0}

goal (1 subgoal):
 1. vec.span (rows A) = {0}
[PROOF STEP]
using vec.span_zero
[PROOF STATE]
proof (prove)
using this:
vec.span (rows A) = {} \<or> vec.span (rows A) = {0}
0 \<in> vec.span ?S

goal (1 subgoal):
 1. vec.span (rows A) = {0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row_space A = {0}

goal (1 subgoal):
 1. rank A = 0 \<Longrightarrow> False
[PROOF STEP]
hence "rows A = {} \<or> rows A = {0}"
[PROOF STATE]
proof (prove)
using this:
row_space A = {0}

goal (1 subgoal):
 1. rows A = {} \<or> rows A = {0}
[PROOF STEP]
unfolding row_space_def
[PROOF STATE]
proof (prove)
using this:
vec.span (rows A) = {0}

goal (1 subgoal):
 1. rows A = {} \<or> rows A = {0}
[PROOF STEP]
using vec.span_0_imp_set_empty_or_0
[PROOF STATE]
proof (prove)
using this:
vec.span (rows A) = {0}
vec.span ?A = {0} \<Longrightarrow> ?A = {} \<or> ?A = {0}

goal (1 subgoal):
 1. rows A = {} \<or> rows A = {0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rows A = {} \<or> rows A = {0}

goal (1 subgoal):
 1. rank A = 0 \<Longrightarrow> False
[PROOF STEP]
hence "rows A = {0}"
[PROOF STATE]
proof (prove)
using this:
rows A = {} \<or> rows A = {0}

goal (1 subgoal):
 1. rows A = {0}
[PROOF STEP]
unfolding rows_def row_def
[PROOF STATE]
proof (prove)
using this:
{vec_lambda (($) (A $ i)) |i. i \<in> UNIV} = {} \<or> {vec_lambda (($) (A $ i)) |i. i \<in> UNIV} = {0}

goal (1 subgoal):
 1. {vec_lambda (($) (A $ i)) |i. i \<in> UNIV} = {0}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
rows A = {0}

goal (1 subgoal):
 1. rank A = 0 \<Longrightarrow> False
[PROOF STEP]
hence "A = 0"
[PROOF STATE]
proof (prove)
using this:
rows A = {0}

goal (1 subgoal):
 1. A = 0
[PROOF STEP]
unfolding rows_def row_def vec_nth_inverse
[PROOF STATE]
proof (prove)
using this:
{A $ i |i. i \<in> UNIV} = {0}

goal (1 subgoal):
 1. A = 0
[PROOF STEP]
by (auto, metis (mono_tags) mem_Collect_eq singleton_iff vec_lambda_unique zero_index)
[PROOF STATE]
proof (state)
this:
A = 0

goal (1 subgoal):
 1. rank A = 0 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
A = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A = 0
A \<noteq> 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Gauss_Jordan_not_0:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
assumes "A \<noteq> 0"
shows "Gauss_Jordan A \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A \<noteq> 0
[PROOF STEP]
by (metis assms less_not_refl3 rank_0 rank_Gauss_Jordan rank_greater_zero)