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ℎ ∈ 𝐻 ) ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) )