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 = BaseSet U
0oval.6 Z = 0 vec W
0oval.0 O = U 0 op W
Assertion 0ofval U NrmCVec W NrmCVec O = X × Z

Proof

Step Hyp Ref Expression
1 0oval.1 X = BaseSet U
2 0oval.6 Z = 0 vec W
3 0oval.0 O = U 0 op W
4 fveq2 u = U BaseSet u = BaseSet U
5 4 1 syl6eqr u = U BaseSet u = X
6 5 xpeq1d u = U BaseSet u × 0 vec w = X × 0 vec w
7 fveq2 w = W 0 vec w = 0 vec W
8 7 2 syl6eqr w = W 0 vec w = Z
9 8 sneqd w = W 0 vec w = Z
10 9 xpeq2d w = W X × 0 vec w = X × Z
11 df-0o 0 op = u NrmCVec , w NrmCVec BaseSet u × 0 vec w
12 1 fvexi X V
13 snex Z V
14 12 13 xpex X × Z V
15 6 10 11 14 ovmpo U NrmCVec W NrmCVec U 0 op W = X × Z
16 3 15 syl5eq U NrmCVec W NrmCVec O = X × Z