P. 324 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32301-32400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hstle 32301	Ordering property of a Hilbert-space-valued state. (Contributed by NM, 26-Jun-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵)) → (normℎ‘(𝑆‘𝐴)) ≤ (normℎ‘(𝑆‘𝐵)))
Theorem	hstles 32302	Ordering property of a Hilbert-space-valued state. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵)) → ((normℎ‘(𝑆‘𝐴)) = 1 → (normℎ‘(𝑆‘𝐵)) = 1))
Theorem	hstoh 32303	A Hilbert-space-valued state orthogonal to the state of the lattice one is zero. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.)
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ∧ ((𝑆‘𝐴) ·ih (𝑆‘ ℋ)) = 0) → (𝑆‘𝐴) = 0ℎ)
Theorem	hst0 32304	A Hilbert-space-valued state is zero at the zero subspace. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ (𝑆 ∈ CHStates → (𝑆‘0ℋ) = 0ℎ)
Theorem	sthil 32305	The value of a state at the full Hilbert space. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝑆‘ ℋ) = 1)
Theorem	stj 32306	The value of a state on a join. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐴 ⊆ (⊥‘𝐵)) → (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) + (𝑆‘𝐵))))
Theorem	sto1i 32307	The state of a subspace plus the state of its orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘𝐴) + (𝑆‘(⊥‘𝐴))) = 1)
Theorem	sto2i 32308	The state of the orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝑆‘(⊥‘𝐴)) = (1 − (𝑆‘𝐴)))
Theorem	stge1i 32309	If a state is greater than or equal to 1, it is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (1 ≤ (𝑆‘𝐴) ↔ (𝑆‘𝐴) = 1))
Theorem	stle0i 32310	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 32311	Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → (𝑆‘𝐴) ≤ (𝑆‘𝐵)))
Theorem	stlesi 32312	Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → ((𝑆‘𝐴) = 1 → (𝑆‘𝐵) = 1)))
Theorem	stji1i 32313	Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → (𝑆‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) = ((𝑆‘(⊥‘𝐴)) + (𝑆‘(𝐴 ∩ 𝐵))))
Theorem	stm1i 32314	State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐴) = 1))
Theorem	stm1ri 32315	State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐵) = 1))
Theorem	stm1addi 32316	Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → ((𝑆‘𝐴) + (𝑆‘𝐵)) = 2))
Theorem	staddi 32317	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 32318	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 32319	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 32320	The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝑆 ∈ States → (𝑆‘0ℋ) = 0)
Theorem	strlem1 32321*	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 32322*	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 32323*	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 32324*	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 32325*	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 32326*	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 32327*	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 32328*	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 32329*	Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (∀𝑓 ∈ States ((𝑓‘𝐴) = 1 → (𝑓‘𝐵) = 1) ↔ 𝐴 ⊆ 𝐵)
Theorem	hstrlem2 32330*	Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢))    ⇒   ⊢ (𝐶 ∈ Cℋ → (𝑆‘𝐶) = ((projℎ‘𝐶)‘𝑢))
Theorem	hstrlem3a 32331*	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 32332*	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 32333*	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 32334*	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 32335*	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 32336*	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 32337*	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 32338*	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 32339	Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ ((𝑢 ∈ ℋ ∧ (normℎ‘𝑢) = 1) → (𝑢 ∈ 𝐴 ↔ ((normℎ‘((projℎ‘𝐴)‘𝑢))↑2) = 1))
Theorem	jplem2 32340*	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 32341*	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 32323 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 32342	Lemma for Godowski's equation. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))    &   ⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶))    &   ⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴))    &   ⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))    &   ⊢ 𝑅 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵))    &   ⊢ 𝑆 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶))    ⇒   ⊢ (𝑓 ∈ States → (((𝑓‘𝐹) + (𝑓‘𝐺)) + (𝑓‘𝐻)) = (((𝑓‘𝐷) + (𝑓‘𝑅)) + (𝑓‘𝑆)))
Theorem	golem2 32343	Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))    &   ⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶))    &   ⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴))    &   ⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴))    &   ⊢ 𝑅 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵))    &   ⊢ 𝑆 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶))    ⇒   ⊢ (𝑓 ∈ States → ((𝑓‘((𝐹 ∩ 𝐺) ∩ 𝐻)) = 1 → (𝑓‘𝐷) = 1))
Theorem	goeqi 32344	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 32345*	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 32346*	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 32347*	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 32348*	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 32349*	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 32350*	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 32353 and cvbr2 32354 for membership relations. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ ⋖ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ (𝑥 ⊊ 𝑦 ∧ ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)))}
Definition	df-md 32351*	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 32365 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
⊢ 𝑀ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑧 ⊆ 𝑦 → ((𝑧 ∨ℋ 𝑥) ∩ 𝑦) = (𝑧 ∨ℋ (𝑥 ∩ 𝑦))))}
Definition	df-dmd 32352*	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 32370 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝑀ℋ* = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))))}
Theorem	cvbr 32353*	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 32354*	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 32355	Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 ↔ (⊥‘𝐵) ⋖ℋ (⊥‘𝐴)))
Theorem	cvpss 32356	The covers relation implies proper subset. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵))
Theorem	cvnbtwn 32357	The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ (𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵)))
Theorem	cvnbtwn2 32358	The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵) → 𝐶 = 𝐵)))
Theorem	cvnbtwn3 32359	The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵) → 𝐶 = 𝐴)))
Theorem	cvnbtwn4 32360	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 32361	The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ 𝐵 ⋖ℋ 𝐴))
Theorem	cvnref 32362	The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → ¬ 𝐴 ⋖ℋ 𝐴)
Theorem	cvntr 32363	The covers relation is not transitive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ⋖ℋ 𝐵 ∧ 𝐵 ⋖ℋ 𝐶) → ¬ 𝐴 ⋖ℋ 𝐶))
Theorem	spansncv2 32364	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 32365*	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 32366	Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝐶 ⊆ 𝐵)) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐶 ∨ℋ (𝐴 ∩ 𝐵)))
Theorem	mdbr2 32367*	Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 32365. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))))
Theorem	mdbr3 32368*	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 32369*	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 32370*	Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))))
Theorem	dmdmd 32371	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 32372	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 32373	Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶)) → ((𝐶 ∩ 𝐴) ∨ℋ 𝐵) = (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))
Theorem	dmdbr2 32374*	Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr 32370. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝐵 ⊆ 𝑥 → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵))))
Theorem	dmdi2 32375	Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶)) → (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝐶 ∩ 𝐴) ∨ℋ 𝐵))
Theorem	dmdbr3 32376*	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 32377*	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 32378	Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 → ((𝐶 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐶 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))
Theorem	dmdbr5 32379*	Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))))
Theorem	mddmd2 32380*	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 32381	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 32382	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 32383	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 32384	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 32385	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 32386	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 32387	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 32388	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 32389	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 32390	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 32391	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 32392*	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 32393*	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 32394*	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 32395	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 32396	Lemma for mdslmd1i 32400. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))
Theorem	mdslmd1lem2 32397	Lemma for mdslmd1i 32400. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)))))
Theorem	mdslmd1lem3 32398*	Lemma for mdslmd1i 32400. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ ((𝑥 ∈ Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))
Theorem	mdslmd1lem4 32399*	Lemma for mdslmd1i 32400. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ ((𝑥 ∈ Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷)))))
Theorem	mdslmd1i 32400	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ℋ    ⇒   ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐶 𝑀ℋ 𝐷 ↔ (𝐶 ∩ 𝐵) 𝑀ℋ (𝐷 ∩ 𝐵)))