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	ipidsq 30801	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 30802	Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (√‘(𝐴𝑃𝐴)))
Theorem	dipcl 30803	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 30804	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 30805	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 30806	An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑃𝐵) · (𝐵𝑃𝐴)) = ((abs‘(𝐴𝑃𝐵))↑2))
Theorem	diporthcom 30807	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 30808	Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = 0)
Theorem	dip0l 30809	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 30810	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 30811	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 30812	Extend class notation with the class of all subspaces of normed complex vector spaces.
class SubSp
Definition	df-ssp 30813*	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 30814*	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 30815	The predicate "is a subspace." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐹 = ( +𝑣 ‘𝑊)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ (𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁))))
Theorem	sspid 30816	A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑈 ∈ 𝐻)
Theorem	sspnv 30817	A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.)
⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec)
Theorem	sspba 30818	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 30819	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 30820	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 30821	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 30822	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 30823*	Lemma for sspm 30825 and others. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    &   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))    &   ⊢ (𝑊 ∈ NrmCVec → 𝐹:(𝑌 × 𝑌)⟶𝑅)    &   ⊢ (𝑈 ∈ NrmCVec → 𝐺:((BaseSet‘𝑈) × (BaseSet‘𝑈))⟶𝑆)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌)))
Theorem	sspmval 30824	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 30825	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 30826	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 30827	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 30828	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 30829	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 30830	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 30831	Extend class notation with the class of linear operators on normed complex vector spaces.
class LnOp
Syntax	cnmoo 30832	Extend class notation with the class of operator norms on normed complex vector spaces.
class normOpOLD
Syntax	cblo 30833	Extend class notation with the class of bounded linear operators on normed complex vector spaces.
class BLnOp
Syntax	c0o 30834	Extend class notation with the class of zero operators on normed complex vector spaces.
class 0op
Definition	df-lno 30835*	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 30836*	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 30837*	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 30838*	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 30839	Adjoint of an operator.
class adj
Syntax	chmo 30840	Set of Hermitional (self-adjoint) operators.
class HmOp
Definition	df-aj 30841*	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 30842*	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 30843*	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 30844*	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 30845	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 30846	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 30847	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 30848	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 30849	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 30850	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 30851	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 30852	Two ways to express a zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑇 = (𝑋 × {𝑍}) ↔ ran 𝑇 = {𝑍}))
Theorem	nmoofval 30853*	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 30854*	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 30855*	The set in the supremum of the operator norm definition df-nmoo 30836 is a set of reals. (Contributed by NM, 13-Nov-2007.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑊)    ⇒   ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝑀‘𝑧) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑧)))} ⊆ ℝ)
Theorem	nmosetn0 30856*	The set in the supremum of the operator norm definition df-nmoo 30836 is nonempty. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (𝑁‘(𝑇‘𝑍)) ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝑀‘𝑦) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑦)))})
Theorem	nmoxr 30857	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 30858	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 30859	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 30860	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 30861	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 30862	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 30863*	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 30864*	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 30865*	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 30866*	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 30867*	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 30868*	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 30869*	Alternate shorter proof of nmounbseqi 30868 based on Axioms ax-reg 9498 and ax-ac2 10374 instead of ax-cc 10346. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝑁‘𝑇) = +∞) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ ((𝐿‘(𝑓‘𝑘)) ≤ 1 ∧ 𝑘 < (𝑀‘(𝑇‘(𝑓‘𝑘))))))
Theorem	nmobndseqi 30870*	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 30871*	Alternate shorter proof of nmobndseqi 30870 based on Axioms ax-reg 9498 and ax-ac2 10374 instead of ax-cc 10346. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐿 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑊 ∈ NrmCVec    ⇒   ⊢ ((𝑇:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝐿‘(𝑓‘𝑘)) ≤ 1) → ∃𝑘 ∈ ℕ (𝑀‘(𝑇‘(𝑓‘𝑘))) ≤ 𝑘)) → (𝑁‘𝑇) ∈ ℝ)
Theorem	bloval 30872*	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 30873	The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) < +∞)))
Theorem	isblo2 30874	The predicate "is a bounded linear operator." (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) ∈ ℝ)))
Theorem	bloln 30875	A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝐿 = (𝑈 LnOp 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇 ∈ 𝐿)
Theorem	blof 30876	A bounded operator is an operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇:𝑋⟶𝑌)
Theorem	nmblore 30877	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 30878	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 30879	Value of the zero operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑊)    &   ⊢ 𝑂 = (𝑈 0op 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) = 𝑍)
Theorem	0oo 30880	The zero operator is an operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑍 = (𝑈 0op 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:𝑋⟶𝑌)
Theorem	0lno 30881	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 30882	The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.)
⊢ 𝑁 = (𝑈 normOpOLD 𝑊)    &   ⊢ 𝑍 = (𝑈 0op 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = 0)
Theorem	0blo 30883	The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑍 = (𝑈 0op 𝑊)    &   ⊢ 𝐵 = (𝑈 BLnOp 𝑊)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐵)
Theorem	nmlno0lem 30884	Lemma for nmlno0i 30885. (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 30885	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 30886	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 30887*	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 30888	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 30889*	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 30890	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 30891	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 30892*	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 30893*	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 30894	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 30895	Lemma for blocni 30896 and lnocni 30897. 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 30896	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 30897	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 30898	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 30899	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 30900*	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) → 𝐴 = {⟨𝑡, 𝑠⟩ ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))})