Metamath Proof Explorer


Theorem shsel1i

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

Ref Expression
Hypotheses shincl.1
|- A e. SH
shincl.2
|- B e. SH
Assertion shsel1i
|- ( C e. A -> C e. ( A +H B ) )

Proof

Step Hyp Ref Expression
1 shincl.1
 |-  A e. SH
2 shincl.2
 |-  B e. SH
3 shsel1
 |-  ( ( A e. SH /\ B e. SH ) -> ( C e. A -> C e. ( A +H B ) ) )
4 1 2 3 mp2an
 |-  ( C e. A -> C e. ( A +H B ) )