# 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}\in {\mathbf{S}}_{ℋ}↔\left(\left({H}\subseteq ℋ\wedge {0}_{ℎ}\in {H}\right)\wedge \left(\forall {x}\in {H}\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{+}_{ℎ}{y}\in {H}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}\right)\right)$

### Proof

Step Hyp Ref Expression
1 issh ${⊢}{H}\in {\mathbf{S}}_{ℋ}↔\left(\left({H}\subseteq ℋ\wedge {0}_{ℎ}\in {H}\right)\wedge \left({+}_{ℎ}\left[{H}×{H}\right]\subseteq {H}\wedge {\cdot }_{ℎ}\left[ℂ×{H}\right]\subseteq {H}\right)\right)$
2 ax-hfvadd ${⊢}{+}_{ℎ}:ℋ×ℋ⟶ℋ$
3 ffun ${⊢}{+}_{ℎ}:ℋ×ℋ⟶ℋ\to \mathrm{Fun}{+}_{ℎ}$
4 2 3 ax-mp ${⊢}\mathrm{Fun}{+}_{ℎ}$
5 xpss12 ${⊢}\left({H}\subseteq ℋ\wedge {H}\subseteq ℋ\right)\to {H}×{H}\subseteq ℋ×ℋ$
6 5 anidms ${⊢}{H}\subseteq ℋ\to {H}×{H}\subseteq ℋ×ℋ$
7 2 fdmi ${⊢}\mathrm{dom}{+}_{ℎ}=ℋ×ℋ$
8 6 7 sseqtrrdi ${⊢}{H}\subseteq ℋ\to {H}×{H}\subseteq \mathrm{dom}{+}_{ℎ}$
9 funimassov ${⊢}\left(\mathrm{Fun}{+}_{ℎ}\wedge {H}×{H}\subseteq \mathrm{dom}{+}_{ℎ}\right)\to \left({+}_{ℎ}\left[{H}×{H}\right]\subseteq {H}↔\forall {x}\in {H}\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{+}_{ℎ}{y}\in {H}\right)$
10 4 8 9 sylancr ${⊢}{H}\subseteq ℋ\to \left({+}_{ℎ}\left[{H}×{H}\right]\subseteq {H}↔\forall {x}\in {H}\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{+}_{ℎ}{y}\in {H}\right)$
11 ax-hfvmul ${⊢}{\cdot }_{ℎ}:ℂ×ℋ⟶ℋ$
12 ffun ${⊢}{\cdot }_{ℎ}:ℂ×ℋ⟶ℋ\to \mathrm{Fun}{\cdot }_{ℎ}$
13 11 12 ax-mp ${⊢}\mathrm{Fun}{\cdot }_{ℎ}$
14 xpss2 ${⊢}{H}\subseteq ℋ\to ℂ×{H}\subseteq ℂ×ℋ$
15 11 fdmi ${⊢}\mathrm{dom}{\cdot }_{ℎ}=ℂ×ℋ$
16 14 15 sseqtrrdi ${⊢}{H}\subseteq ℋ\to ℂ×{H}\subseteq \mathrm{dom}{\cdot }_{ℎ}$
17 funimassov ${⊢}\left(\mathrm{Fun}{\cdot }_{ℎ}\wedge ℂ×{H}\subseteq \mathrm{dom}{\cdot }_{ℎ}\right)\to \left({\cdot }_{ℎ}\left[ℂ×{H}\right]\subseteq {H}↔\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}\right)$
18 13 16 17 sylancr ${⊢}{H}\subseteq ℋ\to \left({\cdot }_{ℎ}\left[ℂ×{H}\right]\subseteq {H}↔\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}\right)$
19 10 18 anbi12d ${⊢}{H}\subseteq ℋ\to \left(\left({+}_{ℎ}\left[{H}×{H}\right]\subseteq {H}\wedge {\cdot }_{ℎ}\left[ℂ×{H}\right]\subseteq {H}\right)↔\left(\forall {x}\in {H}\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{+}_{ℎ}{y}\in {H}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}\right)\right)$
20 19 adantr ${⊢}\left({H}\subseteq ℋ\wedge {0}_{ℎ}\in {H}\right)\to \left(\left({+}_{ℎ}\left[{H}×{H}\right]\subseteq {H}\wedge {\cdot }_{ℎ}\left[ℂ×{H}\right]\subseteq {H}\right)↔\left(\forall {x}\in {H}\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{+}_{ℎ}{y}\in {H}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}\right)\right)$
21 20 pm5.32i ${⊢}\left(\left({H}\subseteq ℋ\wedge {0}_{ℎ}\in {H}\right)\wedge \left({+}_{ℎ}\left[{H}×{H}\right]\subseteq {H}\wedge {\cdot }_{ℎ}\left[ℂ×{H}\right]\subseteq {H}\right)\right)↔\left(\left({H}\subseteq ℋ\wedge {0}_{ℎ}\in {H}\right)\wedge \left(\forall {x}\in {H}\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{+}_{ℎ}{y}\in {H}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}\right)\right)$
22 1 21 bitri ${⊢}{H}\in {\mathbf{S}}_{ℋ}↔\left(\left({H}\subseteq ℋ\wedge {0}_{ℎ}\in {H}\right)\wedge \left(\forall {x}\in {H}\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{+}_{ℎ}{y}\in {H}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}\right)\right)$