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

Metamath Proof Explorer

Theorem shub1

Description: Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shub1 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ⊆ A ∨ ℋ B

Proof

Step Hyp Ref Expression
1 shsub1 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ⊆ A + ℋ B
2 shslej ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A + ℋ B ⊆ A ∨ ℋ B
3 1 2 sstrd ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ⊆ A ∨ ℋ B