---

Step * 1 of Lemma rv-orthog-ext_wf


1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. Orthogonal(f)
4. TERMOF{rv-orthogonal-implies-extensional-ext:o, 1:l, i:l} rv f ∈ ∀x,y:Point.  (f x # f y ⇒ x # y)
⊢ rv-orthog-ext(rv;f) ∈ ∀x,y:Point.  (f x # f y ⇒ x # y)
BY
{ (Subst' TERMOF{rv-orthogonal-implies-extensional-ext:o, 1:l, i:l} rv f ~ rv-orthog-ext(rv;f) -1 THEN Auto) }

1
.....equality..... 
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. Orthogonal(f)
4. TERMOF{rv-orthogonal-implies-extensional-ext:o, 1:l, i:l} rv f ∈ ∀x,y:Point.  (f x # f y ⇒ x # y)
⊢ TERMOF{rv-orthogonal-implies-extensional-ext:o, 1:l, i:l} rv f ~ rv-orthog-ext(rv;f)

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  f  :  Point  {}\mrightarrow{}  Point
3.  Orthogonal(f)
4.  TERMOF\{rv-orthogonal-implies-extensional-ext:o,  1:l,  i:l\}  rv  f  \mmember{}  \mforall{}x,y:Point.
                                                                                                                                            (f  x  \#  f  y  {}\mRightarrow{}  x  \#  y)
\mvdash{}  rv-orthog-ext(rv;f)  \mmember{}  \mforall{}x,y:Point.    (f  x  \#  f  y  {}\mRightarrow{}  x  \#  y)


By

---

Latex:
(Subst'  TERMOF\{rv-orthogonal-implies-extensional-ext:o,  1:l,  i:l\}  rv  f  \msim{}  rv-orthog-ext(rv;f)  -1
  THEN  Auto
  )

---

Home Index