# Metamath Proof Explorer

Description: Lemma for cnlnadji . F is an adjoint of T (later, we will show it is unique). (Contributed by NM, 18-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)$
cnlnadjlem.5 ${⊢}{F}=\left({y}\in ℋ⟼{B}\right)$
Assertion cnlnadjlem5 ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left({C}\right){\cdot }_{\mathrm{ih}}{A}={C}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)$

### 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 cnlnadjlem.5 ${⊢}{F}=\left({y}\in ℋ⟼{B}\right)$
6 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
7 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}ℋ$
8 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{f}$
9 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{\cdot }_{\mathrm{ih}}$
10 nfmpt1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in ℋ⟼{B}\right)$
11 5 10 nfcxfr ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{F}$
12 11 6 nffv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{F}\left({A}\right)$
13 8 9 12 nfov ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left({f}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)\right)$
14 13 nfeq2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{A}={f}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
15 7 14 nfralw ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{A}={f}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
16 oveq2 ${⊢}{y}={A}\to {T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({f}\right){\cdot }_{\mathrm{ih}}{A}$
17 fveq2 ${⊢}{y}={A}\to {F}\left({y}\right)={F}\left({A}\right)$
18 17 oveq2d ${⊢}{y}={A}\to {f}{\cdot }_{\mathrm{ih}}{F}\left({y}\right)={f}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
19 16 18 eqeq12d ${⊢}{y}={A}\to \left({T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{F}\left({y}\right)↔{T}\left({f}\right){\cdot }_{\mathrm{ih}}{A}={f}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)\right)$
20 19 ralbidv ${⊢}{y}={A}\to \left(\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{F}\left({y}\right)↔\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{A}={f}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)\right)$
21 riotaex ${⊢}\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 \mathrm{V}$
22 4 21 eqeltri ${⊢}{B}\in \mathrm{V}$
23 5 fvmpt2 ${⊢}\left({y}\in ℋ\wedge {B}\in \mathrm{V}\right)\to {F}\left({y}\right)={B}$
24 22 23 mpan2 ${⊢}{y}\in ℋ\to {F}\left({y}\right)={B}$
25 fveq2 ${⊢}{v}={f}\to {T}\left({v}\right)={T}\left({f}\right)$
26 25 oveq1d ${⊢}{v}={f}\to {T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}$
27 oveq1 ${⊢}{v}={f}\to {v}{\cdot }_{\mathrm{ih}}{w}={f}{\cdot }_{\mathrm{ih}}{w}$
28 26 27 eqeq12d ${⊢}{v}={f}\to \left({T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}↔{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{w}\right)$
29 28 cbvralvw ${⊢}\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}↔\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{w}$
30 29 a1i ${⊢}{w}\in ℋ\to \left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}↔\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{w}\right)$
31 1 2 3 cnlnadjlem1 ${⊢}{f}\in ℋ\to {G}\left({f}\right)={T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}$
32 31 eqeq1d ${⊢}{f}\in ℋ\to \left({G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}↔{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{w}\right)$
33 32 ralbiia ${⊢}\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}↔\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{w}$
34 30 33 syl6bbr ${⊢}{w}\in ℋ\to \left(\forall {v}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({v}\right){\cdot }_{\mathrm{ih}}{y}={v}{\cdot }_{\mathrm{ih}}{w}↔\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right)$
35 34 riotabiia ${⊢}\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)=\left(\iota {w}\in ℋ|\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right)$
36 4 35 eqtri ${⊢}{B}=\left(\iota {w}\in ℋ|\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right)$
37 1 2 3 cnlnadjlem2 ${⊢}{y}\in ℋ\to \left({G}\in \mathrm{LinFn}\wedge {G}\in \mathrm{ContFn}\right)$
38 elin ${⊢}{G}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)↔\left({G}\in \mathrm{LinFn}\wedge {G}\in \mathrm{ContFn}\right)$
39 37 38 sylibr ${⊢}{y}\in ℋ\to {G}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)$
40 riesz4 ${⊢}{G}\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)\to \exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}$
41 riotacl2 ${⊢}\exists !{w}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\to \left(\iota {w}\in ℋ|\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right)\in \left\{{w}\in ℋ|\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right\}$
42 39 40 41 3syl ${⊢}{y}\in ℋ\to \left(\iota {w}\in ℋ|\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right)\in \left\{{w}\in ℋ|\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right\}$
43 36 42 eqeltrid ${⊢}{y}\in ℋ\to {B}\in \left\{{w}\in ℋ|\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right\}$
44 24 43 eqeltrd ${⊢}{y}\in ℋ\to {F}\left({y}\right)\in \left\{{w}\in ℋ|\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right\}$
45 oveq2 ${⊢}{w}={F}\left({y}\right)\to {f}{\cdot }_{\mathrm{ih}}{w}={f}{\cdot }_{\mathrm{ih}}{F}\left({y}\right)$
46 45 eqeq2d ${⊢}{w}={F}\left({y}\right)\to \left({T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{w}↔{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{F}\left({y}\right)\right)$
47 46 ralbidv ${⊢}{w}={F}\left({y}\right)\to \left(\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{w}↔\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{F}\left({y}\right)\right)$
48 33 47 syl5bb ${⊢}{w}={F}\left({y}\right)\to \left(\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}↔\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{F}\left({y}\right)\right)$
49 48 elrab ${⊢}{F}\left({y}\right)\in \left\{{w}\in ℋ|\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right\}↔\left({F}\left({y}\right)\in ℋ\wedge \forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{F}\left({y}\right)\right)$
50 49 simprbi ${⊢}{F}\left({y}\right)\in \left\{{w}\in ℋ|\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{G}\left({f}\right)={f}{\cdot }_{\mathrm{ih}}{w}\right\}\to \forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{F}\left({y}\right)$
51 44 50 syl ${⊢}{y}\in ℋ\to \forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{y}={f}{\cdot }_{\mathrm{ih}}{F}\left({y}\right)$
52 6 15 20 51 vtoclgaf ${⊢}{A}\in ℋ\to \forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{A}={f}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
53 fveq2 ${⊢}{f}={C}\to {T}\left({f}\right)={T}\left({C}\right)$
54 53 oveq1d ${⊢}{f}={C}\to {T}\left({f}\right){\cdot }_{\mathrm{ih}}{A}={T}\left({C}\right){\cdot }_{\mathrm{ih}}{A}$
55 oveq1 ${⊢}{f}={C}\to {f}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)={C}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
56 54 55 eqeq12d ${⊢}{f}={C}\to \left({T}\left({f}\right){\cdot }_{\mathrm{ih}}{A}={f}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)↔{T}\left({C}\right){\cdot }_{\mathrm{ih}}{A}={C}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)\right)$
57 56 rspccva ${⊢}\left(\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({f}\right){\cdot }_{\mathrm{ih}}{A}={f}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)\wedge {C}\in ℋ\right)\to {T}\left({C}\right){\cdot }_{\mathrm{ih}}{A}={C}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)$
58 52 57 sylan ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\right)\to {T}\left({C}\right){\cdot }_{\mathrm{ih}}{A}={C}{\cdot }_{\mathrm{ih}}{F}\left({A}\right)$