Nuprl Lemma : rv-ip-add2

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


Proof




Definitions occuring in Statement :  rv-ip: x ⋅ y inner-product-space: InnerProductSpace rv-add: y req: y radd: b uall: [x:A]. B[x]
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)
Lemmas referenced :  req_witness rv-ip_wf rv-add_wf inner-product-space_subtype radd_wf Error :ss-point_wf,  real-vector-space_subtype1 subtype_rel_transitivity inner-product-space_wf real-vector-space_wf Error :separation-space_wf,  rv-ip-add req_functionality rv-ip-symmetry radd_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality hypothesis sqequalRule independent_functionElimination inhabitedIsType isect_memberEquality_alt because_Cache isectIsTypeImplies universeIsType instantiate independent_isectElimination productElimination

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



Date html generated: 2020_05_20-PM-01_10_59
Last ObjectModification: 2019_12_09-PM-11_53_23

Theory : inner!product!spaces


Home Index