P. 299 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29801-29900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lejdii 29801	An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)) ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐶))
Theorem	lejdiri 29802	An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∩ 𝐵) ∨ℋ 𝐶) ⊆ ((𝐴 ∨ℋ 𝐶) ∩ (𝐵 ∨ℋ 𝐶))
Theorem	ledi 29803	An ortholattice is distributive in one ordering direction. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)))
19.5.4  Span (cont.) and one-dimensional subspaces
Theorem	spansn0 29804	The span of the singleton of the zero vector is the zero subspace. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.)
⊢ (span‘{0ℎ}) = 0ℋ
Theorem	span0 29805	The span of the empty set is the zero subspace. Remark 11.6.e of [Schechter] p. 276. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ (span‘∅) = 0ℋ
Theorem	elspani 29806*	Membership in the span of a subset of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ ℋ → (𝐵 ∈ (span‘𝐴) ↔ ∀𝑥 ∈ Sℋ (𝐴 ⊆ 𝑥 → 𝐵 ∈ 𝑥)))
Theorem	spanuni 29807	The span of a union is the subspace sum of spans. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ⊆ ℋ    &   ⊢ 𝐵 ⊆ ℋ    ⇒   ⊢ (span‘(𝐴 ∪ 𝐵)) = ((span‘𝐴) +ℋ (span‘𝐵))
Theorem	spanun 29808	The span of a union is the subspace sum of spans. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (span‘(𝐴 ∪ 𝐵)) = ((span‘𝐴) +ℋ (span‘𝐵)))
Theorem	sshhococi 29809	The join of two Hilbert space subsets (not necessarily closed subspaces) equals the join of their closures (double orthocomplements). (Contributed by NM, 1-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ⊆ ℋ    &   ⊢ 𝐵 ⊆ ℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) = ((⊥‘(⊥‘𝐴)) ∨ℋ (⊥‘(⊥‘𝐵)))
Theorem	hne0 29810	Hilbert space has a nonzero vector iff it is not trivial. (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.)
⊢ ( ℋ ≠ 0ℋ ↔ ∃𝑥 ∈ ℋ 𝑥 ≠ 0ℎ)
Theorem	chsup0 29811	The supremum of the empty set. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ ( ∨ℋ ‘∅) = 0ℋ
Theorem	h1deoi 29812	Membership in orthocomplement of 1-dimensional subspace. (Contributed by NM, 7-Jul-2001.) (New usage is discouraged.)
⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘{𝐵}) ↔ (𝐴 ∈ ℋ ∧ (𝐴 ·ih 𝐵) = 0))
Theorem	h1dei 29813*	Membership in 1-dimensional subspace. (Contributed by NM, 7-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ ℋ ((𝐵 ·ih 𝑥) = 0 → (𝐴 ·ih 𝑥) = 0)))
Theorem	h1did 29814	A generating vector belongs to the 1-dimensional subspace it generates. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (⊥‘(⊥‘{𝐴})))
Theorem	h1dn0 29815	A nonzero vector generates a (nonzero) 1-dimensional subspace. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (⊥‘(⊥‘{𝐴})) ≠ 0ℋ)
Theorem	h1de2i 29816	Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 17-Jul-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) → ((𝐵 ·ih 𝐵) ·ℎ 𝐴) = ((𝐴 ·ih 𝐵) ·ℎ 𝐵))
Theorem	h1de2bi 29817	Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐵 ≠ 0ℎ → (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ 𝐴 = (((𝐴 ·ih 𝐵) / (𝐵 ·ih 𝐵)) ·ℎ 𝐵)))
Theorem	h1de2ctlem 29818*	Lemma for h1de2ci 29819. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ ∃𝑥 ∈ ℂ 𝐴 = (𝑥 ·ℎ 𝐵))
Theorem	h1de2ci 29819*	Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 21-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ ∃𝑥 ∈ ℂ 𝐴 = (𝑥 ·ℎ 𝐵))
Theorem	spansni 29820	The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (span‘{𝐴}) = (⊥‘(⊥‘{𝐴}))
Theorem	elspansni 29821*	Membership in the span of a singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (𝐵 ∈ (span‘{𝐴}) ↔ ∃𝑥 ∈ ℂ 𝐵 = (𝑥 ·ℎ 𝐴))
Theorem	spansn 29822	The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) = (⊥‘(⊥‘{𝐴})))
Theorem	spansnch 29823	The span of a Hilbert space singleton belongs to the Hilbert lattice. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) ∈ Cℋ )
Theorem	spansnsh 29824	The span of a Hilbert space singleton is a subspace. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) ∈ Sℋ )
Theorem	spansnchi 29825	The span of a singleton in Hilbert space is a closed subspace. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (span‘{𝐴}) ∈ Cℋ
Theorem	spansnid 29826	A vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (span‘{𝐴}))
Theorem	spansnmul 29827	A scalar product with a vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) → (𝐵 ·ℎ 𝐴) ∈ (span‘{𝐴}))
Theorem	elspansncl 29828	A member of a span of a singleton is a vector. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ (span‘{𝐴})) → 𝐵 ∈ ℋ)
Theorem	elspansn 29829*	Membership in the span of a singleton. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐵 ∈ (span‘{𝐴}) ↔ ∃𝑥 ∈ ℂ 𝐵 = (𝑥 ·ℎ 𝐴)))
Theorem	elspansn2 29830	Membership in the span of a singleton. All members are collinear with the generating vector. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ) → (𝐴 ∈ (span‘{𝐵}) ↔ 𝐴 = (((𝐴 ·ih 𝐵) / (𝐵 ·ih 𝐵)) ·ℎ 𝐵)))
Theorem	spansncol 29831	The singletons of collinear vectors have the same span. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (span‘{(𝐵 ·ℎ 𝐴)}) = (span‘{𝐴}))
Theorem	spansneleqi 29832	Membership relation implied by equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((span‘{𝐴}) = (span‘{𝐵}) → 𝐴 ∈ (span‘{𝐵})))
Theorem	spansneleq 29833	Membership relation that implies equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (𝐴 ∈ (span‘{𝐵}) → (span‘{𝐴}) = (span‘{𝐵})))
Theorem	spansnss 29834	The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴) → (span‘{𝐵}) ⊆ 𝐴)
Theorem	elspansn3 29835	A member of the span of the singleton of a vector is a member of a subspace containing the vector. (Contributed by NM, 16-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ (span‘{𝐵})) → 𝐶 ∈ 𝐴)
Theorem	elspansn4 29836	A span membership condition implying two vectors belong to the same subspace. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ (span‘{𝐵}) ∧ 𝐶 ≠ 0ℎ)) → (𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴))
Theorem	elspansn5 29837	A vector belonging to both a subspace and the span of the singleton of a vector not in it must be zero. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ Sℋ → (((𝐵 ∈ ℋ ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝐶 ∈ (span‘{𝐵}) ∧ 𝐶 ∈ 𝐴)) → 𝐶 = 0ℎ))
Theorem	spansnss2 29838	The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 16-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ) → (𝐵 ∈ 𝐴 ↔ (span‘{𝐵}) ⊆ 𝐴))
Theorem	normcan 29839	Cancellation-type law that "extracts" a vector 𝐴 from its inner product with a proportional vector 𝐵. (Contributed by NM, 18-Mar-2006.) (New usage is discouraged.)
⊢ ((𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ∧ 𝐴 ∈ (span‘{𝐵})) → (((𝐴 ·ih 𝐵) / ((normℎ‘𝐵)↑2)) ·ℎ 𝐵) = 𝐴)
Theorem	pjspansn 29840	A projection on the span of a singleton. (The proof ws shortened by Mario Carneiro, 15-Dec-2013.) (Contributed by NM, 28-May-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → ((projℎ‘(span‘{𝐴}))‘𝐵) = (((𝐵 ·ih 𝐴) / ((normℎ‘𝐴)↑2)) ·ℎ 𝐴))
Theorem	spansnpji 29841	A subset of Hilbert space is orthogonal to the span of the singleton of a projection onto its orthocomplement. (Contributed by NM, 4-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ⊆ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ 𝐴 ⊆ (⊥‘(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)}))
Theorem	spanunsni 29842	The span of the union of a closed subspace with a singleton equals the span of its union with an orthogonal singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (span‘(𝐴 ∪ {𝐵})) = (span‘(𝐴 ∪ {((projℎ‘(⊥‘𝐴))‘𝐵)}))
Theorem	spanpr 29843	The span of a pair of vectors. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (span‘{(𝐴 +ℎ 𝐵)}) ⊆ (span‘{𝐴, 𝐵}))
Theorem	h1datomi 29844	A 1-dimensional subspace is an atom. (Contributed by NM, 20-Jul-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ⊆ (⊥‘(⊥‘{𝐵})) → (𝐴 = (⊥‘(⊥‘{𝐵})) ∨ 𝐴 = 0ℋ))
Theorem	h1datom 29845	A 1-dimensional subspace is an atom. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ⊆ (⊥‘(⊥‘{𝐵})) → (𝐴 = (⊥‘(⊥‘{𝐵})) ∨ 𝐴 = 0ℋ)))
19.5.5  Commutes relation for Hilbert lattice elements
Definition	df-cm 29846*	Define the commutes relation (on the Hilbert lattice). Definition of commutes in [Kalmbach] p. 20, who uses the notation xCy for "x commutes with y." See cmbri 29853 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
⊢ 𝐶ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 = ((𝑥 ∩ 𝑦) ∨ℋ (𝑥 ∩ (⊥‘𝑦))))}
Theorem	cmbr 29847	Binary relation expressing 𝐴 commutes with 𝐵. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵)))))
Theorem	pjoml2i 29848	Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵)
Theorem	pjoml3i 29849	Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵)
Theorem	pjoml4i 29850	Variation of orthomodular law. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∩ ((⊥‘𝐴) ∨ℋ (⊥‘𝐵)))) = (𝐴 ∨ℋ 𝐵)
Theorem	pjoml5i 29851	The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵)
Theorem	pjoml6i 29852*	An equivalent of the orthomodular law. Theorem 29.13(e) of [MaedaMaeda] p. 132. (Contributed by NM, 30-May-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → ∃𝑥 ∈ Cℋ (𝐴 ⊆ (⊥‘𝑥) ∧ (𝐴 ∨ℋ 𝑥) = 𝐵))
Theorem	cmbri 29853	Binary relation expressing the commutes relation. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵))))
Theorem	cmcmlem 29854	Commutation is symmetric. Theorem 3.4 of [Beran] p. 45. (Contributed by NM, 3-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐵 𝐶ℋ 𝐴)
Theorem	cmcmi 29855	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴)
Theorem	cmcm2i 29856	Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ (⊥‘𝐵))
Theorem	cmcm3i 29857	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵)
Theorem	cmcm4i 29858	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ (⊥‘𝐵))
Theorem	cmbr2i 29859	Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ (⊥‘𝐵))))
Theorem	cmcmii 29860	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    ⇒   ⊢ 𝐵 𝐶ℋ 𝐴
Theorem	cmcm2ii 29861	Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    ⇒   ⊢ 𝐴 𝐶ℋ (⊥‘𝐵)
Theorem	cmcm3ii 29862	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    ⇒   ⊢ (⊥‘𝐴) 𝐶ℋ 𝐵
Theorem	cmbr3i 29863	Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ 𝐵))
Theorem	cmbr4i 29864	Alternate definition for the commutes relation. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) ⊆ 𝐵)
Theorem	lecmi 29865	Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 𝐶ℋ 𝐵)
Theorem	lecmii 29866	Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 𝐶ℋ 𝐵
Theorem	cmj1i 29867	A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ (𝐴 ∨ℋ 𝐵)
Theorem	cmj2i 29868	A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐵 𝐶ℋ (𝐴 ∨ℋ 𝐵)
Theorem	cmm1i 29869	A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ (𝐴 ∩ 𝐵)
Theorem	cmm2i 29870	A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐵 𝐶ℋ (𝐴 ∩ 𝐵)
Theorem	cmbr3 29871	Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ 𝐵)))
Theorem	cm0 29872	The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → 0ℋ 𝐶ℋ 𝐴)
Theorem	cmidi 29873	The commutes relation is reflexive. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ 𝐴
Theorem	pjoml2 29874	Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵)
Theorem	pjoml3 29875	Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵))
Theorem	pjoml5 29876	The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵))
Theorem	cmcm 29877	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴))
Theorem	cmcm3 29878	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵))
Theorem	cmcm2 29879	Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ (⊥‘𝐵)))
Theorem	lecm 29880	Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐴 𝐶ℋ 𝐵)
19.5.6  Foulis-Holland theorem
Theorem	fh1 29881	Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of [Kalmbach] p. 25. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))
Theorem	fh2 29882	Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Second of two parts. Theorem 5 of [Kalmbach] p. 25. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))
Theorem	cm2j 29883	A lattice element that commutes with two others also commutes with their join. Theorem 4.2 of [Beran] p. 49. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → 𝐴 𝐶ℋ (𝐵 ∨ℋ 𝐶))
Theorem	fh1i 29884	Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of [Kalmbach] p. 25. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶))
Theorem	fh2i 29885	Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Second of two parts. Theorem 5 of [Kalmbach] p. 25. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐶)) = ((𝐵 ∩ 𝐴) ∨ℋ (𝐵 ∩ 𝐶))
Theorem	fh3i 29886	Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)) = ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐶))
Theorem	fh4i 29887	Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐵 ∨ℋ (𝐴 ∩ 𝐶)) = ((𝐵 ∨ℋ 𝐴) ∩ (𝐵 ∨ℋ 𝐶))
Theorem	cm2ji 29888	A lattice element that commutes with two others also commutes with their join. Theorem 4.2 of [Beran] p. 49. (Contributed by NM, 11-May-2009.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ 𝐴 𝐶ℋ (𝐵 ∨ℋ 𝐶)
Theorem	cm2mi 29889	A lattice element that commutes with two others also commutes with their meet. Theorem 4.2 of [Beran] p. 49. (Contributed by NM, 11-May-2009.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ 𝐴 𝐶ℋ (𝐵 ∩ 𝐶)
19.5.7  Quantum Logic Explorer axioms
Theorem	qlax1i 29890	One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-1" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 = (⊥‘(⊥‘𝐴))
Theorem	qlax2i 29891	One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-2" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴)
Theorem	qlax3i 29892	One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-3" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶))
Theorem	qlax4i 29893	One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-4" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∨ℋ (⊥‘𝐵))) = (𝐵 ∨ℋ (⊥‘𝐵))
Theorem	qlax5i 29894	One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-5" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ (⊥‘((⊥‘𝐴) ∨ℋ 𝐵))) = 𝐴
Theorem	qlaxr1i 29895	One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r1" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ 𝐵 = 𝐴
Theorem	qlaxr2i 29896	One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r2" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 = 𝐵    &   ⊢ 𝐵 = 𝐶    ⇒   ⊢ 𝐴 = 𝐶
Theorem	qlaxr4i 29897	One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r4" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ (⊥‘𝐴) = (⊥‘𝐵)
Theorem	qlaxr5i 29898	One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r5" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐴 ∨ℋ 𝐶) = (𝐵 ∨ℋ 𝐶)
Theorem	qlaxr3i 29899	A variation of the orthomodular law, showing Cℋ is an orthomodular lattice. (This corresponds to axiom "ax-r3" in the Quantum Logic Explorer.) (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ (𝐶 ∨ℋ (⊥‘𝐶)) = ((⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) ∨ℋ (⊥‘(𝐴 ∨ℋ 𝐵)))    ⇒   ⊢ 𝐴 = 𝐵
19.5.8  Orthogonal subspaces
Theorem	chscllem1 29900*	Lemma for chscl 29904. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶𝐴)