Nuprl Lemma : rv-ip-add-squared

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


Proof




Definitions occuring in Statement :  rv-ip: x ⋅ y inner-product-space: InnerProductSpace rv-add: y req: y rmul: b radd: b int-to-real: r(n) uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B implies:  Q guard: {T} uimplies: supposing a uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) all: x:A. B[x] req_int_terms: t1 ≡ t2 false: False not: ¬A top: Top
Lemmas referenced :  req_witness rv-ip_wf rv-add_wf inner-product-space_subtype radd_wf rmul_wf int-to-real_wf Error :ss-point_wf,  real-vector-space_subtype1 subtype_rel_transitivity inner-product-space_wf real-vector-space_wf Error :separation-space_wf,  req_functionality req_transitivity rv-ip-add radd_functionality rv-ip-add2 req_weakening rv-ip-symmetry itermSubtract_wf itermAdd_wf itermVar_wf itermMultiply_wf itermConstant_wf req-iff-rsub-is-0 real_polynomial_null istype-int real_term_value_sub_lemma istype-void real_term_value_add_lemma real_term_value_var_lemma real_term_value_mul_lemma real_term_value_const_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality hypothesis sqequalRule because_Cache natural_numberEquality independent_functionElimination inhabitedIsType isect_memberEquality_alt isectIsTypeImplies universeIsType instantiate independent_isectElimination productElimination dependent_functionElimination approximateComputation lambdaEquality_alt int_eqEquality voidElimination

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[x,y:Point(rv)].    (x  +  y\^{}2  =  ((x\^{}2  +  (r(2)  *  x  \mcdot{}  y))  +  y\^{}2))



Date html generated: 2020_05_20-PM-01_11_20
Last ObjectModification: 2019_12_09-PM-11_48_35

Theory : inner!product!spaces


Home Index