# Metamath Proof Explorer

## Theorem 0oval

Description: Value of the zero operator. (Contributed by NM, 28-Nov-2007) (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 0oval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {A}\in {X}\right)\to {O}\left({A}\right)={Z}$

### 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 1 2 3 0ofval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {O}={X}×\left\{{Z}\right\}$
5 4 fveq1d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {O}\left({A}\right)=\left({X}×\left\{{Z}\right\}\right)\left({A}\right)$
6 5 3adant3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {A}\in {X}\right)\to {O}\left({A}\right)=\left({X}×\left\{{Z}\right\}\right)\left({A}\right)$
7 2 fvexi ${⊢}{Z}\in \mathrm{V}$
8 7 fvconst2 ${⊢}{A}\in {X}\to \left({X}×\left\{{Z}\right\}\right)\left({A}\right)={Z}$
9 8 3ad2ant3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {A}\in {X}\right)\to \left({X}×\left\{{Z}\right\}\right)\left({A}\right)={Z}$
10 6 9 eqtrd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {A}\in {X}\right)\to {O}\left({A}\right)={Z}$