# Metamath Proof Explorer

## Theorem lnof

Description: A linear operator is a mapping. (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 18-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lnof.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
lnof.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
lnof.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
Assertion lnof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}:{X}⟶{Y}$

### Proof

Step Hyp Ref Expression
1 lnof.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 lnof.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 lnof.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
4 eqid ${⊢}{+}_{v}\left({U}\right)={+}_{v}\left({U}\right)$
5 eqid ${⊢}{+}_{v}\left({W}\right)={+}_{v}\left({W}\right)$
6 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
7 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
8 1 2 4 5 6 7 3 islno ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {L}↔\left({T}:{X}⟶{Y}\wedge \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}{\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)$
9 8 simprbda ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {T}\in {L}\right)\to {T}:{X}⟶{Y}$
10 9 3impa ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}:{X}⟶{Y}$