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 e. SH
shincl.2
|- B e. SH
Assertion shub1i
|- A C_ ( A vH B )

Proof

Step Hyp Ref Expression
1 shincl.1
 |-  A e. SH
2 shincl.2
 |-  B e. SH
3 1 2 shsub1i
 |-  A C_ ( A +H B )
4 1 2 shsleji
 |-  ( A +H B ) C_ ( A vH B )
5 3 4 sstri
 |-  A C_ ( A vH B )