Nuprl Lemma : subtype-rv-isometry-group

[rv:InnerProductSpace]
  ({fg:Point ⟶ Point × (Point ⟶ Point)| let f,g fg in (∀x:Point. (g x) ≡ x) ∧ Isometry(f)}  ⊆Point)


Proof




Definitions occuring in Statement :  rv-isometry-group: Isom(rv) rv-isometry: Isometry(f) inner-product-space: InnerProductSpace ss-eq: x ≡ y ss-point: Point subtype_rel: A ⊆B uall: [x:A]. B[x] all: x:A. B[x] and: P ∧ Q set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] spread: spread def product: x:A × B[x]
Definitions unfolded in proof :  guard: {T} pi1: fst(t) so_apply: x[s] so_lambda: λ2x.t[x] prop: implies:  Q uimplies: supposing a cand: c∧ B and: P ∧ Q btrue: tt mk-ss: mk-ss bfalse: ff ifthenelse: if then else fi  eq_atom: =a y top: Top all: x:A. B[x] mk-s-group: mk-s-group(ss; e; i; o; sep; invsep) set-ss: set-ss(ss;x.P[x]) mk-s-subgroup: mk-s-subgroup(sg;x.P[x]) ss-point: Point rv-isometry-group: Isom(rv) subtype_rel: A ⊆B 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 real-vector-space_subtype1 top_wf subtype_rel_product pi1_wf_top rv-isometry_wf ss-eq_wf all_wf ss-sep_wf rv-isometry-injective rv-isometry-implies-extensional rv-isometry-inverse ss-point_wf rv-perm-point rec_select_update_lemma
Rules used in proof :  axiomEquality instantiate setEquality functionEquality productEquality independent_functionElimination independent_isectElimination lambdaFormation independent_pairFormation because_Cache hypothesisEquality applyEquality functionExtensionality independent_pairEquality dependent_set_memberEquality isectElimination hypothesis voidEquality voidElimination isect_memberEquality dependent_functionElimination extract_by_obid sqequalRule sqequalHypSubstitution productElimination rename thin setElimination lambdaEquality cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[rv:InnerProductSpace]
    (\{fg:Point  {}\mrightarrow{}  Point  \mtimes{}  (Point  {}\mrightarrow{}  Point)|  let  f,g  =  fg  in  (\mforall{}x:Point.  f  (g  x)  \mequiv{}  x)  \mwedge{}  Isometry(f)\} 
          \msubseteq{}r  Point)



Date html generated: 2016_11_08-AM-09_21_12
Last ObjectModification: 2016_11_03-PM-00_12_07

Theory : inner!product!spaces


Home Index