mmtheorems98 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 9701-9800 - Page 98 of 175

Type	Label	Description
Statement
Theorem	4ipval3 9701	Four times the inner product value ipval3 9698, useful for simplifying certain proofs.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   &   |- P = (.i` U)   &   |- M = (-v` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (4 x. (APB)) = ((((N` (AGB))^2) - ((N` (AMB))^2)) + (_i x. (((N` (AG(_iSB)))^2) - ((N` (AM(_iSB)))^2)))))
Theorem	ipid 9702	The inner product of a vector with itself is the square of the vector's norm. Equation I4 of [Ponnusamy] p. 362.
|- X = (BaseSet` U)   &   |- N = (norm` U)   &   |- P = (.i` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (APA) = ((N` A)^2))
Theorem	ipnm 9703	Norm expressed in terms of inner product.
|- X = (BaseSet` U)   &   |- N = (norm` U)   &   |- P = (.i` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (N` A) = (sqr` (APA)))
Theorem	ipcl 9704	An inner product is a complex number.
|- X = (BaseSet` U)   &   |- P = (.i` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) e. CC)
Theorem	ipf 9705	Mapping for the inner product operation.
|- X = (BaseSet` U)   &   |- P = (.i` U)   =>   |- (U e. NrmCVec -> P:(X X. X)-->CC)
Theorem	ipcj 9706	The complex conjugate of an inner product reverses its arguments. Equation I1 of [Ponnusamy] p. 362.
|- X = (BaseSet` U)   &   |- P = (.i` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (*` (APB)) = (BPA))
Theorem	ipipcj 9707	An inner product times its conjugate.
|- X = (BaseSet` U)   &   |- P = (.i` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((APB) x. (BPA)) = ((abs` (APB))^2))
Theorem	iporthcom 9708	Orthogonality (meaning inner product is 0) is commutative.
|- X = (BaseSet` U)   &   |- P = (.i` U)   =>   |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((APB) = 0 <-> (BPA) = 0))
Theorem	ip0r 9709	Inner product with a zero second argument.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   &   |- P = (.i` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (APZ) = 0)
Theorem	ip0l 9710	Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   &   |- P = (.i` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> (ZPA) = 0)
Theorem	ipz 9711	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.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   &   |- P = (.i` U)   =>   |- ((U e. NrmCVec /\ A e. X) -> ((APA) = 0 <-> A = Z))
Theorem	ip1cnilem1 9712	Lemma for ip1cni 9718.
Theorem	ip1cnilem2 9713	Lemma for ip1cni 9718.
Theorem	ip1cnilem3 9714	Lemma for ip1cni 9718.
Theorem	ip1cnilem4 9715	Lemma for ip1cni 9718.
Theorem	ip1cnilem5 9716	Lemma for ip1cni 9718.
Theorem	ip1cnilem6 9717	Lemma for ip1cni 9718.
Theorem	ip1cni 9718	Inner product is continuous in its first operand.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- P = (.i` U)   &   |- C = (IndMet` U)   &   |- D = (abs o. - )   &   |- J = (Open` C)   &   |- K = (Open` D)   &   |- F = {<.w, v>. | (w e. X /\ v = (wPA))}   &   |- U e. NrmCVec   &   |- A e. X   =>   |- F e. (J Cn K)
Subspaces
Syntax	css 9719	Extend class notation with the class of all subspaces of complex normed vector spaces.
class SubSp
Definition	df-ssp 9720	Define the class of all subspaces of complex normed vector spaces.
|- SubSp = {<.u, s>. | (u e. NrmCVec /\ s = {w e. NrmCVec | ((+v` w) C_ (+v` u) /\ (.s` w) C_ (.s` u) /\ (norm` w) C_ (norm` u))})}
Theorem	sspval 9721	The set of all subspaces of a normed complex vector space.
|- G = (+v` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   &   |- H = (SubSp` U)   =>   |- (U e. NrmCVec -> H = {w e. NrmCVec | ((+v` w) C_ G /\ (.s` w) C_ S /\ (norm` w) C_ N)})
Theorem	isssp 9722	The predicate "is a subspace."
|- G = (+v` U)   &   |- F = (+v` W)   &   |- S = (.s` U)   &   |- R = (.s` W)   &   |- N = (norm` U)   &   |- M = (norm` W)   &   |- H = (SubSp` U)   =>   |- (U e. NrmCVec -> (W e. H <-> (W e. NrmCVec /\ (F C_ G /\ R C_ S /\ M C_ N))))
Theorem	sspid 9723	A normed complex vector space is a subspace of itself.
|- H = (SubSp` U)   =>   |- (U e. NrmCVec -> U e. H)
Theorem	sspnv 9724	A subspace is a normed complex vector space.
|- H = (SubSp` U)   =>   |- ((U e. NrmCVec /\ W e. H) -> W e. NrmCVec)
Theorem	sspba 9725	The base set of a subspace is included in the parent base set.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- H = (SubSp` U)   =>   |- ((U e. NrmCVec /\ W e. H) -> Y C_ X)
Theorem	sspg 9726	Vector addition on a subspace is a restriction of vector addition on the parent space.
|- Y = (BaseSet` W)   &   |- G = (+v` U)   &   |- F = (+v` W)   &   |- H = (SubSp` U)   =>   |- ((U e. NrmCVec /\ W e. H) -> F = (G |` (Y X. Y)))
Theorem	sspgval 9727	Vector addition on a subspace in terms of vector addition on the parent space.
|- Y = (BaseSet` W)   &   |- G = (+v` U)   &   |- F = (+v` W)   &   |- H = (SubSp` U)   =>   |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ B e. Y)) -> (AFB) = (AGB))
Theorem	ssps 9728	Scalar multiplication on a subspace is a restriction of scalar multiplication on the parent space.
|- Y = (BaseSet` W)   &   |- S = (.s` U)   &   |- R = (.s` W)   &   |- H = (SubSp` U)   =>   |- ((U e. NrmCVec /\ W e. H) -> R = (S |` (CC X. Y)))
Theorem	sspsval 9729	Scalar multiplication on a subspace in terms of scalar multiplication on the parent space.
|- Y = (BaseSet` W)   &   |- S = (.s` U)   &   |- R = (.s` W)   &   |- H = (SubSp` U)   =>   |- (((U e. NrmCVec /\ W e. H) /\ (A e. CC /\ B e. Y)) -> (ARB) = (ASB))
Theorem	sspmlem 9730	Lemma for sspm 9732 and others.
Theorem	sspmval 9731	Vector addition on a subspace in terms of vector addition on the parent space.
|- Y = (BaseSet` W)   &   |- M = (-v` U)   &   |- L = (-v` W)   &   |- H = (SubSp` U)   =>   |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ B e. Y)) -> (ALB) = (AMB))
Theorem	sspm 9732	Vector subtraction on a subspace is a restriction of vector subtraction on the parent space.
|- Y = (BaseSet` W)   &   |- M = (-v` U)   &   |- L = (-v` W)   &   |- H = (SubSp` U)   =>   |- ((U e. NrmCVec /\ W e. H) -> L = (M |` (Y X. Y)))
Theorem	sspz 9733	The zero vector of a subspace is the same as the parent's.
|- Z = (0v` U)   &   |- Q = (0v` W)   &   |- H = (SubSp` U)   =>   |- ((U e. NrmCVec /\ W e. H) -> Q = Z)
Theorem	sspn 9734	The norm on a subspace is a restriction of the norm on the parent space.
|- Y = (BaseSet` W)   &   |- N = (norm` U)   &   |- M = (norm` W)   &   |- H = (SubSp` U)   =>   |- ((U e. NrmCVec /\ W e. H) -> M = (N |` Y))
Theorem	sspnval 9735	The norm on a subspace in terms of the norm on the parent space.
|- Y = (BaseSet` W)   &   |- N = (norm` U)   &   |- M = (norm` W)   &   |- H = (SubSp` U)   =>   |- ((U e. NrmCVec /\ W e. H /\ A e. Y) -> (M` A) = (N` A))
Theorem	sspival 9736	The inner product on a subspace in terms of the inner product on the parent space.
|- Y = (BaseSet` W)   &   |- P = (.i` U)   &   |- Q = (.i` W)   &   |- H = (SubSp` U)   =>   |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ B e. Y)) -> (AQB) = (APB))
Theorem	sspi 9737	The inner product on a subspace is a restriction of the inner product on the parent space.
|- Y = (BaseSet` W)   &   |- P = (.i` U)   &   |- Q = (.i` W)   &   |- H = (SubSp` U)   =>   |- ((U e. NrmCVec /\ W e. H) -> Q = (P |` (Y X. Y)))
Theorem	sspimsval 9738	The induced metric on a subspace in terms of the induced metric on the parent space.
|- Y = (BaseSet` W)   &   |- D = (IndMet` U)   &   |- C = (IndMet` W)   &   |- H = (SubSp` U)   =>   |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ B e. Y)) -> (ACB) = (ADB))
Theorem	sspims 9739	The induced metric on a subspace is a restriction of the induced metric on the parent space.
|- Y = (BaseSet` W)   &   |- D = (IndMet` U)   &   |- C = (IndMet` W)   &   |- H = (SubSp` U)   =>   |- ((U e. NrmCVec /\ W e. H) -> C = (D |` (Y X. Y)))
Operators on complex vector spaces
Definitions and basic properties
Syntax	clno 9740	Extend class notation with the class of linear operators on normed complex vector spaces.
class LnOp
Syntax	cnmo 9741	Extend class notation with the class of operator norms on normed complex vector spaces.
class normOp
Syntax	cblo 9742	Extend class notation with the class of bounded linear operators on normed complex vector spaces.
class BLnOp
Syntax	c0o 9743	Extend class notation with the class of zero operators on normed complex vector spaces.
class 0op
Definition	df-lno 9744	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.
|- LnOp = {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t | (t:(BaseSet` u)-->(BaseSet` w) /\ A.x e. (BaseSet` u)A.y e. CC A.z e. (BaseSet` u)(t` (x(+v` u)(y(.s` u)z))) = ((t` x)(+v` w)(y(.s` w)(t` z))))})}
Definition	df-nmo 9745	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 <.u, w>.. 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.
|- normOp = {<.<.u, w>., n>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ n = {<.t, y>. | (t:(BaseSet` u)-->(BaseSet` w) /\ y = sup({x | E.z e. (BaseSet` u)(((norm` u)` z) <_ 1 /\ x = ((norm` w)` (t` z)))}, RR*, < ))})}
Definition	df-blo 9746	Define the class of bounded linear operators between two normed complex vector spaces.
|- BLnOp = {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t e. (u LnOp w) | ((unormOpw)` t) < +oo})}
Definition	df-0o 9747	Define the zero operator between two normed complex vector spaces.
|- 0op = {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = ((BaseSet` u) X. {(0v` w)}))}
Syntax	caj 9748	Adjoint of an operator.
class adj
Syntax	chmo 9749	Set of Hermitional (self-adjoint) operators.
class HmOp
Definition	df-aj 9750	Define the adjoint of an operator (if it exists). The domain of UadjW is the set of all operators from U to W that have an adjoint. Definition 3.9-1 of [Kreyszig] p. 196, although we don't require that U and W 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.
|- adj = {<.<.u, w>., a>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ a = {<.t, s>. | (t:(BaseSet` u)-->(BaseSet` w) /\ s:(BaseSet` w)-->(BaseSet` u) /\ A.x e. (BaseSet` u)A.y e. (BaseSet` w)((t` x)(.i` w)y) = (x(.i` u)(s` y)))})}
Definition	df-hmo 9751	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.
|- HmOp = {<.u, o>. | (u e. NrmCVec /\ o = {t e. dom ( uadju) | ((uadju)` t) = t})}
Theorem	lnoval 9752	The set of linear operators between two normed complex vector spaces.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- G = (+v` U)   &   |- H = (+v` W)   &   |- R = (.s` U)   &   |- S = (.s` W)   &   |- L = (U LnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> L = {t | (t:X-->Y /\ A.x e. X A.y e. CC A.z e. X (t` (xG(yRz))) = ((t` x)H(yS(t` z))))})
Theorem	islno 9753	The predicate "is a linear operator."
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- G = (+v` U)   &   |- H = (+v` W)   &   |- R = (.s` U)   &   |- S = (.s` W)   &   |- L = (U LnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> (T e. L <-> (T:X-->Y /\ A.x e. X A.y e. CC A.z e. X (T` (xG(yRz))) = ((T` x)H(yS(T` z))))))
Theorem	lnolin 9754	Basic linearity property of a linear operator.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- G = (+v` U)   &   |- H = (+v` W)   &   |- R = (.s` U)   &   |- S = (.s` W)   &   |- L = (U LnOp W)   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) /\ (A e. X /\ B e. CC /\ C e. X)) -> (T` (AG(BRC))) = ((T` A)H(BS(T` C))))
Theorem	lnof 9755	A linear operator is a mapping.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (U LnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> T:X-->Y)
Theorem	lno0 9756	The value of a linear operator at zero is zero.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- Q = (0v` U)   &   |- Z = (0v` W)   &   |- L = (U LnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> (T` Q) = Z)
Theorem	lnocoi 9757	The composition of two linear operators is linear.
|- L = (U LnOp W)   &   |- M = (W LnOp X)   &   |- N = (U LnOp X)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   &   |- X e. NrmCVec   &   |- S e. L   &   |- T e. M   =>   |- (T o. S) e. N
Theorem	lnoadd 9758	Addition property of a linear operator.
|- X = (BaseSet` U)   &   |- G = (+v` U)   &   |- H = (+v` W)   &   |- L = (U LnOp W)   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) /\ (A e. X /\ B e. X)) -> (T` (AGB)) = ((T` A)H(T` B)))
Theorem	lnosub 9759	Subtraction property of a linear operator.
|- X = (BaseSet` U)   &   |- M = (-v` U)   &   |- N = (-v` W)   &   |- L = (U LnOp W)   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) /\ (A e. X /\ B e. X)) -> (T` (AMB)) = ((T` A)N(T` B)))
Theorem	lnomul 9760	Scalar multiplication property of a linear operator.
|- X = (BaseSet` U)   &   |- R = (.s` U)   &   |- S = (.s` W)   &   |- L = (U LnOp W)   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) /\ (A e. CC /\ B e. X)) -> (T` (ARB)) = (AS(T` B)))
Theorem	nvcnpi3 9761	Epsilon-delta property of a linear operator continuous at a point.)
|- X = (BaseSet` U)   &   |- M = (norm` U)   &   |- N = (norm` W)   &   |- R = (-v` U)   &   |- C = (IndMet` U)   &   |- D = (IndMet` W)   &   |- J = (Open` C)   &   |- K = (Open` D)   &   |- L = (U LnOp W)   &   |- T e. L   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ (T e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. X ((M` (yRP)) <_ x -> (N` (T` (yRP))) <_ A)))
Theorem	nvcnpi4 9762	Epsilon-delta property of a linear operator continuous at a point.)
|- X = (BaseSet` U)   &   |- M = (norm` U)   &   |- N = (norm` W)   &   |- R = (-v` U)   &   |- C = (IndMet` U)   &   |- D = (IndMet` W)   &   |- J = (Open` C)   &   |- K = (Open` D)   &   |- L = (U LnOp W)   &   |- T e. L   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ (T e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. X ((M` (PRy)) <_ x -> (N` (T` (PRy))) <_ A)))
Theorem	nvo00 9763	Two ways to express a zero operator.
|- X = (BaseSet` U)   =>   |- ((U e. NrmCVec /\ T:X-->Y) -> (T = (X X. {Z}) <-> ran T = {Z}))
Theorem	nmofval 9764	The operator norm function.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> N = {<.t, y>. | (t:X-->Y /\ y = sup({x | E.z e. X ((L` z) <_ 1 /\ x = (M` (t` z)))}, RR*, < ))})
Theorem	nmoval 9765	The operator norm function.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T:X-->Y) -> (N` T) = sup({x | E.z e. X ((L` z) <_ 1 /\ x = (M` (T` z)))}, RR*, < ))
Theorem	nmosetre 9766	The set in the supremum of the operator norm definition df-nmo 9745 is a set of reals.
|- Y = (BaseSet` W)   &   |- N = (norm` W)   =>   |- ((W e. NrmCVec /\ T:X-->Y) -> {x | E.z e. X ((M` z) <_ 1 /\ x = (N` (T` z)))} C_ RR)
Theorem	nmosetn0 9767	The set in the supremum of the operator norm definition df-nmo 9745 is nonempty.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   &   |- M = (norm` U)   =>   |- (U e. NrmCVec -> (N` (T` Z)) e. {x | E.y e. X ((M` y) <_ 1 /\ x = (N` (T` y)))})
Theorem	nmoxr 9768	The norm of an operator is an extended real.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- N = (UnormOpW)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T:X-->Y) -> (N` T) e. RR*)
Theorem	nmoge0 9769	The norm of an operator is nonnegative.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- N = (UnormOpW)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T:X-->Y) -> 0 <_ (N` T))
Theorem	nmorepnf 9770	The norm of an operator is either real or plus infinity.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- N = (UnormOpW)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T:X-->Y) -> ((N` T) e. RR <-> (N` T) =/= +oo))
Theorem	nmoreltpnf 9771	The norm of any operator is real iff it is less than plus infinity.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- N = (UnormOpW)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T:X-->Y) -> ((N` T) e. RR <-> (N` T) < +oo))
Theorem	nmogtmnf 9772	The norm of an operator is greater than minus infinity.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- N = (UnormOpW)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T:X-->Y) -> -oo < (N` T))
Theorem	nmolb 9773	A lower bound for an operator norm.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ T:X-->Y) /\ (A e. X /\ (L` A) <_ 1)) -> (M` (T` A)) <_ (N` T))
Theorem	nmoubi 9774	An upper bound for an operator norm.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   =>   |- ((T:X-->Y /\ A e. RR* /\ A.x e. X ((L` x) <_ 1 -> (M` (T` x)) <_ A)) -> (N` T) <_ A)
Theorem	nmoub3i 9775	An upper bound for an operator norm.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   =>   |- ((T:X-->Y /\ A e. RR /\ A.x e. X (M` (T` x)) <_ (A x. (L` x))) -> (N` T) <_ (abs` A))
Theorem	nmoub2i 9776	An upper bound for an operator norm.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   =>   |- ((T:X-->Y /\ (A e. RR /\ 0 <_ A) /\ A.x e. X (M` (T` x)) <_ (A x. (L` x))) -> (N` T) <_ A)
Theorem	nmobndi 9777	Two ways to express that an operator is bounded.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   =>   |- (T:X-->Y -> ((N` T) e. RR <-> E.r e. RR A.y e. X ((L` y) <_ 1 -> (M` (T` y)) <_ r)))
Theorem	nmounbi 9778	Two ways two express that an operator is unbounded.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   =>   |- (T:X-->Y -> ((N` T) = +oo <-> A.r e. RR E.y e. X ((L` y) <_ 1 /\ r < (M` (T` y)))))
Theorem	nmounbseqi 9779	An unbounded operator determines an unbounded sequence.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   =>   |- ((T:X-->Y /\ (N` T) = +oo) -> E.f(f:NN-->X /\ A.k e. NN ((L` (f` k)) <_ 1 /\ k < (M` (T` (f` k))))))
Theorem	nmobndseqi 9780	A bounded sequence determines a bounded operator.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   =>   |- ((T:X-->Y /\ A.f((f:NN-->X /\ A.k e. NN (L` (f` k)) <_ 1) -> E.k e. NN (M` (T` (f` k))) <_ k)) -> (N` T) e. RR)
Theorem	bloval 9781	The class of bounded linear operators between two normed complex vector spaces.
|- N = (UnormOpW)   &   |- L = (U LnOp W)   &   |- B = (U BLnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> B = {t e. L | (N` t) < +oo})
Theorem	isblo 9782	The predicate "is a bounded linear operator."
|- N = (UnormOpW)   &   |- L = (U LnOp W)   &   |- B = (U BLnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> (T e. B <-> (T e. L /\ (N` T) < +oo)))
Theorem	isblo2 9783	The predicate "is a bounded linear operator."
|- N = (UnormOpW)   &   |- L = (U LnOp W)   &   |- B = (U BLnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> (T e. B <-> (T e. L /\ (N` T) e. RR)))
Theorem	bloln 9784	A bounded operator is a linear operator.
|- L = (U LnOp W)   &   |- B = (U BLnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. B) -> T e. L)
Theorem	blof 9785	A bounded operator is an operator.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- B = (U BLnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. B) -> T:X-->Y)
Theorem	nmblore 9786	The norm of a bounded operator is a real number.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- N = (UnormOpW)   &   |- B = (U BLnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. B) -> (N` T) e. RR)
Theorem	0ofval 9787	The zero operator between two normed complex vector spaces.
|- X = (BaseSet` U)   &   |- Z = (0v` W)   &   |- O = (U 0op W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> O = (X X. {Z}))
Theorem	0oval 9788	Value of the zero operator.
|- X = (BaseSet` U)   &   |- Z = (0v` W)   &   |- O = (U 0op W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ A e. X) -> (O` A) = Z)
Theorem	0oo 9789	The zero operator is an operator.
|- X = (BaseSet` U)   &   |- Y = (BaseSet` W)   &   |- Z = (U 0op W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> Z:X-->Y)
Theorem	0lno 9790	The zero operator is linear.
|- Z = (U 0op W)   &   |- L = (U LnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> Z e. L)
Theorem	nmo0 9791	The operator norm of the zero operator.
|- N = (UnormOpW)   &   |- Z = (U 0op W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> (N` Z) = 0)
Theorem	0blo 9792	The zero operator is a bounded linear operator.
|- Z = (U 0op W)   &   |- B = (U BLnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec) -> Z e. B)
Theorem	nmlno0lem 9793	Lemma for nmlno0i 9794.
Theorem	nmlno0i 9794	The norm of a linear operator is zero iff the operator is zero.
|- N = (UnormOpW)   &   |- Z = (U 0op W)   &   |- L = (U LnOp W)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   =>   |- (T e. L -> ((N` T) = 0 <-> T = Z))
Theorem	nmlno0 9795	The norm of a linear operator is zero iff the operator is zero.
|- N = (UnormOpW)   &   |- Z = (U 0op W)   &   |- L = (U LnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> ((N` T) = 0 <-> T = Z))
Theorem	nmlnoubi 9796	An upper bound for the operator norm of a linear operator, using only the properties of nonzero arguments.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   &   |- K = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   &   |- L = (U LnOp W)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   =>   |- ((T e. L /\ (A e. RR /\ 0 <_ A) /\ A.x e. X (x =/= Z -> (M` (T` x)) <_ (A x. (K` x)))) -> (N` T) <_ A)
Theorem	nmlnogt0 9797	The norm of a nonzero linear operator is positive.
|- N = (UnormOpW)   &   |- Z = (U 0op W)   &   |- L = (U LnOp W)   =>   |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> (T =/= Z <-> 0 < (N` T)))
Theorem	lnon0 9798	The domain of a nonzero linear operator contains a nonzero vector.
|- X = (BaseSet` U)   &   |- Z = (0v` U)   &   |- O = (U 0op W)   &   |- L = (U LnOp W)   =>   |- (((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) /\ T =/= O) -> E.x e. X x =/= Z)
Theorem	nmblolbii 9799	A lower bound for the norm of a bounded linear operator.
|- X = (BaseSet` U)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   &   |- B = (U BLnOp W)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   &   |- T e. B   =>   |- (A e. X -> (M` (T` A)) <_ ((N` T) x. (L` A)))
Theorem	nmblolbi 9800	A lower bound for the norm of a bounded linear operator.
|- X = (BaseSet` U)   &   |- L = (norm` U)   &   |- M = (norm` W)   &   |- N = (UnormOpW)   &   |- B = (U BLnOp W)   &   |- U e. NrmCVec   &   |- W e. NrmCVec   =>   |- ((T e. B /\ A e. X) -> (M` (T` A)) <_ ((N` T) x. (L` A)))