mmtheorems95 - 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-10682

Statement List for Metamath Proof Explorer - 9401-9500 - Page 95 of 107

Type	Label	Description
Statement
Theorem	chlubt 9401	Hilbert lattice join is the least upper bound of two elements.
|- ((A e. CH /\ B e. CH /\ C e. CH) -> ((A (_ C /\ B (_ C) <-> (A vH B) (_ C))
Theorem	chlej1t 9402	Add join to both sides of Hilbert lattice ordering.
|- (((A e. CH /\ B e. CH /\ C e. CH) /\ A (_ B) -> (A vH C) (_ (B vH C))
Theorem	chlej2t 9403	Add join to both sides of Hilbert lattice ordering.
|- (((A e. CH /\ B e. CH /\ C e. CH) /\ A (_ B) -> (C vH A) (_ (C vH B))
Theorem	chlejb1t 9404	Hilbert lattice ordering in terms of join.
|- ((A e. CH /\ B e. CH) -> (A (_ B <-> (A vH B) = B))
Theorem	chlejb2t 9405	Hilbert lattice ordering in terms of join.
|- ((A e. CH /\ B e. CH) -> (A (_ B <-> (B vH A) = B))
Theorem	chnlet 9406	Equivalent expressions for "not less than" in the Hilbert lattice.
|- ((A e. CH /\ B e. CH) -> (-. B (_ A <-> A (. (A vH B)))
Theorem	chjot 9407	The join of a closed subspace and its orthocomplement is all of Hilbert space.
|- (A e. CH -> (A vH (_|_` A)) = H~)
Theorem	chabs1t 9408	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.
|- ((A e. CH /\ B e. CH) -> (A vH (A i^i B)) = A)
Theorem	chabs2t 9409	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.
|- ((A e. CH /\ B e. CH) -> (A i^i (A vH B)) = A)
Theorem	chabs1 9410	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.
|- A e. CH   &   |- B e. CH   =>   |- (A vH (A i^i B)) = A
Theorem	chabs2 9411	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.
|- A e. CH   &   |- B e. CH   =>   |- (A i^i (A vH B)) = A
Theorem	chjidmt 9412	Idempotent law for Hilbert lattice join.
|- (A e. CH -> (A vH A) = A)
Theorem	chjidm 9413	Idempotent law for Hilbert lattice join.
|- A e. CH   =>   |- (A vH A) = A
Theorem	chj12 9414	A rearrangement of Hilbert lattice join.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   =>   |- (A vH (B vH C)) = (B vH (A vH C))
Theorem	chj4 9415	Rearrangement of the join of 4 Hilbert lattice elements.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   &   |- D e. CH   =>   |- ((A vH B) vH (C vH D)) = ((A vH C) vH (B vH D))
Theorem	chjjdir 9416	Hilbert lattice join distributes over itself.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   =>   |- ((A vH B) vH C) = ((A vH C) vH (B vH C))
Theorem	chdmm1t 9417	DeMorgan's law for meet in a Hilbert lattice.
|- ((A e. CH /\ B e. CH) -> (_|_` (A i^i B)) = ((_|_` A) vH (_|_` B)))
Theorem	chdmm2t 9418	DeMorgan's law for meet in a Hilbert lattice.
|- ((A e. CH /\ B e. CH) -> (_|_` ((_|_` A) i^i B)) = (A vH (_|_` B)))
Theorem	chdmm3t 9419	DeMorgan's law for meet in a Hilbert lattice.
|- ((A e. CH /\ B e. CH) -> (_|_` (A i^i (_|_` B))) = ((_|_` A) vH B))
Theorem	chdmm4t 9420	DeMorgan's law for meet in a Hilbert lattice.
|- ((A e. CH /\ B e. CH) -> (_|_` ((_|_` A) i^i (_|_` B))) = (A vH B))
Theorem	chdmj1t 9421	DeMorgan's law for join in a Hilbert lattice.
|- ((A e. CH /\ B e. CH) -> (_|_` (A vH B)) = ((_|_` A) i^i (_|_` B)))
Theorem	chdmj2t 9422	DeMorgan's law for join in a Hilbert lattice.
|- ((A e. CH /\ B e. CH) -> (_|_` ((_|_` A) vH B)) = (A i^i (_|_` B)))
Theorem	chdmj3t 9423	DeMorgan's law for join in a Hilbert lattice.
|- ((A e. CH /\ B e. CH) -> (_|_` (A vH (_|_` B))) = ((_|_` A) i^i B))
Theorem	chdmj4t 9424	DeMorgan's law for join in a Hilbert lattice.
|- ((A e. CH /\ B e. CH) -> (_|_` ((_|_` A) vH (_|_` B))) = (A i^i B))
Theorem	chjasst 9425	Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14.
|- ((A e. CH /\ B e. CH /\ C e. CH) -> ((A vH B) vH C) = (A vH (B vH C)))
Theorem	chj12t 9426	A rearrangement of Hilbert lattice join.
|- ((A e. CH /\ B e. CH /\ C e. CH) -> (A vH (B vH C)) = (B vH (A vH C)))
Theorem	chj4t 9427	Rearrangement of the join of 4 Hilbert lattice elements.
|- (((A e. CH /\ B e. CH) /\ (C e. CH /\ D e. CH)) -> ((A vH B) vH (C vH D)) = ((A vH C) vH (B vH D)))
Theorem	ledi 9428	An ortholattice is distributive in one ordering direction.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   =>   |- ((A i^i B) vH (A i^i C)) (_ (A i^i (B vH C))
Theorem	ledir 9429	An ortholattice is distributive in one ordering direction.
|- A e. CH   &   |- B e. CH   &   |- C e. CH   =>   |- ((A i^i C) vH (B i^i C)) (_ ((A vH B) i^i C)
Theorem	lejdi 9430	An ortholattice is distributive in one ordering direction (join version).
|- A e. CH   &   |- B e. CH   &   |- C e. CH   =>   |- (A vH (B i^i C)) (_ ((A vH B) i^i (A vH C))
Theorem	lejdir 9431	An ortholattice is distributive in one ordering direction (join version).
|- A e. CH   &   |- B e. CH   &   |- C e. CH   =>   |- ((A i^i B) vH C) (_ ((A vH C) i^i (B vH C))
Theorem	ledit 9432	An ortholattice is distributive in one ordering direction.
|- ((A e. CH /\ B e. CH /\ C e. CH) -> ((A i^i B) vH (A i^i C)) (_ (A i^i (B vH C)))
Span (cont.) and one-dimensional subspaces
Theorem	spansn0 9433	The span of the singleton of the zero vector is the zero subspace.
|- (span` {0h}) = 0H
Theorem	span0 9434	The span of the empty set is the zero subspace. Remark 11.6.e of [Schechter] p. 276.
|- (span` (/)) = 0H
Theorem	elspan 9435	Membership in the span of a subset of Hilbert space.
|- B e. V   =>   |- (A (_ H~ -> (B e. (span` A) <-> A.x e. SH (A (_ x -> B e. x)))
Theorem	spanun 9436	The span of a union is the subspace sum of spans.
|- A (_ H~   &   |- B (_ H~   =>   |- (span` (A u. B)) = ((span` A) +H (span` B))
Theorem	spanunt 9437	The span of a union is the subspace sum of spans.
|- ((A (_ H~ /\ B (_ H~) -> (span` (A u. B)) = ((span` A) +H (span` B)))
Theorem	sshhococ 9438	The join of two Hilbert space subsets (not necessarily closed subspaces) equals the join of their closures (double orthocomplements).
|- A (_ H~   &   |- B (_ H~   =>   |- (A vH B) = ((_|_` (_|_` A)) vH (_|_` (_|_` B)))
Theorem	hne0 9439	Hilbert space has a nonzero vector iff it is not trivial.
|- (H~ =/= 0H <-> E.x e. H~ x =/= 0h)
Theorem	chsup0 9440	The supremum of the empty set.
|- ( \/H ` (/)) = 0H
Theorem	h1deot 9441	Membership in orthocomplement of 1-dimensional subspace.
|- B e. H~   =>   |- (A e. (_|_` {B}) <-> (A e. H~ /\ (A .ih B) = 0))
Theorem	h1det 9442	Membership in 1-dimensional subspace.
|- B e. H~   =>   |- (A e. (_|_` (_|_` {B})) <-> (A e. H~ /\ A.x e. H~ ((B .ih x) = 0 -> (A .ih x) = 0)))
Theorem	h1did 9443	A generating vector belongs to the 1-dimensional subspace it generates.
|- (A e. H~ -> A e. (_|_` (_|_` {A})))
Theorem	h1dn0 9444	A non-zero vector generates a (non-zero) 1-dimensional subspace.
|- ((A e. H~ /\ A =/= 0h) -> (_|_` (_|_` {A})) =/= 0H)
Theorem	h1de2 9445	Membership in 1-dimensional subspace. All members are collinear with the generating vector.
|- A e. H~   &   |- B e. H~   =>   |- (A e. (_|_` (_|_` {B})) -> ((B .ih B) .h A) = ((A .ih B) .h B))
Theorem	h1de2b 9446	Membership in 1-dimensional subspace. All members are collinear with the generating vector.
|- A e. H~   &   |- B e. H~   =>   |- (B =/= 0h -> (A e. (_|_` (_|_` {B})) <-> A = (((A .ih B) / (B .ih B)) .h B)))
Theorem	h1de2bOLD 9447	Membership in 1-dimensional subspace. All members are collinear with the generating vector.
|- A e. H~   &   |- B e. H~   =>   |- (-. B = 0h -> (A e. (_|_` (_|_` {B})) <-> A = (((A .ih B) / (B .ih B)) .h B)))
Theorem	h1de2ctlem 9448	Lemma for h1de2ct 9449.
Theorem	h1de2ct 9449	Membership in 1-dimensional subspace. All members are collinear with the generating vector.
|- B e. H~   =>   |- (A e. (_|_` (_|_` {B})) <-> E.x e. CC A = (x .h B))
Theorem	spansn 9450	The span of a singleton in Hilbert space equals its closure.
|- A e. H~   =>   |- (span` {A}) = (_|_` (_|_` {A}))
Theorem	elspansn 9451	Membership in the span of a singleton.
|- A e. H~   =>   |- (B