P. 315 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31401-31500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nmoreltpnf 31401	The norm of any operator is real iff it is less than plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → ((𝑁‘𝑇) ∈ ℝ ↔ (𝑁‘𝑇) < +∞))
Theorem	nmogtmnf 31402	The norm of an operator is greater than minus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → -∞ < (𝑁‘𝑇))
Theorem	nmoolb 31403	A lower bound for an operator norm. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) ∧ (𝐴 ∈ 𝑋 ∧ (𝐿‘𝐴) ≤ 1)) → (𝑀‘(𝑇‘𝐴)) ≤ (𝑁‘𝑇))
Theorem	nmoubi 31404*	An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ*) → ((𝑁‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ 𝐴)))
Theorem	nmoub3i 31405*	An upper bound for an operator norm. (Contributed by NM, 12-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ (abs‘𝐴))
Theorem	nmoub2i 31406*	An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ 𝐴)
Theorem	nmobndi 31407*	Two ways to express that an operator is bounded. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ (𝑇:𝑋⟶𝑌 → ((𝑁‘𝑇) ∈ ℝ ↔ ∃𝑟 ∈ ℝ ∀𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 → (𝑀‘(𝑇‘𝑦)) ≤ 𝑟)))
Theorem	nmounbi 31408*	Two ways two express that an operator is unbounded. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ (𝑇:𝑋⟶𝑌 → ((𝑁‘𝑇) = +∞ ↔ ∀𝑟 ∈ ℝ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑟 < (𝑀‘(𝑇‘𝑦)))))
Theorem	nmounbseqi 31409*	An unbounded operator determines an unbounded sequence. (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 7-Apr-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝑁‘𝑇) = +∞) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ ((𝐿‘(𝑓‘𝑘)) ≤ 1 ∧ 𝑘 < (𝑀‘(𝑇‘(𝑓‘𝑘))))))
Theorem	nmounbseqiALT 31410*	Alternate shorter proof of nmounbseqi 31409 based on Axioms ax-reg 9613 and ax-ac2 10568 instead of ax-cc 10540. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝑁‘𝑇) = +∞) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ ((𝐿‘(𝑓‘𝑘)) ≤ 1 ∧ 𝑘 < (𝑀‘(𝑇‘(𝑓‘𝑘))))))
Theorem	nmobndseqi 31411*	A bounded sequence determines a bounded operator. (Contributed by NM, 18-Jan-2008.) (Revised by Mario Carneiro, 7-Apr-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝐿‘(𝑓‘𝑘)) ≤ 1) → ∃𝑘 ∈ ℕ (𝑀‘(𝑇‘(𝑓‘𝑘))) ≤ 𝑘)) → (𝑁‘𝑇) ∈ ℝ)
Theorem	nmobndseqiALT 31412*	Alternate shorter proof of nmobndseqi 31411 based on Axioms ax-reg 9613 and ax-ac2 10568 instead of ax-cc 10540. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝐿‘(𝑓‘𝑘)) ≤ 1) → ∃𝑘 ∈ ℕ (𝑀‘(𝑇‘(𝑓‘𝑘))) ≤ 𝑘)) → (𝑁‘𝑇) ∈ ℝ)
Theorem	bloval 31413*	The class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐵 = {𝑡 ∈ 𝐿 ∣ (𝑁‘𝑡) < +∞})
Theorem	isblo 31414	The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) < +∞)))
Theorem	isblo2 31415	The predicate "is a bounded linear operator." (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) ∈ ℝ)))
Theorem	bloln 31416	A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇 ∈ 𝐿)
Theorem	blof 31417	A bounded operator is an operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇:𝑋⟶𝑌)
Theorem	nmblore 31418	The norm of a bounded operator is a real number. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → (𝑁‘𝑇) ∈ ℝ)
Theorem	0ofval 31419	The zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑊)    &   ⊢ 𝑂 = (𝑈 0op 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑂 = (𝑋 × {𝑍}))
Theorem	0oval 31420	Value of the zero operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑊)    &   ⊢ 𝑂 = (𝑈 0op 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) = 𝑍)
Theorem	0oo 31421	The zero operator is an operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑍 = (𝑈 0op 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:𝑋⟶𝑌)
Theorem	0lno 31422	The zero operator is linear. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝑍 = (𝑈 0op 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐿)
Theorem	nmoo0 31423	The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑍 = (𝑈 0op 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = 0)
Theorem	0blo 31424	The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑍 = (𝑈 0op 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐵)
Theorem	nmlno0lem 31425	Lemma for nmlno0i 31426. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑍 = (𝑈 0op 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ 𝑇 ∈ 𝐿    &   ⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝑃 = (0vec‘𝑈)    &   ⊢ 𝑄 = (0vec‘𝑊)    &   ⊢ 𝐾 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    ⇒   ⊢ ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍)
Theorem	nmlno0i 31426	The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑍 = (𝑈 0op 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ (𝑇 ∈ 𝐿 → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍))
Theorem	nmlno0 31427	The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑍 = (𝑈 0op 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍))
Theorem	nmlnoubi 31428*	An upper bound for the operator norm of a linear operator, using only the properties of nonzero arguments. (Contributed by NM, 1-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝐾 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → (𝑁‘𝑇) ≤ 𝐴)
Theorem	nmlnogt0 31429	The norm of a nonzero linear operator is positive. (Contributed by NM, 10-Dec-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑍 = (𝑈 0op 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇 ≠ 𝑍 ↔ 0 < (𝑁‘𝑇)))
Theorem	lnon0 31430*	The domain of a nonzero linear operator contains a nonzero vector. (Contributed by NM, 15-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑂 = (𝑈 0op 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ 𝑇 ≠ 𝑂) → ∃𝑥 ∈ 𝑋 𝑥 ≠ 𝑍)
Theorem	nmblolbii 31431	A lower bound for the norm of a bounded linear operator. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ 𝑇 ∈ 𝐵    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴)))
Theorem	nmblolbi 31432	A lower bound for the norm of a bounded linear operator. (Contributed by NM, 10-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇 ∈ 𝐵 ∧ 𝐴 ∈ 𝑋) → (𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴)))
Theorem	isblo3i 31433*	The predicate "is a bounded linear operator." Definition 2.7-1 of [Kreyszig] p. 91. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))))
Theorem	blo3i 31434*	Properties that determine a bounded linear operator. (Contributed by NM, 13-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇 ∈ 𝐿 ∧ 𝐴 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝐴 · (𝑀‘𝑦))) → 𝑇 ∈ 𝐵)
Theorem	blometi 31435	Upper bound for the distance between the values of a bounded linear operator. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) → ((𝑇‘𝑃)𝐷(𝑇‘𝑄)) ≤ ((𝑁‘𝑇) · (𝑃𝐶𝑄)))
Theorem	blocnilem 31436	Lemma for blocni 31437 and lnocni 31438. If a linear operator is continuous at any point, it is bounded. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ 𝑇 ∈ 𝐿    &   ⊢ 𝑋 = (BaseSet‘𝑈)    ⇒   ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵)
Theorem	blocni 31437	A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ 𝑇 ∈ 𝐿    ⇒   ⊢ (𝑇 ∈ (𝐽 Cn 𝐾) ↔ 𝑇 ∈ 𝐵)
Theorem	lnocni 31438	If a linear operator is continuous at any point, it is continuous everywhere. Theorem 2.7-9(b) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ 𝑇 ∈ 𝐿    &   ⊢ 𝑋 = (BaseSet‘𝑈)    ⇒   ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ (𝐽 Cn 𝐾))
Theorem	blocn 31439	A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 25-Dec-2007.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ (𝑇 ∈ 𝐿 → (𝑇 ∈ (𝐽 Cn 𝐾) ↔ 𝑇 ∈ 𝐵))
Theorem	blocn2 31440	A bounded linear operator is continuous. (Contributed by NM, 25-Dec-2007.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑊)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ (𝑇 ∈ 𝐵 → 𝑇 ∈ (𝐽 Cn 𝐾))
Theorem	ajfval 31441*	The adjoint function. (Contributed by NM, 25-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑄 = (·𝑖OLD‘𝑊)    &   ⊢ 𝐴 = (𝑈 adj 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐴 = {⟨𝑡, 𝑠⟩ ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))})
Theorem	hmoval 31442*	The set of Hermitian (self-adjoint) operators on a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝐻 = (HmOp‘𝑈)    &   ⊢ 𝐴 = (𝑈 adj 𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐻 = {𝑡 ∈ dom 𝐴 ∣ (𝐴‘𝑡) = 𝑡})
Theorem	ishmo 31443	The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ 𝐻 = (HmOp‘𝑈)    &   ⊢ 𝐴 = (𝑈 adj 𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (𝑇 ∈ 𝐻 ↔ (𝑇 ∈ dom 𝐴 ∧ (𝐴‘𝑇) = 𝑇)))
19.5  Inner product (pre-Hilbert) spaces
19.5.1  Definition and basic properties
Syntax	ccphlo 31444	Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces).
class CPreHilOLD
Definition	df-ph 31445*	Define the class of all complex inner product spaces. An inner product space is a normed vector space whose norm satisfies the parallelogram law (a property that induces an inner product). Based on Exercise 4(b) of [ReedSimon] p. 63. The vector operation is 𝑔, the scalar product is 𝑠, and the norm is 𝑛. An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
⊢ CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔( -1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))})
Theorem	phnv 31446	Every complex inner product space is a normed complex vector space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec)
Theorem	phrel 31447	The class of all complex inner product spaces is a relation. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
⊢ Rel CPreHilOLD
Theorem	phnvi 31448	Every complex inner product space is a normed complex vector space. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ 𝑈 ∈ NrmCVec
Theorem	isphg 31449*	The predicate "is a complex inner product space." An inner product space is a normed vector space whose norm satisfies the parallelogram law. The vector (group) addition operation is 𝐺, the scalar product is 𝑆, and the norm is 𝑁. An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ∧ 𝑁 ∈ 𝐶) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ CPreHilOLD ↔ (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺( -1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))))
Theorem	phop 31450	A complex inner product space in terms of ordered pair components. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 = ⟨⟨𝐺, 𝑆⟩, 𝑁⟩)
19.5.2  Examples of pre-Hilbert spaces
Theorem	cncph 31451	The set of complex numbers is an inner product (pre-Hilbert) space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (Revised by Mario Carneiro, 7-Nov-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ 𝑈 ∈ CPreHilOLD
Theorem	elimph 31452	Hypothesis elimination lemma for complex inner product spaces to assist weak deduction theorem. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ if(𝐴 ∈ 𝑋, 𝐴, 𝑍) ∈ 𝑋
Theorem	elimphu 31453	Hypothesis elimination lemma for complex inner product spaces to assist weak deduction theorem. (Contributed by NM, 6-May-2007.) (New usage is discouraged.)
⊢ if(𝑈 ∈ CPreHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) ∈ CPreHilOLD
19.5.3  Properties of pre-Hilbert spaces
Theorem	isph 31454*	The predicate "is an inner product space." (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ CPreHilOLD ↔ (𝑈 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))
Theorem	phpar2 31455	The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝑀𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))))
Theorem	phpar 31456	The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))))
Theorem	ip0i 31457	A slight variant of Equation 6.46 of [Ponnusamy] p. 362, where 𝐽 is either 1 or -1 to represent +-1. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝐶 ∈ 𝑋    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐽 ∈ ℂ    ⇒   ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(𝐽𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺( -𝐽𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺(𝐽𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺( -1𝑆𝐵))𝐺( -𝐽𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(𝐽𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺( -𝐽𝑆𝐶)))↑2)))
Theorem	ip1ilem 31458	Lemma for ip1i 31459. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝐶 ∈ 𝑋    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐽 ∈ ℂ    ⇒   ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))
Theorem	ip1i 31459	Equation 6.47 of [Ponnusamy] p. 362. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝐶 ∈ 𝑋    ⇒   ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺( -1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))
Theorem	ip2i 31460	Equation 6.48 of [Ponnusamy] p. 362. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ ((2𝑆𝐴)𝑃𝐵) = (2 · (𝐴𝑃𝐵))
Theorem	ipdirilem 31461	Lemma for ipdiri 31462. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝐶 ∈ 𝑋    ⇒   ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))
Theorem	ipdiri 31462	Distributive law for inner product. Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)))
Theorem	ipasslem1 31463	Lemma for ipassi 31473. Show the inner product associative law for nonnegative integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋) → ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵)))
Theorem	ipasslem2 31464	Lemma for ipassi 31473. Show the inner product associative law for nonpositive integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋) → (( -𝑁𝑆𝐴)𝑃𝐵) = ( -𝑁 · (𝐴𝑃𝐵)))
Theorem	ipasslem3 31465	Lemma for ipassi 31473. Show the inner product associative law for all integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋) → ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵)))
Theorem	ipasslem4 31466	Lemma for ipassi 31473. Show the inner product associative law for positive integer reciprocals. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋) → (((1 / 𝑁)𝑆𝐴)𝑃𝐵) = ((1 / 𝑁) · (𝐴𝑃𝐵)))
Theorem	ipasslem5 31467	Lemma for ipassi 31473. Show the inner product associative law for rational numbers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ ((𝐶 ∈ ℚ ∧ 𝐴 ∈ 𝑋) → ((𝐶𝑆𝐴)𝑃𝐵) = (𝐶 · (𝐴𝑃𝐵)))
Theorem	ipasslem7 31468*	Lemma for ipassi 31473. Show that ((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵)) is continuous on ℝ. (Contributed by NM, 23-Aug-2007.) (Revised by Mario Carneiro, 6-May-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝐹 = (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵))))    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ 𝐹 ∈ (𝐽 Cn 𝐾)
Theorem	ipasslem8 31469*	Lemma for ipassi 31473. By ipasslem5 31467, 𝐹 is 0 for all ℚ; since it is continuous and ℚ is dense in ℝ by qdensere2 25146, we conclude 𝐹 is 0 for all ℝ. (Contributed by NM, 24-Aug-2007.) (Revised by Mario Carneiro, 6-May-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝐹 = (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵))))    ⇒   ⊢ 𝐹:ℝ⟶{0}
Theorem	ipasslem9 31470	Lemma for ipassi 31473. Conclude from ipasslem8 31469 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ (𝐶 ∈ ℝ → ((𝐶𝑆𝐴)𝑃𝐵) = (𝐶 · (𝐴𝑃𝐵)))
Theorem	ipasslem10 31471	Lemma for ipassi 31473. Show the inner product associative law for the imaginary number i. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((i𝑆𝐴)𝑃𝐵) = (i · (𝐴𝑃𝐵))
Theorem	ipasslem11 31472	Lemma for ipassi 31473. Show the inner product associative law for all complex numbers. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ (𝐶 ∈ ℂ → ((𝐶𝑆𝐴)𝑃𝐵) = (𝐶 · (𝐴𝑃𝐵)))
Theorem	ipassi 31473	Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)))
Theorem	dipdir 31474	Distributive law for inner product. Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)))
Theorem	dipdi 31475	Distributive law for inner product. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝐺𝐶)) = ((𝐴𝑃𝐵) + (𝐴𝑃𝐶)))
Theorem	ip2dii 31476	Inner product of two sums. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝐶 ∈ 𝑋    &   ⊢ 𝐷 ∈ 𝑋    ⇒   ⊢ ((𝐴𝐺𝐵)𝑃(𝐶𝐺𝐷)) = (((𝐴𝑃𝐶) + (𝐵𝑃𝐷)) + ((𝐴𝑃𝐷) + (𝐵𝑃𝐶)))
Theorem	dipass 31477	Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)))
Theorem	dipassr 31478	"Associative" law for second argument of inner product (compare dipass 31477). (Contributed by NM, 22-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑆𝐶)) = ((∗‘𝐵) · (𝐴𝑃𝐶)))
Theorem	dipassr2 31479	"Associative" law for inner product. Conjugate version of dipassr 31478. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃((∗‘𝐵)𝑆𝐶)) = (𝐵 · (𝐴𝑃𝐶)))
Theorem	dipsubdir 31480	Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) − (𝐵𝑃𝐶)))
Theorem	dipsubdi 31481	Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑀𝐶)) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶)))
Theorem	pythi 31482	The Pythagorean theorem for an arbitrary complex inner product (pre-Hilbert) space 𝑈. The square of the norm of the sum of two orthogonal vectors (i.e. whose inner product is 0) is the sum of the squares of their norms. Problem 2 in [Kreyszig] p. 135. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ ((𝐴𝑃𝐵) = 0 → ((𝑁‘(𝐴𝐺𝐵))↑2) = (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))
Theorem	siilem1 31483	Lemma for sii 31486. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ    &   ⊢ 0 ≤ (𝐶 · (𝐴𝑃𝐵))    ⇒   ⊢ ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	siilem2 31484	Lemma for sii 31486. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    ⇒   ⊢ ((𝐶 ∈ ℂ ∧ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ ∧ 0 ≤ (𝐶 · (𝐴𝑃𝐵))) → ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))))
Theorem	siii 31485	Inference from sii 31486. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐴 ∈ 𝑋    &   ⊢ 𝐵 ∈ 𝑋    ⇒   ⊢ (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))
Theorem	sii 31486	Obsolete version of ipcau 25589 as of 22-Sep-2024. Schwarz inequality. Part of Lemma 3-2.1(a) of [Kreyszig] p. 137. This is also called the Cauchy-Schwarz inequality by some authors and Bunjakovaskij-Cauchy-Schwarz inequality by others. See also Theorems bcseqi 31752, bcsiALT 31811, bcsiHIL 31812, csbren 25750. (Contributed by NM, 12-Jan-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)))
Theorem	ipblnfi 31487*	A function 𝐹 generated by varying the first argument of an inner product (with its second argument a fixed vector 𝐴) is a bounded linear functional, i.e. a bounded linear operator from the vector space to ℂ. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝐶 = ⟨⟨ + , · ⟩, abs⟩    &   ⊢ 𝐵 = (𝑈 BLnOp 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝑥𝑃𝐴))    ⇒   ⊢ (𝐴 ∈ 𝑋 → 𝐹 ∈ 𝐵)
Theorem	ip2eqi 31488*	Two vectors are equal iff their inner products with all other vectors are equal. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (𝑥𝑃𝐴) = (𝑥𝑃𝐵) ↔ 𝐴 = 𝐵))
Theorem	phoeqi 31489*	A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ 𝑆 = 𝑇))
Theorem	ajmoi 31490*	Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑈 ∈ CPreHilOLD    ⇒   ⊢ ∃*𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))
Theorem	ajfuni 31491	The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝐴 = (𝑈 adj 𝑊)    &   ⊢ 𝑈 ∈ CPreHilOLD    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ Fun 𝐴
Theorem	ajfun 31492	The adjoint function is a function. This is not immediately apparent from df-aj 31382 but results from the uniqueness shown by ajmoi 31490. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ 𝐴 = (𝑈 adj 𝑊)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec) → Fun 𝐴)
Theorem	ajval 31493*	Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑄 = (·𝑖OLD‘𝑊)    &   ⊢ 𝐴 = (𝑈 adj 𝑊)    ⇒   ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝐴‘𝑇) = (℩𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))))
19.6  Complex Banach spaces
19.6.1  Definition and basic properties
Syntax	ccbn 31494	Extend class notation with the class of all complex Banach spaces.
class CBan
Definition	df-cbn 31495	Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 25687 instead. (New usage is discouraged.)
⊢ CBan = {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))}
Theorem	iscbn 31496	A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 25689 instead. (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ CBan ↔ (𝑈 ∈ NrmCVec ∧ 𝐷 ∈ (CMet‘𝑋)))
Theorem	cbncms 31497	The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) Use bncmet 25698 (or preferably bncms 25695) instead. (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋))
Theorem	bnnv 31498	Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 25691 instead. (New usage is discouraged.)
⊢ (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)
Theorem	bnrel 31499	The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.)
⊢ Rel CBan
Theorem	bnsscmcl 31500	A subspace of a Banach space is a Banach space iff it is closed in the norm-induced metric of the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐻 = (SubSp‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    ⇒   ⊢ ((𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻) → (𝑊 ∈ CBan ↔ 𝑌 ∈ (Clsd‘𝐽)))