P. 322 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32101-32200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pjoml3 32101	Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵))
Theorem	pjoml5 32102	The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵))
Theorem	cmcm 32103	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴))
Theorem	cmcm3 32104	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵))
Theorem	cmcm2 32105	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 32106	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 32107	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 32108	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 32109	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 32110	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 32111	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 32112	Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)) = ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐶))
Theorem	fh4i 32113	Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐵 ∨ℋ (𝐴 ∩ 𝐶)) = ((𝐵 ∨ℋ 𝐴) ∩ (𝐵 ∨ℋ 𝐶))
Theorem	cm2ji 32114	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 32115	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 32116	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 32117	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 32118	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 32119	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 32120	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 32121	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 32122	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 32123	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 32124	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 32125	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 32126*	Lemma for chscl 32130. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶𝐴)
Theorem	chscllem2 32127*	Lemma for chscl 32130. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑣 )
Theorem	chscllem3 32128*	Lemma for chscl 32130. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐹‘𝑁))
Theorem	chscllem4 32129*	Lemma for chscl 32130. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐵)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑢 ∈ (𝐴 +ℋ 𝐵))
Theorem	chscl 32130	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 32131	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 31882, although "the hard part" of this proof, chscl 32130, requires no choice. (Contributed by NM, 28-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ⊆ (⊥‘𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	osumcori 32132	Corollary of osumi 32131. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∩ 𝐵) +ℋ (𝐴 ∩ (⊥‘𝐵))) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵)))
Theorem	osumcor2i 32133	Corollary of osumi 32131, showing it holds under the weaker hypothesis that 𝐴 and 𝐵 commute. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	osum 32134	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 32135	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 32136	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 32137	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 32138	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 32139	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 32140	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 32141	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 32142	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 32143	Lemma for orthoarguesian law 5OA. (Contributed by NM, 1-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝑅 ∈ Sℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐶 ∧ (𝑥 −ℎ 𝑧) ∈ 𝑅)) → 𝑣 ∈ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ 𝑅))))
Theorem	5oalem2 32144	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) → (𝑥 −ℎ 𝑧) ∈ ((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)))
Theorem	5oalem3 32145	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    ⇒   ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺))))
Theorem	5oalem4 32146	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    ⇒   ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)))))
Theorem	5oalem5 32147	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 32148	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 32149	Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) TODO: replace uses of ee4anv 2382 with 4exdistrv 1989 as in 3oalem3 32153. (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    &   ⊢ 𝑅 ∈ Sℋ    &   ⊢ 𝑆 ∈ Sℋ    ⇒   ⊢ (((𝐴 +ℋ 𝐵) ∩ (𝐶 +ℋ 𝐷)) ∩ ((𝐹 +ℋ 𝐺) ∩ (𝑅 +ℋ 𝑆))) ⊆ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))))))))
Theorem	5oai 32150	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 32151*	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)))
Theorem	3oalem2 32152*	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))))
Theorem	3oalem3 32153	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) ⊆ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))
Theorem	3oalem4 32154	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    ⇒   ⊢ 𝑅 ⊆ (⊥‘𝐵)
Theorem	3oalem5 32155	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    &   ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴))    ⇒   ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) = ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆))
Theorem	3oalem6 32156	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    &   ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴))    ⇒   ⊢ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆)))))
Theorem	3oai 32157	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 32158	Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐻 ∈ Cℋ → (((projℎ‘𝐻)‘𝐴) ·ih ((projℎ‘(⊥‘𝐻))‘𝐵)) = 0)
Theorem	pjch1 32159	Property of identity projection. Remark in [Beran] p. 111. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((projℎ‘ ℋ)‘𝐴) = 𝐴)
Theorem	pjo 32160	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 32161	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 32162	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 32163	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 32164	Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵))
Theorem	pjinormii 32165	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 32166	Projection of (scalar) product is product of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐶 ·ℎ 𝐴)) = (𝐶 ·ℎ ((projℎ‘𝐻)‘𝐴))
Theorem	pjsubii 32167	Projection of vector difference is difference of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵))
Theorem	pjsslem 32168	Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    &   ⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐺 ∈ Cℋ    ⇒   ⊢ (((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ ((projℎ‘(⊥‘𝐺))‘𝐴)) = (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴))
Theorem	pjss2i 32169	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 32170	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 32171	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 32172	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 32173	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 32174	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 32175	Projection of vector sum is sum of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjinormi 32176	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 32177	Projection of vector difference is difference of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjmuli 32178	Projection of scalar product is scalar product of projection. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((projℎ‘𝐻)‘(𝐴 ·ℎ 𝐵)) = (𝐴 ·ℎ ((projℎ‘𝐻)‘𝐵)))
Theorem	pjige0i 32179	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 32180	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 32181	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 32182	The projection of the zero vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐻)‘0ℎ) = 0ℎ
Theorem	pjch 32183	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 32184	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 32185*	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 32186*	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 32187	Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ (⊥‘(𝐺 ∩ 𝐻)) → ((projℎ‘𝐺)‘𝐴) ∈ (⊥‘(𝐺 ∩ 𝐻)))
Theorem	pjini 32188	Membership of projection in an intersection. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (𝐴 ∈ (𝐺 ∩ 𝐻) → ((projℎ‘𝐺)‘𝐴) ∈ (𝐺 ∩ 𝐻))
Theorem	pjjsi 32189*	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 32190	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 32191	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 32192	A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻): ℋ–onto→𝐻
Theorem	pjfi 32193	The mapping of a projection. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ (projℎ‘𝐻): ℋ⟶ ℋ
Theorem	pjvi 32194	The value of a projection in terms of components. (Contributed by NM, 28-Nov-2000.) (New usage is discouraged.)
⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = 𝐴)
Theorem	pjhfo 32195	A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻): ℋ–onto→𝐻)
Theorem	pjrn 32196	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 32197	The mapping of a projection. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻): ℋ⟶ ℋ)
Theorem	pjfn 32198	Functionality of a projection. (Contributed by NM, 30-May-2006.) (New usage is discouraged.)
⊢ (𝐻 ∈ Cℋ → (projℎ‘𝐻) Fn ℋ)
Theorem	pjsumi 32199	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 32200	One-to-one correspondence of projection and subspace. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.)
⊢ 𝐺 ∈ Cℋ    &   ⊢ 𝐻 ∈ Cℋ    ⇒   ⊢ ((projℎ‘𝐺) = (projℎ‘𝐻) ↔ 𝐺 = 𝐻)