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=ULnOpW
Assertion lno0 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈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=ULnOpW
6 neg1cn ⊢−1∈ℂ
7 6 a1i ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→−1∈ℂ
8 1 3 nvzcl ⊢U∈NrmCVec→Q∈X
9 8 3ad2ant1 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→Q∈X
10 7 9 9 3jca ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→−1∈ℂ∧Q∈X∧Q∈X
11 eqid ⊢+v⁡U=+v⁡U
12 eqid ⊢+v⁡W=+v⁡W
13 eqid ⊢⋅𝑠OLD⁡U=⋅𝑠OLD⁡U
14 eqid ⊢⋅𝑠OLD⁡W=⋅𝑠OLD⁡W
15 1 2 11 12 13 14 5 lnolin ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L∧−1∈ℂ∧Q∈X∧Q∈X→T⁡-1⋅𝑠OLD⁡UQ+v⁡UQ=-1⋅𝑠OLD⁡WT⁡Q+v⁡WT⁡Q
16 10 15 mpdan ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→T⁡-1⋅𝑠OLD⁡UQ+v⁡UQ=-1⋅𝑠OLD⁡WT⁡Q+v⁡WT⁡Q
17 1 11 13 3 nvlinv ⊢U∈NrmCVec∧Q∈X→-1⋅𝑠OLD⁡UQ+v⁡UQ=Q
18 8 17 mpdan ⊢U∈NrmCVec→-1⋅𝑠OLD⁡UQ+v⁡UQ=Q
19 18 fveq2d ⊢U∈NrmCVec→T⁡-1⋅𝑠OLD⁡UQ+v⁡UQ=T⁡Q
20 19 3ad2ant1 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→T⁡-1⋅𝑠OLD⁡UQ+v⁡UQ=T⁡Q
21 simp2 ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→W∈NrmCVec
22 1 2 5 lnof ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→T:X⟶Y
23 22 9 ffvelcdmd ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→T⁡Q∈Y
24 2 12 14 4 nvlinv ⊢W∈NrmCVec∧T⁡Q∈Y→-1⋅𝑠OLD⁡WT⁡Q+v⁡WT⁡Q=Z
25 21 23 24 syl2anc ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→-1⋅𝑠OLD⁡WT⁡Q+v⁡WT⁡Q=Z
26 16 20 25 3eqtr3d ⊢U∈NrmCVec∧W∈NrmCVec∧T∈L→T⁡Q=Z