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=BaseSetU
lno0.2 Y=BaseSetW
lno0.5 Q=0vecU
lno0.z Z=0vecW
lno0.7 L=ULnOpW
Assertion lno0 UNrmCVecWNrmCVecTLTQ=Z

Proof

Step Hyp Ref Expression
1 lno0.1 X=BaseSetU
2 lno0.2 Y=BaseSetW
3 lno0.5 Q=0vecU
4 lno0.z Z=0vecW
5 lno0.7 L=ULnOpW
6 neg1cn 1
7 6 a1i UNrmCVecWNrmCVecTL1
8 1 3 nvzcl UNrmCVecQX
9 8 3ad2ant1 UNrmCVecWNrmCVecTLQX
10 7 9 9 3jca UNrmCVecWNrmCVecTL1QXQX
11 eqid +vU=+vU
12 eqid +vW=+vW
13 eqid 𝑠OLDU=𝑠OLDU
14 eqid 𝑠OLDW=𝑠OLDW
15 1 2 11 12 13 14 5 lnolin UNrmCVecWNrmCVecTL1QXQXT-1𝑠OLDUQ+vUQ=-1𝑠OLDWTQ+vWTQ
16 10 15 mpdan UNrmCVecWNrmCVecTLT-1𝑠OLDUQ+vUQ=-1𝑠OLDWTQ+vWTQ
17 1 11 13 3 nvlinv UNrmCVecQX-1𝑠OLDUQ+vUQ=Q
18 8 17 mpdan UNrmCVec-1𝑠OLDUQ+vUQ=Q
19 18 fveq2d UNrmCVecT-1𝑠OLDUQ+vUQ=TQ
20 19 3ad2ant1 UNrmCVecWNrmCVecTLT-1𝑠OLDUQ+vUQ=TQ
21 simp2 UNrmCVecWNrmCVecTLWNrmCVec
22 1 2 5 lnof UNrmCVecWNrmCVecTLT:XY
23 22 9 ffvelcdmd UNrmCVecWNrmCVecTLTQY
24 2 12 14 4 nvlinv WNrmCVecTQY-1𝑠OLDWTQ+vWTQ=Z
25 21 23 24 syl2anc UNrmCVecWNrmCVecTL-1𝑠OLDWTQ+vWTQ=Z
26 16 20 25 3eqtr3d UNrmCVecWNrmCVecTLTQ=Z