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 𝐴S
shincl.2 𝐵S
Assertion shub1i 𝐴 ⊆ ( 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 shincl.1 𝐴S
2 shincl.2 𝐵S
3 1 2 shsub1i 𝐴 ⊆ ( 𝐴 + 𝐵 )
4 1 2 shsleji ( 𝐴 + 𝐵 ) ⊆ ( 𝐴 𝐵 )
5 3 4 sstri 𝐴 ⊆ ( 𝐴 𝐵 )