This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (C \in (A +_{ℋ} B) \leftrightarrow \exists x \in A \exists y \in B C = x +_{ℎ} y)$

Proof

Step	Hyp	Ref	Expression
1		shsval	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A +_{ℋ} B = +_{ℎ} [A \times B]$
2	1	eleq2d	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (C \in (A +_{ℋ} B) \leftrightarrow C \in +_{ℎ} [A \times B])$
3		ax-hfvadd	$⊢ +_{ℎ} : ℋ \times ℋ ⟶ ℋ$
4		ffn	$⊢ +_{ℎ} : ℋ \times ℋ ⟶ ℋ \to +_{ℎ} Fn (ℋ \times ℋ)$
5	3 4	ax-mp	$⊢ +_{ℎ} Fn (ℋ \times ℋ)$
6		shss	$⊢ A \in S_{ℋ} \to A \subseteq ℋ$
7		shss	$⊢ B \in S_{ℋ} \to B \subseteq ℋ$
8		xpss12	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to A \times B \subseteq ℋ \times ℋ$
9	6 7 8	syl2an	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A \times B \subseteq ℋ \times ℋ$
10		ovelimab	$⊢ (+_{ℎ} Fn (ℋ \times ℋ) \land A \times B \subseteq ℋ \times ℋ) \to (C \in +_{ℎ} [A \times B] \leftrightarrow \exists x \in A \exists y \in B C = x +_{ℎ} y)$
11	5 9 10	sylancr	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (C \in +_{ℎ} [A \times B] \leftrightarrow \exists x \in A \exists y \in B C = x +_{ℎ} y)$
12	2 11	bitrd	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (C \in (A +_{ℋ} B) \leftrightarrow \exists x \in A \exists y \in B C = x +_{ℎ} y)$