mmtheorems97 - Metamath Proof Explorer

Home	Metamath Proof Explorer	< Previous Next >
		Browser slow? Try the Unicode version.

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

Color key:

Metamath Proof Explorer
(1-9062)

Hilbert Space Explorer
(9063-10650)

Users' Mathboxes
(10651-12229)

**Statement List for Metamath Proof Explorer -** 9601-9700 - Page 97 of 123
Type	Label	Description
Statement

Theorem	dfchj3 9601	Alternate definition of join in the set of closed subspaces of Hilbert space : the join is the supremum of its two arguments. Based on the definition of join in [Beran] p. 3. For later convenience we prove a general version that works for any subset of Hilbert space, not just the elements of the lattice .
$/\$ $/\$ $\/H$

Theorem	sshjval3 9602	Value of join for subsets of Hilbert space in terms of supremum: the join is the supremum of its two arguments. Based on the definition of join in [Beran] p. 3.
$/\$ $\/H$

Theorem	sshjcl 9603	Closure of join for subsets of Hilbert space.
$/\$

Theorem	shjcl 9604	Closure of join in .
$/\$

Theorem	chjcl 9605	Closure of join in .
$/\$

Theorem	shjcom 9606	Commutative law for Hilbert lattice join of subspaces.
$/\$

Theorem	shincli 9607	Closure of intersection of two subspaces.


Theorem	shscomi 9608	Commutative law for subspace sum.


Theorem	shsvai 9609	Vector sum belongs to subspace sum.
$/\$

Theorem	shsel1i 9610	A subspace sum contains a member of one of its subspaces.


Theorem	shsel2i 9611	A subspace sum contains a member of one of its subspaces.


Theorem	shsvsi 9612	Vector subtraction belongs to subspace sum.
$/\$

Theorem	shunssi 9613	Union is smaller than subspace sum.


Theorem	shsleji 9614	Subspace sum is smaller than Hilbert lattice join. Remark in [Kalmbach] p. 65.


Theorem	shunssji 9615	Union is smaller than Hilbert lattice join.


Theorem	shjcomi 9616	Commutative law for join in .


Theorem	shsub1i 9617	Subspace sum is an upper bound of its arguments.


Theorem	shsub2i 9618	Subspace sum is an upper bound of its arguments.


Theorem	shub1i 9619	Hilbert lattice join is an upper bound of two subspaces.


Theorem	shjcli 9620	Closure of join.


Theorem	shjshcli 9621	closure of join.


Theorem	shlubi 9622	Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces.
$/\$

Theorem	shlessi 9623	Subset implies subset of subspace sum.


Theorem	shlej1i 9624	Add disjunct to both sides of Hilbert subspace ordering.


Theorem	shlej2i 9625	Add disjunct to both sides of Hilbert subspace ordering.


Theorem	shslej 9626	Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65.
$/\$

Theorem	shincl 9627	Closure of intersection of two subspaces.
$/\$

Theorem	shub1 9628	Hilbert lattice join is an upper bound of two subspaces.
$/\$

Theorem	shub2 9629	A subspace is a subset of its Hilbert lattice join with another.
$/\$

Theorem	shlub 9630	Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces.
$/\$ $/\$ $/\$

Theorem	shlej1 9631	Add disjunct to both sides of Hilbert subspace ordering.
$/\$ $/\$ $/\$

Theorem	shlej2 9632	Add disjunct to both sides of Hilbert subspace ordering.
$/\$ $/\$ $/\$

Theorem	shsidmi 9633	Idempotent law for Hilbert subspace sum.


Theorem	shslubi 9634	Least upper bound law for Hilbert subspace sum.
$/\$

Theorem	shlesb1i 9635	Hilbert lattice ordering in terms of subspace sum.


Theorem	shsumval2i 9636	An alternate way to express subspace sum.


Theorem	shsumval3i 9637	An alternate way to express subspace sum.


Theorem	shmodsi 9638	The modular law holds for subspace sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70.


Theorem	shmodi 9639	The modular law is implied by the closure of subspace sum. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70.
$/\$

Hilbert lattice operations

Theorem	sh0le 9640	The zero subspace is the smallest subspace.


Theorem	ch0le 9641	The zero subspace is the smallest member of .


Theorem	shle0 9642	No subspace is smaller than the zero subspace.


Theorem	chle0 9643	No Hilbert lattice element is smaller than zero.


Theorem	chnlen0 9644	A Hilbert lattice element that is not a subset of another is nonzero.


