matrix_rank_selected_point_selector_transport

forall b c w rb rc cb cc q Rb Rc Cb Cc i a. (forall mdr_i_point_rows mdr_a_point_rows. (exists mdr_gap_point_rowsb. mdr_gap_point_rowsb + S (mdr_i_point_rows) = (q)) -> (((exists ff_h_mdr_point_rowso. ff_h_mdr_point_rowso + S (mdr_a_point_rows) = S ((S (mdr_i_point_rows)) * rc)) /\ exists ff_q_mdr_point_rowso. rb = ff_q_mdr_point_rowso * S ((S (mdr_i_point_rows)) * rc) + (mdr_a_point_rows))) -> (((exists ff_h_mdr_point_rowsn. ff_h_mdr_point_rowsn + S (mdr_a_point_rows) = S ((S (mdr_i_point_rows)) * Rc)) /\ exists ff_q_mdr_point_rowsn. Rb = ff_q_mdr_point_rowsn * S ((S (mdr_i_point_rows)) * Rc) + (mdr_a_point_rows)))) -> (forall mdr_i_point_columns mdr_a_point_columns. (exists mdr_gap_point_columnsb. mdr_gap_point_columnsb + S (mdr_i_point_columns) = (q)) -> (((exists ff_h_mdr_point_columnso. ff_h_mdr_point_columnso + S (mdr_a_point_columns) = S ((S (mdr_i_point_columns)) * cc)) /\ exists ff_q_mdr_point_columnso. cb = ff_q_mdr_point_columnso * S ((S (mdr_i_point_columns)) * cc) + (mdr_a_point_columns))) -> (((exists ff_h_mdr_point_columnsn. ff_h_mdr_point_columnsn + S (mdr_a_point_columns) = S ((S (mdr_i_point_columns)) * Cc)) /\ exists ff_q_mdr_point_columnsn. Cb = ff_q_mdr_point_columnsn * S ((S (mdr_i_point_columns)) * Cc) + (mdr_a_point_columns)))) -> (exists mdr_gap_point_index. mdr_gap_point_index + S (i) = (q * q)) -> (exists mdr_r_point_source mdr_s_point_source mdr_u_point_source mdr_v_point_source. ((i = (q) * mdr_r_point_source + mdr_s_point_source) /\ ((exists mdr_gap_point_sourcecolumn. mdr_gap_point_sourcecolumn + S (mdr_s_point_source) = (q)) /\ ((((exists ff_h_mdr_point_sourcerow_index. ff_h_mdr_point_sourcerow_index + S (mdr_u_point_source) = S ((S (mdr_r_point_source)) * rc)) /\ exists ff_q_mdr_point_sourcerow_index. rb = ff_q_mdr_point_sourcerow_index * S ((S (mdr_r_point_source)) * rc) + (mdr_u_point_source))) /\ ((((exists ff_h_mdr_point_sourcecolumn_index. ff_h_mdr_point_sourcecolumn_index + S (mdr_v_point_source) = S ((S (mdr_s_point_source)) * cc)) /\ exists ff_q_mdr_point_sourcecolumn_index. cb = ff_q_mdr_point_sourcecolumn_index * S ((S (mdr_s_point_source)) * cc) + (mdr_v_point_source))) /\ (((exists ff_h_mdr_point_sourcesource. ff_h_mdr_point_sourcesource + S (a) = S ((S ((mdr_u_point_source) * (w) + (mdr_v_point_source))) * c)) /\ exists ff_q_mdr_point_sourcesource. b = ff_q_mdr_point_sourcesource * S ((S ((mdr_u_point_source) * (w) + (mdr_v_point_source))) * c) + (a)))))))) -> (exists mdr_r_point_target mdr_s_point_target mdr_u_point_target mdr_v_point_target. ((i = (q) * mdr_r_point_target + mdr_s_point_target) /\ ((exists mdr_gap_point_targetcolumn. mdr_gap_point_targetcolumn + S (mdr_s_point_target) = (q)) /\ ((((exists ff_h_mdr_point_targetrow_index. ff_h_mdr_point_targetrow_index + S (mdr_u_point_target) = S ((S (mdr_r_point_target)) * Rc)) /\ exists ff_q_mdr_point_targetrow_index. Rb = ff_q_mdr_point_targetrow_index * S ((S (mdr_r_point_target)) * Rc) + (mdr_u_point_target))) /\ ((((exists ff_h_mdr_point_targetcolumn_index. ff_h_mdr_point_targetcolumn_index + S (mdr_v_point_target) = S ((S (mdr_s_point_target)) * Cc)) /\ exists ff_q_mdr_point_targetcolumn_index. Cb = ff_q_mdr_point_targetcolumn_index * S ((S (mdr_s_point_target)) * Cc) + (mdr_v_point_target))) /\ (((exists ff_h_mdr_point_targetsource. ff_h_mdr_point_targetsource + S (a) = S ((S ((mdr_u_point_target) * (w) + (mdr_v_point_target))) * c)) /\ exists ff_q_mdr_point_targetsource. b = ff_q_mdr_point_targetsource * S ((S ((mdr_u_point_target) * (w) + (mdr_v_point_target))) * c) + (a))))))))