Theorem shless

Description: Subset implies subset of subspace sum. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	shless	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge A\subseteq B\right)\to A{+}_{\mathscr{H}}C\subseteq B{+}_{\mathscr{H}}C$$

Proof

Step	Hyp	Ref	Expression
1		ssrexv	$$⊢A\subseteq B\to \left(\exists y\in A\exists z\in Cx=y{+}_{ℎ}z\to \exists y\in B\exists z\in Cx=y{+}_{ℎ}z\right)$$
2	1	adantl	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge A\subseteq B\right)\to \left(\exists y\in A\exists z\in Cx=y{+}_{ℎ}z\to \exists y\in B\exists z\in Cx=y{+}_{ℎ}z\right)$$
3		simpl1	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge A\subseteq B\right)\to A\in {\mathbf{S}}_{\mathscr{H}}$$
4		simpl3	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge A\subseteq B\right)\to C\in {\mathbf{S}}_{\mathscr{H}}$$
5		shsel	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(x\in \left(A{+}_{\mathscr{H}}C\right)\leftrightarrow \exists y\in A\exists z\in Cx=y{+}_{ℎ}z\right)$$
6	3 4 5	syl2anc	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge A\subseteq B\right)\to \left(x\in \left(A{+}_{\mathscr{H}}C\right)\leftrightarrow \exists y\in A\exists z\in Cx=y{+}_{ℎ}z\right)$$
7		simpl2	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge A\subseteq B\right)\to B\in {\mathbf{S}}_{\mathscr{H}}$$
8		shsel	$$⊢\left(B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(x\in \left(B{+}_{\mathscr{H}}C\right)\leftrightarrow \exists y\in B\exists z\in Cx=y{+}_{ℎ}z\right)$$
9	7 4 8	syl2anc	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge A\subseteq B\right)\to \left(x\in \left(B{+}_{\mathscr{H}}C\right)\leftrightarrow \exists y\in B\exists z\in Cx=y{+}_{ℎ}z\right)$$
10	2 6 9	3imtr4d	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge A\subseteq B\right)\to \left(x\in \left(A{+}_{\mathscr{H}}C\right)\to x\in \left(B{+}_{\mathscr{H}}C\right)\right)$$
11	10	ssrdv	$$⊢\left(\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\wedge C\in {\mathbf{S}}_{\mathscr{H}}\right)\wedge A\subseteq B\right)\to A{+}_{\mathscr{H}}C\subseteq B{+}_{\mathscr{H}}C$$