P. 323 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32201-32300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	stle0i 32201	If a state is less than or equal to 0, it is 0. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘𝐴) ≤ 0 ↔ (𝑆‘𝐴) = 0))
Theorem	stlei 32202	Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → (𝑆‘𝐴) ≤ (𝑆‘𝐵)))
Theorem	stlesi 32203	Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → ((𝑆‘𝐴) = 1 → (𝑆‘𝐵) = 1)))
Theorem	stji1i 32204	Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝑆‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) = ((𝑆‘(⊥‘𝐴)) + (𝑆‘(𝐴 ∩ 𝐵))))
Theorem	stm1i 32205	State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐴) = 1))
Theorem	stm1ri 32206	State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐵) = 1))
Theorem	stm1addi 32207	Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → ((𝑆‘𝐴) + (𝑆‘𝐵)) = 2))
Theorem	staddi 32208	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 32209	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 32210	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 32211	The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝑆‘0ℋ) = 0)
Theorem	strlem1 32212*	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 32213*	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 32214*	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 32215*	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 32216*	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 32217*	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 32218*	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 32219*	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 32220*	Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑓 ∈ States ((𝑓‘𝐴) = 1 → (𝑓‘𝐵) = 1) ↔ 𝐴 ⊆ 𝐵)
Theorem	hstrlem2 32221*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    ⇒   ⊢ (𝐶 ∈ Cℋ → (𝑆‘𝐶) = ((projℎ‘𝐶)‘𝑢))
Theorem	hstrlem3a 32222*	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 32223*	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 32224*	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 32225*	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 32226*	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 32227*	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 32228*	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 32229*	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 32230	Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((𝑢 ∈ ℋ ∧ (normℎ‘𝑢) = 1) → (𝑢 ∈ 𝐴 ↔ ((normℎ‘((projℎ‘𝐴)‘𝑢))↑2) = 1))
Theorem	jplem2 32231*	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 32232*	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 32214 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 32233	Lemma for Godowski's equation. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))    &   ⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶))    &   ⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴))    &   ⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))    &   ⊢ 𝑅 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵))    &   ⊢ 𝑆 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶))    ⇒   ⊢ (𝑓 ∈ States → (((𝑓‘𝐹) + (𝑓‘𝐺)) + (𝑓‘𝐻)) = (((𝑓‘𝐷) + (𝑓‘𝑅)) + (𝑓‘𝑆)))
Theorem	golem2 32234	Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))    &   ⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶))    &   ⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴))    &   ⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))    &   ⊢ 𝑅 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵))    &   ⊢ 𝑆 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶))    ⇒   ⊢ (𝑓 ∈ States → ((𝑓‘((𝐹 ∩ 𝐺) ∩ 𝐻)) = 1 → (𝑓‘𝐷) = 1))
Theorem	goeqi 32235	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 32236*	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 32237*	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 32238*	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 32239*	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 32240*	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 32241*	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 32244 and cvbr2 32245 for membership relations. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ ⋖ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ (𝑥 ⊊ 𝑦 ∧ ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)))}
Definition	df-md 32242*	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 32256 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
⊢ 𝑀ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑧 ⊆ 𝑦 → ((𝑧 ∨ℋ 𝑥) ∩ 𝑦) = (𝑧 ∨ℋ (𝑥 ∩ 𝑦))))}
Definition	df-dmd 32243*	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 32261 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝑀ℋ* = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))))}
Theorem	cvbr 32244*	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 32245*	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 32246	Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 ↔ (⊥‘𝐵) ⋖ℋ (⊥‘𝐴)))
Theorem	cvpss 32247	The covers relation implies proper subset. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵))
Theorem	cvnbtwn 32248	The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ (𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵)))
Theorem	cvnbtwn2 32249	The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵) → 𝐶 = 𝐵)))
Theorem	cvnbtwn3 32250	The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵) → 𝐶 = 𝐴)))
Theorem	cvnbtwn4 32251	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 32252	The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ 𝐵 ⋖ℋ 𝐴))
Theorem	cvnref 32253	The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → ¬ 𝐴 ⋖ℋ 𝐴)
Theorem	cvntr 32254	The covers relation is not transitive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ⋖ℋ 𝐵 ∧ 𝐵 ⋖ℋ 𝐶) → ¬ 𝐴 ⋖ℋ 𝐶))
Theorem	spansncv2 32255	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 32256*	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 32257	Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝐶 ⊆ 𝐵)) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐶 ∨ℋ (𝐴 ∩ 𝐵)))
Theorem	mdbr2 32258*	Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 32256. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))))
Theorem	mdbr3 32259*	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 32260*	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 32261*	Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))))
Theorem	dmdmd 32262	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 32263	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 32264	Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶)) → ((𝐶 ∩ 𝐴) ∨ℋ 𝐵) = (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))
Theorem	dmdbr2 32265*	Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr 32261. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝐵 ⊆ 𝑥 → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵))))
Theorem	dmdi2 32266	Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶)) → (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝐶 ∩ 𝐴) ∨ℋ 𝐵))
Theorem	dmdbr3 32267*	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 32268*	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 32269	Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 → ((𝐶 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐶 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))
Theorem	dmdbr5 32270*	Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))))
Theorem	mddmd2 32271*	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 32272	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 32273	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 32274	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 32275	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 32276	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 32277	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 32278	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 32279	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 32280	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 32281	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 32282	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 32283*	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 32284*	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 32285*	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 32286	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 32287	Lemma for mdslmd1i 32291. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))
Theorem	mdslmd1lem2 32288	Lemma for mdslmd1i 32291. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)))))
Theorem	mdslmd1lem3 32289*	Lemma for mdslmd1i 32291. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ ((𝑥 ∈ Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))
Theorem	mdslmd1lem4 32290*	Lemma for mdslmd1i 32291. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ ((𝑥 ∈ Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷)))))
Theorem	mdslmd1i 32291	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 32292	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 32293	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 32294	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 32295	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 32296*	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 32297	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 32298	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 32299	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 32300	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 32301 and elat2 32302 for membership relations. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.)
⊢ HAtoms = {𝑥 ∈ Cℋ ∣ 0ℋ ⋖ℋ 𝑥}