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 19-Jul-2008 at 5:53 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
19-Jul-2008	nvoprne 8271	The vector addition and scalar product operations are not identical.
⊢ (⟨⟨G, S⟩, N⟩ ∈ NrmCVec → G ≠ S)
18-Jul-2008	expnlbndt 6601	The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound.
⊢ ((A ∈ ℝ+ ⋀ B ∈ ℝ ⋀ 1 < B) → ∃k ∈ ℕ (1 / (B↑k)) < A)
18-Jul-2008	rpne0t 6239	A positive real is nonzero.
⊢ (A ∈ ℝ+ → A ≠ 0)
17-Jul-2008	infpss 7535	Every infinite set has an equinumerous proper subset. Exercise 7 of [TakeutiZaring] p. 91.
⊢ A ∈ V    ⇒   ⊢ (ω ≼ A → ∃x(x ⊂ A ⋀ x ≈ A))
16-Jul-2008	relelrng 3343	The second argument of a binary relation belongs to its range.
⊢ ((B ∈ C ⋀ Rel R ⋀ ARB) → B ∈ ran R)
15-Jul-2008	flfract 6195	The fractional part of a real number is less than one.
⊢ (A ∈ ℝ → (A − (⌊ ‘A)) < 1)
15-Jul-2008	flreclt 6186	The floor (greatest integer) function is real.
⊢ (A ∈ ℝ → (⌊ ‘A) ∈ ℝ)
14-Jul-2008	dmdbr7at 10306	Dual modular pair property in terms of atoms.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A Mℋ* B ↔ ∀x ∈ Atoms ((A ∨ℋ B) ∩ x) ⊆ (((x ∨ℋ B) ∩ A) ∨ℋ B))
14-Jul-2008	syld3an1 870	A syllogism inference.
⊢ ((φ ⋀ ψ ⋀ χ) → θ)    &   ⊢ ((τ ⋀ ψ ⋀ χ) → φ)    ⇒   ⊢ ((τ ⋀ ψ ⋀ χ) → θ)
13-Jul-2008	dmdbr4at 10303	Dual modular pair property in terms of atoms.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A Mℋ* B ↔ ∀x ∈ Atoms ((x ∨ℋ B) ∩ (A ∨ℋ B)) ⊆ (((x ∨ℋ B) ∩ A) ∨ℋ B))
12-Jul-2008	atdmd2 10296	Two Hilbert lattice elements have the dual modular pair property if the second is an atom.
⊢ ((A ∈ Cℋ ⋀ B ∈ Atoms) → A Mℋ* B)
12-Jul-2008	dmdbr5 10190	Binary relation expressing the dual modular pair property.
⊢ ((A ∈ Cℋ ⋀ B ∈ Cℋ ) → (A Mℋ* B ↔ ∀x ∈ Cℋ (x ⊆ (A ∨ℋ B) → x ⊆ (((x ∨ℋ B) ∩ A) ∨ℋ B))))
11-Jul-2008	clmfnn 7047	Express the predicate F converges to A for an explicit function, using natural numbers.
⊢ ((F:ℕ–→ℂ ⋀ A ∈ ℂ) → (F ⇝ A ↔ ∀x ∈ ℝ+ ∃j ∈ ℕ ∀k ∈ ℕ (j ≤ k → (abs ‘((F ‘k) − A)) < x)))
10-Jul-2008	metcls 7929	The closure of a subset of a metric space is equal to its points of convergence. Theorem 1.4-6(a) of [Kreyszig] p. 30.
⊢ X = dom dom D    &   ⊢ J = (Open ‘D)    ⇒   ⊢ ((D ∈ Met ⋀ M ⊆ X) → ((cls ‘J) ‘M) = {x∣∃f(f:ℕ–→M ⋀ f(⇝m ‘D)x)})
10-Jul-2008	expne0t 6532	Natural number exponentiation is nonzero iff its mantissa is nonzero.
⊢ ((A ∈ ℂ ⋀ N ∈ ℕ) → ((A↑N) ≠ 0 ↔ A ≠ 0))
9-Jul-2008	iscaunns 7907	Express the property "F is a Cauchy sequence of metric D."
⊢ X = dom dom D    &   ⊢ (k ∈ ℕ → A = (F ‘k))    ⇒   ⊢ ((D ∈ Met ⋀ F:ℕ–→X) → (F ∈ (Cau ‘D) ↔ ∀x ∈ ℝ+ ∃j ∈ ℕ ∀k ∈ ℕ (j ≤ k → ([j / k]ADA) < x)))
8-Jul-2008	nmopub2t 9790	An upper bound for an operator norm.
⊢ ((T: ℋ –→ ℋ ⋀ (A ∈ ℝ ⋀ 0 ≤ A) ⋀ ∀x ∈ ℋ (normh ‘(T ‘x)) ≤ (A · (normh ‘x))) → (normop ‘T) ≤ A)
8-Jul-2008	projlem 9172	Lemma 3.6 of [Beran] p. 101: "Let H be a complete subspace of a (pre-)Hilbert space ℋ and let A ∈ ℋ. Then there exists a vector x ∈ H such that (norm ‘(x −h A)) ≤ (norm ‘(y −h A)) for every y ∈ H." This is a lemma for the projection theorem.
⊢ A ∈ ℋ    &   ⊢ H ∈ Cℋ    ⇒   ⊢ ∃x ∈ H ∀y ∈ H (normh ‘(x −h A)) ≤ (normh ‘(y −h A))
8-Jul-2008	climabs0 7067	Convergence to zero of the absolute value implies convergence to zero.
⊢ F ∈ V    &   ⊢ G ∈ V    &   ⊢ (k ∈ ℕ → (G ‘k) = (abs ‘(F ‘k)))    ⇒   ⊢ ((∀k ∈ ℕ (F ‘k) ∈ ℂ ⋀ G ⇝ 0) → F ⇝ 0)
7-Jul-2008	dmdi2 10186	Consequence of the dual modular pair property.
⊢ (((A ∈ Cℋ ⋀ B ∈ Cℋ ⋀ C ∈ Cℋ ) ⋀ (A Mℋ* B ⋀ B ⊆ C)) → (C ∩ (A ∨ℋ B)) ⊆ ((C ∩ A) ∨ℋ B))
7-Jul-2008	spwpr2 8614	Property of supremum defining condition for an unordered pair.
⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy)))    ⇒   ⊢ (((R ∈ T ⋀ A = {B, C}) ⋀ (B ∈ U ⋀ C ∈ W)) → (φ ↔ ((BRx ⋀ CRx) ⋀ ∀y ∈ X ((BRy ⋀ CRy) → xRy))))
7-Jul-2008	2pwuninel 4476	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.
⊢ ¬ ℘℘∪A ∈ A
7-Jul-2008	dmex 3356	The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26.
⊢ A ∈ V    ⇒   ⊢ dom A ∈ V
6-Jul-2008	lmbrnns 7905	Express the binary relation "sequence F converges to point P " in a metric space."
⊢ X = dom dom D    &   ⊢ (k ∈ ℕ → A = (F ‘k))    ⇒   ⊢ ((D ∈ Met ⋀ P ∈ X ⋀ F:ℕ–→X) → (F(⇝m ‘D)P ↔ ∀x ∈ ℝ+ ∃j ∈ ℕ ∀k ∈ ℕ (j ≤ k → (ADP) < x)))
6-Jul-2008	releldm 3342	The first argument of a binary relation belongs to its domain.
⊢ ((Rel R ⋀ ARB) → A ∈ dom R)
5-Jul-2008	pjocco 10061	Composition of projections of a subspace and its orthocomplement.
⊢ H ∈ Cℋ    ⇒   ⊢ ((proj ‘H) ∘ (proj ‘(⊥ ‘H))) = 0hop
5-Jul-2008	leoptrt 10025	The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49.
⊢ (((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) ⋀ (S ≤op T ⋀ T ≤op U)) → S ≤op U)
5-Jul-2008	iscau4 7903	Express the property "F is a Cauchy sequence of metric D."
⊢ X = dom dom D    ⇒   ⊢ (D ∈ Met → (F ∈ (Cau ‘D) ↔ (F ⊆ (ℂ × X) ⋀ ∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ ℤ (j ≤ k → ((F ‘j) ∈ X ⋀ (F ‘k) ∈ X ⋀ ((F ‘j)D(F ‘k)) < x))))))
4-Jul-2008	bracnlnvalt 10002	The vector that a continuous linear functional is the bra of.
⊢ (T ∈ (LinFn ∩ ConFn) → T = (bra ‘∪{y ∈ ℋ ∣∀x ∈ ℋ (T ‘x) = (x ·ih y)}))
3-Jul-2008	unisn3 2872	Union of a singleton in the form of a restricted class abstraction.
⊢ (A ∈ B → ∪{x ∈ B∣x = A} = A)
2-Jul-2008	nmopcoadj0 9991	An operator composed with its adjoint is zero iff the operator is zero. Theorem 3.11(vii) of [Beran] p. 106.
⊢ T ∈ BndLinOp    ⇒   ⊢ ((T ∘ (adjh ‘T)) = 0hop ↔ T = 0hop )
2-Jul-2008	sylancom 475	Syllogism inference with commutation of antecents.
⊢ ((φ ⋀ ψ) → χ)    &   ⊢ ((χ ⋀ ψ) → θ)    ⇒   ⊢ ((φ ⋀ ψ) → θ)
1-Jul-2008	supmax 4572	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 ∈ A ⋀ C ∈ B ⋀ ∀y ∈ B ¬ CRy) → sup(B, A, R) = C)
1-Jul-2008	supmaxlem 4571	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 ∈ A ⋀ C ∈ B ⋀ ∀z ∈ B ¬ CRz) → ∃x ∈ A (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz)))
1-Jul-2008	opelxpex2 3275	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⟩ ∈ ((C × D) ∖ I) → B ∈ V)
30-Jun-2008	adjeq0 9979	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 9106	Hilbert space property of a closed subspace.
⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩    &   ⊢ H ∈ Cℋ    ⇒   ⊢ W ∈ CHil
29-Jun-2008	hhssims2 9100	Induced metric of a subspace.
⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩    &   ⊢ D = (IndMet ‘W)    &   ⊢ H ∈ Sℋ    ⇒   ⊢ D = ((normh ∘ −h ) ↾ (H × H))
29-Jun-2008	brelrn 3340	The second argument of a binary relation belongs to its range.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (ACB → B ∈ ran C)
29-Jun-2008	brelrng 3339	The second argument of a binary relation belongs to its range.
⊢ ((A ∈ F ⋀ B ∈ G ⋀ ACB) → B ∈ ran C)
29-Jun-2008	ordtri3or 2975	A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38.
⊢ ((Ord A ⋀ Ord B) → (A ∈ B ⋁ A = B ⋁ B ∈ A))
29-Jun-2008	moi2 1921	Consequence of "at most one."
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (((A ∈ B ⋀ ∃*xφ) ⋀ (φ ⋀ ψ)) → x = A)
28-Jun-2008	rehaus 7880	The standard topology on the reals is Hausdorff.
⊢ (topGen ‘ran (,)) ∈ Haus
27-Jun-2008	hhssims 9099	Induced metric of a subspace.
⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩    &   ⊢ H ∈ Sℋ    &   ⊢ D = ((normh ∘ −h ) ↾ (H × H))    ⇒   ⊢ D = (IndMet ‘W)
27-Jun-2008	hhsssh2 9094	The predicate "H is a subspace of Hilbert space."
⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩    ⇒   ⊢ (H ∈ Sℋ ↔ (W ∈ NrmCVec ⋀ H ⊆ ℋ ))
27-Jun-2008	pwuninel 4475	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.
⊢ ¬ ℘∪A ∈ A
26-Jun-2008	oteqex 2795	Equivalence of existence implied by equality of ordered triples.
⊢ (⟨⟨A, B⟩, C⟩ = ⟨⟨R, S⟩, T⟩ → (A ∈ V ↔ R ∈ V))
25-Jun-2008	nvdm 8254	Two ways to express the set of vectors in a normed complex vector space.
⊢ G = ( +v ‘U)    &   ⊢ N = (norm ‘U)    ⇒   ⊢ (U ∈ NrmCVec → (X = dom N ↔ X = ran G))
24-Jun-2008	hhssablt 9087	Abelian group property of subspace addition.
⊢ (H ∈ Sℋ → ( +h ↾ (H × H)) ∈ Abel)
24-Jun-2008	spwnex 8617	Non-closure when the supremum doesn't exist.
⊢ X = dom R    &   ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy)))    ⇒   ⊢ ((R ∈ Poset ⋀ A ∈ W ⋀ ¬ ∃x ∈ X φ) → ¬ (R supw A) ∈ X)
23-Jun-2008	axhilex 8805	Derive axiom ax-hilex 8823 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 8805 through axhcompl 8822, 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 8791 above. See also the comment in ax-hilex 8823.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ ℋ ∈ V
23-Jun-2008	metnei 7841	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 ∈ Met ⋀ P ∈ X) → ((nei ‘J) ‘{P}) = {x∣(x ⊆ X ⋀ ∃r ∈ ℝ (0 < r ⋀ (P( ball ‘D)r) ⊆ x))})
22-Jun-2008	axhcompl 8822	Derive axiom ax-hcompl 9025 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ (F ∈ Cauchy → ∃x ∈ ℋ F ⇝v x)
22-Jun-2008	axhis4 8821	Derive axiom ax-his4 8906 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    &   ⊢ ·ih = ( ·i ‘U)    ⇒   ⊢ ((A ∈ ℋ ⋀ A ≠ 0h) → 0 < (A ·ih A))
22-Jun-2008	metne0 7784	A metric space is nonempty iff its base set is nonempty.
⊢ X = dom dom D    ⇒   ⊢ (D ∈ Met → (D ≠ ∅ ↔ X ≠ ∅))
21-Jun-2008	axhis3 8820	Derive axiom ax-his3 8905 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    &   ⊢ ·ih = ( ·i ‘U)    ⇒   ⊢ ((A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → ((A ·h B) ·ih C) = (A · (B ·ih C)))
21-Jun-2008	axhis2 8819	Derive axiom ax-his2 8904 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    &   ⊢ ·ih = ( ·i ‘U)    ⇒   ⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → ((A +h B) ·ih C) = ((A ·ih C) + (B ·ih C)))
21-Jun-2008	axhis1 8818	Derive axiom ax-his1 8903 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    &   ⊢ ·ih = ( ·i ‘U)    ⇒   ⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ) → (A ·ih B) = (∗ ‘(B ·ih A)))
21-Jun-2008	axhfi 8817	Derive axiom ax-hfi 8900 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    &   ⊢ ·ih = ( ·i ‘U)    ⇒   ⊢ ·ih :( ℋ × ℋ )–→ℂ
21-Jun-2008	iscnp2 7722	The predicate "F is a continuous function from topology J to topology K at point P."
⊢ X = ∪J    &   ⊢ Y = ∪K    ⇒   ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ P ∈ X) → (F ∈ ((J CnP K) ‘P) ↔ (F:X–→Y ⋀ ∀y ∈ K ((F ‘P) ∈ y → ∃x ∈ J (P ∈ x ⋀ x ⊆ (◡F “ y))))))
20-Jun-2008	dveeq1ALT 1354	Version of dveeq1 1353 using ax-16 1209 instead of ax-17 970.
⊢ (¬ ∀x x = y → (y = z → ∀x y = z))
19-Jun-2008	axhvmul0 8816	Derive axiom ax-hvmul0 8834 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ (A ∈ ℋ → (0 ·h A) = 0h)
19-Jun-2008	axhvdistr2 8815	Derive axiom ax-hvdistr2 8833 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℋ ) → ((A + B) ·h C) = ((A ·h C) +h (B ·h C)))
19-Jun-2008	dveeq2ALT 1212	Version of dveeq2 1211 using ax-16 1209 instead of ax-17 970.
⊢ (¬ ∀x x = y → (z = y → ∀x z = y))
18-Jun-2008	pstr 8608	A poset is transitive.
⊢ ((R ∈ Poset ⋀ ARB ⋀ BRC) → ARC)
17-Jun-2008	ee7.2a 10382	Lemma for Euclid's Elements, Book 7, proposition 2. The original mentions the smaller measure being 'continually subtracted' from the larger. Many authors interpret this phrase as A mod B. Here, just one subtraction step is proved to preserve the gcd. The rec function will be used in other proofs for iterated subtraction.
⊢ ((A ∈ ℕ ⋀ B ∈ ℕ) → (A < B → gcd(A, B) = gcd(A, (B − A))))
17-Jun-2008	nndivlub 10379	A factor of a natural number cannot exceed it.
⊢ ((A ∈ ℕ ⋀ B ∈ ℕ) → ((A / B) ∈ ℕ → B ≤ A))
17-Jun-2008	nndivsub 10378	Please add description here.
⊢ (((A ∈ ℕ ⋀ B ∈ ℕ ⋀ C ∈ ℕ) ⋀ ((A / C) ∈ ℕ ⋀ A < B)) → ((B / C) ∈ ℕ ↔ ((B − A) / C) ∈ ℕ))
17-Jun-2008	nnssi3 10377	Convert a theorem for real/complex numbers into one for natural numbers.
⊢ ℕ ⊆ D    &   ⊢ (C ∈ ℕ → φ)    &   ⊢ (((A ∈ D ⋀ B ∈ D ⋀ C ∈ D) ⋀ φ) → ψ)    ⇒   ⊢ ((A ∈ ℕ ⋀ B ∈ ℕ ⋀ C ∈ ℕ) → ψ)
17-Jun-2008	nnssi2 10376	Convert a theorem for real/complex numbers into one for natural numbers.
⊢ ℕ ⊆ D    &   ⊢ (B ∈ ℕ → φ)    &   ⊢ ((A ∈ D ⋀ B ∈ D ⋀ φ) → ψ)    ⇒   ⊢ ((A ∈ ℕ ⋀ B ∈ ℕ) → ψ)
17-Jun-2008	gelsupvalOLD 10375	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. OBSOLETE - Use supmax 4572 instead.
⊢ R Or A    ⇒   ⊢ ((C ∈ B ⋀ (C ∈ A ⋀ ∀y ∈ B ¬ CRy)) → sup(B, A, R) = C)
17-Jun-2008	gelcomplOLD 10374	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. OBSOLETE - Use supmaxlem 4571 instead.
⊢ ((x ∈ A ⋀ (∀z ∈ B ¬ xRz ⋀ x ∈ B)) → ∃x ∈ A (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz)))
17-Jun-2008	axhvdistr1 8814	Derive axiom ax-hvdistr1 8832 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ ((A ∈ ℂ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → (A ·h (B +h C)) = ((A ·h B) +h (A ·h C)))
16-Jun-2008	cldlp 7711	A subset of a topological space is closed iff it contains all its limit points. Corollary 6.7 of [Munkres] p. 97.
⊢ X = ∪J    ⇒   ⊢ ((J ∈ Top ⋀ S ⊆ X) → (S ∈ (Clsd ‘J) ↔ ((limPt ‘J) ‘S) ⊆ S))
15-Jun-2008	ntr0 7671	The interior of the empty set.
⊢ (J ∈ Top → ((int ‘J) ‘∅) = ∅)
15-Jun-2008	dvelimALT 1352	Version of dvelim 1351 that doesn't use ax-10 965. (See dvelimfALT 1152 for a version that doesn't use ax-11 966.)
⊢ (φ → ∀xφ)    &   ⊢ (z = y → (φ ↔ ψ))    ⇒   ⊢ (¬ ∀x x = y → (ψ → ∀xψ))
14-Jun-2008	axhvmulass 8813	Derive axiom ax-hvmulass 8831 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℋ ) → ((A · B) ·h C) = (A ·h (B ·h C)))
14-Jun-2008	axhvmulid 8812	Derive axiom ax-hvmulid 8830 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ (A ∈ ℋ → (1 ·h A) = A)
14-Jun-2008	axhfvmul 8811	Derive axiom ax-hfvmul 8829 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ ·h :(ℂ × ℋ )–→ ℋ
14-Jun-2008	axhvaddid 8810	Derive axiom ax-hvaddid 8828 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ (A ∈ ℋ → (A +h 0h) = A)
14-Jun-2008	axhv0cl 8809	Derive axiom ax-hv0cl 8827 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ 0h ∈ ℋ
14-Jun-2008	axhvass 8808	Derive axiom ax-hvass 8826 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ⋀ C ∈ ℋ ) → ((A +h B) +h C) = (A +h (B +h C)))
14-Jun-2008	axhvcom 8807	Derive axiom ax-hvcom 8825 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ) → (A +h B) = (B +h A))
14-Jun-2008	axhfvadd 8806	Derive axiom ax-hfvadd 8824 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ +h :( ℋ × ℋ )–→ ℋ
13-Jun-2008	unidmrn 3511	The double union of the converse of a class is its field.
⊢ ∪∪◡A = (dom A ∪ ran A)
13-Jun-2008	opeqex 2794	Equivalence of existence implied by equality of ordered pairs.
⊢ (⟨A, B⟩ = ⟨C, D⟩ → (A ∈ V ↔ C ∈ V))
12-Jun-2008	dfhnorm2 8942	Alternate definition of the norm of a vector of Hilbert space. Definition of norm in [Beran] p. 96.
⊢ normh = {⟨x, y⟩∣(x ∈ ℋ ⋀ y = (√ ‘(x ·ih x)))}
12-Jun-2008	h2hlm 8804	The limit sequences of Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    &   ⊢ ℋ = (Base ‘U)    &   ⊢ D = (IndMet ‘U)    ⇒   ⊢ ⇝v = ((⇝m ‘D) ↾ ( ℋ ↑m ℕ))
12-Jun-2008	h2hcau 8803	The Cauchy sequences of Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    &   ⊢ ℋ = (Base ‘U)    &   ⊢ D = (IndMet ‘U)    ⇒   ⊢ Cauchy = ((Cau ‘D) ∩ ( ℋ ↑m ℕ))
12-Jun-2008	xp11b 3473	The second argument of a cross product is one-to-one.
⊢ (A ≠ ∅ → ((A × A) = (A × B) ↔ A = B))
12-Jun-2008	hbia1 1013	Lemma 23 of [Monk2] p. 114.
⊢ ((∀xφ → ∀xψ) → ∀x(∀xφ → ∀xψ))
11-Jun-2008	h2hmetdval 8802	Value of the distance function of the metric space of Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    &   ⊢ ℋ = (Base ‘U)    &   ⊢ D = (IndMet ‘U)    ⇒   ⊢ ((A ∈ ℋ ⋀ B ∈ ℋ ) → (ADB) = (normh ‘(A −h B)))
11-Jun-2008	h2hmetba 8801	The base set for the metric for Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    &   ⊢ ℋ = (Base ‘U)    &   ⊢ D = (IndMet ‘U)    ⇒   ⊢ ℋ = dom dom D
11-Jun-2008	h2hvs 8800	The vector subtraction operation of Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    &   ⊢ ℋ = (Base ‘U)    ⇒   ⊢ −h = ( −v ‘U)
11-Jun-2008	h2hnm 8799	The norm function of Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    ⇒   ⊢ normh = (norm ‘U)
11-Jun-2008	h2hsm 8798	The scalar product operation of Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    ⇒   ⊢ ·h = ( ·s ‘U)
11-Jun-2008	h2hva 8797	The group (addition) operation of Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    ⇒   ⊢ +h = ( +v ‘U)
10-Jun-2008	hlnvi 8554	Every complex Hilbert space is a normed complex vector space.
⊢ U ∈ CHil    ⇒   ⊢ U ∈ NrmCVec
10-Jun-2008	isnvi 8197	Properties that determine a normed complex vector space.
⊢ X = ran G    &   ⊢ Z = (Id ‘G)    &   ⊢ ⟨G, S⟩ ∈ CVec    &   ⊢ N:X–→ℝ    &   ⊢ ((x ∈ X ⋀ (N ‘x) = 0) → x = Z)    &   ⊢ ((y ∈ ℂ ⋀ x ∈ X) → (N ‘(ySx)) = ((abs ‘y) · (N ‘x)))    &   ⊢ ((x ∈ X ⋀ y ∈ X) → (N ‘(xGy)) ≤ ((N ‘x) + (N ‘y)))    &   ⊢ U = ⟨⟨G, S⟩, N⟩    ⇒   ⊢ U ∈ NrmCVec
10-Jun-2008	isnv 8196	The predicate "is a normed complex vector space."
⊢ X = ran G    &   ⊢ Z = (Id ‘G)    ⇒   ⊢ (⟨⟨G, S⟩, N⟩ ∈ NrmCVec ↔ (⟨G, S⟩ ∈ CVec ⋀ N:X–→ℝ ⋀ ∀x ∈ X (((N ‘x) = 0 → x = Z) ⋀ ∀y ∈ ℂ (N ‘(ySx)) = ((abs ‘y) · (N ‘x)) ⋀ ∀y ∈ X (N ‘(xGy)) ≤ ((N ‘x) + (N ‘y)))))

Also new:

(23-May-2008) Gérard Lang pointed me to Bob Solovay's note on AC and strongly inaccessible cardinals. One of the eventual goals for set.mm is to prove the Axiom of Choice from Grothendieck's axiom, like Mizar does, and this note may be helpful for anyone wanting to attempt that. Separately, I also came across a history of the size reduction of grothprim (viewable in Firefox and some versions of Internet Explorer).

(14-Apr-2008) A "/join" qualifier was added to the "search" command in the metamath program (version 0.07.37). This qualifier will join the $e hypotheses to the $a or $p for searching, so that math tokens in the $e's can be matched as well. For example, "search *com* +v" produces no results, but "search *com* +v /join" yields commutative laws involving vector addition. Thanks to Stefan Allan for suggesting this idea.

(8-Apr-2008) The 8,000th theorem, hlrel, was added to the Metamath Proof Explorer part of the database.

(2-Mar-2008) I added a small section to the end of the Deduction Theorem page.

(17-Feb-2008) ocat has uploaded the "1-Mar-2008" mmj2: mmj2.zip. See the description.

(16-Jan-2008) O'Cat has written mmj2 Proof Assistant Quick Tips.

(30-Dec-2007)