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.

As a speed-up experiment, all mpegif/mpeuni HTML pages except mmrecent.html have been gzipped (on us2 only). If your browser has a problem with this, please let me know or discuss here. Thanks. — Norm 21 Nov 2007

Last updated on 6-May-2008 at 2:08 PM ET.

Recent Additions to the Metamath Proof Explorer   Notes (last updated 6-May-08 )   News (last updated 14-Apr-08 )

Date	Label	Description
Theorem
6-May-2008	pnfnemnf 5460	Plus and minus infinity are distinguished elements of RR*.
|- +oo =/= -oo
6-May-2008	mnfnre 5420	Minus infinity is not a real number.
|- -oo e/ RR
6-May-2008	pnfnre 5419	Plus infinity is not a real number.
|- +oo e/ RR
6-May-2008	mnfxr 5417	Minus infinity belongs to the set of extended reals.
|- -oo e. RR*
6-May-2008	pnfxr 5416	Plus infinity belongs to the set of extended reals.
|- +oo e. RR*
6-May-2008	axinf2 4548	A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf 4546 and Regularity ax-reg 4517. This theorem should not be referenced in any proof. Instead, use ax-inf2 4549 below so that the uses of Regularity and standard Infinity can be more easily identified.
|- E.x(E.y(y e. x /\ A.z -. z e. y) /\ A.y(y e. x -> E.z(z e. x /\ A.w(w e. z <-> (w e. y \/ w = y)))))
6-May-2008	sdomn2lp 4409	Strict dominance has no 2-cycle loops.
|- -. (A ~< B /\ B ~< A)
5-May-2008	sspid 8253	A normed complex vector space is a subspace of itself.
|- H = (SubSp` U)   =>   |- (U e. NrmCVec -> U e. H)
5-May-2008	curry1val 4038	The value of a curried function with a constant first argument.
|- G = (F o. `'(2nd |` ({C} X. V)))   =>   |- ((F Fn (A X. B) /\ C e. A /\ D e. U) -> (G` D) = (CFD))
5-May-2008	curry1f 4037	Functionality of a curried function with a constant first argument.
|- G = (F o. `'(2nd |` ({C} X. V)))   =>   |- ((F:(A X. B)-->D /\ C e. A) -> G:B-->D)
4-May-2008	minvecex2 8454	Existence version of minvecle 8452.
|- X = (Base` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   &   |- Y = (Base` W)   &   |- U e. CPreHil   &   |- W e. ((SubSp` U) i^i CBan)   &   |- A e. X   =>   |- E.x e. Y A.y e. Y (N` (AMx)) <_ (N` (AMy))
4-May-2008	minveclem39 8453	Lemma for minvecex2 8454.
|- X = (Base` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   &   |- Y = (Base` W)   &   |- R = {x | E.y e. Y x = -u(N` (AMy))}   &   |- P = -usup(R, RR, < )   &   |- U e. CPreHil   &   |- W e. ((SubSp` U) i^i CBan)   &   |- A e. X   &   |- Q = U.{b e. Y | (N` (AMb)) = P}   =>   |- E.a e. Y A.f e. Y (N` (AMa)) <_ (N` (AMf))
4-May-2008	ntridm 7592	The interior operation is idempotent.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((int` J)` ((int` J)` S)) = ((int` J)` S))
3-May-2008	minvecle 8452	The minimizing vector from minveceu 8449 has the smallest distance.
|- X = (Base` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   &   |- Y = (Base` W)   &   |- R = {x | E.y e. Y x = -u(N` (AMy))}   &   |- P = -usup(R, RR, < )   &   |- U e. CPreHil   &   |- W e. ((SubSp` U) i^i CBan)   &   |- A e. X   &   |- Q = U.{b e. Y | (N` (AMb)) = P}   =>   |- (B e. Y -> (N` (AMQ)) <_ (N` (AMB)))
3-May-2008	minvecdist 8451	Distance of the minimizing vector of minveceu 8449.
|- X = (Base` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   &   |- Y = (Base` W)   &   |- R = {x | E.y e. Y x = -u(N` (AMy))}   &   |- P = -usup(R, RR, < )   &   |- U e. CPreHil   &   |- W e. ((SubSp` U) i^i CBan)   &   |- A e. X   &   |- Q = U.{b e. Y | (N` (AMb)) = P}   =>   |- (N` (AMQ)) = P
3-May-2008	minveccl 8450	The minimizing vector of minveceu 8449 belongs to the subspace Y.
|- X = (Base` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   &   |- Y = (Base` W)   &   |- R = {x | E.y e. Y x = -u(N` (AMy))}   &   |- P = -usup(R, RR, < )   &   |- U e. CPreHil   &   |- W e. ((SubSp` U) i^i CBan)   &   |- A e. X   &   |- Q = U.{b e. Y | (N` (AMb)) = P}   =>   |- Q e. Y
2-May-2008	minveceu 8449	Minimizing vector theorem. There is exactly one vector in a complete subspace W that minimizes the distance to an arbitrary vector A in a parent inner product space. Theorem 3.3-1 of [Kreyszig] p. 144, specialized to subspaces instead of convex subsets. Note that we work with the negative of the supremum of negatives instead of infimum in order to use theorems we already have available.
|- X = (Base` U)   &   |- M = (-v` U)   &   |- N = (norm` U)   &   |- Y = (Base` W)   &   |- R = {x | E.y e. Y x = -u(N` (AMy))}   &   |- P = -usup(R, RR, < )   &   |- U e. CPreHil   &   |- W e. ((SubSp` U) i^i CBan)   &   |- A e. X   =>   |- E!a e. Y (N` (AMa)) = P
2-May-2008	minveclem38 8448	Lemma for minveceu 8449.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   &   |- Y = (Base` W)   &   |- U e. CPreHil   &   |- A e. X   &   |- W e. (SubSp` U)   &   |- P = -usup(R, RR, < )   &   |- R = {x | E.y e. Y x = -u(N` (AMy))}   =>   |- (((a e. Y /\ b e. Y) /\ ((N` (AMa)) = P /\ (N` (AMb)) = P)) -> (N` (aMb)) <_ 0)
1-May-2008	minveclem37 8447	Lemma for minveceu 8449.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   &   |- Y = (Base` W)   &   |- U e. CPreHil   &   |- A e. X   &   |- W e. (SubSp` U)   &   |- P = -usup(R, RR, < )   &   |- R = {x | E.y e. Y x = -u(N` (AMy))}   =>   |- ((a e. Y /\ b e. Y) -> P <_ (N` (AM((1 / 2)S(aGb)))))
1-May-2008	minveclem36 8446	Lemma for minveceu 8449.
|- X = (Base` U)   &   |- G = (+v` U)   &   |- M = (-v` U)   &   |- S = (.s` U)   &   |- N = (norm` U)   &   |- Y = (Base` W)   &   |- U e. CPreHil   &   |- A e. X   &   |- W e. (SubSp` U)   &   |- P = -usup(R, RR, < )   &   |- R = {x | E.y e. Y x = -u(N` (AMy))}   =>   |- (((a e. X /\ b e. X) /\ ((N` (AMa)) = P /\ (N` (AMb)) = P)) -> ((N` (aMb))^2) = ((2 x. ((P^2) + (P^2))) - ((N` ((AMa)G(AMb)))^2)))
1-May-2008	grprndm 7936	A group's range in terms of its domain.
|- (G e. Grp -> ran G = dom dom G)
30-Apr-2008	ho02 9886	A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S10) of [Beran] p. 95.
|- T:H~-->H~   =>   |- (A.x e. H~ A.y e. H~ (x .ih (T` y)) = 0 <-> T = 0hop)
30-Apr-2008	hhssnm 9282	The norm operation on a subspace.
|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.   =>   |- (normh |` H) = (norm` W)
30-Apr-2008	sb6f 1185	Equivalence for substitution when y is not free in ph.
|- (ph -> A.yph)   =>   |- ([y / x]ph <-> A.x(x = y -> ph))
29-Apr-2008	hhsssm 9281	The scalar multiplication operation on a subspace.
|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.   =>   |- ( .h |` (CC X. H)) = (.s` W)
28-Apr-2008	clsidm 7591	The closure operation is idempotent.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((cls` J)` ((cls` J)` S)) = ((cls` J)` S))
27-Apr-2008	icmpmon 8937	If (GRF) is monic then F is monic. JFM CAT1 th. 62 (Part of FL's sandbox.)
|- O = dom (id` T)   &   |- H = (hom` T)   &   |- R = (o` T)   =>   |- ((T e. Cat /\ ((A e. O /\ B e. O /\ C e. O) /\ (F e. (H` <.A, B>.) /\ G e. (H` <.B, C>.)) /\ (GRF) e. (Monic` T))) -> F e. (Monic` T))
27-Apr-2008	cnfilca 8801	Condition to have a filter finer than a given filter and containing a set A. (Part of FL's sandbox.) Bourbaki T.G. I.37 cor. 1
|- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> (E.g e. Fil (A e. g /\ F (_ g) <-> A.x e. F (x i^i A) =/= (/)))
27-Apr-2008	efilcp2 8800	A filter containing a set A exists iff A has the finite intersection property (i.e. no finite intersection of elements of A is empty). Bourbaki TG I.37 prop. 1. (Part of FL's sandbox.)
|- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. (fi` A