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 )