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

Metamath Proof Explorer

Theorem shub1i

Description: Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1 ⊢ A ∈ S ℋ
shincl.2 ⊢ B ∈ S ℋ
Assertion shub1i ⊢ A ⊆ A ∨ ℋ B

Proof

Step Hyp Ref Expression
1 shincl.1 ⊢ A ∈ S ℋ
2 shincl.2 ⊢ B ∈ S ℋ
3 1 2 shsub1i ⊢ A ⊆ A + ℋ B
4 1 2 shsleji ⊢ A + ℋ B ⊆ A ∨ ℋ B
5 3 4 sstri ⊢ A ⊆ A ∨ ℋ B