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	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(C\in B\to C\in \left(A{+}_{\mathscr{H}}B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		shsel1	$$⊢\left(B\in {\mathbf{S}}_{\mathscr{H}}\wedge A\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(C\in B\to C\in \left(B{+}_{\mathscr{H}}A\right)\right)$$
2	1	ancoms	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(C\in B\to C\in \left(B{+}_{\mathscr{H}}A\right)\right)$$
3		shscom	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B=B{+}_{\mathscr{H}}A$$
4	3	eleq2d	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(C\in \left(A{+}_{\mathscr{H}}B\right)\leftrightarrow C\in \left(B{+}_{\mathscr{H}}A\right)\right)$$
5	2 4	sylibrd	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(C\in B\to C\in \left(A{+}_{\mathscr{H}}B\right)\right)$$