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 5-Jul-2008 at 2:29 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
5-Jul-2008	pjocco 10077	Composition of projections of a subspace and its orthocomplement.
⊢ H ∈ Cℋ    ⇒   ⊢ ((proj ‘H) ∘ (proj ‘(⊥ ‘H))) = 0hop
5-Jul-2008	leoptrt 10041	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 10018	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 2875	Union of a singleton in the form of a restricted class abstraction.
⊢ (A ∈ B → ∪{x ∈ B∣x = A} = A)
2-Jul-2008	nmopcoadj0 10007	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 472	Syllogism inference with commutation of antecents.
⊢ ((φ ⋀ ψ) → χ)    &   ⊢ ((χ ⋀ ψ) → θ)    ⇒   ⊢ ((φ ⋀ ψ) → θ)
1-Jul-2008	supmax 4580	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 4579	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 3279	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 9995	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 9124	Hilbert space property of a closed subspace.
⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩    &   ⊢ H ∈ Cℋ    ⇒   ⊢ W ∈ CHil
29-Jun-2008	hhssims2 9118	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	funop 3548	A Kuratowski ordered pair is a function only if its components are equal.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (Fun ⟨A, B⟩ → A = B)
29-Jun-2008	brelrn 3345	The second argument of a binary relation belongs to its range.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (ACB → B ∈ ran C)
29-Jun-2008	brelrng 3343	The second argument of a binary relation belongs to its range.
⊢ ((A ∈ F ⋀ B ∈ G ⋀ ACB) → B ∈ ran C)
29-Jun-2008	ordtri3or 2978	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 1920	Consequence of "at most one."
⊢ (x = A → (φ ↔ ψ))    ⇒   ⊢ (((A ∈ B ⋀ ∃*xφ) ⋀ (φ ⋀ ψ)) → x = A)
28-Jun-2008	hhssims 9117	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 9112	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 4483	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 8255	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 9105	Abelian group property of subspace addition.
⊢ (H ∈ Sℋ → ( +h ↾ (H × H)) ∈ Abel)
24-Jun-2008	spwnex 8616	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 8823	Derive axiom ax-hilex 8841 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 8823 through axhcompl 8840, 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 8809 above. See also the comment in ax-hilex 8841.
⊢ 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 8840	Derive axiom ax-hcompl 9043 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ (F ∈ Cauchy → ∃x ∈ ℋ F ⇝v x)
22-Jun-2008	axhis4 8839	Derive axiom ax-his4 8924 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 8838	Derive axiom ax-his3 8923 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 8837	Derive axiom ax-his2 8922 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 8836	Derive axiom ax-his1 8921 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 8835	Derive axiom ax-hfi 8918 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 1353	Version of dveeq1 1352 using ax-16 1208 instead of ax-17 969.
⊢ (¬ ∀x x = y → (y = z → ∀x y = z))
19-Jun-2008	axhvmul0 8834	Derive axiom ax-hvmul0 8852 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ (A ∈ ℋ → (0 ·h A) = 0h)
19-Jun-2008	axhvdistr2 8833	Derive axiom ax-hvdistr2 8851 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 1211	Version of dveeq2 1210 using ax-16 1208 instead of ax-17 969.
⊢ (¬ ∀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 10395	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. (Part of Jeff Hoffman's sandbox.)
⊢ ((A ∈ ℕ ⋀ B ∈ ℕ) → (A < B → gcd(A, B) = gcd(A, (B − A))))
17-Jun-2008	nndivlub 10392	A factor of a natural number cannot exceed it. (Part of Jeff Hoffman's sandbox.)
⊢ ((A ∈ ℕ ⋀ B ∈ ℕ) → ((A / B) ∈ ℕ → B ≤ A))
17-Jun-2008	nndivsub 10391	Please add description here. (Part of Jeff Hoffman's sandbox.)
⊢ (((A ∈ ℕ ⋀ B ∈ ℕ ⋀ C ∈ ℕ) ⋀ ((A / C) ∈ ℕ ⋀ A < B)) → ((B / C) ∈ ℕ ↔ ((B − A) / C) ∈ ℕ))
17-Jun-2008	nnssi3 10390	Convert a theorem for real/complex numbers into one for natural numbers. (Part of Jeff Hoffman's sandbox.)
⊢ ℕ ⊆ D    &   ⊢ (C ∈ ℕ → φ)    &   ⊢ (((A ∈ D ⋀ B ∈ D ⋀ C ∈ D) ⋀ φ) → ψ)    ⇒   ⊢ ((A ∈ ℕ ⋀ B ∈ ℕ ⋀ C ∈ ℕ) → ψ)
17-Jun-2008	nnssi2 10389	Convert a theorem for real/complex numbers into one for natural numbers. (Part of Jeff Hoffman's sandbox.)
⊢ ℕ ⊆ D    &   ⊢ (B ∈ ℕ → φ)    &   ⊢ ((A ∈ D ⋀ B ∈ D ⋀ φ) → ψ)    ⇒   ⊢ ((A ∈ ℕ ⋀ B ∈ ℕ) → ψ)
17-Jun-2008	gelsupval 10388	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. (Part of Jeff Hoffman's sandbox.)
⊢ R Or A    ⇒   ⊢ ((C ∈ B ⋀ (C ∈ A ⋀ ∀y ∈ B ¬ CRy)) → sup(B, A, R) = C)
17-Jun-2008	gelcompl 10387	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. (Part of Jeff Hoffman's sandbox.)
⊢ ((x ∈ A ⋀ (∀z ∈ B ¬ xRz ⋀ x ∈ B)) → ∃x ∈ A (∀y ∈ B ¬ xRy ⋀ ∀y ∈ A (yRx → ∃z ∈ B yRz)))
17-Jun-2008	axhvdistr1 8832	Derive axiom ax-hvdistr1 8850 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 1351	Version of dvelim 1350 that doesn't use ax-10 964. (See dvelimfALT 1151 for a version that doesn't use ax-11 965.)
⊢ (φ → ∀xφ)    &   ⊢ (z = y → (φ ↔ ψ))    ⇒   ⊢ (¬ ∀x x = y → (ψ → ∀xψ))
14-Jun-2008	axhvmulass 8831	Derive axiom ax-hvmulass 8849 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 8830	Derive axiom ax-hvmulid 8848 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ (A ∈ ℋ → (1 ·h A) = A)
14-Jun-2008	axhfvmul 8829	Derive axiom ax-hfvmul 8847 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ ·h :(ℂ × ℋ )–→ ℋ
14-Jun-2008	axhvaddid 8828	Derive axiom ax-hvaddid 8846 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ (A ∈ ℋ → (A +h 0h) = A)
14-Jun-2008	axhv0cl 8827	Derive axiom ax-hv0cl 8845 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ 0h ∈ ℋ
14-Jun-2008	axhvass 8826	Derive axiom ax-hvass 8844 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 8825	Derive axiom ax-hvcom 8843 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 8824	Derive axiom ax-hfvadd 8842 from Hilbert space under ZF set theory.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ CHil    ⇒   ⊢ +h :( ℋ × ℋ )–→ ℋ
13-Jun-2008	unidmrn 3517	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 8960	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 8822	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 8821	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 3478	The second argument of a cross product is one-to-one.
⊢ (A ≠ ∅ → ((A × A) = (A × B) ↔ A = B))
12-Jun-2008	hbia1 1012	Lemma 23 of [Monk2] p. 114.
⊢ ((∀xφ → ∀xψ) → ∀x(∀xφ → ∀xψ))
11-Jun-2008	h2hmetdval 8820	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 8819	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 8818	The vector subtraction operation of Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    &   ⊢ ℋ = (Base ‘U)    ⇒   ⊢ −h = ( −v ‘U)
11-Jun-2008	h2hnm 8817	The norm function of Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    ⇒   ⊢ normh = (norm ‘U)
11-Jun-2008	h2hsm 8816	The scalar product operation of Hilbert space.
⊢ U = ⟨⟨ +h , ·h ⟩, normh⟩    &   ⊢ U ∈ NrmCVec    ⇒   ⊢ ·h = ( ·s ‘U)
11-Jun-2008	h2hva 8815	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)))))
9-Jun-2008	nvex 8195	The components of a normed complex vector space are sets.
⊢ (⟨⟨G, S⟩, N⟩ ∈ NrmCVec → (G ∈ V ⋀ S ∈ V ⋀ N ∈ V))
8-Jun-2008	funopg 3549	A Kuratowski ordered pair is a function only if its components are equal.
⊢ ((B ∈ C ⋀ Fun ⟨A, B⟩) → A = B)
7-Jun-2008	isnvlem 8193	Lemma for isnv 8196.
⊢ X = ran G    &   ⊢ Z = (Id ‘G)    ⇒   ⊢ ((G ∈ V ⋀ S ∈ V ⋀ N ∈ V) → (⟨⟨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))))))
7-Jun-2008	relop 3275	A necessary and sufficient condition for a Kuratowski ordered pair to be a relation.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (Rel ⟨A, B⟩ ↔ ∃x∃y(A = {x} ⋀ B = {x, y}))
7-Jun-2008	ax16ALT 1269	Version of ax16 1207 that doesn't require ax-10 964 or ax-12 966 for its proof.
⊢ (∀x x = y → (φ → ∀xφ))
6-Jun-2008	abscncfALT 8305	Absolute value is continuous. Alternate proof of abscncf 7229.
⊢ abs ∈ (ℂ–cn→ℝ)
6-Jun-2008	nvvcop 8177	A normed complex vector space is a vector space.
⊢ (⟨⟨G, S⟩, N⟩ ∈ NrmCVec → ⟨G, S⟩ ∈ CVec)
6-Jun-2008	opeqpr 2800	Equivalence for an ordered pair equal to an unordered pair.
⊢ C ∈ V    &   ⊢ D ∈ V    ⇒   ⊢ (⟨A, B⟩ = {C, D} ↔ ((C = {A} ⋀ D = {A, B}) ⋁ (C = {A, B} ⋀ D = {A})))
5-Jun-2008	hhssph 9116	Inner product space property of a subspace.
⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩    &   ⊢ H ∈ Sℋ    ⇒   ⊢ W ∈ CPreHil
5-Jun-2008	abscn 8304	The absolute value function on complex numbers is continuous.
⊢ C = (abs ∘ − )    &   ⊢ R = ((abs ∘ − ) ↾ (ℝ × ℝ))    &   ⊢ J = (Open ‘C)    &   ⊢ K = (Open ‘R)    ⇒   ⊢ abs ∈ (J Cn K)
5-Jun-2008	opeqsn 2799	Equivalence for an ordered pair equal to a singleton.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ (⟨A, B⟩ = {C} ↔ (A = B ⋀ C = {A}))
4-Jun-2008	symgidi 10375	The value of the identity element of the symmetry group on A (Contributed by Paul Chapman, 25-Feb-2008.)
⊢ A ∈ V    ⇒   ⊢ (Id ‘(SymGrp ‘A)) = (I ↾ A)
4-Jun-2008	symggrpi 10374	The symmetry group on A is a group (inference version). (Contributed by Paul Chapman, 25-Feb-2008.)
⊢ A ∈ V    ⇒   ⊢ (SymGrp ‘A) ∈ Grp
4-Jun-2008	spwcl 8615	Closure of a supremum.
⊢ X = dom R    &   ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy)))    ⇒   ⊢ ((R ∈ Poset ⋀ A ∈ W ⋀ ∃x ∈ X φ) → (R supw A) ∈ X)
4-Jun-2008	unidmrnOLD 3516	The double union of the universal restriction of a class.
⊢ ∪∪(A ↾ V) = (dom A ∪ ran A)
4-Jun-2008	preqsn 2483	Equivalence for a pair equal to a singleton.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C ∈ V    ⇒   ⊢ ({A, B} = {C} ↔ (A = B ⋀ B = C))
3-Jun-2008	hhssbn 9123	Banach space property of a closed subspace.
⊢ W = ⟨⟨( +h ↾ (H × H)), ( ·h ↾ (ℂ × H))⟩, (normh ↾ H)⟩    &   ⊢ H ∈ Cℋ    ⇒   ⊢ W ∈ CBan
3-Jun-2008	isvc 8164	The predicate "is a complex vector space."
⊢ X = ran G    ⇒   ⊢ (⟨G, S⟩ ∈ CVec ↔ (G ∈ Abel ⋀ S:(ℂ × X)–→X ⋀ ∀x ∈ X ((1Sx) = x ⋀ ∀y ∈ ℂ (∀z ∈ X (yS(xGz)) = ((ySx)G(ySz)) ⋀ ∀z ∈ ℂ (((y + z)Sx) = ((ySx)G(zSx)) ⋀ ((y · z)Sx) = (yS(zSx)))))))
3-Jun-2008	ssxpr 3475	A cross-product subclass relationship implies the relationship for it components.
⊢ (((A × B) ≠ ∅ ⋀ (A × B) ⊆ (C × D)) → (A ⊆ C ⋀ B ⊆ D))
2-Jun-2008	vcex 8163	The components of a complex vector space are sets.
⊢ (⟨G, S⟩ ∈ CVec → (G ∈ V ⋀ S ∈ V))
2-Jun-2008	vcoprne 8162	The operations of a complex vector space cannot be identical.
⊢ (⟨G, S⟩ ∈ CVec → G ≠ S)
2-Jun-2008	isvclem 8160	Lemma for isvc 8164.
⊢ X = ran G    ⇒   ⊢ ((G ∈ V ⋀ S ∈ V) → (⟨G, S⟩ ∈ CVec ↔ (G ∈ Abel ⋀ S:(ℂ × X)–→X ⋀ ∀x ∈ X ((1Sx) = x ⋀ ∀y ∈ ℂ (∀z ∈ X (yS(xGz)) = ((ySx)G(ySz)) ⋀ ∀z ∈ ℂ (((y + z)Sx) = ((ySx)G(zSx)) ⋀ ((y · z)Sx) = (yS(zSx))))))))
2-Jun-2008	ax16i 1268	Inference with ax-16 1208 as its conclusion, that doesn't require ax-10 964, ax-11 965, or ax-12 966 for its proof. The hypotheses may be eliminable without one or more of these axioms in special cases.
⊢ (x = z → (φ ↔ ψ))    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x x = y → (φ → ∀xφ))
1-Jun-2008	idcvvidc 10667	Functor preserves codomain. JFM CAT1 th. 98.
⊢ M1 = dom (dom ‘T)    &   ⊢ C1 = (cod ‘T)    &   ⊢ I1 = (id ‘T)    &   ⊢ I2 = (id ‘U)    &   ⊢ C2 = (cod ‘U)    ⇒   ⊢ ((T ∈ Cat ⋀ U ∈ Cat) → (F ∈ (Func ‘⟨T, U⟩) → ∀m ∈ M1 (F ‘(I1 ‘(C1 ‘m))) = (I2 ‘(C2 ‘(F ‘m)))))
1-Jun-2008	iddvvidd 10666	Functors preserves domain. JFM CAT1 th. 98.
⊢ M1 = dom (dom ‘T)    &   ⊢ D1 = (dom ‘T)    &   ⊢ I1 = (id ‘T)    &   ⊢ I2</