# Metamath Proof Explorer

Description: Lemma for cnlnadji . By riesz4 , B is the unique vector such that ( Tv ) .ih y ) = ( v .ih w ) for all v . (Contributed by NM, 17-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 ${⊢}{T}\in \mathrm{LinOp}$
cnlnadjlem.2 ${⊢}{T}\in \mathrm{ContOp}$
cnlnadjlem.3 ${⊢}{G}=\left({g}\in ℋ⟼{T}\left({g}\right){\cdot }_{\mathrm{ih}}{y}\right)$
cnlnadjlem.4 ${⊢}{B}=\left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
Assertion cnlnadjlem3 ${⊢}{y}\in ℋ\to {B}\in ℋ$

### Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 ${⊢}{T}\in \mathrm{LinOp}$
2 cnlnadjlem.2 ${⊢}{T}\in \mathrm{ContOp}$
3 cnlnadjlem.3 ${⊢}{G}=\left({g}\in ℋ⟼{T}\left({g}\right){\cdot }_{\mathrm{ih}}{y}\right)$
4 cnlnadjlem.4 ${⊢}{B}=\left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
5 1 2 3 cnlnadjlem2 ${⊢}{y}\in ℋ\to \left({G}\in \mathrm{LinFn}\wedge {G}\in \mathrm{ContFn}\right)$
6 elin ${⊢}{G}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)↔\left({G}\in \mathrm{LinFn}\wedge {G}\in \mathrm{ContFn}\right)$
7 5 6 sylibr ${⊢}{y}\in ℋ\to {G}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)$
8 riesz4 ${⊢}{G}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}$
9 7 8 syl ${⊢}{y}\in ℋ\to \exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}$
10 1 2 3 cnlnadjlem1 ${⊢}{v}\in ℋ\to {G}\left({v}\right)={T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}$
11 10 eqeq1d ${⊢}{v}\in ℋ\to \left({G}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}↔{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)$
12 11 ralbiia ${⊢}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}↔\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}$
13 12 reubii ${⊢}\exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({v}\right)={v}{\cdot }_{\mathrm{ih}}{w}↔\exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}$
14 9 13 sylib ${⊢}{y}\in ℋ\to \exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}$
15 riotacl ${⊢}\exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\to \left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)\in ℋ$
16 14 15 syl ${⊢}{y}\in ℋ\to \left(\iota {w}\in ℋ|\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}\right)\in ℋ$
17 4 16 eqeltrid ${⊢}{y}\in ℋ\to {B}\in ℋ$