Metamath Proof Explorer


Theorem shsel2

Description: A subspace sum contains a member of one of its subspaces. (Contributed by NM, 15-Dec-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 shsel1
 |-  ( ( B e. SH /\ A e. SH ) -> ( C e. B -> C e. ( B +H A ) ) )
2 1 ancoms
 |-  ( ( A e. SH /\ B e. SH ) -> ( C e. B -> C e. ( B +H A ) ) )
3 shscom
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( B +H A ) )
4 3 eleq2d
 |-  ( ( A e. SH /\ B e. SH ) -> ( C e. ( A +H B ) <-> C e. ( B +H A ) ) )
5 2 4 sylibrd
 |-  ( ( A e. SH /\ B e. SH ) -> ( C e. B -> C e. ( A +H B ) ) )