Metamath Proof Explorer

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

Jump to page: 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-5787

Color key:

Metamath Proof Explorer (1-4957)

Hilbert Space Explorer (4958-5787)

**Statement List for Metamath Proof Explorer -** 5701-5787 - Page 58 of 58
Type	Label	Description
Statement

Theorem	jplem1 5701	Lemma for Jauch-Piron theorem.
$/\$

Theorem	jplem2 5702	Lemma for Jauch-Piron theorem.
$/\$ $/\$

Theorem	jp 5703	The function , that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a Jauch-Piron state. Remark of [Mayet] p. 370. (See strlem3a 5693 for the proof that is a state.)
$/\$ $/\$ $/\$

Theorem	golem1 5704	Lemma for Godowski's equation.


Theorem	golem2 5705	Lemma for Godowski's equation.


Theorem	goeq 5706	Godowski's equation, shown here as a variant equivalent to Equation (SF) of [Godowski] p. 730.


Theorem	stcltr1 5707	Property of a strong classical state.
$/\$

Theorem	stcltr2 5708	Property of a strong classical state.
$/\$

Theorem	stcltrlem1 5709	Lemma for strong classical state theorem.
$/\$

Theorem	stcltrlem2 5710	Lemma for strong classical state theorem.
$/\$

Theorem	stcltrth 5711	Strong classical state theorem. If there exists a "strong classical" state on lattice , then any two elements of the lattice commute, i.e., the lattice is distributive. (Proof due to Mladen Pavicic.) Theorem 3.3 of [MegillPavicic] p. 2344.


Definition	df-cv 5712	Define the covers relation (on the Hilbert lattice). Definition 3.2.18 of [PtakPulmannova] p. 68, whose notation we use. Ptak/Pulmannova's notation is read " covers " or " is covered by " , and it means that is larger than and there is nothing in between. See cvbrt 5714 and cvbr2t 5715 for membership relations.
$/\$ $/\$ $/\$ $/\$

Definition	df-md 5713	Define the modular pair relation (on the Hilbert lattice). Definition 1.1 of [MaedaMaeda] p. 1, who use the notation (x,y)M for "the ordered pair <x,y> is a modular pair." See mdbr 5726 for membership relation.
$/\$ $/\$

Theorem	cvbrt 5714	Binary relation expressing covers , which means that is larger than and there is nothing in between. Definition 3.2.18 of [PtakPulmannova] p. 68.
$/\$ $/\$ $/\$

Theorem	cvbr2t 5715	Binary relation expressing covers . Definition of covers in [Kalmbach] p. 15.
$/\$ $/\$ $/\$

Theorem	cvcon3t 5716	Contraposition law for the covers relation.
$/\$

Theorem	cvpsst 5717	The covering relation implies proper subset.
$/\$

Theorem	cvnbtwnt 5718	The covering relation implies no in-betweenness.
$/\$ $/\$ $/\$

Theorem	cvnbtwn2t 5719	The covering relation implies no in-betweenness.
$/\$ $/\$ $/\$

Theorem	cvnbtwn3t 5720	The covering relation implies no in-betweenness.
$/\$ $/\$ $/\$

Theorem	cvnbtwn4t 5721	The covering relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31.
$/\$ $/\$ $/\$ $\/$

Theorem	cvnsymt 5722	The covering relation is not symmetric.
$/\$

Theorem	cvnreft 5723	The covering relation is not reflexive.


Theorem	cvntrt 5724	The covering relation is not transitive.
$/\$ $/\$ $/\$

Theorem	spansncv2t 5725	Hilbert space has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153.
$/\$

Theorem	mdbr 5726	Binary relation expressing is a modular pair. Definition 1.1 of [MaedaMaeda] p. 1.
$/\$

Theorem	mdi 5727	Consequence of the modular pair property.
$/\$ $/\$

Theorem	mdbr2 5728	Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 5726.
$/\$

Theorem	mdbr3 5729	Binary relation expressing the modular pair property. This version quantifies an equality instead of an inference.
$/\$

Theorem	mdbr4 5730	Binary relation expressing the modular pair property. This version quantifies an ordering instead of an inference.
$/\$

Theorem	dmdbr 5731	Binary relation expressing the dual modular pair property. Remark 29.6 of [MaedaMaeda] p. 130. We will use the idiom to mean and are a dual modular pair, since the equivalence happens to hold in Hilbert lattices, as this theorem shows.
$/\$