---

Step * of Lemma subtype-rv-isometry-group

∀[rv:InnerProductSpace]
  ({fg:Point ⟶ Point × (Point ⟶ Point)| let f,g = fg in (∀x:Point. f (g x) ≡ x) ∧ Isometry(f)}  ⊆r Point)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 (DVar `x')
   THEN All Reduce
   THEN RepUR ``ss-point rv-isometry-group mk-s-subgroup mk-s-group set-ss mk-ss`` 0
   THEN Fold `ss-point` 0
   THEN (RWO "rv-perm-point" 0 THENA Auto)
   THEN RepeatFor 2 ((MemTypeCD THEN Reduce 0 THEN Auto))
   THEN (FLemma `rv-isometry-inverse` [4;5] THENA Auto)
   THEN InstLemma `rv-isometry-implies-extensional` [⌜rv⌝;⌜x2⌝]⋅
   THEN Auto
   THEN InstLemma `rv-isometry-implies-extensional` [⌜rv⌝;⌜x1⌝]⋅
   THEN Auto
   THEN InstLemma `rv-isometry-injective` [⌜rv⌝;⌜x1⌝]⋅
   THEN Auto) }

---

Latex:

---

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)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (DVar  `x')
  THEN  All  Reduce
  THEN  RepUR  ``ss-point  rv-isometry-group  mk-s-subgroup  mk-s-group  set-ss  mk-ss``  0
  THEN  Fold  `ss-point`  0
  THEN  (RWO  "rv-perm-point"  0  THENA  Auto)
  THEN  RepeatFor  2  ((MemTypeCD  THEN  Reduce  0  THEN  Auto))
  THEN  (FLemma  `rv-isometry-inverse`  [4;5]  THENA  Auto)
  THEN  InstLemma  `rv-isometry-implies-extensional`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstLemma  `rv-isometry-implies-extensional`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstLemma  `rv-isometry-injective`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index