Nuprl Lemma : adj-solution-column

∀[r:CRng]. ∀[n:ℕ]. ∀[A:Matrix(n;n;r)]. ∀[c:|r|]. ∀[b:Column(n;r)].
  (adj-solution(r;n;A;c;b) = c*matrix(|matrix(if y=j then b[x,0] else A[x,y])|) ∈ Column(n;r))


Proof



Definitions occuring in Statement :  adj-solution: adj-solution(r;n;A;c;b),  matrix-scalar-mul: k*M,  matrix-det: |M|,  mx: matrix(M[x; y]),  matrix-ap: M[i,j],  matrix: Matrix(n;m;r),  nat: ℕ,  uall: ∀[x:A]. B[x],  int_eq: if a=b then c else d,  natural_number: $n,  equal: s = t ∈ T,  crng: CRng,  rng_car: |r|
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  adj-solution: adj-solution(r;n;A;c;b),  squash: ↓T,  prop: ℙ,  nat: ℕ,  crng: CRng,  rng: Rng,  le: A ≤ B,  and: P ∧ Q,  less_than': less_than'(a;b),  false: False,  not: ¬A,  implies: P ⇒ Q,  matrix-times: (M*N),  so_lambda: λ2x y.t[x; y],  adjugate: adj(M),  all: ∀x:A. B[x],  top: Top,  so_apply: x[s1;s2],  so_lambda: λ2x.t[x],  int_seg: {i..j-},  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  uimplies: b supposing a,  ifthenelse: if b then t else f fi ,  guard: {T},  ge: i ≥ j ,  lelt: i ≤ j < k,  decidable: Dec(P),  or: P ∨ Q,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  bfalse: ff,  subtype_rel: A ⊆r B,  so_apply: x[s],  sq_type: SQType(T),  bnot: ¬bb,  assert: ↑b,  less_than: a < b,  true: True,  nequal: a ≠ b ∈ T ,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  matrix-minor: matrix-minor(i;j;m),  mx: matrix(M[x; y]),  subtract: n - m,  ringeq_int_terms: t1 ≡ t2
Lemmas referenced :  matrix-scalar-mul_wf,  squash_wf,  true_wf,  matrix_wf,  nat_wf,  rng_car_wf,  rng_sig_wf,  istype-false,  le_wf,  mx_wf,  int_seg_wf,  istype-int,  matrix_ap_mx_lemma,  istype-void,  expand-det-by-column,  equal_wf,  istype-universe,  rng_sum_wf,  isEven_wf,  eqtt_to_assert,  infix_ap_wf,  rng_times_wf,  matrix-det_wf,  subtract_wf,  int_seg_properties,  nat_properties,  decidable__le,  full-omega-unsat,  intformand_wf,  intformnot_wf,  intformle_wf,  itermConstant_wf,  itermSubtract_wf,  itermVar_wf,  intformless_wf,  int_formula_prop_and_lemma,  int_formula_prop_not_lemma,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  int_term_value_subtract_lemma,  int_term_value_var_lemma,  int_formula_prop_less_lemma,  int_formula_prop_wf,  matrix-minor_wf,  matrix-ap_wf,  eqff_to_assert,  set_subtype_base,  lelt_wf,  int_subtype_base,  bool_cases_sqequal,  subtype_base_sq,  bool_wf,  bool_subtype_base,  assert-bnot,  rng_minus_wf,  eq_int_wf,  assert_of_eq_int,  less_than_wf,  neg_assert_of_eq_int,  subtype_rel_self,  iff_weakening_equal,  rng_wf,  crng_wf,  add-commutes,  assert_elim,  not_assert_elim,  btrue_neq_bfalse,  lt_int_wf,  assert_of_lt_int,  istype-top,  decidable__lt,  iff_weakening_uiff,  assert_wf,  add-member-int_seg2,  intformeq_wf,  int_formula_prop_eq_lemma,  itermAdd_wf,  int_term_value_add_lemma,  decidable__equal_int,  crng_times_comm,  itermMultiply_wf,  itermMinus_wf,  ringeq-iff-rsub-is-0,  ring_polynomial_null,  int-to-ring_wf,  ring_term_value_add_lemma,  ring_term_value_mul_lemma,  ring_term_value_minus_lemma,  ring_term_value_var_lemma,  ring_term_value_const_lemma,  int-to-ring-zero
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  introduction,  cut,  applyEquality,  thin,  lambdaEquality_alt,  sqequalHypSubstitution,  imageElimination,  extract_by_obid,  isectElimination,  hypothesisEquality,  equalityTransitivity,  hypothesis,  equalitySymmetry,  universeIsType,  setElimination,  rename,  inhabitedIsType,  because_Cache,  dependent_set_memberEquality_alt,  natural_numberEquality,  sqequalRule,  independent_pairFormation,  lambdaFormation_alt,  functionIsType,  dependent_functionElimination,  isect_memberEquality_alt,  voidElimination,  universeEquality,  addEquality,  unionElimination,  equalityElimination,  productElimination,  independent_isectElimination,  approximateComputation,  independent_functionElimination,  dependent_pairFormation_alt,  int_eqEquality,  equalityIsType2,  baseApply,  closedConclusion,  baseClosed,  intEquality,  promote_hyp,  instantiate,  cumulativity,  equalityIsType1,  int_eqReduceTrueSq,  imageMemberEquality,  productIsType,  int_eqReduceFalseSq,  axiomEquality,  hyp_replacement,  applyLambdaEquality,  equalityIsType4,  lessCases,  axiomSqEquality
Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:Matrix(n;n;r)].  \mforall{}[c:|r|].  \mforall{}[b:Column(n;r)].
    (adj-solution(r;n;A;c;b)  =  c*matrix(|matrix(if  y=j  then  b[x,0]  else  A[x,y])|))


Date html generated: 2019_10_16-AM-11_28_38
Last ObjectModification: 2018_10_11-PM-04_15_47

Theory : matrices


Home Index