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

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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
0oo.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
0oo.0 ⊢ 𝑍 = ( 𝑈 0op 𝑊 )
Assertion 0oo ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 : 𝑋 ⟶ 𝑌 )

Proof

Step Hyp Ref Expression
1 0oo.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 0oo.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 0oo.0 ⊢ 𝑍 = ( 𝑈 0op 𝑊 )
4 fvex ⊢ ( 0vec ‘ 𝑊 ) ∈ V
5 4 fconst ⊢ ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ { ( 0vec ‘ 𝑊 ) }
6 eqid ⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
7 2 6 nvzcl ⊢ ( 𝑊 ∈ NrmCVec → ( 0vec ‘ 𝑊 ) ∈ 𝑌 )
8 7 snssd ⊢ ( 𝑊 ∈ NrmCVec → { ( 0vec ‘ 𝑊 ) } ⊆ 𝑌 )
9 fss ⊢ ( ( ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ { ( 0vec ‘ 𝑊 ) } ∧ { ( 0vec ‘ 𝑊 ) } ⊆ 𝑌 ) → ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ 𝑌 )
10 5 8 9 sylancr ⊢ ( 𝑊 ∈ NrmCVec → ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ 𝑌 )
11 10 adantl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ 𝑌 )
12 1 6 3 0ofval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 = ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) )
13 12 feq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑍 : 𝑋 ⟶ 𝑌 ↔ ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) : 𝑋 ⟶ 𝑌 ) )
14 11 13 mpbird ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 : 𝑋 ⟶ 𝑌 )