Nuprl Lemma : matrix-transpose-times
∀[n,k,m:ℕ]. ∀[r:CRng]. ∀[M:Matrix(n;k;r)]. ∀[N:Matrix(k;m;r)]. ((M*N)' = (N'*M') ∈ Matrix(m;n;r))
Proof
Definitions occuring in Statement :
matrix-times: (M*N),
matrix-transpose: M',
matrix: Matrix(n;m;r),
nat: ℕ,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
crng: CRng
Definitions unfolded in proof :
so_apply: x[s1;s2],
so_apply: x[s],
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
guard: {T},
uimplies: b supposing a,
subtype_rel: A ⊆r B,
true: True,
so_lambda: λ2x.t[x],
mx: matrix(M[x; y]),
matrix-ap: M[i,j],
so_lambda: λ2x y.t[x; y],
rng: Rng,
crng: CRng,
nat: ℕ,
prop: ℙ,
squash: ↓T,
matrix-times: (M*N),
matrix-transpose: M',
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
nat_wf,
crng_wf,
matrix_wf,
iff_weakening_equal,
rng_times_wf,
infix_ap_wf,
matrix-ap_wf,
crng_times_comm,
equal_wf,
rng_wf,
rng_sum_wf,
rng_sig_wf,
rng_car_wf,
int_seg_wf,
true_wf,
squash_wf,
mx_wf
Rules used in proof :
axiomEquality,
isect_memberEquality,
independent_functionElimination,
productElimination,
independent_isectElimination,
baseClosed,
imageMemberEquality,
universeEquality,
sqequalRule,
rename,
setElimination,
intEquality,
because_Cache,
natural_numberEquality,
functionEquality,
equalitySymmetry,
hypothesis,
equalityTransitivity,
hypothesisEquality,
isectElimination,
extract_by_obid,
imageElimination,
sqequalHypSubstitution,
lambdaEquality,
thin,
applyEquality,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[n,k,m:\mBbbN{}]. \mforall{}[r:CRng]. \mforall{}[M:Matrix(n;k;r)]. \mforall{}[N:Matrix(k;m;r)]. ((M*N)' = (N'*M'))
Date html generated:
2018_05_21-PM-09_34_47
Last ObjectModification:
2017_12_13-PM-03_00_14
Theory : matrices
Home
Index