[STATEMENT]
lemma fst_snd_Gauss_Jordan_column_k_iarrays_PA_eq: 
shows "fst (snd (Gauss_Jordan_column_k_iarrays_PA (P,i,A) k)) = fst (Gauss_Jordan_column_k_iarrays (i,A) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_iarrays_PA (P, i, A) k)) = fst (Gauss_Jordan_column_k_iarrays (i, A) k)
[PROOF STEP]
unfolding Gauss_Jordan_column_k_iarrays_PA_def Gauss_Jordan_column_k_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (let Pa = fst (P, i, A); ia = fst (snd (P, i, A)); A = snd (snd (P, i, A)) in if vector_all_zero_from_index (ia, column_iarray k A) \<or> ia = nrows_iarray A then (Pa, ia, A) else let Gauss = Gauss_Jordan_in_ij_iarrays_PA (Pa, A) ia k in (fst Gauss, ia + 1, snd Gauss))) = fst (let Aa = snd (i, A); i = fst (i, A) in if vector_all_zero_from_index (i, column_iarray k Aa) \<or> i = nrows_iarray Aa then (i, Aa) else (Suc i, Gauss_Jordan_in_ij_iarrays Aa i k))
[PROOF STEP]
unfolding Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (if vector_all_zero_from_index (i, column_iarray k A) \<or> i = nrows_iarray A then (P, i, A) else (fst (Gauss_Jordan_in_ij_iarrays_PA (P, A) i k), i + 1, snd (Gauss_Jordan_in_ij_iarrays_PA (P, A) i k)))) = fst (if vector_all_zero_from_index (i, column_iarray k A) \<or> i = nrows_iarray A then (i, A) else (Suc i, Gauss_Jordan_in_ij_iarrays A i k))
[PROOF STEP]
by auto