P. 316 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31501-31600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	spansncol 31501	The singletons of collinear vectors have the same span. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (span‘{(𝐵 ·ℎ 𝐴)}) = (span‘{𝐴}))
Theorem	spansneleqi 31502	Membership relation implied by equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((span‘{𝐴}) = (span‘{𝐵}) → 𝐴 ∈ (span‘{𝐵})))
Theorem	spansneleq 31503	Membership relation that implies equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (𝐴 ∈ (span‘{𝐵}) → (span‘{𝐴}) = (span‘{𝐵})))
Theorem	spansnss 31504	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 31505	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 31506	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 31507	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 31508	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 31509	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 31510	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 31511	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 31512	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 31513	The span of a pair of vectors. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (span‘{(𝐴 +ℎ 𝐵)}) ⊆ (span‘{𝐴, 𝐵}))
Theorem	h1datomi 31514	A 1-dimensional subspace is an atom. (Contributed by NM, 20-Jul-2001.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ⊆ (⊥‘(⊥‘{𝐵})) → (𝐴 = (⊥‘(⊥‘{𝐵})) ∨ 𝐴 = 0ℋ))
Theorem	h1datom 31515	A 1-dimensional subspace is an atom. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ⊆ (⊥‘(⊥‘{𝐵})) → (𝐴 = (⊥‘(⊥‘{𝐵})) ∨ 𝐴 = 0ℋ)))
20.5.5  Commutes relation for Hilbert lattice elements
Definition	df-cm 31516*	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 31523 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
⊢ 𝐶ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 = ((𝑥 ∩ 𝑦) ∨ℋ (𝑥 ∩ (⊥‘𝑦))))}
Theorem	cmbr 31517	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 31518	Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵)
Theorem	pjoml3i 31519	Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵)
Theorem	pjoml4i 31520	Variation of orthomodular law. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∩ ((⊥‘𝐴) ∨ℋ (⊥‘𝐵)))) = (𝐴 ∨ℋ 𝐵)
Theorem	pjoml5i 31521	The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵)
Theorem	pjoml6i 31522*	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 31523	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 31524	Commutation is symmetric. Theorem 3.4 of [Beran] p. 45. (Contributed by NM, 3-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐵 𝐶ℋ 𝐴)
Theorem	cmcmi 31525	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴)
Theorem	cmcm2i 31526	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 31527	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵)
Theorem	cmcm4i 31528	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ (⊥‘𝐵))
Theorem	cmbr2i 31529	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 31530	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    ⇒   ⊢ 𝐵 𝐶ℋ 𝐴
Theorem	cmcm2ii 31531	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 31532	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    ⇒   ⊢ (⊥‘𝐴) 𝐶ℋ 𝐵
Theorem	cmbr3i 31533	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 31534	Alternate definition for the commutes relation. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) ⊆ 𝐵)
Theorem	lecmi 31535	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 31536	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 31537	A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ (𝐴 ∨ℋ 𝐵)
Theorem	cmj2i 31538	A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐵 𝐶ℋ (𝐴 ∨ℋ 𝐵)
Theorem	cmm1i 31539	A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ (𝐴 ∩ 𝐵)
Theorem	cmm2i 31540	A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ 𝐵 𝐶ℋ (𝐴 ∩ 𝐵)
Theorem	cmbr3 31541	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 31542	The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ Cℋ → 0ℋ 𝐶ℋ 𝐴)
Theorem	cmidi 31543	The commutes relation is reflexive. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    ⇒   ⊢ 𝐴 𝐶ℋ 𝐴
Theorem	pjoml2 31544	Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵)
Theorem	pjoml3 31545	Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵))
Theorem	pjoml5 31546	The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵))
Theorem	cmcm 31547	Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴))
Theorem	cmcm3 31548	Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵))
Theorem	cmcm2 31549	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 31550	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 31551	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 31552	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 31553	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 31554	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 31555	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 31556	Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)) = ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐶))
Theorem	fh4i 31557	Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝐴 𝐶ℋ 𝐵    &   ⊢ 𝐴 𝐶ℋ 𝐶    ⇒   ⊢ (𝐵 ∨ℋ (𝐴 ∩ 𝐶)) = ((𝐵 ∨ℋ 𝐴) ∩ (𝐵 ∨ℋ 𝐶))
Theorem	cm2ji 31558	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 31559	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 31560	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 31561	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 31562	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 31563	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 31564	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 31565	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 31566	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 31567	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 31568	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 31569	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 31570*	Lemma for chscl 31574. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶𝐴)
Theorem	chscllem2 31571*	Lemma for chscl 31574. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑣 )
Theorem	chscllem3 31572*	Lemma for chscl 31574. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐹‘𝑁))
Theorem	chscllem4 31573*	Lemma for chscl 31574. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ∈ Cℋ )    &   ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴))    &   ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵))    &   ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐵)‘(𝐻‘𝑛)))    ⇒   ⊢ (𝜑 → 𝑢 ∈ (𝐴 +ℋ 𝐵))
Theorem	chscl 31574	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 31575	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 31326, although "the hard part" of this proof, chscl 31574, requires no choice. (Contributed by NM, 28-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 ⊆ (⊥‘𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	osumcori 31576	Corollary of osumi 31575. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ ((𝐴 ∩ 𝐵) +ℋ (𝐴 ∩ (⊥‘𝐵))) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵)))
Theorem	osumcor2i 31577	Corollary of osumi 31575, showing it holds under the weaker hypothesis that 𝐴 and 𝐵 commute. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    ⇒   ⊢ (𝐴 𝐶ℋ 𝐵 → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵))
Theorem	osum 31578	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 31579	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 31580	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 31581	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 31582	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 31583	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 31584	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 31585	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 31586	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 31587	Lemma for orthoarguesian law 5OA. (Contributed by NM, 1-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝑅 ∈ Sℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐶 ∧ (𝑥 −ℎ 𝑧) ∈ 𝑅)) → 𝑣 ∈ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ 𝑅))))
Theorem	5oalem2 31588	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) → (𝑥 −ℎ 𝑧) ∈ ((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)))
Theorem	5oalem3 31589	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    ⇒   ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺))))
Theorem	5oalem4 31590	Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    ⇒   ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)))))
Theorem	5oalem5 31591	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 31592	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 31593	Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) TODO: replace uses of ee4anv 2342 with 4exdistrv 1953 as in 3oalem3 31597. (New usage is discouraged.)
⊢ 𝐴 ∈ Sℋ    &   ⊢ 𝐵 ∈ Sℋ    &   ⊢ 𝐶 ∈ Sℋ    &   ⊢ 𝐷 ∈ Sℋ    &   ⊢ 𝐹 ∈ Sℋ    &   ⊢ 𝐺 ∈ Sℋ    &   ⊢ 𝑅 ∈ Sℋ    &   ⊢ 𝑆 ∈ Sℋ    ⇒   ⊢ (((𝐴 +ℋ 𝐵) ∩ (𝐶 +ℋ 𝐷)) ∩ ((𝐹 +ℋ 𝐺) ∩ (𝑅 +ℋ 𝑆))) ⊆ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))))))))
Theorem	5oai 31594	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 31595*	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)))
Theorem	3oalem2 31596*	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))))
Theorem	3oalem3 31597	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 ∈ Cℋ    &   ⊢ 𝑆 ∈ Cℋ    ⇒   ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) ⊆ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))
Theorem	3oalem4 31598	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    ⇒   ⊢ 𝑅 ⊆ (⊥‘𝐵)
Theorem	3oalem5 31599	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    &   ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴))    ⇒   ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) = ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆))
Theorem	3oalem6 31600	Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ Cℋ    &   ⊢ 𝐵 ∈ Cℋ    &   ⊢ 𝐶 ∈ Cℋ    &   ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴))    &   ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴))    ⇒   ⊢ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆)))))