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	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) ↔ ( 𝐴 ∨ℋ 𝐵 ) ⊆ 𝐶 )