Nuprl Lemma : rv-ip-symmetry

[rv:InnerProductSpace]. ∀[x,y:Point].  (x ⋅ y ⋅ x)


Proof




Definitions occuring in Statement :  rv-ip: x ⋅ y inner-product-space: InnerProductSpace ss-point: Point req: y uall: [x:A]. B[x]
Definitions unfolded in proof :  uimplies: supposing a sq_stable: SqStable(P) squash: T rv-ip: x ⋅ y exists: x:A. B[x] all: x:A. B[x] so_apply: x[s] prop: implies:  Q so_lambda: λ2x.t[x] and: P ∧ Q guard: {T} btrue: tt ifthenelse: if then else fi  eq_atom: =a y subtype_rel: A ⊆B record-select: r.x record+: record+ inner-product-space: InnerProductSpace member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  separation-space_wf real-vector-space_wf inner-product-space_wf subtype_rel_transitivity inner-product-space_subtype rv-ip_wf req_witness sq_stable__req exists_wf int-to-real_wf rless_wf rv-0_wf ss-sep_wf rmul_wf rv-mul_wf radd_wf rv-add_wf req_wf ss-eq_wf all_wf real_wf real-vector-space_subtype1 ss-point_wf subtype_rel_self
Rules used in proof :  dependent_functionElimination isect_memberEquality independent_isectElimination instantiate productElimination independent_functionElimination imageElimination baseClosed imageMemberEquality Error :applyLambdaEquality,  rename setElimination natural_numberEquality functionExtensionality hypothesisEquality lambdaEquality productEquality because_Cache equalitySymmetry equalityTransitivity functionEquality setEquality isectElimination extract_by_obid tokenEquality applyEquality hypothesis thin dependentIntersectionEqElimination sqequalRule dependentIntersectionElimination sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[x,y:Point].    (x  \mcdot{}  y  =  y  \mcdot{}  x)



Date html generated: 2016_11_08-AM-09_14_47
Last ObjectModification: 2016_10_31-PM-04_27_48

Theory : inner!product!spaces


Home Index