[STATEMENT]
lemma Hermite_of_row_i_range_res:
  assumes ji: "j<i" and not_zero_i_A: "\<not> is_zero_row i A" and r: "res_function res"
  shows "Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> 0) 
  \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
let ?n="(LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
define M where "M = mult_row A i (ass (A $ i $ ?n) div A $ i $ ?n)"
[PROOF STATE]
proof (state)
this:
M = mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)))

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
let ?R="row_add M j i ((res (M $ i $ ?n) (M $ j $ ?n) 
    - M $ j $ ?n) div M $ i $ ?n)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
have Hii: "Hermite_of_row_i ass res A i $ i $ ?n = M $ i $ ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))
[PROOF STEP]
by (rule Hermite_of_row_i_works2[OF not_zero_i_A])
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
have rw: "Hermite_of_row_i ass res A i $ j $ ?n = ?R $ j $ ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = row_add M j i ((res (M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) (M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) - M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = row_add (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)))) j i ((res (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) - mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))
[PROOF STEP]
by (rule Hermite_of_row_i_works[OF ji not_zero_i_A])
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = row_add M j i ((res (M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) (M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) - M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
have "\<forall>b ba. \<exists>bb. ba + bb * b = res b ba"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b ba. \<exists>bb. ba + bb * b = res b ba
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
res_function res

goal (1 subgoal):
 1. \<forall>b ba. \<exists>bb. ba + bb * b = res b ba
[PROOF STEP]
unfolding res_function_def
[PROOF STATE]
proof (prove)
using this:
\<forall>c. (\<forall>a b. cong a b c = (res c a = res c b)) \<and> pairwise (\<lambda>a b. \<not> cong a b c) (range (res c)) \<and> (\<forall>a. \<exists>k. res c a = a + k * c)

goal (1 subgoal):
 1. \<forall>b ba. \<exists>bb. ba + bb * b = res b ba
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>b ba. \<exists>bb. ba + bb * b = res b ba

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>b ba. \<exists>bb. ba + bb * b = res b ba

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
using rw
[PROOF STATE]
proof (prove)
using this:
\<forall>b ba. \<exists>bb. ba + bb * b = res b ba
Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = row_add M j i ((res (M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) (M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) - M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))
[PROOF STEP]
unfolding image_def Hii row_add_def
[PROOF STATE]
proof (prove)
using this:
\<forall>b ba. \<exists>bb. ba + bb * b = res b ba
Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = (\<chi>ia ja. if ia = j then M $ j $ ja + (res (M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) (M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) - M $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))) div M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b)) * M $ i $ ja else M $ ia $ ja) $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b))

goal (1 subgoal):
 1. Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> {y. \<exists>x\<in>UNIV. y = res (M $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))) x}
[PROOF STEP]
by auto
      (metis (lifting) add_diff_cancel_left' nonzero_mult_div_cancel_left mult.commute mult_eq_0_iff)
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i ass res A i $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) \<in> range (res (Hermite_of_row_i ass res A i $ i $ (LEAST n. A $ i $ n \<noteq> (0::'b))))

goal:
No subgoals!
[PROOF STEP]
qed