Metamath Proof Explorer

Theorem 0lno

Description: The zero operator is linear. (Contributed by NM, 28-Nov-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses 0lno.0 ⊢ Z = U 0 op W
0lno.7 ⊢ L = U LnOp W
Assertion 0lno ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z ∈ L

Proof

Step Hyp Ref Expression
1 0lno.0 ⊢ Z = U 0 op W
2 0lno.7 ⊢ L = U LnOp W
3 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
4 eqid ⊢ BaseSet ⁡ W = BaseSet ⁡ W
5 3 4 1 0oo ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z : BaseSet ⁡ U ⟶ BaseSet ⁡ W
6 simplll ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → U ∈ NrmCVec
7 simpllr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → W ∈ NrmCVec
8 simplr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → x ∈ ℂ
9 simprl ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → y ∈ BaseSet ⁡ U
10 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
11 3 10 nvscl ⊢ U ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U → x ⋅ 𝑠OLD ⁡ U y ∈ BaseSet ⁡ U
12 6 8 9 11 syl3anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → x ⋅ 𝑠OLD ⁡ U y ∈ BaseSet ⁡ U
13 simprr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → z ∈ BaseSet ⁡ U
14 eqid ⊢ + v ⁡ U = + v ⁡ U
15 3 14 nvgcl ⊢ U ∈ NrmCVec ∧ x ⋅ 𝑠OLD ⁡ U y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → x ⋅ 𝑠OLD ⁡ U y + v ⁡ U z ∈ BaseSet ⁡ U
16 6 12 13 15 syl3anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → x ⋅ 𝑠OLD ⁡ U y + v ⁡ U z ∈ BaseSet ⁡ U
17 eqid ⊢ 0 vec ⁡ W = 0 vec ⁡ W
18 3 17 1 0oval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ⋅ 𝑠OLD ⁡ U y + v ⁡ U z ∈ BaseSet ⁡ U → Z ⁡ x ⋅ 𝑠OLD ⁡ U y + v ⁡ U z = 0 vec ⁡ W
19 6 7 16 18 syl3anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → Z ⁡ x ⋅ 𝑠OLD ⁡ U y + v ⁡ U z = 0 vec ⁡ W
20 3 17 1 0oval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ y ∈ BaseSet ⁡ U → Z ⁡ y = 0 vec ⁡ W
21 6 7 9 20 syl3anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → Z ⁡ y = 0 vec ⁡ W
22 21 oveq2d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → x ⋅ 𝑠OLD ⁡ W Z ⁡ y = x ⋅ 𝑠OLD ⁡ W 0 vec ⁡ W
23 3 17 1 0oval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ z ∈ BaseSet ⁡ U → Z ⁡ z = 0 vec ⁡ W
24 6 7 13 23 syl3anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → Z ⁡ z = 0 vec ⁡ W
25 22 24 oveq12d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → x ⋅ 𝑠OLD ⁡ W Z ⁡ y + v ⁡ W Z ⁡ z = x ⋅ 𝑠OLD ⁡ W 0 vec ⁡ W + v ⁡ W 0 vec ⁡ W
26 eqid ⊢ ⋅ 𝑠OLD ⁡ W = ⋅ 𝑠OLD ⁡ W
27 26 17 nvsz ⊢ W ∈ NrmCVec ∧ x ∈ ℂ → x ⋅ 𝑠OLD ⁡ W 0 vec ⁡ W = 0 vec ⁡ W
28 7 8 27 syl2anc ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → x ⋅ 𝑠OLD ⁡ W 0 vec ⁡ W = 0 vec ⁡ W
29 28 oveq1d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → x ⋅ 𝑠OLD ⁡ W 0 vec ⁡ W + v ⁡ W 0 vec ⁡ W = 0 vec ⁡ W + v ⁡ W 0 vec ⁡ W
30 4 17 nvzcl ⊢ W ∈ NrmCVec → 0 vec ⁡ W ∈ BaseSet ⁡ W
31 eqid ⊢ + v ⁡ W = + v ⁡ W
32 4 31 17 nv0rid ⊢ W ∈ NrmCVec ∧ 0 vec ⁡ W ∈ BaseSet ⁡ W → 0 vec ⁡ W + v ⁡ W 0 vec ⁡ W = 0 vec ⁡ W
33 7 30 32 syl2anc2 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → 0 vec ⁡ W + v ⁡ W 0 vec ⁡ W = 0 vec ⁡ W
34 25 29 33 3eqtrd ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → x ⋅ 𝑠OLD ⁡ W Z ⁡ y + v ⁡ W Z ⁡ z = 0 vec ⁡ W
35 19 34 eqtr4d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ ∧ y ∈ BaseSet ⁡ U ∧ z ∈ BaseSet ⁡ U → Z ⁡ x ⋅ 𝑠OLD ⁡ U y + v ⁡ U z = x ⋅ 𝑠OLD ⁡ W Z ⁡ y + v ⁡ W Z ⁡ z
36 35 ralrimivva ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ x ∈ ℂ → ∀ y ∈ BaseSet ⁡ U ∀ z ∈ BaseSet ⁡ U Z ⁡ x ⋅ 𝑠OLD ⁡ U y + v ⁡ U z = x ⋅ 𝑠OLD ⁡ W Z ⁡ y + v ⁡ W Z ⁡ z
37 36 ralrimiva ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → ∀ x ∈ ℂ ∀ y ∈ BaseSet ⁡ U ∀ z ∈ BaseSet ⁡ U Z ⁡ x ⋅ 𝑠OLD ⁡ U y + v ⁡ U z = x ⋅ 𝑠OLD ⁡ W Z ⁡ y + v ⁡ W Z ⁡ z
38 3 4 14 31 10 26 2 islno ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z ∈ L ↔ Z : BaseSet ⁡ U ⟶ BaseSet ⁡ W ∧ ∀ x ∈ ℂ ∀ y ∈ BaseSet ⁡ U ∀ z ∈ BaseSet ⁡ U Z ⁡ x ⋅ 𝑠OLD ⁡ U y + v ⁡ U z = x ⋅ 𝑠OLD ⁡ W Z ⁡ y + v ⁡ W Z ⁡ z
39 5 37 38 mpbir2and ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z ∈ L