This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem shlubi

Description: Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shlub.1	⊢ 𝐴 ∈ S_ℋ
	shlub.2	⊢ 𝐵 ∈ S_ℋ
	shlub.3	⊢ 𝐶 ∈ C_ℋ
Assertion	shlubi	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 ∨_ℋ 𝐵 ) ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		shlub.1	⊢ 𝐴 ∈ S_ℋ
2		shlub.2	⊢ 𝐵 ∈ S_ℋ
3		shlub.3	⊢ 𝐶 ∈ C_ℋ
4		shlub	⊢ ( ( 𝐴 ∈ S_ℋ ∧ 𝐵 ∈ S_ℋ ∧ 𝐶 ∈ C_ℋ ) → ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 ∨_ℋ 𝐵 ) ⊆ 𝐶 ) )
5	1 2 3 4	mp3an	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 ∨_ℋ 𝐵 ) ⊆ 𝐶 )