---

Step * of Lemma orthogonal-group_wf

∀[rv:InnerProductSpace]. (O(rv) ∈ s-Group)
BY
{ (ProveWfLemma
   THEN Try ((D 0 THEN Auto))
   THEN All (RWW "rv-perm-point rv-perm-id rv-perm-op rv-perm-inv")
   THEN Auto
   THEN Reduce 0
   THEN Auto
   THEN RepeatFor 2 (DVar `fg')
   THEN Try (RepeatFor 2 (DVar `y'))
   THEN All Reduce
   THEN EAuto 1) }

1
1. rv : InnerProductSpace
2. f1 : Point ⟶ Point
3. f2 : Point ⟶ Point
4. [%2] : (∀x:Point. f1 (f2 x) ≡ x)
∧ (∀x:Point. f2 (f1 x) ≡ x)
∧ (∀x,y:Point.  (f1 x # f1 y ⇒ x # y))
∧ (∀x,y:Point.  (f2 x # f2 y ⇒ x # y))
5. Orthogonal(f1)
⊢ Orthogonal(f2)

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  (O(rv)  \mmember{}  s-Group)


By

---

Latex:
(ProveWfLemma
  THEN  Try  ((D  0  THEN  Auto))
  THEN  All  (RWW  "rv-perm-point  rv-perm-id  rv-perm-op  rv-perm-inv")
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto
  THEN  RepeatFor  2  (DVar  `fg')
  THEN  Try  (RepeatFor  2  (DVar  `y'))
  THEN  All  Reduce
  THEN  EAuto  1)

---

Home Index