802 and iU: "i \<in> ?U" |
802 and iU: "i \<in> ?U" |
803 and ci: "c i \<noteq> 0" |
803 and ci: "c i \<noteq> 0" |
804 unfolding invertible_right_inverse |
804 unfolding invertible_right_inverse |
805 unfolding matrix_right_invertible_independent_rows |
805 unfolding matrix_right_invertible_independent_rows |
806 by blast |
806 by blast |
807 have *: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b" |
|
808 apply (drule_tac f="(+) (- a)" in cong[OF refl]) |
|
809 apply (simp only: ab_left_minus add.assoc[symmetric]) |
|
810 apply simp |
|
811 done |
|
812 have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})" |
807 have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})" |
813 apply (rule vector_mul_lcancel_imp[OF ci]) |
808 unfolding sum_cmul |
814 using c ci unfolding sum.remove[OF fU iU] sum_cmul |
809 using c ci |
815 apply (auto simp add: field_simps *) |
810 by (auto simp add: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff) |
816 done |
|
817 have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}" |
811 have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}" |
818 unfolding thr0 |
812 unfolding thr0 |
819 apply (rule span_sum) |
813 apply (rule span_sum) |
820 apply simp |
814 apply simp |
821 apply (rule span_mul [where 'a="real^'n"]) |
815 apply (rule span_mul) |
822 apply (rule span_superset) |
816 apply (rule span_superset) |
823 apply auto |
817 apply auto |
824 done |
818 done |
825 let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n" |
819 let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n" |
826 have thrb: "row i ?B = 0" using iU by (vector row_def) |
820 have thrb: "row i ?B = 0" using iU by (vector row_def) |