Metamath Proof Explorer

Theorem ellnop

Description: Property defining a linear Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion ellnop ${⊢}{T}\in \mathrm{LinOp}↔\left({T}:ℋ⟶ℋ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$

Proof

Step Hyp Ref Expression
1 fveq1 ${⊢}{t}={T}\to {t}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)={T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)$
2 fveq1 ${⊢}{t}={T}\to {t}\left({y}\right)={T}\left({y}\right)$
3 2 oveq2d ${⊢}{t}={T}\to {x}{\cdot }_{ℎ}{t}\left({y}\right)={x}{\cdot }_{ℎ}{T}\left({y}\right)$
4 fveq1 ${⊢}{t}={T}\to {t}\left({z}\right)={T}\left({z}\right)$
5 3 4 oveq12d ${⊢}{t}={T}\to \left({x}{\cdot }_{ℎ}{t}\left({y}\right)\right){+}_{ℎ}{t}\left({z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)$
6 1 5 eqeq12d ${⊢}{t}={T}\to \left({t}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{t}\left({y}\right)\right){+}_{ℎ}{t}\left({z}\right)↔{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
7 6 ralbidv ${⊢}{t}={T}\to \left(\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{t}\left({y}\right)\right){+}_{ℎ}{t}\left({z}\right)↔\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
8 7 2ralbidv ${⊢}{t}={T}\to \left(\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{t}\left({y}\right)\right){+}_{ℎ}{t}\left({z}\right)↔\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
9 df-lnop ${⊢}\mathrm{LinOp}=\left\{{t}\in \left({ℋ}^{ℋ}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{t}\left({y}\right)\right){+}_{ℎ}{t}\left({z}\right)\right\}$
10 8 9 elrab2 ${⊢}{T}\in \mathrm{LinOp}↔\left({T}\in \left({ℋ}^{ℋ}\right)\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
11 ax-hilex ${⊢}ℋ\in \mathrm{V}$
12 11 11 elmap ${⊢}{T}\in \left({ℋ}^{ℋ}\right)↔{T}:ℋ⟶ℋ$
13 12 anbi1i ${⊢}\left({T}\in \left({ℋ}^{ℋ}\right)\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)↔\left({T}:ℋ⟶ℋ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$
14 10 13 bitri ${⊢}{T}\in \mathrm{LinOp}↔\left({T}:ℋ⟶ℋ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left(\left({x}{\cdot }_{ℎ}{y}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{T}\left({y}\right)\right){+}_{ℎ}{T}\left({z}\right)\right)$