This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtr4di ⊢ 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 eqtr4di ⊢ 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 eqtrid ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → O = X × Z