P. 286 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28501-28600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	chnle 28501	Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ (𝐴 ∨ℋ 𝐵)))
Theorem	chjo 28502	The join of a closed subspace and its orthocomplement is all of Hilbert space. (Contributed by NM, 31-Oct-2005.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → (𝐴 ∨ℋ (⊥‘𝐴)) = ℋ)
Theorem	chabs1 28503	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ (𝐴 ∩ 𝐵)) = 𝐴)
Theorem	chabs2 28504	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 16-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴)
Theorem	chabs1i 28505	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ (𝐴 ∩ 𝐵)) = 𝐴
Theorem	chabs2i 28506	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 16-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴
Theorem	chjidm 28507	Idempotent law for Hilbert lattice join. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → (𝐴 ∨ℋ 𝐴) = 𝐴)
Theorem	chjidmi 28508	Idempotent law for Hilbert lattice join. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ 𝐴) = 𝐴
Theorem	chj12i 28509	A rearrangement of Hilbert lattice join. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) = (𝐵 ∨ℋ (𝐴 ∨ℋ 𝐶))
Theorem	chj4i 28510	Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ (𝐶 ∨ℋ 𝐷)) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐷))
Theorem	chjjdiri 28511	Hilbert lattice join distributes over itself. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐶))
Theorem	chdmm1 28512	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∩ 𝐵)) = ((⊥‘𝐴) ∨ℋ (⊥‘𝐵)))
Theorem	chdmm2 28513	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∩ 𝐵)) = (𝐴 ∨ℋ (⊥‘𝐵)))
Theorem	chdmm3 28514	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∩ (⊥‘𝐵))) = ((⊥‘𝐴) ∨ℋ 𝐵))
Theorem	chdmm4 28515	De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))) = (𝐴 ∨ℋ 𝐵))
Theorem	chdmj1 28516	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∨ℋ 𝐵)) = ((⊥‘𝐴) ∩ (⊥‘𝐵)))
Theorem	chdmj2 28517	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ (⊥‘𝐵)))
Theorem	chdmj3 28518	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∨ℋ (⊥‘𝐵))) = ((⊥‘𝐴) ∩ 𝐵))
Theorem	chdmj4 28519	De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) = (𝐴 ∩ 𝐵))
Theorem	chjass 28520	Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)))
Theorem	chj12 28521	A rearrangement of Hilbert lattice join. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) = (𝐵 ∨ℋ (𝐴 ∨ℋ 𝐶)))
Theorem	chj4 28522	Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ (𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )) → ((𝐴 ∨ℋ 𝐵) ∨ℋ (𝐶 ∨ℋ 𝐷)) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐷)))
Theorem	ledii 28523	An ortholattice is distributive in one ordering direction. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))
Theorem	lediri 28524	An ortholattice is distributive in one ordering direction. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∩ 𝐶) ∨ℋ (𝐵 ∩ 𝐶)) ⊆ ((𝐴 ∨ℋ 𝐵) ∩ 𝐶)
Theorem	lejdii 28525	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 28526	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 28527	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 28528	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 28529	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 28530*	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 28531	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 28532	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 28533	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 28534	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 28535	The supremum of the empty set. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.)
⊢ ( ∨ℋ ‘∅) = 0ℋ
Theorem	h1deoi 28536	Membership in orthocomplement of 1-dimensional subspace. (Contributed by NM, 7-Jul-2001.) (New usage is discouraged.)
⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘{𝐵}) ↔ (𝐴 ∈ ℋ ∧ (𝐴 ·ih 𝐵) = 0))
Theorem	h1dei 28537*	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 28538	A generating vector belongs to the 1-dimensional subspace it generates. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (⊥‘(⊥‘{𝐴})))
Theorem	h1dn0 28539	A nonzero vector generates a (nonzero) 1-dimensional subspace. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (⊥‘(⊥‘{𝐴})) ≠ 0ℋ)
Theorem	h1de2i 28540	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 28541	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 28542*	Lemma for h1de2ci 28543. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ ∃𝑥 ∈ ℂ 𝐴 = (𝑥 ·ℎ 𝐵))
Theorem	h1de2ci 28543*	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 28544	The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (span‘{𝐴}) = (⊥‘(⊥‘{𝐴}))
Theorem	elspansni 28545*	Membership in the span of a singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (𝐵 ∈ (span‘{𝐴}) ↔ ∃𝑥 ∈ ℂ 𝐵 = (𝑥 ·ℎ 𝐴))
Theorem	spansn 28546	The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) = (⊥‘(⊥‘{𝐴})))
Theorem	spansnch 28547	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 28548	The span of a Hilbert space singleton is a subspace. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) ∈ Sℋ )
Theorem	spansnchi 28549	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 28550	A vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (span‘{𝐴}))
Theorem	spansnmul 28551	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 28552	A member of a span of a singleton is a vector. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ (span‘{𝐴})) → 𝐵 ∈ ℋ)
Theorem	elspansn 28553*	Membership in the span of a singleton. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐵 ∈ (span‘{𝐴}) ↔ ∃𝑥 ∈ ℂ 𝐵 = (𝑥 ·ℎ 𝐴)))
Theorem	elspansn2 28554	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 28555	The singletons of collinear vectors have the same span. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (span‘{(𝐵 ·ℎ 𝐴)}) = (span‘{𝐴}))
Theorem	spansneleqi 28556	Membership relation implied by equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((span‘{𝐴}) = (span‘{𝐵}) → 𝐴 ∈ (span‘{𝐵})))
Theorem	spansneleq 28557	Membership relation that implies equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (𝐴 ∈ (span‘{𝐵}) → (span‘{𝐴}) = (span‘{𝐵})))
Theorem	spansnss 28558	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 28559	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 28560	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 28561	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 28562	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 28563	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 28564	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 28565	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 28566	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 28567	The span of a pair of vectors. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (span‘{(𝐴 +ℎ 𝐵)}) ⊆ (span‘{𝐴, 𝐵}))
Theorem	h1datomi 28568	A 1-dimensional subspace is an atom. (Contributed by NM, 20-Jul-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ⊆ (⊥‘(⊥‘{𝐵})) → (𝐴 = (⊥‘(⊥‘{𝐵})) ∨ 𝐴 = 0ℋ))
Theorem	h1datom 28569	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 28570*	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 28577 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
⊢ 𝐶ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 = ((𝑥 ∩ 𝑦) ∨ℋ (𝑥 ∩ (⊥‘𝑦))))}
Theorem	cmbr 28571	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 28572	Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵)
Theorem	pjoml3i 28573	Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵)
Theorem	pjoml4i 28574	Variation of orthomodular law. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∩ ((⊥‘𝐴) ∨ℋ (⊥‘𝐵)))) = (𝐴 ∨ℋ 𝐵)
Theorem	pjoml5i 28575	The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵)
Theorem	pjoml6i 28576*	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 28577	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 28578	Commutation is symmetric. Theorem 3.4 of [Beran] p. 45. (Contributed by NM, 3-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐵 𝐶ℋ 𝐴)
Theorem	cmcmi 28579	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴)
Theorem	cmcm2i 28580	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 28581	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵)
Theorem	cmcm4i 28582	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ (⊥‘𝐵))
Theorem	cmbr2i 28583	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 28584	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    ⇒   ⊢ 𝐵 𝐶ℋ 𝐴
Theorem	cmcm2ii 28585	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 28586	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    ⇒   ⊢ (⊥‘𝐴) 𝐶ℋ 𝐵
Theorem	cmbr3i 28587	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 28588	Alternate definition for the commutes relation. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) ⊆ 𝐵)
Theorem	lecmi 28589	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 28590	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 28591	A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ (𝐴 ∨ℋ 𝐵)
Theorem	cmj2i 28592	A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐵 𝐶ℋ (𝐴 ∨ℋ 𝐵)
Theorem	cmm1i 28593	A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ (𝐴 ∩ 𝐵)
Theorem	cmm2i 28594	A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐵 𝐶ℋ (𝐴 ∩ 𝐵)
Theorem	cmbr3 28595	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 28596	The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → 0ℋ 𝐶ℋ 𝐴)
Theorem	cmidi 28597	The commutes relation is reflexive. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ 𝐴
Theorem	pjoml2 28598	Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵)
Theorem	pjoml3 28599	Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵))
Theorem	pjoml5 28600	The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵))