Theorem shsel1

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

Proof

Step	Hyp	Ref	Expression
1		shel	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in A\right)\to C\in \mathscr{H}$$
2		ax-hvaddid	$$⊢C\in \mathscr{H}\to C{+}_{ℎ}{0}_{ℎ}=C$$
3	1 2	syl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in A\right)\to C{+}_{ℎ}{0}_{ℎ}=C$$
4	3	adantlr	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge C\in A\right)\to C{+}_{ℎ}{0}_{ℎ}=C$$
5		sh0	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}\to 0_{ℎ}\in B$$
6	5	adantl	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to 0_{ℎ}\in B$$
7		shsva	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(\left(C\in A\wedge 0_{ℎ}\in B\right)\to C{+}_{ℎ}{0}_{ℎ}\in \left(A{+}_{\mathscr{H}}B\right)\right)$$
8	6 7	mpan2d	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(C\in A\to C{+}_{ℎ}{0}_{ℎ}\in \left(A{+}_{\mathscr{H}}B\right)\right)$$
9	8	imp	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge C\in A\right)\to C{+}_{ℎ}{0}_{ℎ}\in \left(A{+}_{\mathscr{H}}B\right)$$
10	4 9	eqeltrrd	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge C\in A\right)\to C\in \left(A{+}_{\mathscr{H}}B\right)$$
11	10	ex	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(C\in A\to C\in \left(A{+}_{\mathscr{H}}B\right)\right)$$