# Metamath Proof Explorer

## Theorem lnoval

Description: The set of linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lnoval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
lnoval.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
lnoval.3 ${⊢}{G}={+}_{v}\left({U}\right)$
lnoval.4 ${⊢}{H}={+}_{v}\left({W}\right)$
lnoval.5 ${⊢}{R}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
lnoval.6 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
lnoval.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
Assertion lnoval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {L}=\left\{{t}\in \left({{Y}}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{t}\left({y}\right)\right){H}{t}\left({z}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 lnoval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 lnoval.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 lnoval.3 ${⊢}{G}={+}_{v}\left({U}\right)$
4 lnoval.4 ${⊢}{H}={+}_{v}\left({W}\right)$
5 lnoval.5 ${⊢}{R}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
6 lnoval.6 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
7 lnoval.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
8 fveq2 ${⊢}{u}={U}\to \mathrm{BaseSet}\left({u}\right)=\mathrm{BaseSet}\left({U}\right)$
9 8 1 syl6eqr ${⊢}{u}={U}\to \mathrm{BaseSet}\left({u}\right)={X}$
10 9 oveq2d ${⊢}{u}={U}\to {\mathrm{BaseSet}\left({w}\right)}^{\mathrm{BaseSet}\left({u}\right)}={\mathrm{BaseSet}\left({w}\right)}^{{X}}$
11 fveq2 ${⊢}{u}={U}\to {+}_{v}\left({u}\right)={+}_{v}\left({U}\right)$
12 11 3 syl6eqr ${⊢}{u}={U}\to {+}_{v}\left({u}\right)={G}$
13 fveq2 ${⊢}{u}={U}\to {\cdot }_{\mathrm{𝑠OLD}}\left({u}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
14 13 5 syl6eqr ${⊢}{u}={U}\to {\cdot }_{\mathrm{𝑠OLD}}\left({u}\right)={R}$
15 14 oveqd ${⊢}{u}={U}\to {x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}={x}{R}{y}$
16 eqidd ${⊢}{u}={U}\to {z}={z}$
17 12 15 16 oveq123d ${⊢}{u}={U}\to \left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}=\left({x}{R}{y}\right){G}{z}$
18 17 fveqeq2d ${⊢}{u}={U}\to \left({t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)↔{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right)$
19 9 18 raleqbidv ${⊢}{u}={U}\to \left(\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)↔\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right)$
20 9 19 raleqbidv ${⊢}{u}={U}\to \left(\forall {y}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right)$
21 20 ralbidv ${⊢}{u}={U}\to \left(\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)↔\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right)$
22 10 21 rabeqbidv ${⊢}{u}={U}\to \left\{{t}\in \left({\mathrm{BaseSet}\left({w}\right)}^{\mathrm{BaseSet}\left({u}\right)}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right\}=\left\{{t}\in \left({\mathrm{BaseSet}\left({w}\right)}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right\}$
23 fveq2 ${⊢}{w}={W}\to \mathrm{BaseSet}\left({w}\right)=\mathrm{BaseSet}\left({W}\right)$
24 23 2 syl6eqr ${⊢}{w}={W}\to \mathrm{BaseSet}\left({w}\right)={Y}$
25 24 oveq1d ${⊢}{w}={W}\to {\mathrm{BaseSet}\left({w}\right)}^{{X}}={{Y}}^{{X}}$
26 fveq2 ${⊢}{w}={W}\to {+}_{v}\left({w}\right)={+}_{v}\left({W}\right)$
27 26 4 syl6eqr ${⊢}{w}={W}\to {+}_{v}\left({w}\right)={H}$
28 fveq2 ${⊢}{w}={W}\to {\cdot }_{\mathrm{𝑠OLD}}\left({w}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
29 28 6 syl6eqr ${⊢}{w}={W}\to {\cdot }_{\mathrm{𝑠OLD}}\left({w}\right)={S}$
30 29 oveqd ${⊢}{w}={W}\to {x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)={x}{S}{t}\left({y}\right)$
31 eqidd ${⊢}{w}={W}\to {t}\left({z}\right)={t}\left({z}\right)$
32 27 30 31 oveq123d ${⊢}{w}={W}\to \left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)=\left({x}{S}{t}\left({y}\right)\right){H}{t}\left({z}\right)$
33 32 eqeq2d ${⊢}{w}={W}\to \left({t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)↔{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{t}\left({y}\right)\right){H}{t}\left({z}\right)\right)$
34 33 2ralbidv ${⊢}{w}={W}\to \left(\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)↔\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{t}\left({y}\right)\right){H}{t}\left({z}\right)\right)$
35 34 ralbidv ${⊢}{w}={W}\to \left(\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)↔\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{t}\left({y}\right)\right){H}{t}\left({z}\right)\right)$
36 25 35 rabeqbidv ${⊢}{w}={W}\to \left\{{t}\in \left({\mathrm{BaseSet}\left({w}\right)}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right\}=\left\{{t}\in \left({{Y}}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{t}\left({y}\right)\right){H}{t}\left({z}\right)\right\}$
37 df-lno ${⊢}\mathrm{LnOp}=\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\left\{{t}\in \left({\mathrm{BaseSet}\left({w}\right)}^{\mathrm{BaseSet}\left({u}\right)}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({u}\right)\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({u}\right){y}\right){+}_{v}\left({u}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({w}\right){t}\left({y}\right)\right){+}_{v}\left({w}\right){t}\left({z}\right)\right\}\right)$
38 ovex ${⊢}{{Y}}^{{X}}\in \mathrm{V}$
39 38 rabex ${⊢}\left\{{t}\in \left({{Y}}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{t}\left({y}\right)\right){H}{t}\left({z}\right)\right\}\in \mathrm{V}$
40 22 36 37 39 ovmpo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {U}\mathrm{LnOp}{W}=\left\{{t}\in \left({{Y}}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{t}\left({y}\right)\right){H}{t}\left({z}\right)\right\}$
41 7 40 syl5eq ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {L}=\left\{{t}\in \left({{Y}}^{{X}}\right)|\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}\forall {z}\in {X}\phantom{\rule{.4em}{0ex}}{t}\left(\left({x}{R}{y}\right){G}{z}\right)=\left({x}{S}{t}\left({y}\right)\right){H}{t}\left({z}\right)\right\}$