P. 318 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31701-31800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cmj2i 31701	A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐵 𝐶ℋ (𝐴 ∨ℋ 𝐵)
Theorem	cmm1i 31702	A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ (𝐴 ∩ 𝐵)
Theorem	cmm2i 31703	A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐵 𝐶ℋ (𝐴 ∩ 𝐵)
Theorem	cmbr3 31704	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 31705	The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → 0ℋ 𝐶ℋ 𝐴)
Theorem	cmidi 31706	The commutes relation is reflexive. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ 𝐴
Theorem	pjoml2 31707	Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵)
Theorem	pjoml3 31708	Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵))
Theorem	pjoml5 31709	The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵))
Theorem	cmcm 31710	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴))
Theorem	cmcm3 31711	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵))
Theorem	cmcm2 31712	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 31713	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ℋ ∧ 𝐴 ⊆ 𝐵) → 𝐴 𝐶ℋ 𝐵)
20.5.6  Foulis-Holland theorem
Theorem	fh1 31714	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 31715	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 31716	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 31717	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 31718	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 31719	Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)) = ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐶))
Theorem	fh4i 31720	Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐵 ∨ℋ (𝐴 ∩ 𝐶)) = ((𝐵 ∨ℋ 𝐴) ∩ (𝐵 ∨ℋ 𝐶))
Theorem	cm2ji 31721	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 31722	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ℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ 𝐴 𝐶ℋ (𝐵 ∩ 𝐶)
20.5.7  Quantum Logic Explorer axioms
Theorem	qlax1i 31723	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 31724	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 31725	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 31726	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 31727	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 31728	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 31729	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 31730	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 31731	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 31732	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ℋ    &   ⊢ (𝐶 ∨ℋ (⊥‘𝐶)) = ((⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) ∨ℋ (⊥‘(𝐴 ∨ℋ 𝐵)))    ⇒   ⊢ 𝐴 = 𝐵
20.5.8  Orthogonal subspaces
Theorem	chscllem1 31733*	Lemma for chscl 31737. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶𝐴)
Theorem	chscllem2 31734*	Lemma for chscl 31737. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑣 )
Theorem	chscllem3 31735*	Lemma for chscl 31737. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐹‘𝑁))
Theorem	chscllem4 31736*	Lemma for chscl 31737. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐵)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑢 ∈ (𝐴 +ℋ 𝐵))
Theorem	chscl 31737	The subspace sum of two closed orthogonal spaces is closed. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    ⇒   ⊢ (𝜑 → (𝐴 +ℋ 𝐵) ∈ Cℋ )
Theorem	osumi 31738	If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of [Kalmbach] p. 67. Note that the (countable) Axiom of Choice is used for this proof via pjhth 31489, although "the hard part" of this proof, chscl 31737, requires no choice. (Contributed by NM, 28-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ⊆ (⊥‘𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	osumcori 31739	Corollary of osumi 31738. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∩ 𝐵) +ℋ (𝐴 ∩ (⊥‘𝐵))) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵)))
Theorem	osumcor2i 31740	Corollary of osumi 31738, showing it holds under the weaker hypothesis that 𝐴 and 𝐵 commute. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	osum 31741	If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of [Kalmbach] p. 67. (Contributed by NM, 31-Oct-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵)) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	spansnji 31742	The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Proof suggested by Eric Schechter 1-Jun-2004.) (Contributed by NM, 1-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 +ℋ (span‘{𝐵})) = (𝐴 ∨ℋ (span‘{𝐵}))
Theorem	spansnj 31743	The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℋ (span‘{𝐵})) = (𝐴 ∨ℋ (span‘{𝐵})))
Theorem	spansnscl 31744	The subspace sum of a closed subspace and a one-dimensional subspace is closed. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℋ (span‘{𝐵})) ∈ Cℋ )
Theorem	sumspansn 31745	The sum of two vectors belong to the span of one of them iff the other vector also belongs. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) ∈ (span‘{𝐴}) ↔ 𝐵 ∈ (span‘{𝐴})))
Theorem	spansnm0i 31746	The meet of different one-dimensional subspaces is the zero subspace. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (¬ 𝐴 ∈ (span‘{𝐵}) → ((span‘{𝐴}) ∩ (span‘{𝐵})) = 0ℋ)
Theorem	nonbooli 31747	A Hilbert lattice with two or more dimensions fails the distributive law and therefore cannot be a Boolean algebra. This counterexample demonstrates a condition where ((𝐻 ∩ 𝐹) ∨ℋ (𝐻 ∩ 𝐺)) = 0ℋ but (𝐻 ∩ (𝐹 ∨ℋ 𝐺)) ≠ 0ℋ. The antecedent specifies that the vectors 𝐴 and 𝐵 are nonzero and non-colinear. The last three hypotheses assign one-dimensional subspaces to 𝐹, 𝐺, and 𝐻. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐹 = (span‘{𝐴})    &   ⊢ 𝐺 = (span‘{𝐵})    &   ⊢ 𝐻 = (span‘{(𝐴 +ℎ 𝐵)})    ⇒   ⊢ (¬ (𝐴 ∈ 𝐺 ∨ 𝐵 ∈ 𝐹) → (𝐻 ∩ (𝐹 ∨ℋ 𝐺)) ≠ ((𝐻 ∩ 𝐹) ∨ℋ (𝐻 ∩ 𝐺)))
Theorem	spansncvi 31748	Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → 𝐵 = (𝐴 ∨ℋ (span‘{𝐶})))
Theorem	spansncv 31749	Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → 𝐵 = (𝐴 ∨ℋ (span‘{𝐶}))))
20.5.9  Orthoarguesian laws 5OA and 3OA
Theorem	5oalem1 31750	Lemma for orthoarguesian law 5OA. (Contributed by NM, 1-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝑅 ∈ Sℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐶 ∧ (𝑥 −ℎ 𝑧) ∈ 𝑅)) → 𝑣 ∈ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ 𝑅))))
Theorem	5oalem2 31751	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) → (𝑥 −ℎ 𝑧) ∈ ((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)))
Theorem	5oalem3 31752	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    ⇒   ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺))))
Theorem	5oalem4 31753	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    ⇒   ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)))))
Theorem	5oalem5 31754	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-May-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    &   ⊢ 𝑅 ∈ Sℋ    &   ⊢ 𝑆 ∈ Sℋ    ⇒   ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺) ∧ (𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆))) ∧ (((𝑥 +ℎ 𝑦) = (𝑣 +ℎ 𝑢) ∧ (𝑧 +ℎ 𝑤) = (𝑣 +ℎ 𝑢)) ∧ (𝑓 +ℎ 𝑔) = (𝑣 +ℎ 𝑢))) → (𝑥 −ℎ 𝑧) ∈ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))))))
Theorem	5oalem6 31755	Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    &   ⊢ 𝑅 ∈ Sℋ    &   ⊢ 𝑆 ∈ Sℋ    ⇒   ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ℎ = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷) ∧ ℎ = (𝑧 +ℎ 𝑤))) ∧ (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺) ∧ ℎ = (𝑓 +ℎ 𝑔)) ∧ ((𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆) ∧ ℎ = (𝑣 +ℎ 𝑢)))) → ℎ ∈ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆))))))))))
Theorem	5oalem7 31756	Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) TODO: replace uses of ee4anv 2359 with 4exdistrv 1963 as in 3oalem3 31760. (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    &   ⊢ 𝑅 ∈ Sℋ    &   ⊢ 𝑆 ∈ Sℋ    ⇒   ⊢ (((𝐴 +ℋ 𝐵) ∩ (𝐶 +ℋ 𝐷)) ∩ ((𝐹 +ℋ 𝐺) ∩ (𝑅 +ℋ 𝑆))) ⊆ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))))))))
Theorem	5oai 31757	Orthoarguesian law 5OA. This 8-variable inference is called 5OA because it can be converted to a 5-variable equation (see Quantum Logic Explorer). (Contributed by NM, 5-May-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐷 ∈ Cℋ    &   ⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    &   ⊢ 𝐴 ⊆ (⊥‘𝐵)    &   ⊢ 𝐶 ⊆ (⊥‘𝐷)    &   ⊢ 𝐹 ⊆ (⊥‘𝐺)    &   ⊢ 𝑅 ⊆ (⊥‘𝑆)    ⇒   ⊢ (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ ((𝐹 ∨ℋ 𝐺) ∩ (𝑅 ∨ℋ 𝑆))) ⊆ (𝐵 ∨ℋ (𝐴 ∩ (𝐶 ∨ℋ ((((𝐴 ∨ℋ 𝐶) ∩ (𝐵 ∨ℋ 𝐷)) ∩ (((𝐴 ∨ℋ 𝑅) ∩ (𝐵 ∨ℋ 𝑆)) ∨ℋ ((𝐶 ∨ℋ 𝑅) ∩ (𝐷 ∨ℋ 𝑆)))) ∩ ((((𝐴 ∨ℋ 𝐹) ∩ (𝐵 ∨ℋ 𝐺)) ∩ (((𝐴 ∨ℋ 𝑅) ∩ (𝐵 ∨ℋ 𝑆)) ∨ℋ ((𝐹 ∨ℋ 𝑅) ∩ (𝐺 ∨ℋ 𝑆)))) ∨ℋ (((𝐶 ∨ℋ 𝐹) ∩ (𝐷 ∨ℋ 𝐺)) ∩ (((𝐶 ∨ℋ 𝑅) ∩ (𝐷 ∨ℋ 𝑆)) ∨ℋ ((𝐹 ∨ℋ 𝑅) ∩ (𝐺 ∨ℋ 𝑆)))))))))
Theorem	3oalem1 31758*	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)))
Theorem	3oalem2 31759*	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))))
Theorem	3oalem3 31760	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) ⊆ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))
Theorem	3oalem4 31761	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    ⇒   ⊢ 𝑅 ⊆ (⊥‘𝐵)
Theorem	3oalem5 31762	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    &   ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴))    ⇒   ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) = ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆))
Theorem	3oalem6 31763	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    &   ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴))    ⇒   ⊢ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆)))))
Theorem	3oai 31764	3OA (weak) orthoarguesian law. Equation IV of [GodowskiGreechie] p. 249. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    &   ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴))    ⇒   ⊢ ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆)) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆)))))
20.5.10  Projectors (cont.)
Theorem	pjorthi 31765	Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐻 ∈ Cℋ → (((projℎ‘𝐻)‘𝐴) ·ih ((projℎ‘(⊥‘𝐻))‘𝐵)) = 0)
Theorem	pjch1 31766	Property of identity projection. Remark in [Beran] p. 111. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((projℎ‘ ℋ)‘𝐴) = 𝐴)
Theorem	pjo 31767	The orthogonal projection. Lemma 4.4(i) of [Beran] p. 111. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘𝐻))‘𝐴) = (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)))
Theorem	pjcompi 31768	Component of a projection. (Contributed by NM, 31-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = 𝐴)
Theorem	pjidmi 31769	A projection is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘((projℎ‘𝐻)‘𝐴)) = ((projℎ‘𝐻)‘𝐴)
Theorem	pjadjii 31770	A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (((projℎ‘𝐻)‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((projℎ‘𝐻)‘𝐵))
Theorem	pjaddii 31771	Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵))
Theorem	pjinormii 31772	The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (((projℎ‘𝐻)‘𝐴) ·ih 𝐴) = ((normℎ‘((projℎ‘𝐻)‘𝐴))↑2)
Theorem	pjmulii 31773	Projection of (scalar) product is product of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐶 ·ℎ 𝐴)) = (𝐶 ·ℎ ((projℎ‘𝐻)‘𝐴))
Theorem	pjsubii 31774	Projection of vector difference is difference of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵))
Theorem	pjsslem 31775	Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ ((projℎ‘(⊥‘𝐺))‘𝐴)) = (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴))
Theorem	pjss2i 31776	Subset relationship for projections. Theorem 4.5(i)->(ii) of [Beran] p. 112. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (𝐻 ⊆ 𝐺 → ((projℎ‘𝐻)‘((projℎ‘𝐺)‘𝐴)) = ((projℎ‘𝐻)‘𝐴))
Theorem	pjssmii 31777	Projection meet property. Remark in [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (𝐻 ⊆ 𝐺 → (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴))
Theorem	pjssge0ii 31778	Theorem 4.5(iv)->(v) of [Beran] p. 112. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) → 0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴))
Theorem	pjdifnormii 31779	Theorem 4.5(v)<->(vi) of [Beran] p. 112. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴) ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) ≤ (normℎ‘((projℎ‘𝐺)‘𝐴)))
Theorem	pjcji 31780	The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (𝐻 ⊆ (⊥‘𝐺) → ((projℎ‘(𝐻 ∨ℋ 𝐺))‘𝐴) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴)))
Theorem	pjadji 31781	A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (((projℎ‘𝐻)‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((projℎ‘𝐻)‘𝐵)))
Theorem	pjaddi 31782	Projection of vector sum is sum of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjinormi 31783	The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐻)‘𝐴) ·ih 𝐴) = ((normℎ‘((projℎ‘𝐻)‘𝐴))↑2))
Theorem	pjsubi 31784	Projection of vector difference is difference of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjmuli 31785	Projection of scalar product is scalar product of projection. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjige0i 31786	The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → 0 ≤ (((projℎ‘𝐻)‘𝐴) ·ih 𝐴))
Theorem	pjige0 31787	The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → 0 ≤ (((projℎ‘𝐻)‘𝐴) ·ih 𝐴))
Theorem	pjcjt2 31788	The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐺 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐻 ⊆ (⊥‘𝐺) → ((projℎ‘(𝐻 ∨ℋ 𝐺))‘𝐴) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴))))
Theorem	pj0i 31789	The projection of the zero vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐻)‘0ℎ) = 0ℎ
Theorem	pjch 31790	Projection of a vector in the projection subspace. Lemma 4.4(ii) of [Beran] p. 111. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ 𝐻 ↔ ((projℎ‘𝐻)‘𝐴) = 𝐴))
Theorem	pjid 31791	The projection of a vector in the projection subspace is itself. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ 𝐻) → ((projℎ‘𝐻)‘𝐴) = 𝐴)
Theorem	pjvec 31792*	The set of vectors belonging to the subspace of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → 𝐻 = {𝑥 ∈ ℋ ∣ ((projℎ‘𝐻)‘𝑥) = 𝑥})
Theorem	pjocvec 31793*	The set of vectors belonging to the orthocomplemented subspace of a projection. Second part of Theorem 27.3 of [Halmos] p. 45. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (⊥‘𝐻) = {𝑥 ∈ ℋ ∣ ((projℎ‘𝐻)‘𝑥) = 0ℎ})
Theorem	pjocini 31794	Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘(𝐺 ∩ 𝐻)) → ((projℎ‘𝐺)‘𝐴) ∈ (⊥‘(𝐺 ∩ 𝐻)))
Theorem	pjini 31795	Membership of projection in an intersection. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ (𝐺 ∩ 𝐻) → ((projℎ‘𝐺)‘𝐴) ∈ (𝐺 ∩ 𝐻))
Theorem	pjjsi 31796*	A sufficient condition for subspace join to be equal to subspace sum. (Contributed by NM, 29-May-2004.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Sℋ    ⇒   ⊢ (∀𝑥 ∈ (𝐺 ∨ℋ 𝐻)((projℎ‘(⊥‘𝐺))‘𝑥) ∈ 𝐻 → (𝐺 ∨ℋ 𝐻) = (𝐺 +ℋ 𝐻))
Theorem	pjfni 31797	Functionality of a projection. (Contributed by NM, 30-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻) Fn ℋ
Theorem	pjrni 31798	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 30-Oct-1999.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ran (projℎ‘𝐻) = 𝐻
Theorem	pjfoi 31799	A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻): ℋ–onto→𝐻
Theorem	pjfi 31800	The mapping of a projection. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻): ℋ⟶ ℋ