Metamath Proof Explorer


Theorem shlej2i

Description: Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1
|- A e. SH
shincl.2
|- B e. SH
shless.1
|- C e. SH
Assertion shlej2i
|- ( A C_ B -> ( C vH A ) C_ ( C vH B ) )

Proof

Step Hyp Ref Expression
1 shincl.1
 |-  A e. SH
2 shincl.2
 |-  B e. SH
3 shless.1
 |-  C e. SH
4 1 2 3 shlej1i
 |-  ( A C_ B -> ( A vH C ) C_ ( B vH C ) )
5 3 1 shjcomi
 |-  ( C vH A ) = ( A vH C )
6 3 2 shjcomi
 |-  ( C vH B ) = ( B vH C )
7 4 5 6 3sstr4g
 |-  ( A C_ B -> ( C vH A ) C_ ( C vH B ) )