Metamath Proof Explorer

Theorem shless

Description: Subset implies subset of subspace sum. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion shless 
|- ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( A +H C ) C_ ( B +H C ) )

Proof

Step Hyp Ref Expression
1 ssrexv 
 |-  ( A C_ B -> ( E. y e. A E. z e. C x = ( y +h z ) -> E. y e. B E. z e. C x = ( y +h z ) ) )
2 1 adantl 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( E. y e. A E. z e. C x = ( y +h z ) -> E. y e. B E. z e. C x = ( y +h z ) ) )
3 simpl1 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> A e. SH )
4 simpl3 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> C e. SH )
5 shsel 
 |-  ( ( A e. SH /\ C e. SH ) -> ( x e. ( A +H C ) <-> E. y e. A E. z e. C x = ( y +h z ) ) )
6 3 4 5 syl2anc 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( x e. ( A +H C ) <-> E. y e. A E. z e. C x = ( y +h z ) ) )
7 simpl2 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> B e. SH )
8 shsel 
 |-  ( ( B e. SH /\ C e. SH ) -> ( x e. ( B +H C ) <-> E. y e. B E. z e. C x = ( y +h z ) ) )
9 7 4 8 syl2anc 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( x e. ( B +H C ) <-> E. y e. B E. z e. C x = ( y +h z ) ) )
10 2 6 9 3imtr4d 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( x e. ( A +H C ) -> x e. ( B +H C ) ) )
11 10 ssrdv 
 |-  ( ( ( A e. SH /\ B e. SH /\ C e. SH ) /\ A C_ B ) -> ( A +H C ) C_ ( B +H C ) )