This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )