# Metamath Proof Explorer

Assertion cnlnadj ${⊢}{T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \exists {t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)$
1 cnlnadjeu ${⊢}{T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \exists !{t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)$
2 reurex ${⊢}\exists !{t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)\to \exists {t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)$
3 1 2 syl ${⊢}{T}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\to \exists {t}\in \left(\mathrm{LinOp}\cap \mathrm{ContOp}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{y}={x}{\cdot }_{\mathrm{ih}}{t}\left({y}\right)$