Theorem	ch0pss 9645	The zero subspace is a proper subset of non-zero Hilbert lattice elements.


Theorem	orthin 9646	The intersection of orthogonal subspaces is the zero subspace.
$/\$

Theorem	shne0i 9647	A non-zero subspace has a non-zero vector.


Theorem	shs0i 9648	Hilbert subspace sum with the zero subspace.


Theorem	shs00i 9649	Two subspaces are zero iff their join is zero.
$/\$

Theorem	ch0lei 9650	The closed subspace zero is the smallest member of .


Theorem	chle0i 9651	No Hilbert closed subspace is smaller than zero.


Theorem	chne0i 9652	A non-zero closed subspace has a non-zero vector.


Theorem	chocini 9653	Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of [Kalmbach] p. 65.


Theorem	chj0i 9654	Join with lattice zero in .


Theorem	chm1i 9655	Meet with lattice one in .


Theorem	chjcli 9656	Closure of join.


Theorem	chsleji 9657	Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65.


Theorem	chseli 9658	Membership in subspace sum.


Theorem	chincli 9659	Closure of Hilbert lattice intersection.


Theorem	chsscon3i 9660	Hilbert lattice contraposition law.


Theorem	chsscon1i 9661	Hilbert lattice contraposition law.


Theorem	chsscon2i 9662	Hilbert lattice contraposition law.


Theorem	chcon2i 9663	Hilbert lattice contraposition law.


Theorem	chcon1i 9664	Hilbert lattice contraposition law.


Theorem	chcon3i 9665	Hilbert lattice contraposition law.


Theorem	chunssji 9666	Union is smaller than join.


Theorem	chjcomi 9667	Commutative law for join in .


Theorem	chub1i 9668	join is an upper bound of two elements.


Theorem	chub2i 9669	join is an upper bound of two elements.


Theorem	chlubi 9670	Hilbert lattice join is the least upper bound of two elements.
$/\$

Theorem	chlubii 9671	Hilbert lattice join is the least upper bound of two elements (one direction of chlubi 9670).
$/\$

Theorem	chlej1i 9672	Add join to both sides of a Hilbert lattice ordering.


Theorem	chlej2i 9673	Add join to both sides of a Hilbert lattice ordering.


Theorem	chlej12i 9674	Add join to both sides of a Hilbert lattice ordering.
$/\$

Theorem	chlejb1i 9675	Hilbert lattice ordering in terms of join.


Theorem	chdmm1i 9676	DeMorgan's law for meet in a Hilbert lattice.


Theorem	chdmm2i 9677	DeMorgan's law for meet in a Hilbert lattice.


Theorem	chdmm3i 9678	DeMorgan's law for meet in a Hilbert lattice.


Theorem	chdmm4i 9679	DeMorgan's law for meet in a Hilbert lattice.


Theorem	chdmj1i 9680	DeMorgan's law for join in a Hilbert lattice.


Theorem	chdmj2i 9681	DeMorgan's law for join in a Hilbert lattice.


Theorem	chdmj3i 9682	DeMorgan's law for join in a Hilbert lattice.


Theorem	chdmj4i 9683	DeMorgan's law for join in a Hilbert lattice.


Theorem	chnlei 9684	Equivalent expressions for "not less than" in the Hilbert lattice.


Theorem	chjassi 9685	Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14.


Theorem	chj00i 9686	Two Hilbert lattice elements are zero iff their join is zero.
$/\$

Theorem	chjoi 9687	The join of a closed subspace and its orthocomplement.


Theorem	chj1i 9688	Join with Hilbert lattice unit.


Theorem	chm0i 9689	Meet with Hilbert lattice zero.


Theorem	chm0 9690	Meet with Hilbert lattice zero.


Theorem	shjshsi 9691	Hilbert lattice join equals the double orthocomplement of subspace sum.


Theorem	shjshseli 9692	A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of [MaedaMaeda] p. 136.


Theorem	chne0 9693	A non-zero closed subspace has a nonzero vector.


Theorem	chocin 9694	Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of [Kalmbach] p. 65.


Theorem	chssoc 9695	A closed subspace less than its orthocomplement is zero.


Theorem	chj0 9696	Join with Hilbert lattice zero.


Theorem	chslej 9697	Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65.
$/\$

Theorem	chincl 9698	Closure of Hilbert lattice intersection.
$/\$

Theorem	chsscon3 9699	Hilbert lattice contraposition law.
$/\$

Theorem	chsscon1 9700	Hilbert lattice contraposition law.
$/\$

MPE Home Contents

< Previous Next >