# Metamath Proof Explorer

## Theorem issh3

Description: Subspace H of a Hilbert space. (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

Ref Expression
Assertion issh3 ${⊢}{H}\subseteq ℋ\to \left({H}\in {\mathbf{S}}_{ℋ}↔\left({0}_{ℎ}\in {H}\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)\right)$

### Proof

Step Hyp Ref Expression
1 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)$
2 anass ${⊢}\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)↔\left({H}\subseteq ℋ\wedge \left({0}_{ℎ}\in {H}\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)\right)$
3 2 baib ${⊢}{H}\subseteq ℋ\to \left(\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)↔\left({0}_{ℎ}\in {H}\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)\right)$
4 1 3 syl5bb ${⊢}{H}\subseteq ℋ\to \left({H}\in {\mathbf{S}}_{ℋ}↔\left({0}_{ℎ}\in {H}\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)\right)$