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