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 = 0 vec ⁡ U
lno0.z ⊢ Z = 0 vec ⁡ W
lno0.7 ⊢ L = U LnOp W
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 = 0 vec ⁡ U
4 lno0.z ⊢ Z = 0 vec ⁡ W
5 lno0.7 ⊢ L = U LnOp W
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 ⁡ U Q + v ⁡ U Q = -1 ⋅ 𝑠OLD ⁡ W T ⁡ Q + v ⁡ W T ⁡ Q
16 10 15 mpdan ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T ⁡ -1 ⋅ 𝑠OLD ⁡ U Q + v ⁡ U Q = -1 ⋅ 𝑠OLD ⁡ W T ⁡ Q + v ⁡ W T ⁡ Q
17 1 11 13 3 nvlinv ⊢ U ∈ NrmCVec ∧ Q ∈ X → -1 ⋅ 𝑠OLD ⁡ U Q + v ⁡ U Q = Q
18 8 17 mpdan ⊢ U ∈ NrmCVec → -1 ⋅ 𝑠OLD ⁡ U Q + v ⁡ U Q = Q
19 18 fveq2d ⊢ U ∈ NrmCVec → T ⁡ -1 ⋅ 𝑠OLD ⁡ U Q + v ⁡ U Q = T ⁡ Q
20 19 3ad2ant1 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T ⁡ -1 ⋅ 𝑠OLD ⁡ U Q + v ⁡ U Q = 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 ffvelrnd ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T ⁡ Q ∈ Y
24 2 12 14 4 nvlinv ⊢ W ∈ NrmCVec ∧ T ⁡ Q ∈ Y → -1 ⋅ 𝑠OLD ⁡ W T ⁡ Q + v ⁡ W T ⁡ Q = Z
25 21 23 24 syl2anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → -1 ⋅ 𝑠OLD ⁡ W T ⁡ Q + v ⁡ W T ⁡ Q = Z
26 16 20 25 3eqtr3d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T ∈ L → T ⁡ Q = Z