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 ⊢ H ∈ S ℋ ↔ H ⊆ ℋ ∧ 0 ℎ ∈ H ∧ ∀ x ∈ H ∀ y ∈ H x + ℎ y ∈ H ∧ ∀ x ∈ ℂ ∀ y ∈ H x ⋅ ℎ y ∈ H

Proof

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