Metamath Proof Explorer - mmtheorems58

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

Statement List for Metamath Proof Explorer - 5701-5787 - Page 58 of 58

Type	Label	Description
Statement
Theorem	jplem1 5701	Lemma for Jauch-Piron theorem.
⊢ A ∈ Cℋ    ⇒   ⊢ ((u ∈ ℋ ∧ (norm ‘u) = 1) → (u ∈ A ↔ ((norm ‘((Proj ‘A) ‘u))↑2) = 1))
Theorem	jplem2 5702	Lemma for Jauch-Piron theorem.
⊢ S = {⟨x, y⟩∣(x ∈ Cℋ ∧ y = ((norm ‘((Proj ‘x) ‘u))↑2))}    &   ⊢ A ∈ Cℋ    ⇒   ⊢ ((u ∈ ℋ ∧ (norm ‘u) = 1) → (u ∈ A ↔ (S ‘A) = 1))
Theorem	jp 5703	The function S, 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 S is a state.)
⊢ S = {⟨x, y⟩∣(x ∈ Cℋ ∧ y = ((norm ‘((Proj ‘x) ‘u))↑2))}    &   ⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ ((u ∈ ℋ ∧ (norm ‘u) = 1) → (((S ‘A) = 1 ∧ (S ‘B) = 1) ↔ (S ‘(A ∩ B)) = 1))
Theorem	golem1 5704	Lemma for Godowski's equation.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    &   ⊢ F = ((⊥ ‘A) ∨ℋ (A ∩ B))    &   ⊢ G = ((⊥ ‘B) ∨ℋ (B ∩ C))    &   ⊢ H = ((⊥ ‘C) ∨ℋ (C ∩ A))    &   ⊢ D = ((⊥ ‘B) ∨ℋ (B ∩ A))    &   ⊢ R = ((⊥ ‘C) ∨ℋ (C ∩ B))    &   ⊢ S = ((⊥ ‘A) ∨ℋ (A ∩ C))    ⇒   ⊢ (f ∈ States → (((f ‘F) + (f ‘G)) + (f ‘H)) = (((f ‘D) + (f ‘R)) + (f ‘S)))
Theorem	golem2 5705	Lemma for Godowski's equation.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    &   ⊢ F = ((⊥ ‘A) ∨ℋ (A ∩ B))    &   ⊢ G = ((⊥ ‘B) ∨ℋ (B ∩ C))    &   ⊢ H = ((⊥ ‘C) ∨ℋ (C ∩ A))    &   ⊢ D = ((⊥ ‘B) ∨ℋ (B ∩ A))    &   ⊢ R = ((⊥ ‘C) ∨ℋ (C ∩ B))    &   ⊢ S = ((⊥ ‘A) ∨ℋ (A ∩ C))    ⇒   ⊢ (f ∈ States → ((f ‘((F ∩ G) ∩ H)) = 1 → (f ‘D) = 1))
Theorem	goeq 5706	Godowski's equation, shown here as a variant equivalent to Equation (SF) of [Godowski] p. 730.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    &   ⊢ F = ((⊥ ‘A) ∨ℋ (A ∩ B))    &   ⊢ G = ((⊥ ‘B) ∨ℋ (B ∩ C))    &   ⊢ H = ((⊥ ‘C) ∨ℋ (C ∩ A))    &   ⊢ D = ((⊥ ‘B) ∨ℋ (B ∩ A))    ⇒   ⊢ ((F ∩ G) ∩ H) ⊆ D
Theorem	stcltr1 5707	Property of a strong classical state.
⊢ (φ ↔ (S ∈ States ∧ ∀x ∈ Cℋ ∀y ∈ Cℋ (((S ‘x) = 1 → (S ‘y) = 1) → x ⊆ y)))    &   ⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (φ → (((S ‘A) = 1 → (S ‘B) = 1) → A ⊆ B))
Theorem	stcltr2 5708	Property of a strong classical state.
⊢ (φ ↔ (S ∈ States ∧ ∀x ∈ Cℋ ∀y ∈ Cℋ (((S ‘x) = 1 → (S ‘y) = 1) → x ⊆ y)))    &   ⊢ A ∈ Cℋ    ⇒   ⊢ (φ → ((S ‘A) = 1 → A = ℋ ))
Theorem	stcltrlem1 5709	Lemma for strong classical state theorem.
⊢ (φ ↔ (S ∈ States ∧ ∀x ∈ Cℋ ∀y ∈ Cℋ (((S ‘x) = 1 → (S ‘y) = 1) → x ⊆ y)))    &   ⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (φ → ((S ‘B) = 1 → (S ‘((⊥ ‘A) ∨ℋ (A ∩ B))) = 1))
Theorem	stcltrlem2 5710	Lemma for strong classical state theorem.
⊢ (φ ↔ (S ∈ States ∧ ∀x ∈ Cℋ ∀y ∈ Cℋ (((S ‘x) = 1 → (S ‘y) = 1) → x ⊆ y)))    &   ⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (φ → B ⊆ ((⊥ ‘A) ∨ℋ (A ∩ B)))
Theorem	stcltrth 5711	Strong classical state theorem. If there exists a "strong classical" state on lattice Cℋ, 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.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ ∃s ∈ States ∀x ∈ Cℋ ∀y ∈ Cℋ (((s ‘x) = 1 → (s ‘y) = 1) → x ⊆ y)    ⇒   ⊢ B ⊆ ((⊥ ‘A) ∨ℋ (A ∩ B))
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 A ⋖ B is read "B covers A" or "A is covered by B" , and it means that B is larger than A and there is nothing in between. See cvbrt 5714 and cvbr2t 5715 for membership relations.
⊢ ⋖ = {⟨x, y⟩∣((x ∈ Cℋ ∧ y ∈ Cℋ ) ∧ (x ⊂ y ∧ ¬ ∃z ∈ Cℋ (x ⊂ z ∧ z ⊂ y)))}
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.
⊢ Mℋ = {⟨x, y⟩∣((x ∈ Cℋ ∧ y ∈ Cℋ ) ∧ ∀z ∈ Cℋ (z ⊆ y → ((z ∨ℋ x) ∩ y) = (z ∨ℋ (x ∩ y))))}
Theorem	cvbrt 5714	Binary relation expressing B covers A, which means that B is larger than A and there is nothing in between. Definition 3.2.18 of [PtakPulmannova] p. 68.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⋖ B ↔ (A ⊂ B ∧ ¬ ∃x ∈ Cℋ (A ⊂ x ∧ x ⊂ B))))
Theorem	cvbr2t 5715	Binary relation expressing B covers A. Definition of covers in [Kalmbach] p. 15.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⋖ B ↔ (A ⊂ B ∧ ∀x ∈ Cℋ ((A ⊂ x ∧ x ⊆ B) → x = B))))
Theorem	cvcon3t 5716	Contraposition law for the covers relation.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⋖ B ↔ (⊥ ‘B) ⋖ (⊥ ‘A)))
Theorem	cvpsst 5717	The covering relation implies proper subset.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⋖ B → A ⊂ B))
Theorem	cvnbtwnt 5718	The covering relation implies no in-betweenness.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → (A ⋖ B → ¬ (A ⊂ C ∧ C ⊂ B)))
Theorem	cvnbtwn2t 5719	The covering relation implies no in-betweenness.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → (A ⋖ B → ((A ⊂ C ∧ C ⊆ B) → C = B)))
Theorem	cvnbtwn3t 5720	The covering relation implies no in-betweenness.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → (A ⋖ B → ((A ⊆ C ∧ C ⊂ B) → C = A)))
Theorem	cvnbtwn4t 5721	The covering relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → (A ⋖ B → ((A ⊆ C ∧ C ⊆ B) → (C = A ∨ C = B))))
Theorem	cvnsymt 5722	The covering relation is not symmetric.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⋖ B → ¬ B ⋖ A))
Theorem	cvnreft 5723	The covering relation is not reflexive.
⊢ (A ∈ Cℋ → ¬ A ⋖ A)
Theorem	cvntrt 5724	The covering relation is not transitive.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → ((A ⋖ B ∧ B ⋖ C) → ¬ A ⋖ C))
Theorem	spansncv2t 5725	Hilbert space has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153.
⊢ ((A ∈ Cℋ ∧ B ∈ ℋ ) → (¬ (span ‘{B}) ⊆ A → A ⋖ (A ∨ℋ (span ‘{B}))))
Theorem	mdbr 5726	Binary relation expressing ⟨A, B⟩ is a modular pair. Definition 1.1 of [MaedaMaeda] p. 1.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A Mℋ B ↔ ∀x ∈ Cℋ (x ⊆ B → ((x ∨ℋ A) ∩ B) = (x ∨ℋ (A ∩ B)))))
Theorem	mdi 5727	Consequence of the modular pair property.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → (A Mℋ B → (C ⊆ B → ((C ∨ℋ A) ∩ B) = (C ∨ℋ (A ∩ B)))))
Theorem	mdbr2 5728	Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 5726.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A Mℋ B ↔ ∀x ∈ Cℋ (x ⊆ B → ((x ∨ℋ A) ∩ B) ⊆ (x ∨ℋ (A ∩ B)))))
Theorem	mdbr3 5729	Binary relation expressing the modular pair property. This version quantifies an equality instead of an inference.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A Mℋ B ↔ ∀x ∈ Cℋ (((x ∩ B) ∨ℋ A) ∩ B) = ((x ∩ B) ∨ℋ (A ∩ B))))
Theorem	mdbr4 5730	Binary relation expressing the modular pair property. This version quantifies an ordering instead of an inference.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A Mℋ B ↔ ∀x ∈ Cℋ (((x ∩ B) ∨ℋ A) ∩ B) ⊆ ((x ∩ B) ∨ℋ (A ∩ B))))
Theorem	dmdbr 5731	Binary relation expressing the dual modular pair property. Remark 29.6 of [MaedaMaeda] p. 130. We will use the idiom (⊥ ‘A) Mℋ (⊥ ‘B) to mean A and B are a dual modular pair, since the equivalence happens to hold in Hilbert lattices, as this theorem shows.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → ((⊥ ‘A) Mℋ (⊥ ‘B) ↔ ∀x ∈ Cℋ (B ⊆ x → ((x ∩ A) ∨ℋ B) = (x ∩ (A ∨ℋ B)))))
Theorem	dmdi 5732	Consequence of the dual modular pair property.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → ((⊥ ‘A) Mℋ (⊥ ‘B) → (B ⊆ C → ((C ∩ A) ∨ℋ B) = (C ∩ (A ∨ℋ B)))))
Theorem	dmdbr2 5733	Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr 5731.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → ((⊥ ‘A) Mℋ (⊥ ‘B) ↔ ∀x ∈ Cℋ (B ⊆ x → (x ∩ (A ∨ℋ B)) ⊆ ((x ∩ A) ∨ℋ B))))
Theorem	ssmd1 5734	Ordering implies the modular pair property. Remark of [MaedaMaeda] p. 1.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⊆ B → A Mℋ B))
Theorem	ssmd2 5735	Ordering implies the modular pair property. Remark of [MaedaMaeda] p. 1.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⊆ B → B Mℋ A))
Theorem	ssdmd1 5736	Ordering implies the dual modular pair property. Remark of [MaedaMaeda] p. 1.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⊆ B → (⊥ ‘A) Mℋ (⊥ ‘B)))
Definition	df-at 5737	Define the set of atoms in a Hilbert lattice. An atom is a non-zero element of a lattice such that anything less than it is zero, i.e. it is a smallest non-zero element of the lattice. Definition of atom in [Kalmbach] p. 15. See elat 5738 and elat2 5739 for membership relations.
⊢ Atoms = {x ∈ Cℋ ∣0ℋ ⋖ x}
Theorem	elat 5738	Atoms in a Hilbert lattice are the elements that cover the zero subspace. Definition of atom in [Kalmbach] p. 15.
⊢ (A ∈ Atoms ↔ (A ∈ Cℋ ∧ 0ℋ ⋖ A))
Theorem	elat2 5739	Expanded membership relation for the set of atoms, i.e. the predicate "is an atom (of the Hilbert lattice)." An atom is a non-zero element of a lattice such that anything less than it is zero, i.e. it is a smallest non-zero element of the lattice.
⊢ (A ∈ Atoms ↔ (A ∈ Cℋ ∧ (¬ A = 0ℋ ∧ ∀x ∈ Cℋ (x ⊆ A → (x = A ∨ x = 0ℋ)))))
Theorem	atcv0 5740	An atom covers the zero subspace.
⊢ (A ∈ Atoms → 0ℋ ⋖ A)
Theorem	atssch 5741	Atoms are a subset of the Hilbert lattice.
⊢ Atoms ⊆ Cℋ
Theorem	atelch 5742	An atom is a Hilbert lattice element.
⊢ (A ∈ Atoms → A ∈ Cℋ )
Theorem	atn0 5743	An atom is not the Hilbert lattice zero.
⊢ (A ∈ Atoms → ¬ A = 0ℋ)
Theorem	atss 5744	A lattice element smaller than an atom is either the atom or zero.
⊢ ((A ∈ Cℋ ∧ B ∈ Atoms) → (A ⊆ B → (A = B ∨ A = 0ℋ)))
Theorem	atsseq 5745	Two atoms in a subset relationship are equal.
⊢ ((A ∈ Atoms ∧ B ∈ Atoms) → (A ⊆ B ↔ A = B))
Theorem	atcveq0 5746	A Hilbert lattice element covered by an atom must be the zero subspace.
⊢ ((A ∈ Cℋ ∧ B ∈ Atoms) → (A ⋖ B ↔ A = 0ℋ))
Theorem	h1dat 5747	A 1-dimensional subspace is an atom.
⊢ ((A ∈ ℋ ∧ ¬ A = 0v) → (⊥ ‘(⊥ ‘{A})) ∈ Atoms)
Theorem	sh1dle 5748	A 1-dimensional subspace is less than or equal to any subspace containing its generating vector.
⊢ ((A ∈ Sℋ ∧ B ∈ A) → (⊥ ‘(⊥ ‘{B})) ⊆ A)
Theorem	ch1dle 5749	A 1-dimensional subspace is less than or equal to any member of Cℋ containing its generating vector.
⊢ ((A ∈ Cℋ ∧ B ∈ A) → (⊥ ‘(⊥ ‘{B})) ⊆ A)
Theorem	atom1d 5750	The 1-dimensional subspaces of Hilbert space are its atoms. Part of Remark 10.3.5 of [BeltramettiCassinelli] p. 107.
⊢ (A ∈ Atoms ↔ ∃x ∈ ℋ (¬ x = 0v ∧ A = (span ‘{x})))
Theorem	chcv1t 5751	The Hilbert lattice has the covering property. Proposition 1(ii) of [Kalmbach] p. 140 (and its converse).
⊢ ((A ∈ Cℋ ∧ B ∈ Atoms) → (¬ B ⊆ A ↔ A ⋖ (A ∨ℋ B)))
Theorem	chcv2t 5752	The Hilbert lattice has the covering property.
⊢ ((A ∈ Cℋ ∧ B ∈ Atoms) → (A ⊂ (A ∨ℋ B) ↔ A ⋖ (A ∨ℋ B)))
Theorem	shatomic 5753	The lattice of Hilbert subspaces is atomic, i.e. any non-zero element is greater than or equal to some atom. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70.
⊢ A ∈ Sℋ    ⇒   ⊢ (¬ A = 0ℋ → ∃x ∈ Atoms x ⊆ A)
Theorem	hatomic 5754	The Hilbert lattice is atomic, i.e. any non-zero element is greater than or equal to some atom. Remark of [Kalmbach] p. 140.
⊢ A ∈ Cℋ    ⇒   ⊢ (¬ A = 0ℋ → ∃x ∈ Atoms x ⊆ A)
Theorem	hatomistic 5755	Cℋ is atomistic, i.e. any element is the supremum of its atoms. Remark of [Kalmbach] p. 140.
⊢ A ∈ Cℋ    ⇒   ⊢ A = ( ∨ℋ ‘{x ∈ Atoms∣x ⊆ A})
Theorem	chpssat 5756	Two Hilbert lattice elements in a proper subset relationship imply the existence of an atom less than or equal to one but not the other.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ⊂ B → ∃x ∈ Atoms (x ⊆ B ∧ ¬ x ⊆ A))
Theorem	chrelat 5757	The Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ⊂ B → ∃x ∈ Atoms (A ⊂ (A ∨ℋ x) ∧ (A ∨ℋ x) ⊆ B))
Theorem	chrelat2 5758	A consequence of relative atomicity.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (¬ A ⊆ B ↔ ∃x ∈ Atoms (x ⊆ A ∧ ¬ x ⊆ B))
Theorem	cvexchlem 5759	Lemma for cvexch 5760.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ ((A ∩ B) ⋖ B → A ⋖ (A ∨ℋ B))
Theorem	cvexch 5760	The Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ ((A ∩ B) ⋖ B ↔ A ⋖ (A ∨ℋ B))
Theorem	chrelat2t 5761	A consequence of relative atomicity.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (¬ A ⊆ B ↔ ∃x ∈ Atoms (x ⊆ A ∧ ¬ x ⊆ B)))
Theorem	chrelat3t 5762	A consequence of relative atomicity.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⊆ B ↔ ∀x ∈ Atoms (x ⊆ A → x ⊆ B)))
Theorem	cvexcht 5763	The Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → ((A ∩ B) ⋖ B ↔ A ⋖ (A ∨ℋ B)))
Theorem	cvp 5764	The Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse.
⊢ ((A ∈ Cℋ ∧ B ∈ Atoms) → ((A ∩ B) = 0ℋ ↔ A ⋖ (A ∨ℋ B)))
Theorem	atnssm0 5765	The meet of a Hilbert lattice element and an incomparable atom is the zero subspace.
⊢ ((A ∈ Cℋ ∧ B ∈ Atoms) → (¬ B ⊆ A ↔ (A ∩ B) = 0ℋ))
Theorem	atnem0 5766	The meet of distinct atoms is the zero subspace.
⊢ ((A ∈ Atoms ∧ B ∈ Atoms) → (¬ A = B ↔ (A ∩ B) = 0ℋ))
Theorem	atcv0eq 5767	Two atoms covering the zero subspace are equal.
⊢ ((A ∈ Atoms ∧ B ∈ Atoms) → (0ℋ ⋖ (A ∨ℋ B) ↔ A = B))
Theorem	atcv1 5768	Two atoms covering the zero subspace are equal.
⊢ (((A ∈ Cℋ ∧ B ∈ Atoms ∧ C ∈ Atoms) ∧ A ⋖ (B ∨ℋ C)) → (A = 0ℋ ↔ B = C))
Theorem	atexch 5769	The Hilbert lattice satisfies the atom exchange property. Proposition 1(i) of [Kalmbach] p. 140. A version of this theorem related to vector analysis was originally proved by Hermann Grassmann in 1862.
⊢ ((A ∈ Cℋ ∧ B ∈ Atoms ∧ C ∈ Atoms) → ((B ⊆ (A ∨ℋ C) ∧ (A ∩ B) = 0ℋ) → C ⊆ (A ∨ℋ B)))
Theorem	atcvatlem 5770	Lemma for atcvat 5771.
⊢ A ∈ Cℋ    ⇒   ⊢ (((B ∈ Atoms ∧ C ∈ Atoms) ∧ (¬ A = 0ℋ ∧ A ⊂ (B ∨ℋ C))) → (¬ B ⊆ A → A ∈ Atoms))
Theorem	atcvat 5771	A nonzero Hilbert lattice element less than the join of two atoms is an atom.
⊢ A ∈ Cℋ    ⇒   ⊢ ((B ∈ Atoms ∧ C ∈ Atoms) → ((¬ A = 0ℋ ∧ A ⊂ (B ∨ℋ C)) → A ∈ Atoms))
Theorem	atcvat2 5772	A Hilbert lattice element covered by the join of two distinct atoms is an atom.
⊢ A ∈ Cℋ    ⇒   ⊢ ((B ∈ Atoms ∧ C ∈ Atoms) → ((¬ B = C ∧ A ⋖ (B ∨ℋ C)) → A ∈ Atoms))
Theorem	atcvat2t 5773	A Hilbert lattice element covered by the join of two distinct atoms is an atom.
⊢ ((A ∈ Cℋ ∧ B ∈ Atoms ∧ C ∈ Atoms) → ((¬ B = C ∧ A ⋖ (B ∨ℋ C)) → A ∈ Atoms))
Theorem	atcvat3 5774	A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68.
⊢ A ∈ Cℋ    ⇒   ⊢ ((B ∈ Atoms ∧ C ∈ Atoms) → (((¬ B = C ∧ ¬ C ⊆ A) ∧ B ⊆ (A ∨ℋ C)) → (A ∩ (B ∨ℋ C)) ∈ Atoms))
Theorem	atcvat4 5775	A condition implying existence of an atom with the properties shown. Lemma 3.2.20 of [PtakPulmannova] p. 68.
⊢ A ∈ Cℋ    ⇒   ⊢ ((B ∈ Atoms ∧ C ∈ Atoms) → ((¬ A = 0ℋ ∧ B ⊆ (A ∨ℋ C)) → ∃x ∈ Atoms (x ⊆ A ∧ B ⊆ (C ∨ℋ x))))
Theorem	mdsymlem1 5776	Lemma for mdsym 5784.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C = (A ∨ℋ p)    ⇒   ⊢ (((p ∈ Cℋ ∧ (B ∩ C) ⊆ A) ∧ ((⊥ ‘B) Mℋ (⊥ ‘A) ∧ p ⊆ (A ∨ℋ B))) → p ⊆ A)
Theorem	mdsymlem2 5777	Lemma for mdsym 5784.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C = (A ∨ℋ p)    ⇒   ⊢ (((p ∈ Atoms ∧ (B ∩ C) ⊆ A) ∧ ((⊥ ‘B) Mℋ (⊥ ‘A) ∧ p ⊆ (A ∨ℋ B))) → (¬ B = 0ℋ → ∃r ∈ Atoms ∃q ∈ Atoms (p ⊆ (q ∨ℋ r) ∧ (q ⊆ A ∧ r ⊆ B))))
Theorem	mdsymlem3 5778	Lemma for mdsym 5784.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C = (A ∨ℋ p)    ⇒   ⊢ ((((p ∈ Atoms ∧ ¬ (B ∩ C) ⊆ A) ∧ p ⊆ (A ∨ℋ B)) ∧ ¬ A = 0ℋ) → ∃r ∈ Atoms ∃q ∈ Atoms (p ⊆ (q ∨ℋ r) ∧ (q ⊆ A ∧ r ⊆ B)))
Theorem	mdsymlem4 5779	Lemma for mdsym 5784. This is the forward direction of Lemma 4(i) of [Maeda] p. 168.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C = (A ∨ℋ p)    ⇒   ⊢ (p ∈ Atoms → (((⊥ ‘B) Mℋ (⊥ ‘A) ∧ ((¬ A = 0ℋ ∧ ¬ B = 0ℋ) ∧ p ⊆ (A ∨ℋ B))) → ∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (q ∨ℋ r) ∧ (q ⊆ A ∧ r ⊆ B))))
Theorem	mdsymlem5 5780	Lemma for mdsym 5784.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C = (A ∨ℋ p)    ⇒   ⊢ ((q ∈ Atoms ∧ r ∈ Atoms) → (¬ q = p → ((p ⊆ (q ∨ℋ r) ∧ (q ⊆ A ∧ r ⊆ B)) → (((c ∈ Cℋ ∧ A ⊆ c) ∧ p ∈ Atoms) → (p ⊆ c → p ⊆ ((c ∩ B) ∨ℋ A))))))
Theorem	mdsymlem6 5781	Lemma for mdsym 5784. This is the converse direction of Lemma 4(i) of [Maeda] p. 168, and is based on the proof of Theorem 1(d) to (e) of [Maeda] p. 167.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C = (A ∨ℋ p)    ⇒   ⊢ (∀p ∈ Atoms (p ⊆ (A ∨ℋ B) → ∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (q ∨ℋ r) ∧ (q ⊆ A ∧ r ⊆ B))) → (⊥ ‘B) Mℋ (⊥ ‘A))
Theorem	mdsymlem7 5782	Lemma for mdsym 5784. Lemma 4(i) of [Maeda] p. 168. Note that Maeda reverses the arguments in his definition of dual modular pair.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C = (A ∨ℋ p)    ⇒   ⊢ ((¬ A = 0ℋ ∧ ¬ B = 0ℋ) → ((⊥ ‘B) Mℋ (⊥ ‘A) ↔ ∀p ∈ Atoms (p ⊆ (A ∨ℋ B) → ∃q ∈ Atoms ∃r ∈ Atoms (p ⊆ (q ∨ℋ r) ∧ (q ⊆ A ∧ r ⊆ B)))))
Theorem	mdsymlem8 5783	Lemma for mdsym 5784. Lemma 4(ii) of [Maeda] p. 168.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C = (A ∨ℋ p)    ⇒   ⊢ ((¬ A = 0ℋ ∧ ¬ B = 0ℋ) → ((⊥ ‘B) Mℋ (⊥ ‘A) ↔ (⊥ ‘A) Mℋ (⊥ ‘B)))
Theorem	mdsym 5784	M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A Mℋ B ↔ B Mℋ A)
Theorem	sumdmdi 5785	If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark of [MaedaMaeda] p. 139.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ ((A +ℋ B) = (A ∨ℋ B) → (⊥ ‘A) Mℋ (⊥ ‘B))
Theorem	sumdmdlem 5786	Lemma for sumdmd 5787. The span of vector C not in the subspace sum is "trimmed off."
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ ((C ∈ ℋ ∧ ¬ C ∈ (A +ℋ B)) → ((B +ℋ (span ‘{C})) ∩ A) = (B ∩ A))
Theorem	sumdmd 5787	The subspace sum of two Hilbert lattice elements is closed iff the elements are a dual modular pair. Theorem 2 of [Holland] p. 1519.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ ((A +ℋ B) = (A ∨ℋ B) ↔ (⊥ ‘A) Mℋ (⊥ ‘B))

metamath.org

< Previous  Wrap >