# Metamath Proof Explorer

## Theorem choc0

Description: The orthocomplement of the zero subspace is the unit subspace. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion choc0 ${⊢}\perp \left({0}_{ℋ}\right)=ℋ$

### Proof

Step Hyp Ref Expression
1 h0elsh ${⊢}{0}_{ℋ}\in {\mathbf{S}}_{ℋ}$
2 shocel ${⊢}{0}_{ℋ}\in {\mathbf{S}}_{ℋ}\to \left({x}\in \perp \left({0}_{ℋ}\right)↔\left({x}\in ℋ\wedge \forall {y}\in {0}_{ℋ}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}=0\right)\right)$
3 1 2 ax-mp ${⊢}{x}\in \perp \left({0}_{ℋ}\right)↔\left({x}\in ℋ\wedge \forall {y}\in {0}_{ℋ}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}=0\right)$
4 hi02 ${⊢}{x}\in ℋ\to {x}{\cdot }_{\mathrm{ih}}{0}_{ℎ}=0$
5 df-ral ${⊢}\forall {y}\in {0}_{ℋ}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}=0↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {0}_{ℋ}\to {x}{\cdot }_{\mathrm{ih}}{y}=0\right)$
6 elch0 ${⊢}{y}\in {0}_{ℋ}↔{y}={0}_{ℎ}$
7 6 imbi1i ${⊢}\left({y}\in {0}_{ℋ}\to {x}{\cdot }_{\mathrm{ih}}{y}=0\right)↔\left({y}={0}_{ℎ}\to {x}{\cdot }_{\mathrm{ih}}{y}=0\right)$
8 7 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {0}_{ℋ}\to {x}{\cdot }_{\mathrm{ih}}{y}=0\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={0}_{ℎ}\to {x}{\cdot }_{\mathrm{ih}}{y}=0\right)$
9 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
10 9 elexi ${⊢}{0}_{ℎ}\in \mathrm{V}$
11 oveq2 ${⊢}{y}={0}_{ℎ}\to {x}{\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{0}_{ℎ}$
12 11 eqeq1d ${⊢}{y}={0}_{ℎ}\to \left({x}{\cdot }_{\mathrm{ih}}{y}=0↔{x}{\cdot }_{\mathrm{ih}}{0}_{ℎ}=0\right)$
13 10 12 ceqsalv ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={0}_{ℎ}\to {x}{\cdot }_{\mathrm{ih}}{y}=0\right)↔{x}{\cdot }_{\mathrm{ih}}{0}_{ℎ}=0$
14 8 13 bitri ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {0}_{ℋ}\to {x}{\cdot }_{\mathrm{ih}}{y}=0\right)↔{x}{\cdot }_{\mathrm{ih}}{0}_{ℎ}=0$
15 5 14 bitri ${⊢}\forall {y}\in {0}_{ℋ}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}=0↔{x}{\cdot }_{\mathrm{ih}}{0}_{ℎ}=0$
16 4 15 sylibr ${⊢}{x}\in ℋ\to \forall {y}\in {0}_{ℋ}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}=0$
17 abai ${⊢}\left({x}\in ℋ\wedge \forall {y}\in {0}_{ℋ}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}=0\right)↔\left({x}\in ℋ\wedge \left({x}\in ℋ\to \forall {y}\in {0}_{ℋ}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}=0\right)\right)$
18 16 17 mpbiran2 ${⊢}\left({x}\in ℋ\wedge \forall {y}\in {0}_{ℋ}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{\mathrm{ih}}{y}=0\right)↔{x}\in ℋ$
19 3 18 bitri ${⊢}{x}\in \perp \left({0}_{ℋ}\right)↔{x}\in ℋ$
20 19 eqriv ${⊢}\perp \left({0}_{ℋ}\right)=ℋ$