# Metamath Proof Explorer

## Theorem df0op2

Description: Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion df0op2 ${⊢}{0}_{\mathrm{hop}}=ℋ×{0}_{ℋ}$

### Proof

Step Hyp Ref Expression
1 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
2 ffn ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ\to {0}_{\mathrm{hop}}Fnℋ$
3 1 2 ax-mp ${⊢}{0}_{\mathrm{hop}}Fnℋ$
4 ho0val ${⊢}{x}\in ℋ\to {0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
5 4 rgen ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}$
6 fconstfv ${⊢}{0}_{\mathrm{hop}}:ℋ⟶\left\{{0}_{ℎ}\right\}↔\left({0}_{\mathrm{hop}}Fnℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{0}_{\mathrm{hop}}\left({x}\right)={0}_{ℎ}\right)$
7 3 5 6 mpbir2an ${⊢}{0}_{\mathrm{hop}}:ℋ⟶\left\{{0}_{ℎ}\right\}$
8 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
9 8 elexi ${⊢}{0}_{ℎ}\in \mathrm{V}$
10 9 fconst2 ${⊢}{0}_{\mathrm{hop}}:ℋ⟶\left\{{0}_{ℎ}\right\}↔{0}_{\mathrm{hop}}=ℋ×\left\{{0}_{ℎ}\right\}$
11 7 10 mpbi ${⊢}{0}_{\mathrm{hop}}=ℋ×\left\{{0}_{ℎ}\right\}$
12 df-ch0 ${⊢}{0}_{ℋ}=\left\{{0}_{ℎ}\right\}$
13 12 xpeq2i ${⊢}ℋ×{0}_{ℋ}=ℋ×\left\{{0}_{ℎ}\right\}$
14 11 13 eqtr4i ${⊢}{0}_{\mathrm{hop}}=ℋ×{0}_{ℋ}$