P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	stlei 32501	Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → (𝑆‘𝐴) ≤ (𝑆‘𝐵)))
Theorem	stlesi 32502	Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → ((𝑆‘𝐴) = 1 → (𝑆‘𝐵) = 1)))
Theorem	stji1i 32503	Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝑆‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) = ((𝑆‘(⊥‘𝐴)) + (𝑆‘(𝐴 ∩ 𝐵))))
Theorem	stm1i 32504	State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐴) = 1))
Theorem	stm1ri 32505	State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐵) = 1))
Theorem	stm1addi 32506	Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → ((𝑆‘𝐴) + (𝑆‘𝐵)) = 2))
Theorem	staddi 32507	If the sum of 2 states is 2, then each state is 1. (Contributed by NM, 12-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (((𝑆‘𝐴) + (𝑆‘𝐵)) = 2 → (𝑆‘𝐴) = 1))
Theorem	stm1add3i 32508	Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘((𝐴 ∩ 𝐵) ∩ 𝐶)) = 1 → (((𝑆‘𝐴) + (𝑆‘𝐵)) + (𝑆‘𝐶)) = 3))
Theorem	stadd3i 32509	If the sum of 3 states is 3, then each state is 1. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((((𝑆‘𝐴) + (𝑆‘𝐵)) + (𝑆‘𝐶)) = 3 → (𝑆‘𝐴) = 1))
Theorem	st0 32510	The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝑆‘0ℋ) = 0)
Theorem	strlem1 32511*	Lemma for strong state theorem: if closed subspace 𝐴 is not contained in 𝐵, there is a unit vector 𝑢 in their difference. (Contributed by NM, 25-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (¬ 𝐴 ⊆ 𝐵 → ∃𝑢 ∈ (𝐴 ∖ 𝐵)(normℎ‘𝑢) = 1)
Theorem	strlem2 32512*	Lemma for strong state theorem. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    ⇒   ⊢ (𝐶 ∈ Cℋ → (𝑆‘𝐶) = ((normℎ‘((projℎ‘𝐶)‘𝑢))↑2))
Theorem	strlem3a 32513*	Lemma for strong state theorem: the function 𝑆, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    ⇒   ⊢ ((𝑢 ∈ ℋ ∧ (normℎ‘𝑢) = 1) → 𝑆 ∈ States)
Theorem	strlem3 32514*	Lemma for strong state theorem: the function 𝑆, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. This lemma restates the hypotheses in a more convenient form to work with. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → 𝑆 ∈ States)
Theorem	strlem4 32515*	Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → (𝑆‘𝐴) = 1)
Theorem	strlem5 32516*	Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → (𝑆‘𝐵) < 1)
Theorem	strlem6 32517*	Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → ¬ ((𝑆‘𝐴) = 1 → (𝑆‘𝐵) = 1))
Theorem	stri 32518*	Strong state theorem. The states on a Hilbert lattice define an ordering. Remark in [Mayet] p. 370. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑓 ∈ States ((𝑓‘𝐴) = 1 → (𝑓‘𝐵) = 1) → 𝐴 ⊆ 𝐵)
Theorem	strb 32519*	Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑓 ∈ States ((𝑓‘𝐴) = 1 → (𝑓‘𝐵) = 1) ↔ 𝐴 ⊆ 𝐵)
Theorem	hstrlem2 32520*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    ⇒   ⊢ (𝐶 ∈ Cℋ → (𝑆‘𝐶) = ((projℎ‘𝐶)‘𝑢))
Theorem	hstrlem3a 32521*	Lemma for strong set of CH states theorem: the function 𝑆, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    ⇒   ⊢ ((𝑢 ∈ ℋ ∧ (normℎ‘𝑢) = 1) → 𝑆 ∈ CHStates)
Theorem	hstrlem3 32522*	Lemma for strong set of CH states theorem: the function 𝑆, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. This lemma restates the hypotheses in a more convenient form to work with. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → 𝑆 ∈ CHStates)
Theorem	hstrlem4 32523*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → (normℎ‘(𝑆‘𝐴)) = 1)
Theorem	hstrlem5 32524*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → (normℎ‘(𝑆‘𝐵)) < 1)
Theorem	hstrlem6 32525*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    &   ⊢ (𝜑 ↔ (𝑢 ∈ (𝐴 ∖ 𝐵) ∧ (normℎ‘𝑢) = 1))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → ¬ ((normℎ‘(𝑆‘𝐴)) = 1 → (normℎ‘(𝑆‘𝐵)) = 1))
Theorem	hstri 32526*	Hilbert space admits a strong set of Hilbert-space-valued states (CH-states). Theorem in [Mayet3] p. 10. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑓 ∈ CHStates ((normℎ‘(𝑓‘𝐴)) = 1 → (normℎ‘(𝑓‘𝐵)) = 1) → 𝐴 ⊆ 𝐵)
Theorem	hstrbi 32527*	Strong CH-state theorem (bidirectional version). Theorem in [Mayet3] p. 10 and its converse. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑓 ∈ CHStates ((normℎ‘(𝑓‘𝐴)) = 1 → (normℎ‘(𝑓‘𝐵)) = 1) ↔ 𝐴 ⊆ 𝐵)
Theorem	largei 32528*	A Hilbert lattice admits a largei set of states. Remark in [Mayet] p. 370. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (¬ 𝐴 = 0ℋ ↔ ∃𝑓 ∈ States (𝑓‘𝐴) = 1)
Theorem	jplem1 32529	Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((𝑢 ∈ ℋ ∧ (normℎ‘𝑢) = 1) → (𝑢 ∈ 𝐴 ↔ ((normℎ‘((projℎ‘𝐴)‘𝑢))↑2) = 1))
Theorem	jplem2 32530*	Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    &   ⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((𝑢 ∈ ℋ ∧ (normℎ‘𝑢) = 1) → (𝑢 ∈ 𝐴 ↔ (𝑆‘𝐴) = 1))
Theorem	jpi 32531*	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 in [Mayet] p. 370. (See strlem3a 32513 for the proof that 𝑆 is a state.) (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝑢 ∈ ℋ ∧ (normℎ‘𝑢) = 1) → (((𝑆‘𝐴) = 1 ∧ (𝑆‘𝐵) = 1) ↔ (𝑆‘(𝐴 ∩ 𝐵)) = 1))
20.7.2  Godowski's equation
Theorem	golem1 32532	Lemma for Godowski's equation. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))    &   ⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶))    &   ⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴))    &   ⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))    &   ⊢ 𝑅 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵))    &   ⊢ 𝑆 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶))    ⇒   ⊢ (𝑓 ∈ States → (((𝑓‘𝐹) + (𝑓‘𝐺)) + (𝑓‘𝐻)) = (((𝑓‘𝐷) + (𝑓‘𝑅)) + (𝑓‘𝑆)))
Theorem	golem2 32533	Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))    &   ⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶))    &   ⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴))    &   ⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))    &   ⊢ 𝑅 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵))    &   ⊢ 𝑆 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶))    ⇒   ⊢ (𝑓 ∈ States → ((𝑓‘((𝐹 ∩ 𝐺) ∩ 𝐻)) = 1 → (𝑓‘𝐷) = 1))
Theorem	goeqi 32534	Godowski's equation, shown here as a variant equivalent to Equation SF of [Godowski] p. 730. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))    &   ⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶))    &   ⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴))    &   ⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))    ⇒   ⊢ ((𝐹 ∩ 𝐺) ∩ 𝐻) ⊆ 𝐷
Theorem	stcltr1i 32535*	Property of a strong classical state. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑆 ∈ States ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (((𝑆‘𝑥) = 1 → (𝑆‘𝑦) = 1) → 𝑥 ⊆ 𝑦)))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → (((𝑆‘𝐴) = 1 → (𝑆‘𝐵) = 1) → 𝐴 ⊆ 𝐵))
Theorem	stcltr2i 32536*	Property of a strong classical state. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑆 ∈ States ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (((𝑆‘𝑥) = 1 → (𝑆‘𝑦) = 1) → 𝑥 ⊆ 𝑦)))    &   ⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝜑 → ((𝑆‘𝐴) = 1 → 𝐴 = ℋ))
Theorem	stcltrlem1 32537*	Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑆 ∈ States ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (((𝑆‘𝑥) = 1 → (𝑆‘𝑦) = 1) → 𝑥 ⊆ 𝑦)))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → ((𝑆‘𝐵) = 1 → (𝑆‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) = 1))
Theorem	stcltrlem2 32538*	Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝜑 ↔ (𝑆 ∈ States ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (((𝑆‘𝑥) = 1 → (𝑆‘𝑦) = 1) → 𝑥 ⊆ 𝑦)))    &   ⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝜑 → 𝐵 ⊆ ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵)))
Theorem	stcltrthi 32539*	Theorem for classically strong set of states. If there exists a "classically strong set of states" on lattice Cℋ (or actually any ortholattice, which would have an identical proof), then any two elements of the lattice commute, i.e., the lattice is distributive. (Proof due to Mladen Pavicic.) Theorem 3.3 of [MegPav2000] p. 2344. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ ∃𝑠 ∈ States ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (((𝑠‘𝑥) = 1 → (𝑠‘𝑦) = 1) → 𝑥 ⊆ 𝑦)    ⇒   ⊢ 𝐵 ⊆ ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))
20.8  Cover relation, atoms, exchange axiom, and modular symmetry
20.8.1  Covers relation; modular pairs
Definition	df-cv 32540*	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 cvbr 32543 and cvbr2 32544 for membership relations. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ ⋖ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ (𝑥 ⊊ 𝑦 ∧ ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)))}
Definition	df-md 32541*	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 32555 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
⊢ 𝑀ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑧 ⊆ 𝑦 → ((𝑧 ∨ℋ 𝑥) ∩ 𝑦) = (𝑧 ∨ℋ (𝑥 ∩ 𝑦))))}
Definition	df-dmd 32542*	Define the dual 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 dual modular pair." See dmdbr 32560 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝑀ℋ* = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))))}
Theorem	cvbr 32543*	Binary relation expressing 𝐵 covers 𝐴, which means that 𝐵 is larger than 𝐴 and there is nothing in between. Definition 3.2.18 of [PtakPulmannova] p. 68. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∧ ¬ ∃𝑥 ∈ Cℋ (𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵))))
Theorem	cvbr2 32544*	Binary relation expressing 𝐵 covers 𝐴. Definition of covers in [Kalmbach] p. 15. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∧ ∀𝑥 ∈ Cℋ ((𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ 𝐵) → 𝑥 = 𝐵))))
Theorem	cvcon3 32545	Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 ↔ (⊥‘𝐵) ⋖ℋ (⊥‘𝐴)))
Theorem	cvpss 32546	The covers relation implies proper subset. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵))
Theorem	cvnbtwn 32547	The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ (𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵)))
Theorem	cvnbtwn2 32548	The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵) → 𝐶 = 𝐵)))
Theorem	cvnbtwn3 32549	The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵) → 𝐶 = 𝐴)))
Theorem	cvnbtwn4 32550	The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) → (𝐶 = 𝐴 ∨ 𝐶 = 𝐵))))
Theorem	cvnsym 32551	The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ 𝐵 ⋖ℋ 𝐴))
Theorem	cvnref 32552	The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → ¬ 𝐴 ⋖ℋ 𝐴)
Theorem	cvntr 32553	The covers relation is not transitive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ⋖ℋ 𝐵 ∧ 𝐵 ⋖ℋ 𝐶) → ¬ 𝐴 ⋖ℋ 𝐶))
Theorem	spansncv2 32554	Hilbert space has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (¬ (span‘{𝐵}) ⊆ 𝐴 → 𝐴 ⋖ℋ (𝐴 ∨ℋ (span‘{𝐵}))))
Theorem	mdbr 32555*	Binary relation expressing ⟨𝐴, 𝐵⟩ is a modular pair. Definition 1.1 of [MaedaMaeda] p. 1. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))))
Theorem	mdi 32556	Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝐶 ⊆ 𝐵)) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐶 ∨ℋ (𝐴 ∩ 𝐵)))
Theorem	mdbr2 32557*	Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 32555. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))))
Theorem	mdbr3 32558*	Binary relation expressing the modular pair property. This version quantifies an equality instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵))))
Theorem	mdbr4 32559*	Binary relation expressing the modular pair property. This version quantifies an ordering instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵))))
Theorem	dmdbr 32560*	Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))))
Theorem	dmdmd 32561	The dual modular pair property expressed in terms of the modular pair property, that hold in Hilbert lattices. Remark 29.6 of [MaedaMaeda] p. 130. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ (⊥‘𝐴) 𝑀ℋ (⊥‘𝐵)))
Theorem	mddmd 32562	The modular pair property expressed in terms of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ (⊥‘𝐴) 𝑀ℋ* (⊥‘𝐵)))
Theorem	dmdi 32563	Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶)) → ((𝐶 ∩ 𝐴) ∨ℋ 𝐵) = (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))
Theorem	dmdbr2 32564*	Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr 32560. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝐵 ⊆ 𝑥 → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵))))
Theorem	dmdi2 32565	Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶)) → (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝐶 ∩ 𝐴) ∨ℋ 𝐵))
Theorem	dmdbr3 32566*	Binary relation expressing the dual modular pair property. This version quantifies an equality instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) = ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))))
Theorem	dmdbr4 32567*	Binary relation expressing the dual modular pair property. This version quantifies an ordering instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))
Theorem	dmdi4 32568	Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 → ((𝐶 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐶 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))
Theorem	dmdbr5 32569*	Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))))
Theorem	mddmd2 32570*	Relationship between modular pairs and dual-modular pairs. Lemma 1.2 of [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → (∀𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀𝑥 ∈ Cℋ 𝐴 𝑀ℋ* 𝑥))
Theorem	mdsl0 32571	A sublattice condition that transfers the modular pair property. Exercise 12 of [Kalmbach] p. 103. Also Lemma 1.5.3 of [MaedaMaeda] p. 2. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ (𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )) → ((((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ 𝐴 𝑀ℋ 𝐵) → 𝐶 𝑀ℋ 𝐷))
Theorem	ssmd1 32572	Ordering implies the modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐴 𝑀ℋ 𝐵)
Theorem	ssmd2 32573	Ordering implies the modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐵 𝑀ℋ 𝐴)
Theorem	ssdmd1 32574	Ordering implies the dual modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐴 𝑀ℋ* 𝐵)
Theorem	ssdmd2 32575	Ordering implies the dual modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → (⊥‘𝐵) 𝑀ℋ (⊥‘𝐴))
Theorem	dmdsl3 32576	Sublattice mapping for a dual-modular pair. Part of Theorem 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 26-Apr-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∩ 𝐵) ∨ℋ 𝐴) = 𝐶)
Theorem	mdsl3 32577	Sublattice mapping for a modular pair. Part of Theorem 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 26-Apr-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵)) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = 𝐶)
Theorem	mdslle1i 32578	Order preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ ((𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) → (𝐶 ⊆ 𝐷 ↔ (𝐶 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵)))
Theorem	mdslle2i 32579	Order preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵) → (𝐶 ⊆ 𝐷 ↔ (𝐶 ∨ℋ 𝐴) ⊆ (𝐷 ∨ℋ 𝐴)))
Theorem	mdslj1i 32580	Join preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∨ℋ 𝐷) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵)))
Theorem	mdslj2i 32581	Meet preservation of the reverse mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵)) → ((𝐶 ∩ 𝐷) ∨ℋ 𝐴) = ((𝐶 ∨ℋ 𝐴) ∩ (𝐷 ∨ℋ 𝐴)))
Theorem	mdsl1i 32582*	If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of [MaedaMaeda] p. 2. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑥 ∈ Cℋ (((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))) ↔ 𝐴 𝑀ℋ 𝐵)
Theorem	mdsl2i 32583*	If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of [MaedaMaeda] p. 2. (Contributed by NM, 28-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))
Theorem	mdsl2bi 32584*	If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of [MaedaMaeda] p. 2. (Contributed by NM, 24-Dec-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))
Theorem	cvmdi 32585	The covering property implies the modular pair property. Lemma 7.5.1 of [MaedaMaeda] p. 31. (Contributed by NM, 16-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∩ 𝐵) ⋖ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵)
Theorem	mdslmd1lem1 32586	Lemma for mdslmd1i 32590. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))
Theorem	mdslmd1lem2 32587	Lemma for mdslmd1i 32590. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)))))
Theorem	mdslmd1lem3 32588*	Lemma for mdslmd1i 32590. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ ((𝑥 ∈ Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))
Theorem	mdslmd1lem4 32589*	Lemma for mdslmd1i 32590. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ ((𝑥 ∈ Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷)))))
Theorem	mdslmd1i 32590	Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2 (meet version). (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐶 𝑀ℋ 𝐷 ↔ (𝐶 ∩ 𝐵) 𝑀ℋ (𝐷 ∩ 𝐵)))
Theorem	mdslmd2i 32591	Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2 (join version). (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵)) → (𝐶 𝑀ℋ 𝐷 ↔ (𝐶 ∨ℋ 𝐴) 𝑀ℋ (𝐷 ∨ℋ 𝐴)))
Theorem	mdsldmd1i 32592	Preservation of the dual modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐶 𝑀ℋ* 𝐷 ↔ (𝐶 ∩ 𝐵) 𝑀ℋ* (𝐷 ∩ 𝐵)))
Theorem	mdslmd3i 32593	Modular pair conditions that imply the modular pair property in a sublattice. Lemma 1.5.1 of [MaedaMaeda] p. 2. (Contributed by NM, 23-Dec-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) → 𝐷 𝑀ℋ (𝐵 ∩ 𝐶))
Theorem	mdslmd4i 32594	Modular pair condition that implies the modular pair property in a sublattice. Lemma 1.5.2 of [MaedaMaeda] p. 2. (Contributed by NM, 24-Dec-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵)) → 𝐶 𝑀ℋ 𝐷)
Theorem	csmdsymi 32595*	Cross-symmetry implies M-symmetry. Theorem 1.9.1 of [MaedaMaeda] p. 3. (Contributed by NM, 24-Dec-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((∀𝑐 ∈ Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐) ∧ 𝐴 𝑀ℋ 𝐵) → 𝐵 𝑀ℋ 𝐴)
Theorem	mdexchi 32596	An exchange lemma for modular pairs. Lemma 1.6 of [MaedaMaeda] p. 2. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) 𝑀ℋ 𝐵 ∧ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵)))
Theorem	cvmd 32597	The covering property implies the modular pair property. Lemma 7.5.1 of [MaedaMaeda] p. 31. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ (𝐴 ∩ 𝐵) ⋖ℋ 𝐵) → 𝐴 𝑀ℋ 𝐵)
Theorem	cvdmd 32598	The covering property implies the dual modular pair property. Lemma 7.5.2 of [MaedaMaeda] p. 31. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐵 ⋖ℋ (𝐴 ∨ℋ 𝐵)) → 𝐴 𝑀ℋ* 𝐵)
20.8.2  Atoms
Definition	df-at 32599	Define the set of atoms in a Hilbert lattice. An atom is a nonzero element of a lattice such that anything less than it is zero, i.e. it is the smallest nonzero element of the lattice. Definition of atom in [Kalmbach] p. 15. See ela 32600 and elat2 32601 for membership relations. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.)
⊢ HAtoms = {𝑥 ∈ Cℋ ∣ 0ℋ ⋖ℋ 𝑥}
Theorem	ela 32600	Atoms in a Hilbert lattice are the elements that cover the zero subspace. Definition of atom in [Kalmbach] p. 15. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ HAtoms ↔ (𝐴 ∈ Cℋ ∧ 0ℋ ⋖ℋ 𝐴))