# 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}=\mathrm{BaseSet}\left({U}\right)$
lno0.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
lno0.5 ${⊢}{Q}={0}_{\mathrm{vec}}\left({U}\right)$
lno0.z ${⊢}{Z}={0}_{\mathrm{vec}}\left({W}\right)$
lno0.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
Assertion lno0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}\left({Q}\right)={Z}$

### Proof

Step Hyp Ref Expression
1 lno0.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 lno0.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 lno0.5 ${⊢}{Q}={0}_{\mathrm{vec}}\left({U}\right)$
4 lno0.z ${⊢}{Z}={0}_{\mathrm{vec}}\left({W}\right)$
5 lno0.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
6 neg1cn ${⊢}-1\in ℂ$
7 6 a1i ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to -1\in ℂ$
8 1 3 nvzcl ${⊢}{U}\in \mathrm{NrmCVec}\to {Q}\in {X}$
9 8 3ad2ant1 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {Q}\in {X}$
10 7 9 9 3jca ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left(-1\in ℂ\wedge {Q}\in {X}\wedge {Q}\in {X}\right)$
11 eqid ${⊢}{+}_{v}\left({U}\right)={+}_{v}\left({U}\right)$
12 eqid ${⊢}{+}_{v}\left({W}\right)={+}_{v}\left({W}\right)$
13 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
14 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
15 1 2 11 12 13 14 5 lnolin ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge \left(-1\in ℂ\wedge {Q}\in {X}\wedge {Q}\in {X}\right)\right)\to {T}\left(\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Q}\right){+}_{v}\left({U}\right){Q}\right)=\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){T}\left({Q}\right)\right){+}_{v}\left({W}\right){T}\left({Q}\right)$
16 10 15 mpdan ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}\left(\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Q}\right){+}_{v}\left({U}\right){Q}\right)=\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){T}\left({Q}\right)\right){+}_{v}\left({W}\right){T}\left({Q}\right)$
17 1 11 13 3 nvlinv ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {Q}\in {X}\right)\to \left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Q}\right){+}_{v}\left({U}\right){Q}={Q}$
18 8 17 mpdan ${⊢}{U}\in \mathrm{NrmCVec}\to \left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Q}\right){+}_{v}\left({U}\right){Q}={Q}$
19 18 fveq2d ${⊢}{U}\in \mathrm{NrmCVec}\to {T}\left(\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Q}\right){+}_{v}\left({U}\right){Q}\right)={T}\left({Q}\right)$
20 19 3ad2ant1 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}\left(\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){Q}\right){+}_{v}\left({U}\right){Q}\right)={T}\left({Q}\right)$
21 simp2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {W}\in \mathrm{NrmCVec}$
22 1 2 5 lnof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}:{X}⟶{Y}$
23 22 9 ffvelrnd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}\left({Q}\right)\in {Y}$
24 2 12 14 4 nvlinv ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {T}\left({Q}\right)\in {Y}\right)\to \left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){T}\left({Q}\right)\right){+}_{v}\left({W}\right){T}\left({Q}\right)={Z}$
25 21 23 24 syl2anc ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){T}\left({Q}\right)\right){+}_{v}\left({W}\right){T}\left({Q}\right)={Z}$
26 16 20 25 3eqtr3d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}\left({Q}\right)={Z}$