P. 309 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30801-30900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ipval2lem3 30801	Lemma for ipval3 30805. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺𝐵))↑2) ∈ ℝ)
Theorem	ipval2lem4 30802	Lemma for ipval3 30805. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℂ)
Theorem	ipval2 30803	Expansion of the inner product value ipval 30799. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐵)))↑2)))) / 4))
Theorem	4ipval2 30804	Four times the inner product value ipval3 30805, useful for simplifying certain proofs. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (4 · (𝐴𝑃𝐵)) = ((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐵)))↑2)))))
Theorem	ipval3 30805	Expansion of the inner product value ipval 30799. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝑀𝐵))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝑀(i𝑆𝐵)))↑2)))) / 4))
Theorem	ipidsq 30806	The inner product of a vector with itself is the square of the vector's norm. Equation I4 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝐴) = ((𝑁‘𝐴)↑2))
Theorem	ipnm 30807	Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (√‘(𝐴𝑃𝐴)))
Theorem	dipcl 30808	An inner product is a complex number. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) ∈ ℂ)
Theorem	ipf 30809	Mapping for the inner product operation. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑃:(𝑋 × 𝑋)⟶ℂ)
Theorem	dipcj 30810	The complex conjugate of an inner product reverses its arguments. Equation I1 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∗‘(𝐴𝑃𝐵)) = (𝐵𝑃𝐴))
Theorem	ipipcj 30811	An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑃𝐵) · (𝐵𝑃𝐴)) = ((abs‘(𝐴𝑃𝐵))↑2))
Theorem	diporthcom 30812	Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑃𝐵) = 0 ↔ (𝐵𝑃𝐴) = 0))
Theorem	dip0r 30813	Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = 0)
Theorem	dip0l 30814	Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑍𝑃𝐴) = 0)
Theorem	ipz 30815	The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → ((𝐴𝑃𝐴) = 0 ↔ 𝐴 = 𝑍))
Theorem	dipcn 30816	Inner product is jointly continuous in both arguments. (Contributed by NM, 21-Aug-2007.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝑃 = (·𝑖OLD‘𝑈)    &   ⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑃 ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
19.3.5  Subspaces
Syntax	css 30817	Extend class notation with the class of all subspaces of normed complex vector spaces.
class SubSp
Definition	df-ssp 30818*	Define the class of all subspaces of normed complex vector spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ SubSp = (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ ( +𝑣 ‘𝑢) ∧ ( ·𝑠OLD ‘𝑤) ⊆ ( ·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆ (normCV‘𝑢))})
Theorem	sspval 30819*	The set of all subspaces of a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐻 = {𝑤 ∈ NrmCVec ∣ (( +𝑣 ‘𝑤) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁)})
Theorem	isssp 30820	The predicate "is a subspace." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐹 = ( +𝑣 ‘𝑊)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ (𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁))))
Theorem	sspid 30821	A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑈 ∈ 𝐻)
Theorem	sspnv 30822	A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.)
⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec)
Theorem	sspba 30823	The base set of a subspace is included in the parent base set. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑌 ⊆ 𝑋)
Theorem	sspg 30824	Vector addition on a subspace is a restriction of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐹 = ( +𝑣 ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌)))
Theorem	sspgval 30825	Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐹 = ( +𝑣 ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌)) → (𝐴𝐹𝐵) = (𝐴𝐺𝐵))
Theorem	ssps 30826	Scalar multiplication on a subspace is a restriction of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑅 = (𝑆 ↾ (ℂ × 𝑌)))
Theorem	sspsval 30827	Scalar multiplication on a subspace in terms of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑌)) → (𝐴𝑅𝐵) = (𝐴𝑆𝐵))
Theorem	sspmlem 30828*	Lemma for sspm 30830 and others. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    &   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))    &   ⊢ (𝑊 ∈ NrmCVec → 𝐹:(𝑌 × 𝑌)⟶𝑅)    &   ⊢ (𝑈 ∈ NrmCVec → 𝐺:((BaseSet‘𝑈) × (BaseSet‘𝑈))⟶𝑆)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌)))
Theorem	sspmval 30829	Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝐿 = ( −𝑣 ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌)) → (𝐴𝐿𝐵) = (𝐴𝑀𝐵))
Theorem	sspm 30830	Vector subtraction on a subspace is a restriction of vector subtraction on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝐿 = ( −𝑣 ‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐿 = (𝑀 ↾ (𝑌 × 𝑌)))
Theorem	sspz 30831	The zero vector of a subspace is the same as the parent's. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑄 = (0vec‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑄 = 𝑍)
Theorem	sspn 30832	The norm on a subspace is a restriction of the norm on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑀 = (𝑁 ↾ 𝑌))
Theorem	sspnval 30833	The norm on a subspace in terms of the norm on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ∧ 𝐴 ∈ 𝑌) → (𝑀‘𝐴) = (𝑁‘𝐴))
Theorem	sspimsval 30834	The induced metric on a subspace in terms of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐶 = (IndMet‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌)) → (𝐴𝐶𝐵) = (𝐴𝐷𝐵))
Theorem	sspims 30835	The induced metric on a subspace is a restriction of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝐶 = (IndMet‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐶 = (𝐷 ↾ (𝑌 × 𝑌)))
19.4  Operators on complex vector spaces
19.4.1  Definitions and basic properties
Syntax	clno 30836	Extend class notation with the class of linear operators on normed complex vector spaces.
class LnOp
Syntax	cnmoo 30837	Extend class notation with the class of operator norms on normed complex vector spaces.
class normOpOLD
Syntax	cblo 30838	Extend class notation with the class of bounded linear operators on normed complex vector spaces.
class BLnOp
Syntax	c0o 30839	Extend class notation with the class of zero operators on normed complex vector spaces.
class 0op
Definition	df-lno 30840*	Define the class of linear operators between two normed complex vector spaces. In the literature, an operator may be a partial function, i.e., the domain of an operator is not necessarily the entire vector space. However, since the domain of a linear operator is a vector subspace, we define it with a complete function for convenience and will use subset relations to specify the partial function case. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
⊢ LnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))})
Definition	df-nmoo 30841*	Define the norm of an operator between two normed complex vector spaces. This definition produces an operator norm function for each pair of vector spaces ⟨𝑢, 𝑤⟩. Based on definition of linear operator norm in [AkhiezerGlazman] p. 39, although we define it for all operators for convenience. It isn't necessarily meaningful for nonlinear operators, since it doesn't take into account operator values at vectors with norm greater than 1. See Equation 2 of [Kreyszig] p. 92 for a definition that does (although it ignores the value at the zero vector). However, operator norms are rarely if ever used for nonlinear operators. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
⊢ normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))
Definition	df-blo 30842*	Define the class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
⊢ BLnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞})
Definition	df-0o 30843*	Define the zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.)
⊢ 0op = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ ((BaseSet‘𝑢) × {(0vec‘𝑤)}))
Syntax	caj 30844	Adjoint of an operator.
class adj
Syntax	chmo 30845	Set of Hermitional (self-adjoint) operators.
class HmOp
Definition	df-aj 30846*	Define the adjoint of an operator (if it exists). The domain of 𝑈adj𝑊 is the set of all operators from 𝑈 to 𝑊 that have an adjoint. Definition 3.9-1 of [Kreyszig] p. 196, although we don't require that 𝑈 and 𝑊 be Hilbert spaces nor that the operators be linear. Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)
⊢ adj = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))})
Definition	df-hmo 30847*	Define the set of Hermitian (self-adjoint) operators on a normed complex vector space (normally a Hilbert space). Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ HmOp = (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡})
Theorem	lnoval 30848*	The set of 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.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐻 = ( +𝑣 ‘𝑊)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐿 = {𝑡 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))})
Theorem	islno 30849*	The predicate "is a linear operator." (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐻 = ( +𝑣 ‘𝑊)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐿 ↔ (𝑇:𝑋⟶𝑌 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑇‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑇‘𝑦))𝐻(𝑇‘𝑧)))))
Theorem	lnolin 30850	Basic linearity property of a linear operator. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐻 = ( +𝑣 ‘𝑊)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝑇‘((𝐴𝑅𝐵)𝐺𝐶)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶)))
Theorem	lnof 30851	A linear operator is a mapping. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 18-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑌)
Theorem	lno0 30852	The value of a linear operator at zero is zero. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 18-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑄 = (0vec‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘𝑄) = 𝑍)
Theorem	lnocoi 30853	The composition of two linear operators is linear. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝑀 = (𝑊 LnOp 𝑋)    &   ⊢ 𝑁 = (𝑈 LnOp 𝑋)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    &   ⊢ 𝑋 ∈ NrmCVec    &   ⊢ 𝑆 ∈ 𝐿    &   ⊢ 𝑇 ∈ 𝑀    ⇒   ⊢ (𝑇 ∘ 𝑆) ∈ 𝑁
Theorem	lnoadd 30854	Addition property of a linear operator. (Contributed by NM, 7-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐻 = ( +𝑣 ‘𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘(𝐴𝐺𝐵)) = ((𝑇‘𝐴)𝐻(𝑇‘𝐵)))
Theorem	lnosub 30855	Subtraction property of a linear operator. (Contributed by NM, 7-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = ( −𝑣 ‘𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘(𝐴𝑀𝐵)) = ((𝑇‘𝐴)𝑁(𝑇‘𝐵)))
Theorem	lnomul 30856	Scalar multiplication property of a linear operator. (Contributed by NM, 5-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → (𝑇‘(𝐴𝑅𝐵)) = (𝐴𝑆(𝑇‘𝐵)))
Theorem	nvo00 30857	Two ways to express a zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑇 = (𝑋 × {𝑍}) ↔ ran 𝑇 = {𝑍}))
Theorem	nmoofval 30858*	The operator norm function. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑁 = (𝑡 ∈ (𝑌 ↑m 𝑋) ↦ sup({𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝐿‘𝑧) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑡‘𝑧)))}, ℝ*, < )))
Theorem	nmooval 30859*	The operator norm function. (Contributed by NM, 27-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑁‘𝑇) = sup({𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝐿‘𝑧) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, < ))
Theorem	nmosetre 30860*	The set in the supremum of the operator norm definition df-nmoo 30841 is a set of reals. (Contributed by NM, 13-Nov-2007.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑊)    ⇒   ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝑀‘𝑧) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑧)))} ⊆ ℝ)
Theorem	nmosetn0 30861*	The set in the supremum of the operator norm definition df-nmoo 30841 is nonempty. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (𝑁‘(𝑇‘𝑍)) ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝑀‘𝑦) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑦)))})
Theorem	nmoxr 30862	The norm of an operator is an extended real. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑁‘𝑇) ∈ ℝ*)
Theorem	nmooge0 30863	The norm of an operator is nonnegative. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → 0 ≤ (𝑁‘𝑇))
Theorem	nmorepnf 30864	The norm of an operator is either real or plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → ((𝑁‘𝑇) ∈ ℝ ↔ (𝑁‘𝑇) ≠ +∞))
Theorem	nmoreltpnf 30865	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 30866	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 30867	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 30868*	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 30869*	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 30870*	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 30871*	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 30872*	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 30873*	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 30874*	Alternate shorter proof of nmounbseqi 30873 based on Axioms ax-reg 9504 and ax-ac2 10383 instead of ax-cc 10355. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝑁‘𝑇) = +∞) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ ((𝐿‘(𝑓‘𝑘)) ≤ 1 ∧ 𝑘 < (𝑀‘(𝑇‘(𝑓‘𝑘))))))
Theorem	nmobndseqi 30875*	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 30876*	Alternate shorter proof of nmobndseqi 30875 based on Axioms ax-reg 9504 and ax-ac2 10383 instead of ax-cc 10355. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝐿‘(𝑓‘𝑘)) ≤ 1) → ∃𝑘 ∈ ℕ (𝑀‘(𝑇‘(𝑓‘𝑘))) ≤ 𝑘)) → (𝑁‘𝑇) ∈ ℝ)
Theorem	bloval 30877*	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 30878	The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) < +∞)))
Theorem	isblo2 30879	The predicate "is a bounded linear operator." (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) ∈ ℝ)))
Theorem	bloln 30880	A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇 ∈ 𝐿)
Theorem	blof 30881	A bounded operator is an operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇:𝑋⟶𝑌)
Theorem	nmblore 30882	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 30883	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 30884	Value of the zero operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑊)    &   ⊢ 𝑂 = (𝑈 0op 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) = 𝑍)
Theorem	0oo 30885	The zero operator is an operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑍 = (𝑈 0op 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:𝑋⟶𝑌)
Theorem	0lno 30886	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 30887	The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑍 = (𝑈 0op 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = 0)
Theorem	0blo 30888	The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑍 = (𝑈 0op 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐵)
Theorem	nmlno0lem 30889	Lemma for nmlno0i 30890. (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 30890	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 30891	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 30892*	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 30893	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 30894*	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 30895	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 30896	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 30897*	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 30898*	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 30899	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 30900	Lemma for blocni 30901 and lnocni 30902. 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 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵)