P. 282 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28101-28200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nvgt0 28101	A nonzero norm is positive. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴 ≠ 𝑍 ↔ 0 < (𝑁‘𝐴)))
Theorem	nv1 28102	From any nonzero vector, construct a vector whose norm is one. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍) → (𝑁‘((1 / (𝑁‘𝐴))𝑆𝐴)) = 1)
Theorem	nvop 28103	A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑈 = ⟨⟨𝐺, 𝑆⟩, 𝑁⟩)
18.3.2  Examples of normed complex vector spaces
Theorem	cnnv 28104	The set of complex numbers is a normed complex vector space. The vector operation is +, the scalar product is ·, and the norm function is abs. (Contributed by Steve Rodriguez, 3-Dec-2006.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ 𝑈 ∈ NrmCVec
Theorem	cnnvg 28105	The vector addition (group) operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ + = ( +𝑣 ‘𝑈)
Theorem	cnnvba 28106	The base set of the normed complex vector space of complex numbers. (Contributed by NM, 7-Nov-2007.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ ℂ = (BaseSet‘𝑈)
Theorem	cnnvs 28107	The scalar product operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ · = ( ·𝑠OLD ‘𝑈)
Theorem	cnnvnm 28108	The norm operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ abs = (normCV‘𝑈)
Theorem	cnnvm 28109	The vector subtraction operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    ⇒   ⊢ − = ( −𝑣 ‘𝑈)
Theorem	elimnv 28110	Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ if(𝐴 ∈ 𝑋, 𝐴, 𝑍) ∈ 𝑋
Theorem	elimnvu 28111	Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007.) (New usage is discouraged.)
⊢ if(𝑈 ∈ NrmCVec, 𝑈, ⟨⟨ + , · ⟩, abs⟩) ∈ NrmCVec
18.3.3  Induced metric of a normed complex vector space
Theorem	imsval 28112	Value of the induced metric of a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐷 = (𝑁 ∘ 𝑀))
Theorem	imsdval 28113	Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 27-Dec-2014.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴𝑀𝐵)))
Theorem	imsdval2 28114	Value of the distance function of the induced metric of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴𝐺(-1𝑆𝐵))))
Theorem	nvnd 28115	The norm of a normed complex vector space expressed in terms of the distance function of its induced metric. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐷𝑍))
Theorem	imsdf 28116	Mapping for the induced metric distance function of a normed complex vector space. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐷:(𝑋 × 𝑋)⟶ℝ)
Theorem	imsmetlem 28117	Lemma for imsmet 28118. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑀 = (inv‘𝐺)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    ⇒   ⊢ 𝐷 ∈ (Met‘𝑋)
Theorem	imsmet 28118	The induced metric of a normed complex vector space is a metric space. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
Theorem	imsxmet 28119	The induced metric of a normed complex vector space is an extended metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐷 = (IndMet‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋))
Theorem	cnims 28120	The metric induced on the complex numbers. cnmet 22983 proves that it is a metric. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by NM, 15-Jan-2008.) (New usage is discouraged.)
⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩    &   ⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ 𝐷 = (IndMet‘𝑈)
Theorem	vacn 28121	Vector addition is jointly continuous in both arguments. (Contributed by Jeff Hankins, 16-Jun-2009.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝐺 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
Theorem	nmcvcn 28122	The norm of a normed complex vector space is a continuous function. (Contributed by NM, 16-May-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.)
⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (topGen‘ran (,))    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑁 ∈ (𝐽 Cn 𝐾))
Theorem	nmcnc 28123	The norm of a normed complex vector space is a continuous function to ℂ. (For ℝ, see nmcvcn 28122.) (Contributed by NM, 12-Aug-2007.) (New usage is discouraged.)
⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑁 ∈ (𝐽 Cn 𝐾))
Theorem	smcnlem 28124*	Lemma for smcn 28125. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑈 ∈ NrmCVec    &   ⊢ 𝑇 = (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))    ⇒   ⊢ 𝑆 ∈ ((𝐾 ×t 𝐽) Cn 𝐽)
Theorem	smcn 28125	Scalar multiplication is jointly continuous in both arguments. (Contributed by NM, 16-Jun-2009.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑆 ∈ ((𝐾 ×t 𝐽) Cn 𝐽))
Theorem	vmcn 28126	Vector subtraction is jointly continuous in both arguments. (Contributed by Mario Carneiro, 6-May-2014.) (New usage is discouraged.)
⊢ 𝐶 = (IndMet‘𝑈)    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝑀 = ( −𝑣 ‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑀 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
18.3.4  Inner product
Syntax	cdip 28127	Extend class notation with the class inner product functions.
class ·𝑖OLD
Definition	df-dip 28128*	Define a function that maps a normed complex vector space to its inner product operation in case its norm satisfies the parallelogram identity (otherwise the operation is still defined, but not meaningful). Based on Exercise 4(a) of [ReedSimon] p. 63 and Theorem 6.44 of [Ponnusamy] p. 361. Vector addition is (1st ‘𝑤), the scalar product is (2nd ‘𝑤), and the norm is 𝑛. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.)
⊢ ·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD ‘𝑢)𝑦)))↑2)) / 4)))
Theorem	dipfval 28129*	The inner product function on a normed complex vector space. The definition is meaningful for vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law. (Contributed by NM, 10-Apr-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑃 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2)) / 4)))
Theorem	ipval 28130*	Value of the inner product. The definition is meaningful for normed complex vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law, although for convenience we define it for any normed complex vector space. The vector (group) addition operation is 𝐺, the scalar product is 𝑆, the norm is 𝑁, and the set of vectors is 𝑋. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) / 4))
Theorem	ipval2lem2 28131	Lemma for ipval3 28136. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℝ)
Theorem	ipval2lem3 28132	Lemma for ipval3 28136. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺𝐵))↑2) ∈ ℝ)
Theorem	ipval2lem4 28133	Lemma for ipval3 28136. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐶 ∈ ℂ) → ((𝑁‘(𝐴𝐺(𝐶𝑆𝐵)))↑2) ∈ ℂ)
Theorem	ipval2 28134	Expansion of the inner product value ipval 28130. (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 28135	Four times the inner product value ipval3 28136, 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 28136	Expansion of the inner product value ipval 28130. (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 28137	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 28138	Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (√‘(𝐴𝑃𝐴)))
Theorem	dipcl 28139	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 28140	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 28141	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 28142	An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑃𝐵) · (𝐵𝑃𝐴)) = ((abs‘(𝐴𝑃𝐵))↑2))
Theorem	diporthcom 28143	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 28144	Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑃 = (·𝑖OLD‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝑃𝑍) = 0)
Theorem	dip0l 28145	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 28146	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 28147	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 𝐾))
18.3.5  Subspaces
Syntax	css 28148	Extend class notation with the class of all subspaces of normed complex vector spaces.
class SubSp
Definition	df-ssp 28149*	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 28150*	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 28151	The predicate "is a subspace." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
⊢ 𝐺 = ( +𝑣 ‘𝑈)    &   ⊢ 𝐹 = ( +𝑣 ‘𝑊)    &   ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)    &   ⊢ 𝑅 = ( ·𝑠OLD ‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ NrmCVec ∧ (𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁))))
Theorem	sspid 28152	A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.)
⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → 𝑈 ∈ 𝐻)
Theorem	sspnv 28153	A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.)
⊢ 𝐻 = (SubSp‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ NrmCVec)
Theorem	sspba 28154	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 28155	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 28156	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 28157	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 28158	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 28159*	Lemma for sspm 28161 and others. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝐻 = (SubSp‘𝑈)    &   ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))    &   ⊢ (𝑊 ∈ NrmCVec → 𝐹:(𝑌 × 𝑌)⟶𝑅)    &   ⊢ (𝑈 ∈ NrmCVec → 𝐺:((BaseSet‘𝑈) × (BaseSet‘𝑈))⟶𝑆)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐹 = (𝐺 ↾ (𝑌 × 𝑌)))
Theorem	sspmval 28160	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 28161	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 28162	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 28163	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 28164	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 28165	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 28166	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 ∧ 𝑊 ∈ 𝐻) → 𝐶 = (𝐷 ↾ (𝑌 × 𝑌)))
18.4  Operators on complex vector spaces
18.4.1  Definitions and basic properties
Syntax	clno 28167	Extend class notation with the class of linear operators on normed complex vector spaces.
class LnOp
Syntax	cnmoo 28168	Extend class notation with the class of operator norms on normed complex vector spaces.
class normOpOLD
Syntax	cblo 28169	Extend class notation with the class of bounded linear operators on normed complex vector spaces.
class BLnOp
Syntax	c0o 28170	Extend class notation with the class of zero operators on normed complex vector spaces.
class 0op
Definition	df-lno 28171*	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‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))})
Definition	df-nmoo 28172*	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‘𝑤) ↑𝑚 (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < )))
Definition	df-blo 28173*	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 28174*	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 28175	Adjoint of an operator.
class adj
Syntax	chmo 28176	Set of Hermitional (self-adjoint) operators.
class HmOp
Definition	df-aj 28177*	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 28178*	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 28179*	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) → 𝐿 = {𝑡 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))})
Theorem	islno 28180*	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 28181	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 28182	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 28183	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 28184	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 28185	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 28186	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 28187	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 28188	Two ways to express a zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    ⇒   ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑇 = (𝑋 × {𝑍}) ↔ ran 𝑇 = {𝑍}))
Theorem	nmoofval 28189*	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) → 𝑁 = (𝑡 ∈ (𝑌 ↑𝑚 𝑋) ↦ sup({𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝐿‘𝑧) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑡‘𝑧)))}, ℝ*, < )))
Theorem	nmooval 28190*	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 28191*	The set in the supremum of the operator norm definition df-nmoo 28172 is a set of reals. (Contributed by NM, 13-Nov-2007.) (New usage is discouraged.)
⊢ 𝑌 = (BaseSet‘𝑊)    &   ⊢ 𝑁 = (normCV‘𝑊)    ⇒   ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝑀‘𝑧) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑧)))} ⊆ ℝ)
Theorem	nmosetn0 28192*	The set in the supremum of the operator norm definition df-nmoo 28172 is nonempty. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.)
⊢ 𝑋 = (BaseSet‘𝑈)    &   ⊢ 𝑍 = (0vec‘𝑈)    &   ⊢ 𝑀 = (normCV‘𝑈)    ⇒   ⊢ (𝑈 ∈ NrmCVec → (𝑁‘(𝑇‘𝑍)) ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝑀‘𝑦) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑦)))})
Theorem	nmoxr 28193	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 28194	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 28195	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 28196	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 28197	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 28198	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 28199*	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 28200*	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‘𝐴))