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=BaseSetU
0oval.6 Z=0vecW
0oval.0 O=U0opW
Assertion 0ofval UNrmCVecWNrmCVecO=X×Z

Proof

Step Hyp Ref Expression
1 0oval.1 X=BaseSetU
2 0oval.6 Z=0vecW
3 0oval.0 O=U0opW
4 fveq2 u=UBaseSetu=BaseSetU
5 4 1 eqtr4di u=UBaseSetu=X
6 5 xpeq1d u=UBaseSetu×0vecw=X×0vecw
7 fveq2 w=W0vecw=0vecW
8 7 2 eqtr4di w=W0vecw=Z
9 8 sneqd w=W0vecw=Z
10 9 xpeq2d w=WX×0vecw=X×Z
11 df-0o 0op=uNrmCVec,wNrmCVecBaseSetu×0vecw
12 1 fvexi XV
13 snex ZV
14 12 13 xpex X×ZV
15 6 10 11 14 ovmpo UNrmCVecWNrmCVecU0opW=X×Z
16 3 15 eqtrid UNrmCVecWNrmCVecO=X×Z