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