# Metamath Proof Explorer

## Theorem ho01i

Description: A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of Beran p. 95. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

Ref Expression
Hypothesis ho0.1 ${⊢}{T}:ℋ⟶ℋ$
Assertion ho01i ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}=0↔{T}={0}_{\mathrm{hop}}$

### Proof

Step Hyp Ref Expression
1 ho0.1 ${⊢}{T}:ℋ⟶ℋ$
2 ffn ${⊢}{T}:ℋ⟶ℋ\to {T}Fnℋ$
3 1 2 ax-mp ${⊢}{T}Fnℋ$
4 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
5 4 elexi ${⊢}{0}_{ℎ}\in \mathrm{V}$
6 5 fconst ${⊢}\left(ℋ×\left\{{0}_{ℎ}\right\}\right):ℋ⟶\left\{{0}_{ℎ}\right\}$
7 ffn ${⊢}\left(ℋ×\left\{{0}_{ℎ}\right\}\right):ℋ⟶\left\{{0}_{ℎ}\right\}\to \left(ℋ×\left\{{0}_{ℎ}\right\}\right)Fnℋ$
8 6 7 ax-mp ${⊢}\left(ℋ×\left\{{0}_{ℎ}\right\}\right)Fnℋ$
9 eqfnfv ${⊢}\left({T}Fnℋ\wedge \left(ℋ×\left\{{0}_{ℎ}\right\}\right)Fnℋ\right)\to \left({T}=ℋ×\left\{{0}_{ℎ}\right\}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)=\left(ℋ×\left\{{0}_{ℎ}\right\}\right)\left({x}\right)\right)$
10 3 8 9 mp2an ${⊢}{T}=ℋ×\left\{{0}_{ℎ}\right\}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)=\left(ℋ×\left\{{0}_{ℎ}\right\}\right)\left({x}\right)$
11 df0op2 ${⊢}{0}_{\mathrm{hop}}=ℋ×{0}_{ℋ}$
12 df-ch0 ${⊢}{0}_{ℋ}=\left\{{0}_{ℎ}\right\}$
13 12 xpeq2i ${⊢}ℋ×{0}_{ℋ}=ℋ×\left\{{0}_{ℎ}\right\}$
14 11 13 eqtri ${⊢}{0}_{\mathrm{hop}}=ℋ×\left\{{0}_{ℎ}\right\}$
15 14 eqeq2i ${⊢}{T}={0}_{\mathrm{hop}}↔{T}=ℋ×\left\{{0}_{ℎ}\right\}$
16 1 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
17 hial0 ${⊢}{T}\left({x}\right)\in ℋ\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}=0↔{T}\left({x}\right)={0}_{ℎ}\right)$
18 16 17 syl ${⊢}{x}\in ℋ\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}=0↔{T}\left({x}\right)={0}_{ℎ}\right)$
19 5 fvconst2 ${⊢}{x}\in ℋ\to \left(ℋ×\left\{{0}_{ℎ}\right\}\right)\left({x}\right)={0}_{ℎ}$
20 19 eqeq2d ${⊢}{x}\in ℋ\to \left({T}\left({x}\right)=\left(ℋ×\left\{{0}_{ℎ}\right\}\right)\left({x}\right)↔{T}\left({x}\right)={0}_{ℎ}\right)$
21 18 20 bitr4d ${⊢}{x}\in ℋ\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}=0↔{T}\left({x}\right)=\left(ℋ×\left\{{0}_{ℎ}\right\}\right)\left({x}\right)\right)$
22 21 ralbiia ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}=0↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)=\left(ℋ×\left\{{0}_{ℎ}\right\}\right)\left({x}\right)$
23 10 15 22 3bitr4ri ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}=0↔{T}={0}_{\mathrm{hop}}$