mmtheorems96 - 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-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 9501-9600 - Page 96 of 123

Type	Label	Description
Statement
Theorem	pjthlem7 9501	Lemma for pjthi 9509.
Theorem	pjthlem8 9502	Lemma for pjthi 9509.
Theorem	pjthlem9 9503	Lemma for pjthi 9509.
Theorem	pjthlem10 9504	Lemma for pjthi 9509.
Theorem	pjthlem11 9505	Lemma for pjthi 9509.
Theorem	pjthlem12 9506	Lemma for pjthi 9509.
Theorem	pjthlem13 9507	Lemma for pjthi 9509.
Theorem	pjthlem14 9508	Lemma for pjthi 9509.
Theorem	pjthi 9509	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	pjth 9510	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	pjtheui 9511	Uniqueness of x for the projection theorem. See pjtheu2i 9526 for the uniqueness of y.
|- H e. CH   =>   |- (A e. H~ -> E!x e. H E.y e. (_|_` H)A = (x +h y))
Theorem	pjtheu 9512	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 9513	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	pjmval 9514	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	pjval 9515	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	axpjcl 9516	Closure of a projection in its subspace. If we consider this together with axpjpj 9532 to be axioms, the need for the ax-hcompl 9347 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 pjomli 9544.)
|- ((H e. CH /\ A e. H~) -> ((proj` H)` A) e. H)
Theorem	pjeq2 9517	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	pjeq 9518	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	pjhcl 9519	Closure of a projection in Hilbert space.
|- ((H e. CH /\ A e. H~) -> ((proj` H)` A) e. H~)
Orthomodular law
Theorem	omlsilem 9520	Lemma for orthomodular law in the Hilbert lattice.
Theorem	omlsii 9521	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	omlsi 9522	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	ococi 9523	Complement of complement of a closed subspace of Hilbert space. Theorem 3.7(ii) of [Beran] p. 102.
|- A e. CH   =>   |- (_|_` (_|_` A)) = A
Theorem	ococ 9524	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 9525	Alternate definition of the Hilbert lattice.
|- CH = {x | (x (_ H~ /\ (_|_` (_|_` x)) = x)}
Projectors (cont.)
Theorem	pjtheu2i 9526	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	pjcli 9527	Closure of a projection in its subspace.
|- H e. CH   =>   |- (A e. H~ -> ((proj` H)` A) e. H)
Theorem	pjhcli 9528	Closure of a projection in Hilbert space.
|- H e. CH   =>   |- (A e. H~ -> ((proj` H)` A) e. H~)
Theorem	pjclii 9529	Closure of a projection in its subspace.
|- H e. CH   &   |- A e. H~   =>   |- ((proj` H)` A) e. H
Theorem	pjhclii 9530	Closure of a projection in Hilbert space.
|- H e. CH   &   |- A e. H~   =>   |- ((proj` H)` A) e. H~
Theorem	pjpj0i 9531	Decomposition of a vector into projections.
|- H e. CH   &   |- A e. H~   =>   |- A = (((proj` H)` A) +h ((proj` (_|_` H))` A))
Theorem	axpjpj 9532	Decomposition of a vector into projections. See comment in axpjcl 9516.
|- ((H e. CH /\ A e. H~) -> A = (((proj` H)` A) +h ((proj` (_|_` H))` A)))
Theorem	pjpji 9533	Decomposition of a vector into projections.
|- H e. CH   &   |- A e. H~   =>   |- A = (((proj` H)` A) +h ((proj` (_|_` H))` A))
Theorem	pjpjth 9534	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	pjpjthi 9535	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	pjop 9536	Orthocomplement projection in terms of projection.
|- ((H e. CH /\ A e. H~) -> ((proj` (_|_` H))` A) = (A -h ((proj` H)` A)))
Theorem	pjpo 9537	Projection in terms of orthocomplement projection.
|- ((H e. CH /\ A e. H~) -> ((proj` H)` A) = (A -h ((proj` (_|_` H))` A)))
Theorem	pjopi 9538	Orthocomplement projection in terms of projection.
|- H e. CH   &   |- A e. H~   =>   |- ((proj` (_|_` H))` A) = (A -h ((proj` H)` A))
Theorem	pjpoi 9539	Projection in terms of orthocomplement projection.
|- H e. CH   &   |- A e. H~   =>   |- ((proj` H)` A) = (A -h ((proj` (_|_` H))` A))
Theorem	pjoc1i 9540	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	pjchi 9541	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	pjoccl 9542	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	pjoc1 9543	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	pjomli 9544	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 omlsi 9522.
|- A e. CH   &   |- B e. SH   =>   |- ((A (_ B /\ (B i^i (_|_` A)) = 0H) -> A = B)
Theorem	pjoml 9545	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 omlsi 9522.
|- (((A e. CH /\ B e. SH) /\ (A (_ B /\ (B i^i (_|_` A)) = 0H)) -> A = B)
Theorem	pjococi 9546	Proof of orthocomplement theorem using projections. Compare ococ 9524.
|- H e. CH   =>   |- (_|_` (_|_` H)) = H
Theorem	pjoc2i 9547	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	pjoc2 9548	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 9549	Define subspace sum in SH. See shsumval 9553, shsumval2i 9636, and shsumval3i 9637 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 9550	Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanval 9575 for its value.
|- span = {<.x, y>. | (x (_ H~ /\ y = |^|{z e. SH | x (_ z})}
Definition	df-chj 9551	Define Hilbert lattice join. See chjval 9598 for its value and chjcl 9605 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 sshjcl 9603. For an alternate definition see dfchj2 9600.
|- vH = {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))}
Definition	df-chsup 9552	Define the supremum of a set of Hilbert lattice elements. See chsupval2 9578 for its value and dfchsup2 9574 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 hsupcl 9583.
|- \/H = {<.x, y>. | (x (_ P~H~ /\ y = (_|_` (_|_` U.x)))}
Theorem	shsumval 9553	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	shsel 9554	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	shsel3 9555	Membership in the subspace sum of two Hilbert subspaces, using vector subtraction.
|- ((A e. SH /\ B e. SH) -> (C e. (A +H B) <-> E.x e. A E.y e. B C = (x -h y)))
Theorem	shseli 9556	Membership in subspace sum.
|- A e. SH   &   |- B e. SH   =>   |- (C e. (A +H B) <-> E.x e. A E.y e. B C = (x +h y))
Theorem	shscli 9557	Closure of subspace sum.
|- A e. SH   &   |- B e. SH   =>   |- (A +H B) e. SH
Theorem	shscl 9558	Closure of subspace sum.
|- ((A e. SH /\ B e. SH) -> (A +H B) e. SH)
Theorem	shscom 9559	Commutative law for subspace sum.
|- ((A e. SH /\ B e. SH) -> (A +H B) = (B +H A))
Theorem	shsva 9560	Vector sum belongs to subspace sum.
|- ((A e. SH /\ B e. SH) -> ((C e. A /\ D e. B) -> (C +h D) e. (A +H B)))
Theorem	shsel1 9561	A subspace sum contains a member of one of its subspaces.
|- ((A e. SH /\ B e. SH) -> (C e. A -> C e. (A +H B)))
Theorem	shsel2 9562	A subspace sum contains a member of one of its subspaces.
|- ((A e. SH /\ B e. SH) -> (C e. B -> C e. (A +H B)))
Theorem	shsvs 9563	Vector subtraction belongs to subspace sum.
|- ((A e. SH /\ B e. SH) -> ((C e. A /\ D e. B) -> (C -h D) e. (A +H B)))
Theorem	shsub1 9564	Subspace sum is an upper bound of its arguments.
|- ((A e. SH /\ B e. SH) -> A (_ (A +H B))
Theorem	shsub2 9565	Subspace sum is an upper bound of its arguments.
|- ((A e. SH /\ B e. SH) -> A (_ (B +H A))
Theorem	choc0 9566	The orthocomplement of the zero subspace is the unit subspace.
|- (_|_` 0H) = H~
Theorem	choc1 9567	The orthocomplement of the unit subspace is the zero subspace. Does not require Axiom of Choice.
|- (_|_` H~) = 0H
Theorem	chocnul 9568	Orthogonal complement of the empty set.
|- (_|_` (/)) = H~
Theorem	shintcli 9569	Closure of intersection of a non-empty subset of SH.
|- (A (_ SH /\ A =/= (/))   =>   |- |^|A e. SH
Theorem	shintcl 9570	The intersection of a non-empty set of subspaces is a subspace.
|- ((A (_ SH /\ A =/= (/)) -> |^|A e. SH)
Theorem	chintcli 9571	The intersection of a non-empty set of closed subspaces is a closed subspace.
|- (A (_ CH /\ A =/= (/))   =>   |- |^|A e. CH
Theorem	chintcl 9572	The intersection (infimum) of a non-empty subset of CH belongs to CH. Part of Theorem 3.13 of [Beran] p. 108. Also part of Definition 3.4-1 in [MegillPavicic] p. 2345 (PDF p. 8).
|- ((A (_ CH /\ A =/= (/)) -> |^|A e. CH)
Theorem	ococin 9573	The double complement is the smallest closed subspace containing a subset of Hilbert space. Remark 3.12(B) of [Beran] p. 107.
|- (A (_ H~ -> (_|_` (_|_` A)) = |^|{x e. CH | A (_ x})
Theorem	dfchsup2 9574	Alternate definition of supremum of a subset of the Hilbert lattice. Definition in Proposition 1 of [Kalmbach] p. 65. We actually define it on any collection of Hilbert space subsets, not just the Hilbert lattice CH, to allow more general theorems.
|- \/H = {<.x, y>. | (x (_ P~H~ /\ y = |^|{z e. CH | U.x (_ z})}
Theorem	spanval 9575	Value of the linear span of a subset of Hilbert space. The span is the intersection of all subspaces constraining the subset. Definition of span in [Schechter] p. 276.
|- (A (_ H~ -> (span` A) = |^|{x e. SH | A (_ x})
Theorem	hsupval2 9576	Value of supremum of set of subsets of Hilbert space. Definition of supremum in Proposition 1 of [Kalmbach] p. 65.
|- (A (_ P~H~ -> ( \/H ` A) = |^|{x e. CH | U.A (_ x})
Theorem	hsupval 9577	Value of supremum of set of subsets of Hilbert space. For an alternate version of the value, see hsupval2 9576.
|- (A (_ P~H~ -> ( \/H ` A) = (_|_` (_|_` U.A)))
Theorem	chsupval2 9578	The value of the supremum of a set of closed subspaces of Hilbert space. Definition of supremum in Proposition 1 of [Kalmbach] p. 65.
|- (A (_ CH -> ( \/H ` A) = |^|{x e. CH | U.A (_ x})
Theorem	chsupval 9579	The value of the supremum of a set of closed subspaces of Hilbert space. For an alternate version of the value, see chsupval2 9578.
|- (A (_ CH -> ( \/H ` A) = (_|_` (_|_` U.A)))
Theorem	spancl 9580	The span of a subset of Hilbert space is a subspace.
|- (A (_ H~ -> (span` A) e. SH)
Theorem	elspancl 9581	A member of a span is a vector.
|- ((A (_ H~ /\ B e. (span` A)) -> B e. H~)
Theorem	shsupcl 9582	Closure of the subspace supremum of set of subsets of Hilbert space.
|- (A (_ P~H~ -> (span` U.A) e. SH)
Theorem	hsupcl 9583	Closure of supremum of set of subsets of Hilbert space. Note that the supremum belongs to CH even if the subsets do not.
|- (A (_ P~H~ -> ( \/H ` A) e. CH)
Theorem	chsupcl 9584	Closure of supremum of subset of CH. Definition of supremum in Proposition 1 of [Kalmbach] p. 65. Shows that CH is a complete lattice. Also part of Definition 3.4-1 in [MegillPavicic] p. 2345 (PDF p. 8).
|- (A (_ CH -> ( \/H ` A) e. CH)
Theorem	hsupss 9585	Subset relation for supremum of Hilbert space subsets.
|- ((A (_ P~H~ /\ B (_ P~H~) -> (A (_ B -> ( \/H ` A) (_ ( \/H ` B)))
Theorem	chsupss 9586	Subset relation for supremum of subset of CH.
|- ((A (_ CH /\ B (_ CH) -> (A (_ B -> ( \/H ` A) (_ ( \/H ` B)))
Theorem	chsupid 9587	A subspace is the supremum of all smaller subspaces.
|- (A e. CH -> ( \/H ` {x e. CH | x (_ A}) = A)
Theorem	chsupsn 9588	Value of supremum of subset of CH on a singleton.
|- (A e. CH -> ( \/H ` {A}) = A)
Theorem	hsupunss 9589	The union of a set of Hilbert space subsets is smaller than its supremum.
|- (A (_ P~H~ -> U.A (_ ( \/H ` A))
Theorem	spanss2 9590	A subset of Hilbert space is included in its span.
|- (A (_ H~ -> A (_ (span` A))
Theorem	shsupunss 9591	The union of a set of subspaces is smaller than its supremum.
|- (A (_ SH -> U.A (_ (span` U.A))
Theorem	chsupunss 9592	The union of a set of closed subspaces is smaller than its supremum.
|- (A (_ CH -> U.A (_ ( \/H ` A))
Theorem	spanid 9593	A subspace of Hilbert space is its own span.
|- (A e. SH -> (span` A) = A)
Theorem	spanss 9594	Ordering relationship for the spans of subsets of Hilbert space.
|- ((B (_ H~ /\ A (_ B) -> (span` A) (_ (span` B))
Theorem	spanssoc 9595	The span of a subset of Hilbert space is less than or equal to its closure (double orthogonal complement).
|- (A (_ H~ -> (span` A) (_ (_|_` (_|_` A)))
Theorem	sshjval 9596	Value of join for subsets of Hilbert space.
|- ((A (_ H~ /\ B (_ H~) -> (A vH B) = (_|_` (_|_` (A u. B))))
Theorem	shjval 9597	Value of join in SH.
|- ((A e. SH /\ B e. SH) -> (A vH B) = (_|_` (_|_` (A u. B))))
Theorem	chjval 9598	Value of join in CH.
|- ((A e. CH /\ B e. CH) -> (A vH B) = (_|_` (_|_` (A u. B))))
Theorem	chjvali 9599	Value of join in CH.
|- A e. CH   &   |- B e. CH   =>   |- (A vH B) = (_|_` (_|_` (A u. B)))
Theorem	dfchj2 9600	Alternate definition of join in the set of closed subspaces of Hilbert space CH.
|- vH = {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = |^|{w e. CH | (x u. y) (_ w})}