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 ) ) ) |
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 ) ) ) |