mmtheorems93 - 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-10687

<

Statement List for Metamath Proof Explorer - 9201-9300 - Page 93 of 107

Type	Label	Description
Statement
Theorem	pjthlem12 9201	Lemma for pjth 9204.
Theorem	pjthlem13 9202	Lemma for pjth 9204.
Theorem	pjthlem14 9203	Lemma for pjth 9204.
Theorem	pjth 9204	Projection Theorem: Any Hilbert space vector A can be decomposed into a member x of a closed subspace H and a member y of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part).
|- A e. H~   &   |- H e. CH   =>   |- E.x e. H E.y e. (_|_` H)A = (x +h y)
Theorem	pjtht 9205	Projection Theorem: Any Hilbert space vector A can be decomposed into a member x of a closed subspace H and a member y of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part).
|- ((H e. CH /\ A e. H~) -> E.x e. H E.y e. (_|_` H)A = (x +h y))
Theorem	pjtheu 9206	Uniqueness of x for the projection theorem. See pjtheu2 9221 for the uniqueness of y.
|- H e. CH   =>   |- (A e. H~ -> E!x e. H E.y e. (_|_` H)A = (x +h y))
Theorem	pjtheut 9207	Uniqueness of x for the projection theorem.
|- ((H e. CH /\ A e. H~) -> E!x e. H E.y e. (_|_` H)A = (x +h y))
Projectors
Definition	df-pj 9208	Define the projection function on a Hilbert space, as a mapping from the Hilbert lattice to a function on Hilbert space. Every closed subspace is associated with a unique projection function. Remark in [Kalmbach] p. 66, adopted as a definition. (proj` H)` A is the projection of vector A onto closed subspace H. Note that the range of proj is the set of all projection operators, so T e. ran proj means that T is a projection operator.
|- proj = {<.h, f>. | (h e. CH /\ f = {<.x, y>. | (x e. H~ /\ y = U.{z e. h | E.w e. (_|_` h)x = (z +h w)})})}
Theorem	pjmvalt 9209	The value of the projection map.
|- (H e. CH -> (proj` H) = {<.x, y>. | (x e. H~ /\ y = U.{z e. H | E.w e. (_|_` H)x = (z +h w)})})
Theorem	pjvalt 9210	Value of a projection.
|- ((H e. CH /\ A e. H~) -> ((proj` H)` A) = U.{x e. H | E.y e. (_|_` H)A = (x +h y)})
Theorem	axpjclt 9211	Closure of a projection in its subspace. If we consider this together with axpjpjt 9227 to be axioms, the need for the ax-hcompl 9043 can often be avoided for the kinds of theorems we are interested in here. An interesting project is to see how far we can go by using them in place of it. In particular, we can prove the orthomodular law pjoml 9239.)
|- ((H e. CH /\ A e. H~) -> ((proj` H)` A) e. H)
Theorem	pjeq2t 9212	Equality with a projection.
|- ((H e. CH /\ A e. H~ /\ B e. H) -> (((proj` H)` A) = B <-> E.x e. (_|_` H)A = (B +h x)))
Theorem	pjeqt 9213	Equality with a projection.
|- ((H e. CH /\ A e. H~) -> (((proj` H)` A) = B <-> (B e. H /\ E.x e. (_|_` H)A = (B +h x))))
Theorem	pjhclt 9214	Closure of a projection in Hilbert space.
|- ((H e. CH /\ A e. H~) -> ((proj` H)` A) e. H~)
Orthomodular law
Theorem	omlsilem 9215	Lemma for orthomodular law in the Hilbert lattice.
Theorem	omlsi 9216	Subspace inference form of orthomodular law in the Hilbert lattice.
|- A e. CH   &   |- B e. SH   &   |- A (_ B   &   |- (B i^i (_|_` A)) = 0H   =>   |- A = B
Theorem	omls 9217	Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22.
|- A e. CH   &   |- B e. SH   =>   |- ((A (_ B /\ (B i^i (_|_` A)) = 0H) -> A = B)
Theorem	ococ 9218	Complement of complement of a closed subspace of Hilbert space. Theorem 3.7(ii) of [Beran] p. 102.
|- A e. CH   =>   |- (_|_` (_|_` A)) = A
Theorem	ococt 9219	Complement of complement of a closed subspace of Hilbert space. Theorem 3.7(ii) of [Beran] p. 102.
|- (A e. CH -> (_|_` (_|_` A)) = A)
Theorem	dfch2 9220	Alternate definition of the Hilbert lattice.
|- CH = {x | (x (_ H~ /\ (_|_` (_|_` x)) = x)}
Projectors (cont.)
Theorem	pjtheu2 9221	Uniqueness of y for the projection theorem.
|- H e. CH   =>   |- (A e. H~ -> E!y e. (_|_` H)E.x e. H A = (x +h y))
Theorem	pjcl 9222	Closure of a projection in its subspace.
|- H e. CH   =>   |- (A e. H~ -> ((proj` H)` A) e. H)
Theorem	pjhcl 9223	Closure of a projection in Hilbert space.
|- H e. CH   =>   |- (A e. H~ -> ((proj` H)` A) e. H~)
Theorem	pjcli 9224	Closure of a projection in its subspace.
|- H e. CH   &   |- A e. H~   =>   |- ((proj` H)` A) e. H
Theorem	pjhcli 9225	Closure of a projection in Hilbert space.
|- H e. CH   &   |- A e. H~   =>   |- ((proj` H)` A) e. H~
Theorem	pjpj0 9226	Decomposition of a vector into projections.
|- H e. CH   &   |- A e. H~   =>   |- A = (((proj` H)` A) +h ((proj` (_|_` H))` A))
Theorem	axpjpjt 9227	Decomposition of a vector into projections. See comment in axpjclt 9211.
|- ((H e. CH /\ A e. H~) -> A = (((proj` H)` A) +h ((proj` (_|_` H))` A)))
Theorem	pjpj 9228	Decomposition of a vector into projections.
|- H e. CH   &   |- A e. H~   =>   |- A = (((proj` H)` A) +h ((proj` (_|_` H))` A))
Theorem	pjpjtht 9229	Projection Theorem: Any Hilbert space vector A can be decomposed into a member x of a closed subspace H and a member y of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part).
|- ((H e. CH /\ A e. H~) -> E.x e. H E.y e. (_|_` H)A = (x +h y))
Theorem	pjpjth 9230	Projection Theorem: Any Hilbert space vector A can be decomposed into a member x of a closed subspace H and a member y of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part).
|- A e. H~   &   |- H e. CH   =>   |- E.x e. H E.y e. (_|_` H)A = (x +h y)
Theorem	pjopt 9231	Orthocomplement projection in terms of projection.
|- ((H e. CH /\ A e. H~) -> ((proj` (_|_` H))` A) = (A -h ((proj` H)` A)))
Theorem	pjpot 9232	Projection in terms of orthocomplement projection.
|- ((H e. CH /\ A e. H~) -> ((proj` H)` A) = (A -h ((proj` (_|_` H))` A)))
Theorem	pjop 9233	Orthocomplement projection in terms of projection.
|- H e. CH   &   |- A e. H~   =>   |- ((proj` (_|_` H))` A) = (A -h ((proj` H)` A))
Theorem	pjpo 9234	Projection in terms of orthocomplement projection.
|- H e. CH   &   |- A e. H~   =>   |- ((proj` H)` A) = (A -h ((proj` (_|_` H))` A))
Theorem	pjoc1 9235	Projection of a vector in the orthocomplement of the projection subspace.
|- H e. CH   &   |- A e. H~   =>   |- (A e. H <-> ((proj` (_|_` H))` A) = 0h)
Theorem	pjch 9236	Projection of a vector in the projection subspace. Lemma 4.4(ii) of [Beran] p. 111.
|- H e. CH   &   |- A e. H~   =>   |- (A e. H <-> ((proj` H)` A) = A)
Theorem	pjocclt 9237	The part of a vector that belongs to the orthocomplemented space.
|- ((H e. CH /\ A e. H~) -> (A -h ((proj` H)` A)) e. (_|_` H))
Theorem	pjoc1t 9238	Projection of a vector in the orthocomplement of the projection subspace.
|- ((H e. CH /\ A e. H~) -> (A e. H <-> ((proj` (_|_` H))` A) = 0h))
Theorem	pjoml 9239	Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22. Derived using projections; compare omls 9217.
|- A e. CH   &   |- B e. SH   =>   |- ((A (_ B /\ (B i^i (_|_` A)) = 0H) -> A = B)
Theorem	pjomlt 9240	Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22. Derived using projections; compare omls 9217.
|- (((A e. CH /\ B e. SH) /\ (A (_ B /\ (B i^i (_|_` A)) = 0H)) -> A = B)
Theorem	pjococ 9241	Proof of orthocomplement theorem using projections. Compare ococ 9218.
|- H e. CH   =>   |- (_|_` (_|_` H)) = H
Theorem	pjoc2 9242	Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of [Beran] p. 111.
|- H e. CH   &   |- A e. H~   =>   |- (A e. (_|_` H) <-> ((proj` H)` A) = 0h)
Theorem	pjoc2t 9243	Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of [Beran] p. 111.
|- ((H e. CH /\ A e. H~) -> (A e. (_|_` H) <-> ((proj` H)` A) = 0h))
Subspace sum, span, lattice join, lattice supremum
Definition	df-shsum 9244	Define subspace sum in SH. See shsumvalt 9248, shsumval2 9331, and shsumval3 9332 for its value.
|- +H = {<.<.x, y>., z>. | ((x e. SH /\ y e. SH) /\ z = {w e. H~ | E.v e. x E.u e. y w = (v +h u)})}
Definition	df-span 9245	Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanvalt 9270 for its value.
|- span = {<.x, y>. | (x (_ H~ /\ y = |^|{z e. SH | x (_ z})}
Definition	df-chj 9246	Define Hilbert lattice join. See chjvalt 9293 for its value and chjclt 9300 for its closure law. Note that we define it over all Hilbert space subsets to allow proving more general theorems. Even for general subsets the join belongs to CH; see sshjclt 9298. For an alternate definition see dfchj2 9295.
|- vH = {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))}
Definition	df-chsup 9247	Define the supremum of a set of Hilbert lattice elements. See chsupval2t 9273 for its value and dfchsup2 9269 for an alternate definition. We actually define the supremum for an arbitrary collection of Hilbert space subsets, not just elements of the Hilbert lattice CH, to allow more general theorems. Even for general subsets the supremum still a Hilbert lattice element; see hsupclt 9278.
|- \/H = {<.x, y>. | (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))}
Theorem	shsumvalt 9248	Value of subspace sum of two Hilbert space subspaces. Definition of subspace sum in [Kalmbach] p. 65.
|- ((A e. SH /\ B e. SH) -> (A +H B) = {x e. H~ | E.y e. A E.z e. B x = (y +h z)})
Theorem	shselt 9249	Membership in the subspace sum of two Hilbert subspaces.
|- ((A e. SH /\ B e. SH) -> (C e. (A +H B) <-> E.x e. A E.y e. B C = (x +h y)))
Theorem	shsel3t 9250	Membership in the subspace sum of two Hilbert subspaces, using vector subtraction.