# 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` ( ( -u 1 ( .sOLD ` U ) Q ) ( +v ` U ) Q ) ) = ( T ` Q ) )`
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> W e. NrmCVec )`
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> Y )`
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` Q ) e. Y )`
` |-  ( ( W e. NrmCVec /\ ( T ` Q ) e. Y ) -> ( ( -u 1 ( .sOLD ` W ) ( T ` Q ) ) ( +v ` W ) ( T ` Q ) ) = Z )`
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( ( -u 1 ( .sOLD ` W ) ( T ` Q ) ) ( +v ` W ) ( T ` Q ) ) = Z )`
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` Q ) = Z )`