mmtheorems94 - Metamath Proof Explorer

Jump to page: Contents + 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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10752

Statement List for Metamath Proof Explorer - 9301-9400 - Page 94 of 108

Type	Label	Description
Statement
Theorem	shsupclt 9301	Closure of the subspace supremum of set of subsets of Hilbert space.
⊢ (A ⊆ ℘ ℋ → (span ‘∪A) ∈ Sℋ )
Theorem	hsupclt 9302	Closure of supremum of set of subsets of Hilbert space. Note that the supremum belongs to Cℋ even if the subsets do not.
⊢ (A ⊆ ℘ ℋ → ( ∨ℋ ‘A) ∈ Cℋ )
Theorem	chsupclt 9303	Closure of supremum of subset of Cℋ. Definition of supremum in Proposition 1 of [Kalmbach] p. 65. Shows that Cℋ is a complete lattice. Also part of Definition 3.4-1 in [MegillPavicic] p. 2345 (PDF p. 8).
⊢ (A ⊆ Cℋ → ( ∨ℋ ‘A) ∈ Cℋ )
Theorem	hsupss 9304	Subset relation for supremum of Hilbert space subsets.
⊢ ((A ⊆ ℘ ℋ ⋀ B ⊆ ℘ ℋ ) → (A ⊆ B → ( ∨ℋ ‘A) ⊆ ( ∨ℋ ‘B)))
Theorem	chsupss 9305	Subset relation for supremum of subset of Cℋ.
⊢ ((A ⊆ Cℋ ⋀ B ⊆ Cℋ ) → (A ⊆ B → ( ∨ℋ ‘A) ⊆ ( ∨ℋ ‘B)))
Theorem	chsupid 9306	A subspace is the supremum of all smaller subspaces.
⊢ (A ∈ Cℋ → ( ∨ℋ ‘{x ∈ Cℋ ∣x ⊆ A}) = A)
Theorem	chsupsn 9307	Value of supremum of subset of Cℋ on a singleton.
⊢ (A ∈ Cℋ → ( ∨ℋ ‘{A}) = A)
Theorem	hsupunss 9308	The union of a set of Hilbert space subsets is smaller than its supremum.
⊢ (A ⊆ ℘ ℋ → ∪A ⊆ ( ∨ℋ ‘A))
Theorem	spanss2 9309	A subset of Hilbert space is included in its span.
⊢ (A ⊆ ℋ → A ⊆ (span ‘A))
Theorem	shsupunss 9310	The union of a set of subspaces is smaller than its supremum.
⊢ (A ⊆ Sℋ → ∪A ⊆ (span ‘∪A))
Theorem	chsupunss 9311	The union of a set of closed subspaces is smaller than its supremum.
⊢ (A ⊆ Cℋ → ∪A ⊆ ( ∨ℋ ‘A))
Theorem	spanid 9312	A subspace of Hilbert space is its own span.
⊢ (A ∈ Sℋ → (span ‘A) = A)
Theorem	spanss 9313	Ordering relationship for the spans of subsets of Hilbert space.
⊢ ((B ⊆ ℋ ⋀ A ⊆ B) → (span ‘A) ⊆ (span ‘B))
Theorem	spanssoc 9314	The span of a subset of Hilbert space is less than or equal to its closure (double orthogonal complement).
⊢ (A ⊆ ℋ → (span ‘A) ⊆ (⊥ ‘(⊥ ‘A)))
Theorem	sshjvalt 9315	Value of join for subsets of Hilbert space.
⊢ ((A ⊆ ℋ ⋀ B ⊆ ℋ ) → (A ∨ℋ B) = (⊥ ‘(⊥ ‘(A ∪ B))))
Theorem	shjvalt 9316	Value of join in Sℋ.
⊢ ((A ∈ Sℋ ⋀ B ∈ Sℋ ) → (A ∨ℋ B) = (⊥ ‘(⊥ ‘(A ∪ B))))
Theorem	chjvalt 9317	Value of join in Cℋ.
⊢ ((A ∈ Cℋ ⋀ B ∈ Cℋ ) → (A ∨ℋ B) = (⊥ ‘(⊥ ‘(A ∪ B))))
Theorem	chjval 9318	Value of join in Cℋ.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∨ℋ B) = (⊥ ‘(⊥ ‘(A ∪ B)))
Theorem	dfchj2 9319	Alternate definition of join in the set of closed subspaces of Hilbert space Cℋ.
⊢ ∨ℋ = {⟨⟨x, y⟩, z⟩∣((x ⊆ ℋ ⋀ y ⊆ ℋ ) ⋀ z = ∩{w ∈ Cℋ ∣(x ∪ y) ⊆ w})}
Theorem	dfchj3 9320	Alternate definition of join in the set of closed subspaces of Hilbert space Cℋ: the join is the supremum of its two arguments. Based on the definition of join in [Beran] p. 3. For later convenience we prove a general version that works for any subset of Hilbert space, not just the elements of the lattice Cℋ.
⊢ ∨ℋ = {⟨⟨x, y⟩, z⟩∣((x ⊆ ℋ ⋀ y ⊆ ℋ ) ⋀ z = ( ∨ℋ ‘{x, y}))}
Theorem	sshjval3t 9321	Value of join for subsets of Hilbert space in terms of supremum: the join is the supremum of its two arguments. Based on the definition of join in [Beran] p. 3.
⊢ ((A ⊆ ℋ ⋀ B ⊆ ℋ ) → (A ∨ℋ B) = ( ∨ℋ ‘{A, B}))
Theorem	sshjclt 9322	Closure of join for subsets of Hilbert space.
⊢ ((A ⊆ ℋ ⋀ B ⊆ ℋ ) → (A ∨ℋ B) ∈ Cℋ )
Theorem	shjclt 9323	Closure of join in Sℋ.
⊢ ((A ∈ Sℋ ⋀ B ∈ Sℋ ) → (A ∨ℋ B) ∈ Cℋ )
Theorem	chjclt 9324	Closure of join in Cℋ.
⊢ ((A ∈ Cℋ ⋀ B ∈ Cℋ ) → (A ∨ℋ B) ∈ Cℋ )
Theorem	shjcomt 9325	Commutative law for Hilbert lattice join of subspaces.
⊢ ((A ∈ Sℋ ⋀ B ∈ Sℋ ) → (A ∨ℋ B) = (B ∨ℋ A))
Theorem	shincl 9326	Closure of intersection of two subspaces.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∩ B) ∈ Sℋ
Theorem	shscom 9327	Commutative law for subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A +ℋ B) = (B +ℋ A)
Theorem	shsva 9328	Vector sum belongs to subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ ((C ∈ A ⋀ D ∈ B) → (C +h D) ∈ (A +ℋ B))
Theorem	shsel1 9329	A subspace sum contains a member of one of its subspaces.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (C ∈ A → C ∈ (A +ℋ B))
Theorem	shsel2 9330	A subspace sum contains a member of one of its subspaces.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (C ∈ B → C ∈ (A +ℋ B))
Theorem	shsvs 9331	Vector subtraction belongs to subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ ((C ∈ A ⋀ D ∈ B) → (C −h D) ∈ (A +ℋ B))
Theorem	shunss 9332	Union is smaller than subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∪ B) ⊆ (A +ℋ B)
Theorem	shslej 9333	Subspace sum is smaller than Hilbert lattice join. Remark in [Kalmbach] p. 65.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A +ℋ B) ⊆ (A ∨ℋ B)
Theorem	shunssj 9334	Union is smaller than Hilbert lattice join.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∪ B) ⊆ (A ∨ℋ B)
Theorem	shjcom 9335	Commutative law for join in Sℋ.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∨ℋ B) = (B ∨ℋ A)
Theorem	shsub1 9336	Subspace sum is an upper bound of its arguments.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ A ⊆ (A +ℋ B)
Theorem	shsub2 9337	Subspace sum is an upper bound of its arguments.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ A ⊆ (B +ℋ A)
Theorem	shub1 9338	Hilbert lattice join is an upper bound of two subspaces.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ A ⊆ (A ∨ℋ B)
Theorem	shjcl 9339	Closure of Cℋ join.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∨ℋ B) ∈ Cℋ
Theorem	shjshcl 9340	Sℋ closure of join.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∨ℋ B) ∈ Sℋ
Theorem	shlub 9341	Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ ((A ⊆ C ⋀ B ⊆ C) ↔ (A ∨ℋ B) ⊆ C)
Theorem	shless 9342	Subset implies subset of subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Sℋ    ⇒   ⊢ (A ⊆ B → (A +ℋ C) ⊆ (B +ℋ C))
Theorem	shlej1 9343	Add disjunct to both sides of Hilbert subspace ordering.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Sℋ    ⇒   ⊢ (A ⊆ B → (A ∨ℋ C) ⊆ (B ∨ℋ C))
Theorem	shlej2 9344	Add disjunct to both sides of Hilbert subspace ordering.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Sℋ    ⇒   ⊢ (A ⊆ B → (C ∨ℋ A) ⊆ (C ∨ℋ B))
Theorem	shslejt 9345	Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65.
⊢ ((A ∈ Sℋ ⋀ B ∈ Sℋ ) → (A +ℋ B) ⊆ (A ∨ℋ B))
Theorem	shinclt 9346	Closure of intersection of two subspaces.
⊢ ((A ∈ Sℋ ⋀ B ∈ Sℋ ) → (A ∩ B) ∈ Sℋ )
Theorem	shub1t 9347	Hilbert lattice join is an upper bound of two subspaces.
⊢ ((A ∈ Sℋ ⋀ B ∈ Sℋ ) → A ⊆ (A ∨ℋ B))
Theorem	shub2t 9348	A subspace is a subset of its Hilbert lattice join with another.
⊢ ((A ∈ Sℋ ⋀ B ∈ Sℋ ) → A ⊆ (B ∨ℋ A))
Theorem	shlubt 9349	Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces.
⊢ ((A ∈ Sℋ ⋀ B ∈ Sℋ ⋀ C ∈ Cℋ ) → ((A ⊆ C ⋀ B ⊆ C) ↔ (A ∨ℋ B) ⊆ C))
Theorem	shlej1t 9350	Add disjunct to both sides of Hilbert subspace ordering.
⊢ (((A ∈ Sℋ ⋀ B ∈ Sℋ ⋀ C ∈ Sℋ ) ⋀ A ⊆ B) → (A ∨ℋ C) ⊆ (B ∨ℋ C))
Theorem	shlej2t 9351	Add disjunct to both sides of Hilbert subspace ordering.
⊢ (((A ∈ Sℋ ⋀ B ∈ Sℋ ⋀ C ∈ Sℋ ) ⋀ A ⊆ B) → (C ∨ℋ A) ⊆ (C ∨ℋ B))
Theorem	shsidm 9352	Idempotent law for Hilbert subspace sum.
⊢ A ∈ Sℋ    ⇒   ⊢ (A +ℋ A) = A
Theorem	shslub 9353	Least upper bound law for Hilbert subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Sℋ    ⇒   ⊢ ((A ⊆ C ⋀ B ⊆ C) ↔ (A +ℋ B) ⊆ C)
Theorem	shlesb1 9354	Hilbert lattice ordering in terms of subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ⊆ B ↔ (A +ℋ B) = B)
Theorem	shsumval2 9355	An alternate way to express subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A +ℋ B) = ∩{x ∈ Sℋ ∣(A ∪ B) ⊆ x}
Theorem	shsumval3 9356	An alternate way to express subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A +ℋ B) = (span ‘(A ∪ B))
Theorem	shmods 9357	The modular law holds for subspace sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Sℋ    ⇒   ⊢ (A ⊆ C → ((A +ℋ B) ∩ C) ⊆ (A +ℋ (B ∩ C)))
Theorem	shmod 9358	The modular law is implied by the closure of subspace sum. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Sℋ    ⇒   ⊢ (((A +ℋ B) = (A ∨ℋ B) ⋀ A ⊆ C) → ((A ∨ℋ B) ∩ C) ⊆ (A ∨ℋ (B ∩ C)))
Hilbert lattice operations
Theorem	sh0let 9359	The zero subspace is the smallest subspace.
⊢ (A ∈ Sℋ → 0ℋ ⊆ A)
Theorem	ch0let 9360	The zero subspace is the smallest member of Cℋ.
⊢ (A ∈ Cℋ → 0ℋ ⊆ A)
Theorem	shle0t 9361	No subspace is smaller than the zero subspace.
⊢ (A ∈ Sℋ → (A ⊆ 0ℋ ↔ A = 0ℋ))
Theorem	chle0t 9362	No Hilbert lattice element is smaller than zero.
⊢ (A ∈ Cℋ → (A ⊆ 0ℋ ↔ A = 0ℋ))
Theorem	chnlen0 9363	A Hilbert lattice element that is not a subset of another is nonzero.
⊢ (B ∈ Cℋ → (¬ A ⊆ B → ¬ A = 0ℋ))
Theorem	ch0psst 9364	The zero subspace is a proper subset of non-zero Hilbert lattice elements.
⊢ (A ∈ Cℋ → (0ℋ ⊂ A ↔ A ≠ 0ℋ))
Theorem	orthin 9365	The intersection of orthogonal subspaces is the zero subspace.
⊢ ((A ∈ Sℋ ⋀ B ∈ Sℋ ) → (A ⊆ (⊥ ‘B) → (A ∩ B) = 0ℋ))
Theorem	shne0 9366	A non-zero subspace has a non-zero vector.
⊢ A ∈ Sℋ    ⇒   ⊢ (A ≠ 0ℋ ↔ ∃x ∈ A x ≠ 0h)
Theorem	shs0 9367	Hilbert subspace sum with the zero subspace.
⊢ A ∈ Sℋ    ⇒   ⊢ (A +ℋ 0ℋ) = A
Theorem	shs00 9368	Two subspaces are zero iff their join is zero.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ ((A = 0ℋ ⋀ B = 0ℋ) ↔ (A +ℋ B) = 0ℋ)
Theorem	ch0le 9369	The closed subspace zero is the smallest member of Cℋ.
⊢ A ∈ Cℋ    ⇒   ⊢ 0ℋ ⊆ A
Theorem	chle0 9370	No Hilbert closed subspace is smaller than zero.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ⊆ 0ℋ ↔ A = 0ℋ)
Theorem	chne0 9371	A non-zero closed subspace has a non-zero vector.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ≠ 0ℋ ↔ ∃x ∈ A x ≠ 0h)
Theorem	chocin 9372	Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of [Kalmbach] p. 65.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ∩ (⊥ ‘A)) = 0ℋ
Theorem	chj0 9373	Join with lattice zero in Cℋ.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ∨ℋ 0ℋ) = A
Theorem	chm1 9374	Meet with lattice one in Cℋ.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ∩ ℋ ) = A
Theorem	chjcl 9375	Closure of Cℋ join.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∨ℋ B) ∈ Cℋ
Theorem	chslej 9376	Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A +ℋ B) ⊆ (A ∨ℋ B)
Theorem	chsel 9377	Membership in subspace sum.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (C ∈ (A +ℋ B) ↔ ∃x ∈ A ∃y ∈ B C = (x +h y))
Theorem	chincl 9378	Closure of Hilbert lattice intersection.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∩ B) ∈ Cℋ
Theorem	chsscon3 9379	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ⊆ B ↔ (⊥ ‘B) ⊆ (⊥ ‘A))
Theorem	chsscon1 9380	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ ((⊥ ‘A) ⊆ B ↔ (⊥ ‘B) ⊆ A)
Theorem	chsscon2 9381	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ⊆ (⊥ ‘B) ↔ B ⊆ (⊥ ‘A))
Theorem	chcon2 9382	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A = (⊥ ‘B) ↔ B = (⊥ ‘A))
Theorem	chcon1 9383	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ ((⊥ ‘A) = B ↔ (⊥ ‘B) = A)
Theorem	chcon3 9384	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A = B ↔ (⊥ ‘B) = (⊥ ‘A))
Theorem	chunssj 9385	Union is smaller than Cℋ join.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∪ B) ⊆ (A ∨ℋ B)
Theorem	chjcom 9386	Commutative law for join in Cℋ.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∨ℋ B) = (B ∨ℋ A)
Theorem	chub1 9387	Cℋ join is an upper bound of two elements.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ A ⊆ (A ∨ℋ B)
Theorem	chub2 9388	Cℋ join is an upper bound of two elements.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ A ⊆ (B ∨ℋ A)
Theorem	chlub 9389	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	chlubi 9390	Hilbert lattice join is the least upper bound of two elements (one direction of chlub 9389).
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ ((A ⊆ C ⋀ B ⊆ C) → (A ∨ℋ B) ⊆ C)
Theorem	chlej1 9391	Add join to both sides of a Hilbert lattice ordering.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ (A ⊆ B → (A ∨ℋ C) ⊆ (B ∨ℋ C))
Theorem	chlej2 9392	Add join to both sides of a Hilbert lattice ordering.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ (A ⊆ B → (C ∨ℋ A) ⊆ (C ∨ℋ B))
Theorem	chlej12 9393	Add join to both sides of a Hilbert lattice ordering.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    &   ⊢ D ∈ Cℋ    ⇒   ⊢ ((A ⊆ B ⋀ C ⊆ D) → (A ∨ℋ C) ⊆ (B ∨ℋ D))
Theorem	chlejb1 9394	Hilbert lattice ordering in terms of join.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ⊆ B ↔ (A ∨ℋ B) = B)
Theorem	chdmm1 9395	DeMorgan's law for meet in a Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (⊥ ‘(A ∩ B)) = ((⊥ ‘A) ∨ℋ (⊥ ‘B))
Theorem	chdmm2 9396	DeMorgan's law for meet in a Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (⊥ ‘((⊥ ‘A) ∩ B)) = (A ∨ℋ (⊥ ‘B))
Theorem	chdmm3 9397	DeMorgan's law for meet in a Hilbert lattice.
⊢ A ∈ Cℋ