Metamath Proof Explorer

Theorem 0oo

Description: The zero operator is an operator. (Contributed by NM, 28-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses 0oo.1 ⊢ X = BaseSet ⁡ U
0oo.2 ⊢ Y = BaseSet ⁡ W
0oo.0 ⊢ Z = U 0 op W
Assertion 0oo ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z : X ⟶ Y

Proof

Step Hyp Ref Expression
1 0oo.1 ⊢ X = BaseSet ⁡ U
2 0oo.2 ⊢ Y = BaseSet ⁡ W
3 0oo.0 ⊢ Z = U 0 op W
4 fvex ⊢ 0 vec ⁡ W ∈ V
5 4 fconst ⊢ X × 0 vec ⁡ W : X ⟶ 0 vec ⁡ W
6 eqid ⊢ 0 vec ⁡ W = 0 vec ⁡ W
7 2 6 nvzcl ⊢ W ∈ NrmCVec → 0 vec ⁡ W ∈ Y
8 7 snssd ⊢ W ∈ NrmCVec → 0 vec ⁡ W ⊆ Y
9 fss ⊢ X × 0 vec ⁡ W : X ⟶ 0 vec ⁡ W ∧ 0 vec ⁡ W ⊆ Y → X × 0 vec ⁡ W : X ⟶ Y
10 5 8 9 sylancr ⊢ W ∈ NrmCVec → X × 0 vec ⁡ W : X ⟶ Y
11 10 adantl ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → X × 0 vec ⁡ W : X ⟶ Y
12 1 6 3 0ofval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z = X × 0 vec ⁡ W
13 12 feq1d ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z : X ⟶ Y ↔ X × 0 vec ⁡ W : X ⟶ Y
14 11 13 mpbird ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → Z : X ⟶ Y