[STATEMENT]
lemma invertible_Gauss_Jordan_column_k:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}" and k::nat
  shows "\<exists>P. invertible P \<and> (snd (Gauss_Jordan_column_k (i,A) k)) = P**A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (i, A) k) = P ** A
[PROOF STEP]
unfolding Gauss_Jordan_column_k_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> snd (if (\<forall>m\<ge>mod_type_class.from_nat (fst (i, A)). snd (i, A) $ m $ mod_type_class.from_nat k = (0::'a)) \<or> fst (i, A) = nrows (snd (i, A)) then (fst (i, A), snd (i, A)) else (fst (i, A) + 1, Gauss_Jordan_in_ij (snd (i, A)) (mod_type_class.from_nat (fst (i, A))) (mod_type_class.from_nat k))) = P ** A
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) \<Longrightarrow> \<exists>P. invertible P \<and> A = P ** A
 2. i = nrows A \<Longrightarrow> \<exists>P. invertible P \<and> A = P ** A
 3. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
show "\<exists>P. invertible P \<and> A = P ** A" and "\<exists>P. invertible P \<and> A = P ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> A = P ** A &&& \<exists>P. invertible P \<and> A = P ** A
[PROOF STEP]
using invertible_mat_1 matrix_mul_lid[of A]
[PROOF STATE]
proof (prove)
using this:
invertible (mat (1::?'a))
mat (1::'a) ** A = A

goal (1 subgoal):
 1. \<exists>P. invertible P \<and> A = P ** A &&& \<exists>P. invertible P \<and> A = P ** A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> A = P ** A
\<exists>P. invertible P \<and> A = P ** A

goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
assume i: "i \<noteq> nrows A"
    and i_le_m: "from_nat i \<le> m" and Amk_not_zero: "A $ m $ from_nat k \<noteq> 0"
[PROOF STATE]
proof (state)
this:
i \<noteq> nrows A
mod_type_class.from_nat i \<le> m
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
define A_interchange where "A_interchange = interchange_rows A (from_nat i) (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> (from_nat i) \<le> n)"
[PROOF STATE]
proof (state)
this:
A_interchange = interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
define A_mult where "A_mult = mult_row A_interchange (from_nat i) (1 / (A_interchange $ (from_nat i) $ from_nat k))"
[PROOF STATE]
proof (state)
this:
A_mult = mult_row A_interchange (mod_type_class.from_nat i) ((1::'a) / A_interchange $ mod_type_class.from_nat i $ mod_type_class.from_nat k)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
obtain P where inv_P: "invertible P" and PA: "A_interchange = P**A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrakk>invertible P; A_interchange = P ** A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding A_interchange_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrakk>invertible P; interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) = P ** A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using interchange_rows_mat_1[of "from_nat i" "(LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> from_nat i \<le> n)" A]
[PROOF STATE]
proof (prove)
using this:
interchange_rows (mat (1::'a)) (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) ** A = interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>invertible P; interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) = P ** A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using invertible_interchange_rows[of "from_nat i" "(LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> from_nat i \<le> n)"]
[PROOF STATE]
proof (prove)
using this:
interchange_rows (mat (1::'a)) (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) ** A = interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)
invertible (interchange_rows (mat (1::?'a)) (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n))

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>invertible P; interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) = P ** A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
invertible P
A_interchange = P ** A

goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
define Q :: "'a^'m::{mod_type}^'m::{mod_type}"
    where "Q = mult_row (mat 1) (from_nat i) (1 / (A_interchange $ (from_nat i) $ from_nat k))"
[PROOF STATE]
proof (state)
this:
Q = mult_row (mat (1::'a)) (mod_type_class.from_nat i) ((1::'a) / A_interchange $ mod_type_class.from_nat i $ mod_type_class.from_nat k)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
have Q_A_interchange: "A_mult = Q**A_interchange"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A_mult = Q ** A_interchange
[PROOF STEP]
unfolding A_mult_def A_interchange_def Q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_row (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (mod_type_class.from_nat i) ((1::'a) / interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) $ mod_type_class.from_nat i $ mod_type_class.from_nat k) = mult_row (mat (1::'a)) (mod_type_class.from_nat i) ((1::'a) / interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) $ mod_type_class.from_nat i $ mod_type_class.from_nat k) ** interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)
[PROOF STEP]
unfolding mult_row_mat_1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_row (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (mod_type_class.from_nat i) ((1::'a) / interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) $ mod_type_class.from_nat i $ mod_type_class.from_nat k) = mult_row (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (mod_type_class.from_nat i) ((1::'a) / interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) $ mod_type_class.from_nat i $ mod_type_class.from_nat k)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A_mult = Q ** A_interchange

goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
have inv_Q: "invertible Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible Q
[PROOF STEP]
proof (unfold Q_def, rule invertible_mult_row', unfold A_interchange_def, rule LeastI2_ex)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>a. A $ a $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> a
 2. \<And>x. A $ x $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> x \<Longrightarrow> (1::'a) / interchange_rows A (mod_type_class.from_nat i) x $ mod_type_class.from_nat i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
show "\<exists>a. A $ a $ from_nat k \<noteq> 0 \<and> (from_nat i) \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. A $ a $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> a
[PROOF STEP]
using i_le_m Amk_not_zero
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat i \<le> m
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>a. A $ a $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>a. A $ a $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> a

goal (1 subgoal):
 1. \<And>x. A $ x $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> x \<Longrightarrow> (1::'a) / interchange_rows A (mod_type_class.from_nat i) x $ mod_type_class.from_nat i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
show "\<And>x. A $ x $ from_nat k \<noteq> 0 \<and> (from_nat i) \<le> x \<Longrightarrow> 1 / interchange_rows A (from_nat i) x $ (from_nat i) $ from_nat k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. A $ x $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> x \<Longrightarrow> (1::'a) / interchange_rows A (mod_type_class.from_nat i) x $ mod_type_class.from_nat i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using interchange_rows_i mult_zero_left nonzero_divide_eq_eq zero_neq_one
[PROOF STATE]
proof (prove)
using this:
interchange_rows ?A ?i ?j $ ?i = ?A $ ?j
(0::?'a) * ?a = (0::?'a)
?c \<noteq> (0::?'a) \<Longrightarrow> (?b / ?c = ?a) = (?b = ?a * ?c)
(0::?'a) \<noteq> (1::?'a)

goal (1 subgoal):
 1. \<And>x. A $ x $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> x \<Longrightarrow> (1::'a) / interchange_rows A (mod_type_class.from_nat i) x $ mod_type_class.from_nat i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
A $ ?x $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> ?x \<Longrightarrow> (1::'a) / interchange_rows A (mod_type_class.from_nat i) ?x $ mod_type_class.from_nat i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invertible Q

goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
obtain Pa where inv_Pa: "invertible Pa" and Pa: "row_add_iterate (Q ** (P ** A)) (nrows A - 1) (from_nat i) (from_nat k) = Pa ** (Q ** (P ** A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Pa. \<lbrakk>invertible Pa; row_add_iterate (Q ** (P ** A)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** (Q ** (P ** A))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using invertible_row_add_iterate
[PROOF STATE]
proof (prove)
using this:
?n < nrows ?A \<Longrightarrow> \<exists>P. invertible P \<and> row_add_iterate ?A ?n ?i ?j = P ** ?A

goal (1 subgoal):
 1. (\<And>Pa. \<lbrakk>invertible Pa; row_add_iterate (Q ** (P ** A)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** (Q ** (P ** A))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (full_types) diff_less nrows_def zero_less_card_finite zero_less_one)
[PROOF STATE]
proof (state)
this:
invertible Pa
row_add_iterate (Q ** (P ** A)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** (Q ** (P ** A))

goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
show "\<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (from_nat i) (from_nat k) = P ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A
[PROOF STEP]
proof (rule exI[of _ "Pa**Q**P"], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. invertible (Pa ** Q ** P)
 2. Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A
[PROOF STEP]
show "invertible (Pa ** Q ** P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible (Pa ** Q ** P)
[PROOF STEP]
using inv_P inv_Pa inv_Q invertible_mult
[PROOF STATE]
proof (prove)
using this:
invertible P
invertible Pa
invertible Q
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)

goal (1 subgoal):
 1. invertible (Pa ** Q ** P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
invertible (Pa ** Q ** P)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A
[PROOF STEP]
have "Gauss_Jordan_in_ij A (from_nat i) (from_nat k) = row_add_iterate A_mult (nrows A - 1) (from_nat i) (from_nat k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = row_add_iterate A_mult (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k)
[PROOF STEP]
unfolding row_add_iterate_eq_Gauss_Jordan_in_ij[symmetric]  A_mult_def A_interchange_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate (mult_row (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (mod_type_class.from_nat i) ((1::'a) / interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) $ mod_type_class.from_nat i $ mod_type_class.from_nat k)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = row_add_iterate (mult_row (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (mod_type_class.from_nat i) ((1::'a) / interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n) $ mod_type_class.from_nat i $ mod_type_class.from_nat k)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = row_add_iterate A_mult (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = row_add_iterate A_mult (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A
[PROOF STEP]
have "... = Pa ** (Q ** (P ** A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A_mult (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** (Q ** (P ** A))
[PROOF STEP]
using Pa
[PROOF STATE]
proof (prove)
using this:
row_add_iterate (Q ** (P ** A)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** (Q ** (P ** A))

goal (1 subgoal):
 1. row_add_iterate A_mult (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** (Q ** (P ** A))
[PROOF STEP]
unfolding PA[symmetric] Q_A_interchange[symmetric]
[PROOF STATE]
proof (prove)
using this:
row_add_iterate A_mult (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** A_mult

goal (1 subgoal):
 1. row_add_iterate A_mult (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** A_mult
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
row_add_iterate A_mult (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** (Q ** (P ** A))

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row_add_iterate A_mult (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** (Q ** (P ** A))

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A
[PROOF STEP]
have "... = Pa ** Q ** P ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pa ** (Q ** (P ** A)) = Pa ** Q ** P ** A
[PROOF STEP]
unfolding matrix_mul_assoc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pa ** Q ** P ** A = Pa ** Q ** P ** A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Pa ** (Q ** (P ** A)) = Pa ** Q ** P ** A

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A
[PROOF STEP]
show "Gauss_Jordan_in_ij A (from_nat i) (from_nat k) = Pa ** Q ** P ** A"
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = Pa ** Q ** P ** A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> Gauss_Jordan_in_ij A (mod_type_class.from_nat i) (mod_type_class.from_nat k) = P ** A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invertible_Gauss_Jordan_up_to_k:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "\<exists>P. invertible P \<and> (Gauss_Jordan_upt_k A k) = P**A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A 0 = P ** A
 2. \<And>k. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (Suc k) = P ** A
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A 0 = P ** A
 2. \<And>k. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (Suc k) = P ** A
[PROOF STEP]
have rw: "[0..<Suc 0] = [0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<Suc 0] = [0]
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[0..<Suc 0] = [0]

goal (2 subgoals):
 1. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A 0 = P ** A
 2. \<And>k. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (Suc k) = P ** A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A 0 = P ** A
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_def rw foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (0, A) 0) = P ** A
[PROOF STEP]
using invertible_Gauss_Jordan_column_k
[PROOF STATE]
proof (prove)
using this:
\<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (?i, ?A) ?k) = P ** ?A

goal (1 subgoal):
 1. \<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (0, A) 0) = P ** A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> Gauss_Jordan_upt_k A 0 = P ** A

goal (1 subgoal):
 1. \<And>k. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (Suc k) = P ** A
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A

goal (1 subgoal):
 1. \<And>k. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (Suc k) = P ** A
[PROOF STEP]
have rw2: "[0..<Suc (Suc k)] = [0..< Suc k] @ [(Suc k)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]

goal (1 subgoal):
 1. \<And>k. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (Suc k) = P ** A
[PROOF STEP]
obtain P' where inv_P': "invertible P'" and Gk_eq_P'A: "Gauss_Jordan_upt_k A k = P' ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>invertible P'; Gauss_Jordan_upt_k A k = P' ** A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Suc.hyps
[PROOF STATE]
proof (prove)
using this:
\<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A

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

goal (1 subgoal):
 1. \<And>k. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (Suc k) = P ** A
[PROOF STEP]
have g: "Gauss_Jordan_upt_k A k = snd (foldl Gauss_Jordan_column_k (0, A) [0..<Suc k])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_upt_k A k = snd (foldl Gauss_Jordan_column_k (0, A) [0..<Suc k])
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (foldl Gauss_Jordan_column_k (0, A) [0..<Suc k]) = snd (foldl Gauss_Jordan_column_k (0, A) [0..<Suc k])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_upt_k A k = snd (foldl Gauss_Jordan_column_k (0, A) [0..<Suc k])

goal (1 subgoal):
 1. \<And>k. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A \<Longrightarrow> \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (Suc k) = P ** A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (Suc k) = P ** A
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> snd (foldl Gauss_Jordan_column_k (0, A) [0..<Suc (Suc k)]) = P ** A
[PROOF STEP]
unfolding rw2 foldl_append foldl.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (foldl Gauss_Jordan_column_k (0, A) [0..<Suc k]) (Suc k)) = P ** A
[PROOF STEP]
apply (subst prod.collapse[symmetric, of "(foldl Gauss_Jordan_column_k (0, A) [0..<Suc k])", unfolded g[symmetric]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (fst (foldl Gauss_Jordan_column_k (0, A) [0..<Suc k]), Gauss_Jordan_upt_k A k) (Suc k)) = P ** A
[PROOF STEP]
using invertible_Gauss_Jordan_column_k
[PROOF STATE]
proof (prove)
using this:
\<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (?i, ?A) ?k) = P ** ?A

goal (1 subgoal):
 1. \<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (fst (foldl Gauss_Jordan_column_k (0, A) [0..<Suc k]), Gauss_Jordan_upt_k A k) (Suc k)) = P ** A
[PROOF STEP]
using Suc.hyps
[PROOF STATE]
proof (prove)
using this:
\<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (?i, ?A) ?k) = P ** ?A
\<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A

goal (1 subgoal):
 1. \<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (fst (foldl Gauss_Jordan_column_k (0, A) [0..<Suc k]), Gauss_Jordan_upt_k A k) (Suc k)) = P ** A
[PROOF STEP]
using invertible_mult matrix_mul_assoc
[PROOF STATE]
proof (prove)
using this:
\<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (?i, ?A) ?k) = P ** ?A
\<exists>P. invertible P \<and> Gauss_Jordan_upt_k A k = P ** A
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)
?A ** (?B ** ?C) = ?A ** ?B ** ?C

goal (1 subgoal):
 1. \<exists>P. invertible P \<and> snd (Gauss_Jordan_column_k (fst (foldl Gauss_Jordan_column_k (0, A) [0..<Suc k]), Gauss_Jordan_upt_k A k) (Suc k)) = P ** A
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (Suc k) = P ** A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_index_independent_rows:
  fixes A::"'a::{field}^'m::{mod_type}^'n::{finite,one,plus,ord}"
  assumes rref_A: "reduced_row_echelon_form A"
  and x: "row x A \<in> {row i A |i. row i A \<noteq> 0}"
  and eq: "A $ x = A $ y"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
assume x_not_y: "x \<noteq> y"
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
have not_zero_x: "\<not> is_zero_row x A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row x A
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
row x A \<in> {row i A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. \<not> is_zero_row x A
[PROOF STEP]
unfolding is_zero_row_def
[PROOF STATE]
proof (prove)
using this:
row x A \<in> {row i A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k x (ncols A) A
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
row x A \<in> {row i A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < ncols A \<longrightarrow> A $ x $ j = (0::'a))
[PROOF STEP]
unfolding row_def vec_eq_iff
    ncols_def
[PROOF STATE]
proof (prove)
using this:
vec_lambda (($) (A $ x)) \<in> {uu_. \<exists>i. (\<forall>ia. uu_ $ ia = vec_lambda (($) (A $ i)) $ ia) \<and> \<not> (\<forall>ia. vec_lambda (($) (A $ i)) $ ia = 0 $ ia)}

goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < CARD('m) \<longrightarrow> A $ x $ j = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row x A

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
hence not_zero_y: "\<not> is_zero_row y A"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row x A

goal (1 subgoal):
 1. \<not> is_zero_row y A
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row x A
A $ x = A $ y

goal (1 subgoal):
 1. \<not> is_zero_row y A
[PROOF STEP]
unfolding is_zero_row_def'
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j. A $ x $ j = (0::'a))
A $ x = A $ y

goal (1 subgoal):
 1. \<not> (\<forall>j. A $ y $ j = (0::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row y A

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
have Ax: "A $ x $ (LEAST k. A $ x $ k \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ x $ (LEAST k. A $ x $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using not_zero_x rref_condition2[OF rref_A]
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row x A
\<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 $ x $ (LEAST k. A $ x $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $ x $ (LEAST k. A $ x $ k \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
have Ay: "A $ x $ (LEAST k. A $ y $ k \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ x $ (LEAST k. A $ y $ k \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
using not_zero_y x_not_y rref_condition4[OF rref_A]
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row y A
x \<noteq> y
\<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))

goal (1 subgoal):
 1. A $ x $ (LEAST k. A $ y $ k \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
A $ x $ (LEAST k. A $ y $ k \<noteq> (0::'a)) = (0::'a)

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using Ax Ay
[PROOF STATE]
proof (prove)
using this:
A $ x $ (LEAST k. A $ x $ k \<noteq> (0::'a)) = (1::'a)
A $ x $ (LEAST k. A $ y $ k \<noteq> (0::'a)) = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding eq
[PROOF STATE]
proof (prove)
using this:
A $ y $ (LEAST k. A $ y $ k \<noteq> (0::'a)) = (1::'a)
A $ y $ (LEAST k. A $ y $ k \<noteq> (0::'a)) = (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invertible_Gauss_Jordan:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "\<exists>P. invertible P \<and> (Gauss_Jordan A) = P**A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> Gauss_Jordan A = P ** A
[PROOF STEP]
unfolding Gauss_Jordan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (ncols A - 1) = P ** A
[PROOF STEP]
using invertible_Gauss_Jordan_up_to_k
[PROOF STATE]
proof (prove)
using this:
\<exists>P. invertible P \<and> Gauss_Jordan_upt_k ?A ?k = P ** ?A

goal (1 subgoal):
 1. \<exists>P. invertible P \<and> Gauss_Jordan_upt_k A (ncols A - 1) = P ** A
[PROOF STEP]
.


[STATEMENT]
lemma Gauss_Jordan:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "\<exists>P. invertible P \<and> (Gauss_Jordan A) = P**A \<and> reduced_row_echelon_form (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. invertible P \<and> Gauss_Jordan A = P ** A \<and> reduced_row_echelon_form (Gauss_Jordan A)
[PROOF STEP]
by (simp add: invertible_Gauss_Jordan rref_Gauss_Jordan)


[STATEMENT]
lemma rref_rank:
  fixes A::"'a::{field}^'m::{mod_type}^'n::{finite,one,plus,ord}"
  assumes rref_A: "reduced_row_echelon_form A"
  shows "rank A = card {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = card {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
unfolding rank_def row_rank_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (row_space A) = card {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
proof (rule vec.dim_unique[of "{row i A | i. row i A \<noteq> 0}"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. {row i A |i. row i A \<noteq> 0} \<subseteq> row_space A
 2. row_space A \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
 3. vec.independent {row i A |i. row i A \<noteq> 0}
 4. card {row i A |i. row i A \<noteq> 0} = card {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
show "{row i A |i. row i A \<noteq> 0} \<subseteq> row_space A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {row i A |i. row i A \<noteq> 0} \<subseteq> row_space A
[PROOF STEP]
proof (auto, unfold row_space_def rows_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. row i A \<noteq> 0 \<Longrightarrow> row i A \<in> vec.span {row i A |i. i \<in> UNIV}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. row i A \<noteq> 0 \<Longrightarrow> row i A \<in> vec.span {row i A |i. i \<in> UNIV}
[PROOF STEP]
assume "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> row i A \<in> vec.span {row i A |i. i \<in> UNIV}
[PROOF STEP]
show "row i A \<in> vec.span {row i A |i. i \<in> UNIV}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row i A \<in> vec.span {row i A |i. i \<in> UNIV}
[PROOF STEP]
by (rule vec.span_base, auto)
[PROOF STATE]
proof (state)
this:
row i A \<in> vec.span {row i A |i. i \<in> UNIV}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{row i A |i. row i A \<noteq> 0} \<subseteq> row_space A

goal (3 subgoals):
 1. row_space A \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
 2. vec.independent {row i A |i. row i A \<noteq> 0}
 3. card {row i A |i. row i A \<noteq> 0} = card {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
show "row_space A \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_space A \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
proof (unfold row_space_def rows_def, cases "\<exists>i. row i A = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
 2. \<nexists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>i. row i A = 0

goal (2 subgoals):
 1. \<exists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
 2. \<nexists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
have set_rw: "{row i A |i. i \<in> UNIV} = insert 0 {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {row i A |i. i \<in> UNIV} = insert 0 {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
\<exists>i. row i A = 0

goal (1 subgoal):
 1. {row i A |i. i \<in> UNIV} = insert 0 {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{row i A |i. i \<in> UNIV} = insert 0 {row i A |i. row i A \<noteq> 0}

goal (2 subgoals):
 1. \<exists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
 2. \<nexists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
have "vec.span {row i A |i. i \<in> UNIV} = vec.span {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.span {row i A |i. i \<in> UNIV} = vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
unfolding set_rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.span (insert 0 {row i A |i. row i A \<noteq> 0}) = vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
using vec.span_insert_0
[PROOF STATE]
proof (prove)
using this:
vec.span (insert 0 ?S) = vec.span ?S

goal (1 subgoal):
 1. vec.span (insert 0 {row i A |i. row i A \<noteq> 0}) = vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
vec.span {row i A |i. i \<in> UNIV} = vec.span {row i A |i. row i A \<noteq> 0}

goal (2 subgoals):
 1. \<exists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
 2. \<nexists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
thus "vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
using this:
vec.span {row i A |i. i \<in> UNIV} = vec.span {row i A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. \<nexists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>i. row i A = 0

goal (1 subgoal):
 1. \<nexists>i. row i A = 0 \<Longrightarrow> vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
show "vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. row i A = 0

goal (1 subgoal):
 1. vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec.span {row i A |i. i \<in> UNIV} \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_space A \<subseteq> vec.span {row i A |i. row i A \<noteq> 0}

goal (2 subgoals):
 1. vec.independent {row i A |i. row i A \<noteq> 0}
 2. card {row i A |i. row i A \<noteq> 0} = card {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
show "vec.independent {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.independent {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
by (rule independent_not_zero_rows_rref[OF rref_A])
[PROOF STATE]
proof (state)
this:
vec.independent {row i A |i. row i A \<noteq> 0}

goal (1 subgoal):
 1. card {row i A |i. row i A \<noteq> 0} = card {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
show "card {row i A |i. row i A \<noteq> 0} = card {row i A |i. row i A \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {row i A |i. row i A \<noteq> 0} = card {row i A |i. row i A \<noteq> 0}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
card {row i A |i. row i A \<noteq> 0} = card {row i A |i. row i A \<noteq> 0}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma column_leading_coefficient_component_eq:
  fixes A::"'a::{field}^'m::{mod_type}^'n::{finite,one,plus,ord}"
  assumes rref_A: "reduced_row_echelon_form A"
  and v: "v \<in> {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}"
  and vx: "v $ x \<noteq> 0"
  and vy: "v $ y \<noteq> 0"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[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. x = y
[PROOF STEP]
have vb_not_zero: "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. x = y
[PROOF STEP]
have b_eq_x: "b = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = x
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> x \<Longrightarrow> False
[PROOF STEP]
assume b_not_x: "b\<noteq>x"
[PROOF STATE]
proof (state)
this:
b \<noteq> x

goal (1 subgoal):
 1. b \<noteq> x \<Longrightarrow> False
[PROOF STEP]
have "A $ x $ (LEAST n. A $ b $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ x $ (LEAST n. A $ b $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
by (rule rref_condition4_explicit[OF rref_A _ b_not_x], simp add: is_zero_row_eq_row_zero row_b)
[PROOF STATE]
proof (state)
this:
A $ x $ (LEAST n. A $ b $ n \<noteq> (0::'a)) = (0::'a)

goal (1 subgoal):
 1. b \<noteq> x \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
A $ x $ (LEAST n. A $ b $ n \<noteq> (0::'a)) = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using vx
[PROOF STATE]
proof (prove)
using this:
A $ x $ (LEAST n. A $ b $ n \<noteq> (0::'a)) = (0::'a)
v $ x \<noteq> (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding b column_def
[PROOF STATE]
proof (prove)
using this:
A $ x $ (LEAST n. A $ b $ n \<noteq> (0::'a)) = (0::'a)
(\<chi>i. A $ i $ (LEAST n. A $ b $ n \<noteq> (0::'a))) $ x \<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:
b = x

goal (1 subgoal):
 1. x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b = x

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have b_eq_y: "b = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = y
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> y \<Longrightarrow> False
[PROOF STEP]
assume b_not_y: "b\<noteq>y"
[PROOF STATE]
proof (state)
this:
b \<noteq> y

goal (1 subgoal):
 1. b \<noteq> y \<Longrightarrow> False
[PROOF STEP]
have "A $ y $ (LEAST n. A $ b $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ y $ (LEAST n. A $ b $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
by (rule rref_condition4_explicit[OF rref_A _ b_not_y], simp add: is_zero_row_eq_row_zero row_b)
[PROOF STATE]
proof (state)
this:
A $ y $ (LEAST n. A $ b $ n \<noteq> (0::'a)) = (0::'a)

goal (1 subgoal):
 1. b \<noteq> y \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
A $ y $ (LEAST n. A $ b $ n \<noteq> (0::'a)) = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using vy
[PROOF STATE]
proof (prove)
using this:
A $ y $ (LEAST n. A $ b $ n \<noteq> (0::'a)) = (0::'a)
v $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding b column_def
[PROOF STATE]
proof (prove)
using this:
A $ y $ (LEAST n. A $ b $ n \<noteq> (0::'a)) = (0::'a)
(\<chi>i. A $ i $ (LEAST n. A $ b $ n \<noteq> (0::'a))) $ y \<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:
b = y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b = x
b = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = x
b = y

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma column_leading_coefficient_component_1:
  fixes A::"'a::{field}^'m::{mod_type}^'n::{finite,one,plus,ord}"
  assumes rref_A: "reduced_row_echelon_form A"
  and v: "v \<in> {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}"
  and vx: "v $ x \<noteq> 0"
  shows "v $ x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v $ x = (1::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v $ x = (1::'a)
[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. v $ x = (1::'a)
[PROOF STEP]
have vb_not_zero: "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. v $ x = (1::'a)
[PROOF STEP]
have b_eq_x: "b = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = x
[PROOF STEP]
by (metis b column_def is_zero_row_eq_row_zero row_b rref_A rref_condition4 transpose_row_code transpose_row_def vx)
[PROOF STATE]
proof (state)
this:
b = x

goal (1 subgoal):
 1. v $ x = (1::'a)
[PROOF STEP]
show?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v $ x = (1::'a)
[PROOF STEP]
using rref_condition2_explicit[OF rref_A, of b] row_b
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row b A \<Longrightarrow> A $ b $ (LEAST k. A $ b $ k \<noteq> (0::'a)) = (1::'a)
row b A \<noteq> 0

goal (1 subgoal):
 1. v $ x = (1::'a)
[PROOF STEP]
unfolding b column_def is_zero_row_def'
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j. A $ b $ j = (0::'a)) \<Longrightarrow> A $ b $ (LEAST k. A $ b $ k \<noteq> (0::'a)) = (1::'a)
row b A \<noteq> 0

goal (1 subgoal):
 1. (\<chi>i. A $ i $ (LEAST n. A $ b $ n \<noteq> (0::'a))) $ x = (1::'a)
[PROOF STEP]
by (metis (mono_tags) \<open>\<not> is_zero_row b A \<Longrightarrow> A $ b $ (LEAST k. A $ b $ k \<noteq> 0) = 1\<close>
          b_eq_x is_zero_row_eq_row_zero vec_lambda_beta)
[PROOF STATE]
proof (state)
this:
v $ x = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma column_leading_coefficient_component_0:
  fixes A::"'a::{field}^'m::{mod_type}^'n::{finite,one,plus,ord}"
  assumes rref_A: "reduced_row_echelon_form A"
  and v: "v \<in> {column (LEAST n. A $ i $ n \<noteq> 0) A |i. row i A \<noteq> 0}"
  and vx: "v $ x \<noteq> 0"
  and x_not_y: "x \<noteq> y"
  shows "v $ y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v $ y = (0::'a)
[PROOF STEP]
using column_leading_coefficient_component_eq[OF rref_A v vx] x_not_y
[PROOF STATE]
proof (prove)
using this:
v $ ?y \<noteq> (0::'a) \<Longrightarrow> x = ?y
x \<noteq> y

goal (1 subgoal):
 1. v $ y = (0::'a)
[PROOF STEP]
by auto