mmtheorems87 - 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-10783

Statement List for Metamath Proof Explorer - 8601-8700 - Page 87 of 108

Type	Label	Description
Statement
Theorem	hlmet 8601	The induced metric on a complex Hilbert space.
|- D = (IndMet` U)   =>   |- (U e. CHil -> D e. Met)
Standard axioms for a complex Hilbert space
Theorem	hlex 8602	The base set of a Hilbert space is a set.
|- X = (Base` U)   =>   |- X e. V
Theorem	hladdf 8603	Mapping for Hilbert space vector addition.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- (U e. CHil -> G:(X X. X)-->X)
Theorem	hlcom 8604	Hilbert space vector addition is commutative.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- ((U e. CHil /\ A e. X /\ B e. X) -> (AGB) = (BGA))
Theorem	hlass 8605	Hilbert space vector addition is associative.
|- X = (Base` U)   &   |- G = (+v` U)   =>   |- ((U e. CHil /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = (AG(BGC)))
Theorem	hl0cl 8606	The Hilbert space zero vector.
|- X = (Base` U)   &   |- Z = (0v` U)   =>   |- (U e. CHil -> Z e. X)
Theorem	hladdid 8607	Hilbert space addition with the zero vector.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- Z = (0v` U)   =>   |- ((U e. CHil /\ A e. X) -> (AGZ) = A)
Theorem	hlmulf 8608	Mapping for Hilbert space scalar multiplication.
|- X = (Base` U)   &   |- S = (.s` U)   =>   |- (U e. CHil -> S:(CC X. X)-->X)
Theorem	hlmulid 8609	Hilbert space scalar multiplication by one.
|- X = (Base` U)   &   |- S = (.s` U)   =>   |- ((U e. CHil /\ A e. X) -> (1SA) = A)
Theorem	hlmulass 8610	Hilbert space scalar multiplication associative law.
|- X = (Base` U)   &   |- S = (.s` U)   =>   |- ((U e. CHil /\ (A e. CC /\ B e. CC /\ C e. X)) -> ((A x. B)SC) = (AS(BSC)))
Theorem	hldi 8611	Hilbert space scalar multiplication distributive law.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   =>   |- ((U e. CHil /\ (A e. CC /\ B e. X /\ C e. X)) -> (AS(BGC)) = ((ASB)G(ASC)))
Theorem	hldir 8612	Hilbert space scalar multiplication distributive law.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- S = (.s` U)   =>   |- ((U e. CHil /\ (A e. CC /\ B e. CC /\ C e. X)) -> ((A + B)SC) = ((ASC)G(BSC)))
Theorem	hlmul0 8613	Hilbert space scalar multiplication by zero.
|- X = (Base` U)   &   |- S = (.s` U)   &   |- Z = (0v` U)   =>   |- ((U e. CHil /\ A e. X) -> (0SA) = Z)
Theorem	hlipf 8614	Mapping for Hilbert space inner product.
|- X = (Base` U)   &   |- P = (.i` U)   =>   |- (U e. CHil -> P:(X X. X)-->CC)
Theorem	hlipcj 8615	Conjugate law for Hilbert space inner product.
|- X = (Base` U)   &   |- P = (.i` U)   =>   |- ((U e. CHil /\ A e. X /\ B e. X) -> (APB) = (*` (BPA)))
Theorem	hlipdir 8616	Distributive law for Hilbert space inner product.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- P = (.i` U)   =>   |- ((U e. CHil /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)PC) = ((APC) + (BPC)))
Theorem	hlipass 8617	Associative law for Hilbert space inner product.
|- X = (Base` U)   &   |- S = (.s` U)   &   |- P = (.i` U)   =>   |- ((U e. CHil /\ (A e. CC /\ B e. X /\ C e. X)) -> ((ASB)PC) = (A x. (BPC)))
Theorem	hlipgt0 8618	The inner product of a Hilbert space vector by itself is positive.
|- X = (Base` U)   &   |- Z = (0v` U)   &   |- P = (.i` U)   =>   |- ((U e. CHil /\ A e. X /\ A =/= Z) -> 0 < (APA))
Theorem	hlcompl 8619	Completeness of a Hilbert space.
|- X = (Base` U)   &   |- D = (IndMet` U)   =>   |- ((U e. CHil /\ F e. (Cau` D)) -> E.x e. X F(~~>m` D)x)
Examples of complex Hilbert spaces
Theorem	cnhl 8620	The set of complex numbers is a complex Hilbert space. (Contributed by Steve Rodriguez, 28-Apr-2007.)
|- U = <.<. + , x. >., abs>.   =>   |- U e. CHil
Subspaces
Theorem	ssphl 8621	A Banach subspace of an inner product space is a Hilbert space.
|- H = (SubSp` U)   =>   |- ((U e. CPreHil /\ W e. H /\ W e. CBan) -> W e. CHil)
Hellinger-Toeplitz Theorem
Theorem	htthlem1 8622	Lemma for htthi 8634. Closure of values of an operator T on an auxiliary sequence of vectors f.
Theorem	htthlem2 8623	Lemma for htthi 8634. Elevate set variables to class variables in the self-adjoint hypothesis.
Theorem	htthlem3 8624	Lemma for htthi 8634. Construct an auxiliary sequence of functionals F` k from inner products of the given function T and auxiliary vector sequence f.
Theorem	htthlem4 8625	Lemma for htthi 8634. Value of a functional F` k.
Theorem	htthlem5 8626	Lemma for htthi 8634. Each F` k is a bounded linear functional (i.e. a bounded linear operator from the vector space to CC).
Theorem	htthlem6 8627	Lemma for htthi 8634. An upper bound of all F` k at a given vector A, when the norms of auxiliary vector sequence f are all 1 or less.
Theorem	htthlem7 8628	Lemma for htthi 8634. Convert upper bound in htthlem6 8627 to an existence condition.
Theorem	htthlem8 8629	Lemma for htthi 8634.
Theorem	htthlem9 8630	Lemma for htthi 8634.
Theorem	htthlem10 8631	Lemma for htthi 8634.
Theorem	htthlem11 8632	Lemma for htthi 8634. Use the Uniform Boundedness Theorem ubthi 8546 to show that the functional F` k is bounded.
Theorem	htthlem12 8633	Lemma for htthi 8634. Linear operator T is bounded.
Theorem	htthi 8634	Hellinger-Toeplitz Theorem: any self-adjoint linear operator defined on all of Hilbert space is bounded. Theorem 10.1-1 of [Kreyszig] p. 525. Discovered by E. Hellinger and O. Toeplitz in 1910, "it aroused both admiration and puzzlement since the theorem establishes a relation between properties of two different kinds, namely, the properties of being defined everywhere and being bounded."
|- X = (Base` U)   &   |- P = (.i` U)   &   |- L = (U LnOp U)   &   |- B = (U BLnOp U)   &   |- U e. CHil   &   |- T e. L   &   |- ((x e. X /\ y e. X) -> ((T` x)Py) = (xP(T` y)))   =>   |- T e. B
Posets and lattices
Definition and basic properties
Syntax	cps 8635	Extend class notation with the class of all posets.
class Poset
Syntax	cspw 8636	Extend class notation with the supremum of an ordered set.
class supw
Syntax	cinf 8637	Extend class notation with the supremum of an ordered set.
class infw
Syntax	cjn 8638	Extend class notation with the join of two ordered sets.
class join
Syntax	cmee 8639	Extend class notation with the meet of two ordered sets.
class meet
Syntax	cla 8640	Extend class notation with the class of all lattices.
class Lat
Definition	df-ps 8641	Define the class of all posets (partially ordered sets) with weak ordering (e.g. "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric.
|- Poset = {r | (Rel r /\ (r o. r) (_ r /\ (r i^i `'r) = (I |` U.U.r))}
Definition	df-spw 8642	Define suprema under weak orderings. Unlike df-sup 4574 for strong orderings, supw is evaluates to a member of the field of R iff the supremum exists. Read R supw A as the R -supremum of set A.
|- supw = {<.<.r, x>., y>. | E.z(z = {w e. U.U.r | (A.v e. x vrw /\ A.v e. U.U.r(A.u e. x urv -> wrv))} /\ y = if(z =/= (/), U.z, P~U.U.U.r))}
Definition	df-nfw 8643	Define the class of all infima of a weak ordering relation.
|- infw = {<.<.r, x>., y>. | y = (`'r supw x)}
Definition	df-jn 8644	Define the class of all join operations on week orderings.
|- join = {<.r, w>. | w = {<.<.x, y>., z>. | ((x e. U.U.r /\ y e. U.U.r) /\ z = (r supw {x, y}))}}
Definition	df-mee 8645	Define the class of all meet operations on week orderings.
|- meet = {<.r, w>. | w = {<.<.x, y>., z>. | ((x e. U.U.r /\ y e. U.U.r) /\ z = (r infw {x, y}))}}
Definition	df-la 8646	Define the class of all lattices, which are posets in which every two elements have upper and lower bounds.
|- Lat = {r e. Poset | A.x e. dom rA.y e. dom r((r supw {x, y}) e. dom r /\ (r infw {x, y}) e. dom r)}
Theorem	isps 8647	The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation.
|- (R e. A -> (R e. Poset <-> (Rel R /\ (R o. R) (_ R /\ (R i^i `'R) = (I |` U.U.R))))
Theorem	psrel 8648	A poset is a relation.
|- (A e. Poset -> Rel A)
Theorem	pslem 8649	Lemma for psref 8651 and others.
Theorem	psdmrn 8650	The domain and range of a poset equal its field.
|- (R e. Poset -> (dom R = U.U.R /\ ran R = U.U.R))
Theorem	psref 8651	A poset is reflexive.
|- X = dom R   =>   |- ((R e. Poset /\ A e. X) -> ARA)
Theorem	psrn 8652	The range of a poset equals it domain.
|- X = dom R   =>   |- (R e. Poset -> X = ran R)
Theorem	psasym 8653	A poset is antisymmetric.
|- ((R e. Poset /\ ARB /\ BRA) -> A = B)
Theorem	pstr 8654	A poset is transitive.
|- ((R e. Poset /\ ARB /\ BRC) -> ARC)
Theorem	spwval2 8655	Value of supremum under a weak ordering. Read R supw A as "the R -supremum of A." U.U.R is the field of a relation R by relfld 3515. Unlike df-sup 4574 for strong orderings, the supremum exists iff R supw A belongs to the field.
|- X = U.U.R   &   |- Z = {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))}   =>   |- ((R e. U /\ A e. W) -> (R supw A) = if(Z =/= (/), U.Z, P~U.X))
Theorem	spwval3 8656	Value of a supremum.
|- X = U.U.R   &   |- (ph <-> (A.y