P. 295 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29401-29500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fh1i 29401	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 29402	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 29403	Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)) = ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐶))
Theorem	fh4i 29404	Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐵 ∨ℋ (𝐴 ∩ 𝐶)) = ((𝐵 ∨ℋ 𝐴) ∩ (𝐵 ∨ℋ 𝐶))
Theorem	cm2ji 29405	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 29406	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 29407	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 29408	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 29409	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 29410	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 29411	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 29412	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 29413	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 29414	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 29415	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 29416	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 29417*	Lemma for chscl 29421. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶𝐴)
Theorem	chscllem2 29418*	Lemma for chscl 29421. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑣 )
Theorem	chscllem3 29419*	Lemma for chscl 29421. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐹‘𝑁))
Theorem	chscllem4 29420*	Lemma for chscl 29421. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐵)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑢 ∈ (𝐴 +ℋ 𝐵))
Theorem	chscl 29421	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 29422	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 29173, although "the hard part" of this proof, chscl 29421, requires no choice. (Contributed by NM, 28-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ⊆ (⊥‘𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	osumcori 29423	Corollary of osumi 29422. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∩ 𝐵) +ℋ (𝐴 ∩ (⊥‘𝐵))) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵)))
Theorem	osumcor2i 29424	Corollary of osumi 29422, showing it holds under the weaker hypothesis that 𝐴 and 𝐵 commute. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	osum 29425	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 29426	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 29427	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 29428	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 29429	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 29430	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 29431	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 29432	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 29433	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‘{𝐶}))))
19.5.9  Orthoarguesian laws 5OA and 3OA
Theorem	5oalem1 29434	Lemma for orthoarguesian law 5OA. (Contributed by NM, 1-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝑅 ∈ Sℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐶 ∧ (𝑥 −ℎ 𝑧) ∈ 𝑅)) → 𝑣 ∈ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ 𝑅))))
Theorem	5oalem2 29435	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) → (𝑥 −ℎ 𝑧) ∈ ((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)))
Theorem	5oalem3 29436	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    ⇒   ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺))))
Theorem	5oalem4 29437	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    ⇒   ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)))))
Theorem	5oalem5 29438	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 29439	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 29440	Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) TODO: replace uses of ee4anv 2371 with 4exdistrv 1956 as in 3oalem3 29444. (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    &   ⊢ 𝑅 ∈ Sℋ    &   ⊢ 𝑆 ∈ Sℋ    ⇒   ⊢ (((𝐴 +ℋ 𝐵) ∩ (𝐶 +ℋ 𝐷)) ∩ ((𝐹 +ℋ 𝐺) ∩ (𝑅 +ℋ 𝑆))) ⊆ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))))))))
Theorem	5oai 29441	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 29442*	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)))
Theorem	3oalem2 29443*	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))))
Theorem	3oalem3 29444	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) ⊆ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))
Theorem	3oalem4 29445	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    ⇒   ⊢ 𝑅 ⊆ (⊥‘𝐵)
Theorem	3oalem5 29446	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    &   ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴))    ⇒   ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) = ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆))
Theorem	3oalem6 29447	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    &   ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴))    ⇒   ⊢ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆)))))
Theorem	3oai 29448	3OA (weak) orthoarguesian law. Equation IV of [GodowskiGreechie] p. 249. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    &   ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴))    ⇒   ⊢ ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆)) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆)))))
19.5.10  Projectors (cont.)
Theorem	pjorthi 29449	Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐻 ∈ Cℋ → (((projℎ‘𝐻)‘𝐴) ·ih ((projℎ‘(⊥‘𝐻))‘𝐵)) = 0)
Theorem	pjch1 29450	Property of identity projection. Remark in [Beran] p. 111. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((projℎ‘ ℋ)‘𝐴) = 𝐴)
Theorem	pjo 29451	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 29452	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 29453	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 29454	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 29455	Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵))
Theorem	pjinormii 29456	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 29457	Projection of (scalar) product is product of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐶 ·ℎ 𝐴)) = (𝐶 ·ℎ ((projℎ‘𝐻)‘𝐴))
Theorem	pjsubii 29458	Projection of vector difference is difference of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵))
Theorem	pjsslem 29459	Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ ((projℎ‘(⊥‘𝐺))‘𝐴)) = (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴))
Theorem	pjss2i 29460	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 29461	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 29462	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 29463	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 29464	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 29465	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 29466	Projection of vector sum is sum of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjinormi 29467	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 29468	Projection of vector difference is difference of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjmuli 29469	Projection of scalar product is scalar product of projection. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjige0i 29470	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 29471	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 29472	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 29473	The projection of the zero vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐻)‘0ℎ) = 0ℎ
Theorem	pjch 29474	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 29475	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 29476*	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 29477*	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 29478	Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘(𝐺 ∩ 𝐻)) → ((projℎ‘𝐺)‘𝐴) ∈ (⊥‘(𝐺 ∩ 𝐻)))
Theorem	pjini 29479	Membership of projection in an intersection. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ (𝐺 ∩ 𝐻) → ((projℎ‘𝐺)‘𝐴) ∈ (𝐺 ∩ 𝐻))
Theorem	pjjsi 29480*	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 29481	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 29482	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 29483	A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻): ℋ–onto→𝐻
Theorem	pjfi 29484	The mapping of a projection. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻): ℋ⟶ ℋ
Theorem	pjvi 29485	The value of a projection in terms of components. (Contributed by NM, 28-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = 𝐴)
Theorem	pjhfo 29486	A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻): ℋ–onto→𝐻)
Theorem	pjrn 29487	The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → ran (projℎ‘𝐻) = 𝐻)
Theorem	pjhf 29488	The mapping of a projection. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻): ℋ⟶ ℋ)
Theorem	pjfn 29489	Functionality of a projection. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) Fn ℋ)
Theorem	pjsumi 29490	The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ ℋ → (𝐺 ⊆ (⊥‘𝐻) → ((projℎ‘(𝐺 +ℋ 𝐻))‘𝐴) = (((projℎ‘𝐺)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐴))))
Theorem	pj11i 29491	One-to-one correspondence of projection and subspace. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐺) = (projℎ‘𝐻) ↔ 𝐺 = 𝐻)
Theorem	pjdsi 29492	Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 21-Jun-2006.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ (𝐺 ∨ℋ 𝐻) ∧ 𝐺 ⊆ (⊥‘𝐻)) → 𝐴 = (((projℎ‘𝐺)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐴)))
Theorem	pjds3i 29493	Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.)
⊢ 𝐹 ∈ Cℋ    &   ⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (((𝐴 ∈ ((𝐹 ∨ℋ 𝐺) ∨ℋ 𝐻) ∧ 𝐹 ⊆ (⊥‘𝐺)) ∧ (𝐹 ⊆ (⊥‘𝐻) ∧ 𝐺 ⊆ (⊥‘𝐻))) → 𝐴 = ((((projℎ‘𝐹)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴)) +ℎ ((projℎ‘𝐻)‘𝐴)))
Theorem	pj11 29494	One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ ((𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ) → ((projℎ‘𝐺) = (projℎ‘𝐻) ↔ 𝐺 = 𝐻))
Theorem	pjmfn 29495	Functionality of the projection function. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ projℎ Fn Cℋ
Theorem	pjmf1 29496	The projector function maps one-to-one into the set of Hilbert space operators. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ projℎ: Cℋ –1-1→( ℋ ↑m ℋ)
Theorem	pjoi0 29497	The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ (((𝐺 ∈ Cℋ ∧ 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) ∧ 𝐺 ⊆ (⊥‘𝐻)) → (((projℎ‘𝐺)‘𝐴) ·ih ((projℎ‘𝐻)‘𝐴)) = 0)
Theorem	pjoi0i 29498	The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (𝐺 ⊆ (⊥‘𝐻) → (((projℎ‘𝐺)‘𝐴) ·ih ((projℎ‘𝐻)‘𝐴)) = 0)
Theorem	pjopythi 29499	Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (𝐺 ⊆ (⊥‘𝐻) → ((normℎ‘(((projℎ‘𝐺)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐴)))↑2) = (((normℎ‘((projℎ‘𝐺)‘𝐴))↑2) + ((normℎ‘((projℎ‘𝐻)‘𝐴))↑2)))
Theorem	pjopyth 29500	Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐻 ∈ Cℋ ∧ 𝐺 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐻 ⊆ (⊥‘𝐺) → ((normℎ‘(((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐺)‘𝐴)))↑2) = (((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) + ((normℎ‘((projℎ‘𝐺)‘𝐴))↑2))))