# Metamath Proof Explorer

## Theorem 0ofval

Description: The zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses 0oval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
0oval.6 ${⊢}{Z}={0}_{\mathrm{vec}}\left({W}\right)$
0oval.0 ${⊢}{O}={U}{0}_{\mathrm{op}}{W}$
Assertion 0ofval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {O}={X}×\left\{{Z}\right\}$

### Proof

Step Hyp Ref Expression
1 0oval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 0oval.6 ${⊢}{Z}={0}_{\mathrm{vec}}\left({W}\right)$
3 0oval.0 ${⊢}{O}={U}{0}_{\mathrm{op}}{W}$
4 fveq2 ${⊢}{u}={U}\to \mathrm{BaseSet}\left({u}\right)=\mathrm{BaseSet}\left({U}\right)$
5 4 1 syl6eqr ${⊢}{u}={U}\to \mathrm{BaseSet}\left({u}\right)={X}$
6 5 xpeq1d ${⊢}{u}={U}\to \mathrm{BaseSet}\left({u}\right)×\left\{{0}_{\mathrm{vec}}\left({w}\right)\right\}={X}×\left\{{0}_{\mathrm{vec}}\left({w}\right)\right\}$
7 fveq2 ${⊢}{w}={W}\to {0}_{\mathrm{vec}}\left({w}\right)={0}_{\mathrm{vec}}\left({W}\right)$
8 7 2 syl6eqr ${⊢}{w}={W}\to {0}_{\mathrm{vec}}\left({w}\right)={Z}$
9 8 sneqd ${⊢}{w}={W}\to \left\{{0}_{\mathrm{vec}}\left({w}\right)\right\}=\left\{{Z}\right\}$
10 9 xpeq2d ${⊢}{w}={W}\to {X}×\left\{{0}_{\mathrm{vec}}\left({w}\right)\right\}={X}×\left\{{Z}\right\}$
11 df-0o ${⊢}{0}_{\mathrm{op}}=\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\mathrm{BaseSet}\left({u}\right)×\left\{{0}_{\mathrm{vec}}\left({w}\right)\right\}\right)$
12 1 fvexi ${⊢}{X}\in \mathrm{V}$
13 snex ${⊢}\left\{{Z}\right\}\in \mathrm{V}$
14 12 13 xpex ${⊢}{X}×\left\{{Z}\right\}\in \mathrm{V}$
15 6 10 11 14 ovmpo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {U}{0}_{\mathrm{op}}{W}={X}×\left\{{Z}\right\}$
16 3 15 syl5eq ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {O}={X}×\left\{{Z}\right\}$