Metamath Proof Explorer - mmtheorems54

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 - 5301-5400 - Page 54 of 58

Type	Label	Description
Statement
Theorem	hsupval2t 5301	Value of supremum of set of subsets of Hilbert space. Definition of supremum in Proposition 1 of [Kalmbach] p. 65.
⊢ (A ⊆ ℘ ℋ → ( ∨ℋ ‘A) = ∩{x ∈ Cℋ ∣∪A ⊆ x})
Theorem	hsupvalt 5302	Value of supremum of set of subsets of Hilbert space. For an alternate version of the value, see hsupval2t 5301.
⊢ (A ⊆ ℘ ℋ → ( ∨ℋ ‘A) = (⊥ ‘(⊥ ‘∪A)))
Theorem	chsupval2t 5303	The value of the supremum of a set of closed subspaces of Hilbert space. Definition of supremum in Proposition 1 of [Kalmbach] p. 65.
⊢ (A ⊆ Cℋ → ( ∨ℋ ‘A) = ∩{x ∈ Cℋ ∣∪A ⊆ x})
Theorem	chsupvalt 5304	The value of the supremum of a set of closed subspaces of Hilbert space. For an alternate version of the value, see chsupval2t 5303.
⊢ (A ⊆ Cℋ → ( ∨ℋ ‘A) = (⊥ ‘(⊥ ‘∪A)))
Theorem	spanclt 5305	The span of a subset of Hilbert space is a subspace.
⊢ (A ⊆ ℋ → (span ‘A) ∈ Sℋ )
Theorem	elspanclt 5306	A member of a span is a vector.
⊢ ((A ⊆ ℋ ∧ B ∈ (span ‘A)) → B ∈ ℋ )
Theorem	shsupclt 5307	Closure of the subspace supremum of set of subsets of Hilbert space.
⊢ (A ⊆ ℘ ℋ → (span ‘∪A) ∈ Sℋ )
Theorem	hsupclt 5308	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 5309	Closure of supremum of subset of Cℋ. Definition of supremum in Proposition 1 of [Kalmbach] p. 65. Shows that Cℋ is a complete lattice.
⊢ (A ⊆ Cℋ → ( ∨ℋ ‘A) ∈ Cℋ )
Theorem	hsupss 5310	Subset relation for supremum of Hilbert space subsets.
⊢ ((A ⊆ ℘ ℋ ∧ B ⊆ ℘ ℋ ) → (A ⊆ B → ( ∨ℋ ‘A) ⊆ ( ∨ℋ ‘B)))
Theorem	chsupss 5311	Subset relation for supremum of subset of Cℋ.
⊢ ((A ⊆ Cℋ ∧ B ⊆ Cℋ ) → (A ⊆ B → ( ∨ℋ ‘A) ⊆ ( ∨ℋ ‘B)))
Theorem	chsupid 5312	A subspace is the supremum of all smaller subspaces.
⊢ (A ∈ Cℋ → ( ∨ℋ ‘{x ∈ Cℋ ∣x ⊆ A}) = A)
Theorem	chsupsn 5313	Value of supremum of subset of Cℋ on a singleton.
⊢ (A ∈ Cℋ → ( ∨ℋ ‘{A}) = A)
Theorem	hsupunss 5314	The union of a set of Hilbert space subsets is smaller than its supremum.
⊢ (A ⊆ ℘ ℋ → ∪A ⊆ ( ∨ℋ ‘A))
Theorem	spanss2 5315	A subset of Hilbert space is included in its span.
⊢ (A ⊆ ℋ → A ⊆ (span ‘A))
Theorem	shsupunss 5316	The union of a set of subspaces is smaller than its supremum.
⊢ (A ⊆ Sℋ → ∪A ⊆ (span ‘∪A))
Theorem	chsupunss 5317	The union of a set of closed subspaces is smaller than its supremum.
⊢ (A ⊆ Cℋ → ∪A ⊆ ( ∨ℋ ‘A))
Theorem	spanid 5318	A subspace of Hilbert space is its own span.
⊢ (A ∈ Sℋ → (span ‘A) = A)
Theorem	spanss 5319	Ordering relationship for the spans of subsets of Hilbert space.
⊢ ((B ⊆ ℋ ∧ A ⊆ B) → (span ‘A) ⊆ (span ‘B))
Theorem	spanssoc 5320	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 5321	Value of join for subsets of Hilbert space.
⊢ ((A ⊆ ℋ ∧ B ⊆ ℋ ) → (A ∨ℋ B) = (⊥ ‘(⊥ ‘(A ∪ B))))
Theorem	shjvalt 5322	Value of join in Sℋ.
⊢ ((A ∈ Sℋ ∧ B ∈ Sℋ ) → (A ∨ℋ B) = (⊥ ‘(⊥ ‘(A ∪ B))))
Theorem	chjvalt 5323	Value of join in Cℋ.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ∨ℋ B) = (⊥ ‘(⊥ ‘(A ∪ B))))
Theorem	chjval 5324	Value of join in Cℋ.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∨ℋ B) = (⊥ ‘(⊥ ‘(A ∪ B)))
Theorem	dfchj2 5325	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 5326	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 5327	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 5328	Closure of join for subsets of Hilbert space.
⊢ ((A ⊆ ℋ ∧ B ⊆ ℋ ) → (A ∨ℋ B) ∈ Cℋ )
Theorem	shjclt 5329	Closure of join in Sℋ.
⊢ ((A ∈ Sℋ ∧ B ∈ Sℋ ) → (A ∨ℋ B) ∈ Cℋ )
Theorem	chjclt 5330	Closure of join in Cℋ.
⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (A ∨ℋ B) ∈ Cℋ )
Theorem	shjcomt 5331	Commutative law for Hilbert lattice join of subspaces.
⊢ ((A ∈ Sℋ ∧ B ∈ Sℋ ) → (A ∨ℋ B) = (B ∨ℋ A))
Theorem	shincl 5332	Closure of intersection of two subspaces.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∩ B) ∈ Sℋ
Theorem	shscom 5333	Commutative law for subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A +ℋ B) = (B +ℋ A)
Theorem	shsva 5334	Vector sum belongs to subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ ((C ∈ A ∧ D ∈ B) → (C +v D) ∈ (A +ℋ B))
Theorem	shsel1 5335	A subspace sum contains a member of one of its subspaces.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (C ∈ A → C ∈ (A +ℋ B))
Theorem	shsel2 5336	A subspace sum contains a member of one of its subspaces.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (C ∈ B → C ∈ (A +ℋ B))
Theorem	shsvs 5337	Vector subtraction belongs to subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ ((C ∈ A ∧ D ∈ B) → (C −v D) ∈ (A +ℋ B))
Theorem	shunss 5338	Union is smaller than subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∪ B) ⊆ (A +ℋ B)
Theorem	shslej 5339	Subspace sum is smaller than Hilbert lattice join. Remark of [Kalmbach] p. 65.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A +ℋ B) ⊆ (A ∨ℋ B)
Theorem	shunssj 5340	Union is smaller than Hilbert lattice join.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∪ B) ⊆ (A ∨ℋ B)
Theorem	shjcom 5341	Commutative law for join in Sℋ.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∨ℋ B) = (B ∨ℋ A)
Theorem	shsub1 5342	Subspace sum is an upper bound of its arguments.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ A ⊆ (A +ℋ B)
Theorem	shsub2 5343	Subspace sum is an upper bound of its arguments.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ A ⊆ (B +ℋ A)
Theorem	shub1 5344	Hilbert lattice join is an upper bound of two subspaces.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ A ⊆ (A ∨ℋ B)
Theorem	shjcl 5345	Closure of Cℋ join.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∨ℋ B) ∈ Cℋ
Theorem	shjshcl 5346	Sℋ closure of join.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ∨ℋ B) ∈ Sℋ
Theorem	shlub 5347	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 5348	Subset implies subset of subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Sℋ    ⇒   ⊢ (A ⊆ B → (A +ℋ C) ⊆ (B +ℋ C))
Theorem	shlej1 5349	Add disjunct to both sides of Hilbert subspace ordering.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Sℋ    ⇒   ⊢ (A ⊆ B → (A ∨ℋ C) ⊆ (B ∨ℋ C))
Theorem	shlej2 5350	Add disjunct to both sides of Hilbert subspace ordering.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Sℋ    ⇒   ⊢ (A ⊆ B → (C ∨ℋ A) ⊆ (C ∨ℋ B))
Theorem	shslejt 5351	Subspace sum is smaller than subspace join. Remark of [Kalmbach] p. 65.
⊢ ((A ∈ Sℋ ∧ B ∈ Sℋ ) → (A +ℋ B) ⊆ (A ∨ℋ B))
Theorem	shinclt 5352	Closure of intersection of two subspaces.
⊢ ((A ∈ Sℋ ∧ B ∈ Sℋ ) → (A ∩ B) ∈ Sℋ )
Theorem	shub1t 5353	Hilbert lattice join is an upper bound of two subspaces.
⊢ ((A ∈ Sℋ ∧ B ∈ Sℋ ) → A ⊆ (A ∨ℋ B))
Theorem	shub2t 5354	A subspace is a subset of its Hilbert lattice join with another.
⊢ ((A ∈ Sℋ ∧ B ∈ Sℋ ) → A ⊆ (B ∨ℋ A))
Theorem	shlubt 5355	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 5356	Add disjunct to both sides of Hilbert subspace ordering.
⊢ ((A ∈ Sℋ ∧ B ∈ Sℋ ∧ C ∈ Sℋ ) → (A ⊆ B → (A ∨ℋ C) ⊆ (B ∨ℋ C)))
Theorem	shlej2t 5357	Add disjunct to both sides of Hilbert subspace ordering.
⊢ ((A ∈ Sℋ ∧ B ∈ Sℋ ∧ C ∈ Sℋ ) → (A ⊆ B → (C ∨ℋ A) ⊆ (C ∨ℋ B)))
Theorem	shsidm 5358	Idempotent law for Hilbert subspace sum.
⊢ A ∈ Sℋ    ⇒   ⊢ (A +ℋ A) = A
Theorem	shslub 5359	Least upper bound law for Hilbert subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    &   ⊢ C ∈ Sℋ    ⇒   ⊢ ((A ⊆ C ∧ B ⊆ C) ↔ (A +ℋ B) ⊆ C)
Theorem	shlesb1 5360	Hilbert lattice ordering in terms of subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A ⊆ B ↔ (A +ℋ B) = B)
Theorem	shsumval2 5361	An alternate way to express subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A +ℋ B) = ∩{x ∈ Sℋ ∣(A ∪ B) ⊆ x}
Theorem	shsumval3 5362	An alternate way to express subspace sum.
⊢ A ∈ Sℋ    &   ⊢ B ∈ Sℋ    ⇒   ⊢ (A +ℋ B) = (span ‘(A ∪ B))
Theorem	shmods 5363	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 5364	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)))
Theorem	sh0let 5365	The zero subspace is the smallest subspace.
⊢ (A ∈ Sℋ → 0ℋ ⊆ A)
Theorem	ch0let 5366	The zero subspace is the smallest member of Cℋ.
⊢ (A ∈ Cℋ → 0ℋ ⊆ A)
Theorem	shle0t 5367	No subspace is smaller than the zero subspace.
⊢ (A ∈ Sℋ → (A ⊆ 0ℋ ↔ A = 0ℋ))
Theorem	chle0t 5368	No Hilbert lattice element is smaller than zero.
⊢ (A ∈ Cℋ → (A ⊆ 0ℋ ↔ A = 0ℋ))
Theorem	chnlen0 5369	A Hilbert lattice element that is not a subset of another is nonzero.
⊢ (B ∈ Cℋ → (¬ A ⊆ B → ¬ A = 0ℋ))
Theorem	ch0psst 5370	The zero subspace is a proper subset of non-zero Hilbert lattice elements.
⊢ (A ∈ Cℋ → (0ℋ ⊂ A ↔ ¬ A = 0ℋ))
Theorem	orthin 5371	The intersection of orthogonal subspaces is the zero subspace.
⊢ ((A ∈ Sℋ ∧ B ∈ Sℋ ) → (A ⊆ (⊥ ‘B) → (A ∩ B) = 0ℋ))
Theorem	shne0 5372	A non-zero subspace has a non-zero vector.
⊢ A ∈ Sℋ    ⇒   ⊢ (¬ A = 0ℋ ↔ ∃x ∈ A ¬ x = 0v)
Theorem	ch0le 5373	The closed subspace zero is the smallest member of Cℋ.
⊢ A ∈ Cℋ    ⇒   ⊢ 0ℋ ⊆ A
Theorem	chle0 5374	No Hilbert closed subspace is smaller than zero.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ⊆ 0ℋ ↔ A = 0ℋ)
Theorem	chne0 5375	A non-zero closed subspace has a non-zero vector.
⊢ A ∈ Cℋ    ⇒   ⊢ (¬ A = 0ℋ ↔ ∃x ∈ A ¬ x = 0v)
Theorem	chocin 5376	Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of [Kalmbach] p. 65.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ∩ (⊥ ‘A)) = 0ℋ
Theorem	chj0 5377	Join with lattice zero in Cℋ.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ∨ℋ 0ℋ) = A
Theorem	chm1 5378	Meet with lattice one in Cℋ.
⊢ A ∈ Cℋ    ⇒   ⊢ (A ∩ ℋ ) = A
Theorem	chjcl 5379	Closure of Cℋ join.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∨ℋ B) ∈ Cℋ
Theorem	chslej 5380	Subspace sum is smaller than subspace join. Remark of [Kalmbach] p. 65.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A +ℋ B) ⊆ (A ∨ℋ B)
Theorem	chsel 5381	Membership in subspace sum.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (C ∈ (A +ℋ B) ↔ ∃x ∈ A ∃y ∈ B C = (x +v y))
Theorem	chincl 5382	Closure of Hilbert lattice intersection.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∩ B) ∈ Cℋ
Theorem	chsscon3 5383	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ⊆ B ↔ (⊥ ‘B) ⊆ (⊥ ‘A))
Theorem	chsscon1 5384	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ ((⊥ ‘A) ⊆ B ↔ (⊥ ‘B) ⊆ A)
Theorem	chsscon2 5385	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ⊆ (⊥ ‘B) ↔ B ⊆ (⊥ ‘A))
Theorem	chcon2 5386	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A = (⊥ ‘B) ↔ B = (⊥ ‘A))
Theorem	chcon3 5387	Hilbert lattice contraposition law.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A = B ↔ (⊥ ‘B) = (⊥ ‘A))
Theorem	chunssj 5388	Union is smaller than Cℋ join.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∪ B) ⊆ (A ∨ℋ B)
Theorem	chjcom 5389	Commutative law for join in Cℋ.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ∨ℋ B) = (B ∨ℋ A)
Theorem	chub1 5390	Cℋ join is an upper bound of two elements.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ A ⊆ (A ∨ℋ B)
Theorem	chub2 5391	Cℋ join is an upper bound of two elements.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ A ⊆ (B ∨ℋ A)
Theorem	chlub 5392	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 5393	Hilbert lattice join is the least upper bound of two elements (one direction of chlub 5392).
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ ((A ⊆ C ∧ B ⊆ C) → (A ∨ℋ B) ⊆ C)
Theorem	chlej1 5394	Add join to both sides of a Hilbert lattice ordering.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ (A ⊆ B → (A ∨ℋ C) ⊆ (B ∨ℋ C))
Theorem	chlej2 5395	Add join to both sides of a Hilbert lattice ordering.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    &   ⊢ C ∈ Cℋ    ⇒   ⊢ (A ⊆ B → (C ∨ℋ A) ⊆ (C ∨ℋ B))
Theorem	chlej12 5396	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 5397	Hilbert lattice ordering in terms of join.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (A ⊆ B ↔ (A ∨ℋ B) = B)
Theorem	chdmm1 5398	DeMorgan's law for meet in a Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (⊥ ‘(A ∩ B)) = ((⊥ ‘A) ∨ℋ (⊥ ‘B))
Theorem	chdmm2 5399	DeMorgan's law for meet in a Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (⊥ ‘((⊥ ‘A) ∩ B)) = (A ∨ℋ (⊥ ‘B))
Theorem	chdmm3 5400	DeMorgan's law for meet in a Hilbert lattice.
⊢ A ∈ Cℋ    &   ⊢ B ∈ Cℋ    ⇒   ⊢ (⊥ ‘(A ∩ (⊥ ‘B))) = ((⊥ ‘A) ∨ℋ B)