# 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 = ( BaseSet ` U )`
lnof.2
`|- Y = ( BaseSet ` W )`
lnof.7
`|- L = ( U LnOp W )`
Assertion lnof
`|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> Y )`

### Proof

Step Hyp Ref Expression
1 lnof.1
` |-  X = ( BaseSet ` U )`
2 lnof.2
` |-  Y = ( BaseSet ` W )`
3 lnof.7
` |-  L = ( U LnOp W )`
4 eqid
` |-  ( +v ` U ) = ( +v ` U )`
5 eqid
` |-  ( +v ` W ) = ( +v ` W )`
6 eqid
` |-  ( .sOLD ` U ) = ( .sOLD ` U )`
7 eqid
` |-  ( .sOLD ` W ) = ( .sOLD ` W )`
8 1 2 4 5 6 7 3 islno
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. L <-> ( T : X --> Y /\ A. x e. CC A. y e. X A. z e. X ( T ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` W ) ( T ` y ) ) ( +v ` W ) ( T ` z ) ) ) ) )`
9 8 simprbda
` |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ T e. L ) -> T : X --> Y )`
10 9 3impa
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> Y )`