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\leftrightarrow \left(T:X⟶Y\wedge \forall x\in ℂ\forall y\in X\forall z\in XT\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$$