Theorem shsel

Description: Membership in the subspace sum of two Hilbert subspaces. (Contributed by NM, 14-Dec-2004) (Revised by Mario Carneiro, 29-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	shsel	$$⊢\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 \exists x\in A\exists y\in BC=x{+}_{ℎ}y\right)$$

Proof

Step	Hyp	Ref	Expression
1		shsval	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B={+}_{ℎ}\left[A\times B\right]$$
2	1	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[A\times B\right]\right)$$
3		ax-hfvadd	$$⊢{+}_{ℎ}:\mathscr{H}\times \mathscr{H}⟶\mathscr{H}$$
4		ffn	$$⊢{+}_{ℎ}:\mathscr{H}\times \mathscr{H}⟶\mathscr{H}\to {+}_{ℎ}Fn\left(\mathscr{H}\times \mathscr{H}\right)$$
5	3 4	ax-mp	$$⊢{+}_{ℎ}Fn\left(\mathscr{H}\times \mathscr{H}\right)$$
6		shss	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to A\subseteq \mathscr{H}$$
7		shss	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}\to B\subseteq \mathscr{H}$$
8		xpss12	$$⊢\left(A\subseteq \mathscr{H}\wedge B\subseteq \mathscr{H}\right)\to A\times B\subseteq \mathscr{H}\times \mathscr{H}$$
9	6 7 8	syl2an	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A\times B\subseteq \mathscr{H}\times \mathscr{H}$$
10		ovelimab	$$⊢\left({+}_{ℎ}Fn\left(\mathscr{H}\times \mathscr{H}\right)\wedge A\times B\subseteq \mathscr{H}\times \mathscr{H}\right)\to \left(C\in {+}_{ℎ}\left[A\times B\right]\leftrightarrow \exists x\in A\exists y\in BC=x{+}_{ℎ}y\right)$$
11	5 9 10	sylancr	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to \left(C\in {+}_{ℎ}\left[A\times B\right]\leftrightarrow \exists x\in A\exists y\in BC=x{+}_{ℎ}y\right)$$
12	2 11	bitrd	$$⊢\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 \exists x\in A\exists y\in BC=x{+}_{ℎ}y\right)$$