Nuprl Lemma : scalar-product-3
∀[r,a,b:Top]. ((a . b) ~ ((0 +r ((a 0) * (b 0))) +r ((a 1) * (b 1))) +r ((a 2) * (b 2)))
Proof
Definitions occuring in Statement :
scalar-product: (a . b),
uall: ∀[x:A]. B[x],
top: Top,
infix_ap: x f y,
apply: f a,
natural_number: $n,
sqequal: s ~ t,
rng_times: *,
rng_zero: 0,
rng_plus: +r
Definitions unfolded in proof :
bfalse: ff,
btrue: tt,
ifthenelse: if b then t else f fi ,
subtract: n - m,
lt_int: i <z j,
ycomb: Y,
itop: Π(op,id) lb ≤ i < ub. E[i],
grp_id: e,
pi1: fst(t),
pi2: snd(t),
grp_op: *,
add_grp_of_rng: r↓+gp,
mon_itop: Π lb ≤ i < ub. E[i],
rng_sum: rng_sum,
scalar-product: (a . b),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
top_wf
Rules used in proof :
because_Cache,
hypothesisEquality,
thin,
isectElimination,
isect_memberEquality,
sqequalHypSubstitution,
extract_by_obid,
sqequalAxiom,
hypothesis,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[r,a,b:Top]. ((a . b) \msim{} ((0 +r ((a 0) * (b 0))) +r ((a 1) * (b 1))) +r ((a 2) * (b 2)))
Date html generated:
2018_05_21-PM-09_42_20
Last ObjectModification:
2017_12_21-PM-01_38_24
Theory : matrices
Home
Index