# Metamath Proof Explorer

## Theorem 0oo

Description: The zero operator is an operator. (Contributed by NM, 28-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses 0oo.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
0oo.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
0oo.0 ${⊢}{Z}={U}{0}_{\mathrm{op}}{W}$
Assertion 0oo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {Z}:{X}⟶{Y}$

### Proof

Step Hyp Ref Expression
1 0oo.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 0oo.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 0oo.0 ${⊢}{Z}={U}{0}_{\mathrm{op}}{W}$
4 fvex ${⊢}{0}_{\mathrm{vec}}\left({W}\right)\in \mathrm{V}$
5 4 fconst ${⊢}\left({X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\right):{X}⟶\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}$
6 eqid ${⊢}{0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right)$
7 2 6 nvzcl ${⊢}{W}\in \mathrm{NrmCVec}\to {0}_{\mathrm{vec}}\left({W}\right)\in {Y}$
8 7 snssd ${⊢}{W}\in \mathrm{NrmCVec}\to \left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\subseteq {Y}$
9 fss ${⊢}\left(\left({X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\right):{X}⟶\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\wedge \left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\subseteq {Y}\right)\to \left({X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\right):{X}⟶{Y}$
10 5 8 9 sylancr ${⊢}{W}\in \mathrm{NrmCVec}\to \left({X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\right):{X}⟶{Y}$
11 10 adantl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\right):{X}⟶{Y}$
12 1 6 3 0ofval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {Z}={X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}$
13 12 feq1d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({Z}:{X}⟶{Y}↔\left({X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\right):{X}⟶{Y}\right)$
14 11 13 mpbird ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {Z}:{X}⟶{Y}$