Most Recent Proofs - Metamath Proof Explorer

Most Recent Proofs    These are the 10 (GIF, Unicode) or 100 (GIF, Unicode) most recent proofs in the Metamath Proof Explorer and the Hilbert Space Explorer. The official, cleaned up set.mm database file in the Metamath program download is sometimes several days behind the preproduction set.mm (7MB) that corresponds to this page. Email: Norm Megill. Wikis: AsteroidMeta (Recent Changes); Ghestalt (Recent Changes). Mailing list: Google Groups. Syndication: RSS feed (web version) courtesy of Dan Getz.

Some users have reported that they cannot always access this page, apparently because port 8888 is sometimes mysteriously blocked. I added two other ports, and this page can now be accessed via ports 88, 443, and 8888. You can discuss this problem here. — Norm 24 Jun 2008

Last updated on 8-Jul-2008 at 4:15 PM ET.

Recent Additions to the Metamath Proof Explorer   Notes (last updated 22-May-08 )   News (last updated 23-May-08 )

Date	Label	Description
Theorem
8-Jul-2008	nmopub2t 9778	An upper bound for an operator norm.
|- ((T:H~-->H~ /\ (A e. RR /\ 0 <_ A) /\ A.x e. H~ (normh` (T` x)) <_ (A x. (normh` x))) -> (normop` T) <_ A)
8-Jul-2008	projlem 9160	Lemma 3.6 of [Beran] p. 101: "Let H be a complete subspace of a (pre-)Hilbert space H~ and let A e. H~. Then there exists a vector x e. H such that (norm` (x -h A)) <_ (norm` (y -h A)) for every y e. H." This is a lemma for the projection theorem.
|- A e. H~   &   |- H e. CH   =>   |- E.x e. H A.y e. H (normh` (x -h A)) <_ (normh` (y -h A))
8-Jul-2008	climabs0 7059	Convergence to zero of the absolute value implies convergence to zero.
|- F e. V   &   |- G e. V   &   |- (k e. NN -> (G` k) = (abs` (F` k)))   =>   |- ((A.k e. NN (F` k) e. CC /\ G ~~> 0) -> F ~~> 0)
7-Jul-2008	dmdi2 10174	Consequence of the dual modular pair property.
|- (((A e. CH /\ B e. CH /\ C e. CH) /\ (A MH* B /\ B (_ C)) -> (C i^i (A vH B)) (_ ((C i^i A) vH B))
7-Jul-2008	spwpr2 8602	Property of supremum defining condition for an unordered pair.
|- (ph <-> (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)))   =>   |- (((R e. T /\ A = {B, C}) /\ (B e. U /\ C e. W)) -> (ph <-> ((BRx /\ CRx) /\ A.y e. X ((BRy /\ CRy) -> xRy))))
7-Jul-2008	2pwuninel 4474	The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set.
|- -. P~P~U.A e. A
7-Jul-2008	dmex 3354	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26.
|- A e. V   =>   |- dom A e. V
6-Jul-2008	lmbrnns 7896	Express the binary relation "sequence F converges to point P " in a metric space."
|- X = dom dom D   &   |- (k e. NN -> A = (F` k))   =>   |- ((D e. Met /\ P e. X /\ F:NN-->X) -> (F(~~>m` D)P <-> A.x e. RR+ E.j e. NN A.k e. NN (j <_ k -> (ADP) < x)))
6-Jul-2008	releldm 3341	The first argument of a binary relation belongs to its domain.
|- ((Rel R /\ ARB) -> A e. dom R)
5-Jul-2008	pjocco 10049	Composition of projections of a subspace and its orthocomplement.
|- H e. CH   =>   |- ((proj` H) o. (proj` (_|_` H))) = 0hop
5-Jul-2008	leoptrt 10013	The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49.
|- (((S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp) /\ (S <_op T /\ T <_op U)) -> S <_op U)
5-Jul-2008	iscau4 7894	Express the property "F is a Cauchy sequence of metric D."
|- X = dom dom D   =>   |- (D e. Met -> (F e. (Cau` D) <-> (F (_ (CC X. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` j) e. X /\ (F` k) e. X /\ ((F` j)D(F` k)) < x))))))
4-Jul-2008	bracnlnvalt 9990	The vector that a continuous linear functional is the bra of.
|- (T e. (LinFn i^i ConFn) -> T = (bra` U.{y e. H~ | A.x e. H~ (T` x) = (x .ih y)}))
3-Jul-2008	unisn3 2871	Union of a singleton in the form of a restricted class abstraction.
|- (A e. B -> U.{x e. B | x = A} = A)
2-Jul-2008	nmopcoadj0 9979	An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106.
|- T e. BndLinOp   =>   |- ((T o. (adjh` T)) = 0hop <-> T = 0hop)
2-Jul-2008	sylancom 475	Syllogism inference with commutation of antecents.
|- ((ph /\ ps) -> ch)   &   |- ((ch /\ ps) -> th)   =>   |- ((ph /\ ps) -> th)
1-Jul-2008	supmax 4570	The greatest element of a set is the supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008.)
|- R Or A   =>   |- ((C e. A /\ C e. B /\ A.y e. B -. CRy) -> sup(B, A, R) = C)
1-Jul-2008	supmaxlem 4569	A set that contains a greatest element satisfies the antecedent in supremum theorems. This allows sup(A, B, R) to be used in some situations without the completeness axiom. (Contributed by Jeff Hoffman, 17-Jun-2008.)
|- ((C e. A /\ C e. B /\ A.z e. B -. CRz) -> E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)))
1-Jul-2008	opelxpex2 3274	The second member of an ordered pair of classes in a cross product exists when the order pair doesn't belong to I.
|- (<.A, B>. e. ((C X. D) \ I) -> B e. V)
30-Jun-2008	adjeq0 9967	An operator is zero iff its adjoint is zero. Theorem 3.11(i) of [Beran] p. 106.
|- (T = 0hop <-> (adjh` T) = 0hop)
30-Jun-2008	hhsshl 9094	Hilbert space property of a closed subspace.
|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.   &   |- H e. CH   =>   |- W e. CHil
29-Jun-2008	hhssims2 9088	Induced metric of a subspace.
|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.   &   |- D = (IndMet` W)   &   |- H e. SH   =>   |- D = ((normh o. -h ) |` (H X. H))
29-Jun-2008	brelrn 3339	The second argument of a binary relation belongs to its range.
|- A e. V   &   |- B e. V   =>   |- (ACB -> B e. ran C)
29-Jun-2008	brelrng 3338	The second argument of a binary relation belongs to its range.
|- ((A e. F /\ B e. G /\ ACB) -> B e. ran C)
29-Jun-2008	ordtri3or 2974	A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38.
|- ((Ord A /\ Ord B) -> (A e. B \/ A = B \/ B e. A))
29-Jun-2008	moi2 1920	Consequence of "at most one."
|- (x = A -> (ph <-> ps))   =>   |- (((A e. B /\ E*xph) /\ (ph /\ ps)) -> x = A)
28-Jun-2008	rehaus 7871	The standard topology on the reals is Hausdorff.
|- (topGen` ran (,)) e. Haus
27-Jun-2008	hhssims 9087	Induced metric of a subspace.
|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.   &   |- H e. SH   &   |- D = ((normh o. -h ) |` (H X. H))   =>   |- D = (IndMet` W)
27-Jun-2008	hhsssh2 9082	The predicate "H is a subspace of Hilbert space."
|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.   =>   |- (H e. SH <-> (W e. NrmCVec /\ H (_ H~))
27-Jun-2008	pwuninel 4473	The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set.
|- -. P~U.A e. A
26-Jun-2008	oteqex 2794	Equivalence of existence implied by equality of ordered triples.
|- (<.<.A, B>., C>. = <.<.R, S>., T>. -> (A e. V <-> R e. V))
25-Jun-2008	nvdm 8243	Two ways to express the set of vectors in a normed complex vector space.
|- G = (+v` U)   &   |- N = (norm` U)   =>   |- (U e. NrmCVec -> (X = dom N <-> X = ran G))
24-Jun-2008	hhssablt 9075	Abelian group property of subspace addition.
|- (H e. SH -> ( +h |` (H X. H)) e. Abel)
24-Jun-2008	spwnex 8605	Non-closure when the supremum doesn't exist.
|- X = dom R   &   |- (ph <-> (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)))   =>   |- ((R e. Poset /\ A e. W /\ -. E.x e. X ph) -> -. (R supw A) e. X)
23-Jun-2008	axhilex 8793	Derive axiom ax-hilex 8811 from Hilbert space under ZF set theory. Before introducing the 18 axioms for Hilbert space, we first prove them as the conclusions of theorems axhilex 8793 through axhcompl 8810, using ZFC set theory only. These show that if we are given a known, fixed Hilbert space U = <.<. +h , .h >., normh>. that satisfies their hypotheses, then we can derive the Hilbert space axioms as theorems of ZFC set theory. In practice, in order to use these theorems to convert the Hilbert Space explorer to a ZFC-only subtheory, we would also have to provide definitions for the 3 (otherwise primitive) class constants +h, .h, and .ih before df-hnorm 8779 above. See also the comment in ax-hilex 8811.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- H~ e. V
23-Jun-2008	metnei 7832	The neighborhoods around a point P of a metric space are those subsets containing a ball around P. Definition of neighborhood in [Kreyszig] p. 19.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- ((D e. Met /\ P e. X) -> ((nei` J)` {P}) = {x | (x (_ X /\ E.r e. RR (0 < r /\ (P( ball ` D)r) (_ x))})
22-Jun-2008	axhcompl 8810	Derive axiom ax-hcompl 9013 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   =>   |- (F e. Cauchy -> E.x e. H~ F ~~>v x)
22-Jun-2008	axhis4 8809	Derive axiom ax-his4 8894 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- ((A e. H~ /\ A =/= 0h) -> 0 < (A .ih A))
22-Jun-2008	metne0 7775	A metric space is nonempty iff its base set is nonempty.
|- X = dom dom D   =>   |- (D e. Met -> (D =/= (/) <-> X =/= (/)))
21-Jun-2008	axhis3 8808	Derive axiom ax-his3 8893 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- ((A e. CC /\ B e. H~ /\ C e. H~) -> ((A .h B) .ih C) = (A x. (B .ih C)))
21-Jun-2008	axhis2 8807	Derive axiom ax-his2 8892 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- ((A e. H~ /\ B e. H~ /\ C e. H~) -> ((A +h B) .ih C) = ((A .ih C) + (B .ih C)))
21-Jun-2008	axhis1 8806	Derive axiom ax-his1 8891 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- ((A e. H~ /\ B e. H~) -> (A .ih B) = (*` (B .ih A)))
21-Jun-2008	axhfi 8805	Derive axiom ax-hfi 8888 from Hilbert space under ZF set theory.
|- U = <.<. +h , .h >., normh>.   &   |- U e. CHil   &   |- .ih = (.i` U)   =>   |- .ih :