Metamath Proof Explorer - mmtheorems55

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 5401-5500 - Page 55 of 58

Type	Label	Description
Statement
Theorem	chdmm4 5401	DeMorgan's law for meet in a Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (⊥ ‘((⊥ ‘A) ∩ (⊥ ‘B))) = (A ∨ℋ B)
Theorem	chdmj1 5402	DeMorgan's law for join in a Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (⊥ ‘(A ∨ℋ B)) = ((⊥ ‘A) ∩ (⊥ ‘B))
Theorem	chdmj2 5403	DeMorgan's law for join in a Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (⊥ ‘((⊥ ‘A) ∨ℋ B)) = (A ∩ (⊥ ‘B))
Theorem	chdmj3 5404	DeMorgan's law for join in a Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (⊥ ‘(A ∨ℋ (⊥ ‘B))) = ((⊥ ‘A) ∩ B)
Theorem	chdmj4 5405	DeMorgan's law for join in a Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (⊥ ‘((⊥ ‘A) ∨ℋ (⊥ ‘B))) = (A ∩ B)
Theorem	chnle 5406	Equivalent expressions for "not less than" in the Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (¬ B ⊆ A ↔ A ⊂ (A ∨ℋ B))
Theorem	chjass 5407	Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ ((A ∨ℋ B) ∨ℋ C) = (A ∨ℋ (B ∨ℋ C))
Theorem	chj00 5408	Two Hilbert lattice elements are zero iff their join is zero.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ ((A = 0ℋ ∧ B = 0ℋ) ↔ (A ∨ℋ B) = 0ℋ)
Theorem	chjo 5409	The join of a closed subspace and its orthocomplement.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ∨ℋ (⊥ ‘A)) = ℋ
Theorem	chj1 5410	Join with Hilbert lattice unit.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ∨ℋ ℋ ) = ℋ
Theorem	chm0 5411	Meet with Hilbert lattice zero.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ∩ 0ℋ) = 0ℋ
Theorem	shjshs 5412	Hilbert lattice join equals the double orthocomplement of subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∨ℋ B) = (⊥ ‘(⊥ ‘(A +ℋ B)))
Theorem	shjshsel 5413	A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of [MaedaMaeda] p. 136.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ ((A +ℋ B) ∈ Cℋ ↔ (A +ℋ B) = (A ∨ℋ B))
Theorem	chj0t 5414	Join with Hilbert lattice zero.
⊢ (A ∈ Cℋ → (A ∨ℋ 0ℋ) = A)
Theorem	chslejt 5415	Subspace sum is smaller than subspace join. Remark of [Kalmbach] p. 65.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A +ℋ B) ⊆ (A ∨ℋ B))
Theorem	chinclt 5416	Closure of Hilbert lattice intersection.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ∩ B) ∈ Cℋ )
Theorem	chsscon3t 5417	Hilbert lattice contraposition law.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⊆ B ↔ (⊥ ‘B) ⊆ (⊥ ‘A)))
Theorem	chsscon1t 5418	Hilbert lattice contraposition law.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → ((⊥ ‘A) ⊆ B ↔ (⊥ ‘B) ⊆ A))
Theorem	chsscon2t 5419	Hilbert lattice contraposition law.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⊆ (⊥ ‘B) ↔ B ⊆ (⊥ ‘A)))
Theorem	chpsscon3t 5420	Hilbert lattice contraposition law for strict ordering.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⊂ B ↔ (⊥ ‘B) ⊂ (⊥ ‘A)))
Theorem	chpsscon1t 5421	Hilbert lattice contraposition law for strict ordering.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → ((⊥ ‘A) ⊂ B ↔ (⊥ ‘B) ⊂ A))
Theorem	chpsscon2t 5422	Hilbert lattice contraposition law for strict ordering.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⊂ (⊥ ‘B) ↔ B ⊂ (⊥ ‘A)))
Theorem	chjcomt 5423	Commutative law for Hilbert lattice join.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ∨ℋ B) = (B ∨ℋ A))
Theorem	chub1t 5424	Hilbert lattice join is greater than or equal to its first argument.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → A ⊆ (A ∨ℋ B))
Theorem	chub2t 5425	Hilbert lattice join is greater than or equal to its second argument.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → A ⊆ (B ∨ℋ A))
Theorem	chlubt 5426	Hilbert lattice join is the least upper bound of two elements.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → ((A ⊆ C ∧ B ⊆ C) ↔ (A ∨ℋ B) ⊆ C))
Theorem	chlej1t 5427	Add join to both sides of Hilbert lattice ordering.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → (A ⊆ B → (A ∨ℋ C) ⊆ (B ∨ℋ C)))
Theorem	chlej2t 5428	Add join to both sides of Hilbert lattice ordering.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → (A ⊆ B → (C ∨ℋ A) ⊆ (C ∨ℋ B)))
Theorem	chlejb1t 5429	Hilbert lattice ordering in terms of join.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⊆ B ↔ (A ∨ℋ B) = B))
Theorem	chlejb2t 5430	Hilbert lattice ordering in terms of join.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ⊆ B ↔ (B ∨ℋ A) = B))
Theorem	chnlet 5431	Equivalent expressions for "not less than" in the Hilbert lattice.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (¬ B ⊆ A ↔ A ⊂ (A ∨ℋ B)))
Theorem	chabs1t 5432	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ∨ℋ (A ∩ B)) = A)
Theorem	chabs2t 5433	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ∩ (A ∨ℋ B)) = A)
Theorem	chabs1 5434	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∨ℋ (A ∩ B)) = A
Theorem	chabs2 5435	Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∩ (A ∨ℋ B)) = A
Theorem	chjidmt 5436	Idempotent law for Hilbert lattice join.
⊢ (A ∈ Cℋ → (A ∨ℋ A) = A)
Theorem	chjidm 5437	Idempotent law for Hilbert lattice join.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ∨ℋ A) = A
Theorem	chdmm1t 5438	DeMorgan's law for meet in a Hilbert lattice.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (⊥ ‘(A ∩ B)) = ((⊥ ‘A) ∨ℋ (⊥ ‘B)))
Theorem	chdmm2t 5439	DeMorgan's law for meet in a Hilbert lattice.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (⊥ ‘((⊥ ‘A) ∩ B)) = (A ∨ℋ (⊥ ‘B)))
Theorem	chdmm3t 5440	DeMorgan's law for meet in a Hilbert lattice.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (⊥ ‘(A ∩ (⊥ ‘B))) = ((⊥ ‘A) ∨ℋ B))
Theorem	chdmm4t 5441	DeMorgan's law for meet in a Hilbert lattice.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (⊥ ‘((⊥ ‘A) ∩ (⊥ ‘B))) = (A ∨ℋ B))
Theorem	chdmj1t 5442	DeMorgan's law for join in a Hilbert lattice.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (⊥ ‘(A ∨ℋ B)) = ((⊥ ‘A) ∩ (⊥ ‘B)))
Theorem	chdmj2t 5443	DeMorgan's law for join in a Hilbert lattice.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (⊥ ‘((⊥ ‘A) ∨ℋ B)) = (A ∩ (⊥ ‘B)))
Theorem	chdmj3t 5444	DeMorgan's law for join in a Hilbert lattice.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (⊥ ‘(A ∨ℋ (⊥ ‘B))) = ((⊥ ‘A) ∩ B))
Theorem	chdmj4t 5445	DeMorgan's law for join in a Hilbert lattice.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (⊥ ‘((⊥ ‘A) ∨ℋ (⊥ ‘B))) = (A ∩ B))
Theorem	chjasst 5446	Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ Cℋ ) → ((A ∨ℋ B) ∨ℋ C) = (A ∨ℋ (B ∨ℋ C)))
Theorem	ledi 5447	An ortholattice is distributive in one ordering direction.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ ((A ∩ B) ∨ℋ (A ∩ C)) ⊆ (A ∩ (B ∨ℋ C))
Theorem	span0 5448	The span of the empty set is the zero subspace. Remark 11.6.e of [Schechter] p. 276.
⊢ (span ‘∅) = 0ℋ
Theorem	elspan 5449	Membership in the span of a subset of Hilbert space.
⊢ B ∈ V    ⇒   ⊢ (A ⊆ ℋ → (B ∈ (span ‘A) ↔ ∀x ∈ Sℋ (A ⊆ x → B ∈ x)))
Theorem	spanun 5450	The span of a union is the subspace sum of spans.
⊢ A ⊆ ℋ    &   ⊢ B ⊆ ℋ    ⇒   ⊢ (span ‘(A ∪ B)) = ((span ‘A) +ℋ (span ‘B))
Theorem	sshhococ 5451	The join of two Hilbert space subsets (not necessarily closed subspaces) equals the join of their closures (double orthocomplements).
⊢ A ⊆ ℋ    &   ⊢ B ⊆ ℋ    ⇒   ⊢ (A ∨ℋ B) = ((⊥ ‘(⊥ ‘A)) ∨ℋ (⊥ ‘(⊥ ‘B)))
Theorem	chne0t 5452	A non-zero closed subspace has a non-zero vector.
⊢ (A ∈ Cℋ → (¬ A = 0ℋ ↔ ∃x ∈ A ¬ x = 0v))
Theorem	chsup0 5453	The supremum of the empty set.
⊢ ( ∨ℋ ‘∅) = 0ℋ
Theorem	h1deot 5454	Membership in orthocomplement of 1-dimensional subspace.
⊢ B ∈ ℋ    ⇒   ⊢ (A ∈ (⊥ ‘{B}) ↔ (A ∈ ℋ ∧ (A ·i B) = 0))
Theorem	h1det 5455	Membership in 1-dimensional subspace.
⊢ B ∈ ℋ    ⇒   ⊢ (A ∈ (⊥ ‘(⊥ ‘{B})) ↔ (A ∈ ℋ ∧ ∀x ∈ ℋ ((B ·i x) = 0 → (A ·i x) = 0)))
Theorem	h1did 5456	A generating vector belongs to the 1-dimensional subspace it generates.
⊢ (A ∈ ℋ → A ∈ (⊥ ‘(⊥ ‘{A})))
Theorem	h1dn0 5457	A non-zero vector generates a (non-zero) 1-dimensional subspace.
⊢ ((A ∈ ℋ ∧ ¬ A = 0v) → ¬ (⊥ ‘(⊥ ‘{A})) = 0ℋ)
Theorem	h1de2 5458	Membership in 1-dimensional subspace. All members are collinear with the generating vector.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (A ∈ (⊥ ‘(⊥ ‘{B})) → ((B ·i B) ·s A) = ((A ·i B) ·s B))
Theorem	h1de2b 5459	Membership in 1-dimensional subspace. All members are collinear with the generating vector.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (¬ B = 0v → (A ∈ (⊥ ‘(⊥ ‘{B})) ↔ A = (((A ·i B) / (B ·i B)) ·s B)))
Theorem	h1de2ctlem 5460	Lemma for h1de2ct 5461.
⊢ A ∈ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (A ∈ (⊥ ‘(⊥ ‘{B})) ↔ ∃x ∈ ℂ A = (x ·s B))
Theorem	h1de2ct 5461	Membership in 1-dimensional subspace. All members are collinear with the generating vector.
⊢ B ∈ ℋ    ⇒   ⊢ (A ∈ (⊥ ‘(⊥ ‘{B})) ↔ ∃x ∈ ℂ A = (x ·s B))
Theorem	spansn 5462	The span of a singleton in Hilbert space equals its closure.
⊢ A ∈ ℋ    ⇒   ⊢ (span ‘{A}) = (⊥ ‘(⊥ ‘{A}))
Theorem	elspansn 5463	Membership in the span of a singleton.
⊢ A ∈ ℋ    ⇒   ⊢ (B ∈ (span ‘{A}) ↔ ∃x ∈ ℂ B = (x ·s A))
Theorem	spansnt 5464	The span of a singleton in Hilbert space equals its closure.
⊢ (A ∈ ℋ → (span ‘{A}) = (⊥ ‘(⊥ ‘{A})))
Theorem	spansncht 5465	The span of a Hilbert space singleton belongs to the Hilbert lattice.
⊢ (A ∈ ℋ → (span ‘{A}) ∈ Cℋ )
Theorem	spansnsht 5466	The span of a Hilbert space singleton is a subspace.
⊢ (A ∈ ℋ → (span ‘{A}) ∈ Sℋ )
Theorem	spansnch 5467	The span of a singleton in Hilbert space is a closed subspace.
⊢ A ∈ ℋ    ⇒   ⊢ (span ‘{A}) ∈ Cℋ
Theorem	spansnid 5468	A vector belongs to the span of its singleton.
⊢ (A ∈ ℋ → A ∈ (span ‘{A}))
Theorem	spansnmul 5469	A scalar product with a vector belongs to the span of its singleton.
⊢ ((A ∈ ℋ ∧ B ∈ ℂ) → (B ·s A) ∈ (span ‘{A}))
Theorem	elspansnclt 5470	A member of a span of a singleton is a vector.
⊢ ((A ∈ ℋ ∧ B ∈ (span ‘{A})) → B ∈ ℋ )
Theorem	elspansnt 5471	Membership in the span of a singleton.
⊢ (A ∈ ℋ → (B ∈ (span ‘{A}) ↔ ∃x ∈ ℂ B = (x ·s A)))
Theorem	elspansn2t 5472	Membership in the span of a singleton. All members are collinear with the generating vector.
⊢ ((A ∈ ℋ ∧ B ∈ ℋ ∧ ¬ B = 0v) → (A ∈ (span ‘{B}) ↔ A = (((A ·i B) / (B ·i B)) ·s B)))
Theorem	spansncol 5473	The singletons of collinear vectors have the same span.
⊢ ((A ∈ ℋ ∧ B ∈ ℂ ∧ B ≠ 0) → (span ‘{(B ·s A)}) = (span ‘{A}))
Theorem	spansneleqi 5474	Membership relation implied by equality of spans.
⊢ (A ∈ ℋ → ((span ‘{A}) = (span ‘{B}) → A ∈ (span ‘{B})))
Theorem	spansneleq 5475	Membership relation that implies equality of spans.
⊢ ((B ∈ ℋ ∧ ¬ A = 0v) → (A ∈ (span ‘{B}) → (span ‘{A}) = (span ‘{B})))
Theorem	spansnsst 5476	The span of the singleton of an element of a subspace is included in the subspace.
⊢ ((A ∈ Sℋ ∧ B ∈ A) → (span ‘{B}) ⊆ A)
Theorem	elspansn3t 5477	A member of the span of the singleton of a vector is a member of a subspace containing the vector.
⊢ (A ∈ Sℋ → ((B ∈ A ∧ C ∈ (span ‘{B})) → C ∈ A))
Theorem	elspansn4t 5478	A span membership condition implying two vectors belong to the same subspace.
⊢ (((A ∈ Sℋ ∧ B ∈ ℋ ) ∧ (C ∈ (span ‘{B}) ∧ ¬ C = 0v)) → (B ∈ A ↔ C ∈ A))
Theorem	elspansn5t 5479	A vector belonging to both a subspace and the span of the singleton of a vector not in it must be zero.
⊢ (A ∈ Sℋ → (((B ∈ ℋ ∧ ¬ B ∈ A) ∧ (C ∈ (span ‘{B}) ∧ C ∈ A)) → C = 0v))
Theorem	spansnss2t 5480	The span of the singleton of an element of a subspace is included in the subspace.
⊢ ((A ∈ Sℋ ∧ B ∈ ℋ ) → (B ∈ A ↔ (span ‘{B}) ⊆ A))
Theorem	spansnpj 5481	A subset of Hilbert space is orthogonal to the span of the singleton of a projection onto its orthocomplement.
⊢ A ⊆ ℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ A ⊆ (⊥ ‘(span ‘{((Proj ‘(⊥ ‘A)) ‘B)}))
Theorem	spanunsn 5482	The span of the union of a closed subspace with a singleton equals the span of its union with an orthogonal singleton.
⊢ A ∈ Cℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (span ‘(A ∪ {B})) = (span ‘(A ∪ {((Proj ‘(⊥ ‘A)) ‘B)}))
Theorem	h1datom 5483	A 1-dimensional subspace is an atom.
⊢ A ∈ Cℋ    &   ⊢ B ∈ ℋ    ⇒   ⊢ (A ⊆ (⊥ ‘(⊥ ‘{B})) → (A = (⊥ ‘(⊥ ‘{B})) ∨ A = 0ℋ))
Theorem	h1datomt 5484	A 1-dimensional subspace is an atom.
⊢ ((A ∈ Cℋ ∧ B ∈ ℋ ) → (A ⊆ (⊥ ‘(⊥ ‘{B})) → (A = (⊥ ‘(⊥ ‘{B})) ∨ A = 0ℋ)))
Definition	df-hosum 5485	Define the sum of two Hilbert space operators. Definition of [Beran] p. 111.
⊢ +P = {⟨⟨f, g⟩, h⟩∣((f: ℋ –→ ℋ ∧ g: ℋ –→ ℋ ) ∧ h = {⟨x, y⟩∣(x ∈ ℋ ∧ y = ((f ‘x) +v (g ‘x)))})}
Definition	df-pjdif 5486	Define the difference of two Hilbert space operators. Definition of [Beran] p. 111.
⊢ −P = {⟨⟨f, g⟩, h⟩∣((f: ℋ –→ ℋ ∧ g: ℋ –→ ℋ ) ∧ h = {⟨x, y⟩∣(x ∈ ℋ ∧ y = ((f ‘x) −v (g ‘x)))})}
Theorem	hosmvalt 5487	Value of sum of two Hilbert space operators.
⊢ ((S: ℋ –→ ℋ ∧ T: ℋ –→ ℋ ) → (S +P T) = {⟨x, y⟩∣(x ∈ ℋ ∧ y = ((S ‘x) +v (T ‘x)))})
Theorem	hodmvalt 5488	Value of difference of two Hilbert space operators.
⊢ ((S: ℋ –→ ℋ ∧ T: ℋ –→ ℋ ) → (S −P T) = {⟨x, y⟩∣(x ∈ ℋ ∧ y = ((S ‘x) −v (T ‘x)))})
Theorem	hosvalt 5489	Value of sum of two Hilbert space operators.
⊢ (((S: ℋ –→ ℋ ∧ T: ℋ –→ ℋ ) ∧ A ∈ ℋ ) → ((S +P T) ‘A) = ((S ‘A) +v (T ‘A)))
Theorem	hodvalt 5490	Value of difference of two Hilbert space operators.
⊢ (((S: ℋ –→ ℋ ∧ T: ℋ –→ ℋ ) ∧ A ∈ ℋ ) → ((S −P T) ‘A) = ((S ‘A) −v (T ‘A)))
Theorem	hosclt 5491	Closure of sum of two Hilbert space operators.
⊢ (((S: ℋ –→ ℋ ∧ T: ℋ –→ ℋ ) ∧ A ∈ ℋ ) → ((S +P T) ‘A) ∈ ℋ )
Theorem	hodclt 5492	Closure of difference of two Hilbert space operators.
⊢ (((S: ℋ –→ ℋ ∧ T: ℋ –→ ℋ ) ∧ A ∈ ℋ ) → ((S −P T) ‘A) ∈ ℋ )
Definition	df-cm 5493	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 cmbr 5499 for membership relation.
⊢ Com = {⟨x, y⟩∣((x ∈ Cℋ ∧ y ∈ Cℋ ) ∧ x = ((x ∩ y) ∨ℋ (x ∩ (⊥ ‘y))))}
Theorem	cmbrt 5494	Binary relation expressing A commutes with B. Definition of commutes in [Kalmbach] p. 20.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A Com B ↔ A = ((A ∩ B) ∨ℋ (A ∩ (⊥ ‘B)))))
Theorem	pjoml2 5495	Variation of orthomodular law. Definition in [Kalmbach] p. 22.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ⊆ B → (A ∨ℋ ((⊥ ‘A) ∩ B)) = B)
Theorem	pjoml3 5496	Variation of orthomodular law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (B ⊆ A → (A ∩ ((⊥ ‘A) ∨ℋ B)) = B)
Theorem	pjoml4 5497	Variation of orthomodular law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∨ℋ (B ∩ ((⊥ ‘A) ∨ℋ (⊥ ‘B)))) = (A ∨ℋ B)
Theorem	pjoml5 5498	An equivalent of the orthomodular law. Theorem 29.13(e) of [MaedaMaeda] p. 132.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ⊆ B → ∃x ∈ Cℋ (A ⊆ (⊥ ‘x) ∧ (A ∨ℋ x) = B))
Theorem	cmbr 5499	Binary relation expressing the commutes relation. Definition of commutes in [Kalmbach] p. 20.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A Com B ↔ A = ((A ∩ B) ∨ℋ (A ∩ (⊥ ‘B))))
Theorem	cmcmlem 5500	Commutation is symmetric. Theorem 3.4 of [Beran] p. 45.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A Com B → B Com A)