Metamath Proof Explorer

Theorem lno0

Description: The value of a linear operator at zero is zero. (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 18-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses lno0.1 
|- X = ( BaseSet ` U )
lno0.2 
|- Y = ( BaseSet ` W )
lno0.5 
|- Q = ( 0vec ` U )
lno0.z 
|- Z = ( 0vec ` W )
lno0.7 
|- L = ( U LnOp W )
Assertion lno0 
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` Q ) = Z )

Proof

Step Hyp Ref Expression
1 lno0.1 
 |-  X = ( BaseSet ` U )
2 lno0.2 
 |-  Y = ( BaseSet ` W )
3 lno0.5 
 |-  Q = ( 0vec ` U )
4 lno0.z 
 |-  Z = ( 0vec ` W )
5 lno0.7 
 |-  L = ( U LnOp W )
6 neg1cn 
 |-  -u 1 e. CC
7 6 a1i 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> -u 1 e. CC )
8 1 3 nvzcl 
 |-  ( U e. NrmCVec -> Q e. X )
9 8 3ad2ant1 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> Q e. X )
10 7 9 9 3jca 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( -u 1 e. CC /\ Q e. X /\ Q e. X ) )
11 eqid 
 |-  ( +v ` U ) = ( +v ` U )
12 eqid 
 |-  ( +v ` W ) = ( +v ` W )
13 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
14 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
15 1 2 11 12 13 14 5 lnolin 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ ( -u 1 e. CC /\ Q e. X /\ Q e. X ) ) -> ( T ` ( ( -u 1 ( .sOLD ` U ) Q ) ( +v ` U ) Q ) ) = ( ( -u 1 ( .sOLD ` W ) ( T ` Q ) ) ( +v ` W ) ( T ` Q ) ) )
16 10 15 mpdan 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` ( ( -u 1 ( .sOLD ` U ) Q ) ( +v ` U ) Q ) ) = ( ( -u 1 ( .sOLD ` W ) ( T ` Q ) ) ( +v ` W ) ( T ` Q ) ) )
17 1 11 13 3 nvlinv 
 |-  ( ( U e. NrmCVec /\ Q e. X ) -> ( ( -u 1 ( .sOLD ` U ) Q ) ( +v ` U ) Q ) = Q )
18 8 17 mpdan 
 |-  ( U e. NrmCVec -> ( ( -u 1 ( .sOLD ` U ) Q ) ( +v ` U ) Q ) = Q )
19 18 fveq2d 
 |-  ( U e. NrmCVec -> ( T ` ( ( -u 1 ( .sOLD ` U ) Q ) ( +v ` U ) Q ) ) = ( T ` Q ) )
20 19 3ad2ant1 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` ( ( -u 1 ( .sOLD ` U ) Q ) ( +v ` U ) Q ) ) = ( T ` Q ) )
21 simp2 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> W e. NrmCVec )
22 1 2 5 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> Y )
23 22 9 ffvelcdmd 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` Q ) e. Y )
24 2 12 14 4 nvlinv 
 |-  ( ( W e. NrmCVec /\ ( T ` Q ) e. Y ) -> ( ( -u 1 ( .sOLD ` W ) ( T ` Q ) ) ( +v ` W ) ( T ` Q ) ) = Z )
25 21 23 24 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( ( -u 1 ( .sOLD ` W ) ( T ` Q ) ) ( +v ` W ) ( T ` Q ) ) = Z )
26 16 20 25 3eqtr3d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` Q ) = Z )