# Metamath Proof Explorer

Description: Lemma for cnlnadji . F is linear. (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)$
cnlnadjlem.5 ${⊢}{F}=\left({y}\in ℋ⟼{B}\right)$
Assertion cnlnadjlem6 ${⊢}{F}\in \mathrm{LinOp}$

### 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 1 2 3 4 cnlnadjlem3 ${⊢}{y}\in ℋ\to {B}\in ℋ$
7 5 6 fmpti ${⊢}{F}:ℋ⟶ℋ$
8 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
9 8 ffvelrni ${⊢}{t}\in ℋ\to {T}\left({t}\right)\in ℋ$
10 9 adantl ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {T}\left({t}\right)\in ℋ$
11 hvmulcl ${⊢}\left({x}\in ℂ\wedge {f}\in ℋ\right)\to {x}{\cdot }_{ℎ}{f}\in ℋ$
12 11 ad2antrr ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {x}{\cdot }_{ℎ}{f}\in ℋ$
13 simplr ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {z}\in ℋ$
14 his7 ${⊢}\left({T}\left({t}\right)\in ℋ\wedge {x}{\cdot }_{ℎ}{f}\in ℋ\wedge {z}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)=\left({T}\left({t}\right){\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{f}\right)\right)+\left({T}\left({t}\right){\cdot }_{\mathrm{ih}}{z}\right)$
15 10 12 13 14 syl3anc ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)=\left({T}\left({t}\right){\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{f}\right)\right)+\left({T}\left({t}\right){\cdot }_{\mathrm{ih}}{z}\right)$
16 hvaddcl ${⊢}\left({x}{\cdot }_{ℎ}{f}\in ℋ\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\in ℋ$
17 11 16 sylan ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\in ℋ$
18 1 2 3 4 5 cnlnadjlem5 ${⊢}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\in ℋ\wedge {t}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)={t}{\cdot }_{\mathrm{ih}}{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)$
19 17 18 sylan ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)={t}{\cdot }_{\mathrm{ih}}{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)$
20 simpll ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to {x}\in ℂ$
21 9 adantl ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to {T}\left({t}\right)\in ℋ$
22 simplr ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to {f}\in ℋ$
23 his5 ${⊢}\left({x}\in ℂ\wedge {T}\left({t}\right)\in ℋ\wedge {f}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{f}\right)=\stackrel{‾}{{x}}\left({T}\left({t}\right){\cdot }_{\mathrm{ih}}{f}\right)$
24 20 21 22 23 syl3anc ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{f}\right)=\stackrel{‾}{{x}}\left({T}\left({t}\right){\cdot }_{\mathrm{ih}}{f}\right)$
25 simpr ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to {t}\in ℋ$
26 1 2 3 4 5 cnlnadjlem4 ${⊢}{f}\in ℋ\to {F}\left({f}\right)\in ℋ$
27 26 ad2antlr ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to {F}\left({f}\right)\in ℋ$
28 his5 ${⊢}\left({x}\in ℂ\wedge {t}\in ℋ\wedge {F}\left({f}\right)\in ℋ\right)\to {t}{\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right)=\stackrel{‾}{{x}}\left({t}{\cdot }_{\mathrm{ih}}{F}\left({f}\right)\right)$
29 20 25 27 28 syl3anc ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to {t}{\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right)=\stackrel{‾}{{x}}\left({t}{\cdot }_{\mathrm{ih}}{F}\left({f}\right)\right)$
30 1 2 3 4 5 cnlnadjlem5 ${⊢}\left({f}\in ℋ\wedge {t}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}{f}={t}{\cdot }_{\mathrm{ih}}{F}\left({f}\right)$
31 30 adantll ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}{f}={t}{\cdot }_{\mathrm{ih}}{F}\left({f}\right)$
32 31 oveq2d ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to \stackrel{‾}{{x}}\left({T}\left({t}\right){\cdot }_{\mathrm{ih}}{f}\right)=\stackrel{‾}{{x}}\left({t}{\cdot }_{\mathrm{ih}}{F}\left({f}\right)\right)$
33 29 32 eqtr4d ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to {t}{\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right)=\stackrel{‾}{{x}}\left({T}\left({t}\right){\cdot }_{\mathrm{ih}}{f}\right)$
34 24 33 eqtr4d ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {t}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{f}\right)={t}{\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right)$
35 34 adantlr ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{f}\right)={t}{\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right)$
36 1 2 3 4 5 cnlnadjlem5 ${⊢}\left({z}\in ℋ\wedge {t}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}{z}={t}{\cdot }_{\mathrm{ih}}{F}\left({z}\right)$
37 36 adantll ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {T}\left({t}\right){\cdot }_{\mathrm{ih}}{z}={t}{\cdot }_{\mathrm{ih}}{F}\left({z}\right)$
38 35 37 oveq12d ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to \left({T}\left({t}\right){\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{f}\right)\right)+\left({T}\left({t}\right){\cdot }_{\mathrm{ih}}{z}\right)=\left({t}{\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right)\right)+\left({t}{\cdot }_{\mathrm{ih}}{F}\left({z}\right)\right)$
39 simpr ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {t}\in ℋ$
40 hvmulcl ${⊢}\left({x}\in ℂ\wedge {F}\left({f}\right)\in ℋ\right)\to {x}{\cdot }_{ℎ}{F}\left({f}\right)\in ℋ$
41 26 40 sylan2 ${⊢}\left({x}\in ℂ\wedge {f}\in ℋ\right)\to {x}{\cdot }_{ℎ}{F}\left({f}\right)\in ℋ$
42 41 ad2antrr ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {x}{\cdot }_{ℎ}{F}\left({f}\right)\in ℋ$
43 1 2 3 4 5 cnlnadjlem4 ${⊢}{z}\in ℋ\to {F}\left({z}\right)\in ℋ$
44 43 ad2antlr ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {F}\left({z}\right)\in ℋ$
45 his7 ${⊢}\left({t}\in ℋ\wedge {x}{\cdot }_{ℎ}{F}\left({f}\right)\in ℋ\wedge {F}\left({z}\right)\in ℋ\right)\to {t}{\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\right)=\left({t}{\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right)\right)+\left({t}{\cdot }_{\mathrm{ih}}{F}\left({z}\right)\right)$
46 39 42 44 45 syl3anc ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {t}{\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\right)=\left({t}{\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right)\right)+\left({t}{\cdot }_{\mathrm{ih}}{F}\left({z}\right)\right)$
47 38 46 eqtr4d ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to \left({T}\left({t}\right){\cdot }_{\mathrm{ih}}\left({x}{\cdot }_{ℎ}{f}\right)\right)+\left({T}\left({t}\right){\cdot }_{\mathrm{ih}}{z}\right)={t}{\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\right)$
48 15 19 47 3eqtr3d ${⊢}\left(\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\wedge {t}\in ℋ\right)\to {t}{\cdot }_{\mathrm{ih}}{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)={t}{\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\right)$
49 48 ralrimiva ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\to \forall {t}\in ℋ\phantom{\rule{.4em}{0ex}}{t}{\cdot }_{\mathrm{ih}}{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)={t}{\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\right)$
50 1 2 3 4 5 cnlnadjlem4 ${⊢}\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\in ℋ\to {F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)\in ℋ$
51 17 50 syl ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\to {F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)\in ℋ$
52 hvaddcl ${⊢}\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\in ℋ\wedge {F}\left({z}\right)\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\in ℋ$
53 41 43 52 syl2an ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\in ℋ$
54 hial2eq2 ${⊢}\left({F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)\in ℋ\wedge \left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\in ℋ\right)\to \left(\forall {t}\in ℋ\phantom{\rule{.4em}{0ex}}{t}{\cdot }_{\mathrm{ih}}{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)={t}{\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\right)↔{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\right)$
55 51 53 54 syl2anc ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\to \left(\forall {t}\in ℋ\phantom{\rule{.4em}{0ex}}{t}{\cdot }_{\mathrm{ih}}{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)={t}{\cdot }_{\mathrm{ih}}\left(\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\right)↔{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\right)$
56 49 55 mpbid ${⊢}\left(\left({x}\in ℂ\wedge {f}\in ℋ\right)\wedge {z}\in ℋ\right)\to {F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)$
57 56 ralrimiva ${⊢}\left({x}\in ℂ\wedge {f}\in ℋ\right)\to \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)$
58 57 rgen2 ${⊢}\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)$
59 ellnop ${⊢}{F}\in \mathrm{LinOp}↔\left({F}:ℋ⟶ℋ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {f}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}{F}\left(\left({x}{\cdot }_{ℎ}{f}\right){+}_{ℎ}{z}\right)=\left({x}{\cdot }_{ℎ}{F}\left({f}\right)\right){+}_{ℎ}{F}\left({z}\right)\right)$
60 7 58 59 mpbir2an ${⊢}{F}\in \mathrm{LinOp}$