# Metamath Proof Explorer

## Theorem issh2

Description: Subspace H of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. Definition of Beran p. 95. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion issh2 ( 𝐻S ↔ ( ( 𝐻 ⊆ ℋ ∧ 0𝐻 ) ∧ ( ∀ 𝑥𝐻𝑦𝐻 ( 𝑥 + 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦𝐻 ( 𝑥 · 𝑦 ) ∈ 𝐻 ) ) )

### Proof

Step Hyp Ref Expression
1 issh ( 𝐻S ↔ ( ( 𝐻 ⊆ ℋ ∧ 0𝐻 ) ∧ ( ( + “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( · “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) )
2 ax-hfvadd + : ( ℋ × ℋ ) ⟶ ℋ
3 ffun ( + : ( ℋ × ℋ ) ⟶ ℋ → Fun + )
4 2 3 ax-mp Fun +
5 xpss12 ( ( 𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ ) → ( 𝐻 × 𝐻 ) ⊆ ( ℋ × ℋ ) )
6 5 anidms ( 𝐻 ⊆ ℋ → ( 𝐻 × 𝐻 ) ⊆ ( ℋ × ℋ ) )
7 2 fdmi dom + = ( ℋ × ℋ )
8 6 7 sseqtrrdi ( 𝐻 ⊆ ℋ → ( 𝐻 × 𝐻 ) ⊆ dom + )
9 funimassov ( ( Fun + ∧ ( 𝐻 × 𝐻 ) ⊆ dom + ) → ( ( + “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ↔ ∀ 𝑥𝐻𝑦𝐻 ( 𝑥 + 𝑦 ) ∈ 𝐻 ) )
10 4 8 9 sylancr ( 𝐻 ⊆ ℋ → ( ( + “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ↔ ∀ 𝑥𝐻𝑦𝐻 ( 𝑥 + 𝑦 ) ∈ 𝐻 ) )
11 ax-hfvmul · : ( ℂ × ℋ ) ⟶ ℋ
12 ffun ( · : ( ℂ × ℋ ) ⟶ ℋ → Fun · )
13 11 12 ax-mp Fun ·
14 xpss2 ( 𝐻 ⊆ ℋ → ( ℂ × 𝐻 ) ⊆ ( ℂ × ℋ ) )
15 11 fdmi dom · = ( ℂ × ℋ )
16 14 15 sseqtrrdi ( 𝐻 ⊆ ℋ → ( ℂ × 𝐻 ) ⊆ dom · )
17 funimassov ( ( Fun · ∧ ( ℂ × 𝐻 ) ⊆ dom · ) → ( ( · “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ↔ ∀ 𝑥 ∈ ℂ ∀ 𝑦𝐻 ( 𝑥 · 𝑦 ) ∈ 𝐻 ) )
18 13 16 17 sylancr ( 𝐻 ⊆ ℋ → ( ( · “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ↔ ∀ 𝑥 ∈ ℂ ∀ 𝑦𝐻 ( 𝑥 · 𝑦 ) ∈ 𝐻 ) )
19 10 18 anbi12d ( 𝐻 ⊆ ℋ → ( ( ( + “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( · “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ↔ ( ∀ 𝑥𝐻𝑦𝐻 ( 𝑥 + 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦𝐻 ( 𝑥 · 𝑦 ) ∈ 𝐻 ) ) )
20 19 adantr ( ( 𝐻 ⊆ ℋ ∧ 0𝐻 ) → ( ( ( + “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( · “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ↔ ( ∀ 𝑥𝐻𝑦𝐻 ( 𝑥 + 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦𝐻 ( 𝑥 · 𝑦 ) ∈ 𝐻 ) ) )
21 20 pm5.32i ( ( ( 𝐻 ⊆ ℋ ∧ 0𝐻 ) ∧ ( ( + “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( · “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) ↔ ( ( 𝐻 ⊆ ℋ ∧ 0𝐻 ) ∧ ( ∀ 𝑥𝐻𝑦𝐻 ( 𝑥 + 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦𝐻 ( 𝑥 · 𝑦 ) ∈ 𝐻 ) ) )
22 1 21 bitri ( 𝐻S ↔ ( ( 𝐻 ⊆ ℋ ∧ 0𝐻 ) ∧ ( ∀ 𝑥𝐻𝑦𝐻 ( 𝑥 + 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦𝐻 ( 𝑥 · 𝑦 ) ∈ 𝐻 ) ) )