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	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		shsval	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( +ℎ “ ( 𝐴 × 𝐵 ) ) )
2	1	eleq2d	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ 𝐶 ∈ ( +ℎ “ ( 𝐴 × 𝐵 ) ) ) )
3		ax-hfvadd	⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ
4		ffn	⊢ ( +ℎ : ( ℋ × ℋ ) ⟶ ℋ → +ℎ Fn ( ℋ × ℋ ) )
5	3 4	ax-mp	⊢ +ℎ Fn ( ℋ × ℋ )
6		shss	⊢ ( 𝐴 ∈ Sℋ → 𝐴 ⊆ ℋ )
7		shss	⊢ ( 𝐵 ∈ Sℋ → 𝐵 ⊆ ℋ )
8		xpss12	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 × 𝐵 ) ⊆ ( ℋ × ℋ ) )
9	6 7 8	syl2an	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 × 𝐵 ) ⊆ ( ℋ × ℋ ) )
10		ovelimab	⊢ ( ( +ℎ Fn ( ℋ × ℋ ) ∧ ( 𝐴 × 𝐵 ) ⊆ ( ℋ × ℋ ) ) → ( 𝐶 ∈ ( +ℎ “ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) )
11	5 9 10	sylancr	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ ( +ℎ “ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) )
12	2 11	bitrd	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐶 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝐶 = ( 𝑥 +ℎ 𝑦 ) ) )