# 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}_{\mathrm{op}}{W}$
0lno.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
Assertion 0lno ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {Z}\in {L}$

### Proof

Step Hyp Ref Expression
1 0lno.0 ${⊢}{Z}={U}{0}_{\mathrm{op}}{W}$
2 0lno.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
3 eqid ${⊢}\mathrm{BaseSet}\left({U}\right)=\mathrm{BaseSet}\left({U}\right)$
4 eqid ${⊢}\mathrm{BaseSet}\left({W}\right)=\mathrm{BaseSet}\left({W}\right)$
5 3 4 1 0oo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {Z}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)$
6 simplll ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {U}\in \mathrm{NrmCVec}$
7 simpllr ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {W}\in \mathrm{NrmCVec}$
8 simplr ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {x}\in ℂ$
9 simprl ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {y}\in \mathrm{BaseSet}\left({U}\right)$
10 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
11 3 10 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {x}\in ℂ\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\to {x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\in \mathrm{BaseSet}\left({U}\right)$
12 6 8 9 11 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\in \mathrm{BaseSet}\left({U}\right)$
13 simprr ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {z}\in \mathrm{BaseSet}\left({U}\right)$
14 eqid ${⊢}{+}_{v}\left({U}\right)={+}_{v}\left({U}\right)$
15 3 14 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right){+}_{v}\left({U}\right){z}\in \mathrm{BaseSet}\left({U}\right)$
16 6 12 13 15 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right){+}_{v}\left({U}\right){z}\in \mathrm{BaseSet}\left({U}\right)$
17 eqid ${⊢}{0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right)$
18 3 17 1 0oval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge \left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right){+}_{v}\left({U}\right){z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {Z}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right){+}_{v}\left({U}\right){z}\right)={0}_{\mathrm{vec}}\left({W}\right)$
19 6 7 16 18 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {Z}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right){+}_{v}\left({U}\right){z}\right)={0}_{\mathrm{vec}}\left({W}\right)$
20 3 17 1 0oval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {y}\in \mathrm{BaseSet}\left({U}\right)\right)\to {Z}\left({y}\right)={0}_{\mathrm{vec}}\left({W}\right)$
21 6 7 9 20 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {Z}\left({y}\right)={0}_{\mathrm{vec}}\left({W}\right)$
22 21 oveq2d ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){Z}\left({y}\right)={x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)$
23 3 17 1 0oval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\to {Z}\left({z}\right)={0}_{\mathrm{vec}}\left({W}\right)$
24 6 7 13 23 syl3anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {Z}\left({z}\right)={0}_{\mathrm{vec}}\left({W}\right)$
25 22 24 oveq12d ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){Z}\left({y}\right)\right){+}_{v}\left({W}\right){Z}\left({z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)\right){+}_{v}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)$
26 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({W}\right)$
27 26 17 nvsz ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {x}\in ℂ\right)\to {x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right)$
28 7 8 27 syl2anc ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right)$
29 28 oveq1d ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)\right){+}_{v}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right){+}_{v}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)$
30 4 17 nvzcl ${⊢}{W}\in \mathrm{NrmCVec}\to {0}_{\mathrm{vec}}\left({W}\right)\in \mathrm{BaseSet}\left({W}\right)$
31 eqid ${⊢}{+}_{v}\left({W}\right)={+}_{v}\left({W}\right)$
32 4 31 17 nv0rid ${⊢}\left({W}\in \mathrm{NrmCVec}\wedge {0}_{\mathrm{vec}}\left({W}\right)\in \mathrm{BaseSet}\left({W}\right)\right)\to {0}_{\mathrm{vec}}\left({W}\right){+}_{v}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right)$
33 7 30 32 syl2anc2 ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {0}_{\mathrm{vec}}\left({W}\right){+}_{v}\left({W}\right){0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right)$
34 25 29 33 3eqtrd ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){Z}\left({y}\right)\right){+}_{v}\left({W}\right){Z}\left({z}\right)={0}_{\mathrm{vec}}\left({W}\right)$
35 19 34 eqtr4d ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\wedge \left({y}\in \mathrm{BaseSet}\left({U}\right)\wedge {z}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to {Z}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right){+}_{v}\left({U}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){Z}\left({y}\right)\right){+}_{v}\left({W}\right){Z}\left({z}\right)$
36 35 ralrimivva ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {x}\in ℂ\right)\to \forall {y}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}{Z}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right){+}_{v}\left({U}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){Z}\left({y}\right)\right){+}_{v}\left({W}\right){Z}\left({z}\right)$
37 36 ralrimiva ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}{Z}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right){+}_{v}\left({U}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){Z}\left({y}\right)\right){+}_{v}\left({W}\right){Z}\left({z}\right)$
38 3 4 14 31 10 26 2 islno ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({Z}\in {L}↔\left({Z}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}{Z}\left(\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right){+}_{v}\left({U}\right){z}\right)=\left({x}{\cdot }_{\mathrm{𝑠OLD}}\left({W}\right){Z}\left({y}\right)\right){+}_{v}\left({W}\right){Z}\left({z}\right)\right)\right)$
39 5 37 38 mpbir2and ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {Z}\in {L}$