Metamath Proof Explorer

Theorem shlej2

Description: Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shlej2 
|- ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( C vH A ) C_ ( C vH B ) )

Proof

Step Hyp Ref Expression
1 shlej1 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( A vH C ) C_ ( B vH C ) )
2 shjcom 
 |-  ( ( A e. SH /\ C e. SH ) -> ( A vH C ) = ( C vH A ) )
3 2 3adant2 
 |-  ( ( A e. SH /\ B e. SH /\ C e. SH ) -> ( A vH C ) = ( C vH A ) )
4 3 adantr 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( A vH C ) = ( C vH A ) )
5 shjcom 
 |-  ( ( B e. SH /\ C e. SH ) -> ( B vH C ) = ( C vH B ) )
6 5 3adant1 
 |-  ( ( A e. SH /\ B e. SH /\ C e. SH ) -> ( B vH C ) = ( C vH B ) )
7 6 adantr 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( B vH C ) = ( C vH B ) )
8 1 4 7 3sstr3d 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( C vH A ) C_ ( C vH B ) )